diff --git a/theories/examples/kvnode2.v b/theories/examples/kvnode2.v
new file mode 100644
index 0000000000000000000000000000000000000000..d8ac2896a8c4e154ba5079ebbf8c6fb03d5a0ae1
--- /dev/null
+++ b/theories/examples/kvnode2.v
@@ -0,0 +1,1070 @@
+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
+
+From igps Require Export malloc repeat notation escrows.
+From igps Require Import persistor viewpred proofmode weakestpre protocols singlewriter logically_atomic
+ invariants fork.
+From igps.gps Require Import shared plain recursive.
+From igps.examples Require Import abs_hashtable snapshot hist_protocol repeat for_loop list_lemmas.
+Require Recdef.
+
+Import uPred lang.base.
+
+Section kvnode.
+
+(*Context (m_entries : loc) (results : loc).*)
+
+Local Notation version := 0.
+Local Notation data := 1.
+
+(* There's no default location, so make sure i is in-bounds. *)
+Local Notation undef := 1%positive.
+
+Section code.
+
+Program Definition read : val := @RecV <> "n" (λ: "out",
+ (rec: "f" <> :=
+ let: "snap" := ["n" + #version]_at in
+ if: "snap" `mod` #2 = #1 then "f" #()
+ else (for: ("i" := #0; "i" < #8; "i" + #1)
+ ["out" + "i"]_na <- ["n" + #data + "i"]_at);;
+ let: "v" := ["n" + #version]_at in
+ if: "v" = "snap" then #() else "f" #()) #()) _.
+Next Obligation.
+Proof.
+ apply I.
+Qed.
+
+Program Definition write : val := @RecV <> "n" (λ: "in",
+ let: "v" := ["n" + #version]_at in
+ ["n" + #version]_at <- ("v" + #1);;
+ (for: ("i" := #0; "i" < #8; "i" + #1)
+ ["n" + #data + "i"]_at <- ["in" + "i"]_na);;
+ ["n" + #version]_at <- ("v" + #2)) _.
+Next Obligation.
+Proof.
+ apply I.
+Qed.
+
+Program Definition make_node : val := @RecV <> <>
+ (let: "n" := malloc #9 in
+ ["n" + #version]_na <- #0;;
+ (for: ("i" := #0; "i" < #8; "i" + #1)
+ ["n" + #data + "i"]_na <- #0);;
+ "n") _.
+Next Obligation.
+Proof.
+ apply I.
+Qed.
+
+Program Definition writer : val := @RecV <> "n"
+ (let: "data" := malloc #8 in
+ (for: ("i" := #0; "i" < #8; "i" + #1)
+ ["data" + "i"]_na <- #0);;
+ for: ("i" := #0; "i" < #3; "i" + #1)
+ (for: ("j" := #0; "j" < #8; "j" + #1)
+ ["data" + "j"]_na <- (["data" + "j"]_na + #1));;
+ write "n" "data") _.
+Next Obligation.
+Proof.
+ apply I.
+Qed.
+
+Definition reader : val := @RecV <> "n"
+ (let: "data" := malloc #8 in
+ read "n" "data") _.
+
+End code.
+
+Canonical Structure versionProtocol : protocolT := ProtocolT _ le.
+
+Instance versionPrt_facts : protocol_facts versionProtocol.
+Proof. esplit; apply _.
+Qed.
+
+Instance version_join : Join le := { join a b := Some (max a b) }.
+Proof.
+ - apply Nat.le_0_l.
+ - intros ????? Hc He; inversion Hc; inversion He; subst.
+ do 2 eexists; eauto.
+ by rewrite Max.max_assoc (Max.max_comm a b).
+ - intros ??.
+ by rewrite Max.max_comm.
+ - intros ??? X; inversion X.
+ apply Nat.le_max_l.
+ - intros.
+ by rewrite Max.max_r.
+Qed.
+
+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.
+
+Section Interpretation.
+ Context `{foundationG Σ} `{histG : inG Σ (snapR (hist_join (list.listC ZC)))}
+ `{persG : persistorG Σ}
+ `{gpGv: !gpsG Σ versionProtocol _}
+ `{gpGd: !gpsG Σ histProtocol _}.
+
+ (*
+ Fixpoint versionP version locs (γ : gname) : interpC Σ versionProtocol := (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⌠∗
+ ⎡@own _ _ histG γ (Snapshot L)⎤ ∗
+ [∗ list] i↦x ∈ locs, [XP x in (fun l => nth i l 0) <$> L | dataP version locs γ]_R)%I
+ with dataP version locs (γ : gname) : interpC Σ histProtocol := (fun _ _ s v =>
+ ∃ ver, ⌜even ver = true /\ log_latest s ver v⌠∗ [XP version in (ver - 1)%nat | versionP version locs γ]_R)%I.
+ *)
+
+ Definition dataP' n versionP : interpC Σ histProtocol := (fun _ _ s v =>
+ ∃ 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), ⌜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 map_nth i L 0 | dataP' n R]_R)%I.
+
+ Instance versionP_contractive n γ : Contractive (versionP_fun n γ).
+ Proof.
+ repeat intro. unfold versionP_fun. do 9 f_equiv.
+ apply dist_dist_later=>????. unfold dataP'. by do 4 f_equiv.
+ Qed.
+
+ Definition versionP n γ : interpC Σ versionProtocol := fixpoint (versionP_fun n γ).
+
+ 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), ⌜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 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), ⌜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 map_nth i L 0 | dataP n γ]_R)%I.
+ Proof.
+ apply versionP_eq'.
+ Qed.
+
+ (*(* adapted from message_passing *)
+ Definition XE (γ: gname) (P : vProp Σ) := [es ⎡own γ (Excl ())⎤ ⇠P ]%I.
+
+ Definition onceP (γ : gname) (P : vProp Σ) : interpC Σ boolProtocol := (fun b _ s v =>
+ ⌜(if s then v = 1 else v = 0)%Z⌠∗ if s then XE γ P else True)%I.*)
+
+End Interpretation.
+
+Section proof.
+ Context `{fG : foundationG Σ}
+ `{persG : persistorG Σ}
+ `{histG : inG Σ (snapR (hist_join (list.listC ZC)))}
+ `{gpGv: !gpsG Σ versionProtocol _}
+ `{gpGd: !gpsG Σ histProtocol _}
+ `{agreeGk : !gps_agreeG Σ versionProtocol}
+ `{agreeGv : !gps_agreeG Σ histProtocol}.
+
+ Set Default Proof Using "Type".
+
+ (* The collection of protocol assertions that describes a stable state of the node. *)
+ Definition node_state_R L v n g :=
+ (⌜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 map_nth i L 0 | dataP n g]_R)%I.
+
+ Definition node_state_W L v n g :=
+ (⌜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 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;
+ unfold subst; fold subst; try (rewrite !subst_for; try done); unfold subst; fold subst; simpl end.
+
+ Definition base_mask : coPset := ↑physN ∪ (*↑fracN ∪*) ↑persist_locN.
+
+ Lemma phys_base : ↑physN ⊆ base_mask.
+ Proof.
+ (*etransitivity; *)apply union_subseteq_l.
+ Qed.
+
+(* Lemma frac_base {A} {_ : EqDecision A} {_ : Countable A} (i : A) :
+ ↑namespaces.ndot fracN i ⊆ base_mask.
+ Proof.
+ etransitivity; last apply union_subseteq_l.
+ etransitivity; last apply union_subseteq_r.
+ apply namespaces.nclose_subseteq.
+ Qed.*)
+
+ Lemma persist_base {A} {_ : EqDecision A} {_ : Countable A} (i : A) :
+ ↑namespaces.ndot persist_locN i ⊆ base_mask.
+ Proof.
+ etransitivity; last apply union_subseteq_r.
+ apply namespaces.nclose_subseteq.
+ Qed.
+
+ Hint Resolve phys_base (*frac_base*) persist_base.
+
+ Instance versionP_persistent n g b l s v: Persistent (versionP n g b l s v).
+ Proof.
+ intros.
+ rewrite versionP_eq.
+ apply sep_persistent; first apply _.
+ apply exist_persistent; intro.
+ apply sep_persistent; first apply _.
+ apply sep_persistent; first apply _.
+ apply big_sepL_persistent; intros.
+ apply _.
+ Qed.
+
+ Instance node_state_R_persistent L v n g: Persistent (node_state_R L v n g).
+ Proof.
+ apply sep_persistent; first apply _.
+ apply sep_persistent; first apply _.
+ apply sep_persistent; first apply _.
+ apply big_sepL_persistent; intros.
+ apply _.
+ Qed.
+
+ Opaque seq.
+
+ 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.
+
+ 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. apply @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.
+
+(* Definition kvnode_prot_R {A} n (s : A) (t1 t2 : A -> list Z -> Prop) g :=
+ ∃ L v vs h, ⌜log_latest L v vs⌠∗ node_state_R L v n g ∗ ghost_hist h ∗
+ [∗ list] (s, d) ∈ h, t2 s d.
+
+ Lemma read_spec n out s t1 t2 P Q (HQ : forall s' vals, s ⊑ s' -> P ∗ t1 s' vals -∗ Q):
+ {{{ ⎡PSCtx⎤ ∗ ([∗ list] i ∈ seq 0 8, ZplusPos (Z.of_nat i) out ↦ ?) ∗ kvnode_prot_R n s t1 t2 * P }}}
+ read #n #out
+ {{{ RET (); ∃ s' vals, ⌜s ⊑ s'⌠∗ ([∗ list] i↦x ∈ vals, ZplusPos (Z.of_nat i) out ↦ x) ∗ kvnode_prot_R n s' t * Q }}}.
+ base_mask ⊤ (read #n #out).
+ Proof.
+ 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".
+ 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.
+ 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).
+ by iLeft; iIntros (?) "[? _]".
+ - iNext; do 2 (rewrite monPred_objectively_forall; iIntros (?)).
+ iApply objectively_entails.
+ iIntros "[? #?]"; iModIntro; iFrame "#".
+ - iSplit; first auto.
+ by iDestruct "node_state" as "(? & ? & ?)". }
+ iNext; iIntros (v1 ?) "(% & #kV & Hrest)".
+ rewrite versionP_eq.
+ 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 (v1 mod 2 = 1)).
+ { rewrite bool_decide_true; last done.
+ wp_if_true.
+ 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 (wp_for_simple with "[] [out Hdata]").
+ - instantiate (1 := (fun i => ⌜i <= 8⌠∗ ∃ 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', ⌜(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 map_nth i L1 0 | dataP n g]_R))%I).
+ iIntros "!#" (i ?) "!# (% & _ & H) Hpost".
+ iDestruct "H" as (vals) "(% & Hout & Hrest & H)".
+ 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 monPred_objectively_forall; iIntros (?)).
+ iApply objectively_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.
+ 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.
+ 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.
+ 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".
+ iPoseProof (own_snap_ord _ _ _ L2 with "oL2 oL3") as "%".
+ iFrame "oL2"; iSplit; first auto.
+ 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 monPred_objectively_forall; iIntros (?)).
+ iApply objectively_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.
+
+From igps Require Import shared2.
+
+Section Protocol.
+(* A kvnode protocol is much like a single-location protocol, but it collects a set of writes to 8 locations at the same view
+ for each event. "The same view" might cause some problems. *)
+
+Definition kvtype := (nat * (Z * Z * Z * Z * Z * Z * Z * Z))%type.
+
+Definition kvget i (d : kvtype) :=
+ let '(_, (a, b, c, d, e, f, g, h)) := d in
+ match i with
+ | 0 => a
+ | 1 => b
+ | 2 => c
+ | 3 => d
+ | 4 => e
+ | 5 => f
+ | 6 => g
+ | 7 => h
+ | _ => 0
+ end.
+
+Notation kvnode_interpC Σ Prtcl := (bool -c> loc -c> pr_state Prtcl -c> kvtype -c> vProp Σ).
+
+Notation kvnode_state_sort Prtcl := (leibnizC (pr_state Prtcl * (kvtype * View))%type).
+Notation kvnode_state_type Prtcl := (gset (kvnode_state_sort Prtcl)).
+
+Context `{PF : !protocol_facts Prtcl} `{GPSG : !gpsG(A := kvtype) Σ Prtcl PF} `(IP : gname -> kvnode_interpC Σ Prtcl).
+
+Definition kvnode_Hist (n : loc) (h : gset (kvtype * View)) :=
+ (Hist (ZplusPos version n) (map_gset (fun '(d, V) => (VInj (Z.of_nat (fst d)), V)) h) ∗
+ [∗ list] i ∈ seq 0 8, Hist (ZplusPos (Z.of_nat i) (ZplusPos data n)) (map_gset (fun '(d, V) => (VInj (kvget i d), V)) h))%I.
+
+Definition kvnode_list (d : kvtype) :=
+ let '(_, (a, b, c, d, e, f, g, h)) := d in a :: b :: c :: d :: e :: f :: g :: h :: nil.
+
+ Definition kvnode_prots_R g n v vs : vProp Σ :=
+ (∃ L, ⌜map_size L 8 /\ 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 map_nth i L 0 | dataP n g]_R)%I.
+
+ Definition kvnode_prots_W g n v vs :=
+ (∃ L, ⌜map_size L 8 /\ 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 map_nth i L 0 | dataP n g]_W)%I.
+
+Definition kvnode_IP γ γ' b n ζ (e_x : kvtype) :=
+ (IP γ b n ζ e_x ∗ if b then kvnode_prots_W γ' n (fst e_x) (kvnode_list e_x) else kvnode_prots_R γ' n (fst e_x) (kvnode_list e_x))%I.
+
+Definition kvnode_inv n γ γ_x γ' : iProp Σ
+ := (∃ ζ h e_x, own.own γ (◠(◠ζ ⋅ ◯ ζ))
+ ∗ own.own γ_x (◠(Some (1%Qp, to_agree e_x)))
+ ∗ kvnode_Hist n h ∗ ProtoInv (kvnode_IP γ γ') n ζ e_x
+ ∗ (*⌜init n h⌠∗*) ⌜SortInv n ζ⌠∗ ⌜e_x ∈ ζâŒ
+ ∗ ⌜Consistent ζ h⌠∗ ⌜FinalInv n e_x ζ⌠∗ ⌜StateInjection ζâŒ)%I.
+
+ Definition kvnodeSWnRaw γ l n : iProp Σ :=
+ (∃ (γ_x: gname) γ',
+ ⌜n = encode (γ,γ_x,γ')⌠∗ kvnode_inv l γ γ_x γ')%I.
+
+ Definition kvnodeWriterSWnRaw γ s l n : vProp Σ :=
+ (∃ (γ_x: gname) (γ': gname),
+ ⌜n = encode (γ,γ_x,γ')⌠∗ WAEx(A := kvtype)(GPSG := GPSG) l γ γ_x s)%I.
+
+Program Definition kvnode_nWSP_def γ l s : vProp Σ :=
+ MonPred (λ V, persisted l (kvnodeSWnRaw γ) (λ l X, kvnodeWriterSWnRaw γ s l X V)) _.
+Next Obligation. solve_proper. Qed.
+
+ Notation F γ := (IP γ true).
+ Notation F_past γ := (IP γ false).
+
+ Lemma write_spec n ain vals
+ γ s s' (E : coPset)
+ (P: vProp Σ) (Q : gname → pr_state Prtcl → vProp Σ)
+ (Le: s ⊑ s') (HN : ↑physN ⊆ E) (HNl: ↑persist_locN .@ n ⊆ E):
+ {{{ ⎡PSCtx⎤ ∗ ([∗ list] i ∈ seq 0 8, ZplusPos (Z.of_nat i) ain ↦ kvget i vals) ∗ ▷ (∀ v', P ∗ F γ n s v' ∗ kvnode_nWSP_def γ n s'
+ ={E ∖ ↑persist_locN .@ n}=∗ Q γ s' ∗ ▷ (F γ n s' vals) ∗ ▷ F_past γ n s' vals)
+ ∗ P ∗ kvnode_nWSP_def γ n s }}} write #n #ain
+ {{{ RET #(); Q γ s' }}}.
+ Proof.
+ iIntros (Φ) "(#ctx & in & Hshift & P & prot) Hpost".
+
+ 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.
+ iMod (persistor_open with "prot").
+
+(* iDestruct "node_state" as "(% & kV & oL & data)".
+ iApply (GPS_SW_Read_ex (versionP n g) with "[$kI $kV]");
+ [auto | auto | ..].
+ { iNext; rewrite monPred_objectively_forall; iIntros (?).
+ iApply objectively_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⌠∗
+ ([∗ 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 ?) "!# (% & % & 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.
+ 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.
+ - 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 (L1) "[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_master_eq _ _ _ _ _ (hist_join (list.listC ZC)) with "oL oL'") as "%"; subst L1.
+ 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 own_op.
+ erewrite <- master_op, own_op.
+ iMod "oL" as "((oL & oL') & #?)".
+ 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".
+ { 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 "#".
+ Qed.*)
+Admitted.
+
+ Opaque replicate write mult.
+
+ Lemma writer_spec n L v g N (HN : base_mask ## ↑N):
+ {{{ ⎡PSCtx⎤ ∗ node_state_W L v n g ∗ inv N (∃ L, ⎡own g (Master (1/2) L)⎤) }}} writer #n
+ {{{ RET #();
+ let L' := map_of_list (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 3))) ∪ L in
+ node_state_W L' (v + 6) n g }}}.
+ Proof.
+ intros; iIntros "(#kI & node_state & #I) Hpost".
+ unfold writer.
+ unfold of_val at 1.
+ wp_rec'.
+ rewrite subst_for; last done.
+ unfold subst; fold subst; simpl.
+ rewrite !is_closed_nil_subst; try done.
+ match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
+ wp_bind (malloc _)%E; clear Hclosed.
+ iApply wp_mask_mono; first auto.
+ iApply (malloc_spec with "kI"); [omega|done|].
+ iNext; iIntros (l) "data".
+ wp_rec'.
+ 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 (wp_for_simple with "[] [data]").
+ { instantiate (1 := (fun i : Z => ⌜0 <= i <= 8⌠∗
+ ([∗ list] i ∈ seq 0 (Z.to_nat i), (ZplusPos (Z.of_nat i) l ↦ 0)) ∗
+ ([∗ list] i ∈ seq (Z.to_nat i) (8 - Z.to_nat i), (ZplusPos (Z.of_nat i) l ↦ ?)))%I).
+ iIntros "!#" (i ?) "!# (% & % & data & rest) Hpost".
+ wp_let.
+ wp_op.
+ destruct (8 - Z.to_nat i)%nat eqn: Hi.
+ { lapply (Nat.sub_gt 8 (Z.to_nat i)); first done.
+ change 8%nat with (Z.to_nat 8); apply Z2Nat.inj_lt; omega. }
+ change (seq _ (S _)) with (Z.to_nat i :: seq (S (Z.to_nat i)) n0); simpl.
+ iDestruct "rest" as "[Hi rest]".
+ rewrite Z2Nat.id; last omega.
+ iApply (na_write with "[$kI $Hi]"); first auto.
+ iNext; iIntros; iApply "Hpost".
+ iSplit; first by iPureIntro; omega.
+ rewrite Z2Nat.inj_add; try omega.
+ rewrite Nat.sub_add_distr Hi Nat.add_1_r seq_S big_sepL_app; simpl.
+ rewrite Nat.sub_0_r; iFrame.
+ rewrite Z2Nat.id; [auto | omega]. }
+ { simpl; change (seq 0 (Z.to_nat 0)) with (@nil nat); auto. }
+ iNext; iIntros "H"; iDestruct "H" as (i) "(% & % & data & _)".
+ assert (i = 8) by omega; subst.
+ wp_rec'.
+ iApply (wp_for_simple with "[] [node_state data]").
+ - apply I.
+ - instantiate (1 := (fun i => ⌜0 <= i <= 3⌠∗ ([∗ list] j ∈ seq 0 8, (ZplusPos (Z.of_nat j) l ↦ i)) ∗
+ let L' := map_of_list (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 (Z.to_nat i))))
+ ∪ L in node_state_W L' (v + (2 * Z.to_nat i)) n g)%I).
+ iIntros "!#" (i ?) "!# (% & % & data & node_state) Hpost".
+ match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
+ wp_let.
+ rewrite is_closed_nil_subst; last apply I.
+ wp_bind (for_loop _ _ _ _).
+ iApply (wp_for_simple with "[] [data]").
+ + instantiate (1 := (fun j => ⌜0 <= j <= 8⌠∗
+ ([∗ list] j ∈ seq 0 (Z.to_nat j), (ZplusPos (Z.of_nat j) l ↦ (i + 1))) ∗
+ ([∗ list] j ∈ seq (Z.to_nat j) (8 - Z.to_nat j), (ZplusPos (Z.of_nat j) l ↦ i)))%I).
+ iIntros "!#" (j ?) "!# (% & % & data & rest) Hpost".
+ wp_let.
+ do 2 wp_op.
+ wp_bind ([_]_na)%E.
+ destruct (8 - Z.to_nat j)%nat eqn: Hi.
+ { lapply (Nat.sub_gt 8 (Z.to_nat j)); first done.
+ change 8%nat with (Z.to_nat 8); apply Z2Nat.inj_lt; omega. }
+ change (seq _ (S _)) with (Z.to_nat j :: seq (S (Z.to_nat j)) n0); simpl.
+ iDestruct "rest" as "[Hj rest]".
+ rewrite Z2Nat.id; last omega.
+ iApply (na_read with "[$kI $Hj]"); first auto.
+ iNext; iIntros (?) "[% Hj]"; subst.
+ wp_op.
+ iApply (na_write with "[$kI $Hj]"); first auto.
+ iNext; iIntros; iApply "Hpost".
+ iSplit; first by iPureIntro; omega.
+ rewrite Z2Nat.inj_add; try omega.
+ rewrite Nat.sub_add_distr Hi Nat.add_1_r seq_S big_sepL_app; simpl.
+ rewrite Nat.sub_0_r; iFrame.
+ rewrite Z2Nat.id; [auto | omega].
+ + simpl; change (seq 0 (Z.to_nat 0)) with (@nil nat); auto.
+ + iNext; iIntros "H"; iDestruct "H" as (j) "(% & % & data & _)".
+ assert (j = 8) by omega; subst.
+ wp_seq.
+ iApply (wp_wand with "[-Hpost]"); last by iApply "Hpost".
+ iAssert ([∗ list] j↦x ∈ replicate 8 (i+1), ZplusPos (Z.of_nat j) l ↦ x)%I with "[data]" as "data".
+ { by rewrite big_sepL_replicate. }
+ iApply (LA_Inv' _ _ _ _ _ (fun L => ⎡own g (Master (1/2) L)⎤)%I with "[-]"); [auto | auto | ..].
+ { iApply LA_Csq; last (by iApply write_spec; last by iFrame); auto.
+ iIntros "!#" (??) "[oL H]".
+ iModIntro; iSplitL "oL"; [auto | iApply "H"]. }
+ unfold atomic_shift.
+ iExists emp%I; iSplit; first auto.
+ iIntros "!# _".
+ iModIntro; iExists (); iFrame "I"; iSplit; first auto.
+ iIntros (?) "H"; iModIntro.
+ iSplit; first by iPureIntro; omega.
+ iDestruct "H" as (?) "(% & ? & ?)"; subst.
+ rewrite big_sepL_replicate; iFrame.
+ rewrite Z2Nat.inj_add; try omega.
+ rewrite Nat.add_1_r seq_S List.map_app rev_app_distr; simpl.
+ rewrite Z2Nat.id; last omega.
+ by rewrite -(Nat.add_1_r (Z.to_nat i)) !Nat.mul_add_distr_l -!plus_assoc insert_union_l.
+ - simpl; change (seq 0 (Z.to_nat 0)) with (@nil nat); simpl.
+ rewrite left_id Nat.add_0_r; iFrame; auto.
+ - iNext; iIntros "H"; iDestruct "H" as (i) "(% & % & data & node_state)".
+ assert (i = 3) by omega; subst.
+ by iApply "Hpost".
+ Qed.
+
+ Opaque read.
+
+ Lemma reader_spec n L v g N (HN : base_mask ## ↑N):
+ {{{ ⎡PSCtx⎤ ∗ node_state_R L v n g ∗ inv N (∃ L, ⎡own g (Master (1/2) L)⎤) }}} reader #n
+ {{{ RET #(); ∃ L' v', ⌜L ⊆ L'⌠∗ node_state_R L' v' n g }}}.
+ Proof.
+ intros; iIntros "(#kI & node_state & #I) Hpost".
+ unfold reader.
+ wp_let.
+ wp_bind (malloc _)%E.
+ iApply wp_mask_mono; first auto.
+ iApply (malloc_spec with "kI"); [omega|done|].
+ iNext; iIntros (l) "data".
+ wp_let.
+ iApply (wp_wand with "[-Hpost]");
+ last by instantiate (1 := (fun v => ⌜v = #()⌠∗ _)%I); iIntros (?) "[%?]"; subst; iApply "Hpost".
+ iApply (LA_Inv' _ _ _ _ _ (fun L => ⎡own g (Master (1/2) L)⎤)%I with "[-]"); [auto | auto | ..].
+ { iApply LA_Csq; last (by iApply read_spec; last by iFrame); auto.
+ iIntros "!#" (??) "[oL H]".
+ iModIntro; iSplitL "oL"; [auto | iApply "H"]. }
+ unfold atomic_shift.
+ iExists emp%I; iSplit; first auto.
+ iIntros "!# _".
+ iModIntro; iExists (); iFrame "I"; iSplit; first auto.
+ iIntros (?) "H"; iModIntro.
+ iDestruct "H" as (?) "(% & H)"; iSplit; first auto.
+ iDestruct "H" as (???) "((% & % & % & % & %) & ? & ?)"; eauto.
+ Qed.
+
+End Protocol.
+
+End proof.
+
+End kvnode.
diff --git a/theories/gps/shared2.v b/theories/gps/shared2.v
new file mode 100644
index 0000000000000000000000000000000000000000..6c0f1e053ea70d604682e21d5e1a5af9d02faa6a
--- /dev/null
+++ b/theories/gps/shared2.v
@@ -0,0 +1,425 @@
+From iris.algebra Require Export auth frac excl gmap gset local_updates agree.
+From iris.program_logic Require Import ectx_lifting.
+From iris.bi Require Import big_op.
+From iris.proofmode Require Import tactics.
+
+From igps Require Export tactics notation.
+From igps Require Export blocks_generic blocks proofmode viewpred shared.
+From igps.base Require Export ghosts.
+
+Section Data.
+
+Context {A : Type} `{CountableA : Countable A}.
+
+Notation interpC Σ Prtcl := (bool -c> loc -c> pr_state Prtcl -c> A -c> vProp Σ).
+
+Notation state_sort Prtcl := (leibnizC (pr_state Prtcl * (A * View))%type).
+Notation state_type Prtcl := (gset (state_sort Prtcl)).
+
+Section STS.
+ Context {Σ : gFunctors} {fG : foundationG Σ} {Prtcl : protocolT} `{PF : !protocol_facts Prtcl}.
+ Set Default Proof Using "Type*".
+
+ Global Instance pr_SqSubsetEq : SqSubsetEq (pr_state Prtcl)
+ := λ s_0 s_1, pr_steps _ s_0 s_1.
+ (* Global Instance pr_PreOrder : PreOrder ((⊑) : relation (pr_state Prtcl)). *)
+ (* Proof using PF. *)
+ (* econstructor. *)
+ (* - exact: pr_steps_refl. *)
+ (* - exact: pr_steps_trans. *)
+ (* Qed. *)
+
+ Notation stR := (gsetUR (state_sort Prtcl)).
+ Definition stateR := authR (authUR stR).
+ Global Instance gsetR_singleton `{Countable T} : Singleton T (gsetR T).
+ Proof. unfold gsetR. intros x. unfold cmra_car. apply {[x]}. Defined.
+
+ Global Instance stateR_IsOp (S1 S2 : stR) :
+ @proofmode_classes.IsOp stateR (â—¯ (â— S1 â‹… â—¯ S2)) (â—¯ (â— S1)) (â—¯ (â—¯ S2)) := _.
+
+ Global Instance stateR_IsOp_ (S1 S2 : stR) :
+ @proofmode_classes.IsOp stateR (◯ (Auth (ExclBot') ∅)) (◯ (◠S1)) (◯ (◠S2)).
+ Proof.
+ unfold proofmode_classes.IsOp. rewrite -auth_frag_op. done.
+ Qed.
+
+ Definition st_prst : state_sort Prtcl -> _ := fst.
+ Definition st_val : state_sort Prtcl -> _ := fst ∘ snd.
+ Definition st_view : state_sort Prtcl -> _ := snd ∘ snd.
+ Definition st_time := λ x s, st_view s !! x.
+
+
+ Global Instance st_time_adj_dec l :
+ ∀ a b : state_sort Prtcl, Decision (rel_of (st_time l) adj_opt a b).
+ Proof. move => a b /=.
+ case: (st_time l a); last first.
+ - right. move => [? [H ?]]. by inversion H.
+ - case: (st_time _ _); last first.
+ + right. move => [? [? H]]. by inversion H.
+ + move => t2 t1. case (decide (t2 = t1 + 1)%positive) => [->|H].
+ * left. by eexists.
+ * right. move => [? [[?] [?]]]. by subst.
+ Qed.
+
+End STS.
+
+Class gpsG Σ Prtcl (PF : protocol_facts Prtcl) :=
+ {
+ gps_inG :> inG Σ stateR;
+ gps_ExWrG :> inG Σ (authR (optionUR (prodR fracR (agreeR (state_sort Prtcl)))))
+ }.
+Definition gpsΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors :=
+ #[ GFunctor (constRF stateR); GFunctor (constRF (authR (optionUR (prodR fracR (agreeR (state_sort Prtcl)))))) ].
+
+Instance subG_gpsG {Σ} Prtcl PF : subG (gpsΣ Prtcl PF) Σ → gpsG Σ Prtcl PF.
+Proof. solve_inG. Qed.
+
+Arguments st_prst [_] _ /.
+Arguments st_val [_] _ /.
+Arguments st_view [_] _ /.
+(* Arguments st_time [_] _ _ /. *)
+(* Arguments sts.tok [_] _ /. *)
+Arguments gpsG _ _ _ : clear implicits.
+(* Arguments gpsG _ _ _ _ _ : clear implicits. *)
+(* Arguments stateR _ _. *)
+
+
+Section Setup.
+ Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
+ Set Default Proof Using "Type".
+ Local Notation iProp := (iProp Σ).
+ Local Notation vPred := (vProp Σ).
+ Notation state_sort := (leibnizC (pr_state Prtcl * (A * View)))%type.
+ Implicit Types
+ (s : pr_state Prtcl)
+ (ζ : state_type Prtcl)
+ (e : state_sort)
+ (S : state_sort)
+ (v : A)
+ (V : View)
+ (h : gset (A * View)).
+
+ Notation F := (IP true l).
+ Notation F_past := (IP false l).
+
+
+ Section Assertions.
+
+ Definition sBE ζ := block_ends (rel_of (st_time l) (adj_opt)) ζ.
+ Definition sEx ζ (e_x: state_sort) : gset state_sort
+ := {[ e <- ζ | (st_view e_x !! l : option positive) ⊑ st_view e !! l]}.
+
+ Definition BE_Inv ζ e_x :=
+ ([∗ set] b ∈ sEx (sBE ζ) e_x, monPred_at (F (st_prst b) (st_val b)) (st_view b))%I.
+
+ Definition All_Inv ζ :=
+ ([∗ set] b ∈ ζ, monPred_at (F_past (st_prst b) (st_val b)) (st_view b))%I.
+
+ Definition ProtoInv ζ e_x := (BE_Inv ζ e_x ∗ All_Inv ζ)%I.
+
+ Definition SortInv l ζ : Prop :=
+ ∀ S1 S2,
+ S1 ∈ ζ → S2 ∈ ζ →
+ st_time l S1 ⊑ st_time l S2 → st_prst S1 ⊑ st_prst S2.
+
+ Definition Consistent ζ h : Prop :=
+ @equiv _ collection_equiv {[ (st_val e, st_view e) | e <- ζ]} h.
+
+ Instance Consistent_proper:
+ Proper (collection_equiv ==> collection_equiv ==> (flip impl) ) Consistent.
+ Proof.
+ unfold Consistent.
+ move => X Y HXY h1 h2 Hh12 ?.
+ rewrite -/(equiv _) in HXY. rewrite -/(equiv _) in Hh12. by rewrite -> HXY, Hh12.
+ Qed.
+
+ Lemma Consistent_insert ζ h s v V:
+ Consistent ζ h → Consistent ({[s, (v, V)]} ∪ ζ) ({[v, V]} ∪ h).
+ Proof.
+ rewrite /Consistent. move => <-.
+ rewrite (_: {[v, V]} =
+ {[(st_val e, st_view e) | e <- {[s, (v, V)]}]}).
+ by rewrite -gset_map_union.
+ apply set_unfold_2. split.
+ - move => ->. by exists (s, (v, V)).
+ - by move => [? [-> ->]].
+ Qed.
+
+ Definition exwr γ_x p e := own.own γ_x (◯ (Some (p, to_agree e))).
+
+ Definition final_st s := ∀ s', s' ⊑ s.
+
+ Definition FinalInv (e_x : state_sort) ζ :=
+ ∀ e t, e ∈ ζ -> st_time l e_x ⊑ Some t -> Some t ⊑ st_time l e ->
+ (∀ e', e' ∈ ζ -> st_time l e' ≠Some t) -> final_st (st_prst e).
+
+ Definition StateInjection ζ :=
+ ∀ e1 e2, e1 ∈ ζ → e2 ∈ ζ →
+ (st_val e1, st_view e1) = (st_val e2, st_view e2) ↔ e1 = e2.
+
+(* Definition gps_inv γ γ_x : iProp
+ := (∃ ζ h e_x, own.own γ (◠(◠ζ ⋅ ◯ ζ))
+ ∗ own.own γ_x (◠(Some (1%Qp, to_agree e_x)))
+ ∗ Hist l h ∗ ProtoInv ζ e_x
+ ∗ ⌜init l h⌠∗ ⌜SortInv l ζ⌠∗ ⌜e_x ∈ ζâŒ
+ ∗ ⌜Consistent ζ h⌠∗ ⌜FinalInv e_x ζ⌠∗ ⌜StateInjection ζâŒ)%I.*)
+
+ Notation gps_own := (λ γ aζ, @own.own _ _(gps_inG) γ (◯ aζ)).
+ Definition Writer γ ζ : iProp := (gps_own γ (◠ζ ⋅ ◯ ζ)).
+ Definition Reader γ ζ : iProp := (gps_own γ (◯ ζ)).
+
+ Definition maxTime V ζ : Prop := ∀ e, e ∈ ζ → (st_view e) !! l ⊑ (V !! l : option positive).
+
+ Arguments Writer _ _ /.
+ Arguments Reader _ _ /.
+
+ (* WIP: exposing state ghost name and observance *)
+ Definition PrtSeen γ s := (∃ V_0 v, monPred_in V_0 ∧ ⎡Reader γ {[s, (v, V_0)]}⎤)%I.
+
+ (* TODO: probably not needed anymore *)
+ (* Global Instance PrtSeen_persistent γ s V : *)
+ (* Persistent (PrtSeen γ s). *)
+ (* Proof. *)
+ (* split => ?. *)
+ (* rewrite /PrtSeen. unseal. *)
+ (* apply: bi.exist_persistent. *)
+ (* Qed. *)
+
+ Lemma StateInjection_insert s v V h ζ
+ (Cons: Consistent ζ h) (SI: StateInjection ζ) (HDisj: h ## {[v,V]})
+ : StateInjection ({[s, (v, V)]} ∪ ζ).
+ Proof.
+ move => e1 e2 /elem_of_union [/elem_of_singleton ->| In1]
+ /elem_of_union [/elem_of_singleton ->| In2];
+ [done|..|by apply SI].
+ - split; last by move => <-.
+ move => Eq. exfalso. apply disjoint_singleton_r in HDisj.
+ apply HDisj. rewrite Eq -Cons elem_of_map_gset. by exists e2.
+ - split; last move => -> //.
+ move => Eq. exfalso. apply disjoint_singleton_r in HDisj.
+ apply HDisj. rewrite -Eq -Cons elem_of_map_gset. by exists e1.
+ Qed.
+
+ Section Agreement.
+ Lemma Writer_latest γ ζ1 ζ2
+ : Reader γ ζ1 ∗ Writer γ ζ2
+ ⊢ ⌜ζ1 ⊆ ζ2âŒ.
+ Proof.
+ iIntros "(Reader & Writer)".
+ iCombine "Writer" "Reader" as "oS".
+ iDestruct (own.own_valid with "oS") as %[V1 V2].
+ iPureIntro. move: (V1 O) => /=.
+ rewrite gset_op_union /includedN.
+ abstract set_solver+.
+ Qed.
+
+ Lemma Writer_Exclusive γ ζ1 ζ2
+ : Writer γ ζ1 ∗ Writer γ ζ2 ⊢ False.
+ Proof.
+ iIntros "(Writer1 & Writer2)".
+ iCombine "Writer1" "Writer2" as "oW".
+ by iDestruct (own.own_valid with "oW") as %[].
+ Qed.
+
+ Instance Reader_persistent γ ζ: Persistent (Reader γ ζ) := _.
+
+ Lemma Reader_extract γ ζ1 ζ2 (Sub: ζ2 ⊆ ζ1) :
+ Reader γ ζ1 ⊢ Reader γ ζ2.
+ Proof.
+ rewrite (union_difference_L _ _ Sub).
+ rewrite (_: ζ2 ∪ ζ1 ∖ ζ2 = ζ2 ⋅ (ζ1 ∖ ζ2)) => //.
+ rewrite /Reader !auth_frag_op.
+ iIntros "[$ _]".
+ Qed.
+
+
+ Lemma Writer_to_Reader γ ζ:
+ Writer γ ζ ⊢ Reader γ ζ.
+ Proof. iIntros "[_ $]". Qed.
+
+ Lemma Reader_fork_Auth γ ζ:
+ own.own γ (◠(◠ζ ⋅ ◯ ζ)) ⊢ |==> own.own γ (◠(◠ζ ⋅ ◯ ζ)) ∗ Reader γ ζ.
+ Proof.
+ iIntros "oA".
+ iMod (own.own_update _ _ (◠(◠ζ ⋅ ◯ ζ) ⋅ ◯ (◯ ζ)) with "[$oA]")
+ as "[oA oR]"; last by iFrame.
+ apply auth_update_alloc.
+ move => n /=.
+ move => [c|] [/= Le Val] [/= Ha Hb] /=;
+ rewrite /op /cmra_op /= in Ha;
+ rewrite ->!(left_id _ _) in Hb;
+ rewrite ->(left_id _ _) in Le; last first.
+ - repeat split => //=; by rewrite ->(left_id _ _).
+ - destruct c as [ac bc]. rewrite -!auth_both_op. repeat split => //=.
+ + apply union_subseteq_l.
+ + simpl in Hb. rewrite -Hb. abstract set_solver+.
+ Qed.
+
+ Lemma Reader_fork_Auth_2 γ ζ ζ' (Sub: ζ' ⊆ ζ):
+ own.own γ (◠(◠ζ ⋅ ◯ ζ)) ⊢ |==> own.own γ (◠(◠ζ ⋅ ◯ ζ)) ∗ Reader γ ζ'.
+ Proof.
+ iIntros "oA".
+ iMod (Reader_fork_Auth with "[$oA]") as "[oA oR]".
+ iModIntro. iFrame.
+ by iApply (Reader_extract _ ζ).
+ Qed.
+
+ Lemma Writer_fork_Reader γ ζ ζ' (Sub: ζ' ⊆ ζ):
+ Writer γ ζ ⊢ Writer γ ζ ∗ Reader γ ζ'.
+ Proof.
+ iIntros "Writer".
+ iDestruct (Writer_to_Reader with "[$Writer]") as "#Reader".
+ iFrame. by iApply (Reader_extract _ ζ).
+ Qed.
+
+ Lemma Writer_exact γ ζ ζ':
+ own.own γ (â— (◠ζ' â‹… â—¯ ζ')) ∗ Writer γ ζ ⊢ ⌜ζ' = ζâŒ.
+ Proof.
+ iIntros "[oA oW]".
+ iCombine "oA" "oW" as "oS".
+ iDestruct (own.own_valid with "oS") as %[V1 _].
+ iPureIntro.
+ move: {V1} (V1 O) => /cmra_discrete_included_iff /=.
+ rewrite auth_included; move => [/Excl_included /leibniz_equiv_iff Eq _].
+ by subst.
+ Qed.
+
+ Lemma Writer_extract γ ζ:
+ own.own γ (◠(◠ζ ⋅ ◯ ζ)) ∗ own.own γ (◯ (◠ζ))
+ ⊢ |==> own.own γ (◠(◠ζ ⋅ ◯ ζ)) ∗ Writer γ ζ.
+ Proof.
+ rewrite -2!own.own_op {2}(auth_both_op ζ ∅).
+ apply own.own_update, auth_update, auth_local_update => //.
+ by apply gset_local_update.
+ Qed.
+
+ Lemma Writer_update γ ζ ζ' (Sub: ζ ⊆ ζ'):
+ own.own γ (◠(◠ζ ⋅ ◯ ζ)) ∗ Writer γ ζ
+ ⊢ |==> own.own γ (◠(◠ζ' ⋅ ◯ ζ')) ∗ Writer γ ζ'.
+ Proof.
+ rewrite /Writer -2!own.own_op.
+ apply own.own_update, auth_update, auth_local_update => //.
+ by apply gset_local_update.
+ Qed.
+
+ Lemma Writer_update_2 γ ζ0 ζ ζ' (Sub: ζ ⊆ ζ'):
+ own.own γ (◠(◠ζ0 ⋅ ◯ ζ0)) ∗ Writer γ ζ
+ ⊢ |==> own.own γ (◠(◠ζ' ⋅ ◯ ζ')) ∗ Writer γ ζ'.
+ Proof.
+ iIntros "(oA & Writer)".
+ iDestruct (Writer_exact with "[$oA $Writer]") as %Eq.
+ rewrite Eq.
+ by iApply (Writer_update with "[$oA $Writer]").
+ Qed.
+
+ Lemma Reader_Writer_sub γ ζ ζ':
+ Writer γ ζ' ∗ Reader γ ζ ⊢ ⌜ζ ⊆ ζ'âŒ.
+ Proof.
+ rewrite -own.own_op. iIntros "oA".
+ iDestruct (own.own_valid with "oA") as %Valid%auth_valid_discrete.
+ iPureIntro.
+ move : Valid => /= /auth_valid_discrete /=.
+ move => [/gset_included H _]. move: H.
+ rewrite -> (left_id _ _). abstract set_solver+.
+ Qed.
+
+ Lemma Reader_Auth_sub γ ζ ζ':
+ own.own γ (â— (◠ζ' â‹… â—¯ ζ')) ∗ Reader γ ζ ⊢ ⌜ζ ⊆ ζ'âŒ.
+ Proof.
+ rewrite -own.own_op.
+ iIntros "oA".
+ iDestruct (own.own_valid with "oA") as %Valid%auth_valid_discrete.
+ iPureIntro.
+ move : Valid => /=.
+ rewrite auth_included /= => [[[_ /gset_included Incl] _]].
+ set_solver+Incl.
+ Qed.
+
+(* Lemma Reader_singleton_agree γ γ_x s1 v1 V1 s2 v2 V2 E:
+ ▷ gps_inv γ γ_x ∗
+ Reader γ {[s1, (v1, V1)]} ∗ Reader γ {[s2, (v2, V2)]}
+ ⊢ |={E}=> â–· gps_inv γ γ_x ∗ ⌜s1 ⊑ s2 ∨ s2 ⊑ s1âŒ.
+ Proof.
+ iIntros "(oI & #oR1 & #oR2)". unfold gps_inv.
+ iDestruct "oI" as (ζ h e_x) "(>oA & ? & ? & ? & ? & >% & ?)".
+ iDestruct (Reader_Auth_sub with "[$oA $oR1]")
+ as %In1%elem_of_subseteq_singleton.
+ iDestruct (Reader_Auth_sub with "[$oA $oR2]")
+ as %In2%elem_of_subseteq_singleton.
+ iModIntro. iSplitR "".
+ - iExists ζ, h, e_x. iFrame. by iNext.
+ - iPureIntro.
+ case (decide ((V1 !! l : option positive) ⊑ V2 !! l)) => [Le|NLe].
+ + left. apply (H _ _ In1 In2 Le).
+ + right. apply (H _ _ In2 In1).
+ rewrite /st_time /=. move : NLe.
+ case: (V1 !! l); case : (V2 !! l) => //. cbn.
+ move => t1 t2 /Pos.lt_nle NLe. by apply Pos.lt_le_incl.
+ Qed.
+
+
+ Lemma Writer_sorted γ γ_x ζ E:
+ ▷ gps_inv γ γ_x ∗ Writer γ ζ
+ ⊢ |={E}=> â–· gps_inv γ γ_x ∗ Writer γ ζ ∗ ⌜SortInv l ζâŒ.
+ Proof.
+ iIntros "[oI oW]".
+ iDestruct "oI" as (ζ' h e_x) "(>oA & oEx & Hist & oPr & ? & >% & ?)".
+ iDestruct (Writer_exact with "[$oA $oW]") as %?. subst ζ'.
+ iFrame (H) "oW".
+ iModIntro. iNext.
+ iExists ζ, h, e_x. by iFrame.
+ Qed.*)
+
+ Lemma ExWrite_agree γ e1 e2 q1 q2:
+ own.own γ (â— Some (q1, to_agree e1)) ∗ exwr γ q2 e2 ⊢ ⌜e1 = e2âŒ.
+ Proof.
+ rewrite -own.own_op. iIntros "oX".
+ iDestruct (own.own_valid with "oX")
+ as %[oXIn%Some_included oX]%auth_valid_discrete_2.
+ by move: oXIn => [[_ /to_agree_inj]|/prod_included[_ /to_agree_included]].
+ Qed.
+
+ End Agreement.
+
+Definition WAEx γ γ_x s : vProp Σ
+ := (∃ v V_0 ζ, (monPred_in V_0)
+ ∧ ⎡Writer γ ζ ∗ exwr γ_x 1%Qp (s, (v, V_0))
+ ∗ Reader γ {[s, (v, V_0)]}
+ ∗ ⌜maxTime V_0 ζâŒâŽ¤)%I.
+
+ End Assertions.
+End Setup.
+End Data.
+
+Arguments WAEx _ _ _ / _.
+
+Notation interpC Σ Prtcl A := (bool -c> loc -c> pr_state Prtcl -c> A -c> vProp Σ).
+Notation state_sort Prtcl A := (leibnizC (pr_state Prtcl * (A * View))%type).
+Notation state_type Prtcl A := (gset (state_sort Prtcl A)).
+
+(*Global Instance gps_inv_ne `{foundationG Σ} `{gpsG Σ prtcl} :
+ Proper (dist n ==> (=) ==> (=) ==> (=) ==> dist n) gps_inv.
+Proof.
+ intros n f1 f2 Hf ??-> ??-> ??->.
+ rewrite /= /gps_inv /ProtoInv /BE_Inv /All_Inv.
+ repeat f_equiv; apply Hf.
+Qed.
+
+Global Instance ProtoInv_proper {Σ Prtcl PF}:
+ Proper ((≡) ==> (=) ==> (≡) ==> (=) ==> (≡)) (@ProtoInv Σ Prtcl PF).
+Proof.
+ rewrite /ProtoInv /All_Inv /BE_Inv /sEx /sBE.
+ intros ? ? H1 ? ? H2 ? ? H3 ? ? H4.
+ subst. apply bi.sep_proper.
+ - rewrite big_opS_proper; last first.
+ + intros ??. apply H1.
+ + f_equiv; set_solver.
+ - rewrite big_opS_proper; last first.
+ + intros ??. apply H1.
+ + f_equiv; set_solver.
+Qed.
+
+Global Instance gps_inv_proper `{foundationG Σ} `{gpsG Σ prtcl} :
+ Proper ((≡) ==> (=) ==> (=) ==> (=) ==> (≡)) gps_inv.
+Proof. rewrite /gps_inv. solve_proper. Qed.
+*)
\ No newline at end of file