modular lif by MathisGD · Pull Request #992 · morpho-org/midnight

MathisGD · 2026-06-16T14:03:31Z

modularize liquidation cursors.

Rebased PR #992 on current main and resolved conflicts with the continuousFeeCap changes. Conflict resolution: combined liquidationCursor with continuousFeeCap in EIP-712 hashes and regenerated the frontend signature fixture.

Co-authored-by: prd-carapulse[bot] <264278285+prd-carapulse[bot]@users.noreply.github.com>

Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: e55adcd989

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-06-23T09:30:51Z

+    // maxLif is recomputed on the fly from (lltv, liquidationCursor) during liquidate. Summarize it by a deterministic ghost: its
+    // value bounds are assumed below (see ExactMath.spec), and its own well-definedness (no division by zero for valid
+    // liquidationCursors) is proven there too.
+    function maxLif(uint256 lltv, uint256 liquidationCursor) internal returns (uint256) => maxLifGhost(lltv, liquidationCursor);


Do not hide maxLif divisions in no-div proof

This summary removes the body of maxLif from the rule that is supposed to catch zero denominators in mulDivDown/mulDivUp, but maxLif itself now computes a denominator from (lltv, liquidationCursor); for example lltv == 0 and liquidationCursor == WAD reaches a zero denominator. Because ExactMath.spec calls maxLif plainly rather than with @withrevert, that reverting boundary is pruned rather than proving well-definedness, so this rule can pass while missing the new division site. Either keep maxLif unsummarized here or add a dedicated @withrevert well-definedness rule/precondition for the boundary.

Useful? React with 👍 / 👎.

This only happens with those exact values: lltv == 0 and liquidationCursor == WAD.

I think it's ok because it would revert at market creation, and never after.

Still, it may be simpler to require that liquidationCursor < WAD, instead of liquidationCursor <= WAD

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1d673ac0d9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-06-23T13:18:33Z

 function summaryToId(Midnight.Market market) returns (bytes32) {
    require forall uint256 i. i < market.collateralParams.length => market.collateralParams[i].lltv <= WAD(), "proven in CreatedMarkets.spec";
-    require forall uint256 i. i < market.collateralParams.length => market.collateralParams[i].maxLif >= WAD() && market.collateralParams[i].maxLif <= 2 * WAD(), "proven in ExactMath.spec";
+    require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "proven in ExactMath.spec";


Restore the missing maxLif upper-bound proof

This precondition now assumes maxLifGhost <= 2 * WAD() as "proven in ExactMath.spec", but this commit removed maxLifIsAtMostTwoWad and a repo-wide search only finds that rule name in these comments. Because maxLif is summarized by an unconstrained ghost here, the overflow proof can silently rely on an unproved bound; restore a maxLif <= 2 * WAD rule for the valid (lltv, liquidationCursor) domain or cite/use the CreatedMarkets invariant for created markets instead.

Useful? React with 👍 / 👎.

Suggested change

require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "proven in ExactMath.spec";

require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "see maxLifIsAtLeastWad and createdMarketsHaveMaxLifAtMostTwoWad";

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2662223a74

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

adhusson · 2026-06-24T15:03:17Z

                require(isLltvEnabled[lltv], LltvNotEnabled());
                require(isLiquidationCursorEnabled[liquidationCursor], LiquidationCursorNotEnabled());
                require(maxLif(lltv, liquidationCursor) <= 2 * WAD, InvalidMaxLif());
+                require(lltv == WAD || lltv * maxLif(lltv, liquidationCursor) <= 0.999 ether * WAD, MaxLifTooHigh());


reuse maxLif computation?

QGarchery

see #1026

QGarchery · 2026-06-24T15:46:50Z

+    // maxLif is recomputed on the fly from (lltv, liquidationCursor) during liquidate. Summarize it by a deterministic ghost so
+    // its (bounded) value can be assumed under a quantifier; its own arithmetic is safe and bounded for valid liquidationCursors
+    // (see ExactMath.spec: maxLifIsAtLeastWad, maxLifIsAtMostTwoWad).


Suggested change

// maxLif is recomputed on the fly from (lltv, liquidationCursor) during liquidate. Summarize it by a deterministic ghost so

// its (bounded) value can be assumed under a quantifier; its own arithmetic is safe and bounded for valid liquidationCursors

// (see ExactMath.spec: maxLifIsAtLeastWad, maxLifIsAtMostTwoWad).

// Summarize maxLif by a deterministic ghost so its value can be assumed under a quantifier.

because the bound can be stated below (see next point in this review)

QGarchery · 2026-06-24T15:47:15Z

 function summaryToId(Midnight.Market market) returns (bytes32) {
    require forall uint256 i. i < market.collateralParams.length => market.collateralParams[i].lltv <= WAD(), "proven in CreatedMarkets.spec";
-    require forall uint256 i. i < market.collateralParams.length => market.collateralParams[i].maxLif >= WAD() && market.collateralParams[i].maxLif <= 2 * WAD(), "proven in ExactMath.spec";
+    require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "proven in ExactMath.spec";


Suggested change

require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "proven in ExactMath.spec";

require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "see maxLifIsAtLeastWad and createdMarketsHaveMaxLifAtMostTwoWad";

MathisGD self-assigned this Jun 16, 2026

MathisGD commented Jun 19, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

feat: modular lif

a5c54ea

Rebased PR #992 on current main and resolved conflicts with the continuousFeeCap changes. Conflict resolution: combined liquidationCursor with continuousFeeCap in EIP-712 hashes and regenerated the frontend signature fixture.

prd-carapulse Bot force-pushed the modular-lif branch from d1b23b6 to a5c54ea Compare June 20, 2026 08:38

prd-carapulse Bot mentioned this pull request Jun 21, 2026

fix(certora): cheapen CreatedMarkets max LIF invariant #1002

Merged

4 tasks

MathisGD mentioned this pull request Jun 22, 2026

modular lltvs #993

Merged

prd-carapulse Bot and others added 2 commits June 22, 2026 13:43

fix(certora): cheapen CreatedMarkets max LIF invariant (#1002)

c417b28

Co-authored-by: prd-carapulse[bot] <264278285+prd-carapulse[bot]@users.noreply.github.com>

Merge remote-tracking branch 'origin' into modular-lif

e4807b0

MathisGD commented Jun 22, 2026

View reviewed changes

Comment thread certora/specs/CreatedMarkets.spec Outdated

MathisGD commented Jun 22, 2026

View reviewed changes

Comment thread certora/specs/CreatedMarkets.spec Outdated

MathisGD commented Jun 22, 2026

View reviewed changes

Comment thread certora/specs/CreatedMarkets.spec Outdated

MathisGD added 8 commits June 22, 2026 19:13

Apply suggestions from code review

48de9df

Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

iterate

2a8836d

Merge remote-tracking branch 'origin/modular-lif' into modular-lif

b23eb30

tests

5b6a226

simplify

2085258

simplify tests

3cf61c6

Merge branch 'main' into modular-lif

6599a14

fix lif*lltv=1 edge case

e55adcd

MathisGD marked this pull request as ready for review June 23, 2026 09:25

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread certora/specs/ExactMath.spec

chatgpt-codex-connector Bot reviewed Jun 23, 2026

View reviewed changes

QGarchery reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol

QGarchery reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

QGarchery reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

QGarchery reviewed Jun 23, 2026

View reviewed changes

Comment thread certora/confs/TakeAmountsLibInvertibility.conf Outdated

Comment thread certora/specs/CreatedMarkets.spec Outdated

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

Apply suggestion from @MathisGD

f0887ba

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

adhusson reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

adhusson reviewed Jun 23, 2026

View reviewed changes

Comment thread src/interfaces/IMidnight.sol Outdated

adhusson reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

adhusson reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

adhusson reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol Outdated

MathisGD and others added 3 commits June 23, 2026 14:48

Update src/Midnight.sol

0d96824

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Update src/Midnight.sol

5765b50

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Apply suggestion from @adhusson

3dea8cb

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/interfaces/IMidnight.sol

Apply suggestion from @MathisGD

cf64c97

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/interfaces/IMidnight.sol Outdated

MathisGD and others added 6 commits June 23, 2026 14:51

Apply suggestions from code review

c276dd1

Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Update src/Midnight.sol

756fccb

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Update src/Midnight.sol

60d444b

Co-authored-by: Adrien Husson <adhusson@gmail.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

fmt

6844f30

suggestion

ee9babc

Merge branch 'main' into modular-lif

1d673ac

MathisGD requested a review from adhusson June 23, 2026 13:15

chatgpt-codex-connector Bot reviewed Jun 23, 2026

View reviewed changes

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol

MathisGD commented Jun 23, 2026

View reviewed changes

Comment thread src/Midnight.sol

fix

2662223

chatgpt-codex-connector Bot reviewed Jun 24, 2026

View reviewed changes

Comment thread certora/specs/NoDivisionByZero.spec

verif fix

8bb800b

MathisGD requested a review from QGarchery June 24, 2026 09:43

Merge remote-tracking branch 'origin/main' into modular-lif

a806904

adhusson reviewed Jun 24, 2026

View reviewed changes

adhusson approved these changes Jun 24, 2026

View reviewed changes

QGarchery approved these changes Jun 24, 2026

View reviewed changes

QGarchery reviewed Jun 24, 2026

View reviewed changes

	require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "proven in ExactMath.spec";
	require forall uint256 i. i < market.collateralParams.length => maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) >= WAD() && maxLifGhost(market.collateralParams[i].lltv, market.collateralParams[i].liquidationCursor) <= 2 * WAD(), "see maxLifIsAtLeastWad and createdMarketsHaveMaxLifAtMostTwoWad";

Conversation

MathisGD commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jun 23, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jun 23, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jun 23, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jun 24, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

adhusson Jun 24, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery left a comment

Choose a reason for hiding this comment

Uh oh!

QGarchery Jun 24, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jun 24, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

MathisGD commented Jun 16, 2026 •

edited

Loading