From 6a32a5951cec99a7316adf7ccb96acf72b645219 Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 21 May 2026 17:24:17 -0400 Subject: [PATCH] Fix Boole tests after merge --- Strata/Languages/Boole/Verify.lean | 8 +- Strata/Languages/Core/Factory.lean | 5 +- .../Boole/FeatureRequests/seq_slicing.lean | 6 +- .../sha256_compact_indexed.lean | 308 ++++++++++++++++-- 4 files changed, 293 insertions(+), 34 deletions(-) diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 927f39fc1..524062943 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -469,9 +469,11 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do let intSub : Core.Expression.Expr := .op () ⟨"Int.Sub", ()⟩ none return mkCoreApp Core.seqTakeOp [mkCoreApp Core.seqDropOp [s', lo'], mkCoreApp intSub [hi', lo']] - -- Typed empty-sequence constant (Sequence.empty for bv32; other types can be added when needed). - | .seq_empty_bv8 _ | .seq_empty_bv16 _ | .seq_empty_bv32 _ - | .seq_empty_bv64 _ | .seq_empty_int _ => return Core.seqEmptyOp + | .seq_empty_bv8 _ => return Core.seqEmptyOp (some (.bitvec 8)) + | .seq_empty_bv16 _ => return Core.seqEmptyOp (some (.bitvec 16)) + | .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⟩ diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean index 67002bf27..a5ea88df7 100644 --- a/Strata/Languages/Core/Factory.lean +++ b/Strata/Languages/Core/Factory.lean @@ -1050,7 +1050,10 @@ def mapConstOp : Expression.Expr := mapConstFunc.opExpr def mapSelectOp : Expression.Expr := mapSelectFunc.opExpr def mapUpdateOp : Expression.Expr := mapUpdateFunc.opExpr def seqLengthOp : Expression.Expr := seqLengthFunc.opExpr -def seqEmptyOp : Expression.Expr := seqEmptyFunc.opExpr +def seqEmptyOp (elemTy : Option LMonoTy := none) : Expression.Expr := + match elemTy with + | none => seqEmptyFunc.opExpr + | some ty => .op default "Sequence.empty" (some (seqTy ty)) def seqAppendOp : Expression.Expr := seqAppendFunc.opExpr def seqSelectOp : Expression.Expr := seqSelectFunc.opExpr def seqBuildOp : Expression.Expr := seqBuildFunc.opExpr diff --git a/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean b/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean index d4fcd12b8..c4b2a152f 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean @@ -183,7 +183,11 @@ spec { #end /-- info: -Obligation: seq_oob_seed_ensures_0_3481 +Obligation: set_v_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ❓ unknown + +Obligation: seq_oob_seed_ensures_0_4964 Property: assert Result: ❓ unknown-/ #guard_msgs in diff --git a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean index 47ded901b..a8a818df4 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean @@ -27,19 +27,21 @@ program Boole; type nat; function int_to_nat (i : int) : nat; type Set (T : Type); - function Seq_len (s : Sequence T) : nat { + function Seq_len (s : Sequence bv32) : nat { int_to_nat(Sequence.length(s)) } - function Seq_lib_insert (s : Sequence T, i : int, val : T) : Sequence T { + function Seq_lib_insert (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 -> T) : Sequence T; - function Seq_lib_map (s : Sequence T, f : int -> T -> U) : Sequence U; - function Seq_lib_map_values (s : Sequence T, f : T -> U) : Sequence U; - function Seq_lib_filter (s : Sequence T, p : T -> bool) : Sequence T; - function Seq_lib_sort_by (s : Sequence T, less : T -> T -> bool) : Sequence T; - function Seq_lib_to_set (s : Sequence T) : Set T; - function Set_finite (s : Set T) : bool; + 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 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)] @@ -55,11 +57,16 @@ spec { }; procedure to_u32s (block : Sequence bv8) returns (_pct_return : (Sequence bv32)) spec { + requires Sequence.length(block) >= 64; + ensures Sequence.length(_pct_return) == 16; } { var j : int; var res : (Sequence bv32); res := Sequence.of_bv32[bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0), bv{32}(0)]; - for i : int := 0 to 16 - 1{ + for i : int := 0 to 16 - 1 + invariant 0 <= i + invariant Sequence.length(res) == 16 + { j := i * 4; assert 0 <= 24 && 24 < 32; assert 0 <= 16 && 16 < 32; @@ -71,6 +78,8 @@ spec { }; procedure compress_u32 (state : Sequence bv32, block : Sequence bv32) returns (state_out : (Sequence bv32)) spec { + requires Sequence.length(state) >= 8 && Sequence.length(block) >= 16; + ensures Sequence.length(state_out) == Sequence.length(state); } { var tmp15 : bv32; var tmp16 : bv32; @@ -113,7 +122,11 @@ spec { f := Sequence.select(state_out, 5); g := Sequence.select(state_out, 6); h := Sequence.select(state_out, 7); - for i : int := 0 to 64 - 1{ + for i : int := 0 to 64 - 1 + invariant 0 <= i + invariant Sequence.length(block_local) >= 16 + invariant Sequence.length(state_out) >= 8 + { if (i < 16) { tmp36 := Sequence.select(block_local, i); } else { @@ -176,10 +189,15 @@ spec { }; procedure compress (state : Sequence bv32, blocks : Sequence (Sequence bv8)) returns (state_out : (Sequence bv32)) spec { + requires Sequence.length(state) >= 8; + requires ∀ k:int . 0 <= k && k < Sequence.length(blocks) ==> Sequence.length(Sequence.select(blocks, k)) >= 64; } { var tmp6 : (Sequence bv32); state_out := state; - for k : int := 0 to Sequence.length(blocks) - 1{ + for k : int := 0 to Sequence.length(blocks) - 1 + invariant 0 <= k + invariant Sequence.length(state_out) >= 8 + { call tmp6 := to_u32s(Sequence.select(blocks, k)); call state_out := compress_u32(state_out, tmp6); @@ -195,71 +213,303 @@ spec { #end /-- info: -Obligation: assert_1_3021 +Obligation: Seq_lib_insert_body_calls_Sequence.take_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: Seq_lib_insert_body_calls_Sequence.drop_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: assert_2_3107 +Property: assert +Result: ✅ pass + +Obligation: assert_3_3150 +Property: assert +Result: ✅ pass + +Obligation: entry_invariant_0_0 +Property: assert +Result: ✅ pass + +Obligation: entry_invariant_0_1 +Property: assert +Result: ✅ pass + +Obligation: assert_6_3830 +Property: assert +Result: ✅ pass + +Obligation: assert_7_3861 +Property: assert +Result: ✅ pass + +Obligation: assert_8_3892 +Property: assert +Result: ✅ pass + +Obligation: set_res_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_res_calls_Sequence.select_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_res_calls_Sequence.select_2 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_res_calls_Sequence.select_3 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_res_calls_Sequence.update_4 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: arbitrary_iter_maintain_invariant_0_0 +Property: assert +Result: ✅ pass + +Obligation: arbitrary_iter_maintain_invariant_0_1 +Property: assert +Result: ✅ pass + +Obligation: to_u32s_ensures_5_3422 +Property: assert +Result: ✅ pass + +Obligation: set_a_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_b_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_c_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_d_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_e_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_f_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_g_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_h_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: entry_invariant_0_0 +Property: assert +Result: ✅ pass + +Obligation: entry_invariant_0_1 +Property: assert +Result: ✅ pass + +Obligation: entry_invariant_0_2 +Property: assert +Result: ✅ pass + +Obligation: set_tmp36_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_w15_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: callElimAssert_rotate_right_requires_1_3056_39 Property: assert Result: ✅ pass -Obligation: assert_2_3064 +Obligation: callElimAssert_rotate_right_requires_1_3056_35 Property: assert Result: ✅ pass -Obligation: assert_3_3596 +Obligation: assert_12_5815 Property: assert Result: ✅ pass -Obligation: assert_4_3627 +Obligation: set_w2_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: callElimAssert_rotate_right_requires_1_3056_31 Property: assert Result: ✅ pass -Obligation: assert_5_3658 +Obligation: callElimAssert_rotate_right_requires_1_3056_27 +Property: assert +Result: ✅ pass + +Obligation: assert_13_6054 +Property: assert +Result: ✅ pass + +Obligation: set_new_w_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_new_w_calls_Sequence.select_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_block_local_calls_Sequence.update_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: callElimAssert_rotate_right_requires_1_3056_23 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_39 +Obligation: callElimAssert_rotate_right_requires_1_3056_19 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_35 +Obligation: callElimAssert_rotate_right_requires_1_3056_15 Property: assert Result: ✅ pass -Obligation: assert_7_5332 +Obligation: set_t1_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: callElimAssert_rotate_right_requires_1_3056_11 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_31 +Obligation: callElimAssert_rotate_right_requires_1_3056_7 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_27 +Obligation: callElimAssert_rotate_right_requires_1_3056_3 Property: assert Result: ✅ pass -Obligation: assert_8_5571 +Obligation: arbitrary_iter_maintain_invariant_0_0 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_23 +Obligation: arbitrary_iter_maintain_invariant_0_1 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_19 +Obligation: arbitrary_iter_maintain_invariant_0_2 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_15 +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: set_state_out_calls_Sequence.update_1 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: compress_u32_ensures_11_4416 +Property: assert +Result: ✅ pass + +Obligation: compress_pre_compress_requires_16_7819_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: entry_invariant_0_0 +Property: assert +Result: ✅ pass + +Obligation: entry_invariant_0_1 +Property: assert +Result: ✅ pass + +Obligation: init_calls_Sequence.select_0 +Property: out-of-bounds access check +Result: ✅ pass + +Obligation: callElimAssert_to_u32s_requires_4_3381_47 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_11 +Obligation: callElimAssert_compress_u32_requires_10_4344_43 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_7 +Obligation: arbitrary_iter_maintain_invariant_0_0 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_3 +Obligation: arbitrary_iter_maintain_invariant_0_1 Property: assert Result: ✅ pass-/ #guard_msgs in