# Expressions

HeyVL expressions can be used inside specifications and statements and evaluate to values in some program state.

## Expression Syntax

The syntax of expressions (`Expr`

) consists of the following parts:

- Quantifiers:
`inf Ident: Type, Ident: Type. Expr`

`sup Ident: Type, Ident: Type. Expr`

`forall Ident: Type, Ident: Type. Expr`

`exists Ident: Type, Ident: Type. Expr`

- Quantifier annotations such as triggers are also allowed, e.g.
`forall Ident: Type @trigger(Expr). Expr`

- Boolean Operators (returning type
`Bool`

):- Logical And:
`Expr && Expr`

- Logical Or:
`Expr || Expr`

- Equals:
`Expr == Expr`

- Less Than:
`Expr <= Expr`

- Not Equals:
`Expr != Expr`

- Greater Or Equals:
`Expr >= Expr`

- Greater:
`Expr > Expr`

- Logical And:
- Binary Lattice and Heyting Algebra Operators (on types
`Bool`

and`EUReal`

):- Binary Minimum/Infimum:
`Expr ⊓ Expr`

or`Expr \cap Expr`

- Binary Maximum/Supremum:
`Expr ⊔ Expr`

or`Expr \cup Expr`

- Implication:
`Expr → Expr`

or`Expr ==> Expr`

- Coimplication:
`Expr ← Expr`

or`Expr <== Expr`

(note that this is**not**just a flipped version of the implication`→`

, but rather its lattice-theoretic dual!) - Comparison:
`Expr ↘ Expr`

- Cocomparison:
`Expr ↖ Expr`

- Binary Minimum/Infimum:
- Arithmetical Operators (c.f. number types):
- Addition:
`Expr + Expr`

- Subtraction/Monus:
`Expr - Expr`

- Multiplication:
`Expr * Expr`

- Division:
`Expr / Expr`

- Modulo:
`Expr % Expr`

- Addition:
- Other Expressions:
- Let Expressions:
`let(Ident, Expr, Expr)`

- If-Then-Else Expressions:
`ite(Expr, Expr, Expr)`

- Function Calls:
`Ident(Expr, ..., Expr)`

- Negation:
`!Expr`

- Conegation:
`~Expr`

- Embed:
`?Expr`

(usually written with parentheses:`?(Expr)`

) - Iverson:
`[Expr]`

- Parentheses:
`(Expr)`

- Let Expressions:
- Literals:
- String Literals: text enclosed by
`"`

characters (regular expression:`"[^"]*"`

). Note that Caesar does not support a proper`String`

type yet. - Integers: given by regular expression
`[0-9]+`

(default type:`UInt`

) - Decimals: given by regular expression
`[0-9]+\.[0-9]+`

(default type:`UReal`

) - Boolean Constants:
`true`

and`false`

- String Literals: text enclosed by
- Identifiers (
`Ident`

): Names of things, from the language of the regular expression`[_a-zA-Z][_a-zA-Z0-9']*`

.

Types (`Type`

) are types from Caesar's standard library and user-defined types from domains.

The above list is presented roughly in order of operator precedence. Note that we plan to change some operator precedences, so when in doubt, use more parentheses to guarantee the correct interpretation.

The most precise grammar specification can be found in Caesar's source code (`src/front/parser/grammar.lalrpop`

).

## Semantics and Under-Specified Expressions

In our paper on HeyVL (cf. Section 2), we give a formal semantics for *HeyLo*, our logic for reasoning about expected values.
HeyLo includes operators such as `==>`

, `<==`

, `!`

, `~`

, `?(e)`

, and more.
Caesar's expressions are a superset of HeyLo.
In particular, the paper explains in detail the lattice and Heyting algebra operators that Caesar supports.

Note that some operations are not fully specified (*under-specified*).
The division and remainder operators (`Expr / Expr`

and `Expr % Expr`

) are not fully defined for all values.
Caesar translates these operators directly to SMT, where the SMT solver may assign arbitrary interpretations to e.g. divisions by zero.
You can find more information in the Z3 documentation on division.

The `-`

operator is always fully defined in Caesar.
On unsigned types such as `UInt`

, it corresponds to *monus*, i.e. truncating subtraction that is always at least `0`

.
On signed types such as `Int`

, it corresponds to the usual subtraction.

## If-Then-Else

The `ite`

built-in function allows to choose one of two expressions based on the result of a Boolean expression.
For example:

`var x: UInt = ite(true, 32, 64);`

The first parameter is the Boolean expression.
If it evaluates to `true`

, the result of evaluating the second expression is returned.
Otherwise, the third expression is evaluated.

## Let Expressions

`let`

expressions enable the declaration of local variables within an expression.
For example:

`var x: UInt = let(b, true, ite(b, 32, 64));`

The `let`

expression creates a new local variable `b`

and sets its value to `true`

.
This variable `b`

is available within the `let`

expression's third argument.

In contrast to variable declaration statements using `var`

, `let`

expressions do not require type annotations.
The type of the variable is inferred from the second expression.

## Quantifiers

HeyVL features Boolean and quantitative quantifiers: `forall`

, `exists`

, `inf`

, `sup`

.
For example:

`forall x: Int, y: UInt. x == y || x != y`

### Triggers

We also support *triggers* for the Boolean quantifiers via annotations.
They are *patterns* that will instruct the SMT solver to instantiate quantifiers if the pattern is found in the current list of terms it maintains.
For example:

`forall list: []Int @trigger(len(list)). len(list) >= 0`

*Multi-patterns* are also supported, by writing a comma-separated list inside the `@trigger`

annotation:

`forall list: []Int @trigger(len(list), len(list)). len(list) >= 0`

For more information on how triggers/patterns work in general, see the Z3 User Guide and the Dafny documentation.

## Relative Completeness

Caesar's expression syntax is based on the expressive assertion language for probabilistic verification by Batz et al.
In theory, *expressiveness* means that for many programs and properties, we know that we can express *all* pre-expectations and invariants in the expression syntax when a post-expectation is written in that syntax.

Formally, we have that the weakest pre-expectation calculus `wp`

is *relatively complete* with respect to this language, which means that `wp[P](post)`

is effectively constructible for all programs `P`

and expectations `post`

in their syntax.

Their syntax includes enough constructs to specify many interesting properties, such as termination probabilities or the distribution over final states, even including stuff like harmonic numbers. See the paper's Section 12 for more details.

Of course, this does not mean that all of these verification problems are decidable.
It just means that in theory, the undecidable part is *only* in the final inequality check `pre <= wp[P](post)`

instead of the computation of `wp[P](post)`

.
The section on SMT theories and incompleteness specifies which of these inequalities are actually decidable with Caesar.

## SMT Theories and Incompleteness

Expressions are the main reason for *incompleteness* of Caesar, i.e. instances Caesar is unable to decide whether a given HeyVL program verifies or not.
Caesar's incompleteness comes from incompleteness of the underlying SMT solver which is used to prove or disprove verification.

At the moment, Caesar's translation of HeyVL verification problems is rather direct: most expressions are translated as one would intuitively expect. If operators have a direct correspondence in SMT-LIB, then we translate directly to those. Otherwise, usually only additional simple case distinctions are introduced. We have some more explanations in Section 5 of our paper on HeyVL.

As a consequence, it is usually pretty simple to predict which SMT-LIB theories will be used for the SMT query done by Caesar. Also refer to the Z3 documentation on arithmetic theories, since a lot of Caesar's reasoning will need arithmetic.

Here are some rules of thumb for (in-)completeness:

- Linear integer and real arithmetic (QF_LRA, QF_LIRA) is decidable.
- Nonlinear integer arithmetic (QF_NIA) is undecidable.
- Nonlinear real arithmetic (QF_NRA) is decidable for algebraic reals.
- Quantifiers usually introduce undecidability, although there are a bunch of strategies and fragments in Z3 that allow decidability.
- In particular, restrictive quantifier triggers can help e-matching prove many instances.

- HeyVL's quantitative quantifiers (
`inf`

and`sup`

) currently have a very naive default encoding that is problematic for Z3. If the quantitative quantifiers cannot be eliminated by Caesar's quantifier elimination (QE) procedure, then they are often a cause of nontermination of Caesar.- Quantitative quantifiers also come from the semantics of
`havoc`

and`cohavoc`

. However, for e.g. the induction-based proof rules, the HeyVL encodings fall into a fragment where Caesar's QE applies and the generated quantifiers are eliminated.

- Quantitative quantifiers also come from the semantics of
- In practice, the SMT solver can often
*prove*correctness, but it often has problems with*refutations*(i.e. providing counter-examples).