A compiler for arithmetic expressions

A formalization of the correctness of a compiler from arithmetic expressions to machine language described by McCarthy and Painter, which is considered the first proof of compiler correctness.

Main definitions

• Expr : the syntax of the source language.
• value : the semantics of the source language.
• Instruction: the syntax of the target language.
• step : the semantics of the target language.
• compile : the compiler.

Main results

• compiler_correctness: the compiler correctness theorem.

Notation

• ≃[t]/ac: partial equality of two machine states excluding registers x ≥ t and the accumulator.
• ≃[t] : partial equality of two machine states excluding registers x ≥ t.

References

• John McCarthy and James Painter. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics. American Mathematical Society, 1967.

Tags

compiler

Types

@[reducible, inline]

abbrev Arithcc.Word : Type

Value type shared by both source and target languages.

Equations

• Arithcc.Word = ℕ

@[reducible, inline]

abbrev Arithcc.Identifier : Type

Variable identifier type in the source language.

Equations

• Arithcc.Identifier = String

@[reducible, inline]

abbrev Arithcc.Register : Type

Register name type in the target language.

Equations

• Arithcc.Register = ℕ

theorem Arithcc.Register.lt_succ_self (r : Arithcc.Register) : r < r + 1

theorem Arithcc.Register.le_of_lt_succ {r₁ : Arithcc.Register} {r₂ : Arithcc.Register} : r₁ < r₂ + 1 → r₁ ≤ r₂

Source language

inductive Arithcc.Expr : Type

An expression in the source language is formed by constants, variables, and sums.

• const: Arithcc.Word → Arithcc.Expr
• var: Arithcc.Identifier → Arithcc.Expr
• sum: Arithcc.Expr → Arithcc.Expr → Arithcc.Expr

instance Arithcc.instInhabitedExpr : Inhabited Arithcc.Expr

Equations

• Arithcc.instInhabitedExpr = { default := Arithcc.Expr.const default }

def Arithcc.value : Arithcc.Expr → (Arithcc.Identifier → Arithcc.Word) → Arithcc.Word

The semantics of the source language (2.1).

Equations

• Arithcc.value (Arithcc.Expr.const v) x = v
• Arithcc.value (Arithcc.Expr.var x_2) x = x x_2
• Arithcc.value (s₁.sum s₂) x = Arithcc.value s₁ x + Arithcc.value s₂ x

Target language

inductive Arithcc.Instruction : Type

Instructions of the target machine language (3.1--3.7).

• li: Arithcc.Word → Arithcc.Instruction
• load: Arithcc.Register → Arithcc.Instruction
• sto: Arithcc.Register → Arithcc.Instruction
• add: Arithcc.Register → Arithcc.Instruction

instance Arithcc.instInhabitedInstruction : Inhabited Arithcc.Instruction

Equations

• Arithcc.instInhabitedInstruction = { default := Arithcc.Instruction.li default }

structure Arithcc.State : Type

Machine state consists of the accumulator and a vector of registers.

The paper uses two functions c and a for accessing both the accumulator and registers. For clarity, we make accessing the accumulator explicit and use read/write for registers.

• ac : Arithcc.Word
• rs : Arithcc.Register → Arithcc.Word

instance Arithcc.instInhabitedState : Inhabited Arithcc.State

Equations

• Arithcc.instInhabitedState = { default := { ac := 0, rs := fun (x : Arithcc.Register) => 0 } }

def Arithcc.read (r : Arithcc.Register) (η : Arithcc.State) : Arithcc.Word

This is similar to the c function (3.8), but for registers only.

Equations

• Arithcc.read r η = η.rs r

def Arithcc.write (r : Arithcc.Register) (v : Arithcc.Word) (η : Arithcc.State) : Arithcc.State

This is similar to the a function (3.9), but for registers only.

Equations

• Arithcc.write r v η = { ac := η.ac, rs := fun (x : Arithcc.Register) => if x = r then v else η.rs x }

def Arithcc.step : Arithcc.Instruction → Arithcc.State → Arithcc.State

The semantics of the target language (3.11).

Equations

• One or more equations did not get rendered due to their size.

def Arithcc.outcome : List Arithcc.Instruction → Arithcc.State → Arithcc.State

The resulting machine state of running a target program from a given machine state (3.12).

Equations

• Arithcc.outcome [] x = x
• Arithcc.outcome (i :: is) x = Arithcc.outcome is (Arithcc.step i x)

@[simp]

theorem Arithcc.outcome_append (p₁ : List Arithcc.Instruction) (p₂ : List Arithcc.Instruction) (η : Arithcc.State) : Arithcc.outcome (p₁ ++ p₂) η = Arithcc.outcome p₂ (Arithcc.outcome p₁ η)

A lemma on the concatenation of two programs (3.13).

Compiler

def Arithcc.loc (ν : Arithcc.Identifier) (map : Arithcc.Identifier → Arithcc.Register) : Arithcc.Register

Map a variable in the source expression to a machine register.

Equations

• Arithcc.loc ν map = map ν

def Arithcc.compile (map : Arithcc.Identifier → Arithcc.Register) : Arithcc.Expr → Arithcc.Register → List Arithcc.Instruction

The implementation of the compiler (4.2).

This definition explicitly takes a map from variables to registers.

Equations

• Arithcc.compile map (Arithcc.Expr.const v) x = [Arithcc.Instruction.li v]
• Arithcc.compile map (Arithcc.Expr.var x_2) x = [Arithcc.Instruction.load (Arithcc.loc x_2 map)]
• Arithcc.compile map (s₁.sum s₂) x = Arithcc.compile map s₁ x ++ [Arithcc.Instruction.sto x] ++ Arithcc.compile map s₂ (x + 1) ++ [Arithcc.Instruction.add x]

Correctness

def Arithcc.StateEqRs (t : Arithcc.Register) (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) : Prop

Machine states ζ₁ and ζ₂ are equal except for the accumulator and registers {x | x ≥ t}.

Equations

• (ζ₁ ≃[t]/ac ζ₂) = ∀ (r : Arithcc.Register), r < t → ζ₁.rs r = ζ₂.rs r

def Arithcc.«term_≃[_]/ac_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Arithcc.StateEqRs.refl (t : Arithcc.Register) (ζ : Arithcc.State) : ζ ≃[t]/ac ζ

theorem Arithcc.StateEqRs.symm {t : Arithcc.Register} (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) : ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₁

theorem Arithcc.StateEqRs.trans {t : Arithcc.Register} (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) (ζ₃ : Arithcc.State) : ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃

def Arithcc.StateEq (t : Arithcc.Register) (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) : Prop

Machine states ζ₁ and ζ₂ are equal except for registers {x | x ≥ t}.

Equations

• (ζ₁ ≃[t] ζ₂) = (ζ₁.ac = ζ₂.ac ∧ ζ₁ ≃[t]/ac ζ₂)

def Arithcc.«term_≃[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Arithcc.StateEq.refl (t : Arithcc.Register) (ζ : Arithcc.State) : ζ ≃[t] ζ

theorem Arithcc.StateEq.symm {t : Arithcc.Register} (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) : ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₁

theorem Arithcc.StateEq.trans {t : Arithcc.Register} (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) (ζ₃ : Arithcc.State) : ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₃ → ζ₁ ≃[t] ζ₃

instance Arithcc.instTransStateStateEqHAddRegisterOfNat (t : Arithcc.Register) : Trans (Arithcc.StateEq (t + 1)) (Arithcc.StateEq (t + 1)) (Arithcc.StateEq (t + 1))

Equations

• Arithcc.instTransStateStateEqHAddRegisterOfNat t = { trans := ⋯ }

theorem Arithcc.StateEqStateEqRs.trans (t : Arithcc.Register) (ζ₁ : Arithcc.State) (ζ₂ : Arithcc.State) (ζ₃ : Arithcc.State) : ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃

Transitivity of chaining ≃[t] and ≃[t]/ac.

instance Arithcc.instTransStateStateEqHAddRegisterOfNatStateEqRs (t : Arithcc.Register) : Trans (Arithcc.StateEq (t + 1)) (Arithcc.StateEqRs (t + 1)) (Arithcc.StateEqRs (t + 1))

Equations

• Arithcc.instTransStateStateEqHAddRegisterOfNatStateEqRs t = { trans := ⋯ }

theorem Arithcc.stateEq_implies_write_eq {t : Arithcc.Register} {ζ₁ : Arithcc.State} {ζ₂ : Arithcc.State} (h : ζ₁ ≃[t] ζ₂) (v : Arithcc.Word) : Arithcc.write t v ζ₁ ≃[t + 1] Arithcc.write t v ζ₂

Writing the same value to register t gives ≃[t + 1] from ≃[t].

theorem Arithcc.stateEqRs_implies_write_eq_rs {t : Arithcc.Register} {ζ₁ : Arithcc.State} {ζ₂ : Arithcc.State} (h : ζ₁ ≃[t]/ac ζ₂) (r : Arithcc.Register) (v : Arithcc.Word) : Arithcc.write r v ζ₁ ≃[t]/ac Arithcc.write r v ζ₂

Writing the same value to any register preserves ≃[t]/ac.

theorem Arithcc.write_eq_implies_stateEq {t : Arithcc.Register} {v : Arithcc.Word} {ζ₁ : Arithcc.State} {ζ₂ : Arithcc.State} (h : ζ₁ ≃[t + 1] Arithcc.write t v ζ₂) : ζ₁ ≃[t] ζ₂

≃[t + 1] with writing to register t implies ≃[t].

theorem Arithcc.compiler_correctness (map : Arithcc.Identifier → Arithcc.Register) (e : Arithcc.Expr) (ξ : Arithcc.Identifier → Arithcc.Word) (η : Arithcc.State) (t : Arithcc.Register) (hmap : ∀ (x : Arithcc.Identifier), Arithcc.read (Arithcc.loc x map) η = ξ x) (ht : ∀ (x : Arithcc.Identifier), Arithcc.loc x map < t) : Arithcc.outcome (Arithcc.compile map e t) η ≃[t] { ac := Arithcc.value e ξ, rs := η.rs }

The main compiler correctness theorem.

Unlike Theorem 1 in the paper, both map and the assumption on t are explicit.