Prove invariance w.r.t. PCR prepare (except stability)

src/program_proof/rsm/big_sep.v

@@ -474,7 +474,7 @@ Section bi.
     by iDestruct (big_sepS_subseteq_difference_2 with "HY HXY") as "HX"; first apply Hsubseteq.
   Qed.
 
-  Lemma big_sepS_partition
+  Lemma big_sepS_partition_1
     `{!BiAffine PROP} `{Countable A} (Φ : A -> PROP) (X : gset A) `{Countable B} (Y : gset B)
     (P : A -> B -> Prop) `{∀ x y, Decision (P x y)} :
     (∀ x y1 y2, y1 ≠ y2 -> P x y1 -> not (P x y2)) ->
@@ -516,6 +516,38 @@ Section bi.
     iApply (big_sepS_insert_2 with "Hx HX").
   Qed.
 
+  Lemma big_sepS_partition_2
+    `{!BiAffine PROP} `{Countable A} (Φ : A -> PROP) (X : gset A) `{Countable B} (Y : gset B)
+    (P : A -> B -> Prop) `{∀ x y, Decision (P x y)} :
+    (∀ x, x ∈ X -> ∃ y, y ∈ Y ∧ P x y) ->
+    ([∗ set] y ∈ Y, [∗ set] x ∈ filter (λ x', P x' y) X, Φ x) -∗
+    ([∗ set] x ∈ X, Φ x).
+  Proof.
+    iIntros (Hpart) "HYX".
+    iInduction X as [| x X Hnotin] "IH" using set_ind_L.
+    { by iApply big_sepS_empty. }
+    rewrite big_sepS_union; last set_solver.
+    assert (Hx : x ∈ {[x]} ∪ X) by set_solver.
+    pose proof (Hpart _ Hx) as (y & Hy & HP).
+    iDestruct (big_sepS_elem_of_acc_impl with "HYX") as "[HΦ HYX]"; first apply Hy.
+    rewrite filter_union_L big_sepS_union; last set_solver.
+    iDestruct "HΦ" as "[Hx HX]".
+    (* rewrite filter_union_L elem_of_union in Hpart. *)
+    (* destruct Hpart as [Hin | Hcontra]; last set_solver. *)
+    rewrite filter_singleton_L; last apply HP.
+    iFrame "Hx".
+    iSpecialize ("HYX" $! (λ y, [∗ set] x ∈ filter (λ x', P x' y) X, Φ x)%I with "[] HX").
+    { iIntros "!>" (y' _ _) "HΦ".
+      rewrite filter_union_L big_sepS_union; last set_solver.
+      by iDestruct "HΦ" as "[_ HΦ]".
+    }
+    iApply ("IH" with "[] HYX").
+    iPureIntro.
+    intros x' Hx'.
+    assert (Hin : x' ∈ {[x]} ∪ X) by set_solver.
+    by apply Hpart.
+  Qed.
+
 End bi.
 
 Section bupd.

src/program_proof/rsm/pure/extend.v

@@ -153,4 +153,9 @@ Section lemmas.
     by rewrite Hlast.
   Qed.
 
+  Lemma last_extend_not_nil_inv n l :
+    last_extend n l ≠ [] ->
+    l ≠ [].
+  Proof. intros Hext Hl. by rewrite /last_extend Hl /= in Hext. Qed.
+
 End lemmas.

src/program_proof/rsm/pure/quorum.v

@@ -56,6 +56,12 @@ Section lemma.
     lia.
   Qed.
 
+  Lemma cquorum_elem_of c q x :
+    x ∈ q ->
+    cquorum c q ->
+    x ∈ c.
+  Proof. intros Helem [Hincl _]. set_solver. Qed.
+
   Lemma quorums_overlapped c q1 q2 :
     (cquorum c q1 ∨ fquorum c q1) ->
     (cquorum c q2 ∨ fquorum c q2) ->
@@ -74,6 +80,15 @@ Section lemma.
       (apply (quorums_overlapped_raw c); [done | done | lia]).
   Qed.
 
+  Lemma cquorums_overlapped c q1 q2 :
+    cquorum c q1 ->
+    cquorum c q2 ->
+    ∃ x, x ∈ q1 ∧ x ∈ q2.
+  Proof.
+    intros Hq1 Hq2.
+    by eapply quorums_overlapped; left.
+  Qed.
+
   Lemma quorums_sufficient c qc qf :
     cquorum_size c qc ->
     fquorum_size c qf ->
@@ -96,7 +111,7 @@ Section lemma.
   Qed.
 
   Lemma cquorum_refl c :
-    (1 < size c)%nat ->
+    (1 ≤ size c)%nat ->
     cquorum c c.
   Proof.
     split; first done.

src/program_proof/tulip/base.v

@@ -89,8 +89,10 @@ Definition txnst_to_u64 (s : txnst) :=
   | StAborted => (U64 3)
   end.
 
-Definition groupid := w64.
-Definition gids_all : gset groupid := list_to_set (fmap W64 (seqZ 0 2)).
+Definition gids_all : gset u64 := list_to_set (fmap W64 (seqZ 0 2)).
+
+(* TODO: Parametrize the number of replicas in each group. *)
+Definition rids_all : gset u64 := list_to_set (fmap W64 (seqZ 0 2)).
 
 (** Transaction R/C/A action. *)
 Inductive action :=
@@ -100,10 +102,8 @@ Inductive action :=
 
 (** State-machine commands. *)
 Inductive command :=
-| CmdRead (tid : nat) (key : dbkey)
-| CmdPrep (tid : nat) (wrs : dbmap)
-| CmdCmt (tid : nat)
-| CmdAbt (tid : nat).
+| CmdCommit (tid : nat) (pwrs : dbmap)
+| CmdAbort (tid : nat).
 
 #[global]
 Instance command_eq_decision :
@@ -119,11 +119,11 @@ Admitted.
 Definition dblog := list command.
 
 (** Converting keys to group IDs. *)
-Definition key_to_group (key : dbkey) : groupid.
+Definition key_to_group (key : dbkey) : u64.
 Admitted.
 
 (** Participant groups. *)
-Definition ptgroups (keys : gset dbkey) : gset groupid :=
+Definition ptgroups (keys : gset dbkey) : gset u64 :=
   set_map key_to_group keys.
 
 Definition wrs_group gid (wrs : dbmap) :=
@@ -132,10 +132,14 @@ Definition wrs_group gid (wrs : dbmap) :=
 Definition tpls_group gid (tpls : gmap dbkey dbtpl) :=
   filter (λ t, key_to_group t.1 = gid) tpls.
 
+(* TODO: [filter_group] subsumes [wrs_group] and [tpls_group]. *)
+Definition filter_group `{Countable A} gid (m : gmap dbkey A) :=
+  filter (λ t, key_to_group t.1 = gid) m.
+
 Definition keys_group gid (keys : gset dbkey) :=
   filter (λ k, key_to_group k = gid) keys.
 
-Definition valid_pwrs (gid : groupid) (pwrs : dbmap) :=
+Definition valid_pwrs (gid : u64) (pwrs : dbmap) :=
   dom pwrs ⊆ keys_group gid keys_all.
 
 Lemma elem_of_key_to_group key :
@@ -217,6 +221,9 @@ Definition readable (tid : nat) (hist : dbhist) (tsprep : nat) :=
 Definition lockable (tid : nat) (hist : dbhist) (tsprep : nat) :=
   tsprep = O ∧ (length hist ≤ tid)%nat.
 
+Definition tuples_lockable (tid : nat) (tpls : gmap dbkey dbtpl) :=
+  map_Forall (λ _ tpl, lockable tid tpl.1 tpl.2) tpls.
+
 (* Note the coercion here. [word] seems to work better with this. *)
 Definition valid_ts (ts : nat) := 0 < ts < 2 ^ 64.