Merge branch 'master' into eytan/independent_satisfy

.github/CODEOWNERS

@@ -0,0 +1 @@
+/docs/gambit/gambit.md @chandrakananandi

docs/cvl/builtin.md

@@ -15,7 +15,7 @@ Built-in rules can be included in any spec file by writing `use builtin rule
 Syntax
 ------
 
-The syntax for rules is given by the following [EBNF grammar](syntax):
+The syntax for rules is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 built_in_rule ::= "use" "builtin" "rule" built_in_rule_name ";"

docs/cvl/defs.md

@@ -1,14 +1,41 @@
 Definitions
 ===========
 
-```{todo}
-The documentation for this feature is incomplete.  See [the old documentation](/docs/confluence/anatomy/definitions)
+Definitions are declared at the top-level of a specification and are in scope inside every rule, function and inside other definitions.
+A definition binds parameters for use in an arbitrary expression on the right-hand side, which should evaluate to a value of the declared return type.
+
+Examples
+--------
+
+The following [example](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/base.spec#L22) 
+introduces a definition called `filterDef` which takes a method argument `m` and produces a `bool`:
+
+```cvl
+definition filterDef(method f) returns bool = f.selector == sig:someUInt().selector;
+```
+
+This definition can then be used as shorthand for `f.selector == sig:someUInt().selector`. 
+For example, in this spec it is [used in the filter](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/base.spec#L28)
+for `parametricRule`:
+
+```cvl
+rule parametricRuleInBase(method f) filtered { f -> filterDef(f)  }
+{
+...
+}
+```
+This is equivalent to
+
+```cvl
+rule parametricRuleInBase(method f) filtered { f -> f.selector == sig:someUInt().selector  } {
+...
+}
 ```
 
 Syntax
 ------
 
-The syntax for definitions is given by the following [EBNF grammar](syntax):
+The syntax for definitions is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 definition ::= [ "override" ]

docs/cvl/expr.md

@@ -10,7 +10,7 @@ possible expressions in CVL and explains how they are evaluated.
 Syntax
 ------
 
-The syntax for CVL expressions is given by the following [EBNF grammar](syntax):
+The syntax for CVL expressions is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 expr ::= literal
@@ -96,10 +96,6 @@ denotes bitwise exclusive or and `**` denotes exponentiation, whereas in CVL,
 `^` denotes exponentiation and `xor` denotes exclusive or.
 ```
 
-```{todo}
-The `>>>` operator is currently undocumented.
-```
-
 % TODO: migrate this information here.
 See {ref}`cvl2-integer-types` for more information about the interaction between
 mathematical types and the meaning of mathematical operations.
@@ -344,7 +340,7 @@ while verifying the rule, and will provide a separate verification report for
 each checked method.  Rules that use this feature are referred to as
 {term}`parametric rule`s.
 
-
+(with-revert)=
 After the function name, but before the arguments, you can write an optional
 method tag, one of `@norevert`, `@withrevert`, or `@dontsummarize`.
  * `@norevert` indicates that examples where the method revert should not be
@@ -353,6 +349,9 @@ method tag, one of `@norevert`, `@withrevert`, or `@dontsummarize`.
    considered.  In this case, the method will set the `lastReverted` and
    `lastHasThrown` variables to `true` in case the called method reverts or
    throws an exception.
+
+   [`withrevert` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/storage/certora/specs/storage.spec#L45C19-L45C19)
+
  * ```{todo}
    The `@dontsummarize` tag is currently undocumented.
    ```
@@ -483,7 +482,7 @@ and array/map dereference operations together. For example, if the current contr
 type definitions and state variables:
 
 ```solidity
-contract Example
+contract Example {
    struct Foo {
       mapping (address => uint[]) bar;
    }

docs/cvl/functions.md

@@ -1,12 +1,14 @@
+(functions-doc)=
 Functions
 =========
 
-A CVL function provides basic encapsulation for code reuse in a specification.
+CVL functions allow you to reuse parts of a specification, such as common assumptions, assertions, 
+or basic calculations. Additionally they can be used for basic calculations and  for [function summaries](https://github.com/Certora/Examples/blob/bf3255766c28068eea2d0513edb8daca7bcaa206/CVLByExample/function-summary/multi-contract/certora/specs/spec_with_summary.spec#L6).
 
 Syntax
 ------
 
-The syntax for CVL functions is given by the following [EBNF grammar](syntax):
+The syntax for CVL functions is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 function ::= [ "override" ]
@@ -19,7 +21,24 @@ function ::= [ "override" ]
 See {doc}`basics` for the `id` production, {doc}`types` for the `type` production,
 and {doc}`statements` for the `block` production.
 
-```{todo}
-This documentation is incomplete.  See [the old documentation](/docs/confluence/anatomy/functions).
-```
+Examples
+--------
+
+- Function with a return:
+    ```cvl
+    function abs_value_difference(uint256 x, uint256 y) returns uint256 {
+        if (x < y) {
+          return y - x;
+        } else {
+          return x - y;
+        }
+    }```
+  
+- [CVL function with no return](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/LiquidityPool/certora/specs/pool.spec#L24)
+
+- [Overriding a function from imported spec](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L38)
+  
+Using CVL functions
+-------------------
+  CVL Function may be called from within a rule, or from within another CVL function.