Skip to content

Changes from my Code Review. #1017

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jhoenicke wants to merge 5 commits into
base: certora/liquidationLiveness
Choose a base branch
from
+33 −25
Open

Changes from my Code Review. #1017

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e719780
Replace require->assert for recovery >= maxDebtContrib
jhoenicke Jun 23, 2026
4877102
Replaced some require with assert.
jhoenicke Jun 23, 2026
9e0d041
reverted one require/assert change
jhoenicke Jun 23, 2026
f00014c
Lint definitions
jhoenicke Jun 23, 2026
fb17b6e
Replace one require with assert.
jhoenicke Jun 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 33 additions & 25 deletions certora/specs/LiquidateLiveness.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,12 @@ definition WAD() returns uint256 = 10 ^ 18;

definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36;

definition getPrice(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = collateralIndex == 0 ? ghostPrice(params[0].oracle) : collateralIndex == 1 ? ghostPrice(params[1].oracle) : ghostPrice(params[2].oracle);

definition getLltv(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = collateralIndex == 0 ? params[0].lltv : collateralIndex == 1 ? params[1].lltv : params[2].lltv;

definition getMaxLif(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = collateralIndex == 0 ? params[0].maxLif : collateralIndex == 1 ? params[1].maxLif : params[2].maxLif;

// Assume the market is already created.
function summaryToId(Midnight.Market market) returns bytes32 {
return Utils.hashMarket(market);
Expand Down Expand Up @@ -151,7 +157,7 @@ function seizablePreamble(env e, Midnight.Market market, bytes32 id, address bor
threeCollatSetup(e, market, id, borrower);
require collateralIndex == 0 || collateralIndex == 1 || collateralIndex == 2, "seized index in {0,1,2} (<= loop_iter)";
require summaryGetBit(collateralBitmap(id, borrower), collateralIndex), "the seized collateral is active";
require (collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle)) > 0, "the seized collateral is priced (LIVENESS)";
require getPrice(collateralIndex, market.collateralParams) > 0, "the seized collateral is priced (LIVENESS)";
}

/// maxDebt = sum over all collaterals of collat * price * lltv (down-rounded).
Expand Down Expand Up @@ -194,17 +200,17 @@ function lowLltvScaffolding(Midnight.Market market, bytes32 id, address borrower
uint128 collat2 = collateral(id, borrower, 2);

// recovery_i >= maxDebtContrib_i for every collateral
require ghostMulDivUp(ghostMulDivUp(collat0, price0, ORACLE_PRICE_SCALE()), WAD(), maxLif0) >= ghostMulDivDown(ghostMulDivDown(collat0, price0, ORACLE_PRICE_SCALE()), lltv0, WAD()), "recovery0 >= maxDebtContrib0 (any valid collateral, incl. inactive)";
require ghostMulDivUp(ghostMulDivUp(collat1, price1, ORACLE_PRICE_SCALE()), WAD(), maxLif1) >= ghostMulDivDown(ghostMulDivDown(collat1, price1, ORACLE_PRICE_SCALE()), lltv1, WAD()), "recovery1 >= maxDebtContrib1 (any valid collateral, incl. inactive)";
require ghostMulDivUp(ghostMulDivUp(collat2, price2, ORACLE_PRICE_SCALE()), WAD(), maxLif2) >= ghostMulDivDown(ghostMulDivDown(collat2, price2, ORACLE_PRICE_SCALE()), lltv2, WAD()), "recovery2 >= maxDebtContrib2 (any valid collateral, incl. inactive)";
assert ghostMulDivUp(ghostMulDivUp(collat0, price0, ORACLE_PRICE_SCALE()), WAD(), maxLif0) >= ghostMulDivDown(ghostMulDivDown(collat0, price0, ORACLE_PRICE_SCALE()), lltv0, WAD()), "recovery0 >= maxDebtContrib0 (any valid collateral, incl. inactive)";
assert ghostMulDivUp(ghostMulDivUp(collat1, price1, ORACLE_PRICE_SCALE()), WAD(), maxLif1) >= ghostMulDivDown(ghostMulDivDown(collat1, price1, ORACLE_PRICE_SCALE()), lltv1, WAD()), "recovery1 >= maxDebtContrib1 (any valid collateral, incl. inactive)";
assert ghostMulDivUp(ghostMulDivUp(collat2, price2, ORACLE_PRICE_SCALE()), WAD(), maxLif2) >= ghostMulDivDown(ghostMulDivDown(collat2, price2, ORACLE_PRICE_SCALE()), lltv2, WAD()), "recovery2 >= maxDebtContrib2 (any valid collateral, incl. inactive)";

// Seized collateral: ExactMath denominator bound (=> WAD*WAD - maxLif*lltv >= WAD >= 1) and strict
// recovery > maxDebtContrib (=> debtAfter > maxDebt, so maxRepaid >= 1; needs collatJ*priceJ >= ORACLE_PRICE_SCALE).
uint256 lltvJ = collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv;
uint256 maxLifJ = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif;
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 lltvJ = getLltv(collateralIndex, market.collateralParams);
uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint128 collatJ = collateral(id, borrower, collateralIndex);
require maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1";
assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1";
require ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)";
}

Expand All @@ -216,11 +222,11 @@ rule unhealthyLltvFullLiquidatableForAnySafeAmount(env e, Midnight.Market market
bytes32 id = summaryToId(market);
seizablePreamble(e, market, id, borrower, collateralIndex);

uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif;
require (collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)";
uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams);
require getLltv(collateralIndex, market.collateralParams) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)";

uint128 collatJ = collateral(id, borrower, collateralIndex);
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint256 _debt = debtOf(id, borrower);
mathint debtAfter = debtAfterBadDebt(market, id, borrower);
require _debt > maxDebtSum(market, id, borrower), "unhealthy: debt > maxDebt";
Expand All @@ -240,12 +246,12 @@ rule unhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market market,
bytes32 id = summaryToId(market);
seizablePreamble(e, market, id, borrower, collateralIndex);

uint256 lltv = collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv;
uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif;
uint256 lltv = getLltv(collateralIndex, market.collateralParams);
uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams);
require lltv < WAD(), "lltv < WAD partition";

uint128 collatJ = collateral(id, borrower, collateralIndex);
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint256 _debt = debtOf(id, borrower);
mathint maxDebt = maxDebtSum(market, id, borrower);
mathint debtAfter = debtAfterBadDebt(market, id, borrower);
Expand All @@ -256,6 +262,7 @@ rule unhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market market,
// maxRepaid (RCF check) = mulDivUp(debtAfter - maxDebt, WAD*WAD, WAD*WAD - lif*lltv), lif = maxLif here.
// Reconstructed bit-for-bit so the bound matches the RCF check exactly; denominator > 0 and debtAfter >= maxDebt from lowLltvScaffolding.
mathint maxRepaid = ghostMulDivUp(assert_uint256(debtAfter - maxDebt), assert_uint256(WAD() * WAD()), assert_uint256(WAD() * WAD() - maxLif * lltv));
assert maxRepaid > 0, "it's possible to repay at least one unit";

@chatgpt-codex-connector chatgpt-codex-connector Bot Jun 23, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Prove a concrete safe amount, not just a positive cap

This assertion does not actually prevent the low-LLTV repay rule from becoming vacuous for the later requires: maxRepaid > 0 can hold while every positive repaidUnits is pruned by the collateral-fit guard. For example, with one active collateral unit priced below ORACLE_PRICE_SCALE, maxRepaid can be positive, but repaidUnits = 1 computes more seized collateral than the borrower has, so all paths are eliminated after this point. If the intent is to prove the safe interval is non-empty, add a satisfy/sanity check or assert a concrete amount also satisfies the debt and collateral guards.

Useful? React with 👍 / 👎.


require repaidUnits > 0;
require repaidUnits <= maxRepaid, "RCF check passes";
Expand All @@ -276,9 +283,9 @@ rule postMaturityLiquidatableForAnySafeAmount(env e, Midnight.Market market, add

require e.block.timestamp > market.maturity, "post-maturity partition (liquidatable by expiry)";

uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif;
uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams);
uint128 collatJ = collateral(id, borrower, collateralIndex);
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint256 _debt = debtOf(id, borrower);
mathint debtAfter = debtAfterBadDebt(market, id, borrower);

Expand All @@ -292,19 +299,19 @@ rule postMaturityLiquidatableForAnySafeAmount(env e, Midnight.Market market, add
assert debtOf(id, borrower) < _debt;
}

/// SEIZE PATH (seizedAssets > 0, repaidUnits = 0): contract derives repaidUnits = mulDivUp(mulDivUp(seizedAssets, price0, ORACLE_PRICE_SCALE), WAD, lif).
/// Collateral guard is a direct `seizedAssets <= collateral[0]`; debt-underflow / RCF apply to the derived repaidUnits, which is >= 1 (seizedAssets > 0, price0 > 0) so progress holds.
/// SEIZE PATH (seizedAssets > 0, repaidUnits = 0): contract derives repaidUnits = mulDivUp(mulDivUp(seizedAssets, price, ORACLE_PRICE_SCALE), WAD, lif).
/// Collateral guard is a direct `seizedAssets <= collateral`; debt-underflow / RCF apply to the derived repaidUnits, which is >= 1 (seizedAssets > 0, price > 0) so progress holds.

/// Seize path, unhealthy, lltv == WAD: maxRepaid = uint256.max (RCF auto-passes), lif = maxLif.
rule seizeUnhealthyLltvFullLiquidatableForAnySafeAmount(env e, Midnight.Market market, address borrower, address receiver, uint256 collateralIndex, uint256 seizedAssets) {
bytes32 id = summaryToId(market);
seizablePreamble(e, market, id, borrower, collateralIndex);

uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif;
require (collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)";
uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams);
require getLltv(collateralIndex, market.collateralParams) == WAD(), "lltv == WAD partition (maxRepaid = uint256.max)";

uint128 collatJ = collateral(id, borrower, collateralIndex);
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint256 _debt = debtOf(id, borrower);
mathint debtAfter = debtAfterBadDebt(market, id, borrower);
require _debt > maxDebtSum(market, id, borrower), "unhealthy: debt > maxDebt";
Expand All @@ -326,12 +333,12 @@ rule seizeUnhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market ma
bytes32 id = summaryToId(market);
seizablePreamble(e, market, id, borrower, collateralIndex);

uint256 lltv = collateralIndex == 0 ? market.collateralParams[0].lltv : collateralIndex == 1 ? market.collateralParams[1].lltv : market.collateralParams[2].lltv;
uint256 maxLif = collateralIndex == 0 ? market.collateralParams[0].maxLif : collateralIndex == 1 ? market.collateralParams[1].maxLif : market.collateralParams[2].maxLif;
uint256 lltv = getLltv(collateralIndex, market.collateralParams);
uint256 maxLif = getMaxLif(collateralIndex, market.collateralParams);
require lltv < WAD(), "lltv < WAD partition";

uint128 collatJ = collateral(id, borrower, collateralIndex);
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint256 _debt = debtOf(id, borrower);
mathint maxDebt = maxDebtSum(market, id, borrower);
mathint debtAfter = debtAfterBadDebt(market, id, borrower);
Expand All @@ -342,6 +349,7 @@ rule seizeUnhealthyLowLltvLiquidatableForAnySafeAmount(env e, Midnight.Market ma
// maxRepaid (RCF check) = mulDivUp(debtAfter - maxDebt, WAD*WAD, WAD*WAD - lif*lltv),
// lif = maxLif here. Reconstructed bit-for-bit so the bound matches the contract's RCF check exactly.
mathint maxRepaid = ghostMulDivUp(assert_uint256(debtAfter - maxDebt), assert_uint256(WAD() * WAD()), assert_uint256(WAD() * WAD() - maxLif * lltv));
assert maxRepaid > 0, "it's possible to repay at least one unit";

mathint repaidUnits = ghostMulDivUp(ghostMulDivUp(seizedAssets, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLif);

Expand All @@ -365,7 +373,7 @@ rule seizePostMaturityLiquidatableForAnySafeAmount(env e, Midnight.Market market
require e.block.timestamp > market.maturity, "post-maturity partition (liquidatable by expiry)";

uint128 collatJ = collateral(id, borrower, collateralIndex);
uint256 priceJ = collateralIndex == 0 ? ghostPrice(market.collateralParams[0].oracle) : collateralIndex == 1 ? ghostPrice(market.collateralParams[1].oracle) : ghostPrice(market.collateralParams[2].oracle);
uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
uint256 _debt = debtOf(id, borrower);
mathint debtAfter = debtAfterBadDebt(market, id, borrower);

Expand Down