Update dependency certora-cli to v8 (#5844)

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
Co-authored-by: ernestognw <ernestognw@gmail.com>
Co-authored-by: James Toussaint <33313130+james-toussaint@users.noreply.github.com>

.github/workflows/formal-verification.yml

@@ -12,7 +12,7 @@ on:
 env:
   PIP_VERSION: '3.11'
   JAVA_VERSION: '11'
-  SOLC_VERSION: '0.8.20'
+  SOLC_VERSION: '0.8.27'
 
 concurrency: ${{ github.workflow }}-${{ github.ref }}
 
@@ -64,7 +64,7 @@ jobs:
       - name: Verify specification
         run: |
           make -C certora apply
-          node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
+          node certora/run.js ${{ steps.arguments.outputs.result }} -p 1 -v >> "$GITHUB_STEP_SUMMARY"
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 

certora/diff/token_ERC721_ERC721.sol.patch

@@ -0,0 +1,11 @@
+--- token/ERC721/ERC721.sol	2025-08-19 17:23:33.436823903 +0200
++++ token/ERC721/ERC721.sol	2025-08-19 17:23:07.328925282 +0200
+@@ -27,7 +27,7 @@
+ 
+     mapping(uint256 tokenId => address) private _owners;
+ 
+-    mapping(address owner => uint256) private _balances;
++    mapping(address owner => uint256) internal _balances; // private → internal for FV
+ 
+     mapping(uint256 tokenId => address) private _tokenApprovals;
+ 

certora/harnesses/ERC20WrapperHarness.sol

@@ -12,18 +12,6 @@ contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper {
         string memory _symbol
     ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {}
 
-    function underlyingTotalSupply() public view returns (uint256) {
-        return underlying().totalSupply();
-    }
-
-    function underlyingBalanceOf(address account) public view returns (uint256) {
-        return underlying().balanceOf(account);
-    }
-
-    function underlyingAllowanceToThis(address account) public view returns (uint256) {
-        return underlying().allowance(account, address(this));
-    }
-
     function recover(address account) public returns (uint256) {
         return _recover(account);
     }

certora/harnesses/ERC721Harness.sol

@@ -23,6 +23,10 @@ contract ERC721Harness is ERC721 {
         _burn(tokenId);
     }
 
+    function unsafeBalanceOf(address owner) public view returns (uint256) {
+        return _balances[owner];
+    }
+
     function unsafeOwnerOf(uint256 tokenId) external view returns (address) {
         return _ownerOf(tokenId);
     }

certora/run.js

@@ -1,33 +1,25 @@
 #!/usr/bin/env node
 
 // USAGE:
-//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
+//    node certora/run.js [CONFIG]* [--all]
 // EXAMPLES:
 //    node certora/run.js --all
-//    node certora/run.js AccessControl
-//    node certora/run.js AccessControlHarness:AccessControl
+//    node certora/run.js ERC721
+//    node certora/run.js certora/specs/ERC721.conf
 
-import { spawn } from 'child_process';
-import { PassThrough } from 'stream';
-import { once } from 'events';
-import path from 'path';
-import yargs from 'yargs';
-import { hideBin } from 'yargs/helpers';
-import pLimit from 'p-limit';
-import fs from 'fs/promises';
+const glob = require('glob');
+const fs = require('fs');
+const pLimit = require('p-limit').default;
+const { hideBin } = require('yargs/helpers');
+const yargs = require('yargs/yargs');
+const { exec } = require('child_process');
 
-const argv = yargs(hideBin(process.argv))
+const { argv } = yargs(hideBin(process.argv))
   .env('')
   .options({
     all: {
-      alias: 'a',
       type: 'boolean',
     },
-    spec: {
-      alias: 's',
-      type: 'string',
-      default: path.resolve(import.meta.dirname, 'specs.json'),
-    },
     parallel: {
       alias: 'p',
       type: 'number',
@@ -38,131 +30,39 @@ const argv = yargs(hideBin(process.argv))
       type: 'count',
       default: 0,
     },
-    options: {
-      alias: 'o',
-      type: 'array',
-      default: [],
-    },
-  })
-  .parse();
-
-function match(entry, request) {
-  const [reqSpec, reqContract] = request.split(':').reverse();
-  return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
-}
-
-const specs = JSON.parse(fs.readFileSync(argv.spec, 'utf8')).filter(s => argv.all || argv._.some(r => match(s, r)));
+  });
 
+const pattern = 'certora/specs/*.conf';
 const limit = pLimit(argv.parallel);
 
 if (argv._.length == 0 && !argv.all) {
   console.error(`Warning: No specs requested. Did you forget to toggle '--all'?`);
-}
-
-for (const r of argv._) {
-  if (!specs.some(s => match(s, r))) {
-    console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`);
-    process.exitCode = 1;
-  }
-}
-
-if (process.exitCode) {
-  process.exit(process.exitCode);
-}
-
-for (const { spec, contract, files, options = [] } of specs) {
-  limit(() =>
-    runCertora(
-      spec,
-      contract,
-      files,
-      [...options, ...argv.options].flatMap(opt => opt.split(' ')),
-    ),
-  );
-}
-
-// Run certora, aggregate the output and print it at the end
-async function runCertora(spec, contract, files, options = []) {
-  const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
-  if (argv.verbose) {
-    console.log('Running:', args.join(' '));
-  }
-  const child = spawn('certoraRun', args);
-
-  const stream = new PassThrough();
-  const output = collect(stream);
-
-  child.stdout.pipe(stream, { end: false });
-  child.stderr.pipe(stream, { end: false });
-
-  // as soon as we have a job id, print the output link
-  stream.on('data', function logStatusUrl(data) {
-    const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries(
-      data
-        .toString('utf8')
-        .match(/-D\S+=\S+/g)
-        ?.map(s => s.split('=')) || [],
-    );
-
-    if (jobId && userId) {
-      console.error(`[${spec}] https://prover.certora.com/output/${userId}/${jobId}/`);
-      stream.off('data', logStatusUrl);
-    }
-  });
-
-  // wait for process end
-  const [code, signal] = await once(child, 'exit');
-
-  // error
-  if (code || signal) {
-    console.error(`[${spec}] Exited with code ${code || signal}`);
-    process.exitCode = 1;
-  }
-
-  // get all output
-  stream.end();
-
-  // write results in markdown format
-  writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
-
-  // write all details
-  console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));
-}
-
-// Collects stream data into a string
-async function collect(stream) {
-  const buffers = [];
-  for await (const data of stream) {
-    const buf = Buffer.isBuffer(data) ? data : Buffer.from(data);
-    buffers.push(buf);
-  }
-  return Buffer.concat(buffers).toString('utf8');
-}
-
-// Formatting
-let hasHeader = false;
-
-function formatRow(...array) {
-  return ['', ...array, ''].join(' | ');
-}
-
-function writeHeader() {
-  console.log(formatRow('spec', 'contract', 'result', 'status', 'output'));
-  console.log(formatRow('-', '-', '-', '-', '-'));
-}
-
-function writeEntry(spec, contract, success, url) {
-  if (!hasHeader) {
-    hasHeader = true;
-    writeHeader();
-  }
-  console.log(
-    formatRow(
-      spec,
-      contract,
-      success ? ':heavy_check_mark:' : ':x:',
-      url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error',
-      url ? `[link](${url})` : 'error',
+  process.exitCode = 1;
+} else {
+  Promise.all(
+    (argv.all ? glob.sync(pattern) : argv._.map(name => (fs.existsSync(name) ? name : pattern.replace('*', name)))).map(
+      (conf, i, { length }) =>
+        limit(
+          () =>
+            new Promise(resolve => {
+              if (argv.verbose) console.log(`[${i + 1}/${length}] Running ${conf}`);
+              exec(`certoraRun ${conf}`, (error, stdout, stderr) => {
+                const match = stdout.match(
+                  'https://prover.certora.com/output/[a-z0-9]+/[a-z0-9]+[?]anonymousKey=[a-z0-9]+',
+                );
+                if (error) {
+                  console.error(`[ERR] ${conf} failed with:\n${stderr || stdout}`);
+                  process.exitCode = 1;
+                } else if (match) {
+                  console.log(`${conf} - ${match[0]}`);
+                } else {
+                  console.error(`[ERR] Could not parse stdout for ${conf}:\n${stdout}`);
+                  process.exitCode = 1;
+                }
+                resolve();
+              });
+            }),
+        ),
     ),
   );
 }

certora/specs.json

@@ -1,110 +0,0 @@
-[
-  {
-    "spec": "Pausable",
-    "contract": "PausableHarness",
-    "files": ["certora/harnesses/PausableHarness.sol"]
-  },
-  {
-    "spec": "AccessControl",
-    "contract": "AccessControlHarness",
-    "files": ["certora/harnesses/AccessControlHarness.sol"]
-  },
-  {
-    "spec": "AccessControlDefaultAdminRules",
-    "contract": "AccessControlDefaultAdminRulesHarness",
-    "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"]
-  },
-  {
-    "spec": "AccessManager",
-    "contract": "AccessManagerHarness",
-    "files": ["certora/harnesses/AccessManagerHarness.sol"],
-    "options": ["--optimistic_hashing", "--optimistic_loop"]
-  },
-  {
-    "spec": "AccessManaged",
-    "contract": "AccessManagedHarness",
-    "files": [
-      "certora/harnesses/AccessManagedHarness.sol",
-      "certora/harnesses/AccessManagerHarness.sol"
-    ],
-    "options": [
-      "--optimistic_hashing",
-      "--optimistic_loop",
-      "--link AccessManagedHarness:_authority=AccessManagerHarness"
-    ]
-  },
-  {
-    "spec": "DoubleEndedQueue",
-    "contract": "DoubleEndedQueueHarness",
-    "files": ["certora/harnesses/DoubleEndedQueueHarness.sol"]
-  },
-  {
-    "spec": "Ownable",
-    "contract": "OwnableHarness",
-    "files": ["certora/harnesses/OwnableHarness.sol"]
-  },
-  {
-    "spec": "Ownable2Step",
-    "contract": "Ownable2StepHarness",
-    "files": ["certora/harnesses/Ownable2StepHarness.sol"]
-  },
-  {
-    "spec": "ERC20",
-    "contract": "ERC20PermitHarness",
-    "files": ["certora/harnesses/ERC20PermitHarness.sol"],
-    "options": ["--optimistic_loop"]
-  },
-  {
-    "spec": "ERC20FlashMint",
-    "contract": "ERC20FlashMintHarness",
-    "files": [
-      "certora/harnesses/ERC20FlashMintHarness.sol",
-      "certora/harnesses/ERC3156FlashBorrowerHarness.sol"
-    ],
-    "options": ["--optimistic_loop"]
-  },
-  {
-    "spec": "ERC20Wrapper",
-    "contract": "ERC20WrapperHarness",
-    "files": [
-      "certora/harnesses/ERC20PermitHarness.sol",
-      "certora/harnesses/ERC20WrapperHarness.sol"
-    ],
-    "options": [
-      "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
-      "--optimistic_loop"
-    ]
-  },
-  {
-    "spec": "ERC721",
-    "contract": "ERC721Harness",
-    "files": ["certora/harnesses/ERC721Harness.sol", "certora/harnesses/ERC721ReceiverHarness.sol"],
-    "options": ["--optimistic_loop"]
-  },
-  {
-    "spec": "Initializable",
-    "contract": "InitializableHarness",
-    "files": ["certora/harnesses/InitializableHarness.sol"]
-  },
-  {
-    "spec": "EnumerableSet",
-    "contract": "EnumerableSetHarness",
-    "files": ["certora/harnesses/EnumerableSetHarness.sol"]
-  },
-  {
-    "spec": "EnumerableMap",
-    "contract": "EnumerableMapHarness",
-    "files": ["certora/harnesses/EnumerableMapHarness.sol"]
-  },
-  {
-    "spec": "TimelockController",
-    "contract": "TimelockControllerHarness",
-    "files": ["certora/harnesses/TimelockControllerHarness.sol"],
-    "options": ["--optimistic_hashing", "--optimistic_loop"]
-  },
-  {
-    "spec": "Nonces",
-    "contract": "NoncesHarness",
-    "files": ["certora/harnesses/NoncesHarness.sol"]
-  }
-]

certora/specs/AccessControl.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/AccessControlHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "AccessControlHarness:certora/specs/AccessControl.spec"
+}

certora/specs/AccessControlDefaultAdminRules.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "AccessControlDefaultAdminRulesHarness:certora/specs/AccessControlDefaultAdminRules.spec"
+}

certora/specs/AccessControlDefaultAdminRules.spec

@@ -67,11 +67,14 @@ invariant defaultAdminRoleAdminConsistency()
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: owner is the defaultAdmin                                                                                │
+│ Rule: owner is the defaultAdmin                                                                                     │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant ownerConsistency()
-  defaultAdmin() == owner();
+// Writing this as an invariant would be flagged by Certora as trivial. Writing it as a rule is just as valid: we
+// verify the is true for any state of the storage
+rule ownerConsistency() {
+  assert defaultAdmin() == owner();
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

certora/specs/AccessManaged.conf

@@ -0,0 +1,14 @@
+{
+    "files": [
+        "certora/harnesses/AccessManagedHarness.sol",
+        "certora/harnesses/AccessManagerHarness.sol"
+    ],
+    "link": [
+        "AccessManagedHarness:_authority=AccessManagerHarness"
+    ],
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "AccessManagedHarness:certora/specs/AccessManaged.spec"
+}

certora/specs/AccessManaged.spec

@@ -7,6 +7,21 @@ methods {
     function authority_canCall_immediate(address) external returns (bool);
     function authority_canCall_delay(address)     external returns (uint32);
     function authority_getSchedule(address)       external returns (uint48);
+
+    // Summarization for external calls (cause havoc in isConsumingScheduledOpClean invariant):
+
+    // Called by AccessManager.updateAuthority() on target contracts. This modifies
+    // the target contract's authority but doesn't affect the AccessManager's _consumingSchedule state.
+    function _.setAuthority(address) external => NONDET;
+
+    // Called by AccessManaged._checkCanCall() to consume scheduled operations on the AccessManager.
+    // This function should complete successfully and only affect the AccessManager's internal state,
+    // not the _consumingSchedule state of the calling AccessManaged contract.
+    function _.consumeScheduledOp(address, bytes) external => NONDET;
+
+    // For unresolved external calls (like low-level target.call{value: value}(data))
+    // made via Address.functionCallWithValue in AccessManager.execute().
+    unresolved external in _._ => DISPATCH [] default NONDET;
 }
 
 invariant isConsumingScheduledOpClean()

certora/specs/AccessManager.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harnesses/AccessManagerHarness.sol"
+    ],
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "AccessManagerHarness:certora/specs/AccessManager.spec"
+}

certora/specs/AccessManager.spec

@@ -130,24 +130,35 @@ rule getAdminRestrictions(env e, bytes data) {
         assert restricted == false;
         assert roleId     == 0;
         assert delay      == 0;
+    } else if (
+        selector == to_bytes4(sig:labelRole(uint64,string).selector) ||
+        selector == to_bytes4(sig:setRoleAdmin(uint64,uint64).selector) ||
+        selector == to_bytes4(sig:setRoleGuardian(uint64,uint64).selector) ||
+        selector == to_bytes4(sig:setGrantDelay(uint64,uint32).selector) ||
+        selector == to_bytes4(sig:setTargetAdminDelay(address,uint32).selector)
+    ) {
+        assert restricted == true;
+        assert roleId     == ADMIN_ROLE();
+        assert delay      == 0;
+    } else if (
+        selector == to_bytes4(sig:updateAuthority(address,address).selector) ||
+        selector == to_bytes4(sig:setTargetClosed(address,bool).selector) ||
+        selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector)
+    ) {
+        assert restricted == true;
+        assert roleId     == ADMIN_ROLE();
+        assert delay      == getTargetAdminDelay(e, getFirstArgumentAsAddress(data));
+    } else if (
+        selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector) ||
+        selector == to_bytes4(sig:revokeRole(uint64,address).selector)
+    ) {
+        assert restricted == true;
+        assert roleId     == getRoleAdmin(getFirstArgumentAsUint64(data));
+        assert delay      == 0;
     } else {
-        assert restricted ==
-            isOnlyAuthorized(selector);
-
-        assert roleId == (
-            (restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) ||
-            (restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector      ))
-            ? getRoleAdmin(getFirstArgumentAsUint64(data))
-            : ADMIN_ROLE()
-        );
-
-        assert delay == (
-            (restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector              )) ||
-            (restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector                 )) ||
-            (restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector))
-            ? getTargetAdminDelay(e, getFirstArgumentAsAddress(data))
-            : 0
-        );
+        assert restricted == false;
+        assert roleId     == getTargetFunctionRole(currentContract, selector);
+        assert delay      == 0;
     }
 }
 
@@ -213,29 +224,32 @@ rule canCallExtended(env e) {
 
     bool   immediate      = canCallExtended_immediate(e, caller, target, data);
     uint32 delay          = canCallExtended_delay(e, caller, target, data);
-    bool   enabled        = getAdminRestrictions_restricted(e, data);
+    bool   restricted     = getAdminRestrictions_restricted(e, data);
+    bool   closed         = isTargetClosed(target);
     uint64 roleId         = getAdminRestrictions_roleAdminId(e, data);
     uint32 operationDelay = getAdminRestrictions_executionDelay(e, data);
     bool   inRole         = hasRole_isMember(e, roleId, caller);
     uint32 executionDelay = hasRole_executionDelay(e, roleId, caller);
 
-    if (target == currentContract) {
+    if (data.length < 4) {
+        assert immediate == false;
+        assert delay     == 0;
+    } else if (target == currentContract) {
         // Can only execute without delay in the specific cases:
         // - caller is the AccessManager and the executionId is set
         // or
-        // - data matches an admin restricted function
+        // - data matches an admin restricted function OR non-admin restricted function on open target
         // - caller has the necessary role
         // - operation delay is not set
         // - execution delay is not set
         assert immediate <=> (
             (
                 caller         == currentContract &&
-                data.length    >= 4               &&
                 executionId()  == hashExecutionId(target, selector)
             ) || (
                 caller         != currentContract &&
-                enabled                           &&
                 inRole                            &&
+                (restricted || !closed)           &&
                 operationDelay == 0               &&
                 executionDelay == 0
             )
@@ -247,21 +261,18 @@ rule canCallExtended(env e) {
 
         // Can only execute with delay in specific cases:
         // - caller is a third party
-        // - data matches an admin restricted function
+        // - data matches an admin restricted function OR non-admin restricted function on open target
         // - caller has the necessary role
-        // -operation delay or execution delay is set
+        // - operation delay or execution delay is set
         assert delay > 0 <=> (
             caller != currentContract &&
-            enabled                   &&
             inRole                    &&
+            (restricted || !closed)   &&
             (operationDelay > 0 || executionDelay > 0)
         );
 
         // If there is a delay, then it must be the maximum of caller's execution delay and the operation delay
         assert delay > 0 => to_mathint(delay) == max(operationDelay, executionDelay);
-    } else if (data.length < 4) {
-        assert immediate == false;
-        assert delay     == 0;
     } else {
         // results are equivalent when targeting third party contracts
         assert immediate == canCall_immediate(e, caller, target, selector);

certora/specs/DoubleEndedQueue.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/DoubleEndedQueueHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "DoubleEndedQueueHarness:certora/specs/DoubleEndedQueue.spec"
+}

certora/specs/DoubleEndedQueue.spec

@@ -23,25 +23,25 @@ definition full() returns bool = length() == max_uint128;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: empty() is length 0 and no element exists                                                                │
+│ Rule: front points to the first index and back points to the last one                                               │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant emptiness()
-    empty() <=> length() == 0
-    filtered { f -> !f.isView }
+rule emptiness() {
+    assert empty() <=> length() == 0;
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: front points to the first index and back points to the last one                                          │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant queueFront()
-    at_(0) == front()
-    filtered { f -> !f.isView }
+rule queueFront() {
+    assert at_(0) == front();
+}
 
-invariant queueBack()
-    at_(require_uint256(length() - 1)) == back()
-    filtered { f -> !f.isView }
+rule queueBack() {
+    assert at_(require_uint256(length() - 1)) == back();
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

certora/specs/ERC20.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "certora/harnesses/ERC20PermitHarness.sol"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "ERC20PermitHarness:certora/specs/ERC20.spec"
+}

certora/specs/ERC20.spec

@@ -19,15 +19,15 @@ ghost mathint sumOfBalances {
 
 // Because `balance` has a uint256 type, any balance addition in CVL1 behaved as a `require_uint256()` casting,
 // leaving out the possibility of overflow. This is not the case in CVL2 where casting became more explicit.
-// A counterexample in CVL2 is having an initial state where Alice initial balance is larger than totalSupply, which 
-// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an 
+// A counterexample in CVL2 is having an initial state where Alice initial balance is larger than totalSupply, which
+// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an
 // already used address (or upgraded from corrupted state).
 // We restrict such behavior by making sure no balance is greater than the sum of balances.
-hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+hook Sload uint256 balance _balances[KEY address addr] {
     require sumOfBalances >= to_mathint(balance);
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 

certora/specs/ERC20FlashMint.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harnesses/ERC20FlashMintHarness.sol",
+        "certora/harnesses/ERC3156FlashBorrowerHarness.sol"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec"
+}

certora/specs/ERC20Wrapper.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "certora/harnesses/ERC20PermitHarness.sol",
+        "certora/harnesses/ERC20WrapperHarness.sol"
+    ],
+    "link": [
+        "ERC20WrapperHarness:_underlying=ERC20PermitHarness"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec"
+}

certora/specs/ERC20Wrapper.spec

@@ -1,15 +1,22 @@
 import "helpers/helpers.spec";
 import "ERC20.spec";
 
+using ERC20PermitHarness as underlying;
+
 methods {
-    function underlying()                       external returns(address) envfree;
-    function underlyingTotalSupply()            external returns(uint256) envfree;
-    function underlyingBalanceOf(address)       external returns(uint256) envfree;
-    function underlyingAllowanceToThis(address) external returns(uint256) envfree;
-
-    function depositFor(address, uint256)       external returns(bool);
-    function withdrawTo(address, uint256)       external returns(bool);
-    function recover(address)                   external returns(uint256);
+    function underlying()                          external returns(address) envfree;
+    function depositFor(address, uint256)          external returns(bool);
+    function withdrawTo(address, uint256)          external returns(bool);
+    function recover(address)                      external returns(uint256);
+
+    function underlying.totalSupply()              external returns (uint256) envfree;
+    function underlying.balanceOf(address)         external returns (uint256) envfree;
+    function underlying.allowance(address,address) external returns (uint256) envfree;
+
+    unresolved external in _._ => DISPATCH(optimistic=true) [
+        underlying.transferFrom(address, address, uint256),
+        underlying.transfer(address, uint256)
+    ];
 }
 
 use invariant totalSupplyIsSumOfBalances;
@@ -19,11 +26,24 @@ use invariant totalSupplyIsSumOfBalances;
 │ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying                                           │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-definition underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool =
-    underlyingBalanceOf(a) <= underlyingTotalSupply();
-
 definition sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool =
-    a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= to_mathint(underlyingTotalSupply());
+    a != b => underlying.balanceOf(a) + underlying.balanceOf(b) <= to_mathint(underlying.totalSupply());
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: wrapped token should not allow any third party to spend its tokens                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant noAllowance(address user)
+    underlying.allowance(currentContract, user) == 0
+    {
+        preserved ERC20PermitHarness.approve(address spender, uint256 value) with (env e) {
+            require e.msg.sender != currentContract;
+        }
+        preserved ERC20PermitHarness.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) with (env e) {
+            require owner != currentContract;
+        }
+    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -31,21 +51,29 @@ definition sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant totalSupplyIsSmallerThanUnderlyingBalance()
-    totalSupply() <= underlyingBalanceOf(currentContract) &&
-    underlyingBalanceOf(currentContract) <= underlyingTotalSupply() &&
-    underlyingTotalSupply() <= max_uint256
+    totalSupply() <= underlying.balanceOf(currentContract) &&
+    underlying.balanceOf(currentContract) <= underlying.totalSupply() &&
+    underlying.totalSupply() <= max_uint256
     {
-        preserved {
+        preserved with (env e) {
             requireInvariant totalSupplyIsSumOfBalances;
-            require underlyingBalancesLowerThanUnderlyingSupply(currentContract);
-        }
-        preserved depositFor(address account, uint256 amount) with (env e) {
+            require e.msg.sender != currentContract;
             require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract);
         }
+        preserved ERC20PermitHarness.transferFrom(address from, address to, uint256 amount) with (env e) {
+            requireInvariant noAllowance(e.msg.sender);
+            require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(from, to);
+        }
+        preserved ERC20PermitHarness.burn(address from, uint256 amount) with (env e) {
+            // If someone can burn from the wrapper, than the invariant obviously doesn't hold.
+            require from != currentContract;
+            require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(from, currentContract);
+        }
     }
 
-invariant noSelfWrap()
-    currentContract != underlying();
+rule noSelfWrap() {
+    assert currentContract != underlying();
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -61,20 +89,20 @@ rule depositFor(env e) {
     uint256 amount;
 
     // sanity
-    requireInvariant noSelfWrap;
+    require currentContract != underlying();
     requireInvariant totalSupplyIsSumOfBalances;
     requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
     require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, sender);
 
     uint256 balanceBefore                   = balanceOf(receiver);
     uint256 supplyBefore                    = totalSupply();
-    uint256 senderUnderlyingBalanceBefore   = underlyingBalanceOf(sender);
-    uint256 senderUnderlyingAllowanceBefore = underlyingAllowanceToThis(sender);
-    uint256 wrapperUnderlyingBalanceBefore  = underlyingBalanceOf(currentContract);
-    uint256 underlyingSupplyBefore          = underlyingTotalSupply();
+    uint256 senderUnderlyingBalanceBefore   = underlying.balanceOf(sender);
+    uint256 senderUnderlyingAllowanceBefore = underlying.allowance(sender, currentContract);
+    uint256 wrapperUnderlyingBalanceBefore  = underlying.balanceOf(currentContract);
+    uint256 underlyingSupplyBefore          = underlying.totalSupply();
 
     uint256 otherBalanceBefore              = balanceOf(other);
-    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
+    uint256 otherUnderlyingBalanceBefore    = underlying.balanceOf(other);
 
     depositFor@withrevert(e, receiver, amount);
     bool success = !lastReverted;
@@ -93,14 +121,14 @@ rule depositFor(env e) {
     assert success => (
         to_mathint(balanceOf(receiver)) == balanceBefore + amount &&
         to_mathint(totalSupply()) == supplyBefore + amount &&
-        to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount &&
-        to_mathint(underlyingBalanceOf(sender)) == senderUnderlyingBalanceBefore - amount
+        to_mathint(underlying.balanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount &&
+        to_mathint(underlying.balanceOf(sender)) == senderUnderlyingBalanceBefore - amount
     );
 
     // no side effect
-    assert underlyingTotalSupply() == underlyingSupplyBefore;
+    assert underlying.totalSupply() == underlyingSupplyBefore;
     assert balanceOf(other)           != otherBalanceBefore           => other == receiver;
-    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract);
+    assert underlying.balanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract);
 }
 
 /*
@@ -117,19 +145,19 @@ rule withdrawTo(env e) {
     uint256 amount;
 
     // sanity
-    requireInvariant noSelfWrap;
+    require currentContract != underlying();
     requireInvariant totalSupplyIsSumOfBalances;
     requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
     require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, receiver);
 
     uint256 balanceBefore                   = balanceOf(sender);
     uint256 supplyBefore                    = totalSupply();
-    uint256 receiverUnderlyingBalanceBefore = underlyingBalanceOf(receiver);
-    uint256 wrapperUnderlyingBalanceBefore  = underlyingBalanceOf(currentContract);
-    uint256 underlyingSupplyBefore          = underlyingTotalSupply();
+    uint256 receiverUnderlyingBalanceBefore = underlying.balanceOf(receiver);
+    uint256 wrapperUnderlyingBalanceBefore  = underlying.balanceOf(currentContract);
+    uint256 underlyingSupplyBefore          = underlying.totalSupply();
 
     uint256 otherBalanceBefore              = balanceOf(other);
-    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
+    uint256 otherUnderlyingBalanceBefore    = underlying.balanceOf(other);
 
     withdrawTo@withrevert(e, receiver, amount);
     bool success = !lastReverted;
@@ -146,14 +174,14 @@ rule withdrawTo(env e) {
     assert success => (
         to_mathint(balanceOf(sender)) == balanceBefore - amount &&
         to_mathint(totalSupply()) == supplyBefore - amount &&
-        to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
-        to_mathint(underlyingBalanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
+        to_mathint(underlying.balanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
+        to_mathint(underlying.balanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
     );
 
     // no side effect
-    assert underlyingTotalSupply() == underlyingSupplyBefore;
+    assert underlying.totalSupply() == underlyingSupplyBefore;
     assert balanceOf(other)           != otherBalanceBefore           => other == sender;
-    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract);
+    assert underlying.balanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract);
 }
 
 /*
@@ -168,16 +196,16 @@ rule recover(env e) {
     address other;
 
     // sanity
-    requireInvariant noSelfWrap;
+    require currentContract != underlying();
     requireInvariant totalSupplyIsSumOfBalances;
     requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
 
-    mathint value                        = underlyingBalanceOf(currentContract) - totalSupply();
+    mathint value                        = underlying.balanceOf(currentContract) - totalSupply();
     uint256 supplyBefore                 = totalSupply();
     uint256 balanceBefore                = balanceOf(receiver);
 
     uint256 otherBalanceBefore           = balanceOf(other);
-    uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
+    uint256 otherUnderlyingBalanceBefore = underlying.balanceOf(other);
 
     recover@withrevert(e, receiver);
     bool success = !lastReverted;
@@ -189,10 +217,10 @@ rule recover(env e) {
     assert success => (
         to_mathint(balanceOf(receiver)) == balanceBefore + value &&
         to_mathint(totalSupply()) == supplyBefore + value &&
-        totalSupply() == underlyingBalanceOf(currentContract)
+        totalSupply() == underlying.balanceOf(currentContract)
     );
 
     // no side effect
-    assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore;
+    assert underlying.balanceOf(other) == otherUnderlyingBalanceBefore;
     assert balanceOf(other) != otherBalanceBefore => other == receiver;
 }

certora/specs/ERC721.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harnesses/ERC721Harness.sol",
+        "certora/harnesses/ERC721ReceiverHarness.sol"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "ERC721Harness:certora/specs/ERC721.spec"
+}

certora/specs/ERC721.spec

@@ -9,6 +9,7 @@ methods {
     function safeMint(address,uint256,bytes) external;
     function burn(uint256) external;
 
+    function unsafeBalanceOf(address) external returns (uint256) envfree;
     function unsafeOwnerOf(uint256) external returns (address) envfree;
     function unsafeGetApproved(uint256) external returns (address) envfree;
 }
@@ -19,12 +20,10 @@ methods {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
-definition authSanity(env e) returns bool = e.msg.sender != 0;
-
 // Could be broken in theory, but not in practice
-definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
+definition balanceLimited(address account) returns bool = unsafeBalanceOf(account) < max_uint256;
 
-function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
+function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) returns bool {
     if (f.selector == sig:transferFrom(address,address,uint256).selector) {
         transferFrom@withrevert(e, from, to, tokenId);
     } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
@@ -37,9 +36,10 @@ function helperTransferWithRevert(env e, method f, address from, address to, uin
         calldataarg args;
         f@withrevert(e, args);
     }
+    return !lastReverted;
 }
 
-function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
+function helperMintWithRevert(env e, method f, address to, uint256 tokenId) returns bool {
     if (f.selector == sig:mint(address,uint256).selector) {
         mint@withrevert(e, to, tokenId);
     } else if (f.selector == sig:safeMint(address,uint256).selector) {
@@ -51,6 +51,7 @@ function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
     } else {
         require false;
     }
+    return !lastReverted;
 }
 
 function helperSoundFnCall(env e, method f) {
@@ -100,6 +101,17 @@ function helperSoundFnCall(env e, method f) {
     }
 }
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helper: check that unsafe getter match their unsafe counterpart                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule unsafeConsistency(address user, uint256 tokenId) {
+    assert user                   != 0 => unsafeBalanceOf(user)      == balanceOf(user);
+    assert unsafeOwnerOf(tokenId) != 0 => unsafeOwnerOf(tokenId)     == ownerOf(tokenId);
+    assert unsafeOwnerOf(tokenId) != 0 => unsafeGetApproved(tokenId) == getApproved(tokenId);
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Ghost & hooks: ownership count                                                                                      │
@@ -113,7 +125,7 @@ ghost mapping(address => mathint) _ownedByUser {
     init_state axiom forall address a. _ownedByUser[a] == 0;
 }
 
-hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
+hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
     _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
     _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
     _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
@@ -132,13 +144,13 @@ ghost mapping(address => mathint) _balances {
     init_state axiom forall address a. _balances[a] == 0;
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     _supply = _supply - oldValue + newValue;
 }
 
 // TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add
 // many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved.
-hook Sload uint256 value _balances[KEY address user] STORAGE {
+hook Sload uint256 value _balances[KEY address user] {
     require _balances[user] == to_mathint(value);
 }
 
@@ -189,8 +201,8 @@ invariant ownedTotalIsSumOfBalances()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant balanceOfConsistency(address user)
-    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
-    to_mathint(balanceOf(user)) == _balances[user]
+    to_mathint(unsafeBalanceOf(user)) == _ownedByUser[user] &&
+    to_mathint(unsafeBalanceOf(user)) == _balances[user]
     {
         preserved {
             require balanceLimited(user);
@@ -203,7 +215,7 @@ invariant balanceOfConsistency(address user)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant ownerHasBalance(uint256 tokenId)
-    balanceOf(ownerOf(tokenId)) > 0
+    unsafeOwnerOf(tokenId) == 0 || unsafeBalanceOf(unsafeOwnerOf(tokenId)) > 0
     {
         preserved {
             requireInvariant balanceOfConsistency(ownerOf(tokenId));
@@ -216,6 +228,9 @@ invariant ownerHasBalance(uint256 tokenId)
 │ Rule: balance of address(0) is 0                                                                                    │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
+invariant zeroAddressUnsafeBalanceIsZero()
+    unsafeBalanceOf(0) == 0;
+
 rule zeroAddressBalanceRevert() {
     balanceOf@withrevert(0);
     assert lastReverted;
@@ -301,9 +316,9 @@ rule balanceChange(env e, address account) {
     requireInvariant balanceOfConsistency(account);
     require balanceLimited(account);
 
-    mathint balanceBefore = balanceOf(account);
+    mathint balanceBefore = unsafeBalanceOf(account);
     method f; helperSoundFnCall(e, f);
-    mathint balanceAfter  = balanceOf(account);
+    mathint balanceAfter  = unsafeBalanceOf(account);
 
     // balance can change by at most 1
     assert balanceBefore != balanceAfter => (
@@ -397,18 +412,20 @@ rule approvedForAllChange(env e, address owner, address spender) {
 */
 rule transferFrom(env e, address from, address to, uint256 tokenId) {
     require nonpayable(e);
-    require authSanity(e);
+    require nonzerosender(e);
 
     address operator = e.msg.sender;
     uint256 otherTokenId;
     address otherAccount;
 
+    requireInvariant zeroAddressHasNoApprovedOperator(operator);
+    requireInvariant notMintedUnset(tokenId);
     requireInvariant ownerHasBalance(tokenId);
     require balanceLimited(to);
 
-    uint256 balanceOfFromBefore  = balanceOf(from);
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    uint256 balanceOfFromBefore  = unsafeBalanceOf(from);
+    uint256 balanceOfToBefore    = unsafeBalanceOf(to);
+    uint256 balanceOfOtherBefore = unsafeBalanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
     address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
     address approvalBefore       = unsafeGetApproved(tokenId);
@@ -427,14 +444,14 @@ rule transferFrom(env e, address from, address to, uint256 tokenId) {
 
     // effect
     assert success => (
-        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
-        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
-        unsafeOwnerOf(tokenId)                 == to &&
-        unsafeGetApproved(tokenId)             == 0
+        to_mathint(unsafeBalanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
+        to_mathint(unsafeBalanceOf(to))   == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
+        unsafeOwnerOf(tokenId)            == to &&
+        unsafeGetApproved(tokenId)        == 0
     );
 
     // no side effect
-    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
+    assert unsafeBalanceOf(otherAccount)   != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
     assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
     assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
 }
@@ -449,25 +466,26 @@ rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId
     f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
 } {
     require nonpayable(e);
-    require authSanity(e);
+    require nonzerosender(e);
 
     address operator = e.msg.sender;
     uint256 otherTokenId;
     address otherAccount;
 
+    requireInvariant zeroAddressHasNoApprovedOperator(operator);
+    requireInvariant notMintedUnset(tokenId);
     requireInvariant ownerHasBalance(tokenId);
     require balanceLimited(to);
 
-    uint256 balanceOfFromBefore  = balanceOf(from);
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    uint256 balanceOfFromBefore  = unsafeBalanceOf(from);
+    uint256 balanceOfToBefore    = unsafeBalanceOf(to);
+    uint256 balanceOfOtherBefore = unsafeBalanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
     address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
     address approvalBefore       = unsafeGetApproved(tokenId);
     address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
 
-    helperTransferWithRevert(e, f, from, to, tokenId);
-    bool success = !lastReverted;
+    bool success = helperTransferWithRevert(e, f, from, to, tokenId);
 
     assert success <=> (
         from == ownerBefore &&
@@ -478,14 +496,14 @@ rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId
 
     // effect
     assert success => (
-        to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
-        to_mathint(balanceOf(to))   == balanceOfToBefore   + assert_uint256(from != to ? 1: 0) &&
-        unsafeOwnerOf(tokenId)      == to &&
-        unsafeGetApproved(tokenId)  == 0
+        to_mathint(unsafeBalanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
+        to_mathint(unsafeBalanceOf(to))   == balanceOfToBefore   + assert_uint256(from != to ? 1: 0) &&
+        unsafeOwnerOf(tokenId)            == to &&
+        unsafeGetApproved(tokenId)        == 0
     );
 
     // no side effect
-    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
+    assert unsafeBalanceOf(otherAccount)   != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
     assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
     assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
 }
@@ -505,8 +523,8 @@ rule mint(env e, address to, uint256 tokenId) {
     require balanceLimited(to);
 
     mathint supplyBefore         = _supply;
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    uint256 balanceOfToBefore    = unsafeBalanceOf(to);
+    uint256 balanceOfOtherBefore = unsafeBalanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
     address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
 
@@ -521,14 +539,14 @@ rule mint(env e, address to, uint256 tokenId) {
 
     // effect
     assert success => (
-        _supply                   == supplyBefore + 1 &&
-        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
-        unsafeOwnerOf(tokenId)    == to
+        _supply                         == supplyBefore + 1 &&
+        to_mathint(unsafeBalanceOf(to)) == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId)          == to
     );
 
     // no side effect
-    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
-    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeBalanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to;
+    assert unsafeOwnerOf(otherTokenId)   != otherOwnerBefore     => otherTokenId == tokenId;
 }
 
 /*
@@ -549,13 +567,12 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
     require balanceLimited(to);
 
     mathint supplyBefore         = _supply;
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
+    uint256 balanceOfToBefore    = unsafeBalanceOf(to);
+    uint256 balanceOfOtherBefore = unsafeBalanceOf(otherAccount);
     address ownerBefore          = unsafeOwnerOf(tokenId);
     address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
 
-    helperMintWithRevert(e, f, to, tokenId);
-    bool success = !lastReverted;
+    bool success = helperMintWithRevert(e, f, to, tokenId);
 
     assert success <=> (
         ownerBefore == 0 &&
@@ -564,14 +581,14 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
 
     // effect
     assert success => (
-        _supply                   == supplyBefore + 1 &&
-        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
-        unsafeOwnerOf(tokenId)    == to
+        _supply                         == supplyBefore + 1 &&
+        to_mathint(unsafeBalanceOf(to)) == balanceOfToBefore + 1 &&
+        unsafeOwnerOf(tokenId)          == to
     );
 
     // no side effect
-    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
-    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
+    assert unsafeBalanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to;
+    assert unsafeOwnerOf(otherTokenId)   != otherOwnerBefore     => otherTokenId == tokenId;
 }
 
 /*
@@ -582,17 +599,16 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
 rule burn(env e, uint256 tokenId) {
     require nonpayable(e);
 
-    address from = unsafeOwnerOf(tokenId);
     uint256 otherTokenId;
     address otherAccount;
 
     requireInvariant ownerHasBalance(tokenId);
 
     mathint supplyBefore         = _supply;
-    uint256 balanceOfFromBefore  = balanceOf(from);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
-    address ownerBefore          = unsafeOwnerOf(tokenId);
+    address ownerBefore          = unsafeOwnerOf(tokenId); // from
     address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
+    uint256 balanceOfOwnerBefore = unsafeBalanceOf(ownerBefore);
+    uint256 balanceOfOtherBefore = unsafeBalanceOf(otherAccount);
     address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
 
     burn@withrevert(e, tokenId);
@@ -606,13 +622,13 @@ rule burn(env e, uint256 tokenId) {
     // effect
     assert success => (
         _supply                     == supplyBefore - 1 &&
-        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
+        to_mathint(unsafeBalanceOf(ownerBefore)) == balanceOfOwnerBefore - 1 &&
         unsafeOwnerOf(tokenId)      == 0 &&
         unsafeGetApproved(tokenId)  == 0
     );
 
     // no side effect
-    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
+    assert unsafeBalanceOf(otherAccount)   != balanceOfOtherBefore => otherAccount == ownerBefore;
     assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
     assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
 }
@@ -624,7 +640,7 @@ rule burn(env e, uint256 tokenId) {
 */
 rule approve(env e, address spender, uint256 tokenId) {
     require nonpayable(e);
-    require authSanity(e);
+    require nonzerosender(e);
 
     address caller = e.msg.sender;
     address owner = unsafeOwnerOf(tokenId);

certora/specs/EnumerableMap.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/EnumerableMapHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "EnumerableMapHarness:certora/specs/EnumerableMap.spec"
+}

certora/specs/EnumerableMap.spec

@@ -21,7 +21,7 @@ methods {
 │ Helpers                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-definition sanity() returns bool =
+definition lengthSanity() returns bool =
     length() < max_uint256;
 
 /*
@@ -33,7 +33,7 @@ invariant noValueIfNotContained(bytes32 key)
     !contains(key) => tryGet_value(key) == to_bytes32(0)
     {
         preserved set(bytes32 otherKey, bytes32 someValue) {
-            require sanity();
+            require lengthSanity();
         }
     }
 
@@ -57,8 +57,13 @@ invariant indexedContained(uint256 index)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant atUniqueness(uint256 index1, uint256 index2)
-    index1 == index2 <=> key_at(index1) == key_at(index2)
+    (index1 < length() && index2 < length()) =>
+    (index1 == index2 <=> key_at(index1) == key_at(index2))
     {
+        preserved {
+            requireInvariant consistencyIndex(index1);
+            requireInvariant consistencyIndex(index2);
+        }
         preserved remove(bytes32 key) {
             requireInvariant atUniqueness(index1, require_uint256(length() - 1));
             requireInvariant atUniqueness(index2, require_uint256(length() - 1));
@@ -89,6 +94,9 @@ invariant consistencyKey(bytes32 key)
         key_at(require_uint256(_positionOf(key) - 1)) == key
     )
     {
+        preserved {
+            require lengthSanity();
+        }
         preserved remove(bytes32 otherKey) {
             requireInvariant consistencyKey(otherKey);
             requireInvariant atUniqueness(
@@ -98,14 +106,26 @@ invariant consistencyKey(bytes32 key)
         }
     }
 
+invariant absentKeyIsNotStored(bytes32 key, uint256 index)
+    index < length() => (!contains(key) => key_at(index) != key)
+    {
+        preserved remove(bytes32 otherKey) {
+            requireInvariant consistencyIndex(index);
+            requireInvariant consistencyKey(key);
+            requireInvariant atUniqueness(index, require_uint256(length() - 1));
+        }
+    }
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rule: state only changes by setting or removing elements                                                            │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule stateChange(env e, bytes32 key) {
-    require sanity();
+    require lengthSanity();
     requireInvariant consistencyKey(key);
+    requireInvariant absentKeyIsNotStored(key, require_uint256(length() - 1));
+    requireInvariant noValueIfNotContained(key);
 
     uint256 lengthBefore   = length();
     bool    containsBefore = contains(key);
@@ -142,6 +162,7 @@ rule stateChange(env e, bytes32 key) {
 */
 rule liveness_1(bytes32 key) {
     requireInvariant consistencyKey(key);
+    requireInvariant noValueIfNotContained(key);
 
     // contains never revert
     bool contains = contains@withrevert(key);
@@ -155,7 +176,7 @@ rule liveness_1(bytes32 key) {
     tryGet_value@withrevert(key);
     assert !lastReverted;
 
-    // get reverts iff  the key is not in the map
+    // get reverts iff the key is not in the map
     get@withrevert(key);
     assert !lastReverted <=> contains;
 }
@@ -200,7 +221,7 @@ rule getAndTryGet(bytes32 key) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule set(bytes32 key, bytes32 value, bytes32 otherKey) {
-    require sanity();
+    require lengthSanity();
 
     uint256 lengthBefore        = length();
     bool    containsBefore      = contains(key);
@@ -237,6 +258,7 @@ rule set(bytes32 key, bytes32 value, bytes32 otherKey) {
 rule remove(bytes32 key, bytes32 otherKey) {
     requireInvariant consistencyKey(key);
     requireInvariant consistencyKey(otherKey);
+    requireInvariant indexedContained(require_uint256(length() - 1));
 
     uint256 lengthBefore        = length();
     bool    containsBefore      = contains(key);
@@ -268,7 +290,7 @@ rule remove(bytes32 key, bytes32 otherKey) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule setEnumerability(bytes32 key, bytes32 value, uint256 index) {
-    require sanity();
+    require lengthSanity();
 
     bytes32 atKeyBefore = key_at(index);
     bytes32 atValueBefore = value_at(index);
@@ -299,35 +321,44 @@ rule removeEnumerability(bytes32 key, uint256 index) {
     requireInvariant consistencyKey(key);
     requireInvariant consistencyIndex(index);
     requireInvariant consistencyIndex(last);
+    requireInvariant indexedContained(index);
 
     bytes32 atKeyBefore     = key_at(index);
     bytes32 atValueBefore   = value_at(index);
     bytes32 lastKeyBefore   = key_at(last);
     bytes32 lastValueBefore = value_at(last);
 
-    remove(key);
+    bool removed = remove(key);
 
     // can't read last value & keys (length decreased)
     bytes32 atKeyAfter = key_at@withrevert(index);
-    assert lastReverted <=> index == last;
+    assert lastReverted <=> (removed && index == last);
 
     bytes32 atValueAfter = value_at@withrevert(index);
-    assert lastReverted <=> index == last;
-
-    // One value that is allowed to change is if previous value was removed,
-    // in that case the last value before took its place.
-    assert (
-        index != last &&
-        atKeyBefore != atKeyAfter
-    ) => (
-        atKeyBefore == key &&
-        atKeyAfter == lastKeyBefore
+    assert lastReverted <=> (removed && index == last);
+
+    // Cases where a key or value can change are:
+    // 1. an item was removed and we are looking at the old last index. In that case the reading reverted.
+    // 2. an item was removed and we are looking at its old position. In that case the new value is the old lastValue.
+    // This rule implies that if no item was removed, then keys and values cannot change.
+    assert atKeyBefore != atKeyAfter => (
+        (
+            removed &&
+            index == last
+        ) || (
+            removed &&
+            atKeyBefore == key &&
+            atKeyAfter == lastKeyBefore
+        )
     );
 
-    assert (
-        index != last &&
-        atValueBefore != atValueAfter
-    ) => (
-        atValueAfter == lastValueBefore
+    assert atValueBefore != atValueAfter => (
+        (
+            removed &&
+            index == last
+        ) || (
+            removed &&
+            atValueAfter == lastValueBefore
+        )
     );
 }

certora/specs/EnumerableSet.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/EnumerableSetHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "EnumerableSetHarness:certora/specs/EnumerableSet.spec"
+}

certora/specs/EnumerableSet.spec

@@ -17,7 +17,7 @@ methods {
 │ Helpers                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-definition sanity() returns bool =
+definition lengthSanity() returns bool =
     length() < max_uint256;
 
 /*
@@ -40,8 +40,13 @@ invariant indexedContained(uint256 index)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant atUniqueness(uint256 index1, uint256 index2)
-    index1 == index2 <=> at_(index1) == at_(index2)
+    (index1 < length() && index2 < length()) =>
+    (index1 == index2 <=> at_(index1) == at_(index2))
     {
+        preserved {
+            requireInvariant consistencyIndex(index1);
+            requireInvariant consistencyIndex(index2);
+        }
         preserved remove(bytes32 key) {
             requireInvariant atUniqueness(index1, require_uint256(length() - 1));
             requireInvariant atUniqueness(index2, require_uint256(length() - 1));
@@ -72,6 +77,9 @@ invariant consistencyKey(bytes32 key)
         at_(require_uint256(_positionOf(key) - 1)) == key
     )
     {
+        preserved {
+            require lengthSanity();
+        }
         preserved remove(bytes32 otherKey) {
             requireInvariant consistencyKey(otherKey);
             requireInvariant atUniqueness(
@@ -81,14 +89,25 @@ invariant consistencyKey(bytes32 key)
         }
     }
 
+invariant absentKeyIsNotStored(bytes32 key, uint256 index)
+    index < length() => (!contains(key) => at_(index) != key)
+    {
+        preserved remove(bytes32 otherKey) {
+            requireInvariant consistencyIndex(index);
+            requireInvariant consistencyKey(key);
+            requireInvariant atUniqueness(index, require_uint256(length() - 1));
+        }
+    }
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rule: state only changes by adding or removing elements                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule stateChange(env e, bytes32 key) {
-    require sanity();
+    require lengthSanity();
     requireInvariant consistencyKey(key);
+    requireInvariant absentKeyIsNotStored(key, require_uint256(length() - 1));
 
     uint256 lengthBefore   = length();
     bool    containsBefore = contains(key);
@@ -142,7 +161,7 @@ rule liveness_2(uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule add(bytes32 key, bytes32 otherKey) {
-    require sanity();
+    require lengthSanity();
 
     uint256 lengthBefore        = length();
     bool    containsBefore      = contains(key);
@@ -175,6 +194,7 @@ rule add(bytes32 key, bytes32 otherKey) {
 rule remove(bytes32 key, bytes32 otherKey) {
     requireInvariant consistencyKey(key);
     requireInvariant consistencyKey(otherKey);
+    requireInvariant indexedContained(require_uint256(length() - 1));
 
     uint256 lengthBefore        = length();
     bool    containsBefore      = contains(key);
@@ -202,7 +222,7 @@ rule remove(bytes32 key, bytes32 otherKey) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule addEnumerability(bytes32 key, uint256 index) {
-    require sanity();
+    require lengthSanity();
 
     bytes32 atBefore = at_(index);
     add(key);
@@ -224,23 +244,29 @@ rule removeEnumerability(bytes32 key, uint256 index) {
     requireInvariant consistencyKey(key);
     requireInvariant consistencyIndex(index);
     requireInvariant consistencyIndex(last);
+    requireInvariant indexedContained(index);
 
     bytes32 atBefore = at_(index);
     bytes32 lastBefore = at_(last);
 
-    remove(key);
+    bool removed = remove(key);
 
-    // can't read last value (length decreased)
+    // can't read last value (length decreased) if an item was removed
     bytes32 atAfter = at_@withrevert(index);
-    assert lastReverted <=> index == last;
-
-    // One value that is allowed to change is if previous value was removed,
-    // in that case the last value before took its place.
-    assert (
-        index != last &&
-        atBefore != atAfter
-    ) => (
-        atBefore == key &&
-        atAfter == lastBefore
+    assert lastReverted <=> (removed && index == last);
+
+    // Cases where a value can change are:
+    // 1. an item was removed and we are looking at the old last index. In that case the reading reverted.
+    // 2. an item was removed and we are looking at its old position. In that case the new value is the old lastValue.
+    // This rule implies that if no item was removed, then atBefore and atAfter must be equal
+    assert atBefore != atAfter => (
+        (
+            removed &&
+            index == last
+        ) || (
+            removed &&
+            atBefore == key &&
+            atAfter == lastBefore
+        )
     );
 }

certora/specs/Initializable.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/InitializableHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "InitializableHarness:certora/specs/Initializable.spec"
+}

certora/specs/Initializable.spec

@@ -31,18 +31,29 @@ definition isDisabled()      returns bool = version() == max_uint64;
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant notInitializing()
-    !initializing();
+    !initializing()
+    filtered { f ->
+        f.selector != sig:nested_init_init().selector &&
+        f.selector != sig:nested_init_reinit(uint64).selector &&
+        f.selector != sig:nested_reinit_init(uint64).selector &&
+        f.selector != sig:nested_reinit_reinit(uint64,uint64).selector
+    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rule: The version cannot decrease & disable state is irrevocable.                                                   │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule increasingVersion(env e) {
+rule increasingVersion(env e, method f) filtered { f ->
+    f.selector != sig:nested_init_init().selector &&
+    f.selector != sig:nested_init_reinit(uint64).selector &&
+    f.selector != sig:nested_reinit_init(uint64).selector &&
+    f.selector != sig:nested_reinit_reinit(uint64,uint64).selector
+} {
     uint64 versionBefore = version();
     bool disabledBefore = isDisabled();
 
-    method f; calldataarg args;
+    calldataarg args;
     f(e, args);
 
     assert versionBefore <= version(), "_initialized must only increase";

certora/specs/Nonces.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/NoncesHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "NoncesHarness:certora/specs/Nonces.spec"
+}

certora/specs/Ownable.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/OwnableHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "OwnableHarness:certora/specs/Ownable.spec"
+}

certora/specs/Ownable2Step.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/Ownable2StepHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "Ownable2StepHarness:certora/specs/Ownable2Step.spec"
+}

certora/specs/Pausable.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harnesses/PausableHarness.sol"
+    ],
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "PausableHarness:certora/specs/Pausable.spec"
+}

certora/specs/TimelockController.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harnesses/TimelockControllerHarness.sol"
+    ],
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "TimelockControllerHarness:certora/specs/TimelockController.spec"
+}

certora/specs/TimelockController.spec

@@ -30,12 +30,20 @@ methods {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 // Uniformly handle scheduling of batched and non-batched operations.
-function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
+function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) returns bool {
     if (f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
         address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
         require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
         schedule@withrevert(e, target, value, data, predecessor, salt, delay);
     } else if (f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) {
+
+        // NOTE: while the "single" correlation requirement works, the prover is not able to deal with the the "batch"
+        // correlation requirement. This requirement is necessary to ensure that the call arguments correspond to the
+        // operation ID that we are observing. This failure, from the prover, to "identify" a set of arguments that
+        // correspond to the operation ID causes vacuity.
+        //
+        // Therefore, this path should not be used for now. Using it will cause the sanity check to fail.
+
         address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt;
         require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
         scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay);
@@ -43,15 +51,24 @@ function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
         calldataarg args;
         f@withrevert(e, args);
     }
+    return !lastReverted;
 }
 
 // Uniformly handle execution of batched and non-batched operations.
-function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) {
+function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) returns bool {
     if (f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector) {
         address target; uint256 value; bytes data; bytes32 salt;
         require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
         execute@withrevert(e, target, value, data, predecessor, salt);
     } else if (f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) {
+
+        // NOTE: while the "single" correlation requirement works, the prover is not able to deal with the the "batch"
+        // correlation requirement. This requirement is necessary to ensure that the call arguments correspond to the
+        // operation ID that we are observing. This failure, from the prover, to "identify" a set of arguments that
+        // correspond to the operation ID causes vacuity.
+        //
+        // Therefore, this path should not be used for now. Using it will cause the sanity check to fail.
+
         address[] targets; uint256[] values; bytes[] payloads; bytes32 salt;
         require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation
         executeBatch@withrevert(e, targets, values, payloads, predecessor, salt);
@@ -59,6 +76,7 @@ function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecesso
         calldataarg args;
         f@withrevert(e, args);
     }
+    return !lastReverted;
 }
 
 /*
@@ -81,46 +99,52 @@ definition state(env e, bytes32 id)     returns uint8 = (isUnset(e, id) ? UNSET(
 │ Invariants: consistency of accessors                                                                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant isOperationCheck(env e, bytes32 id)
-    isOperation(e, id) <=> getTimestamp(id) > 0
-    filtered { f -> !f.isView }
+rule isOperationCheck(env e, bytes32 id) {
+    assert isOperation(e, id) <=> getTimestamp(id) > 0;
+}
 
-invariant isOperationPendingCheck(env e, bytes32 id)
-    isOperationPending(e, id) <=> getTimestamp(id) > DONE_TIMESTAMP()
-    filtered { f -> !f.isView }
+rule isOperationPendingCheck(env e, bytes32 id) {
+    assert isOperationPending(e, id) <=> getTimestamp(id) > DONE_TIMESTAMP();
+}
 
-invariant isOperationDoneCheck(env e, bytes32 id)
-    isOperationDone(e, id) <=> getTimestamp(id) == DONE_TIMESTAMP()
-    filtered { f -> !f.isView }
+rule isOperationDoneCheck(env e, bytes32 id) {
+    assert isOperationDone(e, id) <=> getTimestamp(id) == DONE_TIMESTAMP();
+}
 
-invariant isOperationReadyCheck(env e, bytes32 id)
-    isOperationReady(e, id) <=> (isOperationPending(e, id) && getTimestamp(id) <= e.block.timestamp)
-    filtered { f -> !f.isView }
+rule isOperationReadyCheck(env e, bytes32 id) {
+    assert isOperationReady(e, id) <=> (isOperationPending(e, id) && getTimestamp(id) <= e.block.timestamp);
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: a proposal id is either unset, pending or done                                                           │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant stateConsistency(bytes32 id, env e)
+rule stateConsistency(env e, bytes32 id) {
     // Check states are mutually exclusive
-    (isUnset(e, id)   <=> (!isPending(e, id) && !isDone(e, id)   )) &&
-    (isPending(e, id) <=> (!isUnset(e, id)   && !isDone(e, id)   )) &&
-    (isDone(e, id)    <=> (!isUnset(e, id)   && !isPending(e, id))) &&
+    assert isUnset(e, id)   <=> (!isPending(e, id) && !isDone(e, id)   );
+    assert isPending(e, id) <=> (!isUnset(e, id)   && !isDone(e, id)   );
+    assert isDone(e, id)    <=> (!isUnset(e, id)   && !isPending(e, id));
+
     // Check that the state helper behaves as expected:
-    (isUnset(e, id)   <=> state(e, id) == UNSET()              ) &&
-    (isPending(e, id) <=> state(e, id) == PENDING()            ) &&
-    (isDone(e, id)    <=> state(e, id) == DONE()               ) &&
+    assert isUnset(e, id)   <=> state(e, id) == UNSET();
+    assert isPending(e, id) <=> state(e, id) == PENDING();
+    assert isDone(e, id)    <=> state(e, id) == DONE();
+
     // Check substate
-    isOperationReady(e, id) => isPending(e, id)
-    filtered { f -> !f.isView }
+    assert isOperationReady(e, id) => isPending(e, id);
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rule: state transition rules                                                                                        │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
+rule stateTransition(bytes32 id, env e, method f, calldataarg args) filtered { f ->
+    f.selector != sig:hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32).selector &&
+    f.selector != sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector &&
+    f.selector != sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+} {
     require e.block.timestamp > 1; // Sanity
 
     uint8 stateBefore = state(e, id);
@@ -156,10 +180,13 @@ rule stateTransition(bytes32 id, env e, method f, calldataarg args) {
 │ Rule: minimum delay can only be updated through a timelock execution                                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule minDelayOnlyChange(env e) {
+rule minDelayOnlyChange(env e, method f, calldataarg args) filtered { f ->
+    f.selector != sig:hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32).selector &&
+    f.selector != sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector &&
+    f.selector != sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+} {
     uint256 delayBefore = getMinDelay();
 
-    method f; calldataarg args;
     f(e, args);
 
     assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == sig:updateDelay(uint256).selector), "Unauthorized delay update";
@@ -171,8 +198,8 @@ rule minDelayOnlyChange(env e) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
-    f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector ||
-    f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
+    f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
+// || f.selector == sig:scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector
 } {
     require nonpayable(e);
 
@@ -187,8 +214,7 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
     bool  isDelaySufficient = delay >= getMinDelay();
     bool  isProposerBefore  = hasRole(PROPOSER_ROLE(), e.msg.sender);
 
-    helperScheduleWithRevert(e, f, id, delay);
-    bool success = !lastReverted;
+    bool success = helperScheduleWithRevert(e, f, id, delay);
 
     // liveness
     assert success <=> (
@@ -211,8 +237,8 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
-    f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector ||
-    f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
+    f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector
+// || f.selector == sig:executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector
 } {
     bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId);
 
@@ -221,8 +247,7 @@ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
     bool  isExecutorOrOpen       = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0);
     bool  predecessorDependency  = predecessor == to_bytes32(0) || isDone(e, predecessor);
 
-    helperExecuteWithRevert(e, f, id, predecessor);
-    bool success = !lastReverted;
+    bool success = helperExecuteWithRevert(e, f, id, predecessor);
 
     // The underlying transaction can revert, and that would cause the execution to revert. We can check that all non
     // reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency.

certora/specs/helpers/helpers.spec

@@ -1,6 +1,7 @@
 // environment
+definition nonzero(address account) returns bool = account != 0;
 definition nonpayable(env e) returns bool = e.msg.value == 0;
-definition nonzerosender(env e) returns bool = e.msg.sender != 0;
+definition nonzerosender(env e) returns bool = nonzero(e.msg.sender);
 definition sanity(env e) returns bool = clock(e) > 0 && clock(e) <= max_uint48;
 
 // math

fv-requirements.txt

@@ -1,4 +1,4 @@
-certora-cli==4.13.1
+certora-cli==8.1.1
 # File uses a custom name (fv-requirements.txt) so that it isn't picked by Netlify's build
 # whose latest Python version is 0.3.8, incompatible with most recent versions of Halmos
 halmos==0.3.1