Kontrol Formal Verification for SecurityCouncilAzorius

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "lib/openzeppelin-contracts"]
 	path = lib/openzeppelin-contracts
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts
+[submodule "lib/kontrol-cheatcodes"]
+	path = lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes

foundry.toml

@@ -10,6 +10,7 @@ optimizer = true
 optimizer_runs = 10000
 via_ir = true
 fs_permissions = [{ access = "read", path = "./" }]
+no_match_path = "test/kontrol/**"
 
 [rpc_endpoints]
 mainnet = "${RPC_URL}"

kontrol.toml

@@ -0,0 +1,50 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = false
+rekompile                  = false
+verbose                    = false
+debug                      = false
+require                    = 'test/kontrol/kontrol-lemmas.k'
+module-import              = 'SecurityCouncilAzoriusKontrolInvariantTest:KONTROL-LEMMAS'
+ast                        = true
+auxiliary-lemmas           = true
+
+[prove]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 100000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 1
+max-frontier-parallel      = 6
+maintenance-rate           = 32
+assume-defined             = true
+no-log-rewrites            = true
+no-stack-checks            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify --equation-max-recursion 20 --equation-max-iterations 1000'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+auto_abstract              = true
+run-constructor            = false
+bmc-depth                  = 2
+match-test                 = [
+        "SecurityCouncilAzoriusKontrolInvariantTest.test_",
+    ]
+ast                        = true
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = true
+debug                      = false

test/kontrol/KontrolTest.sol

@@ -0,0 +1,117 @@
+pragma solidity ^0.8.19;
+
+import "forge-std/Vm.sol";
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+contract KontrolTest is Test, KontrolCheats {
+    // Note: there are lemmas dependent on `ethUpperBound`
+    uint256 constant ethMaxWidth = 96;
+    uint256 constant ethUpperBound = 2 ** ethMaxWidth;
+    // Note: 2 ** 35 takes us to year 3058
+    uint256 constant timeUpperBound = 2 ** 35;
+
+    function infoAssert(bool condition, string memory message) external pure {
+        if (!condition) {
+            revert(message);
+        }
+    }
+
+    enum Mode {
+        Assume,
+        Try,
+        Assert
+    }
+
+    function _establish(Mode mode, bool condition) internal pure returns (bool) {
+        if (mode == Mode.Assume) {
+            vm.assume(condition);
+            return true;
+        } else if (mode == Mode.Try) {
+            return condition;
+        } else {
+            assert(condition);
+            return true;
+        }
+    }
+
+    function _loadData(
+        address contractAddress,
+        uint256 slot,
+        uint256 offset,
+        uint256 width
+    ) internal view returns (uint256) {
+        // `offset` and `width` must not overflow the slot
+        assert(offset + width <= 32);
+
+        // Slot read mask
+        uint256 mask;
+        unchecked {
+            mask = (2 ** (8 * width)) - 1;
+        }
+        // Value right shift
+        uint256 shift = 8 * offset;
+
+        // Current slot value
+        uint256 slotValue = uint256(vm.load(contractAddress, bytes32(slot)));
+
+        // Isolate and return data to retrieve
+        return mask & (slotValue >> shift);
+    }
+
+    function _storeData(address contractAddress, uint256 slot, uint256 offset, uint256 width, uint256 value) internal {
+        // `offset` and `width` must not overflow the slot
+        assert(offset + width <= 32);
+        // and `value` must fit into the designated part
+        assert(width == 32 || value < 2 ** (8 * width));
+
+        // Slot update mask
+        uint256 maskLeft;
+        unchecked {
+            maskLeft = ~((2 ** (8 * (offset + width))) - 1);
+        }
+        uint256 maskRight = (2 ** (8 * offset)) - 1;
+        uint256 mask = maskLeft | maskRight;
+
+        value = (2 ** (8 * offset)) * value;
+
+        // Current slot value
+        uint256 slotValue = uint256(vm.load(contractAddress, bytes32(slot)));
+        // Updated slot value
+        slotValue = value | (mask & slotValue);
+
+        vm.store(contractAddress, bytes32(slot), bytes32(slotValue));
+    }
+
+    function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) {
+        return _loadData(contractAddress, slot, 0, 32);
+    }
+
+    function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) {
+        return address(uint160(_loadData(contractAddress, slot, 0, 20)));
+    }
+
+    function _storeUInt256(address contractAddress, uint256 slot, uint256 value) internal {
+        _storeData(contractAddress, slot, 0, 32, value);
+    }
+
+    function _storeAddress(address contractAddress, uint256 slot, address value) internal {
+        _storeData(contractAddress, slot, 0, 20, uint160(value));
+    }
+
+    function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal {
+        _storeUInt256(contractAddress, slot, uint256(value));
+    }
+
+    function _assumeNoOverflow(uint256 augend, uint256 addend) internal pure {
+        unchecked {
+            vm.assume(augend < augend + addend);
+        }
+    }
+
+    function freshBoundedUInt(uint256 upperBound, string memory name) internal view returns (uint8) {
+        uint8 value = freshUInt8(name);
+        vm.assume(value < upperBound);
+        return value;
+    }
+}

test/kontrol/MockAzorius.k.sol

@@ -0,0 +1,145 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.19;
+
+import {Enum, IAzorius} from "src/SecurityCouncilAzorius.sol";
+import {KontrolTest} from "test/kontrol/KontrolTest.sol"; 
+
+contract MockAzorius is IAzorius, KontrolTest {
+    struct Proposal {
+        address strategy;
+        uint32 timelockPeriod;
+        uint32 executionPeriod;
+        uint32 executionCounter;
+        bytes32[] txHashes;
+    }
+
+    mapping(uint32 => Proposal) internal proposals;
+
+    function setProposal(
+        uint32 proposalId,
+        bytes32[] memory txHashes,
+        address strategy,
+        uint32 timelockPeriod,
+        uint32 executionPeriod,
+        uint32 executionCounter
+    ) external {
+        Proposal storage proposal = proposals[proposalId];
+        proposal.strategy = strategy;
+        proposal.timelockPeriod = timelockPeriod;
+        proposal.executionPeriod = executionPeriod;
+        proposal.executionCounter = executionCounter;
+
+        delete proposal.txHashes;
+        uint256 txsLen = txHashes.length;
+        for (uint256 i = 0; i < txsLen;) {
+            proposal.txHashes.push(txHashes[i]);
+            unchecked {
+                ++i;
+            }
+        }
+    }
+
+    /// @dev Populates the txHashes array of a proposal with symbolic values for use
+    ///      in Kontrol symbolic execution proofs.
+    ///
+    ///      The Solidity storage layout for `proposals[proposalId]` is:
+    ///        proposalIdSlot + 0 : packed (strategy, timelockPeriod, executionPeriod, executionCounter)
+    ///        proposalIdSlot + 1 : txHashes.length  (dynamic array length)
+    ///        keccak256(proposalIdSlot + 1) + i : txHashes[i]  (array element slots)
+    ///
+    ///      The function builds the array by writing one fresh symbolic bytes32 per
+    ///      iteration directly into the element slots. Each iteration continues only
+    ///      if kevm.freshBool() returns true, so the symbolic length is unbounded but
+    ///      finite on every concrete execution path explored by KEVM. After the loop,
+    ///      the accumulated length is written to the length slot so that Solidity array
+    ///      reads return a consistent view of the symbolic data.
+    function setSymbolicProposal(uint32 proposalId) external {
+        Proposal storage proposal = proposals[proposalId];
+
+        uint256 proposalIdSlot;
+        assembly {
+            proposalIdSlot := proposal.slot
+        }
+
+        uint256 txsLen;
+        for (txsLen = 0; kevm.freshBool();) {
+            uint256 txHash = freshUInt256(string(abi.encodePacked("txHash", vm.toString(txsLen))));
+            uint256 txHashSlot = uint256(keccak256(abi.encode(proposalIdSlot + 1))) + txsLen;
+            _storeUInt256(address(this), txHashSlot, txHash);
+            unchecked {
+                ++txsLen;
+            }
+        }
+        // Store the length of the txHashes array
+        _storeUInt256(address(this), proposalIdSlot + 1, txsLen);
+    }
+
+
+    function getProposalTxHashes(uint32 proposalId)
+        external
+        view
+        override
+        returns (bytes32[] memory txHashes)
+    {
+        Proposal storage proposal = proposals[proposalId];
+        uint256 txsLen = proposal.txHashes.length;
+        txHashes = new bytes32[](txsLen);
+        for (uint256 i = 0; i < txsLen;) {
+            txHashes[i] = proposal.txHashes[i];
+            unchecked {
+                ++i;
+            }
+        }
+    }
+
+    function getProposal(uint32 proposalId)
+        external
+        view
+        override
+        returns (
+            address strategy,
+            bytes32[] memory txHashes,
+            uint32 timelockPeriod,
+            uint32 executionPeriod,
+            uint32 executionCounter
+        )
+    {
+        Proposal storage proposal = proposals[proposalId];
+        uint256 txsLen = proposal.txHashes.length;
+        txHashes = new bytes32[](txsLen);
+        for (uint256 i = 0; i < txsLen;) {
+            txHashes[i] = proposal.txHashes[i];
+            unchecked {
+                ++i;
+            }
+        }
+
+        return
+            (proposal.strategy, txHashes, proposal.timelockPeriod, proposal.executionPeriod, proposal.executionCounter);
+    }
+
+    function getTxHash(address to, uint256 value, bytes memory data, Enum.Operation operation)
+        external
+        pure
+        override
+        returns (bytes32)
+    {
+        return _hashTx(to, value, data, operation);
+    }
+
+    function hashTx(address to, uint256 value, bytes memory data, Enum.Operation operation)
+        external
+        pure
+        returns (bytes32)
+    {
+        return _hashTx(to, value, data, operation);
+    }
+
+    function _hashTx(address to, uint256 value, bytes memory data, Enum.Operation operation)
+        internal
+        pure
+        returns (bytes32)
+    {
+        return keccak256(abi.encode(to, value, data, operation));
+    }
+}