[Prover] Upgrade the Boogie version from 3.0.9 to 3.2.4 (aptos-labs#1…

…4487) * temp * ci action
0xjunha · Sep 6, 2024 · d5f9496 · d5f9496
1 parent d5de09a
commit d5f9496
Show file tree

Hide file tree

Showing 61 changed files with 32,994 additions and 21,901 deletions.
diff --git a/.github/workflows/lint-test.yaml b/.github/workflows/lint-test.yaml
@@ -163,6 +163,24 @@ jobs:
         with:
           ref: ${{ github.event.pull_request.head.sha }}
           fetch-depth: 0 # Fetch all git history for accurate target determination
+
+      - name: Check if dev_setup.sh has changed
+        id: check_changes
+        run: |
+          git fetch origin ${{ github.event.pull_request.base.sha }}
+          if git diff --name-only ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -q 'scripts/dev_setup.sh'; then
+            echo "scripts/dev_setup.sh has changed"
+            echo "dev_setup_changed=true" >> $GITHUB_ENV
+          else
+            echo "scripts/dev_setup.sh has not changed"
+            echo "dev_setup_changed=false" >> $GITHUB_ENV
+          fi
+
+      - name: Run dev_setup.sh
+        if: env.dev_setup_changed == 'true'
+        run: |
+          scripts/dev_setup.sh -b -p -r -y -P -t
+
       - name: Run targeted rust unit tests
         uses: ./.github/actions/rust-targeted-unit-tests
         with:

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/scripts/dev_setup.sh b/scripts/dev_setup.sh
@@ -26,7 +26,7 @@ VAULT_VERSION=1.5.0
 Z3_VERSION=4.11.2
 CVC5_VERSION=0.0.3
 DOTNET_VERSION=6.0
-BOOGIE_VERSION=3.0.9
+BOOGIE_VERSION=3.2.4
 ALLURE_VERSION=2.15.pr1135
 # this is 3.21.4; the "3" is silent
 PROTOC_VERSION=21.4

diff --git a/third_party/move/move-prover/boogie-backend/src/options.rs b/third_party/move/move-prover/boogie-backend/src/options.rs
@@ -22,7 +22,7 @@ const DEFAULT_BOOGIE_FLAGS: &[&str] = &[
 /// but not always. Setting the max version allows Prover to warn users for the higher version of
 /// boogie and z3 because those may be incompatible.
 const MIN_BOOGIE_VERSION: Option<&str> = Some("3.0.1.0");
-const MAX_BOOGIE_VERSION: Option<&str> = Some("3.0.9.0");
+const MAX_BOOGIE_VERSION: Option<&str> = Some("3.2.4.0");
 
 const MIN_Z3_VERSION: Option<&str> = Some("4.11.2");
 const MAX_Z3_VERSION: Option<&str> = Some("4.11.2");

diff --git a/third_party/move/move-prover/lab/Cargo.toml b/third_party/move/move-prover/lab/Cargo.toml
@@ -7,8 +7,9 @@ edition = "2021"
 license = "Apache-2.0"
 
 [dependencies]
-# diem dependencies
+# Move dependencies
 move-compiler = { path = "../../move-compiler" }
+move-compiler-v2 = { path = "../../move-compiler-v2" }
 move-model = { path = "../../move-model" }
 move-prover = { path = ".." }
 move-prover-boogie-backend = { path = "../boogie-backend" }

diff --git a/third_party/move/move-prover/lab/data/aptos-framework/prover.toml b/third_party/move/move-prover/lab/data/aptos-framework/prover.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/current_boogie_1.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/current_boogie_1.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/current_boogie_2.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/current_boogie_2.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/current_boogie_3.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/current_boogie_3.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/new_boogie_1.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/new_boogie_1.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/new_boogie_2.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/new_boogie_2.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/new_boogie_3.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-framework/new_boogie_3.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",

diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-stdlib/current_boogie_1.fun_data b/third_party/move/move-prover/lab/data/new-boogie-aptos-stdlib/current_boogie_1.fun_data
diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-stdlib/current_boogie_1.mod_data b/third_party/move/move-prover/lab/data/new-boogie-aptos-stdlib/current_boogie_1.mod_data
@@ -1,35 +1,35 @@
 # config: current_boogie_1.toml
-# time  : 2023-12-29 10:47:37.902136 UTC
-0x1::bls12381_algebra                             416           ok
-0x1::bn254_algebra                                411           ok
-0x1::type_info                                    744           ok
-0x1::from_bcs                                     763           ok
-0x1::any                                          674           ok
-0x1::aptos_hash                                   718           ok
-0x1::table                                        639           ok
-0x1::table_with_length                            411           ok
-0x1::big_vector                                 52083           ok
-0x1::bls12381                                    1249           ok
-0x1::capability                                   872           ok
-0x1::comparator                                   788           ok
-0x1::copyable_any                                 673           ok
-0x1::crypto_algebra                              1259           ok
-0x1::string_utils                                 827           ok
-0x1::debug                                        644           ok
-0x1::ed25519                                      939           ok
-0x1::fixed_point64                               3364           ok
-0x1::math128                                      808           ok
-0x1::math64                                       777           ok
-0x1::math_fixed                                   842           ok
-0x1::math_fixed64                                 840           ok
-0x1::multi_ed25519                               1113           ok
-0x1::simple_map                                   420           ok
-0x1::pool_u64                                     410           ok
-0x1::pool_u64_unbound                            1335           ok
-0x1::ristretto255                                2006           ok
-0x1::ristretto255_pedersen                       1084           ok
-0x1::ristretto255_bulletproofs                    721           ok
-0x1::ristretto255_elgamal                        1204           ok
-0x1::secp256k1                                    752           ok
-0x1::smart_table                                  413           ok
-0x1::smart_vector                              194763           ok
+# time  : 2024-08-31 01:37:43.990021 UTC
+0x1::bls12381_algebra                            1249           ok
+0x1::bn254_algebra                               1251           ok
+0x1::type_info                                   2084           ok
+0x1::from_bcs                                    2130           ok
+0x1::any                                         2044           ok
+0x1::aptos_hash                                  2078           ok
+0x1::table                                       1948           ok
+0x1::table_with_length                           1250           ok
+0x1::big_vector                                 62071           ok
+0x1::bls12381                                    2706           ok
+0x1::capability                                  2370           ok
+0x1::comparator                                  2186           ok
+0x1::copyable_any                                2014           ok
+0x1::crypto_algebra                              2803           ok
+0x1::string_utils                                2218           ok
+0x1::debug                                       1979           ok
+0x1::ed25519                                     2356           ok
+0x1::fixed_point64                               5119           ok
+0x1::math128                                     2206           ok
+0x1::math64                                      2164           ok
+0x1::math_fixed                                  2290           ok
+0x1::math_fixed64                                2246           ok
+0x1::multi_ed25519                               2573           ok
+0x1::simple_map                                  1254           ok
+0x1::pool_u64                                    1279           ok
+0x1::pool_u64_unbound                            2932           ok
+0x1::ristretto255                                3809           ok
+0x1::ristretto255_pedersen                       2531           ok
+0x1::ristretto255_bulletproofs                   2061           ok
+0x1::ristretto255_elgamal                        2723           ok
+0x1::secp256k1                                   2138           ok
+0x1::smart_table                                 1257           ok
+0x1::smart_vector                               17807           ok
diff --git a/third_party/move/move-prover/lab/data/new-boogie-aptos-stdlib/current_boogie_1.toml b/third_party/move/move-prover/lab/data/new-boogie-aptos-stdlib/current_boogie_1.toml
@@ -6,6 +6,8 @@ move_named_address_values = [
     "core_resources=0xA550C18",
     "vm_reserved=0x0",
     "Extensions=0x1",
+    "vm=0x0",
+    "aptos_fungible_asset=0xA"
 ]
 move_deps = [
     "../../../../../../aptos-move/framework/move-stdlib/sources",