[Certora] Prove revert conditions for allocate, deallocate, setName, setSymbol #877

bhargavbh · 2026-01-07T13:18:33Z

This PR proves RevertConditions for allocate(), deallocate(), setName(), setSymbol(), and setLiquidityAdapterAndData()
Most of the constraints for allocate() and deallocate() are captured in the post-conditions of the adapter's allocate and deallocate.

The revert conditions for the following remain pending due to certora issues:

submit()

…strings

…e have an added assumption that safeTransfer/From is not reverting

bhargavbh · 2026-01-20T14:24:42Z

certora/specs/AllocateDeallocateReverts.spec

+
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= 2 ^ 255 - 1, "assume allocation is small enough to cast to int256";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change >= 0, "see changeForAllocateOrDeallocateIsBoundedByAllocation";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change <= currentContract.caps[ids[i]].absoluteCap, "assume updated allocation respects absolute cap";


IIUC this can not be proved using the assumption that allocation <= absoluteCap. TBC

bhargavbh · 2026-01-20T14:28:07Z

certora/specs/AllocateDeallocateReverts.spec

+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation > 0, "assume allocation is positive";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= 2 ^ 255 - 1, "assume allocation is small enough to cast to int256";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change >= 0, "see changeForAllocateOrDeallocateIsBoundedByAllocation";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change <= 2 ^ 255 - 1, "assume updated allocation is small enough to cast to int256";


same; explicit assumption is required and can not be proved assuming allocation<=max_int256

QGarchery · 2026-01-16T14:27:09Z

certora/specs/Reverts.spec

+    function currentContract.firstTotalAssets() external returns (uint256) envfree;
+    function currentContract.liquidityAdapter() external returns (address) envfree;
+    function currentContract.liquidityData() external returns (bytes) envfree;


Suggested change

function currentContract.firstTotalAssets() external returns (uint256) envfree;

function currentContract.liquidityAdapter() external returns (address) envfree;

function currentContract.liquidityData() external returns (bytes) envfree;

function firstTotalAssets() external returns (uint256) envfree;

function liquidityAdapter() external returns (address) envfree;

function liquidityData() external returns (bytes) envfree;

QGarchery · 2026-01-21T13:09:00Z

certora/specs/AllocateDeallocateReverts.spec

+    require ids[1] != ids[2], "ack";
+
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation > 0, "assume allocation is positive";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= 2 ^ 255 - 1, "assume allocation is small enough to cast to int256";


this one is proven in the rule allocationIsInt256 (same remark in summaryAllocate)

QGarchery · 2026-01-21T13:11:10Z

certora/specs/AllocateDeallocateInputValidation.spec

+    assert !callerIsAllocator || !adapterIsRegistered || e.msg.value != 0 => lastReverted;
+}
+
+rule deallocateRevertCondition(env e, address adapter, bytes data, uint256 assets) {


do we need this rule here ? The file is named `*InputValidation', and we have a rule with the same name in the other specification file

certora/specs/AllocateDeallocateInputValidation.spec

QGarchery · 2026-01-21T13:14:38Z

certora/specs/AllocateDeallocateInputValidation.spec

+    return (ids, change);
+}
+
+rule allocateInputValidation(env e, address adapter, bytes data, uint256 assets) {


Because we have the revert condition rule already, here we can just show that it reverts for the reasons that are not covered by the revert condition rule. More formally, if we have something like P => (Q <=> reverted) already, then we want to show that P => reverted and we can omit Q (because we know that P && Q => reverted.
More concretely, what is interesting is that if the allocation is 0 on some id then deallocate reverts, and if absolute cap is 0 on some id then allocate revert. This will prove that it's not possible to interact with unknown markets

QGarchery · 2026-01-21T13:18:36Z

certora/helpers/Utils.sol

+    function libMulDivDown(
+        uint256 x,
+        uint256 y,
+        uint256 d
+    ) external pure returns (uint256) {
+        return MathLib.mulDivDown(x, y, d);
+    }


weird formatting: I get something else when doing forge fmt

QGarchery · 2026-01-21T13:28:27Z

certora/specs/AllocateDeallocateReverts.spec

+    return (ids, change);
+}
+
+rule allocateRevertCondition(env e, address adapter, bytes data, uint256 assets) {


I think it would make sense to add all the assumptions that are made at the top of the rule, like for the sentinelCanDeallocate rules. This is because we are making a few assumptions, so it's not completely clear what this rule (and the next one) is proving

QGarchery · 2026-01-21T13:43:17Z

certora/specs/AllocateDeallocateReverts.spec

+    require ids[1] != ids[2], "ack";
+
+    // CVL does not allow function calls within quantifiers, hence explicitly listed here.
+    require currentContract.firstTotalAssets() * currentContract.caps[ids[0]].relativeCap <= max_uint256, "assume firstTotalASsets is bounded by max_uint256/WAD";


Suggested change

require currentContract.firstTotalAssets() * currentContract.caps[ids[0]].relativeCap <= max_uint256, "assume firstTotalASsets is bounded by max_uint256/WAD";

require currentContract.firstTotalAssets() * currentContract.caps[ids[0]].relativeCap <= max_uint256, "safe because firstTotalASsets cannot exceed by max_uint256/WAD";

I don't think this is really an assumption of the rule, because it is assumed that the loan token is passed to market v1, which bounds the total supply to max_uint128. Actually, the following would be even clearer:

Suggested change

require currentContract.firstTotalAssets() * currentContract.caps[ids[0]].relativeCap <= max_uint256, "assume firstTotalASsets is bounded by max_uint256/WAD";

require currentContract.firstTotalAssets() <= 2 ^ 20 * 2 ^ 128, "market v1 fits total supply assets on 128 bits, and assume at most 2^20 markets";

QGarchery · 2026-01-21T13:46:29Z

certora/specs/AllocateDeallocateReverts.spec

+function summaryAllocate(env e, bytes data, uint256 assets, bytes4 selector, address sender) returns (bytes32[], int256) {
+    bytes32[] ids;
+    int256 change;
+    require ids.length == 3, "see IdsMorphoMarketV1Adapter";


Suggested change

require ids.length == 3, "see IdsMorphoMarketV1Adapter";

require ids.length == 3, "for simplicity, assume a fixed number of markets of 3";

because we cannot just assume that the adapter used is the market v1 adapter

QGarchery · 2026-01-21T13:47:30Z

certora/specs/AllocateDeallocateReverts.spec

+    require ids[0] != ids[1], "ack";
+    require ids[0] != ids[2], "ack";
+    require ids[1] != ids[2], "ack";


Let's give a reason for those: it's in the specs on adapters that they should return distinct ids

bhargavbh added 6 commits January 5, 2026 06:08

setName and setSymbol revertconditions pass after bounding lenght of …

6057914

…strings

fresh attempt at summarising deallocate via onl deallocateInternal

090a4b0

fresh attempt at summarising deallocate via onl deallocateInternal

16bff13

deallocate passes

e7898c6

deallocate passes even with inadequate assumtpions

7067392

deallocate passes even with inadequate assumtpions

bba4095

bhargavbh marked this pull request as draft January 7, 2026 13:18

bhargavbh added 9 commits January 8, 2026 14:54

hack for setName and setSymbol using string length

333687b

typo fixed

d29abfe

ignore erturned value of getStringLength call

dd46e13

formatted

cdc35d5

summaries for safeTransferFrom

c040b55

deallocate passes; issues with allocate mulDivDown

5e427dc

deallocate passes; issues with allocate mulDivDown

0d09212

issues with allocate mulDivDown but compiles

803a570

allocateRevertCondition passes

28b0802

bhargavbh changed the title ~~[Certora] Prove revert conditions for Allocate and Deallocate~~ [Certora] Prove revert conditions for Allocate, Deallocate, setName, setSymbol Jan 16, 2026

increased loop_iter in conf

a7780d3

bhargavbh changed the title ~~[Certora] Prove revert conditions for Allocate, Deallocate, setName, setSymbol~~ [Certora] Prove revert conditions for allocate, deallocate, setName, setSymbol Jan 16, 2026

added rule setLiquidityAdapterAndDataRevertCondition

d0ef327

bhargavbh marked this pull request as ready for review January 16, 2026 06:39

bhargavbh requested review from MathisGD and QGarchery January 16, 2026 06:40

bhargavbh added 7 commits January 20, 2026 11:34

separated spec and conf created for allocate and deallocate because w…

2510d79

…e have an added assumption that safeTransfer/From is not reverting

cleanup and added more meaningful error messages for require

dec3c0a

tuned

7edd399

tuned

4eadde8

tuned

1a1a010

removed allocate deallocate rules from Reverts.spec

b33d4b3

tuned

44209c5

bhargavbh commented Jan 20, 2026

View reviewed changes

input validation for allocate and deallocate

f39b37f

bhargavbh self-assigned this Jan 21, 2026

cleanup confs

5525ce4

QGarchery reviewed Jan 21, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Certora] Prove revert conditions for allocate, deallocate, setName, setSymbol #877

[Certora] Prove revert conditions for allocate, deallocate, setName, setSymbol #877

Uh oh!

bhargavbh commented Jan 7, 2026 •

edited

Loading

Uh oh!

bhargavbh Jan 20, 2026

Uh oh!

bhargavbh Jan 20, 2026

Uh oh!

QGarchery Jan 16, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

QGarchery Jan 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	require currentContract.firstTotalAssets() * currentContract.caps[ids[0]].relativeCap <= max_uint256, "assume firstTotalASsets is bounded by max_uint256/WAD";
	require currentContract.firstTotalAssets() * currentContract.caps[ids[0]].relativeCap <= max_uint256, "safe because firstTotalASsets cannot exceed by max_uint256/WAD";

	require ids.length == 3, "see IdsMorphoMarketV1Adapter";
	require ids.length == 3, "for simplicity, assume a fixed number of markets of 3";

[Certora] Prove revert conditions for allocate, deallocate, setName, setSymbol #877

Are you sure you want to change the base?

[Certora] Prove revert conditions for allocate, deallocate, setName, setSymbol #877

Uh oh!

Conversation

bhargavbh commented Jan 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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

bhargavbh commented Jan 7, 2026 •

edited

Loading