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 #

@[reducible]
def arithcc.word  :

Value type shared by both source and target languages.

Equations
@[reducible]

Variable identifier type in the source language.

Equations
@[reducible]

Register name type in the target language.

Equations
theorem arithcc.register.le_of_lt_succ {r₁ r₂ : arithcc.register} :
r₁ < r₂ + 1 r₁ r₂

Source language #

@[protected, instance]
inductive arithcc.expr  :

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

Instances for arithcc.expr
@[simp]

The semantics of the source language (2.1).

Equations

Target language #

inductive arithcc.instruction  :

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

Instances for arithcc.instruction
structure arithcc.state  :

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
@[protected, instance]
Equations
@[simp]

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

Equations
@[simp]

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

Equations
@[simp]

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

Equations
@[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 #

@[simp]

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

Equations
@[simp]

The implementation of the compiler (4.2).

This definition explicitly takes a map from variables to registers.

Equations

Correctness #

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
@[protected, refl]
@[protected, symm]
theorem arithcc.state_eq_rs.symm {t : arithcc.register} (ζ₁ ζ₂ : arithcc.state) :
ζ₁ ≃[t]/ac ζ₂ ζ₂ ≃[t]/ac ζ₁
@[protected, trans]
theorem arithcc.state_eq_rs.trans {t : arithcc.register} (ζ₁ ζ₂ ζ₃ : arithcc.state) :
ζ₁ ≃[t]/ac ζ₂ ζ₂ ≃[t]/ac ζ₃ ζ₁ ≃[t]/ac ζ₃
def arithcc.state_eq (t : arithcc.register) (ζ₁ ζ₂ : arithcc.state) :
Prop

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

Equations
@[protected, refl]
@[protected, symm]
theorem arithcc.state_eq.symm {t : arithcc.register} (ζ₁ ζ₂ : arithcc.state) :
ζ₁ ≃[t] ζ₂ ζ₂ ≃[t] ζ₁
@[protected, trans]
theorem arithcc.state_eq.trans {t : arithcc.register} (ζ₁ ζ₂ ζ₃ : arithcc.state) :
ζ₁ ≃[t] ζ₂ ζ₂ ≃[t] ζ₃ ζ₁ ≃[t] ζ₃
@[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.

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].

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.

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].

The main compiler correctness theorem.

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