# mathlib3documentation

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 #

• 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. http://jmc.stanford.edu/articles/mcpain/mcpain.pdf

## 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  :
• const :
• var :
• sum :

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 #

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

The semantics of the target language (3.11).

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₂) η = η)

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

### Compiler #

@[simp]

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

Equations
• map = map ν
@[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) :
ζ₁ ≃[t + 1] ζ₂

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) :
ζ₁ ≃[t]/ac ζ₂

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] ζ₂) :
ζ₁ ≃[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.