Upstream Certora Specifications

.gitignore

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

certora/README.md

@@ -0,0 +1,25 @@
+# Overview and Directory Structure
+This directory contains formal verification specifications for the Certora
+Prover and written in the Certora Verification Language (CVL). The subdirectory
+contents are as follows:
+ * confs -- contains configuration files to run the verification jobs
+ * harness -- contains test harnesses to help with verification, and mock 
+   versions of ERC20 contracts that are relevant to but not part of this solidity project
+ * mutation -- contains mutation tests that we used to gain further assurance 
+   about our specifications
+ * helpers -- contains a mock WithdrawalQueue and two simple contracts that inherit from Escrow
+   to alow us to model multiple distinct Escrow addresses
+*  specs -- contains our formal verification specifications
+
+# Run instructions
+Ensure you have installed the Certora Prover. These specifications were tested with 
+`certora-cli 7.17.2`. Launch each of the verification jobs from the root directory of the project with
+`certoraRun certora/confs/DualGovernance.conf`
+`certoraRun certora/confs/EmergencyProtectedTimelock.conf`
+`certoraRun certora/confs/Escrow.conf`
+`certoraRun certora/confs/Escrow_solvency.conf`
+`certoraRun certora/confs/Escrow_validState.conf`
+
+One of the rules in Escrow_solvency.conf `solvency_ETH` can have performance issues resulting in 
+a timeout. As a workaround, it can be run separately by running 
+`certoraRun certora/confs/Escrow_solvency.conf --rule solvency_ETH` in which case it should pass.

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;
+    }
+}