feat: update boogie opt for some specs

Author: andrii-a8c

specs-bv/Move.lock

@@ -3,9 +3,22 @@
 [move]
 version = 3
 manifest_digest = "BC4FE2501E5714DD8780B061932D369DCC8BFB79C46BCADD3F0CD18558FFDD06"
-deps_digest = "F8BBB0CCB2491CA29A3DF03D6F92277A4F3574266507ACD77214D37ECA3F3082"
+deps_digest = "397E6A9F7A624706DBDFEE056CE88391A15876868FD18A88504DA74EB458D697"
 dependencies = [
+  { id = "DeepBook", name = "DeepBook" },
+  { id = "MoveStdlib", name = "MoveStdlib" },
+  { id = "Sui", name = "Sui" },
   { id = "SuiProver", name = "SuiProver" },
+  { id = "SuiSystem", name = "SuiSystem" },
+]
+
+[[move.package]]
+id = "DeepBook"
+source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/deepbook" }
+
+dependencies = [
+  { id = "MoveStdlib", name = "MoveStdlib" },
+  { id = "Sui", name = "Sui" },
 ]
 
 [[move.package]]
@@ -38,9 +51,18 @@ dependencies = [
 
 [[move.package]]
 id = "SuiSpecs"
-source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-framework-specs" }
+source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-specs" }
 
 dependencies = [
   { id = "Prover", name = "Prover" },
   { id = "Sui", name = "Sui" },
 ]
+
+[[move.package]]
+id = "SuiSystem"
+source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/sui-system" }
+
+dependencies = [
+  { id = "MoveStdlib", name = "MoveStdlib" },
+  { id = "Sui", name = "Sui" },
+]

specs/sources/i32_specs.move

@@ -209,7 +209,7 @@ public fun sub_spec(num1: I32, num2: I32): I32 {
  ✅ Computes `num1 * num2`.
  ⏮️ The function aborts when the result does not fit in `I32`.
 */
-#[spec(prove, target = mul, boogie_opt=b"proverOpt:O:smt.QI.EAGER_THRESHOLD=100")]
+#[spec(prove, target = mul, boogie_opt=b"vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:300")]
 public fun mul_spec(num1: I32, num2: I32): I32 {
     let num1_int = num1.to_int();
     let num2_int = num2.to_int();
@@ -263,7 +263,7 @@ public fun abs_u32_spec(v: I32): u32 {
  ✅ Computes `v << shift`.
  ⏮️ The function aborts unless `shift < 32`.
 */
-#[spec(prove, target = shl)]
+#[spec(prove, target = shl, boogie_opt=b"vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:300")]
 public fun shl_spec(v: I32, shift: u8): I32 {
     asserts(shift < 32);
     let result = shl(v, shift);

specs/sources/i64_specs.move

@@ -208,7 +208,7 @@ public fun sub_spec(num1: I64, num2: I64): I64 {
  ✅ Computes `num1 * num2`.
  ⏮️ The function aborts when the result does not fit in `I64`.
 */
-#[spec(prove, target = mul)]
+#[spec(prove, target = mul, boogie_opt=b"vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:300")]
 public fun mul_spec(num1: I64, num2: I64): I64 {
     let num1_int = num1.to_int();
     let num2_int = num2.to_int();
@@ -262,7 +262,7 @@ public fun abs_u64_spec(v: I64): u64 {
  ✅ Computes `v << shift`.
  ⏮️ The function aborts unless `shift < 64`.
 */
-#[spec(prove, target = shl)]
+#[spec(prove, target = shl, boogie_opt=b"vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:600")]
 public fun shl_spec(v: I64, shift: u8): I64 {
     asserts(shift < 64);
     let result = shl(v, shift);