fix: rule instead of invariant

QGarchery · QGarchery · commit 092221b74f23 · 2025-12-10T16:03:17.000+01:00
diff --git a/certora/specs/AllocationMorphoMarketV1AdapterV2.spec b/certora/specs/AllocationMorphoMarketV1AdapterV2.spec
@@ -94,7 +94,7 @@ rule allocationAfterAllocate(env e, bytes data, uint256 assets) {
 
     MorphoHarness.MarketParams marketParams = Utils.decodeMarketParams(data);
     uint256 expected = MorphoMarketV1AdapterV2.expectedSupplyAssets(e, Utils.id(marketParams));
-    require expected < 2 ^ 128, "see expectedSupplyAssetsIsBounded invariant";
+    require expected < 2 ^ 128, "see rule expectedSupplyAssetsIsBounded";
 
     assert MorphoMarketV1AdapterV2.allocation(marketParams) == expected;
 }
@@ -132,7 +132,7 @@ rule allocationAfterDeallocate(env e, bytes data, uint256 assets) {
 
     MorphoHarness.MarketParams marketParams = Utils.decodeMarketParams(data);
     uint256 expected = MorphoMarketV1AdapterV2.expectedSupplyAssets(e, Utils.id(marketParams));
-    require expected < 2 ^ 128, "see expectedSupplyAssetsIsBounded invariant";
+    require expected < 2 ^ 128, "see rule expectedSupplyAssetsIsBounded";
 
     assert MorphoMarketV1AdapterV2.allocation(marketParams) == expected;
 }

Original file line number	Diff line number	Diff line change
`@@ -94,7 +94,7 @@ rule allocationAfterAllocate(env e, bytes data, uint256 assets) {`
`94`	`94`
`95`	`95`	`MorphoHarness.MarketParams marketParams = Utils.decodeMarketParams(data);`
`96`	`96`	`uint256 expected = MorphoMarketV1AdapterV2.expectedSupplyAssets(e, Utils.id(marketParams));`
`97`		`- require expected < 2 ^ 128, "see expectedSupplyAssetsIsBounded invariant";`
	`97`	`+ require expected < 2 ^ 128, "see rule expectedSupplyAssetsIsBounded";`
`98`	`98`
`99`	`99`	`assert MorphoMarketV1AdapterV2.allocation(marketParams) == expected;`
`100`	`100`	`}`
`@@ -132,7 +132,7 @@ rule allocationAfterDeallocate(env e, bytes data, uint256 assets) {`
`132`	`132`
`133`	`133`	`MorphoHarness.MarketParams marketParams = Utils.decodeMarketParams(data);`
`134`	`134`	`uint256 expected = MorphoMarketV1AdapterV2.expectedSupplyAssets(e, Utils.id(marketParams));`
`135`		`- require expected < 2 ^ 128, "see expectedSupplyAssetsIsBounded invariant";`
	`135`	`+ require expected < 2 ^ 128, "see rule expectedSupplyAssetsIsBounded";`
`136`	`136`
`137`	`137`	`assert MorphoMarketV1AdapterV2.allocation(marketParams) == expected;`
`138`	`138`	`}`