Skip to content

Commit

Permalink
Add Spec for FlapperUniV2SwapOnly (WIP as well)
Browse files Browse the repository at this point in the history
  • Loading branch information
sunbreak1211 committed Dec 6, 2023
1 parent ad86fba commit b4deb55
Show file tree
Hide file tree
Showing 3 changed files with 434 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
PATH := ~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts/solc-0.5.16:~/.solc-select/artifacts/solc-0.4.18:~/.solc-select/artifacts:$(PATH)
certora-flapper-univ2 :; PATH=${PATH} certoraRun certora/FlapperUniV2.conf$(if $(rule), --rule $(rule),)
certora-flapper-univ2 :; PATH=${PATH} certoraRun certora/FlapperUniV2.conf$(if $(rule), --rule $(rule),)
certora-flapper-univ2-swap-only :; PATH=${PATH} certoraRun certora/FlapperUniV2SwapOnly.conf$(if $(rule), --rule $(rule),) --cache none
63 changes: 63 additions & 0 deletions certora/FlapperUniV2SwapOnly.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
{
"files": [
"src/FlapperUniV2SwapOnly.sol",
"certora/dss/Vat.sol",
"certora/dss/DaiJoin.sol",
"certora/dss/Dai.sol",
"certora/dss/DSToken.sol",
"certora/dss/SpotterMock.sol",
"certora/dss/PipMock.sol",
"certora/univ2/UniswapV2Pair.sol",
"certora/univ2/UniswapV2FactoryMock.sol"
],
"link": [
"FlapperUniV2SwapOnly:vat=Vat",
"FlapperUniV2SwapOnly:daiJoin=DaiJoin",
"FlapperUniV2SwapOnly:dai=Dai",
"FlapperUniV2SwapOnly:gem=DSToken",
"FlapperUniV2SwapOnly:spotter=SpotterMock",
"FlapperUniV2SwapOnly:pip=PipMock",
"FlapperUniV2SwapOnly:pair=UniswapV2Pair",
"DaiJoin:vat=Vat",
"DaiJoin:dai=Dai",
"UniswapV2Pair:token0=Dai",
"UniswapV2Pair:token1=DSToken",
"UniswapV2Pair:factory=UniswapV2FactoryMock"
],
"rule_sanity": "basic",
"solc_map": {
"FlapperUniV2SwapOnly": "solc-0.8.16",
"Vat": "solc-0.5.12",
"DaiJoin": "solc-0.5.12",
"Dai": "solc-0.5.12",
"DSToken": "solc-0.4.18",
"SpotterMock": "solc-0.8.16",
"PipMock": "solc-0.8.16",
"UniswapV2Pair": "solc-0.5.16",
"UniswapV2FactoryMock": "solc-0.8.16"
},
"solc_optimize_map": {
"FlapperUniV2SwapOnly": "200",
"Vat": "0",
"DaiJoin": "0",
"Dai": "0",
"DSToken": "200",
"SpotterMock": "0",
"PipMock": "0",
"UniswapV2Pair": "999999",
"UniswapV2FactoryMock": "0"
},
"verify": "FlapperUniV2SwapOnly:certora/FlapperUniV2SwapOnly.spec",
"parametric_contracts": [
"FlapperUniV2SwapOnly"
],
"prover_args": [
"-splitParallel true",
"-mediumTimeout 3600",
"-depth 30"
],
"smt_timeout": "3600",
"optimistic_loop": true,
"multi_assert_check": true,
"wait_for_results": "all"
}
Loading

0 comments on commit b4deb55

Please sign in to comment.