Commented ProgramDerivation, with chapter renumbering in Coq code

ConcurrentSeparationLogic.v

@@ -1,5 +1,5 @@
 (** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
-  * Chapter 17: Concurrent Separation Logic
+  * Chapter 18: Concurrent Separation Logic
   * Author: Adam Chlipala
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
 

MessagesAndRefinement.v

@@ -1,5 +1,5 @@
 (** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
-  * Chapter 18: Process Algebra and Behavioral Refinement
+  * Chapter 19: Process Algebra and Behavioral Refinement
   * Author: Adam Chlipala
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
 

ProgramDerivation.v

@@ -4,7 +4,7 @@
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/
   * Some material borrowed from Fiat <http://plv.csail.mit.edu/fiat/> *)
 
-Require Import FrapWithoutSets.
+Require Import Frap.
 Require Import Program Setoids.Setoid Classes.RelationClasses Classes.Morphisms Morphisms_Prop.
 Require Import Eqdep.
 
@@ -14,17 +14,49 @@ Ltac inv_pair :=
   end.
 
 
+(* We have generally focused so far on proving that programs meet
+ * specifications.  What if we could generate programs from their
+ * specifications, in ways that guarantee correctness?  Let's explore that
+ * direction, in the tradition of *program derivation* via
+ * *stepwise refinement*. *)
+
+
 (** * The computation monad *)
 
-Definition comp (A : Type) := A -> Prop.
+(* One counterintuitive design choice will be to represent specifications and
+ * implementations in the same "language," which is essentially Gallina with the
+ * added ability to pick elements nondeterministically from arbitrary sets. *)
 
+(* Specifically, a process producing type [A] is represents as [comp A]. *)
+Definition comp (A : Type) := A -> Prop.
+(* The computation is represented by the set of legal values it might
+ * generate. *)
+
+(* Computations form a monad, with the following two operators. *)
 Definition ret {A} (x : A) : comp A := eq x.
+(* Note how [eq x] is one way of writing "the singleton set of [x],", using
+ * partial application of the two-argument equality predicate [eq]. *)
 Definition bind {A B} (c1 : comp A) (c2 : A -> comp B) : comp B :=
   fun b => exists a, c1 a /\ c2 a b.
-Definition pick_ {A} (P : A -> Prop) : comp A := P.
+(* As in some of our earlier examples, [bind] is for sequencing one computation
+ * after another.  For this monad, existential quantification provides a natural
+ * explanation of sequencing. *)
 
+Definition pick_ {A} (P : A -> Prop) : comp A := P.
+(* Here is a convenient wrapper function for injecting an arbitrary set into
+ * [comp].  This operator stands for nondeterministic choice of any value in the
+ * set. *)
+
+(* Here is the correctness condition, for when [c2] implements [c1].  From left
+ * to right in the operands of [refine], we move closer to a concrete
+ * implementation. *)
 Definition refine {A} (c1 c2 : comp A) :=
   forall a, c2 a -> c1 a.
+(* Note how this definition is just subset inclusion, in the right direction. *)
+
+(* Next, we use Coq's *setoid* feature to declare compatibility of our
+ * definitions with the [rewrite] tactic.  See the Coq manual on setoids for
+ * background on what we are doing and why. *)
 
 Ltac morphisms := unfold refine, impl, pointwise_relation, bind, ret, pick_; hnf; first_order; subst; eauto.
 
@@ -58,12 +90,19 @@ Proof.
   morphisms.
 Qed.
 
+(** ** OK, back to the details we want to focus on. *)
+
+(* Here we have one of the monad laws, showing how traditional computational
+ * reduction is compatible with refinement. *)
 Theorem bind_ret : forall A B (v : A) (c2 : A -> comp B),
     refine (bind (ret v) c2) (c2 v).
 Proof.
   morphisms.
 Qed.
 
+(* Here's an example specific to this monad.  One way to resolve a
+ * nondeterministic pick from a set is to replace it with a specific element
+ * from the set. *)
 Theorem pick_one : forall {A} {P : A -> Prop} v,
     P v
     -> refine (pick_ P) (ret v).
@@ -77,6 +116,8 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) (at level 81, right associati
 
 (** * Picking a number not in a list *)
 
+(* Let's illustrate the big idea with an example derivation. *)
+
 (* A specification of what it means to choose a number that is not in a
  * particular list *)
 Definition notInList (ls : list nat) :=
@@ -125,6 +166,8 @@ Proof.
   linear_arithmetic.
 Qed.
 
+(** ** Interlude: defining some tactics for key parts of derivation *)
+
 (* We run this next step to hide an evar, so that rewriting isn't too eager to
  * make up values for it. *)
 Ltac hide_evars :=
@@ -134,9 +177,12 @@ Ltac hide_evars :=
   | [ |- refine _ ?f ] => set f
   end.
 
+(* This tactic starts a script that finds a term to refine another. *)
 Ltac begin :=
   eexists; simplify; hide_evars.
 
+(* This tactic ends such a derivation, in effect undoing the effect of
+ * [hide_evars]. *)
 Ltac finish :=
   match goal with
   | [ |- refine ?e (?f ?arg1 ?arg2) ] =>
@@ -158,24 +204,24 @@ Ltac finish :=
     unify f' e; reflexivity
   end.
 
+(** ** Back to the example *)
+
 (* Let's derive an efficient implementation. *)
-Theorem implementation : { f : list nat -> comp nat | forall ls, refine (notInList ls) (f ls) }.
+Theorem implementation : sig (fun f : list nat -> comp nat => forall ls, refine (notInList ls) (f ls)).
 Proof.
   begin.
   rewrite notInList_decompose.
   rewrite listMax_refines.
-  setoid_rewrite increment_refines.
-  (* ^-- Different tactic here to let us rewrite under a binder! *)
   rewrite bind_ret.
+  rewrite increment_refines.
   finish.
 Defined.
 
 (* We can extract the program that we found as a standlone, executable Gallina
  * term. *)
 Definition impl := Eval simpl in proj1_sig implementation.
-Print impl.
 
-(* We'll temporarily expose the definition of [max], so we can compute neatly
+(* We'll locally expose the definition of [max], so we can compute neatly
  * here. *)
 Transparent max.
 Eval compute in impl (1 :: 7 :: 8 :: 2 :: 13 :: 6 :: nil).
@@ -183,13 +229,32 @@ Eval compute in impl (1 :: 7 :: 8 :: 2 :: 13 :: 6 :: nil).
 
 (** * Abstract data types (ADTs) *)
 
+(* Stepwise refinement can be most satisfying to build objects with multiple
+ * methods.  The specification of such an object is often called an abstract
+ * data type (ADT), and we studied them (from a verification perspective) in
+ * module DataAbstraction.  Let's see how we can build implementations
+ * automatically from ADTs.  First, some preliminary definitions. *)
+
+(* Every method inhabits this type, where [state] is the type of private state
+ * for the object. *)
 Record method_ {state : Type} := {
   MethodName : string;
   MethodBody : state -> nat -> comp (state * nat)
 }.
+(* A body takes the current state as input and produces the new state as output.
+ * Additionally, we have hardcoded both the parameter type and the return type
+ * to [nat], for simplicity.  The only wrinkle is that a body result is in the
+ * [comp] monad, to let it mix features from specification and
+ * implementation. *)
 
 Arguments method_ : clear implicits.
+Notation "'method' name [[ self , arg ]] = body" :=
+  {| MethodName := name;
+     MethodBody := fun self arg => body |}
+    (at level 100, self at level 0, arg at level 0).
 
+(* Next, this type collects several method definitions, given a list of their
+ * names. *)
 Inductive methods {state : Type} : list string -> Type :=
 | MethodsNil : methods []
 | MethodsCons : forall (m : method_ state) {names},
@@ -198,16 +263,15 @@ Inductive methods {state : Type} : list string -> Type :=
 
 Arguments methods : clear implicits.
 
-Notation "'method' name [[ self , arg ]] = body" :=
-  {| MethodName := name;
-     MethodBody := fun self arg => body |}
-    (at level 100, self at level 0, arg at level 0).
-
+(* Finally, the definition of an abstract data type, which will apply to both
+ * specifications (the classical sense of ADT) and implementations. *)
 Record adt {names : list string} := {
   AdtState : Type;
   AdtConstructor : comp AdtState;
   AdtMethods : methods AdtState names
 }.
+(* An ADT has a state type, one constructor to initialize the state, and a set
+ * of methods that may read and write the state. *)
 
 Arguments adt : clear implicits.
 
@@ -219,26 +283,54 @@ Notation "'ADT' { 'rep' = state 'and' 'constructor' = constr ms }" :=
 Notation "'and' m1 'and' .. 'and' mn" :=
   (MethodsCons m1 (.. (MethodsCons mn MethodsNil) ..)) (at level 101).
 
+(* Here's one quick example, of a counter with duplicate "increment" methods. *)
+
+Definition counter := ADT {
+  rep = nat
+  and constructor = ret 0
+  and method "increment1"[[self, arg]] = ret (self + arg, 0)
+  and method "increment2"[[self, arg]] = ret (self + arg, 0)
+  and method "value"[[self, _]] = ret (self, self)
+}.
+
+(* This example hasn't used the power of the [comp] monad, but we will get
+ * there later. *)
+
 
 (** * ADT refinement *)
 
+(* What does it mean to take sound implementation steps from an ADT toward an
+ * efficient implementation?  We formalize refinement for ADTs as well.  The key
+ * principle will be *simulation*, very similarly to how we used the idea for
+ * compiler verification. *)
+
+(* For a "before" state type [state1] and an "after" state type [state2], we
+ * require choice of a simulation relation [R].  This next inductive relation
+ * captures when all methods are pairwise compatible with [R], between the
+ * "before" and "after" ADTs. *)
 Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop)
   : forall {names}, methods state1 names -> methods state2 names -> Prop :=
 | RmNil : RefineMethods R MethodsNil MethodsNil
 | RmCons : forall name names (f1 : state1 -> nat -> comp (state1 * nat))
                   (f2 : state2 -> nat -> comp (state2 * nat))
                   (ms1 : methods state1 names) (ms2 : methods state2 names),
+
+    (* This condition is the classic "simulation diagram." *)
     (forall s1 s2 arg s2' res,
         R s1 s2
         -> f2 s2 arg (s2', res)
         -> exists s1', f1 s1 arg (s1', res)
                        /\ R s1' s2')
+
     -> RefineMethods R ms1 ms2
     -> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
                        (MethodsCons {| MethodName := name; MethodBody := f2 |} ms2).
 
 Hint Constructors RefineMethods.
 
+(* When does [adt2] refine [adt1]?  When there exists a simulation relation,
+ * with respect to which the constructors and methods all satisfy the usual
+ * simulation diagram. *)
 Record adt_refine {names} (adt1 adt2 : adt names) : Prop := {
   ArRel : AdtState adt1 -> AdtState adt2 -> Prop;
   ArConstructors : forall s2,
@@ -248,6 +340,7 @@ Record adt_refine {names} (adt1 adt2 : adt names) : Prop := {
   ArMethods : RefineMethods ArRel (AdtMethods adt1) (AdtMethods adt2)
 }.
 
+(* We will use this handy tactic to prove ADT refinements. *)
 Ltac choose_relation R :=
   match goal with
   | [ |- adt_refine ?a ?b ] => apply (Build_adt_refine _ a b R)
@@ -255,13 +348,8 @@ Ltac choose_relation R :=
 
 (** ** Example: numeric counter *)
 
-Definition counter := ADT {
-  rep = nat
-  and constructor = ret 0
-  and method "increment1"[[self, arg]] = ret (self + arg, 0)
-  and method "increment2"[[self, arg]] = ret (self + arg, 0)
-  and method "value"[[self, _]] = ret (self, self)
-}.
+(* Let's refine the previous counter spec into an implementation that maintains
+ * two separate counters and adds them on demand. *)
 
 Definition split_counter := ADT {
   rep = nat * nat
@@ -273,6 +361,7 @@ Definition split_counter := ADT {
 
 Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic.
 
+(* Here is why the new implementation is correct. *)
 Theorem split_counter_ok : adt_refine counter split_counter.
 Proof.
   choose_relation (fun n p => n = fst p + snd p).
@@ -292,6 +381,8 @@ Qed.
 
 (** * General refinement strategies *)
 
+(* ADT refinement forms a preorder, as the next two theorems show. *)
+
 Lemma RefineMethods_refl : forall state names (ms : methods state names),
     RefineMethods eq ms ms.
 Proof.
@@ -346,6 +437,13 @@ Proof.
   first_order.
 Qed.
 
+(* Note the use of relation composition for [refine_trans]. *)
+
+(** ** Refining constructors *)
+
+(* One way to refine an ADT is to perform [comp]-level refinement within its
+ * constructor definition. *)
+
 Theorem refine_constructor : forall names state constr1 constr2 (ms : methods _ names),
     refine constr1 constr2
     -> adt_refine {| AdtState := state;
@@ -359,6 +457,13 @@ Proof.
   choose_relation (@eq state); eauto.
 Qed.
 
+(** ** Refining methods *)
+
+(* Conceptually quite similar, refining within methods requires more syntactic
+ * framework. *)
+
+(* This relation captures the process of replacing [oldbody] of method [name]
+ * with [newbody]. *)
 Inductive ReplaceMethod {state} (name : string)
           (oldbody newbody : state -> nat -> comp (state * nat))
   : forall {names}, methods state names -> methods state names -> Prop :=
@@ -373,7 +478,9 @@ Inductive ReplaceMethod {state} (name : string)
                   (MethodsCons {| MethodName := name'; MethodBody := oldbody' |} ms1)
                   (MethodsCons {| MethodName := name'; MethodBody := oldbody' |} ms2).
 
-Theorem ReplaceMethod_ok : forall state name
+(* Let's skip ahead to the next [Theorem]. *)
+
+Lemma ReplaceMethod_ok : forall state name
                                   (oldbody newbody : state -> nat -> comp (state * nat))
                                   names (ms1 ms2 : methods state names),
     (forall s arg, refine (oldbody s arg) (newbody s arg))
@@ -391,6 +498,7 @@ Qed.
 
 Hint Resolve ReplaceMethod_ok.
 
+(* It is OK to replace a method body if the new refines the old as a [comp]. *)
 Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))
                                names (ms1 ms2 : methods state names) constr,
     (forall s arg, refine (oldbody s arg) (newbody s arg))
@@ -406,6 +514,12 @@ Proof.
   choose_relation (@eq state); eauto.
 Qed.
 
+(** ** Representation changes *)
+
+(* Some of the most interesting refinements select new data structures.  That
+ * is, they pick new state types.  Here we formalize that idea in terms of
+ * existence of an *abstraction function* from the new state type to the old. *)
+
 Inductive RepChangeMethods {state1 state2} (absfunc : state2 -> state1)
   : forall {names}, methods state1 names -> methods state2 names -> Prop :=
 | RchNil :
@@ -418,6 +532,12 @@ Inductive RepChangeMethods {state1 state2} (absfunc : state2 -> state1)
                          p <- oldbody (absfunc s) arg;
                          s' <- pick s' where absfunc s' = fst p;
                          ret (s', snd p)) |} ms2).
+(* Interestingly, we managed to rewrite all method bodies automatically, to be
+ * compatible with a new data structure!  The catch is that our language of
+ * method bodies is inherently noncomputational.  We leave nontrivial work for
+ * ourselves, in further refinement of method bodies to remove "pick"
+ * operations.  Note how the generic method template above relies on "pick"
+ * operations to invert abstraction functions. *)
 
 Lemma RepChangeMethods_ok : forall state1 state2 (absfunc : state2 -> state1)
   names (ms1 : methods state1 names) (ms2 : methods state2 names),
@@ -461,12 +581,19 @@ Ltac refine_method nam := eapply refine_trans; [ eapply refine_method with (name
   | repeat (refine (RepmHead _ _ _ _ _)
             || (refine (RepmSkip _ _ _ _ _ _ _ _ _ _); [ equality | ])) ];
     cbv beta; simplify; hide_evars | ].
+(* Don't be thrown off by the [refine] tactic used here.  It is not related to
+ * our notion of refinement!  See module SubsetTypes for an explanation of
+ * it. *)
 
 Ltac refine_finish := apply refine_refl.
 
 (** ** Example: the numeric counter again *)
 
-Definition derived_counter : { counter' | adt_refine counter counter' }.
+(* Let's generate the two-counter variant through the process of finding a
+ * proof, in contrast to theorem [split_counter_ok], which started with the full
+ * code of the transformed ADT. *)
+
+Definition derived_counter : sig (adt_refine counter).
   unfold counter; eexists.
   refine_rep (fun p => fst p + snd p).
 
@@ -505,15 +632,28 @@ Eval simpl in proj1_sig derived_counter.
 
 (** * Another refinement strategy: introducing a cache (a.k.a. finite differencing) *)
 
+(* Some methods begin life as expensive computations, such that it pays off to
+ * precompute their values.  A generic refinement strategy follows this plan by
+ * introducing *caches*. *)
+
+(* Here, [name] names a method whose body leaves the state alone and returns the
+ * result of [func] applied to that state. *)
 Inductive CachingMethods {state} (name : string) (func : state -> nat)
   : forall {names}, methods state names -> methods (state * nat) names -> Prop :=
 | CmNil :
     CachingMethods name func MethodsNil MethodsNil
+
+(* Here is how we rewrite [name] itself.  We are extending state with an extra
+ * cache of [func]'s value, so it is legal just to return that cache. *)
 | CmCached : forall names (ms1 : methods state names) (ms2 : methods _ names),
     CachingMethods name func ms1 ms2
     -> CachingMethods name func
        (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, func s)) |} ms1)
        (MethodsCons {| MethodName := name; MethodBody := (fun s arg => ret (s, snd s)) |} ms2)
+
+(* Any other method now picks up an obligation to recompute the cache value
+ * whenever changing the state.  We express that recomputation with a pick, to
+ * be refined later into efficient logic. *)
 | CmDefault : forall name' names oldbody (ms1 : methods state names) (ms2 : methods _ names),
     name' <> name
     -> CachingMethods name func ms1 ms2
@@ -575,6 +715,8 @@ Ltac refine_cache nam := eapply refine_trans; [ eapply refine_cache with (name :
 
 (** ** An example with lists of numbers *)
 
+(* Let's work out an example of caching. *)
+
 Definition sum := fold_right plus 0.
 
 Definition nats := ADT {
@@ -584,7 +726,7 @@ Definition nats := ADT {
   and method "sum"[[self, _]] = ret (self, sum self)
 }.
 
-Definition optimized_nats : { nats' | adt_refine nats nats' }.
+Definition optimized_nats : sig (adt_refine nats).
   unfold nats; eexists.
 
   refine_cache "sum".

README.md

@@ -27,9 +27,10 @@ The main narrative, also present in the book PDF, presents standard program-proo
 * Chapter 13: `DeepAndShallowEmbeddings.v`
 * Chapter 14: `SeparationLogic.v`
 * Chapter 15: `Connecting.v`
-* Chapter 16: `SharedMemory.v`
-* Chapter 17: `ConcurrentSeparationLogic.v`
-* Chapter 18: `MessagesAndRefinement.v`
+* Chapter 16: `ProgramDerivation.v`
+* Chapter 17: `SharedMemory.v`
+* Chapter 18: `ConcurrentSeparationLogic.v`
+* Chapter 19: `MessagesAndRefinement.v`
 
 There are also two supplementary files that are independent of the main narrative, for introducing programming with dependent types, a distinctive Coq feature that we neither use nor recommend for the problem sets, but which many students find interesting (and useful in other contexts).
 * `SubsetTypes.v`: a first introduction to dependent types by attaching predicates to normal types (used after `CompilerCorrectness.v` in the last course offering)

SharedMemory.v

@@ -1,5 +1,5 @@
 (** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
-  * Chapter 16: Operational Semantics for Shared-Memory Concurrency
+  * Chapter 17: Operational Semantics for Shared-Memory Concurrency
   * Author: Adam Chlipala
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)