Glossary

Todo

This document is incomplete.

environment

The environment of a method call refers to the global variables that solidity provides, including msg, block, and tx. CVL represents these variables in a structure of type env. The environment does not include the contract state or the state of other contracts — these are referred to as the storage.

havoc

In some cases, the Prover should assume that some variables can change in an unknown way. For example, an external function on an unknown contract may have an arbitrary effect on the state of a third contract. In this case, we say that the variable was “havoced”. See Havoc summaries: HAVOC_ALL and HAVOC_ECF and havoc statements for more details.

hyperproperty

A hyperproperty describes a relationship between two hypothetical sequences of operations starting from the same initial state. For example, a statement like “two small deposits will have the same effect as one large deposit” is a hyperproperty. See The storage type for more details.

model

example

counterexample

The terms “model”, “example”, and “counterexample” are used interchangeably. They all refer to an assignment of values to all of the CVL variables and contract storage. See Overview.

overapproximation

underapproximation

Sometimes it is useful to replace a complex piece of code with something simpler that is easier to reason about. If the approximation includes all of the possible behaviors of the original code (and possibly others), it is called an “overapproximation”; if it does not then it is called an “underapproximation”. For example, a NONDET summary is an overapproximation because every possible value that the original implementation could return is considered by the Prover, while an ALWAYS summary is an underapproximation if the summarized method could return more than one value.

Proofs on overapproximated programs are sound, but there may be spurious counterexamples caused by behavior that the original code did not exhibit. Underapproximations are more dangerous because a property that is successfully verified on the underapproximation may not hold on the approximated code.

parametric rule

A parametric rule is a rule that calls an ambiguous method, either using a method variable, or using an overloaded function name. The Prover will generate a separate report for each possible instantiation of the method. See Parametric rules for more information.

quantifier

quantified expression

The symbols forall and exist are sometimes referred to as quantifiers, and expressions of the form forall type v . e and exist type v . e are referred to as quantified expressions. See Extended logical operations for details about quantifiers in CVL.

sanity

Todo

This section is incomplete. See --rule_sanity for partial information.

scene

The scene refers to the set of contract instances that the Prover knows about.

sound

unsound

Soundness means that any rule violations in the code being verified are guaranteed to be reported by the Prover. Unsound approximations such as loop unrolling or certain kinds of harnessing may cause real bugs to be missed by the Prover, and should therefore be used with caution. See Prover Approximations for more details.

summary

summarize

A method summary is a user-provided approximation of the behavior of a contract method. Summaries are useful if the implementation of a method is not available or if the implementation is too complex for the Prover to analyze without timing out. See The Methods Block for complete information on different types of method summaries.

wildcard

exact

A methods block entry that explicitly uses _ as a receiver is a wildcard entry; all other entries are called exact entries. See The Methods Block.