114 lines
3.7 KiB
Bash
Executable File
114 lines
3.7 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
set -euxo pipefail
|
|
|
|
forge_build() {
|
|
# Avoid building Migrator contract (see PROOFS.md for explanation)
|
|
forge build --skip Migrator.sol
|
|
}
|
|
|
|
foundry_kompile() {
|
|
kevm foundry-kompile --verbose \
|
|
--require wormhole-lemmas.k \
|
|
--module-import WORMHOLE-LEMMAS \
|
|
${rekompile} \
|
|
${regen}
|
|
}
|
|
|
|
foundry_prove() {
|
|
kevm foundry-prove \
|
|
--max-depth ${max_depth} \
|
|
--max-iterations ${max_iterations} \
|
|
--workers ${workers} \
|
|
--verbose \
|
|
${reinit} \
|
|
${debug} \
|
|
${simplify_init} \
|
|
${implication_every_block} \
|
|
${break_every_step} \
|
|
${break_on_calls} \
|
|
${auto_abstract} \
|
|
${tests[*]}
|
|
}
|
|
|
|
max_depth=5000
|
|
max_iterations=5000
|
|
|
|
# Number of processes run by the prover in parallel
|
|
# Should be at most (M - 8) / 8 in a machine with M GB of RAM
|
|
workers=1
|
|
|
|
# Switch the options below to turn them on or off
|
|
|
|
# Turn on to regenerate K definitions if Solidity code or KEVM version changes
|
|
regen=--regen
|
|
regen=
|
|
|
|
# Turn on if new lemmas have been added to wormhole-lemmas.k (subsumed by --regen)
|
|
rekompile=--rekompile
|
|
rekompile=
|
|
|
|
# Progress is saved automatically so an unfinished proof can be resumed from where it left off
|
|
# Turn on to restart proof from the beginning instead of resuming
|
|
reinit=--reinit
|
|
reinit=
|
|
|
|
debug=--debug
|
|
debug=
|
|
|
|
simplify_init=--no-simplify-init
|
|
simplify_init=
|
|
|
|
implication_every_block=--implication-every-block
|
|
implication_every_block=
|
|
|
|
break_every_step=--break-every-step
|
|
break_every_step=
|
|
|
|
# Turn off to save the state before every call to the KCFG
|
|
break_on_calls=
|
|
break_on_calls=--no-break-on-calls
|
|
|
|
auto_abstract=--auto-abstract
|
|
auto_abstract=
|
|
|
|
# List of tests to symbolically execute
|
|
|
|
tests=(
|
|
"--test TestSetters.testUpdateGuardianSetIndex_KEVM "
|
|
"--test TestSetters.testExpireGuardianSet_KEVM "
|
|
"--test TestSetters.testSetMessageFee_KEVM "
|
|
"--test TestSetters.testSetGovernanceContract_KEVM "
|
|
"--test TestSetters.testSetInitialized_KEVM "
|
|
"--test TestSetters.testSetGovernanceActionConsumed_KEVM "
|
|
"--test TestSetters.testSetChainId_KEVM "
|
|
"--test TestSetters.testSetGovernanceChainId_KEVM "
|
|
"--test TestSetters.testSetNextSequence_KEVM "
|
|
"--test TestSetters.testSetEvmChainId_Success_KEVM "
|
|
"--test TestSetters.testSetEvmChainId_Revert_KEVM "
|
|
"--test TestGetters.testGetGuardianSetIndex_KEVM "
|
|
"--test TestGetters.testGetMessageFee_KEVM "
|
|
"--test TestGetters.testGetGovernanceContract_KEVM "
|
|
"--test TestGetters.testIsInitialized_KEVM "
|
|
"--test TestGetters.testGetGovernanceActionConsumed_KEVM "
|
|
"--test TestGetters.testChainId_KEVM "
|
|
"--test TestGetters.testGovernanceChainId_KEVM "
|
|
"--test TestGetters.testNextSequence_KEVM "
|
|
"--test TestGetters.testEvmChainId_KEVM "
|
|
"--test TestGovernanceStructs.testParseContractUpgrade_KEVM "
|
|
"--test TestGovernanceStructs.testParseContractUpgradeWrongAction_KEVM "
|
|
"--test TestGovernanceStructs.testParseSetMessageFee_KEVM "
|
|
"--test TestGovernanceStructs.testParseSetMessageFeeWrongAction_KEVM "
|
|
"--test TestGovernanceStructs.testParseTransferFees_KEVM "
|
|
"--test TestGovernanceStructs.testParseTransferFeesWrongAction_KEVM "
|
|
"--test TestGovernanceStructs.testParseRecoverChainId_KEVM "
|
|
"--test TestGovernanceStructs.testParseRecoverChainIdWrongAction_KEVM "
|
|
"--test TestSetup.testInitialize_after_setup_revert_KEVM "
|
|
"--test TestSetup.testSetup_after_setup_revert_KEVM "
|
|
)
|
|
|
|
# Comment these lines as needed
|
|
pkill kore-rpc || true
|
|
forge_build
|
|
foundry_kompile
|
|
foundry_prove
|