Niv/fix sanity failure

.gitignore

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

CVLByExample/TransientStorage/Hooks/Mutexer.spec

@@ -16,12 +16,21 @@ hook ALL_TSTORE(uint loc, uint v) {
 
 hook ALL_TLOAD(uint loc) uint v {
     if (loc == getContractLock() && executingContract == currentContract) {
-        require contract_lock_status == isLocked(v);
+        require contract_lock_status == isLocked(v), "Match contract lock status";
     }
 }
 
-invariant lockStatusDontChange()
-    !contract_lock_status;
+// invariant version is getting SANITY_FAILURE using the below rule instead
+// invariant lockStatusDontChange()
+//     !contract_lock_status;
+
+rule lockStatusDontChange() {
+    require !contract_lock_status, "Pre condition"; // require contract is not locked
+    // Check that after any method call, the lock is not held
+    method f; env e; calldataarg args;
+    f(e, args);
+    assert !contract_lock_status;
+}
 
 // if contract was locked function call always reverted
 rule checkContractLockReverts(){

CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec

@@ -1,14 +1,11 @@
-invariant isUnlocked(env e) 
-   getLock(e) == 0;
-
 invariant deltaZeroWhenUnlocked(env e)
     getLock(e) == 0 => getDelta(e) == 0;
 
 invariant deltaEqualsStorage(env e)
    getDelta(e) == currentContract.storageValue
 {
    preserved onTransactionBoundary with(env e2) {
-      requireInvariant isUnlocked(e2);
+      require getLock(e2) == 0, "Contract must be unlocked";
       requireInvariant deltaZeroWhenUnlocked(e2);
    }
 }

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();