Skip to content

Commit

Permalink
refactor(DssVestTransferrable): fix Certora spec
Browse files Browse the repository at this point in the history
  • Loading branch information
amusingaxl committed Oct 14, 2024
1 parent 5934d3e commit b50b46a
Show file tree
Hide file tree
Showing 3 changed files with 115 additions and 87 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ echidna-suckable :; ./echidna/echidna.sh suckable
echidna-transferrable :; ./echidna/echidna.sh transferrable
certora-mintable :; PATH=${PATH} certoraRun certora/DssVestMintable.conf $(if $(rule), --rule $(rule),)
certora-suckable :; PATH=${PATH} certoraRun certora/DssVestSuckable.conf $(if $(rule), --rule $(rule),)
certora-transferrable :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/solc-0.6.12 src/DssVest.sol:DssVestTransferrable certora/Dai.sol --link DssVestTransferrable:gem=Dai --verify DssVestTransferrable:certora/DssVestTransferrable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
certora-transferrable :; PATH=${PATH} certoraRun certora/DssVestTransferrable.conf $(if $(rule), --rule $(rule),)
deploy-mintable :; make && dapp create DssVestMintable $(gem)
deploy-suckable :; make && dapp create DssVestSuckable 0xdA0Ab1e0017DEbCd72Be8599041a2aa3bA7e740F
deploy-transferrable :; make && dapp create DssVestTransferrable $(owner) $(gem)
32 changes: 32 additions & 0 deletions certora/DssVestTransferrable.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
{
"files": [
"src/DssVest.sol:DssVestTransferrable",
"certora/mocks/Dai.sol",
],
"link": [
"DssVestTransferrable:gem=Dai"
],
"rule_sanity": "basic",
"multi_assert_check": true,
"wait_for_results": "all",
"solc_map": {
"DssVestTransferrable": "solc-0.6.12",
"Dai": "solc-0.6.12"
},
"solc_optimize_map": {
"DssVestTransferrable": "200",
"Dai": "0"
},
"verify": "DssVestTransferrable:certora/DssVestTransferrable.spec",
"prover_args": [
"-smt_hashingScheme plainInjectivity",
"-s [yices,z3]",
"-splitParallel true",
"-mediumTimeout 3600",
"-depth 30",
"-enableSolidityBasedInlining true"
],
"parametric_contracts": [
"DssVestTransferrable"
]
}
Loading

0 comments on commit b50b46a

Please sign in to comment.