Merge pull request #153 from Certora/jaroslav/UnsatCores

DOC-343: Unsat Cores Visualisation

docs/prover/checking/coverage-info.md

@@ -0,0 +1,107 @@
+# Coverage Info
+
+The {ref}`--coverage_info` flag enables automatic computation of coverage
+information for a verification run. In particular, using this flag can help you
+answer questions such as:
+
+* *Are all solidity functions from the input involved in proving my rules?*
+* *Are all solidity commands from the input involved in proving my rules?*
+* *Supposing an `assert` in my rule is not reachable, what is the reason for the
+  unreachability?*
+* *Do I really need all hooks that are defined in my `.spec` file(s)?*
+* *Do I really need all `require` statements in my rule?*
+* *Do I really need to initialize a CVL variable in my rule?*
+* *Do I really need all of the preserved blocks in my CVL `invariant`?*
+
+To answer the above questions, the Certora Prover identifies a minimal subset of
+the commands in the input `.sol` and `.spec` files that are relevant for proving
+the CVL properties. If some of the input `.sol` commands are not relevant for
+deriving the proof, it might indicate that the specification does not cover all
+behavior implemented in the smart contract. If some of the input `.spec`
+commands are irrelevant (typically unnecessary `require` statements or variable
+initializations), it indicates that the CVL rules/invariants can be made
+stronger. 
+
+You can access the coverage visualization via `Job Info -> Coverage Info page`
+buttons:
+
+![Coverage Info Button](coverage-info-button.png)
+
+
+## Examples
+
+### Tautology example
+Consider the following CVL rule called `tautology`: 
+
+```cvl
+rule tautology(uint256 fundId, method f) { 
+	env e;
+	address manager =  getCurrentManager(fundId);
+	address other;
+	require other != manager && other != e.msg.sender;
+	calldataarg args;
+	f(e,args);
+	address newManager = getCurrentManager(fundId);
+	assert newManager!= other || newManager != manager;
+}
+```
+
+Notice that we required that `other != manager` and hence the `assert` is
+necessarily `true` (see the concept of a {term}`tautology`). The executions of
+`getCurrentManager(...)` and `f(...)` are completely irrelevant. 
+
+
+The coverage visualization is shown below. It consists of two *panes*: 
+1. The left pane shows *per-line* visualization.
+2. The right pane shows detailed info about individual visualized lines. 
+
+![Example Coverage Info Visualization](tautology-sol-and-spec-cropped.png)
+
+
+In particular, in the left pane, we highlight lines from individual `.sol` and
+`.spec` files. Every line may optionally have a green, yellow, or red background
+color. No background means we have no information about this line, i.e. it might
+or might not be needed for the proof. Green, red or yellow background means we
+have some information about values of commands on the line:
+
+1. Green means that all of the values on the line are relevant for proving the
+   property. 
+2. Red means that none of the values on the line is relevant for proving the
+   property. In particular, you can arbitrary change the values and the property
+   would still hold.
+3. Yellow means that some of the values on the line are relevant and some are
+   not. 
+
+Furthermore, if we have multiple rules/invariants or a parametric rule (such as
+our `tautology`), we can also have multiple rules/invariants mapping to a single
+`.sol` or `.spec` line. In such a case, a yellow line means that some of the
+values on the line are relevant for proving some of the rules/methods/invariants
+and some of the values are not relevant. If you want to generate coverage
+visualization for a single rule or method, use {ref}`--rule` or {ref}`--method`.
+
+The right pane provides detailed information about individual values mapped to
+the lines grouped by the rule/method/invariant name (denoted *rule*). For
+instance, in the Tautology example, we can see that the value of the command
+`other != manager` on line `11` matters, whereas the value of `other !=
+e.msg.sender` is irrelevant for the proof. Also, note that the pane shows e.g.
+both `other != manager` and `other == manager`; this is due our internal
+representation of the input where we encode `other != manager` as `!(other ==
+manager)`. 
+
+
+## Basic vs. advanced mode
+
+The `--coverage_info` flag takes three possible values: `none`, `basic` and
+`advanced`:
+1. `none` means no coverage analysis, 
+2. `basic` means relatively fast but possibly very imprecise analysis (i.e. can
+   claim that some values are not relevant even if they are, and also vice
+   versa), 
+3. and `advanced` means possibly slow but more precise analysis. 
+
+## Completeness
+We perform the coverage analysis on our internal {term}`SMT` representation of the {term}`verification condition`, and then map the results of
+the analysis to the `.sol` and `.spec` files. Unfortunately, due to the
+compilation of the solidity code to EVM bytecode, we cannot maintain a complete
+mapping between commands from solidity and commands in our SMT representation.
+Consequently, the visualization on `.sol` files can be very limited. 

docs/prover/checking/index.md

@@ -10,6 +10,7 @@ tools that you can use to help find bugs in your specifications.
 :caption: Contents
 
 sanity.md
+coverage-info.md
 injection.md
 mutation.md
 ```

docs/prover/cli/options.md

@@ -326,7 +326,22 @@ useful check if you notice rules passing surprisingly quickly or easily.
 **Example**
 `certoraRun Bank.sol --verify Bank:Bank.spec --rule_sanity basic`
 
+(--coverage_info)=
+### `--coverage_info`
+
+**What does it do?**
+This option enables .sol and .spec coverage analysis and visualization.  The `--coverage_info` option may
+be followed by one of `none`, `basic`, or `advanced`;
+See {doc}`../checking/coverage-info` for more information about the analysis.
+
+**When to use it?**  
+We suggest using this option when you have finished (a subset of) your rules and the prover verified them. The analysis tells you which parts of the solidity input are covered by the rules, and also which parts of the rules are actually needed to prove the rules. 
+
+**Example**
+`certoraRun Bank.sol --verify Bank:Bank.spec --coverage_info advanced`
+
 (--short_output)=
+
 ### `--short_output`
 
 **What does it do?**

docs/user-guide/glossary.md

@@ -256,6 +256,7 @@ summarize
   Prover to analyze without timing out.  See {doc}`/docs/cvl/methods` for
   complete information on different types of method summaries.
 
+
 TAC
   TAC (originally short for "three address code") is an intermediate
   representation

spelling_wordlist.txt

@@ -88,6 +88,7 @@ hyperproperties
 hyperproperty
 immutable
 immutables
+initializations
 injective
 injectivity
 inlined
@@ -183,6 +184,7 @@ unquantified
 unroller
 unsat
 unsatisfiable
+unsatisfiability
 unsummarized
 untrusted
 upcast