Finish ERC20

certora/specs/ERC20.spec

@@ -17,12 +17,16 @@ methods {
 │ Ghost & hooks: sum of all balances                                                                                  │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-ghost sumOfBalances() returns mathint {
-  init_state axiom sumOfBalances() == 0;
+ghost mathint sumOfBalances {
+    init_state axiom sumOfBalances == 0;
+}
+
+hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+    require sumOfBalances >= to_mathint(balance);
 }
 
 hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
-    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+    sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 
 /*
@@ -31,7 +35,7 @@ hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STOR
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant totalSupplyIsSumOfBalances()
-    to_mathint(totalSupply()) == sumOfBalances();
+    to_mathint(totalSupply()) == sumOfBalances;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

certora/specs/methods/IERC2612.spec

@@ -1,5 +1,5 @@
 methods {
-    permit(address,address,uint256,uint256,uint8,bytes32,bytes32) => DISPATCHER(true)
-    nonces(address)    returns (uint256) envfree                  => DISPATCHER(true)
-    DOMAIN_SEPARATOR() returns (bytes32) envfree                  => DISPATCHER(true)
+    function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external;
+    function nonces(address)    external returns (uint256) envfree;
+    function DOMAIN_SEPARATOR() external returns (bytes32) envfree;
 }