Relational compilation for end-to-end verification

1 Introduction

Vulnerabilities in critical systems fall into roughly two categories: logic mistakes (incorrect business logic) and programming mistakes (use-after-free, out-of-bounds accesses, etc.). High-level languages attempt to eliminate logic mistakes by promoting higher levels of abstraction that facilitate reasoning about program behavior, and they protect against low-level issues using static and dynamic checks and safer programming paradigms (garbage collection to rule out use-after-free errors, stream- and result-oriented APIs for out-of-bounds accesses, etc.).

At one extreme, purely functional languages offer very strong protections against low-level mistakes and readily lend themselves to mathematical reasoning. By eliminating arrays, exceptions, state, and other low-level concerns and encouraging higher-order programming, languages like Coq [Coq+Zenodo2021], Lean [Lean+deMoura+CADE2015], Idris [Idris+Brady+JFP2013], or the pure subsets of Haskell and F* [FStar+Swamy+POPL2016] [Haskell+Hudak+HOPL2007] offer programming models much less susceptible to the low-level issues that plague the vast majority of today's critical systems.

Unfortunately, this combination of flexibility and safety comes at a significant performance cost: it is an unsolved problem to program a compiler for any of these purely functional languages that verifiably preserves all of their high-level guarantees while offering performance competitive with the usual low-level suspects, especially C.

In fact, to ground this discussion of high-level inefficiencies, let us consider the simple task of converting an ASCII string str to uppercase, maybe as part of a network program that receives a request and normalizes its contents to use them as a key in a table of records.

In a purely functional language like Gallina (part of the Coq proof assistant), this task can be implemented succinctly as follows (with strings being linked list of characters, characters an inductive type with 256 cases, and toupper a switch with one case per lowercase letter):

String.map Char.toupper str

This program accurately captures the intent of the task, but how fast does it run? When extracted to OCaml, it will pointer-chase through a linked list to traverse the original string (creating data dependencies and cache pressure), create a fresh string (costing allocations, cache misses, and an extra traversal for garbage collection), and either stack-overflow on long strings (due to a non-tail-recursive map, though there have been recent developments in that space), or traverse the string twice (doubling allocation and pointer-chasing costs), or accumulate continuations (even more allocations).

In contrast, the low-level implementation below performs a single pass, occupies constant stack space, does not allocate, is cache-friendly, can be unrolled, and is trivially vectorizable (toupper on ASCII chars is just a comparison and a bitmask): it assumes that the original string is never reused, represents str as a contiguous array of characters, and mutates it with a simple for loop.

for (int i = 0; i < len; i++)
  str[i] = toupper(str[i]);

It is possible to see this low-level program as a transformation of the high-level one above, but only if we broadly generalize the way we think about compiler extensions.

Rethinking compiler extensions — The traditional extension point in a compiler is a single-language rewrite rule (e.g., in GHC Haskell), and much past research has studied compiler optimizations through the lens of term-rewriting systems. In fact, many compilers are implemented as sequences of lowering passes interleaved with optimization passes that operate on single languages. Unfortunately, single-language rewrite rules are poorly suited to the kind of cross-language transformations with potentially complex side conditions that would be needed to automatically generate the C program above from the Coq one preceding it.

Expressing the translation of String.map into for loop with mutation as a rewrite rule, for example, would require us either to encode mutation and for loops explicitly in the source language (so that the transformation could be performed within Gallina), or to extend C to support higher-order functions and folds (so that the transformation could be performed within C), or to use a generic compiler to lower folds into C and subsequently eliminate all the resulting cruft (including closures and a GC) using more rewrite rules. This expressivity issue, in addition to the fact that such transformations are often conditional on relatively complex side conditions that are best solved by user-provided partial decision procedures, makes rewrite rules poorly suited to our problem.

The aim of this thesis is to make it possible to build custom compilers that support complex cross-language optimizations, allowing users to translate the functional String.map program above into an efficient in-place loop. Such transformations are crucial to get good performance, easy to express for specific programs or domains, but either too narrow in scope or too complex to generalize to be a good fit for a general-purpose compiler.

A different kind of compiler — To realize this vision, this thesis describes a different approach to the compilation of functional programs. Its defining characteristic is that it trades completeness for performance: in my approach, users assemble custom compilers for specific programs or collections of programs, and as a result these compilers do not need to support the full complexity of the source language. By abandoning completeness, code patterns that would be complex and costly to compile in full generality (e.g. requiring garbage collection, closures, a runtime system, etc.) can be mapped to simple low-level constructs like loops and mutations by exploiting domain- or program- specific assumptions.

This vision is realized as a compiler-construction toolkit, Rupicola, implemented in the Coq proof assistant. In Rupicola, users assemble compilers by combining individual theorems that connect high-level patterns in Gallina (Coq's functional programming language) to low-level code fragments in Bedrock2 (a low-level imperative language developed at MIT [Lightbulb+Erbsen+PLDI2021]). So, for example, a Rupicola user may prove a theorem that translates all maps on lists into for loops that mutate arrays in place. Such an implementation choice is not applicable to all uses of maps and lists: it works only if mutation is acceptable (i.e. if the original list is not needed anymore after the map), and if the original code neither adds to nor removes from the list (these operations have no direct equivalent on a fixed-length array).

Rupicola is not intended to replace all program extraction. Instead, Rupicola is restricted, out of the box, to a minimal set of constructs (essentially arithmetic, simple data structures, and some control flow), yielding a predictable and transparent compilation process. Users are expected (and enabled) to extend it as needed for each new domain, plugging in domain- or program-specific compilation hints that capture the insight that humans would normally apply when manually implementing high-level specifications in a low-level language: details of memory layout and memory management, implementation strategies for data-structure traversals, etc.

shows where Rupicola fits in a complete pipeline from high-level specifications to assembly code.

Rupicola's target audience and use cases — Rupicola works best for small, performance-critical programs, where precise control over implementation choices and optimization is crucial — the kind of programs that experts write directly in C, to avoid the overheads introduced by traditional functional-programming compilers. In other words, Rupicola's user are intended to know what kind of low-level code they want, and Rupicola's task is to allow them to generate that code from functional models instead of writing it directly. Rupicola's value proposition, in this use case, is a combination of automation and ease of reasoning:

• Transformations that would be repeatedly applied by hand when manually implementing a low-level program from a high-level description are instead encoded a single time as compiler extensions, and subsequently applied many times across a range of related programs. Users pay a bit more upfront (they have to encode the transformation into a Rupicola plug-in) but reap the benefits down the line.

• Reasoning about the source programs becomes much simpler: since the source programs are valid Gallina code, proofs about these programs do not have to deal with the subtleties of low-level languages like mutation, complex control flow, or memory allocation. This makes verifying code from end to end much easier, because all program-specific reasoning and proofs happen on shallowly embedded purely functional programs, which are only then translated into efficient imperative code.

In a sense, Rupicola codifies and automates away the most unpleasant part of traditional end-to-end verification pipelines. In the traditional world, authors not willing to rely on Coq's extraction (for performance or trust reasons) will manually relate handwritten, deeply embedded low-level programs to functional models, and then they will separately relate each functional model to a high-level specification. In that world, authors must repeatedly deal with the complexities of the low-level language's semantics and with details such as when to allocate or free memory or how to relate low-level memory layouts to high-level functional models. Rupicola, in contrast, completely automates the first phase of this process, generating the deeply embedded low-level program from its functional model by leveraging user-provided hints and program annotations. In Rupicola, programmers only supply shallowly embedded programs written in a subset of Gallina that naturally maps to low-level constructs, and the tooling produces low-level, deeply embedded code. Unchanged is the second phase that relates these functional models to abstract specifications: that part is still the programmer's responsibility. [1] But because Rupicola's inputs are shallowly embedded, this phase is disconnected from the details of the low-level language's semantics, and the traditional reasoning patterns best supported by Coq — especially structural induction — are fully applicable.

2 Prelude: Interactive theorem proving and formal verification

The software artifacts that support this thesis are built within the Coq proof assistant. Coq is a venerable piece of software: its development started in 1984 [3], and has over time produced a powerful and versatile programming and verification environment.

At the core of Coq is a programming language called Gallina. It resembles traditional functional languages like SML, OCaml, F#; here, for example, is how one can define a Coq function that filters a list according to a predicate:

From Coq Require Import List.
Import ListNotations.

Fixpoint filter {α} (p: α -> bool) (l: list α) {struct l} :=
  match l with
  | [] => []
  | h :: t => let t' := filter p t in
              if p h then h :: t' else t'
  end.

A function defined in this way can be executed interactively using the Compute command:

Compute filter Nat.even [1; 2; 4; 13; 42; 139; 506].
= [2; 4; 42; 506]
: list nat

The same function can then be extracted — that is, translated — to other languages, including OCaml (this is the way most Coq programs are converted into executable binaries today):

From Coq Require Import Extraction ExtrOcamlBasic.
Extraction filter.
(** val filter : ('a1 -> bool) -> 'a1 list -> 'a1 list **)

let rec filter p = function
| [] -> []
| h :: t -> let t' = filter p t in if p h then h :: t' else t'

Beyond these superficial similarities, Coq diverges from traditional functional languages in multiple important ways — some theoretical and some practical. For the purposes of the discussion to follow, the following are the most relevant differences:

First, there are no effects in Coq: no mutable variables, no exceptions, no nondeterminism, no I/O and no control flow except for recursion and pattern matching. As a result, computations in Coq are very similar to mathematical computations: calling the same function twice with the same arguments always returns the same values.

Second, all programs written in Coq terminate (there are no unbounded loops, only well-founded recursion); hence Coq rejects the following incorrect program, for example:

Fixpoint filter {α} (p: α -> bool) (l: list α) {struct l} :=
  match l with
  | [] => []
  | h :: t =>
    let t' := filter p l in
    if p h then h :: t' else t'
  end.
Recursive definition of filter is ill-formed.
In environment
filter : forall α : Type, (α -> bool) -> list α -> list α
α : Type
p : α -> bool
l : list α
h : α
t : list α
Recursive call to filter has principal argument equal to 
"l" instead of "t".
Recursive definition is:
"fun (α : Type) (p : α -> bool) (l : list α) =>
 match l with
 | [] => []
 | h :: _ => let t' := filter α p l in if p h then h :: t' else t'
 end".

As a consequence, with a few exceptions irrelevant to this discussion, reduction strategies do not matter in Coq. This is important because computation is at the core of everything in Coq, and unlike most languages Coq supports partial evaluation, reduction under binders, and reduction with holes:

Eval cbv in filter ?[f] [1; 2].
= if ?f 1 then 1 :: (if ?f 2 then [2] else []) else if ?f 2 then [2] else []
: list nat
Eval simpl in (fun x => filter Nat.even [1; x; 4; 13; 42]).
= fun x : nat => if Nat.even x then [x; 4; 42] else [4; 42]
: nat -> list nat

Third, Coq has a particularly powerful type system, capable of capturing not just the simple types of OCaml, but also relations between types and values — in fact, Coq does not distinguish between types and values: the types of natural numbers and lists are defined by induction, but so are the types of logical disjunctions, existentially quantified propositions, or even equalities:

Print nat.
Inductive nat : Set :=  O : nat | S : nat -> nat
Print list.
Inductive list (A : Type) : Type :=  nil : list A | cons : A -> list A -> list A

Print or.
Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B
Print ex.
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    ex_intro : forall x : A, P x -> exists y, P y
Print "=".
Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

This allows Coq's language, Gallina, to be used not just for writing programs, but also for stating properties and proving them. For example, we can define predicates and prove theorems about the filter function above. The predicate contains below returns a mathematical proposition capturing whether a value is contained in a list:

Fixpoint contains {α} (l: list α) (x: α) : Prop :=
  match l with
  | [] => False
  | h :: t => h = x \/ contains t x
  end.

Proofs in Coq are simply values that inhabit a certain types: just like we can say that 5 has type nat (for natural numbers), we can say that Nat.add_comm has type forall n m: nat, n + m = m + n — and really what this means is that Nat.add_comm is a function that, given two numbers m and n, returns a proof (a value) of type n + m = m + n:

From Coq Require Import Arith.
Check Nat.add_comm.
Nat.add_comm
     : forall n m : nat, n + m = m + n

Here is a theorem about the filter function defined above. Its statement is a type, that of a function which given a function f, a list l, a value x, and a proof of type contains (filter f l) x, returns a proof that f x equals true:

Lemma f_if {A B} (f: A -> B) (b: bool) a a':
  f (if b then a else a') = if b then f a else f a'.
A, B: Type
f: A -> B
b: bool
a, a': A
f (if b then a else a') = (if b then f a else f a')
Proof. destruct b; reflexivity. Qed.

Theorem filter_sound {α} (f: α -> bool):
  forall l x, contains (filter f l) x -> f x = true.
α: Type
f: α -> bool
forall (l : list α) (x : α), contains (filter f l) x -> f x = true

Proofs in Coq are typically written using a meta-language that generates terms under the hood; this is called the tactic language. Coq is an interactive system: proofs are written step by step, and after each step the system displays the current state of the proof, a collection of open “goals”, which are secondary theorems that need to be proved to complete the main proof. Let us see a concrete example; in what follows the gray boxes indicate Coq's output, and the text without background is user input. [4]

Proof.

The Proof command begins the proof. Above the bar are the hypotheses that hold at this point in the proof. Below the bar is the goal, the theorem that we are trying to prove. Since the contains predicate is defined by induction on l, we follow that structure in the proof, using the induction command; this corresponds to distinguishing two cases in the proof: empty and non-empty lists.

  induction l.
α: Type
f: α -> bool
1
forall x : α, contains (filter f []) x -> f x = true
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
forall x : α, contains (filter f (a :: l)) x -> f x = true

We are now presented with two “subgoals” — two cases. In the first (1) the list l has been replaced by the empty list []; in the second the list is assumed to be non-empty, and l has been replaced by a cons of a newly introduced element a and a new list l.

The all: combinator below applies a tactic to all goals, and intros moves forall-quantified variables and premises of implications into the context as hypotheses:

  all: intros.
α: Type
f: α -> bool
x: α
H: contains (filter f []) x2
f x = true
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
H: contains (filter f (a :: l)) x
f x = true

The - below focuses the proof on the first subgoal. In that goal, hypothesis H: contains (filter f []) x (2) is contradictory, as filter f [] reduces to [], and contains [] x reduces to False; and indeed, using the simpl tactic to perform evaluation.:

  -
α: Type
f: α -> bool
x: α
H: contains (filter f []) x
f x = true simpl in H.
α: Type
f: α -> bool
x: α
H: False
f x = true

What H: False means is that hypothesis H has type False. In Coq False is defined as an empty inductive case, so H inhabiting the type False is inconsistent: case analysis on H completes this branch of the proof:

    destruct H.

The second goal is less simple; this time, simplification suggests two cases: f a = true and f a = false, so we can perform a case analysis on that value:

  -
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
H: contains (filter f (a :: l)) x
f x = true simpl in H.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
H: contains (if f a then a :: filter f l else filter f l) x
f x = true
    destruct (f a) eqn:Hf.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: contains (a :: filter f l) x
f x = true
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = false
H: contains (filter f l) x
f x = true

We find ourselves with two new subgoals: in the first f a is true (as indicated by Hf: f a = true) and filter f (a :: l) reduced to a :: filter f l; in the second f a is false (Hf: f a = false) and filter f (a :: l) reduced to filter f l. Further simplification will suggest one more case split, as contains (a :: filter f l) itself reduces to a disjunction: either a = x or x is in the result of filter f l.

    +
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: contains (a :: filter f l) x
f x = true simpl in H.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: a = x \/ contains (filter f l) x
f x = true
      destruct H.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: a = x
f x = true
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true3
x: α
Hf: f a = true
H: contains (filter f l) x
f x = true

In the first case a = x, and we are in the case in which f a is true; hence the goal holds:

      *
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: a = x
f x = true rewrite H in Hf.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f x = true
H: a = x
f x = true
        assumption.

In the second case we know by assumption that x is in (filter f l) (3), but also by induction that all x in (filter f l) satisfy f (3):

      *
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: contains (filter f l) x
f x = true apply IHl.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = true
H: contains (filter f l) x
contains (filter f l) x
        assumption.

Finally we read the case in which f a = false, and the induction hypothesis applies immediately:

    +
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = false
H: contains (filter f l) x
f x = true apply IHl.
α: Type
f: α -> bool
a: α
l: list α
IHl: forall x : α, contains (filter f l) x -> f x = true
x: α
Hf: f a = false
H: contains (filter f l) x
contains (filter f l) x assumption.

A satisfying Qed closes the proof:

Qed.

Under the hood tactic generate proof terms, and in fact it is possible to write proofs directly as plain Gallina programs. The result is seldom readable, however:

Fixpoint filter_complete {α} (f: α -> bool) l {struct l}:
  forall x, contains l x -> f x = true -> contains (filter f l) x :=
  match l return (forall x, contains l x -> f x = true ->
                  contains (filter f l) x) with
  | [] => fun x (H: False) _ => H
  | a :: l => fun x (Hc: a = x \/ contains l x) Hf =>
      match Hc with
      | or_introl Heq =>
        eq_rect_r
         (fun a => contains (if f a then a :: _ else _) x)
         (eq_rect_r (x := true)
            (fun b => contains (if b then x :: _ else _) x)
            (or_introl eq_refl) Hf)
         Heq
      | or_intror Hc =>
          if f a as b return (contains (if b then a :: _ else _) x)
          then or_intror (filter_complete f l x Hc Hf)
          else filter_complete f l x Hc Hf
      end
  end.

A final distinguishing characteristic of Coq is its support for advanced notations: unlike traditional languages, almost all the syntax of Coq is defined through extensions of its parser; later in this document we will use this to define special syntax for dictionaries, Hoare triples, function specifications, etc.

Coq proofs are usually written using specialized IDEs [ProofGeneral+Aspinall+ETAPS2000] [CompanyCoq+PitClaudel+CoqPL2016] that support showing Coq code side by side with the corresponding proof state.

For more information on the Coq proof assistant, readers can consult any of the books and tutorials listed at https://coq.inria.fr/documentation. In the rest of this document should be accessible to readers with limited Coq experience; the following chapters assume some Coq proficiency.

3 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. [5]

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.

Inductive S :=
| SInt z
| SOpp (s : S)
| SAdd (s1 s2 : S).

Inductive T_Op :=
| TPush z
| TPopSub
| TPopAdd.

Definition T := list T_Op.

Fixpoint σS s : Z :=
  match s with
  | SInt z     => z
  | SOpp s     => - σS s
  | SAdd s1 s2 => σS s1 + σS s2
  end.

 Notation Stack := (list Z).

 Definition σOp (ts: Stack) op : Stack :=
   match op, ts with
   | TPush n, ts => n :: ts
   | TPopAdd, n2::n1::ts => n1+n2 :: ts
   | TPopSub, n2::n1::ts => n1-n2 :: ts
   | _, ts => ts (* Invalid: no-op *)
   end.

Definition σT t (ts: Stack) : Stack :=
  List.fold_left σOp t ts.

Notation "t ∼ s" := (forall ts, σT t ts = σS s :: ts).

Fixpoint StoT s := match s with
  | SInt z     => [TPush z]
  | SOpp s     => [TPush 0] ++ StoT s ++ [TPopSub]
  | SAdd s1 s2 => StoT s1 ++ StoT s2 ++ [TPopAdd]
end.

Example s7 :=
  SAdd (SAdd (SInt 3) (SInt 6))
        (SOpp (SInt 2)).

Lemma StoT_Rok : forall s, StoT s ∼ s.
forall s, StoT s ∼ s
Proof.4
  induction s.
z: Z
StoT (SInt z) ∼ SInt z
s: S
IHs: StoT s ∼ s
StoT (SOpp s) ∼ SOpp s
s1, s2: S
IHs1: StoT s1 ∼ s1
IHs2: StoT s2 ∼ s2
StoT (SAdd s1 s2) ∼ SAdd s1 s2
  all: intros; unfold σT; simpl.
z: Z
ts: Stack
z :: ts = z :: ts
s: S
IHs: StoT s ∼ s
ts: Stack
fold_left σOp (StoT s ++ [TPopSub]) (0 :: ts) = - σS s :: ts
s1, s2: S
IHs1: StoT s1 ∼ s1
IHs2: StoT s2 ∼ s2
ts: Stack
fold_left σOp (StoT s1 ++ StoT s2 ++ [TPopAdd]) ts = σS s1 + σS s2 :: ts
  - (* `SInt` case *)
z: Z
ts: Stack
z :: ts = z :: ts
    reflexivity.
  - (* `SOpp` case *)
s: S
IHs: StoT s ∼ s
ts: Stack
fold_left σOp (StoT s ++ [TPopSub]) (0 :: ts) = - σS s :: ts
    rewrite fold_left_app.
s: S
IHs: StoT s ∼ s
ts: Stack
fold_left σOp [TPopSub] (fold_left σOp (StoT s) (0 :: ts)) = - σS s :: ts
    rewrite IHs.
s: S
IHs: StoT s ∼ s
ts: Stack
fold_left σOp [TPopSub] (σS s :: 0 :: ts) = - σS s :: ts
    reflexivity.
  - (* `SAdd` case *)
s1, s2: S
IHs1: StoT s1 ∼ s1
IHs2: StoT s2 ∼ s2
ts: Stack
fold_left σOp (StoT s1 ++ StoT s2 ++ [TPopAdd]) ts = σS s1 + σS s2 :: ts
    rewrite !fold_left_app.
s1, s2: S
IHs1: StoT s1 ∼ s1
IHs2: StoT s2 ∼ s2
ts: Stack
fold_left σOp [TPopAdd] (fold_left σOp (StoT s2) (fold_left σOp (StoT s1) ts)) =
σS s1 + σS s2 :: ts
    rewrite IHs1, IHs2.
s1, s2: S
IHs1: StoT s1 ∼ s1
IHs2: StoT s2 ∼ s2
ts: Stack
fold_left σOp [TPopAdd] (σS s2 :: σS s1 :: ts) = σS s1 + σS s2 :: ts
    reflexivity.
Qed.

Inductive StoT_rel : T -> S -> Prop :=
| StoT_RNat : forall z,
    [TPush z] ℜ SInt z
| StoT_ROpp : forall t s,
    t ℜ s ->
    [TPush 0] ++ t ++ [TPopSub] ℜ SOpp s
| StoT_RAdd : forall t1 s1 t2 s2,
    t1 ℜ s1 ->
    t2 ℜ s2 ->
    t1 ++ t2 ++ [TPopAdd] ℜ SAdd s1 s2
where "t 'ℜ' s" := (StoT_rel t s).

Theorem StoT_rel_ok : forall t s,
    t ℜ s -> t ∼ s.
forall t s, t ℜ s -> t ∼ s
Proof.5
  induction 1.
z: Z
[TPush z] ∼ SInt z
t: T
s: S
H: t ℜ s
IHStoT_rel: t ∼ s
[TPush 0] ++ t ++ [TPopSub] ∼ SOpp s
t1: T
s1: S
t2: T
s2: S
H: t1 ℜ s1
H0: t2 ℜ s2
IHStoT_rel1: t1 ∼ s1
IHStoT_rel2: t2 ∼ s2
t1 ++ t2 ++ [TPopAdd] ∼ SAdd s1 s2
  all: intros; unfold σT; simpl.
z: Z
ts: Stack
z :: ts = z :: ts
t: T
s: S
H: t ℜ s
IHStoT_rel: t ∼ s
ts: Stack
fold_left σOp (t ++ [TPopSub]) (0 :: ts) = - σS s :: ts
t1: T
s1: S
t2: T
s2: S
H: t1 ℜ s1
H0: t2 ℜ s2
IHStoT_rel1: t1 ∼ s1
IHStoT_rel2: t2 ∼ s2
ts: Stack
fold_left σOp (t1 ++ t2 ++ [TPopAdd]) ts = σS s1 + σS s2 :: ts
  - (* `StoT_RNat` case *)
z: Z
ts: Stack
z :: ts = z :: ts
    reflexivity.
  - (* `StoT_ROpp` case *)
t: T
s: S
H: t ℜ s
IHStoT_rel: t ∼ s
ts: Stack
fold_left σOp (t ++ [TPopSub]) (0 :: ts) = - σS s :: ts
    rewrite fold_left_app.
t: T
s: S
H: t ℜ s
IHStoT_rel: t ∼ s
ts: Stack
fold_left σOp [TPopSub] (fold_left σOp t (0 :: ts)) = - σS s :: ts
    rewrite IHStoT_rel.
t: T
s: S
H: t ℜ s
IHStoT_rel: t ∼ s
ts: Stack
fold_left σOp [TPopSub] (σS s :: 0 :: ts) = - σS s :: ts
    reflexivity.
  - (* `StoT_RAdd` case *)
t1: T
s1: S
t2: T
s2: S
H: t1 ℜ s1
H0: t2 ℜ s2
IHStoT_rel1: t1 ∼ s1
IHStoT_rel2: t2 ∼ s2
ts: Stack
fold_left σOp (t1 ++ t2 ++ [TPopAdd]) ts = σS s1 + σS s2 :: ts
    rewrite !fold_left_app.
t1: T
s1: S
t2: T
s2: S
H: t1 ℜ s1
H0: t2 ℜ s2
IHStoT_rel1: t1 ∼ s1
IHStoT_rel2: t2 ∼ s2
ts: Stack
fold_left σOp [TPopAdd] (fold_left σOp t2 (fold_left σOp t1 ts)) =
σS s1 + σS s2 :: ts
    rewrite IHStoT_rel1, IHStoT_rel2.
t1: T
s1: S
t2: T
s2: S
H: t1 ℜ s1
H0: t2 ℜ s2
IHStoT_rel1: t1 ∼ s1
IHStoT_rel2: t2 ∼ s2
ts: Stack
fold_left σOp [TPopAdd] (σS s2 :: σS s1 :: ts) = σS s1 + σS s2 :: ts
    reflexivity.
Qed.

Goal ([TPush 3] ++ [TPush 6] ++ [TPopAdd]) ++
     ([TPush 0] ++ [TPush 2] ++ [TPopSub]) ++
     [TPopAdd] ℜ
     SAdd (SAdd (SInt 3) (SInt 6))
     (SOpp (SInt 2)).
([TPush 3] ++ [TPush 6] ++ [TPopAdd]) ++
([TPush 0] ++ [TPush 2] ++ [TPopSub]) ++ [TPopAdd]
ℜ SAdd (SAdd (SInt 3) (SInt 6)) (SOpp (SInt 2))
Proof.
  apply StoT_RAdd.
[TPush 3] ++ [TPush 6] ++ [TPopAdd] ℜ SAdd (SInt 3) (SInt 6)
[TPush 0] ++ [TPush 2] ++ [TPopSub] ℜ SOpp (SInt 2)
  -
[TPush 3] ++ [TPush 6] ++ [TPopAdd] ℜ SAdd (SInt 3) (SInt 6) apply StoT_RAdd.
[TPush 3] ℜ SInt 3
[TPush 6] ℜ SInt 6
    +
[TPush 3] ℜ SInt 3 apply StoT_RNat.
    +
[TPush 6] ℜ SInt 6 apply StoT_RNat.
  -
[TPush 0] ++ [TPush 2] ++ [TPopSub] ℜ SOpp (SInt 2) apply StoT_ROpp.
[TPush 2] ℜ SInt 2
    +
[TPush 2] ℜ SInt 2 apply StoT_RNat.
Qed.

Example t7_rel: { t7 | t7 ℜ s7 }.
{t7 : T | t7 ℜ s7}
Proof.
  unfold s7; eexists.
?t7 ℜ SAdd (SAdd (SInt 3) (SInt 6)) (SOpp (SInt 2))

  apply StoT_RAdd.
?t1 ℜ SAdd (SInt 3) (SInt 6)
?t2 ℜ SOpp (SInt 2)

  -
?t1 ℜ SAdd (SInt 3) (SInt 6) apply StoT_RAdd.
?t1 ℜ SInt 3
?t20 ℜ SInt 6
    +
?t1 ℜ SInt 3 apply StoT_RNat.
    +
?t20 ℜ SInt 6 apply StoT_RNat.
  -
?t2 ℜ SOpp (SInt 2) apply StoT_ROpp.
?t ℜ SInt 2
    +
?t ℜ SInt 2 apply StoT_RNat.
Defined.

Compute t7_rel.
= exist [TPush 3; TPush 6; TPopAdd; TPush 0; TPush 2; TPopSub; TPopAdd]
: {t7 : T | t7 ℜ s7}

(exist ?t7)  apply StoT_RAdd.
(exist (?t1 ++ ?t2 ++ [TPopAdd]))  - apply StoT_RAdd.
(exist ((?t1 ++ ?t20 ++ [TPopAdd]) ++ ?t2 ++ [TPopAdd]))    + apply StoT_RNat.
(exist (([TPush 3] ++ ?t20 ++ [TPopAdd]) ++ ?t2 ++ [TPopAdd]))    + apply StoT_RNat.
(exist (([TPush 3] ++ [TPush 6] ++ [TPopAdd]) ++ ?t2 ++ [TPopAdd]))  - apply StoT_ROpp.
(exist
   (([TPush 3] ++ [TPush 6] ++ [TPopAdd]) ++
    ([TPush 0] ++ ?t ++ [TPopSub]) ++ [TPopAdd]))    + apply StoT_RNat.
(exist
   (([TPush 3] ++ [TPush 6] ++ [TPopAdd]) ++
    ([TPush 0] ++ [TPush 2] ++ [TPopSub]) ++ [TPopAdd]))

Create HintDb cc.
Hint Constructors StoT_rel : cc.

Example t7_rel_eauto: { t7 | t7 ℜ s7 }.
{t7 : T | t7 ℜ s7}
Proof. eauto with cc. Defined.

Compute t7_rel_eauto.
= exist [TPush 3; TPush 6; TPopAdd; TPush 0; TPush 2; TPopSub; TPopAdd]
: {t7 : T | t7 ℜ s7}

Eval cbn in type of (proj2_sig t7_rel_eauto).
= [TPush 3; TPush 6; TPopAdd; TPush 0; TPush 2; TPopSub; TPopAdd] ℜ s7
: Type

Lemma StoT_Int z :
    [TPush z] ∼ SInt z.
z: Z
[TPush z] ∼ SInt z

Lemma StoT_Opp t s :
    t ∼ s ->
    [TPush 0] ++ t ++ [TPopSub] ∼ SOpp s.
t: T
s: S
t ∼ s -> [TPush 0] ++ t ++ [TPopSub] ∼ SOpp s

Lemma StoT_Plus t1 s1 t2 s2 :
    t1 ∼ s1 ->
    t2 ∼ s2 ->
    t1 ++ t2 ++ [TPopAdd] ∼ SAdd s1 s2.
t1: T
s1: S
t2: T
s2: S
t1 ∼ s1 -> t2 ∼ s2 -> t1 ++ t2 ++ [TPopAdd] ∼ SAdd s1 s2

Create HintDb c.
Opaque σS σT.
Hint Resolve StoT_Int : c.
Hint Resolve StoT_Opp : c.
Hint Resolve StoT_Plus : c.

Example t7_fn_eauto: { t7 | t7 ∼ s7 }.
{t7 : T | t7 ∼ s7}
Proof. eauto with c. Defined.

Compute t7_fn_eauto.
= exist [TPush 3; TPush 6; TPopAdd; TPush 0; TPush 2; TPopSub; TPopAdd]
: {t7 : T | t7 ∼ s7}

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

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}

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)}

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

Section Interp.
  Variable Σ: string -> (list Z -> Z).6
  Variable R: list (string * Z).7

  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.

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

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

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

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

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

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

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)]}

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

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

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

?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)]".

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.

?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)]

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

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

?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)]

c1
circuit

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

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

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

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)]}

Create HintDb circuits.

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

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

  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.

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

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.

?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)]".

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

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

?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)]

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

  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]

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]

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.

  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

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.

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

  Context Σ R c z
          (Hadd: forall x y, Σ "add" [x; y] = x + y)
          (Hc: c ≋ z @ Σ // R).

  Derive c3 SuchThat (c3 ≋ z + z + z @ Σ // R) As c3ok.
Σ: string -> list Z -> Z
c: circuit
z: Z
Hadd: forall x y : Z, Σ "add" [x; y] = x + y
Hc: c ≋ z @ Σ // R
c3:= ?Goal: circuit
c3 ≋ z + z + z @ Σ // R
  Proof. compile with circuits. Qed.

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

  Hint Extern 2 => simple apply c3ok : circuits.

  Derive c6 SuchThat (c6 ≋ (z+z+z) + (z+z+z) @ Σ // R) As c6ok.
Σ: string -> list Z -> Z
c: circuit
z: Z
Hadd: forall x y : Z, Σ "add" [x; y] = x + y
Hc: c ≋ z @ Σ // R
c6:= ?Goal: circuit
c6 ≋ z + z + z + (z + z + z) @ Σ // R
  Proof. compile with circuits. Qed.

  Print c6.
c6 = Op "add" [c3; c3]
     : circuit

Lemma compile_lsl {Σ R} c1 g1 c2 g2:
  (forall x y, Σ "lsl" [x; y] = x << y) ->
  c1 ≋ g1 @ Σ // R -> c2 ≋ g2 @ Σ // R ->
  Op "lsl" [c1; c2] ≋ g1 << g2 @ Σ // R.
Σ: string -> list Z -> Z
c1: circuit
g1: Z
c2: circuit
g2: Z
(forall x y : Z, Σ "lsl" [x; y] = x << y) ->
c1 ≋ g1 @ Σ // R -> c2 ≋ g2 @ Σ // R -> Op "lsl" [c1; c2] ≋ g1 << g2 @ Σ // R
Proof. cbn; repeat intros ->; reflexivity. Qed.

Hint Extern 2 => simple apply compile_lsl; shelve : circuits.

Example Σ1 fn args := match fn, args with
  | "lsl", [z1; z2] => z1 << z2
  | _, _ => Σ0 fn args
end.

Derive c4 SuchThat (forall z, c4 ≋ z << 2 @ Σ1 // [("z", z)]) As c4ok.
c4:= ?Goal: circuit
forall z, c4 ≋ z << 2 @ Σ1 // [("z", z)]
Proof. compile with circuits. Qed.

Print c4.
c4 = Op "lsl" [Read "z"; Const 2]
     : circuit

Ltac assocv v ctx :=
  lazymatch ctx with
  | []             => fail
  | (?k, v) :: _    => k
  |       _ :: ?ctx => assocv v ctx
  | _ => let ctx := eval red in ctx in assocv v ctx
  end.

Compute assocv 14 [("x", 3); ("y", 14)].
= "y"
: string

Ltac instantiate_assoc_eq := match goal with
  | |- ?v = ?ctx.[?k] =>
    is_evar k; let k0 := assocv v ctx in unify k k0
end.

3 = [("x", 1); ("y", 3)].[?k]  instantiate_assoc_eq.
3 = [("x", 1); ("y", 3)].["y"]

Hint Extern 1 => instantiate_assoc_eq : circuits.

Derive cc2 SuchThat
  (forall x y, cc2 ≋ x + y @ Σ0 // [("x", x); ("y", y)])
As cc2ok.
cc2:= ?Goal: circuit
forall x y : Z, cc2 ≋ x + y @ Σ0 // [("x", x); ("y", y)] compile with circuits. Qed.

Print cc2.
cc2 = Op "add" [Read "x"; Read "y"]
     : circuit

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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 }>

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 }>