Operational Proof Engineering

The previous sections developed two ways to prove: forward proof builds new theorems from existing ones, and backward proof decomposes a stated goal through a goal tree. Both are declarative in spirit: the user states the target — a theorem, a post-state — and then justifies it.

This part of the tutorial turns to a third style, the one C* proofs lean on most in day-to-day verification: operational proof.

The two styles rest on the same foundation — every state change is ultimately backed by an entailment theorem checked by the kernel. They differ in what the user writes: a declarative step spells out the result, repeating everything that did not change; an operational step names only the intent (“unfold the list at pp”), and the library instantiates the result, preserves the untouched frame, and constructs the theorem.

Proved View Shifts lays the ground: the same concrete memory admits many separation-logic views, every change of view is backed by an entailment theorem, and the declarative and operational styles differ only in where the target view comes from. It also introduces the lifting machinery that lets a small-footprint entailment act on the full symbolic state, and the library’s generic state transformers.

Declaring and Applying Operations opens the operation framework itself: how a reusable operation is declared as a consume/produce schema with a proof obligation discharged at declaration time, how its patterns select resources from the current state, and how one application turns into a single committed full-state theorem — demonstrated on an entirely operational proof of in-place list reversal.

Proof-Spec-Impl Capsules is the proof-engineering payoff of the operational style. It shows how an implementation fragment, its specification, and the proof connecting them are packaged into one reusable, independently verified C function — and why that gives a stronger guarantee than encapsulation disciplines that must trust what is inside the box.