[ci] publish ubuntu bins for CI use

.github/workflows/formal.yaml

@@ -13,8 +13,6 @@ on:
   #     - 'release**'
   #     - 'main'
 
-env:
-
 jobs:
   formal:
     runs-on: ubuntu-latest

.github/workflows/publish.yaml

@@ -0,0 +1,82 @@
+name: publish bin
+on:
+  push:
+    tags:
+      - '[0-9]+.[0-9]+.[0-9]+'
+      - '[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+'
+    branches:
+      - 'ci'
+      - 'publish' # TODO: temp until this gets merged to main
+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/[email protected]
+        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

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

@@ -252,7 +252,8 @@ module ol_framework::sacred_cows {
   }
 
   // get the stored value
-  fun get_stored<T>(): u64 acquires SacredCow {
+  public fun get_stored<T>(): u64 acquires SacredCow {
+    if (!exists<SacredCow<T>>(@0x2)) return 0;
     let stored = borrow_global_mut<SacredCow<T>>(@0x2);
     stored.value
   }
@@ -263,4 +264,4 @@ module ol_framework::sacred_cows {
     assert_same(stored, SLOW_WALLET_EPOCH_DRIP);
     SLOW_WALLET_EPOCH_DRIP
   }
-}
+}

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

@@ -24,6 +24,10 @@ module ol_framework::slow_wallet {
   const EGENESIS_ERROR: u64 = 1;
 
 
+
+  /// Maximum possible aggregatable coin value.
+  const MAX_U64: u128 = 18446744073709551615;
+
     struct SlowWallet has key {
         unlocked: u64,
         transferred: u64,
@@ -104,14 +108,25 @@ module ol_framework::slow_wallet {
         }
     }
 
-    public fun slow_wallet_epoch_drip(vm: &signer, amount: u64) acquires SlowWallet, SlowWalletList{
+    public fun slow_wallet_epoch_drip(vm: &signer, amount: u64) acquires
+    SlowWallet, SlowWalletList{
+
       system_addresses::assert_ol(vm);
       let list = get_slow_list();
+      let len = vector::length<address>(&list);
+      if (len == 0) return;
       let i = 0;
-      while (i < vector::length<address>(&list)) {
+      while (i < len) {
         let addr = vector::borrow<address>(&list, i);
         let total = coin::balance<GasCoin>(*addr);
+        if (!exists<SlowWallet>(*addr)) continue; // NOTE: formal verifiction caught
+        // this, not sure how it's possible
+
         let state = borrow_global_mut<SlowWallet>(*addr);
+
+        // TODO implement this as a `spec`
+        if ((state.unlocked as u128) + (amount as u128) >= MAX_U64) continue;
+
         let next_unlock = state.unlocked + amount;
         state.unlocked = if (next_unlock > total) { total } else { next_unlock };
         i = i + 1;

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

@@ -4,8 +4,21 @@ spec ol_framework::slow_wallet {
         // pragma aborts_if_is_strict;
     }
 
+    // setting a slow wallet should abort only if there is no SlowWalletList
+    // present in the 0x1 address
     spec set_slow(sig: &signer) {
-        // use diem_framework::
         aborts_if !exists<SlowWalletList>(@ol_framework);
     }
+
+    // at epoch boundaries the slow wallet drip should never abort
+    // if genesis is initialized properly
+    spec on_new_epoch(vm: &signer) {
+        use ol_framework::sacred_cows::{SacredCow, SlowDrip};
+
+        aborts_if !system_addresses::signer_is_ol_root(vm);
+
+        aborts_if !exists<SacredCow<SlowDrip>>(@0x2);
+
+        aborts_if borrow_global<SacredCow<SlowDrip>>(@0x2).value != 100000;
+    }
 }

framework/libra-framework/sources/system_addresses.move

@@ -94,4 +94,9 @@ module diem_framework::system_addresses {
         assert!(is_ol_framework_address(addr) || is_reserved_address(addr) || is_core_resource_address(addr) || addr == @0x2,
         error::permission_denied(ENOT_OL_ROOT_ADDRESS))
     }
+
+    public fun signer_is_ol_root(sig: &signer): bool {
+      let addr = signer::address_of(sig);
+      is_ol_framework_address(addr) || is_reserved_address(addr) || is_core_resource_address(addr) || addr == @0x2
+    }
 }