Skip to content

Core: Sequence bounds preconditions and VC-printer fallback fix #1100

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
fabiomadge wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Core: Sequence bounds preconditions and VC-printer fallback fix #1100

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9ed6582
fix(core): render unknown 0-ary ops as generic calls instead of re.none
fabiomadge May 2, 2026
4a73eb3
refactor(lambda): let polyUneval take optional preconditions
fabiomadge May 2, 2026
915164a
feat(core): add bounds preconditions to Sequence.select/update/take/drop
fabiomadge May 2, 2026
8325c0e
test(core): bounds obligations for Sequence.* and printer regression
fabiomadge May 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions Strata/DL/Imperative/CmdEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,11 +66,7 @@ def Cmd.eval [BEq P.Ident] [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P
let e := EC.eval σ e
let assumptions := EC.getPathConditions σ
let c' := .assert label e md
let propType := match md.getPropertyType with
| some s => if s == MetaData.divisionByZero then .divisionByZero
else if s == MetaData.arithmeticOverflow then .arithmeticOverflow
else .assert
| none => .assert
let propType := convertMetaDataPropertyType md
match EC.denoteBool e with
| some true => -- Proved via evaluation.
(c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
Expand Down
18 changes: 17 additions & 1 deletion Strata/DL/Imperative/EvalContext.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,12 +102,13 @@ inductive PropertyType where
| assert
| divisionByZero
| arithmeticOverflow
| outOfBoundsAccess
deriving Repr, DecidableEq

/-- Whether an unreachable path counts as pass for this property type.
Assertions pass vacuously when unreachable; covers fail. -/
def PropertyType.passWhenUnreachable : PropertyType → Bool
| .assert | .divisionByZero | .arithmeticOverflow => true
| .assert | .divisionByZero | .arithmeticOverflow | .outOfBoundsAccess => true
| .cover => false

instance : ToFormat PropertyType where
Expand All @@ -116,6 +117,21 @@ instance : ToFormat PropertyType where
| .assert => "assert"
| .divisionByZero => "division by zero check"
| .arithmeticOverflow => "arithmetic overflow check"
| .outOfBoundsAccess => "out-of-bounds access check"

/-- Convert a `MetaData` entry's property-type classification string to the
`PropertyType` enum. Falls back to `.assert` when the metadata carries
no classification or an unrecognized string; callers that emit
propertyType classifications should add a matching arm here. -/
def convertMetaDataPropertyType {P : PureExpr} [BEq P.Ident]
(md : MetaData P) : PropertyType :=
match md.getPropertyType with
| some s =>
if s == MetaData.divisionByZero then .divisionByZero
else if s == MetaData.arithmeticOverflow then .arithmeticOverflow
else if s == MetaData.outOfBoundsAccess then .outOfBoundsAccess
else .assert
| none => .assert
Comment on lines +122 to +134
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We now have three parallel representations of the same enum:

  1. MetaData.divisionByZero / arithmeticOverflow / outOfBoundsAccess — String constants (MetaData.lean:293–299).
  2. propertyTypeToClassification : PropertyType → String (SarifOutput.lean:92) — the display side, kebab-case.
  3. convertMetaDataPropertyType : MetaData → PropertyType — the decode side, using the constants from (1).

Adding a new PropertyType variant requires changes in all three places plus a new kebab/camel string pair, and forgetting (1)+(3) silently degrades to .assert at runtime — there's no compile-time check that (1) and (3) stay in sync.

One way to consolidate: a single definition that tabulates the serialization plus inverse:

/-- Canonical mapping from `PropertyType` to the pair of (metadata tag, SARIF classification) strings. -/
def PropertyType.serialization : PropertyType → Option (String × String)
  | .divisionByZero     => some ("divisionByZero",     "division-by-zero")
  | .arithmeticOverflow => some ("arithmeticOverflow", "arithmetic-overflow")
  | .outOfBoundsAccess  => some ("outOfBoundsAccess",  "out-of-bounds-access")
  | .cover              => some ("cover",              "cover")
  | .assert             => none

Then propertyTypeToClassification and convertMetaDataPropertyType both derive from this single source, and the MetaData.* constants can go. A #[simp] round-trip lemma (fromClassification? (toClassification p) = some p) gives compile-time coverage of the set. See the proof-coverage suggestion in the main review body.

Copy link
Copy Markdown
Contributor Author

@fabiomadge fabiomadge May 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed on the architectural observation. Deferring per your "not blocking" framing — a PropertyType.serialization table with the round-trip lemma you sketched is the right shape, but it touches pre-existing constants (MetaData.divisionByZero etc.) and the SARIF classifier, so a standalone cleanup PR is cleaner than folding it in here.

Comment on lines +122 to +134
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Per your "deferring to a follow-up PR" reply on the triple-representation thread — agreed on scope. One cheap intermediate measure worth adding here, before the full PropertyType.serialization consolidation lands, is a @[simp] roundtrip theorem. It doesn't change the code shape, but it gives you a compile-time error if someone adds a MetaData.* constant without a matching convertMetaDataPropertyType arm (or vice versa):

/-- Encoding `p` as a MetaData propertyType string and decoding it back
    yields `p` (for all non-`.assert` variants; `.assert` is the default). -/
@[simp]
theorem convertMetaDataPropertyType_roundTrip
    {P : PureExpr} [BEq P.Ident] (p : PropertyType) :
    p ≠ .assert →
    let md : MetaData P := MetaData.fromPair MetaData.propertyType
      (match p with
       | .divisionByZero     => MetaData.divisionByZero
       | .arithmeticOverflow => MetaData.arithmeticOverflow
       | .outOfBoundsAccess  => MetaData.outOfBoundsAccess
       | .cover              => "cover"    -- if .cover is ever tagged via MetaData
       | .assert             => "")
    convertMetaDataPropertyType md = p := by
  intro hne
  cases p <;> simp_all [convertMetaDataPropertyType, MetaData.getPropertyType, ...]
  -- the `.cover` case needs a MetaData string constant if you want it covered here,
  -- or split the theorem to non-`.cover`-and-non-`.assert` PropertyTypes.

(Exact simp set depends on how MetaData.fromPair / getPropertyType reduce; adjust from there. If .cover isn't meant to flow through MetaData, restrict the theorem's scope.)

When you do the full consolidation follow-up, this theorem becomes the inverse-of-forward lemma and is still useful. If a new PropertyType variant gets added without the corresponding MetaData.* + convertMetaDataPropertyType arm, cases p now produces an unhandled case and the proof stops compiling. That's the compile-time coverage the triple-representation is currently missing.

Copy link
Copy Markdown
Contributor Author

@fabiomadge fabiomadge May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Deferring. I prototyped the three variant round-trip theorems locally and they go through, but proving them requires adding @[expose] to about seven definitions in Strata/DL/Imperative/MetaData.lean (pushElem, findElem, propertyType, getPropertyType, Field.beq, and the three property-type string constants) plus convertMetaDataPropertyType itself in EvalContext.lean, because their bodies are otherwise opaque to simp/decide outside their defining file.

Exposing pre-existing MetaData internals is a public-API change that predates this PR's scope, and (as you note) the cleanest version is bundled with the full PropertyType.serialization consolidation. I'd rather do it once, cleanly, in the follow-up PR than slip the exposure in here.

Secondary note: the construction in your sketch uses MetaData.fromPair, which doesn't exist in the current codebase — the canonical form is MetaData.empty.pushElem MetaData.propertyType (.msg MetaData.divisionByZero). Mentioning in case it's useful when you come back to this.


/--
A proof obligation can be discharged by some backend solver or a dedicated
Expand Down
3 changes: 3 additions & 0 deletions Strata/DL/Imperative/MetaData.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -295,6 +295,9 @@ def MetaData.divisionByZero : String := "divisionByZero"
/-- Metadata value for arithmetic-overflow property type classification. -/
def MetaData.arithmeticOverflow : String := "arithmeticOverflow"

/-- Metadata value for out-of-bounds-access property type classification. -/
def MetaData.outOfBoundsAccess : String := "outOfBoundsAccess"

/-- Read the property type classification from metadata, if present. -/
def MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option String :=
match md.findElem MetaData.propertyType with
Expand Down
13 changes: 9 additions & 4 deletions Strata/DL/Lambda/IntBoolFactory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,22 +120,27 @@ instance (n : Nat) : LambdaLeanType (.bitvec n) (BitVec n) where

These build well-formed `WFLFunc`s that have no `concreteEval` or `body`. -/

/-- General polymorphic unevaluated function with optional axioms.
Handles any arity and any number of type arguments. -/
/-- General polymorphic unevaluated function with optional axioms and
preconditions. Handles any arity and any number of type arguments. -/
@[inline]
def polyUneval (n : T.Identifier) (typeArgs : List String)
(inputs : List (T.Identifier × LMonoTy)) (output : LMonoTy)
(axioms : List (LExpr T.mono) := [])
(preconditions :
List (FuncPrecondition (LExpr T.mono) T.Metadata) := [])
(h_nodup : List.Nodup (inputs.map (·.1.name)) := by first | decide | grind)
(h_ta_nodup : List.Nodup typeArgs := by grind)
(h_inputs : ∀ ty, ty ∈ ListMap.values inputs →
ty.freeVars ⊆ typeArgs := by first | decide | grind)
(h_output : output.freeVars ⊆ typeArgs
:= by first | decide | grind)
(h_precond : ∀ p, p ∈ preconditions →
(LExpr.freeVars p.expr).map (·.1.name) ⊆ inputs.map (·.1.name)
:= by first | decide | grind)
(h_ta_no_gen : ∀ ta, ta ∈ typeArgs → ¬ ("$__ty".toList.isPrefixOf ta.toList = true)
:= by first | decide | grind) : WFLFunc T :=
⟨{ name := n, typeArgs := typeArgs, inputs := inputs, output := output,
axioms := axioms }, {
axioms := axioms, preconditions := preconditions }, {
arg_nodup := h_nodup
body_freevars := by intro b hb; simp at hb
concreteEval_argmatch := by intro fn _ _ _ hfn; simp at hfn
Expand All @@ -144,7 +149,7 @@ def polyUneval (n : T.Identifier) (typeArgs : List String)
typeArgs_nodup := h_ta_nodup
inputs_typevars_in_typeArgs := h_inputs
output_typevars_in_typeArgs := h_output
precond_freevars := by intro p hp; simp at hp
precond_freevars := h_precond
typeArgs_no_gen_prefix := h_ta_no_gen
}⟩

Expand Down
8 changes: 4 additions & 4 deletions Strata/Languages/Core/DDMTransform/FormatCore.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -295,10 +295,10 @@ def handleZeroaryOps {M} [Inhabited M] (name : String)
| .re .All => pure (.re_all default)
| .re .AllChar => pure (.re_allchar default)
| .re .None => pure (.re_none default)
-- TODO: seq_empty is not yet parseable (see Grammar.lean); handle here when added.
| _ => do
ToCSTM.logError "lopToExpr" "0-ary op not found" name
pure (.re_none default)
-- TODO: `Sequence.empty` is not yet parseable (see Grammar.lean); when
-- grammar support lands, handle it with a dedicated case above.
-- Any other 0-ary op is rendered as a generic call.
| _ => mkGenericCall "handleZeroaryOps" name []

/-- Handle unary operations -/
def handleUnaryOps {M} [Inhabited M] (name : String) (arg : CoreDDM.Expr M)
Expand Down
57 changes: 53 additions & 4 deletions Strata/Languages/Core/Factory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -499,10 +499,53 @@ def seqAppendFunc : WFLFunc CoreLParams :=
else #true))]
])

/- A `Sequence` selection function with type `∀a. Sequence a → int → a`. -/
/-! ### Sequence bounds preconditions

`Sequence.select` / `update` / `take` / `drop` carry bounds
preconditions; the other `Sequence.*` ops are total. -/

/-- Choice of upper-bound operator in `mkSeqBoundsPrecond`: `Lt` (strict) for
`Sequence.select`/`update`, `Le` (non-strict) for `Sequence.take`/`drop`.
Restricting the parameter to this inductive rather than taking an
arbitrary `WFLFunc` or `LExpr` makes it impossible to attach a partial
operator (which would create a nested precondition obligation) by
accident. -/
private inductive SeqBoundKind where | Lt | Le

/-- Returns the *upper-bound* comparison for `mkSeqBoundsPrecond`.
The lower bound is always `0 ≤ x` (see `mkSeqBoundsPrecond`), so this
method characterises only the upper comparison. A future partial
Sequence op requiring a non-`int` comparison (e.g. a bitvector variant)
should introduce a separate helper rather than extend this enum. -/
private def SeqBoundKind.upperOpExpr : SeqBoundKind → LExpr CoreLParams.mono
| .Lt => (intLtFunc (T := CoreLParams)).opExpr
| .Le => (intLeFunc (T := CoreLParams)).opExpr
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor: SeqBoundKind.opExpr hard-codes intLtFunc / intLeFunc for the current two kinds. Fine for today. If a third partial-Sequence op ever needs a different comparison (e.g. a Nat-typed variant, or bitvector sequences), the inductive grows and so does this match. Worth a one-line comment tying the enum to "comparison operators over int" so a future bvLtFunc-flavoured kind is clearly a separate thing rather than another arm here.

Also a naming nit: SeqBoundKind.opExpr returns the upper-bound comparison; mkSeqBoundsPrecond uses k.opExpr only for the upper bound (the lower is hardcoded to intLeFunc). A name like SeqBoundKind.upperOpExpr reads more self-documenting:

Suggested change
| .Le => (intLeFunc (T := CoreLParams)).opExpr
private def SeqBoundKind.upperOpExpr : SeqBoundKind → LExpr CoreLParams.mono
| .Lt => (intLtFunc (T := CoreLParams)).opExpr
| .Le => (intLeFunc (T := CoreLParams)).opExpr

Copy link
Copy Markdown
Contributor Author

@fabiomadge fabiomadge May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done — renamed to upperOpExpr and added a scoping comment noting this is int-comparison-only and that a non-int variant (e.g. bitvector) should introduce a separate helper rather than extend this enum.


/-- Precondition `0 <= varName && varName `k.upperOpExpr` Sequence.length(s)`.

Assumes the enclosing function names its `Sequence a` input `"s"`.
Mismatches are caught at elaboration by `polyUneval`'s `h_precond`
free-vars check. -/
private def mkSeqBoundsPrecond
(varName : String) (k : SeqBoundKind) :
Strata.DL.Util.FuncPrecondition (LExpr CoreLParams.mono) CoreLParams.Metadata :=
let sVar : LExpr CoreLParams.mono := .fvar default "s" (some (seqTy mty[%a]))
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Implicit coupling: mkSeqBoundsPrecond hard-codes "s" here, which is only correct because the four callers (seqSelectFunc, seqUpdateFunc, seqTakeFunc, seqDropFunc) all happen to name their sequence input "s". The h_precond proof obligation on polyUneval catches mismatches at definition time — so this isn't a correctness trap, but the constraint isn't documented at the point where it bites.

Either take a second seqVarName parameter (symmetric with the existing varName for the index/count):

Suggested change
let sVar : LExpr CoreLParams.mono := .fvar default "s" (some (seqTy mty[%a]))
/-- Precondition `0 <= varName && varName `k.opExpr` Sequence.length(seqVarName)`. -/
private def mkSeqBoundsPrecond
(seqVarName : String) (varName : String) (k : SeqBoundKind) :
Strata.DL.Util.FuncPrecondition (LExpr CoreLParams.mono) CoreLParams.Metadata :=
let sVar : LExpr CoreLParams.mono := .fvar default seqVarName (some (seqTy mty[%a]))
let xVar : LExpr CoreLParams.mono := .fvar default varName (some mty[int])

and update the four call sites to mkSeqBoundsPrecond "s" "i" .Lt etc. — slightly more verbose at the call sites, but the helper's contract is now self-describing.

Or, if you prefer to keep the helper's signature narrow, add a one-line doc note: Assumes the enclosing function names its sequence input "s".

Copy link
Copy Markdown
Contributor Author

@fabiomadge fabiomadge May 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added a docstring note — the "s" hardcoding is a convention that mirrors yNeZeroPrecond's "y" in IntBoolFactory.lean, and polyUneval's h_precond free-vars check catches mismatches at elaboration time. Kept the signature narrow rather than adding a parameter, matching the existing pattern.

let xVar : LExpr CoreLParams.mono := .fvar default varName (some mty[int])
let zero : LExpr CoreLParams.mono := .intConst default 0
let lenS : LExpr CoreLParams.mono := .app default seqLengthFunc.opExpr sVar
let lower : LExpr CoreLParams.mono :=
.app default (.app default (intLeFunc (T := CoreLParams)).opExpr zero) xVar
let upper : LExpr CoreLParams.mono :=
.app default (.app default k.upperOpExpr xVar) lenS
⟨.app default (.app default (boolAndFunc (T := CoreLParams)).opExpr lower) upper,
default⟩
Comment on lines +529 to +541
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Proof coverage: a @[simp] free-vars theorem here, parallel to yNeZeroPrecond_freeVars at Strata/DL/Lambda/IntBoolFactory.lean:432, would both document the invariant and trivially discharge polyUneval's h_precond at every call site:

@[simp]
private theorem mkSeqBoundsPrecond_freeVars (varName : String) (k : SeqBoundKind) :
    ((mkSeqBoundsPrecond varName k).expr.freeVars).map (·.1.name) = ["s", varName] := by
  cases k <;>
  simp [mkSeqBoundsPrecond, LExpr.freeVars, SeqBoundKind.opExpr,
        LFunc.opExpr, intLeFunc, intLtFunc, boolAndFunc, seqLengthFunc]

(Exact simp lemmas will depend on how each helper is defined; the pattern in IntBoolFactory.lean:432 gives the template. If the .map (·.1.name) = ["s", varName] equality is too tight — e.g. ordering-dependent — a ⊆ variant is the weaker-but-still-useful form.)

With that in place, the "s" hardcoding noted in your docstring becomes a theorem, not a convention maintained by vigilance. And the h_precond in each of the four seqSelect/Update/Take/Drop call sites discharges via simp rather than relying on grind's opacity-sensitive behaviour.

Second, stronger theorem that I think is more valuable — see the inline on the test file — is a structural theorem mkSeqBoundsPrecond_form pinning the top-level AST to boolAnd (intLe 0 _) (k.opExpr _ _). That one catches the off-by-one regression I flagged last round at elaboration time. Sketch:

theorem mkSeqBoundsPrecond_form (varName : String) (k : SeqBoundKind) :
    ∃ lo up,
      (mkSeqBoundsPrecond varName k).expr =
        .app default (.app default (boolAndFunc (T := CoreLParams)).opExpr lo) up ∧
      -- lo is `0 ≤ x` with `intLeFunc` (independent of `k`)
      lo = .app default (.app default (intLeFunc (T := CoreLParams)).opExpr (.intConst default 0))
             (.fvar default varName (some mty[int])) ∧
      -- up is `x ≤/< length(s)` with `k.opExpr`
      up = .app default (.app default k.opExpr
               (.fvar default varName (some mty[int])))
             (.app default seqLengthFunc.opExpr (.fvar default "s" (some (seqTy mty[%a])))) := by
  cases k <;> exact ⟨_, _, rfl, rfl, rfl⟩

If rfl holds as written (I'd expect it to, the definition is entirely concrete), this theorem is essentially free and closes the Test 10 content-check gap structurally.

Copy link
Copy Markdown
Contributor Author

@fabiomadge fabiomadge May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Landed mkSeqBoundsPrecond_form per your sketch — cases k <;> rfl closes it. One subtlety: the up clause needs to pin the upper-bound op per-kind rather than abstract it as k.upperOpExpr, otherwise any change to the mapping inside upperOpExpr satisfies rfl trivially (both sides reduce through the same function). Verified locally that swapping intLtFunc → intLeFunc in upperOpExpr now breaks this proof.

Deferring mkSeqBoundsPrecond_freeVars_subset to a follow-up: I landed it locally and confirmed the ⊆ [varName, "s"] form works (with rw [mkSeqBoundsPrecond_form] then cases k <;> simp [LExpr.freeVars, WFLFunc.opExpr, LFunc.opExpr, List.subset_def]). But I also probed stripping the @[simp] tag — the existing polyUneval default first | decide | grind was already closing h_precond at all four call sites, so the tag provides no observable benefit in this PR. Happy to land it separately if you want the theorem purely for documentation value.

Independently, mkSeqBoundsPrecond_form does not catch the call-site regression (.Lt → .Le at a preconditions := [mkSeqBoundsPrecond "i" _]): the theorem is universally quantified over k, so a specific k at the call site is not pinned. That class is covered by the pretty-print snapshots on the test-file thread (see reply there).

Copy link
Copy Markdown
Contributor Author

@fabiomadge fabiomadge May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Follow-up: after pushback from @joscoh here, I've dropped mkSeqBoundsPrecond_form. His argument is that the theorem reduces to restating the definition — writing code twice — and enforcing that a function is definitionally equal to its own unfolding.

I probed whether the theorem catches anything unique vs the per-op pretty-print snapshots (Test 10a) and confirmed it doesn't:

  • upperOpExpr .Lt => .Le drift → all 4 snapshots fire.
  • Swapping lower/upper inside mkSeqBoundsPrecond's body → all 4 snapshots fire.
  • Callsite .Lt → .Le → snapshot for that callsite fires (which the theorem never caught anyway, since it's quantified over k).

The theorem was only buying earlier detection at the feat-commit boundary, not unique coverage. Dropped to avoid the redundancy.

Keeping the upperOpExpr rename + scoping docstring (those are independent wins) and the snapshot tests (those do the coverage work).


/- A `Sequence` selection function with type `∀a. Sequence a → int → a`.
Partial: requires `0 <= i && i < Sequence.length(s)`. -/
def seqSelectFunc : WFLFunc CoreLParams :=
polyUneval "Sequence.select" ["a"]
[("s", seqTy mty[%a]), ("i", mty[int])] mty[%a]
(preconditions := [mkSeqBoundsPrecond "i" .Lt])

/- A `Sequence` build (snoc) function with type `∀a. Sequence a → a → Sequence a`.
`build(s, v)` appends a single element `v` to the end of `s`. -/
Expand Down Expand Up @@ -555,7 +598,8 @@ def seqBuildFunc : WFLFunc CoreLParams :=
])

/- A `Sequence` update function with type `∀a. Sequence a → int → a → Sequence a`.
`update(s, i, v)` returns a sequence identical to `s` except at index `i` where the value is `v`. -/
`update(s, i, v)` returns a sequence identical to `s` except at index `i` where the value is `v`.
Partial: requires `0 <= i && i < Sequence.length(s)`. -/
def seqUpdateFunc : WFLFunc CoreLParams :=
polyUneval "Sequence.update" ["a"]
[("s", seqTy mty[%a]), ("i", mty[int]), ("v", mty[%a])]
Expand Down Expand Up @@ -606,6 +650,7 @@ def seqUpdateFunc : WFLFunc CoreLParams :=
(((~Sequence.select : (Sequence %a) → int → %a) %3) %0)
else #true)))]
])
(preconditions := [mkSeqBoundsPrecond "i" .Lt])

/- A `Sequence` contains function with type `∀a. Sequence a → a → bool`.
`contains(s, v)` is true iff there exists an index `i` such that `select(s, i) == v`. -/
Expand All @@ -628,7 +673,8 @@ def seqContainsFunc : WFLFunc CoreLParams :=
])

/- A `Sequence` take function with type `∀a. Sequence a → int → Sequence a`.
`take(s, n)` returns the first `n` elements of `s`. -/
`take(s, n)` returns the first `n` elements of `s`.
Partial: requires `0 <= n && n <= Sequence.length(s)`. -/
def seqTakeFunc : WFLFunc CoreLParams :=
polyUneval "Sequence.take" ["a"]
[("s", seqTy mty[%a]), ("n", mty[int])]
Expand Down Expand Up @@ -664,9 +710,11 @@ def seqTakeFunc : WFLFunc CoreLParams :=
(((~Sequence.select : (Sequence %a) → int → %a) %2) %0)
else #true))]
])
(preconditions := [mkSeqBoundsPrecond "n" .Le])

/- A `Sequence` drop function with type `∀a. Sequence a → int → Sequence a`.
`drop(s, n)` returns the sequence with the first `n` elements removed. -/
`drop(s, n)` returns the sequence with the first `n` elements removed.
Partial: requires `0 <= n && n <= Sequence.length(s)`. -/
def seqDropFunc : WFLFunc CoreLParams :=
polyUneval "Sequence.drop" ["a"]
[("s", seqTy mty[%a]), ("n", mty[int])]
Expand Down Expand Up @@ -709,6 +757,7 @@ def seqDropFunc : WFLFunc CoreLParams :=
(((~Int.Add : int → int → int) %0) %1))
else #true))]
])
(preconditions := [mkSeqBoundsPrecond "n" .Le])

def emptyTriggersFunc : WFLFunc CoreLParams :=
nullaryUneval "Triggers.empty" mty[Triggers]
Expand Down
6 changes: 1 addition & 5 deletions Strata/Languages/Core/ObligationExtraction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,7 @@ def extractGo (pc : PathConditions Expression) : Statements →
| s :: rest, acc =>
match s with
| .cmd (.cmd (.assert label e md)) =>
let propType := match md.getPropertyType with
| some s => if s == MetaData.divisionByZero then .divisionByZero
else if s == MetaData.arithmeticOverflow then .arithmeticOverflow
else .assert
| none => .assert
let propType := convertMetaDataPropertyType md
extractGo pc rest (acc.push (ProofObligation.mk label propType pc e md))

| .cmd (.cmd (.cover label e md)) =>
Expand Down
10 changes: 7 additions & 3 deletions Strata/Languages/Core/SarifOutput.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,8 @@ def outcomeToLevel (mode : VerificationMode) (property : Imperative.PropertyType
match mode, property, outcome.satisfiabilityProperty, outcome.validityProperty with
-- Cover satisfied (sat on P∧Q): always pass
| _, .cover, .sat _, _ => .none
-- Unreachable (both unsat): deductive=warning for assert/divisionByZero/arithmeticOverflow, error for cover and bugFinding modes
-- Unreachable (both unsat): deductive=warning for assert-like properties
-- (those that pass vacuously), error for cover and bugFinding modes.
| .deductive, p, .unsat, .unsat => if p.passWhenUnreachable then .warning else .error
| _, _, .unsat, .unsat => .error
-- Pass: validity proven (unsat on P∧¬Q)
Expand Down Expand Up @@ -91,6 +92,7 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
def propertyTypeToClassification : Imperative.PropertyType → String
| .divisionByZero => "division-by-zero"
| .arithmeticOverflow => "arithmetic-overflow"
| .outOfBoundsAccess => "out-of-bounds-access"
| .cover => "cover"
| .assert => "assert"

Expand All @@ -114,6 +116,8 @@ def extractRelatedLocations (files : Map Strata.Uri Lean.FileMap) (md : Imperati
def vcResultToSarifResult (mode : VerificationMode) (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult) : Strata.Sarif.Result :=
let ruleId := vcr.obligation.label
let relatedLocations := extractRelatedLocations files vcr.obligation.metadata
let properties : Strata.Sarif.PropertyBag :=
{ propertyType := propertyTypeToClassification vcr.obligation.property }
match vcr.outcome with
| .error err =>
let level := .error
Expand All @@ -122,15 +126,15 @@ def vcResultToSarifResult (mode : VerificationMode) (files : Map Strata.Uri Lean
let locations := match extractLocation files vcr.obligation.metadata with
| some loc => #[locationToSarif loc]
| none => #[]
{ ruleId, level, message, locations, relatedLocations }
{ ruleId, level, message, locations, relatedLocations, properties }
| .ok outcome =>
let level := outcomeToLevel mode vcr.obligation.property outcome
let messageText := outcomeToMessage outcome
let message : Strata.Sarif.Message := { text := messageText }
let locations := match extractLocation files vcr.obligation.metadata with
| some loc => #[locationToSarif loc]
| none => #[]
{ ruleId, level, message, locations, relatedLocations }
{ ruleId, level, message, locations, relatedLocations, properties }

/-- Convert VCResults to a SARIF document -/
def vcResultsToSarif (mode : VerificationMode) (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
Expand Down
6 changes: 1 addition & 5 deletions Strata/Languages/Core/StatementEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -320,11 +320,7 @@ private def createUnreachableAssertObligations
Imperative.ProofObligations Expression :=
asserts.toArray.map
(fun (label, md) =>
let propType := match md.getPropertyType with
| some s => if s == Imperative.MetaData.divisionByZero then .divisionByZero
else if s == Imperative.MetaData.arithmeticOverflow then .arithmeticOverflow
else .assert
| _ => .assert
let propType := Imperative.convertMetaDataPropertyType md
(Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md))

/--
Expand Down
2 changes: 1 addition & 1 deletion Strata/Languages/Core/Verifier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ def label (o : VCOutcome) (property : Imperative.PropertyType)
-- Simplified labels for minimal check level
else if checkLevel == .minimal then
if property.passWhenUnreachable then
-- Assert-like property (assert, divisionByZero, arithmeticOverflow)
-- Assert-like property (i.e. passes vacuously on unreachable paths).
if checkMode == .deductive then
match o.validityProperty with
| .unsat => "pass"
Expand Down
2 changes: 2 additions & 0 deletions Strata/Transform/PrecondElim.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,8 @@ private def classifyPrecondition (funcName : String) (precondIdx : Nat := 0) : O
| .bv ⟨_, .SafeAdd⟩ | .bv ⟨_, .SafeSub⟩ | .bv ⟨_, .SafeMul⟩ | .bv ⟨_, .SafeNeg⟩
| .bv ⟨_, .SafeUAdd⟩ | .bv ⟨_, .SafeUSub⟩ | .bv ⟨_, .SafeUMul⟩ | .bv ⟨_, .SafeUNeg⟩ =>
some Imperative.MetaData.arithmeticOverflow
| .seq .Select | .seq .Update | .seq .Take | .seq .Drop =>
some Imperative.MetaData.outOfBoundsAccess
| _ => none

/--
Expand Down
4 changes: 2 additions & 2 deletions StrataTest/Languages/Core/Examples/Loops.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,10 +379,10 @@ before_loop$_15:
loop_entry$_1:
assert [inv$_12]: x >= 0;
assert [inv$_13]: x <= n;
assert [inv$_14]: n < re.none();
assert [inv$_14]: n < top;

-- Errors encountered during conversion:
Unsupported construct in lopToExpr: 0-ary op not found: top
Unsupported construct in handleZeroaryOps: unknown operation, rendering as generic call: top
Context: Global scope:
var loop_measure$_2 : int;
assume [assume_loop_measure$_2]: loop_measure$_2 == n - x;
Expand Down
Loading
Loading