Proving on the LCF Architecture

The previous sections explained what specifications to write and how verification conditions (VCs) are generated: separation logic supplies the assertion language, and the symbolic-execution engine reduces an annotated program to a small set of logical implications. We still need to establish who proves those verification conditions. C* currently uses HOL Light for this task, as we saw when starting the prover in Your First C* Program. HOL Light’s design traces back to Edinburgh LCF in the 1970s. Its soundness and extensibility rely on the same design, usually called the LCF architecture. This section introduces that architecture and the idea of programmable proof, together with HOL Light’s higher-order logic, its definition mechanisms, and how deductive proofs are carried out. We focus here on the concepts behind LCF and HOL Light; later sections introduce C*‘s concrete proof syntax.

An interactive theorem prover lets a user build a proof step by step. We need to know why its results can be trusted as theorems. If an internal bug or a way to bypass an inference rule lets a user insert an arbitrary conclusion, the prover can no longer guarantee that its results are theorems. Milner addressed this problem in Edinburgh LCF in the 1970s (LCF = Logic for Computable Functions). His design remains a basis for mainstream theorem provers.

Early proof checkers kept the entire proof in memory, and their scale was limited as a result. Gordon compares this to a mathematics lecturer working on a small blackboard: after completing a step, the lecturer erases the intermediate work to make room for the next, keeping only the conclusion. LCF likewise keeps the result of a proof, the theorem, without retaining the whole proof.

Milner’s key idea was to implement a theorem as an abstract data type named thmthm. The predefined values of this type are the logic’s axioms, the operations on it are the inference rules, and there is no other way to build one. The host language’s strict type checking ensures the following property:

The axioms and inference rules that can produce a thmthm together form the system’s trusted kernel. Code outside the kernel, including proof automation, cannot construct a thmthm directly; it must call the kernel rules. Trust in the prover therefore reduces to trust in a kernel small enough to review line by line.

This design, combining a small kernel with a programmable shell, became known as the LCF approach. It has two main properties:

1. Every proof reduces to a small set of primitive inferences; if the kernel is correct, the conclusions are sound.
2. The system is embedded in a functional programming language that supports writing new inference rules and proof procedures. The language’s type discipline ensures that these extensions still reduce to the primitive rules.

The language in the second point is ML, short for “Meta Language,” which was originally designed for LCF. Two levels must be distinguished here: the logic being reasoned about is the object language, while the programming language used to write inferences and tactics is the metalanguage. ML was made strongly typed precisely to support the abstract-type mechanism above, and functional so that proof tactics could be expressed naturally as functions.

A small kernel requires a simple underlying logic. This simplicity accounts for much of the Light in HOL Light’s name.

Its object language is higher-order logic: more precisely, simple type theory with polymorphic type variables, based on the simply typed -calculus with polymorphism. Higher-order means quantifiers may range over functions and predicates, not just individuals.

Types. We start from two primitive types: (booleans / propositions) and (individuals); from any two types , we can build a function type . Every term carries a single well-defined type, and the type system rules out meaningless expressions.

Terms. There are four kinds of term:

• Variables, such as ;
• Constants, such as ;
• Applications, a function applied to an argument, such as ;
• -abstractions, , the function “yielding for a given .”

A formula is a term of Boolean type, so formulas do not need a separate syntactic category. The proposition and the numerical expression are both terms: the former has type and the latter type . Other notation is syntactic sugar over these four kinds of term: the quantifier is a constant applied to an abstraction, , and a binding is a -application. All variable binding reduces to -binding, so the kernel need only handle these four kinds of term.

Equality-based. The core logic of HOL Light has, in essence, just one predefined logical constant: equality (plus an operator for choice). The Boolean if and only if is equality on Booleans. Every other connective is defined in terms of equality, for example:

The usual natural-deduction rules can be derived from these definitions. Nearly all primitive rules concern only equality, which keeps the logic small.

The kernel contains 10 primitive inference rules. An assertion is written as a sequent , read “under the set of assumptions , the boolean term holds.” Below are a few representative ones ( denotes the union of two assumption sets):

These rules express reflexivity, transitivity, and congruence of equality, as well as assumption introduction (ASSUME) and rewriting with an equivalence (EQ_MP). The remaining ones (MK_COMB, DEDUCT_ANTISYM_RULE, INST, INST_TYPE) handle, respectively, congruence for function application, deriving an equivalence from two implications, and capture-avoiding substitution for term variables and type variables. ABS has a side condition: must not occur free in . This condition is required for soundness.

Beyond these 10 rules, three mathematical axioms are added outside the kernel: extensionality (-conversion), the axiom of choice, and the axiom of infinity. HOL Light’s core logic is constructive. Classical principles such as the law of excluded middle can be derived only after adding the axiom of choice, so the logic’s classicality is introduced explicitly.

We can now consider how to develop mathematical structures such as the naturals, lists, and reals from this kernel. Postulating axioms to describe these structures directly risks introducing a contradiction with each new axiom. HOL takes another route: develop theories by definition rather than by axiom. New constants and types may be introduced only as a conservative extension — roughly, “an abbreviation for some expression in the existing theory” — so they add nothing new to the logic, and consistency is guaranteed by construction.

Constant definition. new_definitionnew_definition takes an equation , defines the constant , and returns the theorem :

# let wordlimit = new_definition `wordlimit = 2 EXP 32`;;
val wordlimit : thm = |- wordlimit = 2 EXP 32

# let wordlimit = new_definition `wordlimit = 2 EXP 32`;;
val wordlimit : thm = |- wordlimit = 2 EXP 32

Restrictions on definitions preserve consistency. For example, an existing constant cannot be redefined to have a different meaning:

# let wordlimit' = new_definition `wordlimit = 2 EXP 64`;;
Exception: Failure "new_definition: 'wordlimit' already defined".

# let wordlimit' = new_definition `wordlimit = 2 EXP 64`;;
Exception: Failure "new_definition: 'wordlimit' already defined".

If redefinition were allowed, the system would contain both and , hence , and a contradiction follows. The definitional principle prevents such unjustified additional assertions.

Type definition. new_type_definitionnew_type_definition starts from a nonempty subset of an existing type (the subset is picked out by a characteristic predicate, and one must first prove it nonempty) and builds a new type in bijection with that subset; the two directions of the bijection are conventionally called the abstraction and representation functions. Notions on the new type must then be defined explicitly through these two functions, and theorems can be translated back to the representing type for proof. For this reason, type definition, like constant definition, is conservative: anything provable using the new type can also be proved without it, by relativizing the statement to that subset — the new type lets us avoid writing this relativization explicitly.

The second property of the LCF approach is that a proof is a program in the metalanguage. This supports two complementary proof styles.

Forward proof. Start from axioms and known theorems and apply inference rules to derive new ones. In HOL, an inference rule is an ML function returning a thmthm. For example, transitivity TRANSTRANS has type thm -> thm -> thmthm -> thm -> thm, combining and into :

# TRANS (ARITH_RULE `1 + 3 = 4`) (ARITH_RULE `4 = 2 + 2`);;
val it : thm = |- 1 + 3 = 2 + 2

# TRANS (ARITH_RULE `1 + 3 = 4`) (ARITH_RULE `4 = 2 + 2`);;
val it : thm = |- 1 + 3 = 2 + 2

Backward proof. It is often easier to start from the desired goal and decompose it into simpler subgoals until each can be solved directly. This goal-directed style uses two notions:

• a goal: a boolean term to be proved, together with a set of usable assumptions;
• a goalstack: the stack of subgoals still to be proved, maintained by the system.

Backward proof proceeds by applying tactics:

As the user applies tactics, the system uses the validation functions to translate the backward proof into the kernel’s primitive inferences. Backward proof therefore still relies on the trusted kernel and its 10 rules.

Tacticals. Higher-order functions that combine tactics are called tacticals. Common examples are THENTHEN (apply the first tactic, then apply the second to all resulting subgoals), THENLTHENL (assign different tactics to different subgoals), REPEATREPEAT (repeat as many times as possible), and ORELSEORELSE (try the first, and on failure try the second). These functions combine a sequence of proof steps into a compact expression.

Within this framework, a user can write their own specialized inference rules and even decision procedures in the same style as the kernel rules. These derived tools run outside the kernel and ultimately call its primitive inference rules, which check each inference step. This also separates finding a proof from checking it: an arbitrary program, including an external tool, may search for a proof whose result is then formally verified by the kernel.

HOL Light provides an ordinary OCaml read-eval-print loop (REPL) with a library of theorems and proof tools loaded. Terms are written inside backquotes, and theorems are printed with a leading |-|- (an ASCII approximation of the turnstile ).

The following backward proof establishes the commutativity of addition. proveprove takes a goal and a tactic and returns the theorem:

# let ADD_SYM = prove
   (`!m n. m + n = n + m`,
    INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
val ADD_SYM : thm = |- !m n. m + n = n + m

# let ADD_SYM = prove
   (`!m n. m + n = n + m`,
    INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
val ADD_SYM : thm = |- !m n. m + n = n + m

INDUCT_TACINDUCT_TAC applies mathematical induction on , splitting the goal into a base case () and an induction step, and automatically placing the induction hypothesis into the step’s assumption list; THENTHEN applies the following tactic to both subgoals; ASM_REWRITE_TAC[...]ASM_REWRITE_TAC[...] rewrites repeatedly using the current assumptions together with a more basic theorem ADD_CLAUSESADD_CLAUSES, discharging both subgoals.

To inspect intermediate steps, we can work interactively on the goalstack: gg sets a goal, ee applies one tactic (expand), bb undoes the last step (back up), and top_thm()top_thm() retrieves the theorem once all subgoals are proved.

# g `!m n. m + n = n + m`;;
val it : goalstack = 1 subgoal (1 total)
`!m n. m + n = n + m`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)
...

# g `!m n. m + n = n + m`;;
val it : goalstack = 1 subgoal (1 total)
`!m n. m + n = n + m`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)
...

Different goal forms call for different tactics. The table below lists the tactics discussed here and a few common automation tactics:

Procedural proof scripts often require patience to write and can be difficult to read or modify. They record how a result was proved, while the result itself may be difficult to identify from the sequence of steps. The following sections explain how C* uses this LCF architecture to offer a more intuitive way to write proofs for C program verification.

• The LCF architecture represents theorems with an abstract type thmthm. The type system ensures that values of this type can arise only through the kernel’s axioms and inference rules. This theorem security reduces trust in the prover to trust in a small kernel;
• HOL Light’s higher-order logic is lean and equality-based: two primitive types, four kinds of term, formulas-as-boolean-terms, and connectives all defined via equality;
• HOL Light’s logical foundation consists of a small set of primitive inference rules and three mathematical axioms, and the logic’s classicality is introduced explicitly by the axiom of choice;
• New constants and types may only be defined as conservative extensions (rather than postulated as axioms), so consistency holds by construction;
• A proof is a program in the metalanguage: rules derive theorems forward, tactics decompose goals backward, and tacticals combine proof steps. These tools run outside the kernel and ultimately call its primitive inference rules for checking.