On relational compilation

The traditional process for developing a verified compiler is to define types that model the source (\(S\)) and target (\(T\)) languages, and to write a function \(f: S \rightarrow T\) that transforms an instance \(s\) of the source type into an instance \(t = f(s)\) of the target type, such all behaviors of \(t\) match existing behaviors of \(s\) (“refinement”) and sometimes additionally such that all behaviors of \(s\) can be achieved by \(t\) (“equivalence”, or “correctness”).

Naturally, proving correctness for such a compiler requires a formal understanding of the semantics of languages \(S\) and \(T\) (that is, a way to give meaning to programs \(s \in S\) and \(t \in T\), so that it is possible to speak of the behaviors of a program: return values, I/O, resource usage, etc.). Then the refinement criterion above translates to \(\sigma _T(t) \subseteq \sigma _S(s)\) (where \(\sigma _S(s)\) denotes the behaviors of \(s\) and \(\sigma _T(t)\) those of \(t\)), and the correctness criterion defines a relation \(~\) between source and target programs such that \(t \sim s\) iff. \(\sigma _T(t) = \sigma _S(s)\). With that, a compiler \(f\) is correct iff. \(f(s) \sim s\) for all \(s\).

Relational compilation is a twist on that approach: it turns out that instead of writing the compiler as a monolithic program and separately verifying it, we can break up the compiler's correctness proof into a collection of orthogonal correctness theorems, and use these theorems to drive a code-generating proof search process. It is a Prolog-style “compilers as relations” approach, but taken one step further to get “compilers as (constructive) decision procedures”.

Instead of writing our compiler as a function \(f: S \rightarrow T\), we will write the compiler as a (partial) decision procedure: an automated proof-search process for proving theorems of the form \(\exists t, \sigma _T(t) = \sigma _S(s)\). In a constructive setting, any proof of that statement must exhibit a witness \(t\), which will be the (correct) compiled version of \(s\). (Note that the theorem does not \(\forall \)-quantify \(s\), as we want to generate one distinct proof per input program — otherwise, with a \(\forall s\) quantification, the theorem would be equivalent by skolemization to \(\exists f, \forall s, \sigma _T(f(s)) = \sigma _S(s)\), which is the same as defining a single compilation function \(f\)… and precisely what we're trying to avoid.)

The two main benefits of this approach are flexibility and trustworthiness: it provides a very natural and modular way to think of compiler extensions, and it makes it possible to extract shallowly embedded programs without trusting an extraction routine (in contrast, extraction in Coq is trusted). The main cost? Completeness: a (total) function always terminates and produces a compiled output; a (partial) proof search process may loop or fail to produce an output. [1]

This is not an entirely new idea: variations on this trick have been variously referred to in the literature as proof-producing compilation, certifying compilation, and, when the source language is shallowly embedded (we will get to that a bit later), proof-producing extraction, certifying extraction, or binary extraction. I have not seen a systematic explanation of it yet, so here is my attempt. I like to call this style of compilation “relational compilation”, and to explain it I like to start from a traditional verified compiler and progressively derive a relational compiler from it.

Use case 1: Compiling shallowly embedded DSLs

The original set up of the problem (compiling from language \(S\) to language \(T\)) required us to exhibit a function \(f: S \rightarrow T\). Not so with the new set up, which instead requires us to prove instances of the ∼ relation (one per program). What this means is that we can apply this compilation technique to compile shallowly embedded programs, including shallowly embedded DSLs [3].

Here is how we would change our previous example to compile arithmetic expressions written directly in Gallina (Gallina is functional programming language inside of the Coq proof assistant):

Start by redefining the relation to use Gallina expressions on the right side of the equivalence (there are no more references to \(S\) nor σS):
```
Notation "t ≈ s" := (forall ts, σT t ts = s :: ts).
```

Add compilation lemmas (the proofs are exactly the same as before, so they are omitted). Note that on the right side we have plain Gallina + and -, not SAdd and SOp, so each lemma now relates a shallow program to an equivalent deep-embedded one:

Lemma GallinatoT_Z z :
  [TPush z] ≈ z.z: Z
[TPush z] ≈ z

Lemma GallinatoT_Zopp t z :
  t ≈ z ->
  [TPush 0] ++ t ++ [TPopSub] ≈ - z.t: T
z: Z
t ≈ z -> [TPush 0] ++ t ++ [TPopSub] ≈ - z

Lemma GallinatoT_Zadd t1 z1 t2 z2 :
  t1 ≈ z1 ->
  t2 ≈ z2 ->
  t1 ++ t2 ++ [TPopAdd] ≈ z1 + z2.t1: T
z1: Z
t2: T
z2: Z
t1 ≈ z1 -> t2 ≈ z2 -> t1 ++ t2 ++ [TPopAdd] ≈ z1 + z2

These lemmas are sufficient to create a small compiler: as before we populate a hint database with our compilation lemmas:

Create HintDb stack.
Hint Resolve GallinatoT_Z | 10 : stack.
Hint Resolve GallinatoT_Zopp : stack.
Hint Resolve GallinatoT_Zadd : stack.

And then we run our relational compiler on shallowly embedded input programs:

Example g7 := 3 + 6 + Z.opp 2.

Example t7_shallow: { t7 | t7 ≈ g7 }.{t7 : T | t7 ≈ g7}
Proof. eauto with stack. Defined.

Compute t7_shallow.= exist [TPush 7]
: {t7 : T | t7 ≈ g7}

Of course, it is easy to package this in a convenient notation (the pattern match Set return T with _ => X end is a roundabout way to force the type of the value X):

Notation compile gallina_term :=
  (match Set return { t | t ≈ gallina_term } with
   | _ => ltac:(eauto with stack)
   end)
  (only parsing).

Compute compile (3 + 6 + Z.opp 2).= exist [TPush 7]
: {t : T | t ≈ 3 + 6 + - (2)}

There is something slightly magical happening here. By rephrasing compilation as a proof search problem, we are been able to make a compiler that would not even be expressible (let alone provable!) as a regular Gallina function. Reasoning on shallowly embedded programs is often much nicer than reasoning on deeply embedded programs, and this technique offers a convenient way to bridge the gap.

Use case 2: Extensible compilation

Up to this point we assumed that the input language was fixed, but in fact now that we are compiling shallowly embedded Gallina programs we can trivially extend the source language with additional constructs. Fortunately, the relational compilation technique above readily supports extending the compiler to support new source expressions.

In fact, extensible languages is one place where relational compilation shines. As an example, suppose we are modeling combinational hardware circuits in Coq. Our target type (deep-embedded Boolean expressions) is very simple:

Inductive circuit :=
| Const (z: Z)
| Read (reg_name: string)
| Mux (cond l r: circuit)
| Op (op_name: string) (args: list circuit).

Notice how the Op and Reg constructors (used to call built-in operators and to read registers) take names as strings: this means that to define an interpreter for the language we need an environment Σ of functions defining the semantics of the builtin operators of the language (3) and a context R giving the value of each register (4). The code below uses the notation c.[k] to look up key k in context c (it defaults to an arbitrary value if the key k cannot be found):

Section Interp.
  Variable Σ: string -> (list Z -> Z).3
  Variable R: list (string * Z).4

  Fixpoint cinterp (c: circuit) : Z := match c with
    | Const z => z
    | Read r => R.[r]
    | Mux cond t f =>
      if cinterp cond =? 0 then cinterp f else cinterp t
    | Op op args =>
      Σ op (List.map cinterp args)
  end.
End Interp.

Here is an example.

First, we define an environment of built-in functions:

Definition testbit z n :=
  if Z.testbit z n then 1 else 0.

Example Σ0 fn args := match fn, args with
  | "add", [z1; z2] => Z.add z1 z2
  | "xor", [z1; z2] => Z.lxor z1 z2
  | "nth", [z; n] => testbit z n
  | _, _ => 0 (* Default to 0 for simplicity *)
end.

Then, we define an environment of registers:

Example R0 :=
  [("pc", 16); ("ppc", 14); ("r1", 5); ("r2", 7)].

And finally we can run the interpreter on an example circuit c1:

Example c1 :=
  Mux (Op "xor" [Read "pc"; Read "ppc"])
      (Read "r1") (Read "r2").

Reducing everything but Σ0 shows the interpretation of Mux in this term:

Eval cbn -[Σ0] in cinterp Σ0 R0 c1.= if Σ0 "xor" [16; 14] =? 0 then 7 else 5
: Z

… and reducing everything gives us the value of this example circuit:

Compute cinterp Σ0 R0 c1.= 5
: Z

Relational compilation is a simple and convenient way to generate such circuits from Gallina expressions. First, we need a compilation relation:

Notation "c ≋ g @ Σ // R" := (cinterp Σ R c = g).

Then, we need compilation lemmas relating source programs in Gallina and their circuit equivalents.

First, constants:

Lemma compile_Const {Σ R} z:
  Const z ≋ z @ Σ // R.Σ: string -> list Z -> Z
z: Z
Const z ≋ z @ Σ // R

Then variable accesses, compiled to register reads:

Lemma compile_Read {Σ R} r z:
  z = R.[r] ->
  Read r ≋ z @ Σ // R.Σ: string -> list Z -> Z
r: string
z: Z
z = R.[r] -> Read r ≋ z @ Σ // R

Then conditionals:

Lemma compile_Mux {Σ R} ccond gcond ct gt cf gf:
  ccond ≋ gcond @ Σ // R ->
  ct    ≋ gt    @ Σ // R ->
  cf    ≋ gf    @ Σ // R ->
  Mux ccond ct cf ≋ if gcond =? 0 then gf else gt @ Σ // R.Σ: string -> list Z -> Z
ccond: circuit
gcond: Z
ct: circuit
gt: Z
cf: circuit
gf: Z
ccond ≋ gcond @ Σ // R ->
ct ≋ gt @ Σ // R ->
cf ≋ gf @ Σ // R -> Mux ccond ct cf ≋ if gcond =? 0 then gf else gt @ Σ // R

And finally operators. Note that compilation lemmas are parametric on the environment of functions, only requiring that the one function it uses be found in the environment:

Lemma compile_add {Σ R} c1 g1 c2 g2:
  (forall x y, Σ "add" [x; y] = Z.add x y) ->
  c1 ≋ g1 @ Σ // R ->
  c2 ≋ g2 @ Σ // R ->
  Op "add" [c1; c2] ≋ Z.add g1 g2 @ Σ // R.Σ: string -> list Z -> Z
c1: circuit
g1: Z
c2: circuit
g2: Z
(forall x y : Z, Σ "add" [x; y] = x + y) ->
c1 ≋ g1 @ Σ // R -> c2 ≋ g2 @ Σ // R -> Op "add" [c1; c2] ≋ g1 + g2 @ Σ // R

Lemma compile_xor {Σ R} c1 g1 c2 g2:
  (forall x y, Σ "xor" [x; y] = Z.lxor x y) ->
  c1 ≋ g1 @ Σ // R ->
  c2 ≋ g2 @ Σ // R ->
  Op "xor" [c1; c2] ≋ Z.lxor g1 g2 @ Σ // R.Σ: string -> list Z -> Z
c1: circuit
g1: Z
c2: circuit
g2: Z
(forall x y : Z, Σ "xor" [x; y] = Z.lxor x y) ->
c1 ≋ g1 @ Σ // R -> c2 ≋ g2 @ Σ // R -> Op "xor" [c1; c2] ≋ Z.lxor g1 g2 @ Σ // R

Lemma compile_nth {Σ R} cz gz cn gn:
  (forall z n, Σ "nth" [z; n] = testbit z n) ->
  cz ≋ gz @ Σ // R ->
  cn ≋ gn @ Σ // R ->
  Op "nth" [cz; cn] ≋ testbit gz gn @ Σ // R.Σ: string -> list Z -> Z
cz: circuit
gz: Z
cn: circuit
gn: Z
(forall z n : Z, Σ "nth" [z; n] = testbit z n) ->
cz ≋ gz @ Σ // R ->
cn ≋ gn @ Σ // R -> Op "nth" [cz; cn] ≋ testbit gz gn @ Σ // R

That is enough to compile a simple EDSL for circuits. There are a few things worthy of note here; first, we now have a mechanism to refer to bound variables, through the R environment; second, each compilation lemma is parametric on the environment of functions, so the whole compiler is extensible. Let us see these two points in action with a more complex program:

Definition gc1 pc ppc (r1 r2: Z) :=
  let correct := pc =? ppc in
  let v := if correct then r1 else r2 in
  testbit v 4.

This program checks if its first two arguments to see if they are equal, and returns a different value in each case. The relational compilation goal will looks a bit different from previous ones, because we now need to account for an environment of variables:

Example cc1 : { cc1 | forall pc ppc r1 r2,
   cc1 ≋ gc1 pc ppc r1 r2 @ Σ0
   // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)] }.{cc1 : circuit
| forall pc ppc r1 r2 : Z,
  cc1 ≋ gc1 pc ppc r1 r2 @ Σ0 //
  [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]}

In other words: there exists a circuit cc1 equivalent to the Gallina program gc1 for all inputs pc, ppc, r1, and r2, assuming that these inputs are available in registers and that the circuit runs with the environment of built-ins Σ0 The proof too looks a bit different, because there now are side conditions for certain lemmas:

Proof.
  eexists; intros; unfold gc1.?cc1 ≋ testbit (if pc =? ppc then r1 else r2) 4 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

The program starts with a call to testbit, so we plug in the circuit primitive "nth":

  eapply compile_nth.forall z n : Z, Σ0 "nth" [z; n] = testbit z n
?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?cn ≋ 4 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

We now get three subgoals: one asserting that we can call the function "nth" given the current function environment Σ, and two corresponding to each of the arguments to testbit in Gallina:

  1: reflexivity.?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?cn ≋ 4 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

Of the two argument subgoals, the first one is a conditional to which none of our compilation lemmas apply: as we defined it, compile_Mux requires a specific Gallina pattern, _ =? 0, which is not present here:

?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]    apply compile_Mux.In environment
pc, ppc, r1, r2 : Z
Unable to unify
 "Mux ?M1440 ?M1442 ?M1444 ≋ if ?M1441 =? 0 then ?M1445 else ?M1443 @ ?Σ // ?R"
with
 "?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
  [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]".

This is the first instance where the extensibility of relational compilation comes into play. For this example, we can extend the compiler by plugging in a rewrite rule that transforms the program to match a shape supported by the compiler, after which Compile_Mux applies:

Z_lxor_eqb
     : forall z1 z2, (z1 =? z2) = (Z.lxor z1 z2 =? 0)    rewrite Z_lxor_eqb.?cz ≋ if Z.lxor pc ppc =? 0 then r1 else r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
    apply compile_Mux.

Compiling the conditional leaves us with three more subgoals: one for the test, one for the right branch, and one for the left branch:

?ccond ≋ Z.lxor pc ppc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?ct ≋ r2 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?cf ≋ r1 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

The first part can be handled using the compile_xor lemma:

      apply compile_xor; try reflexivity.?c1 ≋ pc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?c2 ≋ ppc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

And this is where the second interesting part of this proof comes about: handling variables. First, let us try something that looks right, but will not work:

        apply compile_Const.In environment
pc, ppc, r1, r2 : Z
Unable to unify "?c1" with "Const pc" (cannot instantiate 
"?c1" because "pc" is not in its scope).

It is very important that this shouldn't work, but it is not immediately obvious why it wouldn't. The value pc is indeed not a constant, but it you look just at the types, things do line up:

?c1 ≋ pc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]compile_Const pc
     : Const pc ≋ pc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

The reason it doesn't work is captured in the error message above. When Coq creates the evars denoted by ?…, it associates with each of them a context that records which variables they may refer to. Here is, for example, the internal goal that Coq generated for ?c1:


c1circuit

In other words, the evar ?c1 cannot refer to any of the local variables — which is good, since we're trying to build a closed term! What we want, of course, is compile_Read, which reads into the environment of registers, not compile_Const:

        apply compile_Read with (r := "pc"); reflexivity.

The same lemma applies to the next three goals, in fact:

?c2 ≋ ppc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]        apply compile_Read with (r := "ppc"); reflexivity.

?ct ≋ r2 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]      apply compile_Read with (r := "r2"); reflexivity.

?cf ≋ r1 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]      apply compile_Read with (r := "r1"); reflexivity.

And finally we have the second argument to the original testbit, the index of the bit that we want to extract:

?cn ≋ 4 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]    apply compile_Const.
Defined.

The resulting generated program is as expected, and correct by construction:

Print cc1.cc1 = 
exist
  (Op "nth"
     [Mux (Op "xor" [Read "pc"; Read "ppc"]) (Read "r2") (Read "r1"); Const 4])
     : {cc1 : circuit
       | forall pc ppc r1 r2 : Z,
         cc1 ≋ gc1 pc ppc r1 r2 @ Σ0 //
         [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]}

Automating the derivation

The process above is closer to tool-assisted program derivation than to “compilation”. Automating it is not hard, but it requires tricks beyond what we have seen above. We will start by creating a hint database to hold our custom compilation lemmas:

Create HintDb circuits.

For readability, we will use Coq's Derive feature to state our compilation goal. Derive defines a dependent pair (a term and a proof of a property about it) as two separate names:

Derive cc1' SuchThat (forall pc ppc r1 r2,
    cc1' ≋ gc1 pc ppc r1 r2 @ Σ0
    // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)])
  As cc1'ok.cc1':= ?Goal: circuit
forall pc ppc r1 r2 : Z,
cc1' ≋ gc1 pc ppc r1 r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
Proof.
  unfold cc1', gc1; clear cc1'.forall pc ppc r1 r2 : Z,
?Goal ≋ testbit (if pc =? ppc then r1 else r2) 4 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

The first trick we will introduce is forward reasoning. Until now, we have used eauto to pull from a database of lemmas to try to derive a complete proof of a goal. In this mode, eauto is all-or-nothing: it will not make any progress on this goal until we introduce all relevant lemmas:

  eauto using compile_nth.forall pc ppc r1 r2 : Z,
?Goal ≋ testbit (if pc =? ppc then r1 else r2) 4 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

This isn't sustainable: we need to guess exactly all lemmas that are required, or nothing happens. Instead we will use a partial progress style popularized by [CoqProlog+Zimmermann+TTT2017], in which we program eauto to take a single step and then return to its caller:

  Hint Extern 2 => simple apply compile_Const; shelve : circuits.
  Hint Extern 2 => simple apply compile_add; shelve : circuits.
  Hint Extern 2 => simple apply compile_xor; shelve : circuits.
  Hint Extern 2 => simple apply compile_nth; shelve : circuits.

Each of these hints allow eauto to shelve the current goal after applying the corresponding lemma, which removes the subgoals generated by that lemma from the pool of things the eauto is required to solve and places the on Coq's shelf.

Coq's shelf is a side collection of goals that typically hold terms whose definition will follow from solving other goals. For example, in the following proof, the definition of ?x is on the shelf: it is expected that solving .io#shelf-example.s(eexists).g.ccl will instantiate ?x (note how the call to Show Existentials mentions that ?x is shelved):

Goal exists x, x + 1 = 2.exists x : Z, x + 1 = 2
  eexists.?x + 1 = 2
  Show Existentials.Existential 1 = ?x : [ |- Z] (shelved)
Existential 2 = ?Goal : [ |- ?x + 1 = 2]

Using the shelf allows us to define forward-reasoning tactics: we use unshelve to bring back the intermediate goals that were shelved within eauto (typeclasses eauto, in fact, since eauto puts things on the wrong shelf — Coq has more than one), and shelve_unifiable to move evars that are not propositional goals back on the shelf:

  Tactic Notation "step" "with" ident(db) :=
    intros; unshelve typeclasses eauto with db; shelve_unifiable.

  Tactic Notation "forward" "with" ident(db) :=
    progress repeat step with db.

These hints are enough to get us started with the derivation of our program. forward with … is a tactic similar to eauto, but it supports partial progress:

   forward with circuits.forall z n : Z, Σ0 "nth" [z; n] = testbit z n
?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

The first goal we get asks us to prove that we have the right function under the name "nth" in our function context, as before:

forall z n : Z, Σ0 "nth" [z; n] = testbit z n    Hint Extern 1 => reflexivity : circuits.forall z n : Z, Σ0 "nth" [z; n] = testbit z n
    forward with circuits.

The second goal is where this new approach of partial compilation begins to be useful: we have partially compiled our program, and we can now add more hints to continue making progress. As before, compile_Mux doesn't apply:

?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]    apply compile_Mux.In environment
pc, ppc, r1, r2 : Z
Unable to unify
 "Mux ?M1502 ?M1504 ?M1506 ≋ if ?M1503 =? 0 then ?M1507 else ?M1505 @ ?Σ // ?R"
with
 "?cz ≋ if pc =? ppc then r1 else r2 @ Σ0 //
  [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]".

We could use Z_lxor_eqb as before to rewrite the equality test pc =? ppc into an exclusive-or test Z.lxor pc ppc =? 0, but for consistency we will prove a new compilation lemma instead (this gives us a unified way to handle all extensions):

Lemma compile_Mux_eqb {Σ R} c1 g1 c2 g2 ct gt cf gf:
  (forall x y, Σ "xor" [x; y] = Z.lxor x y) ->
  c1 ≋ g1 @ Σ // R ->
  c2 ≋ g2 @ Σ // R ->
  ct ≋ gt @ Σ // R ->
  cf ≋ gf @ Σ // R ->
  Mux (Op "xor" [c1; c2]) ct cf ≋
  if g1 =? g2 then gf else gt @ Σ // R.Σ: string -> list Z -> Z
c1: circuit
g1: Z
c2: circuit
g2: Z
ct: circuit
gt: Z
cf: circuit
gf: Z
(forall x y : Z, Σ "xor" [x; y] = Z.lxor x y) ->
c1 ≋ g1 @ Σ // R ->
c2 ≋ g2 @ Σ // R ->
ct ≋ gt @ Σ // R ->
cf ≋ gf @ Σ // R ->
Mux (Op "xor" [c1; c2]) ct cf ≋ if g1 =? g2 then gf else gt @ Σ // R

This is enough to step further in the compilation process, leaving us with four very similar goals:

  Hint Extern 2 =>
    simple apply compile_Mux_eqb; shelve : circuits.forall pc ppc r1 r2 : Z,
?Goal ≋ testbit (if pc =? ppc then r1 else r2) 4 @ Σ0 //
[("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
  forward with circuits.?c1 ≋ pc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?c2 ≋ ppc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?ct ≋ r2 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?cf ≋ r1 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

This time, we get stuck because we did not register compile_Read:

?c1 ≋ pc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?c2 ≋ ppc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?ct ≋ r2 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?cf ≋ r1 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

Why not? Because as written, compile_Read applies to all goals, often leaving an unsolvable goal: when applied to a goal _ ≋ g @ _ // R, compile_Read will simply generate a goal asking to find g in R, regardless of whether such a binding in fact exists in R. For example:

  eexists ?[c].?c ≋ 1 + 1 @ Σ0 // [("r0", 14)]
  apply compile_Read.1 + 1 = [("r0", 14)].[?r]
Abort.

There are two ways to proceed in such cases: add logic to apply compile_Read eagerly, and backtrack if no corresponding binding can be found; or use a more clever strategy to apply compile_Read more discerningly. Up to this point our derivations have all been deterministic, and we want the compiler to be as predictable as possible, so we will do the latter by restricting the use of the compile_Read lemma to cases where the Gallina term g is a single variable. Additionally, we will give compile_Read a low priority (the backtracking approach is discussed in a note at the end of this section):

  Hint Extern 3 (_ ≋ ?v @ _ // _) =>
    is_var v; simple apply compile_Read; shelve : circuits.?c1 ≋ pc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?c2 ≋ ppc @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?ct ≋ r2 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]
?cf ≋ r1 @ Σ0 // [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)]

  all: forward with circuits.pc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r]
ppc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r0]
r2 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r1]
r1 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r2]

The remaining goals are the preconditions of compile_Read: the variables should in fact be in context:

pc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r]
ppc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r0]
r2 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r1]
r1 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r2]

To solve these goals automatically, we will use two simple lemmas.

assoc_hd, which handles the case in which the value we're looking for is the first in the list:

Lemma assoc_hd (v: V) k tl:
  v = ((k, v) :: tl).[k].V: Type
H: HasDefault V
v: V
k: string
tl: list (string * V)
v = ((k, v) :: tl).[k]

assoc_tl, which handles the case in which the value we're looking for is in the tail of the list:

Lemma assoc_tl (v v': V) k k' tl:
  v = tl.[k'] ->
  k <> k' ->
  v = ((k, v') :: tl).[k'].V: Type
H: HasDefault V
v, v': V
k, k': string
tl: list (string * V)
v = tl.[k'] -> k <> k' -> v = ((k, v') :: tl).[k']

Here is how these come into play, on a standalone example. We start with a goal asking us to locate the value 3 in a context. Applying assoc_tl discards the first binding ("x", 1) and asks us to find 3 among the remaining bindings; then, applying assoc_hd selects the first of the remaining bindings ("y", 3):

3 = [("x", 1); ("y", 3)].[?k]  apply assoc_tl.3 = [("y", 3)].[?k]
"x" <> ?k
  -3 = [("y", 3)].[?k] apply assoc_hd.
  -"x" <> "y" congruence.

Plugging in these two lemmas completes the derivation:

  Hint Extern 1 => congruence : circuits.pc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r]
ppc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r0]
r2 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r1]
r1 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r2]
  Hint Resolve assoc_hd assoc_tl | 2 : circuits.pc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r]
ppc = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r0]
r2 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r1]
r1 = [("pc", pc); ("ppc", ppc); ("r1", r1); ("r2", r2)].[?r2]
  all: forward with circuits.
Qed.

Print cc1'.cc1' = 
Op "nth"
  [Mux (Op "xor" [Read "pc"; Read "ppc"]) (Read "r2") (Read "r1"); Const 4]
     : circuit

In my experience, it is almost always best to reduce or eliminate backtracking. Crafting compilers is already a tricky business, and introducing backtracking makes debugging significantly harder. Generating proofs along programs ensure that the compiler does not produce incorrect output, but it does not rule out undesirable output, such as inefficient programs.

Still, in the compile_Read case above, an alternative approach would have been to apply the lemma unconditionally, but without shelving: in that case eauto would only have applied it when it is able to solve the resulting assoc subgoals:

Hint Resolve compile_Read assoc_hd assoc_tl : circuits.

Automating the initial setup

This handles the derivation itself; the initial unfolding phase of the derivation can be also handled automatically using a simple Ltac script to reveal the evar created by Derive and unfold toplevel program definitions, like gc1 above; we do all this in a new tactic compile with <database>:

Tactic Notation "setup" "with" ident(db) :=
  intros; autounfold with db;
  lazymatch goal with c := _ |- _ => subst c end.

Tactic Notation "compile" "with" ident(db) :=
  setup with db; forward with db.

And with this, we have our first, tiny, extensible compiler! Of course, this new compiler is applicable to a wide range of programs, not just the one we just compiled:

Derive c SuchThat (forall z, c ≋ z + z @ Σ0 // [("z", z)]) As cok.c:= ?Goal: circuit
forall z, c ≋ z + z @ Σ0 // [("z", z)]
Proof. compile with circuits. Qed.

Print c.c = Op "add" [Read "z"; Read "z"]
     : circuit

Leveraging contextual information

The last extension is important enough that it deserves its own section. It is a common pattern in functional programming languages to use a monad to describe an effect that is not supported by the language. Part of compiling the program down to a lower-level language is mapping the monadic structure to low-level primitives, and we can do that using relational compilation.

Even better, we can support native compilation of arbitrary monads (!): unlike traditional compilers that hard-code a list of built-in monads that get special compiler support (think IO in Haskell), we can plug-in native compilation support for arbitrary user-defined monads. This means that we never have to define an interpreter for a free monad (this is the usual approach in Coq for extraction effectful program: define a free monad specialized to a functor capturing effects, extract to OCaml, and define an unverified interpreter to map the effects to native OCaml effects; here, we can instead directly map the monad to effects of the target language).

We will start by exploring the example of the Writer monad with a compiler specialized for that monad, and then we will see an extra twist that allows us to define the pure parts of the compiler in a monad-agnostic way, so that they can be shared between different EDSL compilers specialized to different monads, reducing duplication. Rupicola itself has many more examples of relational compilation for monadic programs.

The writer monad

In this example, programs will return not just values, but also a list of strings, the "output" of the program:

Definition Trace := list string.
Record S {α: Type} := { val: α; trace: Trace }.

Example puts str := {| val := tt; trace := [str] |}.

The usual monadic operators are readily defined: a pure computation is like a monadic computation with an empty trace, and two effectful computations running in sequence produce the result of the second and the concatenation of the two traces:

Definition ret (a: α) : S α :=
  {| val := a; trace := [] |}.

Definition tr_bind (a: S α) (b: S β) :=
  {| val := b.(val); trace := a.(trace) ++ b.(trace) |}.

Definition bind (a: S α) (k: α -> S β) : S β :=
  tr_bind a (k a.(val)).

Notation "v ← a ; body" := (bind a%string (fun v => body)).

It is straightforward to prove that the usual monad properties hold:

Lemma bind_ret (ca: S α) :
  bind ca ret = ca.α, β, γ: Type
ca: S α
v ← ca;
ret v = ca
Lemma ret_bind a (k: α -> S β) :
  bind (ret a) k = (k a).α, β, γ: Type
a: α
k: α -> S β
v ← ret a;
k v = k a
Lemma bind_bind ca (ka: α -> S β) (kb: β -> S γ) :
  bind (bind ca ka) kb = bind ca (fun a => bind (ka a) kb).α, β, γ: Type
ca: S α
ka: α -> S β
kb: β -> S γ
v ← v ← ca;
    ka v;
kb v = a ← ca;
       v ← ka a;
       kb v

We will compile this to a simple imperative string language with traces. Here is the definition of expressions and statements in that language; this will also give us the opportunity to start discussing assignments:

Inductive Expr :=
| Ref var
| Const str
| Concat (e1 e2: Expr).

Inductive T :=
| Seq (t1 t2: T)
| Assign var (e: Expr)
| Puts (e: Expr)
| Skip.

The semantics of expressions is given by an interpreter:

Definition Ctx := list (Var * string).

Fixpoint interp ctx e : string := match e with
  | Ref var      => ctx.[var]
  | Const str    => str
  | Concat e1 e2 => interp ctx e1 ++ interp ctx e2
end.

… and, to spice things up, the semantics of statements is given by a big-step evaluation relation:

Inductive RunsTo : Ctx -> T -> Ctx -> Trace -> Prop :=
| RunsToSeq ctx0 t1 ctx1 tr1 t2 ctx2 tr2:
    ⟨ctx0, t1⟩ ⇓ ⟨ctx1, tr1⟩ ->
    ⟨ctx1, t2⟩ ⇓ ⟨ctx2, tr2⟩ ->
    ⟨ctx0, Seq t1 t2⟩ ⇓ ⟨ctx2, tr1 ++ tr2⟩
| RunsToAssign ctx var e:
    ⟨ctx, Assign var e⟩ ⇓ ⟨(var, interp ctx e) :: ctx, []⟩
| RunsToPuts ctx e:
    ⟨ctx, Puts e⟩ ⇓ ⟨ctx, [interp ctx e]⟩
| RunsToSkip ctx e:
    ⟨ctx, Skip⟩ ⇓ ⟨ctx, []⟩
where "⟨ ctx , p ⟩ ⇓ ⟨ ctx' , tr ⟩" :=
  (RunsTo ctx p ctx' tr).

The relational compiler for expressions is routine at this point, so we omit it for brevity. We simply define a relation ~ₑ for expressions, and prove lemmas relating outputs and inputs of interp. For very simple cases like this one, what we are really building is in fact a reification procedure, implemented by programming a decision procedure to invert the function interp:

Notation "e ~ₑ g // ctx" := (interp ctx e = g%string).

Derive eHello SuchThat (forall name,
  eHello ~ₑ ("hello, " ++ name) // [("name", name)])
As eHello_ok.eHello:= ?Goal: Expr
forall name : string, eHello ~ₑ "hello, " ++ name // [("name", name)] compile with str. Qed.

Print eHello.eHello = Concat (Const "hello, ") (Ref "name")
     : Expr

Conversely, there are a few new things in the relational compiler for statements. Specifically, we want to convert uses of monadic bind into a sequence, translating pure expressions using the expression compiler and using primitives to implement stateful computations like puts.

There is one significant difference from previous examples, however: our new target language has assignments, and these assignments are not directly reflected in the source language. As a result the final state of the program may contain arbitrary bindings, and it would be quite inconvenient to have to declare exactly which temporary variables may be used when starting the compilation process. Instead, we will use a slightly more complicated compilation relation. Unlike the equalities used previously, we now state that a low-level program is related to a high-level one if they produce the same traces, and if the result of the high-level program can be found in the final context, under a name specified as part of the compilation relation. Beyond this, the final context is allowed to contain arbitrary bindings.

Definition related t g var ctx :=
  (forall ctx' tr,
      ⟨ ctx, t ⟩ ⇓ ⟨ ctx', tr ⟩ ->
      g.(trace) = tr /\
      g.(val) = ctx'.[var]).

Notation "t ~ₜ g @ var // ctx" :=
  (related t g%string var ctx).

Each lemma about the new compilation relation ~ₜ matches a corresponding constructor of RunsTo closely, but not exactly, because we need to phrase things in terms of monadic operations. First we show how to compile Puts, which writes a value out:

Lemma compile_Puts ctx e g t k var:
  e ~ₑ g // ctx ->
  t ~ₜ k tt @ var // ctx ->
  Seq (Puts e) t ~ₜ bind (puts g) k @ var // ctx.ctx: Ctx
e: Expr
g: string
t: T
k: unit -> S string
var: Var
e ~ₑ g // ctx ->
t ~ₜ k tt @ var // ctx -> Seq (Puts e) t ~ₜ v ← puts g;
                                            k v @ var // ctx

Then Assign (quantifying over the value v prevents the expression g from getting inlined into the continuation k):

Lemma compile_Assign ctx e g t k var tmp:
  e ~ₑ g // ctx ->
  (forall v, v = g -> t ~ₜ k v @ var // (tmp, v) :: ctx) ->
  Seq (Assign tmp e) t ~ₜ bind (ret g) k @ var // ctx.ctx: Ctx
e: Expr
g: string
t: T
k: string -> S string
var, tmp: Var
e ~ₑ g // ctx ->
(forall v : string, v = g -> t ~ₜ k v @ var // (tmp, v) :: ctx) ->
Seq (Assign tmp e) t ~ₜ v ← ret g;
                        k v @ var // ctx

And finally a lemma to conclude the compilation, which uses an assignment because the way our compilation relation is phrased (see sidebar).

Lemma compile_Skip ctx e str var:
  e ~ₑ str // ctx ->
  Assign var e ~ₜ ret str @ var // ctx.ctx: Ctx
e: Expr
str: string
var: Var
e ~ₑ str // ctx -> Assign var e ~ₜ ret str @ var // ctx

It may be surprising that we do not have a lemma for compiling an arbitrary sequence — one that would handle any Gallina bind. Instead, we have two lemmas, specialized to the two kinds of expressions that may be bound, Puts and Assign, both with an arbitrary continuation. Is that not limiting? Not really.

The reason we do not have an arbitrary bind is that our equivalence relation is not precise enough: it does not specify exactly what the environment of variables is after running a piece of code. This is convenient, since it allows to phrase our lemmas concisely and easily; but it prevents us from phrasing a lemma to relate bind and Seq in general (and it makes it so that our Skip lemma does not in fact use Skip). What would such a bind lemma look like? We might hope to write something like the following, but this is not valid:

Lemma compile_Seq ctx t1 s1 t2 s2 var tmp:
  t1 ~ₜ s1 @ tmp // ctx ->
  t2 ~ₜ s2 s1.(val) @ var // (tmp, s1.(val)) :: ctx ->
  Seq t1 t2 ~ₜ bind s1 s2 @ var // ctx.ctx: Ctx
t1: T
s1: S string
t2: T
s2: string -> S string
var, tmp: Var
t1 ~ₜ s1 @ tmp // ctx ->
t2 ~ₜ s2 (val s1) @ var // (tmp, val s1) :: ctx ->
Seq t1 t2 ~ₜ v ← s1;
             s2 v @ var // ctx
Abort.

Indeed, the first premise says very little about the state of the machine after running t1: only that it will contain a binding tmp ↦ s1.(val). It does not say that ctx will be unmodified otherwise (t1 may create new bindings), and hence the environment in which Seq t1 t2 will run t2 is not guaranteed to be (tmp, s1.(val)) :: ctx, as required by the second premise.

This is not an issue for straightline code, but it does cause trouble for conditionals and loops that appear in the value part of a bind (what local variables can we assume the environment to contain after an if?). The monad-agnostic approach that we present in the next step solves this problem.

These compilation rules are enough to compile full programs (below, the tactic binder_name translates a Coq-level binder name into a string):

Hint Extern 1 => simple apply compile_Puts; shelve : str.
Hint Extern 1 => simple apply compile_Skip; shelve : str.

Hint Extern 1 (_ ~ₜ bind ?s ?k @ _ // _) =>
  simple apply compile_Assign
    with (tmp := ltac:(binder_name k)); shelve : str.

Definition greet (name: string) :=
  greeting ← ret ("hello, " ++ name);
  _ ← puts greeting;
  _ ← puts "!";
  ret greeting.
Hint Unfold greet : str.

Derive tHello SuchThat (forall name,
  tHello ~ₜ greet name @ "out" // [("name", name)])
As tHello_ok.tHello:= ?Goal: T
forall name : string, tHello ~ₜ greet name @ "out" // [("name", name)] compile with str. Qed.

Print tHello.tHello = 
Seq (Assign "greeting" (Concat (Const "hello, ") (Ref "name")))
  (Seq (Puts (Ref "greeting"))
     (Seq (Puts (Const "!")) (Assign "out" (Ref "greeting"))))
     : T

Monad-agnostic extraction

In the above, we defined a new extraction procedure for each monad, but we can reduce the required effort by generalizing further. We can define things in such a way that lemmas about non-monadic code work for all monad, which means that different domain-specific languages, using different monads, can all use the same code for compiling pure values. The key here is to completely generalize over the pre and post-conditions that the compiler uses, leaving only a distinguished argument to the postcondition indicating which program we are compiling. For this we define a Hoare triple on top of our program semantics (for brevity we define it on top of our big-step semantics instead of defining a new relation, and we omit the precondition, which will live in the ambient proof context instead):

Definition triple {α}
           (ctx: Ctx) (prog: T) (spec: α)
           (post: α -> Trace -> Ctx -> Prop) :=
  forall ctx' tr,
    ⟨ctx, prog⟩ ⇓ ⟨ctx', tr⟩ -> post spec tr ctx'.

Notation "<{ ctx }> prog <{ spec | post }>" :=
  (triple ctx prog spec post).

Note how the post-condition post takes a special argument spec, which is where we will plug in our Gallina programs (this trick makes it easy to spot the program that we're compiling when writing tactics that inspect the goal). Crucially, spec does not take a monadic argument in: any Gallina program is fair game to plug into this spot that drives the compiler. Our previous relation is a special case of this one, and in fact all lemmas will carry naturally. Specifically, we have:

Goal forall t g var ctx,
    <{ ctx }>
    t
    <{ g | fun g tr' ctx' =>
         g.(val) = ctx'.[var] /\
         g.(trace) = tr' }> ->
    t ~ₜ g @ var // ctx.forall t (g : S string) var ctx,
<{ ctx }> t <{ g
| fun (g0 : S string) (tr' : Trace) ctx' => val g0 = ctx'.[var] /\ trace g0 = tr'
}> -> t ~ₜ g @ var // ctx

Here is compile_Assign written in this new style. We quantify the hypothesis about expressions over all states allowed by the precondition, and as the postcondition we plug in the strongest postcondition for the assignment statement (which looks simpler than the usual SP of an assignment because of the choice to move preconditions to the surrounding logic).

Lemma compile_Assign e g ctx tmp:
  e ~ₑ g // ctx ->
  <{ ctx }>
    Assign tmp e
  <{ g | fun v tr ctx' =>
       tr = [] /\ ctx' = (tmp, v) :: ctx }>.e: Expr
g: string
ctx: Ctx
tmp: Var
e ~ₑ g // ctx ->
<{ ctx }> Assign tmp e <{ g
| fun (v : string) (tr : Trace) ctx' => tr = [] /\ ctx' = (tmp, v) :: ctx }>

And with these generalized pre-post pairs, we can now define a compilation lemma for bind, as well as a proper Skip lemma, both of which vexed us previously; this time the first program is compiled with an arbitrary postcondition, with will be resolved through unification as part of the compilation process; and the second program assumes this intermediate postcondition as its starting point and completes its run with a modified postcondition that appends the corresponding trace. Because this lemma does mention low-level effects, of course, we do need to mention the monad that we use to implement trace-modifying effects.

Lemma compile_Seq {α β} ctx post middle p1 p2 (s1: S α) (s2: α -> S β):
  <{ ctx }> p1 <{ s1 | middle }> ->
  (forall g1 tr1 ctx1, g1 = s1 -> middle g1 tr1 ctx1 ->
   let post' g2 tr2 := post (tr_bind g1 g2) (tr1 ++ tr2) in
   <{ ctx1 }> p2 <{ s2 g1.(val) | post' }>) ->
  <{ ctx }> Seq p1 p2 <{ bind s1 s2 | post }>.α, β: Type
ctx: Ctx
post: S β -> list string -> Ctx -> Prop
middle: S α -> Trace -> Ctx -> Prop
p1, p2: T
s1: S α
s2: α -> S β
<{ ctx }> p1 <{ s1 | middle }> ->
(forall (g1 : S α) (tr1 : Trace) ctx1,
 g1 = s1 ->
 middle g1 tr1 ctx1 ->
 let post' :=
   fun (g2 : S β) (tr2 : list string) => post (tr_bind g1 g2) (tr1 ++ tr2) in
 <{ ctx1 }> p2 <{ s2 (val g1) | post' }>) ->
<{ ctx }> Seq p1 p2 <{ v ← s1;
                       s2 v | post }>

Lemma compile_Skip g ctx post :
  post g [] ctx ->
  <{ ctx }> Skip <{ g | post }>.α: Type
g: α
ctx: Ctx
post: α -> Trace -> Ctx -> Prop
post g [] ctx -> <{ ctx }> Skip <{ g | post }>

Conditionals and loops can be handled similarly to sequences. For straightline code, we do not need to instantiate this “middle” clause explicitly: instead we can simply let it be derived by unification as part of compiling the first part of the sequence. For conditionals and for loops there is no free lunch, however, so we need to infer a predicate that captures the effect of both branches (for conditionals) or arbitrary repetitions (for loops). Luckily this inference problem is easier than it seems at first: specifically, we can pick the strongest postcondition, with carefully chosen heuristics and manipulations to ensure that we chose a postcondition that is readable and workable for the rest of the compilation process. The exact choice of heuristics is out of scope for this section, but we detail it later when we dive into the specifics of Rupicola ().

At this point, if we consider the case of a source program made of a sequence of let-bindings, we realize that the compilation process will now be an alternation of compile_Seq and specialized compilation lemmas, the former introducing cuts in the derivation and the latter refining the precondition of the program. Once we're done with all let-bindings (or monadic binds), we unify the final precondition that the compiler has derived with the postcondition that we were hoping to achieve.

It is because of this last step that we usually prefer to add an explicit continuation to each lemma, even though our new representation allows for a general cut lemma compile_Seq: making continuations explicit allows us to craft our intermediate postconditions very precisely as part of writing each lemma, instead of relying on unification. (Careful readers will have noticed the difficulty already popping up in a small way in compile_Assign above, which referred to a variable name tmp that we could not infer from goal, since we had already eliminated the corresponding let binding.) This makes the last unification step trivial in almost all cases. Here is what compile_Assign looks like in this style (using a wrapper blet — for “blocked let” — around let-bindings to prevent Coq from unfolding too aggressively without depending on a specific monad and bind + ret):

Lemma compile_Assign {α} ctx e g t (k: string -> α) tmp post:
  e ~ₑ g // ctx ->
  (forall v, v = g -> <{ (tmp, v) :: ctx }> t <{ k v | post }>) ->
  <{ ctx }> Seq (Assign tmp e) t <{ blet g k | post }>.α: Type
ctx: Ctx
e: Expr
g: string
t: T
k: string -> α
tmp: Var
post: α -> Trace -> Ctx -> Prop
e ~ₑ g // ctx ->
(forall v : string, v = g -> <{ (tmp, v) :: ctx }> t <{ k v | post }>) ->
<{ ctx }> Seq (Assign tmp e) t <{ blet g k | post }>
Proof. unfold triple; hammer. Qed.

This is the last step of our journey, and since our final compiler looks so similar to the previous iteration, we omit it for brevity; curious readers can consult the complete development for details.

Bibliography

[Cogent+Amani+ASPLOS2016]

Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. Cogent: verifying high-assurance file system implementations. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '16, 175–188. New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2872362.2872404, doi:10.1145/2872362.2872404.

[CertiCoq+Anand+CoqPL2017]

Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. CertiCoq: A verified compiler for Coq. In CoqPL'17: The Third International Workshop on Coq for PL. January 2017.

[VST+Appel+ESOP2011]

Andrew W. Appel. Verified software toolchain. In Proceedings of the 20th European Conference on Programming Languages and Systems: Part of the Joint European Conferences on Theory and Practice of Software, ESOP'11/ETAPS'11, 1–17. Berlin, Heidelberg, 2011. Springer-Verlag.

[ProofGeneral+Aspinall+ETAPS2000]

David Aspinall. Proof General: A generic tool for proof development. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, 38–42. 2000. doi:10.1007/3-540-46419-0\_3.

[Curve25519+Bernstein+PKC2006]

Daniel J. Bernstein. Curve25519: new diffie-hellman speed records. In Public Key Cryptography - PKC 2006, 9th International Conference on Theory and Practice of Public-Key Cryptography, New York, NY, USA, April 24-26, 2006, Proceedings, 207–228. 2006. URL: https://doi.org/10.1007/11745853\_14, doi:10.1007/11745853\_14.

[Koika+Bourgeat+PLDI2020]

Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Arvind. The essence of Bluespec: a core language for rule-based hardware design. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, 243–257. New York, NY, USA, 2020. Association for Computing Machinery. URL: https://pit-claudel.fr/clement/papers/koika-PLDI20.pdf, doi:10.1145/3385412.3385965.

[Idris+Brady+JFP2013]

Edwin C. Brady. Idris, a general-purpose dependently typed programming language: design and implementation. Journal of Functional Programming, 23(5):552–593, 2013. URL: https://doi.org/10.1017/S095679681300018X, doi:10.1017/S095679681300018X.

[Chajed+Perennial+SOSP2019]

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent, crash-safe systems with perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, 243–258. 2019. URL: https://doi.org/10.1145/3341301.3359632, doi:10.1145/3341301.3359632.

[OCamlFLambda+Chambart+Online2021]

Pierre Chambart, Mark Shinwell, Damien Doligez, and OCaml Contributors. Optimization with flambda. Feb 2016. URL: https://ocaml.org/manual/flambda.html.

[Charguéraud+CFML+ICFP2011]

Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, 418–430. 2011. URL: https://doi.org/10.1145/2034773.2034828, doi:10.1145/2034773.2034828.

[Bedrock+Chlipala+ICFP2013]

Adam Chlipala. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA - September 25 - 27, 2013, 391–402. 2013. doi:10.1145/2500365.2500592.

[Fiat+Chlipala+SNAPL2017]

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. The end of history? Using a proof assistant to replace language design with library design. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages (SNAPL 2017), volume 71 of Leibniz International Proceedings in Informatics (LIPIcs), 3:1–3:15. Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2017/7123/, doi:10.4230/LIPIcs.SNAPL.2017.3.

[Fiat+Delaware+SNAPL2017]

[Lean+deMoura+CADE2015]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, 378–388. 2015. URL: https://doi.org/10.1007/978-3-319-21401-6\_26, doi:10.1007/978-3-319-21401-6\_26.

[Fiat+Delaware+POPL2015]

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: deductive synthesis of abstract data types in a proof assistant. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '15, 689–700. ACM Press, 2015. URL: https://pit-claudel.fr/clement/papers/fiat-POPL15.pdf, doi:10.1145/2676726.2677006.

[Narcissus+Delaware+ICFP2019]

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proceedings of the ACM on Programming Languages, 3(ICFP):82:1–82:29, July 2019. URL: https://pit-claudel.fr/clement/papers/narcissus-ICFP19.pdf, doi:10.1145/3341686.

[EWD:EWD209]

Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967. URL: https://www.cs.utexas.edu/users/EWD/ewd02xx/EWD209.PDF.

[FiatCrypto+Erbsen+MIT2017]

Andres Erbsen. Crafting certified elliptic curve cryptography implementations in coq. Master's thesis, Massachusetts Institute of Technology, 2017. URL: https://dspace.mit.edu/handle/1721.1/112843.

[Lightbulb+Erbsen+PLDI2021]

Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. Integration verification across software and hardware for a simple embedded system. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 604–619. New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454065.

[FiatCrypto+Erbsen+IEEESP2019]

Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic - with proofs, without compromises. 2019 IEEE Symposium on Security and Privacy (SP), May 2019. URL: http://dx.doi.org/10.1109/sp.2019.00005, doi:10.1109/sp.2019.00005.

[CertifyingExtraction+Forster+ITP2019]

Yannick Forster and Fabian Kunze. A certifying extraction with time bounds from coq to call-by-value λ-calculus. In Interactive Theorem Proving - 10th International Conference, ITP 2019, Portland, USA, 17:1–17:19. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Apr 2019. Also available as arXiv:1904.11818.

[HOL+Gordon+Cambridge1993]

M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, USA, 1993. ISBN 0521441897.

[Greenaway_AK_12]

David Greenaway, June Andronick, and Gerwin Klein. Bridging the gap: automatic verified abstraction of C. In International Conference on Interactive Theorem Proving, ITP 2012, Princeton, NJ, USA, August 13-15, 2012, 99–115. 2012. doi:10.1007/978-3-642-32347-8\_8.

[DataRepresentationSynthesis+Hawkins+PLDI2011]

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, and Mooly Sagiv. Data representation synthesis. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, 38–49. 2011. doi:10.1145/1993498.1993504.

[CakeMLExtraction+Ho+IJCAR2018]

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, and Michael Norrish. Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. Lecture Notes in Computer Science, pages 646–662, 2018. doi:10.1007/978-3-319-94205-6\_42.

[Haskell+Hudak+HOPL2007]

Paul Hudak, John Hughes, Simon L. Peyton Jones, and Philip Wadler. A history of haskell: being lazy with class. In Proceedings of the Third ACM SIGPLAN History of Programming Languages Conference (HOPL-III), San Diego, California, USA, 9-10 June 2007, 1–55. 2007. URL: https://doi.org/10.1145/1238844.1238856, doi:10.1145/1238844.1238856.

[HOLCakeML+Hupel+ESOP2018]

Lars Hupel and Tobias Nipkow. A verified compiler from isabelle/hol to cakeml. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, 999–1026. 2018. URL: https://doi.org/10.1007/978-3-319-89884-1\_35, doi:10.1007/978-3-319-89884-1\_35.

[10.1007/978-3-642-28869-2_20]

Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating lr(1) parsers. In Helmut Seidl, editor, Programming Languages and Systems, 397–416. Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.

[ValidatingParsers+Jourdan+ESOP2012]

Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating lr(1) parsers. In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings, 397–416. Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.

[BinaryCodeExtraction+Kumar+ITP2109]

Ramana Kumar, Eric Mullen, Zachary Tatlock, and Magnus O. Myreen. Software verification with itps should use binary code extraction to reduce the TCB - (short paper). In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, 362–369. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8\_21, doi:10.1007/978-3-319-94821-8\_21.

[CakeML+Kumar+POPL2014]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. Cakeml: A verified implementation of ML. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, January 20-21, 2014, 179–192. 2014. doi:10.1145/2535838.2535841.

[ImperativeHOL+Lammich+ITP2015]

Peter Lammich. Refinement to Imperative/HOL. In International Conference on Interactive Theorem Proving, ITP 2015, Nanjing, China, August 24-27, 2015, 253–269. 2015. doi:10.1007/978-3-319-22102-1\_17.

[LLVMHOL+Lammich+ITP2019]

Peter Lammich. Generating verified LLVM from Isabelle/HOL. In International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, 22:1–22:19. 2019. doi:10.4230/LIPIcs.ITP.2019.22.

[Dafny+Leino+LPAR2010]

K. Rustan M. Leino. Dafny: an automatic program verifier for functional correctness. Logic for Programming, Artificial Intelligence, and Reasoning, pages 348–370, 2010.

[DafnyTriggers+CAV2016]

K. Rustan M. Leino and Clément Pit-Claudel. Trigger selection strategies to stabilize program verifiers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 361–381. Springer International Publishing, July 2016. URL: https://pit-claudel.fr/clement/papers/dafny-trigger-selection-CAV16.pdf, doi:10.1007/978-3-319-41528-4_20.

[Rhodium+Lerner+2005]

Sorin Lerner, Todd D. Millstein, Erika Rice, and Craig Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, 364–377. 2005. doi:10.1145/1040305.1040335.

[CompCert+Leroy+POPL2006]

Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, 42–54. 2006. doi:10.1145/1111037.1111042.

[CoqExtraction+Letouzey+TYPES2002]

Pierre Letouzey. A new extraction for coq. In International Workshop on Types for Proofs and Programs, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, 200–219. Springer Berlin Heidelberg, 2002. URL: http://dx.doi.org/10.1007/3-540-39185-1_12, doi:10.1007/3-540-39185-1_12.

[CertiCoqRewriteRules+Li+ICFP2021]

John M. Li and Andrew W. Appel. Deriving efficient program transformations from rewrite rules. Proc. ACM Program. Lang., August 2021. URL: https://doi.org/10.1145/3473579, doi:10.1145/3473579.

[HOLVerilog+Loow+FormaliSE2019]

Andreas Lööw and Magnus O. Myreen. A proof-producing translator for verilog development in HOL. In Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019, 99–108. 2019. URL: https://doi.org/10.1109/FormaliSE.2019.00020, doi:10.1109/FormaliSE.2019.00020.

[L_w_2021]

Andreas Lööw. Lutsig: a verified verilog compiler for verified circuit development. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2021. URL: http://dx.doi.org/10.1145/3437992.3439916, doi:10.1145/3437992.3439916.

[VerilogExtraction+Lööw+PLDI2019]

Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. Verified compilation on a verified processor. Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2019. URL: http://dx.doi.org/10.1145/3314221.3314622, doi:10.1145/3314221.3314622.

[DeductiveSynthesis+Manna+TOPLAS1980]

Zohar Manna and Richard J. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90–121, January 1980. doi:10.1145/357084.357090.

[MetaFStar+Martínez+ESOP2019]

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. Meta-F*: proof automation with SMT, tactics, and metaprograms. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, 30–59. Springer International Publishing, 2019. URL: https://pit-claudel.fr/clement/papers/meta-fstar-ESOP19.pdf, doi:10.1007/978-3-030-17184-1_2.

[Ladder+Montgomery+MC1987]

Peter L. Montgomery. Speeding the pollard and elliptic curve methods of factorization. Mathematics of Computation, 48(177):243–264, 1987. URL: http://dx.doi.org/10.1090/s0025-5718-1987-0866113-7, doi:10.1090/s0025-5718-1987-0866113-7.

[OEuf+Mullen+CPP2018]

Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman. Œuf: minimizing the coq extraction tcb. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, 172–185. New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167089, doi:10.1145/3167089.

[MyreenGS12]

Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. Decompilation into logic - improved. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012, 78–81. 2012. URL: https://ieeexplore.ieee.org/document/6462558/.

[CakeMLExtraction+Myreen+ICFP2012]

Magnus O. Myreen and Scott Owens. Proof-producing synthesis of ML from higher-order logic. In ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, Copenhagen, Denmark, September 9-15, 2012, 115–126. 2012. doi:10.1145/2364527.2364545.

[CakeMLExtraction+Myreen+JFP2014]

Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. Journal of Functional Programming, 24(2-3):284–315, Jan 2014. URL: http://dx.doi.org/10.1017/s0956796813000282, doi:10.1017/s0956796813000282.

[TranslationValidation+Necula+PLDI2000]

George C. Necula. Translation validation for an optimizing compiler. Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation - PLDI ’00, 2000. URL: http://dx.doi.org/10.1145/349299.349314, doi:10.1145/349299.349314.

[Cogent+OConnor+JFP2021]

Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele Keller. Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31:25, 2021. doi:10.1017/S095679682100023X.

[Cogent+OConnor+2016]

Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, and Gerwin Klein. COGENT: certified compilation for a functional systems language. CoRR, 2016. URL: https://arxiv.org/abs/1601.05520.

[CertiCoqCompositional+Paraskevopoulou+ICFP2021]

Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. Compositional optimizations for certicoq. Proc. ACM Program. Lang., August 2021. URL: https://doi.org/10.1145/3473591, doi:10.1145/3473591.

[MetaProgramming+Parreaux+EPFL2020]

Lionel Parreaux. Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages. PhD thesis, EPFL, Lausanne, 2020. URL: http://infoscience.epfl.ch/record/281735, doi:10.5075/epfl-thesis-10285.

[CoqExtraction+PaulinMohring+JSC1989]

Christine Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. Theses, Université Paris-Diderot - Paris VII, January 1989. URL: https://tel.archives-ouvertes.fr/tel-00431825.

[CoqMLSynthesis+PaulinMohring+JSC1993]

Christine Paulin-Mohring and Benjamin Werner. Synthesis of ml programs in the system coq. J. Symb. Comput., 15(5–6):607–640, May 1993. URL: https://doi.org/10.1016/S0747-7171(06)80007-6, doi:10.1016/S0747-7171(06)80007-6.

[FiatCrypto+Philipoom+MIT2018]

Jade Philipoom. Correct-by-construction finite field arithmetic in coq. Master's thesis, Massachusetts Institute of Technology, 2018. URL: https://dspace.mit.edu/handle/1721.1/119582.

[FiatToFacade+PitClaudel+MIT2016]

Clément Pit-Claudel. Compilation using correct-by-construction program synthesis. Master's thesis, Massachusetts Institute of Technology, August 2016. URL: http://pit-claudel.fr/clement/MSc/.

[Alectryon+PitClaudel+SLE2020]

Clément Pit-Claudel. Untangling mechanized proofs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, 155–174. New York, NY, USA, 2020. Association for Computing Machinery. URL: https://pit-claudel.fr/clement/papers/alectryon-SLE20.pdf, doi:10.1145/3426425.3426940.

[DSLs+PitClaudel+CoqPL2021]

Clément Pit-Claudel and Thomas Bourgeat. An experience report on writing usable DSLs in coq. In CoqPL'21: The Seventh International Workshop on Coq for PL. April 2021. URL: https://pit-claudel.fr/clement/papers/koika-dsl-CoqPL21.pdf.

[Cuttlesim+ASPLOS2021]

Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Adam Chlipala, and Arvind. Effective simulation and debugging for a high-level hardware language using software compilers. In Tim Sherwood, Emery Berger, and Christos Kozyrakis, editors, Proceedings of the Twenty-Sixth International Conference on Architectural Support for Programming Languages and Operating Systems, Virtual, April 19-23, 2021, ASPLOS 2021. Association for Computing Machinery, 2021. URL: https://pit-claudel.fr/clement/papers/cuttlesim-ASPLOS21.pdf.

[CompanyCoq+PitClaudel+CoqPL2016]

Clément Pit-Claudel and Pierre Courtieu. Company-Coq: taking Proof General one step closer to a real IDE. In CoqPL'16: The Second International Workshop on Coq for PL. January 2016. URL: https://hdl.handle.net/1721.1/101149, doi:10.5281/zenodo.44331.

[FiatToFacade+PitClaudel+IJCAR2020]

Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, and Adam Chlipala. Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, 119–137. Springer International Publishing, July 2020. URL: https://pit-claudel.fr/clement/papers/fiat-to-facade-IJCAR20.pdf, doi:10.1007/978-3-030-51054-1_7.

[TranslationValidation+Pnueli+TACAS1998]

A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Bernhard Steffen, editor, Tools and Algorithms for the Construction and Analysis of Systems - 4th International Conference, TACAS'98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98 Lisbon, Portugal, March 28 – April 4, 1998 Proceedings, 151–166. Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.

[MetaFunctors+Protzenko+2021]

Jonathan Protzenko and Son Ho. Zero-cost meta-programmed stateful functors in F. CoRR, 2021. URL: https://arxiv.org/abs/2102.01644, arXiv:2102.01644.

[EverCrypt+Protzenko+IEEESP2020]

Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cedric Fournet, and et al. Evercrypt: a fast, verified, cross-platform cryptographic provider. 2020 IEEE Symposium on Security and Privacy (SP), May 2020. URL: http://dx.doi.org/10.1109/sp40000.2020.00114, doi:10.1109/sp40000.2020.00114.

[Kremlin+Protzenko+ICFP2017]

Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified low-level programming embedded in F*. Proceedings of the ACM on Programming Languages, 1(ICFP):17:1–17:29, 2017. doi:10.1145/3110261.

[Perceus+Reinking+PLDI2021]

Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. Perceus: garbage free reference counting with reuse. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Jun 2021. URL: http://dx.doi.org/10.1145/3453483.3454032, doi:10.1145/3453483.3454032.

[SeparationLogic+Reynolds+LICS2002]

John C. Reynolds. Separation logic: A logic for shared mutable data structures. In IEEE Symposium on Logic in Computer Science, LICS 2002, 22-25 July 2002, Copenhagen, Denmark, 55–74. 2002. doi:10.1109/LICS.2002.1029817.

[NoAlias+Ritchie+CompLangC1988]

Dennis Ritchie. Noalias comments to x3j11. 1988. URL: https://usenetarchives.com/view.php?id=comp.lang.c&mid=PDc3NTNAYWxpY2UuVVVDUD4.

[Sewell+PLDI+PLDI2013]

Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16-19, 2013, 471–482. 2013. doi:10.1145/2491956.2462183.

[Solar-Lezama2009]

Armando Solar-Lezama. The sketching approach to program synthesis. In Asian Symposium on Programming Languages and Systems, APLAS 2009, Seoul, Korea, December 14-16, 2009, 4–13. 2009. doi:10.1007/978-3-642-10672-9\_3.

[SpectorZabusky+HS2Coq+CPP2018]

Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. Total haskell is reasonable coq. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, 14–27. 2018. URL: https://doi.org/10.1145/3167092, doi:10.1145/3167092.

[LXM+Steele+OOPSLA2021]

Guy L. Steele Jr. and Sebastiano Vigna. Lxm: better splittable pseudorandom number generators (and almost as fast). Proceedings of the ACM on Programming Languages, 5(OOPSLA):1–31, Oct 2021. URL: http://dx.doi.org/10.1145/3485525, doi:10.1145/3485525.

[CompCompPOPL15]

Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. Compositional CompCert. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, 275–287. 2015. doi:10.1145/2676726.2676985.

[FStar+Swamy+POPL2016]

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, 256–270. 2016. URL: https://doi.org/10.1145/2837614.2837655, doi:10.1145/2837614.2837655.

[Xcert+Tatlock+PLDI2010]

Zachary Tatlock and Sorin Lerner. Bringing extensibility to verified compilers. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, 111–121. 2010. doi:10.1145/1806596.1806611.

[Coq+Zenodo2021]

The Coq Development Team. The coq proof assistant. January 2021. URL: https://doi.org/10.5281/zenodo.4501022, doi:10.5281/zenodo.4501022.

[CoqRefMan+Zenodo2021]

The Coq Development Team. The Coq Proof Assistant: Reference Manual, version 8.13. January 2021. URL: https://doi.org/10.5281/zenodo.4501022, doi:10.5281/zenodo.4501022.

[Racket+TobinHochstadt+PLDI11]

Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. Languages as libraries. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, 132–141. 2011. doi:10.1145/1993498.1993514.

[LLVMTranslationValidation+Tristan+PLDI2011]

Jean-Baptiste Tristan, Paul Govereau, and Greg Morrisett. Evaluating value-graph translation validation for llvm. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, 295–305. New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/1993498.1993533, doi:10.1145/1993498.1993533.

[InstructionSchedulingValidation+Tristan+POPL2008]

Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: a case study on instruction scheduling optimizations. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, 17–27. New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1328438.1328444, doi:10.1145/1328438.1328444.

[CodeMotionVerification+Tristan+PLDI2009]

Jean-Baptiste Tristan and Xavier Leroy. Verified validation of lazy code motion. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '09, 316–326. New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1542476.1542512, doi:10.1145/1542476.1542512.

[ByteOrder+Tunney+Blog2021]

Justine Tunney. The byte order fiasco. 2021. URL: https://justine.lol/endian.html.

[Monads+Wadler+MSC1992]

Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, 1992. doi:10.1017/S0960129500001560.

[facade-tr]

Peng Wang. The Facade language. Technical Report, MIT CSAIL, 2016. URL: https://people.csail.mit.edu/wangpeng/facade-tr.pdf.

[Cito+Wang+OOPSLA2014]

Peng Wang, Santiago Cuellar, and Adam Chlipala. Compiler verification meets cross-language linking via data abstraction. In ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, 675–690. 2014. doi:10.1145/2660193.2660201.

[CertifiedSynthesis+Watanabe+2021]

Yasunari Watanabe, Kiran Gopinathan, George P\^ırlea, Nadia Polikarpova, and Ilya Sergey. Certifying the synthesis of heap-manipulating programs. Proc. ACM Program. Lang., August 2021. URL: https://doi.org/10.1145/3473589, doi:10.1145/3473589.

[ISOC+Yodaiken+PLOS2021]

Victor Yodaiken. How iso c became unusable for operating systems development. In Proceedings of the 11th Workshop on Programming Languages and Operating Systems, PLOS '21, 84–90. New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3477113.3487274, doi:10.1145/3477113.3487274.

[HELIX+Zaliva+CoqPL2019]

Vadim Zaliva and Matthieu Sozeau. Reification of shallow-embedded DSLs in coq with automated verification. In CoqPL'19: The Fifth International Workshop on Coq for PL. 2019.

[FiatMonitors+SETTA2018]

Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clément Pit-Claudel, Insup Lee, and Oleg Sokolsky. Correct-by-construction implementation of runtime monitors using stepwise refinement. In Xinyu Feng, Markus Müller-Olm, and Zijiang Yang, editors, Proceedings of the 4th International Symposium Dependable Software Engineering: Theories, Tools, and Applications - SETTA '18, 31–49. Springer International Publishing, 2018. URL: https://pit-claudel.fr/clement/papers/monitors-SETTA18.pdf, doi:10.1007/978-3-319-99933-3_3.

[CoqProlog+Zimmermann+TTT2017]

Théo Zimmermann and Hugo Herbelin. Coq's Prolog and application to defining semi-automatic tactics. In Type Theory Based Tools. Paris, France, January 2017. URL: https://hal.archives-ouvertes.fr/hal-01671994.

On relational compilation

A step by step example

Language definitions

Semantics

Compilation

Compiler correctness

Compiling with relations

Open-ended compilation