Core: Sequence bounds preconditions

Strata/DL/Imperative/CmdEval.lean

@@ -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))

Strata/DL/Imperative/EvalContext.lean

@@ -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
@@ -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
 
 /--
 A proof obligation can be discharged by some backend solver or a dedicated

Strata/DL/Imperative/MetaData.lean

@@ -320,6 +320,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

Strata/DL/Lambda/IntBoolFactory.lean

@@ -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
@@ -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
   }⟩
 

Strata/Languages/Core/Factory.lean

@@ -499,10 +499,57 @@ 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
+
+/-- Precondition `0 <= varName && varName `k.upperOpExpr` Sequence.length(seqName)`.
+
+    `seqName` defaults to `"s"` since all four current call sites
+    (`Sequence.select`/`update`/`take`/`drop`) name their `Sequence a` input
+    that way. The parameter exists so a future partial Sequence op with a
+    different input name need only pass it explicitly rather than rely on a
+    hidden string literal. Either way, mismatches between the function's
+    declared inputs and the names used here are caught at elaboration by
+    `polyUneval`'s `h_precond` free-vars check. -/
+private def mkSeqBoundsPrecond
+    (varName : String) (k : SeqBoundKind) (seqName : String := "s") :
+    Strata.DL.Util.FuncPrecondition (LExpr CoreLParams.mono) CoreLParams.Metadata :=
+  let sVar  : LExpr CoreLParams.mono := .fvar default seqName (some (seqTy mty[%a]))
+  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⟩
+
+/- 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`. -/
@@ -555,7 +602,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])]
@@ -606,6 +654,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`. -/
@@ -628,7 +677,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])]
@@ -664,9 +714,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])]
@@ -709,6 +761,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]

Strata/Languages/Core/ObligationExtraction.lean

@@ -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)) =>

Strata/Languages/Core/SarifOutput.lean

@@ -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)
@@ -88,6 +89,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"
 
@@ -111,6 +113,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
@@ -119,15 +123,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 :=

Strata/Languages/Core/StatementEval.lean

@@ -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))
 
 /--

Strata/Languages/Core/Verifier.lean

@@ -786,7 +786,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"

Strata/Transform/PrecondElim.lean

@@ -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
 
 /--