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

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() -> top, error message format updated).

Author: fabiomadge

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;

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

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

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;