Certora - Formal verification of KatToken and MerkleMinter

.github/workflows/run-confs.yml

@@ -0,0 +1,45 @@
+name: test
+
+on: pull_request
+
+env:
+  FOUNDRY_PROFILE: ci
+  CONFIGS: |
+    certora/confs/exp2-check-summary.conf
+    certora/confs/exp2-implementation.conf
+    certora/confs/KatToken-exp2.conf
+    certora/confs/KatToken-simple.conf
+    certora/confs/MerkleMinter-simple.conf
+    certora/confs/sanity-KatToken.conf
+    certora/confs/sanity-MerkleMinter.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: install foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: install dependencies
+        run: |
+          forge soldeer install
+          npm i
+
+      - name: run configs
+        uses: Certora/certora-run-action@v1
+        with:
+          configurations: ${{ env.CONFIGS }}
+          solc-versions: 0.8.28
+          solc-remove-version-prefix: "0."
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -14,4 +14,12 @@ docs/
 .env
 
 dependencies/
-node_modules/
+node_modules/
+
+# Certora files
+.certora_internal/
+.venv/
+emv-*-certora-*
+package-lock.json
+remappings.txt
+soldeer.lock

certora/.gitattributes

@@ -0,0 +1,3 @@
+*.spec linguist-language=Solidity
+*.conf linguist-detectable
+*.conf linguist-language=JSON5

certora/confs/KatToken.conf

@@ -0,0 +1,20 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/KatTokenHarness.sol"
+    ],
+    "global_timeout": "7200",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "msg": "KatToken",
+    "packages": [
+        "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree",
+        "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0",
+        "forge-std-1.9.4=dependencies/forge-std-1.9.4"
+    ],
+    "process": "emv",
+    "server": "production",
+    "solc": "solc8.28",
+    "solc_via_ir": false,
+    "verify": "KatTokenHarness:certora/specs/KatToken.spec"
+}

certora/confs/MerkleMinter.conf

@@ -0,0 +1,26 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "src/MerkleMinter.sol",
+        "src/KatToken.sol"
+    ],
+    "global_timeout": "7200",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "link": [
+        "MerkleMinter:katToken=KatToken"
+    ],
+    //"parametric_contracts": [ "MerkleMinter" ],
+    "msg": "MerkleMinter",
+    "packages": [
+        "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree",
+        "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0",
+        "forge-std-1.9.4=dependencies/forge-std-1.9.4"
+    ],
+
+    "process": "emv",
+    "server": "production",
+    "solc": "solc8.28",
+    "solc_via_ir": false,
+    "verify": "MerkleMinter:certora/specs/MerkleMinter.spec"
+}

certora/confs/powUtil.conf

@@ -0,0 +1,23 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/PowUtilHarness.sol",
+        "src/KatToken.sol",
+    ],
+    "global_timeout": "7200",
+    "smt_timeout": "7200",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree",
+        "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0",
+        "forge-std-1.9.4=dependencies/forge-std-1.9.4"
+    ],
+
+    "process": "emv",
+    "server": "production",
+    "solc": "solc8.28",
+    "solc_via_ir": false,
+    "verify": "PowUtilHarness:certora/specs/powUtil.spec",
+    "msg": "Check exp2",
+}

certora/harnesses/KatTokenHarness.sol

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: SEE LICENSE IN LICENSE
+pragma solidity 0.8.28;
+import {KatToken} from "src/KatToken.sol";
+
+contract KatTokenHarness is KatToken {
+    constructor(
+        string memory _name,
+        string memory _symbol,
+        address _inflationAdmin,
+        address _inflationBeneficiary,
+        address _merkleMinter
+    ) KatToken(_name, _symbol, _inflationAdmin, _inflationBeneficiary, _merkleMinter) 
+    {
+    }
+
+    function get_lastMintCapacityIncrease() public view returns (uint256) {
+        return lastMintCapacityIncrease;
+    }
+
+    function get_distributedSupplyCap() public view returns (uint256) {
+        return distributedSupplyCap;
+    }
+
+}

certora/harnesses/PowUtilHarness.sol

@@ -0,0 +1,11 @@
+//SPDX-License-Identifier: MIT
+pragma solidity 0.8.28;
+
+import {PowUtil} from "../../src/Powutil.sol";
+
+// Makes it easier to access `PowUtil.exp2`.
+contract PowUtilHarness {
+    function exp2(uint256 x) public pure returns (uint256 result) {
+        return PowUtil.exp2(x);
+    }
+}

certora/scripts/run.sh

@@ -0,0 +1,7 @@
+certoraRun certora/confs/KatToken.conf
+certoraRun certora/confs/KatToken.conf --verify KatTokenHarness:certora/specs/KatToken_changeInflation.spec --msg changeInflation_revertConditions
+
+# the rule indexIsClaimedValueChange requires using bitVector theory
+certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" 
+# all the other rules can be verified using the default integer theory
+certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange

certora/specs/KatToken.spec

@@ -0,0 +1,207 @@
+import "./exp2-summary.spec";
+
+methods {
+    function inflationAdmin() external returns (address) envfree;
+    function pendingInflationAdmin() external returns (address) envfree;
+    function inflationBeneficiary() external returns (address) envfree;
+    function pendingInflationBeneficiary() external returns (address) envfree;
+    function inflationFactor() external returns (uint256) envfree;
+    function MAX_INFLATION() external returns (uint256) envfree;
+    function merkleMinter() external returns (address) envfree;
+    function mintCapacity(address) external returns (uint256) envfree;
+
+    //harness methods declared envfree
+    function get_lastMintCapacityIncrease() external returns (uint256) envfree;
+    function get_distributedSupplyCap() external returns (uint256) envfree;
+
+    function ERC20._mint(address to, uint256 amount) internal
+        => _mintCVL(to, amount);
+
+    //MerkleProof
+    function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE;
+
+    function _.eip712Domain() external => NONDET DELETE;
+}
+
+rule integrityOfchangeInflationAdmin(env e) {
+    address oldOwner = inflationAdmin();
+    address newOwner;
+
+    changeInflationAdmin(e, newOwner);
+
+    assert(e.msg.sender == oldOwner);
+    assert(pendingInflationAdmin() == newOwner);
+}
+
+rule integrityOfchangeInflationBeneficiary(env e) {
+    address oldOwner = inflationBeneficiary();
+    address newOwner;
+
+    changeInflationBeneficiary(e, newOwner);
+
+    assert(e.msg.sender == oldOwner);
+    assert(pendingInflationBeneficiary() == newOwner);
+}
+
+rule lastMintCapacityIncreaseNeverDecreases(env e, method f)
+{
+    uint256 lastMintCapacityIncrease_pre = get_lastMintCapacityIncrease();
+
+    calldataarg args;
+    f(e, args);
+    uint256 lastMintCapacityIncrease_post = get_lastMintCapacityIncrease();
+    assert lastMintCapacityIncrease_post >= lastMintCapacityIncrease_pre;
+}
+
+rule distributedSupplyCapNeverDecreases(env e, method f)
+{
+    uint256 distributedSupplyCap_pre = get_distributedSupplyCap();
+
+    calldataarg args;
+    f(e, args);
+    uint256 distributedSupplyCap_post = get_distributedSupplyCap();
+    assert distributedSupplyCap_post >= distributedSupplyCap_pre;
+}
+
+rule integrityOfDistributeMintCapacity(env e) {
+    address to;
+    uint256 amount;
+
+    uint256 ownCapacityBefore = mintCapacity(e.msg.sender);
+    uint256 toCapacityBefore = mintCapacity(to);
+
+    distributeMintCapacity(e, to, amount);
+
+    uint256 ownCapacityAfter = mintCapacity(e.msg.sender);
+    uint256 toCapacityAfter = mintCapacity(to);
+
+    assert(ownCapacityBefore >= amount);
+    assert(ownCapacityBefore + toCapacityBefore == ownCapacityAfter + toCapacityAfter);
+}
+
+ghost mapping(address => mathint) mintedTo;
+ghost mathint totalMintCapacityChange;
+ghost mathint totalMintedChange;
+
+function _mintCVL(address to, uint256 amount)
+{
+    mintedTo[to] = mintedTo[to] + amount;
+    totalMintedChange = totalMintedChange + amount;
+}
+
+hook Sstore KatTokenHarness.mintCapacity[KEY address user] uint256 newCap (uint256 oldCap) {
+    totalMintCapacityChange = totalMintCapacityChange + newCap - oldCap;
+}
+
+function initGhosts()
+{
+    totalMintCapacityChange = 0;
+    totalMintedChange = 0;
+}
+
+rule mintCapacityPlusMintedNeverDecrease(env e, method f)
+{
+    initGhosts();
+    calldataarg args;
+    f(e, args);
+    assert totalMintedChange + totalMintCapacityChange >= 0;
+}
+
+rule mintCapacityPlusMintedEqualsDistributedSupplyCap(env e, method f)
+{
+    initGhosts();
+    uint256 distributedSupplyCap_pre = get_distributedSupplyCap();
+    calldataarg args;
+    f(e, args);
+    uint256 distributedSupplyCap_post = get_distributedSupplyCap();
+    assert distributedSupplyCap_post - distributedSupplyCap_pre ==
+        totalMintedChange + totalMintCapacityChange;
+}
+
+/**
+ * The inflation factor is bounded by MAX_INFLATION.
+ */
+invariant inflationFactorIsBounded()
+    inflationFactor() <= MAX_INFLATION();
+
+rule integrityOfRenounceInflationAdmin(env e, method f)
+{
+    address admin_pre = inflationAdmin();
+    renounceInflationAdmin(e);
+    address admin_post = inflationAdmin();
+
+    assert admin_pre == e.msg.sender;
+    assert admin_post == 0;
+}
+
+rule integrityOfRenounceInflationBeneficiary(env e, method f)
+{
+    address beneficiary_pre = inflationBeneficiary();
+    renounceInflationBeneficiary(e);
+    address beneficiary_post = inflationBeneficiary();
+
+    assert beneficiary_pre == e.msg.sender;
+    assert beneficiary_post == 0;
+}
+
+// once renounceInflationAdmin is performed, the inflationAdmin will always be zero
+// we've proved that renounceInflationAdmin changes it to zero so here we just prove
+// that it cannot change from 0 to non-zero
+rule inflationAdminValueChange(env e, method f)
+{
+    requireInvariant zeroAdminThenZeroPendingAdmin();
+    address admin_pre = inflationAdmin();
+    require e.msg.sender != 0;
+    calldataarg args;
+    f(e, args);
+    address admin_post = inflationAdmin();
+    assert admin_pre == 0 => admin_post == 0;
+}
+
+// once renounceInflationBeneficiary is performed, the inflationBeneficiary will always be zero
+// we've proved that renounceInflationBeneficiary changes it to zero so here we just prove
+// that it cannot change from 0 to non-zero
+rule inflationBeneficiaryValueChange(env e, method f)
+{
+    requireInvariant zeroBeneficiaryThenZeroPendingBeneficiary();
+    address beneficiary_pre = inflationBeneficiary();
+    require e.msg.sender != 0;
+    calldataarg args;
+    f(e, args);
+    address beneficiary_post = inflationBeneficiary();
+    assert beneficiary_pre == 0 => beneficiary_post == 0;
+}
+
+invariant mintCapacityOfZeroIsZero()
+    mintCapacity(0) == 0
+    { preserved
+        with (env e) 
+        { 
+            requireInvariant noBeneficiaryThenNoInflation();
+            require e.msg.sender != 0; 
+        }
+    }
+
+invariant noBeneficiaryThenNoInflation()
+    inflationBeneficiary() == 0 => inflationFactor() == 0
+    { preserved with (env e) 
+        { 
+            require e.msg.sender != 0; 
+        }
+    }
+
+invariant zeroAdminThenZeroPendingAdmin()
+    inflationAdmin() == 0 => pendingInflationAdmin() == 0
+    { preserved with (env e) 
+        { 
+            require e.msg.sender != 0; 
+        }
+    }
+
+invariant zeroBeneficiaryThenZeroPendingBeneficiary()
+    inflationBeneficiary() == 0 => pendingInflationBeneficiary() == 0
+    { preserved with (env e) 
+        { 
+            require e.msg.sender != 0; 
+        }
+    }