Operational Proof Engineering

The previous sections introduced two ways to construct proofs: forward proof builds new theorems from existing ones, and backward proof decomposes a stated goal through a goal tree. Both follow a declarative approach: the user states a target, such as a theorem or a post-state, and then justifies it.

This part of the tutorial introduces operational proof, the style most commonly used in day-to-day C* verification.

Both styles rely on entailment theorems checked by the kernel to justify every state change. They differ in what the user writes: a declarative step specifies the result, repeating everything that did not change; an operational step specifies only the intent (“unfold the list at pp”), and the library instantiates the result, preserves the unchanged frame, and constructs the theorem.

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

Declaring and Applying Operations describes the operation framework: 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 produces a single full-state theorem and commits it. An entirely operational proof of in-place list reversal demonstrates these steps.

Proof-Spec-Impl Capsules shows how the operational style supports proof engineering. It explains how an implementation fragment, its specification, and the proof connecting them are packaged into one reusable, independently verified C function, and why this gives a stronger guarantee than encapsulation disciplines that must trust the enclosed implementation.