adding more info and comments, resolving comments

certora/README.md

@@ -7,28 +7,31 @@ There are two configurations:
 
 ## Run From the Command Line
 
-To run the checks from the command line, first install the Python SDK:
-`pip install certora-cli`
+Follow this guide to install the prover and its dependencies:
+[Installation Guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html)
 
-Set your Certora Key:  
-`export CERTORAKEY=<personal_access_key>` 
-
-Then run from this directory:  
+Once installations are set, run from this directory:  
 `certoraRun ./certora/confs/ghost.conf`  
+
+## Recommended IDE
+
+We recommended using VSCode with the following extension:
+[Certora Verification Language LSP](https://marketplace.visualstudio.com/items?itemName=Certora.evmspec-lsp)
+This extension is found in the VSCode extensions/marketplace. It provides syntactic support for the Certora Verification Language (CVL) - the language in which we will be writing specifications.
 
 ## Files
 
 Folder `specs` contains the specification files: 
 1. `ghost.spec` contains basic rules that are not dependent on any interface.
-1. `moreExmaplesERC20.spec` contains basic examples including ghost, hooks, and multi-contract features.
+2. `moreExmaplesERC20.spec` contains basic examples including ghost, hooks, and multi-contract features.
 
 Folder `confs` contains the configuration files for running the Certora Prover:  
 1. File `ghost.conf` for running `ghost.spec` on `ghost.sol` file.  
 This configuration is suitable for a standalone project, containing:  
     * external calls are assumed to be non-state changing and returning random value on each call.  
     * loops are unrolled three times.   
     * calls to fallbacks are assumed to be side-effect-free and only update the native balance.   
- 1. File `ghostWithERC20s.conf` running `moreExmaplesERC20.spec` on `ghost.sol` with additional ERC20-related contracts.   
+2. File `ghostWithERC20s.conf` running `moreExmaplesERC20.spec` on `ghost.sol` with additional ERC20-related contracts.   
 This demonstrates how to setup a project with multi-contract 
 
 

certora/confs/ghost.conf

@@ -1,18 +1,22 @@
-// A default configuration for a standalone contract
+#  A default configuration for a contract using ERC20s
 {
-  // list of files that are part of the system 
+#    list of files that are part of the system 
   "files": [
     "src/contracts/Ghost.sol"
   ],
-  // main contract to verify ghost and  spec file 
+#    main contract to verify (Ghost):spec file (ghost) 
   "verify": "Ghost:certora/specs/ghost.spec",
-  // check the spec 
+#    apply very important sanity checks that should always be run before finishing a verification
+#    docs: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html?highlight=rule%20sanity
   "rule_sanity" :"basic",
-  // assume 3 unroling of loops is enought 
+#    assume 3 unrolling of loops, i.e. every loop will run for at most 3 iterations. 3 is usually enough in most cases.
+#    this in turn will impose requirements on the length of the array (etc.) that a loop is iterating on (the stop condition of the loop)
+#    docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#loop-iter
   "loop_iter" : "3",
+#   docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-loop
   "optimistic_loop" : true,
   "prover_args": [
-      // assume calls to fallback are to EOAs (e.g., no code, only balance updated)
+      #  assume calls to fallback are to EOAs (e.g., no code, only balance updated)
       " -optimisticFallback true"
   ],
   "msg": "Ghost template file"

certora/confs/ghostWithERC20s.conf

@@ -1,20 +1,24 @@
-// A default configuration for a contract using ERC20s
+#  A default configuration for a contract using ERC20s
 {
-  // list of files that are part of the system 
+#    list of files that are part of the system 
   "files": [
     "src/contracts/Ghost.sol",
     "certora/helpers/ERC20Helper.sol",
     "certora/helpers/SimpleERC20.sol"
   ],
-  // main contract to verify ghost, spec file 
+#    main contract to verify (Ghost):spec file (moreExamplesERC20) 
   "verify": "Ghost:certora/specs/moreExamplesERC20.spec",
-  // check the spec 
+#    apply very important sanity checks that should always be run before finishing a verification
+#    docs: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html?highlight=rule%20sanity
   "rule_sanity" :"basic",
-  // assume 3 unroling of loops is enought 
+#    assume 3 unrolling of loops, i.e. every loop will run for at most 3 iterations. 3 is usually enough in most cases.
+#    this in turn will impose requirements on the length of the array (etc.) that a loop is iterating on (the stop condition of the loop)
+#    docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#loop-iter
   "loop_iter" : "3",
+#   docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-loop
   "optimistic_loop" : true,
   "prover_args": [
-        // assume calls to fallback are to EOAs (e.g., no code, only balance updated)
+        #  assume calls to fallback are to EOAs (e.g., no code, only balance updated)
         " -optimisticFallback true"
     ],
   "msg": "Ghost with ERC20 template file"

certora/specs/ghost.spec

@@ -8,7 +8,7 @@ See https://docs.certora.com for a complete guide.
 
 /*
     Declaration of methods that are used in the rules. `envfree` indicates that
-    the method is not dependent on the environment (`msg.value`, `msg.sender`).
+    the method is not dependent on the environment (`msg.value`, `msg.sender`, `block.timestamp`).
     Methods that are not declared here are assumed to be dependent on the
     environment.
 */
@@ -51,21 +51,21 @@ rule noRevert(method f) filtered {f -> nonReveritngFunction(f) }
     @dev This property is implemented as a relational property - it compares two different executions on the same state.
 **/ 
 rule simpleFrontRunning(method f, method g) 
-	/// usually a heavy rule, use filtering to decide on which this property should hole 
+	/// usually a heavy rule, use filtering to decide which functions this property should check
 	/* filtered { f-> !f.isView, g-> !g.isView } */ 
 {
 	env e1;
-	calldataarg arg;
+	calldataarg args1;
 
-	storage initialStorage = lastStorage;
-	f(e1, arg); 
+	storage initialStorage = lastStorage; // creating a storage snapshot for later use
+	f(e1, args1); 
 
 	env e2;
-	calldataarg arg2;
+	calldataarg args2;
 	require e2.msg.sender != e1.msg.sender;
-	g(e2, arg2) at initialStorage;  //roll back to state before calling f 
+	g(e2, args2) at initialStorage; // first rolling back the state to the storage snapshot, then calls a function g
 
-	f@withrevert(e1, arg);
+	f@withrevert(e1, args1); // f is called on the state snapshot + g
 	bool succeeded = !lastReverted;
 
 	assert succeeded, "should be called also if frontrunned";
@@ -81,27 +81,27 @@ rule simpleFrontRunning(method f, method g)
 rule privilegedOperation(method f, address privileged)
 {
 	env e1;
-	calldataarg arg;
+	calldataarg args1;
 	require e1.msg.sender == privileged;
 
 	storage initialStorage = lastStorage;
-	f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation.
+	f@withrevert(e1, args1); // privileged succeeds executing candidate privileged operation.
 	bool firstSucceeded = !lastReverted;
 
 	env e2;
-	calldataarg arg2;
+	calldataarg args2;
 	require e2.msg.sender != privileged;
-	f@withrevert(e2, arg2) at initialStorage; // unprivileged
+	f@withrevert(e2, args2) at initialStorage; // unprivileged
 	bool secondSucceeded = !lastReverted;
 
 	satisfy  (firstSucceeded && secondSucceeded), "function is not privileged";
 }
 
 
 /** 
-    @title This rule check with ether is sent out.    
+    @title This rule check if ether is sent out.    
     @dev nativeBalances[u] is u.balance in solidity 
-	  @dev currentContract is the main contract under verification
+	@dev currentContract is the main contract under verification
 */
 rule decreaseInSystemEth(method f) {
 

certora/specs/moreExamplesERC20.spec

@@ -16,6 +16,8 @@ using SimpleERC20 as simpleERC20;
 // Declaration of erc20 functions 
 methods {
     // When there is an unresolved call it will check all implementaions found in the list of contracts 
+    // See docs for more information on dispatcher summary:
+    // https://docs.certora.com/en/latest/docs/cvl/methods.html?highlight=dispatcher#dispatcher-summaries
     function _.name() external => DISPATCHER(true);
     function _.symbol() external => DISPATCHER(true);
     function _.decimals() external => DISPATCHER(true);
@@ -34,9 +36,10 @@ methods {
 
 
 /**
-	  @title decrease in system's erc20 balance
-	  @dev calls another contract 
+    @title decrease in system's erc20 balance
+    @dev calls another contract 
     @dev example for filtering and checking only on methods from the main contract 
+    @notice method f must be defined in the rule signature to be recognized by the filter
 */ 
 rule decreaseInERC20(method f, address token) filtered { f-> f.contract == currentContract } {
 
@@ -53,7 +56,7 @@ rule decreaseInERC20(method f, address token) filtered { f-> f.contract == curre
 } 
 
 /**
-    @title sum of erc20 balances if totalSupply 
+    @title sum of erc20 balances is totalSupply 
     @dev usign a ghost variable and hooks to track changes to _balances
 **/
 ghost mathint simpleERC20_sumOfBalances  {