refactor: apply suggestions from code review

gd-colin · QGarchery · web-flow · commit f5c5cc66468a · 2024-12-30T15:24:40.000+01:00
Co-authored-by: Quentin Garchery &lt;garchery.quentin@gmail.com&gt;
Signed-off-by: Colin | Morpho 🦋 &lt;colin@morpho.xyz&gt;
diff --git a/certora/specs/Bundler.spec b/certora/specs/Bundler.spec
@@ -44,7 +44,7 @@ rule reenterAfterMulticall(method f, env e, calldataarg data) {
 }
 
 // Check that non zero initiator will trigger a revert upon a multicall.
-rule zeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {
+rule nonZeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {
     address initiatorBefore = initiator();
 
     multicall@withrevert(e, bundle);
@@ -53,7 +53,7 @@ rule zeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {
 }
 
 // Check that a null reenterHash will trigger a revert upon reentering the bundler.
-rule zeroReenterHashReverts(env e, Bundler.Call[] bundle) {
+rule zeroReenterHashRevertsReenter(env e, Bundler.Call[] bundle) {
     bytes32 reenterHashBefore = reenterHash();
 
     reenter@withrevert(e, bundle);

Original file line number	Diff line number	Diff line change
`@@ -44,7 +44,7 @@ rule reenterAfterMulticall(method f, env e, calldataarg data) {`
`44`	`44`	`}`
`45`	`45`
`46`	`46`	`// Check that non zero initiator will trigger a revert upon a multicall.`
`47`		`-rule zeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {`
	`47`	`+rule nonZeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {`
`48`	`48`	`address initiatorBefore = initiator();`
`49`	`49`
`50`	`50`	`multicall@withrevert(e, bundle);`
`@@ -53,7 +53,7 @@ rule zeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {`
`53`	`53`	`}`
`54`	`54`
`55`	`55`	`// Check that a null reenterHash will trigger a revert upon reentering the bundler.`
`56`		`-rule zeroReenterHashReverts(env e, Bundler.Call[] bundle) {`
	`56`	`+rule zeroReenterHashRevertsReenter(env e, Bundler.Call[] bundle) {`
`57`	`57`	`bytes32 reenterHashBefore = reenterHash();`
`58`	`58`
`59`	`59`	`reenter@withrevert(e, bundle);`