Statements

HeyVL statements describe programs and proofs inside procedure bodies.

Program statements

Blocks · Variables
Assignments and calls
Boolean choices
Nondeterministic choices
While loops
Rewards
Weights

Proofs and semantics

Assertions
Assumptions
Havoc
Validations
Verification conditions
Game semantics
Legacy statements

Concrete Statements

Blocks

A block is a sequence of statements enclosed by curly braces.

{ ... }

Variables declared inside a block are local to it. Assignments to outer variables remain visible afterwards:

var x: UInt = 1
{
    var y: UInt = 2
    x = x + y
}
// x is now 3
// y is no longer in scope

Blocks can be nested, and an empty block {} has no effect. Semicolons between statements are optional.

Variable Declarations

Declare a variable with its type and an optional initial value.

var x: T
var x: T = e

var count: UInt = 0 declares an unsigned integer with initial value 0. Without an initializer, verification considers every possible value of the variable's type. See the standard library for built-in types and domains for user-defined types.

Assignments and Procedure Calls

An assignment stores the value of an expression in a variable.

x = e

x = 39 + y updates x using the current value of y. Assignments can update local variables and output parameters. Input parameters are immutable. The assigned value must have a compatible type.

A distribution call samples a random value. HeyVL provides Bernoulli, uniform, binomial, and hypergeometric distributions.

x = flip(p)
x = ber(pa, pb)
x = unif(a, b)
x = binom(n, pa, pb)
x = hyper(N, k, n)

var b: Bool = flip(0.5) assigns true or false with equal probability. Distribution calls must appear directly on the right-hand side of an assignment or initializer. flip accepts symbolic arguments. The other distributions require numeric literals.

Arbitrary finite discrete probabilistic choices can be implemented using only fair binary probabilistic choice (flip(0.5)) and iteration (while loops)¹. You can also use [weigh] statements and the additive choice statement (if +) to implement any finite discrete distribution, as shown in the example below.

A procedure call assigns its outputs to a list of variables.

x, y = p(args)
p(args)

A call with no outputs stands alone. Caesar verifies calls against the callee's specification.

Boolean Choices

An if executes one of two blocks according to a Boolean condition.

if b { ... } else { ... }

This decrements x if it is positive:

if x > 0 {
    x = x - 1
} else {}

The else block is required, but may be empty.

While Loops

HeyVL supports while loops that run a block of code while a condition evaluates to true.

while b { ... }

For example, keep flipping a coin until it returns false:

var cont: Bool = true
@invariant(...)
while cont {
    cont = flip(0.5)
}

For verification, while loops need proof-rule annotations such as the @invariant(...) annotation in the example. If a while loop does not have a proof-rule annotation, Caesar cannot verify the program and will show an error.

Proof-rule annotations also determine which fixpoint semantics to use for the loop. This can be least fixpoint, or bounded or unbounded greatest fixpoint. The fixpoint semantics determines which reward is collected for executions which do not terminate. Use calculus annotations on procedures to make this choice explicit.

With the model-checking translation, proof-rule annotations are not necessary. It supports probabilistic model checkers such as Storm for a subset of HeyVL programs. You can use these to get an initial estimate of expected values.

Rewards

reward adds a reward, such as elapsed time or resource consumption.

reward e

The reward e must be non-negative. tick e is an alias. Rewards accumulate along an execution. With post 0, reward 2; reward 3 has total reward $5$ . A nonzero post adds a final reward.

Weights

weigh multiplies the remaining program's contribution by a weight.

weigh e

The weight e must be non-negative. For example, weigh 0.5; reward 2 contributes $1$ with post 0, while reward 2; weigh 0.5 contributes $2$ .

Combine weigh with additive choice if + to weight each branch and sum the results. The example below uses this to express a probabilistic choice.

Nondeterministic Choices

Demonic choice if ⊓ minimizes the expected outcome. Angelic choice if ⊔ maximizes it. Additive choice if + sums the contributions of both branches.

if ⊓ { ... } else { ... }
if ⊔ { ... } else { ... }
if + { ... } else { ... }

For example, choose between two rewards:

if ⊓ {
    reward 2
} else {
    reward 6
}

With post 0, changing the choice operator gives:

if ⊓: $2$ , the smaller reward.
if ⊔: $6$ , the larger reward.
if +: $8$ , the sum of both rewards.

For ASCII spellings, use \cap for ⊓, \cup for ⊔, and \oplus for +. Additive choice also accepts ⊕.

One can use the additive choice operator and the weigh statement to implement any sampling from finite discrete distributions. The example below applies this to implement a x = flip(0.3) assignment.

Probabilistic choice implemented with additive choice and weights

The example below implements a x = flip(0.3) assignment using additive choice and weights. We just need to weigh the branches of the additive choice according to the desired probabilities.

proc expected_reward() -> (x: Bool)
    pre 0.3
    post [x]
{
    if + {
        weigh 0.3
        x = true
    } else {
        weigh 0.7
        x = false
    }
}

This approach can be easily generalized to implement any finite discrete distribution.

Verification Statements

Verification statements express conditions to prove, assumptions to use, and changes to the proof state. Each verification statement has a dual with a co prefix, such as assert and coassert. Both forms can occur in a proc or coproc.

These statements have quantitative semantics. We introduce common Boolean uses first for intuition, then give the general quantitative rules.

Caesar's proof rules generate these statements for supported proof techniques.

Verification Conditions

An expectation assigns a non-negative number or $\infty$ to each program state. Starting from post, Caesar works backwards through the body to compute a verification pre-expectation. We write $\mathrm{vp}\llbracket S\rrbracket(f)$ for the result before statement $S$ , where $f$ is the expectation for the remaining code. All operations on expectations below are pointwise. For a whole procedure body $S$ , the verification condition (VC) compares this result with pre in every initial state:

proc: $\mathrm{pre} \leq \mathrm{vp}\llbracket S\rrbracket(\mathrm{post})$ (lower bound).
coproc: $\mathrm{pre} \geq \mathrm{vp}\llbracket S\rrbracket(\mathrm{post})$ (upper bound).

A smaller pre-expectation can make a lower-bound proof harder and an upper-bound proof easier. Probabilistic failures can involve several statements across multiple paths. See the slicing guide for how to diagnose them.

The VS Code extension can show pre-expectations inline with the command Caesar: Explain Verification Condition Generation.

Rules for program statements

Sequential composition works backwards:

\mathrm{vp}\llbracket S_1; S_2\rrbracket(f) = \mathrm{vp}\llbracket S_1\rrbracket\bigl(\mathrm{vp}\llbracket S_2\rrbracket(f)\bigr).

An empty block leaves $f$ unchanged. For a choice with branches $S_1,S_2$ , write $f_i=\mathrm{vp}\llbracket S_i\rrbracket(f)$ . Each line gives $\mathrm{vp}\llbracket S\rrbracket(f)$ for the indicated statement.

x = e: $f[x\mapsto e]$
x = flip(p): $p\,f[x\mapsto\mathrm{true}]+(1-p)\,f[x\mapsto\mathrm{false}]$ , for $0\leq p\leq1$ .
if b: $\operatorname{ite}(b,f_1,f_2)$
if ⊓: $\min(f_1,f_2)$
if ⊔: $\max(f_1,f_2)$
if +: $f_1+f_2$
reward e: $e+f$
weigh e: $e\cdot f$ , with $0\cdot\infty=0$ .

Assertions

Boolean

Add a condition that the proof must establish at this point. The usual forms are assert in a proc and coassert in a coproc.

assert ?(b)
coassert !?(b)

For example, assert ?(x >= 1) adds the obligation that x is at least $1$ . In a coproc, write coassert !?(x >= 1) for the same Boolean condition.

Assertions also accept a quantitative expectation e.

Quantitative

assert chooses demonically whether to stop and collect e or continue with the remaining program. coassert makes this choice angelically.

assert e
coassert e

e has type EUReal.

$\mathrm{vp}\llbracket\texttt{assert }e\rrbracket(f)=\min(e,f)$

$\mathrm{vp}\llbracket\texttt{coassert }e\rrbracket(f)=\max(e,f)$

The Boolean forms above use these same rules, with the embeddings ?(b) or !?(b) as e. ?(b) is $\infty$ when b holds and $0$ otherwise. !?(b) is $0$ when b holds and $\infty$ otherwise. When b holds, both forms leave $f$ unchanged. Otherwise, assert ?(b) gives $0$ and coassert !?(b) gives $\infty$ , matching the bound direction of the proof.

The Iverson bracket [b] takes values $1$ and $0$ instead, for reasoning about probabilities.

Assumptions

Boolean

Assume a condition holds at this point in the proof. The usual forms are assume in a proc and coassume in a coproc.

assume ?(b)
coassume !?(b)

For example, with x: UInt, this fragment uses x > 0 to prove x >= 1:

assume ?(x > 0)
assert ?(x >= 1)

In a coproc, use coassume !?(x > 0) followed by coassert !?(x >= 1). Caesar uses the assumed condition without proving it. Proof encodings use assumptions to record branch conditions, loop invariants, and procedure specifications.

Assumptions also accept a quantitative expectation e.

Quantitative

If the remaining expectation is at least e, assume makes a lower-bound goal trivial. coassume does the same for an upper-bound goal when the expectation is at most e.

assume e
coassume e

$\mathrm{vp}\llbracket\texttt{assume }e\rrbracket(f)=\begin{cases}\infty & e\leq f\\f & e>f\end{cases}$

$\mathrm{vp}\llbracket\texttt{coassume }e\rrbracket(f)=\begin{cases}0 & f\leq e\\f & f>e\end{cases}$

The Boolean forms use these same rules with the embeddings ?(b) and !?(b). When b holds, both leave $f$ unchanged. Otherwise, assume ?(b) gives $\infty$ and coassume !?(b) gives $0$ .

Proving an assertion from an assumption

proc positive_integer(x: UInt) -> ()
    pre \infty
    post \infty
{
    // \infty
    assume ?(x > 0)
    // ?(x >= 1)
    assert ?(x >= 1)
}

The comments show the pre-expectation immediately before each statement. The assertion requires x >= 1, which follows from the assumption x > 0. The resulting pre-expectation is $\infty$ in every initial state, so the procedure verifies. The dual proof uses $0$ to represent a satisfied obligation:

coproc positive_integer_dual(x: UInt) -> ()
    pre 0
    post 0
{
    // 0
    coassume !?(x > 0)
    // !?(x >= 1)
    coassert !?(x >= 1)
}

Removing the assumption makes either proof fail at x = 0.

Ending a proof branch

For an expectation I, this fragment has verification pre-expectation exactly $I$ , whatever follows it:

// I
assert I
// \infty
assume 0

Reading backwards, assume 0 transforms any continuation into $\infty$ , and assert I then yields $\min(I,\infty)=I$ . Proof-rule encodings use this to finish a branch after introducing its obligation. The dual fragment is:

// I
coassert I
// 0
coassume \infty

coassume makes the continuation $0$ , and coassert I gives $\max(I,0)=I$ . For complete encodings, see procedure calls and Park induction.

Havoc

Forget the current values of variables and choose replacements. The choice is demonic for havoc and angelic for cohavoc.

havoc x, ...
cohavoc x, ...

To prove a Boolean property for every replacement value, the usual pattern uses havoc in a proc or cohavoc in a coproc. For example, after forgetting the value of a local x: UInt, assume it is positive:

havoc x
assume ?(x > 0)
assert ?(x >= 1)

The proof now concerns an arbitrary positive integer, regardless of the earlier value of x. Loop proofs use this pattern to forget values from earlier iterations and then assume the loop invariant. Procedure-call encodings use it to forget the previous values of output variables.

Both statements accept local variables and output parameters.

$\mathrm{vp}\llbracket\texttt{havoc }x\rrbracket(f)=\inf_{v\in\mathrm{Type}(x)} f[x\mapsto v]$

$\mathrm{vp}\llbracket\texttt{cohavoc }x\rrbracket(f)=\sup_{v\in\mathrm{Type}(x)} f[x\mapsto v]$

Validations

Turn the remaining expectation into a Boolean proof obligation.

validate
covalidate

Validation leaves Boolean obligations unchanged: values $0$ and $\infty$ stay as they are.

$\mathrm{vp}\llbracket\texttt{validate}\rrbracket(f)=\begin{cases}\infty & f=\infty\\0 & f<\infty\end{cases}$

$\mathrm{vp}\llbracket\texttt{covalidate}\rrbracket(f)=\begin{cases}0 & f=0\\\infty & f>0\end{cases}$

validate; assume 2 checks whether the expectation of the following code is at least $2$ . This example fails because its post 1 is below that bound:

proc require_two() -> ()
    pre 1
    post 1
{
    // 0
    validate
    // 1
    assume 2
}

Without validate, the computed pre-expectation would be $1$ , so pre 1 would verify. validate turns that value into $0$ , making the check $1\leq0$ fail. With post 3, assume 2 produces $\infty$ , which validate preserves, so the procedure verifies.

validate; assume I returns $?(I \leq f)$ . Its dual covalidate; coassume I returns $!?(f \leq I)$ .

Combining assert, havoc, and assume

This procedure combines all four statements to verify pre 1:

proc check_bound() -> (x: UInt)
    pre 1
    post x + 2
{
    // 1
    assert 1
    // \infty
    havoc x
    // \infty
    validate
    // \infty
    assume x + 2
}

Reading backwards, assume x + 2 compares $x+2$ with the post, and validate turns the result into $0$ or $\infty$ . havoc x checks the comparison for every replacement value of x, giving $\infty$ here. assert 1 then gives $\min(1,\infty)=1$ .

With post x + 1, the comparison fails for every x. Validation then gives $0$ , so the proof fails. Without validate, the failed comparisons would leave $x+1$ . havoc would give $\inf_{x\in\mathbb{N}}(x+1)=1$ , so the procedure would still verify.

In general, assert P; havoc x; validate; assume Q gives $P$ if $Q\leq f$ holds for every replacement value of x, and $0$ otherwise. Replacing all four statements with their co forms gives $P$ if $f\leq Q$ holds for every replacement value, and $\infty$ otherwise. In both cases, $P$ is evaluated before forgetting x. This pattern appears in procedure-call encodings and loop-invariant proofs.

Game Semantics

HeyVL programs describe a game between two players: the demonic player minimizes expected reward, and the angelic player maximizes it. For the core HeyVL language, the game's value is the pre-expectation defined above.

Programs and choices. A play follows assignments and sampling, collects reward values, and collects post on reaching the end. The demonic player controls if ⊓ and havoc, the angelic player if ⊔ and cohavoc. The remaining game value is the expected reward still to come, accounting for future random outcomes and both players' choices.

Assertions. At assert e, the demonic player may stop for reward e or continue. coassert e gives this choice to the angelic player. Stopping keeps earlier rewards and does not collect future rewards, including post.²

Assumptions. A referee evaluates the value of the remaining game. For assume e, it ends play with reward $\infty$ when that value is at least e. For coassume e, it ends play with reward $0$ when the value is at most e. Otherwise, play continues.

Validations. At validate, the referee lets play continue if the remaining value is $\infty$ , and otherwise stops it with reward $0$ . At covalidate, it lets play continue if the remaining value is $0$ , and otherwise stops it with reward $\infty$ .

Deprecated Statements

caution

The legacy compare, cocompare, negate, and conegate statements may be removed from Caesar. Prefer the supported proof rules and procedure-call syntax when encoding proofs.

Compare

compare f is shorthand for validate; assume f. Its dual cocompare f is shorthand for covalidate; coassume f.

$\mathrm{vp}\llbracket\texttt{compare }e\rrbracket(f)=\begin{cases}\infty & e\leq f\\0 & e>f\end{cases}$

$\mathrm{vp}\llbracket\texttt{cocompare }e\rrbracket(f)=\begin{cases}0 & f\leq e\\\infty & f>e\end{cases}$

Negations

The negate and conegate statements apply HeyLo's negations.

validate is equivalent to conegate; conegate, and covalidate is equivalent to negate; negate.

$\mathrm{vp}\llbracket\texttt{negate}\rrbracket(f)=\begin{cases}\infty & f=0\\0 & f>0\end{cases}$

$\mathrm{vp}\llbracket\texttt{conegate}\rrbracket(f)=\begin{cases}0 & f=\infty\\\infty & f<\infty\end{cases}$

danger

Sound (co)procedure calls require monotonicity. Negation statements can break this property and make calls unsound.

Concrete Statements​

Blocks​

Variable Declarations​

Assignments and Procedure Calls​

Boolean Choices​

While Loops​

Rewards​

Weights​

Nondeterministic Choices​

Verification Statements​

Verification Conditions​

Assertions​

Assumptions​

Havoc​

Validations​

Game Semantics​

Deprecated Statements​

Compare​

Negations​

Further Reading​

Footnotes​