# Calculus Annotations

Caesar supports annotations on procedures to specify a desired calculus to use. By using these annotations, Caesar will help to check that only proof rules are used that are sound for that chosen calculus.

Right now, Caesar supports:

`@wp`

: The**weakest pre-expectation calculus**that operates on non-negative real numbers and infinity.- It corresponds to expected values of probabilistic programs where non-termination yields expected value zero.
- Correspondingly, it uses
*least*fixpoint semantics for loops.

`@wlp`

: The**weakest**that operates on real numbers in the closed interval from zero to one.*liberal*pre-expectation calculus- It corresponds to expected values of probabilistic programs where non-termination yields expected value 1.
- It uses
*greatest*fixpoint semantics for loops.

`@ert`

: The**expected runtime calculus**for reasoning about expected runtimes or expected resource consumption of probabilistic programs.- The calculus is basically the same as the weakest pre-expectation calculus, with a lot of additonal
`+ 1`

s everywhere. In HeyVL, this corresponds to a bunch of`tick 1`

statements.

- The calculus is basically the same as the weakest pre-expectation calculus, with a lot of additonal

The formal details of these three calculi are presented very nicely in Benjamin Kaminski's PhD thesis.

The calculus annotations do not automatically guarantee that your HeyVL file encodes your verification problems in a sound way.
For one, there are some conditions that are not (yet) checked by Caesar's implementation.
See the section What Is *Not* Checked for more information.

## Usage

Simply add the respective annotation to your `proc`

or `coproc`

.

For example, the following `proc`

declaration will not compile because induction is not a sound proof rule to be used with `wp`

reasoning about lower bounds.
A valid proof rule would be ω-invariants.

`@wp`

proc main() -> () {

var x: UInt

@invariant(x)

while 1 <= x {

x = x - 1

}

}

Each built-in proof rule specifies their soundness theorem on their own documentation page (see the *"Soundness"* sections).

## Soundness Overview of Proof Rules

So, what are the proof rules that can be used to reason about which calculus and about which direction?
The following table contains combinations of *sound approximation* combinations, i.e. if the program with the proof rule verifies, then the original program with the true greatest/least fixpoint semantics satisfies the same specification as well.

Proof Rule | `@wp` | `@wlp` | `@ert` |

(k)-Induction | Overapproximation (`coproc` ) | Underapproximation (`proc` ) | Overapproximation (`coproc` ) |

Loop Unrolling | Underapproximation (`proc` ) | Overapproximation (`coproc` ) | Underapproximation (`proc` ) |

ω-invariants | Underapproximation (`proc` ) | Overapproximation (`coproc` ) | Underapproximation (`proc` ) |

The following proof rules implicitly assume that you do not approximate in your while loops, but encode *exact* `wp`

/`ert`

semantics of your program.
This is because these proof rules implicitly do both lower and upper bounds checks on the loop body and thus the exact loop body semantics are required.

Proof Rule | `@wp` | `@wlp` | `@ert` |

Almost-Sure Termination Rule | Exact (`proc` ) | Not Applicable | Not Applicable |

Positive Almost-Sure Termination Rule | Not Applicable | Not Applicable | Exact (`coproc` ) |

Optional Stopping Theorem | Exact (`proc` ) | Not Applicable | Not Applicable |

## What Is *Not* Checked By Caesar

HeyVL is designed as an intermediate verification language and so it allows some dangerous features on purpose. See our OOPSLA '23 paper for more information. However, some items from the list below might also be disallowed in the future.

- You can easily introduce contradictions that lead to unsoundness.
- E.g.
`assume ?(false)`

can be used in`proc`

s to make everything verify trivially. - Unsoundness may come from axioms with contradictions.

- E.g.
`proc`

s may call`coproc`

s and vice versa. However, this is almost never sound.- Right now, you can call procedures of different calculi from each other without a warning.
`tick`

statements may be used with`@wp`

and`wlp`

, and it is not checked that a`tick`

statement actually occurs in an`@ert`

procedure.