Skip to content

Commit

Permalink
Fix
Browse files Browse the repository at this point in the history
  • Loading branch information
sunbreak1211 committed Oct 3, 2024
1 parent 8c3dc21 commit f7a4013
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions certora/LockstakeEngine.spec
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ function dripSummary(bytes32 ilk) returns uint256 {
}

// Verify that each storage layout is only modified in the corresponding functions
rule storageAffected(method f) filtered { f.selector != sig:multicall(bytes[]).selector } {
rule storageAffected(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } {
env e;

address anyAddr;
Expand Down Expand Up @@ -193,7 +193,7 @@ rule storageAffected(method f) filtered { f.selector != sig:multicall(bytes[]).s
assert jugAfter != jugBefore => f.selector == sig:file(bytes32,address).selector, "Assert 10";
}

rule vatGemKeepsUnchanged(method f) filtered { f.selector != sig:multicall(bytes[]).selector } {
rule vatGemKeepsUnchanged(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } {
env e;

address anyAddr;
Expand All @@ -210,7 +210,7 @@ rule vatGemKeepsUnchanged(method f) filtered { f.selector != sig:multicall(bytes
assert vatGemIlkAnyAfter == vatGemIlkAnyBefore, "Assert 1";
}

rule inkChangeMatchesMkrChange(method f) filtered { f.selector != sig:multicall(bytes[]).selector } {
rule inkChangeMatchesMkrChange(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } {
env e;

createdUrn = 0;
Expand Down Expand Up @@ -284,7 +284,7 @@ rule inkChangeMatchesMkrChange(method f) filtered { f.selector != sig:multicall(
mkrBalanceOfVoteDelegateBeforeAfter - mkrBalanceOfVoteDelegateBeforeBefore == mkrBalanceOfVoteDelegateAfterBefore - mkrBalanceOfVoteDelegateAfterAfter, "Assert3";
}

rule inkChangeMatchesLsmkrChange(method f) filtered { f.selector != sig:multicall(bytes[]).selector } {
rule inkChangeMatchesLsmkrChange(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } {
env e;

createdUrn = 0;
Expand Down

0 comments on commit f7a4013

Please sign in to comment.