[Certora] lib/bundler assets/debts reachability by lilCertora · Pull Request #916 · morpho-org/midnight

lilCertora · 2026-05-22T17:54:27Z

No description provided.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: cb5264a55a

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: eabec97f3b

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector · 2026-06-01T07:05:58Z

+    uint256 debtBefore = midnight.debtOf(id, onBehalf);
+    require U > 0 && U <= debtBefore, "target units within current debt";
+
+    require midnight.isAuthorized(onBehalf, currentContract), "bundler must be authorized on Midnight for repay";


Constrain the bundler caller authorization

This only assumes the bundler is authorized for the inner Midnight.repay, but repayAndWithdrawCollateral first requires the external caller to be onBehalf or authorized by onBehalf. For any e.msg.sender that fails that outer check, the plain CVL call below silently prunes the revert path, so the rule can pass without covering those callers. Add require onBehalf == e.msg.sender || midnight.isAuthorized(onBehalf, e.msg.sender) (or switch to @withrevert and assert the expected revert behavior).

Useful? React with 👍 / 👎.

that's the idea of CVL

codex is suggesting to add a require, but do we even need the one that is currently written ?

bhargavbh

very nice roundtrip properties to have for bundler's liveness guarantees.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 6ed13dd96a

ℹ️ About Codex in GitHub

Codex has been enabled to automatically 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 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

bhargavbh

LGTM. Please update the README with the rules description.

Co-authored-by: Bhargav Bhatt <40268131+bhargavbh@users.noreply.github.com> Signed-off-by: lilCertora <lilian@certora.com>

QGarchery · 2026-06-04T10:53:08Z

+import {Offer} from "../../src/interfaces/IMidnight.sol";
+import {TakeAmountsLib} from "../../src/periphery/TakeAmountsLib.sol";
+
+/// @dev Thin harness exposing TakeAmountsLib's `internal` library functions to CVL.


Suggested change

/// @dev Thin harness exposing TakeAmountsLib's `internal` library functions to CVL.

QGarchery · 2026-06-04T11:02:08Z

+    // Deterministic market id (same pattern as Midnight.spec / TakeAmountsLibInvertibility.spec).
+    function IdLib.toId(Midnight.Market memory market, uint256, address) internal returns (bytes32) => summaryToId(market);
+
+    // Deterministic floor division; must not call MulDiv (it delegates back to UtilsLib.mulDivDown).


Suggested change

// Deterministic floor division; must not call MulDiv (it delegates back to UtilsLib.mulDivDown).

// Deterministic mulDivDown.

I don't understand the rest

QGarchery · 2026-06-04T11:02:36Z

+}
+
+function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 {
+    if (d == 0) {


Suggested change

if (d == 0) {

bool overflow;

if (d == 0 || overflow) {

QGarchery · 2026-06-04T11:02:58Z

+    if (d == 0) {
+        revert();
+    }
+    return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d));


Suggested change

return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d));

return require_uint256(a * b / d);

QGarchery · 2026-06-04T11:05:09Z

+    // Deterministic floor division; must not call MulDiv (it delegates back to UtilsLib.mulDivDown).
+    function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d);
+
+    // Token / permit functions are irrelevant to the units formula but NONDET prevent havoc calls.


Suggested change

// Token / permit functions are irrelevant to the units formula but NONDET prevent havoc calls.

// Token / permit functions are irrelevant to the units formula, use a NONDET summary to prevent calls that havoc Midnight.

QGarchery · 2026-06-05T09:00:08Z

+
+/// MULDIV GHOST SUMMARIES (mirrors AccrualRounding.spec) ///
+
+persistent ghost summaryMulDivDownM(mathint, mathint, mathint) returns mathint {


Suggested change

persistent ghost summaryMulDivDownM(mathint, mathint, mathint) returns mathint {

persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint {

QGarchery · 2026-06-05T09:00:40Z

+/* proved in mulDivUpRoundsUp */
+definition axiomUpLowerBound(mathint a, mathint b, mathint d) returns bool = 0 <= a && 0 <= b && 0 < d => summaryMulDivUpM(a, b, d) * d >= a * b;
+
+/* proved in mulDivUpUpperBound */
+definition axiomUpUpperBound(mathint a, mathint b, mathint d) returns bool = 0 <= a && 0 <= b && 0 < d => summaryMulDivUpM(a, b, d) * d <= a * b + d - 1;
+
+/* proved in mulDivDownRoundsDown */
+definition axiomDownUpperBound(mathint a, mathint b, mathint d) returns bool = 0 <= a && 0 <= b && 0 < d => summaryMulDivDownM(a, b, d) * d <= a * b;
+
+/* proved in mulDivDownTightBound */
+definition axiomDownTightBound(mathint a, mathint b, mathint d) returns bool = 0 <= a && 0 <= b && 0 < d => (summaryMulDivDownM(a, b, d) + 1) * d > a * b;


let's put them as axioms in the ghost variables, that avoids defining the requireMulDivAxioms function

QGarchery · 2026-06-05T09:02:47Z

+    requireMulDivAxioms();
+
+    bytes32 id = summaryToId(offer.market);
+    require tickSpacing(id) > 0, "market is already created";


Suggested change

require tickSpacing(id) > 0, "market is already created";

it should not be needed because settlementFee() reverts if the market is not created

QGarchery · 2026-06-05T09:03:09Z

+    requireMulDivAxioms();
+
+    bytes32 id = summaryToId(offer.market);
+    require tickSpacing(id) > 0, "market is already created";


Suggested change

require tickSpacing(id) > 0, "market is already created";

QGarchery · 2026-06-05T09:04:16Z

+    // Mirror the library's sellerPrice computation in CVL to express the WAD precondition.
+    uint256 offerPrice = summaryTickToPrice(offer.tick);
+    uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0;
+    uint256 fee = settlementFee(id, timeToMaturity);
+    require !offer.buy || fee <= offerPrice, "library reverts otherwise";
+


Suggested change

// Mirror the library's sellerPrice computation in CVL to express the WAD precondition.

uint256 offerPrice = summaryTickToPrice(offer.tick);

uint256 timeToMaturity = e.block.timestamp <= offer.market.maturity ? assert_uint256(offer.market.maturity - e.block.timestamp) : 0;

uint256 fee = settlementFee(id, timeToMaturity);

require !offer.buy || fee <= offerPrice, "library reverts otherwise";

same reasoning

lilCertora added 4 commits May 22, 2026 19:52

add spec and conf

1365e14

modif spec

00b3a42

add helper

feb0e82

linter bundler

59df000

lilCertora self-assigned this May 22, 2026

lilCertora added 5 commits May 25, 2026 10:35

modif bundlerRepay spec

ba83a2a

linter spec

1cbfeef

improvement bundler spec

31d81ad

cleaning

7df4449

modif spec comments

470a2de

lilCertora requested review from MathisGD, QGarchery, bhargavbh and jhoenicke May 25, 2026 16:01

lilCertora marked this pull request as ready for review May 25, 2026 16:01

lilCertora mentioned this pull request May 26, 2026

[Certora] verif wish list #109

Open

70 tasks

Merge branch 'main' into certora/bundlerAndTakeAmountLib

cb5264a

chatgpt-codex-connector Bot reviewed May 31, 2026

View reviewed changes

Comment thread certora/specs/TakeAmountsLibInvertibility.spec Outdated

Comment thread certora/specs/BundlerRepayInvertibility.spec Outdated

lilCertora added 2 commits May 31, 2026 18:53

update

f02e464

fix midnight update

eabec97

chatgpt-codex-connector Bot reviewed Jun 1, 2026

View reviewed changes

bhargavbh requested changes Jun 2, 2026

View reviewed changes

Comment thread certora/specs/TakeAmountsLibInvertibility.spec Outdated

Comment thread certora/specs/BundlerRepayInvertibility.spec Outdated

Comment thread certora/specs/BundlerRepayInvertibility.spec Outdated

Review changes

6ed13dd

lilCertora requested a review from bhargavbh June 2, 2026 12:25

chatgpt-codex-connector Bot reviewed Jun 2, 2026

View reviewed changes

Comment thread certora/specs/TakeAmountsLibInvertibility.spec

bhargavbh approved these changes Jun 2, 2026

View reviewed changes

lilCertora and others added 4 commits June 2, 2026 22:55

Update certora/specs/BundlerRepayInvertibility.spec

2e88cda

Co-authored-by: Bhargav Bhatt <40268131+bhargavbh@users.noreply.github.com> Signed-off-by: lilCertora <lilian@certora.com>

Merge branch 'main' into certora/bundlerAndTakeAmountLib

7eaee08

modif readme

aa9a90c

Merge branch 'main' into certora/bundlerAndTakeAmountLib

a31b6f2

QGarchery reviewed Jun 5, 2026

View reviewed changes

	// Deterministic floor division; must not call MulDiv (it delegates back to UtilsLib.mulDivDown).
	// Deterministic mulDivDown.

	return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d));
	return require_uint256(a * b / d);

	// Token / permit functions are irrelevant to the units formula but NONDET prevent havoc calls.
	// Token / permit functions are irrelevant to the units formula, use a NONDET summary to prevent calls that havoc Midnight.


		/// MULDIV GHOST SUMMARIES (mirrors AccrualRounding.spec) ///

		persistent ghost summaryMulDivDownM(mathint, mathint, mathint) returns mathint {

	persistent ghost summaryMulDivDownM(mathint, mathint, mathint) returns mathint {
	persistent ghost ghostMulDivDown(mathint, mathint, mathint) returns mathint {

Conversation

lilCertora commented May 22, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

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 1, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

bhargavbh left a comment

Choose a reason for hiding this comment

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!

Uh oh!

bhargavbh left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants