From 70ea3a08c6abe8fb30d654ccb8c63448d36c5bf4 Mon Sep 17 00:00:00 2001 From: Noa Babliki Date: Thu, 12 Jan 2023 16:52:36 +0200 Subject: [PATCH 1/9] added vscode download recommendation to the readme --- 01.Lesson_GettingStarted/README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/01.Lesson_GettingStarted/README.md b/01.Lesson_GettingStarted/README.md index 696016a0..b7d90f69 100644 --- a/01.Lesson_GettingStarted/README.md +++ b/01.Lesson_GettingStarted/README.md @@ -16,6 +16,8 @@ - [x] In the VSCode extensions/marketplace search for [Certora Verification Language LSP](https://marketplace.visualstudio.com/items?itemName=Certora.evmspec-lsp) and install it. This is an extension developed for supporting the spec language - the language in which we will be writing specifications. The extension supports syntax highlighting, autocompletion and more. +- [x] It is recommanded to install [Certora IDE](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover) in the VSCode extensions/marketplace as well, to get an easy-to-use interface for running jobs. + - [x] It is also recommended to install the [Ethereum Security Bundle](https://marketplace.visualstudio.com/items?itemName=tintinweb.ethereum-security-bundle) by tintinweb on the VSCode extensions/marketplace, to get support for the Solidity contracts.
From f2672a843cac3bad5a62408ccef40a31320cb622 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Wed, 15 Feb 2023 14:48:56 +0200 Subject: [PATCH 2/9] conf files for bank,borda,erc20 --- .../certora/conf/bank_integrityofdeposit.conf | 16 ++++++++++++++++ .../conf/bankfixed_integrityofdeposit.conf | 16 ++++++++++++++++ .../bankfixed_running_with_precondition.conf | 15 +++++++++++++++ .../conf/bankfixed_totalfundsafterdepos.conf | 18 ++++++++++++++++++ .../certora/conf/parametric_rule_on_bank.conf | 15 +++++++++++++++ ...tric_rule_on_bank_validityoftotalfunds.conf | 18 ++++++++++++++++++ .../conf/parametric_rule_on_bankfixed.conf | 15 +++++++++++++++ .../Borda/certora/conf/bordabug1.conf | 16 ++++++++++++++++ .../Borda/certora/conf/bordabug2.conf | 16 ++++++++++++++++ .../Borda/certora/conf/bordabug3.conf | 16 ++++++++++++++++ .../Borda/certora/conf/bordabug4.conf | 16 ++++++++++++++++ .../Borda/certora/conf/bordabugfixed.conf | 16 ++++++++++++++++ .../ERC20/certora/conf/erc20bug1.conf | 16 ++++++++++++++++ .../ERC20/certora/conf/erc20bug2.conf | 16 ++++++++++++++++ .../ERC20/certora/conf/erc20bug3.conf | 16 ++++++++++++++++ .../ERC20/certora/conf/erc20bug4.conf | 16 ++++++++++++++++ .../ERC20/certora/conf/erc20bugfixed.conf | 16 ++++++++++++++++ 17 files changed, 273 insertions(+) create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/bank_integrityofdeposit.conf create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_integrityofdeposit.conf create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_running_with_precondition.conf create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_totalfundsafterdepos.conf create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank.conf create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf create mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bankfixed.conf create mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf create mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf create mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf create mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf create mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf create mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf create mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf create mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf create mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf create mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/bank_integrityofdeposit.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bank_integrityofdeposit.conf new file mode 100644 index 00000000..03dbe2f5 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bank_integrityofdeposit.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "Bank.sol:Bank" + ], + "verify": [ + "Bank:IntegrityOfDeposit.spec" + ], + "solc": "solc7.6", + "msg": "Bank IntegrityOfDeposit", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_integrityofdeposit.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_integrityofdeposit.conf new file mode 100644 index 00000000..fad57ba3 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_integrityofdeposit.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BankFixed.sol:Bank" + ], + "verify": [ + "Bank:IntegrityOfDeposit.spec" + ], + "solc": "solc7.6", + "msg": "BankFixed IntegrityOfDeposit", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_running_with_precondition.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_running_with_precondition.conf new file mode 100644 index 00000000..6ea8a3a0 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_running_with_precondition.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "BankFixed.sol:Bank" + ], + "verify": [ + "Bank:TotalGreaterThanUser.spec" + ], + "solc": "solc7.6", + "msg": "BankFixed running with precondition", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_totalfundsafterdepos.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_totalfundsafterdepos.conf new file mode 100644 index 00000000..293c4f23 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/bankfixed_totalfundsafterdepos.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "BankFixed.sol:Bank" + ], + "verify": [ + "Bank:TotalGreaterThanUser.spec" + ], + "solc": "solc7.6", + "msg": "BankFixed totalFundsAfterDepos", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "rule": [ + "totalFundsAfterDeposit" + ], + "process": "emv" +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank.conf new file mode 100644 index 00000000..03112a68 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "Bank.sol:Bank" + ], + "verify": [ + "Bank:Parametric.spec" + ], + "solc": "solc7.6", + "msg": "parametric rule on Bank", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf new file mode 100644 index 00000000..3340afb0 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "Bank.sol:Bank" + ], + "verify": [ + "Bank:Parametric.spec" + ], + "solc": "solc7.6", + "msg": "", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv", + "rule": [ + "validityOfTotalFunds" + ] +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bankfixed.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bankfixed.conf new file mode 100644 index 00000000..61433558 --- /dev/null +++ b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bankfixed.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "BankFixed.sol:Bank" + ], + "verify": [ + "Bank:Parametric.spec" + ], + "solc": "solc7.6", + "msg": "parametric rule on BankFixed", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf new file mode 100644 index 00000000..a7543b07 --- /dev/null +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BordaBug1.sol:Borda" + ], + "verify": [ + "Borda:Borda.spec" + ], + "solc": "solc7.6", + "msg": "BordaBug1", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf new file mode 100644 index 00000000..d9e47d40 --- /dev/null +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BordaBug2.sol:Borda" + ], + "verify": [ + "Borda:Borda.spec" + ], + "solc": "solc7.6", + "msg": "BordaBug2", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf new file mode 100644 index 00000000..ac97236a --- /dev/null +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BordaBug3.sol:Borda" + ], + "verify": [ + "Borda:Borda.spec" + ], + "solc": "solc7.6", + "msg": "BordaBug3", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf new file mode 100644 index 00000000..d36b839e --- /dev/null +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BordaBug4.sol:Borda" + ], + "verify": [ + "Borda:Borda.spec" + ], + "solc": "solc7.6", + "msg": "BordaBug4", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf new file mode 100644 index 00000000..9a5d83c9 --- /dev/null +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BordaFixed.sol:Borda" + ], + "verify": [ + "Borda:Borda.spec" + ], + "solc": "solc7.6", + "msg": "BordaBugFixed", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf new file mode 100644 index 00000000..25499d97 --- /dev/null +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20Bug1.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "ERC20Bug1", + "optimistic_loop": true, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf new file mode 100644 index 00000000..66af35d3 --- /dev/null +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20Bug2.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "ERC20Bug2", + "optimistic_loop": true, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf new file mode 100644 index 00000000..4dd44651 --- /dev/null +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20Bug3.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "ERC20Bug3", + "optimistic_loop": true, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf new file mode 100644 index 00000000..4a0416e7 --- /dev/null +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20Bug4.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "ERC20Bug4", + "optimistic_loop": true, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf new file mode 100644 index 00000000..b8fa90ce --- /dev/null +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20Fixed.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "ERC20BugFixed", + "optimistic_loop": true, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file From 28804cd3b88a193845aae603d8084a6b3497bfb3 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Wed, 15 Feb 2023 17:11:11 +0200 Subject: [PATCH 3/9] renames, additional confs --- .../conf/{bordabug1.conf => borda_bug_1.conf} | 2 +- .../conf/{bordabug2.conf => borda_bug_2.conf} | 2 +- .../conf/{bordabug3.conf => borda_bug_3.conf} | 2 +- .../conf/{bordabug4.conf => borda_bug_4.conf} | 2 +- .../{bordabugfixed.conf => borda_bug_fixed.conf} | 2 +- .../conf/{erc20bug1.conf => erc20_bug_1.conf} | 2 +- .../conf/{erc20bug2.conf => erc20_bug_2.conf} | 2 +- .../conf/{erc20bug3.conf => erc20_bug_3.conf} | 2 +- .../conf/{erc20bug4.conf => erc20_bug_4.conf} | 2 +- .../{erc20bugfixed.conf => erc20_bug_fixed.conf} | 2 +- .../certora/conf/meeting_scheduler_1.conf | 16 ++++++++++++++++ .../certora/conf/meeting_scheduler_2.conf | 16 ++++++++++++++++ .../certora/conf/meeting_scheduler_3.conf | 16 ++++++++++++++++ .../certora/conf/meeting_scheduler_4.conf | 16 ++++++++++++++++ .../certora/conf/meeting_scheduler_fixed.conf | 16 ++++++++++++++++ .../certora/conf/run_broken.conf | 14 ++++++++++++++ .../certora/conf/run_fixed.conf | 15 +++++++++++++++ .../TicketDepot/certora/conf/sanity.conf | 15 +++++++++++++++ .../BallGame/certora/conf/ball_game.conf | 15 +++++++++++++++ .../Manager/certora/conf/manager.conf | 16 ++++++++++++++++ .../Manager/certora/conf/manager_solution.conf | 16 ++++++++++++++++ 21 files changed, 181 insertions(+), 10 deletions(-) rename 02.Lesson_InvestigateViolations/Borda/certora/conf/{bordabug1.conf => borda_bug_1.conf} (91%) rename 02.Lesson_InvestigateViolations/Borda/certora/conf/{bordabug2.conf => borda_bug_2.conf} (91%) rename 02.Lesson_InvestigateViolations/Borda/certora/conf/{bordabug3.conf => borda_bug_3.conf} (91%) rename 02.Lesson_InvestigateViolations/Borda/certora/conf/{bordabug4.conf => borda_bug_4.conf} (91%) rename 02.Lesson_InvestigateViolations/Borda/certora/conf/{bordabugfixed.conf => borda_bug_fixed.conf} (90%) rename 02.Lesson_InvestigateViolations/ERC20/certora/conf/{erc20bug1.conf => erc20_bug_1.conf} (91%) rename 02.Lesson_InvestigateViolations/ERC20/certora/conf/{erc20bug2.conf => erc20_bug_2.conf} (91%) rename 02.Lesson_InvestigateViolations/ERC20/certora/conf/{erc20bug3.conf => erc20_bug_3.conf} (91%) rename 02.Lesson_InvestigateViolations/ERC20/certora/conf/{erc20bug4.conf => erc20_bug_4.conf} (91%) rename 02.Lesson_InvestigateViolations/ERC20/certora/conf/{erc20bugfixed.conf => erc20_bug_fixed.conf} (90%) create mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf create mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf create mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf create mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf create mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf create mode 100644 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf create mode 100644 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf create mode 100644 06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf create mode 100644 07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf create mode 100644 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf create mode 100644 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_1.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf rename to 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_1.conf index a7543b07..d7d62b30 100644 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug1.conf +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_1.conf @@ -6,7 +6,7 @@ "Borda:Borda.spec" ], "solc": "solc7.6", - "msg": "BordaBug1", + "msg": "borda bug 1", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf rename to 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf index d9e47d40..6aa4d193 100644 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug2.conf +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf @@ -6,7 +6,7 @@ "Borda:Borda.spec" ], "solc": "solc7.6", - "msg": "BordaBug2", + "msg": "borda bug 2", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf rename to 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf index ac97236a..e9cf7955 100644 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug3.conf +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf @@ -6,7 +6,7 @@ "Borda:Borda.spec" ], "solc": "solc7.6", - "msg": "BordaBug3", + "msg": "borda bug 3", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf rename to 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf index d36b839e..bbee0db5 100644 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabug4.conf +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf @@ -6,7 +6,7 @@ "Borda:Borda.spec" ], "solc": "solc7.6", - "msg": "BordaBug4", + "msg": "borda bug 4", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf similarity index 90% rename from 02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf rename to 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf index 9a5d83c9..c755d1eb 100644 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/bordabugfixed.conf +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf @@ -6,7 +6,7 @@ "Borda:Borda.spec" ], "solc": "solc7.6", - "msg": "BordaBugFixed", + "msg": "borda bug fixed", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf rename to 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf index 25499d97..6b53c296 100644 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug1.conf +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "ERC20Bug1", + "msg": "erc20 bug 1", "optimistic_loop": true, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf rename to 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf index 66af35d3..7b1c4f13 100644 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug2.conf +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "ERC20Bug2", + "msg": "erc20 bug 2", "optimistic_loop": true, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf rename to 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf index 4dd44651..30081757 100644 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug3.conf +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "ERC20Bug3", + "msg": "erc20 bug 3", "optimistic_loop": true, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf similarity index 91% rename from 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf rename to 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf index 4a0416e7..5ad8b8f9 100644 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bug4.conf +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "ERC20Bug4", + "msg": "erc20 bug 4", "optimistic_loop": true, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_fixed.conf similarity index 90% rename from 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf rename to 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_fixed.conf index b8fa90ce..488960af 100644 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20bugfixed.conf +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_fixed.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "ERC20BugFixed", + "msg": "erc20 bug fixed", "optimistic_loop": true, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf new file mode 100644 index 00000000..dbe661a5 --- /dev/null +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "MeetingSchedulerBug1.sol:MeetingScheduler" + ], + "verify": [ + "MeetingScheduler:meetings.spec" + ], + "solc": "solc8.7", + "msg": "meeting scheduler 1", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf new file mode 100644 index 00000000..c7362a82 --- /dev/null +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "MeetingSchedulerBug2.sol:MeetingScheduler" + ], + "verify": [ + "MeetingScheduler:meetings.spec" + ], + "solc": "solc8.7", + "msg": "meeting scheduler 2", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf new file mode 100644 index 00000000..1408b1b6 --- /dev/null +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "MeetingSchedulerBug3.sol:MeetingScheduler" + ], + "verify": [ + "MeetingScheduler:meetings.spec" + ], + "solc": "solc8.7", + "msg": "meeting scheduler 3", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf new file mode 100644 index 00000000..b30c57bd --- /dev/null +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "MeetingSchedulerBug4.sol:MeetingScheduler" + ], + "verify": [ + "MeetingScheduler:meetings.spec" + ], + "solc": "solc8.7", + "msg": "meeting scheduler 4", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf new file mode 100644 index 00000000..271f40ae --- /dev/null +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "MeetingSchedulerFixed.sol:MeetingScheduler" + ], + "verify": [ + "MeetingScheduler:meetings.spec" + ], + "solc": "solc8.7", + "msg": "meeting scheduler fixed", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf new file mode 100644 index 00000000..840d9c5b --- /dev/null +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "AuctionBroken.sol:System" + ], + "verify": [ + "System:Auction.spec" + ], + "solc": "solc5.12", + "msg": "run broken", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true +} \ No newline at end of file diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf new file mode 100644 index 00000000..74fd032a --- /dev/null +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "AuctionFixed.sol:System" + ], + "verify": [ + "System:Auction.spec" + ], + "solc": "solc5.12", + "msg": "run fixed", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf b/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf new file mode 100644 index 00000000..82600831 --- /dev/null +++ b/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "TicketDepot.sol:TicketDepot" + ], + "verify": [ + "TicketDepot:sanity.spec" + ], + "solc": "solc6.12", + "msg": "sanity", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf new file mode 100644 index 00000000..f9587669 --- /dev/null +++ b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "BallGame.sol:BallGame" + ], + "verify": [ + "BallGame:BallGame.spec" + ], + "solc": "solc8.6", + "msg": "ball game", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf new file mode 100644 index 00000000..751347d3 --- /dev/null +++ b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "Manager.sol:Manager" + ], + "verify": [ + "Manager:Manager.spec" + ], + "solc": "solc8.6", + "msg": "Manager", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf new file mode 100644 index 00000000..d41b355b --- /dev/null +++ b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "Manager.sol:Manager" + ], + "verify": [ + "Manager:ManagerPartialSolution.spec" + ], + "solc": "solc8.6", + "msg": "Manager solution", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file From 5bb92a4bfae9dcfe0e43446f4317d563f447e953 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Wed, 15 Feb 2023 18:10:15 +0200 Subject: [PATCH 4/9] vscode instructions to ex1 --- .../BankLesson1/README.md | 21 +++++++++++++++++++ ...ric_rule_on_bank_validityoftotalfunds.conf | 18 ---------------- .../Bank/certora/conf/bank_invariant.conf | 14 +++++++++++++ .../certora/conf/managet_invariant.conf | 8 +++---- 4 files changed, 38 insertions(+), 23 deletions(-) delete mode 100644 01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf create mode 100644 07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf rename 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf => 08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf (52%) diff --git a/01.Lesson_GettingStarted/BankLesson1/README.md b/01.Lesson_GettingStarted/BankLesson1/README.md index 131e3548..97dd22e2 100644 --- a/01.Lesson_GettingStarted/BankLesson1/README.md +++ b/01.Lesson_GettingStarted/BankLesson1/README.md @@ -73,6 +73,11 @@ certoraRun --help
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***bank integrityofdeposit***. +
+ ### ***Results*** The prover will print various information to the console. @@ -124,6 +129,11 @@ No violations were found. Great!
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***bankfixed integrityofdeposit***. +
+ ## Preconditions and Helper Variables Let’s define [another property](TotalGreaterThanUser.spec) and verify that after deposit, the `totalFunds` in the system are at least the funds of the `msg.sender`: @@ -169,6 +179,11 @@ You will see the message in the run results mail and in the job's list in [prove
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the jobs ***bankfixed totalfundsafterdepos*** and ***bankfixed running with precondition***. +
+ ## Parametric Rules This property can be generalized to hold to all functions. @@ -212,3 +227,9 @@ Notice that this rule uncovers the bug detected by P1: integrity of deposit. Parametric rules enable expressing reusable and concise correctness conditions. Note that they are not dependent on the implementation. You can integrate them easily into the CI to verify changes to the code, including signature changes, new functions, and implementation changes. + +
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the jobs ***parametric rule on bank*** and ***parametric rule on bankfixed***. +
diff --git a/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf b/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf deleted file mode 100644 index 3340afb0..00000000 --- a/01.Lesson_GettingStarted/BankLesson1/certora/conf/parametric_rule_on_bank_validityoftotalfunds.conf +++ /dev/null @@ -1,18 +0,0 @@ -{ - "files": [ - "Bank.sol:Bank" - ], - "verify": [ - "Bank:Parametric.spec" - ], - "solc": "solc7.6", - "msg": "", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "disableLocalTypeChecking": true, - "process": "emv", - "rule": [ - "validityOfTotalFunds" - ] -} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf new file mode 100644 index 00000000..4b7b7f91 --- /dev/null +++ b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "BankFixed.sol:Bank" + ], + "verify": [ + "Bank:invariant.spec" + ], + "solc": "solc7.6", + "msg": "bank invariant", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf b/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf similarity index 52% rename from 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf rename to 08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf index d41b355b..74e1cc5b 100644 --- a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager_solution.conf +++ b/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf @@ -3,14 +3,12 @@ "Manager.sol:Manager" ], "verify": [ - "Manager:ManagerPartialSolution.spec" + "Manager:ManagerFullSolution.spec" ], "solc": "solc8.6", - "msg": "Manager solution", + "msg": "Managet invariant", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false + "disableLocalTypeChecking": true } \ No newline at end of file From 6b87de959d1216f915d1917d58600b65f4eeb052 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Mon, 6 Mar 2023 13:13:47 +0200 Subject: [PATCH 5/9] deleted spare confs, added vscode to lesson 2 readme --- .../Borda/certora/conf/borda_bug_2.conf | 16 ---------------- .../Borda/certora/conf/borda_bug_3.conf | 16 ---------------- .../Borda/certora/conf/borda_bug_4.conf | 16 ---------------- .../Borda/certora/conf/borda_bug_fixed.conf | 16 ---------------- .../ERC20/certora/conf/erc20_bug_1.conf | 16 ---------------- .../ERC20/certora/conf/erc20_bug_2.conf | 16 ---------------- .../ERC20/certora/conf/erc20_bug_3.conf | 16 ---------------- .../ERC20/certora/conf/erc20_bug_4.conf | 16 ---------------- .../certora/conf/meeting_scheduler_2.conf | 16 ---------------- .../certora/conf/meeting_scheduler_3.conf | 16 ---------------- .../certora/conf/meeting_scheduler_4.conf | 16 ---------------- .../certora/conf/meeting_scheduler_fixed.conf | 16 ---------------- 02.Lesson_InvestigateViolations/README.md | 3 ++- 13 files changed, 2 insertions(+), 193 deletions(-) delete mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf delete mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf delete mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf delete mode 100644 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf delete mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf delete mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf delete mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf delete mode 100644 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf delete mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf delete mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf delete mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf delete mode 100644 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf deleted file mode 100644 index 6aa4d193..00000000 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_2.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "BordaBug2.sol:Borda" - ], - "verify": [ - "Borda:Borda.spec" - ], - "solc": "solc7.6", - "msg": "borda bug 2", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf deleted file mode 100644 index e9cf7955..00000000 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_3.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "BordaBug3.sol:Borda" - ], - "verify": [ - "Borda:Borda.spec" - ], - "solc": "solc7.6", - "msg": "borda bug 3", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf deleted file mode 100644 index bbee0db5..00000000 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_4.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "BordaBug4.sol:Borda" - ], - "verify": [ - "Borda:Borda.spec" - ], - "solc": "solc7.6", - "msg": "borda bug 4", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf deleted file mode 100644 index c755d1eb..00000000 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_fixed.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "BordaFixed.sol:Borda" - ], - "verify": [ - "Borda:Borda.spec" - ], - "solc": "solc7.6", - "msg": "borda bug fixed", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf deleted file mode 100644 index 6b53c296..00000000 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_1.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "ERC20Bug1.sol:ERC20" - ], - "verify": [ - "ERC20:ERC20.spec" - ], - "solc": "solc8.0", - "msg": "erc20 bug 1", - "optimistic_loop": true, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf deleted file mode 100644 index 7b1c4f13..00000000 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_2.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "ERC20Bug2.sol:ERC20" - ], - "verify": [ - "ERC20:ERC20.spec" - ], - "solc": "solc8.0", - "msg": "erc20 bug 2", - "optimistic_loop": true, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf deleted file mode 100644 index 30081757..00000000 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_3.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "ERC20Bug3.sol:ERC20" - ], - "verify": [ - "ERC20:ERC20.spec" - ], - "solc": "solc8.0", - "msg": "erc20 bug 3", - "optimistic_loop": true, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf deleted file mode 100644 index 5ad8b8f9..00000000 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_4.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "ERC20Bug4.sol:ERC20" - ], - "verify": [ - "ERC20:ERC20.spec" - ], - "solc": "solc8.0", - "msg": "erc20 bug 4", - "optimistic_loop": true, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf deleted file mode 100644 index c7362a82..00000000 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_2.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "MeetingSchedulerBug2.sol:MeetingScheduler" - ], - "verify": [ - "MeetingScheduler:meetings.spec" - ], - "solc": "solc8.7", - "msg": "meeting scheduler 2", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf deleted file mode 100644 index 1408b1b6..00000000 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_3.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "MeetingSchedulerBug3.sol:MeetingScheduler" - ], - "verify": [ - "MeetingScheduler:meetings.spec" - ], - "solc": "solc8.7", - "msg": "meeting scheduler 3", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf deleted file mode 100644 index b30c57bd..00000000 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_4.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "MeetingSchedulerBug4.sol:MeetingScheduler" - ], - "verify": [ - "MeetingScheduler:meetings.spec" - ], - "solc": "solc8.7", - "msg": "meeting scheduler 4", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf deleted file mode 100644 index 271f40ae..00000000 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_fixed.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "MeetingSchedulerFixed.sol:MeetingScheduler" - ], - "verify": [ - "MeetingScheduler:meetings.spec" - ], - "solc": "solc8.7", - "msg": "meeting scheduler fixed", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/README.md b/02.Lesson_InvestigateViolations/README.md index 25016d5e..69271b9c 100644 --- a/02.Lesson_InvestigateViolations/README.md +++ b/02.Lesson_InvestigateViolations/README.md @@ -34,11 +34,12 @@ For each of the systems in this directory do as follows:
- [ ] Create a script (or multiple scripts) that will serve you for running the verifications of the system's buggy versions. +- [ ] Alternatively, create a new empty job in the VSCode IDE or upload an existing file. > :bulb: >
> Script Hint -> Craft your script wisely - use the `--rule` to filter out information that isn't of your interest. +> Craft your script wisely - use the `--rule` to filter out information that isn't of your interest ('Rules' is under 'Certora Spec' in the IDE's settings form). >

From 46addca9bbbb4ccaca3dd18efc6ba01ba21e840e Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Tue, 7 Mar 2023 11:05:26 +0200 Subject: [PATCH 6/9] lesson1 after master changes --- .../ERC20Lesson1/README.md | 11 +++++++++- .../conf/bankfixed_integrityofdeposit.conf | 16 -------------- .../bankfixed_running_with_precondition.conf | 15 ------------- .../conf/bankfixed_totalfundsafterdepos.conf | 18 ---------------- ...ank_integrityofdeposit.conf => erc20.conf} | 8 +++---- ...ric_rule_on_bank.conf => erc20_fixed.conf} | 8 +++---- ...kfixed.conf => erc20_parametric_rule.conf} | 8 +++---- .../conf/erc20_totalsupplyaftermint.conf | 21 +++++++++++++++++++ .../erc20_totalsupplyaftermintwithpreco.conf | 21 +++++++++++++++++++ 9 files changed, 64 insertions(+), 62 deletions(-) delete mode 100644 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_integrityofdeposit.conf delete mode 100644 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_running_with_precondition.conf delete mode 100644 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_totalfundsafterdepos.conf rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{bank_integrityofdeposit.conf => erc20.conf} (64%) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{parametric_rule_on_bank.conf => erc20_fixed.conf} (62%) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{parametric_rule_on_bankfixed.conf => erc20_parametric_rule.conf} (60%) create mode 100644 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf create mode 100644 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/README.md b/01.Lesson_GettingStarted/ERC20Lesson1/README.md index 5b540052..e116f5c8 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/README.md +++ b/01.Lesson_GettingStarted/ERC20Lesson1/README.md @@ -78,7 +78,7 @@ certoraRun --help ### ***Running in the IDE*** -Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***bank integrityofdeposit***. +Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***ERC20***.
### ***Results*** @@ -106,6 +106,15 @@ For each rule, the table either displays a checkmark when the rule was proved or
+## Results in VSCode IDE ## + +The results will appear under the job title. After a job is sent to the cloud, the 'Go To Rule Report' icon to the left of +the job will turn light blue. Clicking it will open the rule report in the web. + +To see the call trace, click a violated rule's details. + +
+ ## Understanding Rule Violations The Certora Prover helps understand violations of properties. diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_integrityofdeposit.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_integrityofdeposit.conf deleted file mode 100644 index fad57ba3..00000000 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_integrityofdeposit.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "BankFixed.sol:Bank" - ], - "verify": [ - "Bank:IntegrityOfDeposit.spec" - ], - "solc": "solc7.6", - "msg": "BankFixed IntegrityOfDeposit", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "smt_timeout": "600", - "loop_iter": "1", - "disableLocalTypeChecking": false -} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_running_with_precondition.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_running_with_precondition.conf deleted file mode 100644 index 6ea8a3a0..00000000 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_running_with_precondition.conf +++ /dev/null @@ -1,15 +0,0 @@ -{ - "files": [ - "BankFixed.sol:Bank" - ], - "verify": [ - "Bank:TotalGreaterThanUser.spec" - ], - "solc": "solc7.6", - "msg": "BankFixed running with precondition", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "disableLocalTypeChecking": true, - "process": "emv" -} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_totalfundsafterdepos.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_totalfundsafterdepos.conf deleted file mode 100644 index 293c4f23..00000000 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bankfixed_totalfundsafterdepos.conf +++ /dev/null @@ -1,18 +0,0 @@ -{ - "files": [ - "BankFixed.sol:Bank" - ], - "verify": [ - "Bank:TotalGreaterThanUser.spec" - ], - "solc": "solc7.6", - "msg": "BankFixed totalFundsAfterDepos", - "optimistic_loop": false, - "multi_assert_check": false, - "send_only": true, - "disableLocalTypeChecking": true, - "rule": [ - "totalFundsAfterDeposit" - ], - "process": "emv" -} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bank_integrityofdeposit.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20.conf similarity index 64% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bank_integrityofdeposit.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20.conf index 03dbe2f5..38ea1950 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/bank_integrityofdeposit.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20.conf @@ -1,12 +1,12 @@ { "files": [ - "Bank.sol:Bank" + "ERC20.sol:ERC20" ], "verify": [ - "Bank:IntegrityOfDeposit.spec" + "ERC20:ERC20.spec" ], - "solc": "solc7.6", - "msg": "Bank IntegrityOfDeposit", + "solc": "solc8.0", + "msg": "ERC20", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/parametric_rule_on_bank.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_fixed.conf similarity index 62% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/parametric_rule_on_bank.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_fixed.conf index 03112a68..659a865c 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/parametric_rule_on_bank.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_fixed.conf @@ -1,12 +1,12 @@ { "files": [ - "Bank.sol:Bank" + "ERC20.sol:ERC20" ], "verify": [ - "Bank:Parametric.spec" + "ERC20:ERC20Fixed.spec" ], - "solc": "solc7.6", - "msg": "parametric rule on Bank", + "solc": "solc8.0", + "msg": "erc20 fixed", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/parametric_rule_on_bankfixed.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_parametric_rule.conf similarity index 60% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/parametric_rule_on_bankfixed.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_parametric_rule.conf index 61433558..ff0b39dc 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/parametric_rule_on_bankfixed.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_parametric_rule.conf @@ -1,12 +1,12 @@ { "files": [ - "BankFixed.sol:Bank" + "ERC20.sol:ERC20" ], "verify": [ - "Bank:Parametric.spec" + "ERC20:Parametric.spec" ], - "solc": "solc7.6", - "msg": "parametric rule on BankFixed", + "solc": "solc8.0", + "msg": "erc20 parametric rule", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf new file mode 100644 index 00000000..82098a5e --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:TotalGreaterThanUser.spec" + ], + "solc": "solc8.0", + "msg": "erc20 totalSupplyAfterMint", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "rule": [ + "totalSupplyAfterMint" + ], + "process": "emv", + "settings": [ + "-rule=totalSupplyAfterMint" + ] +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf new file mode 100644 index 00000000..09e3ad5a --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:TotalGreaterThanUser.spec" + ], + "solc": "solc8.0", + "msg": "erc20 totalSupplyAfterMintWithPreco", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "rule": [ + "totalSupplyAfterMintWithPrecondition" + ], + "process": "emv", + "settings": [ + "-rule=totalSupplyAfterMintWithPrecondition" + ] +} \ No newline at end of file From 6eaf0da0768b18f72f63faf27b1fa461b8e2db90 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora <101042618+NoaBablikiCertora@users.noreply.github.com> Date: Tue, 7 Mar 2023 11:27:02 +0200 Subject: [PATCH 7/9] added screenshots from vscode IDE --- 01.Lesson_GettingStarted/ERC20Lesson1/README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/README.md b/01.Lesson_GettingStarted/ERC20Lesson1/README.md index e116f5c8..d5c13e9a 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/README.md +++ b/01.Lesson_GettingStarted/ERC20Lesson1/README.md @@ -111,7 +111,12 @@ For each rule, the table either displays a checkmark when the rule was proved or The results will appear under the job title. After a job is sent to the cloud, the 'Go To Rule Report' icon to the left of the job will turn light blue. Clicking it will open the rule report in the web. -To see the call trace, click a violated rule's details. +![Screen Shot 2023-03-07 at 11 21 42](https://user-images.githubusercontent.com/101042618/223378848-63242073-2987-4efd-adc9-fbb155344837.png) + +To see the call trace, click a violated rule's details: + +![Screen Shot 2023-03-07 at 11 24 10](https://user-images.githubusercontent.com/101042618/223379486-a728d578-4f72-481f-ab8f-959dd4451db3.png) +
From e35755458233e56d4b88b5105f3756c503aff7c1 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Tue, 7 Mar 2023 11:46:31 +0200 Subject: [PATCH 8/9] added vscode to lessson 6 README --- 06.Lesson_ThinkingProperties/AuctionDemonstration/README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md b/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md index 5bd30fc0..a291f62e 100644 --- a/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md @@ -34,7 +34,9 @@ You can read about the catch in the following [blog post](https://blog.makerdao. - [ ] Run the script [runBroken.sh](runBroken.sh) and get a violation. Investigate the reason for the fail and see that you understand it. +- [ ] Alternatively, run the job [run_broken](run_broken.conf) and get a violation. Investigate the reason for the fail and see that you understand it. + - [ ] Try to suggest a solution that will mitigate the wrongful behavior. -- [ ] Compare the 2 contracts - [Auction Broken](AuctionBroken.sol) and [Auction Fixed](AuctionFixed.sol) to find the fix. Run the script [runFixed.sh](runFixed.sh) and see that it is indeed solving the problem. +- [ ] Compare the 2 contracts - [Auction Broken](AuctionBroken.sol) and [Auction Fixed](AuctionFixed.sol) to find the fix. Run the script [runFixed.sh](runFixed.sh) or the job [run_fixed](run_fixed.conf) and see that it is indeed solving the problem. Were you thinking of the same solution or did you think of another one? There could be more than 1 correct answer. From 943eccbb10029464c7bbc7acba66011508bfda29 Mon Sep 17 00:00:00 2001 From: NoaBablikiCertora Date: Wed, 15 Mar 2023 11:50:04 +0200 Subject: [PATCH 9/9] added lessons numbers to confs names --- .../ERC20Lesson1/certora/conf/{erc20.conf => 01_erc20.conf} | 2 +- .../certora/conf/{erc20_fixed.conf => 01_erc20_fixed.conf} | 2 +- ...erc20_parametric_rule.conf => 01_erc20_parametric_rule.conf} | 2 +- ...lsupplyaftermint.conf => 01_erc20_totalsupplyaftermint.conf} | 2 +- ...twithpreco.conf => 01_erc20_totalsupplyaftermintwithpr.conf} | 2 +- .../certora/conf/{borda_bug_1.conf => 02_borda_bug_1.conf} | 2 +- .../conf/{erc20_bug_fixed.conf => 02_erc20_bug_fixed.conf} | 2 +- ...meeting_scheduler_1.conf => 02_meeting_scheduler_bug_1.conf} | 2 +- .../certora/conf/{run_broken.conf => 06_run_broken.conf} | 2 +- .../certora/conf/{run_fixed.conf => 06_run_fixed.conf} | 2 +- .../certora/conf/{sanity.conf => 06_ticket_depot_sanity.conf} | 2 +- .../BallGame/certora/conf/{ball_game.conf => 07_ball_game.conf} | 2 +- .../Manager/certora/conf/{manager.conf => 07_manager.conf} | 2 +- .../conf/{bank_invariant.conf => 07_bank_invariant.conf} | 2 +- .../conf/{managet_invariant.conf => 08_managet_invariant.conf} | 2 +- 15 files changed, 15 insertions(+), 15 deletions(-) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{erc20.conf => 01_erc20.conf} (92%) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{erc20_fixed.conf => 01_erc20_fixed.conf} (90%) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{erc20_parametric_rule.conf => 01_erc20_parametric_rule.conf} (86%) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{erc20_totalsupplyaftermint.conf => 01_erc20_totalsupplyaftermint.conf} (89%) rename 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/{erc20_totalsupplyaftermintwithpreco.conf => 01_erc20_totalsupplyaftermintwithpr.conf} (88%) rename 02.Lesson_InvestigateViolations/Borda/certora/conf/{borda_bug_1.conf => 02_borda_bug_1.conf} (90%) rename 02.Lesson_InvestigateViolations/ERC20/certora/conf/{erc20_bug_fixed.conf => 02_erc20_bug_fixed.conf} (89%) rename 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/{meeting_scheduler_1.conf => 02_meeting_scheduler_bug_1.conf} (88%) rename 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/{run_broken.conf => 06_run_broken.conf} (90%) rename 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/{run_fixed.conf => 06_run_fixed.conf} (91%) rename 06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/{sanity.conf => 06_ticket_depot_sanity.conf} (88%) rename 07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/{ball_game.conf => 07_ball_game.conf} (91%) rename 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/{manager.conf => 07_manager.conf} (92%) rename 07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/{bank_invariant.conf => 07_bank_invariant.conf} (88%) rename 08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/{managet_invariant.conf => 08_managet_invariant.conf} (87%) diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf similarity index 92% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf index 38ea1950..24cd4d84 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "ERC20", + "msg": "01 erc20", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_fixed.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf similarity index 90% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_fixed.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf index 659a865c..e6a22624 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_fixed.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf @@ -6,7 +6,7 @@ "ERC20:ERC20Fixed.spec" ], "solc": "solc8.0", - "msg": "erc20 fixed", + "msg": "01 erc20 fixed", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_parametric_rule.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf similarity index 86% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_parametric_rule.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf index ff0b39dc..cb61d910 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_parametric_rule.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf @@ -6,7 +6,7 @@ "ERC20:Parametric.spec" ], "solc": "solc8.0", - "msg": "erc20 parametric rule", + "msg": "01 erc20 parametric rule", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf similarity index 89% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf index 82098a5e..1ec7471b 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermint.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf @@ -6,7 +6,7 @@ "ERC20:TotalGreaterThanUser.spec" ], "solc": "solc8.0", - "msg": "erc20 totalSupplyAfterMint", + "msg": "01 erc20 totalsupplyaftermint", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf similarity index 88% rename from 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf rename to 01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf index 09e3ad5a..fc5967b0 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/erc20_totalsupplyaftermintwithpreco.conf +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf @@ -6,7 +6,7 @@ "ERC20:TotalGreaterThanUser.spec" ], "solc": "solc8.0", - "msg": "erc20 totalSupplyAfterMintWithPreco", + "msg": "01 erc20 totalsupplyaftermintwithpr", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_1.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf similarity index 90% rename from 02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_1.conf rename to 02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf index d7d62b30..8015e4d8 100644 --- a/02.Lesson_InvestigateViolations/Borda/certora/conf/borda_bug_1.conf +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf @@ -6,7 +6,7 @@ "Borda:Borda.spec" ], "solc": "solc7.6", - "msg": "borda bug 1", + "msg": "02 borda bug 1", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_fixed.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf similarity index 89% rename from 02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_fixed.conf rename to 02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf index 488960af..a08dfa63 100644 --- a/02.Lesson_InvestigateViolations/ERC20/certora/conf/erc20_bug_fixed.conf +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf @@ -6,7 +6,7 @@ "ERC20:ERC20.spec" ], "solc": "solc8.0", - "msg": "erc20 bug fixed", + "msg": "02 erc20 bug fixed", "optimistic_loop": true, "multi_assert_check": false, "send_only": true, diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf similarity index 88% rename from 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf rename to 02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf index dbe661a5..8b50a337 100644 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/meeting_scheduler_1.conf +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf @@ -6,7 +6,7 @@ "MeetingScheduler:meetings.spec" ], "solc": "solc8.7", - "msg": "meeting scheduler 1", + "msg": "02 meeting scheduler bug 1", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf similarity index 90% rename from 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf rename to 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf index 840d9c5b..3c1ab793 100644 --- a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_broken.conf +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf @@ -6,7 +6,7 @@ "System:Auction.spec" ], "solc": "solc5.12", - "msg": "run broken", + "msg": "06 run broken", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf similarity index 91% rename from 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf rename to 06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf index 74fd032a..9cda34c9 100644 --- a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/run_fixed.conf +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf @@ -6,7 +6,7 @@ "System:Auction.spec" ], "solc": "solc5.12", - "msg": "run fixed", + "msg": "06 run fixed", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf b/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf similarity index 88% rename from 06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf rename to 06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf index 82600831..aa803b19 100644 --- a/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/sanity.conf +++ b/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf @@ -6,7 +6,7 @@ "TicketDepot:sanity.spec" ], "solc": "solc6.12", - "msg": "sanity", + "msg": "06 ticket depot sanity", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf similarity index 91% rename from 07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf rename to 07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf index f9587669..9b6fdcd0 100644 --- a/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/ball_game.conf +++ b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf @@ -6,7 +6,7 @@ "BallGame:BallGame.spec" ], "solc": "solc8.6", - "msg": "ball game", + "msg": "07 ball game", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf similarity index 92% rename from 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf rename to 07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf index 751347d3..336cb175 100644 --- a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/manager.conf +++ b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf @@ -6,7 +6,7 @@ "Manager:Manager.spec" ], "solc": "solc8.6", - "msg": "Manager", + "msg": "07 manager", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf similarity index 88% rename from 07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf rename to 07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf index 4b7b7f91..7611b96f 100644 --- a/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/bank_invariant.conf +++ b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf @@ -6,7 +6,7 @@ "Bank:invariant.spec" ], "solc": "solc7.6", - "msg": "bank invariant", + "msg": "07 bank invariant", "optimistic_loop": false, "multi_assert_check": false, "send_only": true, diff --git a/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf b/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf similarity index 87% rename from 08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf rename to 08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf index 74e1cc5b..229970ec 100644 --- a/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/managet_invariant.conf +++ b/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf @@ -6,7 +6,7 @@ "Manager:ManagerFullSolution.spec" ], "solc": "solc8.6", - "msg": "Managet invariant", + "msg": "08 managet invariant", "optimistic_loop": false, "multi_assert_check": false, "send_only": true,