diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index 4cb4bcb..d86f19f 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -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" + } + ] + } } diff --git a/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch b/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch new file mode 120000 index 0000000..54ca445 --- /dev/null +++ b/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch @@ -0,0 +1 @@ +../001_accumulateFlows_off_by_one.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/002_flowOut_rate_calculation.patch b/certora/mutations/Accounts/002_flowOut_rate_calculation.patch new file mode 120000 index 0000000..544c078 --- /dev/null +++ b/certora/mutations/Accounts/002_flowOut_rate_calculation.patch @@ -0,0 +1 @@ +../002_flowOut_rate_calculation.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch b/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch new file mode 120000 index 0000000..c15bd62 --- /dev/null +++ b/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch @@ -0,0 +1 @@ +../004_isSolventAt_boundary_condition.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/005_flowIn_future_timestamp.patch b/certora/mutations/Accounts/005_flowIn_future_timestamp.patch new file mode 120000 index 0000000..faa53e1 --- /dev/null +++ b/certora/mutations/Accounts/005_flowIn_future_timestamp.patch @@ -0,0 +1 @@ +../005_flowIn_future_timestamp.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/017_accountId_encoding_corruption.patch b/certora/mutations/Accounts/017_accountId_encoding_corruption.patch new file mode 120000 index 0000000..cbc374d --- /dev/null +++ b/certora/mutations/Accounts/017_accountId_encoding_corruption.patch @@ -0,0 +1 @@ +../017_accountId_encoding_corruption.patch \ No newline at end of file diff --git a/certora/mutations/Funds/003_status_boundary_condition.patch b/certora/mutations/Funds/003_status_boundary_condition.patch new file mode 120000 index 0000000..9c4390e --- /dev/null +++ b/certora/mutations/Funds/003_status_boundary_condition.patch @@ -0,0 +1 @@ +../003_status_boundary_condition.patch \ No newline at end of file diff --git a/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch b/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch new file mode 120000 index 0000000..14cc89a --- /dev/null +++ b/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch @@ -0,0 +1 @@ +../018_duration_calculation_order_inversion.patch \ No newline at end of file diff --git a/certora/mutations/Vault/015_transfer_authorization_bypass.patch b/certora/mutations/Vault/015_transfer_authorization_bypass.patch new file mode 120000 index 0000000..1d43500 --- /dev/null +++ b/certora/mutations/Vault/015_transfer_authorization_bypass.patch @@ -0,0 +1 @@ +../015_transfer_authorization_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/016_pause_functions_deleted.patch b/certora/mutations/Vault/016_pause_functions_deleted.patch new file mode 120000 index 0000000..9ec9fc7 --- /dev/null +++ b/certora/mutations/Vault/016_pause_functions_deleted.patch @@ -0,0 +1 @@ +../016_pause_functions_deleted.patch \ No newline at end of file diff --git a/certora/mutations/Vault/020_withdraw_pause_bypass.patch b/certora/mutations/Vault/020_withdraw_pause_bypass.patch new file mode 120000 index 0000000..8fd710f --- /dev/null +++ b/certora/mutations/Vault/020_withdraw_pause_bypass.patch @@ -0,0 +1 @@ +../020_withdraw_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/021_deposit_pause_bypass.patch b/certora/mutations/Vault/021_deposit_pause_bypass.patch new file mode 120000 index 0000000..e843aed --- /dev/null +++ b/certora/mutations/Vault/021_deposit_pause_bypass.patch @@ -0,0 +1 @@ +../021_deposit_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/022_transfer_pause_bypass.patch b/certora/mutations/Vault/022_transfer_pause_bypass.patch new file mode 120000 index 0000000..be96903 --- /dev/null +++ b/certora/mutations/Vault/022_transfer_pause_bypass.patch @@ -0,0 +1 @@ +../022_transfer_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/023_flow_pause_bypass.patch b/certora/mutations/Vault/023_flow_pause_bypass.patch new file mode 120000 index 0000000..666ad2b --- /dev/null +++ b/certora/mutations/Vault/023_flow_pause_bypass.patch @@ -0,0 +1 @@ +../023_flow_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/024_lock_pause_bypass.patch b/certora/mutations/Vault/024_lock_pause_bypass.patch new file mode 120000 index 0000000..ce642ba --- /dev/null +++ b/certora/mutations/Vault/024_lock_pause_bypass.patch @@ -0,0 +1 @@ +../024_lock_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/025_extendLock_pause_bypass.patch b/certora/mutations/Vault/025_extendLock_pause_bypass.patch new file mode 120000 index 0000000..855a17a --- /dev/null +++ b/certora/mutations/Vault/025_extendLock_pause_bypass.patch @@ -0,0 +1 @@ +../025_extendLock_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/026_designate_pause_bypass.patch b/certora/mutations/Vault/026_designate_pause_bypass.patch new file mode 120000 index 0000000..9691134 --- /dev/null +++ b/certora/mutations/Vault/026_designate_pause_bypass.patch @@ -0,0 +1 @@ +../026_designate_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch b/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch new file mode 120000 index 0000000..d7c9a37 --- /dev/null +++ b/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch @@ -0,0 +1 @@ +../027_burnDesignated_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/028_burnAccount_pause_bypass.patch b/certora/mutations/Vault/028_burnAccount_pause_bypass.patch new file mode 120000 index 0000000..a84b025 --- /dev/null +++ b/certora/mutations/Vault/028_burnAccount_pause_bypass.patch @@ -0,0 +1 @@ +../028_burnAccount_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/029_freezeFund_pause_bypass.patch b/certora/mutations/Vault/029_freezeFund_pause_bypass.patch new file mode 120000 index 0000000..93d2574 --- /dev/null +++ b/certora/mutations/Vault/029_freezeFund_pause_bypass.patch @@ -0,0 +1 @@ +../029_freezeFund_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch b/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch new file mode 120000 index 0000000..f962414 --- /dev/null +++ b/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch @@ -0,0 +1 @@ +../030_add_missing_whenNotPaused_withdrawByRecipient.patch \ No newline at end of file diff --git a/certora/mutations/Vault/031_pause_access_control_bypass.patch b/certora/mutations/Vault/031_pause_access_control_bypass.patch new file mode 120000 index 0000000..7e2845e --- /dev/null +++ b/certora/mutations/Vault/031_pause_access_control_bypass.patch @@ -0,0 +1 @@ +../031_pause_access_control_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/032_unpause_access_control_bypass.patch b/certora/mutations/Vault/032_unpause_access_control_bypass.patch new file mode 120000 index 0000000..cd222ed --- /dev/null +++ b/certora/mutations/Vault/032_unpause_access_control_bypass.patch @@ -0,0 +1 @@ +../032_unpause_access_control_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch b/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch new file mode 120000 index 0000000..b836cc1 --- /dev/null +++ b/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch @@ -0,0 +1 @@ +../033_withdrawByRecipient_auth_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/006_flow_prelock_bypass.patch b/certora/mutations/VaultBase/006_flow_prelock_bypass.patch new file mode 120000 index 0000000..cbad95a --- /dev/null +++ b/certora/mutations/VaultBase/006_flow_prelock_bypass.patch @@ -0,0 +1 @@ +../006_flow_prelock_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch b/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch new file mode 120000 index 0000000..ba56833 --- /dev/null +++ b/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch @@ -0,0 +1 @@ +../007_checkAccountInvariant_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/008_deposit_storage_corruption.patch b/certora/mutations/VaultBase/008_deposit_storage_corruption.patch new file mode 120000 index 0000000..7bf533d --- /dev/null +++ b/certora/mutations/VaultBase/008_deposit_storage_corruption.patch @@ -0,0 +1 @@ +../008_deposit_storage_corruption.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch b/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch new file mode 120000 index 0000000..72391f7 --- /dev/null +++ b/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch @@ -0,0 +1 @@ +../009_transfer_balance_check_removal.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch b/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch new file mode 120000 index 0000000..3d1dc34 --- /dev/null +++ b/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch @@ -0,0 +1 @@ +../010_burnAccount_logic_inversion.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch b/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch new file mode 120000 index 0000000..585f2bf --- /dev/null +++ b/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch @@ -0,0 +1 @@ +../011_withdraw_reentrancy_ordering.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch b/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch new file mode 120000 index 0000000..3a51b46 --- /dev/null +++ b/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch @@ -0,0 +1 @@ +../012_withdraw_unsafe_transfer.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch b/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch new file mode 120000 index 0000000..4ecfe39 --- /dev/null +++ b/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch @@ -0,0 +1 @@ +../013_deposit_unsafe_transferFrom.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch b/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch new file mode 120000 index 0000000..faccde9 --- /dev/null +++ b/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch @@ -0,0 +1 @@ +../014_all_unsafe_token_transfers.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch b/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch new file mode 120000 index 0000000..ece025c --- /dev/null +++ b/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch @@ -0,0 +1 @@ +../035_withdraw_account_not_deleted.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch b/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch new file mode 120000 index 0000000..84f4792 --- /dev/null +++ b/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch @@ -0,0 +1 @@ +../036_burnAccount_not_deleted.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch b/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch new file mode 120000 index 0000000..8fba259 --- /dev/null +++ b/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch @@ -0,0 +1 @@ +../037_burnDesignated_no_decrement.patch \ No newline at end of file