Prove paxos RA except consensus

src/program_proof/tulip/paxos/base.v

@@ -1,3 +1,6 @@
+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 quorum.
 
@@ -366,9 +369,83 @@ Proof.
   lia.
 Qed.
 
-Class paxos_ghostG (Σ : gFunctors).
+Inductive pxst :=
+| PaxosState (termc terml lsnc : nat) (ledger : ledger)
+| PaxosStuck.
+
+Inductive pxcmd :=
+| CmdPaxosExtend (ents : ledger)
+| CmdPaxosPrepare (term : nat)
+| CmdPaxosAdvance (term lsn : nat) (ents : ledger)
+| CmdPaxosAccept (lsn : nat) (ents : ledger)
+| CmdPaxosExpand (lsn : nat).
+
+Definition stringO := leibnizO string.
+Definition stringmlR := mono_listR stringO.
+Definition lsnmR := gmapR nat (dfrac_agreeR natO).
+Canonical Structure nodedecO := leibnizO nodedec.
+Definition declistR := mono_listR nodedecO.
+Definition node_declistR := gmapR u64 declistR.
+Definition ledgerO := leibnizO ledger.
+Definition proposalmR := gmap_viewR nat (agreeR gnameO).
+Definition node_proposalmR := gmapR u64 proposalmR.
+Definition node_natmR := gmapR u64 (dfrac_agreeR natO).
+Definition node_ledgerR := gmapR u64 (dfrac_agreeR ledgerO).
+Definition pxcmdlO := leibnizO (list pxcmd).
+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] base_proposalG :: ghost_mapG Σ nat ledger;
+    #[global] prepare_lsnG :: inG Σ lsnmR;
+    #[global] node_declistG :: inG Σ node_declistR;
+    #[global] node_proposalG :: inG Σ node_proposalmR;
+    #[global] current_termG :: inG Σ node_natmR;
+    #[global] ledger_termG :: inG Σ node_natmR;
+    #[global] committed_lsnG :: inG Σ node_natmR;
+    #[global] node_ledgerG :: inG Σ node_ledgerR;
+    #[global] node_walG :: inG Σ node_pxcmdlR;
+    #[global] node_wal_fnameG :: inG Σ node_stringR;
+    #[global] trmlmG :: ghost_mapG Σ chan unit;
+  }.
+
+Definition paxos_ghostΣ :=
+  #[ ghost_mapΣ nat gname;
+     GFunctor stringmlR;
+     ghost_mapΣ nat ledger;
+     GFunctor lsnmR;
+     GFunctor node_declistR;
+     GFunctor node_proposalmR;
+     GFunctor node_natmR;
+     GFunctor node_natmR;
+     GFunctor node_natmR;
+     GFunctor node_ledgerR;
+     GFunctor node_pxcmdlR;
+     GFunctor node_stringR;
+     ghost_mapΣ chan unit
+    ].
+
+#[global]
+Instance subG_paxos_ghostG {Σ} :
+  subG paxos_ghostΣ Σ → paxos_ghostG Σ.
+Proof. solve_inG. Qed.
 
 Instance stagedG_paxos_ghostG Σ : paxos_ghostG Σ → stagedG Σ.
 Proof. Admitted.
 
-Record paxos_names := {}.
+Record paxos_names := {
+    proposal : gname;
+    base_proposal : gname;
+    prepare_lsn : gname;
+    node_declist : gname;
+    node_proposal : gname;
+    current_term : gname;
+    ledger_term : gname;
+    committed_lsn : gname;
+    node_ledger : gname;
+    node_wal : gname;
+    node_wal_fname : gname;
+    trmlm : gname;
+  }.

src/program_proof/tulip/paxos/recovery.v

@@ -1,17 +1,6 @@
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.program_proof.tulip.paxos Require Import base.
 
-Inductive pxst :=
-| PaxosState (termc terml lsnc : nat) (ledger : ledger)
-| PaxosStuck.
-
-Inductive pxcmd :=
-| CmdPaxosExtend (ents : ledger)
-| CmdPaxosPrepare (term : nat)
-| CmdPaxosAdvance (term lsn : nat) (ents : ledger)
-| CmdPaxosAccept (lsn : nat) (ents : ledger)
-| CmdPaxosExpand (lsn : nat).
-
 Definition execute_paxos_extend st ents :=
   match st with
   | PaxosState termc terml lsnc ledger =>