Comments for ModelChecking

ModelChecking.v

@@ -8,22 +8,35 @@ Require Import Frap TransitionSystems.
 Set Implicit Arguments.
 
 
+(* Coming up with invariants ourselves can be tedious!  Let's investigate how we
+ * can automate the choice of invariants, for systems with only finitely many
+ * reachable states.  This style is known as model checking.  First, let's think
+ * more deliberately about how to grow a candidate invariant by adding new cases
+ * that we missed.  Here's what it means for one invariant to retain all cases of
+ * another. *)
 Definition oneStepClosure_current {state} (sys : trsys state)
            (invariant1 invariant2 : state -> Prop) :=
   forall st, invariant1 st
              -> invariant2 st.
 
+(* And here's what it means to add all new states reachable from the original
+ * set. *)
 Definition oneStepClosure_new {state} (sys : trsys state)
            (invariant1 invariant2 : state -> Prop) :=
   forall st st', invariant1 st
                  -> sys.(Step) st st'
                  -> invariant2 st'.
 
+(* Putting together the two conditions, we have a closure operator, for
+ * enriching a candidate invariant with all new states reachable from it in a
+ * single step. *)
 Definition oneStepClosure {state} (sys : trsys state)
            (invariant1 invariant2 : state -> Prop) :=
   oneStepClosure_current sys invariant1 invariant2
   /\ oneStepClosure_new sys invariant1 invariant2.
 
+(* Here's a simple restatement of [oneStepClosure] as a theorem with two
+ * premises. *)
 Theorem prove_oneStepClosure : forall state (sys : trsys state) (inv1 inv2 : state -> Prop),
   (forall st, inv1 st -> inv2 st)
   -> (forall st st', inv1 st -> sys.(Step) st st' -> inv2 st')
@@ -33,6 +46,13 @@ Proof.
   propositional.
 Qed.
 
+(* Now imagine the following general procedure to find an invariant.  Start with
+ * the initial states as the candidate invariant.  Now take the one-step
+ * closure, adding all states reachable in one step.  Then take it again, and
+ * again, until the invariant is "big enough."  What is the formal meaning of
+ * this termination condition?  We are done if one-step closure brings us back
+ * to the original set.  (Of course, we must also retain all the initial
+ * states.) *)
 Theorem oneStepClosure_done : forall state (sys : trsys state) (invariant : state -> Prop),
   (forall st, sys.(Initial) st -> invariant st)
   -> oneStepClosure sys invariant invariant
@@ -48,16 +68,28 @@ Proof.
   assumption.
 Qed.
 
+(* Now we define an inductive relation, capturing repeated closure until
+ * convergence. *)
 Inductive multiStepClosure {state} (sys : trsys state)
   : (state -> Prop) -> (state -> Prop) -> Prop :=
+
+(* We might be done, if one-step closure has no effect. *)
 | MscDone : forall inv,
     oneStepClosure sys inv inv
     -> multiStepClosure sys inv inv
+
+(* Or we might need to run another one-step closure and recurse. *)
 | MscStep : forall inv inv' inv'',
     oneStepClosure sys inv inv'
     -> multiStepClosure sys inv' inv''
     -> multiStepClosure sys inv inv''.
 
+(* Now, with the help of a lemma, we prove that multi-step closure is a sound
+ * way to find an invariant for any transition system.  Note that we really do
+ * not have that silver bullet here, because, for many systems, multi-step
+ * closure does not terminate!  However, if it does, we get a correct
+ * invariant. *)
+
 Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv inv' : state -> Prop),
   multiStepClosure sys inv inv'
   -> (forall st, sys.(Initial) st -> inv st)
@@ -88,12 +120,23 @@ Proof.
   propositional.
 Qed.
 
+(* OK, great.  We know how to find invariants if we can evaluate one-step
+ * closure efficiently.  Here's one case that is particularly easy to evaluate,
+ * starting from the empty set as the invariant.  We use a function [constant]
+ * from the FRAP library, for sets of finite size.  In general, we write
+ * [constant [x1; ..., xN]] for the set [{x1, ..., xN}], and in fact the latter
+ * notation is available, too. *)
 Theorem oneStepClosure_empty : forall state (sys : trsys state),
   oneStepClosure sys (constant nil) (constant nil).
 Proof.
   unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; propositional.
 Qed.
 
+(* In general, for finite sets, we'll compute one-step closure by closing
+ * separately over each element of the set.  This theorem implements one step of
+ * that process, where we learn that [inv1] accurately captures where we might
+ * get from state [st] in one step.  States [sts] are those left over to
+ * consider. *)
 Theorem oneStepClosure_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop),
   (forall st', sys.(Step) st st' -> inv1 st')
   -> oneStepClosure sys (constant sts) inv2
@@ -104,6 +147,9 @@ Proof.
   invert H0.
 
   left.
+  (* [left] and [right]: prove a disjunction by proving the left or right case,
+   *   respectively.  Note that here, we are using the fact that set union
+   *   [\cup] is defined in terms of disjunction. *)
   left.
   simplify.
   propositional.
@@ -126,12 +172,26 @@ Proof.
   assumption.
 Qed.
 
+(* A trivial fact about union and singleton sets. *)
+Theorem singleton_in : forall {A} (x : A) rest,
+  ({x} \cup rest) x.
+Proof.
+  simplify.
+  left.
+  simplify.
+  equality.
+Qed.
+
+(* OK, back to our example from last chapter, of factorial as a transition
+ * system.  Here's a good overall correctness condition, which we didn't bother
+ * to state before. *)
 Definition fact_correct (original_input : nat) (st : fact_state) : Prop :=
   match st with
   | AnswerIs ans => fact original_input = ans
   | WithAccumulator _ _ => True
   end.
 
+(* Let's also restate the initial-states set using a singleton set. *)
 Theorem fact_init_is : forall original_input,
   fact_init original_input = {WithAccumulator original_input 1}.
 Proof.
@@ -146,15 +206,91 @@ Proof.
   constructor.
 Qed.
 
-Theorem singleton_in : forall {A} (x : A) rest,
-  ({x} \cup rest) x.
+(* Now we will prove that factorial is correct, for the input 2, without needing
+ * to write out an inductive invariant ourselves.  Note that it's important that
+ * we choose a small, constant input, so that the reachable state space is
+ * finite. *)
+Theorem factorial_ok_2 :
+  invariantFor (factorial_sys 2) (fact_correct 2).
 Proof.
   simplify.
-  left.
+  eapply invariant_weaken.
+  (* We begin like in last chapter, by strengthening to an inductive
+   * invariant. *)
+
+  apply multiStepClosure_ok.
+  (* The difference is that we will use multi-step closure to find the invariant
+   * automatically.  Note that the invariant appears as an existential variable,
+   * whose name begins with a question mark. *)
   simplify.
-  equality.
+  rewrite fact_init_is.
+  (* It's important to phrase the current candidate invariant explicitly as a
+   * finite set, before continuing.  Otherwise, it won't be obvious how to take
+   * the one-step closure. *)
+
+  (* Compute which states are reachable after one step. *)
+  eapply MscStep.
+  apply oneStepClosure_split; simplify.
+  invert H; simplify.
+  apply singleton_in.
+  apply oneStepClosure_empty.
+  simplify.
+
+  (* Compute which states are reachable after two steps. *)
+  eapply MscStep.
+  apply oneStepClosure_split; simplify.
+  invert H; simplify.
+  apply singleton_in.
+  apply oneStepClosure_split; simplify.
+  invert H; simplify.
+  apply singleton_in.
+  apply oneStepClosure_empty.
+  simplify.
+
+  (* Compute which states are reachable after three steps. *)
+  eapply MscStep.
+  apply oneStepClosure_split; simplify.
+  invert H; simplify.
+  apply singleton_in.
+  apply oneStepClosure_split; simplify.
+  invert H; simplify.
+  apply singleton_in.
+  apply oneStepClosure_split; simplify.
+  invert H; simplify.
+  apply singleton_in.
+  apply oneStepClosure_empty.
+  simplify.
+
+  (* Now the candidate invariatn is closed under single steps.  Let's prove
+   * it. *)
+  apply MscDone.
+  apply prove_oneStepClosure; simplify.
+  propositional.
+  propositional; invert H0; try equality.
+  invert H; equality.
+  invert H1; equality.
+
+  (* Finally, we prove that our new invariant implies the simpler, noninductive
+   * one that we started with. *)
+  simplify.
+  propositional; subst; simplify; propositional.
+  (* [subst]: remove all hypotheses like [x = e] for variables [x], simply
+   *   replacing all uses of [x] by [e]. *)
 Qed.
 
+(* That process was so rote that we can automate it all, in a generic way that
+ * will work for most transition systems that have finitely many reachable
+ * states.  Here is a definition of some tactics to do the work.
+ * BEGIN CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *)
+
+Hint Rewrite fact_init_is.
+
+Ltac model_check_done :=
+  apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
+  repeat match goal with
+         | [ H : _ |- _ ] => invert H
+         end; simplify; equality.
+
 Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
   s2 x
   -> (s1 \cup s2) x.
@@ -164,66 +300,6 @@ Proof.
   assumption.
 Qed.
 
-Theorem factorial_ok_2 :
-  invariantFor (factorial_sys 2) (fact_correct 2).
-Proof.
-  simplify.
-  eapply invariant_weaken.
-
-  apply multiStepClosure_ok.
-  simplify.
-  rewrite fact_init_is.
-
-  eapply MscStep.
-  apply oneStepClosure_split; simplify.
-  invert H; simplify.
-  apply singleton_in.
-  apply oneStepClosure_empty.
-  simplify.
-
-  eapply MscStep.
-  apply oneStepClosure_split; simplify.
-  invert H; simplify.
-  apply singleton_in.
-  apply oneStepClosure_split; simplify.
-  invert H; simplify.
-  apply singleton_in.
-  apply oneStepClosure_empty.
-  simplify.
-
-  eapply MscStep.
-  apply oneStepClosure_split; simplify.
-  invert H; simplify.
-  apply singleton_in.
-  apply oneStepClosure_split; simplify.
-  invert H; simplify.
-  apply singleton_in.
-  apply oneStepClosure_split; simplify.
-  invert H; simplify.
-  apply singleton_in.
-  apply oneStepClosure_empty.
-  simplify.
-
-  apply MscDone.
-  apply prove_oneStepClosure; simplify.
-  propositional.
-  propositional; invert H0; try equality.
-  invert H; equality.
-  invert H1; equality.
-
-  simplify.
-  propositional; subst; simplify; propositional.
-              (* ^-- *)
-Qed.
-
-Hint Rewrite fact_init_is.
-
-Ltac model_check_done :=
-  apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
-  repeat match goal with
-         | [ H : _ |- _ ] => invert H
-         end; simplify; equality.
-
 Ltac singletoner :=
   repeat match goal with
          | _ => apply singleton_in
@@ -252,6 +328,11 @@ Ltac model_check_find_invariant :=
 
 Ltac model_check := model_check_find_invariant; model_check_finish.
 
+(* END CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *)
+
+(* Now watch this.  We can check various instances of factorial
+ * automatically. *)
+
 Theorem factorial_ok_2_snazzy :
   invariantFor (factorial_sys 2) (fact_correct 2).
 Proof.
@@ -270,27 +351,46 @@ Proof.
   model_check.
 Qed.
 
+(* Let's see that last one broken into two steps, so that we get a look at the
+ * inferred invariant. *)
+Theorem factorial_ok_5_again :
+  invariantFor (factorial_sys 5) (fact_correct 5).
+Proof.
+  model_check_find_invariant.
+  model_check_finish.
+Qed.
+
 
 (** * Abstraction *)
 
-(*
+(* It's lovely when we happen to be analyzing a system with a finite state
+ * space, but usually we aren't that lucky.  For instance, imagine that we are
+ * using a programming language with infinite-precision integers, and we want to
+ * check this program:
+ * <<
+   int global = 0;
  
-int global = 0;
-
-thread() {
+   thread() {
      int local;
 
      while (true) {
        local = global;
        global = local + 2;
      }
-}
-*)
+   }
+   >>
+ * The program loops indefinitely, adding 2 to a global variable.  We want to
+ * prove that "global" always holds an even value.  Here's how we can formalize
+ * evenness inductively. *)
 
 Inductive isEven : nat -> Prop :=
 | EvenO : isEven 0
 | EvenSS : forall n, isEven n -> isEven (S (S n)).
 
+(* And now we define a transition system for the program, in a process that
+ * should be routine by now.  We use last chapter's concept of a multithreaded
+ * transition system. *)
+
 Inductive add2_thread :=
 | Read
 | Write (local : nat).
@@ -313,18 +413,37 @@ Definition add2_sys1 := {|
 
 Definition add2_sys := parallel add2_sys1 add2_sys1.
 
+(* Here is the invariant we want to prove. *)
+Definition add2_correct (st : threaded_state nat (add2_thread * add2_thread)) :=
+  isEven st.(Shared).
+
+(* We can't model-check [add2_sys] directly, because it can reach infinitely
+ * many states.  Even if we worked with fixed-precision integers, say with 64
+ * bits, the state space would be impractically large to explore directly.
+ * Instead, we will *abstract* this system into another one that retains its
+ * essential properties.  In particular, we want to find another transition
+ * system that *simulates* this one, in the sense made precise by this
+ * definition, where [sys1] will be [add2_sys] for this example. *)
 Inductive simulates state1 state2 (R : state1 -> state2 -> Prop)
+  (* [R] is a relation connecting the states of the two systems. *)
   (sys1 : trsys state1) (sys2 : trsys state2) : Prop :=
 | Simulates :
+  (* Every initial state of [sys1] has some matching initial state of [sys2]. *)
   (forall st1, sys1.(Initial) st1
                -> exists st2, R st1 st2
                               /\ sys2.(Initial) st2)
+
+  (* Starting from a pair of related states, every step in [sys1] can be matched
+   * in [sys2], to destinations that are also related. *)
   -> (forall st1 st2, R st1 st2
                       -> forall st1', sys1.(Step) st1 st1'
                                       -> exists st2', R st1' st2'
                                                       /\ sys2.(Step) st2 st2')
+
   -> simulates R sys1 sys2.
 
+(* Given an invariant for [sys2], we now have a generic way of defining an
+ * invariant for [sys1], by composing with [R]. *)
 Inductive invariantViaSimulation state1 state2 (R : state1 -> state2 -> Prop)
   (inv2 : state2 -> Prop)
   : state1 -> Prop :=
@@ -332,6 +451,8 @@ Inductive invariantViaSimulation state1 state2 (R : state1 -> state2 -> Prop)
   -> inv2 st2
   -> invariantViaSimulation R inv2 st1.
 
+(* By way of a lemma, let's prove that, given a simulation, any
+ * invariant-via-simulation really is an invariant for the original system. *)
 Lemma invariant_simulates' : forall state1 state2 (R : state1 -> state2 -> Prop)
   (sys1 : trsys state1) (sys2 : trsys state2),
   (forall st1 st2, R st1 st2
@@ -347,12 +468,15 @@ Proof.
 
   simplify.
   exists st2.
+  (* [exists E]: prove [exists x, P(x)] by proving [P(E)]. *)
   propositional.
   constructor.
 
   simplify.
   eapply H in H2.
   first_order.
+  (* [first_order]: simplify first-order logic structure.  Be forewarned: this
+   *   one is especially likely to run forever! *)
   apply IHtrc in H2.
   first_order.
   exists x1.
@@ -383,19 +507,23 @@ Proof.
   assumption.
 Qed.
 
-(* Abstracted program:
+(* OK, that's a general theory for abstracting a system with another one that
+ * simulates it.  What abstraction will work for our example of the two threads
+ * and the counter?  Here's another program that has replaced integers with
+ * Booleans, where the Boolean is true iff the matching integer is even.
+ * <<
+    bool global = true;
 
-bool global = true;
-
-thread() {
+    thread() {
       bool local;
 
       while (true) {
         local = global;
         global = local;
       }
-}
-*)
+    }
+   >>
+ * We can formalize this program as a transition system, too. *)
 
 Inductive add2_bthread :=
 | BRead
@@ -419,14 +547,14 @@ Definition add2_bsys1 := {|
 
 Definition add2_bsys := parallel add2_bsys1 add2_bsys1.
 
-Definition add2_correct (st : threaded_state nat (add2_thread * add2_thread)) :=
-  isEven st.(Shared).
-
+(* This invariant formalizes the connection between local states of threads, in
+ * the original and abstracted systems. *)
 Inductive R_private1 : add2_thread -> add2_bthread -> Prop :=
 | RpRead : R_private1 Read BRead
 | RpWrite : forall n b, (b = true <-> isEven n)
                         -> R_private1 (Write n) (BWrite b).
 
+(* We lift [R_private1] to a relation over whole states. *)
 Inductive add2_R : threaded_state nat (add2_thread * add2_thread)
                    -> threaded_state bool (add2_bthread * add2_bthread)
                    -> Prop :=
@@ -437,6 +565,7 @@ Inductive add2_R : threaded_state nat (add2_thread * add2_thread)
   -> add2_R {| Shared := n; Private := (th1, th2) |}
             {| Shared := b; Private := (th1', th2') |}.
 
+(* Let's also recharacterize the initial states via a singleton set. *)
 Theorem add2_init_is :
   parallel1 add2_binit add2_binit = { {| Shared := true; Private := (BRead, BRead) |} }.
 Proof.
@@ -455,14 +584,24 @@ Proof.
   constructor.
 Qed.
 
+(* We ask Coq to remember this lemma as a hint, which will be used by the
+ * model-checking tactics that we refrain from explaining in detail. *)
 Hint Rewrite add2_init_is.
 
+(* Now, let's verify the original system. *)
 Theorem add2_ok :
   invariantFor add2_sys add2_correct.
 Proof.
+  (* First step: strengthen the invariant.  We leave an underscore for the
+   * unknown invariant, to be found by model checking. *)
   eapply invariant_weaken with (invariant1 := invariantViaSimulation add2_R _).
+
+  (* One way to find an invariant-by-simulation is to find an invariant for the
+   * abstracted system, as this step asks to do. *)
   apply invariant_simulates with (sys2 := add2_bsys).
 
+  (* Now we must prove that the simulation via [add2_R] is valid, which is
+   * routine. *)
   constructor; simplify.
 
   invert H.
@@ -533,7 +672,13 @@ Proof.
   constructor.
   constructor.
 
+  (* OK, we're glad to have that over with!  Such a process could also be
+   * automated, but we won't bother doing so here.  However, we are now in a
+   * good state, where our model checker can find the invariant
+   * automatically. *)
   model_check_infer.
+  (* It finds exactly four reachable states.  We finish by showing that they all
+   * obey the original invariant. *)
 
   invert 1.
   invert H0.
@@ -558,9 +703,10 @@ Qed.
 
 (** * Another abstraction example *)
 
-(*
-
-f(int n) {
+(* Let's try a fancier example of abstraction.  Here's a simple integer
+ * function.
+ * <<
+    f(int n) {
       int i, j;
 
       i = 0;
@@ -570,8 +716,10 @@ f(int n) {
         j = j + n;
         n = n - 1;
       }
-}
-*)
+    }
+   >>
+ * We might want to prove that "i" and "j" are always equal at the end.
+ * First, we formalize the transition system. *)
 
 Inductive pc :=
 | i_gets_0
@@ -652,13 +800,32 @@ Definition loopy_sys := {|
   Step := step
 |}.
 
-Inductive absvars := Unknown | i_is_0 | i_eq_j | i_eq_j_plus_n.
+Definition loopy_correct (st : state) :=
+  st.(Pc) = Done -> st.(Vars).(I) = st.(Vars).(J).
 
+(* Which abstraction will give us a finite-state system?  Unlike with factorial,
+ * here we are more ambitious, seeking an abstraction that will be finite-state
+ * even when considering all possible parameter values "n".  Let's try this
+ * simple abstract version of variable state. *)
+Inductive absvars :=
+| Unknown
+  (* We don't know anything about the values of the variables. *)
+| i_is_0
+  (* We know [i == 0]. *)
+| i_eq_j
+  (* We know [i == j]. *)
+| i_eq_j_plus_n.
+  (* We know [i == j + n]. *)
+
+(* To get our abstract states, we keep the same program counters and just change
+ * out the variable state. *)
 Record absstate := {
   APc : pc;
   AVars : absvars
 }.
 
+(* Here's the rather boring new abstract step relation.  Note the clever state
+ * transformations, in terms of our new abstraction. *)
 Inductive absstep : absstate -> absstate -> Prop :=
 | AStep_i_gets_0 : forall vs,
   absstep {| APc := i_gets_0; AVars := vs |}
@@ -703,25 +870,27 @@ Definition absloopy_sys := {|
   Step := absstep
 |}.
 
+(* Now we need our simulation relation.  First, we define one just at the level
+ * of local-variable state.  It formalizes our intuition about those values. *)
 Inductive Rvars : vars -> absvars -> Prop :=
 | Rv_Unknown : forall vs, Rvars vs Unknown
 | Rv_i_is_0 : forall vs, vs.(I) = 0 -> Rvars vs i_is_0
 | Rv_i_eq_j : forall vs, vs.(I) = vs.(J) -> Rvars vs i_eq_j
 | Rv_i_eq_j_plus_n : forall vs, vs.(I) = vs.(J) + vs.(N) -> Rvars vs i_eq_j_plus_n.
 
+(* We lift to full states in the obvious way. *)
 Inductive R : state -> absstate -> Prop :=
 | Rcon : forall pc vs avs, Rvars vs avs -> R {| Pc := pc; Vars := vs |}
                                              {| APc := pc; AVars := avs |}.
 
-Definition loopy_correct (st : state) :=
-  st.(Pc) = Done -> st.(Vars).(I) = st.(Vars).(J).
-
+(* Now we are ready to prove the original system correct. *)
 Theorem loopy_ok :
   invariantFor loopy_sys loopy_correct.
 Proof.
   eapply invariant_weaken with (invariant1 := invariantViaSimulation R _).
   apply invariant_simulates with (sys2 := absloopy_sys).
 
+  (* Here comes another boring simulation proof. *)
   constructor; simplify.
 
   invert H.
@@ -770,14 +939,22 @@ Proof.
   exists {| APc := Loop; AVars := i_eq_j |}; propositional; repeat constructor; equality.
   exists {| APc := Loop; AVars := Unknown |}; propositional; repeat constructor; equality.
 
+  (* Finally, we can call the model checker to find an invariant of the abstract
+   * system. *)
   model_check_infer.
+  (* We get 7 neat little states, one per program counter.  Next, we prove that
+   * each of them implies the original invariant. *)
 
-  invert 1.
+  invert 1. (* Note that this [1] means "first premise below the double
+             * line." *)
   invert H0.
   unfold loopy_correct.
   simplify.
   propositional; subst.
 
+  (* Most of the hypotheses we invert are contradictory, implying that distinct
+   * program counters are equal. *)
+
   invert H2.
 
   invert H1.
@@ -798,18 +975,40 @@ Qed.
 
 (** * Modularity *)
 
+(* Throughout the book, we'll come again and again to our two main weapons in
+ * soundly modeling complex transition systems with simpler ones.  We just
+ * learned about *abstraction*, to replace a full system with a simpler one.
+ * The other key one is *modularity*, to replace a system with several others.
+ * Let's study one example that helps with model checking, allowing us to check
+ * programs with arbitrarily many threads running the same code, while still
+ * finding an invariant automatically by brute-force enumeration. *)
+
+(* The key to this particular technique is instrumenting a step relation to
+ * consider *interference*, or the actions that other threads might take, in
+ * between steps of the thread that we focus on.  This relation is parameterized
+ * on an invariant [inv] that the other threads guarantee to preserve on the
+ * shared state.  That is, the other threads may mess with the shared state
+ * arbitrarily between our own steps, *but* they guarantee that every value they
+ * set for it satisfies [inv]. *)
 Inductive stepWithInterference shared private (inv : shared -> Prop)
           (step : threaded_state shared private -> threaded_state shared private -> Prop)
           : threaded_state shared private -> threaded_state shared private -> Prop :=
+
+(* First kind of step: this thread runs in the normal way. *)
 | StepSelf : forall st st',
   step st st'
   -> stepWithInterference inv step st st'
+
+(* Second kind of step: other threads change shared state to some new value
+ * satisfying [inv]. *)
 | StepEnvironment : forall sh pr sh',
   inv sh'
   -> stepWithInterference inv step
                           {| Shared := sh; Private := pr |}
                           {| Shared := sh'; Private := pr |}.
 
+(* Via this relation, we have an operator to build a new transition system from
+ * an old one, given [inv]. *)
 Definition withInterference shared private (inv : shared -> Prop)
            (sys : trsys (threaded_state shared private))
   : trsys (threaded_state shared private) := {|
@@ -817,12 +1016,17 @@ Definition withInterference shared private (inv : shared -> Prop)
   Step := stepWithInterference inv sys.(Step)
 |}.
 
+(* We also have a ready-made invariant we could try to prove for any such
+ * system, asserting that [inv] always holds of the shared state. *) 
 Inductive sharedInvariant shared private (inv : shared -> Prop)
   : threaded_state shared private -> Prop :=
 | SharedInvariant : forall sh pr,
   inv sh
   -> sharedInvariant inv {| Shared := sh; Private := pr |}.
 
+(* Tired of simulation proofs yet?  Then you'll love this theorem, which shows
+ * a free simulation for any use of [withInterference]!  We even get to pick the
+ * trivial simulation relation, state equality. *)
 Theorem withInterference_abstracts : forall shared private (inv : shared -> Prop)
                                            (sys : trsys (threaded_state shared private)),
   simulates (fun st st' => st = st') sys (withInterference inv sys).
@@ -837,6 +1041,12 @@ Proof.
   equality.
 Qed.
 
+(* That proof was pretty straightforward, because we could construct the
+ * simulation using only the first rule of [stepWithInterference], ignoring the
+ * possibility for steps by other threads.  We go next for a theorem with an
+ * intimidating statement and a much more interesting proof, whose details we
+ * nonetheless won't comment on in text.  It may make sense to skip past the
+ * next two lemma statements to the main theorem [withInterference_parallel]. *)
 Lemma withInterference_parallel1 : forall shared private1 private2
                                           (invs : shared -> Prop)
                                           (sys1 : trsys (threaded_state shared private1))
@@ -1025,6 +1235,12 @@ Proof.
   constructor.
 Qed.
 
+(* OK, we made it to the main theorem.  It helps us find an invariant for a
+ * [parallel] system to which we have applied the [withInterference]
+ * construction.  Crucially, we may check the invariant for each constituent
+ * thread *separately*, avoiding the combinatorial state-space explosion that
+ * would come from analyzing the combined system directly.  This is the essence
+ * of modularity! *)
 Theorem withInterference_parallel : forall shared private1 private2
                                            (invs : shared -> Prop)
                                            (sys1 : trsys (threaded_state shared private1))
@@ -1040,6 +1256,8 @@ Proof.
   simplify.
   invert H1.
 
+  (* [assert P]: first prove proposition [P], then continue with it as a new
+   *   hypothesis. *)
   assert ((withInterference invs sys1).(Step)^*
              {| Shared := sh; Private := pr1 |}
              {| Shared := s'.(Shared); Private := fst s'.(Private) |}).
@@ -1067,8 +1285,9 @@ Proof.
   apply H in H1; try assumption.
 Qed.
 
-(*
-
+(* Let's apply this principle on a concrete example.  Consider a program with
+ * many threads running calls to this function.
+ * <<
     int global = 0;
 
     f() {
@@ -1081,7 +1300,8 @@ Qed.
         global = local;
       }
     }
-*)
+   >>
+ * Here's the usual formalization as a transition system. *)
 
 Inductive twoadd_pc := ReadIt | Add3 | Add7 | WriteIt.
 
@@ -1107,9 +1327,13 @@ Definition twoadd_sys := {|
   Step := twoadd_step
 |}.
 
+(* Invariant to prove: the global variable is always even, again. *)
 Definition twoadd_correct private (st : threaded_state nat private) :=
   isEven st.(Shared).
 
+(* Here's an abstract version of the system where, much like before, we model
+ * integers as Booleans, recording whether they are even or not. *)
+
 Definition twoadd_ainitial := { {| Shared := true; Private := (ReadIt, true) |} }.
 
 Inductive twoadd_astep : threaded_state bool (twoadd_pc * bool)
@@ -1135,9 +1359,13 @@ Definition twoadd_asys := {|
   Step := twoadd_astep
 |}.
 
+(* Here's a simulation relation at the level of integers and their Boolean
+ * counterparts. *)
 Definition even_R (n : nat) (b : bool) :=
   isEven n <-> b = true.
 
+(* A few unsurprising properties hold of [even_R]. *)
+
 Lemma even_R_0 : even_R 0 true.
 Proof.
   unfold even_R; propositional.
@@ -1163,6 +1391,7 @@ Proof.
   constructor; assumption.
 Qed.
 
+(* The cases for evenness of an integer and its successor *)
 Lemma isEven_decide : forall n,
   (isEven n /\ ~isEven (S n)) \/ (~isEven n /\ isEven (S n)).
 Proof.
@@ -1192,6 +1421,7 @@ Proof.
   equality.
 Qed.
 
+(* Here's the top-level simulation relation for our choice of abstraction. *)
 Inductive twoadd_R : threaded_state nat (twoadd_pc * nat)
                      -> threaded_state bool (twoadd_pc * bool) -> Prop :=
 | Twoadd_R : forall pc gn ln gb lb,
@@ -1200,6 +1430,7 @@ Inductive twoadd_R : threaded_state nat (twoadd_pc * nat)
   -> twoadd_R {| Shared := gn; Private := (pc, ln) |}
               {| Shared := gb; Private := (pc, lb) |}.
 
+(* Step 1 of main proof: model-check an individual thread. *)
 Lemma twoadd_ok :
   invariantFor (withInterference isEven twoadd_sys)
                (fun st => isEven (Shared st)).
@@ -1207,6 +1438,7 @@ Proof.
   eapply invariant_weaken.
   apply invariant_simulates with (sys2 := twoadd_asys) (R := twoadd_R).
 
+  (* Boring simulation proof begins here. *)
   constructor; simplify.
 
   invert H.
@@ -1255,8 +1487,10 @@ Proof.
   assumption.
   constructor.
 
+  (* Now find an invariant automatically. *)
   model_check_infer.
 
+  (* Now prove that the invariant implies the correctness condition. *)
   invert 1.
   invert H0.
   simplify.
@@ -1279,6 +1513,8 @@ Proof.
   assumption.
 Qed.
 
+(* Step 2: lift that result to the two-thread system, with no new model
+ * checking. *) 
 Theorem twoadd2_ok :
   invariantFor (parallel twoadd_sys twoadd_sys) (twoadd_correct (private := _)).
 Proof.
@@ -1294,18 +1530,27 @@ Proof.
   assumption.
 Qed.
 
+(* In fact, this modularity technique is so powerful that we now get correctness
+ * for any number of threads, "for free"!  Here's a tactic definition, which we
+ * won't explain, but which is able to derive correctness for any number of
+ * threads, just by repeating use of [withInterference_parallel] and
+ * [twoadd_ok]. *)
 Ltac twoadd := eapply invariant_weaken; [ eapply invariant_simulates; [
                                           apply withInterference_abstracts
                                           | repeat (apply withInterference_parallel
                                                     || apply twoadd_ok) ]
                                         | unfold twoadd_correct; invert 1; assumption ].
 
+(* For instance, let's verify the three-thread version. *)
 Theorem twoadd3_ok :
   invariantFor (parallel twoadd_sys (parallel twoadd_sys twoadd_sys)) (twoadd_correct (private := _)).
 Proof.
   twoadd.
 Qed.
 
+(* To save us time defining versions with many threads, here's a recursive
+ * function, creating exponentially many threads with respect to its
+ * parameter. *)
 Fixpoint manyadds_state (n : nat) : Type :=
   match n with
   | O => twoadd_pc * nat
@@ -1318,6 +1563,7 @@ Fixpoint manyadds (n : nat) : trsys (threaded_state nat (manyadds_state n)) :=
   | S n' => parallel (manyadds n') (manyadds n')
   end.
 
+(* Here are some examples of the systems we produce. *)
 Eval simpl in manyadds 0.
 Eval simpl in manyadds 1.
 Eval simpl in manyadds 2.

_CoqProject

@@ -11,3 +11,4 @@ Interpreters_template.v
 Interpreters.v
 TransitionSystems_template.v
 TransitionSystems.v
+ModelChecking.v