Compiler and correctness

Using the builtin Haskell parsing utilities, the parser function reads,

parser :: String -> Maybe STree
parser input = case parse expr "" input of
		    Left _  -> Nothing
		    Right e -> Just e

where expr of type Parser STree. Well, please read all the details in the file Parser.hs. Keeping simplicity in mind, the data type for the tree is just:

data STree =
  Val Integer
  | Add STree STree

where the leaf is named Val and carries the value of an integer; the constructor Add is a node and by referring recursively to STree it defines the tree . For instance, (1 + 2) + 3 is thus represented by the tree,

     Add
    /   \
  Add    Val 3
 /   \
Val 1 Val 2

where Val are leaves and Add are nodes. So far, so good!

The emulator (virtual machine) runs two instructions (PUSH and ADD), the binary, here, is a list of instructions, and the stack is a list of integers. The Haskell code implementing these words reads,

data Instr =
  PUSH Integer
  | ADD

type Binary = [Instr]
type Stack  = [Integer]

Therefore, the emulator takes a binary, returns a stack and it executes (computes) starting with an empty stack,

emulator :: Binary -> Stack
emulator b = exec b []

For the interested reader, the details of exec is provided here.

The input of the compiler a tree STree and it produces a binary (a list of instructions), i.e., it reads,

compiler :: STree -> Binary
compiler source = comp source []

where comp is an auxiliary function dealing with each case of the tree: if it is a leaf (Val), then the instruction is to PUSH the value in the stack (bytecode), otherwise if it is a node (Add), then compile recursively the subtrees and set the instruction ADD to stack. These words are implemented in Haskell with,

comp :: STree -> Binary -> Binary
comp (Val n) bytecode   = PUSH n : bytecode
comp (Add x y) bytecode = comp x $ comp y $ ADD : bytecode

Nothing fancy!

…to complete a working example, the functions push and pop are here the identity function (do nothing) and take the first element. Well, adding some other minor code,

• cmd for the command line interface and parsing the input string,
• go for gluing the compilation and running parts,
• emit for debugging purpose,

and we end with,

$ ./calc-no-coq -x '(1+2)+3'
= 6
$ ./calc-no-coq -c '(1+2)+3'
Instructions: "PUSH 1, PUSH 2, ADD, PUSH 3, ADD, ;"

Neat!

Similarly to the previous implementation, we straightforwardly adpat the data structure for the instructions and the binary (list of instructions),

Inductive Instr:Type := PUSH (n : nat)
		      | ADD.

Definition Binary := list Instr.

The emulator executes a bytecode (b : Binary) and returns a stack,

Fixpoint exec (b : Binary) (s : Stack) : Stack :=
  match b, s with
    PUSH n :: rest, stack => exec rest (n :: stack)
  | ADD :: rest, m :: n :: stack => exec rest (m + n :: stack)
  | [], stack => stack
  | _, stack => stack
  end.

Definition emulator (b : Binary) := exec b [].

where exec is the function really computing; this function takes two arguments: a list of instructions (Binary) and stack and then returns another stack.

The compiler requires a tree (named above Coq.Tree) and an auxiliary function,

Fixpoint comp (source : Tree) (bytecode : Binary) : Binary :=
  match source with
    Lang.Val n => PUSH n :: bytecode
  | Lang.Add x y => comp x (comp y (ADD :: bytecode))
  end.

Definition compiler (source : Tree) := comp source [].

where all is strongly similar with the previous implementation.

…to a complete working example, we just need to extract from Coq to Haskell with,

Require Export Lang Compiler Emulator.

Require Extraction.
Extraction Language Haskell.
Extraction "Generated.hs" compiler emulator.

additing some Haskell glue code, as push and pop, and command-line and parser, we get,

$ ./calc -x '(1+2)+3'
= 6
$ ./calc -c '(1+2)+3'
Instructions: "PUSH 1, PUSH 2, ADD, PUSH 3, ADD, ;"
$ ./calc -c '1+(2+3)'
Instructions: "PUSH 1, PUSH 2, PUSH 3, ADD, ADD, ;"

Note the order of the instructions depending on the parenthesis order, i.e., depending on the tree, for instance,

  (1+2)+3            1+(2+3)

     Add                Add
    /   \              /   \
  Add    Val 3       Val 1  Add
 /   \                     /   \
Val 1 Val 2              Val 2 Val 3

Neat! However, let avoid to go out of rail and thus let recap!

• we are interested by the emulator and compiler parts,
• for both implementations, the command-line is done by the same Haskell implementation (cmd); idem for parsing (parser).

Now, we want to have a proof that the implementations of emulator and compiler are correct. For the implementation in Haskell, we cannot do much, except run QuickCheck (large number of examples picked randomly). For the implementation in Coq, well Coq is a proof assistant after all, so could we prove something about the correctness?

The emulator is a layer on the top of the execution model – the function exec. Instead of the theorem correctness, we could think about the theorem,

Theorem correctness': forall (code : Tree) (stack : Stack),
    exec (compiler code) stack = eval code :: stack.

and if this theorem correstness' holds, then the proof of the theorem correctness reads,

Corollary correctness'': forall (code : Tree),
    exec (compiler code) [] = eval code :: [].
Proof.
  intro code.
  rewrite correctness'.
  reflexivity.
Qed.

Theorem correctness: forall (code : Tree),
    emulator (compiler code) = eval code :: [].
Proof.
  intro code.
  unfold emulator.
  rewrite correctness''.
  reflexivity.
Qed.

where the corollary is a straightforward application of the (admitted for now) theorem. Then, the proof of correctness just unfolds the function of interest emulator and applies (rewrite) the previous proved corollary.

How do we prove this theorem correctness'?

The correctness is now dependent on the theorem correctness'. Because compiler is a wrapper around the function comp, we could think about the lemma,

Lemma correctness_comp: forall (code : Tree) (bytecode : Binary) (stack : Stack),
    exec (comp code bytecode) stack = exec bytecode (eval code :: stack).

The key point of the proof is the use of the additing commutativity proof Nat.add_comm, \(\forall n, m : n + m = m + n\). Such could appear straightforward, but it is not because it depends on how the numbers are internally represented. For efficiency purpose, a computer somehow represents only a finite set of natural numbers, commonly named integer. Instead Coq is using, by default, the mathematical construction of natural numbers defining a zero, noted O and a successor, i.e., the data structure,

Inductive nat : Type :=
  O
  | S n.

where e.g., 3 is thus S (S (S 0)). That's why, the proof applies Nat.add_comm. Aside this consideration, the proof mainly unfolds and folds the definitions; see below.

Using this correctness_comp lemma, then the corollary correctness_comp' just considers the case of an empty binary,

Corollary correctness_comp': forall (code:Tree) (stack:Stack),
    exec (comp code []) stack = eval code :: stack.

…ending the proof is just unfolding the functions of interest and applying (rewrite) the previous proved results. The complete proof of correctness is therefore (presented linearly as in math textbook),

Lemma correctness_comp: forall (code:Tree) (bytecode:Binary) (stack:Stack),
    exec (comp code bytecode) stack = exec bytecode (eval code :: stack).
Proof.
  intros code.
  induction code.
  - simpl. reflexivity.
  - unfold comp. fold comp.
    intros bytecode stack.
    rewrite IHcode1.
    rewrite IHcode2.
    unfold eval. fold eval.
    unfold exec. fold exec.
    rewrite Nat.add_comm.
    reflexivity.
Qed.

Corollary correctness_comp': forall (code:Tree) (stack:Stack),
    exec (comp code []) stack = eval code :: stack.
Proof.
  intros code stack.
  rewrite correctness_comp.
  unfold exec.
  reflexivity.
Qed.

Theorem correctness': forall (code:Tree) (stack:Stack),
    exec (compiler code) stack = eval code :: stack.
Proof.
  intros code stack.
  unfold compiler.
  rewrite correctness_comp'.
  reflexivity.
Qed.

Corollary correctness'': forall (code:Tree),
    exec (compiler code) [] = eval code :: [].
Proof.
  intro code.
  rewrite correctness'.
  reflexivity.
Qed.

Theorem correctness: forall (code:Tree),
    emulator (compiler code) = eval code :: [].
Proof.
  intro code.
  unfold emulator.
  rewrite correctness''.
  reflexivity.
Qed.

Done! Well, almost. We could also prove that the behaviour of the interpreter eval is correct, i.e., the properties of the addition for mathematical intergers are fully satisfied.