sanity for TimelockController and Votes

certora/munged/security/Pausable.sol

@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (security/Pausable.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/Context.sol";
+
+/**
+ * @dev Contract module which allows children to implement an emergency stop
+ * mechanism that can be triggered by an authorized account.
+ *
+ * This module is used through inheritance. It will make available the
+ * modifiers `whenNotPaused` and `whenPaused`, which can be applied to
+ * the functions of your contract. Note that they will not be pausable by
+ * simply including this module, only once the modifiers are put in place.
+ */
+abstract contract Pausable is Context {
+    /**
+     * @dev Emitted when the pause is triggered by `account`.
+     */
+    event Paused(address account);
+
+    /**
+     * @dev Emitted when the pause is lifted by `account`.
+     */
+    event Unpaused(address account);
+
+    bool private _paused;
+
+    /**
+     * @dev Initializes the contract in unpaused state.
+     */
+    constructor() {
+        _paused = false;
+    }
+
+    /**
+     * @dev Returns true if the contract is paused, and false otherwise.
+     */
+    function paused() public view virtual returns (bool) {
+        return _paused;
+    }
+
+    /**
+     * @dev Modifier to make a function callable only when the contract is not paused.
+     *
+     * Requirements:
+     *
+     * - The contract must not be paused.
+     */
+    modifier whenNotPaused() {
+        require(!paused(), "Pausable: paused");
+        _;
+    }
+
+    /**
+     * @dev Modifier to make a function callable only when the contract is paused.
+     *
+     * Requirements:
+     *
+     * - The contract must be paused.
+     */
+    modifier whenPaused() {
+        require(paused(), "Pausable: not paused");
+        _;
+    }
+
+    /**
+     * @dev Triggers stopped state.
+     *
+     * Requirements:
+     *
+     * - The contract must not be paused.
+     */
+    function _pause() internal virtual whenNotPaused {
+        _paused = true;
+        emit Paused(_msgSender());
+    }
+
+    /**
+     * @dev Returns to normal state.
+     *
+     * Requirements:
+     *
+     * - The contract must be paused.
+     */
+    function _unpause() internal virtual whenPaused {
+        _paused = false;
+        emit Unpaused(_msgSender());
+    }
+}

certora/munged/security/PullPayment.sol

@@ -0,0 +1,70 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (security/PullPayment.sol)
+
+pragma solidity ^0.8.0;
+
+import "../utils/escrow/Escrow.sol";
+
+/**
+ * @dev Simple implementation of a
+ * https://consensys.github.io/smart-contract-best-practices/recommendations/#favor-pull-over-push-for-external-calls[pull-payment]
+ * strategy, where the paying contract doesn't interact directly with the
+ * receiver account, which must withdraw its payments itself.
+ *
+ * Pull-payments are often considered the best practice when it comes to sending
+ * Ether, security-wise. It prevents recipients from blocking execution, and
+ * eliminates reentrancy concerns.
+ *
+ * TIP: If you would like to learn more about reentrancy and alternative ways
+ * to protect against it, check out our blog post
+ * https://blog.openzeppelin.com/reentrancy-after-istanbul/[Reentrancy After Istanbul].
+ *
+ * To use, derive from the `PullPayment` contract, and use {_asyncTransfer}
+ * instead of Solidity's `transfer` function. Payees can query their due
+ * payments with {payments}, and retrieve them with {withdrawPayments}.
+ */
+abstract contract PullPayment {
+    Escrow private immutable _escrow;
+
+    constructor() {
+        _escrow = new Escrow();
+    }
+
+    /**
+     * @dev Withdraw accumulated payments, forwarding all gas to the recipient.
+     *
+     * Note that _any_ account can call this function, not just the `payee`.
+     * This means that contracts unaware of the `PullPayment` protocol can still
+     * receive funds this way, by having a separate account call
+     * {withdrawPayments}.
+     *
+     * WARNING: Forwarding all gas opens the door to reentrancy vulnerabilities.
+     * Make sure you trust the recipient, or are either following the
+     * checks-effects-interactions pattern or using {ReentrancyGuard}.
+     *
+     * @param payee Whose payments will be withdrawn.
+     */
+    function withdrawPayments(address payable payee) public virtual {
+        _escrow.withdraw(payee);
+    }
+
+    /**
+     * @dev Returns the payments owed to an address.
+     * @param dest The creditor's address.
+     */
+    function payments(address dest) public view returns (uint256) {
+        return _escrow.depositsOf(dest);
+    }
+
+    /**
+     * @dev Called by the payer to store the sent amount as credit to be pulled.
+     * Funds sent in this way are stored in an intermediate {Escrow} contract, so
+     * there is no danger of them being spent before withdrawal.
+     *
+     * @param dest The destination address of the funds.
+     * @param amount The amount to transfer.
+     */
+    function _asyncTransfer(address dest, uint256 amount) internal virtual {
+        _escrow.deposit{value: amount}(dest);
+    }
+}

certora/munged/security/README.adoc

@@ -0,0 +1,20 @@
+= Security
+
+[.readme-notice]
+NOTE: This document is better viewed at https://docs.openzeppelin.com/contracts/api/security
+
+These contracts aim to cover common security practices.
+
+* {PullPayment}: A pattern that can be used to avoid reentrancy attacks.
+* {ReentrancyGuard}: A modifier that can prevent reentrancy during certain functions.
+* {Pausable}: A common emergency response mechanism that can pause functionality while a remediation is pending.
+
+TIP: For an overview on reentrancy and the possible mechanisms to prevent it, read our article https://blog.openzeppelin.com/reentrancy-after-istanbul/[Reentrancy After Istanbul].
+
+== Contracts
+
+{{PullPayment}}
+
+{{ReentrancyGuard}}
+
+{{Pausable}}

certora/munged/security/ReentrancyGuard.sol

@@ -0,0 +1,63 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (security/ReentrancyGuard.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Contract module that helps prevent reentrant calls to a function.
+ *
+ * Inheriting from `ReentrancyGuard` will make the {nonReentrant} modifier
+ * available, which can be applied to functions to make sure there are no nested
+ * (reentrant) calls to them.
+ *
+ * Note that because there is a single `nonReentrant` guard, functions marked as
+ * `nonReentrant` may not call one another. This can be worked around by making
+ * those functions `private`, and then adding `external` `nonReentrant` entry
+ * points to them.
+ *
+ * TIP: If you would like to learn more about reentrancy and alternative ways
+ * to protect against it, check out our blog post
+ * https://blog.openzeppelin.com/reentrancy-after-istanbul/[Reentrancy After Istanbul].
+ */
+abstract contract ReentrancyGuard {
+    // Booleans are more expensive than uint256 or any type that takes up a full
+    // word because each write operation emits an extra SLOAD to first read the
+    // slot's contents, replace the bits taken up by the boolean, and then write
+    // back. This is the compiler's defense against contract upgrades and
+    // pointer aliasing, and it cannot be disabled.
+
+    // The values being non-zero value makes deployment a bit more expensive,
+    // but in exchange the refund on every call to nonReentrant will be lower in
+    // amount. Since refunds are capped to a percentage of the total
+    // transaction's gas, it is best to keep them low in cases like this one, to
+    // increase the likelihood of the full refund coming into effect.
+    uint256 private constant _NOT_ENTERED = 1;
+    uint256 private constant _ENTERED = 2;
+
+    uint256 private _status;
+
+    constructor() {
+        _status = _NOT_ENTERED;
+    }
+
+    /**
+     * @dev Prevents a contract from calling itself, directly or indirectly.
+     * Calling a `nonReentrant` function from another `nonReentrant`
+     * function is not supported. It is possible to prevent this from happening
+     * by making the `nonReentrant` function external, and making it call a
+     * `private` function that does the actual work.
+     */
+    modifier nonReentrant() {
+        // On the first call to nonReentrant, _notEntered will be true
+        require(_status != _ENTERED, "ReentrancyGuard: reentrant call");
+
+        // Any calls to nonReentrant after this point will fail
+        _status = _ENTERED;
+
+        _;
+
+        // By storing the original value once again, a refund is triggered (see
+        // https://eips.ethereum.org/EIPS/eip-2200)
+        _status = _NOT_ENTERED;
+    }
+}