[V] Language Description

[V] is a declarative language for writing correctness specifications. Any [V] specification contains several distinct sections – some required, some optional, and some that are mutually exclusive. This document describes these sections, detailing their purpose and syntax.

Overview of Sections

[V] specifications contain the following sections:

vars: <declarations>
(hints: <statements>)?
(fair: <statements>)?
((spec: <ltl_formula>) | (inv: <condition>))

The vars section is required, and is used to declare free variables in the specification. The hints and fair sections are both optional. The hints section is used to restrict the search space of transaction parameter values. The fair section is used to direct the search space of transaction sequences. Exactly one of the spec and inv section is required. The spec section is used to describe a property of the source code that should be checked. The inv section is used to describe invariants, a specific type of property.

vars Section

vars: <varType> <varName>, <varType> <varName>, ...

The vars section contains all variable declarations for the specification. Most often, this include contract variable declarations of the form ContractName varName, but can also include other variables used in the spec.

Any variable declared in the vars section is considered a free variable, meaning that the specification does not hold if any assignment to the variable falsifies the spec.

Besides contract types, the following are accepted as variable types in the vars section:

• address
• string
• bool
• uint8-uint256 and int8-int256. uint and int are equivalent to their 256-bit counterparts.
• bytes
• bytes1-bytes32
• Struct types Contract.StructType
• Enum types Contract.EnumType
• Array types <type>[], <type>[][], etc.
• Tuple types (<type>, <type>), (<type>,<type>,<type>), etc.

spec Section

spec: []!finished(<target>, <condition>) ...

The spec section contains an LTL formula over [V] statements that describes some property of the source code. This section provides a high-level overview of the syntax of the spec section. Other documents discuss [V] Statements and LTL formulae in more detail.

LTL Formulae

OrCa works by checking the validity of the LTL formula provided in the spec section. We say that the formula is valid when the formula is true for (1) any possible assignment of the free variables declared in the vars section and (2) any possible sequence of transactions issued over the contracts in scope. When OrCa finds a set of assignments for free variables and a transaction sequence that falsified the provided formula, OrCa reports this transaction sequence as a "counterexample" to the specification.

The LTL formulae permissible in the spec section is described by the following grammar:

L :   S
    | (L)
    | <> L
    | X L
    | ! L
    | [] L
    | L U L
    | L R L
    | L ; L
    | L && L
    | L || L
    | L ==> L

S in the grammar represents a [V] statement. [V] statements make up the atoms of the LTL formula within a [V] spec. [V] statements are evaluated in the context of a single transaction, as described in the next subsection. The LTL formula S (composed of a single [V] statement) is true for an event sequence if S evaluates to true over the first transaction in the event sequence.

The boolean operators || ("or"), && ("and"), and ! ("not") have their usual meaning. For an in-depth explanation on the semantics of temporal operators <>, X, [], U, R, and ;, see Temporal Specifications.

In general, LTL formula are evaluated over infinite sequeces of events. In the context of blockchain applications, each of these events has an associated blockchain state. There are two ways that OrCa interprets a finite sequence of transactions as an infinite sequence of events to evaluate an LTL formula over:

1. Each transaction is translated into two sequential events: one event where the transaction is started, and one where the transaction is completed (or reverted if the transaction errored). The associated blockchain state of the transaction started event is the state before the transaction is issued, while the state for the completed/finished/reverted event is the state after the transaction is issued.
2. The event sequence is extended infinitely with null-events $\epsilon$ such that any [V] statement S evaluates to false over any null-event $\epsilon$.

[V] Statements

[V] statements make up the atoms of the LTL formula within a [V] spec. The following grammar describes the syntax of a [V] statement:

S : F(T, E)

F :   started
    | reverted
    | executed
    | finished

T :   I.I(I, ...)
    | I.I
    | I.*
    | *

F represents the type of statement, T represents the target of the statement, and E represents the conditional expression. I represents any identifier. Conditional expressions must evaluate to a boolean value. [V] statements describes the expressions allowed for statement conditions in further detail.

A [V] statement F(T, E) is evaluated over a particular point in the event sequence. Specifically, F(T, E) holds for a particular event iff the following conditions hold:

1. The event type matches F.
1. started matches any transaction start event
2. finished matches any transaction completion event where the transaction was successfully executed
3. reverted matches any transaction completion event where the transaction was unsuccessfully executed (i.e. reverted)
4. executed matches any transaction completion event
2. The pertinent transaction matches T
1. c.txn(...) and c.txn match the transaction txn over the contract instance c
2. c.* matches any transaction over the contract instance c
3. * matches any transaction
3. The condition E holds over the associated blockchain state.

inv Section

inv: <condition>

The inv section is shorthand for a set of commonly-expressed specifications. Specifically, the inv section allows users to express invariants over the space of in-scope contracts. The invariant expr holds when expr is true after issuing any transaction.

There are two forms for the inv section:

1. inv: expr
2. inv: expr over target

The invariant expr over target holds iff expr holds after issuing any transaction that matches target. Note that the first form inv: expr is equivalent to inv: expr over *. For example, to express an invariant over one specific contract Contract, use the following [V] specification:

vars: Contract c
inv: <cond> over c.*

The invariant section inv: expr over target is equivalent to the following spec section:

spec: []!finished(target, !expr)

hints Section

hints: finished(<target>, <condition>) ; ...

The hints section contains a sequence of special finished statements. Note that the sequence is not required to end with a ;, but ; is required between each finished statement. These finished statements make up distinct hints.

Each hint contains both a target and a condition. The meaning of hint finished(target, condition) is that transaction target should be issued with transaction arguments (and sender and value values) that satisfy condition.¹

The target, like any [V] statement, may take the following forms:

1. contractVar.function(arg1, arg2, ...)
2. contractVar.function
3. contractVar.*
4. *

Since hints are used to constrain the arguments of transactions, nearly all hints will use the first form of the target (though hints that constrain the transaction sender or value may use the alternate forms).

Hint conditions may contain any expressions from standard [V] statement conditions, but also include some additional syntax. Specifically, the assignment operator := can be used to directly specify a (possibly random) value for transaction arguments.

The assignment expression <L> := <R> must satisfy a few properties:

• <L> must be either a transaction argument or the keyword sender or value
• <R> must be an expression that evaluates to the type of <L>

In general, hint conditions that contain only a conjunction of assignments (e.g. x := f() && y := g()) are more efficient than hints with inequalities or disjunctions. Whenever possible, express hints as a conjunction of assignments for the best performance.

Useful functions for expressing hints

[V] provides several useful function for expressing hints.

The functions ecdsa256_sign(signer, msg) and ecdsa256_sign_bytes(signer, msg) return a signature for msg signed by the address signer. ecdsa256_sign returns the signature as a (uint8, bytes32, bytes32) tuple (v,r,s), while ecdsa256_sign_bytes returns the signature as a 65-byte bytes string.

The function elem_in_range(low, high) returns a random element in the range [low, high). For input values that should always lie within a specific range, use a hint like this:

hints: finished(c.foo(percent), percent := elem_in_range(0,101))

The function user_address() returns random user address. For input addresses that should always be user addresses, use a hint like this:

hints: finished(c.foo(addr), addr := user_address())

fair Section

The fair section allows users to specify a temporal property that should be assumed by OrCa. This section must appear before the spec section in the specification:

fair: prop1
spec: prop2

For this example specification, OrCa will only report counterexamples that both (a) satisfy the fairness property prop1 and (b) violate the correctness property prop2.² See documentation on fairness assumptions for more details on the fair section.

---

1. We plan to allow future versions of OrCa to issue some portion of target transactions that do not satisfy hint conditions. In the current version of OrCa, all issued target transactions must satisfy all pertinent hints.↩
2. Currently, OrCa only uses the fairness property as a precondition for reporting counterexamples. Future versions of OrCa may direct the search to test only sequences that satisfy the fairness property.↩