From aa57576722cbe7fefadd5a49032ea02ec325fe38 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Sun, 29 Mar 2026 16:57:19 +0200 Subject: [PATCH 01/16] issue with different behaviours on seizedAssets and repaidUnits input --- .../confs/RCFUnhealthyAfterLiquidation.conf | 24 +++ .../specs/RCFUnhealthyAfterLiquidation.spec | 188 ++++++++++++++++++ 2 files changed, 212 insertions(+) create mode 100644 certora/confs/RCFUnhealthyAfterLiquidation.conf create mode 100644 certora/specs/RCFUnhealthyAfterLiquidation.spec diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/RCFUnhealthyAfterLiquidation.conf new file mode 100644 index 000000000..6500fa8e0 --- /dev/null +++ b/certora/confs/RCFUnhealthyAfterLiquidation.conf @@ -0,0 +1,24 @@ +{ + "files": [ + "src/Midnight.sol", + "certora/helpers/FlashLiquidateCallback.sol" + ], + "parametric_contracts": [ + "Midnight" + ], + "verify": "Midnight:certora/specs/RCFUnhealthyAfterLiquidation.spec", + "solc": "solc-0.8.31", + "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 7200", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" + ], + "msg": "RCF: Unhealthy After Liquidation" +} diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec new file mode 100644 index 000000000..1613ad3ee --- /dev/null +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -0,0 +1,188 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// Proves that an RCF-limited liquidation (actualRepaid == maxRepaid) makes the +// position at most "slightly healthy": the exact maxDebt exceeds the new debt by +// at most 1 unit. This accounts for the mulDivUp rounding in maxRepaid, which +// the contract acknowledges at Midnight.sol L494-495. + +methods { + function multicall(bytes[]) external => HAVOC_ALL DELETE; + + function _.price() external => CVL_price(calledContract) expect(uint256); + + function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight); + + function UtilsLib.msb(uint256 bitmap) internal returns (uint256) => CVL_msb(bitmap); + function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; + + function UtilsLib.mulDivDown(uint256 a, uint256 b, uint256 d) internal returns (uint256) => CVL_mulDivDown(a, b, d); + + function UtilsLib.mulDivUp(uint256 a, uint256 b, uint256 d) internal returns (uint256) => CVL_mulDivUp(a, b, d); + + 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) internal returns (address) => NONDET; + + function _.onLiquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + + function collateralOf(bytes32, address, uint256) external returns (uint128) envfree; + function debtOf(bytes32, address) external returns (uint256) envfree; + function activatedCollaterals(bytes32, address) external returns (uint128) envfree; + function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; +} + +persistent ghost bytes32 lastId; + +function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { + bytes32 id; + lastId = id; + return id; +} + +ghost CVL_msb(uint256) returns uint256; + +ghost CVL_price(address) returns uint256; + +/// Exact mulDivDown: floor(a * b / d) +function CVL_mulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + require d > 0; + return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d)); +} + +/// Exact mulDivUp: ceil(a * b / d) +function CVL_mulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + require d > 0; + return require_uint256((to_mathint(a) * to_mathint(b) + to_mathint(d) - 1) / to_mathint(d)); +} + +definition WAD() returns uint256 = 10 ^ 18; + +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; + +/// Proves that an RCF-limited liquidation (actualRepaid == maxRepaid) leaves the +/// position at most "slightly healthy": the exact maxDebt exceeds the new debt +/// by at most 3 unit. +/// +/// The mulDivUp rounding in maxRepaid (Midnight.sol L494-497) intentionally +/// overshoots by up to ε * denom / WAD < 1 debt unit in continuous math. +/// The contract acknowledges this: "the position could be slightly healthy +/// after a liquidation." +/// +/// Preconditions exclude cases where the RCF is structurally deactivated: +/// - badDebt > 0: debt is reduced before the RCF check runs +/// - maxRepaid >= debt: RCF imposes no effective limit (denom explosion or lltv ≈ 0) +/// - maxLif < WAD: implicit invariant from the post-maturity lif formula +rule rcfLiquidationBoundedOvershootRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { + require obligation.collaterals.length == 1; + uint256 collateralIndex = 0; + + uint256 lltv = obligation.collaterals[0].lltv; + uint256 maxLif = obligation.collaterals[0].maxLif; + require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise + + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; + uint256 price = CVL_price(obligation.collaterals[0].oracle); + + bytes32 id; + uint256 collatBefore = collateralOf(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require activatedCollaterals(id, borrower) == 1; + require CVL_msb(1) == 0; + + require e.block.timestamp < obligation.maturity; + require seizedAssets > 0 || repaidUnits > 0; + require repaidUnits > 0; + + uint256 actualRepaid; + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + + require id == lastId; + + // Mirror maxRepaid (post-call, exact arithmetic via mathint) + uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); + + uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); + uint256 badDebt = debtBefore > collatValuePerMaxLif ? assert_uint256(debtBefore - collatValuePerMaxLif) : 0; + + require badDebt == 0; // RCF is deactivated when bad debt accrues + + uint256 effectiveDebt = assert_uint256(debtBefore - badDebt); + uint256 denom = assert_uint256(WAD() - lifTimesLltv); + uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(effectiveDebt - _maxDebt), WAD(), denom); + + require _maxRepaid < effectiveDebt; // RCF actually constrains repayment + + // Maxed out the RCF liquidation. + require actualRepaid == _maxRepaid; + + // Read post-liquidation state + uint256 collatAfter = collateralOf(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + assert isHealthy(e,obligation, id, borrower); +} + +rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { + require obligation.collaterals.length == 1; + uint256 collateralIndex = 0; + + uint256 lltv = obligation.collaterals[0].lltv; + uint256 maxLif = obligation.collaterals[0].maxLif; + require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise + + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; + uint256 price = CVL_price(obligation.collaterals[0].oracle); + + bytes32 id; + uint256 collatBefore = collateralOf(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require activatedCollaterals(id, borrower) == 1; + require CVL_msb(1) == 0; + + require e.block.timestamp < obligation.maturity; + require seizedAssets > 0 || repaidUnits > 0; + require seizedAssets > 0; + + uint256 actualRepaid; + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + + require id == lastId; + + // Mirror maxRepaid (post-call, exact arithmetic via mathint) + uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); + + uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); + + require debtBefore <= collatValuePerMaxLif; // RCF is deactivated when bad debt accrues + + uint256 denom = assert_uint256(WAD() - lifTimesLltv); + uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), denom); + + // Maxed out the RCF liquidation. + require actualRepaid == _maxRepaid; + + // Read post-liquidation state + uint256 collatAfter = collateralOf(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + // compute health (debt-maxDebt) after liquidation + uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); + uint256 _newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); + + assert _newMaxDebt >= debtAfter; +} From d9a5486e626fe80cc43f9e7afb50dca4500faf6f Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 30 Mar 2026 16:23:02 +0200 Subject: [PATCH 02/16] performance improvements in conf and used isHealthyNoBitmap --- .../confs/RCFUnhealthyAfterLiquidation.conf | 11 ++- .../specs/RCFUnhealthyAfterLiquidation.spec | 85 +++++++++++++------ 2 files changed, 68 insertions(+), 28 deletions(-) diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/RCFUnhealthyAfterLiquidation.conf index 6500fa8e0..bb76b13a8 100644 --- a/certora/confs/RCFUnhealthyAfterLiquidation.conf +++ b/certora/confs/RCFUnhealthyAfterLiquidation.conf @@ -1,12 +1,12 @@ { "files": [ - "src/Midnight.sol", + "certora/helpers/MidnightWrapper.sol", "certora/helpers/FlashLiquidateCallback.sol" ], "parametric_contracts": [ - "Midnight" + "MidnightWrapper" ], - "verify": "Midnight:certora/specs/RCFUnhealthyAfterLiquidation.spec", + "verify": "MidnightWrapper:certora/specs/RCFUnhealthyAfterLiquidation.spec", "solc": "solc-0.8.31", "solc_evm_version": "osaka", "solc_via_ir": true, @@ -18,7 +18,10 @@ "-depth 5", "-mediumTimeout 20", "-timeout 7200", - "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]" + "-destructiveOptimizations twostage", + "-splitParallel true", + "-dontStopAtFirstSplitTimeout true", + "-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/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 1613ad3ee..7a677cfc7 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -1,9 +1,10 @@ // SPDX-License-Identifier: GPL-2.0-or-later // Proves that an RCF-limited liquidation (actualRepaid == maxRepaid) makes the -// position at most "slightly healthy": the exact maxDebt exceeds the new debt by -// at most 1 unit. This accounts for the mulDivUp rounding in maxRepaid, which -// the contract acknowledges at Midnight.sol L494-495. +// position healthy. Uses exact mulDiv implementations (floor/ceiling arithmetic) +// because the proof requires lower bounds on mulDivUp — specifically that +// mulDivUp(a, WAD, denom) * denom >= a * WAD — which the relational axioms in +// Healthiness.spec do not provide. methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -12,7 +13,7 @@ methods { function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight); - function UtilsLib.msb(uint256 bitmap) internal returns (uint256) => CVL_msb(bitmap); + function UtilsLib.msb(uint128 bitmap) internal returns (uint256) => CVL_msb(bitmap); function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; function UtilsLib.mulDivDown(uint256 a, uint256 b, uint256 d) internal returns (uint256) => CVL_mulDivDown(a, b, d); @@ -34,6 +35,7 @@ methods { function debtOf(bytes32, address) external returns (uint256) envfree; function activatedCollaterals(bytes32, address) external returns (uint128) envfree; function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; + function isHealthyNoBitmap(Midnight.Obligation, bytes32, address) external returns (bool) envfree; } persistent ghost bytes32 lastId; @@ -44,9 +46,9 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni return id; } -ghost CVL_msb(uint256) returns uint256; +ghost CVL_msb(uint128) returns uint256; -ghost CVL_price(address) returns uint256; +persistent ghost CVL_price(address) returns uint256; /// Exact mulDivDown: floor(a * b / d) function CVL_mulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { @@ -64,20 +66,7 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; -/// Proves that an RCF-limited liquidation (actualRepaid == maxRepaid) leaves the -/// position at most "slightly healthy": the exact maxDebt exceeds the new debt -/// by at most 3 unit. -/// -/// The mulDivUp rounding in maxRepaid (Midnight.sol L494-497) intentionally -/// overshoots by up to ε * denom / WAD < 1 debt unit in continuous math. -/// The contract acknowledges this: "the position could be slightly healthy -/// after a liquidation." -/// -/// Preconditions exclude cases where the RCF is structurally deactivated: -/// - badDebt > 0: debt is reduced before the RCF check runs -/// - maxRepaid >= debt: RCF imposes no effective limit (denom explosion or lltv ≈ 0) -/// - maxLif < WAD: implicit invariant from the post-maturity lif formula -rule rcfLiquidationBoundedOvershootRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { +rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { require obligation.collaterals.length == 1; uint256 collateralIndex = 0; @@ -106,7 +95,7 @@ rule rcfLiquidationBoundedOvershootRepaidUnits(env e, Midnight.Obligation obliga require id == lastId; - // Mirror maxRepaid (post-call, exact arithmetic via mathint) + // Mirror maxRepaid uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); @@ -129,7 +118,7 @@ rule rcfLiquidationBoundedOvershootRepaidUnits(env e, Midnight.Obligation obliga uint256 collatAfter = collateralOf(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); - assert isHealthy(e,obligation, id, borrower); + assert isHealthy(e, obligation, id, borrower); } rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { @@ -161,7 +150,7 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig require id == lastId; - // Mirror maxRepaid (post-call, exact arithmetic via mathint) + // Mirror maxRepaid uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); @@ -180,9 +169,57 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig uint256 collatAfter = collateralOf(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); - // compute health (debt-maxDebt) after liquidation + // compute health after liquidation uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); uint256 _newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); assert _newMaxDebt >= debtAfter; } + +// assume badDebt is zero +rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { + require obligation.collaterals.length == 1; + uint256 collateralIndex = 0; + + uint256 lltv = obligation.collaterals[0].lltv; + uint256 maxLif = obligation.collaterals[0].maxLif; + require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise + + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; + uint256 price = CVL_price(obligation.collaterals[0].oracle); + + bytes32 id; + uint256 collatBefore = collateralOf(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require activatedCollaterals(id, borrower) == 1; + require CVL_msb(1) == 0; + + require e.block.timestamp < obligation.maturity; + require seizedAssets > 0 || repaidUnits > 0; + + uint256 actualRepaid; + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + + require id == lastId; + + // Mirror maxRepaid + uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); + + uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); + + // assume no badDebt accrues. + require debtBefore <= collatValuePerMaxLif; + + uint256 denom = assert_uint256(WAD() - lifTimesLltv); + uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), denom); + + // Maxed out the RCF liquidation. + require actualRepaid == _maxRepaid; + + assert isHealthyNoBitmap(obligation, id, borrower); +} From 62d6753f9c6a5551cbdaff8b10d61eb5e278063e Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 27 Apr 2026 14:11:26 +0200 Subject: [PATCH 03/16] checkpoint of attempts --- .../confs/RCFUnhealthyAfterLiquidation.conf | 2 +- .../specs/RCFUnhealthyAfterLiquidation.spec | 185 +++++++++++++++--- 2 files changed, 162 insertions(+), 25 deletions(-) diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/RCFUnhealthyAfterLiquidation.conf index bb76b13a8..64612ae9c 100644 --- a/certora/confs/RCFUnhealthyAfterLiquidation.conf +++ b/certora/confs/RCFUnhealthyAfterLiquidation.conf @@ -7,7 +7,7 @@ "MidnightWrapper" ], "verify": "MidnightWrapper:certora/specs/RCFUnhealthyAfterLiquidation.spec", - "solc": "solc-0.8.31", + "solc": "solc-0.8.34", "solc_evm_version": "osaka", "solc_via_ir": true, "optimistic_loop": true, diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 7a677cfc7..33dd46812 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -31,7 +31,7 @@ methods { function _.onLiquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; - function collateralOf(bytes32, address, uint256) external returns (uint128) envfree; + function collateral(bytes32, address, uint256) external returns (uint128) envfree; function debtOf(bytes32, address) external returns (uint256) envfree; function activatedCollaterals(bytes32, address) external returns (uint128) envfree; function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; @@ -66,20 +66,20 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; -rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { - require obligation.collaterals.length == 1; +rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; uint256 collateralIndex = 0; - uint256 lltv = obligation.collaterals[0].lltv; - uint256 maxLif = obligation.collaterals[0].maxLif; + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collaterals[0].oracle); + uint256 price = CVL_price(obligation.collateralParams[0].oracle); bytes32 id; - uint256 collatBefore = collateralOf(id, borrower, 0); + uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; @@ -91,7 +91,7 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga require repaidUnits > 0; uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); require id == lastId; @@ -115,26 +115,26 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga require actualRepaid == _maxRepaid; // Read post-liquidation state - uint256 collatAfter = collateralOf(id, borrower, 0); + uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); assert isHealthy(e, obligation, id, borrower); } -rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { - require obligation.collaterals.length == 1; +rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; uint256 collateralIndex = 0; - uint256 lltv = obligation.collaterals[0].lltv; - uint256 maxLif = obligation.collaterals[0].maxLif; + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collaterals[0].oracle); + uint256 price = CVL_price(obligation.collateralParams[0].oracle); bytes32 id; - uint256 collatBefore = collateralOf(id, borrower, 0); + uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; @@ -146,7 +146,7 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig require seizedAssets > 0; uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); require id == lastId; @@ -166,7 +166,7 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig require actualRepaid == _maxRepaid; // Read post-liquidation state - uint256 collatAfter = collateralOf(id, borrower, 0); + uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); // compute health after liquidation @@ -176,21 +176,158 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig assert _newMaxDebt >= debtAfter; } +// repaidUnits > 0 path: +// seizedAssets = repaidUnits.mulDivDown(lif, WAD).mulDivDown(OPS, price) — two floors, net error ≤ 1 collateral unit. +// That 1 missing collateral unit propagates through newMaxDebt with a factor of price, giving +// an extra floor(floor(price / OPS) * lltv / WAD) debt units of surplus. +// Additionally, ceil in maxRepaid adds at most 1 debt unit. +// Total surplus ≤ 1 + floor(floor(price / OPS) * lltv / WAD). +rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; + uint256 collateralIndex = 0; + uint256 seizedAssets = 0; + + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; + require maxLif >= WAD(); + + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; + uint256 price = CVL_price(obligation.collateralParams[0].oracle); + + bytes32 id; + uint256 collatBefore = collateral(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require activatedCollaterals(id, borrower) == 1; + require CVL_msb(1) == 0; + + require e.block.timestamp < obligation.maturity; + require repaidUnits > 0; + + uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); + require debtBefore > maxDebt; // pre-maturity unhealthy → lif = maxLif + + uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); + require debtBefore <= collatValuePerMaxLif; // no bad debt + + uint256 actualRepaid; + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + + require id == lastId; + + uint256 denom = assert_uint256(WAD() - lifTimesLltv); + uint256 maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), denom); + + require maxRepaid < debtBefore; // RCF actually constrains repayment + require actualRepaid == maxRepaid; // RCF cap was hit + + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + // liftedSeized = floor(maxRepaid * maxLif / WAD): the collateral-unit equivalent of maxRepaid. + // These two requires encode the floor round-trip property for seizedAssets: + // seizedAssets = floor(floor(maxRepaid * maxLif / WAD) * OPS / price) + // Upper bound: floor(x * OPS/price) * price/OPS ≤ x → seizedActual * price/OPS ≤ liftedSeized + // Lower bound: floor(x * OPS/price) * price/OPS ≥ x - price/OPS - 1 → seizedActual * price/OPS ≥ liftedSeized - floor(price/OPS) - 1 + // Without these the prover must re-derive the bound through 4 levels of nested non-linear arithmetic. + uint256 seizedActual = assert_uint256(collatBefore - collatAfter); + uint256 liftedSeized = CVL_mulDivDown(maxRepaid, maxLif, WAD()); + require CVL_mulDivDown(seizedActual, price, ORACLE_PRICE_SCALE()) <= liftedSeized; + require to_mathint(CVL_mulDivDown(seizedActual, price, ORACLE_PRICE_SCALE())) + >= to_mathint(liftedSeized) - to_mathint(CVL_mulDivDown(1, price, ORACLE_PRICE_SCALE())) - 1; + + uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); + uint256 newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); + + // Bound derivation. From actualRepaid = ceil((debtBefore - maxDebt) * WAD / (WAD - lifTimesLltv)) + // in real arithmetic: actualRepaid * lifTimesLltv / WAD ≤ maxDebt - debtAfter, with slack < 1. + // newMaxDebt ≈ maxDebt - actualRepaid * lifTimesLltv_real / WAD. Since lifTimesLltv is ceiled, + // lifTimesLltv_ceil - lifTimesLltv_real < 1/WAD, so the gap times actualRepaid contributes up to + // actualRepaid/WAD extra surplus — this term dominates when denom is small (actualRepaid large). + // Plus floor(floor(price/OPS) * lltv/WAD) + 1 from 1 collateral unit miss in seizedAssets × price, + // plus 1 from ceil slack in maxRepaid. + uint256 seizedAssetsRoundingError = CVL_mulDivDown(CVL_mulDivDown(1, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + assert to_mathint(newMaxDebt) - to_mathint(debtAfter) + <= (to_mathint(actualRepaid) + to_mathint(WAD()) - 1) / to_mathint(WAD()) + + 2 + to_mathint(seizedAssetsRoundingError); +} + +// seizedAssets > 0 path: +// repaidUnits = seizedAssets.mulDivUp(price, OPS).mulDivUp(WAD, lif) — two ceils, error ≤ 2 debt units. +// newMaxDebt uses exact seizedAssets (given), so no price-multiplied rounding. +// Total surplus ≤ 2. +rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; + uint256 collateralIndex = 0; + uint256 repaidUnits = 0; + + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; + require maxLif >= WAD(); + + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; + uint256 price = CVL_price(obligation.collateralParams[0].oracle); + + bytes32 id; + uint256 collatBefore = collateral(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require activatedCollaterals(id, borrower) == 1; + require CVL_msb(1) == 0; + + require e.block.timestamp < obligation.maturity; + require seizedAssets > 0; + + uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); + require debtBefore > maxDebt; // pre-maturity unhealthy → lif = maxLif + + uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); + require debtBefore <= collatValuePerMaxLif; // no bad debt + + uint256 actualRepaid; + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + + require id == lastId; + + uint256 denom = assert_uint256(WAD() - lifTimesLltv); + uint256 maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), denom); + + require maxRepaid < debtBefore; // RCF actually constrains repayment + require actualRepaid == maxRepaid; // RCF cap was hit + + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); + uint256 newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); + + // Two ceils in repaidUnits = seizedAssets.mulDivUp(price, OPS).mulDivUp(WAD, lif) → surplus ≤ 2. + assert to_mathint(newMaxDebt) - to_mathint(debtAfter) <= 2; +} + // assume badDebt is zero -rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) { - require obligation.collaterals.length == 1; +rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; uint256 collateralIndex = 0; - uint256 lltv = obligation.collaterals[0].lltv; - uint256 maxLif = obligation.collaterals[0].maxLif; + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collaterals[0].oracle); + uint256 price = CVL_price(obligation.collateralParams[0].oracle); bytes32 id; - uint256 collatBefore = collateralOf(id, borrower, 0); + uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; @@ -201,7 +338,7 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s require seizedAssets > 0 || repaidUnits > 0; uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, data); + _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); require id == lastId; From 772ca4770b90d7e6ad0c159d910712e223c290fc Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 6 May 2026 16:49:17 +0200 Subject: [PATCH 04/16] new rule added: healthy after max RCF liquidation --- .../specs/RCFUnhealthyAfterLiquidation.spec | 231 ++++++++++++++++-- 1 file changed, 210 insertions(+), 21 deletions(-) diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 33dd46812..221d7bd6e 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -27,22 +27,60 @@ methods { function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; - function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET; + function IdLib.storeInCode(Midnight.Obligation memory, uint256) internal returns (address) => NONDET; function _.onLiquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; function collateral(bytes32, address, uint256) external returns (uint128) envfree; function debtOf(bytes32, address) external returns (uint256) envfree; - function activatedCollaterals(bytes32, address) external returns (uint128) envfree; + function collateralBitmap(bytes32, address) external returns (uint128) envfree; function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; function isHealthyNoBitmap(Midnight.Obligation, bytes32, address) external returns (bool) envfree; } -persistent ghost bytes32 lastId; +// Global-obligation pinning: rules fix the obligation under test by requiring +// equalsGlobalObligation(obligation), then bind id := globalId directly. +// summaryToId enforces determinism (same obligation → globalId) and injectivity +// (different obligation → not globalId), removing the need for a `lastId == id` +// require after the liquidate call. +persistent ghost address globalObligationLoanToken; +persistent ghost uint256 globalObligationCollateralLength; +persistent ghost mapping(uint256 => address) globalObligationCollateralOracle; +persistent ghost mapping(uint256 => address) globalObligationCollateralToken; +persistent ghost mapping(uint256 => uint256) globalObligationCollateralLLTV; +persistent ghost mapping(uint256 => uint256) globalObligationCollateralMaxLif; +persistent ghost uint256 globalObligationMaturity; +persistent ghost uint256 globalObligationRcfThreshold; +persistent ghost address globalObligationEnterGate; +persistent ghost address globalObligationLiquidatorGate; +persistent ghost bytes32 globalId; + +definition collateralMatches(Midnight.Obligation obligation, uint256 index) returns bool = + (index < globalObligationCollateralLength => + obligation.collateralParams[index].oracle == globalObligationCollateralOracle[index] && + obligation.collateralParams[index].token == globalObligationCollateralToken[index] && + obligation.collateralParams[index].lltv == globalObligationCollateralLLTV[index] && + obligation.collateralParams[index].maxLif == globalObligationCollateralMaxLif[index]); + +function equalsGlobalObligation(Midnight.Obligation obligation) returns bool { + return obligation.loanToken == globalObligationLoanToken && + obligation.collateralParams.length == globalObligationCollateralLength && + collateralMatches(obligation, 0) && + collateralMatches(obligation, 1) && + collateralMatches(obligation, 2) && + obligation.maturity == globalObligationMaturity && + obligation.rcfThreshold == globalObligationRcfThreshold && + obligation.enterGate == globalObligationEnterGate && + obligation.liquidatorGate == globalObligationLiquidatorGate; +} function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { bytes32 id; - lastId = id; + if (equalsGlobalObligation(obligation) && midnight == currentContract) { + require id == globalId, "toId() is deterministic"; + } else { + require id != globalId, "toId() is injective"; + } return id; } @@ -68,6 +106,8 @@ definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -78,12 +118,12 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = globalId; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; - require activatedCollaterals(id, borrower) == 1; + require collateralBitmap(id, borrower) == 1; require CVL_msb(1) == 0; require e.block.timestamp < obligation.maturity; @@ -93,7 +133,6 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; // Mirror maxRepaid uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); @@ -123,6 +162,8 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -133,12 +174,12 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = globalId; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; - require activatedCollaterals(id, borrower) == 1; + require collateralBitmap(id, borrower) == 1; require CVL_msb(1) == 0; require e.block.timestamp < obligation.maturity; @@ -148,7 +189,6 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; // Mirror maxRepaid uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); @@ -169,11 +209,12 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); + // compute health after liquidation uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); uint256 _newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); - assert _newMaxDebt >= debtAfter; + assert _newMaxDebt + 3 >= debtAfter; } // repaidUnits > 0 path: @@ -184,6 +225,8 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig // Total surplus ≤ 1 + floor(floor(price / OPS) * lltv / WAD). rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 seizedAssets = 0; @@ -195,12 +238,12 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = globalId; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; - require activatedCollaterals(id, borrower) == 1; + require collateralBitmap(id, borrower) == 1; require CVL_msb(1) == 0; require e.block.timestamp < obligation.maturity; @@ -217,7 +260,6 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; uint256 denom = assert_uint256(WAD() - lifTimesLltv); uint256 maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), denom); @@ -262,6 +304,8 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u // Total surplus ≤ 2. rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 repaidUnits = 0; @@ -273,12 +317,12 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = globalId; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; - require activatedCollaterals(id, borrower) == 1; + require collateralBitmap(id, borrower) == 1; require CVL_msb(1) == 0; require e.block.timestamp < obligation.maturity; @@ -295,7 +339,6 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; uint256 denom = assert_uint256(WAD() - lifTimesLltv); uint256 maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), denom); @@ -316,6 +359,8 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u // assume badDebt is zero rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -326,21 +371,21 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = globalId; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); require collatBefore > 0; - require activatedCollaterals(id, borrower) == 1; + require collateralBitmap(id, borrower) == 1; require CVL_msb(1) == 0; require e.block.timestamp < obligation.maturity; require seizedAssets > 0 || repaidUnits > 0; + uint256 actualSeized; uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; // Mirror maxRepaid uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); @@ -358,5 +403,149 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s // Maxed out the RCF liquidation. require actualRepaid == _maxRepaid; + // Pin post-liquidate storage: forces SMT to know values that + // isHealthyNoBitmap will read. Defeats write→read link loss across liquidate. + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); + require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); + + assert isHealthyNoBitmap(obligation, id, borrower); +} + +// Two-sided "at the health boundary" rule for RCF max liquidation. +// Covers BOTH liquidation paths (seizedAssets > 0 and repaidUnits > 0) with +// rounding-aware bounds. +// +// Sources of rounding: +// - 4 floors: 2 in maxDebt, 2 in newMaxDebt +// - ceil in maxRepaid (push debtAfter slightly down) +// - ceil in lifTimesLltv (shrinks denom, push maxRepaid slightly up) +// - ceil in repaidUnits (path 1: 2 ceils, lossless when lif = WAD) +// - 2 floors in seizedActual recompute (path 2 only): adds price/OPS-scaled error +// +// Bounds (debt units): +// - Lower: newMaxDebt + 2 >= debtAfter (constant, both paths) +// - Upper: newMaxDebt - debtAfter <= 2 + ceil(actualRepaid / WAD) + seizedAssetsRoundingError +// (path 1: rounding term ≈ 0; path 2: dominates when price > OPS) +// +// Post-state pinning requires (collatAfter / debtAfter) hand the prover the +// storage-write→read link across liquidate, which the SMT otherwise loses for +// nested mapping `position[id][user].collateral[i]`. +rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; + uint256 collateralIndex = 0; + + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; + require maxLif >= WAD(); + + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; + uint256 price = CVL_price(obligation.collateralParams[0].oracle); + + bytes32 id = globalId; + uint256 collatBefore = collateral(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require collateralBitmap(id, borrower) == 1; + require CVL_msb(1) == 0; + + require e.block.timestamp < obligation.maturity; + require seizedAssets > 0 || repaidUnits > 0; + + uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); + + uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); + uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); + + require debtBefore > _maxDebt; // unhealthy → lif = maxLif + require debtBefore <= collatValuePerMaxLif; // no badDebt + + uint256 denom = assert_uint256(WAD() - lifTimesLltv); + uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), denom); + + require _maxRepaid < debtBefore; // RCF actually constrains + + uint256 actualSeized; + uint256 actualRepaid; + actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + + require actualRepaid == _maxRepaid; // RCF cap hit + + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + // Pin post-state — defeats prover artifacts where storage write→read link is lost. + require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); + require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); + + uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); + uint256 newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); + + // floor(price/OPS) propagated through lltv — only nonzero when price > OPS. + uint256 seizedAssetsRoundingError = CVL_mulDivDown(CVL_mulDivDown(1, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + + // Lower bound: position not far above health line (debt overshoot ≤ 2). + assert to_mathint(newMaxDebt) + 2 >= to_mathint(debtAfter), + "RCF: debt exceeds newMaxDebt by at most 2"; + + // Upper bound: position not far below health line. + assert to_mathint(newMaxDebt) - to_mathint(debtAfter) + <= 2 + (to_mathint(actualRepaid) + to_mathint(WAD()) - 1) / to_mathint(WAD()) + + to_mathint(seizedAssetsRoundingError), + "RCF: newMaxDebt exceeds debt by bounded rounding only"; +} + +// Stripped-down version of healthyAfterRcfLiquidation. Pins post-state collat +// and debt slots via re-read + mathint require — forces SMT to constrain the +// storage that isHealthyNoBitmap subsequently reads, defeating the +// write→read link loss across liquidate seen in earlier CEXes. +rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; + require equalsGlobalObligation(obligation); + require globalObligationCollateralLength == 1; + + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; + require maxLif >= WAD(); + uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); + require lifTimesLltv < WAD(); + + uint256 price = CVL_price(obligation.collateralParams[0].oracle); + bytes32 id = globalId; + uint256 collatBefore = collateral(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + // Guards against degenerate/vacuous configurations: non-empty position, + // pre-maturity unhealthy (so lif = maxLif), valid RCF math. + require collatBefore > 0; + require e.block.timestamp < obligation.maturity; + require seizedAssets > 0 || repaidUnits > 0; + + // No badDebt: debt covered by raw collateral value (pre-lif scaling). + require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); + + // RCF max-repayment formula. + uint256 _maxDebt = CVL_mulDivDown(CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + require debtBefore > _maxDebt; // unhealthy → lif = maxLif and assert_uint256 below safe. + uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); + + uint256 actualSeized; + uint256 actualRepaid; + actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, repaidUnits, borrower, receiver, callback, data); + + require actualRepaid == _maxRepaid; + + // Pin post-liquidate storage so isHealthyNoBitmap reads consistent values. + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); + require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); + assert isHealthyNoBitmap(obligation, id, borrower); } From db89cfcb20df7222297eca2bd081a057481691b3 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 6 May 2026 17:04:06 +0200 Subject: [PATCH 05/16] new rule added: healthy after max RCF liquidation --- .../specs/RCFUnhealthyAfterLiquidation.spec | 80 +++++-------------- 1 file changed, 19 insertions(+), 61 deletions(-) diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 221d7bd6e..6aec30427 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -38,49 +38,14 @@ methods { function isHealthyNoBitmap(Midnight.Obligation, bytes32, address) external returns (bool) envfree; } -// Global-obligation pinning: rules fix the obligation under test by requiring -// equalsGlobalObligation(obligation), then bind id := globalId directly. -// summaryToId enforces determinism (same obligation → globalId) and injectivity -// (different obligation → not globalId), removing the need for a `lastId == id` -// require after the liquidate call. -persistent ghost address globalObligationLoanToken; -persistent ghost uint256 globalObligationCollateralLength; -persistent ghost mapping(uint256 => address) globalObligationCollateralOracle; -persistent ghost mapping(uint256 => address) globalObligationCollateralToken; -persistent ghost mapping(uint256 => uint256) globalObligationCollateralLLTV; -persistent ghost mapping(uint256 => uint256) globalObligationCollateralMaxLif; -persistent ghost uint256 globalObligationMaturity; -persistent ghost uint256 globalObligationRcfThreshold; -persistent ghost address globalObligationEnterGate; -persistent ghost address globalObligationLiquidatorGate; -persistent ghost bytes32 globalId; - -definition collateralMatches(Midnight.Obligation obligation, uint256 index) returns bool = - (index < globalObligationCollateralLength => - obligation.collateralParams[index].oracle == globalObligationCollateralOracle[index] && - obligation.collateralParams[index].token == globalObligationCollateralToken[index] && - obligation.collateralParams[index].lltv == globalObligationCollateralLLTV[index] && - obligation.collateralParams[index].maxLif == globalObligationCollateralMaxLif[index]); - -function equalsGlobalObligation(Midnight.Obligation obligation) returns bool { - return obligation.loanToken == globalObligationLoanToken && - obligation.collateralParams.length == globalObligationCollateralLength && - collateralMatches(obligation, 0) && - collateralMatches(obligation, 1) && - collateralMatches(obligation, 2) && - obligation.maturity == globalObligationMaturity && - obligation.rcfThreshold == globalObligationRcfThreshold && - obligation.enterGate == globalObligationEnterGate && - obligation.liquidatorGate == globalObligationLiquidatorGate; -} +// Last-id pattern: CVL_toId stashes the returned id into lastId ghost. +// Each rule binds `bytes32 id;` and requires `id == lastId` after the +// liquidate call to tie the spec's id reads to the contract's internal id. +persistent ghost bytes32 lastId; function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { bytes32 id; - if (equalsGlobalObligation(obligation) && midnight == currentContract) { - require id == globalId, "toId() is deterministic"; - } else { - require id != globalId, "toId() is injective"; - } + lastId = id; return id; } @@ -106,8 +71,6 @@ definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -118,7 +81,7 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -132,6 +95,7 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; // Mirror maxRepaid @@ -162,8 +126,6 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -174,7 +136,7 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -188,6 +150,7 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; // Mirror maxRepaid @@ -225,8 +188,6 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig // Total surplus ≤ 1 + floor(floor(price / OPS) * lltv / WAD). rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 seizedAssets = 0; @@ -238,7 +199,7 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -259,6 +220,7 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; uint256 denom = assert_uint256(WAD() - lifTimesLltv); @@ -304,8 +266,6 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u // Total surplus ≤ 2. rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 repaidUnits = 0; @@ -317,7 +277,7 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -338,6 +298,7 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; uint256 denom = assert_uint256(WAD() - lifTimesLltv); @@ -359,8 +320,6 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u // assume badDebt is zero rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -371,7 +330,7 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -385,6 +344,7 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; // Mirror maxRepaid @@ -434,8 +394,6 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s // nested mapping `position[id][user].collateral[i]`. rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 collateralIndex = 0; uint256 lltv = obligation.collateralParams[0].lltv; @@ -446,7 +404,7 @@ rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, ui require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -474,6 +432,7 @@ rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, ui uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; require actualRepaid == _maxRepaid; // RCF cap hit @@ -507,8 +466,6 @@ rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, ui // write→read link loss across liquidate seen in earlier CEXes. rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; - require equalsGlobalObligation(obligation); - require globalObligationCollateralLength == 1; uint256 lltv = obligation.collateralParams[0].lltv; uint256 maxLif = obligation.collateralParams[0].maxLif; @@ -517,7 +474,7 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 require lifTimesLltv < WAD(); uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = globalId; + bytes32 id; uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -538,6 +495,7 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, repaidUnits, borrower, receiver, callback, data); + require id == lastId; require actualRepaid == _maxRepaid; From 40ed8f5d53f0278e5132a5196e3410725b69eab1 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 6 May 2026 21:10:55 +0200 Subject: [PATCH 06/16] diagnostics to check if actualRepaid is returned correctly in seizedAssets>0 case --- .../specs/RCFUnhealthyAfterLiquidation.spec | 80 ++++++++++++++++++- 1 file changed, 79 insertions(+), 1 deletion(-) diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 6aec30427..848396d73 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -482,7 +482,6 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 // pre-maturity unhealthy (so lif = maxLif), valid RCF math. require collatBefore > 0; require e.block.timestamp < obligation.maturity; - require seizedAssets > 0 || repaidUnits > 0; // No badDebt: debt covered by raw collateral value (pre-lif scaling). require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); @@ -507,3 +506,82 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 assert isHealthyNoBitmap(obligation, id, borrower); } + +// ============================================================================ +// Minimal reproducer rules — diagnose whether the storage write→read link +// across `liquidate` is preserved by the SMT. NO RCF math, no health check, +// no obligation pinning beyond length=1. If these CEX, the prover is failing +// to propagate the slot-write inside liquidate to the slot-read after. +// ============================================================================ + +// Tests: in seizedAssets > 0 path, collat[0] decrements by exactly the +// returned actualSeized value, and debt decrements by actualRepaid. +// Requires no badDebt — otherwise contract decrements debt by an extra +// `badDebt` amount that's NOT returned in the liquidate tuple. +rule storageLinkSeizedPath(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; + + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; + require maxLif >= WAD(); + uint256 price = CVL_price(obligation.collateralParams[0].oracle); + + bytes32 id; + uint256 collatBefore = collateral(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require debtBefore > 0; + require seizedAssets > 0; + + // No badDebt: contract's badDebt branch decrements debt by an amount not + // captured in the liquidate return tuple. + require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); + + uint256 actualSeized; + uint256 actualRepaid; + actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, 0, borrower, receiver, callback, data); + require id == lastId; + + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + assert to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized), + "collat decrement mismatch"; + assert to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid), + "debt decrement mismatch"; +} + +// Tests: in repaidUnits > 0 path. Same property as above for the other branch. +// Same no-badDebt precondition. +rule storageLinkRepaidPath(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require obligation.collateralParams.length == 1; + + uint256 lltv = obligation.collateralParams[0].lltv; + uint256 maxLif = obligation.collateralParams[0].maxLif; + require maxLif >= WAD(); + uint256 price = CVL_price(obligation.collateralParams[0].oracle); + + bytes32 id; + uint256 collatBefore = collateral(id, borrower, 0); + uint256 debtBefore = debtOf(id, borrower); + + require collatBefore > 0; + require debtBefore > 0; + require repaidUnits > 0; + + require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); + + uint256 actualSeized; + uint256 actualRepaid; + actualSeized, actualRepaid = liquidate(e, obligation, 0, 0, repaidUnits, borrower, receiver, callback, data); + require id == lastId; + + uint256 collatAfter = collateral(id, borrower, 0); + uint256 debtAfter = debtOf(id, borrower); + + assert to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized), + "collat decrement mismatch"; + assert to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid), + "debt decrement mismatch"; +} From 9eacc6a261afbddbfb0fcb10ecdbf7e5ead2e4bf Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 7 May 2026 10:14:15 +0200 Subject: [PATCH 07/16] hitting TO with the tight summaries for muldivs --- .../confs/RCFUnhealthyAfterLiquidation.conf | 9 +- .../specs/RCFUnhealthyAfterLiquidation.spec | 126 ++++++++++-------- 2 files changed, 72 insertions(+), 63 deletions(-) diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/RCFUnhealthyAfterLiquidation.conf index 64612ae9c..89248f4ff 100644 --- a/certora/confs/RCFUnhealthyAfterLiquidation.conf +++ b/certora/confs/RCFUnhealthyAfterLiquidation.conf @@ -1,12 +1,13 @@ { "files": [ - "certora/helpers/MidnightWrapper.sol", - "certora/helpers/FlashLiquidateCallback.sol" + "src/Midnight.sol", + "certora/helpers/FlashLiquidateCallback.sol", + "certora/helpers/Utils.sol" ], "parametric_contracts": [ - "MidnightWrapper" + "Midnight" ], - "verify": "MidnightWrapper:certora/specs/RCFUnhealthyAfterLiquidation.spec", + "verify": "Midnight:certora/specs/RCFUnhealthyAfterLiquidation.spec", "solc": "solc-0.8.34", "solc_evm_version": "osaka", "solc_via_ir": true, diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 848396d73..4eea14775 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -6,12 +6,19 @@ // mulDivUp(a, WAD, denom) * denom >= a * WAD — which the relational axioms in // Healthiness.spec do not provide. +using Utils as Utils; + methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function _.price() external => CVL_price(calledContract) expect(uint256); - function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight); + // Deterministic toId via Utils harness — same obligation always returns the + // same id. Avoids the storage write→read link loss seen with the lastId + // ghost pattern (where id is symbolic with a post-hoc constraint). + function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation); + function touchObligation(Midnight.Obligation memory obligation) internal returns (bytes32) => CVL_toId(obligation); + function Utils.hashObligation(Midnight.Obligation) external returns (bytes32) envfree; function UtilsLib.msb(uint128 bitmap) internal returns (uint256) => CVL_msb(bitmap); function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; @@ -35,34 +42,37 @@ methods { function debtOf(bytes32, address) external returns (uint256) envfree; function collateralBitmap(bytes32, address) external returns (uint128) envfree; function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; - function isHealthyNoBitmap(Midnight.Obligation, bytes32, address) external returns (bool) envfree; } -// Last-id pattern: CVL_toId stashes the returned id into lastId ghost. -// Each rule binds `bytes32 id;` and requires `id == lastId` after the -// liquidate call to tie the spec's id reads to the contract's internal id. -persistent ghost bytes32 lastId; - -function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { - bytes32 id; - lastId = id; - return id; +function CVL_toId(Midnight.Obligation obligation) returns bytes32 { + return Utils.hashObligation(obligation); } ghost CVL_msb(uint128) returns uint256; persistent ghost CVL_price(address) returns uint256; -/// Exact mulDivDown: floor(a * b / d) +// Tight relational mulDiv axioms — uniquely pin floor/ceil values, equivalent +// to exact mathint but typically faster for the SMT. +// Axioms proven in MulDiv.spec. +persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 { + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => ghostMulDivDown(a, b, d) * d <= a * b; + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => (ghostMulDivDown(a, b, d) + 1) * d > a * b; +} + +persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256 { + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => ghostMulDivUp(a, b, d) * d >= a * b; + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && ghostMulDivUp(a, b, d) > 0 => (ghostMulDivUp(a, b, d) - 1) * d < a * b; +} + function CVL_mulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { require d > 0; - return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d)); + return ghostMulDivDown(a, b, d); } -/// Exact mulDivUp: ceil(a * b / d) function CVL_mulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { require d > 0; - return require_uint256((to_mathint(a) * to_mathint(b) + to_mathint(d) - 1) / to_mathint(d)); + return ghostMulDivUp(a, b, d); } definition WAD() returns uint256 = 10 ^ 18; @@ -81,7 +91,7 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -95,7 +105,6 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; // Mirror maxRepaid @@ -121,7 +130,7 @@ rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obliga uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); - assert isHealthy(e, obligation, id, borrower); + assert isHealthy(obligation, id, borrower); } rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { @@ -136,7 +145,7 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -150,7 +159,6 @@ rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation oblig uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; // Mirror maxRepaid @@ -199,7 +207,7 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -220,7 +228,6 @@ rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, u uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; uint256 denom = assert_uint256(WAD() - lifTimesLltv); @@ -277,7 +284,7 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -298,7 +305,6 @@ rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, u uint256 actualRepaid; _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; uint256 denom = assert_uint256(WAD() - lifTimesLltv); @@ -330,7 +336,7 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -344,7 +350,6 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; // Mirror maxRepaid @@ -370,7 +375,7 @@ rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 s require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); - assert isHealthyNoBitmap(obligation, id, borrower); + assert isHealthy(obligation, id, borrower); } // Two-sided "at the health boundary" rule for RCF max liquidation. @@ -404,7 +409,7 @@ rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, ui require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -432,7 +437,6 @@ rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, ui uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; require actualRepaid == _maxRepaid; // RCF cap hit @@ -474,7 +478,7 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 require lifTimesLltv < WAD(); uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -494,7 +498,6 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require id == lastId; require actualRepaid == _maxRepaid; @@ -504,7 +507,7 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); - assert isHealthyNoBitmap(obligation, id, borrower); + assert isHealthy(obligation, id, borrower); } // ============================================================================ @@ -514,10 +517,14 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 // to propagate the slot-write inside liquidate to the slot-read after. // ============================================================================ +// Workaround for CVL tuple-return bug: instead of capturing actualSeized/ +// actualRepaid from liquidate's return tuple (the second element gets bound +// incorrectly — confirmed via test/RcfReproTest.sol), discard the returns +// and derive both from storage delta. Forge test confirms storage updates +// are correct. +// // Tests: in seizedAssets > 0 path, collat[0] decrements by exactly the -// returned actualSeized value, and debt decrements by actualRepaid. -// Requires no badDebt — otherwise contract decrements debt by an extra -// `badDebt` amount that's NOT returned in the liquidate tuple. +// user's seizedAssets input (contract does not modify it in this branch). rule storageLinkSeizedPath(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; @@ -526,7 +533,7 @@ rule storageLinkSeizedPath(env e, Midnight.Obligation obligation, uint256 seized require maxLif >= WAD(); uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -534,26 +541,28 @@ rule storageLinkSeizedPath(env e, Midnight.Obligation obligation, uint256 seized require debtBefore > 0; require seizedAssets > 0; - // No badDebt: contract's badDebt branch decrements debt by an amount not - // captured in the liquidate return tuple. + // Bitmap pins collat[0] as the only active collateral. Without this, + // the no-badDebt require below is vacuous (it bounds debt by a spec- + // local hypothetical, but contract's badDebt loop iterates only set + // bits, so with bitmap=0 the contract sees badDebt = full debt). + require collateralBitmap(id, borrower) == 1; + require CVL_msb(1) == 0; + + // No badDebt: with bitmap=1, contract's loop accumulates exactly the + // term below, so this require ⇔ contract's badDebt = 0. require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - uint256 actualSeized; - uint256 actualRepaid; - actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, 0, borrower, receiver, callback, data); - require id == lastId; + _, _ = liquidate(e, obligation, 0, seizedAssets, 0, borrower, receiver, callback, data); uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - assert to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized), - "collat decrement mismatch"; - assert to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid), - "debt decrement mismatch"; + // Contract decrements collat[0] by user's seizedAssets exactly. + assert to_mathint(collatBefore) - to_mathint(collatAfter) == to_mathint(seizedAssets), + "collat decrement equals user's seizedAssets"; } -// Tests: in repaidUnits > 0 path. Same property as above for the other branch. -// Same no-badDebt precondition. +// Tests: in repaidUnits > 0 path, debt decrements by exactly the user's +// repaidUnits input (contract does not modify it in this branch). rule storageLinkRepaidPath(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { require obligation.collateralParams.length == 1; @@ -562,7 +571,7 @@ rule storageLinkRepaidPath(env e, Midnight.Obligation obligation, uint256 repaid require maxLif >= WAD(); uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id; + bytes32 id = toId(e, obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); @@ -570,18 +579,17 @@ rule storageLinkRepaidPath(env e, Midnight.Obligation obligation, uint256 repaid require debtBefore > 0; require repaidUnits > 0; + // Bitmap pins collat[0] as active — same reason as in storageLinkSeizedPath. + require collateralBitmap(id, borrower) == 1; + require CVL_msb(1) == 0; + require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - uint256 actualSeized; - uint256 actualRepaid; - actualSeized, actualRepaid = liquidate(e, obligation, 0, 0, repaidUnits, borrower, receiver, callback, data); - require id == lastId; + _, _ = liquidate(e, obligation, 0, 0, repaidUnits, borrower, receiver, callback, data); - uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); - assert to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized), - "collat decrement mismatch"; - assert to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid), - "debt decrement mismatch"; + // Contract decrements debt by user's repaidUnits exactly (no badDebt → only one decrement). + assert to_mathint(debtBefore) - to_mathint(debtAfter) == to_mathint(repaidUnits), + "debt decrement equals user's repaidUnits"; } From a401a1626201fcc92ac04949877aba9ab5dea2cb Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 7 May 2026 22:44:02 +0200 Subject: [PATCH 08/16] minimal example for inconsistent storage read after constraining lastId=id --- certora/confs/LastIdPatternRepro.conf | 25 ++++++++++ certora/specs/LastIdPatternRepro.spec | 70 +++++++++++++++++++++++++++ 2 files changed, 95 insertions(+) create mode 100644 certora/confs/LastIdPatternRepro.conf create mode 100644 certora/specs/LastIdPatternRepro.spec 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/LastIdPatternRepro.spec b/certora/specs/LastIdPatternRepro.spec new file mode 100644 index 000000000..c90fc5c63 --- /dev/null +++ b/certora/specs/LastIdPatternRepro.spec @@ -0,0 +1,70 @@ +// 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. +// +// Setup: toId summary returns nondet bytes32, side-effects ghost lastId. +// Rule binds `bytes32 id;` (free), reads collateral[id, borrower, 0] before +// the call, then `require id == lastId` after, then reads again. The post +// read uses the resolved id; the pre read uses a symbolic id that the SMT +// can resolve to a different position. Assertion violated. +// +// Foundry test/RcfReproTest.sol confirms storage decrement matches +// returned actualSeized at byte-identical state — so CEX is a CVL artefact. + +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; +} + +// Expected CEX. Contract decrements collateral[collateralIndex] by exactly +// the returned actualSeized in the seizedAssets-input path, regardless of +// badDebt. lastId binding lets SMT decouple pre/post storage reads. +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; +} From 6703471b15fc0bf58c0d1e031e0167a61682a463 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 7 May 2026 22:46:37 +0200 Subject: [PATCH 09/16] tuned comments --- certora/specs/LastIdPatternRepro.spec | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/certora/specs/LastIdPatternRepro.spec b/certora/specs/LastIdPatternRepro.spec index c90fc5c63..a42f507c7 100644 --- a/certora/specs/LastIdPatternRepro.spec +++ b/certora/specs/LastIdPatternRepro.spec @@ -2,15 +2,6 @@ // Minimal reproducer: under the lastId ghost-binding pattern the storage // write→read link across liquidate is lost. -// -// Setup: toId summary returns nondet bytes32, side-effects ghost lastId. -// Rule binds `bytes32 id;` (free), reads collateral[id, borrower, 0] before -// the call, then `require id == lastId` after, then reads again. The post -// read uses the resolved id; the pre read uses a symbolic id that the SMT -// can resolve to a different position. Assertion violated. -// -// Foundry test/RcfReproTest.sol confirms storage decrement matches -// returned actualSeized at byte-identical state — so CEX is a CVL artefact. methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -45,9 +36,7 @@ function CVL_toId(Midnight.Obligation obligation) returns bytes32 { return id; } -// Expected CEX. Contract decrements collateral[collateralIndex] by exactly -// the returned actualSeized in the seizedAssets-input path, regardless of -// badDebt. lastId binding lets SMT decouple pre/post storage reads. + rule storageDecouples_lastId( env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data From 2b401a55a958b46189f5824fb8e4e25e0142d767 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 11 May 2026 19:08:15 +0200 Subject: [PATCH 10/16] concrete and symbolic with summaryToId --- .../specs/RCFUnhealthyAfterLiquidation.spec | 563 ++++-------------- 1 file changed, 105 insertions(+), 458 deletions(-) diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 4eea14775..c7e0e7a33 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -6,19 +6,17 @@ // mulDivUp(a, WAD, denom) * denom >= a * WAD — which the relational axioms in // Healthiness.spec do not provide. -using Utils as Utils; - methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; function _.price() external => CVL_price(calledContract) expect(uint256); - // Deterministic toId via Utils harness — same obligation always returns the - // same id. Avoids the storage write→read link loss seen with the lastId - // ghost pattern (where id is symbolic with a post-hoc constraint). - function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation); + // toId is summarized to a ghost-bound id (`globalId`) when the input matches + // the global obligation ghosts, else to a distinct id. Mirrors Healthiness.spec. + // Eliminates symbolic-keccak reasoning; storage keys become a free ghost + // scalar rather than a hash over the symbolic struct. + function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => summaryToId(obligation, chainId, midnight); function touchObligation(Midnight.Obligation memory obligation) internal returns (bytes32) => CVL_toId(obligation); - function Utils.hashObligation(Midnight.Obligation) external returns (bytes32) envfree; function UtilsLib.msb(uint128 bitmap) internal returns (uint256) => CVL_msb(bitmap); function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; @@ -37,6 +35,7 @@ methods { function IdLib.storeInCode(Midnight.Obligation memory, uint256) internal returns (address) => NONDET; function _.onLiquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; + function UtilsLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; function collateral(bytes32, address, uint256) external returns (uint128) envfree; function debtOf(bytes32, address) external returns (uint256) envfree; @@ -44,8 +43,23 @@ methods { function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; } +// Ghost-bound id used by summaryToId. Free at rule entry; the summary pins +// matching-obligation calls to it and non-matching calls away from it. +persistent ghost bytes32 globalId; + +function summaryToId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { + bytes32 id; + if (equalsGlobalObligation(obligation) && midnight == currentContract) { + require id == globalId, "toId() is deterministic"; + } else { + require id != globalId, "toId() is injective"; + } + return id; +} + +// Legacy entry point retained for touchObligation summary. function CVL_toId(Midnight.Obligation obligation) returns bytes32 { - return Utils.hashObligation(obligation); + return summaryToId(obligation, 0, currentContract); } ghost CVL_msb(uint128) returns uint256; @@ -79,420 +93,138 @@ definition WAD() returns uint256 = 10 ^ 18; definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; -rule rcfLiquidationOvershootBoundedRepaidUnits(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - uint256 collateralIndex = 0; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise - - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; +persistent ghost address globalObligationLoanToken; - require e.block.timestamp < obligation.maturity; - require seizedAssets > 0 || repaidUnits > 0; - require repaidUnits > 0; +persistent ghost uint256 globalObligationCollateralLength; - uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); +persistent ghost mapping(uint256 => address) globalObligationCollateralOracle; +persistent ghost mapping(uint256 => address) globalObligationCollateralToken; - // Mirror maxRepaid - uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); +persistent ghost mapping(uint256 => uint256) globalObligationCollateralLLTV; - uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); - uint256 badDebt = debtBefore > collatValuePerMaxLif ? assert_uint256(debtBefore - collatValuePerMaxLif) : 0; +persistent ghost mapping(uint256 => uint256) globalObligationCollateralMaxLif; - require badDebt == 0; // RCF is deactivated when bad debt accrues +persistent ghost uint256 globalObligationMaturity; - uint256 effectiveDebt = assert_uint256(debtBefore - badDebt); - uint256 denom = assert_uint256(WAD() - lifTimesLltv); - uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(effectiveDebt - _maxDebt), WAD(), denom); +persistent ghost uint256 globalObligationRcfThreshold; - require _maxRepaid < effectiveDebt; // RCF actually constrains repayment +persistent ghost address globalObligationEnterGate; - // Maxed out the RCF liquidation. - require actualRepaid == _maxRepaid; +persistent ghost address globalObligationLiquidatorGate; - // Read post-liquidation state - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); +definition collateralMatches(Midnight.Obligation obligation, uint256 index) returns bool = + (index < globalObligationCollateralLength + => obligation.collateralParams[index].oracle == globalObligationCollateralOracle[index] + && obligation.collateralParams[index].token == globalObligationCollateralToken[index] + && obligation.collateralParams[index].lltv == globalObligationCollateralLLTV[index] + && obligation.collateralParams[index].maxLif == globalObligationCollateralMaxLif[index]); - assert isHealthy(obligation, id, borrower); +function equalsGlobalObligation(Midnight.Obligation obligation) returns (bool) { + return obligation.loanToken == globalObligationLoanToken + && obligation.collateralParams.length == globalObligationCollateralLength + && collateralMatches(obligation, 0) + && collateralMatches(obligation, 1) + && collateralMatches(obligation, 2) + && obligation.maturity == globalObligationMaturity + && obligation.rcfThreshold == globalObligationRcfThreshold + && obligation.enterGate == globalObligationEnterGate + && obligation.liquidatorGate == globalObligationLiquidatorGate; } -rule rcfLiquidationBoundedOvershootSeizedAssets(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - uint256 collateralIndex = 0; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise - - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; - - require e.block.timestamp < obligation.maturity; - require seizedAssets > 0 || repaidUnits > 0; - require seizedAssets > 0; - - uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - - - // Mirror maxRepaid - uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); - - uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); - - require debtBefore <= collatValuePerMaxLif; // RCF is deactivated when bad debt accrues - - uint256 denom = assert_uint256(WAD() - lifTimesLltv); - uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), denom); - - // Maxed out the RCF liquidation. - require actualRepaid == _maxRepaid; - - // Read post-liquidation state - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - - - // compute health after liquidation - uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - uint256 _newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); - - assert _newMaxDebt + 3 >= debtAfter; +function getGlobalObligation() returns (Midnight.Obligation) { + Midnight.Obligation obligation; + require equalsGlobalObligation(obligation), "get global obligation"; + return obligation; } -// repaidUnits > 0 path: -// seizedAssets = repaidUnits.mulDivDown(lif, WAD).mulDivDown(OPS, price) — two floors, net error ≤ 1 collateral unit. -// That 1 missing collateral unit propagates through newMaxDebt with a factor of price, giving -// an extra floor(floor(price / OPS) * lltv / WAD) debt units of surplus. -// Additionally, ceil in maxRepaid adds at most 1 debt unit. -// Total surplus ≤ 1 + floor(floor(price / OPS) * lltv / WAD). -rule rcfLiquidationSurplusBoundedRepaid(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - uint256 collateralIndex = 0; - uint256 seizedAssets = 0; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; +rule concreteObligationHealthyAfterMaxRcfLiquidation(env e, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + require globalObligationLoanToken == 0x0000000000000000000000000000000000001001; + require globalObligationCollateralLength == 1; + require globalObligationCollateralOracle[0] == 0x0000000000000000000000000000000000001003; + require globalObligationCollateralToken[0] == 0x0000000000000000000000000000000000001002; + require globalObligationCollateralLLTV[0] == 770000000000000000; + require globalObligationCollateralMaxLif[0] == 1061007957559681697; + require globalObligationMaturity == 2000000000; + require globalObligationRcfThreshold == 0; + require globalObligationEnterGate == 0; + require globalObligationLiquidatorGate == 0; + require callback == 0; + + Midnight.Obligation obligation = getGlobalObligation(); + + uint256 lltv = globalObligationCollateralLLTV[0]; + uint256 maxLif = globalObligationCollateralMaxLif[0]; require maxLif >= WAD(); - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; - - require e.block.timestamp < obligation.maturity; - require repaidUnits > 0; - - uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); - require debtBefore > maxDebt; // pre-maturity unhealthy → lif = maxLif - - uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); - require debtBefore <= collatValuePerMaxLif; // no bad debt - - uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - - - uint256 denom = assert_uint256(WAD() - lifTimesLltv); - uint256 maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), denom); - - require maxRepaid < debtBefore; // RCF actually constrains repayment - require actualRepaid == maxRepaid; // RCF cap was hit - - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - - // liftedSeized = floor(maxRepaid * maxLif / WAD): the collateral-unit equivalent of maxRepaid. - // These two requires encode the floor round-trip property for seizedAssets: - // seizedAssets = floor(floor(maxRepaid * maxLif / WAD) * OPS / price) - // Upper bound: floor(x * OPS/price) * price/OPS ≤ x → seizedActual * price/OPS ≤ liftedSeized - // Lower bound: floor(x * OPS/price) * price/OPS ≥ x - price/OPS - 1 → seizedActual * price/OPS ≥ liftedSeized - floor(price/OPS) - 1 - // Without these the prover must re-derive the bound through 4 levels of nested non-linear arithmetic. - uint256 seizedActual = assert_uint256(collatBefore - collatAfter); - uint256 liftedSeized = CVL_mulDivDown(maxRepaid, maxLif, WAD()); - require CVL_mulDivDown(seizedActual, price, ORACLE_PRICE_SCALE()) <= liftedSeized; - require to_mathint(CVL_mulDivDown(seizedActual, price, ORACLE_PRICE_SCALE())) - >= to_mathint(liftedSeized) - to_mathint(CVL_mulDivDown(1, price, ORACLE_PRICE_SCALE())) - 1; - - uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - uint256 newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); - - // Bound derivation. From actualRepaid = ceil((debtBefore - maxDebt) * WAD / (WAD - lifTimesLltv)) - // in real arithmetic: actualRepaid * lifTimesLltv / WAD ≤ maxDebt - debtAfter, with slack < 1. - // newMaxDebt ≈ maxDebt - actualRepaid * lifTimesLltv_real / WAD. Since lifTimesLltv is ceiled, - // lifTimesLltv_ceil - lifTimesLltv_real < 1/WAD, so the gap times actualRepaid contributes up to - // actualRepaid/WAD extra surplus — this term dominates when denom is small (actualRepaid large). - // Plus floor(floor(price/OPS) * lltv/WAD) + 1 from 1 collateral unit miss in seizedAssets × price, - // plus 1 from ceil slack in maxRepaid. - uint256 seizedAssetsRoundingError = CVL_mulDivDown(CVL_mulDivDown(1, price, ORACLE_PRICE_SCALE()), lltv, WAD()); - assert to_mathint(newMaxDebt) - to_mathint(debtAfter) - <= (to_mathint(actualRepaid) + to_mathint(WAD()) - 1) / to_mathint(WAD()) - + 2 + to_mathint(seizedAssetsRoundingError); -} - -// seizedAssets > 0 path: -// repaidUnits = seizedAssets.mulDivUp(price, OPS).mulDivUp(WAD, lif) — two ceils, error ≤ 2 debt units. -// newMaxDebt uses exact seizedAssets (given), so no price-multiplied rounding. -// Total surplus ≤ 2. -rule rcfLiquidationSurplusBoundedSeized(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - uint256 collateralIndex = 0; - uint256 repaidUnits = 0; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); - - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collateralParams[0].oracle); + require lifTimesLltv < WAD(); - bytes32 id = toId(e, obligation); + uint256 price = CVL_price(globalObligationCollateralOracle[0]); + bytes32 id = CVL_toId(obligation); uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); + // Guards against degenerate/vacuous configurations: non-empty position, + // pre-maturity unhealthy (so lif = maxLif), valid RCF math. require collatBefore > 0; - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; - require e.block.timestamp < obligation.maturity; - require seizedAssets > 0; - - uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); - require debtBefore > maxDebt; // pre-maturity unhealthy → lif = maxLif - - uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); - require debtBefore <= collatValuePerMaxLif; // no bad debt - - uint256 actualRepaid; - _, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - - - uint256 denom = assert_uint256(WAD() - lifTimesLltv); - uint256 maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), denom); - - require maxRepaid < debtBefore; // RCF actually constrains repayment - require actualRepaid == maxRepaid; // RCF cap was hit - - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - - uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - uint256 newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); - - // Two ceils in repaidUnits = seizedAssets.mulDivUp(price, OPS).mulDivUp(WAD, lif) → surplus ≤ 2. - assert to_mathint(newMaxDebt) - to_mathint(debtAfter) <= 2; -} - -// assume badDebt is zero -rule healthyAfterRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - uint256 collateralIndex = 0; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); // implicit invariant: post-maturity lif formula underflows otherwise - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; + // No badDebt: debt covered by raw collateral value (pre-lif scaling). + require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - require e.block.timestamp < obligation.maturity; - require seizedAssets > 0 || repaidUnits > 0; + // RCF max-repayment formula. + uint256 _maxDebt = CVL_mulDivDown(CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + require debtBefore > _maxDebt; + uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); uint256 actualSeized; uint256 actualRepaid; - actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - - - // Mirror maxRepaid - uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); - - uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); - - // assume no badDebt accrues. - require debtBefore <= collatValuePerMaxLif; - - uint256 denom = assert_uint256(WAD() - lifTimesLltv); - uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), denom); + actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, repaidUnits, borrower, receiver, callback, data); - // Maxed out the RCF liquidation. require actualRepaid == _maxRepaid; - // Pin post-liquidate storage: forces SMT to know values that - // isHealthyNoBitmap will read. Defeats write→read link loss across liquidate. + // Pin post-liquidate storage so isHealthy reads consistent values. uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); - require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); - require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); + assert collatAfter == collatBefore - actualSeized; + assert debtAfter == debtBefore - actualRepaid; assert isHealthy(obligation, id, borrower); } -// Two-sided "at the health boundary" rule for RCF max liquidation. -// Covers BOTH liquidation paths (seizedAssets > 0 and repaidUnits > 0) with -// rounding-aware bounds. -// -// Sources of rounding: -// - 4 floors: 2 in maxDebt, 2 in newMaxDebt -// - ceil in maxRepaid (push debtAfter slightly down) -// - ceil in lifTimesLltv (shrinks denom, push maxRepaid slightly up) -// - ceil in repaidUnits (path 1: 2 ceils, lossless when lif = WAD) -// - 2 floors in seizedActual recompute (path 2 only): adds price/OPS-scaled error -// -// Bounds (debt units): -// - Lower: newMaxDebt + 2 >= debtAfter (constant, both paths) -// - Upper: newMaxDebt - debtAfter <= 2 + ceil(actualRepaid / WAD) + seizedAssetsRoundingError -// (path 1: rounding term ≈ 0; path 2: dominates when price > OPS) -// -// Post-state pinning requires (collatAfter / debtAfter) hand the prover the -// storage-write→read link across liquidate, which the SMT otherwise loses for -// nested mapping `position[id][user].collateral[i]`. -rule rcfMaxLiquidationAtHealthBoundary(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - uint256 collateralIndex = 0; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); - - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(), "See lifTimesLltvIsLessThanOrEqualToOne in ExactMath.spec"; - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; - - require e.block.timestamp < obligation.maturity; - require seizedAssets > 0 || repaidUnits > 0; - - uint256 collatValueDown = CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 _maxDebt = CVL_mulDivDown(collatValueDown, lltv, WAD()); - - uint256 collatValueUp = CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()); - uint256 collatValuePerMaxLif = CVL_mulDivUp(collatValueUp, WAD(), maxLif); - - require debtBefore > _maxDebt; // unhealthy → lif = maxLif - require debtBefore <= collatValuePerMaxLif; // no badDebt - - uint256 denom = assert_uint256(WAD() - lifTimesLltv); - uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), denom); - - require _maxRepaid < debtBefore; // RCF actually constrains - - uint256 actualSeized; - uint256 actualRepaid; - actualSeized, actualRepaid = liquidate(e, obligation, collateralIndex, seizedAssets, repaidUnits, borrower, receiver, callback, data); - - require actualRepaid == _maxRepaid; // RCF cap hit - - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - - // Pin post-state — defeats prover artifacts where storage write→read link is lost. - require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); - require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); - - uint256 newCollatValueDown = CVL_mulDivDown(collatAfter, price, ORACLE_PRICE_SCALE()); - uint256 newMaxDebt = CVL_mulDivDown(newCollatValueDown, lltv, WAD()); - - // floor(price/OPS) propagated through lltv — only nonzero when price > OPS. - uint256 seizedAssetsRoundingError = CVL_mulDivDown(CVL_mulDivDown(1, price, ORACLE_PRICE_SCALE()), lltv, WAD()); +rule symbolicObligationHealthyAfterMaxRcfLiquidation(env e, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { + // Healthiness.spec-style obligation modeling: obligation is bound to global + // ghosts via equalsGlobalObligation, ghost values themselves are free — + // genuinely "symbolic over obligation" without exposing a free struct param + // to via_ir's per-call-site decode. Storage keys come from globalId, not a + // keccak of the symbolic struct. + require globalObligationCollateralLength == 1; - // Lower bound: position not far above health line (debt overshoot ≤ 2). - assert to_mathint(newMaxDebt) + 2 >= to_mathint(debtAfter), - "RCF: debt exceeds newMaxDebt by at most 2"; + Midnight.Obligation obligation = getGlobalObligation(); - // Upper bound: position not far below health line. - assert to_mathint(newMaxDebt) - to_mathint(debtAfter) - <= 2 + (to_mathint(actualRepaid) + to_mathint(WAD()) - 1) / to_mathint(WAD()) - + to_mathint(seizedAssetsRoundingError), - "RCF: newMaxDebt exceeds debt by bounded rounding only"; -} - -// Stripped-down version of healthyAfterRcfLiquidation. Pins post-state collat -// and debt slots via re-read + mathint require — forces SMT to constrain the -// storage that isHealthyNoBitmap subsequently reads, defeating the -// write→read link loss across liquidate seen in earlier CEXes. -rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; + uint256 lltv = globalObligationCollateralLLTV[0]; + uint256 maxLif = globalObligationCollateralMaxLif[0]; require maxLif >= WAD(); uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); require lifTimesLltv < WAD(); - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - bytes32 id = toId(e, obligation); + uint256 price = CVL_price(globalObligationCollateralOracle[0]); + bytes32 id = CVL_toId(obligation); // pinned to globalId by summaryToId uint256 collatBefore = collateral(id, borrower, 0); uint256 debtBefore = debtOf(id, borrower); - // Guards against degenerate/vacuous configurations: non-empty position, - // pre-maturity unhealthy (so lif = maxLif), valid RCF math. + // Pin liquidate's collateral-loop path to index 0. msb(bitmap) is a free + // ghost — without this, solver explores all 128 indices. + require collateralBitmap(id, borrower) == 1; + require CVL_msb(1) == 0; + require collatBefore > 0; - require e.block.timestamp < obligation.maturity; + require e.block.timestamp < globalObligationMaturity; - // No badDebt: debt covered by raw collateral value (pre-lif scaling). require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - // RCF max-repayment formula. uint256 _maxDebt = CVL_mulDivDown(CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); - require debtBefore > _maxDebt; // unhealthy → lif = maxLif and assert_uint256 below safe. + require debtBefore > _maxDebt; uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); uint256 actualSeized; @@ -501,95 +233,10 @@ rule healthyAfterMaxRcfLiquidation(env e, Midnight.Obligation obligation, uint25 require actualRepaid == _maxRepaid; - // Pin post-liquidate storage so isHealthyNoBitmap reads consistent values. uint256 collatAfter = collateral(id, borrower, 0); uint256 debtAfter = debtOf(id, borrower); - require to_mathint(collatAfter) == to_mathint(collatBefore) - to_mathint(actualSeized); - require to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(actualRepaid); + assert collatAfter == collatBefore - actualSeized; + assert debtAfter == debtBefore - actualRepaid; assert isHealthy(obligation, id, borrower); } - -// ============================================================================ -// Minimal reproducer rules — diagnose whether the storage write→read link -// across `liquidate` is preserved by the SMT. NO RCF math, no health check, -// no obligation pinning beyond length=1. If these CEX, the prover is failing -// to propagate the slot-write inside liquidate to the slot-read after. -// ============================================================================ - -// Workaround for CVL tuple-return bug: instead of capturing actualSeized/ -// actualRepaid from liquidate's return tuple (the second element gets bound -// incorrectly — confirmed via test/RcfReproTest.sol), discard the returns -// and derive both from storage delta. Forge test confirms storage updates -// are correct. -// -// Tests: in seizedAssets > 0 path, collat[0] decrements by exactly the -// user's seizedAssets input (contract does not modify it in this branch). -rule storageLinkSeizedPath(env e, Midnight.Obligation obligation, uint256 seizedAssets, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require debtBefore > 0; - require seizedAssets > 0; - - // Bitmap pins collat[0] as the only active collateral. Without this, - // the no-badDebt require below is vacuous (it bounds debt by a spec- - // local hypothetical, but contract's badDebt loop iterates only set - // bits, so with bitmap=0 the contract sees badDebt = full debt). - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; - - // No badDebt: with bitmap=1, contract's loop accumulates exactly the - // term below, so this require ⇔ contract's badDebt = 0. - require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - - _, _ = liquidate(e, obligation, 0, seizedAssets, 0, borrower, receiver, callback, data); - - uint256 collatAfter = collateral(id, borrower, 0); - - // Contract decrements collat[0] by user's seizedAssets exactly. - assert to_mathint(collatBefore) - to_mathint(collatAfter) == to_mathint(seizedAssets), - "collat decrement equals user's seizedAssets"; -} - -// Tests: in repaidUnits > 0 path, debt decrements by exactly the user's -// repaidUnits input (contract does not modify it in this branch). -rule storageLinkRepaidPath(env e, Midnight.Obligation obligation, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require obligation.collateralParams.length == 1; - - uint256 lltv = obligation.collateralParams[0].lltv; - uint256 maxLif = obligation.collateralParams[0].maxLif; - require maxLif >= WAD(); - uint256 price = CVL_price(obligation.collateralParams[0].oracle); - - bytes32 id = toId(e, obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - require collatBefore > 0; - require debtBefore > 0; - require repaidUnits > 0; - - // Bitmap pins collat[0] as active — same reason as in storageLinkSeizedPath. - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; - - require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - - _, _ = liquidate(e, obligation, 0, 0, repaidUnits, borrower, receiver, callback, data); - - uint256 debtAfter = debtOf(id, borrower); - - // Contract decrements debt by user's repaidUnits exactly (no badDebt → only one decrement). - assert to_mathint(debtBefore) - to_mathint(debtAfter) == to_mathint(repaidUnits), - "debt decrement equals user's repaidUnits"; -} From 13b646b624a1506ef9abcb6d2c7916a71fbe80a5 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 18 May 2026 10:04:05 +0200 Subject: [PATCH 11/16] symbolic obligations rule added --- .../confs/RCFUnhealthyAfterLiquidation.conf | 19 +- .../specs/RCFUnhealthyAfterLiquidation.spec | 347 +++++++++--------- 2 files changed, 177 insertions(+), 189 deletions(-) diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/RCFUnhealthyAfterLiquidation.conf index 89248f4ff..8bf2b3aa9 100644 --- a/certora/confs/RCFUnhealthyAfterLiquidation.conf +++ b/certora/confs/RCFUnhealthyAfterLiquidation.conf @@ -1,28 +1,23 @@ { "files": [ - "src/Midnight.sol", - "certora/helpers/FlashLiquidateCallback.sol", - "certora/helpers/Utils.sol" + "certora/helpers/MidnightWrapper.sol", + "certora/helpers/Havoc.sol" ], "parametric_contracts": [ - "Midnight" + "MidnightWrapper" ], - "verify": "Midnight:certora/specs/RCFUnhealthyAfterLiquidation.spec", + "verify": "MidnightWrapper:certora/specs/RCFUnhealthyAfterLiquidation.spec", "solc": "solc-0.8.34", - "solc_evm_version": "osaka", "solc_via_ir": true, + "solc_evm_version": "osaka", "optimistic_loop": true, "loop_iter": 2, "optimistic_hashing": true, "hashing_length_bound": 2048, "prover_args": [ "-depth 5", - "-mediumTimeout 20", - "-timeout 7200", - "-destructiveOptimizations twostage", - "-splitParallel true", - "-dontStopAtFirstSplitTimeout true", - "-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}]" + "-mediumTimeout 60", + "-timeout 3600" ], "msg": "RCF: Unhealthy After Liquidation" } diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index c7e0e7a33..b968a491d 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -1,55 +1,122 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// Proves that an RCF-limited liquidation (actualRepaid == maxRepaid) makes the -// position healthy. Uses exact mulDiv implementations (floor/ceiling arithmetic) -// because the proof requires lower bounds on mulDivUp — specifically that -// mulDivUp(a, WAD, denom) * denom >= a * WAD — which the relational axioms in -// Healthiness.spec do not provide. +import "BitmapSummaries.spec"; + +using Havoc as havocCallback; methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; - function _.price() external => CVL_price(calledContract) expect(uint256); - - // toId is summarized to a ghost-bound id (`globalId`) when the input matches - // the global obligation ghosts, else to a distinct id. Mirrors Healthiness.spec. - // Eliminates symbolic-keccak reasoning; storage keys become a free ghost - // scalar rather than a hash over the symbolic struct. - function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => summaryToId(obligation, chainId, midnight); - function touchObligation(Midnight.Obligation memory obligation) internal returns (bytes32) => CVL_toId(obligation); + 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. + * Under this assumption we can prove that a healthy borrower cannot get unhealthy by + * any action on the contract. + */ + 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 to simplify the verification task. + * Use a ghost function that ensures mulDivDown/Up behaves deterministically and + * add only the axioms about mulDiv that are needed to prove the desired property. + * 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 _.havocAll() external => HAVOC_ALL; + + function _.transferFrom(address from, address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); + function _.transfer(address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); + function _.onLiquidate(bytes32 id, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) external => genericCallbackBytes32() expect(bytes32); +} - function UtilsLib.msb(uint128 bitmap) internal returns (uint256) => CVL_msb(bitmap); - function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET; +/// SUMMARY /// - function UtilsLib.mulDivDown(uint256 a, uint256 b, uint256 d) internal returns (uint256) => CVL_mulDivDown(a, b, d); +definition WAD() returns uint256 = 10 ^ 18; - function UtilsLib.mulDivUp(uint256 a, uint256 b, uint256 d) internal returns (uint256) => CVL_mulDivUp(a, b, d); +definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; - function TickLib.tickToPrice(uint256) internal returns (uint256) => NONDET; - function TickLib.wExp(int256) internal returns (uint256) => NONDET; +persistent ghost summaryPrice(address) returns uint256; - function tradingFee(bytes32, uint256) internal returns (uint256) => NONDET; +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; + /* floor lower bound: mulDivDown(a, b, d) * d <= a * b */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => summaryMulDivDownM(a, b, d) * d <= a * b; + /* floor strictness: (mulDivDown(a, b, d) + 1) * d > a * b */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => (summaryMulDivDownM(a, b, d) + 1) * d > a * b; +} - 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; +persistent ghost summaryMulDivUpM(mathint, mathint, mathint) returns mathint { + /* ceil upper bound: mulDivUp(a, b, d) * d >= a * b */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => summaryMulDivUpM(a, b, d) * d >= a * b; + /* ceil strictness: (mulDivUp(a, b, d) - 1) * d < a * b (when result > 0) */ + axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && summaryMulDivUpM(a, b, d) > 0 => (summaryMulDivUpM(a, b, d) - 1) * d < a * b; +} - function _.onLiquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes) external => NONDET; - function UtilsLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET; +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 collateral(bytes32, address, uint256) external returns (uint128) envfree; - function debtOf(bytes32, address) external returns (uint256) envfree; - function collateralBitmap(bytes32, address) external returns (uint128) envfree; - function isHealthy(Midnight.Obligation, bytes32, address) external returns (bool) envfree; +function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { + bool overflow; + if (overflow || d == 0) { + revert(); + } + return require_uint256(summaryMulDivUpM(a, b, d)); } -// Ghost-bound id used by summaryToId. Free at rule entry; the summary pins -// matching-obligation calls to it and non-matching calls away from it. +// global variable to track whether the user was healthy before the callbacks. +ghost bool healthyBeforeCallback; + +// 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; -function summaryToId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 { +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 (equalsGlobalObligation(obligation) && midnight == currentContract) { + if (equalsGlobalMarket(market) && midnight == currentContract) { require id == globalId, "toId() is deterministic"; } else { require id != globalId, "toId() is injective"; @@ -57,186 +124,112 @@ function summaryToId(Midnight.Obligation obligation, uint256 chainId, address mi return id; } -// Legacy entry point retained for touchObligation summary. -function CVL_toId(Midnight.Obligation obligation) returns bytes32 { - return summaryToId(obligation, 0, currentContract); -} +// Summary for every callback (token transfer, onLiquidate, onFlashloan, onBuy, onSell) +// we check that the user is healthy before the callback, do some external call (to simulate changes by the callback), +// and then require that the user is still healthy after the callback. +function genericCallback() { + address dummy; + env e; + Midnight.Market globalMarket = getGlobalMarket(); -ghost CVL_msb(uint128) returns uint256; + // check that isHealthy holds before the callback. We remember any violation and check that none occurred at the end of each rule. + bool savedHealthyBefore = healthyBeforeCallback && isHealthyNoBitmap(globalMarket, globalId, globalBorrower); -persistent ghost CVL_price(address) returns uint256; + havocCallback.callHavoc(e, dummy); -// Tight relational mulDiv axioms — uniquely pin floor/ceil values, equivalent -// to exact mathint but typically faster for the SMT. -// Axioms proven in MulDiv.spec. -persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 { - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => ghostMulDivDown(a, b, d) * d <= a * b; - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => (ghostMulDivDown(a, b, d) + 1) * d > a * b; -} + // the callback havocs the global variable healthyBeforeCallback, so we restore the variable using the saved value in the local variable. + healthyBeforeCallback = savedHealthyBefore; -persistent ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256 { - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => ghostMulDivUp(a, b, d) * d >= a * b; - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && ghostMulDivUp(a, b, d) > 0 => (ghostMulDivUp(a, b, d) - 1) * d < a * b; + require isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "user is healthy after callback"; } -function CVL_mulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { - require d > 0; - return ghostMulDivDown(a, b, d); +// Same as the summary above except that it also returns a non-deterministic value. +function genericCallbackBool() returns (bool) { + bool result; + genericCallback(); + return result; } -function CVL_mulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { - require d > 0; - return ghostMulDivUp(a, b, d); +function genericCallbackBytes32() returns (bytes32) { + bytes32 result; + genericCallback(); + return result; } -definition WAD() returns uint256 = 10 ^ 18; +//// RULES ////// -definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; +// 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) { + healthyBeforeCallback = true; -persistent ghost address globalObligationLoanToken; + require globalMarketCollateralLength == 1, "single collateral asset"; -persistent ghost uint256 globalObligationCollateralLength; + Midnight.Market globalMarket = getGlobalMarket(); -persistent ghost mapping(uint256 => address) globalObligationCollateralOracle; + 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"; -persistent ghost mapping(uint256 => address) globalObligationCollateralToken; + uint256 price = summaryPrice(globalMarketCollateralOracle[0]); + uint256 collatBefore = collateral(globalId, globalBorrower, 0); + uint256 debtBefore = debtOf(globalId, globalBorrower); -persistent ghost mapping(uint256 => uint256) globalObligationCollateralLLTV; + require collatBefore > 0, "borrower has collateral to seize"; + require e.block.timestamp < globalMarketMaturity, "ensure RCF condition is activated"; -persistent ghost mapping(uint256 => uint256) globalObligationCollateralMaxLif; + uint256 maxDebt = summaryMulDivDown(summaryMulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); + require debtBefore > maxDebt, "position is unhealthy before liquidation"; -persistent ghost uint256 globalObligationMaturity; - -persistent ghost uint256 globalObligationRcfThreshold; - -persistent ghost address globalObligationEnterGate; - -persistent ghost address globalObligationLiquidatorGate; - -definition collateralMatches(Midnight.Obligation obligation, uint256 index) returns bool = - (index < globalObligationCollateralLength - => obligation.collateralParams[index].oracle == globalObligationCollateralOracle[index] - && obligation.collateralParams[index].token == globalObligationCollateralToken[index] - && obligation.collateralParams[index].lltv == globalObligationCollateralLLTV[index] - && obligation.collateralParams[index].maxLif == globalObligationCollateralMaxLif[index]); - -function equalsGlobalObligation(Midnight.Obligation obligation) returns (bool) { - return obligation.loanToken == globalObligationLoanToken - && obligation.collateralParams.length == globalObligationCollateralLength - && collateralMatches(obligation, 0) - && collateralMatches(obligation, 1) - && collateralMatches(obligation, 2) - && obligation.maturity == globalObligationMaturity - && obligation.rcfThreshold == globalObligationRcfThreshold - && obligation.enterGate == globalObligationEnterGate - && obligation.liquidatorGate == globalObligationLiquidatorGate; -} - -function getGlobalObligation() returns (Midnight.Obligation) { - Midnight.Obligation obligation; - require equalsGlobalObligation(obligation), "get global obligation"; - return obligation; -} - -rule concreteObligationHealthyAfterMaxRcfLiquidation(env e, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - require globalObligationLoanToken == 0x0000000000000000000000000000000000001001; - require globalObligationCollateralLength == 1; - require globalObligationCollateralOracle[0] == 0x0000000000000000000000000000000000001003; - require globalObligationCollateralToken[0] == 0x0000000000000000000000000000000000001002; - require globalObligationCollateralLLTV[0] == 770000000000000000; - require globalObligationCollateralMaxLif[0] == 1061007957559681697; - require globalObligationMaturity == 2000000000; - require globalObligationRcfThreshold == 0; - require globalObligationEnterGate == 0; - require globalObligationLiquidatorGate == 0; - require callback == 0; - - Midnight.Obligation obligation = getGlobalObligation(); - - uint256 lltv = globalObligationCollateralLLTV[0]; - uint256 maxLif = globalObligationCollateralMaxLif[0]; - require maxLif >= WAD(); - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(); - - uint256 price = CVL_price(globalObligationCollateralOracle[0]); - bytes32 id = CVL_toId(obligation); - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); - - // Guards against degenerate/vacuous configurations: non-empty position, - // pre-maturity unhealthy (so lif = maxLif), valid RCF math. - require collatBefore > 0; - require e.block.timestamp < obligation.maturity; - - // No badDebt: debt covered by raw collateral value (pre-lif scaling). - require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); - - // RCF max-repayment formula. - uint256 _maxDebt = CVL_mulDivDown(CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); - require debtBefore > _maxDebt; - uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); + uint256 rcfCap = summaryMulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); + require repaidUnits >= rcfCap, "caller asks to repay at least the RCF cap"; uint256 actualSeized; uint256 actualRepaid; - actualSeized, actualRepaid = liquidate(e, obligation, 0, seizedAssets, repaidUnits, borrower, receiver, callback, data); - - require actualRepaid == _maxRepaid; - // Pin post-liquidate storage so isHealthy reads consistent values. - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - assert collatAfter == collatBefore - actualSeized; - assert debtAfter == debtBefore - actualRepaid; + actualSeized, actualRepaid = liquidate(e, globalMarket, 0, seizedAssets, repaidUnits, globalBorrower, receiver, callbackAddr, data); - assert isHealthy(obligation, id, borrower); + require actualRepaid == rcfCap, "liquidate clamps to RCF cap"; + assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower); } -rule symbolicObligationHealthyAfterMaxRcfLiquidation(env e, uint256 seizedAssets, uint256 repaidUnits, address borrower, address receiver, address callback, bytes data) { - // Healthiness.spec-style obligation modeling: obligation is bound to global - // ghosts via equalsGlobalObligation, ghost values themselves are free — - // genuinely "symbolic over obligation" without exposing a free struct param - // to via_ir's per-call-site decode. Storage keys come from globalId, not a - // keccak of the symbolic struct. - require globalObligationCollateralLength == 1; +// 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) { + healthyBeforeCallback = true; - Midnight.Obligation obligation = getGlobalObligation(); + require globalMarketCollateralLength <= 2, "too many collateralParams for the spec to handle"; - uint256 lltv = globalObligationCollateralLLTV[0]; - uint256 maxLif = globalObligationCollateralMaxLif[0]; - require maxLif >= WAD(); - uint256 lifTimesLltv = CVL_mulDivUp(maxLif, lltv, WAD()); - require lifTimesLltv < WAD(); + uint256 collateralIndex; + require collateralIndex < globalMarketCollateralLength, "invalid collateral index"; - uint256 price = CVL_price(globalObligationCollateralOracle[0]); - bytes32 id = CVL_toId(obligation); // pinned to globalId by summaryToId - uint256 collatBefore = collateral(id, borrower, 0); - uint256 debtBefore = debtOf(id, borrower); + Midnight.Market globalMarket = getGlobalMarket(); - // Pin liquidate's collateral-loop path to index 0. msb(bitmap) is a free - // ghost — without this, solver explores all 128 indices. - require collateralBitmap(id, borrower) == 1; - require CVL_msb(1) == 0; + 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"; - require collatBefore > 0; - require e.block.timestamp < globalObligationMaturity; + uint256 price = summaryPrice(globalMarketCollateralOracle[collateralIndex]); + uint256 collatBefore = collateral(globalId, globalBorrower, collateralIndex); + uint256 debtBefore = debtOf(globalId, globalBorrower); - require debtBefore <= CVL_mulDivUp(CVL_mulDivUp(collatBefore, price, ORACLE_PRICE_SCALE()), WAD(), maxLif); + require collatBefore > 0, "borrower has collateral to seize"; + require e.block.timestamp < globalMarketMaturity, "ensure RCF condition is activated"; - uint256 _maxDebt = CVL_mulDivDown(CVL_mulDivDown(collatBefore, price, ORACLE_PRICE_SCALE()), lltv, WAD()); - require debtBefore > _maxDebt; - uint256 _maxRepaid = CVL_mulDivUp(assert_uint256(debtBefore - _maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); + 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, obligation, 0, seizedAssets, repaidUnits, borrower, receiver, callback, data); - require actualRepaid == _maxRepaid; + actualSeized, actualRepaid = liquidate(e, globalMarket, collateralIndex, seizedAssets, repaidUnits, globalBorrower, receiver, callbackAddr, data); - uint256 collatAfter = collateral(id, borrower, 0); - uint256 debtAfter = debtOf(id, borrower); - assert collatAfter == collatBefore - actualSeized; - assert debtAfter == debtBefore - actualRepaid; + require actualRepaid == summaryMulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)), "actualRepaid equals the RCF cap = (debt - maxDebt) / (1 - maxLif * lltv)"; - assert isHealthy(obligation, id, borrower); + assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower); } From c30f61050688b1007124d259939c1f1730e7494c Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 18 May 2026 11:51:37 +0200 Subject: [PATCH 12/16] nondet callbakc summaries --- .../confs/RCFUnhealthyAfterLiquidation.conf | 3 +- .../specs/RCFUnhealthyAfterLiquidation.spec | 62 +++---------------- 2 files changed, 8 insertions(+), 57 deletions(-) diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/RCFUnhealthyAfterLiquidation.conf index 8bf2b3aa9..cb84c28de 100644 --- a/certora/confs/RCFUnhealthyAfterLiquidation.conf +++ b/certora/confs/RCFUnhealthyAfterLiquidation.conf @@ -1,7 +1,6 @@ { "files": [ - "certora/helpers/MidnightWrapper.sol", - "certora/helpers/Havoc.sol" + "certora/helpers/MidnightWrapper.sol" ], "parametric_contracts": [ "MidnightWrapper" diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index b968a491d..5fe8adabb 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -2,8 +2,6 @@ import "BitmapSummaries.spec"; -using Havoc as havocCallback; - methods { function multicall(bytes[]) external => HAVOC_ALL DELETE; @@ -11,25 +9,19 @@ methods { 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. - * Under this assumption we can prove that a healthy borrower cannot get unhealthy by - * any action on the contract. - */ + /* 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 to simplify the verification task. - * Use a ghost function that ensures mulDivDown/Up behaves deterministically and - * add only the axioms about mulDiv that are needed to prove the desired property. - * The axioms are proved in MulDiv.spec. + /* 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 _.havocAll() external => HAVOC_ALL; - function _.transferFrom(address from, address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); - function _.transfer(address to, uint256 amount) external with(env e) => genericCallbackBool() expect(bool); - function _.onLiquidate(bytes32 id, Midnight.Market market, uint256 collateralIndex, uint256 seizedAssets, uint256 repaidUnits, address borrower, bytes data) external => genericCallbackBytes32() expect(bytes32); + 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 /// @@ -72,9 +64,6 @@ function summaryMulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 { return require_uint256(summaryMulDivUpM(a, b, d)); } -// global variable to track whether the user was healthy before the callbacks. -ghost bool healthyBeforeCallback; - // global variable to track which market and borrower we're testing. persistent ghost address globalMarketLoanToken; @@ -124,45 +113,11 @@ function summaryToId(Midnight.Market market, uint256 chainId, address midnight) return id; } -// Summary for every callback (token transfer, onLiquidate, onFlashloan, onBuy, onSell) -// we check that the user is healthy before the callback, do some external call (to simulate changes by the callback), -// and then require that the user is still healthy after the callback. -function genericCallback() { - address dummy; - env e; - Midnight.Market globalMarket = getGlobalMarket(); - - // check that isHealthy holds before the callback. We remember any violation and check that none occurred at the end of each rule. - bool savedHealthyBefore = healthyBeforeCallback && isHealthyNoBitmap(globalMarket, globalId, globalBorrower); - - havocCallback.callHavoc(e, dummy); - - // the callback havocs the global variable healthyBeforeCallback, so we restore the variable using the saved value in the local variable. - healthyBeforeCallback = savedHealthyBefore; - - require isHealthyNoBitmap(globalMarket, globalId, globalBorrower), "user is healthy after callback"; -} - -// Same as the summary above except that it also returns a non-deterministic value. -function genericCallbackBool() returns (bool) { - bool result; - genericCallback(); - return result; -} - -function genericCallbackBytes32() returns (bytes32) { - bytes32 result; - genericCallback(); - return result; -} - //// RULES ////// // 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) { - healthyBeforeCallback = true; - require globalMarketCollateralLength == 1, "single collateral asset"; Midnight.Market globalMarket = getGlobalMarket(); @@ -184,14 +139,13 @@ rule healthyAfterMaxRcfLiquidationSingleCollateral(env e, uint256 seizedAssets, require debtBefore > maxDebt, "position is unhealthy before liquidation"; uint256 rcfCap = summaryMulDivUp(assert_uint256(debtBefore - maxDebt), WAD(), assert_uint256(WAD() - lifTimesLltv)); - require repaidUnits >= rcfCap, "caller asks to repay at least the RCF cap"; uint256 actualSeized; uint256 actualRepaid; actualSeized, actualRepaid = liquidate(e, globalMarket, 0, seizedAssets, repaidUnits, globalBorrower, receiver, callbackAddr, data); - require actualRepaid == rcfCap, "liquidate clamps to RCF cap"; + require actualRepaid == rcfCap, "max allowed to be repaid by RCF condition is repaid"; assert isHealthyNoBitmap(globalMarket, globalId, globalBorrower); } @@ -199,8 +153,6 @@ rule healthyAfterMaxRcfLiquidationSingleCollateral(env e, uint256 seizedAssets, // 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) { - healthyBeforeCallback = true; - require globalMarketCollateralLength <= 2, "too many collateralParams for the spec to handle"; uint256 collateralIndex; From 2777b74df9b5f07d0637dda22e2b932328ab349c Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 18 May 2026 13:56:44 +0200 Subject: [PATCH 13/16] added concrete rule --- .../specs/RCFUnhealthyAfterLiquidation.spec | 86 ++++++++++++++++--- 1 file changed, 76 insertions(+), 10 deletions(-) diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/RCFUnhealthyAfterLiquidation.spec index 5fe8adabb..cf60eaa12 100644 --- a/certora/specs/RCFUnhealthyAfterLiquidation.spec +++ b/certora/specs/RCFUnhealthyAfterLiquidation.spec @@ -35,18 +35,27 @@ 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; - /* floor lower bound: mulDivDown(a, b, d) * d <= a * b */ - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => summaryMulDivDownM(a, b, d) * d <= a * b; - /* floor strictness: (mulDivDown(a, b, d) + 1) * d > a * b */ - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => (summaryMulDivDownM(a, b, d) + 1) * d > a * b; } -persistent ghost summaryMulDivUpM(mathint, mathint, mathint) returns mathint { - /* ceil upper bound: mulDivUp(a, b, d) * d >= a * b */ - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => summaryMulDivUpM(a, b, d) * d >= a * b; - /* ceil strictness: (mulDivUp(a, b, d) - 1) * d < a * b (when result > 0) */ - axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 && summaryMulDivUpM(a, b, d) > 0 => (summaryMulDivUpM(a, b, d) - 1) * d < a * b; -} +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; @@ -115,9 +124,62 @@ function summaryToId(Midnight.Market market, uint256 chainId, address midnight) //// 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(); @@ -153,6 +215,10 @@ rule healthyAfterMaxRcfLiquidationSingleCollateral(env e, uint256 seizedAssets, // 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; From 59290ed7336e07bb20b1c95e17c595f46ae6cdee Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 18 May 2026 13:59:17 +0200 Subject: [PATCH 14/16] renamed spec --- ...FUnhealthyAfterLiquidation.conf => HealthyAfterRCFLiquidation} | 0 ...FUnhealthyAfterLiquidation.spec => HealthyAfterRCFLiquidation} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename certora/confs/{RCFUnhealthyAfterLiquidation.conf => HealthyAfterRCFLiquidation} (100%) rename certora/specs/{RCFUnhealthyAfterLiquidation.spec => HealthyAfterRCFLiquidation} (100%) diff --git a/certora/confs/RCFUnhealthyAfterLiquidation.conf b/certora/confs/HealthyAfterRCFLiquidation similarity index 100% rename from certora/confs/RCFUnhealthyAfterLiquidation.conf rename to certora/confs/HealthyAfterRCFLiquidation diff --git a/certora/specs/RCFUnhealthyAfterLiquidation.spec b/certora/specs/HealthyAfterRCFLiquidation similarity index 100% rename from certora/specs/RCFUnhealthyAfterLiquidation.spec rename to certora/specs/HealthyAfterRCFLiquidation From c381165ac8226dc58eed9aa5aeabe5f220a5a07f Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 18 May 2026 14:00:58 +0200 Subject: [PATCH 15/16] renamed spec --- ...HealthyAfterRCFLiquidation => HealthyAfterRCFLiquidation.conf} | 0 ...HealthyAfterRCFLiquidation => HealthyAfterRCFLiquidation.spec} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename certora/confs/{HealthyAfterRCFLiquidation => HealthyAfterRCFLiquidation.conf} (100%) rename certora/specs/{HealthyAfterRCFLiquidation => HealthyAfterRCFLiquidation.spec} (100%) diff --git a/certora/confs/HealthyAfterRCFLiquidation b/certora/confs/HealthyAfterRCFLiquidation.conf similarity index 100% rename from certora/confs/HealthyAfterRCFLiquidation rename to certora/confs/HealthyAfterRCFLiquidation.conf diff --git a/certora/specs/HealthyAfterRCFLiquidation b/certora/specs/HealthyAfterRCFLiquidation.spec similarity index 100% rename from certora/specs/HealthyAfterRCFLiquidation rename to certora/specs/HealthyAfterRCFLiquidation.spec From bcd93468d011fe37cf679c9897a60afe37005d35 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Mon, 18 May 2026 14:01:26 +0200 Subject: [PATCH 16/16] changed spec referred --- certora/confs/HealthyAfterRCFLiquidation.conf | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/certora/confs/HealthyAfterRCFLiquidation.conf b/certora/confs/HealthyAfterRCFLiquidation.conf index cb84c28de..e8820e388 100644 --- a/certora/confs/HealthyAfterRCFLiquidation.conf +++ b/certora/confs/HealthyAfterRCFLiquidation.conf @@ -5,7 +5,7 @@ "parametric_contracts": [ "MidnightWrapper" ], - "verify": "MidnightWrapper:certora/specs/RCFUnhealthyAfterLiquidation.spec", + "verify": "MidnightWrapper:certora/specs/HealthyAfterRCFLiquidation.spec", "solc": "solc-0.8.34", "solc_via_ir": true, "solc_evm_version": "osaka", @@ -13,10 +13,11 @@ "loop_iter": 2, "optimistic_hashing": true, "hashing_length_bound": 2048, + "smt_timeout": 7200, "prover_args": [ - "-depth 5", - "-mediumTimeout 60", - "-timeout 3600" + "-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" }