diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index 36551a8817949a205a8e94ac5064d7ab5dba2c7b..b6d99b4b5ad3021eed2d66f5ba1e856eb1c68a59 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -310,13 +310,6 @@ Section proof.
 
   Opaque integer_hash const size.
 
-  Lemma half_join : (1/2 ⋅ 1/2 = 1)%Qp.
-  Proof.
-    unfold op, cmra_op; simpl.
-    unfold frac_op.
-    apply Qp_div_2.
-  Qed.
-
   Definition log0 : gmap nat Z := <[O:=0]>∅.
 
   Lemma log0_lookup : forall i x, log0 !! i = Some x -> i = O /\ x = 0.
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 78f141bcbbfb3bb67a35c750a2e1ed4426704838..f18fe8195f96d41b24904032edc4e647920ada71 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -35,10 +35,10 @@ Qed.
 
 Program Definition write : val := @RecV <> "n" (λ: "in",
   let: "v" := ["n" + #version]_at in
-  ["n" + #version]_at <- "v" + #1;;
+  ["n" + #version]_at <- ("v" + #1);;
   (for: ("i" := #0; "i" < #8; "i" + #1)
           ["n" + #data + "i"]_at <- ["in" + "i"]_na);;
-  ["n" + #version]_at <- "v" + #2) _.
+  ["n" + #version]_at <- ("v" + #2)) _.
 Next Obligation.
 Proof.
   apply I.
@@ -95,7 +95,18 @@ Proof.
     by rewrite Max.max_r.
 Qed.
 
-Definition log_latest {A} (m : gmap nat A) n v := m !! n = Some v /\ forall n', (n < n')%nat -> m !! n' = None.
+Definition log_latest {A} (m : gmap nat A) n v := m !! n = Some v /\
+  forall n', is_Some (m !! n') <-> even n' = true /\ (n' <= n)%nat.
+
+Lemma log_latest_even {A} (m : gmap nat A) n v: log_latest m n v -> even n = true.
+Proof.
+  intros [Hn Hdom].
+  apply Hdom; rewrite Hn; eauto.
+Qed.
+
+
+Definition map_size {A B} `{EqDecision A} `{Countable A} (m : gmap A (list B)) n :=
+  map_Forall (fun k a => length a = n) m.
 
 (* The existing version of this requires A to be a cmra, which is completely unnecessary. *)
 Global Instance list_unit {A} : Unit (list A) := nil.
@@ -116,18 +127,21 @@ Section Interpretation.
   *)
 
   Definition dataP' n versionP : interpC Σ histProtocol := (fun _ _ s v =>
-    ∃ ver, ⌜even ver = true /\ log_latest s ver v⌝ ∗ [XP (ZplusPos version n) in (ver - 1)%nat | versionP]_R)%I.
+    ∃ ver, ⌜log_latest s ver v⌝ ∗ [XP (ZplusPos version n) in (ver - 1)%nat | versionP]_R)%I.
 
 (*  Definition versionP_fun version locs γ : (nat -> Z -> vProp Σ) -> (nat -> Z -> vProp Σ) := (λ R s v,
       ⌜(Z.of_nat s = v)%Z⌝ ∗ ∃ L : gmap nat (list Z), ⌜∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
       ⎡@own _ _ histG γ (Snapshot L)⎤ ∗
       [∗ list] i↦x ∈ locs, [XP x in (fun l => nth i l 0) <$> L | dataP' version (fun _ _ => R)]_R)%I.*)
 
+  Definition map_nth {A} i (m : gmap nat (list A)) d := (λ l, nth i l d) <$> m.
+  
   Definition versionP_fun n γ : interpC Σ versionProtocol -> interpC Σ versionProtocol := (λ R _ _ s v,
-      ⌜(Z.of_nat s = v)%Z⌝ ∗ ∃ L : gmap nat (list Z), ⌜∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
+      ⌜(Z.of_nat s = v)%Z⌝ ∗
+      ∃ L : gmap nat (list Z), ⌜map_size L 8 /\ ∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
       ⎡@own _ _ histG γ (Snapshot L)⎤ ∗
       [∗ list] i ∈ seq 0 8,
-        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in (fun l => nth i l 0) <$> L | dataP' n R]_R)%I.
+        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in map_nth i L 0 | dataP' n R]_R)%I.
 
   Instance versionP_contractive n γ : Contractive (versionP_fun n γ).
   Proof.
@@ -150,19 +164,21 @@ Section Interpretation.
   Definition dataP n γ := dataP' n (versionP n γ).
   
   Lemma versionP_eq' n γ: versionP n γ ≡ (fun _ _ s v =>
-      ⌜(Z.of_nat s = v)%Z⌝ ∗ ∃ L : gmap nat (list Z), ⌜∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
+    ⌜(Z.of_nat s = v)%Z⌝ ∗
+    ∃ L : gmap nat (list Z), ⌜map_size L 8 /\ ∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
       ⎡@own _ _ histG γ (Snapshot L)⎤ ∗
       [∗ list] i ∈ seq 0 8,
-        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in (fun l => nth i l 0) <$> L | dataP n γ]_R)%I.
+        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in map_nth i L 0 | dataP n γ]_R)%I.
   Proof.
     by rewrite /versionP fixpoint_unfold.
   Qed.
 
   Lemma versionP_eq n γ b l s v: versionP n γ b l s v ≡
-     (⌜(Z.of_nat s = v)%Z⌝ ∗ ∃ L : gmap nat (list Z), ⌜∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
+      (⌜(Z.of_nat s = v)%Z⌝ ∗
+      ∃ L : gmap nat (list Z), ⌜map_size L 8 /\ ∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌝ ∗
       ⎡@own _ _ histG γ (Snapshot L)⎤ ∗
       [∗ list] i ∈ seq 0 8,
-        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in (fun l => nth i l 0) <$> L | dataP n γ]_R)%I.
+        [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in map_nth i L 0 | dataP n γ]_R)%I.
   Proof.
     apply versionP_eq'.
   Qed.
@@ -188,16 +204,17 @@ Section proof.
 
   (* The collection of protocol assertions that describes a stable state of the node. *)
   Definition node_state_R L v n g :=
-    (⌜even v = true /\ exists vs, log_latest L v vs⌝ ∗
+    (⌜map_size L 8 /\ exists vs, log_latest L v vs⌝ ∗
      [XP (ZplusPos version n) in v | versionP n g]_R ∗ ⎡@own _ _ histG g (Snapshot L)⎤ ∗
      [∗ list] i ∈ seq 0 8,
-       [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in (fun l => nth i l 0) <$> L | dataP n g]_R)%I.
+       [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in map_nth i L 0 | dataP n g]_R)%I.
 
   Definition node_state_W L v n g :=
-    (⌜even v = true /\ exists vs, log_latest L v vs⌝ ∗
-     [XP (ZplusPos version n) in v | versionP n g]_W ∗ ⎡@own _ _ histG g (Master (1/2) L)⎤ ∗
+    (⌜map_size L 8 /\ exists vs, log_latest L v vs⌝ ∗
+     [XP (ZplusPos version n) in v | versionP n g]_W ∗
+     ⎡@own _ _ histG g (@Master _ (gmap_unit(A := list.listC ZC)) (1/2) L)⎤ ∗
      [∗ list] i ∈ seq 0 8,
-       [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in (fun l => nth i l 0) <$> L | dataP n g]_W)%I.
+       [XP (ZplusPos (Z.of_nat i) (ZplusPos data n)) in map_nth i L 0 | dataP n g]_W)%I.
 
   Ltac wp_rec' := lazymatch goal with |-context[Rec ?f ?x ?e] => let H := fresh "Hclosed" in
     assert (Closed (f :b: x :b: nil) e) as H by apply I; wp_rec; clear H;
@@ -250,81 +267,628 @@ Section proof.
 
   Opaque seq.
   
-  Lemma read_spec n out L0 v0 g: atomic_wp
-    (λ L, ⎡PSCtx⎤ ∗ node_state_R L0 v0 n g ∗ ([∗ list] i ∈ seq 0 8, ZplusPos (Z.of_nat i) out ↦ ?) ∗
-                       ⎡own g (Master (1/2) L)⎤)%I
-    (λ L val, ⌜val = #()⌝ ∗ ∃ v vals, ⌜length vals = 8%nat /\ (v0 <= v)%nat /\ L0 ⊆ L /\ L !! v = Some vals⌝ ∗
-          node_state_R (<[v := vals]>L0) v n g ∗ ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) out ↦ x) ∗
+  Lemma log_latest_ord: ∀ m1 m2 n1 n2 v1 v2, m1 ⊑ m2 -> log_latest m1 n1 v1 -> log_latest m2 n2 v2 ->
+                                             (n1 <= n2)%nat.
+  Proof.
+    intros ??????? [Hn1] [? Hn2].
+    eapply lookup_weaken in Hn1; last eauto.
+    apply Hn2; rewrite Hn1; eauto.
+  Qed.
+
+  Lemma Nat2Z_inj_even: ∀ a, Z.even (Z.of_nat a) = even a.
+  Proof.
+    induction a; auto.
+    by rewrite Nat2Z.inj_succ Nat.even_succ Z.even_succ Zodd_even_bool IHa Nat.negb_even.
+  Qed.
+ 
+  Lemma mod_even: ∀ a : nat, (a mod 2 = if even a then 0 else 1)%nat.
+  Proof.
+    intro; apply Nat2Z.inj.
+    rewrite Z2Nat_inj_mod Zmod_even Nat2Z_inj_even.
+    destruct (even a); auto.
+  Qed.
+  
+  Lemma fmap_nth_log_latest : ∀ {A} m n (v : list A) i d, log_latest m n v ->
+    log_latest (map_nth i m d) n (nth i v d).
+  Proof.
+    unfold log_latest; intros.
+    rewrite lookup_fmap.
+    destruct H as [-> H]; split; auto.
+    intros; rewrite lookup_fmap -H.
+    rewrite !is_Some_alt; destruct (m !! n'); done.
+  Qed.
+
+  Require Import Recdef.
+   
+  Function make_log {A} (n : nat) (d : A) { measure id n } : gmap nat A :=
+    <[n := d]>match n with O => ∅ | _ => (make_log (n - 2) d) end.
+  Proof.
+    intros; simpl; omega.
+  Qed.
+  Arguments make_log {_} _ _.
+
+  Lemma log_latest_insert {A} m n (v v' : A): log_latest m n v -> log_latest (<[(n+2)%nat := v']>m) (n + 2) v'.
+  Proof.
+    intro H.
+    pose proof (log_latest_even _ _ _ H) as Heven.
+    destruct H as [Hn Hin].
+    split; first apply lookup_insert.
+    intros; destruct (decide (n' = n + 2)%nat).
+    - subst; rewrite lookup_insert Nat.even_add Heven; split; eauto.
+    - rewrite lookup_insert_ne; last done.
+      rewrite Hin.
+      split; intros []; split; auto; try omega.
+      destruct (decide (n' = n + 1)%nat); last omega.
+      subst; rewrite Nat.even_add Heven in H; done.
+  Qed.
+  
+  Lemma make_log_latest {A} (n : nat) (d : A): even n = true -> log_latest (make_log n d) n d.
+  Proof.
+    functional induction (make_log n d); intros.
+    - split; first apply lookup_insert.
+      intros; destruct (decide (n' = O)).
+      + subst; rewrite lookup_insert; split; eauto.
+      + rewrite lookup_insert_ne; last done.
+        rewrite lookup_empty; split; intros []; [done | omega].
+    - assert (n = (n - 2) + 2)%nat as Heq.
+      { rewrite Nat.sub_add; first done.
+        destruct n; first done.
+        destruct n; [done | omega]. }
+      rewrite {1 3}Heq.
+      eapply log_latest_insert, IHg.
+      rewrite Heq Nat.even_add in H.
+      destruct (Nat.even (n - 2)); auto.
+  Qed.
+
+  Lemma make_log_lookup {A} n (d : A) n' x: make_log n d !! n' = Some x -> x = d.
+  Proof.
+    functional induction (make_log n d).
+    - destruct (decide (n' = O)).
+      + subst; rewrite lookup_insert; congruence.
+      + rewrite lookup_insert_ne; last done.
+        rewrite lookup_empty; done.
+    - destruct (decide (n' = n)).
+      + subst; rewrite lookup_insert; congruence.
+      + rewrite lookup_insert_ne; done.
+  Qed.
+
+  Definition map_app {A B} `{Countable A} `{EqDecision A} (m1 : gmap A (list B)) (m2 : gmap A B) := merge
+    (fun a b => match a, b with Some l, Some x => Some (l ++ x :: nil)%list | _, _ => None end) m1 m2.
+
+  Lemma map_app_latest {A} m1 m2 n vs (v : A): log_latest m1 n vs -> log_latest m2 n v ->
+                                               log_latest (map_app m1 m2) n (vs ++ v :: nil)%list.
+  Proof.
+    intros [Hn1 Hin1] [Hn2 Hin2]; split.
+    - unfold map_app; erewrite lookup_merge, Hn1, Hn2; done.
+    - intros; unfold map_app; erewrite lookup_merge by done.
+      specialize (Hin1 n'); specialize (Hin2 n').
+      destruct (m1 !! n'); last done.
+      destruct (m2 !! n').
+      + split; eauto.
+        intro; apply Hin2; eauto.
+      + split; first by intros [].
+        intro H; apply Hin2 in H as []; done.
+  Qed.
+
+  Lemma nth_snoc {A} i l (x : A) d: nth i (l ++ x :: nil) d = if decide (i = length l) then x else nth i l d.
+  Proof.
+    destruct (decide (i < length l)); [rewrite app_nth1 | rewrite app_nth2]; try omega;
+      destruct (decide _); auto; try omega.
+    - subst; rewrite minus_diag; auto.
+    - rewrite !nth_overflow; auto; simpl; omega.
+  Qed.
+  
+  Lemma map_nth_app {A} m1 n m2 i (d : A) (Hm1: map_size m1 n)
+    (Hdom: map_relation (fun _ _ => true) (fun _ => false) (fun _ => false) m1 m2):
+    map_nth i (map_app m1 m2) d = if decide (i = n) then m2 else map_nth i m1 d.
+  Proof.
+    apply map_eq; intro j.
+    rewrite lookup_fmap.
+    unfold map_app; erewrite lookup_merge; last done.
+    specialize (Hdom j).
+    destruct (m1 !! j) eqn: Hj1, (m2 !! j) eqn: Hj2; try done.
+    - specialize (Hm1 _ _ Hj1); simpl in Hm1; subst.
+      simpl; rewrite nth_snoc.
+      destruct (decide _); first done.
+      rewrite lookup_fmap Hj1; done.
+    - destruct (decide _); first done.
+      rewrite lookup_fmap Hj1; done.
+  Qed.    
+    
+  Lemma log_latest_comprehend: forall n g l L0 v vals, even v = true ->
+    (([∗ list] i↦x ∈ vals, ∃ Li, ⌜log_latest Li v x ∧ map_nth i L0 0 ⊆ Li⌝ ∗ [XP ZplusPos i l in Li | dataP n g ]_R) -∗ ∃ L, ⌜map_size L (length vals) /\ log_latest L v vals ∧
+          ∀ i, (i < length vals)%nat -> map_nth i L0 0 ⊆ map_nth i L 0⌝ ∗
+      ([∗ list] i↦_ ∈ vals, [XP ZplusPos i l in map_nth i L 0 | dataP n g ]_R))%I.
+  Proof.
+    intros; induction vals using rev_ind; simpl; iIntros "H".
+    { iExists (make_log v nil); iFrame; iPureIntro.
+      split; last by (split; [apply make_log_latest | intros; omega]).
+      intros ???%make_log_lookup; subst; auto. }
+    rewrite big_sepL_app; simpl.
+    iDestruct "H" as "(H & Hi & _)".
+    iPoseProof (IHvals with "H") as (L) "[(% & % & %) H]".
+    iDestruct "Hi" as (Li) "[[%%] Hi]".
+    iExists (map_app L Li).
+    assert (map_relation (fun _ _ => true) (fun _ => false) (fun _ => false) L Li).
+    { intro j.
+      destruct H1 as [_ HL]; destruct H3 as [_ HLi].
+      specialize (HL j); specialize (HLi j).
+      rewrite <-HL, !is_Some_alt in HLi.
+      destruct (L !! j), (Li !! j); try done; tauto. }
+    iSplit.
+    - iPureIntro; split; last split.
+      + intros ??; unfold map_app; erewrite lookup_merge by done.
+        destruct (L !! i) eqn: HL; last done.
+        destruct (Li !! i) eqn: HLi; last done.
+        specialize (H0 _ _ HL); simpl in H0.
+        intro X; inversion X.
+        rewrite !app_length; simpl; omega.
+      + by apply map_app_latest.
+      + intro; rewrite app_length /= => ?.
+        intros; erewrite map_nth_app; eauto.
+        rewrite Nat.add_0_r in H4.
+        destruct (decide _); first by subst.
+        apply H2; omega.
+    - rewrite big_sepL_app; simpl.
+      erewrite Nat.add_0_r, map_nth_app; eauto.
+      rewrite decide_True; last done; iFrame.
+      iApply big_sepL_mono; last done.
+      intros ???%lookup_lt_Some; simpl; erewrite map_nth_app; try eassumption.
+      destruct (decide _); auto; omega.
+  Qed.      
+  
+  Lemma node_state_ord L1 L2 v1 v2 n g E (Hv: (v1 ≤ v2)%nat) (HE: ↑persist_locN ⊆ E):
+   (⌜map_size L1 8 ∧ (∃ vs, log_latest L1 v1 vs)⌝ ∗
+    ([∗ list] i ∈ seq 0 8, [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in map_nth i L1 0 | dataP n g ]_R) -∗
+    ⌜map_size L2 8 ∧ (∃ vs, log_latest L2 v2 vs)⌝ ∗
+    ([∗ list] i ∈ seq 0 8, [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in map_nth i L2 0 | dataP n g ]_R) ={E}=∗
+    ⌜L1 ⊆ L2⌝)%I.
+  Proof.
+    iIntros "[% H1] [% H2]".
+    iCombine "H1 H2" as "H"; rewrite -big_sepL_sepL.
+    iPoseProof (big_sepL_mono with "H") as "H".
+    { intros; simpl.
+      iApply GPS_SW_Readers_agree.
+      etrans; [apply namespaces.nclose_subseteq | done]. }
+    rewrite fupd_big_sepL; iMod "H"; iModIntro.
+    rewrite big_sepL_forall.
+    iDestruct "H" as "%"; simpl in *; iPureIntro.
+    intro i.
+    destruct (L1 !! i) eqn: HL1, (L2 !! i) eqn: HL2; try done; simpl.
+    - destruct H as [Hsize1 _], H0 as [Hsize2 _].
+      specialize (Hsize1 _ _ HL1); specialize (Hsize2 _ _ HL2); simpl in *.
+      eapply list_eq_same_length; eauto; intros.
+      specialize (H1 _ _ (lookup_seq _ _ _ H)).
+      destruct H1 as [Hsub | Hsub]; last symmetry; eapply lookup_weaken_inv; try eapply Hsub;
+        unfold map_nth; erewrite lookup_fmap, ?HL1, ?HL2; simpl; erewrite nth_lookup_Some; eauto.
+    - destruct H as (_ & ? & ? & Hin1), H0 as (_ & ? & ? & Hin2).
+      specialize (Hin1 i); specialize (Hin2 i).
+      rewrite HL2 in Hin2; destruct Hin2 as [_ Hin2]; apply is_Some_None in Hin2; first done.
+      destruct Hin1 as [[] _]; first by rewrite HL1; eauto.
+      split; auto; omega.
+  Qed.  
+    
+  Instance prots_persistent: Persistent ([∗ list] i ∈ seq 0 8, [XP ZplusPos (Z.of_nat i) l in map_nth i L 0 | prot]_R)%I.
+  Proof.
+    intros; apply big_sepL_persistent; intros; apply _.
+  Qed.
+
+  Lemma big_sepL_seq {A} P (l : list A):
+    ([∗ list] i↦_ ∈ l, P i : vProp Σ) ⊣⊢ ([∗ list] i ∈ seq 0 (length l), P i).
+  Proof.
+    induction l using rev_ind; first done.
+    rewrite app_length /= Nat.add_1_r seq_S !big_sepL_app /=.
+    rewrite IHl Nat.add_0_r; done.
+  Qed.
+      
+  Lemma read_spec n out L0 v0 g:
+    (* private precondition *)
+    ⎡PSCtx⎤ ∗ ([∗ list] i ∈ seq 0 8, ZplusPos (Z.of_nat i) out ↦ ?) ∗ node_state_R L0 v0 n g -∗
+    atomic_wp
+    (λ L, ⎡own g (Master (1/2) L)⎤)%I
+    (λ L val, ⌜val = #()⌝ ∗ ∃ v vals L', ⌜length vals = 8%nat /\ (v0 <= v)%nat /\ L0 ⊆ L' /\ L' ⊆ L /\ L' !! v = Some vals⌝ ∗
+          node_state_R L' v n g ∗ ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) out ↦ x) ∗
                        ⎡own g (Master (1/2) L)⎤)%I base_mask ⊤ (read #n #out).
   Proof.
-    iIntros (Φ) "shift"; iDestruct "shift" as (P) "[HP #Hshift]".
+    iIntros "(#kI & out & #node_state)" (Φ) "shift"; iDestruct "shift" as (P) "[HP #Hshift]".
     match goal with |-context[(▷ P ={_,_}=∗ ?R)%I] => set (Q := R) end.
 
     unfold read.
     unfold of_val.
     wp_rec'. wp_rec'.
-    iLöb as "IH" (*forall (L0 v0)*).
+    iLöb as "IH".
     wp_rec'.
     match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
     wp_bind ([_]_at)%E; clear Hclosed.
     wp_op.
-    iMod ("Hshift" with "HP") as (L) "((#kI & #node_state & out & oL) & Hclose)".
-    iApply (GPS_SW_Read (versionP n g) emp%I
-      (fun s v => |={base_mask,⊤}=> versionP n g false (ZplusPos 0 n) s v ∗ ▷ P)%I with "[-]");
+    iApply (GPS_SW_Read (versionP n g) emp%I (versionP n g false (ZplusPos version n))%I with "[]");
       [auto | auto | ..].
     { iSplit; first auto.
       iSplitR ""; [|iSplit].
       - iNext; iIntros (s Hs).
-        iLeft; iIntros (v) "[vP _]".
-        iFrame.
-        iApply "Hclose".
-        iFrame; auto.
+        by iLeft; iIntros (?) "[? _]".
       - iNext; do 2 (rewrite all_forall; iIntros (?)).
         iApply all_entails.
         iIntros "[? #?]"; iModIntro; iFrame "#".
       - iSplit; first auto.
         by iDestruct "node_state" as "(? & ? & ?)". }
-    iNext; iIntros (v ?) "(% & #kV & Hrest)".
+    iNext; iIntros (v1 ?) "(% & #kV & Hrest)".
     rewrite versionP_eq.
-    iMod "Hrest" as "((% & HL1) & HP)"; iModIntro.
+    iDestruct "Hrest" as "(% & HL1)".
     iDestruct "HL1" as (L1) "(% & oL1 & Hdata)"; subst.
     match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
     wp_rec'; clear Hclosed.
     wp_op; wp_op.
-    destruct (decide (v mod 2 = 1)).
+    destruct (decide (v1 mod 2 = 1)).
     { rewrite bool_decide_true; last done.
       wp_if_true.
-      by iApply "IH". }
+      iApply ("IH" with "out HP"). }
     rewrite bool_decide_false; last done.
     wp_if_false.
+    rewrite Zmod_even Nat2Z_inj_even in n0; destruct (even v1) eqn: Heven; try done.
+    iMod (node_state_ord with "[] [#]") as "%"; [eauto | auto | ..].
+    { iDestruct "node_state" as "(? & _ & _ & ?)"; auto. }
+    { iSplit; eauto. }
     match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
     wp_bind (for_loop _ _ _ _); clear Hclosed.
-    iApply fupd_wp.
-    iMod ("Hshift" with "HP") as (L2) "((_ & _ & out & oL2) & Hclose)".
-    iApply (wp_for_simple with "[-]").
-    - instantiate (1 := (fun i => ∃ vals, ⌜i = Z.of_nat (length vals)⌝ ∗
+    iApply (wp_for_simple with "[out Hdata]").
+    - instantiate (1 := (fun i => ⌜i <= 8⌝ ∗ ⎡PSCtx⎤ ∗ ∃ vals, ⌜i = Z.of_nat (length vals)⌝ ∗
         ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) out ↦ x) ∗
         ([∗ list] i ∈ seq (Z.to_nat i) (8 - Z.to_nat i), ZplusPos (Z.of_nat i) out ↦ ?) ∗
-        ∃ v', [XP ZplusPos version n in v' | versionP n g]_R ∗ ⎡@own _ _ histG g (Snapshot L1)⎤ ∗
-        ([∗ list] i↦x ∈ vals, ∃ vi, ⌜(v <= vi <= v')%nat⌝ ∗
-           [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in <[vi := x]>((fun l => nth i l 0) <$> L1) | dataP n g]_R) ∗
+        ∃ v', ⌜(v1 <= v' - 1)%nat⌝ ∗ [XP ZplusPos version n in (v' - 1)%nat | versionP n g]_R ∗
+           ([∗ list] i↦x ∈ vals, ∃ Li,
+             ⌜(∃ vi, v1 <= vi <= v' /\ log_latest Li vi x /\ map_nth i L1 0 ⊆ Li)%nat⌝ ∗
+             [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in Li | dataP n g]_R) ∗
         ([∗ list] i ∈ seq (Z.to_nat i) (8 - Z.to_nat i), 
-           [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in (fun l => nth i l 0) <$> L1 | dataP n g]_R))%I).
-      iIntros (i ?) "(% & H) Hpost".
+           [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in map_nth i L1 0 | dataP n g]_R))%I).
+      iIntros (i ?) "(% & _ & #kI & H) Hpost".
       iDestruct "H" as (vals) "(% & Hout & Hrest & H)".
-      iDestruct "H" as (v') "(#kV & oL1 & Hvals & Hdata)".
-      admit.
-    - iExists nil; simpl.
-      iFrame; eauto.
-    - iNext; iIntros (?) "H"; iDestruct "H" as (i) "(% & H)".
-      iDestruct "H" as (vals) "(% & Hout & _ & H)".
-      iDestruct "H" as (v') "(#kV' & oL1 & Hvals & _)".
+      iDestruct "H" as (v') "(% & #kV & Hvals & Hdata)".
+      wp_let.
+      repeat wp_op.
+      wp_bind ([_]_at)%E.
+      destruct (8 - Z.to_nat i)%nat eqn: Hi.
+      { apply Z2Nat.inj_lt in H2; [change (Z.to_nat 8) with 8%nat in H2| |]; omega. }
+      rewrite !big_sepL_cons.
+      iDestruct "Hdata" as "[Hdi Hdata]"; iDestruct "Hrest" as "[Hi Hrest]".
+      rewrite Z2Nat.id; last omega.
+      iApply (GPS_SW_Read (dataP n g) emp%I
+        (fun s d => ∃ vi, ⌜(v1 <= vi)%nat /\ log_latest s vi d⌝ ∗
+                       [XP ZplusPos version n in (vi - 1)%nat | versionP n g]_R)%I with "[Hdi]");
+        [auto | auto | ..].
+      { iSplit; first auto.
+        iSplitR "Hdi"; [|iSplit; last by iFrame].
+        + iNext; iIntros (s Hs).
+          iLeft; iIntros (d) "[dP _]".
+          iDestruct "dP" as (vi) "[% kV']".
+          iModIntro.
+          iExists vi; iFrame.
+          iPureIntro; split; auto.
+          destruct H1 as (_ & ? & ?).
+          eapply log_latest_ord; eauto.
+          apply fmap_nth_log_latest; eauto.
+        + iNext; do 2 (rewrite all_forall; iIntros (?)).
+          iApply all_entails.
+          iIntros "[? #?]"; iModIntro; iFrame "#". }
+      iNext; iIntros (s d) "(% & Hdi & H)"; iDestruct "H" as (vi) "(% & #kV')".
+      iApply wp_fupd.
+      iApply (na_write with "[$kI $Hi]"); first done.
+      iNext; iIntros "Hi".
+      iPoseProof (GPS_SW_Readers_agree (s1 := (v' - 1)%nat) (s2 := (vi - 1)%nat) with "[$kV' $kV]") as "Hcase";
+        first apply coPset_top_subseteq.
+      iMod "Hcase" as %Hcase; iModIntro.
+      iApply "Hpost".
+      iSplit; first by iPureIntro; omega.
+      iSplit; first auto.
+      iExists (vals ++ d :: nil)%list.
+      rewrite Z2Nat.inj_add; try omega.
+      rewrite H3 Nat2Z.id.
+      iSplit.
+      { iPureIntro; rewrite app_length; simpl.
+        by rewrite Nat2Z.inj_add. }
+      rewrite big_sepL_app; simpl.
+      change (Z.to_nat 1) with 1%nat.
+      replace (8 - (length vals + 1))%nat with n1 by (rewrite H3 Nat2Z.id in Hi; omega).
+      rewrite Nat.add_0_r Nat.add_1_r; iFrame.
+      iExists (Nat.max v' vi); rewrite -Nat.sub_max_distr_r.
+      iSplit.
+      { iPureIntro; etrans; eauto; apply Nat.le_max_l. }
+      iSplit.
+      { destruct (Max.max_spec (v' - 1) (vi - 1)) as [[? ->] | [? ->]]; done. }
+      rewrite big_sepL_app; simpl.
+      iSplitL "Hvals".
+      + iApply (big_sepL_mono with "Hvals"); intros; simpl.
+        iIntros "H"; iDestruct "H" as (Li) "[% ?]"; iExists Li; iFrame.
+        destruct H8 as (vj & [] & ? & ?).
+        iPureIntro; exists vj; split; split; auto.
+        etransitivity; [eauto | apply Nat.le_max_l].
+      + iSplit; last auto.
+        iExists s.
+        rewrite Nat.add_0_r; iSplit; auto.
+        rewrite H3 Nat2Z.id in H5.
+        iPureIntro; exists vi; split; split; try tauto.
+        apply Nat.le_max_r.
+    - iSplit; first auto.
+      iSplit; first auto.
+      iExists nil; simpl; iFrame.
+      iSplit; first auto.
+      iExists (v1 + 1)%nat; rewrite Nat.add_sub; auto.
+    - iNext; iIntros (?) "H"; iDestruct "H" as (i) "(% & % & _ & H)".
+      assert (i = 8) by omega; subst.
+      iDestruct "H" as (vals) "(% & out & _ & H)".
+      assert (length vals = 8)%nat as Hlen by omega.
+      iDestruct "H" as (v') "(% & #kV' & Hvals & _)".
       match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
       wp_seq; clear Hclosed.
       match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
       wp_bind ([_]_at)%E; clear Hclosed.      
       wp_op.
-      admit.
+      iMod ("Hshift" with "HP") as (L2) "[oL2 Hclose]".
+      iApply (GPS_SW_Read (s := (v' - 1)%nat) (versionP n g) emp%I (fun s v => ⌜Z.of_nat s = v⌝ ∗
+        |={base_mask, ⊤}=> if decide (v = v1) then Φ #() else ([∗ list] i↦x ∈ vals, (ZplusPos i out ↦ x)) ∗ ▷P)%I
+        with "[-]"); [auto | auto | ..].
+      { iSplit; first auto.
+        iSplitR ""; [|iSplit].
+        - iNext; iIntros (s Hs).
+          iLeft; iIntros (?) "[vP _]".
+          rewrite versionP_eq.
+          iDestruct "vP" as (? L3) "(% & oL3 & Hdata)"; subst.
+          iModIntro; iSplit; first auto.
+          destruct (decide _); last by iFrame; iApply "Hclose".
+          apply Nat2Z.inj in e; subst.
+          rewrite Heven in H7.
+          hnf in Hs.
+          assert (v' - 1 = v1)%nat as Hv by omega.
+          iPoseProof (log_latest_comprehend with "[Hvals]") as (L') "[% Hvals]"; first eauto.
+          { iApply big_sepL_mono; last iApply "Hvals".
+            intros; simpl.
+            iIntros "H"; iDestruct "H" as (Li) "[% ?]"; iExists Li; iFrame.
+            iPureIntro; destruct H8 as (? & ? & Hlatest & ?); split; eauto.
+            pose proof (log_latest_even _ _ _ Hlatest) as Heven'.
+            destruct (decide (x = v1)); first by subst.
+            subst; rewrite Nat.even_sub in Heven; last omega.
+            assert (x = v') by omega; subst.
+            rewrite Heven' in Heven; done. }
+          destruct H6 as (Hsize & Hlatest & Hincl).
+          iMod (node_state_ord _ _ v1 v1 with "[#] [#]") as "%"; first auto.
+          { apply union_subseteq_r. }
+          { iSplit.
+            { iPureIntro; rewrite -Hlen; eauto. }
+            rewrite big_sepL_seq Hlen; done. }
+          { auto. }
+          iApply "Hclose".
+          iSplit; first auto.
+          iPoseProof (own_snap_ord _ _ _ L2 with "oL2 oL3") as "%".
+          iExists v1, vals, L3; iFrame.
+          rewrite Hv; iFrame "kV'".
+          iSplit; last auto.
+          iPureIntro; split; first done.
+          split; first done.
+          split; last split; auto.
+          + etrans; first done.
+            etrans; last done.
+            intro i.
+            destruct (L1 !! i) eqn: HL1, (L' !! i) eqn: HL'; rewrite HL1 HL'; try done; simpl.
+            * destruct H1 as [Hsize1 _].
+              specialize (Hsize1 _ _ HL1); specialize (Hsize _ _ HL'); simpl in *.
+              eapply list_eq_same_length; eauto; intros.
+              { rewrite Hsize1; omega. }
+              eapply lookup_weaken_inv; [| apply Hincl; eauto |];
+                rewrite lookup_fmap; [erewrite HL1 | erewrite HL']; simpl; erewrite nth_lookup_Some; eauto.
+            * lapply (Hincl O); last omega; intro X.
+              specialize (X i); rewrite !lookup_fmap HL1 HL' in X; done.
+          + eapply lookup_weaken; last eauto.
+            destruct Hlatest; done.
+        - iNext; do 2 (rewrite all_forall; iIntros (?)).
+          iApply all_entails.
+          iIntros "[? #?]"; iModIntro; iFrame "#".
+        - iSplit; first auto.
+          by iDestruct "node_state" as "(? & ? & ?)". }
+      iNext; iIntros (v2 ?) "(% & #kV2 & % & Hrest)"; subst.
+      iMod "Hrest"; iModIntro.
+      match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
+      wp_rec'.
+      wp_op.
+      destruct (decide _).
+      + rewrite bool_decide_true; last done.
+        by wp_if_true.
+      + rewrite bool_decide_false; last done.
+        wp_if_false.
+        iDestruct "Hrest" as "[out HP]".
+        iApply ("IH" with "[out] HP").
+        iPoseProof (big_sepL_mono _ (fun i _ => ZplusPos i out ↦ ?)%I with "out") as "out".
+        { intros; simpl; iIntros; iFrame. }
+        by rewrite big_sepL_seq Hlen.
+  Qed.
+
+  Lemma take_1_drop {A} (l : list A) i x (Hx : l !! i = Some x): take 1 (drop i l) = x :: nil.
+  Proof.
+    erewrite <-(take_drop_middle l) by eauto.
+    rewrite drop_app_alt; auto.
+    rewrite take_length.
+    rewrite Min.min_l; first done.
+    apply lookup_lt_Some in Hx; omega.
+  Qed.
+
+  Lemma map_nth_sub {A} (m1 m2 : gmap nat (list A)) i d: m1 ⊆ m2 -> map_nth i m1 d ⊆ map_nth i m2 d.
+  Proof.
+    intros H j; specialize (H j).
+    rewrite !lookup_fmap.
+    destruct (m1 !! j), (m2 !! j); simpl in *; subst; done.
+  Qed.
+
+  Lemma map_nth_insert {A} (m : gmap nat (list A)) v x i d:
+    map_nth i (<[v := x]>m) d = <[v := nth i x d]>(map_nth i m d).
+  Proof.
+    apply map_eq; intro j.
+    rewrite lookup_fmap.
+    destruct (decide (j = v)).
+    - subst; rewrite !lookup_insert; done.
+    - rewrite !lookup_insert_ne; try done.
+      rewrite lookup_fmap; done.
+  Qed.
+
+  Global Instance elim_modal_bupd_fupd_embed E1 E2 P Q :
+    ElimModal (⎡|==> P⎤ : vProp Σ)%I ⎡P⎤ (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+  Proof.
+    rewrite /ElimModal.
+    iStartProof (uPred _); iIntros (?) "[U H]".
+    iMod "U".
+    by iSpecialize ("H" with "[U //]").
+  Qed.
+
+  Lemma big_sepL_nth {A} P l (d : A):
+    ([∗ list] i↦x ∈ l, P i x : vProp Σ) ⊣⊢ ([∗ list] i ∈ seq 0 (length l), P i (nth i l d)).
+  Proof.
+    rewrite -big_sepL_seq.
+    apply big_sepL_proper; intros.
+    erewrite nth_lookup_Some; eauto.
+  Qed.
+  
+  (* We could also have half the write node_state in the atomic part, to make the connection between the abstract
+     state and concrete memory clearer. It would then need a predicate that allows for partial changes. Would this
+     be better than the current version? *)
+  Lemma write_spec n ain vals L v g (Hlen: length vals = 8%nat):
+    ⎡PSCtx⎤ ∗ node_state_W L v n g ∗ ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) ain ↦ x) -∗
+    atomic_wp
+    (λ _ : unit, ⎡@own _ _ histG g (@Master _ (gmap_unit(A := list.listC ZC)) (1/2) L)⎤)%I
+    (λ _ val, ⌜val = #()⌝ ∗ node_state_W (<[(v + 2)%nat := vals]>L) (v + 2)%nat n g ∗
+              ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) ain ↦ x) ∗
+              ⎡@own _ _ histG g (@Master _ (gmap_unit(A := list.listC ZC)) (1/2) (<[(v + 2)%nat := vals]>L))⎤)%I
+      base_mask ⊤ (write #n #ain).
+  Proof.
+    iIntros "(#kI & node_state & in)" (Φ) "shift"; iDestruct "shift" as (P) "[HP #Hshift]".
+    match goal with |-context[(▷ P ={_,_}=∗ ?R)%I] => set (Q := R) end.
+
+    unfold write.
+    unfold of_val.
+    wp_rec'. wp_rec'.
+    match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
+    wp_op.
+    wp_bind ([_]_at)%E; clear Hclosed.
+    iDestruct "node_state" as "(% & kV & oL & data)".
+    iApply (GPS_SW_Read_ex (versionP n g) with "[$kI $kV]");
+      [auto | auto | ..].
+    { iNext; rewrite all_forall; iIntros (?).
+      iApply all_entails.
+      iIntros "#?"; iModIntro; iFrame "#". }
+    iNext; iIntros (?) "(kV & Hv)".
+    rewrite versionP_eq.
+    iDestruct "Hv" as "[% _]"; subst.
+    wp_rec'.
+    match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
+    repeat wp_op.
+    wp_bind ([_]_at <- _)%E; clear Hclosed.
+    destruct H as (Hsize & ? & HL).
+    pose proof (log_latest_even _ _ _ HL) as Heven.
+    iApply (GPS_SW_ExWrite (versionP n g) (v + 1)%nat emp%I (fun s' => [XP ZplusPos version n in s' | versionP n g]_W)
+      with "[$kI $kV]"); [hnf; omega | done | done | ..].
+    { iNext; iIntros (?) "(_ & vP & kV)".
+      iModIntro; iSplitL "kV"; first done.
+      rewrite versionP_eq.
+      iDestruct "vP" as "[_ vP]".
+      iDestruct "vP" as (L0) "[% ?]".
+      rewrite Heven in H.
+      iSplit; iNext; rewrite versionP_eq Nat2Z.inj_add; iSplit; auto; iExists L0; iFrame;
+        rewrite Nat.even_add Heven Nat.add_sub; auto. }
+    iNext; iIntros "[#kV1 kV]".
+    match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
+    wp_seq; clear Hclosed.
+    assert (L ⊆ <[(v+2)%nat := vals]>L) as Hsub.
+    { apply insert_subseteq.
+      destruct HL as [_ Hlast].
+      destruct (Hlast (v + 2)%nat) as [Hnone _].
+      destruct (L !! (v + 2)%nat) eqn: H2; last done.
+      destruct Hnone; [eauto | omega]. }
+    pose proof (log_latest_insert _ _ _ vals HL) as HL'.
+    wp_bind (for_loop _ _ _ _).
+    iApply (wp_for_simple with "[data in]").
+    - instantiate (1 := (fun i => ⌜0 <= i <= 8⌝ ∗ ⎡PSCtx⎤ ∗ [XP ZplusPos version n in (v + 1)%nat | versionP n g ]_R ∗
+        ([∗ list] i↦x ∈ take (Z.to_nat i) vals, [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in 
+                                   <[(v + 2)%nat := x]>(map_nth i L 0) | dataP n g ]_W) ∗
+        ([∗ list] i ∈ seq (Z.to_nat i) (8 - Z.to_nat i), [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in 
+        map_nth i L 0 | dataP n g ]_W) ∗ ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) ain ↦ x))%I).
+      iIntros (i ?) "(% & % & #kI & #kV & Hwrote & Hrest & Hin) Hpost".
+      wp_let.
+      repeat wp_op.
+      wp_bind ([_]_na)%E.
+      destruct (lookup_lt_is_Some_2 vals (Z.to_nat i)) as [p Hp].
+      { rewrite Hlen; apply Nat2Z.inj_lt.
+        rewrite Z2Nat.id; auto; omega. }
+      iPoseProof (big_sepL_lookup_acc with "Hin") as "[Hi Hin]"; first apply Hp.
+      rewrite Z2Nat.id; last omega.
+      iApply (na_read with "[$kI $Hi]"); first auto.
+      iNext; iIntros (?) "[% Hi]"; subst.
+      iPoseProof ("Hin" with "Hi") as "Hin".
+      destruct (8 - Z.to_nat i)%nat eqn: Hi.
+      { apply Z2Nat.inj_lt in H; [change (Z.to_nat 8) with 8%nat in H| |]; omega. }
+      rewrite big_sepL_cons.
+      iDestruct "Hrest" as "[Hi Hrest]".
+      rewrite Z2Nat.id; last omega.
+      iApply (GPS_SW_ExWrite (dataP n g) (<[(v + 2)%nat := p]>(map_nth (Z.to_nat i) L 0)) emp%I _ with "[$kI $Hi]");
+        [ | done | done | ..].
+      { eapply map_nth_sub in Hsub.
+        erewrite map_nth_insert, nth_lookup_Some in Hsub; eauto. }
+      { iNext; iIntros (?) "(_ & _ & kD)".
+        iModIntro; iSplit; first by iApply "kD".
+        unfold dataP, dataP'.
+        eapply fmap_nth_log_latest in HL'.
+        erewrite map_nth_insert, nth_lookup_Some in HL' by eauto.
+        iSplit; iNext; iExists (v + 2)%nat; replace (v + 2 - 1)%nat with (v + 1)%nat by omega; auto. }
+      iNext; iIntros "[_ Hi]".
+      iApply "Hpost".
+      iSplit; first by iPureIntro; omega.
+      iFrame "#".
+      rewrite Z2Nat.inj_add; try omega.
+      rewrite -take_take_drop big_sepL_app.
+      change (Z.to_nat 1) with 1%nat.
+      replace (8 - (Z.to_nat i + 1))%nat with n0 by omega.
+      rewrite !Nat.add_1_r; iFrame.
+      erewrite take_1_drop by eauto; simpl.
+      rewrite take_length Nat.add_0_r Min.min_l; last omega.
+      rewrite Z2Nat.id; last omega; iFrame.
+    - simpl; iSplit; first auto.
+      iFrame "#"; iFrame.
+    - iNext; iIntros (?) "H"; iDestruct "H" as (i) "(% & % & _ & _ & data & _ & in)".
+      assert (i = 8) by omega; subst.
+      rewrite take_ge; last by rewrite Hlen.
+      wp_seq.
+      repeat wp_op.
+      iMod ("Hshift" with "HP") as (?) "[oL' Hclose]".
+      iApply (GPS_SW_ExWrite (s := (v + 1)%nat) (versionP n g) (v + 2)%nat emp%I (fun _ => |={base_mask,⊤}=> Φ #())%I
+        with "[-]"); [hnf; omega | done | done | | by iNext; iIntros "[_ ?]"].
+      iFrame "#"; iFrame.
+      iNext; iIntros (?) "(_ & vP & kV)".
+      iPoseProof (own_update_2 with "oL oL'") as "oL".
+      { rewrite master_op half_join.
+        etrans; first apply make_snap.
+        apply @snap_update with (a' := <[(v+2)%nat := vals]>L); done. }
+      rewrite -{3}half_join.
+      (* can't make the own split properly *)
+      (*      iMod "oL" as "(oL & oL' & #?)".*)
+      iMod "oL"; iAssert (⎡own g (@Master _ (gmap_unit(A := list.listC ZC)) (1/2) (<[(v+2)%nat:=vals]>L)) ∗
+                           own g (@Master _ (gmap_unit(A := list.listC ZC)) (1/2) (<[(v+2)%nat:=vals]>L)) ∗
+                           @own _ _ histG g (Snapshot (<[(v+2)%nat:=vals]>L))⎤)%I with "[oL]"
+        as "(oL & oL' & #?)".
+      { admit. }
+      assert (map_size (<[(v + 2)%nat:=vals]> L) 8).
+      { apply map_Forall_insert_2; auto. }
+      setoid_rewrite big_sepL_nth at 1.
+      rewrite Hlen.
+      iPoseProof (big_sepL_mono with "data") as "data".
+      { intros; simpl.
+        erewrite <-map_nth_insert.
+        iApply (GPS_SW_Writer_Reader (IP := dataP n g)). }
+      rewrite big_sepL_sepL; iDestruct "data" as "[data dataR]".
+      iPoseProof ("Hclose" with "[kV data oL oL' in]") as "Hpost".
+      { iSplit; first auto.
+        iFrame; eauto. }
+      iModIntro; iFrame.
+      iDestruct "vP" as "_".
+      rewrite !versionP_eq.
+      rewrite Nat2Z.inj_add.
+      rewrite Nat.even_add Heven; simpl.
+      iSplit; iNext; iSplit; try done; iExists (<[(v + 2)%nat:=vals]> L); iSplit; eauto; iFrame "#".
   Admitted.
       
 End proof.
diff --git a/theories/examples/snapshot.v b/theories/examples/snapshot.v
index e73d1822767c0fa40be0f1cac7da277dfa773efb..20bd00b097f88a8df945c0be8e0d6f9898c0d63e 100644
--- a/theories/examples/snapshot.v
+++ b/theories/examples/snapshot.v
@@ -13,8 +13,8 @@ Arguments snapshot {_} _.
 Instance: Params (@Snap) 1.
 Instance: Params (@master) 1.
 Instance: Params (@snapshot) 1.
-Notation "'Snapshot' a" := (Snap None (Some a)) (at level 20).
-Notation "'Master' k a" := (Snap (Some (k%Qp, to_agree a)) (Some ε)) (at level 20, k at level 9).
+Definition Snapshot {A} (a : A) := Snap None (Some a).
+Definition Master {A} `{Unit A} k (a : A) := Snap (Some (k, to_agree a)) (Some ε).
 
 (* COFE *)
 Section cofe.
@@ -328,6 +328,17 @@ Proof.
   eapply join_le; rewrite join_comm; eauto.
 Qed.
 
+Lemma master_update a b a' :
+  R a a' → Master 1 a ~~> Master 1 a'.
+Proof.
+  intros Ha' Hlt; apply cmra_total_update; intros.
+  destruct z as [[[]|] bf1]; hnf; hnf in H; simpl in *;
+    destruct bf1; try contradiction; simpl in *; rewrite !join_unit in H |- *; destruct H as (? & ? & ?).
+  { apply Qp_not_plus_q_ge_1 in H; contradiction. }
+  split; last split; auto.
+  etransitivity; eauto.
+Qed.
+
 (*Lemma snap_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ● a ⋅ ◯ b ~~> ● a'.
 Proof. intros. rewrite -(right_id _ _ (● a')). by apply snap_update. Qed.*)
 
@@ -416,3 +427,10 @@ Proof.
   rewrite agree_validI agree_equivI.
   iDestruct "Hagree" as %?; auto.
 Qed.
+
+Lemma half_join : (1/2 ⋅ 1/2 = 1)%Qp.
+Proof.
+  unfold op, cmra_op; simpl.
+  unfold frac_op.
+  apply Qp_div_2.
+Qed.
\ No newline at end of file