[move] Update move-stdlib deps (#62)

Co-authored-by: 0o-de-lally <[email protected]>

.github/workflows/formal.yaml

@@ -0,0 +1,48 @@
+name: formal verification
+on:
+  push:
+    branches: ["ci*"]
+  #   tags:
+  #   - '[0-9]+.[0-9]+.[0-9]+'
+  #   - '[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+'
+  # pull_request:
+  #   types:
+  #     - opened
+  #     - synchronize
+  #   branches:
+  #     - 'release**'
+  #     - 'main'
+
+env:
+
+jobs:
+  formal:
+    runs-on: ubuntu-latest
+    steps:
+        # NOTE: for debugging CI this allow shell access to github runner. Will print out tmate.io terminal url
+      - name: Setup tmate session
+        uses: mxschmitt/action-tmate@v3
+        with:
+          detached: true
+        timeout-minutes: 15
+
+      - uses: actions/checkout@v3
+
+      # - name: setup env
+      #   uses: ./.github/actions/build_env
+
+      - name: install prover dependencies
+        run: >
+            cd .. &&
+            git clone https://github.com/0LNetworkCommunity/diem.git &&
+            cd diem &&
+            ./scripts/dev_setup.sh -ypb
+
+      - name: install diem (for move tests)
+        run: >
+          wget -O ${{github.workspace}}/diem https://github.com/0LNetworkCommunity/diem/releases/latest/download/diem &&
+          sudo chmod 755 ${{github.workspace}}/diem
+
+      - name: prove
+        run: diem move prove -f version
+        working-directory: ./framework/libra-framework

.gitignore

@@ -16,4 +16,7 @@ Cargo.lock
 
 sccache.log
 
-.idea
+.idea
+
+# formal verification files
+*.bpl

docs/core_devs/formal_verification.md

@@ -0,0 +1,98 @@
+# Move Formal Verification
+
+The Move language includes a syntax for annotating code with `spec`
+specifications which can be "formally verified". The syntax is purpose built for
+Move. The stack behind the verification is based on `boogie`.
+
+You will need to install many dependencies for the Move test tooling as well as
+boogie system libraries.
+
+## Quick Start
+
+1) get the libra cli with standard Move tools
+
+Compile the `libra` cli app, and have it in your executable PATH.
+```
+cargo b --profile cli -p libra
+cp target/cli/libra ~/.cargo/bin
+chmod +x ~/.cargo/bin/libra
+
+# check it runs
+libra -h
+# this is the subcommand for the formal verification
+libra move prove -h
+```
+
+2) Install the Boogie dependencies
+
+The most straightforward way is to use the `diem-platform` environment setup.
+The `dev_setup.sh` can be run with these options:
+
+> -y install or update Move Prover tools: z3, cvc5, dotnet, boogie
+
+> -b batch mode, no user interactions and minimal output
+
+> -p update ${HOME}/.profile
+
+```
+# clone diem
+git clone https://github.com/0LNetworkCommunity/diem.git
+cd diem
+
+# run the installer
+./scripts/dev_setup.sh -ypb
+
+# you may need to restart your shell, after env variables are set
+source ~/.profile
+```
+
+You should expect to see some changes in your bash profile
+```
+export DOTNET_ROOT="/Users/you/.dotnet"
+export Z3_EXE="/Users/you/bin/z3"
+export CVC5_EXE="/Users/you/bin/cvc5"
+export BOOGIE_EXE="/Users/you/.dotnet/tools/boogie"
+export SOLC_EXE="/Users/you/bin/solc"
+```
+
+3) check it all works
+you'll be running formal verification specs against `libra-framework` move
+source.
+
+So test it on something we know to work
+```
+cd framework/libra-framework
+
+# test the version.move module
+libra move prove -f version
+```
+
+If you get a response with `Success` you are ready to start.
+
+## Troubleshooting
+
+1) check then env vars were set up `echo $BOOGIE_EXE`
+2) check that all the system libraries were installed `ls $HOME/.dotnet/tools/boogie`
+
+# Goals
+
+Formal verification priority for Libra should mainly check that the network does
+not halt in operations conducted by the VM.
+
+1. epoch_boundary.move
+Should never halt on reconfigure()
+THough there are many downstream modules and functions from here, the largest
+ones being:
+
+    a. stake.move
+
+    b. proof_of_fee.move
+
+2. coin.move
+  a. Transactions by VM should not halt
+
+3. slow_wallet.move
+  a. no transactions should bypass the slow wallet tracker. If there is a slow
+  wallet struct, a trasaction should always alter it.
+  b. no account, not even the VM can withdraw above the unlocked limit.
+  c. the unlocked limit cannot be larger than the total.

framework/libra-framework/sources/modified_source/coin.move

@@ -243,10 +243,8 @@ module diem_framework::coin {
     #[view]
     /// Returns the balance of `owner` for provided `CoinType`.
     public fun balance<CoinType>(owner: address): u64 acquires CoinStore {
-        assert!(
-            is_account_registered<CoinType>(owner),
-            error::not_found(ECOIN_STORE_NOT_PUBLISHED),
-        );
+        // should not abort if the VM might call this
+        if (!is_account_registered<CoinType>(owner)) return 0;
         borrow_global<CoinStore<CoinType>>(owner).coin.value
     }
 

framework/libra-framework/sources/ol_sources/demo.spec.move

@@ -0,0 +1,46 @@
+spec ol_framework::demo {
+    spec module {
+        pragma verify = true;
+        pragma aborts_if_is_strict;
+    }
+
+//     spec set_version(account: &signer, major: u64) {
+//         use std::signer;
+//         use diem_framework::chain_status;
+//         use diem_framework::timestamp;
+//         use diem_framework::stake;
+//         use diem_framework::coin::CoinInfo;
+//         use diem_framework::gas_coin::GasCoin;
+//         use diem_framework::transaction_fee;
+//         // use diem_framework::staking_config;
+//         // Not verified when verify_duration_estimate > vc_timeout
+//         pragma verify_duration_estimate = 120; // TODO: set because of timeout (property proved).
+//         include transaction_fee::RequiresCollectedFeesPerValueLeqBlockDiemSupply;
+//         // include staking_config::StakingRewardsConfigRequirement;
+//         requires chain_status::is_operating();
+//         requires timestamp::spec_now_microseconds() >= reconfiguration::last_reconfiguration_time();
+//         requires exists<stake::ValidatorFees>(@diem_framework);
+//         requires exists<CoinInfo<GasCoin>>(@diem_framework);
+
+//         aborts_if !exists<SetVersionCapability>(signer::address_of(account));
+//         aborts_if !exists<Version>(@diem_framework);
+
+//         let old_major = global<Version>(@diem_framework).major;
+//         aborts_if !(old_major < major);
+//     }
+
+//     /// Abort if resource already exists in `@diem_framwork` when initializing.
+//     spec initialize(diem_framework: &signer, initial_version: u64) {
+//         use std::signer;
+
+//         aborts_if signer::address_of(diem_framework) != @diem_framework;
+//         aborts_if exists<Version>(@diem_framework);
+//         aborts_if exists<SetVersionCapability>(@diem_framework);
+//     }
+
+//     /// This module turns on `aborts_if_is_strict`, so need to add spec for test function `initialize_for_test`.
+//     spec initialize_for_test {
+//         // Don't verify test functions.
+//         pragma verify = false;
+//     }
+}

framework/libra-framework/sources/ol_sources/libra_coin.move

@@ -67,7 +67,7 @@ module 0x1::LibraCoin {
 
     // Public accessor for the value of a coin
     public fun value(coin: &LibraCoin): u64 {
-        value(coin)
+        coin.value
     }
 
     // Splits the given coin into two and returns them both

framework/libra-framework/sources/ol_sources/slow_wallet.spec.move

@@ -0,0 +1,11 @@
+spec ol_framework::slow_wallet {
+    spec module {
+        pragma verify = true;
+        // pragma aborts_if_is_strict;
+    }
+
+    spec set_slow(sig: &signer) {
+        // use diem_framework::
+        aborts_if !exists<SlowWalletList>(@ol_framework);
+    }
+}

framework/move-stdlib/sources/bcs.move

@@ -1,6 +1,6 @@
 /// Utility for converting a Move value to its binary representation in BCS (Binary Canonical
 /// Serialization). BCS is the binary encoding for Move resources and other non-module values
-/// published on-chain. See https://github.com/diem-labs/bcs#binary-canonical-serialization-bcs for more
+/// published on-chain. See https://github.com/aptos-labs/bcs#binary-canonical-serialization-bcs for more
 /// details on BCS.
 module std::bcs {
     /// Return the binary representation of `v` in BCS (Binary Canonical Serialization) format

framework/move-stdlib/sources/bit_vector.move

@@ -85,13 +85,9 @@ module std::bit_vector {
     /// bitvector's length the bitvector will be zeroed out.
     public fun shift_left(bitvector: &mut BitVector, amount: u64) {
         if (amount >= bitvector.length) {
-           let len = vector::length(&bitvector.bit_field);
-           let i = 0;
-           while (i < len) {
-               let elem = vector::borrow_mut(&mut bitvector.bit_field, i);
-               *elem = false;
-               i = i + 1;
-           };
+            vector::for_each_mut(&mut bitvector.bit_field, |elem| {
+                *elem = false;
+            });
         } else {
             let i = amount;