DeepAndShallowEmbeddings: comments

DeepAndShallowEmbeddings.v

@@ -28,6 +28,11 @@ Ltac simp := repeat (simplify; subst; propositional;
 
 (** * Basic concepts of shallow, deep, and mixed embeddings *)
 
+(* We often have many options for how to encode some sort of formal expression.
+ * The simplest way is to write it directly as a Gallina functional program,
+ * which Coq knows how to evaluate directly.  That style is called
+ * *shallow embedding*. *)
+
 Module SimpleShallow.
   Definition foo (x y : nat) : nat :=
     let u := x + y in
@@ -35,8 +40,13 @@ Module SimpleShallow.
     u + v.
 End SimpleShallow.
 
+(* Alternatively, we can do as we have been through most of the chapters: define
+ * inductive types of program syntax, along with semantics for syntax trees.
+ * That style is called *deep embedding*. *)
+
 Module SimpleDeep.
   Inductive exp :=
+  | Const (n : nat)
   | Var (x : var)
   | Plus (e1 e2 : exp)
   | Times (e1 e2 : exp)
@@ -49,6 +59,7 @@ Module SimpleDeep.
 
   Fixpoint interp (e : exp) (v : fmap var nat) : nat :=
     match e with
+    | Const n => n
     | Var x => v $! x
     | Plus e1 e2 => interp e1 v + interp e2 v
     | Times e1 e2 => interp e1 v * interp e2 v
@@ -56,6 +67,8 @@ Module SimpleDeep.
     end.
 End SimpleDeep.
 
+(* We defined function [foo] in shallow and deep styles, and it is easy to prove
+ * that the encodings are equivalent. *)
 Theorem shallow_to_deep : forall x y,
     SimpleShallow.foo x y = SimpleDeep.interp SimpleDeep.foo ($0 $+ ("x", x) $+ ("y", y)).
 Proof.
@@ -64,28 +77,43 @@ Proof.
   reflexivity.
 Qed.
 
+(* More interestingly, we can mix characteristics of the two styles.  To explain
+ * exactly how, it's important to introduce the distinction between the
+ * *metalanguage*, in which we do our proofs (e.g., Coq for us); and the
+ * *object language*, which we formalize explicitly (e.g., lambda calculus,
+ * simple imperative programs, ...).  With *higher-order abstract syntax*, we
+ * represent binders of the object language using the function types of the
+ * metalanguage. *)
 Module SimpleMixed.
   Inductive exp :=
   | Const (n : nat)
+  | Var (x : string)
   | Plus (e1 e2 : exp)
   | Times (e1 e2 : exp)
   | Let (e1 : exp) (e2 : nat -> exp).
+  (* Note a [Let] body is a *function* over the computed value attached to the
+   * variable being bound. *)
 
-  Definition foo (x y : nat) : exp :=
-    Let (Plus (Const x) (Const y))
-        (fun u => Let (Times (Const u) (Const y))
+  Definition foo : exp :=
+    Let (Plus (Var "x") (Var "y"))
+        (fun u => Let (Times (Const u) (Var "y"))
                       (fun v => Plus (Const u) (Const v))).
 
-  Fixpoint interp (e : exp) : nat :=
+  Fixpoint interp (e : exp) (v : fmap var nat) : nat :=
     match e with
+    | Var x => v $! x
     | Const n => n
-    | Plus e1 e2 => interp e1 + interp e2
-    | Times e1 e2 => interp e1 * interp e2
-    | Let e1 e2 => interp (e2 (interp e1))
+    | Plus e1 e2 => interp e1 v + interp e2 v
+    | Times e1 e2 => interp e1 v * interp e2 v
+    | Let e1 e2 => interp (e2 (interp e1 v)) v
     end.
 
+  (* We can even do useful transformations on such expressions within Gallina,
+   * as in this function to recursively simplify additions of 0 and
+   * multiplications by 1. *)
   Fixpoint reduce (e : exp) : exp :=
     match e with
+    | Var x => Var x
     | Const n => Const n
     | Plus e1 e2 =>
       let e1' := reduce e1 in
@@ -115,20 +143,24 @@ Module SimpleMixed.
       end
     end.
 
-  Compute (fun x => reduce (Let (Plus (Const 0) (Const 1)) (fun n => Times (Const n) (Const x)))).
+  (* This example shows simplification, even under binders. *)
+  Compute (reduce (Let (Plus (Const 0) (Const 1))
+                       (fun n => Let (Times (Var "x") (Const 2))
+                                     (fun m => Times (Const n) (Const m))))).
 
-  Theorem reduce_ok : forall e, interp (reduce e) = interp e.
+  (* The transformation is provably meaning-preserving. *)
+  Theorem reduce_ok : forall v e, interp (reduce e) v = interp e v.
   Proof.
     induct e; simplify;
     repeat match goal with
-           | [ H : _ = interp _ |- _ ] => rewrite <- H
+           | [ H : _ = interp _ _ |- _ ] => rewrite <- H
            | [ |- context[match ?E with _ => _ end] ] => cases E; simplify; subst; try linear_arithmetic
     end; eauto.
   Qed.
 End SimpleMixed.
 
 Theorem shallow_to_mixed : forall x y,
-    SimpleShallow.foo x y = SimpleMixed.interp (SimpleMixed.foo x y).
+    SimpleShallow.foo x y = SimpleMixed.interp SimpleMixed.foo ($0 $+ ("x", x) $+ ("y", y)).
 Proof.
   unfold SimpleShallow.foo.
   simplify.
@@ -138,9 +170,19 @@ Qed.
 
 (** * Shallow embedding of a language very similar to the one we used last chapter *)
 
-Module Shallow.
-  Definition cmd result := heap -> heap * result.
+(* With the basic terminology out of the way, let's see these ideas in action,
+ * to encode the sort of imperative language we studied in the previous
+ * chapter. *)
 
+Module Shallow.
+  (* As a shallow embedding, we can represent imperative programs as functional
+   * programs that manipulate heaps explicitly. *)
+  Definition cmd result := heap -> heap * result.
+  (* Parameter [result] gives the type of the value being computed by a
+   * command.  The command is a function taking the initial heap as input, and
+   * it returns a pair of the final heap and the command's result. *)
+
+  (* We can redefine Hoare triples over these functional programs. *)
   Definition hoare_triple (P : assertion) {result} (c : cmd result) (Q : result -> assertion) :=
     forall h, P h
               -> let (h', r) := c h in
@@ -149,6 +191,8 @@ Module Shallow.
   Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
     (hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
 
+  (* Standard rules of Hoare logic can be proved as lemmas.  For instance,
+   * here's the rule of consequence. *)
   Theorem consequence : forall P {result} (c : cmd result) Q
                                (P' : assertion) (Q' : _ -> assertion),
       hoare_triple P c Q
@@ -163,6 +207,9 @@ Module Shallow.
     auto.
   Qed.
 
+  (* However, the programs themselves look quite different from those we saw in
+   * the previous chapter.  This function computes the maximum among the first [i]
+   * cells of memory and the accumulator [acc]. *)
   Fixpoint array_max (i acc : nat) : cmd nat :=
     fun h =>
       match i with
@@ -172,6 +219,8 @@ Module Shallow.
         array_max i' (max h_i' acc) h
       end.
 
+  (* We can prove its correctness via preconditions and postconditions. *)
+
   Lemma array_max_ok' : forall len i acc,
     {{ h ~> forall j, i <= j < len -> h $! j <= acc }}
       array_max i acc
@@ -203,6 +252,7 @@ Module Shallow.
     auto.
   Qed.
 
+  (* We can also run the program on concrete inputs. *)
   Example run_array_max0 : array_max 4 0 h0 = (h0, 8).
   Proof.
     unfold h0.
@@ -210,6 +260,9 @@ Module Shallow.
     reflexivity.
   Qed.
 
+  (* One more example in the same style: increment each of the first [i] cells
+   * of memory. *)
+
   Fixpoint increment_all (i : nat) : cmd unit :=
     fun h =>
       match i with
@@ -262,6 +315,14 @@ End Shallow.
 
 (** * A basic deep embedding *)
 
+(* One disadvantage of the last style of programs is computational efficiency:
+ * real CPU architectures don't manipulate memory as functional maps that are
+ * passed around, and the abstraction gap between our code and CPUs prevents us
+ * from taking maximum advantage of the hardware to achieve good performance.
+ * To help regain that efficiency, let's do a deep embedding of the language.
+ * Actually, it's a mixed embedding, with no explicit concept of variables,
+ * using higher-order abstract syntax to represent binders. *)
+
 Module Deep.
   Inductive cmd : Set -> Type :=
   | Return {result : Set} (r : result) : cmd result
@@ -269,6 +330,9 @@ Module Deep.
   | Read (a : nat) : cmd nat
   | Write (a v : nat) : cmd unit.
 
+  (* These constructors are most easily explained through examples.  We'll
+   * translate both of the programs from the shallowly embedding above. *)
+
   Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
 
   Fixpoint array_max (i acc : nat) : cmd nat :=
@@ -288,6 +352,11 @@ Module Deep.
       increment_all i'
     end.
 
+  (* Note how this is truly a mixed encoding: we freely use Gallina constructs
+   * like [match], mixed in with instructions specific to the object language,
+   * like reading or writing memory.  An interpreter explains what it all means,
+   * reducing programs to their original type from the shallow embedding. *)
+
   Fixpoint interp {result} (c : cmd result) (h : heap) : heap * result :=
     match c with
     | Return r => (h, r)
@@ -313,13 +382,18 @@ Module Deep.
     maps_equal.
   Qed.
 
+  (* This time, we define a Hoare-triple relation syntactically. *)
   Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop :=
   | HtReturn : forall P {result : Set} (v : result),
       hoare_triple P (Return v) (fun r h => P h /\ r = v)
+
   | HtBind : forall P {result' result} (c1 : cmd result') (c2 : result' -> cmd result) Q R,
       hoare_triple P c1 Q
       -> (forall r, hoare_triple (Q r) (c2 r) R)
       -> hoare_triple P (Bind c1 c2) R
+    (* Interesting thing about this rule: the second premise uses nested
+     * universal quantification over all possible results of the first command. *)
+
   | HtRead : forall P a,
       hoare_triple P (Read a) (fun r h => P h /\ r = h $! a)
   | HtWrite : forall P a v,
@@ -339,6 +413,8 @@ Module Deep.
     eapply HtConsequence; eauto.
   Qed.
 
+  (* Here are a few tactics, whose details we won't explain, but which
+   * streamline the individual program proofs below. *)
   Ltac basic := apply HtReturn || eapply HtRead || eapply HtWrite.
   Ltac step0 := basic || eapply HtBind || (eapply HtStrengthen; [ basic | ]).
   Ltac step := step0; simp.
@@ -398,6 +474,8 @@ Module Deep.
     auto.
   Qed.
 
+  (* It's easy to prove the syntactic Hoare-triple relation sound with
+   * respect to the semantic one from the shallow embedding. *)
   Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q,
       hoare_triple P c Q
       -> forall h, P h
@@ -415,6 +493,13 @@ Module Deep.
     eauto.
   Qed.
 
+  (* We use Coq's *extraction* feature to produce OCaml versions of our deeply
+   * embedded programs.  Then we can run them using OCaml intepreters, which are
+   * able to take advantage of the side effects built into OCaml, as a
+   * performance optimization.  This command generates file "Deep.ml", which can
+   * be loaded along with "DeepInterp.ml" to run the generated code.  Note how
+   * the latter file uses OCaml's built-in mutable hash-table type for efficient
+   * representation of program memories. *)
   Extraction "Deep.ml" array_max increment_all.
 End Deep.
 
@@ -422,9 +507,17 @@ End Deep.
 (** * A slightly fancier deep embedding, adding unbounded loops *)
 
 Module Deeper.
+  (* All programs in the last embedding must terminate, but let's add loops with
+   * the potential to run forever, which takes us beyond what is representable
+   * in the shallow embedding, since Gallina enforces terminating of all
+   * programs. *)
+
+  (* We use this type to represent the outcome of a single loop iteration.
+   * These are functional loops, where we successively modify an accumulator
+   * value across iterations. *)
   Inductive loop_outcome acc :=
-  | Done (a : acc)
-  | Again (a : acc).
+  | Done (a : acc)  (* The loop finished, and here is the final accumulator. *)
+  | Again (a : acc) (* Keep looping, with this new accumulator. *).
 
   Inductive cmd : Set -> Type :=
   | Return {result : Set} (r : result) : cmd result
@@ -433,9 +526,12 @@ Module Deeper.
   | Write (a v : nat) : cmd unit
   | Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc.
 
+  (* Again, it's all easier to explain with an example. *)
+
   Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
   Notation "'for' x := i 'loop' c1 'done'" := (Loop i (fun x => c1)) (right associativity, at level 80).
 
+  (* This program finds the first occurrence in memory of value [needle]. *)
   Definition index_of (needle : nat) : cmd nat :=
     for i := 0 loop
       h_i <- Read i;
@@ -445,6 +541,10 @@ Module Deeper.
         Return (Again (S i))
     done.
 
+  (* Next, we write a single-stepping interpreter for this language.  We can
+   * know longer write a straightforward big-stepping interpeter, as programs of
+   * the object language can diverge, while Gallina enforces termination. *)
+
   Inductive stepResult (result : Set) :=
   | Answer (r : result)
   | Stepped (h : heap) (c : cmd result). 
@@ -500,9 +600,13 @@ Module Deeper.
       -> (forall r h, Q r h -> Q' r h)
       -> hoare_triple P' c Q'
 
-  | HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) I,
+  | HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc))
+                    (I : loop_outcome acc -> assertion),
       (forall acc, hoare_triple (I (Again acc)) (body acc) I)
       -> hoare_triple (I (Again init)) (Loop init body) (fun r h => I (Done r) h).
+  (* The loop rule contains a tricky new kind of invariant, parameterized on the
+   * current loop state: either [Done] for a finished loop or [Again] for a loop
+   * still in progress. *)
 
   Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
     (hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
@@ -533,6 +637,9 @@ Module Deeper.
   Ltac use_IH H := conseq; [ apply H | .. ]; ht.
   Ltac loop_inv Inv := eapply HtConsequence; [ apply HtLoop with (I := Inv) | .. ]; ht.
 
+  (* We prove our [index_of] example correct, relying crucially on a tactic
+   * [loop_inv] to prove a loop by giving its loop invariant, which, recall, is
+   * parameterized on a [loop_outcome]. *)
   Theorem index_of_ok : forall hinit needle,
     {{ h ~> h = hinit }}
       index_of needle
@@ -545,18 +652,24 @@ Module Deeper.
                          /\ match r with
                             | Done r' => hinit $! r' = needle
                                          /\ forall i, i < r' -> hinit $! i <> needle
-                                          | Again r' => forall i, i < r' -> hinit $! i <> needle
+                            | Again r' => forall i, i < r' -> hinit $! i <> needle
                             end).
     cases (r ==n needle); ht.
     cases (i ==n acc); simp.
     apply H3 with (i0 := i); auto.
   Qed.
 
+  (* The single-stepping interpreter forms the basis for defining transition
+   * systems from commands. *)
   Definition trsys_of {result} (c : cmd result) (h : heap) := {|
     Initial := {(c, h)};
     Step := fun p1 p2 => step (fst p1) (snd p1) = Stepped (snd p2) (fst p2)
   |}.
 
+  (* We now prove soundness of [hoare_triple], starting from a number of
+   * inversion lemmas for it, collapsing the potential effects of many nested
+   * rule-of-consequence applications. *)
+
   Lemma invert_Return : forall {result : Set} (r : result) P Q,
     hoare_triple P (Return r) Q
     -> forall h, P h -> Q r h.
@@ -581,6 +694,10 @@ Module Deeper.
     auto.
   Qed.
 
+  (* Highly technical point: in some of the inductions below, we wind up needing
+   * to show that the cases for [Read] and [Write] can never overlap, which
+   * would imply that they have the same result types, which would mean that the
+   * types [unit] and [nat] are equal. *)
   Lemma unit_not_nat : unit = nat -> False.
   Proof.
     simplify.
@@ -675,6 +792,9 @@ Module Deeper.
     eauto.
   Qed.
 
+  (* Clever choice of strengthened invariant here: intermediate commands are
+   * checked against degenerate preconditions that force equality to the current
+   * heap, and the postcondition is preserved across all steps. *)
   Lemma hoare_triple_sound' : forall P {result} (c : cmd result) Q,
       hoare_triple P c Q
       -> forall h, P h
@@ -698,6 +818,7 @@ Module Deeper.
     auto.
   Qed.
 
+  (* Proving: if we reach a [Return] state, the postcondition holds. *)
   Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q,
       hoare_triple P c Q
       -> forall h, P h
@@ -721,6 +842,11 @@ End Deeper.
 
 (** * Adding the possibility of program failure *)
 
+(* Let's model another effect that can be implemented using native OCaml
+ * features.  We'll add a very basic form of exceptions, namely just one
+ * (uncatchable) exception, for program failure.  We'll prove, by the end, that
+ * verified programs never throw the exception. *)
+
 Module DeeperWithFail.
   Inductive loop_outcome acc :=
   | Done (a : acc)
@@ -737,6 +863,8 @@ Module DeeperWithFail.
   Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
   Notation "'for' x := i 'loop' c1 'done'" := (Loop i (fun x => c1)) (right associativity, at level 80).
 
+  (* This program loops forever, maintaining a tally in memory address 0.
+   * We periodically test that address, failing if it's ever found to be 0. *)
   Definition forever : cmd nat :=
     _ <- Write 0 1;
     for i := 1 loop
@@ -750,6 +878,8 @@ Module DeeperWithFail.
       end
     done.
 
+  (* We adapt our single-stepper with a new result kind, for failure. *)
+
   Inductive stepResult (result : Set) :=
   | Answer (r : result)
   | Stepped (h : heap) (c : cmd result)
@@ -812,6 +942,8 @@ Module DeeperWithFail.
 
   | HtFail : forall {result},
       hoare_triple (fun _ => False) (Fail (result := result)) (fun _ _ => False).
+    (* The rule for [Fail] simply enforces that this command can't be reachable,
+     * since it gets an unsatisfiable precondition. *)
 
   Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
     (hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
@@ -841,7 +973,6 @@ Module DeeperWithFail.
   Ltac ht := simp; repeat step.
   Ltac conseq := simplify; eapply HtConsequence.
   Ltac use_IH H := conseq; [ apply H | .. ]; ht.
-  Ltac use_lemma H := eapply HtWeaken; [ apply H | .. ]; ht.
   Ltac loop_inv0 Inv := (eapply HtWeaken; [ apply HtLoop with (I := Inv) | .. ])
                         || (eapply HtConsequence; [ apply HtLoop with (I := Inv) | .. ]).
   Ltac loop_inv Inv := loop_inv0 Inv; ht.
@@ -864,6 +995,8 @@ Module DeeperWithFail.
     Step := fun p1 p2 => step (fst p1) (snd p1) = Stepped (snd p2) (fst p2)
   |}.
 
+  (* Next, we adapt the proof of soundness from before. *)
+
   Lemma invert_Return : forall {result : Set} (r : result) P Q,
     hoare_triple P (Return r) Q
     -> forall h, P h -> Q r h.
@@ -1035,6 +1168,12 @@ Module DeeperWithFail.
   (** ** Showcasing the opportunity to create new programming abstractions,
        * without modifying the language definition *)
 
+  (* Here's an example of a new programming construct defined within Gallina,
+   * without extending the definition of object-language syntax.  It's for
+   * folding a command over every one of the first [len] cells in memory.  We
+   * work with some accumulator type [A], initializing the accumulator to [init]
+   * and calling [combine] to update the accumulator for each value we read out
+   * of memory. *)
   Definition heapfold {A : Set} (init : A) (combine : A -> nat -> cmd A) (len : nat) : cmd A :=
     p <- for p := (0, init) loop
            if len <=? fst p then
@@ -1046,6 +1185,8 @@ Module DeeperWithFail.
          done;
     Return (snd p).
 
+  (* Next, two pretty mundane facts about list operations. *)
+
   Lemma firstn_nochange : forall A (ls : list A) n,
       length ls <= n
       -> firstn n ls = ls.
@@ -1076,6 +1217,8 @@ Module DeeperWithFail.
 
   Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic.
 
+  (* Here's the soundness theorem for [heapfold], relying on a hypothesis of
+   * soundness for [combine]. *)
   Theorem heapfold_ok : forall {A : Set} (init : A) combine
                                (ls : list nat) (f : A -> nat -> A),
     (forall P v acc,
@@ -1094,21 +1237,23 @@ Module DeeperWithFail.
                             | Again (i, acc) => acc = fold_left f (firstn i ls) init
                             end).
     cases (length ls <=? a); ht.
-    use_lemma (H (fun h => (forall i, i < Datatypes.length ls -> h $! i = nth_default 0 ls i)
-                           /\ b = fold_left f (firstn a ls) init
-                           /\ r = h $! a)).
+    apply H.
     simp; auto.
     simp.
-    rewrite H1 by assumption.
+    rewrite H2 by assumption.
     simplify.
     reflexivity.
     simp; auto.
     simp.
   Qed.
 
+  (* Here's a concrete use of [heapfold], to implement [array_max] more
+   * succinctly. *)
   Definition array_max (len : nat) : cmd nat :=
     heapfold 0 (fun n m => Return (max n m)) len.
 
+  (* Next, some more lemmas about lists and arithmetic *)
+
   Lemma le_max' : forall v ls acc,
       v <= acc
       -> v <= fold_left max ls acc.
@@ -1133,6 +1278,8 @@ Module DeeperWithFail.
 
   Hint Resolve le_max.
 
+  (* Finally, a short proof of [array_max], appealing mostly to the generic
+   * proof of [heapfold] *)
   Theorem array_max_ok : forall ls : list nat,
     {{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}}
       array_max (length ls)