Add certora template for FV prover

.github/workflows/certora.yml

@@ -0,0 +1,103 @@
+# A workflow file for running Certora verification through GitHub actions.
+# Find results for each push in the "Actions" tab on the GitHub website.
+name: Certora verification
+
+on:
+  push: {}
+  pull_request: {}
+  workflow_dispatch: {}
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    steps:
+      # check out the current version
+      - uses: actions/checkout@v2
+
+      # install Certora dependencies and CLI
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+         # cache: 'pip'
+      - name: Install certora
+        run: pip3 install certora-cli
+
+      # the following is only necessary if your project depends on contracts
+      # installed using yarn
+      # - name: Install yarn
+      #   uses: actions/setup-node@v3
+      #   with:
+      #     node-version: 16
+      #     cache: 'yarn'
+      # - name: Install dependencies
+      #   run: yarn
+
+      # Install the appropriate version of solc
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.8/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.21
+          chmod +x /usr/local/bin/solc8.21
+          ln -s /usr/local/bin/solc8.21 /usr/local/bin/solc
+
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.17
+          chmod +x /usr/local/bin/solc8.17
+
+      # Do the actual verification.  The `run` field could be simply
+      #
+      #   certoraRun certora/conf/${{ matrix.params }}
+      # 
+      # but we do a little extra work to get the commit messages into the
+      # `--msg` argument to `certoraRun`
+      #
+      # Here ${{ matrix.params }} gets replaced with each of the parameters
+      # listed in the `params` section below.
+      - name: Verify ${{ matrix.params.name }}
+        run: >
+          message="$(git log -n 1 --pretty=format:'CI ${{matrix.params.name}} %h .... %s')";
+          certoraRun \
+            certora/confs/${{ matrix.params.command }} \
+            --msg "$(echo $message | sed 's/[^a-zA-Z0-9., _-]/ /g')"
+        env:
+          # For this to work, you must set your CERTORAKEY secret on the GitHub
+          # website (settings > secrets > actions > new repository secret)
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+      # The following two steps save the output json as a GitHub artifact.
+      # This can be useful for automation that collects the output.
+      - name: Download output json
+        if: always()
+        run: >
+          outputLink=$(sed 's/zipOutput/output/g' .zip-output-url.txt | sed 's/?/\/output.json?/g');
+          curl -L -b "certoraKey=$CERTORAKEY;" ${outputLink} --output output.json || true;
+          touch output.json;
+
+      - name: Archive output json
+        if: always()
+        uses: actions/upload-artifact@v3
+        with:
+          name: output for ${{ matrix.params.name }}
+          path: output.json
+
+    strategy:
+      fail-fast: false
+      matrix:
+        params:
+          # each of these commands is passed to the "Verify rule" step above,
+          # which runs certoraRun on certora/conf/<contents of the command>
+          #
+          # Note that each of these lines will appear as a separate run on
+          # prover.certora.com
+          #
+          # It is often helpful to split up by rule or even by method for a
+          # parametric rule, although it is certainly possible to run everything
+          # at once by not passing the `--rule` or `--method` options
+          #- {name: transferSpec,                 command: 'ERC20.conf --rule transferSpec'}
+          #- {name: generalRulesOnERC20, command: 'generalRules_ERC20.conf --debug'}
+          #- {name: generalRulesOnVAULT, command: 'generalRules_VAULT.conf --debug'}
+          - {name: ghostTemplate, command: 'ghost.conf' }
+          - {name: ghostWithERC20, command: 'ghostWithERC20s.conf' }
+
+

.gitignore

@@ -15,3 +15,6 @@ node_modules
 
 # ignore foundry deploy artifacts
 broadcast/
+
+#certora temp files
+.certora_internal

certora/README.md

@@ -0,0 +1,57 @@
+# Certora 
+
+This folder provides a fully functional skeleton for integrating with Certora.
+There are two configurations:
+
+
+
+## Run From the Command Line
+
+Follow this guide to install the prover and its dependencies:
+[Installation Guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html)
+
+Once installations are set, run from this directory:  
+`certoraRun ./certora/confs/ghost.conf`  
+
+## Recommended IDE
+
+We recommended using VSCode with the following extension:
+[Certora Verification Language LSP](https://marketplace.visualstudio.com/items?itemName=Certora.evmspec-lsp)
+This extension is found in the VSCode extensions/marketplace. It provides syntactic support for the Certora Verification Language (CVL) - the language in which we will be writing specifications.
+
+## Files
+
+The folder `specs` contains the specification files: 
+1. `ghost.spec` contains basic rules that are not dependent on any interface.
+2. `moreExmaplesERC20.spec` contains basic examples including ghost, hooks, and multi-contract features.
+
+Folder `confs` contains the configuration files for running the Certora Prover:  
+1. File `ghost.conf` for running `ghost.spec` on `ghost.sol` file.  
+This configuration is suitable for a standalone project, containing:  
+    * external calls are assumed to be non-state changing and return random values on each call.  
+    * loops are unrolled three times.   
+    * calls to fallbacks are assumed to be side-effect-free and only update the native balance.   
+2. File `ghostWithERC20s.conf` running `moreExmaplesERC20.spec` on `ghost.sol` with additional ERC20-related contracts.   
+This demonstrates how to set up a project with multi-contract 
+
+
+## CI Integration
+
+This repository contains a Certora setup in GitHub actions.
+You will need to provide your secret `CERTORAKEY` to GitHub. 
+
+
+
+## Mutation Testing
+The Certora Prover is integrated with <a href=https://www.certora.com/gambit>Gambit</a>, an open-source Solidity mutation testing tool. Mutation testing can give you an estimate of the coverage of your verification.
+
+To run the mutation test from this directory, run:  
+ `certoraMutate --prover_conf certora/confs/ghost.conf --mutation_conf certora/confs/mutation.mconf`. 
+ However, this does not generate any mutates as 'ghost.sol' is too small. 
+ `certoraMutate --prover_conf certora/confs/ghostWithERC20s.conf --mutation_conf certora/confs/mutationWithERC20.mconf ` mutates `SimpleERC20.sol`.  
+
+
+## CVL Examples and Docs
+See more <a href="https://github.com/Certora/Examples/tree/master/CVLByExample" target="_blank">CVL specification general examples</a>
+and <a href="https://docs.certora.com" target="_blank">Documenation</a>.
+More mutation configurations can be found in the [certoraInit repo](https://github.com/Certora/CertoraInit"). 

certora/confs/ghost.conf

@@ -0,0 +1,22 @@
+{
+//    list of files that are part of the system 
+  "files": [
+    "src/contracts/Ghost.sol"
+  ],
+//    // matching the main contract to verify and its spec file - Ghost.sol:ghost.spec 
+  "verify": "Ghost:certora/specs/ghost.spec",
+//    apply very important sanity checks that should always be run before finishing a verification
+//    docs: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html
+  "rule_sanity" :"basic",
+//    constraint loops to three unrolls, i.e. every loop will run for at most 3 iterations. 3 is usually enough to cover all interesting cases
+//    this in turn will impose requirements on the length of the array (etc.) that a loop is iterating on (the stop condition of the loop)
+//    docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html//loop-iter
+  "loop_iter" : "3",
+//   docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html//optimistic-loop
+  "optimistic_loop" : true,
+  "prover_args": [
+      //  assume calls to fallback are to EOAs (e.g., no code, only balance updated)
+      " -optimisticFallback true"
+  ],
+  "msg": "Ghost template file"
+}

certora/confs/ghostWithERC20s.conf

@@ -0,0 +1,25 @@
+  // A default configuration for a contract using ERC20s
+{
+//    list of files that are a part of the system 
+  "files": [
+    "src/contracts/Ghost.sol",
+    "certora/helpers/ERC20Helper.sol",
+    "certora/helpers/SimpleERC20.sol"
+  ],
+//    main contract to verify (Ghost):spec file (moreExamplesERC20) 
+  "verify": "Ghost:certora/specs/moreExamplesERC20.spec",
+//    apply very important sanity checks that should always be run before finishing a verification
+//    docs: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html
+  "rule_sanity" :"basic",
+//    assume 3 unrolling of loops, i.e. every loop will run for at most 3 iterations. 3 is usually enough in most cases.
+//    this in turn will impose requirements on the length of the array (etc.) that a loop is iterating on (the stop condition of the loop)
+//    docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html//loop-iter
+  "loop_iter" : "3",
+//   docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html//optimistic-loop
+  "optimistic_loop" : true,
+  "prover_args": [
+        //  assume calls to fallback are to EOAs (e.g., no code, only balance updated)
+        " -optimisticFallback true"
+    ],
+  "msg": "Ghost with ERC20 template file"
+}

certora/confs/mutation.mconf

@@ -0,0 +1,9 @@
+{
+    "gambit": [
+        {
+            "filename" : "../../src/contracts/Ghost.sol",
+            "num_mutants": 1
+        }
+    ],
+    "msg": "basic mutation configuration"
+} 

certora/confs/mutationWithERC20.mconf

@@ -0,0 +1,9 @@
+{
+    "gambit": [
+        {
+            "filename" : "../helpers/SimpleERC20.sol",
+            "num_mutants": 5
+        }
+    ],
+    "msg": "basic mutation configuration"
+} 

certora/helpers/ERC20Helper.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+
+//probably repalce with an import to the selected library
+interface IERC20 {
+
+     function balanceOf(address account) external view returns (uint256);
+}
+
+contract ERC20Helper {
+    function tokenBalanceOf(address token, address user) public view returns (uint256) {
+            return IERC20(token).balanceOf(user);
+    }
+}

certora/helpers/SimpleERC20.sol

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+//a symbolic erc20 for verification
+
+
+contract SimpleERC20 {
+
+    uint256 private _totalSupply;
+    mapping(address => uint256) private _balance;
+    mapping(address => mapping(address => uint256)) private _allowance;
+
+    function totalSupply() public view returns (uint256) {  
+        return _totalSupply;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return _balance[account];
+    }
+
+    function allowance(address owner, address spender) public view returns (uint256) {
+        return _allowance[owner][spender];
+    }
+
+    function approve(address spender, uint256 amount) external returns (bool) {
+        _allowance[msg.sender][spender] = amount;
+        return true;
+    }
+
+    function transfer(address recipient, uint256 amount) external returns (bool) {
+        _balance[msg.sender] -= amount;
+        _balance[recipient] += amount;
+
+        return true;
+    }
+
+    function transferFrom(address from,address recipient,uint256 amount) external returns (bool) {
+        if (_allowance[from][msg.sender] != type(uint256).max) {
+            _allowance[from][msg.sender] -= amount;}
+        _balance[from] -= amount;
+        _balance[recipient] += amount;
+
+        return true;
+    }
+}