diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 524062943..9707d3d83 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -385,6 +385,16 @@ private partial def toCoreQuantExpr? (e : Boole.Expr) : Option (TranslateM Core. some (toCoreQuant false ds body) | _ => none +/-- Lower a `Sequence.of_[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_[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 diff --git a/StrataTest/Languages/Boole/FeatureRequests/seq_empty_literal.lean b/StrataTest/Languages/Boole/FeatureRequests/seq_empty_literal.lean new file mode 100644 index 000000000..4a5c2cd0e --- /dev/null +++ b/StrataTest/Languages/Boole/FeatureRequests/seq_empty_literal.lean @@ -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_[]` literal lowering. + +`Sequence.empty_` literals carry their element type into Core (see the +`.seq_empty_*` arms in `Boole/Verify.lean`'s `toCoreExpr`). Sequence-literal +syntax `Sequence.of_[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 diff --git a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean index a8a818df4..222cea0d4 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean @@ -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,15 +333,15 @@ 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 @@ -349,15 +349,15 @@ 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,15 +373,15 @@ 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 @@ -389,15 +389,15 @@ 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