diff --git a/certora/confs/HealthyAfterRCFLiquidation.conf b/certora/confs/HealthyAfterRCFLiquidation.conf new file mode 100644 index 000000000..e8820e388 --- /dev/null +++ b/certora/confs/HealthyAfterRCFLiquidation.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "certora/helpers/MidnightWrapper.sol" + ], + "parametric_contracts": [ + "MidnightWrapper" + ], + "verify": "MidnightWrapper:certora/specs/HealthyAfterRCFLiquidation.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 2048, + "smt_timeout": 7200, + "prover_args": [ + "-timeout 7200", + "-split false", + "-destructiveOptimizations twostage -backendStrategy singleRace -smt_useLIA false -smt_useNIA true -depth 0 -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "msg": "RCF: Unhealthy After Liquidation" +} diff --git a/certora/confs/LastIdPatternRepro.conf b/certora/confs/LastIdPatternRepro.conf new file mode 100644 index 000000000..72a802871 --- /dev/null +++ b/certora/confs/LastIdPatternRepro.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "src/Midnight.sol" + ], + "parametric_contracts": [ + "Midnight" + ], + "verify": "Midnight:certora/specs/LastIdPatternRepro.spec", + "solc": "solc-0.8.34", + "solc_evm_version": "osaka", + "solc_via_ir": true, + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 2048, + "prover_args": [ + "-depth 5", + "-mediumTimeout 20", + "-timeout 3600", + "-destructiveOptimizations twostage", + "-splitParallel true", + "-dontStopAtFirstSplitTimeout true" + ], + "msg": "Storage read divergence under ghost-bound id (lastId pattern)" +} diff --git a/certora/specs/HealthyAfterRCFLiquidation.spec b/certora/specs/HealthyAfterRCFLiquidation.spec new file mode 100644 index 000000000..cf60eaa12 --- /dev/null +++ b/certora/specs/HealthyAfterRCFLiquidation.spec @@ -0,0 +1,253 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +import "BitmapSummaries.spec"; + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function collateral(bytes32 id, address user, uint256) external returns (uint128) envfree; + function debtOf(bytes32, address) external returns (uint256) envfree; + function isHealthyNoBitmap(Midnight.Market, bytes32, address) external returns (bool) envfree; + + /* Assumption: price does not change during rules. */ + function _.price() external => summaryPrice(calledContract) expect(uint256); + function IdLib.toId(Midnight.Market memory market, uint256 chainId, address midnight) internal returns (bytes32) => summaryToId(market, chainId, midnight); + + /* Summarize mulDivDown and mulDivUp with tight floor/ceil axioms so the ghosts + * behave like real integer division. The axioms are proved in MulDiv.spec. + */ + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivUp(x, y, d); + + function _.transferFrom(address from, address to, uint256 amount) external => NONDET; + function _.transfer(address to, uint256 amount) external => NONDET; + function _.onLiquidate(bytes32, Midnight.Market, uint256, uint256, uint256, address, bytes) external => NONDET; +} + +/// SUMMARY /// + +definition WAD() returns uint256 = 10 ^ 18; + +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +persistent ghost summaryPrice(address) returns uint256; + +persistent ghost summaryMulDivDownM(mathint, mathint, mathint) returns mathint { + /* proved in mulDivZero in MulDiv.spec */ + axiom forall uint256 b. forall uint256 d. d > 0 => summaryMulDivDownM(0, b, d) == 0; +} + +persistent ghost summaryMulDivUpM(mathint, mathint, mathint) returns mathint; + +/* Axioms exposed as definitions so each rule opts in via `require forall ... axiomX(...)`. + * Keeps quantifier instantiation scoped to the rules that need each axiom. + * Proved in MulDiv.spec. + */ + +/* floor lower bound: mulDivDown(a, b, d) * d <= a * b */ +definition axiomDownLowerBound(mathint a, mathint b, mathint d) returns bool = + 0 <= a && 0 <= b && 0 < d => summaryMulDivDownM(a, b, d) * d <= a * b; + +/* floor strictness: (mulDivDown(a, b, d) + 1) * d > a * b — pins the ghost to the + * actual floor of a*b/d. Without this the SMT can under-approximate and pick 0. */ +definition axiomDownStrictness(mathint a, mathint b, mathint d) returns bool = + 0 <= a && 0 <= b && 0 < d => (summaryMulDivDownM(a, b, d) + 1) * d > a * b; + +/* ceil upper bound: mulDivUp(a, b, d) * d >= a * b */ +definition axiomUpUpperBound(mathint a, mathint b, mathint d) returns bool = + 0 <= a && 0 <= b && 0 < d => summaryMulDivUpM(a, b, d) * d >= a * b; + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(summaryMulDivDownM(a, b, d)); +} + +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(summaryMulDivUpM(a, b, d)); +} + +// global variable to track which market and borrower we're testing. +persistent ghost address globalMarketLoanToken; + +persistent ghost uint256 globalMarketCollateralLength; + +persistent ghost mapping(uint256 => address) globalMarketCollateralOracle; + +persistent ghost mapping(uint256 => address) globalMarketCollateralToken; + +persistent ghost mapping(uint256 => uint256) globalMarketCollateralLLTV; + +persistent ghost mapping(uint256 => uint256) globalMarketCollateralMaxLif; + +persistent ghost uint256 globalMarketMaturity; + +persistent ghost uint256 globalMarketRcfThreshold; + +persistent ghost address globalMarketEnterGate; + +persistent ghost address globalMarketLiquidatorGate; + +persistent ghost bytes32 globalId; + +persistent ghost address globalBorrower; + +// helper function to check if one of the collateralParams of a market matches the global variables. +// It checks for the length and also returns true if the index is out of bounds. This allows us to require this for every index. +definition collateralMatches(Midnight.Market market, uint256 index) returns bool = (index < globalMarketCollateralLength => market.collateralParams[index].oracle == globalMarketCollateralOracle[index] && market.collateralParams[index].token == globalMarketCollateralToken[index] && market.collateralParams[index].lltv == globalMarketCollateralLLTV[index] && market.collateralParams[index].maxLif == globalMarketCollateralMaxLif[index]); + +function equalsGlobalMarket(Midnight.Market market) returns (bool) { + return market.loanToken == globalMarketLoanToken && market.collateralParams.length == globalMarketCollateralLength && collateralMatches(market, 0) && collateralMatches(market, 1) && collateralMatches(market, 2) && market.maturity == globalMarketMaturity && market.rcfThreshold == globalMarketRcfThreshold && market.enterGate == globalMarketEnterGate && market.liquidatorGate == globalMarketLiquidatorGate; +} + +function getGlobalMarket() returns (Midnight.Market) { + Midnight.Market market; + require equalsGlobalMarket(market), "get global market"; + return market; +} + +function summaryToId(Midnight.Market market, uint256 chainId, address midnight) returns (bytes32) { + bytes32 id; + if (equalsGlobalMarket(market) && midnight == currentContract) { + require id == globalId, "toId() is deterministic"; + } else { + require id != globalId, "toId() is injective"; + } + return id; +} + +//// RULES ////// + +// Concrete-market version of healthyAfterMaxRcfLiquidationSingleCollateral: +// pins every globalMarket* ghost to a specific value so the obligation is fully +// determined. Useful as a sanity check and as a faster-to-verify variant. +rule concreteHealthyAfterMaxRcfLiquidationSingleCollateral(env e, uint256 seizedAssets, uint256 repaidUnits, address receiver, address callbackAddr, bytes data) { + require forall mathint a. forall mathint b. forall mathint d. axiomDownLowerBound(a, b, d), "floor lower bound on mulDivDown"; + require forall mathint a. forall mathint b. forall mathint d. axiomDownStrictness(a, b, d), "floor strictness on mulDivDown"; + require forall mathint a. forall mathint b. forall mathint d. axiomUpUpperBound(a, b, d), "ceil upper bound on mulDivUp"; + + // Pin the market to concrete values via the globalMarket* ghosts; equalsGlobalMarket + // then matches a Market with these fields, and summaryToId returns globalId. + require globalMarketLoanToken == 0x0000000000000000000000000000000000001001; + require globalMarketCollateralLength == 1; + require globalMarketCollateralOracle[0] == 0x0000000000000000000000000000000000001003; + require globalMarketCollateralToken[0] == 0x0000000000000000000000000000000000001002; + require globalMarketCollateralLLTV[0] == 770000000000000000; // 0.77 * WAD + require globalMarketCollateralMaxLif[0] == 1061007957559681697; // ~1.061 * WAD + require globalMarketMaturity == 2000000000; + require globalMarketRcfThreshold == 0; + require globalMarketEnterGate == 0; + require globalMarketLiquidatorGate == 0; + + Midnight.Market globalMarket = getGlobalMarket(); + + uint256 lltv = globalMarketCollateralLLTV[0]; + uint256 maxLif = globalMarketCollateralMaxLif[0]; + uint256 lifTimesLltv = summaryMulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "maxLif * lltv < 1 so the RCF denominator (1 - maxLif * lltv) is positive"; + + uint256 price = summaryPrice(globalMarketCollateralOracle[0]); + uint256 collatBefore = collateral(globalId, globalBorrower, 0); + uint256 debtBefore = debtOf(globalId, globalBorrower); + + require collatBefore > 0, "borrower has collateral to seize"; + require e.block.timestamp < globalMarketMaturity, "ensure RCF condition is activated"; + + uint256 maxDebt = summaryMulDivDown(summaryMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + require debtBefore > maxDebt, "position is unhealthy before liquidation"; + + uint256 rcfCap = summaryMulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); + + uint256 actualSeized; + uint256 actualRepaid; + + actualSeized, actualRepaid = liquidate(e, globalMarket, 0, seizedAssets, repaidUnits, globalBorrower, receiver, callbackAddr, data); + + require actualRepaid == rcfCap, "max allowed to be repaid by RCF condition is repaid"; + assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower); +} + +// Single-collateral variant of healthyAfterMaxRcfLiquidation: pins +// globalMarketCollateralLength == 1 so the only valid collateralIndex is 0. +rule healthyAfterMaxRcfLiquidationSingleCollateral(env e, uint256 seizedAssets, uint256 repaidUnits, address receiver, address callbackAddr, bytes data) { + require forall mathint a. forall mathint b. forall mathint d. axiomDownLowerBound(a, b, d), "floor lower bound on mulDivDown"; + require forall mathint a. forall mathint b. forall mathint d. axiomDownStrictness(a, b, d), "floor strictness on mulDivDown"; + require forall mathint a. forall mathint b. forall mathint d. axiomUpUpperBound(a, b, d), "ceil upper bound on mulDivUp"; + + require globalMarketCollateralLength == 1, "single collateral asset"; + + Midnight.Market globalMarket = getGlobalMarket(); + + uint256 lltv = globalMarketCollateralLLTV[0]; + uint256 maxLif = globalMarketCollateralMaxLif[0]; + require maxLif >= WAD(), "maxLif is at least 1"; + uint256 lifTimesLltv = summaryMulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "maxLif * lltv < 1 so the RCF denominator (1 - maxLif * lltv) is positive"; + + uint256 price = summaryPrice(globalMarketCollateralOracle[0]); + uint256 collatBefore = collateral(globalId, globalBorrower, 0); + uint256 debtBefore = debtOf(globalId, globalBorrower); + + require collatBefore > 0, "borrower has collateral to seize"; + require e.block.timestamp < globalMarketMaturity, "ensure RCF condition is activated"; + + uint256 maxDebt = summaryMulDivDown(summaryMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + require debtBefore > maxDebt, "position is unhealthy before liquidation"; + + uint256 rcfCap = summaryMulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); + + uint256 actualSeized; + uint256 actualRepaid; + + actualSeized, actualRepaid = liquidate(e, globalMarket, 0, seizedAssets, repaidUnits, globalBorrower, receiver, callbackAddr, data); + + require actualRepaid == rcfCap, "max allowed to be repaid by RCF condition is repaid"; + assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower); +} + +// Show that a liquidation repaying the maximum amount allowed by the RCF condition +// leaves the position healthy. The market is bound to the global ghosts via +// getGlobalMarket(), so storage keys come from globalId. +rule healthyAfterMaxRcfLiquidation(env e, uint256 seizedAssets, uint256 repaidUnits, address receiver, address callbackAddr, bytes data) { + require forall mathint a. forall mathint b. forall mathint d. axiomDownLowerBound(a, b, d), "floor lower bound on mulDivDown"; + require forall mathint a. forall mathint b. forall mathint d. axiomDownStrictness(a, b, d), "floor strictness on mulDivDown"; + require forall mathint a. forall mathint b. forall mathint d. axiomUpUpperBound(a, b, d), "ceil upper bound on mulDivUp"; + + require globalMarketCollateralLength <= 2, "too many collateralParams for the spec to handle"; + + uint256 collateralIndex; + require collateralIndex < globalMarketCollateralLength, "invalid collateral index"; + + Midnight.Market globalMarket = getGlobalMarket(); + + uint256 lltv = globalMarketCollateralLLTV[collateralIndex]; + uint256 maxLif = globalMarketCollateralMaxLif[collateralIndex]; + require maxLif >= WAD(), "maxLif is at least 1"; + uint256 lifTimesLltv = summaryMulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "maxLif * lltv < 1 so the RCF denominator (1 - maxLif * lltv) is positive"; + + uint256 price = summaryPrice(globalMarketCollateralOracle[collateralIndex]); + uint256 collatBefore = collateral(globalId, globalBorrower, collateralIndex); + uint256 debtBefore = debtOf(globalId, globalBorrower); + + require collatBefore > 0, "borrower has collateral to seize"; + require e.block.timestamp < globalMarketMaturity, "ensure RCF condition is activated"; + + uint256 maxDebt = summaryMulDivDown(summaryMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + require debtBefore > maxDebt, "position is unhealthy before liquidation"; + + uint256 actualSeized; + uint256 actualRepaid; + + actualSeized, actualRepaid = liquidate(e, globalMarket, collateralIndex, seizedAssets, repaidUnits, globalBorrower, receiver, callbackAddr, data); + + require actualRepaid == summaryMulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)), "actualRepaid equals the RCF cap = (debt - maxDebt) / (1 - maxLif * lltv)"; + + assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower); +} diff --git a/certora/specs/LastIdPatternRepro.spec b/certora/specs/LastIdPatternRepro.spec new file mode 100644 index 000000000..a42f507c7 --- /dev/null +++ b/certora/specs/LastIdPatternRepro.spec @@ -0,0 +1,59 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// Minimal reproducer: under the lastId ghost-binding pattern the storage +// write→read link across liquidate is lost. + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function IdLib.toId(Midnight.Obligation memory obligation, uint256, address) internal returns (bytes32) => CVL_toId(obligation); + function touchObligation(Midnight.Obligation memory obligation) internal returns (bytes32) => CVL_toId(obligation); + + function UtilsLib.msb(uint128) internal returns (uint256) => NONDET; + function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; + function UtilsLib.mulDivDown(uint256, uint256, uint256) internal returns (uint256) => NONDET; + function UtilsLib.mulDivUp(uint256, uint256, uint256) internal returns (uint256) => NONDET; + function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; + function TickLib.wExp(int256) internal returns (uint256) => NONDET; + function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; + function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; + function IdLib.storeInCode(Midnight.Obligation memory, uint256) internal returns (address) => NONDET; + + function _.price() external => NONDET; + function _.onLiquidate(bytes32, Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function _.canLiquidate(address) external => NONDET; + + + function collateral(bytes32, address, uint256) external returns (uint128) envfree; +} + +persistent ghost bytes32 lastId; + +function CVL_toId(Midnight.Obligation obligation) returns bytes32 { + bytes32 id; + lastId = id; + return id; +} + + +rule storageDecouples_lastId( + env e, Midnight.Obligation obligation, uint256 seizedAssets, + address borrower, address receiver, address callback, bytes data +) { + require obligation.collateralParams.length == 1; + + bytes32 id; + uint256 collatBefore = collateral(id, borrower, 0); + require seizedAssets > 0; + require collatBefore >= seizedAssets; + + uint256 actualSeized; + actualSeized, _ = liquidate(e, obligation, 0, seizedAssets, 0, borrower, receiver, callback, data); + + require id == lastId; + + uint256 collatAfter = collateral(id, borrower, 0); + + assert collatAfter == collatBefore - actualSeized; +}