From 6a93a2a8228f9e3576003a5c23065d16c3b30f2c Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 11 Nov 2025 15:02:15 +0200 Subject: [PATCH 1/6] wip --- .../src/boogie_backend/options.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs index d3c99ceaa6..ce8cf8f9e9 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs @@ -17,7 +17,7 @@ const DEFAULT_BOOGIE_FLAGS: &[&str] = &[ "-printModel:1", "-enhancedErrorMessages:1", //"-monomorphize", - "-proverOpt:O:model_validate=true", + "-proverOpt:model_validate=true", "-infer:j", ]; @@ -254,7 +254,7 @@ impl BoogieOptions { } /// Extracts the key part of a boogie option (everything except the value). - /// For "-proverOpt:O:smt.QI.EAGER_THRESHOLD=100", returns "-proverOpt:O:smt.QI.EAGER_THRESHOLD" + /// For "-proverOpt:smt.QI.EAGER_THRESHOLD=100", returns "-proverOpt:smt.QI.EAGER_THRESHOLD" /// For "-vcsCores:4", returns "-vcsCores" fn get_option_key(option: &str) -> &str { if let Some(eq_pos) = option.find('=') { @@ -321,15 +321,15 @@ impl BoogieOptions { if self.use_array_theory { add(&["-useArrayAxioms"]); if matches!(self.vector_theory, VectorTheory::SmtArray) { - add(&["/proverOpt:O:smt.array.extensional=false"]) + add(&["/proverOpt:smt.array.extensional=false"]) } } else { add(&[&format!( - "-proverOpt:O:smt.QI.EAGER_THRESHOLD={}", + "-proverOpt:smt.QI.EAGER_THRESHOLD={}", self.eager_threshold )]); add(&[&format!( - "-proverOpt:O:smt.QI.LAZY_THRESHOLD={}", + "-proverOpt:smt.QI.LAZY_THRESHOLD={}", self.lazy_threshold )]); } @@ -348,15 +348,15 @@ impl BoogieOptions { )]); // TODO: see what we can make out of these flags. - //add(&["-proverOpt:O:smt.QI.PROFILE=true"]); - //add(&["-proverOpt:O:trace=true"]); + //add(&["-proverOpt:smt.QI.PROFILE=true"]); + //add(&["-proverOpt:trace=true"]); //add(&["-proverOpt:VERBOSITY=3"]); //add(&["-proverOpt:C:-st"]); if let Some(file) = &self.z3_trace_file { add(&[ - "-proverOpt:O:trace=true", - &format!("-proverOpt:O:trace_file_name={}", file), + "-proverOptZ:trace=true", + &format!("-proverOpt:trace_file_name={}", file), ]); } if self.generate_smt { From d9e7f9191a3ad8a08ac7b795cf95d5a56ee28ab6 Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 11 Nov 2025 15:09:12 +0200 Subject: [PATCH 2/6] wip --- .../src/boogie_backend/options.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs index ce8cf8f9e9..d3c99ceaa6 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs @@ -17,7 +17,7 @@ const DEFAULT_BOOGIE_FLAGS: &[&str] = &[ "-printModel:1", "-enhancedErrorMessages:1", //"-monomorphize", - "-proverOpt:model_validate=true", + "-proverOpt:O:model_validate=true", "-infer:j", ]; @@ -254,7 +254,7 @@ impl BoogieOptions { } /// Extracts the key part of a boogie option (everything except the value). - /// For "-proverOpt:smt.QI.EAGER_THRESHOLD=100", returns "-proverOpt:smt.QI.EAGER_THRESHOLD" + /// For "-proverOpt:O:smt.QI.EAGER_THRESHOLD=100", returns "-proverOpt:O:smt.QI.EAGER_THRESHOLD" /// For "-vcsCores:4", returns "-vcsCores" fn get_option_key(option: &str) -> &str { if let Some(eq_pos) = option.find('=') { @@ -321,15 +321,15 @@ impl BoogieOptions { if self.use_array_theory { add(&["-useArrayAxioms"]); if matches!(self.vector_theory, VectorTheory::SmtArray) { - add(&["/proverOpt:smt.array.extensional=false"]) + add(&["/proverOpt:O:smt.array.extensional=false"]) } } else { add(&[&format!( - "-proverOpt:smt.QI.EAGER_THRESHOLD={}", + "-proverOpt:O:smt.QI.EAGER_THRESHOLD={}", self.eager_threshold )]); add(&[&format!( - "-proverOpt:smt.QI.LAZY_THRESHOLD={}", + "-proverOpt:O:smt.QI.LAZY_THRESHOLD={}", self.lazy_threshold )]); } @@ -348,15 +348,15 @@ impl BoogieOptions { )]); // TODO: see what we can make out of these flags. - //add(&["-proverOpt:smt.QI.PROFILE=true"]); - //add(&["-proverOpt:trace=true"]); + //add(&["-proverOpt:O:smt.QI.PROFILE=true"]); + //add(&["-proverOpt:O:trace=true"]); //add(&["-proverOpt:VERBOSITY=3"]); //add(&["-proverOpt:C:-st"]); if let Some(file) = &self.z3_trace_file { add(&[ - "-proverOptZ:trace=true", - &format!("-proverOpt:trace_file_name={}", file), + "-proverOpt:O:trace=true", + &format!("-proverOpt:O:trace_file_name={}", file), ]); } if self.generate_smt { From e4a026ab6b5e14b93163575418acafa167c30a87 Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 11 Nov 2025 15:49:30 +0200 Subject: [PATCH 3/6] feat: cores change --- crates/move-prover-boogie-backend/src/boogie_backend/options.rs | 2 +- crates/move-prover-lean-backend/src/lean_backend/options.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs index d3c99ceaa6..1f8b245274 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs @@ -215,7 +215,7 @@ impl Default for BoogieOptions { serialize_bound: 0, vector_using_sequences: false, random_seed: 1, - proc_cores: 4, + proc_cores: 2, vc_timeout: 40, keep_artifacts: true, eager_threshold: 10, diff --git a/crates/move-prover-lean-backend/src/lean_backend/options.rs b/crates/move-prover-lean-backend/src/lean_backend/options.rs index 45cf31e43a..dc2d89891b 100644 --- a/crates/move-prover-lean-backend/src/lean_backend/options.rs +++ b/crates/move-prover-lean-backend/src/lean_backend/options.rs @@ -96,7 +96,7 @@ impl Default for LeanOptions { serialize_bound: 0, vector_using_sequences: false, random_seed: 1, - proc_cores: 4, + proc_cores: 2, vc_timeout: 40, keep_artifacts: true, eager_threshold: 100, From 8a2c21f55233b7a702e200d528cadbfb3dc760b8 Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 11 Nov 2025 19:02:53 +0200 Subject: [PATCH 4/6] added large container for integer mate --- .github/workflows/sui-prover.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/sui-prover.yml b/.github/workflows/sui-prover.yml index e37818e404..2a506c32a0 100644 --- a/.github/workflows/sui-prover.yml +++ b/.github/workflows/sui-prover.yml @@ -194,7 +194,7 @@ jobs: integer-mate-specs: needs: build-prover - runs-on: macos-latest + runs-on: macos-latest-large concurrency: group: integer-mate-specs-${{ github.head_ref || github.ref_name }} From d5279c400c0d777ba3fb924cc1a1fd7882c714d1 Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 11 Nov 2025 19:13:48 +0200 Subject: [PATCH 5/6] wip --- .github/workflows/sui-prover.yml | 2 +- crates/move-prover-boogie-backend/src/boogie_backend/options.rs | 2 +- crates/move-prover-lean-backend/src/lean_backend/options.rs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/sui-prover.yml b/.github/workflows/sui-prover.yml index 2a506c32a0..cd676ee8f0 100644 --- a/.github/workflows/sui-prover.yml +++ b/.github/workflows/sui-prover.yml @@ -194,7 +194,7 @@ jobs: integer-mate-specs: needs: build-prover - runs-on: macos-latest-large + runs-on: macos-latest-xlarge concurrency: group: integer-mate-specs-${{ github.head_ref || github.ref_name }} diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs index 1f8b245274..d3c99ceaa6 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs @@ -215,7 +215,7 @@ impl Default for BoogieOptions { serialize_bound: 0, vector_using_sequences: false, random_seed: 1, - proc_cores: 2, + proc_cores: 4, vc_timeout: 40, keep_artifacts: true, eager_threshold: 10, diff --git a/crates/move-prover-lean-backend/src/lean_backend/options.rs b/crates/move-prover-lean-backend/src/lean_backend/options.rs index dc2d89891b..45cf31e43a 100644 --- a/crates/move-prover-lean-backend/src/lean_backend/options.rs +++ b/crates/move-prover-lean-backend/src/lean_backend/options.rs @@ -96,7 +96,7 @@ impl Default for LeanOptions { serialize_bound: 0, vector_using_sequences: false, random_seed: 1, - proc_cores: 2, + proc_cores: 4, vc_timeout: 40, keep_artifacts: true, eager_threshold: 100, From 8014653ee9a62b1659a63b4d11e2089397b388f2 Mon Sep 17 00:00:00 2001 From: Andrii Date: Tue, 11 Nov 2025 19:48:58 +0200 Subject: [PATCH 6/6] wip: cloud execution --- .github/workflows/sui-prover.yml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/.github/workflows/sui-prover.yml b/.github/workflows/sui-prover.yml index 8ff636be67..d700fe70e7 100644 --- a/.github/workflows/sui-prover.yml +++ b/.github/workflows/sui-prover.yml @@ -110,6 +110,9 @@ jobs: - name: Setup run: | mkdir -p ~/.local/bin + + mkdir -p "$HOME/.asymptotic" + echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml" cp ~/prover-bundle/bin/sui-prover ~/.local/bin/ ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie @@ -130,13 +133,13 @@ jobs: git clone https://github.com/asymptotic-code/sui-kit.git sui-kit cd sui-kit/examples/amm - sui-prover --ci + sui-prover --ci --cloud cd ../showcase - sui-prover --ci + sui-prover --ci --cloud cd ../guide - sui-prover --ci + sui-prover --ci --cloud internal-tests: # check if prover needed @@ -194,7 +197,7 @@ jobs: integer-mate-specs: needs: build-prover - runs-on: macos-latest-xlarge + runs-on: macos-latest concurrency: group: integer-mate-specs-${{ github.head_ref || github.ref_name }} @@ -211,6 +214,9 @@ jobs: run: | mkdir -p ~/.local/bin + mkdir -p "$HOME/.asymptotic" + echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml" + cp ~/prover-bundle/bin/sui-prover ~/.local/bin/ ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie @@ -229,10 +235,10 @@ jobs: git clone https://github.com/asymptotic-code/integer-library int-lib cd int-lib/specs - sui-prover --ci + sui-prover --ci --cloud cd ../specs-bv - sui-prover --no-bv-int-encoding --ci + sui-prover --no-bv-int-encoding --ci --cloud token-distribution-specs: needs: build-prover @@ -253,6 +259,9 @@ jobs: run: | mkdir -p ~/.local/bin + mkdir -p "$HOME/.asymptotic" + echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml" + cp ~/prover-bundle/bin/sui-prover ~/.local/bin/ ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie @@ -270,7 +279,7 @@ jobs: run: | git clone --depth 1 -b fix/prover_specs https://github.com/asymptotic-code/sui-smart-contracts.git sui-smart-contracts cd sui-smart-contracts/token-distribution-specs - sui-prover --ci + sui-prover --ci --cloud scallop-bpl-generation: needs: build-prover