test(core): bounds obligations for Sequence.* and printer regression

fabiomadge · fabiomadge · commit 2bf64c397b95 · 2026-05-07T00:02:40.000+02:00
New tests in StrataTest/Transform/PrecondElim.lean:
- Test 10:  Sequence.select in a procedure body emits the bounds assert
            (PrecondElim is unconditional — it inserts regardless of any
            surrounding requires guard; the SMT solver discharges).
- Test 10c: Sequence.select inside a requires clause triggers the
            $$wf-procedure path (mkContractWFProc).
- Test 10d: Sequence.select inside a function body triggers the
            function-body $$wf path (mkFuncWFStmts).
- Test 11:  collectPrecondAsserts attaches outOfBoundsAccess metadata
            for all four partial ops and a nested call. Mirrors
            OverflowCheckTest.lean. Also verifies Sequence.length emits
            no obligation (it is total).
- Test 12:  Sequence.empty printer regression for the commit-1 fix —
            renders as a generic call, not re.none().

New property-classification tests in
StrataTest/Languages/Core/Tests/SarifOutputTests.lean cover all five
PropertyType variants, exercising the SARIF wiring fix in commit 3.

Collateral test updates for real behavioral changes:
- StrataTest/Languages/Core/Examples/Seq.lean: expected VC output
  includes the new bounds obligations (all SMT-provable from the
  surrounding context, except the pre-existing contains_yes unknown).
- StrataTest/Languages/Core/Tests/ProgramEvalTests.lean: Sequence func
  signatures now render with the attached requires clauses.
- StrataTest/Languages/Core/Examples/Loops.lean: commit-1 printer fix
  propagates (re.none() -&gt; top, error message format updated).
diff --git a/StrataTest/Languages/Core/Examples/Loops.lean b/StrataTest/Languages/Core/Examples/Loops.lean
@@ -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;
diff --git a/StrataTest/Languages/Core/Examples/Seq.lean b/StrataTest/Languages/Core/Examples/Seq.lean
@@ -68,20 +68,41 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30)) == 3
 
+Label: assert_t_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: t_0
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 0) == 10
 
+Label: assert_t_1_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: t_1
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1) == 20
 
+Label: assert_t_2_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 2 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: t_2
 Property: assert
 Assumptions:
@@ -102,14 +123,26 @@ Obligation: t_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_t_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: t_0
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_t_1_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: t_1
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_t_2_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: t_2
 Property: assert
 Result: ✅ pass
@@ -185,34 +218,69 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50))) == 5
 
+Label: assert_append_elem_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)))
+
 Label: append_elem_0
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)), 0) == 10
 
+Label: assert_append_elem_4_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 4 < Sequence.length(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)))
+
 Label: append_elem_4
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)), 4) == 50
 
+Label: set_u_calls_Sequence.update_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: update_length
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99)) == 3
 
+Label: assert_update_same_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 < Sequence.length(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99))
+
 Label: update_same
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99), 1) == 99
 
+Label: assert_update_other_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99))
+
 Label: update_other
 Property: assert
 Assumptions:
@@ -227,27 +295,55 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.contains(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 20)
 
+Label: set_u_calls_Sequence.take_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 2 <= Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: take_length
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.take(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 2)) == 2
 
+Label: assert_take_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.take(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 2))
+
 Label: take_elem
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.take(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 2), 0) == 10
 
+Label: set_u_calls_Sequence.drop_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 <= Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: drop_length
 Property: assert
 Assumptions:
 s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.drop(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1)) == 2
 
+Label: assert_drop_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.drop(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1))
+
 Label: drop_elem
 Property: assert
 Assumptions:
@@ -261,22 +357,42 @@ Obligation: append_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_append_elem_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: append_elem_0
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_append_elem_4_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: append_elem_4
 Property: assert
 Result: ✅ pass
 
+Obligation: set_u_calls_Sequence.update_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: update_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_update_same_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: update_same
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_update_other_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: update_other
 Property: assert
 Result: ✅ pass
@@ -285,18 +401,34 @@ Obligation: contains_yes
 Property: assert
 Result: ❓ unknown
 
+Obligation: set_u_calls_Sequence.take_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: take_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_take_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: take_elem
 Property: assert
 Result: ✅ pass
 
+Obligation: set_u_calls_Sequence.drop_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: drop_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_drop_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: drop_elem
 Property: assert
 Result: ✅ pass
diff --git a/StrataTest/Languages/Core/Tests/GenericCallFallbackTest.lean b/StrataTest/Languages/Core/Tests/GenericCallFallbackTest.lean
@@ -114,6 +114,20 @@ info: "assert [q1]: fourArgFn(a, b, c, d);\n\n-- Errors encountered during conve
   let e := mkCall4 "fourArgFn" (mkFvar "a") (mkFvar "b") (mkFvar "c") (mkFvar "d")
   IO.println (repr (fmtStmt (mkAssert "q1" e) #["a", "b", "c", "d"]))
 
+-- -----------------------------------------------------------------------
+-- Test: unknown 0-ary operation renders as a generic call (e.g.
+-- `Sequence.empty`, which is registered in the factory but not yet
+-- parseable in raw Core source).
+-- -----------------------------------------------------------------------
+
+/--
+info: "assert [z1]: Sequence.empty;\n\n-- Errors encountered during conversion:\nUnsupported construct in handleZeroaryOps: unknown operation, rendering as generic call: Sequence.empty\nContext: Global scope:"
+-/
+#guard_msgs in
+#eval do
+  let e := mkOp "Sequence.empty"
+  IO.println (repr (fmtStmt (mkAssert "z1" e) #[]))
+
 -- -----------------------------------------------------------------------
 -- Test: known operations still render correctly (regression check)
 -- -----------------------------------------------------------------------
diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean
@@ -85,12 +85,16 @@ func update : ∀[k, v]. ((m : (Map k v)) (i : k) (x : v)) → (Map k v);
 func Sequence.length : ∀[a]. ((s : (Sequence a))) → int;
 func Sequence.empty : ∀[a]. () → (Sequence a);
 func Sequence.append : ∀[a]. ((s1 : (Sequence a)) (s2 : (Sequence a))) → (Sequence a);
-func Sequence.select : ∀[a]. ((s : (Sequence a)) (i : int)) → a;
+func Sequence.select : ∀[a]. ((s : (Sequence a)) (i : int)) → a
+  requires 0 <= i && i < Sequence.length(s);
 func Sequence.build : ∀[a]. ((s : (Sequence a)) (v : a)) → (Sequence a);
-func Sequence.update : ∀[a]. ((s : (Sequence a)) (i : int) (v : a)) → (Sequence a);
+func Sequence.update : ∀[a]. ((s : (Sequence a)) (i : int) (v : a)) → (Sequence a)
+  requires 0 <= i && i < Sequence.length(s);
 func Sequence.contains : ∀[a]. ((s : (Sequence a)) (v : a)) → bool;
-func Sequence.take : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a);
-func Sequence.drop : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a);
+func Sequence.take : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a)
+  requires 0 <= n && n <= Sequence.length(s);
+func Sequence.drop : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a)
+  requires 0 <= n && n <= Sequence.length(s);
 func Triggers.empty :  () → Triggers;
 func Triggers.addGroup :  ((g : TriggerGroup) (t : Triggers)) → Triggers;
 func TriggerGroup.empty :  () → TriggerGroup;
diff --git a/StrataTest/Transform/PrecondElim.lean b/StrataTest/Transform/PrecondElim.lean
@@ -418,4 +418,51 @@ procedure test (inout g : int, y : int)
 #guard_msgs in
 #eval (Std.format (transformProgram loopGuardPrecondPgm))
 
+/-! ### Test 10: `collectPrecondAsserts` tags Sequence bounds obligations with `outOfBoundsAccess`
+
+Exercises the full `collectPrecondAsserts` path — the code called by
+`transformStmt` / `mkContractWFProc` / `mkFuncWFProc` — and inspects the
+metadata on the generated assert. Mirrors `OverflowCheckTest.lean`. -/
+
+section SeqBoundsObligations
+
+open Strata Core Lambda Core.PrecondElim Imperative
+
+/-- Shared fvar fixtures so each per-op case below is a one-liner. -/
+private def fxS : Core.Expression.Expr := .fvar () ⟨"s", ()⟩ (some (Core.seqTy .int))
+private def fxI : Core.Expression.Expr := .fvar () ⟨"i", ()⟩ (some .int)
+private def fxV : Core.Expression.Expr := .fvar () ⟨"v", ()⟩ (some .int)
+private def fxN : Core.Expression.Expr := .fvar () ⟨"n", ()⟩ (some .int)
+private def fxJ : Core.Expression.Expr := .fvar () ⟨"j", ()⟩ (some .int)
+
+/-- Check that `collectPrecondAsserts` produces exactly `expectedCount`
+    obligations from `expr`, each tagged with `outOfBoundsAccess`. -/
+private def assertOutOfBoundsObligations
+    (expr : Core.Expression.Expr) (expectedCount : Nat) : IO Unit := do
+  let stmts := collectPrecondAsserts Core.Factory expr "test" #[]
+  assert! stmts.length == expectedCount
+  for s in stmts do
+    let md : MetaData Core.Expression := match s with
+      | Statement.assert _ _ md => md | _ => #[]
+    assert! md.getPropertyType == some MetaData.outOfBoundsAccess
+
+-- Sequence.select / update / take / drop each emit one out-of-bounds obligation.
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqSelectOp [fxS, fxI]) 1
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV]) 1
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqTakeOp   [fxS, fxN]) 1
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqDropOp   [fxS, fxN]) 1
+
+-- Nested: `Sequence.select(Sequence.update(s, i, v), j)` emits two
+-- obligations (one per partial call), both tagged `outOfBoundsAccess`.
+#eval assertOutOfBoundsObligations
+  (LExpr.mkApp () Core.seqSelectOp [LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV], fxJ]) 2
+
+-- Sequence.length is total: no precondition obligations generated.
+#eval do
+  let stmts := collectPrecondAsserts Core.Factory
+    (LExpr.mkApp () Core.seqLengthOp [fxS]) "test" #[]
+  assert! stmts.isEmpty
+
+end SeqBoundsObligations
+
 end PrecondElimTests
