Proving on the LCF Architecture

The previous sections settled 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 handful of logical implications. One question is still open, though — who proves those verification conditions? C* hands that job to a theorem prover; as we saw when starting it up in Your First C* Program, the prover C* currently integrates is HOL Light. HOL Light belongs to a lineage that traces back to Edinburgh LCF in the 1970s, and both its soundness and its extensibility come from one and 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 stay at the level of LCF and HOL Light and do not yet touch C*‘s concrete proof syntax — that is for later sections; here we lay the conceptual groundwork.

An interactive theorem prover lets a user build a proof step by step. But that raises a question: why should we believe the “theorems” it produces? If the prover has a bug internally, or if a user can sidestep some rule and simply inject a conclusion, then whatever it proves is worthless. The answer Milner gave in Edinburgh LCF in the 1970s (LCF = Logic for Computable Functions) is still the architectural bedrock of mainstream provers today.

Early proof checkers kept the entire proof in memory, and their scale was limited as a result. Gordon has an apt analogy: a mathematics lecturer works on one small blackboard, finishing a step and wiping it to make room for the next, keeping only the conclusion at the end. LCF took the same view — do not keep the whole proof, keep only its result, that is, the theorem.

The real key was one clever idea of Milner’s: implement 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 typechecking then delivers an iron law:

The axioms and inference rules that can produce a thmthm together form the system’s trusted kernel. No code outside the kernel — however elaborate the proof automation — can conjure a thmthm out of nothing; to produce a theorem, it must ultimately call back into those few kernel rules. Trusting the prover thereby reduces to trusting a small piece of kernel code, and the latter is small enough to read line by line.

This small kernel plus programmable shell design later became known as the LCF approach, which can be summed up in two points:

1. Every proof ultimately reduces to a small set of primitive inferences; as long as this kernel is correct, the conclusions are sound.
2. The whole system is embedded in a powerful functional programming language, in which one can program new inference rules and proof procedures; the language’s type discipline guarantees that these extensions still reduce to that set of primitive rules.

The language in the second point is ML — its name is short for “Meta Language,” and it 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.

For the kernel to be small, the logic it implements must itself be lean. Much of what makes HOL Light Light comes from the simplicity of its underlying logic.

Its object language is higher-order logic — more precisely, simple type theory with polymorphic type variables, i.e. the simply typed -calculus plus 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. Surprisingly, there are only 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 .”

Perhaps the most counterintuitive yet crucial design choice is this: a formula is not a separate syntactic category — it is simply a term of boolean type. The proposition is a term just as the numeral is, only the former has type and the latter type . Every other notation is syntactic sugar over these four kinds of term: the quantifier is really a constant applied to an abstraction, , and a binding is really a -application. All variable binding reduces to -binding — which is exactly why the kernel need only handle 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 nothing more than equality on booleans. Every other connective is defined in terms of equality, for example:

From these definitions the usual natural-deduction rules can be derived. The logic can be this small precisely because nearly all of the primitive rules speak only of equality.

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

Most of these rules just express reflexivity, transitivity, and congruence of equality, plus introducing an assumption (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 carries a side condition: must not occur free in — side conditions like this are not decoration but are 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. The axiom of choice is worth a remark: HOL Light’s core logic is in fact constructive, and it is only from the axiom of choice that classical principles such as the law of excluded middle can be derived. In other words, the logic’s classicality is added explicitly rather than assumed by default.

Given the kernel, how does one develop rich mathematical structures like the naturals, lists, and reals? One dangerous route is to postulate axioms describing them directly — but every extra axiom is one more chance to introduce a contradiction. 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

Why does this not break consistency? Because the definition imposes restrictions — for instance, you may not redefine an existing constant to be something else:

# 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".

Suppose it were allowed: the system would then hold both and , hence , and a contradiction follows. The definitional principle blocks exactly this kind of “saying one extra thing for free.”

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. Thereafter, any notion on the new type must be defined explicitly through this pair of bijections, and any theorem can be transported back to the representing type to be proved. 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 merely spares us the bother of such relativization.

Back to the second point of the LCF approach: a proof is itself a program in the metalanguage. This gives two complementary styles of proof.

Forward proof. Start from axioms and known theorems and apply inference rules to derive new ones. In HOL, an inference rule is neither more nor less than 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. Forward proof is often unintuitive — people prefer to start from the goal they want and decompose it into simpler subgoals until those become trivially solvable. This goal-directed style revolves around 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.

The tool that drives backward proof is the tactic:

The user keeps applying tactics to do backward proof, and behind the scenes the system uses the validation functions to translate the process back into the kernel’s primitive inferences — so backward proof does not bypass the trusted kernel; it still reduces, in the end, to those 10 rules.

Tacticals. Tactics too can be combined — the higher-order functions that combine them are called tacticals. The most common few: 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). With them, a long string of proof steps can be packed into one compact expression.

Within this framework, a user can write their own specialized inference rules and even decision procedures, in the very same style as the kernel rules; all such derived tools are ultimately expanded by the kernel into primitive inferences step by step. This brings an extra benefit: finding a proof and checking it can be separated — an arbitrary program (or even an external tool) may search for the proof, whose result is then formally verified by the kernel.

Once HOL Light is loaded, what you face is really an ordinary OCaml read-eval-print loop (REPL), only with a large stock of theorems and proof tools already loaded. Terms are written inside backquotes, and theorems are printed with a leading |-|- (an ASCII approximation of the turnstile ).

Here is a backward proof of the commutativity of addition. proveprove takes a goal and a tactic and yields the theorem in one go:

# 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

Piece by piece: 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 watch the intermediate steps, one can also 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 shapes call for different handy tactics. The small table below gathers the tactics mentioned in this section along with a few common automation ones:

One honest caveat is in order: such procedural proof scripts often take real patience to write, and are not easy to read or modify — they are essentially highly procedural programs, recording how it was proved rather than making what was proved obvious at a glance. This is precisely the starting point of the sections to come: how C*, on top of this LCF machinery, offers a more intuitive way to write proofs for the verification of C programs.

• The LCF architecture makes a theorem an abstract type thmthm, and relies on the type system to ensure it can arise only through the kernel’s axioms and inference rules — this is theorem security, and it shrinks trusting the prover down to trusting 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;
• The kernel is a small set of primitive inference rules plus 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: apply rules forward, decompose goals backward with tactics, assemble steps with tacticals — and everything is expanded, in the end, inside the kernel.