Upstream Certora Specifications

.gitignore

@@ -15,4 +15,7 @@ out/
 !/broadcast
 /broadcast/*/31337/
 /broadcast/**/dry-run/
+
+#Certora 
+.certora_internal/
 .vscode/

certora/confs/DualGovernance.conf

@@ -0,0 +1,50 @@
+{
+    "files": [
+        "contracts/libraries/DualGovernanceStateMachine.sol",
+        "contracts/Executor.sol",
+        "contracts/EmergencyProtectedTimelock.sol",
+        "contracts/ResealManager.sol",
+        "certora/helpers/EscrowA.sol",
+        "certora/helpers/EscrowB.sol",
+        "contracts/DualGovernanceConfigProvider.sol:ImmutableDualGovernanceConfigProvider",
+        "certora/harnesses/ERC20Like/DummyStETH.sol",
+        "certora/harnesses/ERC20Like/DummyWstETH.sol",
+        "certora/harnesses/DualGovernanceHarness.sol",
+    ],
+    "link": [
+        "DualGovernanceHarness:TIMELOCK=EmergencyProtectedTimelock",
+        "DualGovernanceHarness:_configProvider=ImmutableDualGovernanceConfigProvider",
+        "ResealManager:EMERGENCY_PROTECTED_TIMELOCK=EmergencyProtectedTimelock",
+        "DualGovernanceHarness:RESEAL_MANAGER=ResealManager",
+        "EscrowA:ST_ETH=DummyStETH",
+        "EscrowA:WST_ETH=DummyWstETH",
+        "EscrowA:DUAL_GOVERNANCE=DualGovernanceHarness",
+        "EscrowB:ST_ETH=DummyStETH",
+        "EscrowB:WST_ETH=DummyWstETH",
+        "EscrowB:DUAL_GOVERNANCE=DualGovernanceHarness"
+    ],
+    "struct_link": [
+        "DualGovernanceHarness:resealManager=ResealManager",
+        "EmergencyProtectedTimelock:executor=Executor",
+	],
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts"
+    ],
+    "parametric_contracts": [
+        "DualGovernanceHarness",
+        // "EmergencyProtectedTimelock",
+        // "ResealManager",
+        // "Escrow",
+        // // Not sure these are needed
+        // "DummyStETH",
+        // "DummyWstETH",
+    ],
+    "rule_sanity": "basic",
+    "process": "emv",
+    "solc": "solc8.26",
+    "optimistic_loop": true,
+    "loop_iter": "5",
+    "smt_timeout": "3600",
+    "build_cache": true,
+    "verify": "DualGovernanceHarness:certora/specs/DualGovernance.spec"
+}

certora/confs/EmergencyProtectedTimelock.conf

@@ -0,0 +1,24 @@
+{
+    "files": [
+        "contracts/EmergencyProtectedTimelock.sol",
+        "contracts/Executor.sol",
+        "contracts/libraries/ExecutableProposals.sol",
+        "contracts/libraries/EmergencyProtection.sol",
+        "contracts/types/Timestamp.sol:Timestamps",
+        "contracts/types/Duration.sol:Durations"
+    ],
+    "struct_link": [
+        "EmergencyProtectedTimelock:executor=Executor",
+    ],
+    "msg": "Emergency Protected Timelock",
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts"
+    ],
+    "process": "emv",
+    "solc": "solc8.26",
+    "optimistic_loop": true,
+    "solc_via_ir": false,
+    "verify": "EmergencyProtectedTimelock:certora/specs/Timelock.spec",
+    "rule_sanity": "basic",
+    "server": "production"
+}

certora/confs/Escrow.conf

@@ -0,0 +1,32 @@
+{
+    "files": [
+        "contracts/Escrow.sol",
+        "contracts/DualGovernance.sol",
+        "contracts/DualGovernanceConfigProvider.sol:ImmutableDualGovernanceConfigProvider",
+        "certora/helpers/DummyWithdrawalQueue.sol", 
+        "certora/harnesses/ERC20Like/DummyStETH.sol",
+        "certora/harnesses/ERC20Like/DummyWstETH.sol",
+    ],
+    "link": [
+        "Escrow:DUAL_GOVERNANCE=DualGovernance",
+        "Escrow:WITHDRAWAL_QUEUE=DummyWithdrawalQueue",
+        "Escrow:ST_ETH=DummyStETH",
+        "Escrow:WST_ETH=DummyWstETH",
+        "DummyWstETH:stETH=DummyStETH",
+        "DummyWithdrawalQueue:stETH=DummyStETH",
+        "DualGovernance:_configProvider=ImmutableDualGovernanceConfigProvider",
+    ],
+
+    "msg": "sanity",
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts"
+    ],
+
+    "solc": "solc8.26",
+    "optimistic_loop": true,
+    "optimistic_fallback": true,
+    "loop_iter": "3",
+    "build_cache" : true,
+    "rule_sanity" : "basic",
+    "verify": "Escrow:certora/specs/Escrow.spec"
+}

certora/confs/Escrow_solvency.conf

@@ -0,0 +1,32 @@
+{
+    "files": [
+        "contracts/Escrow.sol",
+        "contracts/DualGovernance.sol",
+        "contracts/DualGovernanceConfigProvider.sol:ImmutableDualGovernanceConfigProvider",
+        "certora/helpers/DummyWithdrawalQueue.sol", 
+        "certora/harnesses/ERC20Like/DummyStETH.sol",
+        "certora/harnesses/ERC20Like/DummyWstETH.sol",
+    ],
+    "link": [
+        "Escrow:DUAL_GOVERNANCE=DualGovernance",
+        "Escrow:WITHDRAWAL_QUEUE=DummyWithdrawalQueue",
+        "Escrow:ST_ETH=DummyStETH",
+        "Escrow:WST_ETH=DummyWstETH",
+        "DummyWstETH:stETH=DummyStETH",
+        "DummyWithdrawalQueue:stETH=DummyStETH",
+        "DualGovernance:_configProvider=ImmutableDualGovernanceConfigProvider",
+    ],
+
+    "msg": "sanity",
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts"
+    ],
+
+    "solc": "solc8.26",
+    "optimistic_loop": true,
+    "optimistic_fallback": true,
+    "loop_iter": "3",
+    "build_cache" : true,
+    "rule_sanity" : "basic",
+    "verify": "Escrow:certora/specs/Escrow_solvency.spec"
+}

certora/confs/Escrow_validState.conf

@@ -0,0 +1,32 @@
+{
+    "files": [
+        "contracts/Escrow.sol",
+        "contracts/DualGovernance.sol",
+        "contracts/DualGovernanceConfigProvider.sol:ImmutableDualGovernanceConfigProvider",
+        "certora/helpers/DummyWithdrawalQueue.sol", 
+        "certora/harnesses/ERC20Like/DummyStETH.sol",
+        "certora/harnesses/ERC20Like/DummyWstETH.sol",
+    ],
+    "link": [
+        "Escrow:DUAL_GOVERNANCE=DualGovernance",
+        "Escrow:WITHDRAWAL_QUEUE=DummyWithdrawalQueue",
+        "Escrow:ST_ETH=DummyStETH",
+        "Escrow:WST_ETH=DummyWstETH",
+        "DummyWstETH:stETH=DummyStETH",
+        "DummyWithdrawalQueue:stETH=DummyStETH",
+        "DualGovernance:_configProvider=ImmutableDualGovernanceConfigProvider",
+    ],
+
+    "msg": "Escrow_validState",
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts"
+    ],
+
+    "solc": "solc8.26",
+    "optimistic_loop": true,
+    "optimistic_fallback": true,
+    "loop_iter": "3",
+    "build_cache" : true,
+    "rule_sanity" : "basic",
+    "verify": "Escrow:certora/specs/Escrow_validState.spec"
+}

certora/harnesses/DualGovernanceHarness.sol

@@ -0,0 +1,145 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.26;
+
+import "../../contracts/libraries/Proposers.sol";
+import "../../contracts/DualGovernance.sol";
+import {Status as ProposalStatus} from "../../contracts/libraries/ExecutableProposals.sol";
+import {Proposal} from "../../contracts/libraries/EnumerableProposals.sol";
+// This is to make a type available for a NONDET summary
+import {IExternalExecutor} from "../../contracts/interfaces/IExternalExecutor.sol";
+import {State, DualGovernanceStateMachine} from "../../contracts/libraries/DualGovernanceStateMachine.sol";
+
+// The following are for methods about checking if max durations have passed
+import {DualGovernanceConfig} from "../../contracts/libraries/DualGovernanceConfig.sol";
+import {PercentD16} from "../../contracts/types/PercentD16.sol";
+import {Timestamp, Timestamps} from "../../contracts/types/Timestamp.sol";
+
+contract DualGovernanceHarness is DualGovernance {
+    using Proposers for Proposers.Context;
+    using Proposers for Proposers.Proposer;
+    using Tiebreaker for Tiebreaker.Context;
+    using DualGovernanceStateMachine for DualGovernanceStateMachine.Context;
+    using DualGovernanceConfig for DualGovernanceConfig.Context;
+
+    // Needed because DualGovernanceStateMachine.State is not
+    // referrable without redeclaring this here.
+    enum DGHarnessState {
+        Unset,
+        Normal,
+        VetoSignalling,
+        VetoSignallingDeactivation,
+        VetoCooldown,
+        RageQuit
+    }
+
+    constructor(
+        ExternalDependencies memory dependencies,
+        SanityCheckParams memory sanityCheckParams
+    ) DualGovernance(dependencies, sanityCheckParams) {}
+
+    // Return is uint32 which is the same as IndexOneBased
+    function getProposerIndexFromExecutor(address proposer) external view returns (uint32) {
+        return IndexOneBased.unwrap(_proposers.executors[proposer].proposerIndex);
+    }
+
+    function getProposalInfoHarnessed(uint256 proposalId)
+        external
+        view
+        returns (uint256 id, ProposalStatus status, address executor, Timestamp submittedAt, Timestamp scheduledAt)
+    {
+        return TIMELOCK.getProposalInfo(proposalId);
+    }
+
+    function getProposalHarnessed(uint256 proposalId) external view returns (ITimelock.Proposal memory proposal) {
+        return TIMELOCK.getProposal(proposalId);
+    }
+
+    function getVetoSignallingActivatedAt() external view returns (Timestamp) {
+        return _stateMachine.vetoSignallingActivatedAt;
+    }
+
+    function asDGHarnessState(State state) public returns (DGHarnessState) {
+        uint256 state_underlying = uint256(state);
+        return DGHarnessState(state_underlying);
+    }
+
+    function getState() external returns (DGHarnessState) {
+        return asDGHarnessState(_stateMachine.state);
+    }
+
+    function getFirstSeal() external view returns (uint256) {
+        return PercentD16.unwrap(_configProvider.getDualGovernanceConfig().firstSealRageQuitSupport);
+    }
+
+    function getSecondSeal() external view returns (uint256) {
+        return PercentD16.unwrap(_configProvider.getDualGovernanceConfig().secondSealRageQuitSupport);
+    }
+
+    function getFirstSealRageQuitSupportCrossed() external view returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isFirstSealRageQuitSupportCrossed(
+            _stateMachine.signallingEscrow.getRageQuitSupport()
+        );
+    }
+
+    function getSecondSealRageQuitSupportCrossed() external view returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isSecondSealRageQuitSupportCrossed(
+            _stateMachine.signallingEscrow.getRageQuitSupport()
+        );
+    }
+
+    function getRageQuitSupportHarnessed() external view returns (PercentD16) {
+        return _stateMachine.signallingEscrow.getRageQuitSupport();
+    }
+
+    function isDynamicTimelockPassed(uint256 rageQuitSupport) public returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isDynamicTimelockDurationPassed(
+            _stateMachine.vetoSignallingActivatedAt, PercentD16.wrap(rageQuitSupport)
+        );
+    }
+
+    function isVetoSignallingReactivationPassed() public returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isVetoSignallingReactivationDurationPassed(
+            Timestamps.max(_stateMachine.vetoSignallingReactivationTime, _stateMachine.vetoSignallingActivatedAt)
+        );
+    }
+
+    function isVetoSignallingDeactivationPassed() public returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isVetoSignallingDeactivationMaxDurationPassed(
+            _stateMachine.enteredAt
+        );
+    }
+
+    function isVetoSignallingDeactivationMaxDurationPassed() public returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isVetoSignallingDeactivationMaxDurationPassed(
+            _stateMachine.enteredAt
+        );
+    }
+
+    function isVetoCooldownDurationPassed() public returns (bool) {
+        return _configProvider.getDualGovernanceConfig().isVetoCooldownDurationPassed(_stateMachine.enteredAt);
+    }
+
+    function isUnset(DGHarnessState state) public returns (bool) {
+        return state == DGHarnessState.Unset;
+    }
+
+    function isNormal(DGHarnessState state) public returns (bool) {
+        return state == DGHarnessState.Normal;
+    }
+
+    function isVetoSignalling(DGHarnessState state) public returns (bool) {
+        return state == DGHarnessState.VetoSignalling;
+    }
+
+    function isVetoSignallingDeactivation(DGHarnessState state) public returns (bool) {
+        return state == DGHarnessState.VetoSignallingDeactivation;
+    }
+
+    function isVetoCooldown(DGHarnessState state) public returns (bool) {
+        return state == DGHarnessState.VetoCooldown;
+    }
+
+    function isRageQuit(DGHarnessState state) public returns (bool) {
+        return state == DGHarnessState.RageQuit;
+    }
+}

certora/harnesses/ERC20Like/DummyERC20A.sol

@@ -0,0 +1,51 @@
+// Represents a symbolic/dummy ERC20 token
+
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+contract DummyERC20A {
+    uint256 t;
+    mapping(address => uint256) b;
+    mapping(address => mapping(address => uint256)) a;
+
+    string public name;
+    string public symbol;
+    uint256 public decimals;
+
+    function myAddress() external view returns (address) {
+        return address(this);
+    }
+
+    function totalSupply() external view returns (uint256) {
+        return t;
+    }
+
+    function balanceOf(address account) external view returns (uint256) {
+        return b[account];
+    }
+
+    function transfer(address recipient, uint256 amount) external returns (bool) {
+        b[msg.sender] -= amount;
+        b[recipient] += amount;
+
+        return true;
+    }
+
+    function allowance(address owner, address spender) external view returns (uint256) {
+        return a[owner][spender];
+    }
+
+    function approve(address spender, uint256 amount) external returns (bool) {
+        a[msg.sender][spender] = amount;
+
+        return true;
+    }
+
+    function transferFrom(address sender, address recipient, uint256 amount) external returns (bool) {
+        b[sender] -= amount;
+        b[recipient] += amount;
+        a[sender][msg.sender] -= amount;
+
+        return true;
+    }
+}