Pre/Post Contracts

Contracts define what a function guarantees. Preconditions specify what must be true before the function runs. Postconditions specify what is guaranteed after it returns. The HOL kernel verifies that the implementation satisfies these contracts. If you have used requires-and-ensures style contracts before, this will feel familiar, except the guarantee is a proof rather than a runtime check.

After this page you will be able to write preconditions and postconditions, express side effects, understand how the kernel checks a contract from first principles, and state assumptions about third-party code cleanly.

Preconditions

A precondition declares the input contract: what must be true about the function’s arguments and environment before execution begins. Preconditions appear in the \begin{pre} ... \end{pre} block of a pf2 annotation.

/* prove:pf2("safe_divide")
\[
\begin{pre}
  a : \mathbb{Z} \land b : \mathbb{Z} \land b \neq 0
\end{pre}
\begin{proof}
\step{1}{ b \neq 0 \Rightarrow a / b \text{ is defined} }
  \pf\ By precondition and DIV\_DEF.
\qedstep
  \pf\ By \stepref{1}.
\end{proof}
\]
*/
fn safe_divide(a: i64, b: i64) -> i64 {
    a / b
}

In this example, the precondition states that both inputs are integers and b is non-zero. The proof then uses the precondition to establish that division is defined.

What Preconditions Can Express

• Type constraints: x : \mathbb{N} (natural number), s : \text{String}
• Value bounds: 0 < x \leq 100, n \geq 1
• Structural properties: \text{sorted}(arr), \text{len}(xs) > 0
• Relational constraints: \text{lo} \leq \text{hi}, a \neq b
• Logical combinations: P \land Q, P \lor Q, P \Rightarrow Q

Postconditions

A postcondition declares what the function guarantees about its return value and any observable effects. Postconditions are established by the proof body: the \qedstep asserts the final postcondition, and the proof steps demonstrate that it follows from the preconditions and the implementation logic.

/* prove:pf2("abs_non_negative")
\[
\begin{pre}
  x : \mathbb{Z}
\end{pre}
\begin{proof}
\step{1}{ x \geq 0 \Rightarrow |x| = x \geq 0 }
  \pf\ By ABS\_DEF, first case.
\step{2}{ x < 0 \Rightarrow |x| = -x > 0 }
  \pf\ By ABS\_DEF, second case, and NEG\_POS.
\step{3}{ |x| \geq 0 }
  \pf\ By case split, \stepref{1} and \stepref{2}.
\qedstep
  \pf\ By \stepref{3}.
  \text{Postcondition: result} \geq 0.
\end{proof}
\]
*/
fn abs_value(x: i64) -> u64 {
    x.unsigned_abs()
}

The proof establishes that the return value is always non-negative, regardless of the input sign. The \qedstep states the postcondition: the result is greater than or equal to zero.

Side Effects

When a function modifies state beyond its return value, the annotation can describe those side effects as part of the contract. Side effects are declared alongside preconditions or documented in the proof steps.

/* prove:pf2("push_increases_length")
\[
\begin{pre}
  \text{len}(vec) = n
\end{pre}
\begin{proof}
\step{1}{ \text{push}(vec, item)
  \Rightarrow \text{len}(vec) = n + 1 }
  \pf\ By VEC\_PUSH\_LEN.
\step{2}{ vec[\text{len}(vec) - 1] = item }
  \pf\ By VEC\_PUSH\_LAST.
\qedstep
  \pf\ By \stepref{1} and \stepref{2}.
  \text{Side effect: vec is mutated.}
\end{proof}
\]
*/

The proof establishes two facts about the side effect: the vector length increases by one, and the pushed item is the last element.

How the Kernel Verifies Contracts

The HOL kernel does not simply check syntax. It verifies that each proof step is a valid inference from the axioms, the preconditions, and previously proven theorems. The verification process:

1. Parse. The pf2 annotation is parsed into a structured proof tree with preconditions, steps, justifications, and the QED step.
2. Resolve references. Each \stepref and theorem citation (e.g., ADD_SYM, DIV_DEF) is looked up in the standard theorem library and the project’s registered theorems.
3. Check each step. The kernel verifies that each step’s conclusion follows from its justification. If a step cites ADD_SYM, the kernel checks that the step’s mathematical content matches what ADD_SYM establishes.
4. Verify closure. The \qedstep must logically follow from the preceding steps, closing the proof. An incomplete or circular proof is rejected.

Every step in the chain traces back to the 4 foundational axioms and 10 primitive inference rules. No step is taken on faith.

Contracts and Third-Party Code

When your code calls external libraries or third-party functions, you can write contracts that assume properties of those dependencies. The precondition block can state assumptions about external behavior:

/* prove:pf2("parse_returns_valid")
\[
\begin{pre}
  \text{input} \text{ is valid JSON}
  \land \text{JSON.parse} \text{ conforms to RFC 8259}
\end{pre}
\begin{proof}
\step{1}{ \text{JSON.parse}(\text{input})
  \neq \text{undefined} }
  \pf\ By precondition: input is valid JSON.
\step{2}{ \text{result} :
  \text{Record}  }
  \pf\ By RFC 8259 conformance and \stepref{1}.
\qedstep
  \pf\ By \stepref{2}.
\end{proof}
\]
*/

The precondition makes the dependency assumption explicit. If the assumption is wrong, the proof is valid but the precondition is violated at runtime. This lets you formally verify your own logic while clearly documenting what you assume about third-party code.

Common Contract Patterns

Pattern	Precondition	Postcondition
Bounds check	0 \leq i < \text{len}(arr)	No out-of-bounds access
Division safety	b \neq 0	Division is defined
Sort preservation	\text{sorted}(arr)	\text{sorted}(\text{result})
Non-empty result	\text{len}(input) > 0	\text{len}(\text{result}) > 0
Idempotency	(none)	f(f(x)) = f(x)
Range clamp	\text{lo} \leq \text{hi}	\text{lo} \leq \text{result} \leq \text{hi}

Next Steps

• Writing pf2 Annotations: full syntax reference
• Certifications: publishing verified contracts as signed certificates
• Lean 4 Cross-Check: independent verification of contract proofs