mathlib3 documentation

mathlib-archive / arithcc

A compiler for arithmetic expressions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main results #

Notation #

References #

Tags #

compiler

Types #

source
@[reducible]
def arithcc.word  :
Type

Value type shared by both source and target languages.

Equations
source
@[reducible]
def arithcc.identifier  :
Type

Variable identifier type in the source language.

Equations
source
@[reducible]
def arithcc.register  :
Type

Register name type in the target language.

Equations
source
theorem arithcc.register.lt_succ_self (r : arithcc.register) :
r < r + 1
source
theorem arithcc.register.le_of_lt_succ {r₁ r₂ : arithcc.register} :
r₁ < r₂ + 1 → r₁ ≤ r₂

Source language #

source
@[protected, instance]
def arithcc.expr.inhabited  :
inhabited arithcc.expr
source
inductive arithcc.expr  :
Type

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

Instances for arithcc.expr
source
@[simp]
def arithcc.value  :
arithcc.expr → (arithcc.identifier → arithcc.word) → arithcc.word

The semantics of the source language (2.1).

Equations

Target language #

source
@[protected, instance]
def arithcc.instruction.inhabited  :
inhabited arithcc.instruction
source
inductive arithcc.instruction  :
Type

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

Instances for arithcc.instruction
source
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.

Instances for arithcc.state
source
@[protected, instance]
def arithcc.state.inhabited  :
inhabited arithcc.state
Equations
source
@[simp]
def arithcc.read (r : arithcc.register) (η : arithcc.state) :
arithcc.word

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

Equations
source
@[simp]
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
source
def arithcc.step  :
arithcc.instruction → arithcc.state → arithcc.state

The semantics of the target language (3.11).

Equations
source
@[simp]
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
source
@[simp]
theorem arithcc.outcome_append (p₁ 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 #

source
@[simp]
def arithcc.loc (ν : arithcc.identifier) (map : arithcc.identifier → arithcc.register) :
arithcc.register

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

Equations
source
@[simp]
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

Correctness #

source
def arithcc.state_eq_rs (t : arithcc.register) (ζ₁ ζ₂ : arithcc.state) :
Prop

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

Equations
source
@[protected, refl]
theorem arithcc.state_eq_rs.refl (t : arithcc.register) (ζ : arithcc.state) :
ζ ≃[t]/ac ζ
source
@[protected, symm]
theorem arithcc.state_eq_rs.symm {t : arithcc.register} (ζ₁ ζ₂ : arithcc.state) :
ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₁
source
@[protected, trans]
theorem arithcc.state_eq_rs.trans {t : arithcc.register} (ζ₁ ζ₂ ζ₃ : arithcc.state) :
ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃
source
def arithcc.state_eq (t : arithcc.register) (ζ₁ ζ₂ : arithcc.state) :
Prop

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

Equations
source
@[protected, refl]
theorem arithcc.state_eq.refl (t : arithcc.register) (ζ : arithcc.state) :
ζ ≃[t] ζ
source
@[protected, symm]
theorem arithcc.state_eq.symm {t : arithcc.register} (ζ₁ ζ₂ : arithcc.state) :
ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₁
source
@[protected, trans]
theorem arithcc.state_eq.trans {t : arithcc.register} (ζ₁ ζ₂ ζ₃ : arithcc.state) :
ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₃ → ζ₁ ≃[t] ζ₃
source
@[protected, trans]
theorem arithcc.state_eq_state_eq_rs.trans (t : arithcc.register) (ζ₁ ζ₂ ζ₃ : arithcc.state) :
ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃

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

source
theorem arithcc.state_eq_implies_write_eq {t : arithcc.register} {ζ₁ ζ₂ : 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].

source
theorem arithcc.state_eq_rs_implies_write_eq_rs {t : arithcc.register} {ζ₁ ζ₂ : 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.

source
theorem arithcc.write_eq_implies_state_eq {t : arithcc.register} {v : arithcc.word} {ζ₁ ζ₂ : arithcc.state} (h : ζ₁ ≃[t + 1] arithcc.write t v ζ₂) :
ζ₁ ≃[t] ζ₂

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

source
theorem arithcc.compiler_correctness (map : arithcc.identifier → arithcc.register) (e : arithcc.expr) (ξ : arithcc.identifier → arithcc.word) (η : arithcc.state) (t : arithcc.register) :
(∀ (x : arithcc.identifier), arithcc.read (arithcc.loc x map) η = ξ x) → (∀ (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.