Merge remote-tracking branch 'origin' into alex/control-flow-splitting

docs/cvl/index.md

@@ -35,4 +35,5 @@ Changes Since CVL 1
 
 cvl2/changes.md
 cvl2/migration.md
+v5-changes.md
 ```

docs/cvl/invariants.md

@@ -11,7 +11,7 @@ verified by the Prover, but it may still be possible for the contract to
 violate it.  The possible sources of unsoundness are {ref}`preserved`,
 {ref}`invariant-filters`, and {ref}`invariant-revert`.  Invariant proofs are
 also unsound if some of the methods are filtered out using the
-{ref}`--method` or {ref}`--contract` flags.  See the linked sections for
+{ref}`--method` or {ref}`--parametric_contracts` flags.  See the linked sections for
 details.
 ```
 

docs/cvl/methods.md

@@ -48,7 +48,7 @@ method_spec      ::= "function"
                      [ "returns" "(" evm_types ")" ]
                      [ "envfree" |  "with" "(" "env" id ")" ]
                      [ "optional" ]
-                     [ "=>" method_summary [ "UNRESOLVED" | "ALL" ] ]
+                     [ "=>" method_summary [ "" | "UNRESOLVED" | "ALL" | "DELETE" ] ]
                      ";"
 
 exact_pattern    ::= [ id "." ] id "(" evm_params ")" visibility [ "returns" "(" evm_types ")" ]
@@ -335,6 +335,7 @@ There are several kinds of summaries available:
 
  - {ref}`auto-summary` are the default for unresolved calls.
 
+(delete-summary)=
 ### Summary application
 
 To decide whether to summarize a given internal or external function call, the
@@ -345,9 +346,16 @@ determine whether the call should be replaced by an approximation.[^dont-summari
 To determine whether a function call is replaced by an approximation, the
 Prover considers the context in which the function is called in addition to the
 application policy for its signature.  If present, the application policy must
-be either `ALL` or `UNRESOLVED`; the default policy is `ALL` with the exception
-of `DISPATCHER` summaries, which have a default of `UNRESOLVED`.  The decision
-to replace a call by an approximation is made as follows:
+be either `ALL`, `UNRESOLVED`, or `DELETE`; the default policy is `ALL` with the exception
+of `DISPATCHER` summaries, which have a default of `UNRESOLVED`.
+
+A `DELETE` summary is similar to an `ALL` summary, except that the `DELETE`
+summary removes the method from the {term}`scene` entirely.  Calling the method
+from CVL will produce a rule violation, and {term}`parametric rule`s will not
+be instantiated on the deleted method.  This can drastically improve
+performance if the deleted method is complex.
+
+The decision to replace a call by an approximation is made as follows:
 
  * If the function is called from CVL rather than from contract code then it is
    never replaced by a summary.

docs/cvl/rules.md

@@ -93,8 +93,10 @@ method that violates the rule, and will indicate if some contract methods
 always satisfy the rule.
 
 You can request that the Prover only run with specific methods using the
-{ref}`--method` and {ref}`--contract` command line arguments.  The set of
+{ref}`--method` and {ref}`--parametric_contracts` command line arguments.  The set of
 methods can also be restricted using {ref}`rule filters <rule-filters>`.
+The Prover will automatically skip any methods that have
+{ref}`` `DELETE` summaries <delete-summary>``.
 
 If you wish to only invoke methods on a certain contract, you can call the
 `method` variable with an explicit receiver contract.  The receiver must be a