diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v
index 820ba26..79bb52e 100644
--- a/ConcurrentSeparationLogic.v
+++ b/ConcurrentSeparationLogic.v
@@ -86,6 +86,13 @@ Inductive step : forall A, heap * locks * cmd A -> heap * locks * cmd A -> Prop
 | StepFree : forall h l a numWords,
   step (h, l, Free a numWords) (deallocate h a numWords, l, Return tt)
 
+| StepLock : forall h l a,
+  ~a \in l
+  -> step (h, l, Lock a) (h, l \cup {a}, Return tt)
+| StepUnlock : forall h l a,
+  a \in l
+  -> step (h, l, Unlock a) (h, l \setminus {a}, Return tt)
+
 | StepPar1 : forall h l c1 c2 h' l' c1',
   step (h, l, c1) (h', l', c1')
   -> step (h, l, Par c1 c2) (h', l', Par c1' c2)
@@ -293,7 +300,7 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu
     (forall acc, hoare_triple linvs (I (Again acc)) (body acc) I)
     -> hoare_triple linvs (I (Again init)) (Loop init body) (fun r => I (Done r))
 | HtFail : forall {result},
-    hoare_triple linvs (fun _ => False) (Fail (result := result)) (fun _ _ => False)
+    hoare_triple linvs [| False |]%sep (Fail (result := result)) (fun _ => [| False |])%sep
 | HtRead : forall a R,
     hoare_triple linvs (exists v, a |-> v * R v)%sep (Read a) (fun r => a |-> r * R r)%sep
 | HtWrite : forall a v',
@@ -318,8 +325,8 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu
 (* When forking into two threads, divide the (local) heap among them. *)
 | HtPar : forall P1 c1 Q1 P2 c2 Q2,
     hoare_triple linvs P1 c1 Q1
-    -> hoare_triple linvs P2 c1 Q2
-    -> hoare_triple linvs (P1 * P1)%sep (Par c1 c2) (fun _ => Q1 tt * Q2 tt)%sep
+    -> hoare_triple linvs P2 c2 Q2
+    -> hoare_triple linvs (P1 * P2)%sep (Par c1 c2) (fun _ => Q1 tt * Q2 tt)%sep
 
 (* Now we repeat these two structural rules from before. *)
 | HtConsequence : forall {result} (c : cmd result) P Q (P' : hprop) (Q' : _ -> hprop),
@@ -332,50 +339,50 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu
     -> hoare_triple linvs (P * R)%sep c (fun r => Q r * R)%sep.
 
 
-(*
-Notation "{{ P }} c {{ r ~> Q }}" :=
-  (hoare_triple P%sep c (fun r => Q%sep)) (at level 90, c at next level).
+Notation "linvs ||- {{ P }} c {{ r ~> Q }}" :=
+  (hoare_triple linvs P%sep c (fun r => Q%sep)) (at level 90, c at next level).
 
-Lemma HtStrengthen : forall {result} (c : cmd result) P Q (Q' : _ -> hprop),
-    hoare_triple P c Q
+Lemma HtStrengthen : forall linvs {result} (c : cmd result) P Q (Q' : _ -> hprop),
+    hoare_triple linvs P c Q
     -> (forall r, Q r ===> Q' r)
-    -> hoare_triple P c Q'.
+    -> hoare_triple linvs P c Q'.
 Proof.
   simplify.
   eapply HtConsequence; eauto.
   reflexivity.
 Qed.
 
-Lemma HtWeaken : forall {result} (c : cmd result) P Q (P' : hprop),
-    hoare_triple P c Q
+Lemma HtWeaken : forall linvs {result} (c : cmd result) P Q (P' : hprop),
+    hoare_triple linvs P c Q
     -> P' ===> P
-    -> hoare_triple P' c Q.
+    -> hoare_triple linvs P' c Q.
 Proof.
   simplify.
   eapply HtConsequence; eauto.
   reflexivity.
 Qed.
 
-Lemma invert_Return : forall {result : Set} (r : result) P Q,
-  hoare_triple P (Return r) Q
-  -> forall h, P h -> Q r h.
+Hint Resolve himp_refl.
+
+Lemma invert_Return : forall linvs {result : Set} (r : result) P Q,
+  hoare_triple linvs P (Return r) Q
+  -> P ===> Q r.
 Proof.
   induct 1; propositional; eauto.
 
-  exists h, $0; propositional; eauto.
-  unfold lift; propositional.
+  cancel.
 
-  unfold himp in *; eauto.
+  eauto using himp_trans.
 
-  unfold star, himp in *; simp; eauto 7.
+  rewrite IHhoare_triple; eauto.
 Qed.
 
 Hint Constructors hoare_triple.
 
-Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
-  hoare_triple P (Bind c1 c2) Q
-  -> exists R, hoare_triple P c1 R
-               /\ forall r, hoare_triple (R r) (c2 r) Q.
+Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
+  hoare_triple linvs P (Bind c1 c2) Q
+  -> exists R, hoare_triple linvs P c1 R
+               /\ forall r, hoare_triple linvs (R r) (c2 r) Q.
 Proof.
   induct 1; propositional; eauto.
 
@@ -395,11 +402,11 @@ Proof.
   eapply HtFrame; eauto.
 Qed.
 
-Lemma invert_Loop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) P Q,
-    hoare_triple P (Loop init body) Q
-    -> exists I, (forall acc, hoare_triple (I (Again acc)) (body acc) I)
-                 /\ (forall h, P h -> I (Again init) h)
-                 /\ (forall r h, I (Done r) h -> Q r h).
+Lemma invert_Loop : forall linvs {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) P Q,
+    hoare_triple linvs P (Loop init body) Q
+    -> exists I, (forall acc, hoare_triple linvs (I (Again acc)) (body acc) I)
+                 /\ P ===> I (Again init)
+                 /\ (forall r, I (Done r) ===> Q r).
 Proof.
   induct 1; propositional; eauto.
 
@@ -407,19 +414,12 @@ Proof.
   exists x; propositional; eauto.
   unfold himp in *; eauto.
 
+  eauto using himp_trans.
+
   simp.
   exists (fun o => x o * R)%sep; propositional; eauto.
-  unfold star in *; simp; eauto 7.
-  unfold star in *; simp; eauto 7.
-Qed.
-
-Lemma invert_Fail : forall result P Q,
-  hoare_triple P (Fail (result := result)) Q
-  -> forall h, P h -> False.
-Proof.
-  induct 1; propositional; eauto.
-
-  unfold star in *; simp; eauto.
+  rewrite H0; eauto.
+  rewrite H3; eauto.
 Qed.
 
 (* Now that we proved enough basic facts, let's hide the definitions of all
@@ -438,16 +438,18 @@ Proof.
   linear_arithmetic.
 Qed.
 
-Lemma invert_Read : forall a P Q,
-  hoare_triple P (Read a) Q
+Lemma invert_Read : forall linvs a P Q,
+  hoare_triple linvs P (Read a) Q
   -> exists R, (P ===> exists v, a |-> v * R v)%sep
                /\ forall r, a |-> r * R r ===> Q r.
 Proof.
   induct 1; simp; eauto.
 
-  exists R; simp.
-  cancel; auto.
-  cancel; auto.
+  apply unit_not_nat in x0; simp.
+
+  apply unit_not_nat in x0; simp.
+
+  apply unit_not_nat in x0; simp.
 
   apply unit_not_nat in x0; simp.
 
@@ -463,8 +465,8 @@ Proof.
   cancel.
 Qed.
 
-Lemma invert_Write : forall a v' P Q,
-  hoare_triple P (Write a v') Q
+Lemma invert_Write : forall linvs a v' P Q,
+  hoare_triple linvs P (Write a v') Q
   -> exists R, (P ===> (exists v, a |-> v) * R)%sep
                /\ a |-> v' * R ===> Q tt.
 Proof.
@@ -491,8 +493,8 @@ Proof.
   cancel.
 Qed.
 
-Lemma invert_Alloc : forall numWords P Q,
-  hoare_triple P (Alloc numWords) Q
+Lemma invert_Alloc : forall linvs numWords P Q,
+  hoare_triple linvs P (Alloc numWords) Q
   -> forall r, P * r |--> zeroes numWords ===> Q r.
 Proof.
   induct 1; simp; eauto.
@@ -503,8 +505,14 @@ Proof.
 
   apply unit_not_nat in x0; simp.
 
-  rewrite H0.
-  eauto using himp_trans.
+  apply unit_not_nat in x0; simp.
+
+  apply unit_not_nat in x0; simp.
+
+  apply unit_not_nat in x0; simp.
+
+  rewrite H0; eauto.
+  eauto 7 using himp_trans.
 
   rewrite <- IHhoare_triple.
   cancel.
@@ -568,7 +576,7 @@ Lemma initialize_fresh : forall a' h a numWords,
 Proof.
   induct numWords; simp; auto.
 Qed.
-  
+
 Lemma zeroes_initialize : forall numWords a h,
     (forall i, i < numWords -> h $? (a + i) = None)
     -> (fun h' => h' = initialize h a numWords) ===> (fun h' => h' = h) * a |--> zeroes numWords.
@@ -586,8 +594,8 @@ Proof.
   rewrite initialize_fresh; auto.
 Qed.
 
-Lemma invert_Free : forall a numWords P Q,
-  hoare_triple P (Free a numWords) Q
+Lemma invert_Free : forall linvs a numWords P Q,
+  hoare_triple linvs P (Free a numWords) Q
   -> P ===> a |->? numWords * Q tt.
 Proof.
   induct 1; simp; eauto.
@@ -651,9 +659,9 @@ Proof.
   Opaque himp.
 Qed.
 
-Lemma HtReturn' : forall P {result : Set} (v : result) Q,
+Lemma HtReturn' : forall linvs P {result : Set} (v : result) Q,
     P ===> Q v
-    -> hoare_triple P (Return v) Q.
+    -> hoare_triple linvs P (Return v) Q.
 Proof.
   simp.
   eapply HtStrengthen.
@@ -662,699 +670,431 @@ Proof.
   cancel.
 Qed.
 
+Opaque heq himp lift star exis ptsto.
+
+Lemma invert_Lock : forall linvs a P Q,
+  hoare_triple linvs P (Lock a) Q
+  -> exists I, nth_error linvs a = Some I
+               /\ P * I ===> Q tt.
+Proof.
+  induct 1; simp; eauto 10.
+
+  symmetry in x0.
+  apply unit_not_nat in x0; simp.
+
+  symmetry in x0.
+  apply unit_not_nat in x0; simp.
+
+  eexists; simp.
+  eauto.
+  cancel.
+
+  eexists; simp.
+  eauto.
+  rewrite H0; eauto using himp_trans.
+
+  eexists; simp.
+  eauto.
+  rewrite <- H2.
+  cancel.
+Qed.
+
+Lemma invert_Unlock : forall linvs a P Q,
+  hoare_triple linvs P (Unlock a) Q
+  -> exists I, nth_error linvs a = Some I
+               /\ P ===> Q tt * I.
+Proof.
+  induct 1; simp; eauto 10.
+
+  symmetry in x0.
+  apply unit_not_nat in x0; simp.
+
+  symmetry in x0.
+  apply unit_not_nat in x0; simp.
+
+  eexists; simp.
+  eauto.
+  cancel.
+
+  eexists; simp.
+  eauto.
+  rewrite <- H1; eauto using himp_trans.
+
+  eexists; simp.
+  eauto.
+  rewrite H2.
+  cancel.
+Qed.
+
+Lemma invert_Par : forall linvs c1 c2 P Q,
+  hoare_triple linvs P (Par c1 c2) Q
+  -> exists P1 P2 Q1 Q2,
+      hoare_triple linvs P1 c1 Q1
+      /\ hoare_triple linvs P2 c2 Q2
+      /\ P ===> P1 * P2
+      /\ Q1 tt * Q2 tt ===> Q tt.
+Proof.
+  induct 1; simp; eauto 10.
+
+  symmetry in x0.
+  apply unit_not_nat in x0; simp.
+
+  symmetry in x0.
+  apply unit_not_nat in x0; simp.
+
+  eauto 10 using himp_trans.
+
+  exists (x * R)%sep, x0, (fun r => x1 r * R)%sep, x2; simp; eauto.
+  rewrite H2; cancel.
+  rewrite <- H4; cancel.
+Qed.
+
 (* Temporarily transparent again! *)
 Transparent heq himp lift star exis ptsto.
 
-Lemma preservation : forall {result} (c : cmd result) h c' h',
-    step (h, c) (h', c')
-    -> forall Q, hoare_triple (fun h' => h' = h) c Q
-                 -> hoare_triple (fun h'' => h'' = h') c' Q.
+(* Guarded predicates *)
+Definition guarded (P : Prop) (p : hprop) : hprop :=
+  fun h => IF P then p h else emp%sep h.
+
+Infix "===>" := guarded : sep_scope.
+
+Theorem guarded_true : forall (P : Prop) p, P
+  -> (P ===> p) === p.
+Proof.
+  unfold heq, guarded, IF_then_else; simp.
+Qed.
+
+Theorem guarded_false : forall (P : Prop) p, ~P
+  -> (P ===> p) === emp.
+Proof.
+  unfold heq, guarded, IF_then_else; simp.
+Qed.
+
+(* Iterated separating conjunction *)
+Fixpoint bigstar A (P : nat -> A -> hprop) (ls : list A) : hprop :=
+  match ls with
+  | nil => emp
+  | x :: ls' => P 0 x * bigstar (fun n => P (S n)) ls'
+  end%sep.
+
+Definition lockChunks (l : locks) (ls : list hprop) :=
+  bigstar (fun i I => (~i \in l) ===> I)%sep ls.
+
+Lemma use_himp : forall P Q, P ===> Q
+  -> forall h, P h -> Q h.
+Proof.
+  auto.
+Qed.
+
+Lemma ptsto_out : forall h a v p,
+    h $? a = Some v
+    -> (exists v', a |-> v' * p v')%sep h
+    -> (a |-> v * p v)%sep h
+       /\ forall v', (a |-> v' * p v)%sep (h $+ (a, v')).
+Proof.
+  invert 2.
+  invert H1.
+  simp.
+
+  invert H2.
+  unfold split in H0; subst.
+  rewrite lookup_join1 in H.
+  unfold heap1 in H.
+  simplify.
+  invert H.
+  exists (heap1 a v), x1; simp.
+  eauto.
+  unfold ptsto.
+  eauto.
+  unfold heap1; simplify.
+  sets.
+
+  invert H2.
+  unfold split in H0; subst.
+  rewrite lookup_join1 in H.
+  unfold heap1 in H.
+  simplify.
+  invert H.
+  exists (heap1 a v'), x1; simp.
+  unfold split.
+  maps_equal.
+  rewrite lookup_join1.
+  unfold heap1; simplify; auto.
+  unfold heap1; simplify; sets.
+  repeat rewrite lookup_join2; auto.
+  unfold heap1; simplify; sets.
+  unfold heap1; simplify; sets.
+  unfold disjoint in *; simp.
+  apply (H1 a0); eauto.
+  cases (a ==n a0); simp.
+  unfold heap1 in *; simplify; equality.
+  unfold heap1 in *; simplify; equality.
+  unfold ptsto.
+  eauto.
+  unfold heap1; simplify; sets.
+Qed.
+
+Lemma specialize_hprop : forall (p : hprop) h,
+    p h
+    -> (fun h' => h' = h) ===> p.
+Proof.
+  unfold himp; equality.
+Qed.
+
+Opaque heq himp lift star exis ptsto.
+
+Lemma bigstar_impl : forall A ls (p q : nat -> A -> hprop),
+    (forall i x, p i x ===> q i x)
+    -> bigstar p ls ===> bigstar q ls.
+Proof.
+  induct ls; simplify; auto.
+  rewrite H.
+  rewrite IHls.
+  cancel.
+  simp.
+  eauto.
+Qed.
+
+Lemma guarded_impl : forall P Q p,
+    P <-> Q
+    -> (P ===> p) ===> (Q ===> p).
+Proof.
+  simp.
+  excluded_middle P.
+  repeat rewrite guarded_true by propositional.
+  auto.
+  repeat rewrite guarded_false by propositional.
+  auto.
+Qed.
+
+Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
+    ~f a \in l
+    -> nth_error linvs a = Some I
+    -> (forall x y, f x = f y -> x = y)
+    -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in l \cup {f a})) ===> I)%sep linvs.
+Proof.
+  induct linvs; simplify.
+
+  cases a; simplify; equality.
+
+  cases a0; simplify.
+  invert H0.
+  rewrite guarded_true by sets.
+  rewrite guarded_false by sets.
+  cancel.
+  apply bigstar_impl.
+  simp.
+  apply guarded_impl.
+  sets.
+  apply H1 in H2.
+  equality.
+
+  apply (IHlinvs (fun n => f (S n))) in H0; auto.
+  rewrite H0.
+  cancel.
+  apply guarded_impl.
+  sets.
+  apply H1 in H3.
+  equality.
+  simp.
+  apply H1 in H2.
+  equality.
+Qed.
+
+Lemma lockChunks_lock : forall a l I linvs,
+    ~a \in l
+    -> nth_error linvs a = Some I
+    -> lockChunks l linvs ===> I * lockChunks (l \cup {a}) linvs.
+Proof.
+  simp.
+  apply lockChunks_lock' with (f := fun n => n); auto.
+Qed.  
+
+Lemma preservation : forall linvs {result} (c : cmd result) h l c' h' l',
+    step (h, l, c) (h', l', c')
+    -> forall P Q, hoare_triple linvs P c Q
+                   -> (P * lockChunks l linvs)%sep h
+                   -> exists P', hoare_triple linvs P' c' Q
+                                 /\ (P' * lockChunks l' linvs)%sep h'.
 Proof.
   induct 1; simplify.
 
   apply invert_Bind in H0; simp.
+  apply IHstep in H0; eauto.
+  simp.
   eauto.
-
+  
   apply invert_Bind in H; simp.
   specialize (invert_Return H); eauto using HtWeaken.
 
   apply invert_Loop in H; simp.
+  eexists; simp.
   econstructor.
-  eapply HtWeaken.
   eauto.
-  assumption.
   simp.
   cases r.
   apply HtReturn'.
-  unfold himp; simp; eauto.
+  auto.
   eapply HtStrengthen.
   eauto.
-  unfold himp; simp; eauto.
+  eauto.
+  eapply use_himp; try eassumption.
+  rewrite H1.
+  eauto.
 
   apply invert_Read in H0; simp.
+  assert ((exists v, a |-> v * (x v * lockChunks l' linvs))%sep h').
+  eapply use_himp; try eassumption.
+  rewrite H0.
+  cancel.
+  eapply ptsto_out in H2; eauto.
+  eexists; simp.
   apply HtReturn'.
-  assert ((exists v, a |-> v * x v)%sep h') by auto.
-  unfold exis, star in H1; simp.
-  unfold ptsto in H4; subst.
-  unfold split in H1; subst.
-  unfold heap1 in H.
-  rewrite lookup_join1 in H by (simp; sets).
-  unfold himp; simp.
-  invert H.
-  apply H2.
-  unfold star.
-  exists (heap1 a v), x2; propositional.
-  unfold split; reflexivity.
-  unfold ptsto; reflexivity.
+  eauto.
+  eapply use_himp; try eassumption.
+  cancel.
 
   apply invert_Write in H0; simp.
+  assert ((exists v, a |-> v * (x * lockChunks l' linvs))%sep h).
+  eapply use_himp; try eassumption.
+  rewrite H0.
+  cancel.
+  eapply ptsto_out in H2; eauto.
+  propositional.
+  eexists; simp.
   apply HtReturn'.
-  simp.
-  assert (((exists v : nat, a |-> v) * x)%sep h) by auto.
-  unfold star in H1; simp.
-  invert H4.
-  unfold ptsto in H5; subst.
-  unfold split in H3; subst.
-  unfold heap1 in H.
-  rewrite lookup_join1 in H by (simp; sets).
-  unfold himp; simp.
-  invert H.
-  apply H2.
-  unfold star.
-  exists ($0 $+ (a, v')), x1; propositional.
-  unfold split.
-  unfold heap1.
-  maps_equal.
-  rewrite lookup_join1 by (simp; sets).
-  simp.
-  repeat rewrite lookup_join2 by (simp; sets); reflexivity.
-  unfold disjoint in *; simp.
-  cases (a0 ==n a); simp.
-  apply H1 with (a0 := a).
-  unfold heap1; simp.
-  equality.
-  assumption.
-  unfold ptsto; reflexivity.
+  eauto.
+  eapply use_himp; try apply H5.
+  cancel.
 
   apply invert_Alloc with (r := a) in H0.
+  eexists; propositional.
   apply HtReturn'.
-  unfold himp; simp.
-  eapply himp_trans in H0; try apply zeroes_initialize.
-  auto.
-  assumption.
+  eassumption.
+  apply use_himp with ((P * lockChunks l' linvs) * a |--> zeroes numWords)%sep.
+  cancel.
+  apply use_himp with ((fun h' => h' = h) * a |--> zeroes numWords)%sep.
+  cancel.
+  eauto using specialize_hprop.
+  eapply use_himp.
+  apply zeroes_initialize; auto.
+  simp.
 
   apply invert_Free in H.
-  assert ((a |->? numWords * Q tt)%sep h) by auto.
+  eexists; propositional.
+  instantiate (1 := Q tt).
   apply HtReturn'.
-  unfold himp; simp.
-  eapply do_deallocate.
-  eauto.
-Qed.
-
-Lemma deallocate_None : forall a' numWords h a,
-    h $? a' = None
-    -> deallocate h a numWords $? a' = None.
-Proof.
-  induct numWords; simp.
-  rewrite IHnumWords; simp.
-  cases (a ==n a'); simp.
-Qed.
-
-Lemma preservation_finite : forall {result} (c : cmd result) h c' h' bound,
-    step (h, c) (h', c')
-    -> (forall a, a >= bound -> h $? a = None)
-    -> exists bound', forall a, a >= bound' -> h' $? a = None.
-Proof.
-  induct 1; simplify; eauto.
-
-  exists bound; simp.
-  cases (a ==n a0); simp.
-  rewrite H0 in H; equality.
   auto.
+  apply do_deallocate; simplify.
+  change (fun f => (Q tt * lockChunks l' linvs) f)%sep with (Q tt * lockChunks l' linvs)%sep.
+  eapply use_himp; try eassumption.
+  rewrite H.
+  cancel.
 
-  exists (max bound (a + numWords)); simp.
-  rewrite initialize_fresh; auto.
+  apply invert_Lock in H0.
+  simp.
+  eexists; propositional.
+  apply HtReturn'; auto.
+  eapply use_himp; try eassumption.
+  rewrite <- H3.
+  cancel.
+  apply lockChunks_lock; auto.
+Admitted.
 
-  exists bound; simp.
-  eauto using deallocate_None.
-Qed.
+Definition allLockChunks (linvs : list hprop) := bigstar (fun _ I => I) linvs.
 
-Hint Constructors step.
-
-Lemma progress : forall {result} (c : cmd result) P Q,
-    hoare_triple P c Q
-    -> forall h h1 h2, split h h1 h2
-                       -> disjoint h1 h2
-                       -> P h1
-                       -> (exists bound, forall a, a >= bound -> h $? a = None)
-                       -> (exists r, c = Return r)
-                          \/ (exists h' c', step (h, c) (h', c')).
+Lemma allLockChunks_lockChunks' : forall linvs (f : nat -> nat),
+   bigstar (fun _ I => I) linvs ===> bigstar (fun i I => (~f i \in {}) ===> I) linvs.
 Proof.
-  induct 1; simp;
-  repeat match goal with
-           | [ H : forall _ h1 _, _ -> _ -> ?P h1 -> _, H' : ?P _ |- _ ] => eapply H in H'; clear H; try eassumption; simp
-         end; eauto.
+  induct linvs; simp; auto.
 
-  invert H1.
-  right; exists h, (Return x0).
-  constructor.
-  unfold split, ptsto, heap1 in *; simp.
-  unfold star in H2; simp.
-  unfold split in H; simp.
-  rewrite lookup_join1; simp.
-  rewrite lookup_join1; simp.
-  sets.
-  eapply lookup_Some_dom.
-  rewrite lookup_join1; simp.
-  sets.
-
-  right; exists (h $+ (a, v')), (Return tt).
-  unfold split, exis, ptsto, heap1 in *; simp.
-  econstructor.
-  rewrite lookup_join1; simp.
-  sets.
-
-  unfold lift in H1; simp.
-  apply split_empty_fwd' in H; simp.
-  right; exists (initialize h2 x numWords), (Return x).
-  constructor.
-  simp; auto.
-
-  unfold star in H2; simp.
-  apply IHhoare_triple with (h := h) (h1 := x0) (h2 := h2 $++ x1); eauto.
-  unfold split in *; simp.
-  rewrite (@join_comm _ _ h2 x1).
-  apply join_assoc.
-  sets.
-  cases (h2 $? x2).
-  cases (x1 $? x2).
-  specialize (H2 x2).
-  specialize (H1 x2).
-  rewrite lookup_join2 in H1.
-  apply H1; equality.
-  unfold not.
-  simplify.
-  cases (x0 $? x2).
-  exfalso; apply H2; equality.
-  apply lookup_None_dom in Heq1; propositional.
-  apply lookup_None_dom in Heq0; propositional.
-  apply lookup_None_dom in Heq; propositional.
-
-  unfold split, disjoint in *; simp.
-  cases (h2 $? a).
-  rewrite lookup_join1 in H8.
-  apply H1 with (a := a); auto.
-  rewrite lookup_join1; auto.
-  cases (x0 $? a); try equality.
-  eauto using lookup_Some_dom.
-  eauto using lookup_Some_dom.
-  rewrite lookup_join2 in H8; eauto.
-  eauto using lookup_None_dom.
+  rewrite guarded_true by sets.
+  rewrite IHlinvs.
+  cancel.
 Qed.
 
-Lemma hoare_triple_sound' : forall P {result} (c : cmd result) Q,
-    hoare_triple P c Q
-    -> P $0
-    -> invariantFor (trsys_of $0 c)
+Lemma allLockChunks_lockChunks : forall linvs,
+    allLockChunks linvs ===> lockChunks {} linvs.
+Proof.
+  simp.
+  apply allLockChunks_lockChunks' with (f := fun n => n).
+Qed.
+
+Lemma hoare_triple_sound' : forall linvs P {result} (c : cmd result) Q,
+    hoare_triple linvs P c Q
+    -> forall h, (P * allLockChunks linvs)%sep h
+    -> invariantFor (trsys_of h {} c)
                     (fun p =>
-                       (exists bound, forall a, a >= bound -> fst p $? a = None)
-                       /\ hoare_triple (fun h' => h' = fst p)
-                                       (snd p)
-                                       Q).
+                       let '(h, l, c) := p in
+                       exists P', hoare_triple linvs P' c Q
+                                  /\ (P' * lockChunks l linvs)%sep h).
 Proof.
   simplify.
 
   apply invariant_induction; simplify.
 
   propositional; subst; simplify.
-  exists 0; simp.
-  eapply HtWeaken; eauto.
-  unfold himp; simplify; equality.
+  eexists; propositional.
+  eauto.
+  eapply use_himp; try eassumption.
+  rewrite allLockChunks_lockChunks.
+  auto.
 
   cases s.
+  cases p.
   cases s'.
+  cases p.
   simp.
-  eauto using preservation_finite.
   eauto using preservation.
 Qed.
 
-Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q,
-    hoare_triple P c Q
-    -> P $0
-    -> invariantFor (trsys_of $0 c)
-                    (fun p => (exists r, snd p = Return r)
-                              \/ (exists p', step p p')).
+Fixpoint notAboutToFail {result} (c : cmd result) :=
+  match c with
+  | Fail _ => false
+  | Bind _ _ c1 _ => notAboutToFail c1
+  | Par c1 c2 => notAboutToFail c1 && notAboutToFail c2
+  | _ => true
+  end.
+
+Lemma hoare_triple_notAboutToFail : forall linvs P result (c : cmd result) Q,
+    hoare_triple linvs P c Q
+    -> notAboutToFail c = false
+    -> P ===> [| False |].
+Proof.
+  induct 1; simp; try equality; eauto using himp_trans.
+
+  apply andb_false_iff in H1; propositional.
+  rewrite H1; cancel.
+  rewrite H1; cancel.
+
+  rewrite H1; cancel.
+Qed.
+
+Lemma False_star : forall p,
+    [| False |] * p ===> [| False |].
+Proof.
+  cancel.
+Qed.
+
+Theorem hoare_triple_sound : forall linvs P {result} (c : cmd result) Q,
+    hoare_triple linvs P c Q
+    -> forall h, (P * allLockChunks linvs)%sep h
+    -> invariantFor (trsys_of h {} c)
+                    (fun p => let '(_, _, c) := p in
+                              notAboutToFail c = true).
 Proof.
   simplify.
 
   eapply invariant_weaken.
   eapply hoare_triple_sound'; eauto.
   simp.
-  specialize (progress H3); simplify.
-  specialize (H2 (fst s) (fst s) $0).
-  assert (split (fst s) (fst s) $0) by auto.
-  assert (disjoint (fst s) $0) by auto.
-  assert (exists bound, forall a, a >= bound -> fst s $? a = None) by eauto.
-  cases s; simp; eauto.
-Qed.
-
-(* Fancy theorem to help us rewrite within preconditions and postconditions *)
-Instance hoare_triple_morphism : forall A,
-  Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple A).
-Proof.
-  Transparent himp.
-  repeat (hnf; intros).
-  unfold pointwise_relation in *; intuition subst.
-
-  eapply HtConsequence; eauto.
-  rewrite H; reflexivity.
-  intros.
-  hnf in H1.
-  specialize (H1 r _ eq_refl).
-  rewrite H1; reflexivity.
-
-  eapply HtConsequence; eauto.
-  rewrite H; reflexivity.
-  intros.
-  hnf in H1.
-  specialize (H1 r _ eq_refl).
-  rewrite H1; reflexivity.
-  Opaque himp.
-Qed.
-
-
-(** * Examples *)
-
-Opaque heq himp lift star exis ptsto.
-
-(* Here comes some automation that we won't explain in detail, instead opting to
- * use examples. *)
-
-Theorem use_lemma : forall result P' (c : cmd result) (Q : result -> hprop) P R,
-  hoare_triple P' c Q
-  -> P ===> P' * R
-  -> hoare_triple P c (fun r => Q r * R)%sep.
-Proof.
+  cases s.
+  cases p.
   simp.
-  eapply HtWeaken.
-  eapply HtFrame.
-  eassumption.
-  eauto.
-Qed.
-
-Theorem HtRead' : forall a v,
-  hoare_triple (a |-> v)%sep (Read a) (fun r => a |-> v * [| r = v |])%sep.
-Proof.
-  simp.
-  apply HtWeaken with (exists r, a |-> r * [| r = v |])%sep.
-  eapply HtStrengthen.
-  apply HtRead.
-  simp.
-  cancel; auto.
-  subst; cancel.
-  cancel; auto.
-Qed.
-
-Theorem HtRead'' : forall p P R,
-  P ===> (exists v, p |-> v * R v)
-  -> hoare_triple P (Read p) (fun r => p |-> r * R r)%sep.
-Proof.
-  simp.
-  eapply HtWeaken.
-  apply HtRead.
-  assumption.
-Qed.
-
-Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree.
-
-Ltac step0 := basic || eapply HtBind || (eapply use_lemma; [ basic | cancel; auto ])
-              || (eapply use_lemma; [ eapply HtRead' | solve [ cancel; auto ] ])
-              || (eapply HtRead''; solve [ cancel ])
-              || (eapply HtStrengthen; [ eapply use_lemma; [ basic | cancel; auto ] | ])
-              || (eapply HtConsequence; [ apply HtFail | .. ]).
-Ltac step := step0; simp.
-Ltac ht := simp; repeat step.
-Ltac conseq := simplify; eapply HtConsequence.
-Ltac use_IH H := conseq; [ 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.
-Ltac use H := (eapply use_lemma; [ eapply H | cancel; auto ])
-              || (eapply HtStrengthen; [ eapply use_lemma; [ eapply H | cancel; auto ] | ]).
-
-Ltac heq := intros; apply himp_heq; split.
-
-(* That's the end of the largely unexplained automation.  Let's prove some
- * programs! *)
-
-
-(** ** Swapping with two pointers *)
-
-Definition swap p q :=
-  tmpp <- Read p;
-  tmpq <- Read q;
-  _ <- Write p tmpq;
-  Write q tmpp.
-
-(* Looking at the precondition here, note how we no longer work with explicit
- * functions over heaps.  All that is hidden within the assertion language.
- * Also note that the definition of [*] gives us nonaliasing of [p] and [q] for
- * free! *)
-Theorem swap_ok : forall p q a b,
-  {{p |-> a * q |-> b}}
-    swap p q
-  {{_ ~> p |-> b * q |-> a}}.
-Proof.
-  unfold swap.
-  (* [simp] is our generic simplifier for this file. *)
-  simp.
-  (* We generally just keep calling [step] to advance forward by one atomic
-   * statement. *)
-  step.
-  step.
-  (* We do often want to use [simp] to clean up the goal after [step] infers an
-   * intermediate assertion. *)
-  simp.
-  step.
-  step.
-  simp.
-  step.
-  step.
-  simp.
-  step.
-  (* The [cancel] procedure repeatedly finds matching subformulas on the two
-   * sides of [===>], removing them and recurring, possibly learning the values
-   * of some unification variables each time. *)
-  cancel.
-  subst.
+  cases (notAboutToFail c0); auto.
+  eapply hoare_triple_notAboutToFail in Heq; eauto.
+  apply use_himp with (Q := [| False |]%sep) in H3.
+  invert H3; propositional.
+  rewrite Heq.
   cancel.
 Qed.
-
-Opaque swap.
-(* This command prevents later proofs from peeking inside the implementation of
- * [swap].  Instead, we only reason about it through [swap_ok]. *)
-
-(* Two swaps in a row provide a kind of rotation across three addresses. *)
-Definition rotate p q r :=
-  _ <- swap p q;
-  swap q r.
-
-Theorem rotate_ok : forall p q r a b c,
-  {{p |-> a * q |-> b * r |-> c}}
-    rotate p q r
-  {{_ ~> p |-> b * q |-> c * r |-> a}}.
-Proof.
-  unfold rotate.
-  simp.
-  step.
-  (* Now we invoke our earlier theorem by name.  Note that its precondition only
-   * matches a subset of our current precondition.  The rest of state is left
-   * alone, which we can prove "for free" by the frame rule. *)
-  use swap_ok.
-  simp.
-  use swap_ok.
-  simp.
-  cancel.
-Qed.
-
-Opaque rotate.
-
-(** ** Initializing a fresh object *)
-
-Definition init :=
-  p <- Alloc 2;
-  _ <- Write p 7;
-  _ <- Write (p+1) 8;
-  Return p.
-
-Theorem init_ok :
-  {{emp}}
-    init
-  {{p ~> p |--> [7; 8]}}.
-Proof.
-  unfold init.
-  simp.
-  step.
-  step.
-  simp.
-  step.
-  step.
-  simp.
-  step.
-  step.
-  simp.
-  step.
-  cancel.
-Qed.
-
-Opaque init.
-
-Theorem the_circle_of_life_ok :
-  {{emp}}
-    p <- init;
-    Free p 2
-  {{_ ~> emp}}.
-Proof.
-  step.
-  use init_ok.
-  simp.
-  step.
-  cancel.
-Qed.
-
-Theorem ultra_combo_ok :
-  {{emp}}
-    p <- init;
-    _ <- swap p (p+1);
-    Return p
-  {{p ~> p |--> [8; 7]}}.
-Proof.
-  step.
-  use init_ok.
-  simp.
-  step.
-  use swap_ok.
-  simp.
-  step.
-  cancel.
-Qed.
-
-(** ** In-place reversal of a singly linked list *)
-
-(* Let's give a recursive definition of how a linked list should be laid out in
- * memory. *)
-Fixpoint linkedList (p : nat) (ls : list nat) :=
-  match ls with
-    | nil => [| p = 0 |]
-      (* An empty list is associated with a null pointer and no memory
-       * contents. *)
-    | x :: ls' => [| p <> 0 |]
-                  * exists p', p |--> [x; p'] * linkedList p' ls'
-      (* A nonempty list is associated with a nonnull pointer and a two-cell
-       * struct, which points to a further list. *)
-  end%sep.
-
-(* The definition of [linkedList] is recursive in the list.  Let's also prove
- * lemmas for simplifying [linkedList] invocations based on values of [p]. *)
-
-Theorem linkedList_null : forall ls,
-  linkedList 0 ls === [| ls = nil |].
-Proof.
-  (* Tactic [heq] breaks an equivalence into two implications. *)
-  heq; cases ls; cancel.
-Qed.
-
-Theorem linkedList_nonnull : forall p ls,
-  p <> 0
-  -> linkedList p ls === exists x ls' p', [| ls = x :: ls' |] * p |--> [x; p'] * linkedList p' ls'.
-Proof.
-  heq; cases ls; cancel; match goal with
-                         | [ H : _ = _ :: _ |- _ ] => invert H
-                         end; cancel.
-Qed.
-
-Hint Rewrite <- rev_alt.
-Hint Rewrite rev_involutive.
-
-(* Let's hide the definition of [linkedList], so that we *only* reason about it
- * via the two lemmas we just proved. *)
-Opaque linkedList.
-
-(* In-place linked-list reverse, the "hello world" of separation logic! *)
-Definition reverse p :=
-  pr <- for pr := (p, 0) loop
-    let (p, r) := pr in
-    if p ==n 0 then
-      Return (Done pr)
-    else
-      tmp <- Read (p + 1);
-      _ <- Write (p+1) r;
-      Return (Again (tmp, p))
-  done;
-  Return (snd pr).
-
-(* Helper function to peel away the [Done]/[Again] status of a [loop_outcome] *)
-Definition valueOf {A} (o : loop_outcome A) :=
-  match o with
-  | Done v => v
-  | Again v => v
-  end.
-
-Theorem reverse_ok : forall p ls,
-  {{linkedList p ls}}
-    reverse p
-  {{r ~> linkedList r (rev ls)}}.
-Proof.
-  unfold reverse.
-  simp.
-  step.
-  (* When we reach a loop, we give the invariant with a special tactic. *)
-  loop_inv (fun o => exists ls1 ls2, [| ls = rev_append ls1 ls2 |]
-                                     * linkedList (fst (valueOf o)) ls2
-                                     * linkedList (snd (valueOf o)) ls1
-                                     * [| match o with
-                                          | Done (p, _) => p = 0
-                                          | _ => True
-                                          end |])%sep.
-  cases (a ==n 0); simp.
-  step.
-  cancel.
-  step.
-  (* We use [setoid_rewrite] for rewriting under binders ([exists], in this
-   * case).  Note that we also specify hypothesis [n] explicitly, since
-   * [setoid_rewrite] isn't smart enough to infer parameters otherwise. *)
-  setoid_rewrite (linkedList_nonnull _ n).
-  step.
-  simp.
-  step.
-  step.
-  simp.
-  step.
-  setoid_rewrite (linkedList_nonnull _ n).
-  cancel.
-  simp.
-  setoid_rewrite linkedList_null.
-  cancel.
-  equality.
-  simp.
-  step.
-  cancel.
-  simp.
-  setoid_rewrite linkedList_null.
-  cancel.
-  simp.
-  cancel.
-Qed.
-
-Opaque reverse.
-
-(* ** Calling [reverse] twice, to illustrate the *frame rule* *)
-
-Theorem reverse_two_ok : forall p1 ls1 p2 ls2,
-  {{linkedList p1 ls1 * linkedList p2 ls2}}
-    p1 <- reverse p1;
-    p2 <- reverse p2;
-    Return (p1, p2)
-  {{ps ~> linkedList (fst ps) (rev ls1) * linkedList (snd ps) (rev ls2)}}.
-Proof.
-  simp.
-  step.
-  use reverse_ok.
-  simp.
-  step.
-  use reverse_ok.
-  simp.
-  step.
-  cancel.
-Qed.
-(* Note that the intuitive correctness theorem would be *false* for lists
- * sharing any cells in common!  The inherent disjointness of [*] saves us from
- * worrying about those cases. *)
-
-
-(* ** Computing the length of a linked list *)
-
-(* To state a good loop invariant, it will be helpful to define
- * *list segments* that end with some pointer beside null. *)
-Fixpoint linkedListSegment (p : nat) (ls : list nat) (q : nat) :=
-  match ls with
-    | nil => [| p = q |]
-    | x :: ls' => [| p <> 0 |] * exists p', p |-> x * (p+1) |-> p' * linkedListSegment p' ls' q
-  end%sep.
-
-(* Next, two [linkedListSegment] lemmas analogous to those for [linkedList]
- * above *)
-
-Lemma linkedListSegment_empty : forall p ls,
-  linkedList p ls ===> linkedList p ls * linkedListSegment p nil p.
-Proof.
-  cancel.
-Qed.
-
-Lemma linkedListSegment_append : forall q r x ls p,
-  q <> 0
-  -> linkedListSegment p ls q * q |-> x * (q+1) |-> r ===> linkedListSegment p (ls ++ x :: nil) r.
-Proof.
-  induct ls; cancel; auto.
-  subst; cancel.
-  rewrite <- IHls; cancel; auto.
-Qed.
-
-(* One more [linkedList] lemma will be helpful.  We'll re-reveal the predicate's
- * definition to prove the lemma. *)
-
-Transparent linkedList.
-
-Lemma linkedListSegment_null : forall ls p,
-  linkedListSegment p ls 0 ===> linkedList p ls.
-Proof.
-  induct ls; cancel; auto.
-Qed.
-
-Opaque linkedList linkedListSegment.
-
-(* A few algebraic properties of list operations: *)
-Hint Rewrite <- app_assoc.
-Hint Rewrite app_length app_nil_r.
-
-(* We tie a few of them together into this lemma. *)
-Lemma move_along : forall A (ls : list A) x2 x1 x0 x,
-  ls = x2 ++ x1
-  -> x1 = x0 :: x
-  -> ls = (x2 ++ [x0]) ++ x.
-Proof.
-  simp.
-Qed.
-
-Hint Resolve move_along.
-
-Theorem length_ok : forall p ls,
-  {{linkedList p ls}}
-    q_len <- for q_len := (p, 0) loop
-      let (q, len) := q_len in
-      if q ==n 0 then
-        Return (Done q_len)
-      else
-        tmp <- Read (q + 1);
-        Return (Again (tmp, len+1))
-    done;
-    Return (snd q_len)
-  {{len ~> linkedList p ls * [| len = length ls |]}}.
-Proof.
-  simp.
-  step.
-  loop_inv (fun o => exists ls1 ls2, [| ls = ls1 ++ ls2 |]
-                                     * linkedListSegment p ls1 (fst (valueOf o))
-                                     * linkedList (fst (valueOf o)) ls2
-                                     * [| snd (valueOf o) = length ls1 |]
-                                     * [| match o with
-                                          | Done (q, _) => q = 0 /\ ls2 = nil
-                                          | _ => True
-                                          end |])%sep.
-  cases (a ==n 0); simp.
-  step.
-  setoid_rewrite linkedList_null.
-  cancel.
-  step.
-  setoid_rewrite (linkedList_nonnull _ n).
-  step.
-  simp.
-  step.
-  cancel.
-  eauto.
-  simp.
-  setoid_rewrite <- linkedListSegment_append.
-  cancel.
-  auto.
-  rewrite linkedListSegment_empty.
-  cancel.
-  simp.
-  step.
-  cancel.
-  simp.
-  simp.
-  rewrite linkedListSegment_null.
-  rewrite linkedList_null.
-  cancel.
-Qed.
-*)