feat: formal verification & fuzz campaign

.github/workflows/coverage_check.yml

@@ -0,0 +1,72 @@
+name: Coverage check on main push
+
+on: [push]
+
+env:
+    COVERAGE_SENSITIVITY_PERCENT: 1
+
+jobs:
+  upload-coverage:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Use Node.js
+        uses: actions/setup-node@v4
+        with:
+          node-version: 18.x
+          cache: 'yarn'
+
+      - name: Install dependencies
+        run: yarn --frozen-lockfile --network-concurrency 1
+
+      - name: Run coverage
+        shell: bash
+        run: forge coverage --report summary --report lcov
+
+      - name: Setup LCOV
+        uses: hrishikesh-kadam/setup-lcov@v1
+
+      - name: Filter directories
+        run: lcov --remove lcov.info 'test/*' 'script/*' --output-file lcovNew.info --rc lcov_branch_coverage=1 --rc derive_function_end_line=0 --ignore-errors unused
+
+      - name: Capture coverage output
+        id: new-coverage
+        uses: zgosalvez/github-actions-report-lcov@v4
+        with:
+          coverage-files: lcovNew.info
+
+      - name: Retrieve previous coverage
+        uses: actions/download-artifact@v2
+        with:
+          name: coverage.info
+        continue-on-error: true
+
+      - name: Check if a previous coverage exists
+        run: |
+          if [ ! -f coverage.info ]; then
+            echo "Artifact not found. Initializing at 0"
+            echo "0" >> coverage.info
+          fi
+
+      - name: Compare previous coverage
+        run: |
+          old=$(cat coverage.info)
+          new=$(( ${{ steps.new-coverage.outputs.total-coverage }} + ${{ env.COVERAGE_SENSITIVITY_PERCENT }} ))
+          if [ "$new" -lt "$old" ]; then
+            echo "Coverage decreased from $old to $new"
+            exit 1
+          fi
+          mv lcovNew.info coverage.info
+
+      - name: Upload the new coverage
+        uses: actions/upload-artifact@v2
+        with:
+          name: coverage.info
+          path: ./coverage.info

.github/workflows/ci.yml → .github/workflows/tests.yml

@@ -64,6 +64,68 @@ jobs:
       - name: Run tests
         run: yarn test:integration
 
+  echidna-tests:
+    name: Echidna Test
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Use Node.js
+        uses: actions/setup-node@v3
+        with:
+          node-version: 18.x
+          cache: 'yarn'
+
+      - name: Install dependencies
+        run: yarn --frozen-lockfile --network-concurrency 1
+
+      - name: Compile contracts
+        run: |
+          forge build --build-info
+
+      - name: Run Echidna
+        uses: crytic/echidna-action@v2
+        with:
+          files: .
+          contract: InvariantGreeter
+          test-mode: assertion
+          crytic-args: --ignore-compile
+
+  halmos-tests:
+    name: Run symbolic execution tests
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Use Node.js
+        uses: actions/setup-node@v3
+        with:
+          node-version: 18.x
+          cache: 'yarn'
+
+      - name: Install dependencies
+        run: yarn --frozen-lockfile --network-concurrency 1
+
+      - name: Precompile with via-ir=false
+        run: yarn build
+
+      - name: Run tests
+        run: yarn test:integration
+
   lint:
     name: Lint Commit Messages
     runs-on: ubuntu-latest

.solhint.tests.json

@@ -6,17 +6,17 @@
     "quotes": ["error", "single"],
     "func-visibility": ["warn", { "ignoreConstructors": true }],
     "not-rely-on-time": "off",
-    "func-name-mixedcase": "off",
+    "style-guide-casing": "off",
     "var-name-mixedcase": "off",
     "const-name-snakecase": "off",
     "no-inline-assembly": "off",
-    "no-empty-blocks": "off",
+    "no-empty-blocks": "error",
     "definition-name-capwords": "off",
     "named-parameters-function": "off",
     "no-global-import": "off",
     "max-states-count": "off",
     "private-vars-leading-underscore": ["warn", { "strict": false }],
-    "ordering": "warn",
+    "ordering": "off",
     "immutable-name-snakecase": "warn",
     "avoid-low-level-calls": "off",
     "one-contract-per-file": "off",

README.md

@@ -18,8 +18,10 @@
   <dt>Deployment scripts</dt>
   <dd>Sample scripts to deploy contracts on both mainnet and testnet.</dd>
 
-  <dt>Sample Integration & Unit tests</dt>
+  <dt>Sample Integration, Unit, Property-based fuzzed and symbolic tests</dt>
   <dd>Example tests showcasing mocking, assertions and configuration for mainnet forking. As well it includes everything needed in order to check code coverage.</dd>
+  <dd>Unit tests are built based on the <a href="https://twitter.com/PaulRBerg/status/1682346315806539776">Branched-Tree Technique</a>, using <a href="https://github.com/alexfertel/bulloak">Bulloak</a>.
+  <dd>Formal verification and property-based fuzzing are achieved with <a href="https://github.com/a16z/halmos">Halmos</a> and <a href="https://github.com/crytic/echidna">Echidna</a> (resp.).
 
   <dt>Linter</dt>
   <dd>Simple and fast solidity linting thanks to forge fmt.</dd>
@@ -78,6 +80,18 @@ In order to just run integration tests, run:
 yarn test:integration
 ```
 
+In order to just run the echidna fuzzing campaign (requires [Echidna](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/introduction/installation.md) installed), run:
+
+```bash
+yarn test:fuzz
+```
+
+In order to just run the symbolic execution tests (requires [Halmos](https://github.com/a16z/halmos/blob/main/README.md#installation) installed), run:
+
+```bash
+yarn test:symbolic
+```
+
 In order to check your current code coverage, run:
 
 ```bash

package.json

@@ -22,7 +22,9 @@
     "lint:sol-tests": "solhint -c .solhint.tests.json 'test/**/*.sol'",
     "prepare": "husky install",
     "test": "forge test -vvv",
+    "test:fuzz": "echidna test/invariants/fuzz/Greeter.t.sol --contract GreeterInvariant --corpus-dir test/invariants/fuzz/echidna_coverage/ --test-mode assertion",
     "test:integration": "forge test --match-contract Integration -vvv",
+    "test:symbolic": "halmos",
     "test:unit": "forge test --match-contract Unit -vvv",
     "test:unit:deep": "FOUNDRY_FUZZ_RUNS=5000 yarn test:unit"
   },
@@ -37,6 +39,7 @@
     "@commitlint/config-conventional": "19.2.2",
     "@defi-wonderland/natspec-smells": "1.1.1",
     "forge-std": "github:foundry-rs/forge-std#1.8.2",
+    "halmos-cheatcodes": "github:a16z/halmos-cheatcodes#c0d8655",
     "husky": ">=8",
     "lint-staged": ">=10",
     "solhint-community": "4.0.0",

remappings.txt

@@ -1,4 +1,5 @@
 forge-std/=node_modules/forge-std/src
+halmos-cheatcodes=node_modules/halmos-cheatcodes
 
 contracts/=src/contracts
 interfaces/=src/interfaces

test/invariants/PROPERTIES.md

@@ -0,0 +1,4 @@
+| Properties                                        | Type       |
+|---------------------------------------------------|------------|
+| Greeting should never be empty | Valid state |
+| Only the owner can set the greeting | State transition |

test/invariants/fuzz/Greeter.t.sol

@@ -0,0 +1,37 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.23;
+
+import {Greeter, IERC20} from 'contracts/Greeter.sol';
+
+interface IHevm {
+  function prank(address) external;
+}
+
+contract InvariantGreeter {
+  IHevm internal _hevm = IHevm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+
+  Greeter internal _targetContract;
+
+  constructor() {
+    _targetContract = new Greeter('a', IERC20(address(1)));
+  }
+
+  function checkGreeterNeverEmpty(string memory newGreeting) public {
+    // Execution
+    (bool success,) = address(_targetContract).call(abi.encodeCall(Greeter.setGreeting, newGreeting));
+
+    // Check output condition
+    assert((success && keccak256(bytes(_targetContract.greeting())) != keccak256(bytes(''))) || !success);
+  }
+
+  function checkOnlyOwnerSetsGreeting(address caller) public {
+    // Input conditions
+    _hevm.prank(caller);
+
+    // Execution
+    (bool success,) = address(this).call(abi.encodeCall(Greeter.setGreeting, 'hello'));
+
+    // Check output condition
+    assert((success && msg.sender == _targetContract.OWNER()) || (!success && msg.sender != _targetContract.OWNER()));
+  }
+}

test/invariants/symbolic/Greeter.t.sol

@@ -0,0 +1,58 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.23;
+
+import {Greeter, IERC20} from 'contracts/Greeter.sol';
+
+import {Test} from 'forge-std/Test.sol';
+import {SymTest} from 'halmos-cheatcodes/src/SymTest.sol'; // See https://github.com/a16z/halmos-cheatcodes?tab=readme-ov-file
+
+contract SymbolicGreeter is SymTest, Test {
+  Greeter public targetContract;
+
+  function setUp() public {
+    string memory initialGreeting = svm.createString(64, 'initial greeting');
+    address token = svm.createAddress('token');
+
+    targetContract = new Greeter(initialGreeting, IERC20(token));
+  }
+
+  function check_validState_greeterNeverEmpty(address caller) public {
+    // Input conditions: any caller
+    vm.prank(caller);
+
+    // Execution: Halmos cannot use a dynamic-sized array, iterate over multiple string lengths
+    bool success;
+    for (uint256 i = 1; i < 3; i++) {
+      string memory greeting = svm.createString(i, 'greeting');
+      (success,) = address(targetContract).call(abi.encodeCall(Greeter.setGreeting, (greeting)));
+
+      // Output condition check
+      vm.assume(success); // discard failing calls
+      assert(keccak256(bytes(targetContract.greeting())) != keccak256(bytes('')));
+    }
+
+    // Add the empty string (bypass the non-empty check of svm.createString)
+    (success,) = address(targetContract).call(abi.encodeCall(Greeter.setGreeting, ('')));
+
+    // Output condition check
+    vm.assume(success); // discard failing calls
+    assert(keccak256(bytes(targetContract.greeting())) != keccak256(bytes('')));
+  }
+
+  function check_setGreeting_onlyOwnerSetsGreeting(address caller) public {
+    // Input conditions
+    string memory newGreeting = svm.createString(64, 'new greeting');
+
+    // Execution
+    vm.prank(caller);
+    (bool success,) = address(targetContract).call(abi.encodeCall(Greeter.setGreeting, (newGreeting)));
+
+    // Output condition check
+    if (success) {
+      assert(caller == targetContract.OWNER());
+      assert(keccak256(bytes(targetContract.greeting())) == keccak256(bytes(newGreeting)));
+    } else {
+      assert(caller != targetContract.OWNER() || keccak256(bytes(newGreeting)) == keccak256(bytes('')));
+    }
+  }
+}