File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -166,7 +166,7 @@ public fun hi_spec(n: u128): u64 {
166166 ✅ Extracts the low 64 bits of a u128 value.
167167 ⏮️ The function does not abort.
168168*/
169- #[spec(prove, target = lo, boogie_opt=b"proverOpt:O:smt.QI.LAZY_THRESHOLD=100 proverOpt:O:smt.QI. EAGER_THRESHOLD=100 ")]
169+ #[spec(prove, target = lo, boogie_opt=b"proverOpt:O:smt.QI.EAGER_THRESHOLD=100 ")]
170170public fun lo_spec (n: u128 ): u64 {
171171 let n_int = n.to_int ();
172172 let result = lo (n);
@@ -205,7 +205,7 @@ public fun lo_u128_spec(n: u128): u128 {
205205 ✅ Constructs a u128 from low and high u64 components.
206206 ⏮️ The function does not abort.
207207*/
208- #[spec(prove, target = from_lo_hi, boogie_opt=b"proverOpt:O:smt.QI.LAZY_THRESHOLD=100 proverOpt:O:smt.QI. EAGER_THRESHOLD=100 ")]
208+ #[spec(prove, target = from_lo_hi, boogie_opt=b"proverOpt:O:smt.QI.EAGER_THRESHOLD=100 ")]
209209public fun from_lo_hi_spec (lo: u64 , hi: u64 ): u128 {
210210 let result = from_lo_hi (lo, hi);
211211 let expected_result = hi.to_int ().mul (1u64 .to_int ().shl (64u64 .to_int ())).add (lo.to_int ());
You can’t perform that action at this time.
0 commit comments