assumptions

runtimeverification · Jun 22, 2024 · ddeba7e · ddeba7e
1 parent 615778d
commit ddeba7e
Show file tree

Hide file tree

Showing 4 changed files with 73 additions and 4 deletions.
diff --git a/contracts/model/DualGovernanceModel.sol b/contracts/model/DualGovernanceModel.sol
@@ -133,6 +133,13 @@ contract DualGovernanceModel {
     function linearInterpolation(uint256 rageQuitSupport) private pure returns (uint256) {
         uint256 L_min = DYNAMIC_TIMELOCK_MIN_DURATION;
         uint256 L_max = DYNAMIC_TIMELOCK_MAX_DURATION;
+        // Assumption: No underflow
+        require(FIRST_SEAL_RAGE_QUIT_SUPPORT <= rageQuitSupport);
+        // Assumption: No overflow
+        require(
+            ((rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) * (L_max - L_min)) / (L_max - L_min)
+                == (rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT)
+        );
         return L_min
             + ((rageQuitSupport - FIRST_SEAL_RAGE_QUIT_SUPPORT) * (L_max - L_min))
                 / (SECOND_SEAL_RAGE_QUIT_SUPPORT - FIRST_SEAL_RAGE_QUIT_SUPPORT);
@@ -181,6 +188,11 @@ contract DualGovernanceModel {
     // State Transitions
 
     function activateNextState() public {
+        // Assumption: various time stamps are in the past
+        require(lastStateChangeTime <= block.timestamp);
+        require(lastSubStateActivationTime <= block.timestamp);
+        require(lastStateReactivationTime <= block.timestamp);
+
         uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport();
 
         State previousState;

diff --git a/contracts/model/EscrowModel.sol b/contracts/model/EscrowModel.sol
@@ -31,18 +31,18 @@ contract EscrowModel {
     StETHModel public stEth;
     mapping(address => uint256) public shares;
     uint256 public totalSharesLocked;
-    uint256 public totalWithdrawalRequestAmount;
     uint256 public totalClaimedEthAmount;
+    uint256 public totalWithdrawalRequestAmount;
+    uint256 public withdrawalRequestCount;
+    bool public lastWithdrawalRequestSubmitted; // Flag indicating the last withdrawal request submitted
+    uint256 public claimedWithdrawalRequests;
     uint256 public totalWithdrawnPostRageQuit;
     mapping(address => uint256) public lastLockedTimes; // Track the last time tokens were locked by each user
-    uint256 public withdrawalRequestCount;
     mapping(uint256 => WithdrawalRequestStatus) public withdrawalRequestStatus;
     mapping(uint256 => uint256) public withdrawalRequestAmount;
     uint256 public rageQuitExtensionDelayPeriodEnd;
     uint256 public rageQuitSequenceNumber;
     uint256 public rageQuitEthClaimTimelockStart;
-    uint256 public claimedWithdrawalRequests;
-    bool public lastWithdrawalRequestSubmitted; // Flag indicating the last withdrawal request submitted
 
     State public currentState;
 
@@ -95,6 +95,10 @@ contract EscrowModel {
     // Returns total rage quit support as a percentage of the total supply.
     function getRageQuitSupport() external view returns (uint256) {
         uint256 totalPooledEth = stEth.getPooledEthByShares(totalSharesLocked);
+        // Assumption: No overflow
+        unchecked {
+            require((totalPooledEth * 10 ** 18) / 10 ** 18 == totalPooledEth);
+        }
         return (totalPooledEth * 10 ** 18) / stEth.totalSupply();
     }
 

diff --git a/contracts/model/StETHModel.sol b/contracts/model/StETHModel.sol
@@ -9,10 +9,14 @@ contract StETHModel {
     uint256 internal constant INFINITE_ALLOWANCE = type(uint256).max;
 
     function setTotalPooledEther(uint256 _value) external {
+        // Assumption: totalPooledEther is not zero
+        require(_value != 0);
         totalPooledEther = _value;
     }
 
     function setTotalShares(uint256 _value) external {
+        // Assumption: totalShares is not zero
+        require(_value != 0);
         totalShares = _value;
     }
 
@@ -25,10 +29,14 @@ contract StETHModel {
     }
 
     function totalSupply() external view returns (uint256) {
+        // Assumption: totalPooledEther is not zero
+        require(totalPooledEther != 0);
         return totalPooledEther;
     }
 
     function getTotalPooledEther() external view returns (uint256) {
+        // Assumption: totalPooledEther is not zero
+        require(totalPooledEther != 0);
         return totalPooledEther;
     }
 
@@ -69,6 +77,8 @@ contract StETHModel {
     }
 
     function getTotalShares() external view returns (uint256) {
+        // Assumption: totalShares is not zero
+        require(totalShares != 0);
         return totalShares;
     }
 
@@ -77,10 +87,22 @@ contract StETHModel {
     }
 
     function getSharesByPooledEth(uint256 _ethAmount) public view returns (uint256) {
+        // Assumption: totalPooledEther is not zero
+        require(totalPooledEther != 0);
+        // Assumption: no overflow
+        unchecked {
+            require((_ethAmount * totalShares) / _ethAmount == totalShares);
+        }
         return _ethAmount * totalShares / totalPooledEther;
     }
 
     function getPooledEthByShares(uint256 _sharesAmount) public view returns (uint256) {
+        // Assumption: totalShares is not zero
+        require(totalShares != 0);
+        // Assumption: no overflow
+        unchecked {
+            require((totalPooledEther * _sharesAmount) / _sharesAmount == totalPooledEther);
+        }
         return _sharesAmount * totalPooledEther / totalShares;
     }
 

diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k
@@ -64,6 +64,10 @@ module LIDO-LEMMAS
       requires #rangeUInt(256, A) andBool #rangeUInt(256, (-1) *Int B)
       [concrete(B), simplification, comm]
 
+    rule chop (0 -Int A) ==Int B => A ==Int (pow256 -Int B) modInt pow256
+      requires #rangeUInt(256, A) andBool #rangeUInt(256, B)
+      [concrete(B), simplification, comm]
+
     // *Int
     rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification]
 
@@ -131,6 +135,33 @@ module LIDO-LEMMAS
       requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1)
       [simplification(45)]
 
+    //
+    // Equality of +Bytes
+    //
+    rule { B:Bytes #Equals B1:Bytes +Bytes B2:Bytes } =>
+           { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And
+           { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 }
+      requires lengthBytes(B1) <=Int lengthBytes(B)
+      [simplification(60), concrete(B, B1)]
+
+    rule { B1:Bytes +Bytes B2:Bytes #Equals B } =>
+           { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And
+           { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 }
+      requires lengthBytes(B1) <=Int lengthBytes(B)
+      [simplification(60), concrete(B, B1)]
+
+    rule { B:Bytes #Equals #buf( N, X:Int ) +Bytes B2:Bytes } =>
+           { X #Equals #asWord ( #range ( B, 0, N ) ) } #And
+           { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 }
+      requires N <=Int lengthBytes(B)
+      [simplification(60), concrete(B, N)]
+
+    rule { #buf( N, X:Int ) +Bytes B2:Bytes #Equals B } =>
+           { X #Equals #asWord ( #range ( B, 0, N ) ) } #And
+           { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 }
+      requires N <=Int lengthBytes(B)
+      [simplification(60), concrete(B, N)]
+
     //
     // Specific simplifications
     //