diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 16c5eda..2021861 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -48,9 +48,11 @@ jobs: - "termRepoServicer-lockFulfill.conf" - "termRepoServicer-lockFulfillReverts.conf" - "termRepoServicer-mintCollapse.conf" + - "termRepoServicer-mintIntegrity.conf" - "termRepoServicer-mintCollapseReverts.conf" - "termRepoServicer-repaymentsRedemptions.conf" - "termRepoServicer-repaymentsRedemptionsReverts.conf" + - "termRepoServicer-rolloverReverts.conf" - "termRepoServicer-stateVariables.conf" - "termRepoServicer.conf" - "termRepoToken.conf" diff --git a/certora/confs/termRepoServicer-mintIntegrity.conf b/certora/confs/termRepoServicer-mintIntegrity.conf new file mode 100644 index 0000000..c5874f9 --- /dev/null +++ b/certora/confs/termRepoServicer-mintIntegrity.conf @@ -0,0 +1,41 @@ +{ + "files": [ + "certora/harness/TermRepoServicerHarness.sol", + "contracts/TermAuctionBidLocker.sol", + "contracts/TermController.sol", + "contracts/TermRepoLocker.sol", + "contracts/TermRepoToken.sol", + "contracts/TermRepoRolloverManager.sol", + "certora/harness/TermRepoCollateralManagerHarness.sol", + "certora/helpers/DummyERC20A.sol" + ], + "link": [ + "TermRepoServicerHarness:termRepoToken=TermRepoToken", + "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", + "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", + "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" + ], + "prover_args": [ + "-smt_initialSplitDepth 5", + "-depth 15", + "-mediumTimeout 2", + "-splitParallel true", + "-splitParallelTimelimit 7200", + "-splitParallelInitialDepth 5" + ], + "solc_optimize": "50", + "loop_iter": "2", + "optimistic_loop": true, + "ignore_solidity_warnings": true, + "smt_timeout": "7200", + "parametric_contracts": [ + "TermRepoServicerHarness" + ], + "rule_sanity": "basic", + "packages": [ + "@chainlink=node_modules/@chainlink", + "@openzeppelin=node_modules/@openzeppelin" + ], + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesMintIntegrity.spec" +} \ No newline at end of file diff --git a/certora/confs/termRepoServicer-rolloverReverts.conf b/certora/confs/termRepoServicer-rolloverReverts.conf new file mode 100644 index 0000000..bfa3666 --- /dev/null +++ b/certora/confs/termRepoServicer-rolloverReverts.conf @@ -0,0 +1,42 @@ +{ + "files": [ + "certora/harness/TermRepoServicerHarness.sol", + "contracts/TermAuctionBidLocker.sol", + "contracts/TermController.sol", + "contracts/TermRepoLocker.sol", + "contracts/TermRepoToken.sol", + "contracts/TermRepoRolloverManager.sol", + "certora/harness/TermRepoCollateralManagerHarness.sol", + "certora/helpers/DummyERC20A.sol" + ], + "link": [ + "TermRepoServicerHarness:termRepoToken=TermRepoToken", + "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", + "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termController=TermController", + "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", + "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" + ], + "prover_args": [ + "-smt_initialSplitDepth 10", + "-depth 20", + "-mediumTimeout 2", + "-splitParallel true", + "-splitParallelTimelimit 7200", + "-splitParallelInitialDepth 10" + ], + "solc_optimize": "50", + "loop_iter": "2", + "optimistic_loop": true, + "ignore_solidity_warnings": true, + "smt_timeout": "7200", + "parametric_contracts": [ + "TermRepoServicerHarness" + ], + "rule_sanity": "basic", + "packages": [ + "@chainlink=node_modules/@chainlink", + "@openzeppelin=node_modules/@openzeppelin" + ], + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRolloverReverts.spec" +} \ No newline at end of file diff --git a/certora/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index f6d568c..212c077 100644 --- a/certora/specs/termRepoServicer/rules.spec +++ b/certora/specs/termRepoServicer/rules.spec @@ -80,7 +80,5 @@ use rule onlyRoleCanCallStorage; use rule openExposureOnRolloverNewIntegrity; use rule openExposureOnRolloverNewDoesNotAffectThirdParty; -use rule openExposureOnRolloverNewRevertConditions; use rule closeExposureOnRolloverExistingIntegrity; use rule closeExposureOnRolloverExistingDoesNotAffectThirdParty; -use rule closeExposureOnRolloverExistingRevertConditions; diff --git a/certora/specs/termRepoServicer/rulesMintCollapse.spec b/certora/specs/termRepoServicer/rulesMintCollapse.spec index abe08c8..8e766f7 100644 --- a/certora/specs/termRepoServicer/rulesMintCollapse.spec +++ b/certora/specs/termRepoServicer/rulesMintCollapse.spec @@ -60,5 +60,4 @@ use rule burnCollapseExposureIntegrity; use rule burnCollapseExposureDoesNotAffectThirdParty; use rule mintOpenExposureMonotonicBehavior; -use rule mintOpenExposureIntegrity; use rule mintOpenExposureDoesNotAffectThirdParty; diff --git a/certora/specs/termRepoServicer/rulesMintIntegrity.spec b/certora/specs/termRepoServicer/rulesMintIntegrity.spec new file mode 100644 index 0000000..11d4d8e --- /dev/null +++ b/certora/specs/termRepoServicer/rulesMintIntegrity.spec @@ -0,0 +1,58 @@ +import "../methods/erc20Methods.spec"; +import "../methods/emitMethods.spec"; +import "./collapses.spec"; +import "./minting.spec"; +import "./stateVariables.spec"; + + +methods { + function upgradeToAndCall(address,bytes) external => NONDET DELETE; + function _.usdValueOfTokens(address,uint256) external => NONDET DELETE; + function _.div_(uint256 x, uint256 y) internal => divCVL(x,y) expect uint256; + function _.mul_(uint256 x, uint256 y) internal => mulCVL(x,y) expect uint256; + + // // TermRepoToken + // function _.totalRedemptionValue() external => DISPATCHER(true); + // function _.redemptionValue() external => DISPATCHER(true); + // function _.burnAndReturnValue(address,uint256) external => DISPATCHER(true); + // function _.mintRedemptionValue(address,uint256) external => DISPATCHER(true); + // function _.mintTokens(address,uint256) external => DISPATCHER(true); + // function _.decrementMintExposureCap(uint256) external => DISPATCHER(true); + // function _.burn(address,uint256) external => DISPATCHER(true); + + // TermRepoLocker + // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); + // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); + + // TermController + function _.getTreasuryAddress() external => ALWAYS(100); + function _.getProtocolReserveAddress() external => ALWAYS(100); + + + // // TermRepoRolloverManager + // function _.getRolloverInstructions(address) external => DISPATCHER(true); + // function _.fulfillRollover(address) external => DISPATCHER(true); + + // // TermRepoCollateralManager + // function _.numOfAcceptedCollateralTokens() external => DISPATCHER(true); + // function _.collateralTokens() external => DISPATCHER(true); + // function _.collateralTokens(uint256) external => DISPATCHER(true); + // function _.calculateMintableExposure(address,uint256) external => DISPATCHER(true); + // function _.encumberedCollateralRemaining() external => DISPATCHER(true); + // function _.unlockCollateralOnRepurchase(address) external => DISPATCHER(true); + // function _.journalBidCollateralToCollateralManager(address,address[],uint256[]) external => DISPATCHER(true); + // function _.mintOpenExposureLockCollateral(address,address,uint256) external => DISPATCHER(true); +} + +function mulCVL(uint256 x, uint256 y) returns uint256 { + return require_uint256(x * y); +} + +function divCVL(uint256 x, uint256 y) returns uint256 { + require y != 0; + return require_uint256(x / y); +} + + +use invariant totalOutstandingRepurchaseExposureIsSumOfRepurchases; +use rule mintOpenExposureIntegrity; diff --git a/certora/specs/termRepoServicer/rulesRolloverReverts.spec b/certora/specs/termRepoServicer/rulesRolloverReverts.spec new file mode 100644 index 0000000..5aea4e5 --- /dev/null +++ b/certora/specs/termRepoServicer/rulesRolloverReverts.spec @@ -0,0 +1,60 @@ +import "../methods/erc20Methods.spec"; +import "../methods/emitMethods.spec"; +import "../common/isTermContractPaired.spec"; +import "../complexity.spec"; +import "./accessRoles.spec"; +import "./rolloverExposure.spec"; +import "./stateVariables.spec"; + +methods { + function upgradeToAndCall(address,bytes) external => NONDET DELETE; + function _.usdValueOfTokens(address,uint256) external => NONDET DELETE; + function _.div_(uint256 x, uint256 y) internal => divCVL(x,y) expect uint256; + function _.mul_(uint256 x, uint256 y) internal => mulCVL(x,y) expect uint256; + + // // TermRepoToken + // function _.totalRedemptionValue() external => DISPATCHER(true); + // function _.redemptionValue() external => DISPATCHER(true); + // function _.burnAndReturnValue(address,uint256) external => DISPATCHER(true); + // function _.mintRedemptionValue(address,uint256) external => DISPATCHER(true); + // function _.mintTokens(address,uint256) external => DISPATCHER(true); + // function _.decrementMintExposureCap(uint256) external => DISPATCHER(true); + // function _.burn(address,uint256) external => DISPATCHER(true); + + // TermRepoLocker + // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); + // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); + + // TermController + function TermController.getTreasuryAddress() external returns (address) => ALWAYS(100); + function TermController.getProtocolReserveAddress() external returns (address) => ALWAYS(100); + + + // // TermRepoRolloverManager + // function _.getRolloverInstructions(address) external => DISPATCHER(true); + // function _.fulfillRollover(address) external => DISPATCHER(true); + + // // TermRepoCollateralManager + // function _.numOfAcceptedCollateralTokens() external => DISPATCHER(true); + // function _.collateralTokens() external => DISPATCHER(true); + // function _.collateralTokens(uint256) external => DISPATCHER(true); + // function _.calculateMintableExposure(address,uint256) external => DISPATCHER(true); + // function _.encumberedCollateralRemaining() external => DISPATCHER(true); + // function _.unlockCollateralOnRepurchase(address) external => DISPATCHER(true); + // function _.journalBidCollateralToCollateralManager(address,address[],uint256[]) external => DISPATCHER(true); + // function _.mintOpenExposureLockCollateral(address,address,uint256) external => DISPATCHER(true); +} + +function mulCVL(uint256 x, uint256 y) returns uint256 { + return require_uint256(x * y); +} + +function divCVL(uint256 x, uint256 y) returns uint256 { + require y != 0; + return require_uint256(x / y); +} + +use invariant totalOutstandingRepurchaseExposureIsSumOfRepurchases; + +use rule openExposureOnRolloverNewRevertConditions; +use rule closeExposureOnRolloverExistingRevertConditions; diff --git a/contracts/TermRepoServicer.sol b/contracts/TermRepoServicer.sol index 673a5d9..5a02065 100644 --- a/contracts/TermRepoServicer.sol +++ b/contracts/TermRepoServicer.sol @@ -46,7 +46,6 @@ contract TermRepoServicer is bytes32 public constant COLLATERAL_MANAGER = keccak256("COLLATERAL_MANAGER"); bytes32 public constant DEVOPS_ROLE = keccak256("DEVOPS_ROLE"); - bytes32 public constant SPECIALIST_ROLE = keccak256("SPECIALIST_ROLE"); bytes32 public constant ROLLOVER_MANAGER = keccak256("ROLLOVER_MANAGER"); bytes32 public constant ROLLOVER_TARGET_AUCTIONEER_ROLE = keccak256("ROLLOVER_TARGET_AUCTIONEER_ROLE");