[move] essential formal verification tests on transfers (0LNetworkCom…

…munity#94)

Co-authored-by: Yotam Katznelson <mr.hemulin@gmail.com>

.github/workflows/ci.yaml

@@ -6,9 +6,6 @@ on:
       - "[0-9]+.[0-9]+.[0-9]+"
       - "[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+"
     branches: ["*"]
-      # - "release**"
-      # - "main"
-      # - "*ci*"
   pull_request:
     types:
       - opened

.github/workflows/cleanliness.yaml

@@ -1,10 +1,10 @@
 name: cleanliness
 on:
   push:
-    branches: ["*"]
     tags:
     - '[0-9]+.[0-9]+.[0-9]+'
     - '[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+'
+    branches: ["*"]
   pull_request:
     types:
       - opened

.github/workflows/formal.yaml

@@ -1,48 +1,50 @@
 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'
-
+    tags:
+      - '[0-9]+.[0-9]+.[0-9]+'
+      - '[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+'
+    branches: ["*"]
+  pull_request:
+    types:
+      - opened
+      - synchronize
+    branches:
+      - 'release**'
+      - 'main'
 env:
+  DOTNET_ROOT: "/home/runner/.dotnet"
+  Z3_EXE: "/home/runner/bin/z3"
+  CVC5_EXE: "/home/runner/bin/cvc5"
+  BOOGIE_EXE: "/home/runner/.dotnet/tools/boogie"
+  SOLC_EXE: "/home/runner/bin/solc"
 
 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
+      #   # 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
+        run: |
+            bash util/dev_setup.sh -byp
 
       - name: install diem (for move tests)
-        run: >
+        run: |
           wget -O ${{github.workspace}}/diem https://github.com/0LNetworkCommunity/diem/releases/latest/download/diem &&
-          sudo chmod 755 ${{github.workspace}}/diem
+          chmod +x ${{github.workspace}}/diem &&
+          cp ${{github.workspace}}/diem ~/.cargo/bin
 
-      - name: prove
-        run: diem move prove -f version
-        working-directory: ./framework/libra-framework
+      # Move framework tests
+      # TODO:
+      - name: prover tests
+        working-directory: ./framework
+        run: make prove

.github/workflows/move.yaml

@@ -5,8 +5,7 @@ on:
     tags:
       - '[0-9]+.[0-9]+.[0-9]+'
       - '[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+'
-    branches:
-      - '*'
+    branches: ['*']
   pull_request:
     types:
       - opened
@@ -31,7 +30,7 @@ jobs:
     - 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
+        chmod +x ${{github.workspace}}/diem
 
     # Move framework tests
     - name: move framework

.github/workflows/publish.yaml

@@ -0,0 +1,81 @@
+name: publish bin
+on:
+  push:
+    tags:
+      - '[0-9]+.[0-9]+.[0-9]+'
+      - '[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+'
+    branches:
+      - 'ci'
+jobs:
+  publish:
+    permissions: write-all
+      # contents: write
+    name: publish
+    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
+      - name: Free Disk Space (Ubuntu)
+        uses: jlumbroso/free-disk-space@main
+        with:
+          # this might remove tools that are actually needed,
+          # if set to "true" but frees about 6 GB
+          tool-cache: false
+
+          # all of these default to true, but feel free to set to
+          # "false" if necessary for your workflow
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: false
+          docker-images: true
+          swap-storage: true
+
+      - uses: dtolnay/rust-toolchain@1.70.0
+        with:
+          components: rustfmt
+
+######## CACHE ########
+      - name: system packages
+        uses: awalsh128/cache-apt-pkgs-action@latest
+        with:
+          packages: build-essential ca-certificates clang curl git libpq-dev libssl-dev pkg-config lsof lld libgmp-dev
+          version: 1.0
+
+      - name: checkout
+        uses: actions/checkout@v3
+
+      - name: sccache
+        uses: 0o-de-lally/sccache-action@local
+
+      # note: building in the same cargo command will lead to "feature unification", which leads to a `diem-node` binary which fails.
+      - name: libra release build
+      # size and performance optimized binary with profile.cli
+        run: cargo b --release -p libra
+
+      - name: libra publish
+        uses: svenstaro/upload-release-action@v2
+        with:
+          repo_token: ${{ secrets.GITHUB_TOKEN }}
+          file: target/release/libra
+          tag: ${{ github.ref }}
+          overwrite: true
+          file_glob: true
+
+      # TODO
+      # - name: libra-framework release build
+      # # size and performance optimized binary with profile.cli
+      #   run: cargo b --release -p libra-framework
+
+      # - name: CLI publish
+      #   uses: svenstaro/upload-release-action@v2
+      #   with:
+      #     repo_token: ${{ secrets.GITHUB_TOKEN }}
+      #     file: target/release/libra-framework
+      #     tag: ${{ github.ref }}
+      #     overwrite: true
+      #     file_glob: true

.pre-commit-config.yaml

@@ -6,7 +6,7 @@ repos:
         files: \.(rs|move)$
       - id: end-of-file-fixer
         files: \.(rs|move)$
-  -   repo: https://github.com/doublify/pre-commit-rust
-      rev: v1.0
-      hooks:
-      -   id: fmt
+  # -   repo: https://github.com/doublify/pre-commit-rust
+  #     rev: v1.0
+  #     hooks:
+  #     -   id: fmt