Certora · NoaBablikiCertora · Jan 12, 2023 · Feb 15, 2023 · Feb 15, 2023 · Feb 15, 2023
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/README.md b/01.Lesson_GettingStarted/ERC20Lesson1/README.md
@@ -76,6 +76,11 @@ certoraRun --help
 
 </br>
 
+### ***Running in the IDE*** 
+
+Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***ERC20***.
+</br>
+
 ### ***Results***
 
 The prover will print various information to the console. 
@@ -99,6 +104,20 @@ Follow the "Verification results" link in the command line, or go to [prover.cer
 You'll see a table with the verification results, similar to this image: ![results](images/results.jpg) 
 For each rule, the table either displays a checkmark when the rule was proved or a x-mark when a violation of the rule was discovered.
 
+</br>
+
+## 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.
+
+![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)
+
+
 </br>
 
 ## Understanding Rule Violations
@@ -131,6 +150,11 @@ No violations were found. Great!
 
 </br>
 
+### ***Running in the IDE*** 
+
+Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***bankfixed integrityofdeposit***.
+</br>
+
 ## Preconditions and Helper Variables
 
 Let’s define [another property](TotalGreaterThanUser.spec) and verify that after mint, the `totalSupply` in the system is at least the balance of the beneficiary:
@@ -176,6 +200,11 @@ You will see the message in the run results mail and in the job's list in [prove
 
 </br>
 
+### ***Running in the IDE*** 
+
+Alternatively, use the ***Certora VSCode extension IDE*** to run the jobs ***bankfixed totalfundsafterdepos*** and ***bankfixed running with precondition***.
+</br>
+
 ## Parametric Rules
 
 Many properties can be generalized to be used for all functions.
@@ -209,3 +238,9 @@ Notice that this rule uncovers a bug in `decreaseAllowance`.
 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. 
+
+</br>
+### ***Running in the IDE*** 
+
+Alternatively, use the ***Certora VSCode extension IDE*** to run the jobs ***parametric rule on bank*** and ***parametric rule on bankfixed***.
+</br>
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "ERC20.sol:ERC20"
+  ],
+  "verify": [
+    "ERC20:ERC20.spec"
+  ],
+  "solc": "solc8.0",
+  "msg": "01 erc20",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "smt_timeout": "600",
+  "loop_iter": "1",
+  "disableLocalTypeChecking": false
+}
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf
@@ -0,0 +1,15 @@
+{
+  "files": [
+    "ERC20.sol:ERC20"
+  ],
+  "verify": [
+    "ERC20:ERC20Fixed.spec"
+  ],
+  "solc": "solc8.0",
+  "msg": "01 erc20 fixed",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "process": "emv"
+}
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf
@@ -0,0 +1,15 @@
+{
+  "files": [
+    "ERC20.sol:ERC20"
+  ],
+  "verify": [
+    "ERC20:Parametric.spec"
+  ],
+  "solc": "solc8.0",
+  "msg": "01 erc20 parametric rule",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "process": "emv"
+}
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf
@@ -0,0 +1,21 @@
+{
+  "files": [
+    "ERC20.sol:ERC20"
+  ],
+  "verify": [
+    "ERC20:TotalGreaterThanUser.spec"
+  ],
+  "solc": "solc8.0",
+  "msg": "01 erc20 totalsupplyaftermint",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "rule": [
+    "totalSupplyAfterMint"
+  ],
+  "process": "emv",
+  "settings": [
+    "-rule=totalSupplyAfterMint"
+  ]
+}
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf
@@ -0,0 +1,21 @@
+{
+  "files": [
+    "ERC20.sol:ERC20"
+  ],
+  "verify": [
+    "ERC20:TotalGreaterThanUser.spec"
+  ],
+  "solc": "solc8.0",
+  "msg": "01 erc20 totalsupplyaftermintwithpr",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "rule": [
+    "totalSupplyAfterMintWithPrecondition"
+  ],
+  "process": "emv",
+  "settings": [
+    "-rule=totalSupplyAfterMintWithPrecondition"
+  ]
+}
diff --git a/01.Lesson_GettingStarted/README.md b/01.Lesson_GettingStarted/README.md
@@ -16,7 +16,10 @@
 
 - [ ] 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.
 
-- [ ] 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.
+- [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.
+
 
 </br>
 

diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "BordaBug1.sol:Borda"
+  ],
+  "verify": [
+    "Borda:Borda.spec"
+  ],
+  "solc": "solc7.6",
+  "msg": "02 borda bug 1",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "smt_timeout": "600",
+  "loop_iter": "1",
+  "disableLocalTypeChecking": false
+}
diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "ERC20Fixed.sol:ERC20"
+  ],
+  "verify": [
+    "ERC20:ERC20.spec"
+  ],
+  "solc": "solc8.0",
+  "msg": "02 erc20 bug fixed",
+  "optimistic_loop": true,
+  "multi_assert_check": false,
+  "send_only": true,
+  "smt_timeout": "600",
+  "loop_iter": "1",
+  "disableLocalTypeChecking": false
+}
diff --git a/...esson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf b/...esson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "MeetingSchedulerBug1.sol:MeetingScheduler"
+  ],
+  "verify": [
+    "MeetingScheduler:meetings.spec"
+  ],
+  "solc": "solc8.7",
+  "msg": "02 meeting scheduler bug 1",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "smt_timeout": "600",
+  "loop_iter": "1",
+  "disableLocalTypeChecking": false
+}
diff --git 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:
 </br>
 
 - [ ] 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:
 > <details>
 >  <summary>Script Hint</summary>
->  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).
 ></details>
 
 </br>

diff --git 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.
diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf
@@ -0,0 +1,14 @@
+{
+  "files": [
+    "AuctionBroken.sol:System"
+  ],
+  "verify": [
+    "System:Auction.spec"
+  ],
+  "solc": "solc5.12",
+  "msg": "06 run broken",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true
+}
diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf
@@ -0,0 +1,15 @@
+{
+  "files": [
+    "AuctionFixed.sol:System"
+  ],
+  "verify": [
+    "System:Auction.spec"
+  ],
+  "solc": "solc5.12",
+  "msg": "06 run fixed",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "process": "emv"
+}
diff --git a/...roperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf b/...roperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf
@@ -0,0 +1,15 @@
+{
+  "files": [
+    "TicketDepot.sol:TicketDepot"
+  ],
+  "verify": [
+    "TicketDepot:sanity.spec"
+  ],
+  "solc": "solc6.12",
+  "msg": "06 ticket depot sanity",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "process": "emv"
+}
diff --git a/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf
@@ -0,0 +1,15 @@
+{
+  "files": [
+    "BallGame.sol:BallGame"
+  ],
+  "verify": [
+    "BallGame:BallGame.spec"
+  ],
+  "solc": "solc8.6",
+  "msg": "07 ball game",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true,
+  "process": "emv"
+}
diff --git a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "Manager.sol:Manager"
+  ],
+  "verify": [
+    "Manager:Manager.spec"
+  ],
+  "solc": "solc8.6",
+  "msg": "07 manager",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "smt_timeout": "600",
+  "loop_iter": "1",
+  "disableLocalTypeChecking": false
+}
diff --git a/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf
@@ -0,0 +1,14 @@
+{
+  "files": [
+    "BankFixed.sol:Bank"
+  ],
+  "verify": [
+    "Bank:invariant.spec"
+  ],
+  "solc": "solc7.6",
+  "msg": "07 bank invariant",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true
+}
diff --git a/...n_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf b/...n_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf
@@ -0,0 +1,14 @@
+{
+  "files": [
+    "Manager.sol:Manager"
+  ],
+  "verify": [
+    "Manager:ManagerFullSolution.spec"
+  ],
+  "solc": "solc8.6",
+  "msg": "08 managet invariant",
+  "optimistic_loop": false,
+  "multi_assert_check": false,
+  "send_only": true,
+  "disableLocalTypeChecking": true
+}