Prove top-level paxos spec

Remove internal log

Add constraints on the external state (i.e., log and cpool)

Adapt invariance w.r.t. ascend, commit, and extend to added constraints

external/Goose/github_com/mit_pdos/tulip/paxos.v

@@ -30,10 +30,14 @@ Definition Paxos := struct.decl [
 
 Definition MAX_NODES : expr := #16.
 
+Definition Paxos__leading: val :=
+  rec: "Paxos__leading" "px" :=
+    struct.loadF Paxos "isleader" "px".
+
 Definition Paxos__Submit: val :=
   rec: "Paxos__Submit" "px" "v" :=
     Mutex__Lock (struct.loadF Paxos "mu" "px");;
-    (if: (~ (struct.loadF Paxos "isleader" "px"))
+    (if: (~ (Paxos__leading "px"))
     then
       Mutex__Unlock (struct.loadF Paxos "mu" "px");;
       (#0, #0)
@@ -244,10 +248,6 @@ Definition Paxos__nominated: val :=
   rec: "Paxos__nominated" "px" :=
     struct.loadF Paxos "iscand" "px".
 
-Definition Paxos__leading: val :=
-  rec: "Paxos__leading" "px" :=
-    struct.loadF Paxos "isleader" "px".
-
 Definition Paxos__heartbeat: val :=
   rec: "Paxos__heartbeat" "px" :=
     struct.storeF Paxos "hb" "px" #true;;

src/program_proof/rsm/mpaxos_proof.v

@@ -139,7 +139,7 @@ Section prog.
   Theorem wp_MkPaxos :
     {{{ True }}}
       MkPaxos #()
-      {{{ (γ : mpaxos_names) (px : loc), RET #px; paxos_init px γ }}}.
+    {{{ (γ : mpaxos_names) (px : loc), RET #px; paxos_init px γ }}}.
   Proof.
     (*@ func MkPaxos() *Paxos {                                                 @*)
     (*@     var px *Paxos                                                       @*)

src/program_proof/tulip/paxos/base.v

@@ -134,7 +134,6 @@ Section def.
     lia.
   Qed.
 
-
   Lemma latest_before_quorum_step_O_or_exists (ts : gmap A nat) :
     map_fold latest_term_before_quorum_step O ts = O ∨
     ∃ x, ts !! x = Some (map_fold latest_term_before_quorum_step O ts).

src/program_proof/tulip/paxos/inv.v

@@ -468,20 +468,22 @@ Section inv.
       "%Hlatest" ∷ ⌜latest_term_nodedec ds = terml⌝ ∗
       "%Hacpt"   ∷ ⌜ds !! terml = Some (Accept v)⌝.
 
+  Definition proposed_cmds γ v : iProp Σ := [∗ list] c ∈ v, is_cmd_receipt γ c.
+
   Definition paxos_inv γ nids : iProp Σ :=
-    ∃ log cpool logi ps psb termlm,
+    ∃ log cpool ps psb termlm,
       (* external states *)
       "Hlog"   ∷ own_log_half γ log ∗
       "Hcpool" ∷ own_cpool_half γ cpool ∗
       (* internal states *)
-      "Hlogi" ∷ own_internal_log γ logi ∗
       "Hps"   ∷ own_proposals γ ps ∗
       "Hpsb"  ∷ own_base_proposals γ psb ∗
       (* node states *)
       "Hnodes" ∷ ([∗ map] nid ↦ terml ∈ termlm, node_inv γ nid terml) ∗
-      (* TODO: constraints between internal and external states *)
+      (* constraints between internal and external states *)
+      "#Hsafelog"   ∷ safe_ledger γ nids log ∗
+      "#Hsubsume"   ∷ ([∗ map] t ↦ v ∈ ps, proposed_cmds γ v) ∗
       (* constraints on internal states *)
-      "#Hsafelogi"  ∷ safe_ledger γ nids logi ∗
       "#Hsafepsb"   ∷ ([∗ map] t ↦ v ∈ psb, safe_base_proposal γ nids t v) ∗
       "%Hvp"        ∷ ⌜valid_proposals ps psb⌝ ∗
       "%Hdomtermlm" ∷ ⌜dom termlm = nids⌝ ∗

src/program_proof/tulip/paxos/invariance/ascend.v

@@ -43,43 +43,43 @@ Section ascend.
     by iDestruct (big_sepM_lookup with "Hpsaubs") as "?"; first apply Hfixed.
   Qed.
 
-  Lemma paxos_inv_ascend γ nids nid termc terml logn logn' :
+  Lemma paxos_inv_ascend γ nids nid termc terml v v' :
     nid ∈ nids ->
     is_term_of_node nid termc ->
     (terml < termc)%nat ->
-    safe_base_proposal_by_length γ nids termc logn' -∗
+    safe_base_proposal_by_length γ nids termc v' -∗
     own_current_term_half γ nid termc -∗
     own_ledger_term_half γ nid terml -∗
-    own_node_ledger_half γ nid logn -∗
+    own_node_ledger_half γ nid v -∗
     paxos_inv γ nids ==∗
     own_current_term_half γ nid termc ∗
     own_ledger_term_half γ nid termc ∗
-    own_node_ledger_half γ nid logn' ∗
+    own_node_ledger_half γ nid v' ∗
     paxos_inv γ nids ∗
-    own_proposal γ termc logn' ∗
-    is_base_proposal_receipt γ termc logn' ∗
-    is_accepted_proposal_lb γ nid termc logn'.
+    own_proposal γ termc v' ∗
+    is_base_proposal_receipt γ termc v' ∗
+    is_accepted_proposal_lb γ nid termc v'.
   Proof.
-    iIntros (Hnid Hton Hlt) "#Hsafelen Htermc Hterml Hlogn Hinv".
+    iIntros (Hnid Hton Hlt) "#Hsafelen Htermc Hterml Hv Hinv".
     iNamed "Hinv".
-    iAssert (safe_base_proposal γ nids termc logn')%nat as "#Hsafe".
+    iAssert (safe_base_proposal γ nids termc v')%nat as "#Hsafe".
     { iNamed "Hsafelen". iNamed "Hvotes".
       rewrite Hdomdss in Hquorum.
       iFrame "Hdss %".
       (* Obtain two nodes [nidx], the node known to have the longest ledger, and
       [nidy], the node to be proved to have the longest ledger. *)
-      destruct Hvlatest as (nidx & dsx & Hdsx & Hlognx).
+      destruct Hvlatest as (nidx & dsx & Hdsx & Hvx).
       pose proof (longest_proposal_in_term_with_spec (mbind nodedec_to_ledger) dss p) as Hspec.
-      destruct (longest_proposal_in_term_with _ _ _) as [logny |] eqn:Hlongest; last first.
+      destruct (longest_proposal_in_term_with _ _ _) as [vy |] eqn:Hlongest; last first.
       { exfalso.
         specialize (Hspec _ _ Hdsx).
-        by rewrite Hlognx in Hspec.
+        by rewrite Hvx in Hspec.
       }
-      destruct Hspec as [(nidy & dsy & Hdsy & Hlogny) Hge].
-      rewrite bind_Some in Hlogny.
-      destruct Hlogny as (d & Hlogny & Hd).
+      destruct Hspec as [(nidy & dsy & Hdsy & Hvy) Hge].
+      rewrite bind_Some in Hvy.
+      destruct Hvy as (d & Hvy & Hd).
       apply nodedec_to_ledger_Some_inv in Hd. subst d.
-      iAssert (prefix_growing_ledger γ p logn')%I as "#Hpfgx".
+      iAssert (prefix_growing_ledger γ p v')%I as "#Hpfgx".
       { iDestruct (big_sepM_lookup with "Hdss") as "#Hdsx"; first apply Hdsx.
         assert (is_Some (termlm !! nidx)) as [terml' Hterml'].
         { rewrite -elem_of_dom Hdomtermlm.
@@ -90,9 +90,9 @@ Section ascend.
         iDestruct (big_sepM_lookup with "Hnodes") as "Hnode"; first apply Hterml'.
         iDestruct (node_inv_extract_ds_psa with "Hnode") as (dss' bs') "[_ Hnode]".
         iApply (node_inv_past_nodedecs_impl_prefix_growing_ledger with "Hdsx Hnode").
-        apply Hlognx.
+        apply Hvx.
       }
-      iAssert (prefix_growing_ledger γ p logny)%I as "#Hpfgy".
+      iAssert (prefix_growing_ledger γ p vy)%I as "#Hpfgy".
       { iDestruct (big_sepM_lookup with "Hdss") as "#Hdsy"; first apply Hdsy.
         assert (is_Some (termlm !! nidy)) as [termly Htermly].
         { rewrite -elem_of_dom Hdomtermlm.
@@ -103,24 +103,46 @@ Section ascend.
         iDestruct (big_sepM_lookup with "Hnodes") as "Hnode"; first apply Htermly.
         iDestruct (node_inv_extract_ds_psa with "Hnode") as (dssy bsy) "[_ Hnode]".
         iApply (node_inv_past_nodedecs_impl_prefix_growing_ledger with "Hdsy Hnode").
-        apply Hlogny.
+        apply Hvy.
       }
       iDestruct (prefix_growing_ledger_impl_prefix with "Hpfgx Hpfgy") as %Hprefix.
       iPureIntro.
       rewrite /equal_latest_longest_proposal_nodedec /equal_latest_longest_proposal_with.
       case_decide as Htermc; first lia.
       rewrite -latest_term_before_quorum_nodedec_unfold Hlatestq.
-      pose proof (length_of_longest_ledger_in_term_spec _ _ _ _ _ Hdsy Hlogny) as Hle.
+      pose proof (length_of_longest_ledger_in_term_spec _ _ _ _ _ Hdsy Hvy) as Hle.
       rewrite Hlongestq in Hle.
       specialize (Hge _ _ Hdsx).
-      rewrite Hlognx /= in Hge.
-      assert (Heqlen : length logny = length logn') by lia.
-      replace logn' with logny; first done.
+      rewrite Hvx /= in Hge.
+      assert (Heqlen : length vy = length v') by lia.
+      replace v' with vy; first done.
       by destruct Hprefix as [Hprefix | Hprefix]; rewrite (prefix_length_eq _ _ Hprefix).
     }
     pose proof Hnid as Hterml.
     rewrite -Hdomtermlm elem_of_dom in Hterml.
     destruct Hterml as [terml' Hterml].
+    (* Obtain [proposed_cmds γ v']. *)
+    iAssert (proposed_cmds γ v')%I as "#Hsubsume'".
+    { iNamed "Hsafelen". iNamed "Hvotes".
+      destruct Hvlatest as (nidx & dslb & Hdslb & Hv').
+      iDestruct (big_sepM_lookup with "Hdss") as "Hdslb"; first apply Hdslb.
+      assert (is_Some (termlm !! nidx)) as [termlx Htermlx].
+      { destruct Hquorum as [Hquorum _].
+        apply elem_of_dom_2 in Hdslb.
+        rewrite -elem_of_dom Hdomtermlm.
+        set_solver.
+      }
+      iDestruct (big_sepM_lookup with "Hnodes") as "Hnode"; first apply Htermlx.
+      iDestruct (node_inv_extract_ds_psa with "Hnode") as (ds psa) "[_ Hdp]".
+      iDestruct (node_inv_past_nodedecs_impl_prefix_growing_ledger with "Hdslb Hdp") as "#Hpfg".
+      { apply Hv'. }
+      iDestruct "Hpfg" as (vub1) "[Hlb %Hprefix1]".
+      iDestruct (proposals_prefix with "Hlb Hps") as %(vub2 & Hvub2 & Hprefix2).
+      iDestruct (big_sepM_lookup with "Hsubsume") as "Hsubsume'"; first apply Hvub2.
+      assert (prefix v' vub2) as [vapp ->]; first by trans vub1.
+      rewrite /proposed_cmds.
+      by iDestruct (big_sepL_app with "Hsubsume'") as "[? _]".
+    }
     iDestruct (big_sepM_delete _ _ nid with "Hnodes") as "[Hnode Hnodes]".
     { apply Hterml. }
     iDestruct (own_ledger_term_node_inv_terml_eq with "Hterml Hnode") as %->.
@@ -130,23 +152,24 @@ Section ascend.
       destruct Hdompsb as [_ Hfree].
       by specialize (Hfree _ _ Hterml _ Hton Hlt).
     }
-    (* Insert [(termc, logn')] into the growing proposals and the base proposals. *)
-    iMod (proposal_insert termc logn' with "Hps") as "[Hps Hp]".
+    (* Insert [(termc, v')] into the growing proposals and the base proposals. *)
+    iMod (proposal_insert termc v' with "Hps") as "[Hps Hp]".
     { apply map_Forall2_dom_L in Hvp as Hdomps. by rewrite Hdomps not_elem_of_dom in Hnotin. }
-    iMod (base_proposal_insert termc logn' with "Hpsb") as "[Hpsb #Hpsbrcp]".
+    iMod (base_proposal_insert termc v' with "Hpsb") as "[Hpsb #Hpsbrcp]".
     { by rewrite not_elem_of_dom in Hnotin. }
     (* Extract witness of the inserted proposal to re-establish the node invariant. *)
     iDestruct (proposal_witness with "Hp") as "#Hplb".
     (* Re-establish node invariant. *)
-    iMod (node_inv_advance logn' with "[] [] Htermc Hterml Hlogn Hnode")
-      as "(Htermc & Hterml & Hlogn & Hnode & #Hacptlb)".
+    iMod (node_inv_advance v' with "[] [] Htermc Hterml Hv Hnode")
+      as "(Htermc & Hterml & Hv & Hnode & #Hacptlb)".
     { apply Hlt. }
     { by iFrame "Hpsbrcp". }
     { by iFrame "Hplb". }
     iDestruct (big_sepM_insert_2 with "Hnode Hnodes") as "Hnodes".
     rewrite insert_delete_insert.
     iFrame "∗ # %".
     iModIntro.
+    iSplit; first by iApply big_sepM_insert_2.
     iSplit.
     { (* Re-establish [safe_base_proposal]. *)
       iApply (big_sepM_insert_2 with "Hsafe Hsafepsb").

src/program_proof/tulip/paxos/invariance/commit.v

@@ -14,14 +14,16 @@ Section commit.
     by iApply (nodes_inv_safe_ledger_in_impl_chosen_in with "Hsafe Hinv").
   Qed.
 
-  Lemma paxos_inv_commit γ nids logi' :
-    safe_ledger γ nids logi' -∗
-    paxos_inv γ nids ==∗
-    paxos_inv γ nids ∗
-    is_internal_log_lb γ logi'.
+  Lemma safe_ledger_log_impl_prefix γ nids v v' :
+    safe_ledger γ nids v' -∗
+    own_log_half γ v -∗
+    paxos_inv γ nids -∗
+    ⌜prefix v v' ∨ prefix v' v⌝.
   Proof.
-    iIntros "#Hsafe Hinv".
+    iIntros "#Hsafe Hloguser Hinv".
     iNamed "Hinv".
+    (* Agreement on the log content. *)
+    iDestruct (log_agree with "Hloguser Hlog") as %->.
     (* Extract past decisions and accepted proposals from the node invariant. *)
     iDestruct (nodes_inv_extract_ds_psa with "Hnodes") as (dss bs) "[Hnodes Hpds]".
     iDestruct (big_sepM2_dom with "Hpds") as %Hdompds.
@@ -40,24 +42,59 @@ Section commit.
     (* Finally, derive [consistency bs]. *)
     pose proof (vlb_vub_vbp_vp_impl_consistency _ _ _ Hvlb Hvub Hvbp Hvp) as Hcst.
     (* Now, derive [chosen bs logi] and [chosen bs logi']. *)
-    iDestruct (nodes_inv_safe_ledger_impl_chosen _ _ bs with "Hsafelogi [Hpds]") as %Hchosen.
+    iDestruct (nodes_inv_safe_ledger_impl_chosen _ _ bs with "Hsafelog [Hpds]") as %Hchosen.
     { apply Hdombs. }
     { by iApply nodes_inv_ds_psa_impl_nodes_inv_psa. }
     iDestruct (nodes_inv_safe_ledger_impl_chosen _ _ bs with "Hsafe [Hpds]") as %Hchosen'.
     { apply Hdombs. }
     { by iApply nodes_inv_ds_psa_impl_nodes_inv_psa. }
     (* Derive [prefix logi logi' ∨ prefix logi' logi]. *)
-    specialize (Hcst _ _ Hchosen Hchosen').
-    (* Merge [node_inv_ds_psa] back. *)
-    iDestruct (nodes_inv_merge_ds_psa with "Hnodes Hpds") as "Hnodes".
-    destruct Hcst as [Hge | Hle]; last first.
-    { (* Case: The old log is at least as long as the new log. Simply extract a witness. *)
-      iDestruct (internal_log_witness logi' with "Hlogi") as "#Hlb"; first apply Hle.
-      by iFrame "∗ # %".
+    by specialize (Hcst _ _ Hchosen Hchosen').
+  Qed.
+
+  Lemma paxos_inv_commit {γ nids nid vcli vnode} vsafe :
+    nid ∈ nids ->
+    prefix vsafe vnode ->
+    safe_ledger γ nids vsafe -∗
+    own_log_half γ vcli -∗
+    own_node_ledger_half γ nid vnode -∗
+    paxos_inv γ nids ==∗
+    (∃ vcli', own_log_half γ vcli' ∧ ⌜prefix vsafe vcli'⌝) ∗
+    own_node_ledger_half γ nid vnode ∗
+    paxos_inv γ nids.
+  Proof.
+    iIntros (Hnid Hprefix) "#Hsafe Hlogcli HlognX Hinv".
+    iDestruct (safe_ledger_log_impl_prefix with "Hsafe Hlogcli Hinv") as %Horprefix.
+    destruct Horprefix as [Hext | Hnoext]; last first.
+    { (* Case: The global log is longer than the committed log on [nid]. No update required. *)
+      by iFrame.
+    }
+    (* Case: The global log is shorted. Extend it to [vsafe]. *)
+    iNamed "Hinv".
+    iDestruct (log_agree with "Hlogcli Hlog") as %->.
+    iAssert (⌜cpool_subsume_log vsafe cpool⌝)%I as %Hsubsume.
+    { rewrite -Hdomtermlm elem_of_dom in Hnid.
+      destruct Hnid as [terml Hterml].
+      iDestruct (big_sepM_lookup with "Hnodes") as "Hnode"; first apply Hterml.
+      iNamed "Hnode".
+      iDestruct (node_ledger_agree with "HlognX Hlogn") as %->.
+      iDestruct (accepted_proposal_lookup with "Hacpt Hpsa") as %Hvnode.
+      iDestruct (big_sepM_lookup with "Hpsaubs") as (vub1) "[#Hvub1 %Hprefix1]"; first apply Hvnode.
+      iDestruct (proposals_prefix with "Hvub1 Hps") as (vub2) "[%Hvub2 %Hprefix2]".
+      assert (Hvsafe : prefix vsafe vub2).
+      { trans vnode; first apply Hprefix.
+        trans vub1; [apply Hprefix1 | apply Hprefix2].
+      }
+      iDestruct (big_sepM_lookup with "Hsubsume") as "Hpcmds"; first apply Hvub2.
+      rewrite /cpool_subsume_log Forall_forall.
+      iIntros (c Hc).
+      pose proof (elem_of_prefix _ _ _ Hc Hvsafe) as Hc'.
+      iDestruct (big_sepL_elem_of with "Hpcmds") as "Hc"; first apply Hc'.
+      iApply (cpool_lookup with "Hc Hcpool").
     }
-    (* Case: The new log is at least as long as the old log. Update the log. *)
-    iMod (internal_log_update with "Hlogi") as "Hlogi"; first apply Hge.
-    iDestruct (internal_log_witness logi' with "Hlogi") as "#Hlb"; first done.
+    iMod (log_update with "Hlogcli Hlog Hcpool") as "(Hlogcli & Hlog & Hcpool)".
+    { apply Hsubsume. }
+    { apply Hext. }
     by iFrame "∗ # %".
   Qed.