-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
7e15bd8
commit eee5944
Showing
11 changed files
with
166 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,10 +1,11 @@ | ||
| 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 | ||
| PATH := ~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:$(PATH) | ||
| certora-buffer :; PATH=${PATH} certoraRun certora/AllocatorBuffer.conf$(if $(rule), --rule $(rule),) | ||
| certora-vault :; PATH=${PATH} certoraRun certora/AllocatorVault.conf$(if $(rule), --rule $(rule),) | ||
| certora-roles :; PATH=${PATH} certoraRun certora/AllocatorRoles.conf$(if $(rule), --rule $(rule),) | ||
| certora-oracle :; PATH=${PATH} certoraRun certora/AllocatorOracle.conf$(if $(rule), --rule $(rule),) | ||
| certora-registry :; PATH=${PATH} certoraRun certora/AllocatorRegistry.conf$(if $(rule), --rule $(rule),) | ||
| certora-swapper :; PATH=${PATH} certoraRun certora/funnels/Swapper.conf$(if $(rule), --rule $(rule),) | ||
| certora-depositoruniv3 :; PATH=${PATH} certoraRun certora/funnels/DepositorUniV3.conf$(if $(rule), --rule $(rule),) | ||
| certora-stable-swapper :; PATH=${PATH} certoraRun certora/funnels/automation/StableSwapper.conf$(if $(rule), --rule $(rule),) | ||
| certora-stable-depositoruniv3 :; PATH=${PATH} certoraRun certora/funnels/automation/StableDepositorUniV3.conf$(if $(rule), --rule $(rule),) | ||
| certora-conduit-mover :; PATH=${PATH} certoraRun certora/funnels/automation/ConduitMover.conf$(if $(rule), --rule $(rule),) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,14 @@ | ||
| { | ||
| "files": [ | ||
| "src/AllocatorBuffer.sol", | ||
| "test/mocks/GemMock.sol" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize_map": { | ||
| "AllocatorBuffer": "200", | ||
| "GemMock": "0" | ||
| }, | ||
| "verify": "AllocatorBuffer:certora/AllocatorBuffer.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| { | ||
| "files": [ | ||
| "src/AllocatorOracle.sol" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize": "200", | ||
| "verify": "AllocatorOracle:certora/AllocatorOracle.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| { | ||
| "files": [ | ||
| "src/AllocatorRegistry.sol" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize": "200", | ||
| "verify": "AllocatorRegistry:certora/AllocatorRegistry.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| { | ||
| "files": [ | ||
| "src/AllocatorRoles.sol" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize": "200", | ||
| "verify": "AllocatorRoles:certora/AllocatorRoles.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,33 @@ | ||
| { | ||
| "files": [ | ||
| "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" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize_map": { | ||
| "AllocatorVault": "200", | ||
| "AllocatorRoles": "200", | ||
| "VatMock": "0", | ||
| "JugMock": "0", | ||
| "NstJoinMock": "0", | ||
| "NstMock": "0" | ||
| }, | ||
| "verify": "AllocatorVault:certora/AllocatorVault.spec", | ||
| "multi_assert_check": true, | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| { | ||
| "files": [ | ||
| "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" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize_map": { | ||
| "DepositorUniV3": "200", | ||
| "AllocatorRoles": "200", | ||
| "PoolUniV3Mock": "0", | ||
| "Gem0Mock": "0", | ||
| "Gem1Mock": "0", | ||
| "Auxiliar": "0" | ||
| }, | ||
| "verify": "DepositorUniV3:certora/funnels/DepositorUniV3.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| { | ||
| "files": [ | ||
| "src/funnels/Swapper.sol", | ||
| "src/AllocatorRoles.sol", | ||
| "test/mocks/Gem0Mock.sol", | ||
| "test/mocks/Gem1Mock.sol", | ||
| "test/mocks/CalleeMock.sol" | ||
| ], | ||
| "link": [ | ||
| "Swapper:roles=AllocatorRoles" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize_map": { | ||
| "Swapper": "200", | ||
| "AllocatorRoles": "200", | ||
| "Gem0Mock": "0", | ||
| "Gem1Mock": "0", | ||
| "CalleeMock": "0" | ||
| }, | ||
| "verify": "Swapper:certora/funnels/Swapper.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| { | ||
| "files": [ | ||
| "src/funnels/automation/ConduitMover.sol" | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize": "200", | ||
| "verify": "ConduitMover:certora/funnels/automation/ConduitMover.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| { | ||
| "files": [ | ||
| "src/funnels/automation/StableDepositorUniV3.sol", | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize": "200", | ||
| "verify": "StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec", | ||
| "wait_for_results": "all" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| { | ||
| "files": [ | ||
| "src/funnels/automation/StableSwapper.sol", | ||
| ], | ||
| "rule_sanity": "basic", | ||
| "solc": "solc-0.8.16", | ||
| "solc_optimize": "200", | ||
| "verify": "StableSwapper:certora/funnels/automation/StableSwapper.spec", | ||
| "wait_for_results": "all" | ||
| } |