# Proof Rules

Caesar supports a number of proof rule encodings out of the box. The proof rules are used via annotations on while loops. All while loops used in HeyVL must have a proof rule annotation so that they can be verified with loop-free verification pre-expectation reasoning.

To help you use proof rules correctly, Caesar supports calculus annotations on procedures. These annotations specify a desired reasoning calculus and limit the proof rules for loops to ensure that only sound proof rules for the respective calculi are used.

If you have read our OOPSLA '23 publication: these proof rules were implemented in our `pgcl2heyvl`

tool to reason about pGCL programs, but are now implemented directly in Caesar.
This allows verifiers for languages other than pGCL to re-use the proof rule encodings.

Proof rules are only sound in specific contexts.
Using proof rules in a wrong way may lead to *unsoundness*, i.e. a program may falsely verify.
To be certain that a proof rule may be applied, correctness of the proof rule needs to be proven with respect to the language semantics that are to be encoded.
See our OOPSLA '23 publication for details on the theory.

## 📄️ Calculus Annotations

Procedure annotations for soundness of proof rules.

## 📄️ Induction and k-Induction

Induction and k-Induction are proof rules for while loops.

## 📄️ Loop Unrolling

Loop unrolling and bounded model checking.

## 📄️ ω-Invariants

TODO.

## 📄️ Almost-Sure Termination

TODO.

## 📄️ Positive Almost-Sure Termination

TODO.

## 📄️ Optional Stopping Theorem

Proof rule for lower bounds on least fixpoints.