strata-org · PROgram52bc · May 22, 2026 · May 22, 2026
@@ -385,6 +385,16 @@ private partial def toCoreQuantExpr? (e : Boole.Expr) : Option (TranslateM Core.
       some (toCoreQuant false ds body)
   | _ => none
 
+/-- Lower a `Sequence.of_<ty>[v0, ..., vn]` literal to a left-fold of
+    `seq_build` over a typed `seq_empty`. The element type is required on
+    the seed so that empty literals retain their type and the
+    bounds-precondition pass does not emit polymorphic obligations. -/
+partial def seqLitToCore (elemTy : Lambda.LMonoTy) (vs : Array Boole.Expr)
+    : TranslateM Core.Expression.Expr := do
+  let vals ← vs.toList.mapM toCoreExpr
+  return vals.foldl (fun acc v => mkCoreApp Core.seqBuildOp [acc, v])
+                    (Core.seqEmptyOp (some elemTy))
+
 partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do
   if let some q := toCoreQuantExpr? e then
     return ← q
@@ -474,12 +484,16 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do
   | .seq_empty_bv32 _ => return Core.seqEmptyOp (some (.bitvec 32))
   | .seq_empty_bv64 _ => return Core.seqEmptyOp (some (.bitvec 64))
   | .seq_empty_int _  => return Core.seqEmptyOp (some .int)
-  -- Sequence literals: Sequence.of_bv32[v0, v1, ..., vn]
-  -- Lowers to a left-fold of seq_build over seq_empty.
-  | .seq_of_bv8  _ ⟨_, vs⟩ | .seq_of_bv16 _ ⟨_, vs⟩ | .seq_of_bv32 _ ⟨_, vs⟩
-  | .seq_of_bv64 _ ⟨_, vs⟩ | .seq_of_int  _ ⟨_, vs⟩ => do
-    let vals ← vs.toList.mapM toCoreExpr
-    return vals.foldl (fun acc v => mkCoreApp Core.seqBuildOp [acc, v]) Core.seqEmptyOp
+  -- Sequence literals: Sequence.of_<ty>[v0, v1, ..., vn]
+  -- Lowers to a left-fold of seq_build over a typed seq_empty seed. The
+  -- element type must be threaded onto the seed: for vs = [] it is the only
+  -- place the type lives, and the bounds-precondition pass otherwise emits
+  -- polymorphic obligations like `0 < Sequence.length (Sequence.empty)`.
+  | .seq_of_bv8  _ ⟨_, vs⟩ => seqLitToCore (.bitvec 8)  vs
+  | .seq_of_bv16 _ ⟨_, vs⟩ => seqLitToCore (.bitvec 16) vs
+  | .seq_of_bv32 _ ⟨_, vs⟩ => seqLitToCore (.bitvec 32) vs
+  | .seq_of_bv64 _ ⟨_, vs⟩ => seqLitToCore (.bitvec 64) vs
+  | .seq_of_int  _ ⟨_, vs⟩ => seqLitToCore .int         vs
   -- Lambda abstraction: `fun x : T => body`  →  Core .abs
   | .lambda _ _ decls body => do
       let declsList := declListToList decls

@@ -0,0 +1,130 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.MetaVerifier
+
+/-!
+Regression test for the empty `Sequence.of_<ty>[]` literal lowering.
+
+`Sequence.empty_<ty>` literals carry their element type into Core (see the
+`.seq_empty_*` arms in `Boole/Verify.lean`'s `toCoreExpr`). Sequence-literal
+syntax `Sequence.of_<ty>[v0, …, vn]` lowers to a left-fold of `seq_build` over
+`seq_empty`. For non-empty `vs` the surrounding `seq_build` calls constrain
+the element type, but for `vs = []` the seed `seq_empty` is the only place
+the type information lives — so the seed must carry it explicitly.
+
+Without that, the bounds-precondition pass produces polymorphic obligations
+like `0 < Sequence.length (Sequence.empty)` that lose track of the element
+type and break verification downstream.
+-/
+
+namespace Strata
+
+open Lambda
+
+/-- Walk a Core expression and yield the `ty` annotation of every
+    `Sequence.empty` op encountered. -/
+private partial def collectSeqEmptyTys
+    (e : Core.Expression.Expr) : List (Option LMonoTy) :=
+  match e with
+  | .op _ ⟨"Sequence.empty", _⟩ ty => [ty]
+  | .app _ f a => collectSeqEmptyTys f ++ collectSeqEmptyTys a
+  | .abs _ _ _ body => collectSeqEmptyTys body
+  | .quant _ _ _ _ trig body =>
+      collectSeqEmptyTys trig ++ collectSeqEmptyTys body
+  | .ite _ c t f =>
+      collectSeqEmptyTys c ++ collectSeqEmptyTys t ++ collectSeqEmptyTys f
+  | .eq _ a b => collectSeqEmptyTys a ++ collectSeqEmptyTys b
+  | _ => []
+
+/-- Render a `Sequence.empty` type annotation: a concrete element type
+    (the post-fix expectation), an unresolved type variable like
+    `Sequence(?a)` (the pre-fix bug — the seed is polymorphic and the
+    bounds-precondition pass produces polymorphic obligations from it),
+    or `untyped` if no annotation is present at all. -/
+private def fmtSeqEmptyTy : Option LMonoTy → String
+  | none => "untyped"
+  | some (.tcons "Sequence" [.bitvec n]) => s!"Sequence bv{n}"
+  | some (.tcons "Sequence" [.tcons name []]) => s!"Sequence {name}"
+  | some (.tcons "Sequence" [.ftvar v]) => s!"Sequence(?{v})"
+  | some ty => s!"other: {repr ty}"
+
+/-- Walk a Core statement (recursing into nested blocks/loops/ites) and
+    return every `Sequence.empty` element-type annotation found on the
+    right-hand side of `set` commands. -/
+private partial def collectFromStmt (s : Core.Statement) : List (Option LMonoTy) :=
+  match s with
+  | .set _ rhs _ => collectSeqEmptyTys rhs
+  | .block _ ss _ => ss.flatMap collectFromStmt
+  | .ite _ thenb elseb _ =>
+      thenb.flatMap collectFromStmt ++ elseb.flatMap collectFromStmt
+  | .loop _ _ _ body _ => body.flatMap collectFromStmt
+  | _ => []
+
+/-- Lower a Boole program to Core and return one string per `Sequence.empty`
+    op found in the body of every procedure. -/
+private def seqEmptyTysIn (p : Strata.Program) : Except String (List String) := do
+  let prog ← (Boole.getProgram p).mapError toString
+  let cp ← (Boole.toCoreProgram prog p.globalContext).mapError
+    fun e => toString (e.format none)
+  let mut out : List String := []
+  for d in cp.decls do
+    match d with
+    | .proc proc _ =>
+      for stmt in proc.body do
+        out := out ++ (collectFromStmt stmt).map fmtSeqEmptyTy
+    | _ => pure ()
+  return out
+
+/-! ## Empty literal: `Sequence.of_bv32[]` must lower to a typed `Sequence.empty`. -/
+
+private def emptyBv32LiteralPgm : Strata.Program :=
+#strata
+program Boole;
+
+procedure p() returns (s: (Sequence bv32))
+spec { }
+{
+  s := Sequence.of_bv32[];
+};
+#end
+
+/-- info: Except.ok ["Sequence bv32"] -/
+#guard_msgs in #eval seqEmptyTysIn emptyBv32LiteralPgm
+
+/-! ## Empty literal: `Sequence.of_int[]` must lower to a typed `Sequence.empty`. -/
+
+private def emptyIntLiteralPgm : Strata.Program :=
+#strata
+program Boole;
+
+procedure p() returns (s: (Sequence int))
+spec { }
+{
+  s := Sequence.of_int[];
+};
+#end
+
+/-- info: Except.ok ["Sequence int"] -/
+#guard_msgs in #eval seqEmptyTysIn emptyIntLiteralPgm
+
+/-! ## Non-empty literal: typing must still come through (sanity check). -/
+
+private def nonEmptyBv32LiteralPgm : Strata.Program :=
+#strata
+program Boole;
+
+procedure p() returns (s: (Sequence bv32))
+spec { }
+{
+  s := Sequence.of_bv32[bv{32}(0), bv{32}(1)];
+};
+#end
+
+/-- info: Except.ok ["Sequence bv32"] -/
+#guard_msgs in #eval seqEmptyTysIn nonEmptyBv32LiteralPgm
+
+end Strata
@@ -27,21 +27,21 @@ program Boole;
  type nat;
  function int_to_nat (i : int) : nat;
  type Set (T : Type);
- function Seq_len (s : Sequence bv32) : nat {
+ function Seq_len_bv32 (s : Sequence bv32) : nat {
   int_to_nat(Sequence.length(s))
 }
- function Seq_lib_insert (s : Sequence bv32, i : int, val : bv32) : Sequence bv32
+ function Seq_lib_insert_bv32 (s : Sequence bv32, i : int, val : bv32) : Sequence bv32
   requires 0 <= i && i <= Sequence.length(s);
  {
   Sequence.append(Sequence.build(Sequence.take(s, i), val), Sequence.drop(s, i))
 }
- function Seq_new (len : nat, f : int -> bv32) : Sequence bv32;
- function Seq_lib_map (s : Sequence bv32, f : int -> bv32 -> bv32) : Sequence bv32;
- function Seq_lib_map_values (s : Sequence bv32, f : bv32 -> bv32) : Sequence bv32;
- function Seq_lib_filter (s : Sequence bv32, p : bv32 -> bool) : Sequence bv32;
- function Seq_lib_sort_by (s : Sequence bv32, less : bv32 -> bv32 -> bool) : Sequence bv32;
- function Seq_lib_to_set (s : Sequence bv32) : Set bv32;
- function Set_finite (s : Set bv32) : bool;
+ function Seq_new_bv32 (len : nat, f : int -> bv32) : Sequence bv32;
+ function Seq_lib_map_bv32 (s : Sequence bv32, f : int -> bv32 -> bv32) : Sequence bv32;
+ function Seq_lib_map_values_bv32 (s : Sequence bv32, f : bv32 -> bv32) : Sequence bv32;
+ function Seq_lib_filter_bv32 (s : Sequence bv32, p : bv32 -> bool) : Sequence bv32;
+ function Seq_lib_sort_by_bv32 (s : Sequence bv32, less : bv32 -> bv32 -> bool) : Sequence bv32;
+ function Seq_lib_to_set_bv32 (s : Sequence bv32) : Set bv32;
+ function Set_finite_bv32 (s : Set bv32) : bool;
  function bv8_to_bv32_u (x : bv8) : bv32;
  function k32 () : Sequence bv32 {
   Sequence.of_bv32[bv{32}(1116352408), bv{32}(1899447441), bv{32}(3049323471), bv{32}(3921009573), bv{32}(961987163), bv{32}(1508970993), bv{32}(2453635748), bv{32}(2870763221), bv{32}(3624381080), bv{32}(310598401), bv{32}(607225278), bv{32}(1426881987), bv{32}(1925078388), bv{32}(2162078206), bv{32}(2614888103), bv{32}(3248222580), bv{32}(3835390401), bv{32}(4022224774), bv{32}(264347078), bv{32}(604807628), bv{32}(770255983), bv{32}(1249150122), bv{32}(1555081692), bv{32}(1996064986), bv{32}(2554220882), bv{32}(2821834349), bv{32}(2952996808), bv{32}(3210313671), bv{32}(3336571891), bv{32}(3584528711), bv{32}(113926993), bv{32}(338241895), bv{32}(666307205), bv{32}(773529912), bv{32}(1294757372), bv{32}(1396182291), bv{32}(1695183700), bv{32}(1986661051), bv{32}(2177026350), bv{32}(2456956037), bv{32}(2730485921), bv{32}(2820302411), bv{32}(3259730800), bv{32}(3345764771), bv{32}(3516065817), bv{32}(3600352804), bv{32}(4094571909), bv{32}(275423344), bv{32}(430227734), bv{32}(506948616), bv{32}(659060556), bv{32}(883997877), bv{32}(958139571), bv{32}(1322822218), bv{32}(1537002063), bv{32}(1747873779), bv{32}(1955562222), bv{32}(2024104815), bv{32}(2227730452), bv{32}(2361852424), bv{32}(2428436474), bv{32}(2756734187), bv{32}(3204031479), bv{32}(3329325298)]
@@ -213,19 +213,19 @@ spec {
 #end
 
 /-- info:
-Obligation: Seq_lib_insert_body_calls_Sequence.take_0
+Obligation: Seq_lib_insert_bv32_body_calls_Sequence.take_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: Seq_lib_insert_body_calls_Sequence.drop_1
+Obligation: Seq_lib_insert_bv32_body_calls_Sequence.drop_1
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: assert_2_3107
+Obligation: assert_2_3152
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_3_3150
+Obligation: assert_3_3195
 Property: assert
 Result: ✅ pass
 
@@ -237,15 +237,15 @@ Obligation: entry_invariant_0_1
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_6_3830
+Obligation: assert_6_3875
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_7_3861
+Obligation: assert_7_3906
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_8_3892
+Obligation: assert_8_3937
 Property: assert
 Result: ✅ pass
 
@@ -277,7 +277,7 @@ Obligation: arbitrary_iter_maintain_invariant_0_1
 Property: assert
 Result: ✅ pass
 
-Obligation: to_u32s_ensures_5_3422
+Obligation: to_u32s_ensures_5_3467
 Property: assert
 Result: ✅ pass
 
@@ -333,31 +333,31 @@ Obligation: set_w15_calls_Sequence.select_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_39
+Obligation: callElimAssert_rotate_right_requires_1_3101_39
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_35
+Obligation: callElimAssert_rotate_right_requires_1_3101_35
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_12_5815
+Obligation: assert_12_5860
 Property: assert
 Result: ✅ pass
 
 Obligation: set_w2_calls_Sequence.select_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_31
+Obligation: callElimAssert_rotate_right_requires_1_3101_31
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_27
+Obligation: callElimAssert_rotate_right_requires_1_3101_27
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_13_6054
+Obligation: assert_13_6099
 Property: assert
 Result: ✅ pass
 
@@ -373,31 +373,31 @@ Obligation: set_block_local_calls_Sequence.update_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_23
+Obligation: callElimAssert_rotate_right_requires_1_3101_23
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_19
+Obligation: callElimAssert_rotate_right_requires_1_3101_19
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_15
+Obligation: callElimAssert_rotate_right_requires_1_3101_15
 Property: assert
 Result: ✅ pass
 
 Obligation: set_t1_calls_Sequence.select_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_11
+Obligation: callElimAssert_rotate_right_requires_1_3101_11
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_7
+Obligation: callElimAssert_rotate_right_requires_1_3101_7
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_rotate_right_requires_1_3056_3
+Obligation: callElimAssert_rotate_right_requires_1_3101_3
 Property: assert
 Result: ✅ pass
 
@@ -477,11 +477,11 @@ Obligation: set_state_out_calls_Sequence.update_1
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: compress_u32_ensures_11_4416
+Obligation: compress_u32_ensures_11_4461
 Property: assert
 Result: ✅ pass
 
-Obligation: compress_pre_compress_requires_16_7819_calls_Sequence.select_0
+Obligation: compress_pre_compress_requires_16_7864_calls_Sequence.select_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
@@ -497,11 +497,11 @@ Obligation: init_calls_Sequence.select_0
 Property: out-of-bounds access check
 Result: ✅ pass
 
-Obligation: callElimAssert_to_u32s_requires_4_3381_47
+Obligation: callElimAssert_to_u32s_requires_4_3426_47
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_compress_u32_requires_10_4344_43
+Obligation: callElimAssert_compress_u32_requires_10_4389_43
 Property: assert
 Result: ✅ pass