Merge remote-tracking branch 'origin/master' into shelly/v5changelog

docs/confluence/anatomy/ghostfunctions.md

@@ -85,7 +85,7 @@ Axioms are **dangerous** and should be used **carefully** as they are a pote
 
 1.  The axiom implies `false`
     
-2.  Somewhere in the program, we assume something about a ghost function that, when conjuncted with a ghost axiom, implies `false`
+2.  Somewhere in the program, we assume something about a ghost function that, when conjoined with a ghost axiom, implies `false`
 ```
 
 

docs/cvl/methods.md

@@ -1,3 +1,4 @@
+(methods-block)=
 The Methods Block
 =================
 

docs/prover/approx/hashing.md

@@ -1,3 +1,4 @@
+(hashing)=
 Modeling of Hashing in the Prover
 ==========================
 

docs/prover/approx/summarization.md

@@ -1,3 +1,4 @@
+(method-summarization)=
 Method Summarization
 ====================
 

docs/prover/cli/options.md

@@ -769,6 +769,57 @@ setting or encoding that models precisely both bitwise operations and `mathint`.
 This option sets the number of program points to test with the `deepSanity`
 built-in rule.  See {ref}`built-in-deep-sanity`.
 
+(--allow_solidity_calls_in_quantifiers)=
+### --allow_solidity_calls_in_quantifiers
+
+**What does it do?**
+
+Instructs the Prover to permit contract method calls in quantified expression
+bodies.
+
+**When to use it?**
+
+Upon instruction from the Certora team.
+
+**Example**
+
+`--allow_solidity_calls_in_quantifiers` instructs the Prover to not generate an
+error on encountering contract method calls in quantified expression bodies.
+
+
+(control-flow-splitting-options)=
+Advanced options that control control flow splitting
+----------------------------------------------------
+
+See [here](control-flow-splitting) for an explanation of control flow splitting.
+
+
+(-mediumTimeout)=
+### `--prover_args '-mediumTimeout <seconds>'`
+
+The "medium timeout" determines how much time is given to checking a split at
+not max-depth before we split again.
+
+
+(-dontStopAtFirstSplitTimeout)=
+### `--prover_args '-dontStopAtFirstSplitTimeout <true/false>'`
+
+We can tell the Certora Prover to not stop when the first split has had a
+maximum-depth timeout. Note that this is only useful for SAT results, since for
+an overall UNSAT results, all splits need to be UNSAT, while for a SAT result it
+is enough that one split is UNSAT.
+
+
+(-smt_initialSplitDepth)=
+### `--prover_args '-smt_initialSplitDepth <number>'`
+
+Splitting can be configured to skip the checks at low splitting levels, thus
+generating sub-splits up to a given depth immediately. Note that the number of
+splits generated here is equal to `2^n` where `n` is the initial splitting depth
+(unless the program has less than `n` branchings, which will be rare in
+practice).
+
+
 
 (--allow_solidity_calls_in_quantifiers)=
 ### --allow_solidity_calls_in_quantifiers

docs/prover/diagnosis/index.md

@@ -0,0 +1,19 @@
+Diagnostic Tools
+================
+
+
+(tac-reports)=
+## TAC Reports
+
+% TODO  write this -- https://certora.atlassian.net/browse/DOC-355
+
+% ## Timeout TAC Reports
+% 
+% ### Statistics- and Explanation-Box
+% 
+% ### Split- and Heuristical Difficulty-Coloring
+% 
+% ### TAC Source Code Box
+
+There is a brief explanation of how to use TAC reports in the 
+[webinar on timeouts](https://www.youtube.com/watch?v=mntP0_EN-ZQ).

docs/prover/index.md

@@ -14,6 +14,8 @@ each topic.
 intro.md
 /docs/user-guide/getting-started/install.md
 approx/index.md
+techniques/index.md
+diagnosis/index.md
 checking/index.md
 cli/index.md
 portal/using.md

docs/prover/portal/report.md

@@ -1,3 +1,4 @@
+(verification-report)=
 Certora Verification Reports
 ============================
 

docs/prover/techniques/index.md

@@ -0,0 +1,31 @@
+Techniques Used by Certora Prover
+=================================
+
+In this chapter we describe techniques used by the Certora Prover whose understanding can be relevant for an expert-level usage of the Prover.
+
+(control-flow-splitting)=
+# Control Flow Splitting
+
+There is a brief explanation of control flow splitting in the 
+[webinar on timeouts](https://www.youtube.com/watch?v=mntP0_EN-ZQ).
+
+% TODO write this -- tracked in https://certora.atlassian.net/browse/DOC-351
+
+(storage-and-memory-analysis)=
+# Storage and Memory Analysis
+
+The Certora Prover works on EVM bytecode as its input. To the bytecode, the
+address space of both Storage and Memory are flat number lines. That two
+contract fields `x` and `y` don't share the same memory is an arithmetic
+property. With more complex data structures like mappings, arrays, and structs,
+this means that every
+["non-aliasing"](https://en.wikipedia.org/wiki/Aliasing_(computing)) argument
+requires reasoning about multiplications, additions, and hash functions. Certora
+Prover models this reasoning correctly, but this naive low-level modeling can
+quickly overwhelm SMT solvers. In order to handle storage efficiently, Certora
+Prover analyses Storage (Memory) accesses in EVM code in order to understand the
+Storage (Memory) layout, thus making information like "an update to mapping `x`
+will never overwrite the scalar variable `y`" much more obvious to the SMT
+solvers. For scaling SMT solving to larger programs, these simplifications are
+essential.
+

docs/user-guide/glossary.md

@@ -1,12 +1,26 @@
 Glossary
 ========
 
-```{todo}
-This document is incomplete.
-```
-
 ````{glossary}
 
+control flow graph
+  Control flow graphs (short: CFGs) are a program representation that 
+  illustrates in which order the program's instructions are processed during 
+  program execution. 
+  The nodes in a control flow graph represent single non-branching sequences 
+  of commands. The edges in a control flow graph represent the possibility of 
+  control passing from the last command of the source node to the first 
+  command of the target node. For instance, an `if`-statement in the program
+  will lead to a branching, i.e., a node with two outgoing edges, in the 
+  control flow graph.
+  A CVL rule can be seen as a program with some extra "assert" commands, thus 
+  a rule has a CFG like regular programs.
+  Certora Prover's [TAC reports](tac-reports) contain a control flow graph of 
+  the {term}`TAC` intermediate representation of each given CVL rule.
+  Further reading: [wikipedia](https://en.wikipedia.org/wiki/Control-flow_graph)
+  % TODO: ok to mention TAC here?
+
+
 environment
   The environment of a method call refers to the global variables that solidity
   provides, including `msg`, `block`, and `tx`.  CVL represents these variables
@@ -39,6 +53,16 @@ counterexample
   They all refer to an assignment of values to all of the CVL variables and
   contract storage.  See {ref}`rule-overview`.
 
+linear arithmetic
+nonlinear arithmetic
+  An arithmetic expression is called linear if it consists only of additions, 
+  subtractions, and multiplications by constant. Division and modulo where the
+  second parameter is a constant are also linear arithmetic.
+  Examples for linear expressions are `x * 3`, `x / 3`, `5 * (x + 3 * y)`.
+  Every arithmetic expression that is not linear is nonlinear.
+  Examples for nonlinear expressions are `x * y`, `x * (1 + y)`, `x * x`, 
+  `3 / x`, `3 ^ x`.
+
 overapproximation
 underapproximation
   Sometimes it is useful to replace a complex piece of code with something
@@ -79,6 +103,22 @@ scene
   The *scene* refers to the set of contract instances that the Prover knows
   about.
 
+SMT
+SMT solver
+  "SMT" is short for "Satisfiability Modulo Theories". An SMT solver takes as 
+  input a formula in predicate logic and returns whether the formula is 
+  satisfiable (short "SAT") or unsatisfiable (short: "UNSAT"). The "Modulo 
+  Theory" part means that the solver assumes a meaning for certain symbols in 
+  the formula. For instance the theory of integer arithmetic stipulates that the 
+  symbols `+`, `-`, `*`, etc. have their regular everyday mathematical 
+  meaning.
+  When the formula is satisfiable, the SMT solver can also return a model for 
+  the formula. I.e. an assignment of the formula's variables that makes the 
+  formula evaluate to "true". For instance, on the formula "x > 5 /\ x = y * y", 
+  a solver will return SAT, and produce any valuation where x is the square of
+  an integer and larger than 5, and y is the root of x.
+  Further reading: [wikipedia](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
+
 sound
 unsound
   Soundness means that any rule violations in the code being verified are
@@ -95,6 +135,18 @@ summarize
   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
+  ([wikipedia](https://en.wikipedia.org/wiki/Intermediate_representation))
+  used by the Certora Prover. TAC code is kept invisible to the 
+  user most of the time, so it's details are not in the scope of this 
+  documentation. We provide a working understanding, which is helpful for some 
+  advanced proving tasks, in the {ref}`tac-reports` section.
+
+tautology
+  A tautology is a logical statement that is always true.
+
 vacuous
 vacuity
   A logical statement is *vacuous* if it is technically true but only because
@@ -107,8 +159,6 @@ vacuity
   doesn't say anything about the program being verified.
   The {doc}`../prover/checking/sanity` help detect vacuous rules.
 
-tautology
-  A tautology is a logical statement that is always true.
 
 wildcard
 exact

docs/user-guide/index.md

@@ -12,7 +12,7 @@ properties/index.md
 satisfy.md
 patterns/index.md
 multicontract/index.md
-timeouts.md
+timeouts/index.md
 checking.md
 troubleshooting.md
 faq.md

docs/user-guide/timeouts/index.md

@@ -0,0 +1,18 @@
+(managing-timeouts)=
+Managing Timeouts
+=================
+
+Certora Prover has a potential to run very long on some inputs. When it runs too
+long, it will give up and return a "timeout" (or in some cases "unknown")
+result. In this chapter, we present a practical guide to diagnosing the causes
+of timeouts and ways to prevent them.
+
+
+```{toctree}
+timeouts-main.md
+timeouts-theory.md
+```
+
+
+
+