Certified Compilation in Agda

Using dependent types, it is possible to specify contracts for Agda programs at a very fundamental level. Today we’ll see how to transform an extremely simple tree-based calculator language to a stack-based one; and use Agda to assert the correctness of our transformation. The complete source code for this post is at ¹.

The tree-based language is defined by the following data-type, with the obvious semantics:

data Exp : Set → Set₁ where
  ↑_ : {A : Set} → A → Exp A
  _plus_ : Exp ℕ → Exp ℕ → Exp ℕ
  _minus_ : Exp ℕ → Exp ℕ → Exp ℕ
  _eq_ : Exp ℕ → Exp ℕ → Exp Bool
  _lt_ : Exp ℕ → Exp ℕ → Exp Bool
  cond_then_else_ : {A : Set} → Exp Bool → Exp A → Exp A → Exp A

Note how dependent types are helpful already – without them we would not be able to elegantly assert ², for instance, that lt takes two Exp ℕs and maps them to an Exp Bool. The semantics are defined by a function with the stereotypical name eval of type Exp A → A.

eval : {A : Set} → Exp A → A
eval (↑ value) = value
eval (a plus b) = eval a + eval b
eval (a minus b) = eval a ∸ eval b
eval (a eq b) with Data.Nat._≟_ (eval a) (eval b)
... | yes _ = true
... | no _ = false
eval (a lt b) with Data.Nat._≤?_ (eval a) (eval b)
... | yes _ = true
... | no _ = false
eval (cond c then t else f) = if eval c then eval t else eval f

Nothing unusual here, expect perhaps the implementation of eval (a eq b) and eval (a lt b). Boolean values aren’t especially useful in dependently-typed programming languages since they don’t carry a proof of why a proposition is true. Operations like ≟ and ≤ therefore evaluate to a Decidable instance; which, apart from the result of the comparision (the yes and no we’re pattern matching on here), also contain a proof term of why the proposition is true or false. Since we don’t need the proofs for this rather simple use-case, we merrily ignore the same by underscores.

The stack-machine we’ll compile to is a bit more interesting – here too we use dependent types to guarantee consistency as much as possible. First of all, we use a stack that tracks the types of all its elements separately:

data TypedStack : List Set → Set₁ where
  nil : TypedStack []
  push : {A : Set} {S : List Set} → A → TypedStack S → TypedStack (A ∷ S)

This signature ensures that, for instance, the first three elements of a stack of type TypedStack (ℕ ∷ ℕ ∷Bool ∷ S) (for some S) will have types ℕ, ℕ and Bool.

The stack machine has six bytecodes, bcAdd, bcSub, bcEq, bcLt, bcCond and push (one of the constructors for TypedStack).

bcAdd : {S : List Set} → TypedStack (ℕ ∷ ℕ ∷ S) → TypedStack (ℕ ∷ S)
bcAdd (push a (push b rest)) = push (a + b) rest

bcEq : {S : List Set} → TypedStack (ℕ ∷ ℕ ∷ S) → TypedStack (Bool ∷ S)
bcEq (push a (push b rest)) with Data.Nat._≟_ a b
... | yes _ = push true rest
... | no _ = push false rest

bcCond : {S : List Set} {A : Set} → TypedStack (Bool ∷ A ∷ A ∷ S) →
         TypedStack (A ∷ S)
bcCond (push c (push x (push y rest))) = push (if c then x else y) rest

The bytecode types specify how the bytecodes will transform the stack. A program in this context is essentially a composition of some of the above bytecodes

StackProgram : Set → Set₁
StackProgram a = {S : List Set} → TypedStack S → TypedStack (a ∷ S)

and a term of type StackProgram X is a program that leaves behind a value of type X when it’s done executing. So, for instance

leaveBehindEleven : StackProgram ℕ
leaveBehindEleven = bcAdd ∘ push 5 ∘ push 6

is well typed but

popsEmptyStack : StackProgram ℕ
popsEmptyStack = bcAdd ∘ push 5

isn’t.

Now we come to the compiler that transforms programs in the tree form to equivalent programs in the stack-machine form. The compiler itself is simple (some cases have been left out):

compile : {A : Set} → Exp A → StackProgram A
compile (↑ y) = push y
compile (a plus b) = bcAdd ∘ compile a ∘ compile b
compile (a eq b) = bcEq ∘ compile a ∘ compile b
compile (cond c then x else y) = bcCond ∘ compile c ∘ compile x ∘ compile y
-- ...

As a proof that the compiler actually preserves program semantics, we look for a term, verifyCompiler of the type {A : Set} → (exp : Exp A) → IsCorrectFor exp where IsCorrectFor exp = (S : List Set) → (compile exp {S} ≡ push{_}{S} (eval exp)). In plain English, an expression exp is correctly compiled, denoted as IsCorrectFor exp, only if compiling and executing the stack-machine version is the same as evaluating the tree version and pushing the evaluated value onto the stack. The compiler is correct only if it correctly compiles all expressions. If you’ve been following along, give writing verifyCompiler yourself a shot!

Agda finds the simplest case for verifyCompiler obvious

verifyCompiler (↑ y) S = refl

To prove that we correctly compile a minus b, we need to show that compile (a minus b) is the same function (compile returns a stack program, which is essentially a function from TypedStack to TypedStack) as push (eval (a minus b)). To do this, we first show that since compile b is the same as push (eval b), compile (a minus b) is bcSub ∘ compile a ∘ compile b is bcSub ∘ compile a ∘ (push (eval b)). This is shown in sub-prf₀. Similarly, in sub-prf₁ we show that since compile a is the same as push (eval a), bcSub ∘ compile a ∘ (push (eval b)) is the same as bcSub ∘ (push (eval a)) ∘ (push (eval b)). These two combined, by transitivity, gives us our proof – Agda is clever enough to see that bcSub ∘ (push (eval a)) ∘ (push (eval b)) reduces to push ((eval a) ∸ (eval b)).

verifyCompiler (a minus b) S =
  let inductionA = verifyCompiler a
      inductionB = verifyCompiler b
      sub-prf₀ = subst (λ term → compile (a minus b)
                       ≡ bcSub ∘ compile a ∘ term)
                 (inductionB S) refl
      sub-prf₁ = subst (λ term → bcSub ∘ compile a ∘ (push (eval b))
                        ≡ bcSub ∘ term ∘ (push (eval b)))
                 (inductionA (ℕ ∷ S)) refl
  in trans sub-prf₀ sub-prf₁

We slightly deviate from this approach when proving correctness when compiling for a lt b and a eq b – I had to case on the two possibilities when comparing a and b.

Certified compilation is a rather ³ interesting ⁴ topic – something I’d like to explore further. A compiler for something a little more substantial than basic arithmetic should be a nice sequel.