Niv/fix sanity failure

.gitignore

@@ -10,3 +10,4 @@
 **/emv*
 **/collect.json
 
+.vscode/

CVLByExample/TransientStorage/Hooks/MockMutexer.sol

@@ -15,17 +15,29 @@ contract MockMutexer is Mutexer {
 
     constructor() contractLock{}
 
-    // getters
-    function lockValue() external returns (uint){
-        return uint(Mutex.Locked);
-    }
-    function getContractLock() public returns (uint256){
-        return CONTRACT_LOCK;
+    function isLocked() external returns (bool){
+        Mutex value;
+        uint256 key = CONTRACT_LOCK;
+        assembly {
+             value := tload(key)
+        }
+        return value == Mutex.Locked;
     }
+
 
    // for testing
 
     function contractLevelAccess() external contractLock {
         emit Accessed(Access.Contract);
     }
+    function changeLock() external  {
+        _mocktstore(CONTRACT_LOCK, Mutex.Locked);
+    }
+
+     function _mocktstore(uint256 key, Mutex value) private {
+        assembly {
+            tstore(key, value)
+        }
+    }
+
 }

CVLByExample/TransientStorage/Hooks/Mutexer.spec

@@ -1,32 +1,34 @@
 methods {
-
-    function lockValue() external returns (uint256) envfree;
-    function getContractLock() external returns (uint256) envfree;
+    function isLocked() external returns (bool) envfree;
 }
 
-definition isLocked(uint256 status) returns bool = status == lockValue();
-
-persistent ghost bool contract_lock_status;
+definition isLockedCVL(uint256 status) returns bool = status == 1;
+definition slot() returns uint = 0xa2e3618ded7ae709dc8e3747186ad9112d852b6c6eef8285dea55c33fdac431f;
 
+persistent ghost bool contract_lock_status{
+    init_state axiom contract_lock_status == false;
+}
 hook ALL_TSTORE(uint loc, uint v) {
-    if (loc == getContractLock() && executingContract == currentContract) {
-        contract_lock_status = isLocked(v);
+    if(loc == slot() && executingContract == currentContract){
+        contract_lock_status = isLockedCVL(v);
+    } else {
+        havoc contract_lock_status;
     }
 }
-
 hook ALL_TLOAD(uint loc) uint v {
-    if (loc == getContractLock() && executingContract == currentContract) {
-        require contract_lock_status == isLocked(v);
+    if(loc == slot() && executingContract == currentContract){
+        require contract_lock_status == isLockedCVL(v);
+    } else {
+        havoc contract_lock_status;
     }
 }
-
 invariant lockStatusDontChange()
     !contract_lock_status;
 
 // if contract was locked function call always reverted
 rule checkContractLockReverts(){
     env e;
-    require contract_lock_status; // require contract is locked
+    require isLocked(); // require contract is locked
 
     contractLevelAccess@withrevert(e);
 

CVLByExample/TransientStorage/Hooks/runTransientStorage.conf

@@ -4,5 +4,6 @@
   ],
   "verify": "MockMutexer:./Mutexer.spec",
   "solc": "solc8.24", 
-  "solc_evm_version": "cancun"
+  "solc_evm_version": "cancun",
+  "prover_args": ["-enableStorageSplitting false"]
 }

CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec

@@ -1,5 +1,12 @@
-invariant isUnlocked(env e) 
-   getLock(e) == 0;
+invariant isUnlocked(env e)
+   getLock(e) == 0 
+   filtered {
+       // The functions repay and borrow use the modifier onlyLocked therefore excluding them here, as it causes vacuity with the invariant expression.
+       f -> f.selector != sig:repay(int256).selector 
+         && f.selector != sig:borrow(int256).selector
+         // The function callback calls repay and borrow, thus same applied as above. 
+         && f.selector != sig:CallBacker.callback().selector 
+         }
 
 invariant deltaZeroWhenUnlocked(env e)
     getLock(e) == 0 => getDelta(e) == 0;

CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec

@@ -129,12 +129,6 @@ hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
     numOfAccounts[user] = newLength;
 }
 
-/**
- An internal step check to verify that our ghost works as expected, it should mirror the number of accounts.
- Once the sload is defined, this invariant becomes a tautology  
- */
-invariant checkNumOfAccounts(address user) 
-    numOfAccounts[user] == bank.getNumberOfAccounts(user);
 
 /// This Sload is required in order to eliminate adding unintializaed account balance to sumBalances.
 hook Sload uint256 length _customers[KEY address user].accounts.length {

DEFI/ConstantProductPool/contracts/broken/ConstantProductPoolBroken.sol

@@ -38,8 +38,8 @@ contract ConstantProductPool is ERC20 {
     }
 
     constructor(address _token0, address _token1)  {
-        require(token0 != address(0));
-        require(token0 != token1);
+        require(_token0 != address(0));
+        require(_token0 != _token1);
         token0 = _token0;
         token1 = _token1;
         locked = 1;

DEFI/LiquidityPool/certora/specs/Full.spec

@@ -441,7 +441,7 @@ rule sharesRoundingTripFavoursContract(env e) {
   prove bug fix
 */
 invariant noClientHasSharesWithMoreValueThanDepositedAmount(address a)
-        sharesToAmount(balanceOf(a)) <= depositedAmount()
+        totalSupply() == 0 || sharesToAmount(balanceOf(a)) <= depositedAmount()
 		{
 			preserved with(env e) {
 				require balanceOf(a) + balanceOf(e.msg.sender) < totalSupply();