dev

.github/workflows/certora.yml

@@ -0,0 +1,32 @@
+name: certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        conf:
+          - Terms
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+      - name: Install certora
+        run: pip install certora-cli
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.28/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.28
+      - name: Verify ${{ matrix.conf }}
+        run: certoraRun certora/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.github/workflows/forge.yml

@@ -0,0 +1,21 @@
+name: forge
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  foundry:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+      - name: Check formatting
+        run: forge fmt --check
+      - name: Run Forge tests
+        run: forge test

.gitignore

@@ -0,0 +1,3 @@
+cache
+out
+.certora_internal

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "lib/forge-std"]
+	path = lib/forge-std
+	url = https://github.com/foundry-rs/forge-std

certora/Terms.conf

@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/helpers/TermsHelpers.sol",
+    "certora/dispatch/ERC20Standard.sol"
+  ],
+  "solc": "solc-0.8.28",
+  "verify": "TermsHelpers:certora/Terms.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "optimistic_hashing": true,
+  "solc_via_ir": true,
+  "hashing_length_bound": "320",
+  "msg": "Terms" 
+}

certora/Terms.spec

@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+/// METHODS ///
+
+methods {
+    function withdrawable(bytes32 id) external returns uint256 envfree;
+    function balanceOf(address, address) external returns uint256 envfree;
+    function id(Terms.Term) external returns bytes32 envfree;
+
+    // function _.transfer(address, uint256) external => DISPATCHER(true);
+    // function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+    // function _.balanceOf(address) external => DISPATCHER(true);
+}
+
+/// HOOKS ///
+
+persistent ghost mapping(bytes32 => mathint) sumBondSharesOf {
+    init_state axiom (forall bytes32 id. sumBondSharesOf[id] == 0);
+}
+hook Sload uint256 bondSharesOfOwner bondSharesOf[KEY address owner][KEY bytes32 id] {
+    require sumBondSharesOf[id] >= to_mathint(bondSharesOfOwner);
+}
+hook Sstore bondSharesOf[KEY address owner][KEY bytes32 id] uint256 newBondShares (uint256 oldBondShares) {
+    sumBondSharesOf[id] = sumBondSharesOf[id] - oldBondShares + newBondShares;
+}
+
+persistent ghost mapping(bytes32 => mathint) sumDebtOf {
+    init_state axiom (forall bytes32 id. sumDebtOf[id] == 0);
+}
+hook Sload uint256 debtOfOwner debtOf[KEY address owner][KEY bytes32 id] {
+    require sumDebtOf[id] >= to_mathint(debtOfOwner);
+}
+hook Sstore debtOf[KEY address owner][KEY bytes32 id] uint256 newDebt (uint256 oldDebt) {
+    sumDebtOf[id] = sumDebtOf[id] - oldDebt + newDebt;
+}
+
+/// SANITY ///
+
+invariant sanitySumBondShares(bytes32 id)
+    sumBondSharesOf[id] >= 0;
+
+invariant sanitySumDebt(bytes32 id)
+    sumDebtOf[id] >= 0;
+
+rule satisfyMatch(env e, calldataarg args) {
+    MATCH(e, args);
+    satisfy true;
+}
+
+/// INVARIANTS ///
+
+// strong invariant sums(bytes32 id)
+//     sumBondOf[id] == sumDebtOf[id] + withdrawable(id);
+
+// invariant balances(TermsHelpers.Term term)
+//     balanceOf(term.loanToken, currentContract) >= withdrawable(id(term));

certora/dispatch/ERC20NoRevert.sol

@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20NoRevert {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) {
+        if (balanceOf[_from] < _amount) {
+            return false;
+        }
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+        return true;
+    }
+
+    function transfer(address _to, uint256 _amount) public returns (bool) {
+        return _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        if (allowance[_from][msg.sender] < _amount) {
+            return false;
+        }
+        allowance[_from][msg.sender] -= _amount;
+        return _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}

certora/dispatch/ERC20Standard.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20Standard {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) {
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+        return true;
+    }
+
+    function transfer(address _to, uint256 _amount) public returns (bool) {
+        return _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        allowance[_from][msg.sender] -= _amount;
+        return _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}

certora/dispatch/ERC20USDT.sol

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20USDT {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal {
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+    }
+
+    function transfer(address _to, uint256 _amount) public {
+        _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public {
+        if (allowance[_from][msg.sender] < type(uint256).max) {
+            allowance[_from][msg.sender] -= _amount;
+        }
+        _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        require(!((_amount != 0) && (allowance[msg.sender][_spender] != 0)));
+
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}

certora/helpers/TermsHelpers.sol

@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import {Terms, Term, IERC20} from "../../src/Terms.sol";
+
+contract TermsHelpers is Terms {
+    function balanceOf(address token, address account) external view returns (uint256) {
+        return IERC20(token).balanceOf(account);
+    }
+
+    function id(Term memory term) external pure returns (bytes32) {
+        return _id(term);
+    }
+}

foundry.toml

@@ -0,0 +1,2 @@
+[profile.default]
+via_ir = true