diff --git a/Makefile b/Makefile index af591cea..8991ec18 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ -certora-buffer :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorBuffer=solc-0.8.16,GemMock=solc-0.8.16 --solc_optimize_map AllocatorBuffer=200,GemMock=0 --rule_sanity basic src/AllocatorBuffer.sol test/mocks/GemMock.sol --verify AllocatorBuffer:certora/AllocatorBuffer.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-vault :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorVault=solc-0.8.16,AllocatorRoles=solc-0.8.16,VatMock=solc-0.8.16,JugMock=solc-0.8.16,NstJoinMock=solc-0.8.16,NstMock=solc-0.8.16 --solc_optimize_map AllocatorVault=200,AllocatorRoles=200,VatMock=0,JugMock=0,NstJoinMock=0,NstMock=0 --rule_sanity basic src/AllocatorVault.sol src/AllocatorRoles.sol test/mocks/VatMock.sol test/mocks/JugMock.sol test/mocks/NstJoinMock.sol test/mocks/NstMock.sol --link AllocatorVault:roles=AllocatorRoles AllocatorVault:vat=VatMock AllocatorVault:jug=JugMock AllocatorVault:nstJoin=NstJoinMock AllocatorVault:nst=NstMock JugMock:vat=VatMock NstJoinMock:vat=VatMock NstJoinMock:nst=NstMock --verify AllocatorVault:certora/AllocatorVault.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results --multi_assert_check -certora-roles :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRoles=solc-0.8.16 --solc_optimize_map AllocatorRoles=200 --rule_sanity basic src/AllocatorRoles.sol --verify AllocatorRoles:certora/AllocatorRoles.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-oracle :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorOracle=solc-0.8.16 --solc_optimize_map AllocatorOracle=200 --rule_sanity basic src/AllocatorOracle.sol --verify AllocatorOracle:certora/AllocatorOracle.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-registry :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRegistry=solc-0.8.16 --solc_optimize_map AllocatorRegistry=200 --rule_sanity basic src/AllocatorRegistry.sol --verify AllocatorRegistry:certora/AllocatorRegistry.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map Swapper=solc-0.8.16,AllocatorRoles=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,CalleeMock=solc-0.8.16 --solc_optimize_map Swapper=200,AllocatorRoles=200,Gem0Mock=0,Gem1Mock=0,CalleeMock=0 --rule_sanity basic src/funnels/Swapper.sol src/AllocatorRoles.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol test/mocks/CalleeMock.sol --link Swapper:roles=AllocatorRoles --verify Swapper:certora/funnels/Swapper.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map DepositorUniV3=solc-0.8.16,AllocatorRoles=solc-0.8.16,PoolUniV3Mock=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,Auxiliar=solc-0.8.16 --solc_optimize_map DepositorUniV3=200,AllocatorRoles=200,PoolUniV3Mock=0,Gem0Mock=0,Gem1Mock=0,Auxiliar=0 --rule_sanity basic src/funnels/DepositorUniV3.sol src/AllocatorRoles.sol test/mocks/PoolUniV3Mock.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol certora/funnels/Auxiliar.sol --link DepositorUniV3:roles=AllocatorRoles --verify DepositorUniV3:certora/funnels/DepositorUniV3.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-stable-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableSwapper=solc-0.8.16 --solc_optimize_map StableSwapper=200 --rule_sanity basic src/funnels/automation/StableSwapper.sol --verify StableSwapper:certora/funnels/automation/StableSwapper.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-stable-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableDepositorUniV3=solc-0.8.16 --solc_optimize_map StableDepositorUniV3=200 --rule_sanity basic src/funnels/automation/StableDepositorUniV3.sol --verify StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results -certora-conduit-mover :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map ConduitMover=solc-0.8.16 --solc_optimize_map ConduitMover=200 --rule_sanity basic src/funnels/automation/ConduitMover.sol --verify ConduitMover:certora/funnels/automation/ConduitMover.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results +certora-buffer :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorBuffer=solc-0.8.16,GemMock=solc-0.8.16 --solc_optimize_map AllocatorBuffer=200,GemMock=0 --rule_sanity basic src/AllocatorBuffer.sol test/mocks/GemMock.sol --verify AllocatorBuffer:certora/AllocatorBuffer.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-vault :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorVault=solc-0.8.16,AllocatorRoles=solc-0.8.16,VatMock=solc-0.8.16,JugMock=solc-0.8.16,NstJoinMock=solc-0.8.16,NstMock=solc-0.8.16 --solc_optimize_map AllocatorVault=200,AllocatorRoles=200,VatMock=0,JugMock=0,NstJoinMock=0,NstMock=0 --rule_sanity basic src/AllocatorVault.sol src/AllocatorRoles.sol test/mocks/VatMock.sol test/mocks/JugMock.sol test/mocks/NstJoinMock.sol test/mocks/NstMock.sol --link AllocatorVault:roles=AllocatorRoles AllocatorVault:vat=VatMock AllocatorVault:jug=JugMock AllocatorVault:nstJoin=NstJoinMock AllocatorVault:nst=NstMock JugMock:vat=VatMock NstJoinMock:vat=VatMock NstJoinMock:nst=NstMock --verify AllocatorVault:certora/AllocatorVault.spec --parametric_contracts AllocatorVault --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --multi_assert_check +certora-roles :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRoles=solc-0.8.16 --solc_optimize_map AllocatorRoles=200 --rule_sanity basic src/AllocatorRoles.sol --verify AllocatorRoles:certora/AllocatorRoles.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-oracle :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorOracle=solc-0.8.16 --solc_optimize_map AllocatorOracle=200 --rule_sanity basic src/AllocatorOracle.sol --verify AllocatorOracle:certora/AllocatorOracle.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-registry :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRegistry=solc-0.8.16 --solc_optimize_map AllocatorRegistry=200 --rule_sanity basic src/AllocatorRegistry.sol --verify AllocatorRegistry:certora/AllocatorRegistry.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map Swapper=solc-0.8.16,AllocatorRoles=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,CalleeMock=solc-0.8.16 --solc_optimize_map Swapper=200,AllocatorRoles=200,Gem0Mock=0,Gem1Mock=0,CalleeMock=0 --rule_sanity basic src/funnels/Swapper.sol src/AllocatorRoles.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol test/mocks/CalleeMock.sol --link Swapper:roles=AllocatorRoles --verify Swapper:certora/funnels/Swapper.spec --parametric_contracts Swapper --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map DepositorUniV3=solc-0.8.16,AllocatorRoles=solc-0.8.16,PoolUniV3Mock=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,Auxiliar=solc-0.8.16 --solc_optimize_map DepositorUniV3=200,AllocatorRoles=200,PoolUniV3Mock=0,Gem0Mock=0,Gem1Mock=0,Auxiliar=0 --rule_sanity basic src/funnels/DepositorUniV3.sol src/AllocatorRoles.sol test/mocks/PoolUniV3Mock.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol certora/funnels/Auxiliar.sol --link DepositorUniV3:roles=AllocatorRoles --verify DepositorUniV3:certora/funnels/DepositorUniV3.spec --parametric_contracts DepositorUniV3 --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-stable-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableSwapper=solc-0.8.16 --solc_optimize_map StableSwapper=200 --rule_sanity basic src/funnels/automation/StableSwapper.sol --verify StableSwapper:certora/funnels/automation/StableSwapper.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-stable-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableDepositorUniV3=solc-0.8.16 --solc_optimize_map StableDepositorUniV3=200 --rule_sanity basic src/funnels/automation/StableDepositorUniV3.sol --verify StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) +certora-conduit-mover :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map ConduitMover=solc-0.8.16 --solc_optimize_map ConduitMover=200 --rule_sanity basic src/funnels/automation/ConduitMover.sol --verify ConduitMover:certora/funnels/automation/ConduitMover.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) diff --git a/certora/AllocatorBuffer.spec b/certora/AllocatorBuffer.spec index 5daeca45..a60d98cc 100644 --- a/certora/AllocatorBuffer.spec +++ b/certora/AllocatorBuffer.spec @@ -8,6 +8,22 @@ methods { function _.approve(address, uint256) external => DISPATCHER(true) UNRESOLVED; } +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + + mathint wardsBefore = wards(anyAddr); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; +} + // Verify correct storage changes for non reverting rely rule rely(address usr) { env e; diff --git a/certora/AllocatorRegistry.spec b/certora/AllocatorRegistry.spec index 3947044b..f114f0ff 100644 --- a/certora/AllocatorRegistry.spec +++ b/certora/AllocatorRegistry.spec @@ -5,26 +5,42 @@ methods { function buffers(bytes32) external returns (address) envfree; } +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + bytes32 anyBytes32; + + mathint wardsBefore = wards(anyAddr); + address buffersBefore = buffers(anyBytes32); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + address buffersAfter = buffers(anyBytes32); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert buffersAfter != buffersBefore => f.selector == sig:file(bytes32,bytes32,address).selector, "buffers[x] changed in an unexpected function"; +} + // Verify correct storage changes for non reverting rely rule rely(address usr) { env e; address other; require other != usr; - bytes32 anyBytes32; mathint wardsOtherBefore = wards(other); - address buffersBefore = buffers(anyBytes32); rely(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - address buffersAfter = buffers(anyBytes32); assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert buffersAfter == buffersBefore, "rely did not keep unchanged every buffers[x]"; } // Verify revert rules on rely @@ -49,20 +65,16 @@ rule deny(address usr) { address other; require other != usr; - bytes32 anyBytes32; mathint wardsOtherBefore = wards(other); - address buffersBefore = buffers(anyBytes32); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - address buffersAfter = buffers(anyBytes32); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert buffersAfter == buffersBefore, "deny did not keep unchanged every buffers[x]"; } // Verify revert rules on deny @@ -85,20 +97,16 @@ rule deny_revert(address usr) { rule file(bytes32 ilk, bytes32 what, address data) { env e; - address anyAddr; bytes32 otherBytes32; require otherBytes32 != ilk; - mathint wardsBefore = wards(anyAddr); address buffersOtherBefore = buffers(otherBytes32); file(e, ilk, what, data); - mathint wardsAfter = wards(anyAddr); address buffersIlkAfter = buffers(ilk); address buffersOtherAfter = buffers(otherBytes32); - assert wardsAfter == wardsBefore, "file did not keep unchanged every wards[x]"; assert buffersIlkAfter == data, "file did not set buffers[ilk] to data"; assert buffersOtherAfter == buffersOtherBefore, "file did not keep unchanged the rest of buffers[x]"; } diff --git a/certora/AllocatorRoles.spec b/certora/AllocatorRoles.spec index 1ccd155b..5f2128cd 100644 --- a/certora/AllocatorRoles.spec +++ b/certora/AllocatorRoles.spec @@ -30,34 +30,49 @@ rule hasActionRole(bytes32 ilk, address target, bytes4 sign, uint8 role) { assert ok2 == ok, "hasActionRole did not return the expected result"; } -// Verify correct storage changes for non reverting rely -rule rely(address usr) { +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { env e; - address other; - require other != usr; - bytes32 anyBytes32; address anyAddr; + bytes32 anyBytes32; bytes4 anyBytes4; - mathint wardsOtherBefore = wards(other); + mathint wardsBefore = wards(anyAddr); address ilkAdminsBefore = ilkAdmins(anyBytes32); bytes32 userRolesBefore = userRoles(anyBytes32, anyAddr); bytes32 actionsRolesBefore = actionsRoles(anyBytes32, anyAddr, anyBytes4); - rely(e, usr); + calldataarg args; + f(e, args); - mathint wardsUsrAfter = wards(usr); - mathint wardsOtherAfter = wards(other); + mathint wardsAfter = wards(anyAddr); address ilkAdminsAfter = ilkAdmins(anyBytes32); bytes32 userRolesAfter = userRoles(anyBytes32, anyAddr); bytes32 actionsRolesAfter = actionsRoles(anyBytes32, anyAddr, anyBytes4); + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert ilkAdminsAfter != ilkAdminsBefore => f.selector == sig:setIlkAdmin(bytes32,address).selector, "ilkAdmins[x] changed in an unexpected function"; + assert userRolesAfter != userRolesBefore => f.selector == sig:setUserRole(bytes32,address,uint8,bool).selector, "userRoles[x][y] changed in an unexpected function"; + assert actionsRolesAfter != actionsRolesBefore => f.selector == sig:setRoleAction(bytes32,uint8,address,bytes4,bool).selector, "actionsRoles[x][y][z] changed in an unexpected function"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert ilkAdminsAfter == ilkAdminsBefore, "rely did not keep unchanged every ilkAdmins[x]"; - assert userRolesAfter == userRolesBefore, "rely did not keep unchanged every userRoles[x][y]"; - assert actionsRolesAfter == actionsRolesBefore, "rely did not keep unchanged every actionsRoles[x][y][z]"; } // Verify revert rules on rely @@ -82,28 +97,16 @@ rule deny(address usr) { address other; require other != usr; - bytes32 anyBytes32; - address anyAddr; - bytes4 anyBytes4; mathint wardsOtherBefore = wards(other); - address ilkAdminsBefore = ilkAdmins(anyBytes32); - bytes32 userRolesBefore = userRoles(anyBytes32, anyAddr); - bytes32 actionsRolesBefore = actionsRoles(anyBytes32, anyAddr, anyBytes4); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - address ilkAdminsAfter = ilkAdmins(anyBytes32); - bytes32 userRolesAfter = userRoles(anyBytes32, anyAddr); - bytes32 actionsRolesAfter = actionsRoles(anyBytes32, anyAddr, anyBytes4); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert ilkAdminsAfter == ilkAdminsBefore, "deny did not keep unchanged every ilkAdmins[x]"; - assert userRolesAfter == userRolesBefore, "deny did not keep unchanged every userRoles[x][y]"; - assert actionsRolesAfter == actionsRolesBefore, "deny did not keep unchanged every actionsRoles[x][y][z]"; } // Verify revert rules on deny @@ -128,28 +131,16 @@ rule setIlkAdmin(bytes32 ilk, address usr) { bytes32 otherBytes32; require otherBytes32 != ilk; - bytes32 anyBytes32; - address anyAddr; - bytes4 anyBytes4; - mathint wardsBefore = wards(anyAddr); address ilkAdminsOtherBefore = ilkAdmins(otherBytes32); - bytes32 userRolesBefore = userRoles(anyBytes32, anyAddr); - bytes32 actionsRolesBefore = actionsRoles(anyBytes32, anyAddr, anyBytes4); setIlkAdmin(e, ilk, usr); - mathint wardsAfter = wards(anyAddr); address ilkAdminsIlkAfter = ilkAdmins(ilk); address ilkAdminsOtherAfter = ilkAdmins(otherBytes32); - bytes32 userRolesAfter = userRoles(anyBytes32, anyAddr); - bytes32 actionsRolesAfter = actionsRoles(anyBytes32, anyAddr, anyBytes4); - assert wardsAfter == wardsBefore, "setIlkAdmin did not keep unchanged every wards[x]"; assert ilkAdminsIlkAfter == usr, "setIlkAdmin did not set ilkAdmins[ilk] to usr"; assert ilkAdminsOtherAfter == ilkAdminsOtherBefore, "setIlkAdmin did not keep unchanged the rest of ilkAdmins[x]"; - assert userRolesAfter == userRolesBefore, "setIlkAdmin did not keep unchanged every userRoles[x][y]"; - assert actionsRolesAfter == actionsRolesBefore, "setIlkAdmin did not keep unchanged every actionsRoles[x][y][z]"; } // Verify revert rules on setIlkAdmin @@ -175,31 +166,19 @@ rule setUserRole(bytes32 ilk, address who, uint8 role, bool enabled) { bytes32 otherBytes32; address otherAddr; require otherBytes32 != ilk || otherAddr != who; - bytes32 anyBytes32; - address anyAddr; - bytes4 anyBytes4; - mathint wardsBefore = wards(anyAddr); - address ilkAdminsBefore = ilkAdmins(anyBytes32); bytes32 userRolesIlkWhoBefore = userRoles(ilk, who); bytes32 userRolesOtherBefore = userRoles(otherBytes32, otherAddr); - bytes32 actionsRolesBefore = actionsRoles(anyBytes32, anyAddr, anyBytes4); uint256 mask = assert_uint256(2^role); bytes32 value = enabled ? userRolesIlkWhoBefore | to_bytes32(mask) : userRolesIlkWhoBefore & to_bytes32(bitNot(mask)); setUserRole(e, ilk, who, role, enabled); - mathint wardsAfter = wards(anyAddr); - address ilkAdminsAfter = ilkAdmins(anyBytes32); bytes32 userRolesIlkWhoAfter = userRoles(ilk, who); bytes32 userRolesOtherAfter = userRoles(otherBytes32, otherAddr); - bytes32 actionsRolesAfter = actionsRoles(anyBytes32, anyAddr, anyBytes4); - assert wardsAfter == wardsBefore, "setUserRole did not keep unchanged every wards[x]"; - assert ilkAdminsAfter == ilkAdminsBefore, "setUserRole did not keep unchanged every ilkAdmins[x]"; assert userRolesIlkWhoAfter == value, "setUserRole did not set userRoles[ilk][who] by the corresponding value"; assert userRolesOtherAfter == userRolesOtherBefore, "setUserRole did not keep unchanged the rest of userRoles[x][y]"; - assert actionsRolesAfter == actionsRolesBefore, "setUserRole did not keep unchanged every actionsRoles[x][y][z]"; } // Verify revert rules on setUserRole @@ -226,12 +205,7 @@ rule setRoleAction(bytes32 ilk, uint8 role, address target, bytes4 sign, bool en address otherAddr; bytes4 otherBytes4; require otherBytes32 != ilk || otherAddr != target || otherBytes4 != sign; - bytes32 anyBytes32; - address anyAddr; - mathint wardsBefore = wards(anyAddr); - address ilkAdminsBefore = ilkAdmins(anyBytes32); - bytes32 userRolesBefore = userRoles(anyBytes32, anyAddr); bytes32 actionsRolesIlkTargetSigBefore = actionsRoles(ilk, target, sign); bytes32 actionsRolesOtherBefore = actionsRoles(otherBytes32, otherAddr, otherBytes4); uint256 mask = assert_uint256(2^role); @@ -239,15 +213,9 @@ rule setRoleAction(bytes32 ilk, uint8 role, address target, bytes4 sign, bool en setRoleAction(e, ilk, role, target, sign, enabled); - mathint wardsAfter = wards(anyAddr); - address ilkAdminsAfter = ilkAdmins(anyBytes32); - bytes32 userRolesAfter = userRoles(anyBytes32, anyAddr); bytes32 actionsRolesIlkTargetSigAfter = actionsRoles(ilk, target, sign); bytes32 actionsRolesOtherAfter = actionsRoles(otherBytes32, otherAddr, otherBytes4); - assert wardsAfter == wardsBefore, "setRoleAction did not keep unchanged every wards[x]"; - assert ilkAdminsAfter == ilkAdminsBefore, "setRoleAction did not keep unchanged every ilkAdmins[x]"; - assert userRolesAfter == userRolesBefore, "setRoleAction did not keep unchanged every userRoles[x][y]"; assert actionsRolesIlkTargetSigAfter == value, "setRoleAction did not set actionsRoles[ilk][target][sig] by the corresponding value"; assert actionsRolesOtherAfter == actionsRolesOtherBefore, "setRoleAction did not keep unchanged the rest of actionsRoles[x][y][z]"; } diff --git a/certora/AllocatorVault.spec b/certora/AllocatorVault.spec index 50d6442c..cb7d80c5 100644 --- a/certora/AllocatorVault.spec +++ b/certora/AllocatorVault.spec @@ -29,6 +29,25 @@ definition RAY() returns mathint = 10^27; definition max_int256() returns mathint = 2^255 - 1; definition divUp(mathint x, mathint y) returns mathint = x != 0 ? ((x - 1) / y) + 1 : 0; +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + + mathint wardsBefore = wards(anyAddr); + address jugBefore = jug(); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + address jugAfter = jug(); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert jugAfter != jugBefore => f.selector == sig:file(bytes32,address).selector, "jug changed in an unexpected function"; +} + // Verify correct storage changes for non reverting rely rule rely(address usr) { env e; @@ -37,17 +56,14 @@ rule rely(address usr) { require other != usr; mathint wardsOtherBefore = wards(other); - address jugBefore = jug(); rely(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - address jugAfter = jug(); assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert jugAfter == jugBefore, "rely did not keep unchanged jug"; } // Verify revert rules on rely @@ -75,17 +91,14 @@ rule deny(address usr) { require other != usr; mathint wardsOtherBefore = wards(other); - address jugBefore = jug(); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - address jugAfter = jug(); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert jugAfter == jugBefore, "deny did not keep unchanged jug"; } // Verify revert rules on deny @@ -109,16 +122,10 @@ rule deny_revert(address usr) { rule file(bytes32 what, address data) { env e; - address any; - - mathint wardsBefore = wards(any); - file(e, what, data); - mathint wardsAfter = wards(any); address jugAfter = jug(); - assert wardsAfter == wardsBefore, "file did not keep unchanged every wards[x]"; assert jugAfter == data, "file did not set jug"; } @@ -145,10 +152,6 @@ rule file_revert(bytes32 what, address data) { rule draw(uint256 wad) { env e; - address any; - - mathint wardsBefore = wards(any); - address jugBefore = jug(); mathint nstTotalSupplyBefore = nst.totalSupply(); mathint nstBalanceOfBufferBefore = nst.balanceOf(buffer()); require nstBalanceOfBufferBefore <= nstTotalSupplyBefore; @@ -160,15 +163,11 @@ rule draw(uint256 wad) { draw(e, wad); - mathint wardsAfter = wards(any); - address jugAfter = jug(); mathint nstTotalSupplyAfter = nst.totalSupply(); mathint nstBalanceOfBufferAfter = nst.balanceOf(buffer()); mathint vatInkVaultAfter; mathint vatArtVaultAfter; vatInkVaultAfter, vatArtVaultAfter = vat.urns(ilk(), currentContract); - assert wardsAfter == wardsBefore, "draw did not keep unchanged every wards[x]"; - assert jugAfter == jugBefore, "draw did not keep unchanged jug"; assert vatInkVaultAfter == vatInkVaultBefore, "draw did not keep vat.urns(ilk,vault).ink unchanged"; assert vatArtVaultAfter == vatArtVaultBefore + dart, "draw did not increase vat.urns(ilk,vault).art by dart"; assert nstBalanceOfBufferAfter == nstBalanceOfBufferBefore + wad, "draw did not increase nst.balanceOf(buffer) by wad"; @@ -230,10 +229,6 @@ rule draw_revert(uint256 wad) { rule wipe(uint256 wad) { env e; - address any; - - mathint wardsBefore = wards(any); - address jugBefore = jug(); mathint nstTotalSupplyBefore = nst.totalSupply(); mathint nstBalanceOfBufferBefore = nst.balanceOf(buffer()); require nstBalanceOfBufferBefore <= nstTotalSupplyBefore; @@ -245,15 +240,11 @@ rule wipe(uint256 wad) { wipe(e, wad); - mathint wardsAfter = wards(any); - address jugAfter = jug(); mathint nstTotalSupplyAfter = nst.totalSupply(); mathint nstBalanceOfBufferAfter = nst.balanceOf(buffer()); mathint vatInkVaultAfter; mathint vatArtVaultAfter; vatInkVaultAfter, vatArtVaultAfter = vat.urns(ilk(), currentContract); - assert wardsAfter == wardsBefore, "wipe did not keep unchanged every wards[x]"; - assert jugAfter == jugBefore, "wipe did not keep unchanged jug"; assert vatInkVaultAfter == vatInkVaultBefore, "wipe did not keep vat.urns(ilk,vault).ink unchanged"; assert vatArtVaultAfter == vatArtVaultBefore - dart, "wipe did not decrease vat.urns(ilk,vault).art by dart"; assert nstBalanceOfBufferAfter == nstBalanceOfBufferBefore - wad, "wipe did not decrease nst.balanceOf(buffer) by wad"; diff --git a/certora/funnels/DepositorUniV3.spec b/certora/funnels/DepositorUniV3.spec index 962fd550..ca02fde7 100644 --- a/certora/funnels/DepositorUniV3.spec +++ b/certora/funnels/DepositorUniV3.spec @@ -49,35 +49,50 @@ function getPoolSummary(address gem0, address gem1, uint24 fee) returns address return _poolMap[gem0][gem1][fee]; } -// Verify correct storage changes for non reverting rely -rule rely(address usr) { +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { env e; - address other; - require other != usr; address anyAddr; address anyAddr_2; uint24 anyUint24; - mathint wardsOtherBefore = wards(other); + mathint wardsBefore = wards(anyAddr); mathint cap0Before; mathint cap1Before; mathint eraBefore; mathint due0Before; mathint due1Before; mathint endBefore; cap0Before, cap1Before, eraBefore, due0Before, due1Before, endBefore = limits(anyAddr, anyAddr_2, anyUint24); + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + mathint cap0After; mathint cap1After; mathint eraAfter; mathint due0After; mathint due1After; mathint endAfter; + cap0After, cap1After, eraAfter, due0After, due1After, endAfter = limits(anyAddr, anyAddr_2, anyUint24); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert cap0After != cap0Before => f.selector == sig:setLimits(address,address,uint24,uint96,uint96,uint32).selector, "limits[x][y][z].cap0 changed in an unexpected function"; + assert cap1After != cap1Before => f.selector == sig:setLimits(address,address,uint24,uint96,uint96,uint32).selector, "limits[x][y][z].cap1 changed in an unexpected function"; + assert eraAfter != eraBefore => f.selector == sig:setLimits(address,address,uint24,uint96,uint96,uint32).selector, "limits[x][y][z].era changed in an unexpected function"; + assert due0After != due0Before => f.selector == sig:setLimits(address,address,uint24,uint96,uint96,uint32).selector || f.selector == sig:deposit(DepositorUniV3.LiquidityParams).selector || f.selector == sig:withdraw(DepositorUniV3.LiquidityParams,bool).selector, "limits[x][y][z].due0 changed in an unexpected function"; + assert due1After != due1Before => f.selector == sig:setLimits(address,address,uint24,uint96,uint96,uint32).selector || f.selector == sig:deposit(DepositorUniV3.LiquidityParams).selector || f.selector == sig:withdraw(DepositorUniV3.LiquidityParams,bool).selector, "limits[x][y][z].due1 changed in an unexpected function"; + assert endAfter != endBefore => f.selector == sig:setLimits(address,address,uint24,uint96,uint96,uint32).selector || f.selector == sig:deposit(DepositorUniV3.LiquidityParams).selector || f.selector == sig:withdraw(DepositorUniV3.LiquidityParams,bool).selector, "limits[x][y][z].end changed in an unexpected function"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + rely(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint cap0After; mathint cap1After; mathint eraAfter; mathint due0After; mathint due1After; mathint endAfter; - cap0After, cap1After, eraAfter, due0After, due1After, endAfter = limits(anyAddr, anyAddr_2, anyUint24); assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert cap0After == cap0Before, "rely did not keep unchanged every limits[x][y][z].cap0"; - assert cap1After == cap1Before, "rely did not keep unchanged every limits[x][y][z].cap1"; - assert eraAfter == eraBefore, "rely did not keep unchanged every limits[x][y][z].era"; - assert due0After == due0Before, "rely did not keep unchanged every limits[x][y][z].due0"; - assert due1After == due1Before, "rely did not keep unchanged every limits[x][y][z].due1"; - assert endAfter == endBefore, "rely did not keep unchanged every limits[x][y][z].end"; } // Verify revert rules on rely @@ -103,29 +118,16 @@ rule deny(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - uint24 anyUint24; mathint wardsOtherBefore = wards(other); - mathint cap0Before; mathint cap1Before; mathint eraBefore; mathint due0Before; mathint due1Before; mathint endBefore; - cap0Before, cap1Before, eraBefore, due0Before, due1Before, endBefore = limits(anyAddr, anyAddr_2, anyUint24); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint cap0After; mathint cap1After; mathint eraAfter; mathint due0After; mathint due1After; mathint endAfter; - cap0After, cap1After, eraAfter, due0After, due1After, endAfter = limits(anyAddr, anyAddr_2, anyUint24); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert cap0After == cap0Before, "deny did not keep unchanged every limits[x][y][z].cap0"; - assert cap1After == cap1Before, "deny did not keep unchanged every limits[x][y][z].cap1"; - assert eraAfter == eraBefore, "deny did not keep unchanged every limits[x][y][z].era"; - assert due0After == due0Before, "deny did not keep unchanged every limits[x][y][z].due0"; - assert due1After == due1Before, "deny did not keep unchanged every limits[x][y][z].due1"; - assert endAfter == endBefore, "deny did not keep unchanged every limits[x][y][z].end"; } // Verify revert rules on deny @@ -149,25 +151,21 @@ rule deny_revert(address usr) { rule setLimits(address gem0, address gem1, uint24 fee, uint96 cap0, uint96 cap1, uint32 era) { env e; - address anyAddr; address otherAddr; address otherAddr_2; uint24 otherUint24; require otherAddr != gem0 || otherAddr_2 != gem1 || otherUint24 != fee; - mathint wardsBefore = wards(anyAddr); mathint cap0OtherBefore; mathint cap1OtherBefore; mathint eraOtherBefore; mathint due0OtherBefore; mathint due1OtherBefore; mathint endOtherBefore; cap0OtherBefore, cap1OtherBefore, eraOtherBefore, due0OtherBefore, due1OtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2, otherUint24); setLimits(e, gem0, gem1, fee, cap0, cap1, era); - mathint wardsAfter = wards(anyAddr); mathint cap0Gem0Gem1FeeAfter; mathint cap1Gem0Gem1FeeAfter; mathint eraGem0Gem1FeeAfter; mathint due0Gem0Gem1FeeAfter; mathint due1Gem0Gem1FeeAfter; mathint endGem0Gem1FeeAfter; cap0Gem0Gem1FeeAfter, cap1Gem0Gem1FeeAfter, eraGem0Gem1FeeAfter, due0Gem0Gem1FeeAfter, due1Gem0Gem1FeeAfter, endGem0Gem1FeeAfter = limits(gem0, gem1, fee); mathint cap0OtherAfter; mathint cap1OtherAfter; mathint eraOtherAfter; mathint due0OtherAfter; mathint due1OtherAfter; mathint endOtherAfter; cap0OtherAfter, cap1OtherAfter, eraOtherAfter, due0OtherAfter, due1OtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2, otherUint24); - assert wardsAfter == wardsBefore, "setLimits did not keep unchanged every wards[x]"; assert cap0Gem0Gem1FeeAfter == to_mathint(cap0), "setLimits did not set limits[gem0][gem1][fee].cap0 to cap0"; assert cap1Gem0Gem1FeeAfter == to_mathint(cap1), "setLimits did not set limits[gem0][gem1][fee].cap1 to cap1"; assert eraGem0Gem1FeeAfter == to_mathint(era), "setLimits did not set limits[gem0][gem1][fee].era to era"; @@ -229,16 +227,9 @@ rule uniswapV3MintCallback(uint256 amt0Owed, uint256 amt1Owed, bytes data) { require gem0 == gem0Con; require gem1 == gem1Con; - address anyAddr; - address anyAddr_2; - uint24 anyUint24; - address buffer = buffer(); require buffer != e.msg.sender; - mathint wardsBefore = wards(anyAddr); - mathint cap0Before; mathint cap1Before; mathint eraBefore; mathint due0Before; mathint due1Before; mathint endBefore; - cap0Before, cap1Before, eraBefore, due0Before, due1Before, endBefore = limits(anyAddr, anyAddr_2, anyUint24); mathint gem0BalanceOfBufferBefore = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferBefore = gem1Con.balanceOf(buffer); mathint gem0BalanceOfSenderBefore = gem0Con.balanceOf(e.msg.sender); @@ -249,21 +240,11 @@ rule uniswapV3MintCallback(uint256 amt0Owed, uint256 amt1Owed, bytes data) { uniswapV3MintCallback(e, amt0Owed, amt1Owed, data); - mathint wardsAfter = wards(anyAddr); - mathint cap0After; mathint cap1After; mathint eraAfter; mathint due0After; mathint due1After; mathint endAfter; - cap0After, cap1After, eraAfter, due0After, due1After, endAfter = limits(anyAddr, anyAddr_2, anyUint24); mathint gem0BalanceOfBufferAfter = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferAfter = gem1Con.balanceOf(buffer); mathint gem0BalanceOfSenderAfter = gem0Con.balanceOf(e.msg.sender); mathint gem1BalanceOfSenderAfter = gem1Con.balanceOf(e.msg.sender); - assert wardsAfter == wardsBefore, "uniswapV3MintCallback did not keep unchanged every wards[x]"; - assert cap0After == cap0Before, "uniswapV3MintCallback did not keep unchanged every limits[x][y][z].cap0"; - assert cap1After == cap1Before, "uniswapV3MintCallback did not keep unchanged every limits[x][y][z].cap1"; - assert eraAfter == eraBefore, "uniswapV3MintCallback did not keep unchanged every limits[x][y][z].era"; - assert due0After == due0Before, "uniswapV3MintCallback did not keep unchanged every limits[x][y][z].due0"; - assert due1After == due1Before, "uniswapV3MintCallback did not keep unchanged every limits[x][y][z].due1"; - assert endAfter == endBefore, "uniswapV3MintCallback did not keep unchanged every limits[x][y][z].end"; assert gem0BalanceOfBufferAfter == gem0BalanceOfBufferBefore - amt0Owed, "uniswapV3MintCallback did not decrease gem0.balanceOf(buffer) by amt0Owed"; assert gem1BalanceOfBufferAfter == gem1BalanceOfBufferBefore - amt1Owed, "uniswapV3MintCallback did not decrease gem1.balanceOf(buffer) by amt1Owed"; assert gem0BalanceOfSenderAfter == gem0BalanceOfSenderBefore + amt0Owed, "uniswapV3MintCallback did not increase gem0.balanceOf(pool) by amt0Owed"; @@ -323,7 +304,6 @@ rule deposit(DepositorUniV3.LiquidityParams p) { require p.gem1 == poolCon.gem1(); require p.fee == poolCon.fee(); - address anyAddr; address otherAddr; address otherAddr_2; uint24 otherUint24; @@ -334,11 +314,12 @@ rule deposit(DepositorUniV3.LiquidityParams p) { address buffer = buffer(); require buffer != poolCon; - mathint wardsBefore = wards(anyAddr); - mathint cap0Gem0Gem1FeeBefore; mathint cap1Gem0Gem1FeeBefore; mathint eraGem0Gem1FeeBefore; mathint due0Gem0Gem1FeeBefore; mathint due1Gem0Gem1FeeBefore; mathint endGem0Gem1FeeBefore; - cap0Gem0Gem1FeeBefore, cap1Gem0Gem1FeeBefore, eraGem0Gem1FeeBefore, due0Gem0Gem1FeeBefore, due1Gem0Gem1FeeBefore, endGem0Gem1FeeBefore = limits(p.gem0, p.gem1, p.fee); - mathint cap0OtherBefore; mathint cap1OtherBefore; mathint eraOtherBefore; mathint due0OtherBefore; mathint due1OtherBefore; mathint endOtherBefore; - cap0OtherBefore, cap1OtherBefore, eraOtherBefore, due0OtherBefore, due1OtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2, otherUint24); + mathint a; mathint b; mathint c; + + mathint cap0Gem0Gem1Fee; mathint cap1Gem0Gem1Fee; mathint eraGem0Gem1Fee; mathint due0Gem0Gem1FeeBefore; mathint due1Gem0Gem1FeeBefore; mathint endGem0Gem1FeeBefore; + cap0Gem0Gem1Fee, cap1Gem0Gem1Fee, eraGem0Gem1Fee, due0Gem0Gem1FeeBefore, due1Gem0Gem1FeeBefore, endGem0Gem1FeeBefore = limits(p.gem0, p.gem1, p.fee); + mathint due0OtherBefore; mathint due1OtherBefore; mathint endOtherBefore; + a, b, c, due0OtherBefore, due1OtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2, otherUint24); mathint gem0BalanceOfBufferBefore = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferBefore = gem1Con.balanceOf(buffer); mathint gem0BalanceOfPoolBefore = gem0Con.balanceOf(poolCon); @@ -355,30 +336,22 @@ rule deposit(DepositorUniV3.LiquidityParams p) { mathint retLiq; mathint retAmt0; mathint retAmt1; retLiq, retAmt0, retAmt1 = deposit(e, p); - mathint wardsAfter = wards(anyAddr); - mathint cap0Gem0Gem1FeeAfter; mathint cap1Gem0Gem1FeeAfter; mathint eraGem0Gem1FeeAfter; mathint due0Gem0Gem1FeeAfter; mathint due1Gem0Gem1FeeAfter; mathint endGem0Gem1FeeAfter; - cap0Gem0Gem1FeeAfter, cap1Gem0Gem1FeeAfter, eraGem0Gem1FeeAfter, due0Gem0Gem1FeeAfter, due1Gem0Gem1FeeAfter, endGem0Gem1FeeAfter = limits(p.gem0, p.gem1, p.fee); - mathint cap0OtherAfter; mathint cap1OtherAfter; mathint eraOtherAfter; mathint due0OtherAfter; mathint due1OtherAfter; mathint endOtherAfter; - cap0OtherAfter, cap1OtherAfter, eraOtherAfter, due0OtherAfter, due1OtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2, otherUint24); + mathint due0Gem0Gem1FeeAfter; mathint due1Gem0Gem1FeeAfter; mathint endGem0Gem1FeeAfter; + a, b, c, due0Gem0Gem1FeeAfter, due1Gem0Gem1FeeAfter, endGem0Gem1FeeAfter = limits(p.gem0, p.gem1, p.fee); + mathint due0OtherAfter; mathint due1OtherAfter; mathint endOtherAfter; + a, b, c, due0OtherAfter, due1OtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2, otherUint24); mathint gem0BalanceOfBufferAfter = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferAfter = gem1Con.balanceOf(buffer); mathint gem0BalanceOfPoolAfter = gem0Con.balanceOf(poolCon); mathint gem1BalanceOfPoolAfter = gem1Con.balanceOf(poolCon); - mathint expectedDue0 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap0Gem0Gem1FeeBefore : due0Gem0Gem1FeeBefore) - amt0; - mathint expectedDue1 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap1Gem0Gem1FeeBefore : due1Gem0Gem1FeeBefore) - amt1; - mathint expectedEnd = to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? e.block.timestamp + eraGem0Gem1FeeBefore : endGem0Gem1FeeBefore; + mathint expectedDue0 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap0Gem0Gem1Fee : due0Gem0Gem1FeeBefore) - amt0; + mathint expectedDue1 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap1Gem0Gem1Fee : due1Gem0Gem1FeeBefore) - amt1; + mathint expectedEnd = to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? e.block.timestamp + eraGem0Gem1Fee : endGem0Gem1FeeBefore; - assert wardsAfter == wardsBefore, "deposit did not keep unchanged every wards[x]"; - assert cap0Gem0Gem1FeeAfter == cap0Gem0Gem1FeeBefore, "deposit did not keep unchanged limits[gem0][gem1][fee].cap0"; - assert cap1Gem0Gem1FeeAfter == cap1Gem0Gem1FeeBefore, "deposit did not keep unchanged limits[gem0][gem1][fee].cap1"; - assert eraGem0Gem1FeeAfter == eraGem0Gem1FeeBefore, "deposit did not keep unchanged limits[gem0][gem1][fee].era"; assert due0Gem0Gem1FeeAfter == expectedDue0, "deposit did not set limits[gem0][gem1][fee].due0 to the expected value"; assert due1Gem0Gem1FeeAfter == expectedDue1, "deposit did not set limits[gem0][gem1][fee].due1 to the expected value"; assert endGem0Gem1FeeAfter == expectedEnd, "deposit did not set limits[gem0][gem1][fee].end to the expected value"; - assert cap0OtherAfter == cap0OtherBefore, "deposit did not keep unchanged the rest of limits[x][y][z].cap0"; - assert cap1OtherAfter == cap1OtherBefore, "deposit did not keep unchanged the rest of limits[x][y][z].cap1"; - assert eraOtherAfter == eraOtherBefore, "deposit did not keep unchanged the rest of limits[x][y][z].era"; assert due0OtherAfter == due0OtherBefore, "deposit did not keep unchanged the rest of limits[x][y][z].due0"; assert due1OtherAfter == due1OtherBefore, "deposit did not keep unchanged the rest of limits[x][y][z].due1"; assert endOtherAfter == endOtherBefore, "deposit did not keep unchanged the rest of limits[x][y][z].end"; @@ -462,7 +435,6 @@ rule withdraw(DepositorUniV3.LiquidityParams p, bool takeFees) { require poolCon.random2() >= poolCon.random0(); require poolCon.random3() >= poolCon.random1(); - address anyAddr; address otherAddr; address otherAddr_2; uint24 otherUint24; @@ -473,11 +445,12 @@ rule withdraw(DepositorUniV3.LiquidityParams p, bool takeFees) { address buffer = buffer(); require buffer != poolCon; - mathint wardsBefore = wards(anyAddr); - mathint cap0Gem0Gem1FeeBefore; mathint cap1Gem0Gem1FeeBefore; mathint eraGem0Gem1FeeBefore; mathint due0Gem0Gem1FeeBefore; mathint due1Gem0Gem1FeeBefore; mathint endGem0Gem1FeeBefore; - cap0Gem0Gem1FeeBefore, cap1Gem0Gem1FeeBefore, eraGem0Gem1FeeBefore, due0Gem0Gem1FeeBefore, due1Gem0Gem1FeeBefore, endGem0Gem1FeeBefore = limits(p.gem0, p.gem1, p.fee); + mathint a; mathint b; mathint c; + + mathint cap0Gem0Gem1Fee; mathint cap1Gem0Gem1Fee; mathint eraGem0Gem1Fee; mathint due0Gem0Gem1FeeBefore; mathint due1Gem0Gem1FeeBefore; mathint endGem0Gem1FeeBefore; + cap0Gem0Gem1Fee, cap1Gem0Gem1Fee, eraGem0Gem1Fee, due0Gem0Gem1FeeBefore, due1Gem0Gem1FeeBefore, endGem0Gem1FeeBefore = limits(p.gem0, p.gem1, p.fee); mathint cap0OtherBefore; mathint cap1OtherBefore; mathint eraOtherBefore; mathint due0OtherBefore; mathint due1OtherBefore; mathint endOtherBefore; - cap0OtherBefore, cap1OtherBefore, eraOtherBefore, due0OtherBefore, due1OtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2, otherUint24); + a, b, c, due0OtherBefore, due1OtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2, otherUint24); mathint gem0BalanceOfBufferBefore = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferBefore = gem1Con.balanceOf(buffer); mathint gem0BalanceOfPoolBefore = gem0Con.balanceOf(poolCon); @@ -496,30 +469,22 @@ rule withdraw(DepositorUniV3.LiquidityParams p, bool takeFees) { mathint retLiq; mathint retAmt0; mathint retAmt1; mathint retFees0; mathint retFees1; retLiq, retAmt0, retAmt1, retFees0, retFees1 = withdraw(e, p, takeFees); - mathint wardsAfter = wards(anyAddr); - mathint cap0Gem0Gem1FeeAfter; mathint cap1Gem0Gem1FeeAfter; mathint eraGem0Gem1FeeAfter; mathint due0Gem0Gem1FeeAfter; mathint due1Gem0Gem1FeeAfter; mathint endGem0Gem1FeeAfter; - cap0Gem0Gem1FeeAfter, cap1Gem0Gem1FeeAfter, eraGem0Gem1FeeAfter, due0Gem0Gem1FeeAfter, due1Gem0Gem1FeeAfter, endGem0Gem1FeeAfter = limits(p.gem0, p.gem1, p.fee); - mathint cap0OtherAfter; mathint cap1OtherAfter; mathint eraOtherAfter; mathint due0OtherAfter; mathint due1OtherAfter; mathint endOtherAfter; - cap0OtherAfter, cap1OtherAfter, eraOtherAfter, due0OtherAfter, due1OtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2, otherUint24); + mathint due0Gem0Gem1FeeAfter; mathint due1Gem0Gem1FeeAfter; mathint endGem0Gem1FeeAfter; + a, b, c, due0Gem0Gem1FeeAfter, due1Gem0Gem1FeeAfter, endGem0Gem1FeeAfter = limits(p.gem0, p.gem1, p.fee); + mathint due0OtherAfter; mathint due1OtherAfter; mathint endOtherAfter; + a, b, c, due0OtherAfter, due1OtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2, otherUint24); mathint gem0BalanceOfBufferAfter = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferAfter = gem1Con.balanceOf(buffer); mathint gem0BalanceOfPoolAfter = gem0Con.balanceOf(poolCon); mathint gem1BalanceOfPoolAfter = gem1Con.balanceOf(poolCon); - mathint expectedDue0 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap0Gem0Gem1FeeBefore : due0Gem0Gem1FeeBefore) - amt0; - mathint expectedDue1 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap1Gem0Gem1FeeBefore : due1Gem0Gem1FeeBefore) - amt1; - mathint expectedEnd = to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? e.block.timestamp + eraGem0Gem1FeeBefore : endGem0Gem1FeeBefore; + mathint expectedDue0 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap0Gem0Gem1Fee : due0Gem0Gem1FeeBefore) - amt0; + mathint expectedDue1 = (to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? cap1Gem0Gem1Fee : due1Gem0Gem1FeeBefore) - amt1; + mathint expectedEnd = to_mathint(e.block.timestamp) >= endGem0Gem1FeeBefore ? e.block.timestamp + eraGem0Gem1Fee : endGem0Gem1FeeBefore; - assert wardsAfter == wardsBefore, "withdraw did not keep unchanged every wards[x]"; - assert cap0Gem0Gem1FeeAfter == cap0Gem0Gem1FeeBefore, "withdraw did not keep unchanged limits[gem0][gem1][fee].cap0"; - assert cap1Gem0Gem1FeeAfter == cap1Gem0Gem1FeeBefore, "withdraw did not keep unchanged limits[gem0][gem1][fee].cap1"; - assert eraGem0Gem1FeeAfter == eraGem0Gem1FeeBefore, "withdraw did not keep unchanged limits[gem0][gem1][fee].era"; assert due0Gem0Gem1FeeAfter == expectedDue0, "withdraw did not set limits[gem0][gem1][fee].due0 to the expected value"; assert due1Gem0Gem1FeeAfter == expectedDue1, "withdraw did not set limits[gem0][gem1][fee].due1 to the expected value"; assert endGem0Gem1FeeAfter == expectedEnd, "withdraw did not set limits[gem0][gem1][fee].end to the expected value"; - assert cap0OtherAfter == cap0OtherBefore, "withdraw did not keep unchanged the rest of limits[x][y][z].cap0"; - assert cap1OtherAfter == cap1OtherBefore, "withdraw did not keep unchanged the rest of limits[x][y][z].cap1"; - assert eraOtherAfter == eraOtherBefore, "withdraw did not keep unchanged the rest of limits[x][y][z].era"; assert due0OtherAfter == due0OtherBefore, "withdraw did not keep unchanged the rest of limits[x][y][z].due0"; assert due1OtherAfter == due1OtherBefore, "withdraw did not keep unchanged the rest of limits[x][y][z].due1"; assert endOtherAfter == endOtherBefore, "withdraw did not keep unchanged the rest of limits[x][y][z].end"; @@ -609,9 +574,6 @@ rule collect(DepositorUniV3.CollectParams p) { address buffer = buffer(); require buffer != poolCon; - mathint wardsBefore = wards(anyAddr); - mathint cap0Before; mathint cap1Before; mathint eraBefore; mathint due0Before; mathint due1Before; mathint endBefore; - cap0Before, cap1Before, eraBefore, due0Before, due1Before, endBefore = limits(anyAddr, anyAddr_2, anyUint24); mathint gem0BalanceOfBufferBefore = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferBefore = gem1Con.balanceOf(buffer); mathint gem0BalanceOfPoolBefore = gem0Con.balanceOf(poolCon); @@ -626,21 +588,11 @@ rule collect(DepositorUniV3.CollectParams p) { mathint retFees0; mathint retFees1; retFees0, retFees1 = collect(e, p); - mathint wardsAfter = wards(anyAddr); - mathint cap0After; mathint cap1After; mathint eraAfter; mathint due0After; mathint due1After; mathint endAfter; - cap0After, cap1After, eraAfter, due0After, due1After, endAfter = limits(anyAddr, anyAddr_2, anyUint24); mathint gem0BalanceOfBufferAfter = gem0Con.balanceOf(buffer); mathint gem1BalanceOfBufferAfter = gem1Con.balanceOf(buffer); mathint gem0BalanceOfPoolAfter = gem0Con.balanceOf(poolCon); mathint gem1BalanceOfPoolAfter = gem1Con.balanceOf(poolCon); - assert wardsAfter == wardsBefore, "collect did not keep unchanged every wards[x]"; - assert cap0After == cap0Before, "collect did not keep unchanged every limits[x][y][z].cap0"; - assert cap1After == cap1Before, "collect did not keep unchanged every limits[x][y][z].cap1"; - assert eraAfter == eraBefore, "collect did not keep unchanged every limits[x][y][z].era"; - assert due0After == due0Before, "collect did not keep unchanged every limits[x][y][z].due0"; - assert due1After == due1Before, "collect did not keep unchanged every limits[x][y][z].due1"; - assert endAfter == endBefore, "collect did not keep unchanged every limits[x][y][z].end"; assert gem0BalanceOfBufferAfter == gem0BalanceOfBufferBefore + fees0, "collect did not increase gem0.balanceOf(buffer) by fees0"; assert gem1BalanceOfBufferAfter == gem1BalanceOfBufferBefore + fees1, "collect did not increase gem1.balanceOf(buffer) by fees1"; assert gem0BalanceOfPoolAfter == gem0BalanceOfPoolBefore - fees0, "collect did not decrease gem0.balanceOf(pool) by fees0"; diff --git a/certora/funnels/Swapper.spec b/certora/funnels/Swapper.spec index 80948028..7d1f3c2b 100644 --- a/certora/funnels/Swapper.spec +++ b/certora/funnels/Swapper.spec @@ -18,32 +18,47 @@ methods { function _.transferFrom(address, address, uint256) external => DISPATCHER(true) UNRESOLVED; } +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + address anyAddr_2; + + mathint wardsBefore = wards(anyAddr); + mathint capBefore; mathint eraBefore; mathint dueBefore; mathint endBefore; + capBefore, eraBefore, dueBefore, endBefore = limits(anyAddr, anyAddr_2); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + mathint capAfter; mathint eraAfter; mathint dueAfter; mathint endAfter; + capAfter, eraAfter, dueAfter, endAfter = limits(anyAddr, anyAddr_2); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert capAfter != capBefore => f.selector == sig:setLimits(address,address,uint96,uint32).selector, "limits[x][y].cap changed in an unexpected function"; + assert eraAfter != eraBefore => f.selector == sig:setLimits(address,address,uint96,uint32).selector, "limits[x][y].era changed in an unexpected function"; + assert dueAfter != dueBefore => f.selector == sig:setLimits(address,address,uint96,uint32).selector || f.selector == sig:swap(address,address,uint256,uint256,address,bytes).selector, "limits[x][y].due changed in an unexpected function"; + assert endAfter != endBefore => f.selector == sig:setLimits(address,address,uint96,uint32).selector || f.selector == sig:swap(address,address,uint256,uint256,address,bytes).selector, "limits[x][y].end changed in an unexpected function"; +} + // Verify correct storage changes for non reverting rely rule rely(address usr) { env e; address other; require other != usr; - address anyAddr; - address anyAddr_2; mathint wardsOtherBefore = wards(other); - mathint capBefore; mathint eraBefore; mathint dueBefore; mathint endBefore; - capBefore, eraBefore, dueBefore, endBefore = limits(anyAddr, anyAddr_2); rely(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint capAfter; mathint eraAfter; mathint dueAfter; mathint endAfter; - capAfter, eraAfter, dueAfter, endAfter = limits(anyAddr, anyAddr_2); assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert capAfter == capBefore, "rely did not keep unchanged every limits[x][y].cap"; - assert eraAfter == eraBefore, "rely did not keep unchanged every limits[x][y].era"; - assert dueAfter == dueBefore, "rely did not keep unchanged every limits[x][y].due"; - assert endAfter == endBefore, "rely did not keep unchanged every limits[x][y].end"; } // Verify revert rules on rely @@ -69,26 +84,16 @@ rule deny(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; mathint wardsOtherBefore = wards(other); - mathint capBefore; mathint eraBefore; mathint dueBefore; mathint endBefore; - capBefore, eraBefore, dueBefore, endBefore = limits(anyAddr, anyAddr_2); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint capAfter; mathint eraAfter; mathint dueAfter; mathint endAfter; - capAfter, eraAfter, dueAfter, endAfter = limits(anyAddr, anyAddr_2); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert capAfter == capBefore, "deny did not keep unchanged every limits[x][y].cap"; - assert eraAfter == eraBefore, "deny did not keep unchanged every limits[x][y].era"; - assert dueAfter == dueBefore, "deny did not keep unchanged every limits[x][y].due"; - assert endAfter == endBefore, "deny did not keep unchanged every limits[x][y].end"; } // Verify revert rules on deny @@ -112,24 +117,20 @@ rule deny_revert(address usr) { rule setLimits(address src, address dst, uint96 cap, uint32 era) { env e; - address anyAddr; address otherAddr; address otherAddr_2; require otherAddr != src || otherAddr_2 != dst; - mathint wardsBefore = wards(anyAddr); mathint capOtherBefore; mathint eraOtherBefore; mathint dueOtherBefore; mathint endOtherBefore; capOtherBefore, eraOtherBefore, dueOtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2); setLimits(e, src, dst, cap, era); - mathint wardsAfter = wards(anyAddr); mathint capSrcDstAfter; mathint eraSrcDstAfter; mathint dueSrcDstAfter; mathint endSrcDstAfter; capSrcDstAfter, eraSrcDstAfter, dueSrcDstAfter, endSrcDstAfter = limits(src, dst); mathint capOtherAfter; mathint eraOtherAfter; mathint dueOtherAfter; mathint endOtherAfter; capOtherAfter, eraOtherAfter, dueOtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2); - assert wardsAfter == wardsBefore, "setLimits did not keep unchanged every wards[x]"; assert capSrcDstAfter == to_mathint(cap), "setLimits did not set limits[src][dst].cap to cap"; assert eraSrcDstAfter == to_mathint(era), "setLimits did not set limits[src][dst].era to era"; assert dueSrcDstAfter == 0, "setLimits did not set limits[src][dst].due to 0"; @@ -176,11 +177,13 @@ rule swap(address src, address dst, uint256 amt, uint256 minOut, address callee, require buffer != currentContract; require buffer != callee; + mathint a; mathint b; + mathint wardsBefore = wards(anyAddr); - mathint capBefore; mathint eraBefore; mathint dueBefore; mathint endBefore; - capBefore, eraBefore, dueBefore, endBefore = limits(src, dst); - mathint capOtherBefore; mathint eraOtherBefore; mathint dueOtherBefore; mathint endOtherBefore; - capOtherBefore, eraOtherBefore, dueOtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2); + mathint cap; mathint era; mathint dueBefore; mathint endBefore; + cap, era, dueBefore, endBefore = limits(src, dst); + mathint dueOtherBefore; mathint endOtherBefore; + a, b, dueOtherBefore, endOtherBefore = limits(otherAddr, otherAddr_2); mathint srcBalanceOfBufferBefore = srcCon.balanceOf(e, buffer); mathint dstBalanceOfBufferBefore = dstCon.balanceOf(e, buffer); @@ -188,24 +191,18 @@ rule swap(address src, address dst, uint256 amt, uint256 minOut, address callee, swap(e, src, dst, amt, minOut, callee, data); - mathint wardsAfter = wards(anyAddr); - mathint capAfter; mathint eraAfter; mathint dueAfter; mathint endAfter; - capAfter, eraAfter, dueAfter, endAfter = limits(src, dst); - mathint capOtherAfter; mathint eraOtherAfter; mathint dueOtherAfter; mathint endOtherAfter; - capOtherAfter, eraOtherAfter, dueOtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2); + mathint dueAfter; mathint endAfter; + a, b, dueAfter, endAfter = limits(src, dst); + mathint dueOtherAfter; mathint endOtherAfter; + a, b, dueOtherAfter, endOtherAfter = limits(otherAddr, otherAddr_2); - mathint expectedDue = (to_mathint(e.block.timestamp) >= endBefore ? capBefore : dueBefore) - amt; - mathint expectedEnd = to_mathint(e.block.timestamp) >= endBefore ? e.block.timestamp + eraBefore : endBefore; + mathint expectedDue = (to_mathint(e.block.timestamp) >= endBefore ? cap : dueBefore) - amt; + mathint expectedEnd = to_mathint(e.block.timestamp) >= endBefore ? e.block.timestamp + era : endBefore; mathint srcBalanceOfBufferAfter = srcCon.balanceOf(e, buffer); mathint dstBalanceOfBufferAfter = dstCon.balanceOf(e, buffer); - assert wardsAfter == wardsBefore, "swap did not keep unchanged every wards[x]"; - assert capAfter == capBefore, "swap did not keep unchanged limits[src][dst].cap"; - assert eraAfter == eraBefore, "swap did not keep unchanged limits[src][dst].era"; assert dueAfter == expectedDue, "swap did not set limits[src][dst].due to expected value"; assert endAfter == expectedEnd, "swap did not set limits[src][dst].end to expected value"; - assert capOtherAfter == capOtherBefore, "swap did not keep unchanged the rest of limits[x][y].cap"; - assert eraOtherAfter == eraOtherBefore, "swap did not keep unchanged the rest of limits[x][y].era"; assert dueOtherAfter == dueOtherBefore, "swap did not keep unchanged the rest of limits[x][y].due"; assert endOtherAfter == endOtherBefore, "swap did not keep unchanged the rest of limits[x][y].end"; assert srcBalanceOfBufferAfter == srcBalanceOfBufferBefore - amt, "swap did not decrease src.balanceOf(buffer) by amt"; diff --git a/certora/funnels/automation/ConduitMover.spec b/certora/funnels/automation/ConduitMover.spec index fb6884ec..d137d661 100644 --- a/certora/funnels/automation/ConduitMover.spec +++ b/certora/funnels/automation/ConduitMover.spec @@ -44,36 +44,51 @@ function depositSummary(address addr, bytes32 ilk, address gem, uint256 amount) return true; } -// Verify correct storage changes for non reverting rely -rule rely(address usr) { +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { env e; - address other; - require other != usr; address anyAddr; address anyAddr_2; address anyAddr_3; - mathint wardsOtherBefore = wards(other); + mathint wardsBefore = wards(anyAddr); mathint budsBefore = buds(anyAddr); mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; numBefore, hopBefore, zzzBefore, lotBefore = configs(anyAddr, anyAddr_2, anyAddr_3); - rely(e, usr); + calldataarg args; + f(e, args); - mathint wardsUsrAfter = wards(usr); - mathint wardsOtherAfter = wards(other); + mathint wardsAfter = wards(anyAddr); mathint budsAfter = buds(anyAddr); mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; numAfter, hopAfter, zzzAfter, lotAfter = configs(anyAddr, anyAddr_2, anyAddr_3); + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert budsAfter != budsBefore => f.selector == sig:kiss(address).selector || f.selector == sig:diss(address).selector, "buds[x] changed in an unexpected function"; + assert numAfter != numBefore => f.selector == sig:setConfig(address,address,address,uint64,uint32,uint128).selector || f.selector == sig:move(address,address,address).selector, "configs[x][y][z].num changed in an unexpected function"; + assert hopAfter != hopBefore => f.selector == sig:setConfig(address,address,address,uint64,uint32,uint128).selector, "configs[x][y][z].hop changed in an unexpected function"; + assert zzzAfter != zzzBefore => f.selector == sig:setConfig(address,address,address,uint64,uint32,uint128).selector || f.selector == sig:move(address,address,address).selector, "configs[x][y][z].zzz changed in an unexpected function"; + assert lotAfter != lotBefore => f.selector == sig:setConfig(address,address,address,uint64,uint32,uint128).selector, "configs[x][y][z].lot changed in an unexpected function"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert budsAfter == budsBefore, "rely did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "rely did not keep unchanged every configs[x][y][z].num"; - assert hopAfter == hopBefore, "rely did not keep unchanged every configs[x][y][z].hop"; - assert zzzAfter == zzzBefore, "rely did not keep unchanged every configs[x][y][z].zzz"; - assert lotAfter == lotBefore, "rely did not keep unchanged every configs[x][y][z].lot"; } // Verify revert rules on rely @@ -98,30 +113,16 @@ rule deny(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - address anyAddr_3; mathint wardsOtherBefore = wards(other); - mathint budsBefore = buds(anyAddr); - mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; - numBefore, hopBefore, zzzBefore, lotBefore = configs(anyAddr, anyAddr_2, anyAddr_3); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint budsAfter = buds(anyAddr); - mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; - numAfter, hopAfter, zzzAfter, lotAfter = configs(anyAddr, anyAddr_2, anyAddr_3); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert budsAfter == budsBefore, "deny did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "deny did not keep unchanged every configs[x][y][z].num"; - assert hopAfter == hopBefore, "deny did not keep unchanged every configs[x][y][z].hop"; - assert zzzAfter == zzzBefore, "deny did not keep unchanged every configs[x][y][z].zzz"; - assert lotAfter == lotBefore, "deny did not keep unchanged every configs[x][y][z].lot"; } // Verify revert rules on deny @@ -146,30 +147,16 @@ rule kiss(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - address anyAddr_3; - mathint wardsBefore = wards(anyAddr); mathint budsOtherBefore = buds(other); - mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; - numBefore, hopBefore, zzzBefore, lotBefore = configs(anyAddr, anyAddr_2, anyAddr_3); kiss(e, usr); - mathint wardsAfter = wards(anyAddr); mathint budsUsrAfter = buds(usr); mathint budsOtherAfter = buds(other); - mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; - numAfter, hopAfter, zzzAfter, lotAfter = configs(anyAddr, anyAddr_2, anyAddr_3); - assert wardsAfter == wardsBefore, "kiss did not keep unchanged every wards[x]"; assert budsUsrAfter == 1, "kiss did not set the buds"; assert budsOtherAfter == budsOtherBefore, "kiss did not keep unchanged the rest of buds[x]"; - assert numAfter == numBefore, "kiss did not keep unchanged every configs[x][y][z].num"; - assert hopAfter == hopBefore, "kiss did not keep unchanged every configs[x][y][z].hop"; - assert zzzAfter == zzzBefore, "kiss did not keep unchanged every configs[x][y][z].zzz"; - assert lotAfter == lotBefore, "kiss did not keep unchanged every configs[x][y][z].lot"; } // Verify revert rules on kiss @@ -194,30 +181,16 @@ rule diss(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - address anyAddr_3; - mathint wardsBefore = wards(anyAddr); mathint budsOtherBefore = buds(other); - mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; - numBefore, hopBefore, zzzBefore, lotBefore = configs(anyAddr, anyAddr_2, anyAddr_3); diss(e, usr); - mathint wardsAfter = wards(anyAddr); mathint budsUsrAfter = buds(usr); mathint budsOtherAfter = buds(other); - mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; - numAfter, hopAfter, zzzAfter, lotAfter = configs(anyAddr, anyAddr_2, anyAddr_3); - assert wardsAfter == wardsBefore, "diss did not keep unchanged every wards[x]"; assert budsUsrAfter == 0, "diss did not set the buds"; assert budsOtherAfter == budsOtherBefore, "diss did not keep unchanged the rest of buds[x]"; - assert numAfter == numBefore, "diss did not keep unchanged every configs[x][y][z].num"; - assert hopAfter == hopBefore, "diss did not keep unchanged every configs[x][y][z].hop"; - assert zzzAfter == zzzBefore, "diss did not keep unchanged every configs[x][y][z].zzz"; - assert lotAfter == lotBefore, "diss did not keep unchanged every configs[x][y][z].lot"; } // Verify revert rules on diss @@ -240,28 +213,21 @@ rule diss_revert(address usr) { rule setConfig(address from, address to, address gem, uint64 num, uint32 hop, uint128 lot) { env e; - address anyAddr; address otherAddr; address otherAddr_2; address otherAddr_3; require otherAddr != from || otherAddr_2 != to || otherAddr_3 != gem; - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); mathint numOtherBefore; mathint hopOtherBefore; mathint zzzOtherBefore; mathint lotOtherBefore; numOtherBefore, hopOtherBefore, zzzOtherBefore, lotOtherBefore = configs(otherAddr, otherAddr_2, otherAddr_3); setConfig(e, from, to, gem, num, hop, lot); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); mathint numFromToGemAfter; mathint hopFromToGemAfter; mathint zzzFromToGemAfter; mathint lotFromToGemAfter; numFromToGemAfter, hopFromToGemAfter, zzzFromToGemAfter, lotFromToGemAfter = configs(from, to, gem); mathint numOtherAfter; mathint hopOtherAfter; mathint zzzOtherAfter; mathint lotOtherAfter; numOtherAfter, hopOtherAfter, zzzOtherAfter, lotOtherAfter = configs(otherAddr, otherAddr_2, otherAddr_3); - assert wardsAfter == wardsBefore, "setConfig did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "setConfig did not keep unchanged every buds[x]"; assert numFromToGemAfter == to_mathint(num), "setConfig did not set configs[from][to][gem].num to num"; assert hopFromToGemAfter == to_mathint(hop), "setConfig did not set configs[from][to][gem].hop to hop"; assert zzzFromToGemAfter == 0, "setConfig did not set configs[from][to][gem].zzz to 0"; @@ -292,7 +258,6 @@ rule setConfig_revert(address from, address to, address gem, uint64 num, uint32 rule move(address from, address to, address gem) { env e; - address anyAddr; address otherAddr; address otherAddr_2; address otherAddr_3; @@ -302,12 +267,12 @@ rule move(address from, address to, address gem) { address buffer = buffer(); - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); - mathint numFromToGemBefore; mathint hopFromToGemBefore; mathint zzzFromToGemBefore; mathint lotFromToGemBefore; - numFromToGemBefore, hopFromToGemBefore, zzzFromToGemBefore, lotFromToGemBefore = configs(from, to, gem); - mathint numOtherBefore; mathint hopOtherBefore; mathint zzzOtherBefore; mathint lotOtherBefore; - numOtherBefore, hopOtherBefore, zzzOtherBefore, lotOtherBefore = configs(otherAddr, otherAddr_2, otherAddr_3); + mathint a; mathint b; + + mathint numFromToGemBefore; mathint lotFromToGem; + numFromToGemBefore, a, b, lotFromToGem = configs(from, to, gem); + mathint numOtherBefore; mathint zzzOtherBefore; + numOtherBefore, a, zzzOtherBefore, b = configs(otherAddr, otherAddr_2, otherAddr_3); bytes32 withdrawIlkBefore = withdrawIlk; address withdrawGemBefore = withdrawGem; @@ -321,28 +286,20 @@ rule move(address from, address to, address gem) { move(e, from, to, gem); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); - mathint numFromToGemAfter; mathint hopFromToGemAfter; mathint zzzFromToGemAfter; mathint lotFromToGemAfter; - numFromToGemAfter, hopFromToGemAfter, zzzFromToGemAfter, lotFromToGemAfter = configs(from, to, gem); - mathint numOtherAfter; mathint hopOtherAfter; mathint zzzOtherAfter; mathint lotOtherAfter; - numOtherAfter, hopOtherAfter, zzzOtherAfter, lotOtherAfter = configs(otherAddr, otherAddr_2, otherAddr_3); + mathint numFromToGemAfter; mathint zzzFromToGemAfter; + numFromToGemAfter, a, zzzFromToGemAfter, b = configs(from, to, gem); + mathint numOtherAfter; mathint zzzOtherAfter; + numOtherAfter, a, zzzOtherAfter, b = configs(otherAddr, otherAddr_2, otherAddr_3); - assert wardsAfter == wardsBefore, "move did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "move did not keep unchanged every buds[x]"; assert numFromToGemAfter == numFromToGemBefore - 1, "move did not decrease configs[from][to][gem].num by 1"; - assert hopFromToGemAfter == hopFromToGemBefore, "move did not keep unchanged configs[from][to][gem].hop"; assert zzzFromToGemAfter == to_mathint(e.block.timestamp), "move did not set configs[from][to][gem].zzz to block.timestamp"; - assert lotFromToGemAfter == lotFromToGemBefore, "move did not keep unchanged configs[from][to][gem].lot"; assert numOtherAfter == numOtherBefore, "move did not keep unchanged the rest of configs[x][y][z].num"; - assert hopOtherAfter == hopOtherBefore, "move did not keep unchanged the rest of configs[x][y][z].hop"; assert zzzOtherAfter == zzzOtherBefore, "move did not keep unchanged the rest of configs[x][y][z].zzz"; - assert lotOtherAfter == lotOtherBefore, "move did not keep unchanged the rest of configs[x][y][z].lot"; assert from != buffer => withdrawCounter == withdrawCounterBefore + 1, "move did not execute exactly one withdraw external call"; assert from != buffer => withdrawAddr == from, "move did not execute the withdraw external call to the correct 'from' contract"; assert from != buffer => withdrawIlk == ilk(), "move did not pass the correct ilk to the withdraw external call"; assert from != buffer => withdrawGem == gem, "move did not pass the correct gen to the withdraw external call"; - assert from != buffer => to_mathint(withdrawAmount) == lotFromToGemBefore, "move did not pass the correct amount to the withdraw external call"; + assert from != buffer => to_mathint(withdrawAmount) == lotFromToGem, "move did not pass the correct amount to the withdraw external call"; assert from == buffer => withdrawCounter == withdrawCounterBefore, "move did execute one or more withdraw external call when it did not correspond"; assert from == buffer => withdrawIlk == withdrawIlkBefore, "move did execute the withdraw external call when it did not correspond"; assert from == buffer => withdrawGem == withdrawGemBefore, "move did execute the withdraw external call when it did not correspond 2"; @@ -351,7 +308,7 @@ rule move(address from, address to, address gem) { assert to != buffer => depositAddr == to, "move did not execute the deposit external call to the correct 'to' contract"; assert to != buffer => depositIlk == ilk(), "move did not pass the correct ilk to the deposit external call"; assert to != buffer => depositGem == gem, "move did not pass the correct gen to the deposit external call"; - assert to != buffer => to_mathint(depositAmount) == lotFromToGemBefore, "move did not pass the correct amount to the deposit external call"; + assert to != buffer => to_mathint(depositAmount) == lotFromToGem, "move did not pass the correct amount to the deposit external call"; assert to == buffer => depositCounter == depositCounterBefore, "move did execute one or more deposit external call when it did not correspond"; assert to == buffer => depositIlk == depositIlkBefore, "move did execute the deposit external call when it did not correspond"; assert to == buffer => depositGem == depositGemBefore, "move did execute the deposit external call when it did not correspond 2"; diff --git a/certora/funnels/automation/StableDepositorUniV3.spec b/certora/funnels/automation/StableDepositorUniV3.spec index 51d82710..62b496f0 100644 --- a/certora/funnels/automation/StableDepositorUniV3.spec +++ b/certora/funnels/automation/StableDepositorUniV3.spec @@ -92,41 +92,56 @@ function collectSummary(address addr, DepositorUniV3Like.CollectParams p) return return (retValue2, retValue3); } -// Verify correct storage changes for non reverting rely -rule rely(address usr) { +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { env e; - address other; - require other != usr; address anyAddr; address anyAddr_2; uint24 anyUint24; int24 anyInt24; int24 anyInt24_2; - mathint wardsOtherBefore = wards(other); + mathint wardsBefore = wards(anyAddr); mathint budsBefore = buds(anyAddr); mathint numBefore; mathint zzzBefore; mathint amt0Before; mathint amt1Before; mathint req0Before; mathint req1Before; mathint hopBefore; numBefore, zzzBefore, amt0Before, amt1Before, req0Before, req1Before, hopBefore = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); - rely(e, usr); + calldataarg args; + f(e, args); - mathint wardsUsrAfter = wards(usr); - mathint wardsOtherAfter = wards(other); + mathint wardsAfter = wards(anyAddr); mathint budsAfter = buds(anyAddr); mathint numAfter; mathint zzzAfter; mathint amt0After; mathint amt1After; mathint req0After; mathint req1After; mathint hopAfter; numAfter, zzzAfter, amt0After, amt1After, req0After, req1After, hopAfter = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert budsAfter != budsBefore => f.selector == sig:kiss(address).selector || f.selector == sig:diss(address).selector, "buds[x] changed in an unexpected function"; + assert numAfter != numBefore => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector || f.selector == sig:deposit(address,address,uint24,int24,int24,uint128,uint128).selector || f.selector == sig:withdraw(address,address,uint24,int24,int24,uint128,uint128).selector, "configs[x][y][z][a][b].num changed in an unexpected function"; + assert zzzAfter != zzzBefore => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector || f.selector == sig:deposit(address,address,uint24,int24,int24,uint128,uint128).selector || f.selector == sig:withdraw(address,address,uint24,int24,int24,uint128,uint128).selector, "configs[x][y][z][a][b].zzz changed in an unexpected function"; + assert amt0After != amt0Before => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector, "configs[x][y][z][a][b].amt0 changed in an unexpected function"; + assert amt1After != amt1Before => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector, "configs[x][y][z][a][b].amt1 changed in an unexpected function"; + assert req0After != req0Before => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector, "configs[x][y][z][a][b].req0 changed in an unexpected function"; + assert req1After != req1Before => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector, "configs[x][y][z][a][b].req1 changed in an unexpected function"; + assert hopAfter != hopBefore => f.selector == sig:setConfig(address,address,uint24,int24,int24,int32,uint32,uint96,uint96,uint96,uint96).selector, "configs[x][y][z][a][b].hop changed in an unexpected function"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert budsAfter == budsBefore, "rely did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "rely did not keep unchanged every configs[x][y][z][a][b].num"; - assert zzzAfter == zzzBefore, "rely did not keep unchanged every configs[x][y][z][a][b].zzz"; - assert amt0After == amt0Before, "rely did not keep unchanged every configs[x][y][z][a][b].amt0"; - assert amt1After == amt1Before, "rely did not keep unchanged every configs[x][y][z][a][b].amt1"; - assert req0After == req0Before, "rely did not keep unchanged every configs[x][y][z][a][b].req0"; - assert req1After == req1Before, "rely did not keep unchanged every configs[x][y][z][a][b].req1"; - assert hopAfter == hopBefore, "rely did not keep unchanged every configs[x][y][z][a][b].hop"; } // Verify revert rules on rely @@ -151,35 +166,16 @@ rule deny(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - uint24 anyUint24; - int24 anyInt24; - int24 anyInt24_2; mathint wardsOtherBefore = wards(other); - mathint budsBefore = buds(anyAddr); - mathint numBefore; mathint zzzBefore; mathint amt0Before; mathint amt1Before; mathint req0Before; mathint req1Before; mathint hopBefore; - numBefore, zzzBefore, amt0Before, amt1Before, req0Before, req1Before, hopBefore = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint budsAfter = buds(anyAddr); - mathint numAfter; mathint zzzAfter; mathint amt0After; mathint amt1After; mathint req0After; mathint req1After; mathint hopAfter; - numAfter, zzzAfter, amt0After, amt1After, req0After, req1After, hopAfter = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert budsAfter == budsBefore, "deny did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "deny did not keep unchanged every configs[x][y][z][a][b].num"; - assert zzzAfter == zzzBefore, "deny did not keep unchanged every configs[x][y][z][a][b].zzz"; - assert amt0After == amt0Before, "deny did not keep unchanged every configs[x][y][z][a][b].amt0"; - assert amt1After == amt1Before, "deny did not keep unchanged every configs[x][y][z][a][b].amt1"; - assert req0After == req0Before, "deny did not keep unchanged every configs[x][y][z][a][b].req0"; - assert req1After == req1Before, "deny did not keep unchanged every configs[x][y][z][a][b].req1"; - assert hopAfter == hopBefore, "deny did not keep unchanged every configs[x][y][z][a][b].hop"; } // Verify revert rules on deny @@ -204,35 +200,16 @@ rule kiss(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - uint24 anyUint24; - int24 anyInt24; - int24 anyInt24_2; - mathint wardsBefore = wards(anyAddr); mathint budsOtherBefore = buds(other); - mathint numBefore; mathint zzzBefore; mathint amt0Before; mathint amt1Before; mathint req0Before; mathint req1Before; mathint hopBefore; - numBefore, zzzBefore, amt0Before, amt1Before, req0Before, req1Before, hopBefore = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); kiss(e, usr); - mathint wardsAfter = wards(anyAddr); mathint budsUsrAfter = buds(usr); mathint budsOtherAfter = buds(other); - mathint numAfter; mathint zzzAfter; mathint amt0After; mathint amt1After; mathint req0After; mathint req1After; mathint hopAfter; - numAfter, zzzAfter, amt0After, amt1After, req0After, req1After, hopAfter = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); - assert wardsAfter == wardsBefore, "kiss did not keep unchanged every wards[x]"; assert budsUsrAfter == 1, "kiss did not set the buds"; assert budsOtherAfter == budsOtherBefore, "kiss did not keep unchanged the rest of buds[x]"; - assert numAfter == numBefore, "kiss did not keep unchanged every configs[x][y][z][a][b].num"; - assert zzzAfter == zzzBefore, "kiss did not keep unchanged every configs[x][y][z][a][b].zzz"; - assert amt0After == amt0Before, "kiss did not keep unchanged every configs[x][y][z][a][b].amt0"; - assert amt1After == amt1Before, "kiss did not keep unchanged every configs[x][y][z][a][b].amt1"; - assert req0After == req0Before, "kiss did not keep unchanged every configs[x][y][z][a][b].req0"; - assert req1After == req1Before, "kiss did not keep unchanged every configs[x][y][z][a][b].req1"; - assert hopAfter == hopBefore, "kiss did not keep unchanged every configs[x][y][z][a][b].hop"; } // Verify revert rules on kiss @@ -257,35 +234,16 @@ rule diss(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - uint24 anyUint24; - int24 anyInt24; - int24 anyInt24_2; - mathint wardsBefore = wards(anyAddr); mathint budsOtherBefore = buds(other); - mathint numBefore; mathint zzzBefore; mathint amt0Before; mathint amt1Before; mathint req0Before; mathint req1Before; mathint hopBefore; - numBefore, zzzBefore, amt0Before, amt1Before, req0Before, req1Before, hopBefore = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); diss(e, usr); - mathint wardsAfter = wards(anyAddr); mathint budsUsrAfter = buds(usr); mathint budsOtherAfter = buds(other); - mathint numAfter; mathint zzzAfter; mathint amt0After; mathint amt1After; mathint req0After; mathint req1After; mathint hopAfter; - numAfter, zzzAfter, amt0After, amt1After, req0After, req1After, hopAfter = configs(anyAddr, anyAddr_2, anyUint24, anyInt24, anyInt24_2); - assert wardsAfter == wardsBefore, "diss did not keep unchanged every wards[x]"; assert budsUsrAfter == 0, "diss did not set the buds"; assert budsOtherAfter == budsOtherBefore, "diss did not keep unchanged the rest of buds[x]"; - assert numAfter == numBefore, "diss did not keep unchanged every configs[x][y][z][a][b].num"; - assert zzzAfter == zzzBefore, "diss did not keep unchanged every configs[x][y][z][a][b].zzz"; - assert amt0After == amt0Before, "diss did not keep unchanged every configs[x][y][z][a][b].amt0"; - assert amt1After == amt1Before, "diss did not keep unchanged every configs[x][y][z][a][b].amt1"; - assert req0After == req0Before, "diss did not keep unchanged every configs[x][y][z][a][b].req0"; - assert req1After == req1Before, "diss did not keep unchanged every configs[x][y][z][a][b].req1"; - assert hopAfter == hopBefore, "diss did not keep unchanged every configs[x][y][z][a][b].hop"; } // Verify revert rules on diss @@ -308,7 +266,6 @@ rule diss_revert(address usr) { rule setConfig(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tickUpper, int32 num, uint32 hop, uint96 amt0, uint96 amt1, uint96 req0, uint96 req1) { env e; - address anyAddr; address otherAddr; address otherAddr_2; uint24 otherUint24; @@ -316,22 +273,16 @@ rule setConfig(address gem0, address gem1, uint24 fee, int24 tickLower, int24 ti int24 otherInt24_2; require otherAddr != gem0 || otherAddr_2 != gem1 || fee != otherUint24 || tickLower != otherInt24 || tickUpper != otherInt24_2; - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); mathint numOtherBefore; mathint zzzOtherBefore; mathint amt0OtherBefore; mathint amt1OtherBefore; mathint req0OtherBefore; mathint req1OtherBefore; mathint hopOtherBefore; numOtherBefore, zzzOtherBefore, amt0OtherBefore, amt1OtherBefore, req0OtherBefore, req1OtherBefore, hopOtherBefore = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); setConfig(e, gem0, gem1, fee, tickLower, tickUpper, num, hop, amt0, amt1, req0, req1); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); mathint numGem0Gem1After; mathint zzzGem0Gem1After; mathint amt0Gem0Gem1After; mathint amt1Gem0Gem1After; mathint req0Gem0Gem1After; mathint req1Gem0Gem1After; mathint hopGem0Gem1After; numGem0Gem1After, zzzGem0Gem1After, amt0Gem0Gem1After, amt1Gem0Gem1After, req0Gem0Gem1After, req1Gem0Gem1After, hopGem0Gem1After = configs(gem0, gem1, fee, tickLower, tickUpper); mathint numOtherAfter; mathint zzzOtherAfter; mathint amt0OtherAfter; mathint amt1OtherAfter; mathint req0OtherAfter; mathint req1OtherAfter; mathint hopOtherAfter; numOtherAfter, zzzOtherAfter, amt0OtherAfter, amt1OtherAfter, req0OtherAfter, req1OtherAfter, hopOtherAfter = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); - assert wardsAfter == wardsBefore, "setConfig did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "setConfig did not keep unchanged every buds[x]"; assert numGem0Gem1After == to_mathint(num), "setConfig did not set configs[gem0][gem1][fee][tickLower][tickUpper].num to num"; assert zzzGem0Gem1After == 0, "setConfig did not set configs[gem0][gem1][fee][tickLower][tickUpper].zzz to 0"; assert amt0Gem0Gem1After == to_mathint(amt0), "setConfig did not set configs[gem0][gem1][fee][tickLower][tickUpper].amt0 to amt0"; @@ -370,7 +321,6 @@ rule setConfig_revert(address gem0, address gem1, uint24 fee, int24 tickLower, i rule deposit(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tickUpper, uint128 amt0Min, uint128 amt1Min) { env e; - address anyAddr; address otherAddr; address otherAddr_2; uint24 otherUint24; @@ -380,40 +330,26 @@ rule deposit(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tick require e.block.timestamp <= max_uint32; - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); - mathint numGem0Gem1Before; mathint zzzGem0Gem1Before; mathint amt0Gem0Gem1Before; mathint amt1Gem0Gem1Before; mathint req0Gem0Gem1Before; mathint req1Gem0Gem1Before; mathint hopGem0Gem1Before; - numGem0Gem1Before, zzzGem0Gem1Before, amt0Gem0Gem1Before, amt1Gem0Gem1Before, req0Gem0Gem1Before, req1Gem0Gem1Before, hopGem0Gem1Before = configs(gem0, gem1, fee, tickLower, tickUpper); - mathint numOtherBefore; mathint zzzOtherBefore; mathint amt0OtherBefore; mathint amt1OtherBefore; mathint req0OtherBefore; mathint req1OtherBefore; mathint hopOtherBefore; - numOtherBefore, zzzOtherBefore, amt0OtherBefore, amt1OtherBefore, req0OtherBefore, req1OtherBefore, hopOtherBefore = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); + mathint a; mathint b; mathint c; mathint d; mathint f; + + mathint numGem0Gem1Before; mathint zzzGem0Gem1Before; mathint amt0Gem0Gem1; mathint amt1Gem0Gem1; mathint req0Gem0Gem1; mathint req1Gem0Gem1; + numGem0Gem1Before, zzzGem0Gem1Before, amt0Gem0Gem1, amt1Gem0Gem1, req0Gem0Gem1, req1Gem0Gem1, a = configs(gem0, gem1, fee, tickLower, tickUpper); + mathint numOtherBefore; mathint zzzOtherBefore; + numOtherBefore, zzzOtherBefore, a, b, c, d, f = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); mathint depositCounterBefore = depositCounter; deposit(e, gem0, gem1, fee, tickLower, tickUpper, amt0Min, amt1Min); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); - mathint numGem0Gem1After; mathint zzzGem0Gem1After; mathint amt0Gem0Gem1After; mathint amt1Gem0Gem1After; mathint req0Gem0Gem1After; mathint req1Gem0Gem1After; mathint hopGem0Gem1After; - numGem0Gem1After, zzzGem0Gem1After, amt0Gem0Gem1After, amt1Gem0Gem1After, req0Gem0Gem1After, req1Gem0Gem1After, hopGem0Gem1After = configs(gem0, gem1, fee, tickLower, tickUpper); - mathint numOtherAfter; mathint zzzOtherAfter; mathint amt0OtherAfter; mathint amt1OtherAfter; mathint req0OtherAfter; mathint req1OtherAfter; mathint hopOtherAfter; - numOtherAfter, zzzOtherAfter, amt0OtherAfter, amt1OtherAfter, req0OtherAfter, req1OtherAfter, hopOtherAfter = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); + mathint numGem0Gem1After; mathint zzzGem0Gem1After; + numGem0Gem1After, zzzGem0Gem1After, a, b, c, d, f = configs(gem0, gem1, fee, tickLower, tickUpper); + mathint numOtherAfter; mathint zzzOtherAfter; + numOtherAfter, zzzOtherAfter, a, b, c, d, f = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); - assert wardsAfter == wardsBefore, "deposit did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "deposit did not keep unchanged every buds[x]"; assert numGem0Gem1After == numGem0Gem1Before - 1, "deposit did not decrease configs[gem0][gem1][fee][tickLower][tickUpper].num by 1"; assert zzzGem0Gem1After == to_mathint(e.block.timestamp), "deposit did not set configs[gem0][gem1][fee][tickLower][tickUpper].zzz to block.timestamp"; - assert amt0Gem0Gem1After == amt0Gem0Gem1Before, "deposit did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].amt0"; - assert amt1Gem0Gem1After == amt1Gem0Gem1Before, "deposit did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].amt1"; - assert req0Gem0Gem1After == req0Gem0Gem1Before, "deposit did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].req0"; - assert req1Gem0Gem1After == req1Gem0Gem1Before, "deposit did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].req1"; - assert hopGem0Gem1After == hopGem0Gem1Before, "deposit did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].hop"; assert numOtherAfter == numOtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].num"; assert zzzOtherAfter == zzzOtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].zzz"; - assert amt0OtherAfter == amt0OtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].amt0"; - assert amt1OtherAfter == amt1OtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].amt1"; - assert req0OtherAfter == req0OtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].req0"; - assert req1OtherAfter == req1OtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].req1"; - assert hopOtherAfter == hopOtherBefore, "deposit did not keep unchanged the rest of configs[x][y][z][a][b].hop"; assert depositCounter == depositCounterBefore + 1, "deposit did not execute exactly one deposit external call"; assert depositAddr == depositor(), "deposit did not execute the deposit external call to the correct 'depositor()' contract"; assert depositGem0 == gem0, "deposit did not pass the correct gem0 to the external call"; @@ -422,10 +358,10 @@ rule deposit(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tick assert depositTickLower == tickLower, "deposit did not pass the correct tickLower to the external call"; assert depositTickUpper == tickUpper, "deposit did not pass the correct tickUpper to the external call"; assert depositLiquidity == 0, "deposit did not pass the correct liquidity to the external call"; - assert to_mathint(depositAmt0Desired) == amt0Gem0Gem1Before, "deposit did not pass the correct amt0Desired to the external call"; - assert to_mathint(depositAmt1Desired) == amt1Gem0Gem1Before, "deposit did not pass the correct amt1Desired to the external call"; - assert to_mathint(depositAmt0Min) == (amt0Min == 0 ? req0Gem0Gem1Before : to_mathint(amt0Min)), "deposit did not pass the correct amt0Min to the external call"; - assert to_mathint(depositAmt1Min) == (amt1Min == 0 ? req1Gem0Gem1Before : to_mathint(amt1Min)), "deposit did not pass the correct amt1Min to the external call"; + assert to_mathint(depositAmt0Desired) == amt0Gem0Gem1, "deposit did not pass the correct amt0Desired to the external call"; + assert to_mathint(depositAmt1Desired) == amt1Gem0Gem1, "deposit did not pass the correct amt1Desired to the external call"; + assert to_mathint(depositAmt0Min) == (amt0Min == 0 ? req0Gem0Gem1 : to_mathint(amt0Min)), "deposit did not pass the correct amt0Min to the external call"; + assert to_mathint(depositAmt1Min) == (amt1Min == 0 ? req1Gem0Gem1 : to_mathint(amt1Min)), "deposit did not pass the correct amt1Min to the external call"; } // Verify revert rules on deposit @@ -461,7 +397,6 @@ rule deposit_revert(address gem0, address gem1, uint24 fee, int24 tickLower, int rule withdraw(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tickUpper, uint128 amt0Min, uint128 amt1Min) { env e; - address anyAddr; address otherAddr; address otherAddr_2; uint24 otherUint24; @@ -471,40 +406,26 @@ rule withdraw(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tic require e.block.timestamp <= max_uint32; - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); - mathint numGem0Gem1Before; mathint zzzGem0Gem1Before; mathint amt0Gem0Gem1Before; mathint amt1Gem0Gem1Before; mathint req0Gem0Gem1Before; mathint req1Gem0Gem1Before; mathint hopGem0Gem1Before; - numGem0Gem1Before, zzzGem0Gem1Before, amt0Gem0Gem1Before, amt1Gem0Gem1Before, req0Gem0Gem1Before, req1Gem0Gem1Before, hopGem0Gem1Before = configs(gem0, gem1, fee, tickLower, tickUpper); - mathint numOtherBefore; mathint zzzOtherBefore; mathint amt0OtherBefore; mathint amt1OtherBefore; mathint req0OtherBefore; mathint req1OtherBefore; mathint hopOtherBefore; - numOtherBefore, zzzOtherBefore, amt0OtherBefore, amt1OtherBefore, req0OtherBefore, req1OtherBefore, hopOtherBefore = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); + mathint a; mathint b; mathint c; mathint d; mathint f; + + mathint numGem0Gem1Before; mathint zzzGem0Gem1Before; mathint amt0Gem0Gem1; mathint amt1Gem0Gem1; mathint req0Gem0Gem1; mathint req1Gem0Gem1; + numGem0Gem1Before, zzzGem0Gem1Before, amt0Gem0Gem1, amt1Gem0Gem1, req0Gem0Gem1, req1Gem0Gem1, a = configs(gem0, gem1, fee, tickLower, tickUpper); + mathint numOtherBefore; mathint zzzOtherBefore; + numOtherBefore, zzzOtherBefore, a, b, c, d, f = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); mathint withdrawCounterBefore = withdrawCounter; withdraw(e, gem0, gem1, fee, tickLower, tickUpper, amt0Min, amt1Min); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); mathint numGem0Gem1After; mathint zzzGem0Gem1After; mathint amt0Gem0Gem1After; mathint amt1Gem0Gem1After; mathint req0Gem0Gem1After; mathint req1Gem0Gem1After; mathint hopGem0Gem1After; - numGem0Gem1After, zzzGem0Gem1After, amt0Gem0Gem1After, amt1Gem0Gem1After, req0Gem0Gem1After, req1Gem0Gem1After, hopGem0Gem1After = configs(gem0, gem1, fee, tickLower, tickUpper); - mathint numOtherAfter; mathint zzzOtherAfter; mathint amt0OtherAfter; mathint amt1OtherAfter; mathint req0OtherAfter; mathint req1OtherAfter; mathint hopOtherAfter; - numOtherAfter, zzzOtherAfter, amt0OtherAfter, amt1OtherAfter, req0OtherAfter, req1OtherAfter, hopOtherAfter = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); + numGem0Gem1After, zzzGem0Gem1After, a, b, c, d, f = configs(gem0, gem1, fee, tickLower, tickUpper); + mathint numOtherAfter; mathint zzzOtherAfter; + numOtherAfter, zzzOtherAfter, a, b, c, d, f = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); - assert wardsAfter == wardsBefore, "withdraw did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "withdraw did not keep unchanged every buds[x]"; assert numGem0Gem1After == numGem0Gem1Before + 1, "withdraw did not increase configs[gem0][gem1][fee][tickLower][tickUpper].num by 1"; assert zzzGem0Gem1After == to_mathint(e.block.timestamp), "withdraw did not set configs[gem0][gem1][fee][tickLower][tickUpper].zzz to block.timestamp"; - assert amt0Gem0Gem1After == amt0Gem0Gem1Before, "withdraw did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].amt0"; - assert amt1Gem0Gem1After == amt1Gem0Gem1Before, "withdraw did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].amt1"; - assert req0Gem0Gem1After == req0Gem0Gem1Before, "withdraw did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].req0"; - assert req1Gem0Gem1After == req1Gem0Gem1Before, "withdraw did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].req1"; - assert hopGem0Gem1After == hopGem0Gem1Before, "withdraw did not keep unchanged configs[gem0][gem1][fee][tickLower][tickUpper].hop"; assert numOtherAfter == numOtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].num"; assert zzzOtherAfter == zzzOtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].zzz"; - assert amt0OtherAfter == amt0OtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].amt0"; - assert amt1OtherAfter == amt1OtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].amt1"; - assert req0OtherAfter == req0OtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].req0"; - assert req1OtherAfter == req1OtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].req1"; - assert hopOtherAfter == hopOtherBefore, "withdraw did not keep unchanged the rest of configs[x][y][z][a][b].hop"; assert withdrawCounter == withdrawCounterBefore + 1, "withdraw did not execute exactly one withdraw external call"; assert withdrawAddr == depositor(), "withdraw did not execute the withdraw external call to the correct 'depositor()' contract"; assert withdrawGem0 == gem0, "withdraw did not pass the correct gem0 to the external call"; @@ -513,10 +434,10 @@ rule withdraw(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tic assert withdrawTickLower == tickLower, "withdraw did not pass the correct tickLower to the external call"; assert withdrawTickUpper == tickUpper, "withdraw did not pass the correct tickUpper to the external call"; assert withdrawLiquidity == 0, "withdraw did not pass the correct liquidity to the external call"; - assert to_mathint(withdrawAmt0Desired) == amt0Gem0Gem1Before, "withdraw did not pass the correct amt0Desired to the external call"; - assert to_mathint(withdrawAmt1Desired) == amt1Gem0Gem1Before, "withdraw did not pass the correct amt1Desired to the external call"; - assert to_mathint(withdrawAmt0Min) == (amt0Min == 0 ? req0Gem0Gem1Before : to_mathint(amt0Min)), "withdraw did not pass the correct amt0Min to the external call"; - assert to_mathint(withdrawAmt1Min) == (amt1Min == 0 ? req1Gem0Gem1Before : to_mathint(amt1Min)), "withdraw did not pass the correct amt1Min to the external call"; + assert to_mathint(withdrawAmt0Desired) == amt0Gem0Gem1, "withdraw did not pass the correct amt0Desired to the external call"; + assert to_mathint(withdrawAmt1Desired) == amt1Gem0Gem1, "withdraw did not pass the correct amt1Desired to the external call"; + assert to_mathint(withdrawAmt0Min) == (amt0Min == 0 ? req0Gem0Gem1 : to_mathint(amt0Min)), "withdraw did not pass the correct amt0Min to the external call"; + assert to_mathint(withdrawAmt1Min) == (amt1Min == 0 ? req1Gem0Gem1 : to_mathint(amt1Min)), "withdraw did not pass the correct amt1Min to the external call"; assert withdrawTakeFees, "withdraw did not pass the correct takeFees to the external call"; } @@ -553,39 +474,10 @@ rule withdraw_revert(address gem0, address gem1, uint24 fee, int24 tickLower, in rule collect(address gem0, address gem1, uint24 fee, int24 tickLower, int24 tickUpper) { env e; - address anyAddr; - address otherAddr; - address otherAddr_2; - uint24 otherUint24; - int24 otherInt24; - int24 otherInt24_2; - require otherAddr != gem0 || otherAddr_2 != gem1 || fee != otherUint24 || tickLower != otherInt24 || tickUpper != otherInt24_2; - - require e.block.timestamp <= max_uint32; - - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); - mathint numBefore; mathint zzzBefore; mathint amt0Before; mathint amt1Before; mathint req0Before; mathint req1Before; mathint hopBefore; - numBefore, zzzBefore, amt0Before, amt1Before, req0Before, req1Before, hopBefore = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); - mathint collectCounterBefore = collectCounter; collect(e, gem0, gem1, fee, tickLower, tickUpper); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); - mathint numAfter; mathint zzzAfter; mathint amt0After; mathint amt1After; mathint req0After; mathint req1After; mathint hopAfter; - numAfter, zzzAfter, amt0After, amt1After, req0After, req1After, hopAfter = configs(otherAddr, otherAddr_2, otherUint24, otherInt24, otherInt24_2); - - assert wardsAfter == wardsBefore, "collect did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "collect did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "collect did not keep unchanged every configs[x][y][z][a][b].num"; - assert zzzAfter == zzzBefore, "collect did not keep unchanged every configs[x][y][z][a][b].zzz"; - assert amt0After == amt0Before, "collect did not keep unchanged every configs[x][y][z][a][b].amt0"; - assert amt1After == amt1Before, "collect did not keep unchanged every configs[x][y][z][a][b].amt1"; - assert req0After == req0Before, "collect did not keep unchanged every configs[x][y][z][a][b].req0"; - assert req1After == req1Before, "collect did not keep unchanged every configs[x][y][z][a][b].req1"; - assert hopAfter == hopBefore, "collect did not keep unchanged every configs[x][y][z][a][b].hop"; assert collectCounter == collectCounterBefore + 1, "collect did not execute exactly one collect external call"; assert collectAddr == depositor(), "collect did not execute the collect external call to the correct 'depositor()' contract"; assert collectGem0 == gem0, "collect did not pass the correct gem0 to the external call"; diff --git a/certora/funnels/automation/StableSwapper.spec b/certora/funnels/automation/StableSwapper.spec index c16f196d..570fcaac 100644 --- a/certora/funnels/automation/StableSwapper.spec +++ b/certora/funnels/automation/StableSwapper.spec @@ -29,36 +29,51 @@ function swapSummary(address addr, address src, address dst, uint256 lot, uint25 return swapRetValue; } -// Verify correct storage changes for non reverting rely -rule rely(address usr) { +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { env e; - address other; - require other != usr; address anyAddr; address anyAddr_2; - mathint wardsOtherBefore = wards(other); + mathint wardsBefore = wards(anyAddr); mathint budsBefore = buds(anyAddr); mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; mathint reqBefore; numBefore, hopBefore, zzzBefore, lotBefore, reqBefore = configs(anyAddr, anyAddr_2); - rely(e, usr); + calldataarg args; + f(e, args); - mathint wardsUsrAfter = wards(usr); - mathint wardsOtherAfter = wards(other); + mathint wardsAfter = wards(anyAddr); mathint budsAfter = buds(anyAddr); mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; mathint reqAfter; numAfter, hopAfter, zzzAfter, lotAfter, reqAfter = configs(anyAddr, anyAddr_2); + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function"; + assert budsAfter != budsBefore => f.selector == sig:kiss(address).selector || f.selector == sig:diss(address).selector, "buds[x] changed in an unexpected function"; + assert numAfter != numBefore => f.selector == sig:setConfig(address,address,uint128,uint32,uint96,uint96).selector || f.selector == sig:swap(address,address,uint256,address,bytes).selector, "configs[x][y].num changed in an unexpected function"; + assert hopAfter != hopBefore => f.selector == sig:setConfig(address,address,uint128,uint32,uint96,uint96).selector, "configs[x][y].hop changed in an unexpected function"; + assert zzzAfter != zzzBefore => f.selector == sig:setConfig(address,address,uint128,uint32,uint96,uint96).selector || f.selector == sig:swap(address,address,uint256,address,bytes).selector, "configs[x][y].zzz changed in an unexpected function"; + assert lotAfter != lotBefore => f.selector == sig:setConfig(address,address,uint128,uint32,uint96,uint96).selector, "configs[x][y].lot changed in an unexpected function"; + assert reqAfter != reqBefore => f.selector == sig:setConfig(address,address,uint128,uint32,uint96,uint96).selector, "configs[x][y].req changed in an unexpected function"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + assert wardsUsrAfter == 1, "rely did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; - assert budsAfter == budsBefore, "rely did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "rely did not keep unchanged every configs[x][y].num"; - assert hopAfter == hopBefore, "rely did not keep unchanged every configs[x][y].hop"; - assert zzzAfter == zzzBefore, "rely did not keep unchanged every configs[x][y].zzz"; - assert lotAfter == lotBefore, "rely did not keep unchanged every configs[x][y].lot"; - assert reqAfter == reqBefore, "rely did not keep unchanged every configs[x][y].req"; } // Verify revert rules on rely @@ -83,30 +98,16 @@ rule deny(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; mathint wardsOtherBefore = wards(other); - mathint budsBefore = buds(anyAddr); - mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; mathint reqBefore; - numBefore, hopBefore, zzzBefore, lotBefore, reqBefore = configs(anyAddr, anyAddr_2); deny(e, usr); mathint wardsUsrAfter = wards(usr); mathint wardsOtherAfter = wards(other); - mathint budsAfter = buds(anyAddr); - mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; mathint reqAfter; - numAfter, hopAfter, zzzAfter, lotAfter, reqAfter = configs(anyAddr, anyAddr_2); assert wardsUsrAfter == 0, "deny did not set the wards"; assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; - assert budsAfter == budsBefore, "deny did not keep unchanged every buds[x]"; - assert numAfter == numBefore, "deny did not keep unchanged every configs[x][y].num"; - assert hopAfter == hopBefore, "deny did not keep unchanged every configs[x][y].hop"; - assert zzzAfter == zzzBefore, "deny did not keep unchanged every configs[x][y].zzz"; - assert lotAfter == lotBefore, "deny did not keep unchanged every configs[x][y].lot"; - assert reqAfter == reqBefore, "deny did not keep unchanged every configs[x][y].req"; } // Verify revert rules on deny @@ -131,30 +132,16 @@ rule kiss(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - mathint wardsBefore = wards(anyAddr); mathint budsOtherBefore = buds(other); - mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; mathint reqBefore; - numBefore, hopBefore, zzzBefore, lotBefore, reqBefore = configs(anyAddr, anyAddr_2); kiss(e, usr); - mathint wardsAfter = wards(anyAddr); mathint budsUsrAfter = buds(usr); mathint budsOtherAfter = buds(other); - mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; mathint reqAfter; - numAfter, hopAfter, zzzAfter, lotAfter, reqAfter = configs(anyAddr, anyAddr_2); - assert wardsAfter == wardsBefore, "kiss did not keep unchanged every wards[x]"; assert budsUsrAfter == 1, "kiss did not set the buds"; assert budsOtherAfter == budsOtherBefore, "kiss did not keep unchanged the rest of buds[x]"; - assert numAfter == numBefore, "kiss did not keep unchanged every configs[x][y].num"; - assert hopAfter == hopBefore, "kiss did not keep unchanged every configs[x][y].hop"; - assert zzzAfter == zzzBefore, "kiss did not keep unchanged every configs[x][y].zzz"; - assert lotAfter == lotBefore, "kiss did not keep unchanged every configs[x][y].lot"; - assert reqAfter == reqBefore, "kiss did not keep unchanged every configs[x][y].req"; } // Verify revert rules on kiss @@ -179,30 +166,16 @@ rule diss(address usr) { address other; require other != usr; - address anyAddr; - address anyAddr_2; - mathint wardsBefore = wards(anyAddr); mathint budsOtherBefore = buds(other); - mathint numBefore; mathint hopBefore; mathint zzzBefore; mathint lotBefore; mathint reqBefore; - numBefore, hopBefore, zzzBefore, lotBefore, reqBefore = configs(anyAddr, anyAddr_2); diss(e, usr); - mathint wardsAfter = wards(anyAddr); mathint budsUsrAfter = buds(usr); mathint budsOtherAfter = buds(other); - mathint numAfter; mathint hopAfter; mathint zzzAfter; mathint lotAfter; mathint reqAfter; - numAfter, hopAfter, zzzAfter, lotAfter, reqAfter = configs(anyAddr, anyAddr_2); - assert wardsAfter == wardsBefore, "diss did not keep unchanged every wards[x]"; assert budsUsrAfter == 0, "diss did not set the buds"; assert budsOtherAfter == budsOtherBefore, "diss did not keep unchanged the rest of buds[x]"; - assert numAfter == numBefore, "diss did not keep unchanged every configs[x][y].num"; - assert hopAfter == hopBefore, "diss did not keep unchanged every configs[x][y].hop"; - assert zzzAfter == zzzBefore, "diss did not keep unchanged every configs[x][y].zzz"; - assert lotAfter == lotBefore, "diss did not keep unchanged every configs[x][y].lot"; - assert reqAfter == reqBefore, "diss did not keep unchanged every configs[x][y].req"; } // Verify revert rules on diss @@ -225,27 +198,20 @@ rule diss_revert(address usr) { rule setConfig(address src, address dst, uint128 num, uint32 hop, uint96 lot, uint96 req) { env e; - address anyAddr; address otherAddr; address otherAddr_2; require otherAddr != src || otherAddr_2 != dst; - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); mathint numOtherBefore; mathint hopOtherBefore; mathint zzzOtherBefore; mathint lotOtherBefore; mathint reqOtherBefore; numOtherBefore, hopOtherBefore, zzzOtherBefore, lotOtherBefore, reqOtherBefore = configs(otherAddr, otherAddr_2); setConfig(e, src, dst, num, hop, lot, req); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); mathint numSrcDstAfter; mathint hopSrcDstAfter; mathint zzzSrcDstAfter; mathint lotSrcDstAfter; mathint reqSrcDstAfter; numSrcDstAfter, hopSrcDstAfter, zzzSrcDstAfter, lotSrcDstAfter, reqSrcDstAfter = configs(src, dst); mathint numOtherAfter; mathint hopOtherAfter; mathint zzzOtherAfter; mathint lotOtherAfter; mathint reqOtherAfter; numOtherAfter, hopOtherAfter, zzzOtherAfter, lotOtherAfter, reqOtherAfter = configs(otherAddr, otherAddr_2); - assert wardsAfter == wardsBefore, "setConfig did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "setConfig did not keep unchanged every buds[x]"; assert numSrcDstAfter == to_mathint(num), "setConfig did not set configs[src][dst].num to num"; assert hopSrcDstAfter == to_mathint(hop), "setConfig did not set configs[src][dst].hop to hop"; assert zzzSrcDstAfter == 0, "setConfig did not set configs[src][dst].zzz to 0"; @@ -278,49 +244,38 @@ rule setConfig_revert(address src, address dst, uint128 num, uint32 hop, uint96 rule swap(address src, address dst, uint256 minOut, address callee, bytes data) { env e; - address anyAddr; address otherAddr; address otherAddr_2; require otherAddr != src || otherAddr_2 != dst; require e.block.timestamp <= max_uint32; - mathint wardsBefore = wards(anyAddr); - mathint budsBefore = buds(anyAddr); - mathint numSrcDstBefore; mathint hopSrcDstBefore; mathint zzzSrcDstBefore; mathint lotSrcDstBefore; mathint reqSrcDstBefore; - numSrcDstBefore, hopSrcDstBefore, zzzSrcDstBefore, lotSrcDstBefore, reqSrcDstBefore = configs(src, dst); - mathint numOtherBefore; mathint hopOtherBefore; mathint zzzOtherBefore; mathint lotOtherBefore; mathint reqOtherBefore; - numOtherBefore, hopOtherBefore, zzzOtherBefore, lotOtherBefore, reqOtherBefore = configs(otherAddr, otherAddr_2); + mathint a; mathint b; mathint c; + + mathint numSrcDstBefore; mathint lotSrcDst; mathint reqSrcDst; + numSrcDstBefore, a, b, lotSrcDst, reqSrcDst = configs(src, dst); + mathint numOtherBefore; mathint zzzOtherBefore; + numOtherBefore, a, zzzOtherBefore, b, c = configs(otherAddr, otherAddr_2); mathint swapCounterBefore = swapCounter; swap(e, src, dst, minOut, callee, data); - mathint wardsAfter = wards(anyAddr); - mathint budsAfter = buds(anyAddr); - mathint numSrcDstAfter; mathint hopSrcDstAfter; mathint zzzSrcDstAfter; mathint lotSrcDstAfter; mathint reqSrcDstAfter; - numSrcDstAfter, hopSrcDstAfter, zzzSrcDstAfter, lotSrcDstAfter, reqSrcDstAfter = configs(src, dst); - mathint numOtherAfter; mathint hopOtherAfter; mathint zzzOtherAfter; mathint lotOtherAfter; mathint reqOtherAfter; - numOtherAfter, hopOtherAfter, zzzOtherAfter, lotOtherAfter, reqOtherAfter = configs(otherAddr, otherAddr_2); + mathint numSrcDstAfter; mathint zzzSrcDstAfter; + numSrcDstAfter, a, zzzSrcDstAfter, b, c = configs(src, dst); + mathint numOtherAfter; mathint zzzOtherAfter; + numOtherAfter, a, zzzOtherAfter, b, c = configs(otherAddr, otherAddr_2); - assert wardsAfter == wardsBefore, "swap did not keep unchanged every wards[x]"; - assert budsAfter == budsBefore, "swap did not keep unchanged every buds[x]"; assert numSrcDstAfter == numSrcDstBefore - 1, "swap did not decrease configs[src][dst].num by 1"; - assert hopSrcDstAfter == hopSrcDstBefore, "swap did not keep unchanged configs[src][dst].hop"; assert zzzSrcDstAfter == to_mathint(e.block.timestamp), "swap did not set configs[src][dst].zzz to block.timestamp"; - assert lotSrcDstAfter == lotSrcDstBefore, "swap did not keep unchanged configs[src][dst].lot"; - assert reqSrcDstAfter == reqSrcDstBefore, "swap did not keep unchanged configs[src][dst].req"; assert numOtherAfter == numOtherBefore, "swap did not keep unchanged the rest of configs[x][y].num"; - assert hopOtherAfter == hopOtherBefore, "swap did not keep unchanged the rest of configs[x][y].hop"; assert zzzOtherAfter == zzzOtherBefore, "swap did not keep unchanged the rest of configs[x][y].zzz"; - assert lotOtherAfter == lotOtherBefore, "swap did not keep unchanged the rest of configs[x][y].lot"; - assert reqOtherAfter == reqOtherBefore, "swap did not keep unchanged the rest of configs[x][y].req"; assert swapCounter == swapCounterBefore + 1, "swap did not execute exactly one swap external call"; assert swapAddr == swapper(), "swap did not execute the swap external call to the correct 'swapper()' contract"; assert swapSrc == src, "swap did not not pass the correct src to the external call"; assert swapDst == dst, "swap did not not pass the correct dst to the external call"; - assert to_mathint(swapLot) == lotSrcDstBefore, "swap did not not pass the correct lot to the external call"; - assert to_mathint(swapMinOut) == (minOut == 0 ? reqSrcDstBefore : to_mathint(minOut)), "swap did not not pass the correct minOut to the external call"; + assert to_mathint(swapLot) == lotSrcDst, "swap did not not pass the correct lot to the external call"; + assert to_mathint(swapMinOut) == (minOut == 0 ? reqSrcDst : to_mathint(minOut)), "swap did not not pass the correct minOut to the external call"; assert swapCallee == callee, "swap did not not pass the correct callee to the external call"; assert swapDataLength == data.length, "swap did not not pass the correct data to the external call"; }