Compilation Using Correct-by-Construction Program Synthesis

At its core, Fiat is simply a collection of Coq tactics and lemmas to reason about the nondeterminism monad (Listing 4). Authors of Fiat programs mix purely functional Gallina code with values obtained through Fiat's Pick operation (which models the selection of a value satisfying an arbitrary predicate) to produce shallowly embedded programs and specifications. For example, a Fiat programmer might write a specification of the following form:

Definition approximate_fixpoint (f: ℝ → ℝ) (ε: ℝ) : Comp (ℝ * ℝ) ≜
  (** Compute an ε-approximate fixpoint ‘x’ of ‘f’
      and return the pair (x, f x) **)
  x ← {x | abs (f x - x) ≤ ε};
  ret (x, f x)

Library authors using Fiat are then free to define domain-specific combinators that desugar to uses of Pick and bind, while exposing a nicer syntax for a given domain. For example, one might define the following simple DSL:

Notation FIXPOINT f ≜ {x | f x = x}
Notation ARGMAX   f ≜ {x | ∀ y, f y ≤ f x}
Notation ARGMIN   f ≜ {x | ∀ y, f y ≥ f x}

Concretely, Fiat has been used to define DSLs for SQL-style queries, BNF-style grammars, and binary encoders (serialization routines); work is planned on using it to derive SMT-style checkers.

High level specifications are then refined, using domain-specific automation written in Ltac (Coq's tactic language), to produce efficient functional programs. This refinement step substitutes most uses of Pick with programs whose outputs satisfy the Pick condition (for example, one might refine {l' | sorted l' ∧ Permutation l l'} with ret (mergesort l)).

In most cases, the resulting programs are thus directly executable, deterministic Gallina programs, which can be extracted and executed using Coq's extraction mechanism and the standard OCaml compiler—this is the approach followed by the original Fiat paper (Delaware et al. 2015).

In more complex cases, however, it can also be useful to leave some Picks in the final program, thereby leaving responsibility for full refinement to later stages of the pipeline (this is discussed in more detail in the next chapter).

Bedrock is a fairly typical assembly language, extended with precise semantics that allow programmers to reason about assembly programs. Bedrock functions are specified using Hoare-style pre- and postconditions expressed in separation logic, and a linking theorem allows programmers to combine individual Bedrock functions into larger units. An example Bedrock program taken from Bedrock's current sources and described in a 2013 paper (Chlipala 2013), together with a specification and proof of correctness, is given below:

Definition swapS : spec ≜ SPEC("x", "y") reserving 2
  Al v, Al w,
  PRE [V]  V "x" ↪ v  ∗  V "y" ↪ w
  POST[_]  V "x" ↪ w  ∗  V "y" ↪ v.

Definition swap ≜ bmodule "swap" {{
  bfunction "swap" ("x", "y", "v", "w") [swapS]
    "v" ⤛ "x";
    "w" ⤛ "y";
    "x" ↞ "w";
    "y" ↞ "v";
    Return 0
  end
}}.

Theorem swapOk : moduleOk swap.
  vcgen; abstract sep_auto.
Qed.

Cito is a much-higher-level imperative language by Wang et al. (2014), featuring relatively straightforward imperative semantics and offering a compiler to Bedrock with a machine-checked proof of partial correctness. Cito's main strengths are its support for separate compilation and its handling of function calls: a Cito program can make either operational calls, which transfer control to a Cito method whose body is explicitly known, or axiomatic calls, which transfer control to a method described only in terms of input-output specifications. Such axiomatic calls are resolved at link time, by providing for each such call a concrete implementation verified to respect the input-output specifications that the source program relies on. The following code samples present an example of such an axiomatic specification for a logical left-shift operation, as well as a Cito program making an axiomatic call to this specification, assuming that the name Intrinsics.LSL points to it.

Definition lsl : AxiomaticSpec unit.
  refine {|
      PreCond  ≜ λ args ⇒
        ∃ x, args = [SCA _ x];
      PostCond ≜ λ args ret ⇒
        ∃ x, args = [(SCA _ x, None)] ∧
             ret = SCA _ ($2 ⊗ x)
    |}; crush_types.
Defined.

output ≜ DCall Intrinsics.LSL(input)

Facade, finally, shares almost all of Cito's syntax but exposes very different operational semantics. Using a collection of syntactic checks on input programs, Facade ensures that each heap-allocated structure is only pointed to by a single name and that no heap-allocated memory is leaked. This allows Facade to present to the user a simple interface to memory, as a collection of names and values. An inductive proof guarantees that injecting Facade's syntax into Cito yields a valid Cito program with equivalent partial-correctness semantics. An example Facade program is presented below:

offset ≜ 0
len ≜ List[W].length(lst)
max ≜ List[W].get(lst, offset)
While (offset < len)
  elem ≜ List[W].get(lst, offset)
  If elem > max Then
    max ≜ elem
  Else
    __
  EndIf
  offset ≜ offset + 1
EndWhile

The missing piece of this stack is a Fiat-to-Facade compiler: a procedure capable of producing, given a Fiat program, an equivalent Facade program¹. This translation should be correct and extensible: users should be able to inject their own domain-specific insight and suggest problem-specific optimizations.

Taken together, these challenges call for a new approach to compiler design: instead of implementing them as monolithic translation functions, we assemble domain-specific compilers from collections of small and specialized routines, each tasked with recognizing a particular pattern of the source language. The correctness of these routines need not be established, as they only drive the compilation process by contributing to an ongoing dialogue with the proof assistant: this ensures that mistakes in compilation routines cannot imperil the correctness of the final program.

This thesis describes a concrete, lightweight implementation of this new approach. We start by presenting some background and details (Section 2) about existing systems that we reuse. We then give an overview of our technique (Section 2), before describing it in full detail (Section 4), along with implementation notes (Section 5). We finish by presenting concrete results (Section 6) obtained using this technique, discussing alternative approaches and related work (Section 7), and concluding with directions for future work and final remarks.

Facade (Peng Wang 2016), the language that our compiler targets, is a recent extension of Cito (Wang et al. 2014) that facilitates reasoning about memory allocation by exposing a memory as a map of keys to values.

Facade programs are packaged in modules, augmented with various proofs to form compile units; each compile unit comprises a collection of possibly mutually recursive methods, along with exports (axiomatic specifications of these methods for use by the module's clients), imports (specifications of all external functions that the module's methods depend on), and various proofs used internally by the compiler. These proofs guarantee many facts about each method of the module (packaged as DFFun entries in the DFModule record, which lives within the CompileUnit record). A subset of these facts is summarized below:

1. Method arguments are not overwritten by direct assignments (ret_not_in_args, no_assign_to_args in DFacade.v's OperationalSpec).
2. Compiler-reserved names do not appear in method bodies, nor in method arguments or return variables (args_name_ok, ret_name_ok, syntax_ok in OperationalSpec).
3. Method arguments have unique names, no uninitialized variables are read, function calls have the right numbers of arguments, and the sum of the number of local variables and the depth of the function body is less than \(2^{32}\) (is_good_func).
4. The axiomatic specification of each method is refined by the operational semantic of its body (ops_refines_axs, whose actual definition is very close to that of ProgOk presented in section 4.1.6); this entails guaranteeing that the program is safe to run in initial conditions satisfying the method's axiomatic preconditions and that it then yields a return value permitted by the method's axiomatic postcondition. This also guarantees, as a side condition of safety, facts such as the following (SafeCallOp, SafeCallAx):
   • All functions that the method calls to are properly imported—that is, each axiomatic call to an external function should be to one of the functions listed in the module's imports.
   • Memory is never leaked by the input program: variables containing a reference to a block of heap-allocated memory are never on the left side of an assignment.

Most of these proofs (1, 2, 3) are reflective (Boutin 1997): each of them checks a decidable property of a Facade program or module, and the corresponding goals can thus be discharged by computation.

We start by defining Fiat states, using a structure called a Telescope. Fiat states are concise and convenient ways to connect the semantics of Fiat and Facade: instead of expressing the pre- and postconditions that a Facade program must satisfy as a pair of arbitrary propositions, we collect all this information in a single data structure. The Coq definition of a telescope is given below (av is a type describing low-level ADTs known to Bedrock):

Inductive Telescope (av: Type) : Type ≜
| Nil : Telescope av
| Cons : ∀ T (key: NameTag av T)
           (val: Comp T)
           (tail: T → Telescope av),
    Telescope av.

As this definition makes clear, Fiat states have interesting properties that Facade states do not possess (recall that Facade states are unordered collections mapping variable names to either machine words, or heap-allocated ADTs described by the type av):

• They allow nondeterminism in values by storing computations instead of actual values. For example, it is legal to write Cons `"k" (λ x ⇒ x > 1) Nil.
• They do not directly distinguish between heap- and stack-allocated values, nor restrict values to Bedrock types; instead, they attach a “name tag” (Section 4.1.2) to each binding.
• They capture dependencies between variables by introducing an explicit ordering between them, allowing later bindings to depend on the values taken by previous ones.

In a sense, Fiat states are hybrids between Fiat programs and Facade states. As we will later see, a Fiat state is essentially isomorphic to a monadic program with names attributed to some of the bindings; thus, just like a Fiat program describes a set of acceptable return values, a Fiat state describes a set of acceptable environments (collections of names and values)—or, in other words, a set of acceptable Facade states.

To make telescopes easier on the eyes, we denote the telescope Cons k v (λ w ⇒ t w) as ⟦ k ⇝ v as w ⟧ ∷ t w. Furthermore, when v is in the form ret v00 we write ⟦ k ↦ v00 as w ⟧ ∷ t w instead, and when the tail of the telescope does not depend on the bound variable w we omit the as clause: ⟦ k ↦ v ⟧ ∷ ….

Each binding in a telescope comes with a name tag:

Inductive NameTag av T ≜
| NTNone : NameTag av T
| NTSome (key: string) (H: FacadeWrapper (Value av) T) : NameTag av T.

This tag describes which name refers to the associated value and how the value is represented in terms of low-level Bedrock types. Tags can be either of the following two values:

• NTNone, in which case the binding is anonymous and is simply a convenient way of expressing a monadic Bind; we might write, for example, something like the following to describe the Fiat program x ← Any; ret x + x (inside telescopes, we abbreviate NTSome k _ by writing `k, and NTNone by stripping the arrow)

  ⟦ Any as x ⟧ ∷ ⟦ `"out" ↦ x + x ⟧ ∷ Nil

• NTSome, in which case the tag carries a name (as a string) and an instance of a type class describing how the associated value should be represented in terms of Bedrock types. This injection (a FacadeWrapper instance—section 4.1.3), is crucial to connect Fiat states to Facade states: it would be inconvenient to restrict Fiat programs to manipulating Bedrock types, but Facade programs have no knowledge of the complex types used at the Fiat level—instead, they think in terms of Facade's Value type, which allows either machine words (W) or low-level ADTs (encoded in a user-supplied type av):

  Inductive Value {av} ≜
  | SCA : W → Value
  | ADT : av → Value.

To give an intuition of why these name tags are important, we return briefly to the definition of Telescopes. As previously mentioned, each cons cell of a telescope contains a computation, and a tail represented as a function mapping values permitted by the head to telescopes. This is a mixed-embedding analogue of a monadic Bind, where the consing operation plays the deeply embedded role of the shallow monadic binding. For this analogy to hold, though, we need the tail function to be passed a value of precisely the type of the head. This essentially prevents us from storing in telescopes only the low-level representation of values: since telescope tails compute on Fiat-level types, we cannot pass them low-level Bedrock encoding of these types (even less so given that Bedrock's encoding collapses all types into a single sum type).

Injections from arbitrary Gallina types into low-level Bedrock types can be conveniently described by packaging them into instances of a FacadeWrapper type class (the importance of the injectivity requirement will become apparent when we discuss the relation used to connect Fiat and Facade states):

Class FacadeWrapper (WrappingType WrappedType: Type) ≜
{ wrap: WrappedType → WrappingType;
  wrap_inj: ∀ v v', wrap v = wrap v' → v = v' }.

The last missing element before we can connect Fiat and Facade states is a way to capture Facade's memory-tracking constraints: while Facade allows overwriting scalars and does not require them to be deallocated before returning control to the caller, it imposes much stronger restrictions on heap-allocated values. Accordingly, we define three relations on Facade states:

• SameADTs ensures that two Facade states have exactly the same heap-allocated variables:

  Definition SameADTs {av} m11 m22 ≜
    ∀ k v, MapsTo k (@ADT av v) m11 ↔
           MapsTo k (@ADT av v) m22.

• SameSCAs ensures that the scalar bindings of one Facade state are all present in a second Facade state:

  Definition SameSCAs {av} m11 m22 ≜
    ∀ k v, MapsTo k (@SCA av v) m11 →
           MapsTo k (@SCA av v) m22.

• WeakEq combines these two predicates:

  Definition WeakEq {av} m11 m22 ≜
    @SameADTs av m11 m22 ∧ @SameSCAs av m11 m22.

The preceding definitions are enough to give the details of the relation connecting Fiat and Facade states. The recursive SameValues predicate expresses the fact that a particular Facade state is allowed by a given Fiat state, augmented for convenience with an unordered collection of deterministic bindings (this unordered collection will prove useful to describe bindings that are unmodified throughout a program's execution):

Fixpoint SameValues {av} ext fmap (tenv: Telescope av) ≜
  match tenv with
  | Nil ⇒ WeakEq ext fmap
  | Cons T key val tail ⇒
    match key with
    | NTSome k _ ⇒
      match StringMap.find k fmap with
      | Some v ⇒ ∃ w, val ↝ w ∧
                      v = wrap w ∧
                      SameValues ext (StringMap.remove k fmap) (tail w)
      | None ⇒ ⊥
      end
    | NTNone ⇒ ∃ w, val ↝ w ∧
                    SameValues ext fmap (tail w)
    end
  end.

This relation expresses the following: a Facade state is related to a given Fiat state if there exists a sequence of nondeterministic choices such that all bindings of the Fiat telescope (augmented with the unordered collection of bindings) are exactly reflected in the Facade state, and any left-over bindings are only to stack-allocated values.

This ensures that:

• The Facade state's heap-allocated values are exactly the low-level encodings (“wrappings”) of the values found along one of the nondeterministic paths in the Fiat telescope augmented with the unordered collection ext.
• The Facade state's stack-allocated values are a superset of the low-level encodings (“wrappings”) of the values along the same nondeterministic path in the Fiat telescope augmented with ext.

Note how the injectivity requirement comes into play: all that we can learn from a SameValues instance is an equality between two wrapped values (v = wrap w, where v is extracted from fmap and thus is most often itself a wrap v00). To be able to substitute v00 for w, in the call to tail w, we need to be able to learn v00 = w from v = wrap w, i.e. from wrap v00 = wrap w; the other alternative being to require each telescope tail to be paired with a proof that the corresponding function is a morphism for the particular wrapping function used in the same cons cell (in other words, one could require the results returned by the tail function to depend only on the value of wrap v, regardless of the specific value of w\({}\)—which amounts to ∀ w w', wrap w = wrap w' → tail w = tail w').

We write fmap ≲ tenv ∪ ext to make developments more readable. The following examples show how SameValues behaves, starting with valid examples:

• ["x" ▹ 1] ∷ ["y" ▹ (1,1)] \(≲\)
  ⟦ `"y" ↦ (1,1) ⟧ ∪ ["x" ▹ 1]
• ["x" ▹ 1] ∷ ["y" ▹ (1,1)] \(≲\)
  ⟦ `"x" ↦ 1 ⟧ ∷ ⟦ `"y" ↦ (1,1) ⟧ ∪ ∅
• ["x" ▹ 1] ∷ ["y" ▹ (1,1)] \(≲\)
  ⟦ `"x" ⇝ Any as x ⟧ ∷ ⟦ `"y" ↦ (x,x) ⟧ ∪ ∅
• ["x" ▹ 1] ∷ ["y" ▹ (1,1)] ∷ ["z" ▹ 2] \(≲\)
  ⟦ `"x" ⇝ Any as x ⟧ ∷ ⟦ `"y" ↦ (x,x) ⟧ ∪ ∅
  (We lost track of the ["z" ▹ 2] binding; since 2 is a scalar, that is not an issue.)

On the other hand, here are some invalid examples:

• ["x" ▹ 1] \(\not\lesssim\)
  ⟦ `"y" ↦ (1,1) ⟧ ∪ ["x" ▹ 1]
  ("y" is missing; this is an issue because (1,1) is an instance of the pair ADT, not a scalar.)
• ["x" ▹ 1] ∷ ["y" ▹ (1,2)] \(\not\lesssim\)
  ⟦ `"x" ⇝ Any as x ⟧ ∷ ⟦ `"y" ↦ (x,x) ⟧ ∪ ∅
  (The value of "y" is not consistent with (x,x).)
• ["x" ▹ 1] ∷ ["y" ▹ (1,1)] ∷ ["z" ▹ (1,2)] \(\not\lesssim\)
  ⟦ `"x" ⇝ Any as x ⟧ ∷ ⟦ `"y" ↦ (x,x) ⟧ ∪ ∅
  (We lost track of the ["z" ▹ (1,2)] binding; since (1,2) is encoded as an ADT value, that is an issue.)

The SameValues relation can conveniently be used to define an equivalence relation on telescopes, TelEq:

Definition TelEq {A} ext (T11 T22: Telescope A) ≜
  ∀ st, st ≲ T11 ∪ ext ↔
        st ≲ T22 ∪ ext.

Due to this definition, any relation that only manipulates Fiat states through SameValues will automatically be a morphism for TelEq.

All of these definitions lead us to the final correctness condition that we base the synthesis process on. ProgOk summarizes the behavior of a Facade program in terms of two Fiat states initial_tstate and final_tstate both augmented with the same unordered collection of bindings ext:

Definition ProgOk {av} ext env prog
    (initial_tstate final_tstate: Telescope av) ≜
  ∀ initial_state: State av,
    (initial_state ≲ initial_tstate ∪ ext) →
    Safe env prog initial_state ∧
    ∀ final_state: State av,
      @RunsTo _ env prog initial_state final_state →
      (final_state ≲ final_tstate ∪ ext).

We write ⦃ t11 ⦄ prog ⦃ t22 ⦄ ∪ ⦃ ext ⦄ // env in code and in text, to mean ProgOk ext env prog t11 t22 (we usually omit env in text); this Hoare-triple notation captures the fact that running the program in any of the Facade states described by the precondition is safe and that, if the program terminates, it yields one of the states allowed by the postcondition. Additionally, this notation makes explicit the set of external methods that the program being refined may use (env).

The injection relation used to describe encodings of Fiat objects into Bedrock ADT values is transitive (injections from \(A\) to \(B\) and \(B\) to \(C\) can be composed to form an injection from \(A\) to \(C\)) and reflexive (the identity function injects a type in itself). These two properties allow us to define a large number of such injections: we inject simple types into Facade scalars (32-bit stack-allocated machine words) and more complex types into Bedrock's type of heap-allocated values.

Most injectivity proofs, when Fiat types conveniently line up with the Bedrock types in which they are encoded, are very simple. In some cases, however, the encoding is more complex: for example, encoding bounded numbers ({n | n < pow22 32}) as machine words entails proving unicity of comparison proofs (i.e. proving that any fact of the form a < b admits a single proof) or taking proof irrelevance as an axiom.

The WeakEq relation is transitive, reflexive, and is a morphism for equality of Facade states (which itself is defined in terms of bi-directional inclusion of the set of pairs of keys and values). Among many other properties, we prove that WeakEq is preserved by symmetric additions to and removals from both states and that various functions used by Facade on states, such as the one checking whether a given variable maps to an ADT value in a given state, are covariant morphism for weak equality of states.

The SameValues relation is a morphism for various relations (more precisely, if TelEq t11 t22 then st ≲ t11 ∪ ext ↔ st ≲ t22 ∪ ext for any st and ext; and if WeakEq st st' and WeakEq ext' ext then st ≲ t ∪ ext → st' ≲ t ∪ ext'). TelEq, on the other hand, is an equivalence relation on Fiat states. Properties of both of these relations are proven in CoreLemmas.v and ExtendedLemmas.v and used as building blocks in proofs of ProgOk statements. In particular, many proofs about SameValues connect the semantics of Fiat states to that of Facade programs; one of the most important such properties concerns Fiat's bind operation; this rule, demonstrated previously, allows us to translate Fiat's anonymous binds into named ones, as cons cells in telescopes:

Lemma SameValues_Fiat_Bind_TelEq :
  ∀ {av A B} (key: NameTag av B) compA compB tail ext,
    TelEq ext
          ⟦ key ⇝ (a ← compA; compB a) as ab ⟧ ∷ tail ab
          ⟦ compA as a ⟧ ∷ ⟦ key ⇝ compB a as ab ⟧ ∷ tail ab.
Proof.
  unfold TelEq; SameValues_Fiat_t.
Qed.

Most proofs of this type are discharged by a single tactic SameValues_Fiat_t, which unfolds SameValues and simplifies the resulting expressions using available information about the Facade state that SameValues is applied to.

Proofs about ProgOk are the most numerous. They fall roughly into four categories:

• Proofs about the semantics of ProgOk, such as ProgOk being a morphism for TelEq, various properties about allocating and forgetting about of scalars, and most importantly variants of the chomp rule (Figure 6):

  Lemma ProgOk_Chomp_Some :
    ∀ `{FacadeWrapper (Value av) A} env key value prog
      (tail11: A → Telescope av) (tail22: A → Telescope av) ext,
      key ∉ ext →
      (∀ v: A, value ↝ v →
               ⦃ tail11 v ⦄
                 prog
               ⦃ tail22 v ⦄ ∪ ⦃ [key ▹ wrap v] ∷ ext ⦄ // env) →
      ⦃ ⟦ `key ⇝ value as v ⟧ ∷ tail11 v ⦄
        prog
      ⦃ ⟦ `key ⇝ value as v ⟧ ∷ tail22 v ⦄ ∪ ⦃ ext ⦄ // env.

• Proofs about the connection between Fiat's monadic semantics and ProgOk itself, and most importantly the bind rule; thanks to ProgOk only manipulating telescopes through the SameValues relation, and thus being a morphism for TelEq, these proofs most often can be recast in terms of TelEq and SameValues — as is the case for the bind rule, which was listed above. This rule, phrased in terms of ProgOk, is shown in figure 7; but by proving that ProgOk is a morphism for telescope equality, we can simply use the setoid machinery (Sozeau 2009) to rewrite with the corresponding TelEq lemma, without materializing a ProgOk one.

• Proofs about the connection between Facade's operational semantics and ProgOk itself; these proofs are essentially recastings of Facade's operational semantics in terms of telescopes and seldom need to unfold the SameValues relation. One special subclass of these rules is call rules, which are important enough to deserve their own section (4.2.5); other ones include simple connections such as CompileRead:

  Lemma CompileRead:
    ∀ {av} name var (val: W) ext (tenv: Telescope av),
      name ∉ ext →
      NotInTelescope name tenv →
      MapsTo var (wrap val) ext →
      ∀ env,
      ⦃ tenv ⦄
        name ≜ var
      ⦃ ⟦ `name ↦ val as _ ⟧ ∷ tenv ⦄ ∪ ⦃ ext ⦄ // env.
  Proof.
    SameValues_Facade_t.
  Qed.

• Proofs of complex optimizations translating Gallina patterns into lower-level operations, such as our motivating example of translating folds into destructive iteration over mutable lists.

Most of these proofs are discharged using a single tactic SameValues_Facade_t; the last category, however, is often a combination of such automation and manual proofs of the most tricky parts of the optimization.

One particularly interesting class of proofs, and arguably one of the places where this new synthesis-based compilation technique shines, is call rules. Facade's semantics allow calls to axiomatically specified methods, guaranteeing that, as long as the method's preconditions are satisfied, the method's postconditions will hold in the post-call state.

This section describes how such calls are introduced in the compilation process.

Compilation tasks are phrased in terms of the ProgOk statement; that is, our main compilation tactic takes a goal whose consequent is a ProgOk and progressively compiles the postcondition by breaking it down into smaller subgoals of the same ProgOk form. At the very beginning, however, our goals are not exactly in ProgOk form: instead, they are in the form of a Σ-type (a pair of values in which the type of the second element depends on the value of the first one) whose first element is a program and whose second element is a proof that that program satisfies a proposition in the form of a ProgOk (possibly quantified by multiple input variables). The following is an example of such a goal:

{prog : Stmt &
 ∀ x y : W,
 ⦃ ⟦ `"x" ↦ x ⟧ ∷ ⟦ `"y" ↦ y ⟧ ∷ Nil ⦄
    prog
 ⦃ ⟦ `"out" ↦ x ⊕ y ⟧ ∷ Nil ⦄ ∪ ⦃ ∅ ⦄ // env}

Crucially, the existential is at the very top of the formula; our first step is to instantiate it with an existential variable whose context is essentially empty. We are thus forced to produce a single program, which may never depend on the values of intermediate variables introduced during compilation.

We start by implementing a basic tactic that perform minor cleanups: introducing variables if the goal is quantified, creating the synthesized program's existential variable if it has not yet been created, substituting equalities if any are present in the context, etc.

We then define simple tactics to handle basic Gallina constructs: conditionals, arithmetic, Boolean tests, and constants. These tactics mostly apply straightforward lemmas, but the arithmetic and conditionals ones do a bit of work to translate Gallina-level operations on machine words into Facade's operators. For simplicity, we do not produce complex Facade expressions; instead, we recursively break down compound arithmetic expressions. Concretely, this means that for (x + (y - 1)) we produce a temporary variable for y - 1 and then add it to x:

tmp ≜ y - 1
out ≜ x + tmp

Fortunately, the Facade compiler is smart enough to (essentially) optimize the temporary away.

The rest of our tactics mix more complex optimizations and compilation patterns with handling of Fiat's nondeterministic semantics:

• We transform uses of Fiat's bind operators into individual telescope cells, using the bind rule, as demonstrated in chapter 3.
• When the head bindings of the pre- and postconditions match we apply the chomp rule to simplify the synthesis goal. Similarly, when we can find matching bindings deep down in the pre- and postconditions, we also heuristically try to move them to the front to apply the chomp rule, using setoid rewriting.
• When we notice that one of the variables in the precondition is not used in the postcondition and we have access to a destructor for its Bedrock type, we deallocate it.
• When we see a fold or a map we apply the corresponding loop compilation rule, which we now describe in more detail.

Many of the programs that we compile involve folds over lists of values; additionally, in many cases, the list is not reused after iteration. This suggests the following optimization: instead of compiling fold_left as a recursive higher-order function then separately compiling the function being folded and finally combining both compiled implementations to implement the original loop, we can instead compile fold_left into a while loop (in a sense doing the analogue of tail call elimination) and then compile the folded function separately into a chunk of Facade code guaranteed to implement the behavior of the original function (except for the fact that the Facade implementation is required to mutate its input arguments). Since the while loop iterates over the source list destructively, the rule does not apply if the list is then reused later in the program (which, as a rough approximation, can be detected by looking for keys mapping to the list itself in the postcondition of the program being synthesized).

Figure 9 shows a deductive-style presentation of one of the loop compilation rules; the corresponding Coq code is a bit of a mouthful but still quite comprehensible (Listing 8). The generality of fold_left allows us to compile maps and reverses in the same way.

Lemma CompileLoop {N} :
∀ {A} `{FacadeWrapper (Value QsADTs.ADTValue) A}
  lst init vheadhead vtesttest vlstlst vretret fPop fEmpty fDealloc facadeLoopBody
  env (ext: StringMap.t (Value QsADTs.ADTValue)) tenv
  (f: Comp A → FiatWTuple N → Comp A),

  MapsTo fPop (Axiomatic Pop) env →
  MapsTo fEmpty (Axiomatic Empty) env →
  MapsTo fDealloc (Axiomatic Delete) env →

  PreconditionSet tenv ext [vheadhead; vtesttest; vlstlst; vretret] →

  (∀ head (acc: Comp A) (s: list (FiatWTuple N)),
      ⦃ ⟦ `vretret ⇝ acc ⟧ ∷ ⟦ `vheadhead ↦ head ⟧ ∷ tenv ⦄
        facadeLoopBody
      ⦃ ⟦ `vretret ⇝ (f acc head) ⟧ ∷ tenv ⦄
      ∪ ⦃ [vtesttest ▹ wrap false] ∷ [vlstlst ▹ wrap s] ∷ ext ⦄ // env) →

  ⦃ ⟦ `vretret ⇝ init ⟧ ∷ ⟦ `vlstlst ↦ lst ⟧ ∷ tenv ⦄
    is_empty ≜ fEmpty(seq)
    While (!is_empty)
        head ≜ fPop(seq)
        facadeLoopBody
        is_empty ≜ fEmpty(seq)
    EndWhile
    call fDealloc(vlstlst)
  ⦃ ⟦ `vretret ⇝ (fold_left f lst init) ⟧ ∷ tenv ⦄ ∪ ⦃ ext ⦄ // env.

Extensibility is one of the key aspects of our compilation strategy. We detail a number of simple ways in which the compiler's behaviors can be extended; in many cases, we make forward references to our benchmarks, in which more detailed examples are given.

• Intrinsics: instead of unfolding Gallina functions, we can prove them equivalent to low-level operations provided by Bedrock and compile them away. This is akin to using compiler intrinsics for better performance; it is demonstrated in the discussion of microbenchmarks (Section 6.1.4).
• Rewrites: It is often easy to apply rewrites to change the goal into a form that can be handled by existing tactics. For example, fold_right can be rewritten in terms of fold_left and rev. Here, too, we give a more detailed example as part of our microbenchmarks (Section 6.1.3).

• Arbitrary new rules: Compilation tactics are independent from each other; they can be ordered, but in general they tend to be specific enough to compose easily, without committing to a given ordering. The intuition is essentially that each tactic is predicated on sufficiently precise conditions that applying it should not lead into a dead end; thus we don't need backtracking, as we can simply add new tactics to handle new patterns.

  To make this task easier, we provide a number of helper tactics:

  • match_ProgOk recognizes a ProgOk goal and passes its individual components to a caller-supplied continuation.
  • may_alloc(var) checks whether a variable is already present in the precondition or if it can be created as a new variable (it helps prevent tactics from looping).
  • gensym(name) constructs a Gallina string not appearing in either the goal or the hypotheses. It uses name as the string's prefix and appends a number to it to guarantee uniqueness.
  • move_to_front(var) uses setoid rewriting to swap independent bindings and move a particular key to the front of a telescope.
  • compile_do_side_conditions handles a number of common side conditions, including ensuring that variable names do not collide, finding a pointer to a specific axiomatic specification in the current environment of imports, ensuring that a name does not appear in a telescope, etc.
  • call_tactic_after_moving_head_binding_to_separate_goal takes a compilation tactic and applies after introducing a carefully crafted intermediate state and running a number of sanity checks. This tactic, like other similar combinators, uses the lemma about Facade's sequencing semantics to introduce an intermediate program point. Applying these combinators properly is generally nontrivial; hence our earlier remarks (Section 4.2.5.3) about including such intermediate states in lemma statements instead.

  The discussion of Any in section 6.1 gives an example of such an extension.

Many of the aforementioned tactics suffer from one small drawback: they often introduce no-ops (Skip) in the final, compiled program. This is due to the way certain compilation lemmas are phrased: this commonly happens if a lemma introduces an intermediate state, which turns out to not be required. For example, a lemma about addition could break down compiling addition into three steps: placing the first argument into a variable a, the second one into a variable b, and finally assigning to the result the Facade sum of the two arguments. It could be, however, than at the particular point in compilation when the lemma is introduced these two variables a and b are already in context; in that case, by calling the lemma with the right parameters, the first two steps are no-ops.

Although later compilation stages are generally good at optimizing away these minor inefficiencies, it is aesthetically more pleasant to remove them before presenting the generated programs to users. For that purpose, we prove our own optimization, in the form of the following compilation rule (parts of its proof were developed by Peng Wang):

Lemma ProgOk_RemoveSkips {av} :
  ∀ (prog : Stmt) (pre post : Telescope av) ext env,
    ⦃ pre ⦄ prog ⦃ post ⦄ ∪ ⦃ ext ⦄ // env →
    ⦃ pre ⦄ RemoveSkips prog ⦃ post ⦄ ∪ ⦃ ext ⦄ // env.
Proof.
  unfold ProgOk; intros * ok ** sv; specialize (ok _ sv);
    intuition eauto using RemoveSkips_Safe, RemoveSkips_RunsTo.
Qed.

In this rule, RemoveSkips stands for the following simple recursive definition:

Definition Is_Skip : ∀ p, { p = Skip } + { p ≠ Skip }.
Proof. … Defined.

Fixpoint RemoveSkips (s: Stmt) ≜
  match s with
  | Skip ⇒ Skip
  | Seq a b ⇒ let a ≜ RemoveSkips a in
              let b ≜ RemoveSkips b in
                if (Is_Skip a) then b
                else if (Is_Skip b) then a
                else (Seq a b)
  | If c t f ⇒ If c (RemoveSkips t) (RemoveSkips f)
  | While c b ⇒ While c (RemoveSkips b)
  | Call r f args ⇒ Call r f args
  | Assign x v ⇒ Assign x v
  end.

Interestingly, this rule can be applied at any time: we apply it a single time, at the very beginning of compilation.

We start by introducing a learn(fact) tactic. This tactic, given a proof a fact, checks whether this fact has already been learnt; if it has, it throws an exception; otherwise, it records the learnt fact, adds it to the context, and returns successfully. Original versions of this tactic checked for a hypothesis of the same type, but this check turned out to be too costly. In its current form, the learn tactic doesn't exactly check whether a given fact is already known before recording it; instead, it checks (syntactically) whether that fact has already been recorded using the learn tactic, failing quickly in the common case where the very same proof has already been used. In practice, this means that learn may create duplicates of already-known facts, and that learn will accept to record syntactically different but intensionally equal facts. Its implementation is very simple:

Inductive Learnt {A: Type} (a: A) ≜
  | AlreadyKnown : Learnt a.

Ltac learn fact ≜
  lazymatch goal with
  | [ H: Learnt fact ⊢ _ ] ⇒
    fail 0 "fact" fact "has already been learnt"
  | _ ⇒ let type ≜ type of fact in
        lazymatch goal with
        | [ H: @Learnt type _ ⊢ _ ] ⇒
          fail 0 "fact" fact "of type" type "was already learnt through" H
        | _ ⇒ pose proof (AlreadyKnown fact); pose proof fact
        end
  end.

This learn tactic elegantly solves the usual issue of having to decide when to specialize a fact, if at all. In our case, it most commonly happens with ProgOk: we may know some instance of ProgOk, and that instance can be specialized to produce a facts about any pair of initial and final Facade states. If we specialize it with the wrong states, however, the goal will become unprovable. Using learn to instantiate a copy of that fact, on the other hand, ensures that we do not weaken an hypothesis, that we do make progress, and that we do not get into a loop, repeatedly learning the same instantiation of the ProgOk fact.

The learn tactic, therefore, is useful doing saturation proofs: we can collect a large number of facts before using bottom-up reasoning (Coq's eauto) to conclude a proof. In a sense, it allows us to implement customizable generalizations of Coq's intuition: tactics can use large numbers of patterns to enrich the context with individual facts before deferring to Coq's eauto once the context is saturated (i.e. no new facts can be learnt by applying the tactics rules).

This style of proofs is convenient in our case, because many proofs consist of nontrivial manipulations of telescopes; by learning many facts about e.g. variants of SameValues with bindings added to the telescope, to the Facade state, or to the extra collection of unordered bindings, we greatly simplify proofs and make many goals easier to discharge automatically.

This technique is inspired by trigger-based instantiation of quantifiers used in SMT solvers; many SMT solvers indeed allow users to annotate their quantifiers with patterns that drive the SMT solver, making it explicit when to learn specialized instances of a quantifier. Our tactics use a similar technique: nonlinear patterns in the branches of our match goal constructs are our generalized equivalents of triggers: they perform the same role of guiding the prover in its learning of facts derived by specializing quantified hypotheses and theorems (Moskal 2009, Dross et al. 2015).

The main entry point of the microbenchmark compiler is the local _compile tactic. It works by repeatedly calling into a collection of small tactics:

• start_compiling, which transforms the simplified notation into a synthesis goal whose head is ProgOk, creating the existential variable corresponding to the program being synthesized.
• subst, intros, and computes_to_inv, which clean up the goal to facilitate the operation of other tactics.
• compile_do_side_conditions, a previously described (Section 4.3.4) collection of decision procedures for commonly occurring side goals.
• _compile_rewrite_bind, _compile_chomp, and _compile_prepare_chomp, which transform telescopes to simplify ProgOk goals (also previously described in section 4.3.2).
• _compile_skip, _compile_map, _compile_fold, and _compile_if, which handle particular Gallina forms.
• compile_simple and compile_simple_inplace, which handle Boolean tests and arithmetic operations and select the right lemma based on the availability in the context of arguments of the operator being compiled.
• _compile_early_hook and _compile_late_hook, two aliases of fail that clients may later rebind using Ltac's dynamic binding semantics to alter the behavior of the compiler.
• _compile_mutation, as well as _compile_constructor and _compile_destructor, which handle certain function calls, allocations of new objects, and deallocations of objects present in the context—as long as corresponding external functions are available in the environment. These tactics are useful for illustration and experimentation purposes, though in most real-life cases writing custom mutation, allocation, and deallocation logic allows more flexibility in the specification of the Bedrock-level operations. More precisely, these tactics only work if one of the available external Bedrock functions is axiomatically specified in terms of the corresponding Gallina type and according to a very specific template. In most real-life cases, however, constructors, destructors, and mutators have more complex signatures, and their specifications tend to include special corner cases—thus requiring custom, individual call rules.

This section details the steps needed to teach the microbenchmark compiler about a new nondeterministic choice.

In many cases, implementing support for a new low-level primitive is not required to compile a new pattern; instead, we can transform the source program to re-express it in terms of constructs that we know how to handle.

For example, the default _compile tactic for microbenchmarks knows how to handle revmap (revmap is defined thus: revmap f s ≜ map f (rev s)) but not map (revmap is a special case of a left fold, in which accumulation is just consing to the head of an output list):

ParametricExtraction
  #vars      seq
  #program   ret (map (λ w ⇒ w ⊗ 2) seq)
  #arguments ⟦ `"seq" ↦ seq ⟧ ∷ Nil
  #env       env.
_compile.

⦃ ⟦ `"seq" ↦ seq ⟧ ∷ Nil ⦄
   ?p
⦃ ⟦ `"out" ↦ map (λ w ⇒ w ⊗ 2) seq ⟧ ∷ Nil ⦄ ∪ ⦃ ∅ ⦄ // env

We could prove a separate lemma for map, but it is just as simple to implement it as a rewrite:

Lemma map_as_revmap {A B} :
  ∀ ls (f: A → B), map f ls = revmap f (rev ls).
Proof.
  unfold revmap; setoid_rewrite rev_involutive; reflexivity.
Qed.

We can then prove a similar lemma for rev; once we extend _compile with these two extra tactics, compilation completes effortlessly:

seq' ≜ List[W].nil()
test ≜ List[W].empty?(seq)
While (test = $0)
    head ≜ List[W].pop(seq)
    call List[W].push(seq', head)
    test ≜ List[W].empty?(seq)
EndWhile
call List[W].delete(seq)
out ≜ List[W].nil()
test ≜ List[W].empty?(seq')
While (test = $0)
    head ≜ List[W].pop(seq')
    r ≜ 2
    head' ≜ head * r
    call List[W].push(out, head')
    test ≜ List[W].empty?(seq')
EndWhile
call List[W].delete(seq')

One last type of interesting extensions to the compilation chain is intrinsics. Many operations can be computed using Gallina alone but admit much faster low-level implementations. As an example, here is a Gallina program that checks whether a nibble (a machine word assumed to be \(<16\)) is a power of two (the call to simpl guarantees that Inb is fully expanded):

Definition nibble_power_of_two_p (w: W) ≜
  Eval simpl in bool2w (Inb w (map Word.natToWord [1; 2; 4; 8])).

One use of such a function might be as follows:

ParametricExtraction
  #vars      x
  #program   ret (nibble_power_of_two_p (x ⊕ 1))
  #arguments ⟦ `"x" ↦ x ⟧ ∷ Nil
  #env       env.

We can tell _compile to handle this function by unfolding it, by adding unfold nibble_power_of_two_p to _compile_early_hook:

Ltac _compile_early_hook ::= progress unfold nibble_power_of_two_p.

The resulting code, however, is rather inefficient:

r ≜ $1
l ≜ x + r
r ≜ $1
test ≜ l == r
If $1 == test Then
    out ≜ $1
Else
   r ≜ $1
   l ≜ x + r
   r ≜ $2
   test00 ≜ l == r
   If $1 == test00 Then
      out ≜ $1
   Else
      r ≜ $1
      l ≜ x + r
      r ≜ $4
      test11 ≜ l == r
      If $1 == test11 Then
         out ≜ $1
      Else
         r ≜ $1
         l ≜ x + r
         r ≜ $8
         test22 ≜ l == r
         If $1 == test22 Then
            out ≜ $1
         Else
            out ≜ $0
         EndIf
      EndIf
   EndIf
EndIf

Instead, we could choose to explicitly rely on an external implementation of the nibble_power_of_two_p function; it would then be the responsibility of the linker to ensure that such an implementation is available. For this, we extend the environment of imports env with an extra function (FacadeImplementationWW lifts a W → W function into an axiomatic specification):

("intrinsics", "nibble_pow2") ↦
Axiomatic (FacadeImplementationWW nibble_power_of_two_p)

The end result is much more succinct, and can be linked against a low-level implementation of nibble_power_of_two_p.

r ≜ $1
arg ≜ x + r
out ≜ intrinsics.nibble_pow22(arg)

The high-level specifications given in this experiment are expressed using a Fiat DSL for binary encoders, elaborated by members of the PLV group at MIT CSAIL. This DSL offers various encoding combinators, each of which takes an output stream (in our case, a list of bytes), a cache (void in our case), and a value to encode, and each of which returns a new copy of the output stream and cache, extended to include the newly encoded value. The sources thus have a very regular structure, made even more apparent by using notations to express the composition operator. This is convenient for compilation and for automatically deriving decoders, though we do not leverage that part of the binary encoders framework in this project.

Out of the box, Fiat's binary encoders library include combinators for encoding lists and numbers into streams of Booleans or bytes, as well as a number of more complex structures that we do not consider here. These combinators are chained together through the compose function, previously denoted as Then:

Definition compose E B
           (transformer : Transformer B)
           (encode11 : E → Comp (B * E))
           (encode22 : E → Comp (B * E)) ≜
  (λ e00 ⇒
    `(p, e11) ← encode11 e00;
    `(q, e22) ← encode22 e11;
    ret (transform p q, e22)).

Note that all of these definitions use Bedrock's dependent word type; we often abbreviate word 32 as W or W3232:

Inductive word : ℕ → Set ≜
| WO : word O
| WS : 𝔹 → ∀ n, word n → word (S n).

Though the original encoding specifications may be nondeterministic, we require the refined programs to be deterministic. Since encoding generally does not require complex data structures, nondeterminism does not provide significant advantages in this particular case.

After refinement, the original encoding programs are therefore deterministic: in theory, this means that we could use the traditional OCaml extractor to obtain binaries from these sources. Doing so, however, yields disappointing results: the extracted code is multiple thousands of lines long and prohibitively slow. This is due to multiple factors:

• The source programs manipulate the dependently type “machine word” data type. Extracting this type naively leads to bad performance and code bloat: in Fiat, operations on this type are specified by roundtripping in and out of unbounded integers, and bit manipulations are done using recursive functions over the individual bits. Instead, when the number of bits in a given word matches one of the native integer types available in the target language, one could hope to extract directly to simple integer types. Unfortunately, the OCaml extraction engine is not able to extract the word type nonuniformly, so that e.g. word 32 would be extracted to int32, and word 8 to char.
• The source programs produce output by explicitly reconstructing bytes from the data stored inside an input packet. For numbers, for example, this means using repeated division to extract individual bits and store them inside a value of type word. For strings, this means iterating over the characters of the string and then iterating over the bits of the representation of each character. This makes it easy to ensure that the source programs have proper semantics, but it is a performance nightmare.
• The source programs produce sequences of bytes, with no particular focus on efficiency: they append to the end of a list using direct concatenation (concretely, to push a single byte out, they use bytes ⧺ [new_byte]). Again, this makes the sources easy to read as a description of the serialization protocol, but it yields horrible performance if extracted directly. Instead, we would like to produce an uninterrupted chunk of machine memory as the output of the encoding process: if the source program produces [0x68; 0x65; 0x79; 0x20; 0x3A; 0x29], we really wish that output to be represented in memory as a contiguous array containing exactly these bytes. Thus mirroring the exact semantics of the source program into OCaml is undesirable, both for performance and for code complexity (we would have to write additional, unverified code to convert the list of bytes produced by our compiled programs into an OCaml array).
• The source programs manipulate explicit records containing the fields of the packet being serialized; this means that if we want to expose our code to, say, a C library, that library will have to construct a C struct for us, which we will then read values from. It would arguably be better, performance-wise, to receive each of these fields as parameters to the encoding function (additionally, it would be best to be easily interoperable with such C code, instead of having to massage the C data to be able to pass it to our extracted encoders). Thus, it would be best for users to have a say on the low-level representation of the data manipulated by these binary encoders.

Fortunately, we can fix each of these issues:

• We don't need to extract the word data type uniformly; instead, we can define separate instances of the FacadeWrapper type class, thereby encoding both bytes and 32-bit words into Facade scalars. Of course, using 32-bit scalars to represent 8-bit words is only correct as long as we don't do arithmetic on these words: the semantics of e.g. addition on 8-bit words are not the same as those on 32-bit words.
• If we choose the right machine representation for the data structures of the source programs, and if we choose the right machine-level representation of integers and strings, we can ensure that their in-memory layout will match the encoding used by the source program. Concretely, if the source program manipulates integers smaller than \(2^8\), we can choose as a wrapper a function that injects such numbers into 8-bit Bedrock words. With this, the code that takes such a number, extracts each bit using repeated division, and concatenates these bits to a Bedrock word can be compiled into code that copies the input number: since it is already represented at the machine level in exactly the way we wish to encode it, the encoding operation is a no-op. Similarly, if we ensure that strings are represented as contiguous arrays of chars, then encoding a string becomes essentially a memory copy from one array of chars to another.
• We can recognize the pattern that consists in appending a single byte to a list of bytes, and choose as a wrapper for list of bytes a function that injects that list of bytes into a contiguous stack of bytes. Then appending maps to the push operation of these stacks, providing a constant-time implementation of this otherwise linear-time operation.
• We are free to specify the form of the input to our encoders and decoders, and thus we can phrase the extraction problem so as to enforce that the program start with one argument variable per field in the original structure. Additionally, by carefully selecting the machine representation of each field, we can ensure easy interoperability with C code.

For this benchmark, we focus on using Fiat to implement the core parts of a process scheduler. We describe the operations that we want it to support in high-level terms, using a variant of a specification language that many programmers are familiar with: SQL. We argue that a process scheduler, the component of an operating system that manages the collection of processes by creating new process records, filtering processes by status, etc. is a good example of a system that has a clear and simple specification, amenable to automatic code generation, and yet is usually hand-written in a low-level language: although database engines provide good abstractions and solid performance for data-manipulating code, the abstraction costs that they introduce—both in terms of performance and in terms of memory footprint of their runtime systems—is too high to consider including one in an operating system kernel. This example is closely inspired by Hawkins et al. (2011).

Even the programs produced by the original release of Fiat, with its derivations producing efficient, verified OCaml code, were still unsuitable for this task: they were dependent on the OCaml runtime, and its garbage collector was a significant source of performance fluctuations in our original testing.

Our Fiat-to-Facade compiler removes the dependency on a garbage collector and compiles all the way down to lightweight assembly. In addition to being verified, the resulting code is fast, lightweight, and calls into hand-verified assembly implementations of the data structures that it uses to manage memory. Taken together, the pipeline is the first instance of a verified, extensible compilation system from high level specifications to assembly, supporting arbitrary delegation to separately verified data structures.

Though the original SQL-like DSL presented by \citeauthor{FiatPOPL15} is rather rich, we restrict ourselves to single-table queries: they are sufficient to demonstrate the main abilities of our framework. Indeed, the task of disentangling complex queries into simpler functional code manipulating complex data structures through function calls is mostly that of the refinement procedure that transforms Fiat specifications into Fiat programs. The Fiat-to-Facade domain-specific compiler, in other words, is only remotely aware of the complexity of the original queries: the code that it processes has a rather different shape from the original specifications and consists mostly of relatively simple combinations of calls to external data structures.

The concrete specifications that we refine and then compile are shown in listing 11. They are expressed in an SQL-like DSL offering combinators for insertion (Insert), enumeration (For), and filtering (Where). These notations desugar into uses of Pick, as explained in Delaware et al. (2015).

Definition SchedulerSpec : ADT _ ≜
  QueryADTRep SchedulerSchema {
    Def Init : rep ≜ empty,

    (** Insert a new process, failing if ‘new_pid’ already exists. *)
    Def Spawn (r : rep) (new_pid cpu state : Word) : rep * 𝔹 ≜
      Insert (<pid ∷ new_pid,
               state ∷ state,
               cpu ∷ cpu>)
        into r.Processes,

    (** Find processes by ‘state’ and return their PIDs. *)
    Def Enumerate (r : rep) (state : State) : rep * list W3232 ≜
      procs ← For (p in r.Processes)
              Where (p.state = state)
              Return (p.pid);
      ret (r, procs),

    (** Find a process by ‘id’ and return its CPU time. *)
    Def GetCPUTime (r : rep) (id : W3232) : rep * list W3232 ≜
      proc ← For (p in r.Processes)
             Where (p.pid = id)
             Return (p.cpu);
      ret (r, proc)
  }.

Each process has three attributes: a unique process ID, a state (either SLEEPING or RUNNING), and CPU time (indicating how long the process has been running for). Each of these attributes are machine words. For efficiency, the data structures that we use to store these processes should be indexed on process ids and on states: this would speed up the retrieval of processes by state and by id.

The derivations of the original Fiat paper produced deterministic programs interweaving list manipulations with access to key-value stores implemented using AVL trees. Optimization opportunities included choosing the right indexing strategy to speed up certain accesses and reordering list computations—the latter being made possible by the absence of ORDER BY clauses, permitting to produce results in any order.

To facilitate its exploration of indexing strategies, the original Fiat paper further introduced a Bag data type, specified in terms of basic multiset operations—essentially addition, deletion, retrieval, and enumeration. Standard-library data structures, including AVL trees, were then proven to conform to this specification, allowing one to phrase refinement theorems in terms of general bags and plug in nested AVL trees during concrete refinement runs.

Since then, the bag interface was rephrased, generalized, and lifted into a proper Fiat ADT: its methods are now Fiat computations, each producing a new copy of the ADT's internal state in addition to the method's results. To run our last experiment, we made sure that the refinement logic left uses of the Bag ADT unrefined; this allows refined programs to be expressed in terms of manipulations of a bag instance, without committing to a specific implementation of such a bag (instead, bag operations remain expressed as operations on collections of values). The rest of the optimization scripts, and in particular aspects of choosing proper indexing strategies and optimizing list computations, were unchanged.

(** Spawn *)
a ← bfind r (_, $id, _);
if length (snd a) = 0 then
  u ← binsert (fst a) [$id, $state, $cpu]
  ret (fst u, true)
else
  ret (fst a, false)

(** Enumerate *)
a ← bfind table ($state, _, _);
ret (fst a, revmap (λ x ⇒ GetAttribute x 0) (snd a))

(** GetCPUTime *)
a ← bfind table (_, $id, _);
ret (fst a, revmap (λ x ⇒ GetAttribute x 2) (snd a))

listing 12 shows the results of refining each of the Process Scheduler's three method specifications. These refined programs use methods of the bag ADT: bfind performs an efficient lookup, either by process state (first level of indexing) or by process ID (second level of indexing), and binsert adds a record to an existing collection.

These refined methods are almost enough to start extracting to Facade. Before doing so, however, we need to do the following:

• Enrich Facade's ADT type to represent database tuples and indexed collections of these tuples; this permits us to specify operations on these basic types which concrete, low-level implementations will have to satisfy. These new structures were hinted at in section 4.2.5.1.
• Decide on low-level representations of input and output values. This fundamentally comes down to the user's choices and preferences, since it amounts to choosing how to represent each of the types manipulated by the final program in terms of newly added and previously existing types available at the Bedrock level.
• Extend the guarantees obtained by extracting refined programs to the original specifications; this allows us to merge proofs of correctness obtained through refinement and compilation into a single proof which, once connected to the correctness proof of the Facade compiler, guarantees that the final binaries obey the original high-level specifications. This is a one-time proof, which applies uniformly to any refinement and extraction, uniformly in the choices of low-level data representations, contributed by Benjamin Delaware.
• Construct pre- and postconditions to drive the extraction of each method, by translating Fiat method signatures into telescopes. These specifications are to be exposed to low-level clients of the compiled Fiat ADT and are phrased in terms of low-level machine types. The corresponding Coq derivation is an elegant bit of dependently typed programming authored by Benjamin Delaware (ADT2CompileUnit.v), in which Fiat signatures are used to construct axiomatic specifications phrased in terms of ProgOk and of the various user-selected wrappers into machine types; these are the specifications that are fed to the extraction engine. This lifting of Fiat specifications into Bedrock specifications is unverified: it is hard to think of exactly what its specification should be, beyond its actual implementation. This is not much of an issue, however, since the output is simple and readily inspected, and most importantly since callers ultimately depend on the generated axiomatic specifications of the extracted programs.

The following paragraphs detail some of these points. Listings 13, 14, and 15 show the result of extracting the scheduler's methods.

snd ≜ Bag22[Tuple[W]].findSecond(rep, arg)
test ≜ List[Tuple[W]].empty?(snd)
If $1 == test Then
  v11 ≜ arg
  v22 ≜ arg11
  v33 ≜ arg00
  o11 ≜ $0
  o22 ≜ $1
  o33 ≜ $2
  vlen ≜ $3
  tup ≜ Tuple[W].new(vlen)
  call Tuple[W].set(tup, o11, v11)
  call Tuple[W].set(tup, o22, v22)
  call Tuple[W].set(tup, o33, v33)
  call Bag22[Tuple[W]].insert(rep, tup)
  tmp ≜ $0
  test00 ≜ List[Tuple[W]].empty?(snd)
  While (test00 = $0)
      head ≜ List[Tuple[W]].pop(snd)
      size ≜ $3
      call Tuple[W].delete(head, size)
      test00 ≜ List[Tuple[W]].empty?(snd)
  EndWhile
  call List[Tuple[W]].delete(snd)
  ret ≜ $1
Else
  tmp ≜ $0
  test00 ≜ List[Tuple[W]].empty?(snd)
  While (test00 = $0)
      head ≜ List[Tuple[W]].pop(snd)
      size ≜ $3
      call Tuple[W].delete(head, size)
      test00 ≜ List[Tuple[W]].empty?(snd)
  EndWhile
  call List[Tuple[W]].delete(snd)
  ret ≜ $0
EndIf

snd ≜ Bag22[Tuple[W]].findFirst(rep, arg)
ret ≜ List[W].new()
test ≜ List[Tuple[W]].empty?(snd)
While (test = $0)
    head ≜ List[Tuple[W]].pop(snd)
    pos ≜ $0
    head' ≜ Tuple[W].get(head, pos)
    size ≜ $3
    call Tuple[W].delete(head, size)
    call List[W].push(ret, head')
    test ≜ List[Tuple[W]].empty?(snd)
EndWhile
call List[Tuple[W]].delete(snd);

snd ≜ Bag22[Tuple[W]].findSecond(rep, arg)
ret ≜ List[W].new()
test ≜ List[Tuple[W]].empty?(snd)
While (test = $0)
    head ≜ List[Tuple[W]].pop(snd)
    pos ≜ $2
    head' ≜ Tuple[W].get(head, pos)
    size ≜ $3
    call Tuple[W].delete(head, size)
    call List[W].push(ret, head')
    test ≜ List[Tuple[W]].empty?(snd)
EndWhile
call List[Tuple[W]].delete(snd);