slow wallet epoch boundary prover test passing

0LNetworkCommunity · Nov 9, 2023 · 84dcb0d · 84dcb0d
1 parent 45fa1a9
commit 84dcb0d
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 5 deletions.
diff --git a/framework/libra-framework/sources/ol_sources/sacred_cows.move b/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
   }
-}
+}
diff --git a/framework/libra-framework/sources/ol_sources/slow_wallet.move b/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;

diff --git a/framework/libra-framework/sources/ol_sources/slow_wallet.spec.move b/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;
+    }
 }
diff --git a/framework/libra-framework/sources/system_addresses.move b/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
+    }
 }