Added mutations to config file

This commit is contained in:
Jochen Hoenicke 2025-08-01 17:33:35 +02:00
parent 6c96ce84de
commit ff6b69caed
36 changed files with 62 additions and 3 deletions

View File

@ -8,14 +8,38 @@
"VaultHarness:_token=ERC20A",
],
"packages": [
"@openzeppelin/=node_modules/@openzeppelin",
"@openzeppelin/=node_modules/@openzeppelin/",
],
"msg": "Verifying Vault",
//"msg": "Verifying Vault",
"multi_assert_check": true,
"rule_sanity": "basic",
"verify": "VaultHarness:certora/specs/Vault.spec",
"loop_iter": "3",
"build_cache": true,
"solc": "solc8.28",
"prover_version": "master" // remove with next Certora release
"prover_version": "master", // remove with next Certora release
"mutations": {
"manual_mutants": [
{
"file_to_mutate": "contracts/Vault.sol",
"mutants_location": "certora/mutations/Vault"
},
{
"file_to_mutate": "contracts/Timestamps.sol",
"mutants_location": "certora/mutations/Timestamps"
},
{
"file_to_mutate": "contracts/vault/Accounts.sol",
"mutants_location": "certora/mutations/Accounts"
},
{
"file_to_mutate": "contracts/vault/Funds.sol",
"mutants_location": "certora/mutations/Funds"
},
{
"file_to_mutate": "contracts/vault/VaultBase.sol",
"mutants_location": "certora/mutations/VaultBase"
}
]
}
}

View File

@ -0,0 +1 @@
../001_accumulateFlows_off_by_one.patch

View File

@ -0,0 +1 @@
../002_flowOut_rate_calculation.patch

View File

@ -0,0 +1 @@
../004_isSolventAt_boundary_condition.patch

View File

@ -0,0 +1 @@
../005_flowIn_future_timestamp.patch

View File

@ -0,0 +1 @@
../017_accountId_encoding_corruption.patch

View File

@ -0,0 +1 @@
../003_status_boundary_condition.patch

View File

@ -0,0 +1 @@
../018_duration_calculation_order_inversion.patch

View File

@ -0,0 +1 @@
../015_transfer_authorization_bypass.patch

View File

@ -0,0 +1 @@
../016_pause_functions_deleted.patch

View File

@ -0,0 +1 @@
../020_withdraw_pause_bypass.patch

View File

@ -0,0 +1 @@
../021_deposit_pause_bypass.patch

View File

@ -0,0 +1 @@
../022_transfer_pause_bypass.patch

View File

@ -0,0 +1 @@
../023_flow_pause_bypass.patch

View File

@ -0,0 +1 @@
../024_lock_pause_bypass.patch

View File

@ -0,0 +1 @@
../025_extendLock_pause_bypass.patch

View File

@ -0,0 +1 @@
../026_designate_pause_bypass.patch

View File

@ -0,0 +1 @@
../027_burnDesignated_pause_bypass.patch

View File

@ -0,0 +1 @@
../028_burnAccount_pause_bypass.patch

View File

@ -0,0 +1 @@
../029_freezeFund_pause_bypass.patch

View File

@ -0,0 +1 @@
../030_add_missing_whenNotPaused_withdrawByRecipient.patch

View File

@ -0,0 +1 @@
../031_pause_access_control_bypass.patch

View File

@ -0,0 +1 @@
../032_unpause_access_control_bypass.patch

View File

@ -0,0 +1 @@
../033_withdrawByRecipient_auth_bypass.patch

View File

@ -0,0 +1 @@
../006_flow_prelock_bypass.patch

View File

@ -0,0 +1 @@
../007_checkAccountInvariant_bypass.patch

View File

@ -0,0 +1 @@
../008_deposit_storage_corruption.patch

View File

@ -0,0 +1 @@
../009_transfer_balance_check_removal.patch

View File

@ -0,0 +1 @@
../010_burnAccount_logic_inversion.patch

View File

@ -0,0 +1 @@
../011_withdraw_reentrancy_ordering.patch

View File

@ -0,0 +1 @@
../012_withdraw_unsafe_transfer.patch

View File

@ -0,0 +1 @@
../013_deposit_unsafe_transferFrom.patch

View File

@ -0,0 +1 @@
../014_all_unsafe_token_transfers.patch

View File

@ -0,0 +1 @@
../035_withdraw_account_not_deleted.patch

View File

@ -0,0 +1 @@
../036_burnAccount_not_deleted.patch

View File

@ -0,0 +1 @@
../037_burnDesignated_no_decrement.patch