Define and prove consensus resources

src/program_proof/rsm/pure/misc.v

@@ -5,3 +5,29 @@ Lemma set_Forall_Forall_subsume `{Countable A} (l : list A) (s : gset A) P :
   Forall (λ x, x ∈ s) l ->
   Forall P l.
 Proof. do 2 rewrite Forall_forall. intros HP Hl x Hin. by auto. Qed.
+
+Lemma gset_to_gmap_same_union `{Countable K} {A} (X Y : gset K) (x : A) :
+  gset_to_gmap x (X ∪ Y) = gset_to_gmap x X ∪ gset_to_gmap x Y.
+Proof.
+  apply map_eq.
+  intros i.
+  rewrite lookup_union 3!lookup_gset_to_gmap.
+  destruct (decide (i ∈ X)) as [Hinx | Hnotinx].
+  { rewrite option_guard_True.
+    { rewrite option_guard_True; last done.
+      by rewrite union_Some_l.
+    }
+    set_solver.
+  }
+  rewrite (option_guard_False (i ∈ X)); last done.
+  rewrite option_union_left_id.
+  destruct (decide (i ∈ Y)) as [Hiny | Hnotiny].
+  { rewrite option_guard_True.
+    { by rewrite option_guard_True. }
+    set_solver.
+  }
+  { rewrite option_guard_False.
+    { by rewrite option_guard_False. }
+    set_solver.
+  }
+Qed.

src/program_proof/tulip/base.v

@@ -308,6 +308,11 @@ Definition histmR := gmapR dbkey histR.
 Definition tsmR := gmapR dbkey (dfrac_agreeR natO).
 Canonical Structure dbkmodO := leibnizO dbkmod.
 Definition dbkmodR := gmapR dbkey (dfrac_agreeR dbkmodO).
+Canonical Structure ccommandO := leibnizO ccommand.
+Definition ccommandlR := mono_listR ccommandO.
+Definition group_ccommandlR := gmapR u64 ccommandlR.
+Definition ccommandsR := gsetR ccommand.
+Definition group_ccommandsR := gmapR u64 (dfrac_agreeR ccommandsR).
 Canonical Structure boolO := leibnizO bool.
 Canonical Structure natboolmvR := gmap_viewR nat (agreeR boolO).
 Definition group_natboolmvR := gmapR u64 natboolmvR.
@@ -341,6 +346,8 @@ Class tulip_ghostG (Σ : gFunctors) :=
     #[global] repl_tsG :: inG Σ tsmR;
     #[global] lnrz_kmodG :: inG Σ dbkmodR;
     #[global] cmtd_kmodG :: inG Σ dbkmodR;
+    #[global] txn_logG :: inG Σ group_ccommandlR;
+    #[global] txn_cpoolG :: inG Σ group_ccommandsR;
     (* txnsys resources defined in res_txnsys.v *)
     #[global] cmtd_histG :: inG Σ histmR;
     #[global] lnrz_histG :: inG Σ histmR;
@@ -383,8 +390,8 @@ Definition tulip_ghostΣ :=
      GFunctor tsmR;
      GFunctor dbkmodR;
      GFunctor dbkmodR;
-     GFunctor histmR;
-     GFunctor histmR;
+     GFunctor group_ccommandlR;
+     GFunctor group_ccommandsR;
      (* res_txnsys.v *)
      GFunctor histmR;
      GFunctor histmR;
@@ -432,6 +439,8 @@ Record tulip_names :=
     repl_ts : gname;
     lnrz_kmod : gname;
     cmtd_kmod : gname;
+    txn_log : gname;
+    txn_cpool : gname;
     (* res_txnsys.v *)
     cmtd_hist : gname;
     lnrz_hist : gname;

src/program_proof/tulip/paxos/base.v

@@ -396,8 +396,9 @@ Definition node_pxcmdlR := gmapR u64 (dfrac_agreeR pxcmdlO).
 Definition node_stringR := gmapR u64 (agreeR stringO).
 
 Class paxos_ghostG (Σ : gFunctors) :=
-  { #[global] proposalG :: ghost_mapG Σ nat gname;
-    #[global] stringmlG :: inG Σ stringmlR;
+  { #[global] stringmlG :: inG Σ stringmlR;
+    #[global] cpoolG :: ghost_mapG Σ string unit;
+    #[global] proposalG :: ghost_mapG Σ nat gname;
     #[global] base_proposalG :: ghost_mapG Σ nat ledger;
     #[global] prepare_lsnG :: inG Σ lsnmR;
     #[global] node_declistG :: inG Σ node_declistR;
@@ -412,10 +413,11 @@ Class paxos_ghostG (Σ : gFunctors) :=
   }.
 
 Definition paxos_ghostΣ :=
-  #[ ghost_mapΣ nat gname;
+  #[ GFunctor lsnmR;
+     ghost_mapΣ string unit;
+     ghost_mapΣ nat gname;
      GFunctor stringmlR;
      ghost_mapΣ nat ledger;
-     GFunctor lsnmR;
      GFunctor node_declistR;
      GFunctor node_proposalmR;
      GFunctor node_natmR;
@@ -432,10 +434,11 @@ Instance subG_paxos_ghostG {Σ} :
   subG paxos_ghostΣ Σ → paxos_ghostG Σ.
 Proof. solve_inG. Qed.
 
-Instance stagedG_paxos_ghostG Σ : paxos_ghostG Σ → stagedG Σ.
-Proof. Admitted.
+(* Instance stagedG_paxos_ghostG Σ : paxos_ghostG Σ → stagedG Σ. *)
 
 Record paxos_names := {
+    consensus_log : gname;
+    consensus_cpool : gname;
     proposal : gname;
     base_proposal : gname;
     prepare_lsn : gname;

src/program_proof/tulip/paxos/inv.v

@@ -505,7 +505,7 @@ Section inv.
   #[global]
   Instance paxos_inv_timeless γ nids :
     Timeless (paxos_inv γ nids).
-  Admitted.
+  Proof. apply _. Defined.
 
   Definition paxoscoreNS := paxosNS .@ "core".
 
@@ -532,7 +532,7 @@ Section inv_file.
   #[global]
   Instance paxos_file_inv_timeless γ nids :
     Timeless (paxos_file_inv γ nids).
-  Admitted.
+  Proof. apply _. Defined.
 
   Definition know_paxos_file_inv γ nids : iProp Σ :=
     inv paxosfileNS (paxos_file_inv γ nids).

src/program_proof/tulip/paxos/res.v

@@ -2,6 +2,7 @@ From iris.algebra Require Import mono_nat mono_list gmap_view gset.
 From iris.algebra.lib Require Import dfrac_agree.
 From Perennial.base_logic Require Import ghost_map mono_nat saved_prop.
 From Perennial.program_proof Require Import grove_prelude.
+From Perennial.program_proof.rsm.pure Require Import misc.
 From Perennial.program_proof.tulip.paxos Require Import base recovery.
 From Perennial.program_proof.tulip.paxos Require Export res_network.
 
@@ -14,21 +15,22 @@ Section res.
 
     (** Elements. *)
 
-    Definition own_log_half γ (l : ledger) : iProp Σ.
-    Admitted.
+    Definition own_log_half γ (l : ledger) : iProp Σ :=
+      own γ.(consensus_log) (mono_list_auth (A:=stringO) (DfracOwn (1 / 2)) l).
 
-    Definition is_log_lb γ (l : ledger) : iProp Σ.
-    Admitted.
+    Definition is_log_lb γ (l : ledger) : iProp Σ :=
+      own γ.(consensus_log) (mono_list_lb (A:=stringO)  l).
 
-    Definition own_cpool_half γ (vs : gset string) : iProp Σ.
-    Admitted.
+    Definition is_cmd_receipt γ (c : string) : iProp Σ :=
+      ghost_map_elem γ.(consensus_cpool) c DfracDiscarded tt.
+
+    Definition own_cpool_half γ (vs : gset string) : iProp Σ :=
+      ghost_map_auth γ.(consensus_cpool) (1 / 2) (gset_to_gmap tt vs) ∗
+      ([∗ set] v ∈ vs, is_cmd_receipt γ v).
 
     Definition own_consensus_half γ (l : ledger) (vs : gset string) : iProp Σ :=
       own_log_half γ l ∗ own_cpool_half γ vs.
 
-    Definition is_cmd_receipt γ (c : string) : iProp Σ.
-    Admitted.
-
     Definition cpool_subsume_log (l : ledger) (vs : gset string) :=
       Forall (λ v, v ∈ vs) l.
 
@@ -37,12 +39,12 @@ Section res.
     #[global]
     Instance is_log_lb_persistent γ l :
       Persistent (is_log_lb γ l).
-    Admitted.
+    Proof. apply _. Defined.
 
     #[global]
     Instance is_cmd_receipt_persistent γ v :
       Persistent (is_cmd_receipt γ v).
-    Admitted.
+    Proof. apply _. Defined.
 
     (** Rules. *)
 
@@ -51,55 +53,101 @@ Section res.
       own_log_half γ l1 -∗
       own_log_half γ l1 ==∗
       own_log_half γ l2 ∗ own_log_half γ l2.
-    Admitted.
+    Proof.
+      iIntros (Hprefix) "Hlx Hly".
+      iCombine "Hlx Hly" as "Hl".
+      iMod (own_update with "Hl") as "Hl".
+      { by apply mono_list_update. }
+      iDestruct "Hl" as "[Hlx Hly]".
+      by iFrame.
+    Qed.
 
     Lemma log_agree {γ} l1 l2 :
       own_log_half γ l1 -∗
       own_log_half γ l2 -∗
       ⌜l2 = l1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hlx Hly".
+      iDestruct (own_valid_2 with "Hlx Hly") as %Hvalid.
+      by apply mono_list_auth_dfrac_op_valid_L in Hvalid as [_ ->].
+    Qed.
 
     Lemma log_witness {γ l} :
       own_log_half γ l -∗
       is_log_lb γ l.
-    Admitted.
+    Proof. iApply own_mono. apply mono_list_included. Qed.
 
     Lemma log_prefix {γ l lb} :
       own_log_half γ l -∗
       is_log_lb γ lb -∗
       ⌜prefix lb l⌝.
-    Admitted.
+    Proof.
+      iIntros "Hl Hlb".
+      iDestruct (own_valid_2 with "Hl Hlb") as %Hvalid.
+      by apply mono_list_both_dfrac_valid_L in Hvalid as [_ ?].
+    Qed.
 
     Lemma log_lb_prefix {γ lb1 lb2} :
       is_log_lb γ lb1 -∗
       is_log_lb γ lb2 -∗
       ⌜prefix lb1 lb2 ∨ prefix lb2 lb1⌝.
-    Admitted.
+    Proof.
+      iIntros "Hlb1 Hlb2".
+      iDestruct (own_valid_2 with "Hlb1 Hlb2") as %Hvalid.
+      by apply mono_list_lb_op_valid_1_L in Hvalid.
+    Qed.
 
     Lemma cpool_update {γ vs1} vs2 :
       vs1 ⊆ vs2 ->
       own_cpool_half γ vs1 -∗
       own_cpool_half γ vs1 ==∗
       own_cpool_half γ vs2 ∗ own_cpool_half γ vs2.
-    Admitted.
+    Proof.
+      iIntros (Hincl) "[Hvsx #Hfrags] [Hvsy _]".
+      set vsnew := vs2 ∖ vs1.
+      iCombine "Hvsx Hvsy" as "Hvs".
+      iMod (ghost_map_insert_persist_big (gset_to_gmap tt vsnew) with "Hvs") as "[Hvs #Hfragsnew]".
+      { rewrite map_disjoint_dom 2!dom_gset_to_gmap. set_solver. }
+      iDestruct "Hvs" as "[Hvsx Hvsy]".
+      rewrite -gset_to_gmap_same_union.
+      rewrite big_sepM_gset_to_gmap.
+      iDestruct (big_sepS_union_2 with "Hfragsnew Hfrags") as "Hfrags'".
+      rewrite difference_union_L.
+      replace (vs2 ∪ vs1) with vs2 by set_solver.
+      by iFrame "∗ #".
+    Qed.
 
     Lemma cpool_agree {γ vs1} vs2 :
       own_cpool_half γ vs1 -∗
       own_cpool_half γ vs2 -∗
       ⌜vs2 = vs1⌝.
-    Admitted.
+    Proof.
+      iIntros "[Hvsx _] [Hvsy _]".
+      iDestruct (ghost_map_auth_agree with "Hvsx Hvsy") as %Heq.
+      iPureIntro.
+      replace vs1 with (dom (gset_to_gmap () vs1)); last by rewrite dom_gset_to_gmap.
+      replace vs2 with (dom (gset_to_gmap () vs2)); last by rewrite dom_gset_to_gmap.
+      by rewrite Heq.
+    Qed.
 
     Lemma cpool_witness {γ vs} v :
       v ∈ vs ->
       own_cpool_half γ vs -∗
       is_cmd_receipt γ v.
-    Admitted.
+    Proof.
+      iIntros (Hin) "[_ Hfrags]".
+      by iApply (big_sepS_elem_of with "Hfrags").
+    Qed.
 
     Lemma cpool_lookup {γ vs} v :
       is_cmd_receipt γ v -∗
       own_cpool_half γ vs -∗
       ⌜v ∈ vs⌝.
-    Admitted.
+    Proof.
+      iIntros "Hfrag [Hauth _]".
+      iDestruct (ghost_map_lookup with "Hauth Hfrag") as %Hlookup.
+      by apply lookup_gset_to_gmap_Some in Hlookup as [? _].
+    Qed.
 
   End consensus.
 

src/program_proof/tulip/program/txnlog/txnlog.v

@@ -230,7 +230,6 @@ Section program.
     (* Update the txn cpool. *)
     set tcpool' := _ ∪ tcpool.
     iMod (txn_cpool_update tcpool' with "Htcpool HtcpoolX") as "[Htcpool HtcpoolX]".
-    { set_solver. }
     (* Apply the view shift. *)
     iMod ("HAU" with "HtcpoolX") as "HΦ".
     (* Re-establish the txnlog invariant. *)
@@ -315,7 +314,6 @@ Section program.
     (* Update the txn cpool. *)
     set tcpool' := _ ∪ tcpool.
     iMod (txn_cpool_update tcpool' with "Htcpool HtcpoolX") as "[Htcpool HtcpoolX]".
-    { set_solver. }
     (* Apply the view shift. *)
     iMod ("HAU" with "HtcpoolX") as "HΦ".
     (* Re-establish the txnlog invariant. *)