Suggestions & updates

docs/source/token/balance_property.rst

@@ -2,8 +2,8 @@
 ===========================================================
 
 What should be the balance of a new address?
-Write a property to check that this is indeed the balance of a new address.
-You can write your property (or rule) in
+Write a property (rule) to check that the value you expect is indeed the balance of a new address.
+You can write your rule in
 :clink:`src/certora/spec.rs <@token-proj/src/certora/spec.rs>` inside the function
 :rust:`init_balance`. We have already provided the right signature for this rule.
 
@@ -18,8 +18,9 @@ from the :rust:`projects/token/confs` directory.
 
 .. dropdown:: Hint
 
-   You'll need to use :rust:`require!(CONDITION, "address must not exists");`
-   to ensure the *address* does not already exist.  
+   You'll need to use :rust:`cvlr_assume!(<boolean>, "address must not exist");`
+   to ensure the *address* does not already exist. And :rust:`cvlr_assert!(<boolean>);`
+   is needed to verify the expected state.
 
 .. dropdown:: Solution
 

docs/source/token/introduction.rst

@@ -1,9 +1,22 @@
 Introduction
 ============
 
+This tutorial builds upon concepts covered in the main Certora Prover Tutorials such 
+as propositional & predicate logic, and the basics of formal verification. If these 
+are not already familiar to you, refer to `section 1 of the Certora Prover Tutorials`_ 
+before proceeding.
+
+
+What is Certora Sunbeam?
+------------------------
+Sunbeam is a tool for formally verifying Soroban smart contracts written in Rust. You can 
+leverage Certora's Cavelier (CVLR) library to write specifications for such contracts in Rust also.
+You can read more about Sunbeam in the `User Guide for Sunbeam`_ documentation.
+
+
 The project
 -----------
-The project's directory is in :clink:`projects/token <@token-proj/>`.
+The tutorial project's directory is in :clink:`projects/token <@token-proj/>`.
 Below is a brief description of this Rust project directory's contents:
 
 * :clink:`src/lib.rs <@token-proj/src/lib.rs>` has a Soroban smart contract with some
@@ -19,3 +32,10 @@ In file :clink:`solutions/solution_specs.rs <@token-proj/solutions/solution_spec
 you'll find the solutions to all exercises of this repository.
 You can consult it if you want to know the answers.
 
+.. Links
+   =====
+
+.. _section 1 of the Certora Prover Tutorials:
+   https://docs.certora.com/projects/tutorials/en/latest/lesson1_prerequisites/index.html
+.. _User Guide for Sunbeam:
+   https://docs.certora.com/en/latest/docs/sunbeam/usage.html#user-guide-for-sunbeam

docs/source/token/mint_burn.rst

@@ -4,9 +4,9 @@
 Now that we have seen rules for ``transfer``, think of some properties for
 ``mint`` and ``burn`` and write them in the
 :clink:`src/certora/spec.rs <@token-proj/src/certora/spec.rs>` file.
-To run them, create your own :file:`.conf` files under :clink:`confs/ <@token-proj/confs/>`
+To run them, create your own :file:`.conf` file(s) under :clink:`confs/ <@token-proj/confs/>`
 by looking at the existing conf files.
-You will only need to change the names of the rules passed into the ``"rule"`` field.
+You will only need to change the names of the rules listed in the ``"rule"`` field.
 The rest should be the same.
 
 You can see several rules we have written for these functions in

docs/source/token/mutations.rst

@@ -4,10 +4,14 @@
 ================================================
 
 How do you know if your rules are good enough to catch potential bugs?
-One technique is called "mutation testing" where small faults are injected in to the
-program and it is checked against the same rule. Verification should fail if the rule
-is good at catching the fault. If verification passes, that means your rule has gaps
-that must be addressed.
+One technique for assessing the quality of a specification is called "mutation testing".
+Small modifications (mutations) are intetionally made, one
+at a time, in the contract source code to cause logic faults. The modified code is checked 
+using your existing rules. It is important that your rules are passing with the original 
+contract code before applying any mutations so that you can safely draw conclusions from
+the mutation tests. With a mutation in the code, verification 
+will fail if the coverage of your rule set is good enough to catch the fault. If 
+verification still passes, that likely means your rules have a gap that must be addressed.
 
 We have provided 3 hand-written mutants in
 :clink:`src/certora/mutants  <@token-proj/src/certora/mutants>`.
@@ -19,10 +23,11 @@ Can you detect what the mutation was, for each mutant?
 You can see the solution in :file:`solutions/bugs-in-mutants.md`.
 
 
-Note that there are other ways to assess the quality of your rule.
-You can mutate the rule to see if it is vacuous, you can check if the rule is a
-tautology, and you can use UNSAT cores to understand what parts of the code were
-covered by the rule.
+.. todo:: The following text needs more explanation / links:
+  Note that there are other ways to assess the quality of your rule.
+  You can mutate the rule to see if it is vacuous, you can check if the rule is a
+  tautology, and you can use UNSAT cores to understand what parts of the code were
+  covered by the rule.
 
 .. dropdown:: Mutant 1. Solution
 

docs/source/token/transfer_rules.rst

@@ -5,11 +5,11 @@ What should be the effect of a ``transfer`` of ``amount`` between two addresses,
 ``to`` and ``from``?
 Write a rule to capture the correct behavior. Whose balance should change by what amount?
 
-Note that ``transfer`` should not affect any address other than the one being transferred
-to and from. Write another rule to encode the effect of ``transfer`` on some ``other``
+Note that ``transfer`` should not affect any address other than the ones specified in the
+transfer. Write another rule to verify that ``transfer`` has no effect on some ``other``
 address. 
 
-You can write these two properties in ``transfer_is_correct`` and
+You can write these two properties in the existing rules ``transfer_is_correct`` and
 ``transfer_no_effect_on_other`` in
 :clink:`src/certora/spec.rs <@token-proj/src/certora/spec.rs>`.
 

docs/source/token/warmup.rst

@@ -22,23 +22,25 @@ You should see an output like so:
    Follow your job and see verification results at <LINK>
 
 Click on that link to see the report page generated by Certora Sunbeam.
-It will show you that a basic :index:`sanity` check has passed.
-You can see the *Source Files* on the report page.
-There is also a *Call Trace* that shows you what sequence of function calls led to this
-outcome.
+It will show you that a basic :index:`sanity` check has passed, indicated
+by a green check mark next to "sanity" in the Rules list. 
+You can see the set of *Source Files* that were used by clicking on the
+File Tree icon to the left of the Rules list.
+Now, click on the "satisfy" rule to display related information in the *Call Trace* 
+panel that shows you the startng state and sequence of function calls that led to this outcome.
 
 .. index:: satisfy
 
 :clink:`src/certora/spec.rs <@token-proj/src/certora/spec.rs>` will show you the
 *sanity* rule we just ran.
 This rule simply calls :rust:`Token::balance()` and checks that the control reaches
-the :cvl:`satisfy` statement that follows.
-You can read more about :cvl:`satisfy`
+the :cvl:`cvlr_satisfy` macro that follows.
+You can read more about the semantics of :cvl:`satisfy`
 `here <https://docs.certora.com/en/latest/docs/cvl/statements.html#satisfy>`_.
 
 .. important::
 
-   If you are not able to run certoraRun, see the `Sunbeam Troubleshooting`_ section in
+   If you are not able to run ``certoraSorobanProver``, see the `Sunbeam Troubleshooting`_ section in
    the Documentation.
 
 .. dropdown:: Solution

projects/token/confs/exercise1.conf

@@ -1,10 +1,7 @@
 {
     "build_script": "../certora_build.py",
-    "process": "emv",
     "rule": [
         "init_balance"
     ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"
+    "precise_bitwise_ops": true
 }

projects/token/confs/exercise2.conf

@@ -1,11 +1,8 @@
 {
     "build_script": "../certora_build.py",
-    "process": "emv",
     "rule": [
         "transfer_is_correct",
         "transfer_no_effect_on_other"
     ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"
+    "precise_bitwise_ops": true
 }

projects/token/confs/exercise3.conf

@@ -1,10 +1,7 @@
 {
     "build_script": "../certora_build.py",
-    "process": "emv",
     "rule": [
         "transfer_fails_if_low_balance"
     ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"
+    "precise_bitwise_ops": true
 }

projects/token/confs/full_sunbeam.conf

@@ -1,13 +1,10 @@
 {
     "build_script": "../certora_build.py",
-    "process": "emv",
     "rule": [
         "init_balance",
         "transfer_is_correct",
         "transfer_no_effect_on_other",
         "transfer_fails_if_low_balance"
     ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"
+    "precise_bitwise_ops": true
 }

projects/token/confs/setup.conf

@@ -1,10 +1,7 @@
 {
     "build_script": "../certora_build.py",
-    "process": "emv",
     "rule": [
         "sanity"
     ],
-    "precise_bitwise_ops": true,
-    "prover_version": "master",
-    "server": "production"
+    "precise_bitwise_ops": true
 }

projects/token/solutions/solution_specs.rs

@@ -35,8 +35,6 @@ fn init_balance(e: Env, addr: Address) {
 // Exercise 2
 #[rule]
 fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i64) {
-    cvlr_assume!(
-        e.storage().persistent().has(&from) && e.storage().persistent().has(&to) && to != from);
     let balance_from_before = Token::balance(&e, from.clone());
     let balance_to_before = Token::balance(&e, to.clone());
     Token::transfer(&e, from.clone(), to.clone(), amount);
@@ -61,13 +59,9 @@ fn transfer_no_effect_on_other(e: Env, amount: i64, from: Address, to: Address,
 // Exercise 3
 #[rule]
 fn transfer_fails_if_low_balance(e: Env, to: Address, from: Address, amount: i64) {
-    cvlr_assume!(
-        e.storage().persistent().has(&from)
-            && e.storage().persistent().has(&to)
-            && to != from
-            && Token::balance(&e, from.clone()) < amount);
+    cvlr_assume!(Token::balance(&e, from.clone()) < amount);
     Token::transfer(&e, from.clone(), to.clone(), amount);
-    // should not reach and therefore rule must pass
+    // Should not reach the next line due to expected revert in transfer(). Rule fails iff it can be reached.
     cvlr_assert!(false);
 }