Set up certora and implement first rules (#122)

Co-authored-by: 0xb337r007 <0xe4e5@proton.me>
Co-authored-by: Adam Uhlíř <adam@uhlir.dev>

.github/workflows/ci.yml

@@ -26,3 +26,46 @@ jobs:
           path: fuzzing/corpus
           key: fuzzing
       - run: npm run fuzz
+
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install Java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install Certora CLI
+        run: pip3 install certora-cli==7.6.3
+
+      - name: Install Solidity
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.23/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+
+      - name: "Install Node.js"
+        uses: "actions/setup-node@v3"
+        with:
+          cache: "npm"
+          node-version: "lts/*"
+
+      - name: "Install the Node.js dependencies"
+        run: "npm install"
+
+      - name: Verify rules
+        run: "npm run verify"
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16

.gitignore

@@ -3,3 +3,4 @@ cache
 artifacts
 deployment-localhost.json
 crytic-export
+.certora_internal

Readme.md

@@ -25,6 +25,23 @@ To start a local Ethereum node with the contracts deployed, execute:
 This will create a `deployment-localhost.json` file containing the addresses of
 the deployed contracts.
 
+
+Running the prover
+------------------
+
+To run the formal verification rules using Certora, first, make sure you have Java (JDK >= 11.0) installed on your machine, and then  install the Certora CLI
+
+```
+$ pip install certora-cli
+```
+
+Once that is done the `certoraRun` command can be used to send CVL specs to the prover.
+
+You can run Certora's specs with the provided `npm` script:
+
+    npm run verify
+
+
 Overview
 --------
 

certora/confs/Marketplace.conf

@@ -0,0 +1,21 @@
+{
+    "files": [
+        "contracts/Marketplace.sol",
+        "contracts/Groth16Verifier.sol",
+        "certora/helpers/ERC20A.sol",
+    ],
+    "parametric_contracts": ["Marketplace"],
+    "link" : [
+        "Marketplace:_token=ERC20A",
+        "Marketplace:_verifier=Groth16Verifier"
+    ],
+    "msg": "Verifying Marketplace",
+    "rule_sanity": "basic",
+    "verify": "Marketplace:certora/specs/Marketplace.spec",
+    "optimistic_loop": true,
+    "loop_iter": "3",
+    "optimistic_hashing": true,
+    "hashing_length_bound": "512",
+}
+
+

certora/helpers/ERC20A.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.23;
+
+import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
+
+contract ERC20A is ERC20 {
+    constructor(string memory name_, string memory symbol_) ERC20(name_, symbol_) {}
+}

certora/specs/Marketplace.spec

@@ -0,0 +1,58 @@
+using ERC20A as Token;
+
+/*--------------------------------------------
+|              Ghosts and hooks              |
+--------------------------------------------*/
+
+ghost mathint totalReceived;
+
+hook Sload uint256 defaultValue currentContract._marketplaceTotals.received {
+    require totalReceived >= to_mathint(defaultValue);
+}
+
+hook Sstore currentContract._marketplaceTotals.received uint256 defaultValue (uint256 defaultValue_old) {
+    totalReceived = totalReceived + defaultValue - defaultValue_old;
+}
+
+ghost mathint totalSent;
+
+hook Sload uint256 defaultValue currentContract._marketplaceTotals.sent {
+    require totalSent >= to_mathint(defaultValue);
+}
+
+hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint256 defaultValue_old) {
+    totalSent = totalSent + defaultValue - defaultValue_old;
+}
+
+/*--------------------------------------------
+|                 Properties                 |
+--------------------------------------------*/
+
+rule sanity(env e, method f) {
+    calldataarg args;
+    f(e, args);
+    assert true;
+    satisfy true;
+}
+
+rule totalReceivedCannotDecrease(env e, method f) {
+    mathint total_before = totalReceived;
+
+    calldataarg args;
+    f(e, args);
+
+    mathint total_after = totalReceived;
+
+    assert total_after >= total_before;
+}
+
+rule totalSentCannotDecrease(env e, method f) {
+    mathint total_before = totalSent;
+
+    calldataarg args;
+    f(e, args);
+
+    mathint total_after = totalSent;
+
+    assert total_after >= total_before;
+}

contracts/FuzzMarketplace.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity ^0.8.0;
+pragma solidity ^0.8.23;
 
 import "./TestToken.sol";
 import "./Marketplace.sol";

contracts/TestEndian.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity ^0.8.0;
+pragma solidity ^0.8.23;
 
 import "./Endian.sol";
 

contracts/TestMarketplace.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity ^0.8.0;
+pragma solidity ^0.8.23;
 
 import "./Marketplace.sol";
 

contracts/TestProofs.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity ^0.8.0;
+pragma solidity ^0.8.23;
 
 import "./Proofs.sol";
 

contracts/TestToken.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity ^0.8.0;
+pragma solidity ^0.8.23;
 
 import "@openzeppelin/contracts/token/ERC20/ERC20.sol";
 

package.json

@@ -9,7 +9,9 @@
     "format": "prettier --write contracts/**/*.sol test/**/*.js",
     "format:check": "prettier --check contracts/**/*.sol test/**/*.js",
     "lint": "solhint contracts/**.sol",
-    "deploy": "hardhat deploy"
+    "deploy": "hardhat deploy",
+    "verify": "npm run verify:marketplace",
+    "verify:marketplace": "certoraRun certora/confs/Marketplace.conf"
   },
   "devDependencies": {
     "@nomiclabs/hardhat-ethers": "^2.2.1",