[certora] allocation at groupId is greater than equal leafId by bhargavbh · Pull Request #905 · morpho-org/vault-v2

bhargavbh · 2026-03-08T19:42:32Z

~~adds invariants that allocation at AdapterId and CollateralId is sum of MarketId allocations.~~
~~as a result, proves:~~
~~- adapter allocation >= any individual market allocation~~
~~- collateral allocation >= any individual market allocation~~

For a generic adapter following a hierarchical model of leafId (e.g. marketId) and groupId (e.g. collateralId), proves that the allocation at the group-level >= allocation at leaf-level.

…of allocations at MarketId

renamed Signed-off-by: Bhargav Bhatt <40268131+bhargavbh@users.noreply.github.com>

lilCertora · 2026-03-18T10:56:41Z

certora/specs/AllocationsHierarchy.spec

+
+    // Require change values to be bounded, else the sum exceeds max_uint256.
+    // Note that the implicit cast from uint256 to int256 is saf here, see allocationIsInt256 in Invariants.spec
+    require allocation(ids[0]) + change >= 0, "group level allocation + change is non-negative";


maybe worth redeclaring :

strong invariant allocationIsInt256(bytes32 id) allocation(id) <= max_int256();

like in AllocationMorphoMarketV1AdapterV2 and require them directly ?

maybe not finally , these lines are stronger than these invariants

lilCertora · 2026-03-18T11:02:45Z

certora/confs/AllocationsHierarchy.conf

+    "-destructiveOptimizations twostage",
+    "-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}]"
+  ],
+  "global_timeout": "7200",


just curious , is it intentional to have both global and smt timeout set to 7200 ?
default smt is 300 but maybe this is wanted

just used the same timeout as a similar spec, but i can try reducing it. here is the prover link.
In general, it is not a very heavy spec.

certora/specs/AllocationsHierarchy.spec

QGarchery · 2026-03-18T12:03:21Z

certora/specs/AllocationsHierarchy.spec

+
+    // assume the following functions return arbitrary value but do not modify the relevant storage for this rule.
+    function _.balanceOf(address) external => NONDET;
+    function _.realAssets() external => NONDET;


Suggested change

function _.realAssets() external => NONDET;

it's unused because accrueInterestView is summarized

QGarchery · 2026-03-18T12:08:42Z

certora/specs/AllocationsHierarchy.spec

+    function _.transfer(address, uint256) external => NONDET;
+    function _.transferFrom(address, address, uint256) external => NONDET;


The comment above assume the following functions return arbitrary value but do not modify the relevant storage for this rule. only really applies to the summary of the transfer functions (and accrueInterest), because the other functions are view so NONDET is an over-approximation since we are not looking at reverts

Btw, wondering if we cannot remove those 2 summaries, since we are proving strong invariants, which models reentrancy

Suggested change

function _.transfer(address, uint256) external => NONDET;

function _.transferFrom(address, address, uint256) external => NONDET;

QGarchery · 2026-03-18T12:11:03Z

certora/specs/AllocationsHierarchy.spec

+    function _.canSendShares(address) external => NONDET;
+    function _.canReceiveAssets(address) external => NONDET;
+    function _.canSendAssets(address) external => NONDET;
+    function accrueInterest() internal => NONDET;


Suggested change

function accrueInterest() internal => NONDET;

would this be possible, since we are already summarizing accrueInterestView ? It would be really nice, because then it removes part of the assumption "the following functions return arbitrary value but do not modify the relevant storage for this rule" which is not trivial to check

QGarchery · 2026-03-18T12:19:50Z

certora/specs/AllocationsHierarchy.spec

+// - groupId and leafId are distinct
+// - groupId is never itself a leaf in any other adapter
+// - leafId is never itself a group in any other adapter
+// - a leaf's parent group never changes across calls


Suggested change

// - a leaf's parent group never changes across calls

// - a leaf has a unique parent group, and that group never changes across calls

because the existence of the group is already an assumption in itself

QGarchery · 2026-03-18T12:22:23Z

certora/specs/AllocationsHierarchy.spec

+    // Require change values to be bounded, else the sum exceeds max_uint256.
+    // Note that the implicit cast from uint256 to int256 is saf here, see allocationIsInt256 in Invariants.spec
+    require allocation(ids[0]) + change >= 0, "group level allocation + change is non-negative";
+    require allocation(ids[0]) + change <= max_uint256, "group level allocation + change is bounded";
+    require allocation(ids[1]) + change >= 0, "leaf level allocation + change is non-negative";
+    require allocation(ids[1]) + change <= max_uint256, "leaf level allocation + change is bounded";


Not clear to me why we need those. If an adapter doesn't have the property then it might revert, but this isn't a path that the prover would consider.
Also note that the property allocation(ids[0]) + change <= max_uint256 is precisely the reason why we are trying to prove the whole spec, so that we "prove" why the requires of this form in the other specs are sound to make

QGarchery · 2026-03-18T13:16:20Z

certora/specs/AllocationsHierarchy.spec

+// Every ghost cell stays within uint256 bounds.
+strong invariant ghostAllocationBounded(bytes32 g, bytes32 l)
+    ghostAllocationByGroupId[g][l] >= 0 && ghostAllocationByGroupId[g][l] <= max_uint256;


Suggested change

// Every ghost cell stays within uint256 bounds.

strong invariant ghostAllocationBounded(bytes32 g, bytes32 l)

ghostAllocationByGroupId[g][l] >= 0 && ghostAllocationByGroupId[g][l] <= max_uint256;

let's just define ghostAllocationByGroupId as a uint256 instead of as a mathint

QGarchery · 2026-03-18T13:18:07Z

certora/specs/AllocationsHierarchy.spec

+    !(ghostIsLeafId[id] && ghostIsGroupId[id]);
+
+// A ghost cell is non-zero only if its leaf is registered and maps to that group.
+strong invariant ghostGroupConsistency(bytes32 groupId, bytes32 leafId)


Suggested change

strong invariant ghostGroupConsistency(bytes32 groupId, bytes32 leafId)

strong invariant nonMatchingLeafAndGroupHasZeroGhostAllocation(bytes32 groupId, bytes32 leafId)

QGarchery · 2026-03-18T13:27:49Z

certora/confs/AllocationsHierarchy.conf

+  "compiler_map": {
+    "VaultV2": "solc-0.8.28"
+  },


Suggested change

"compiler_map": {

"VaultV2": "solc-0.8.28"

},

"solc": "solc-0.8.28",

QGarchery · 2026-03-18T13:33:52Z

certora/specs/AllocationsHierarchy.spec

+    ghostIsGroupId[groupId] => to_mathint(allocation(groupId)) == (usum bytes32 leafId. ghostAllocationByGroupId[groupId][leafId])
+    {
+        preserved with (env e) {
+            bytes32 anyLeafId;


I don't think that this does anything, the anyLeafId can be chosen arbitrarily by the prover, so it could chose nonsensical value for it which would add a useless property to the context. Here is a run that goes through without it

certora/specs/AllocationsHierarchy.spec

bhargavbh added 8 commits March 8, 2026 20:34

adds invariants that allocation at AdapterId and CollateralId is sum …

b986ae7

…of allocations at MarketId

tuned

ec2233a

added new NONDET summaries to avoid Havocs

1fee926

persistent ghost mappings

106bed5

multiple supporting invariants

7120685

usum invariants proven

aa255ce

added consistency invariants to allocationsSumOfMarketIdAllocations

8b858d6

tuned: clean up

bca9c3d

bhargavbh changed the title ~~adds invariants that allocation at AdapterId and CollateralId is sum …~~ [certora] allocation at AdapterId and CollateralId is greater than marketId Mar 16, 2026

bhargavbh added 2 commits March 17, 2026 09:01

geenralised to leafID and groupId

586a711

rearranged invariants; cleaned up assumptions

e990258

bhargavbh changed the title ~~[certora] allocation at AdapterId and CollateralId is greater than marketId~~ [certora] allocation at groupId is greater than leafId Mar 17, 2026

bhargavbh and others added 4 commits March 17, 2026 16:54

renamed spec; added in workflow

b991ef8

Delete certora/confs/AllocationsSumOfMarketIdAllocations.conf

7d90aec

renamed Signed-off-by: Bhargav Bhatt <40268131+bhargavbh@users.noreply.github.com>

Delete certora/specs/AllocationsSumOfMarketIdAllocations.spec

825d39b

renamed Signed-off-by: Bhargav Bhatt <40268131+bhargavbh@users.noreply.github.com>

cleaned up assumptions in adapter

a50772c

bhargavbh self-assigned this Mar 17, 2026

bhargavbh marked this pull request as ready for review March 17, 2026 21:27

bhargavbh changed the title ~~[certora] allocation at groupId is greater than leafId~~ [certora] allocation at groupId is greater than equal leafId Mar 17, 2026

bhargavbh requested review from MathisGD, QGarchery, jhoenicke and lilCertora March 17, 2026 21:40

lilCertora reviewed Mar 18, 2026

View reviewed changes

certora/specs/AllocationsHierarchy.spec Show resolved Hide resolved

QGarchery reviewed Mar 18, 2026

View reviewed changes

QGarchery added the verif-review label Mar 18, 2026

jhoenicke mentioned this pull request Mar 23, 2026

[Certora] canForceDeallocateZero #894

Open

		function _.transfer(address, uint256) external => NONDET;
		function _.transferFrom(address, address, uint256) external => NONDET;

	// - a leaf's parent group never changes across calls
	// - a leaf has a unique parent group, and that group never changes across calls

	// Every ghost cell stays within uint256 bounds.
	strong invariant ghostAllocationBounded(bytes32 g, bytes32 l)
	ghostAllocationByGroupId[g][l] >= 0 && ghostAllocationByGroupId[g][l] <= max_uint256;

	strong invariant ghostGroupConsistency(bytes32 groupId, bytes32 leafId)
	strong invariant nonMatchingLeafAndGroupHasZeroGhostAllocation(bytes32 groupId, bytes32 leafId)

Conversation

bhargavbh commented Mar 8, 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!

lilCertora Mar 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

bhargavbh commented Mar 8, 2026 •

edited

Loading

lilCertora Mar 18, 2026 •

edited

Loading