4.8.3

Co-authored-by: Francisco <fg@frang.io>
(cherry picked from commit 8d633cb7d1)

.changeset/angry-ties-switch.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`TimelockController`: Changed the role architecture to use `DEFAULT_ADMIN_ROLE` as the admin for all roles, instead of the bespoke `TIMELOCK_ADMIN_ROLE` that was used previously. This aligns with the general recommendation for `AccessControl` and makes the addition of new roles easier. Accordingly, the `admin` parameter and timelock will now be granted `DEFAULT_ADMIN_ROLE` instead of `TIMELOCK_ADMIN_ROLE`. ([#3799](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3799))

.changeset/beige-ducks-flow.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove deprecated GovernorProposalThreshold module.

.changeset/bright-tomatoes-sing.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`ERC20`, `ERC1155`: Deleted `_beforeTokenTransfer` and `_afterTokenTransfer` hooks, added a new internal `_update` function for customizations, and refactored all extensions using those hooks to use `_update` instead. ([#3838](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3838), [#3876](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3876))

.changeset/chilled-spiders-attack.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`ERC1155Supply`: add a `totalSupply()` function that returns the total amount of token circulating, this change will restrict the total tokens minted across all ids to 2\*\*256-1 .

.changeset/clever-pumas-beg.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`Ownable`: Add an `initialOwner` parameter to the constructor, making the ownership initialization explicit.

.changeset/config.json

@@ -1,12 +0,0 @@
-{
-  "$schema": "https://unpkg.com/@changesets/config@2.3.0/schema.json",
-  "changelog": [
-    "@changesets/changelog-github",
-    {
-      "repo": "OpenZeppelin/openzeppelin-contracts"
-    }
-  ],
-  "commit": false,
-  "access": "public",
-  "baseBranch": "master"
-}

.changeset/dirty-mangos-sort.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Removed presets in favor of [OpenZeppelin Contracts Wizard](https://wizard.openzeppelin.com/).

.changeset/fluffy-gifts-build.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove ERC1820Implementer.

.changeset/fresh-birds-kiss.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`Checkpoints`: library moved from `utils` to `utils/structs`

.changeset/friendly-suits-camp.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove Checkpoints.History.

.changeset/hungry-impalas-perform.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`ERC165Storage`: Removed this contract in favor of inheritance based approach. ([#3880](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3880))

.changeset/mean-walls-watch.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`Nonces`: Added a new contract to keep track of user nonces. Used for signatures in `ERC20Permit`, `ERC20Votes`, and `ERC721Votes`. ([#3816](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3816))

.changeset/new-ways-own.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`ERC20Pausable`, `ERC721Pausable`, `ERC1155Pausable`: Add note regarding missing public pausing functionality

.changeset/rotten-insects-wash.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`ProxyAdmin`: Removed `getProxyAdmin` and `getProxyImplementation` getters. ([#3820](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3820))

.changeset/selfish-queens-rest.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove PullPayment and Escrow contracts (Escrow, ConditionalEscrow, RefundEscrow).

.changeset/short-eels-enjoy.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Bump minimum compiler version required to 0.8.19

.changeset/silly-bees-beam.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`ERC20Votes`: Changed internal vote accounting to reusable `Votes` module previously used by `ERC721Votes`. Removed implicit `ERC20Permit` inheritance. [#3816](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3816)

.changeset/slimy-penguins-attack.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`TransparentUpgradeableProxy`: Removed `admin` and `implementation` getters, which were only callable by the proxy owner and thus not very useful. ([#3820](https://github.com/OpenZeppelin/openzeppelin-contracts/pull/3820))

.changeset/smooth-books-wink.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`ERC1155`: Remove check for address zero in `balanceOf`.

.changeset/spicy-ducks-cough.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove the Timers library.

.changeset/spotty-hotels-type.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`ERC721Consecutive`: Add a `_firstConsecutiveId` internal function that can be overridden to change the id of the first token minted through `_mintConsecutive`.

.changeset/swift-berries-sort.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove ERC777 implementation.

.changeset/tame-geckos-search.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove SafeMath and SignedSafeMath libraries.

.changeset/three-weeks-double.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-Remove CrossChain contracts, including AccessControlCrossChain and all the vendored bridge interfaces.

.changeset/unlucky-snakes-drive.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': patch
----
-
-`Address`: Removed `isContract` because of its ambiguous nature and potential for misuse.

.changeset/wild-windows-trade.md

@@ -1,5 +0,0 @@
----
-'openzeppelin-solidity': major
----
-
-`SafeERC20`: Refactor `safeDecreaseAllowance` and `safeIncreaseAllowance` to support USDT-like tokens.

.eslintrc

@@ -1,20 +1,62 @@
 {
-  "root": true,
   "extends" : [
-    "eslint:recommended",
-    "prettier",
+    "standard"
+  ],
+  "plugins": [
+    "mocha"
   ],
   "env": {
-    "es2022": true,
-    "browser": true,
-    "node": true,
-    "mocha": true,
+    "browser" : true,
+    "node"    : true,
+    "mocha"   : true,
+    "jest"    : true,
   },
   "globals" : {
-    "artifacts": "readonly",
-    "contract": "readonly",
-    "web3": "readonly",
-    "extendEnvironment": "readonly",
-    "expect": "readonly",
+    "artifacts": false,
+    "contract": false,
+    "assert": false,
+    "web3": false,
+    "usePlugin": false,
+    "extendEnvironment": false,
+  },
+  "rules": {
+
+    // Strict mode
+    "strict": ["error", "global"],
+
+    // Code style
+    "array-bracket-spacing": ["off"],
+    "camelcase": ["error", {"properties": "always"}],
+    "comma-dangle": ["error", "always-multiline"],
+    "comma-spacing": ["error", {"before": false, "after": true}],
+    "dot-notation": ["error", {"allowKeywords": true, "allowPattern": ""}],
+    "eol-last": ["error", "always"],
+    "eqeqeq": ["error", "smart"],
+    "generator-star-spacing": ["error", "before"],
+    "indent": ["error", 2],
+    "linebreak-style": ["error", "unix"],
+    "max-len": ["error", 120, 2],
+    "no-debugger": "off",
+    "no-dupe-args": "error",
+    "no-dupe-keys": "error",
+    "no-mixed-spaces-and-tabs": ["error", "smart-tabs"],
+    "no-redeclare": ["error", {"builtinGlobals": true}],
+    "no-trailing-spaces": ["error", { "skipBlankLines": false }],
+    "no-undef": "error",
+    "no-use-before-define": "off",
+    "no-var": "error",
+    "object-curly-spacing": ["error", "always"],
+    "prefer-const": "error",
+    "quotes": ["error", "single"],
+    "semi": ["error", "always"],
+    "space-before-function-paren": ["error", "always"],
+
+    "mocha/no-exclusive-tests": ["error"],
+
+    "promise/always-return": "off",
+    "promise/avoid-new": "off",
+  },
+  "parserOptions": {
+    "ecmaVersion": 2020
   }
 }

.gitattributes

@@ -0,0 +1 @@
+*.sol linguist-language=Solidity

.github/PULL_REQUEST_TEMPLATE.md

@@ -17,4 +17,4 @@ Fixes #???? <!-- Fill in with issue number -->
 
 - [ ] Tests
 - [ ] Documentation
-- [ ] Changeset entry (run `npx changeset add`)
+- [ ] Changelog entry

.github/actions/setup/action.yml

@@ -6,13 +6,14 @@ runs:
     - uses: actions/setup-node@v3
       with:
         node-version: 14.x
+        cache: npm
     - uses: actions/cache@v3
       id: cache
       with:
         path: '**/node_modules'
         key: npm-v3-${{ hashFiles('**/package-lock.json') }}
     - name: Install dependencies
-      run: npm ci
+      run: npm ci --prefer-offline
       shell: bash
       if: steps.cache.outputs.cache-hit != 'true'
       env:

.github/actions/storage-layout/action.yml

@@ -1,55 +0,0 @@
-name: Compare storage layouts
-inputs:
-  token:
-    description: github token
-    required: true
-  buildinfo:
-    description: compilation artifacts
-    required: false
-    default: artifacts/build-info/*.json
-  layout:
-    description: extracted storage layout
-    required: false
-    default: HEAD.layout.json
-  out_layout:
-    description: storage layout to upload
-    required: false
-    default: ${{ github.ref_name }}.layout.json
-  ref_layout:
-    description: storage layout for the reference branch
-    required: false
-    default: ${{ github.base_ref }}.layout.json
-
-runs:
-  using: composite
-  steps:
-    - name: Extract layout
-      run: |
-        node scripts/checks/extract-layout.js ${{ inputs.buildinfo }} > ${{ inputs.layout }}
-      shell: bash
-    - name: Download reference
-      if: github.event_name == 'pull_request'
-      run: |
-        RUN_ID=`gh run list --repo ${{ github.repository }} --branch ${{ github.base_ref }} --workflow ${{ github.workflow }} --limit 100 --json 'conclusion,databaseId,event' --jq 'map(select(.conclusion=="success" and .event!="pull_request"))[0].databaseId'`
-        gh run download ${RUN_ID} --repo ${{ github.repository }} -n layout
-      env:
-        GITHUB_TOKEN: ${{ inputs.token }}
-      shell: bash
-      continue-on-error: true
-      id: reference
-    - name: Compare layouts
-      if: steps.reference.outcome == 'success' && github.event_name == 'pull_request'
-      run: |
-        node scripts/checks/compare-layout.js --head ${{ inputs.layout }} --ref ${{ inputs.ref_layout }}
-      shell: bash
-    - name: Rename artifacts for upload
-      if: github.event_name != 'pull_request'
-      run: |
-        mv ${{ inputs.layout }} ${{ inputs.out_layout }}
-      shell: bash
-    - name: Save artifacts
-      if: github.event_name != 'pull_request'
-      uses: actions/upload-artifact@v3
-      with:
-        name: layout
-        path: ${{ inputs.out_layout }}

.github/workflows/actionlint.yml

@@ -1,18 +0,0 @@
-name: lint workflows
-
-on:
-  pull_request:
-    paths:
-      - '.github/**/*.ya?ml'
-
-jobs:
-  lint:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Add problem matchers
-        run: |
-          # https://github.com/rhysd/actionlint/blob/3a2f2c7/docs/usage.md#problem-matchers
-          curl -LO https://raw.githubusercontent.com/rhysd/actionlint/main/.github/actionlint-matcher.json
-          echo "::add-matcher::actionlint-matcher.json"
-      - uses: docker://rhysd/actionlint:latest

.github/workflows/changelog.yml

@@ -0,0 +1,28 @@
+name: changelog
+
+on:
+  pull_request:
+    types:
+      - opened
+      - synchronize
+      - labeled
+      - unlabeled
+
+concurrency:
+  group: changelog-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    if: ${{ !contains(github.event.pull_request.labels.*.name, 'ignore-changelog') }}
+    steps:
+      - uses: actions/checkout@v3
+      - name: Check diff
+        run: |
+          git fetch origin ${{ github.base_ref }} --depth=1
+          if git diff --exit-code origin/${{ github.base_ref }} -- CHANGELOG.md ; then
+            echo 'Missing changelog entry'
+            exit 1
+          fi
+

.github/workflows/changeset.yml

@@ -1,28 +0,0 @@
-name: changeset
-
-on:
-  pull_request:
-    branches:
-      - master
-    types:
-      - opened
-      - synchronize
-      - labeled
-      - unlabeled
-
-concurrency:
-  group: changeset-${{ github.ref }}
-  cancel-in-progress: true
-
-jobs:
-  check:
-    runs-on: ubuntu-latest
-    if: ${{ !contains(github.event.pull_request.labels.*.name, 'ignore-changeset') }}
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 0 # Include history so Changesets finds merge-base
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - name: Check changeset
-        run: npx changeset status --since=origin/${{ github.base_ref }}

.github/workflows/checks.yml

@@ -4,7 +4,6 @@ on:
   push:
     branches:
       - master
-      - next-v*
       - release-v*
   pull_request: {}
   workflow_dispatch: {}
@@ -15,6 +14,7 @@ concurrency:
 
 jobs:
   lint:
+    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -26,7 +26,6 @@ jobs:
     runs-on: ubuntu-latest
     env:
       FORCE_COLOR: 1
-      NODE_OPTIONS: --max_old_space_size=4096
       GAS: true
     steps:
       - uses: actions/checkout@v3
@@ -37,36 +36,15 @@ jobs:
       - name: Check linearisation of the inheritance graph
         run: npm run test:inheritance
       - name: Check proceduraly generated contracts are up-to-date
+        if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
         run: npm run test:generation
       - name: Compare gas costs
         uses: ./.github/actions/gas-compare
         with:
           token: ${{ github.token }}
 
-  tests-upgradeable:
-    runs-on: ubuntu-latest
-    env:
-      FORCE_COLOR: 1
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 0 # Include history so patch conflicts are resolved automatically
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - name: Transpile to upgradeable
-        run: bash scripts/upgradeable/transpile.sh
-      - name: Run tests
-        run: npm run test
-        env:
-          NODE_OPTIONS: --max_old_space_size=4096
-      - name: Check linearisation of the inheritance graph
-        run: npm run test:inheritance
-      - name: Check storage layout
-        uses: ./.github/actions/storage-layout
-        with:
-          token: ${{ github.token }}
-
-  tests-foundry:
+  foundry-tests:
+    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -80,6 +58,7 @@ jobs:
         run: forge test -vv
 
   coverage:
+    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -89,27 +68,23 @@ jobs:
         env:
           NODE_OPTIONS: --max_old_space_size=4096
       - uses: codecov/codecov-action@v3
-        with:
-          token: ${{ secrets.CODECOV_TOKEN }}
 
   slither:
+    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
       - name: Set up environment
         uses: ./.github/actions/setup
-      - run: rm foundry.toml
-      - uses: crytic/slither-action@v0.3.0
-        with:
-          node-version: 18.15
+      - uses: crytic/slither-action@v0.2.0
 
   codespell:
+    if: github.repository != 'OpenZeppelin/openzeppelin-contracts-upgradeable'
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
       - name: Run CodeSpell
-        uses: codespell-project/actions-codespell@v2.0
+        uses: codespell-project/actions-codespell@v1.0
         with:
-          check_hidden: true
           check_filenames: true
-          skip: package-lock.json,*.pdf
+          skip: package-lock.json

.github/workflows/formal-verification.yml

@@ -1,68 +0,0 @@
-name: formal verification
-
-on:
-  pull_request:
-    types:
-      - opened
-      - reopened
-      - synchronize
-      - labeled
-  workflow_dispatch: {}
-
-env:
-  PIP_VERSION: '3.10'
-  JAVA_VERSION: '11'
-  SOLC_VERSION: '0.8.19'
-
-concurrency: ${{ github.workflow }}-${{ github.ref }}
-
-jobs:
-  apply-diff:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Apply patches
-        run: make -C certora apply
-
-  verify:
-    runs-on: ubuntu-latest
-    if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification')
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 0
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - name: identify specs that need to be run
-        id: arguments
-        run: |
-          if [[ ${{ github.event_name }} = 'pull_request' ]];
-          then
-            RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done | tr "\n" " ")
-          else
-            RESULT='--all'
-          fi
-          echo "result=$RESULT" >> "$GITHUB_OUTPUT"
-      - name: Install python
-        uses: actions/setup-python@v4
-        with:
-          python-version: ${{ env.PIP_VERSION }}
-          cache: 'pip'
-      - name: Install python packages
-        run: pip install -r requirements.txt
-      - name: Install java
-        uses: actions/setup-java@v3
-        with:
-          distribution: temurin
-          java-version: ${{ env.JAVA_VERSION }}
-      - name: Install solc
-        run: |
-          wget https://github.com/ethereum/solidity/releases/download/v${{ env.SOLC_VERSION }}/solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc
-          chmod +x /usr/local/bin/solc
-      - name: Verify specification
-        run: |
-          make -C certora apply
-          node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
-        env:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.github/workflows/release-cycle.yml

@@ -1,214 +0,0 @@
-#  D: Manual Dispatch
-#  M: Merge release PR
-#  C: Commit
-#  ┌───────────┐     ┌─────────────┐     ┌────────────────┐
-#  │Development├──D──►RC-Unreleased│  ┌──►Final-Unreleased│
-#  └───────────┘     └─┬─────────▲─┘  │  └─┬────────────▲─┘
-#                      │         │    │    │            │
-#                      M         C    D    M            C
-#                      │         │    │    │            │
-#                     ┌▼─────────┴┐   │   ┌▼────────────┴┐
-#                     │RC-Released├───┘   │Final-Released│
-#                     └───────────┘       └──────────────┘
-name: Release Cycle
-
-on:
-  push:
-    branches:
-      - release-v*
-  workflow_dispatch: {}
-
-concurrency: ${{ github.workflow }}-${{ github.ref }}
-
-jobs:
-  state:
-    name: Check state
-    permissions:
-      pull-requests: read
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - id: state
-        name: Get state
-        uses: actions/github-script@v6
-        env:
-          TRIGGERING_ACTOR: ${{ github.triggering_actor }}
-        with:
-          result-encoding: string
-          script: await require('./scripts/release/workflow/state.js')({ github, context, core })
-    outputs:
-      # Job Flags
-      start: ${{ steps.state.outputs.start }}
-      changesets: ${{ steps.state.outputs.changesets }}
-      promote: ${{ steps.state.outputs.promote }}
-      publish: ${{ steps.state.outputs.publish }}
-      merge: ${{ steps.state.outputs.merge }}
-
-      # Global variables
-      is_prerelease: ${{ steps.state.outputs.is_prerelease }}
-
-  start:
-    needs: state
-    name: Start new release candidate
-    permissions:
-      contents: write
-      actions: write
-    if: needs.state.outputs.start == 'true'
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - run: bash scripts/git-user-config.sh
-      - id: start
-        name: Create branch with release candidate
-        run: bash scripts/release/workflow/start.sh
-      - name: Re-run workflow
-        uses: actions/github-script@v6
-        env:
-          REF: ${{ steps.start.outputs.branch }}
-        with:
-          script: await require('./scripts/release/workflow/rerun.js')({ github, context })
-
-  promote:
-    needs: state
-    name: Promote to final release
-    permissions:
-      contents: write
-      actions: write
-    if: needs.state.outputs.promote == 'true'
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - run: bash scripts/git-user-config.sh
-      - name: Exit prerelease state
-        if: needs.state.outputs.is_prerelease == 'true'
-        run: bash scripts/release/workflow/exit-prerelease.sh
-      - name: Re-run workflow
-        uses: actions/github-script@v6
-        with:
-          script: await require('./scripts/release/workflow/rerun.js')({ github, context })
-
-  changesets:
-    needs: state
-    name: Update PR to release
-    permissions:
-      contents: write
-      pull-requests: write
-    if: needs.state.outputs.changesets == 'true'
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 0 # To get all tags
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - name: Set release title
-        uses: actions/github-script@v6
-        with:
-          result-encoding: string
-          script: await require('./scripts/release/workflow/set-changesets-pr-title.js')({ core })
-      - name: Create PR
-        uses: changesets/action@v1
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-          PRERELEASE: ${{ needs.state.outputs.is_prerelease }}
-        with:
-          version: npm run version
-          title: ${{ env.TITLE }}
-          commit: ${{ env.TITLE }}
-          body: | # Wait for support on this https://github.com/changesets/action/pull/250
-            This is an automated PR for releasing ${{ github.repository }}
-            Check [CHANGELOG.md](${{ github.repository }}/CHANGELOG.md)
-
-  publish:
-    needs: state
-    name: Publish to npm
-    environment: npm
-    permissions:
-      contents: write
-    if: needs.state.outputs.publish == 'true'
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - id: pack
-        name: Pack
-        run: bash scripts/release/workflow/pack.sh
-        env:
-          PRERELEASE: ${{ needs.state.outputs.is_prerelease }}
-      - name: Upload tarball artifact
-        uses: actions/upload-artifact@v3
-        with:
-          name: ${{ github.ref_name }}
-          path: ${{ steps.pack.outputs.tarball }}
-      - name: Tag
-        run: npx changeset tag
-      - name: Publish
-        run: bash scripts/release/workflow/publish.sh
-        env:
-          NPM_TOKEN: ${{ secrets.NPM_TOKEN }}
-          TARBALL: ${{ steps.pack.outputs.tarball }}
-          TAG: ${{ steps.pack.outputs.tag }}
-      - name: Push tags
-        run: git push --tags
-      - name: Create Github Release
-        uses: actions/github-script@v6
-        env:
-          PRERELEASE: ${{ needs.state.outputs.is_prerelease }}
-        with:
-          script: await require('./scripts/release/workflow/github-release.js')({ github, context })
-    outputs:
-      tarball_name: ${{ steps.pack.outputs.tarball_name }}
-
-  integrity_check:
-    needs: publish
-    name: Tarball Integrity Check
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - name: Download tarball artifact
-        id: artifact
-        # Replace with actions/upload-artifact@v3 when
-        # https://github.com/actions/download-artifact/pull/194 gets released
-        uses: actions/download-artifact@e9ef242655d12993efdcda9058dee2db83a2cb9b
-        with:
-          name: ${{ github.ref_name }}
-      - name: Check integrity
-        run: bash scripts/release/workflow/integrity-check.sh
-        env:
-          TARBALL: ${{ steps.artifact.outputs.download-path }}/${{ needs.publish.outputs.tarball_name }}
-
-  merge:
-    needs: state
-    name: Create PR back to master
-    permissions:
-      contents: write
-      pull-requests: write
-    if: needs.state.outputs.merge == 'true'
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 0 # All branches
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - run: bash scripts/git-user-config.sh
-      - name: Create branch to merge
-        run: bash scripts/release/workflow/prepare-release-merge.sh
-      - name: Create PR back to master
-        uses: actions/github-script@v6
-        with:
-          script: |
-            await github.rest.pulls.create({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              head: 'merge/${{ github.ref_name }}',
-              base: 'master',
-              title: '${{ format('Merge {0} branch', github.ref_name) }}'
-            });

.github/workflows/upgradeable.yml

@@ -1,4 +1,4 @@
-name: transpile upgradeable
+name: Upgradeable Trigger
 
 on:
   push:
@@ -7,24 +7,17 @@ on:
       - release-v*
 
 jobs:
-  transpile:
-    environment: push-upgradeable
+  trigger:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - id: app
+        uses: getsentry/action-github-app-token@v1
         with:
-          repository: OpenZeppelin/openzeppelin-contracts-upgradeable
-          fetch-depth: 0
-          token: ${{ secrets.GH_TOKEN_UPGRADEABLE }}
-      - name: Fetch current non-upgradeable branch
-        run: |
-          git fetch "https://github.com/${{ github.repository }}.git" "$REF"
-          git checkout FETCH_HEAD
-        env:
-          REF: ${{ github.ref }}
-      - name: Set up environment
-        uses: ./.github/actions/setup
-      - run: bash scripts/git-user-config.sh
-      - name: Transpile to upgradeable
-        run: bash scripts/upgradeable/transpile-onto.sh ${{ github.ref_name }} origin/${{ github.ref_name }}
-      - run: git push origin ${{ github.ref_name }}
+          app_id: ${{ secrets.UPGRADEABLE_APP_ID }}
+          private_key: ${{ secrets.UPGRADEABLE_APP_PK }}
+      - run: |
+          curl -X POST \
+            https://api.github.com/repos/OpenZeppelin/openzeppelin-contracts-upgradeable/dispatches \
+            -H 'Accept: application/vnd.github.v3+json' \
+            -H 'Authorization: token ${{ steps.app.outputs.token }}' \
+            -d '{ "event_type": "Update", "client_payload": { "ref": "${{ github.ref }}" } }'

.gitignore

@@ -54,18 +54,11 @@ allFiredEvents
 .coverage_cache
 .coverage_contracts
 
-# hardat-exposed
-contracts-exposed
-
-# Hardhat
-/cache
-/artifacts
-
-# Foundry
-/out
+# hardhat
+cache
+artifacts
 
 # Certora
 .certora*
 .last_confs
 certora_*
-.zip-output-url.txt

.gitmodules

@@ -2,6 +2,3 @@
 	branch = v1
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
-[submodule "lib/erc4626-tests"]
-	path = lib/erc4626-tests
-	url = https://github.com/a16z/erc4626-tests.git

.prettierrc

@@ -1,13 +1,13 @@
 {
-  "printWidth": 120,
   "singleQuote": true,
   "trailingComma": "all",
-  "arrowParens": "avoid",
   "overrides": [
     {
       "files": "*.sol",
       "options": {
-        "singleQuote": false
+        "singleQuote": false,
+        "printWidth": 120,
+        "explicitTypes": "always"
       }
     }
   ]

.solcover.js

@@ -1,13 +1,15 @@
 module.exports = {
-  norpc: true,
-  testCommand: 'npm test',
-  compileCommand: 'npm run compile',
-  skipFiles: ['mocks'],
-  providerOptions: {
-    default_balance_ether: '10000000000000000000000000',
-  },
-  mocha: {
-    fgrep: '[skip-on-coverage]',
-    invert: true,
-  },
-};
+    norpc: true,
+    testCommand: 'npm test',
+    compileCommand: 'npm run compile',
+    skipFiles: [
+        'mocks',
+    ],
+    providerOptions: {
+        default_balance_ether: '10000000000000000000000000',
+    },
+    mocha: {
+        fgrep: '[skip-on-coverage]',
+        invert: true,
+    },
+}

CODE_OF_CONDUCT.md

@@ -55,7 +55,7 @@ further defined and clarified by project maintainers.
 ## Enforcement
 
 Instances of abusive, harassing, or otherwise unacceptable behavior may be
-reported by contacting the project team at contact@openzeppelin.com. All
+reported by contacting the project team at maintainers@openzeppelin.org. All
 complaints will be reviewed and investigated and will result in a response that
 is deemed necessary and appropriate to the circumstances. The project team is
 obligated to maintain confidentiality with regard to the reporter of an incident.

CONTRIBUTING.md

@@ -1,36 +1,64 @@
-# Contributing Guidelines
+Contributing to OpenZeppelin Contracts
+=======
 
-There are many ways to contribute to OpenZeppelin Contracts.
+We really appreciate and value contributions to OpenZeppelin Contracts. Please take 5' to review the items listed below to make sure that your contributions are merged as soon as possible.
 
-## Troubleshooting
+## Contribution guidelines
 
-You can help other users in the community to solve their smart contract issues in the [OpenZeppelin Forum].
+Smart contracts manage value and are highly vulnerable to errors and attacks. We have very strict [guidelines], please make sure to review them!
 
-[OpenZeppelin Forum]: https://forum.openzeppelin.com/
+## Creating Pull Requests (PRs)
 
-## Opening an issue
+As a contributor, you are expected to fork this repository, work on your own fork and then submit pull requests. The pull requests will be reviewed and eventually merged into the main repo. See ["Fork-a-Repo"](https://help.github.com/articles/fork-a-repo/) for how this works.
 
-You can [open an issue] to suggest a feature or report a minor bug. For serious bugs please do not open an issue, instead refer to our [security policy] for appropriate steps.
+## A typical workflow
 
-If you believe your issue may be due to user error and not a problem in the library, consider instead posting a question on the [OpenZeppelin Forum].
+1) Make sure your fork is up to date with the main repository:
 
-Before opening an issue, be sure to search through the existing open and closed issues, and consider posting a comment in one of those instead.
+```
+cd openzeppelin-contracts
+git remote add upstream https://github.com/OpenZeppelin/openzeppelin-contracts.git
+git fetch upstream
+git pull --rebase upstream master
+```
+NOTE: The directory `openzeppelin-contracts` represents your fork's local copy.
 
-When requesting a new feature, include as many details as you can, especially around the use cases that motivate it. Features are prioritized according to the impact they may have on the ecosystem, so we appreciate information showing that the impact could be high.
+2) Branch out from `master` into `fix/some-bug-#123`:
+(Postfixing #123 will associate your PR with the issue #123 and make everyone's life easier =D)
+```
+git checkout -b fix/some-bug-#123
+```
 
-[security policy]: https://github.com/OpenZeppelin/openzeppelin-contracts/security
-[open an issue]: https://github.com/OpenZeppelin/openzeppelin-contracts/issues/new/choose
+3) Make your changes, add your files, commit, and push to your fork.
 
-## Submitting a pull request
+```
+git add SomeFile.js
+git commit "Fix some bug #123"
+git push origin fix/some-bug-#123
+```
 
-If you would like to contribute code or documentation you may do so by forking the repository and submitting a pull request.
+4) Run tests, linter, etc. This can be done by running local continuous integration and make sure it passes.
 
-Any non-trivial code contribution must be first discussed with the maintainers in an issue (see [Opening an issue](#opening-an-issue)). Only very minor changes are accepted without prior discussion.
+```bash
+npm test
+npm run lint
+```
 
-Make sure to read and follow the [engineering guidelines](./GUIDELINES.md). Run linter and tests to make sure your pull request is good before submitting it.
+5) Go to [github.com/OpenZeppelin/openzeppelin-contracts](https://github.com/OpenZeppelin/openzeppelin-contracts) in your web browser and issue a new pull request.
 
-Changelog entries should be added to each pull request by using [Changesets](https://github.com/changesets/changesets/).
+*IMPORTANT* Read the PR template very carefully and make sure to follow all the instructions. These instructions
+refer to some very important conditions that your PR must meet in order to be accepted, such as making sure that all tests pass, JS linting tests pass, Solidity linting tests pass, etc.
 
-When opening the pull request you will be presented with a template and a series of instructions. Read through it carefully and follow all the steps. Expect a review and feedback from the maintainers afterwards.
+6) Maintainers will review your code and possibly ask for changes before your code is pulled in to the main repository. We'll check that all tests pass, review the coding style, and check for general code correctness. If everything is OK, we'll merge your pull request and your code will be part of OpenZeppelin Contracts.
 
-If you're looking for a good place to start, look for issues labelled ["good first issue"](https://github.com/OpenZeppelin/openzeppelin-contracts/labels/good%20first%20issue)!
+*IMPORTANT* Please pay attention to the maintainer's feedback, since it's a necessary step to keep up with the standards OpenZeppelin Contracts attains to.
+
+## All set!
+
+If you have any questions, feel free to post them to github.com/OpenZeppelin/openzeppelin-contracts/issues.
+
+Finally, if you're looking to collaborate and want to find easy tasks to start, look at the issues we marked as ["Good first issue"](https://github.com/OpenZeppelin/openzeppelin-contracts/labels/good%20first%20issue).
+
+Thanks for your time and code!
+
+[guidelines]: GUIDELINES.md

GUIDELINES.md

@@ -1,117 +1,105 @@
-# Engineering Guidelines
+Design Guidelines
+=======
 
-## Testing
+These are some global design goals in OpenZeppelin Contracts.
 
-Code must be thoroughly tested with quality unit tests.
+#### D0 - Security in Depth
+We strive to provide secure, tested, audited code. To achieve this, we need to match intention with function. Thus, documentation, code clarity, community review and security discussions are fundamental.
 
-We defer to the [Moloch Testing Guide](https://github.com/MolochVentures/moloch/tree/master/test#readme) for specific recommendations, though not all of it is relevant here. Note the introduction:
+#### D1 - Simple and Modular
+Simpler code means easier audits, and better understanding of what each component does. We look for small files, small contracts, and small functions. If you can separate a contract into two independent functionalities you should probably do it.
 
-> Tests should be written, not only to verify correctness of the target code, but to be comprehensively reviewed by other programmers. Therefore, for mission critical Solidity code, the quality of the tests are just as important (if not more so) than the code itself, and should be written with the highest standards of clarity and elegance.
+#### D2 - Naming Matters
 
-Every addition or change to the code must come with relevant and comprehensive tests.
+We take our time with picking names. Code is going to be written once, and read hundreds of times. Renaming for clarity is encouraged.
 
-Refactors should avoid simultaneous changes to tests.
+#### D3 - Tests
 
-Flaky tests are not acceptable.
+Write tests for all your code. We encourage Test Driven Development so we know when our code is right. Even though not all code in the repository is tested at the moment, we aim to test every line of code in the future.
 
-The test suite should run automatically for every change in the repository, and in pull requests tests must pass before merging.
+#### D4 - Check preconditions and post-conditions
 
-The test suite coverage must be kept as close to 100% as possible, enforced in pull requests.
+A very important way to prevent vulnerabilities is to catch a contract’s inconsistent state as early as possible. This is why we want functions to check pre- and post-conditions for executing its logic. When writing code, ask yourself what you are expecting to be true before and after the function runs, and express it in code.
 
-In some cases unit tests may be insufficient and complementary techniques should be used:
+#### D5 - Code Consistency
 
-1. Property-based tests (aka. fuzzing) for math-heavy code.
-2. Formal verification for state machines.
+Consistency on the way classes are used is paramount to an easier understanding of the library. The codebase should be as unified as possible. Read existing code and get inspired before you write your own. Follow the style guidelines. Don’t hesitate to ask for help on how to best write a specific piece of code.
 
-## Code style
+#### D6 - Regular Audits
+Following good programming practices is a way to reduce the risk of vulnerabilities, but professional code audits are still needed. We will perform regular code audits on major releases, and hire security professionals to provide independent review.
 
-Solidity code should be written in a consistent format enforced by a linter, following the official [Solidity Style Guide](https://docs.soliditylang.org/en/latest/style-guide.html). See below for further [Solidity Conventions](#solidity-conventions).
+# Style Guidelines
 
-The code should be simple and straightforward, prioritizing readability and understandability. Consistency and predictability should be maintained across the codebase. In particular, this applies to naming, which should be systematic, clear, and concise.
+The design guidelines have quite a high abstraction level. These style guidelines are more concrete and easier to apply, and also more opinionated. We value clean code and consistency, and those are prerequisites for us to include new code in the repository. Before proposing a change, please read these guidelines and take some time to familiarize yourself with the style of the existing codebase.
 
-Sometimes these guidelines may be broken if doing so brings significant efficiency gains, but explanatory comments should be added.
+## Solidity code
 
-Modularity should be pursued, but not at the cost of the above priorities.
+In order to be consistent with all the other Solidity projects, we follow the
+[official recommendations documented in the Solidity style guide](http://solidity.readthedocs.io/en/latest/style-guide.html).
 
-## Documentation
+Any exception or additions specific to our project are documented below.
 
-For contributors, project guidelines and processes must be documented publicly.
-
-For users, features must be abundantly documented. Documentation should include answers to common questions, solutions to common problems, and recommendations for critical decisions that the user may face.
-
-All changes to the core codebase (excluding tests, auxiliary scripts, etc.) must be documented in a changelog, except for purely cosmetic or documentation changes.
-
-## Peer review
-
-All changes must be submitted through pull requests and go through peer code review.
-
-The review must be approached by the reviewer in a similar way as if it was an audit of the code in question (but importantly it is not a substitute for and should not be considered an audit).
-
-Reviewers should enforce code and project guidelines.
-
-External contributions must be reviewed separately by multiple maintainers.
-
-## Automation
-
-Automation should be used as much as possible to reduce the possibility of human error and forgetfulness.
-
-Automations that make use of sensitive credentials must use secure secret management, and must be strengthened against attacks such as [those on GitHub Actions worklows](https://github.com/nikitastupin/pwnhub).
-
-Some other examples of automation are:
-
-- Looking for common security vulnerabilities or errors in our code (eg. reentrancy analysis).
-- Keeping dependencies up to date and monitoring for vulnerable dependencies.
-
-## Pull requests
-
-Pull requests are squash-merged to keep the `master` branch history clean. The title of the pull request becomes the commit message, so it should be written in a consistent format:
-
-1) Begin with a capital letter.
-2) Do not end with a period.
-3) Write in the imperative: "Add feature X" and not "Adds feature X" or "Added feature X".
-
-This repository does not follow conventional commits, so do not prefix the title with "fix:" or "feat:".
-
-Work in progress pull requests should be submitted as Drafts and should not be prefixed with "WIP:".
-
-Branch names don't matter, and commit messages within a pull request mostly don't matter either, although they can help the review process.
-
-# Solidity Conventions
-
-In addition to the official Solidity Style Guide we have a number of other conventions that must be followed.
+* Try to avoid acronyms and abbreviations.
 
 * All state variables should be private.
 
-  Changes to state should be accompanied by events, and in some cases it is not correct to arbitrarily set state. Encapsulating variables as private and only allowing modification via setters enables us to ensure that events and other rules are followed reliably and prevents this kind of user error.
+* Private state variables should have an underscore prefix.
 
-* Internal or private state variables or functions should have an underscore prefix.
-
-  ```solidity
-  contract TestContract {
+    ```
+    contract TestContract {
       uint256 private _privateVar;
       uint256 internal _internalVar;
-      function _testInternal() internal { ... }
-      function _testPrivate() private { ... }
-  }
-  ```
+    }
+    ```
+
+* Parameters must not be prefixed with an underscore.
+
+    ```
+    function test(uint256 testParameter1, uint256 testParameter2) {
+    ...
+    }
+    ```
+
+* Internal and private functions should have an underscore prefix.
+
+    ```
+    function _testInternal() internal {
+      ...
+    }
+    ```
+
+    ```
+    function _testPrivate() private {
+      ...
+    }
+    ```
 
 * Events should be emitted immediately after the state change that they
-  represent, and should be named in the past tense.
+  represent, and consequently they should be named in past tense.
 
-  ```solidity
-  function _burn(address who, uint256 value) internal {
+    ```
+    function _burn(address who, uint256 value) internal {
       super._burn(who, value);
       emit TokensBurned(who, value);
-  }
-  ```
+    }
+    ```
 
   Some standards (e.g. ERC20) use present tense, and in those cases the
-  standard specification is used.
+  standard specification prevails.
   
 * Interface names should have a capital I prefix.
 
-  ```solidity
-  interface IERC777 {
-  ```
+    ```
+    interface IERC777 {
+    ```
 
-* Unchecked arithmetic blocks should contain comments explaining why overflow is guaranteed not to happen. If the reason is immediately apparent from the line above the unchecked block, the comment may be omitted.
+
+## Tests
+
+* Tests Must be Written Elegantly
+
+    Tests are a good way to show how to use the library, and maintaining them is extremely necessary. Don't write long tests, write helper functions to make them be as short and concise as possible (they should take just a few lines each), and use good variable names.
+
+* Tests Must not be Random
+
+    Inputs for tests should not be generated randomly. Accounts used to create test contracts are an exception, those can be random. Also, the type and structure of outputs should be checked.

LICENSE

@@ -1,6 +1,6 @@
 The MIT License (MIT)
 
-Copyright (c) 2016-2023 zOS Global Limited and contributors
+Copyright (c) 2016-2022 zOS Global Limited and contributors
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the

README.md

@@ -1,13 +1,9 @@
-> **Warning**
-> Version 5.0 is under active development. The code in this branch is not recommended for use.
-
 # <img src="logo.svg" alt="OpenZeppelin" height="40px">
 
+[![Docs](https://img.shields.io/badge/docs-%F0%9F%93%84-blue)](https://docs.openzeppelin.com/contracts)
 [![NPM Package](https://img.shields.io/npm/v/@openzeppelin/contracts.svg)](https://www.npmjs.org/package/@openzeppelin/contracts)
 [![Coverage Status](https://codecov.io/gh/OpenZeppelin/openzeppelin-contracts/graph/badge.svg)](https://codecov.io/gh/OpenZeppelin/openzeppelin-contracts)
-[![GitPOAPs](https://public-api.gitpoap.io/v1/repo/OpenZeppelin/openzeppelin-contracts/badge)](https://www.gitpoap.io/gh/OpenZeppelin/openzeppelin-contracts)
-[![Docs](https://img.shields.io/badge/docs-%F0%9F%93%84-yellow)](https://docs.openzeppelin.com/contracts)
-[![Forum](https://img.shields.io/badge/forum-%F0%9F%92%AC-yellow)](https://docs.openzeppelin.com/contracts)
+[![gitpoap badge](https://public-api.gitpoap.io/v1/repo/OpenZeppelin/openzeppelin-contracts/badge)](https://www.gitpoap.io/gh/OpenZeppelin/openzeppelin-contracts)
 
 **A library for secure smart contract development.** Build on a solid foundation of community-vetted code.
 
@@ -23,7 +19,7 @@
 
 ### Installation
 
-```
+```console
 $ npm install @openzeppelin/contracts
 ```
 
@@ -36,7 +32,7 @@ An alternative to npm is to use the GitHub repository (`openzeppelin/openzeppeli
 Once installed, you can use the contracts in the library by importing them:
 
 ```solidity
-pragma solidity ^0.8.19;
+pragma solidity ^0.8.0;
 
 import "@openzeppelin/contracts/token/ERC721/ERC721.sol";
 
@@ -56,6 +52,7 @@ The guides in the [documentation site](https://docs.openzeppelin.com/contracts)
 
 * [Access Control](https://docs.openzeppelin.com/contracts/access-control): decide who can perform each of the actions on your system.
 * [Tokens](https://docs.openzeppelin.com/contracts/tokens): create tradeable assets or collectives, and distribute them via [Crowdsales](https://docs.openzeppelin.com/contracts/crowdsales).
+* [Gas Station Network](https://docs.openzeppelin.com/contracts/gsn): let your users interact with your contracts without having to pay for gas themselves.
 * [Utilities](https://docs.openzeppelin.com/contracts/utilities): generic useful tools including non-overflowing math, signature verification, and trustless paying systems.
 
 The [full API](https://docs.openzeppelin.com/contracts/api/token/ERC20) is also thoroughly documented, and serves as a great reference when developing your smart contract application. You can also ask for help or follow Contracts's development in the [community forum](https://forum.openzeppelin.com).
@@ -68,17 +65,15 @@ Finally, you may want to take a look at the [guides on our blog](https://blog.op
 
 ## Security
 
-This project is maintained by [OpenZeppelin](https://openzeppelin.com) with the goal of providing a secure and reliable library of smart contract components for the ecosystem. We address security through risk management in various areas such as engineering and open source best practices, scoping and API design, multi-layered review processes, and incident response preparedness.
+This project is maintained by [OpenZeppelin](https://openzeppelin.com), and developed following our high standards for code quality and security. OpenZeppelin Contracts is meant to provide tested and community-audited code, but please use common sense when doing anything that deals with real money! We take no responsibility for your implementation decisions and any security problems you might experience.
 
-The security policy is detailed in [`SECURITY.md`](./SECURITY.md), and specifies how you can report security vulnerabilities, which versions will receive security patches, and how to stay informed about them. We run a [bug bounty program on Immunefi](https://immunefi.com/bounty/openzeppelin) to reward the responsible disclosure of vulnerabilities.
+The core development principles and strategies that OpenZeppelin Contracts is based on include: security in depth, simple and modular code, clarity-driven naming conventions, comprehensive unit testing, pre-and-post-condition sanity checks, code consistency, and regular audits.
 
-The engineering guidelines we follow to promote project quality can be found in [`GUIDELINES.md`](./GUIDELINES.md).
+The latest audit was done on October 2018 on version 2.0.0.
 
-Past audits can be found in [`audits/`](./audits).
+We have a [**bug bounty program** on Immunefi](https://www.immunefi.com/bounty/openzeppelin). Please report any security issues you find through the Immunefi dashboard, or reach out to security@openzeppelin.com.
 
-Smart contracts are a nascent technology and carry a high level of technical risk and uncertainty. Although OpenZeppelin is well known for its security audits, using OpenZeppelin Contracts is not a substitute for a security audit.
-
-OpenZeppelin Contracts is made available under the MIT License, which disclaims all warranties in relation to the project and which limits the liability of those that contribute and maintain the project, including OpenZeppelin. As set out further in the Terms, you acknowledge that you are solely responsible for any use of OpenZeppelin Contracts and you assume all risks associated with any such use.
+Critical bug fixes will be backported to past major releases.
 
 ## Contribute
 
@@ -87,7 +82,3 @@ OpenZeppelin Contracts exists thanks to its contributors. There are many ways yo
 ## License
 
 OpenZeppelin Contracts is released under the [MIT License](LICENSE).
-
-## Legal
-
-Your use of this Project is governed by the terms found at www.openzeppelin.com/tos (the "Terms").

RELEASING.md

@@ -1,47 +1,36 @@
 # Releasing
 
-> Visit the documentation for [details about release schedule](https://docs.openzeppelin.com/contracts/releases-stability).
+> Visit the documentation for [details about release schedule].
 
-OpenZeppelin Contracts uses a fully automated release process that takes care of compiling, packaging, and publishing the library, all of which is carried out in a clean CI environment (GitHub Actions), implemented in the ([`release-cycle`](.github/workflows/release-cycle.yml)) workflow. This helps to reduce the potential for human error and inconsistencies, and ensures that the release process is ongoing and reliable.
+Start on an up-to-date `master` branch.
 
-## Changesets
+Create the release branch with `npm run release start minor`.
 
-[Changesets](https://github.com/changesets/changesets/) is used as part of our release process for `CHANGELOG.md` management. Each change that is relevant for the codebase is expected to include a changeset.
+Publish a release candidate with `npm run release rc`.
 
-## Branching model
+Publish the final release with `npm run release final`.
 
-The release cycle happens on release branches called `release-vX.Y`. Each of these branches starts as a release candidate (rc) and is eventually promoted to final.
+Follow the general [OpenZeppelin Contracts release checklist].
 
-A release branch can be updated with cherry-picked patches from `master`, or may sometimes be committed to directly in the case of old releases. These commits will lead to a new release candidate or a patch increment depending on the state of the release branch.
+[details about release schedule]: https://docs.openzeppelin.com/contracts/releases-stability
+[OpenZeppelin Contracts release checklist]: https://github.com/OpenZeppelin/code-style/blob/master/RELEASE_CHECKLIST.md
 
-```mermaid
-  %%{init: {'gitGraph': {'mainBranchName': 'master'}} }%%
-  gitGraph
-    commit id: "Feature A"
-    commit id: "Feature B"
-    branch release-vX.Y
-    commit id: "Start release"
-    commit id: "Release vX.Y.0-rc.0"
 
-    checkout master
-    commit id: "Feature C"
-    commit id: "Fix A"
+## Merging the release branch
 
-    checkout release-vX.Y
-    cherry-pick id: "Fix A" tag: ""
-    commit id: "Release vX.Y.0-rc.1"
-    commit id: "Release vX.Y.0"
+After the final release, the release branch should be merged back into `master`. This merge must not be squashed because it would lose the tagged release commit. Since the GitHub repo is set up to only allow squashed merges, the merge should be done locally and pushed.
 
-    checkout master
-    merge release-vX.Y
-    commit id: "Feature D"
-    commit id: "Patch B"
+Make sure to have the latest changes from `upstream` in your local release branch.
 
-    checkout release-vX.Y
-    cherry-pick id: "Patch B" tag: ""
-    commit id: "Release vX.Y.1"
-    
-    checkout master
-    merge release-vX.Y
-    commit id: "Feature E"
 ```
+git checkout release-vX.Y.Z
+git pull upstream
+```
+
+```
+git checkout master
+git merge --no-ff release-vX.Y.Z
+git push upstream master
+```
+
+The release branch can then be deleted on GitHub.

SECURITY.md

@@ -1,42 +1,20 @@
 # Security Policy
 
-Security vulnerabilities should be disclosed to the project maintainers through [Immunefi], or alternatively by email to security@openzeppelin.com.
-
-[Immunefi]: https://immunefi.com/bounty/openzeppelin
-
 ## Bug Bounty
 
-Responsible disclosure of security vulnerabilities is rewarded through a bug bounty program on [Immunefi].
+We have a [**bug bounty program** on Immunefi](https://www.immunefi.com/bounty/openzeppelin). Please report any security issues you find through the Immunefi dashboard, or reach out to security@openzeppelin.com.
 
-There is a bonus reward for issues introduced in release candidates that are reported before making it into a stable release.
+Critical bug fixes will be backported to past major releases.
 
-## Security Patches
+## Supported Versions
 
-Security vulnerabilities will be patched as soon as responsibly possible, and published as an advisory on this repository (see [advisories]) and on the affected npm packages.
+The recommendation is to use the latest version available.
 
-[advisories]: https://github.com/OpenZeppelin/openzeppelin-contracts/security/advisories
+| Version | Supported                            |
+| ------- | ------------------------------------ |
+| 4.x     | :white_check_mark::white_check_mark: |
+| 3.4     | :white_check_mark:                   |
+| 2.5     | :white_check_mark:                   |
+| < 2.0   | :x:                                  |
 
-Projects that build on OpenZeppelin Contracts are encouraged to clearly state, in their source code and websites, how to be contacted about security issues in the event that a direct notification is considered necessary. We recommend including it in the NatSpec for the contract as `/// @custom:security-contact security@example.com`.
-
-Additionally, we recommend installing the library through npm and setting up vulnerability alerts such as [Dependabot].
-
-[Dependabot]: https://docs.github.com/en/code-security/supply-chain-security/understanding-your-software-supply-chain/about-supply-chain-security#what-is-dependabot
-
-### Supported Versions
-
-Security patches will be released for the latest minor of a given major release. For example, if an issue is found in versions >=4.6.0 and the latest is 4.8.0, the patch will be released only in version 4.8.1.
-
-Only critical severity bug fixes will be backported to past major releases.
-
-| Version | Critical security fixes | Other security fixes |
-| ------- | ----------------------- | -------------------- |
-| 4.x     | :white_check_mark:      | :white_check_mark:   |
-| 3.4     | :white_check_mark:      | :x:                  |
-| 2.5     | :white_check_mark:      | :x:                  |
-| < 2.0   | :x:                     | :x:                  |
-
-Note as well that the Solidity language itself only guarantees security updates for the latest release.
-
-## Legal
-
-Smart contracts are a nascent techology and carry a high level of technical risk and uncertainty.  OpenZeppelin Contracts is made available under the MIT License, which disclaims all warranties in relation to the project and which limits the liability of those that contribute and maintain the project, including OpenZeppelin. Your use of the project is also governed by the terms found at www.openzeppelin.com/tos (the "Terms"). As set out in the Terms, you are solely responsible for any use of OpenZeppelin Contracts and you assume all risks associated with any such use. This Security Policy in no way evidences or represents an on-going duty by any contributor, including OpenZeppelin, to correct any flaws or alert you to all or any of the potential risks of utilizing the project.
+Note that the Solidity language itself only guarantees security updates for the latest release.

audit/2017-03.md

@@ -1,6 +1,6 @@
 # OpenZeppelin Audit
 
-NOTE ON 2021-07-19: This report makes reference to Zeppelin, OpenZeppelin, OpenZeppelin Contracts, the OpenZeppelin team, and OpenZeppelin library. Many of these things have since been renamed and know that this audit applies to what is currently called the OpenZeppelin Contracts which are maintained by the OpenZeppelin Contracts Community.
+NOTE ON 2021-07-19: This report makes reference to Zeppelin, OpenZeppelin, OpenZeppelin [C]ontracts, the OpenZeppelin team, and OpenZeppelin library. Many of these things have since been renamed and know that this audit applies to what is currently called the OpenZeppelin Contracts which are maintained by the OpenZeppelin Conracts Community.
 
 March, 2017
 Authored by Dennis Peterson and Peter Vessenes

audits/README.md

@@ -1,16 +0,0 @@
-# Audits
-
-| Date         | Version | Commit    | Auditor      | Scope                | Links                                                       |
-| ------------ | ------- | --------- | ------------ | -------------------- | ----------------------------------------------------------- |
-| May 2023     | v4.9.0  | `91df66c` | OpenZeppelin | v4.9 Changes         | [🔗](./2023-05-v4.9.pdf)                                    |
-| October 2022 | v4.8.0  | `14f98db` | OpenZeppelin | ERC4626, Checkpoints | [🔗](./2022-10-ERC4626.pdf) [🔗](./2022-10-Checkpoints.pdf) |
-| October 2018 | v2.0.0  | `dac5bcc` | LevelK       | Everything           | [🔗](./2018-10.pdf)                                         |
-| March 2017   | v1.0.4  | `9c5975a` | New Alchemy  | Everything           | [🔗](./2017-03.md)                                          |
-
-# Formal Verification
-
-| Date         | Version | Commit    | Tool    | Scope                                                                                                                            | Links                                |
-| ------------ | ------- | --------- | ------- | -------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------ |
-| May 2022     | v4.7.0  | `109778c` | Certora | Initializable, GovernorPreventLateQuorum, ERC1155Burnable, ERC1155Pausable, ERC1155Supply, ERC1155Holder, ERC1155Receiver        | [🔗](../certora/reports/2022-05.pdf) |
-| March 2022   | v4.4.0  | `4088540` | Certora | ERC20Votes, ERC20FlashMint, ERC20Wrapper, TimelockController, ERC721Votes, Votes, AccessControl, ERC1155                         | [🔗](../certora/reports/2022-03.pdf) |
-| October 2021 | v4.4.0  | `4088540` | Certora | Governor, GovernorCountingSimple, GovernorProposalThreshold, GovernorTimelockControl, GovernorVotes, GovernorVotesQuorumFraction | [🔗](../certora/reports/2021-10.pdf) |

certora/.gitignore

@@ -1 +0,0 @@
-patched

certora/Makefile

@@ -1,54 +1,24 @@
 default: help
 
-SRC   := ../contracts
-DST   := patched
-DIFF  := diff
-SRCS  := $(shell find $(SRC) -type f)
-DSTS  := $(shell find $(DST) -type f)
-DIFFS := $(shell find $(DIFF) -type f)
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../contracts
+MUNGED_DIR    = munged
 
-###############################################################################
-# Apply all patches in the $DIFF folder to the $DST folder
-apply: $(DST) $(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$(DIFFS)))
-
-# Reset the $DST folder
-$(DST): FORCE
-	@rm -rf $@
-	@cp -r $(SRC) $@
-
-# Update a solidity file in the $DST directory using the corresponding patch
-$(DST)/%.sol: FORCE
-	@echo Applying patch to $@
-	@patch -p0 -d $(DST) < $(patsubst $(DST)_%,$(DIFF)/%.patch,$(subst /,_,$@))
-
-###############################################################################
-# Record all difference between $SRC and $DST in patches
-record: $(DIFF) $(patsubst %,$(DIFF)/%.patch,$(subst /,_,$(subst $(SRC)/,,$(SRCS)) $(subst $(DST)/,,$(DSTS))))
-
-# Create the $DIFF folder
-$(DIFF): FORCE
-	@rm -rf $@
-	@mkdir $@
-
-# Create the patch file by comparing the source and the destination
-$(DIFF)/%.patch: FORCE
-	@echo Generating patch $@
-	@diff -ruN \
-		$(patsubst $(DIFF)/%.patch,$(SRC)/%,$(subst _,/,$@)) \
-		$(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$@)) \
-		| sed 's+$(SRC)/++g' \
-		| sed 's+$(DST)/++g' \
-		> $@
-	@[ -s $@ ] || rm $@
-
-###############################################################################
 help:
 	@echo "usage:"
-	@echo "  make apply:  create $(DST) directory by applying the patches to $(SRC)"
-	@echo "  make record: record the patches capturing the differences between $(SRC) and $(DST)"
 	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
 
 clean:
 	git clean -fdX
+	touch $(PATCH)
 
-FORCE: ;

certora/README.md

@@ -1,60 +1,56 @@
 # Running the certora verification tool
 
-These instructions detail the process for running Certora Verification Tool on OpenZeppelin Contracts.
+These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts.
 
-Documentation for CVT and the specification language are available [here](https://certora.atlassian.net/wiki/spaces/CPD/overview).
-
-## Prerequisites
-
-Follow the [Certora installation guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) in order to get the Certora Prover Package and the `solc` executable folder in your path.
-
-> **Note**
-> An API Key is required for local testing. Although the prover will run on a Github Actions' CI environment on selected Pull Requests.
+Documentation for CVT and the specification language are available
+[here](https://certora.atlassian.net/wiki/spaces/CPD/overview)
 
 ## Running the verification
 
-The Certora Verification Tool proves specs for contracts, which are defined by the `./specs.json` file along with their pre-configured options.
+The scripts in the `certora/scripts` directory are used to submit verification
+jobs to the Certora verification service. After the job is complete, the results will be available on
+[the Certora portal](https://vaas-stg.certora.com/).
 
-The verification script `./run.js` is used to submit verification jobs to the Certora Verification service.
+These scripts should be run from the root directory; for example by running
 
-You can run it from the root of the repository with the following command:
-
-```bash
-node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...]
+```
+sh certora/scripts/verifyAll.sh <meaningful comment>
 ```
 
-Where:
+The most important of these is `verifyAll.sh`, which checks
+all of the harnessed contracts (`certora/harness/Wizard*.sol`) against all of
+the specifications (`certora/spec/*.spec`).
 
-- `CONTRACT_NAME` matches the `contract` key in the `./spec.json` file and may be empty. It will run all matching contracts if not provided.
-- `SPEC_NAME` refers to a `spec` key from the `./specs.json` file. It will run every spec if not provided.
-- `OPTIONS` extend the [Certora Prover CLI options](https://docs.certora.com/en/latest/docs/prover/cli/options.html#certora-prover-cli-options) and will respect the preconfigured options in the `specs.json` file.
+The other scripts run a subset of the specifications or the contracts.  You can
+verify different contracts or specifications by changing the `--verify` option,
+and you can run a single rule or method with the `--rule` or `--method` option.
 
-> **Note**
-> A single spec may be configured to run for multiple contracts, whereas a single contract may run multiple specs.
+For example, to verify the `WizardFirstPriority` contract against the
+`GovernorCountingSimple` specification, you could change the `--verify` line of
+the `WizardControlFirstPriortity.sh` script to:
 
-Example usage:
-
-```bash
-node certora/run.js AccessControl # Run the AccessControl spec against every contract implementing it
+```
+--verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \
 ```
 
 ## Adapting to changes in the contracts
 
-Some of our rules require the code to be simplified in various ways. Our primary tool for performing these simplifications is to run verification on a contract that extends the original contracts and overrides some of the methods. These "harness" contracts can be found in the `certora/harness` directory.
+Some of our rules require the code to be simplified in various ways. Our
+primary tool for performing these simplifications is to run verification on a
+contract that extends the original contracts and overrides some of the methods.
+These "harness" contracts can be found in the `certora/harness` directory.
 
-This pattern does require some modifications to the original code: some methods need to be made virtual or public, for example. These changes are handled by applying a patch
-to the code before verification by running:
+This pattern does require some modifications to the original code: some methods
+need to be made virtual or public, for example. These changes are handled by
+applying a patch to the code before verification.
 
-```bash
-make -C certora apply
-```
+When one of the `verify` scripts is executed, it first applies the patch file
+`certora/applyHarness.patch` to the `contracts` directory, placing the output
+in the `certora/munged` directory. We then verify the contracts in the
+`certora/munged` directory.
 
-Before running the `certora/run.js` script, it's required to apply the corresponding patches to the `contracts` directory, placing the output in the `certora/patched` directory. Then, the contracts are verified by running the verification for the `certora/patched` directory.
-
-If the original contracts change, it is possible to create a conflict with the patch. In this case, the verify scripts will report an error message and output rejected changes in the `patched` directory. After merging the changes, run `make record` in the `certora` directory; this will regenerate the patch file, which can then be checked into git.
-
-For more information about the `make` scripts available, run:
-
-```bash
-make -C certora help
-```
+If the original contracts change, it is possible to create a conflict with the
+patch. In this case, the verify scripts will report an error message and output
+rejected changes in the `munged` directory. After merging the changes, run
+`make record` in the `certora` directory; this will regenerate the patch file,
+which can then be checked into git.

certora/applyHarness.patch

@@ -0,0 +1,101 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1969-12-31 19:00:00.000000000 -0500
++++ .gitignore	2021-12-09 14:46:33.923637220 -0500
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol
+--- governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-09 14:46:33.923637220 -0500
+@@ -245,7 +245,7 @@
+     /**
+      * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
+      */
+-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
++    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
+         ProposalDetails storage details = _proposalDetails[proposalId];
+         return quorum(proposalSnapshot(proposalId)) <= details.forVotes;
+     }
+@@ -253,7 +253,7 @@
+     /**
+      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
+      */
+-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
++    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
+         ProposalDetails storage details = _proposalDetails[proposalId];
+         return details.forVotes > details.againstVotes;
+     }
+diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
+--- governance/extensions/GovernorCountingSimple.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/extensions/GovernorCountingSimple.sol	2021-12-09 14:46:33.923637220 -0500
+@@ -64,7 +64,7 @@
+     /**
+      * @dev See {Governor-_quorumReached}.
+      */
+-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
++    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
+         ProposalVote storage proposalvote = _proposalVotes[proposalId];
+ 
+         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
+@@ -73,7 +73,7 @@
+     /**
+      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
+      */
+-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
++    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
+         ProposalVote storage proposalvote = _proposalVotes[proposalId];
+ 
+         return proposalvote.forVotes > proposalvote.againstVotes;
+diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol
+--- governance/extensions/GovernorTimelockControl.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/extensions/GovernorTimelockControl.sol	2021-12-09 14:46:33.923637220 -0500
+@@ -111,7 +111,7 @@
+         bytes[] memory calldatas,
+         bytes32 descriptionHash
+     ) internal virtual override {
+-        _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
++         _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
+     }
+ 
+     /**
+diff -ruN governance/Governor.sol governance/Governor.sol
+--- governance/Governor.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/Governor.sol	2021-12-09 14:46:56.411503587 -0500
+@@ -38,8 +38,8 @@
+ 
+     string private _name;
+ 
+-    mapping(uint256 => ProposalCore) private _proposals;
+-
++    mapping(uint256 => ProposalCore) public _proposals;
++ 
+     /**
+      * @dev Restrict access to governor executing address. Some module might override the _executor function to make
+      * sure this modifier is consistent with the execution model.
+@@ -167,12 +167,12 @@
+     /**
+      * @dev Amount of votes already cast passes the threshold limit.
+      */
+-    function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
++    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+ 
+     /**
+      * @dev Is the proposal successful or not.
+      */
+-    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
++    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+ 
+     /**
+      * @dev Register a vote with a given support and voting weight.
+diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
+--- token/ERC20/extensions/ERC20Votes.sol	2021-12-03 15:24:56.527654330 -0500
++++ token/ERC20/extensions/ERC20Votes.sol	2021-12-09 14:46:33.927637196 -0500
+@@ -84,7 +84,7 @@
+      *
+      * - `blockNumber` must have been already mined
+      */
+-    function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) {
++    function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) {
+         require(blockNumber < block.number, "ERC20Votes: block not yet mined");
+         return _checkpointsLookup(_checkpoints[account], blockNumber);
+     }

certora/diff/token_ERC721_ERC721.sol.patch

@@ -1,14 +0,0 @@
---- token/ERC721/ERC721.sol	2023-03-07 10:48:47.736822221 +0100
-+++ token/ERC721/ERC721.sol	2023-03-09 19:49:39.669338673 +0100
-@@ -199,6 +199,11 @@
-         return _owners[tokenId];
-     }
- 
-+    // FV
-+    function _getApproved(uint256 tokenId) internal view returns (address) {
-+        return _tokenApprovals[tokenId];
-+    }
-+
-     /**
-      * @dev Returns whether `tokenId` exists.
-      *

certora/harnesses/AccessControlDefaultAdminRulesHarness.sol

@@ -1,47 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/access/AccessControlDefaultAdminRules.sol";
-
-contract AccessControlDefaultAdminRulesHarness is AccessControlDefaultAdminRules {
-    uint48 private _delayIncreaseWait;
-
-    constructor(
-        uint48 initialDelay,
-        address initialDefaultAdmin,
-        uint48 delayIncreaseWait
-    ) AccessControlDefaultAdminRules(initialDelay, initialDefaultAdmin) {
-        _delayIncreaseWait = delayIncreaseWait;
-    }
-
-    // FV
-    function pendingDefaultAdmin_() external view returns (address) {
-        (address newAdmin, ) = pendingDefaultAdmin();
-        return newAdmin;
-    }
-
-    function pendingDefaultAdminSchedule_() external view returns (uint48) {
-        (, uint48 schedule) = pendingDefaultAdmin();
-        return schedule;
-    }
-
-    function pendingDelay_() external view returns (uint48) {
-        (uint48 newDelay, ) = pendingDefaultAdminDelay();
-        return newDelay;
-    }
-
-    function pendingDelaySchedule_() external view returns (uint48) {
-        (, uint48 schedule) = pendingDefaultAdminDelay();
-        return schedule;
-    }
-
-    function delayChangeWait_(uint48 newDelay) external view returns (uint48) {
-        return _delayChangeWait(newDelay);
-    }
-
-    // Overrides
-    function defaultAdminDelayIncreaseWait() public view override returns (uint48) {
-        return _delayIncreaseWait;
-    }
-}

certora/harnesses/AccessControlHarness.sol

@@ -1,7 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/access/AccessControl.sol";
-
-contract AccessControlHarness is AccessControl {}

certora/harnesses/DoubleEndedQueueHarness.sol

@@ -1,59 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/utils/structs/DoubleEndedQueue.sol";
-
-contract DoubleEndedQueueHarness {
-    using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque;
-
-    DoubleEndedQueue.Bytes32Deque private _deque;
-
-    function pushFront(bytes32 value) external {
-        _deque.pushFront(value);
-    }
-
-    function pushBack(bytes32 value) external {
-        _deque.pushBack(value);
-    }
-
-    function popFront() external returns (bytes32 value) {
-        return _deque.popFront();
-    }
-
-    function popBack() external returns (bytes32 value) {
-        return _deque.popBack();
-    }
-
-    function clear() external {
-        _deque.clear();
-    }
-
-    function begin() external view returns (int128) {
-        return _deque._begin;
-    }
-
-    function end() external view returns (int128) {
-        return _deque._end;
-    }
-
-    function length() external view returns (uint256) {
-        return _deque.length();
-    }
-
-    function empty() external view returns (bool) {
-        return _deque.empty();
-    }
-
-    function front() external view returns (bytes32 value) {
-        return _deque.front();
-    }
-
-    function back() external view returns (bytes32 value) {
-        return _deque.back();
-    }
-
-    function at_(uint256 index) external view returns (bytes32 value) {
-        return _deque.at(index);
-    }
-}

certora/harnesses/ERC20FlashMintHarness.sol

@@ -1,36 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/token/ERC20/ERC20.sol";
-import "../patched/token/ERC20/extensions/ERC20Permit.sol";
-import "../patched/token/ERC20/extensions/ERC20FlashMint.sol";
-
-contract ERC20FlashMintHarness is ERC20, ERC20Permit, ERC20FlashMint {
-    uint256 someFee;
-    address someFeeReceiver;
-
-    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
-
-    function mint(address account, uint256 amount) external {
-        _mint(account, amount);
-    }
-
-    function burn(address account, uint256 amount) external {
-        _burn(account, amount);
-    }
-
-    // public accessor
-    function flashFeeReceiver() public view returns (address) {
-        return someFeeReceiver;
-    }
-
-    // internal hook
-    function _flashFee(address, uint256) internal view override returns (uint256) {
-        return someFee;
-    }
-
-    function _flashFeeReceiver() internal view override returns (address) {
-        return someFeeReceiver;
-    }
-}

certora/harnesses/ERC20PermitHarness.sol

@@ -1,17 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/token/ERC20/extensions/ERC20Permit.sol";
-
-contract ERC20PermitHarness is ERC20Permit {
-    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
-
-    function mint(address account, uint256 amount) external {
-        _mint(account, amount);
-    }
-
-    function burn(address account, uint256 amount) external {
-        _burn(account, amount);
-    }
-}

certora/harnesses/ERC20VotesHarness.sol

@@ -0,0 +1,28 @@
+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesHarness is ERC20Votes {
+    constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
+
+    mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
+
+    function _afterTokenTransfer(
+        address from,
+        address to,
+        uint256 amount
+    ) internal virtual override {
+        super._afterTokenTransfer(from, to, amount);
+        _getPastVotes[from][block.number] -= amount;
+        _getPastVotes[to][block.number] += amount;
+    }
+
+    /**
+     * @dev Change delegation for `delegator` to `delegatee`.
+     *
+     * Emits events {DelegateChanged} and {DelegateVotesChanged}.
+     */
+    function _delegate(address delegator, address delegatee) internal virtual override{
+        super._delegate(delegator, delegatee);
+        _getPastVotes[delegator][block.number] -= balanceOf(delegator);
+        _getPastVotes[delegatee][block.number] += balanceOf(delegator);
+    }
+}

certora/harnesses/ERC20WrapperHarness.sol

@@ -1,25 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
-
-contract ERC20WrapperHarness is ERC20Wrapper {
-    constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) 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/ERC3156FlashBorrowerHarness.sol

@@ -1,13 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-import "../patched/interfaces/IERC3156FlashBorrower.sol";
-
-pragma solidity ^0.8.19;
-
-contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower {
-    bytes32 somethingToReturn;
-
-    function onFlashLoan(address, address, uint256, uint256, bytes calldata) external view override returns (bytes32) {
-        return somethingToReturn;
-    }
-}

certora/harnesses/ERC721Harness.sol

@@ -1,37 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/token/ERC721/ERC721.sol";
-
-contract ERC721Harness is ERC721 {
-    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
-
-    function mint(address account, uint256 tokenId) external {
-        _mint(account, tokenId);
-    }
-
-    function safeMint(address to, uint256 tokenId) external {
-        _safeMint(to, tokenId);
-    }
-
-    function safeMint(address to, uint256 tokenId, bytes memory data) external {
-        _safeMint(to, tokenId, data);
-    }
-
-    function burn(uint256 tokenId) external {
-        _burn(tokenId);
-    }
-
-    function tokenExists(uint256 tokenId) external view returns (bool) {
-        return _exists(tokenId);
-    }
-
-    function unsafeOwnerOf(uint256 tokenId) external view returns (address) {
-        return _ownerOf(tokenId);
-    }
-
-    function unsafeGetApproved(uint256 tokenId) external view returns (address) {
-        return _getApproved(tokenId);
-    }
-}

certora/harnesses/ERC721ReceiverHarness.sol

@@ -1,11 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/interfaces/IERC721Receiver.sol";
-
-contract ERC721ReceiverHarness is IERC721Receiver {
-    function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
-        return this.onERC721Received.selector;
-    }
-}

certora/harnesses/EnumerableMapHarness.sol

@@ -1,55 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/utils/structs/EnumerableMap.sol";
-
-contract EnumerableMapHarness {
-    using EnumerableMap for EnumerableMap.Bytes32ToBytes32Map;
-
-    EnumerableMap.Bytes32ToBytes32Map private _map;
-
-    function set(bytes32 key, bytes32 value) public returns (bool) {
-        return _map.set(key, value);
-    }
-
-    function remove(bytes32 key) public returns (bool) {
-        return _map.remove(key);
-    }
-
-    function contains(bytes32 key) public view returns (bool) {
-        return _map.contains(key);
-    }
-
-    function length() public view returns (uint256) {
-        return _map.length();
-    }
-
-    function key_at(uint256 index) public view returns (bytes32) {
-        (bytes32 key,) = _map.at(index);
-        return key;
-    }
-
-    function value_at(uint256 index) public view returns (bytes32) {
-        (,bytes32 value) = _map.at(index);
-        return value;
-    }
-
-    function tryGet_contains(bytes32 key) public view returns (bool) {
-        (bool contained,) = _map.tryGet(key);
-        return contained;
-    }
-
-    function tryGet_value(bytes32 key) public view returns (bytes32) {
-        (,bytes32 value) = _map.tryGet(key);
-        return value;
-    }
-
-    function get(bytes32 key) public view returns (bytes32) {
-        return _map.get(key);
-    }
-
-    function _indexOf(bytes32 key) public view returns (uint256) {
-        return _map._keys._inner._indexes[key];
-    }
-}

certora/harnesses/EnumerableSetHarness.sol

@@ -1,35 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/utils/structs/EnumerableSet.sol";
-
-contract EnumerableSetHarness {
-    using EnumerableSet for EnumerableSet.Bytes32Set;
-
-    EnumerableSet.Bytes32Set private _set;
-
-    function add(bytes32 value) public returns (bool) {
-        return _set.add(value);
-    }
-
-    function remove(bytes32 value) public returns (bool) {
-        return _set.remove(value);
-    }
-
-    function contains(bytes32 value) public view returns (bool) {
-        return _set.contains(value);
-    }
-
-    function length() public view returns (uint256) {
-        return _set.length();
-    }
-
-    function at_(uint256 index) public view returns (bytes32) {
-        return _set.at(index);
-    }
-
-    function _indexOf(bytes32 value) public view returns (uint256) {
-        return _set._inner._indexes[value];
-    }
-}

certora/harnesses/InitializableHarness.sol

@@ -1,23 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.19;
-
-import "../patched/proxy/utils/Initializable.sol";
-
-contract InitializableHarness is Initializable {
-    function initialize()          public initializer      {}
-    function reinitialize(uint8 n) public reinitializer(n) {}
-    function disable()             public { _disableInitializers(); }
-
-    function nested_init_init()                     public initializer      { initialize();    }
-    function nested_init_reinit(uint8 m)            public initializer      { reinitialize(m); }
-    function nested_reinit_init(uint8 n)            public reinitializer(n) { initialize();    }
-    function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); }
-
-    function version() public view returns (uint8) {
-        return _getInitializedVersion();
-    }
-
-    function initializing() public view returns (bool) {
-        return _isInitializing();
-    }
-}

certora/harnesses/Ownable2StepHarness.sol

@@ -1,9 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/access/Ownable2Step.sol";
-
-contract Ownable2StepHarness is Ownable2Step {
-  function restricted() external onlyOwner {}
-}

certora/harnesses/OwnableHarness.sol

@@ -1,9 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/access/Ownable.sol";
-
-contract OwnableHarness is Ownable {
-  function restricted() external onlyOwner {}
-}

certora/harnesses/PausableHarness.sol

@@ -1,19 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-pragma solidity ^0.8.19;
-
-import "../patched/security/Pausable.sol";
-
-contract PausableHarness is Pausable {
-    function pause() external {
-        _pause();
-    }
-
-    function unpause() external {
-        _unpause();
-    }
-
-    function onlyWhenPaused() external whenPaused {}
-
-    function onlyWhenNotPaused() external whenNotPaused {}
-}

certora/harnesses/TimelockControllerHarness.sol

@@ -1,12 +0,0 @@
-pragma solidity ^0.8.19;
-
-import "../patched/governance/TimelockController.sol";
-
-contract TimelockControllerHarness is TimelockController {
-    constructor(
-        uint256 minDelay,
-        address[] memory proposers,
-        address[] memory executors,
-        address admin
-    ) TimelockController(minDelay, proposers, executors, admin) {}
-}

certora/harnesses/WizardControlFirstPriority.sol

@@ -0,0 +1,150 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/governance/extensions/GovernorTimelockControl.sol";
+import "../munged/governance/extensions/GovernorProposalThreshold.sol";
+
+/* 
+Wizard options:
+ProposalThreshhold = 10
+ERC20Votes
+TimelockController
+*/
+
+contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
+    constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
+        Governor(name)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumFraction)
+        GovernorTimelockControl(_timelock)
+    {}
+
+    //HARNESS
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    uint256 _votingDelay;
+
+    uint256 _votingPeriod;
+
+    uint256 _proposalThreshold;
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason
+    ) internal override virtual returns (uint256) {
+        
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;        
+    }
+    
+    function snapshot(uint256 proposalId) public view returns (uint64) {
+        return _proposals[proposalId].voteStart._deadline;
+    }
+
+
+    function getExecutor() public view returns (address){
+        return _executor();
+    }
+
+    // original code, harnessed
+
+    function votingDelay() public view override returns (uint256) {     // HARNESS: pure -> view
+        return _votingDelay;                                            // HARNESS: parametric
+    }
+
+    function votingPeriod() public view override returns (uint256) {    // HARNESS: pure -> view
+        return _votingPeriod;                                           // HARNESS: parametric
+    }
+
+    function proposalThreshold() public view override returns (uint256) {   // HARNESS: pure -> view
+        return _proposalThreshold;                                          // HARNESS: parametric
+    }
+
+    // original code, not harnessed
+    // The following functions are overrides required by Solidity.
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function getVotes(address account, uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotes)
+        returns (uint256)
+    {
+        return super.getVotes(account, blockNumber);
+    }
+
+    function state(uint256 proposalId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (ProposalState)
+    {
+        return super.state(proposalId);
+    }
+
+    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
+        public
+        override(Governor, GovernorProposalThreshold, IGovernor)
+        returns (uint256)
+    {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockControl)
+    {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockControl)
+        returns (uint256)
+    {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor()
+        internal
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (address)
+    {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/harnesses/WizardFirstTry.sol

@@ -0,0 +1,141 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/governance/extensions/GovernorTimelockCompound.sol";
+
+/* 
+Wizard options:
+ERC20Votes
+TimelockCompound
+*/
+
+contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
+    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
+        Governor(name)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumFraction)
+        GovernorTimelockCompound(_timelock)
+    {}
+
+    //HARNESS
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    function snapshot(uint256 proposalId) public view returns (uint64) {
+        return _proposals[proposalId].voteStart._deadline;
+    }
+
+    function getExecutor() public view returns (address){
+        return _executor();
+    }
+
+    uint256 _votingDelay;
+
+    uint256 _votingPeriod;
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason
+    ) internal override virtual returns (uint256) {
+        
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;        
+    }
+
+    // original code, harnessed
+
+    function votingDelay() public view override virtual returns (uint256) {     // HARNESS: pure -> view
+        return _votingDelay;                                                    // HARNESS: parametric
+    }
+
+    function votingPeriod() public view override virtual returns (uint256) {    // HARNESS: pure -> view
+        return _votingPeriod;                                                   // HARNESS: parametric
+    }
+
+    // original code, not harnessed
+    // The following functions are overrides required by Solidity.
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function getVotes(address account, uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotes)
+        returns (uint256)
+    {
+        return super.getVotes(account, blockNumber);
+    }
+
+    function state(uint256 proposalId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (ProposalState)
+    {
+        return super.state(proposalId);
+    }
+
+    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
+        public
+        override(Governor, IGovernor)
+        returns (uint256)
+    {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+    {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+        returns (uint256)
+    {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor()
+        internal
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (address)
+    {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/munged/.gitignore

@@ -0,0 +1,2 @@
+*
+!.gitignore

certora/run.js

@@ -1,146 +0,0 @@
-#!/usr/bin/env node
-
-// USAGE:
-//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
-// EXAMPLES:
-//    node certora/run.js --all
-//    node certora/run.js AccessControl
-//    node certora/run.js AccessControlHarness:AccessControl
-
-const proc = require('child_process');
-const { PassThrough } = require('stream');
-const events = require('events');
-
-const argv = require('yargs')
-  .env('')
-  .options({
-    all: {
-      alias: 'a',
-      type: 'boolean',
-    },
-    spec: {
-      alias: 's',
-      type: 'string',
-      default: __dirname + '/specs.json',
-    },
-    parallel: {
-      alias: 'p',
-      type: 'number',
-      default: 4,
-    },
-    options: {
-      alias: 'o',
-      type: 'array',
-      default: [],
-    },
-  }).argv;
-
-function match(entry, request) {
-  const [reqSpec, reqContract] = request.split(':').reverse();
-  return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
-}
-
-const specs = require(argv.spec).filter(s => argv.all || argv._.some(r => match(s, r)));
-const limit = require('p-limit')(argv.parallel);
-
-if (argv._.length == 0 && !argv.all) {
-  console.error(`Warning: No specs requested. Did you forgot 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.flatMap(opt => opt.split(' ')), ...argv.options]);
-}
-
-// 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];
-  const child = proc.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 events.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 ? ':x:' : ':heavy_check_mark:',
-      url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error',
-      url ? `[link](${url})` : 'error',
-    ),
-  );
-}

certora/scripts/Governor.sh

@@ -0,0 +1,10 @@
+make -C certora munged
+
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
+    --verify GovernorHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.0 \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule voteStartBeforeVoteEnd \
+    --msg "$1"

certora/scripts/GovernorCountingSimple-counting.sh

@@ -0,0 +1,10 @@
+make -C certora munged
+
+certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
+    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
+    --solc solc8.2 \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule hasVotedCorrelation \
+    --msg "$1"

certora/scripts/WizardControlFirstPriority.sh

@@ -0,0 +1,12 @@
+make -C certora munged
+
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
+    --link WizardControlFirstPriority:token=ERC20VotesHarness \
+    --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --disableLocalTypeChecking \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule canVoteDuringVotingPeriod \
+    --msg "$1"

certora/scripts/WizardFirstTry.sh

@@ -0,0 +1,10 @@
+make -C certora munged
+
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
+    --verify WizardFirstTry:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --disableLocalTypeChecking \
+    --settings -copyLoopUnroll=4 \
+    --msg "$1"

certora/scripts/sanity.sh

@@ -0,0 +1,14 @@
+make -C certora munged
+
+for f in certora/harnesses/Wizard*.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+    --solc solc8.2 --staging shelly/forSasha \
+    --optimistic_loop \
+    --msg "checking sanity on ${file%.*}"
+    --settings -copyLoopUnroll=4
+done

certora/scripts/verifyAll.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+
+make -C certora munged
+
+for contract in certora/harnesses/Wizard*.sol;
+do
+    for spec in certora/specs/*.spec;
+    do      
+        contractFile=$(basename $contract)
+        specFile=$(basename $spec)
+        if [[ "${specFile%.*}" != "RulesInProgress" ]];
+        then
+            echo "Processing ${contractFile%.*} with $specFile"
+            if [[ "${contractFile%.*}" = *"WizardControl"* ]];
+            then
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --link ${contractFile%.*}:token=ERC20VotesHarness \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc8.2 \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            else
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc8.2 \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            fi
+        fi
+    done
+done

certora/specs.json

@@ -1,86 +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": "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"]
-  }
-]

certora/specs/AccessControl.spec

@@ -1,126 +0,0 @@
-import "helpers/helpers.spec"
-import "methods/IAccessControl.spec"
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Definitions                                                                                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-definition DEFAULT_ADMIN_ROLE() returns bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000;
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) {
-    calldataarg args;
-
-    bool hasRoleBefore = hasRole(role, account);
-    f(e, args);
-    bool hasRoleAfter = hasRole(role, account);
-
-    assert (
-        !hasRoleBefore &&
-        hasRoleAfter
-    ) => (
-        f.selector == grantRole(bytes32, address).selector
-    );
-
-    assert (
-        hasRoleBefore &&
-        !hasRoleAfter
-    ) => (
-        f.selector == revokeRole(bytes32, address).selector ||
-        f.selector == renounceRole(bytes32, address).selector
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: grantRole only affects the specified user/role combo                                          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule grantRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    grantRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> isCallerAdmin;
-
-    // effect
-    assert success => hasRole(role, account);
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: revokeRole only affects the specified user/role combo                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule revokeRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    revokeRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> isCallerAdmin;
-
-    // effect
-    assert success => !hasRole(role, account);
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: renounceRole only affects the specified user/role combo                                       │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule renounceRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    renounceRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> account == e.msg.sender;
-
-    // effect
-    assert success => !hasRole(role, account);
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
-}

certora/specs/AccessControlDefaultAdminRules.spec

@@ -1,464 +0,0 @@
-import "helpers/helpers.spec"
-import "methods/IAccessControlDefaultAdminRules.spec"
-import "methods/IAccessControl.spec"
-import "AccessControl.spec"
-
-use rule onlyGrantCanGrant filtered {
-  f -> f.selector != acceptDefaultAdminTransfer().selector
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Helpers                                                                                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-definition timeSanity(env e) returns bool =
-  e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48();
-
-definition delayChangeWaitSanity(env e, uint48 newDelay) returns bool =
-  e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48();
-
-definition isSet(uint48 schedule) returns bool =
-  schedule != 0;
-
-definition hasPassed(env e, uint48 schedule) returns bool =
-  schedule < e.block.timestamp;
-
-definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint =
-  e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait());
-
-definition decreasingDelaySchedule(env e, uint48 newDelay) returns mathint =
-  e.block.timestamp + defaultAdminDelay(e) - newDelay;
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: defaultAdmin holds the DEFAULT_ADMIN_ROLE                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant defaultAdminConsistency(address account)
-  (account == defaultAdmin() && account != 0) <=> hasRole(DEFAULT_ADMIN_ROLE(), account)
-  {
-    preserved with (env e) {
-      require nonzerosender(e);
-    }
-  }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: Only one account holds the DEFAULT_ADMIN_ROLE                                                            │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant singleDefaultAdmin(address account, address another)
-  hasRole(DEFAULT_ADMIN_ROLE(), account) && hasRole(DEFAULT_ADMIN_ROLE(), another) => another == account
-  {
-    preserved {
-      requireInvariant defaultAdminConsistency(account);
-      requireInvariant defaultAdminConsistency(another);
-    }
-  }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: DEFAULT_ADMIN_ROLE's admin is always DEFAULT_ADMIN_ROLE                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant defaultAdminRoleAdminConsistency()
-  getRoleAdmin(DEFAULT_ADMIN_ROLE()) == DEFAULT_ADMIN_ROLE()
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: owner is the defaultAdmin                                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant ownerConsistency()
-  defaultAdmin() == owner()
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: revokeRole only affects the specified user/role combo                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule revokeRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    revokeRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> isCallerAdmin && role != DEFAULT_ADMIN_ROLE(),
-      "roles can only be revoked by their owner except for the default admin role";
-
-    // effect
-    assert success => !hasRole(role, account),
-      "role is revoked";
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount),
-      "no other role is affected";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: renounceRole only affects the specified user/role combo                                       │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule renounceRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool    hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-    address adminBefore        = defaultAdmin();
-    address pendingAdminBefore = pendingDefaultAdmin_();
-    uint48  scheduleBefore     = pendingDefaultAdminSchedule_();
-
-    renounceRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool    hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-    address adminAfter        = defaultAdmin();
-    address pendingAdminAfter = pendingDefaultAdmin_();
-    uint48  scheduleAfter     = pendingDefaultAdminSchedule_();
-
-    // liveness
-    assert success <=> (
-      account == e.msg.sender &&
-      (
-        role    != DEFAULT_ADMIN_ROLE() ||
-        account != adminBefore          ||
-        (
-          pendingAdminBefore == 0 &&
-          isSet(scheduleBefore) &&
-          hasPassed(e, scheduleBefore)
-        )
-      )
-    ),
-      "an account only can renounce by itself with a delay for the default admin role";
-
-    // effect
-    assert success => !hasRole(role, account),
-      "role is renounced";
-
-    assert success => (
-      (
-        role    == DEFAULT_ADMIN_ROLE() &&
-        account == adminBefore
-      ) ? (
-        adminAfter        == 0 &&
-        pendingAdminAfter == 0 &&
-        scheduleAfter     == 0
-      ) : (
-        adminAfter        == adminBefore        &&
-        pendingAdminAfter == pendingAdminBefore &&
-        scheduleAfter     == scheduleBefore
-      )
-    ),
-      "renouncing default admin role cleans state iff called by previous admin";
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (
-      role == otherRole &&
-      account == otherAccount
-    ),
-      "no other role is affected";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: defaultAdmin is only affected by accepting an admin transfer or renoucing                                     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noDefaultAdminChange(env e, method f, calldataarg args) {
-  address adminBefore = defaultAdmin();
-  f(e, args);
-  address adminAfter = defaultAdmin();
-
-  assert adminBefore != adminAfter => (
-    f.selector == acceptDefaultAdminTransfer().selector ||
-    f.selector == renounceRole(bytes32,address).selector
-  ),
-    "default admin is only affected by accepting an admin transfer or renoucing";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: pendingDefaultAdmin is only affected by beginning, completing (accept or renounce), or canceling an admin     │
-│ transfer                                                                                                            │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noPendingDefaultAdminChange(env e, method f, calldataarg args) {
-  address pendingAdminBefore = pendingDefaultAdmin_();
-  address scheduleBefore = pendingDefaultAdminSchedule_();
-  f(e, args);
-  address pendingAdminAfter = pendingDefaultAdmin_();
-  address scheduleAfter = pendingDefaultAdminSchedule_();
-
-  assert (
-    pendingAdminBefore != pendingAdminAfter ||
-    scheduleBefore != scheduleAfter
-  ) => (
-    f.selector == beginDefaultAdminTransfer(address).selector ||
-    f.selector == acceptDefaultAdminTransfer().selector ||
-    f.selector == cancelDefaultAdminTransfer().selector ||
-    f.selector == renounceRole(bytes32,address).selector
-  ),
-    "pending admin and its schedule is only affected by beginning, completing, or cancelling an admin transfer";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: defaultAdminDelay can't be changed atomically by any function                                                 │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noDefaultAdminDelayChange(env e, method f, calldataarg args) {
-  uint48 delayBefore = defaultAdminDelay(e);
-  f(e, args);
-  uint48 delayAfter = defaultAdminDelay(e);
-
-  assert delayBefore == delayAfter,
-    "delay can't be changed atomically by any function";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: pendingDefaultAdminDelay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) {
-  uint48 pendingDelayBefore = pendingDelay_(e);
-  f(e, args);
-  uint48 pendingDelayAfter = pendingDelay_(e);
-
-  assert pendingDelayBefore != pendingDelayAfter => (
-    f.selector == changeDefaultAdminDelay(uint48).selector ||
-    f.selector == rollbackDefaultAdminDelay().selector
-  ),
-    "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: defaultAdminDelayIncreaseWait can't be changed atomically by any function                                     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noDefaultAdminDelayIncreaseWaitChange(env e, method f, calldataarg args) {
-  uint48 delayIncreaseWaitBefore = defaultAdminDelayIncreaseWait();
-  f(e, args);
-  uint48 delayIncreaseWaitAfter = defaultAdminDelayIncreaseWait();
-
-  assert delayIncreaseWaitBefore == delayIncreaseWaitAfter,
-    "delay increase wait can't be changed atomically by any function";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: beginDefaultAdminTransfer sets a pending default admin and its schedule                       │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule beginDefaultAdminTransfer(env e, address newAdmin) {
-  require timeSanity(e);
-  require nonpayable(e);
-  require nonzerosender(e);
-  requireInvariant defaultAdminConsistency(e.msg.sender);
-
-  beginDefaultAdminTransfer@withrevert(e, newAdmin);
-  bool success = !lastReverted;
-
-  // liveness
-  assert success <=> e.msg.sender == defaultAdmin(),
-    "only the current default admin can begin a transfer";
-
-  // effect
-  assert success => pendingDefaultAdmin_() == newAdmin,
-    "pending default admin is set";
-  assert success => pendingDefaultAdminSchedule_() == e.block.timestamp + defaultAdminDelay(e),
-    "pending default admin delay is set";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: A default admin can't change in less than the applied schedule                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args, address newAdmin) {
-  require e1.block.timestamp <= e2.block.timestamp;
-
-  uint48 delayBefore = defaultAdminDelay(e1);
-  address adminBefore = defaultAdmin();
-
-  // There might be a better way to generalize this without requiring `beginDefaultAdminTransfer`, but currently
-  // it's the only way in which we can attest that only `delayBefore` has passed before a change.
-  beginDefaultAdminTransfer(e1, newAdmin);
-  f(e2, args);
-
-  address adminAfter = defaultAdmin();
-
-  // change can only happen towards the newAdmin, with the delay
-  assert adminAfter != adminBefore => (
-    adminAfter == newAdmin &&
-    e2.block.timestamp >= e1.block.timestamp + delayBefore
-  ),
-    "The admin can only change after the enforced delay and to the previously scheduled new admin";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: acceptDefaultAdminTransfer updates defaultAdmin resetting the pending admin and its schedule  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule acceptDefaultAdminTransfer(env e) {
-  require nonpayable(e);
-
-  address pendingAdminBefore = pendingDefaultAdmin_();
-  uint48 scheduleBefore = pendingDefaultAdminSchedule_();
-
-  acceptDefaultAdminTransfer@withrevert(e);
-  bool success = !lastReverted;
-
-  // liveness
-  assert success <=> (
-    e.msg.sender == pendingAdminBefore &&
-    isSet(scheduleBefore) &&
-    hasPassed(e, scheduleBefore)
-  ),
-    "only the pending default admin can accept the role after the schedule has been set and passed";
-
-  // effect
-  assert success => defaultAdmin() == pendingAdminBefore,
-    "Default admin is set to the previous pending default admin";
-  assert success => pendingDefaultAdmin_() == 0,
-    "Pending default admin is reset";
-  assert success => pendingDefaultAdminSchedule_() == 0,
-    "Pending default admin delay is reset";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: cancelDefaultAdminTransfer resets pending default admin and its schedule                      │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule cancelDefaultAdminTransfer(env e) {
-  require nonpayable(e);
-  require nonzerosender(e);
-  requireInvariant defaultAdminConsistency(e.msg.sender);
-
-  cancelDefaultAdminTransfer@withrevert(e);
-  bool success = !lastReverted;
-
-  // liveness
-  assert success <=> e.msg.sender == defaultAdmin(),
-    "only the current default admin can cancel a transfer";
-
-  // effect
-  assert success => pendingDefaultAdmin_() == 0,
-    "Pending default admin is reset";
-  assert success => pendingDefaultAdminSchedule_() == 0,
-    "Pending default admin delay is reset";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: changeDefaultAdminDelay sets a pending default admin delay and its schedule                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule changeDefaultAdminDelay(env e, uint48 newDelay) {
-  require timeSanity(e);
-  require nonpayable(e);
-  require nonzerosender(e);
-  require delayChangeWaitSanity(e, newDelay);
-  requireInvariant defaultAdminConsistency(e.msg.sender);
-
-  uint48 delayBefore = defaultAdminDelay(e);
-
-  changeDefaultAdminDelay@withrevert(e, newDelay);
-  bool success = !lastReverted;
-
-  // liveness
-  assert success <=> e.msg.sender == defaultAdmin(),
-    "only the current default admin can begin a delay change";
-
-  // effect
-  assert success => pendingDelay_(e) == newDelay,
-    "pending delay is set";
-
-  assert success => (
-    pendingDelaySchedule_(e) > e.block.timestamp ||
-    delayBefore == newDelay || // Interpreted as decreasing, x - x = 0
-    defaultAdminDelayIncreaseWait() == 0
-  ),
-    "pending delay schedule is set in the future unless accepted edge cases";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: A delay can't change in less than the applied schedule                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 newDelay) {
-  require e1.block.timestamp <= e2.block.timestamp;
-
-  uint48 delayBefore = defaultAdminDelay(e1);
-
-  changeDefaultAdminDelay(e1, newDelay);
-  f(e2, args);
-
-  uint48 delayAfter = defaultAdminDelay(e2);
-
-  mathint delayWait = newDelay > delayBefore ? increasingDelaySchedule(e1, newDelay) : decreasingDelaySchedule(e1, newDelay);
-
-  assert delayAfter != delayBefore => (
-    delayAfter == newDelay &&
-    e2.block.timestamp >= delayWait
-  ),
-    "A delay can only change after the applied schedule";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: pending delay wait is set depending on increasing or decreasing the delay                                     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pendingDelayWait(env e, uint48 newDelay) {
-  uint48 oldDelay = defaultAdminDelay(e);
-  changeDefaultAdminDelay(e, newDelay);
-
-  assert newDelay > oldDelay => pendingDelaySchedule_(e) == increasingDelaySchedule(e, newDelay),
-    "Delay wait is the minimum between the new delay and a threshold when the delay is increased";
-  assert newDelay <= oldDelay => pendingDelaySchedule_(e) == decreasingDelaySchedule(e, newDelay),
-    "Delay wait is the difference between the current and the new delay when the delay is decreased";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: rollbackDefaultAdminDelay resets the delay and its schedule                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule rollbackDefaultAdminDelay(env e) {
-  require nonpayable(e);
-  require nonzerosender(e);
-  requireInvariant defaultAdminConsistency(e.msg.sender);
-
-  rollbackDefaultAdminDelay@withrevert(e);
-  bool success = !lastReverted;
-
-  // liveness
-  assert success <=> e.msg.sender == defaultAdmin(),
-    "only the current default admin can rollback a delay change";
-
-  // effect
-  assert success => pendingDelay_(e) == 0,
-    "Pending default admin is reset";
-  assert success => pendingDelaySchedule_(e) == 0,
-    "Pending default admin delay is reset";
-}

certora/specs/DoubleEndedQueue.spec

@@ -1,366 +0,0 @@
-import "helpers/helpers.spec"
-
-methods {
-    pushFront(bytes32)                    envfree
-    pushBack(bytes32)                     envfree
-    popFront()          returns (bytes32) envfree
-    popBack()           returns (bytes32) envfree
-    clear()                               envfree
-
-    // exposed for FV
-    begin()             returns (int128)  envfree
-    end()               returns (int128)  envfree
-
-    // view
-    length()            returns (uint256) envfree
-    empty()             returns (bool)    envfree
-    front()             returns (bytes32) envfree
-    back()              returns (bytes32) envfree
-    at_(uint256)        returns (bytes32) envfree // at is a reserved word
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Helpers                                                                                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-
-function min_int128() returns mathint {
-    return -(1 << 127);
-}
-
-function max_int128() returns mathint {
-    return (1 << 127) - 1;
-}
-
-// Could be broken in theory, but not in practice
-function boundedQueue() returns bool {
-    return
-        max_int128() > to_mathint(end()) &&
-        min_int128() < to_mathint(begin());
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: end is larger or equal than begin                                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant boundariesConsistency()
-    end() >= begin()
-    filtered { f -> !f.isView }
-    { preserved { require boundedQueue(); } }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: length is end minus begin                                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant lengthConsistency()
-    length() == to_mathint(end()) - to_mathint(begin())
-    filtered { f -> !f.isView }
-    { preserved { require boundedQueue(); } }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: empty() is length 0 and no element exists                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant emptiness()
-    empty() <=> length() == 0
-    filtered { f -> !f.isView }
-    { preserved { require boundedQueue(); } }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: front points to the first index and back points to the last one                                          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant queueEndings()
-    at_(length() - 1) == back() && at_(0) == front()
-    filtered { f -> !f.isView }
-    {
-        preserved {
-            requireInvariant boundariesConsistency();
-            require boundedQueue();
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: pushFront adds an element at the beginning of the queue                                       │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pushFront(bytes32 value) {
-    require boundedQueue();
-
-    uint256 lengthBefore = length();
-
-    pushFront@withrevert(value);
-
-    // liveness
-    assert !lastReverted, "never reverts";
-
-    // effect
-    assert front() == value, "front set to value";
-    assert length() == lengthBefore + 1, "queue extended";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: pushFront preserves the previous values in the queue with a +1 offset                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pushFrontConsistency(uint256 index) {
-    require boundedQueue();
-
-    bytes32 beforeAt = at_(index);
-
-    bytes32 value;
-    pushFront(value);
-
-    // try to read value
-    bytes32 afterAt = at_@withrevert(index + 1);
-
-    assert !lastReverted, "value still there";
-    assert afterAt == beforeAt, "data is preserved";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: pushBack adds an element at the end of the queue                                              │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pushBack(bytes32 value) {
-    require boundedQueue();
-
-    uint256 lengthBefore = length();
-
-    pushBack@withrevert(value);
-
-    // liveness
-    assert !lastReverted, "never reverts";
-
-    // effect
-    assert back() == value, "back set to value";
-    assert length() == lengthBefore + 1, "queue increased";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: pushBack preserves the previous values in the queue                                                           │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pushBackConsistency(uint256 index) {
-    require boundedQueue();
-
-    bytes32 beforeAt = at_(index);
-
-    bytes32 value;
-    pushBack(value);
-
-    // try to read value
-    bytes32 afterAt = at_@withrevert(index);
-
-    assert !lastReverted, "value still there";
-    assert afterAt == beforeAt, "data is preserved";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: popFront removes an element from the beginning of the queue                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule popFront {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    uint256 lengthBefore = length();
-    bytes32 frontBefore = front@withrevert();
-
-    bytes32 popped = popFront@withrevert();
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> lengthBefore != 0, "never reverts if not previously empty";
-
-    // effect
-    assert success => frontBefore == popped, "previous front is returned";
-    assert success => length() == lengthBefore - 1, "queue decreased";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: at(x) is preserved and offset to at(x - 1) after calling popFront                                             |
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule popFrontConsistency(uint256 index) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    // Read (any) value that is not the front (this asserts the value exists / the queue is long enough)
-    require index > 1;
-    bytes32 before = at_(index);
-
-    popFront();
-
-    // try to read value
-    bytes32 after = at_@withrevert(index - 1);
-
-    assert !lastReverted, "value still exists in the queue";
-    assert before == after, "values are offset and not modified";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: popBack removes an element from the end of the queue                                          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule popBack {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    uint256 lengthBefore = length();
-    bytes32 backBefore = back@withrevert();
-
-    bytes32 popped = popBack@withrevert();
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> lengthBefore != 0, "never reverts if not previously empty";
-
-    // effect
-    assert success => backBefore == popped, "previous back is returned";
-    assert success => length() == lengthBefore - 1, "queue decreased";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: at(x) is preserved after calling popBack                                                                     |
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule popBackConsistency(uint256 index) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    // Read (any) value that is not the back (this asserts the value exists / the queue is long enough)
-    require index < length() - 1;
-    bytes32 before = at_(index);
-
-    popBack();
-
-    // try to read value
-    bytes32 after = at_@withrevert(index);
-
-    assert !lastReverted, "value still exists in the queue";
-    assert before == after, "values are offset and not modified";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: clear sets length to 0                                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule clear {
-    clear@withrevert();
-
-    // liveness
-    assert !lastReverted, "never reverts";
-
-    // effect
-    assert length() == 0, "sets length to 0";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: front/back access reverts only if the queue is empty or querying out of bounds                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyEmptyRevert(env e) {
-    require nonpayable(e);
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    method f;
-    calldataarg args;
-
-    bool emptyBefore = empty();
-
-    f@withrevert(e, args);
-
-    assert lastReverted => (
-        (f.selector == front().selector && emptyBefore) ||
-        (f.selector == back().selector && emptyBefore) ||
-        (f.selector == popFront().selector  && emptyBefore) ||
-        (f.selector == popBack().selector  && emptyBefore) ||
-        f.selector == at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
-    ), "only revert if empty or out of bounds";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: at(index) only reverts if index is out of bounds                                                                  |
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyOutOfBoundsRevert(uint256 index) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    at_@withrevert(index);
-
-    assert lastReverted <=> index >= length(), "only reverts if index is out of bounds";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: only clear/push/pop operations can change the length of the queue                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noLengthChange(env e) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    method f;
-    calldataarg args;
-
-    uint256 lengthBefore = length();
-    f(e, args);
-    uint256 lengthAfter = length();
-
-    assert lengthAfter != lengthBefore => (
-        (f.selector == pushFront(bytes32).selector && lengthAfter == lengthBefore + 1) ||
-        (f.selector == pushBack(bytes32).selector && lengthAfter == lengthBefore + 1) ||
-        (f.selector == popBack().selector && lengthAfter == lengthBefore - 1) ||
-        (f.selector == popFront().selector && lengthAfter == lengthBefore - 1) ||
-        (f.selector == clear().selector && lengthAfter == 0)
-    ), "length is only affected by clear/pop/push operations";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: only push/pop can change values bounded in the queue (outside values aren't cleared)                          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noDataChange(env e) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
-    method f;
-    calldataarg args;
-
-    uint256 index;
-    bytes32 atBefore = at_(index);
-    f(e, args);
-    bytes32 atAfter = at_@withrevert(index);
-    bool atAfterSuccess = !lastReverted;
-
-    assert !atAfterSuccess <=> (
-        f.selector == clear().selector ||
-        (f.selector == popBack().selector && index == length()) ||
-        (f.selector == popFront().selector && index == length())
-    ), "indexes of the queue are only removed by clear or pop";
-
-    assert atAfterSuccess && atAfter != atBefore => (
-        f.selector == popFront().selector ||
-        f.selector == pushFront(bytes32).selector
-    ), "values of the queue are only changed by popFront or pushFront";
-}

certora/specs/ERC20.spec

@@ -1,414 +0,0 @@
-import "helpers/helpers.spec"
-import "methods/IERC20.spec"
-import "methods/IERC2612.spec"
-
-methods {
-    // non standard ERC20 functions
-    increaseAllowance(address,uint256) returns (bool)
-    decreaseAllowance(address,uint256) returns (bool)
-
-    // exposed for FV
-    mint(address,uint256)
-    burn(address,uint256)
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost & hooks: sum of all balances                                                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-ghost sumOfBalances() returns uint256 {
-  init_state axiom sumOfBalances() == 0;
-}
-
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
-    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: totalSupply is the sum of all balances                                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant totalSupplyIsSumOfBalances()
-    totalSupply() == sumOfBalances()
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: balance of address(0) is 0                                                                               │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant zeroAddressNoBalance()
-    balanceOf(0) == 0
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: only mint and burn can change total supply                                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noChangeTotalSupply(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-
-    method f;
-    calldataarg args;
-
-    uint256 totalSupplyBefore = totalSupply();
-    f(e, args);
-    uint256 totalSupplyAfter = totalSupply();
-
-    assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector;
-    assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyAuthorizedCanTransfer(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-
-    method f;
-    calldataarg args;
-    address account;
-
-    uint256 allowanceBefore = allowance(account, e.msg.sender);
-    uint256 balanceBefore   = balanceOf(account);
-    f(e, args);
-    uint256 balanceAfter    = balanceOf(account);
-
-    assert (
-        balanceAfter < balanceBefore
-    ) => (
-        f.selector == burn(address,uint256).selector ||
-        e.msg.sender == account ||
-        balanceBefore - balanceAfter <= allowanceBefore
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyHolderOfSpenderCanChangeAllowance(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-
-    method f;
-    calldataarg args;
-    address holder;
-    address spender;
-
-    uint256 allowanceBefore = allowance(holder, spender);
-    f(e, args);
-    uint256 allowanceAfter = allowance(holder, spender);
-
-    assert (
-        allowanceAfter > allowanceBefore
-    ) => (
-        (f.selector == approve(address,uint256).selector           && e.msg.sender == holder) ||
-        (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
-        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
-    );
-
-    assert (
-        allowanceAfter < allowanceBefore
-    ) => (
-        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
-        (f.selector == approve(address,uint256).selector              && e.msg.sender == holder ) ||
-        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
-        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: mint behavior and side effects                                                                               │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule mint(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-    require nonpayable(e);
-
-    address to;
-    address other;
-    uint256 amount;
-
-    // cache state
-    uint256 toBalanceBefore    = balanceOf(to);
-    uint256 otherBalanceBefore = balanceOf(other);
-    uint256 totalSupplyBefore  = totalSupply();
-
-    // run transaction
-    mint@withrevert(e, to, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert to == 0 || totalSupplyBefore + amount > max_uint256;
-    } else {
-        // updates balance and totalSupply
-        assert balanceOf(to) == toBalanceBefore   + amount;
-        assert totalSupply() == totalSupplyBefore + amount;
-
-        // no other balance is modified
-        assert balanceOf(other) != otherBalanceBefore => other == to;
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: burn behavior and side effects                                                                               │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule burn(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-    require nonpayable(e);
-
-    address from;
-    address other;
-    uint256 amount;
-
-    // cache state
-    uint256 fromBalanceBefore  = balanceOf(from);
-    uint256 otherBalanceBefore = balanceOf(other);
-    uint256 totalSupplyBefore  = totalSupply();
-
-    // run transaction
-    burn@withrevert(e, from, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert from == 0 || fromBalanceBefore < amount;
-    } else {
-        // updates balance and totalSupply
-        assert balanceOf(from) == fromBalanceBefore   - amount;
-        assert totalSupply()   == totalSupplyBefore - amount;
-
-        // no other balance is modified
-        assert balanceOf(other) != otherBalanceBefore => other == from;
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: transfer behavior and side effects                                                                            │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule transfer(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-    require nonpayable(e);
-
-    address holder = e.msg.sender;
-    address recipient;
-    address other;
-    uint256 amount;
-
-    // cache state
-    uint256 holderBalanceBefore    = balanceOf(holder);
-    uint256 recipientBalanceBefore = balanceOf(recipient);
-    uint256 otherBalanceBefore     = balanceOf(other);
-
-    // run transaction
-    transfer@withrevert(e, recipient, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
-    } else {
-        // balances of holder and recipient are updated
-        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
-
-        // no other balance is modified
-        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: transferFrom behavior and side effects                                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule transferFrom(env e) {
-    requireInvariant totalSupplyIsSumOfBalances();
-    require nonpayable(e);
-
-    address spender = e.msg.sender;
-    address holder;
-    address recipient;
-    address other;
-    uint256 amount;
-
-    // cache state
-    uint256 allowanceBefore        = allowance(holder, spender);
-    uint256 holderBalanceBefore    = balanceOf(holder);
-    uint256 recipientBalanceBefore = balanceOf(recipient);
-    uint256 otherBalanceBefore     = balanceOf(other);
-
-    // run transaction
-    transferFrom@withrevert(e, holder, recipient, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore;
-    } else {
-        // allowance is valid & updated
-        assert allowanceBefore            >= amount;
-        assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
-
-        // balances of holder and recipient are updated
-        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
-
-        // no other balance is modified
-        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: approve behavior and side effects                                                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule approve(env e) {
-    require nonpayable(e);
-
-    address holder = e.msg.sender;
-    address spender;
-    address otherHolder;
-    address otherSpender;
-    uint256 amount;
-
-    // cache state
-    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
-
-    // run transaction
-    approve@withrevert(e, spender, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert holder == 0 || spender == 0;
-    } else {
-        // allowance is updated
-        assert allowance(holder, spender) == amount;
-
-        // other allowances are untouched
-        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: increaseAllowance behavior and side effects                                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule increaseAllowance(env e) {
-    require nonpayable(e);
-
-    address holder = e.msg.sender;
-    address spender;
-    address otherHolder;
-    address otherSpender;
-    uint256 amount;
-
-    // cache state
-    uint256 allowanceBefore      = allowance(holder, spender);
-    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
-
-    // run transaction
-    increaseAllowance@withrevert(e, spender, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256;
-    } else {
-        // allowance is updated
-        assert allowance(holder, spender) == allowanceBefore + amount;
-
-        // other allowances are untouched
-        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: decreaseAllowance behavior and side effects                                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule decreaseAllowance(env e) {
-    require nonpayable(e);
-
-    address holder = e.msg.sender;
-    address spender;
-    address otherHolder;
-    address otherSpender;
-    uint256 amount;
-
-    // cache state
-    uint256 allowanceBefore      = allowance(holder, spender);
-    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
-
-    // run transaction
-    decreaseAllowance@withrevert(e, spender, amount);
-
-    // check outcome
-    if (lastReverted) {
-        assert holder == 0 || spender == 0 || allowanceBefore < amount;
-    } else {
-        // allowance is updated
-        assert allowance(holder, spender) == allowanceBefore - amount;
-
-        // other allowances are untouched
-        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: permit behavior and side effects                                                                              │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule permit(env e) {
-    require nonpayable(e);
-
-    address holder;
-    address spender;
-    uint256 amount;
-    uint256 deadline;
-    uint8 v;
-    bytes32 r;
-    bytes32 s;
-
-    address account1;
-    address account2;
-    address account3;
-
-    // cache state
-    uint256 nonceBefore          = nonces(holder);
-    uint256 otherNonceBefore     = nonces(account1);
-    uint256 otherAllowanceBefore = allowance(account2, account3);
-
-    // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice
-    require nonceBefore      < max_uint256;
-    require otherNonceBefore < max_uint256;
-
-    // run transaction
-    permit@withrevert(e, holder, spender, amount, deadline, v, r, s);
-
-    // check outcome
-    if (lastReverted) {
-        // Without formally checking the signature, we can't verify exactly the revert causes
-        assert true;
-    } else {
-        // allowance and nonce are updated
-        assert allowance(holder, spender) == amount;
-        assert nonces(holder) == nonceBefore + 1;
-
-        // deadline was respected
-        assert deadline >= e.block.timestamp;
-
-        // no other allowance or nonce is modified
-        assert nonces(account1)              != otherNonceBefore     => account1 == holder;
-        assert allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender);
-    }
-}

certora/specs/ERC20FlashMint.spec

@@ -1,48 +0,0 @@
-import "helpers/helpers.spec"
-import "methods/IERC20.spec"
-import "methods/IERC3156.spec"
-
-methods {
-    // non standard ERC3156 functions
-    flashFeeReceiver() returns (address) envfree
-
-    // function summaries below
-    _mint(address account, uint256 amount)              => specMint(account, amount)
-    _burn(address account, uint256 amount)              => specBurn(account, amount)
-    _transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount)
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost: track mint and burns in the CVL                                                                              │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-ghost mapping(address => uint256)                     trackedMintAmount;
-ghost mapping(address => uint256)                     trackedBurnAmount;
-ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount;
-
-function specMint(address account, uint256 amount)              returns bool { trackedMintAmount[account] = amount;        return true; }
-function specBurn(address account, uint256 amount)              returns bool { trackedBurnAmount[account] = amount;        return true; }
-function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: When doing a flashLoan, "amount" is minted and burnt, additionally, the fee is either burnt                   │
-│ (if the fee recipient is 0) or transferred (if the fee recipient is not 0)                                          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule checkMintAndBurn(env e) {
-    address receiver;
-    address token;
-    uint256 amount;
-    bytes data;
-
-    uint256 fees = flashFee(token, amount);
-    address recipient = flashFeeReceiver();
-
-    flashLoan(e, receiver, token, amount, data);
-
-    assert trackedMintAmount[receiver] == amount;
-    assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0);
-    assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees;
-}

certora/specs/ERC20Wrapper.spec

@@ -1,198 +0,0 @@
-import "helpers/helpers.spec"
-import "ERC20.spec"
-
-methods {
-    underlying()                       returns(address) envfree
-    underlyingTotalSupply()            returns(uint256) envfree
-    underlyingBalanceOf(address)       returns(uint256) envfree
-    underlyingAllowanceToThis(address) returns(uint256) envfree
-
-    depositFor(address, uint256)       returns(bool)
-    withdrawTo(address, uint256)       returns(bool)
-    recover(address)                   returns(uint256)
-}
-
-use invariant totalSupplyIsSumOfBalances
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying                                           │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool {
-    return underlyingBalanceOf(a) <= underlyingTotalSupply();
-}
-
-function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool {
-    return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: wrapped token can't be undercollateralized (solvency of the wrapper)                                     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant totalSupplyIsSmallerThanUnderlyingBalance()
-    totalSupply() <= underlyingBalanceOf(currentContract) &&
-    underlyingBalanceOf(currentContract) <= underlyingTotalSupply() &&
-    underlyingTotalSupply() <= max_uint256
-    {
-        preserved {
-            requireInvariant totalSupplyIsSumOfBalances;
-            require underlyingBalancesLowerThanUnderlyingSupply(currentContract);
-        }
-        preserved depositFor(address account, uint256 amount) with (env e) {
-            require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract);
-        }
-    }
-
-invariant noSelfWrap()
-    currentContract != underlying()
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: depositFor liveness and effects                                                                               │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule depositFor(env e) {
-    require nonpayable(e);
-
-    address sender = e.msg.sender;
-    address receiver;
-    address other;
-    uint256 amount;
-
-    // sanity
-    requireInvariant noSelfWrap;
-    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 otherBalanceBefore              = balanceOf(other);
-    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
-
-    depositFor@withrevert(e, receiver, amount);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> (
-        sender   != currentContract               && // invalid sender
-        sender   != 0                             && // invalid sender
-        receiver != 0                             && // invalid receiver
-        amount   <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
-        amount   <= senderUnderlyingAllowanceBefore  // deposit doesn't exceed allowance
-    );
-
-    // effects
-    assert success => (
-        balanceOf(receiver) == balanceBefore + amount &&
-        totalSupply() == supplyBefore + amount &&
-        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount &&
-        underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount
-    );
-
-    // no side effect
-    assert underlyingTotalSupply() == underlyingSupplyBefore;
-    assert balanceOf(other)           != otherBalanceBefore           => other == receiver;
-    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: withdrawTo liveness and effects                                                                               │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule withdrawTo(env e) {
-    require nonpayable(e);
-
-    address sender = e.msg.sender;
-    address receiver;
-    address other;
-    uint256 amount;
-
-    // sanity
-    requireInvariant noSelfWrap;
-    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 otherBalanceBefore              = balanceOf(other);
-    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
-
-    withdrawTo@withrevert(e, receiver, amount);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> (
-        sender   != 0          && // invalid sender
-        receiver != 0          && // invalid receiver
-        amount   <= balanceBefore // withdraw doesn't exceed balance
-    );
-
-    // effects
-    assert success => (
-        balanceOf(sender) == balanceBefore - amount &&
-        totalSupply() == supplyBefore - amount &&
-        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
-        underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
-    );
-
-    // no side effect
-    assert underlyingTotalSupply() == underlyingSupplyBefore;
-    assert balanceOf(other)           != otherBalanceBefore           => other == sender;
-    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: recover liveness and effects                                                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule recover(env e) {
-    require nonpayable(e);
-
-    address receiver;
-    address other;
-
-    // sanity
-    requireInvariant noSelfWrap;
-    requireInvariant totalSupplyIsSumOfBalances;
-    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
-
-    uint256 value                        = underlyingBalanceOf(currentContract) - totalSupply();
-    uint256 supplyBefore                 = totalSupply();
-    uint256 balanceBefore                = balanceOf(receiver);
-
-    uint256 otherBalanceBefore           = balanceOf(other);
-    uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
-
-    recover@withrevert(e, receiver);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> receiver != 0;
-
-    // effect
-    assert success => (
-        balanceOf(receiver) == balanceBefore + value &&
-        totalSupply() == supplyBefore + value &&
-        totalSupply() == underlyingBalanceOf(currentContract)
-    );
-
-    // no side effect
-    assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore;
-    assert balanceOf(other) != otherBalanceBefore => other == receiver;
-}

certora/specs/ERC721.spec

@@ -1,589 +0,0 @@
-import "helpers/helpers.spec"
-import "methods/IERC721.spec"
-
-methods {
-    // exposed for FV
-    mint(address,uint256)
-    safeMint(address,uint256)
-    safeMint(address,uint256,bytes)
-    burn(uint256)
-
-    tokenExists(uint256) returns (bool) envfree
-    unsafeOwnerOf(uint256) returns (address) envfree
-    unsafeGetApproved(uint256) returns (address) envfree
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Helpers                                                                                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-
-// Could be broken in theory, but not in practice
-function balanceLimited(address account) returns bool {
-    return balanceOf(account) < max_uint256;
-}
-
-function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
-    if (f.selector == transferFrom(address,address,uint256).selector) {
-        transferFrom@withrevert(e, from, to, tokenId);
-    } else if (f.selector == safeTransferFrom(address,address,uint256).selector) {
-        safeTransferFrom@withrevert(e, from, to, tokenId);
-    } else if (f.selector == safeTransferFrom(address,address,uint256,bytes).selector) {
-        bytes params;
-        require params.length < 0xffff;
-        safeTransferFrom@withrevert(e, from, to, tokenId, params);
-    } else {
-        calldataarg args;
-        f@withrevert(e, args);
-    }
-}
-
-function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
-    if (f.selector == mint(address,uint256).selector) {
-        mint@withrevert(e, to, tokenId);
-    } else if (f.selector == safeMint(address,uint256).selector) {
-        safeMint@withrevert(e, to, tokenId);
-    } else if (f.selector == safeMint(address,uint256,bytes).selector) {
-        bytes params;
-        require params.length < 0xffff;
-        safeMint@withrevert(e, to, tokenId, params);
-    } else {
-        require false;
-    }
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost & hooks: ownership count                                                                                      │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-ghost ownedTotal() returns uint256 {
-  init_state axiom ownedTotal() == 0;
-}
-
-ghost mapping(address => uint256) ownedByUser {
-    init_state axiom forall address a. ownedByUser[a] == 0;
-}
-
-hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
-    ownedByUser[newOwner] = ownedByUser[newOwner] + to_uint256(newOwner != 0 ? 1 : 0);
-    ownedByUser[oldOwner] = ownedByUser[oldOwner] - to_uint256(oldOwner != 0 ? 1 : 0);
-
-    havoc ownedTotal assuming ownedTotal@new() == ownedTotal@old()
-        + to_uint256(newOwner != 0 ? 1 : 0)
-        - to_uint256(oldOwner != 0 ? 1 : 0);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost & hooks: sum of all balances                                                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-ghost sumOfBalances() returns uint256 {
-  init_state axiom sumOfBalances() == 0;
-}
-
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
-    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
-}
-
-ghost mapping(address => uint256) ghostBalanceOf {
-    init_state axiom forall address a. ghostBalanceOf[a] == 0;
-}
-
-hook Sload uint256 value _balances[KEY address user] STORAGE {
-    require ghostBalanceOf[user] == value;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: ownedTotal is the sum of all balances                                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant ownedTotalIsSumOfBalances()
-    ownedTotal() == sumOfBalances()
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: balanceOf is the number of tokens owned                                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant balanceOfConsistency(address user)
-    balanceOf(user) == ownedByUser[user] &&
-    balanceOf(user) == ghostBalanceOf[user]
-    {
-        preserved {
-            require balanceLimited(user);
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: owner of a token must have some balance                                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant ownerHasBalance(uint256 tokenId)
-    balanceOf(ownerOf(tokenId)) > 0
-    {
-        preserved {
-            requireInvariant balanceOfConsistency(ownerOf(tokenId));
-            require balanceLimited(ownerOf(tokenId));
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: tokens that do not exist are not owned and not approved                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant notMintedUnset(uint256 tokenId)
-    (!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) &&
-    (!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0)
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: ownerOf and getApproved revert if token does not exist                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule notMintedRevert(uint256 tokenId) {
-    requireInvariant notMintedUnset(tokenId);
-
-    bool e = tokenExists(tokenId);
-
-    address owner = ownerOf@withrevert(tokenId);
-    assert e <=> !lastReverted;
-    assert e => owner == unsafeOwnerOf(tokenId); // notMintedUnset tells us this is non-zero
-
-    address approved = getApproved@withrevert(tokenId);
-    assert e <=> !lastReverted;
-    assert e => approved == unsafeGetApproved(tokenId);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert                                                              │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule unsafeDontRevert(uint256 tokenId) {
-    unsafeOwnerOf@withrevert(tokenId);
-    assert !lastReverted;
-
-    unsafeGetApproved@withrevert(tokenId);
-    assert !lastReverted;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: balance of address(0) is 0                                                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule zeroAddressBalanceRevert() {
-    balanceOf@withrevert(0);
-    assert lastReverted;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: total supply can only change through mint and burn                                                           │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule supplyChange(env e) {
-    uint256 supplyBefore = ownedTotal();
-    method f; calldataarg args; f(e, args);
-    uint256 supplyAfter = ownedTotal();
-
-    assert supplyAfter > supplyBefore => (
-        supplyAfter == supplyBefore + 1 &&
-        (
-            f.selector == mint(address,uint256).selector ||
-            f.selector == safeMint(address,uint256).selector ||
-            f.selector == safeMint(address,uint256,bytes).selector
-        )
-    );
-    assert supplyAfter < supplyBefore => (
-        supplyAfter == supplyBefore - 1 &&
-        f.selector == burn(uint256).selector
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule balanceChange(env e, address account) {
-    requireInvariant balanceOfConsistency(account);
-    require balanceLimited(account);
-
-    uint256 balanceBefore = balanceOf(account);
-    method f; calldataarg args; f(e, args);
-    uint256 balanceAfter  = balanceOf(account);
-
-    // balance can change by at most 1
-    assert balanceBefore != balanceAfter => (
-        balanceAfter == balanceBefore - 1 ||
-        balanceAfter == balanceBefore + 1
-    );
-
-    // only selected function can change balances
-    assert balanceBefore != balanceAfter => (
-        f.selector == transferFrom(address,address,uint256).selector ||
-        f.selector == safeTransferFrom(address,address,uint256).selector ||
-        f.selector == safeTransferFrom(address,address,uint256,bytes).selector ||
-        f.selector == mint(address,uint256).selector ||
-        f.selector == safeMint(address,uint256).selector ||
-        f.selector == safeMint(address,uint256,bytes).selector ||
-        f.selector == burn(uint256).selector
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: ownership can only change through mint, burn or transfers.                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule ownershipChange(env e, uint256 tokenId) {
-    address ownerBefore = unsafeOwnerOf(tokenId);
-    method f; calldataarg args; f(e, args);
-    address ownerAfter  = unsafeOwnerOf(tokenId);
-
-    assert ownerBefore == 0 && ownerAfter != 0 => (
-        f.selector == mint(address,uint256).selector ||
-        f.selector == safeMint(address,uint256).selector ||
-        f.selector == safeMint(address,uint256,bytes).selector
-    );
-
-    assert ownerBefore != 0 && ownerAfter == 0 => (
-        f.selector == burn(uint256).selector
-    );
-
-    assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
-        f.selector == transferFrom(address,address,uint256).selector ||
-        f.selector == safeTransferFrom(address,address,uint256).selector ||
-        f.selector == safeTransferFrom(address,address,uint256,bytes).selector
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule approvalChange(env e, uint256 tokenId) {
-    address approvalBefore = unsafeGetApproved(tokenId);
-    method f; calldataarg args; f(e, args);
-    address approvalAfter  = unsafeGetApproved(tokenId);
-
-    // approve can set any value, other functions reset
-    assert approvalBefore != approvalAfter => (
-        f.selector == approve(address,uint256).selector ||
-        (
-            (
-                f.selector == transferFrom(address,address,uint256).selector ||
-                f.selector == safeTransferFrom(address,address,uint256).selector ||
-                f.selector == safeTransferFrom(address,address,uint256,bytes).selector ||
-                f.selector == burn(uint256).selector
-            ) && approvalAfter == 0
-        )
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule approvedForAllChange(env e, address owner, address spender) {
-    bool approvedForAllBefore = isApprovedForAll(owner, spender);
-    method f; calldataarg args; f(e, args);
-    bool approvedForAllAfter  = isApprovedForAll(owner, spender);
-
-    assert approvedForAllBefore != approvedForAllAfter => f.selector == setApprovalForAll(address,bool).selector;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: transferFrom behavior and side effects                                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule transferFrom(env e, address from, address to, uint256 tokenId) {
-    require nonpayable(e);
-
-    address operator = e.msg.sender;
-    uint256 otherTokenId;
-    address otherAccount;
-
-    requireInvariant ownerHasBalance(tokenId);
-    require balanceLimited(to);
-
-    uint256 balanceOfFromBefore  = balanceOf(from);
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
-    address ownerBefore          = unsafeOwnerOf(tokenId);
-    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
-    address approvalBefore       = unsafeGetApproved(tokenId);
-    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
-
-    transferFrom@withrevert(e, from, to, tokenId);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> (
-        from == ownerBefore &&
-        from != 0 &&
-        to   != 0 &&
-        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
-    );
-
-    // effect
-    assert success => (
-        balanceOf(from)            == balanceOfFromBefore - to_uint256(from != to ? 1 : 0) &&
-        balanceOf(to)              == balanceOfToBefore   + to_uint256(from != to ? 1 : 0) &&
-        unsafeOwnerOf(tokenId)     == to &&
-        unsafeGetApproved(tokenId) == 0
-    );
-
-    // no side effect
-    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
-    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
-    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: safeTransferFrom behavior and side effects                                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
-    f.selector == safeTransferFrom(address,address,uint256).selector ||
-    f.selector == safeTransferFrom(address,address,uint256,bytes).selector
-} {
-    require nonpayable(e);
-
-    address operator = e.msg.sender;
-    uint256 otherTokenId;
-    address otherAccount;
-
-    requireInvariant ownerHasBalance(tokenId);
-    require balanceLimited(to);
-
-    uint256 balanceOfFromBefore  = balanceOf(from);
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(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;
-
-    assert success <=> (
-        from == ownerBefore &&
-        from != 0 &&
-        to   != 0 &&
-        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
-    );
-
-    // effect
-    assert success => (
-        balanceOf(from)            == balanceOfFromBefore - to_uint256(from != to ? 1: 0) &&
-        balanceOf(to)              == balanceOfToBefore   + to_uint256(from != to ? 1: 0) &&
-        unsafeOwnerOf(tokenId)     == to &&
-        unsafeGetApproved(tokenId) == 0
-    );
-
-    // no side effect
-    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
-    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
-    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: mint behavior and side effects                                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule mint(env e, address to, uint256 tokenId) {
-    require nonpayable(e);
-    requireInvariant notMintedUnset(tokenId);
-
-    uint256 otherTokenId;
-    address otherAccount;
-
-    require balanceLimited(to);
-
-    uint256 supplyBefore         = ownedTotal();
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
-    address ownerBefore          = unsafeOwnerOf(tokenId);
-    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
-
-    mint@withrevert(e, to, tokenId);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> (
-        ownerBefore == 0 &&
-        to != 0
-    );
-
-    // effect
-    assert success => (
-        ownedTotal()           == supplyBefore + 1 &&
-        balanceOf(to)          == balanceOfToBefore + 1 &&
-        unsafeOwnerOf(tokenId) == to
-    );
-
-    // no side effect
-    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
-    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: safeMint behavior and side effects                                                                            │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
-    f.selector == safeMint(address,uint256).selector ||
-    f.selector == safeMint(address,uint256,bytes).selector
-} {
-    require nonpayable(e);
-    requireInvariant notMintedUnset(tokenId);
-
-    uint256 otherTokenId;
-    address otherAccount;
-
-    require balanceLimited(to);
-
-    uint256 supplyBefore         = ownedTotal();
-    uint256 balanceOfToBefore    = balanceOf(to);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
-    address ownerBefore          = unsafeOwnerOf(tokenId);
-    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
-
-    helperMintWithRevert(e, f, to, tokenId);
-    bool success = !lastReverted;
-
-    assert success <=> (
-        ownerBefore == 0 &&
-        to != 0
-    );
-
-    // effect
-    assert success => (
-        ownedTotal()           == supplyBefore + 1 &&
-        balanceOf(to)          == balanceOfToBefore + 1 &&
-        unsafeOwnerOf(tokenId) == to
-    );
-
-    // no side effect
-    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
-    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: burn behavior and side effects                                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule burn(env e, uint256 tokenId) {
-    require nonpayable(e);
-
-    address from = unsafeOwnerOf(tokenId);
-    uint256 otherTokenId;
-    address otherAccount;
-
-    requireInvariant ownerHasBalance(tokenId);
-
-    uint256 supplyBefore         = ownedTotal();
-    uint256 balanceOfFromBefore  = balanceOf(from);
-    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
-    address ownerBefore          = unsafeOwnerOf(tokenId);
-    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
-    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
-
-    burn@withrevert(e, tokenId);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> (
-        ownerBefore != 0
-    );
-
-    // effect
-    assert success => (
-        ownedTotal()               == supplyBefore   - 1 &&
-        balanceOf(from)            == balanceOfFromBefore - 1 &&
-        unsafeOwnerOf(tokenId)     == 0 &&
-        unsafeGetApproved(tokenId) == 0
-    );
-
-    // no side effect
-    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
-    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
-    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: approve behavior and side effects                                                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule approve(env e, address spender, uint256 tokenId) {
-    require nonpayable(e);
-
-    address caller = e.msg.sender;
-    address owner = unsafeOwnerOf(tokenId);
-    uint256 otherTokenId;
-
-    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
-
-    approve@withrevert(e, spender, tokenId);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> (
-        owner != 0 &&
-        owner != spender &&
-        (owner == caller || isApprovedForAll(owner, caller))
-    );
-
-    // effect
-    assert success => unsafeGetApproved(tokenId) == spender;
-
-    // no side effect
-    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: setApprovalForAll behavior and side effects                                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule setApprovalForAll(env e, address operator, bool approved) {
-    require nonpayable(e);
-
-    address owner = e.msg.sender;
-    address otherOwner;
-    address otherOperator;
-
-    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);
-
-    setApprovalForAll@withrevert(e, operator, approved);
-    bool success = !lastReverted;
-
-    // liveness
-    assert success <=> owner != operator;
-
-    // effect
-    assert success => isApprovedForAll(owner, operator) == approved;
-
-    // no side effect
-    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
-        otherOwner    == owner &&
-        otherOperator == operator
-    );
-}