Prove third phase of paxos

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

@@ -7,10 +7,6 @@ From Goose Require github_com.mit_pdos.tulip.util.
 
 From Perennial.goose_lang Require Import ffi.grove_prelude.
 
-(* Key invariants:
-   1. @terml <= @termc
-   2. @lsnc <= @len(ents)
-   3. isleader = true -> @termc = @terml *)
 Definition Paxos := struct.decl [
   "peers" :: slice.T uint64T;
   "addrpeers" :: mapT uint64T;
@@ -184,8 +180,13 @@ Definition Paxos__commit: val :=
     (if: "lsn" ≤ (struct.loadF Paxos "lsnc" "px")
     then #()
     else
-      struct.storeF Paxos "lsnc" "px" "lsn";;
-      #()).
+      (if: (slice.len (struct.loadF Paxos "log" "px")) < "lsn"
+      then
+        struct.storeF Paxos "lsnc" "px" (slice.len (struct.loadF Paxos "log" "px"));;
+        #()
+      else
+        struct.storeF Paxos "lsnc" "px" "lsn";;
+        #())).
 
 (* @learn monotonically increase the commit LSN @px.lsnc in term @term to @lsn. *)
 Definition Paxos__learn: val :=
@@ -207,13 +208,15 @@ Definition Paxos__forward: val :=
 
 Definition Paxos__push: val :=
   rec: "Paxos__push" "px" :=
-    let: "lsns" := ref_to (slice.T uint64T) (NewSliceWithCap uint64T #0 ((slice.len (struct.loadF Paxos "peers" "px")) + #1)) in
-    ForSlice uint64T <> "nid" (struct.loadF Paxos "peers" "px")
-      (let: "lsn" := Fst (MapGet (struct.loadF Paxos "lsnpeers" "px") "nid") in
-      "lsns" <-[slice.T uint64T] (SliceAppend uint64T (![slice.T uint64T] "lsns") "lsn"));;
-    let: "lsnc" := quorum.Median (![slice.T uint64T] "lsns") in
-    Paxos__commit "px" "lsnc";;
-    #().
+    (if: (~ (Paxos__cquorum "px" ((MapLen (struct.loadF Paxos "lsnpeers" "px")) + #1)))
+    then (#0, #false)
+    else
+      let: "lsns" := ref_to (slice.T uint64T) (NewSliceWithCap uint64T #0 (struct.loadF Paxos "sc" "px")) in
+      MapIter (struct.loadF Paxos "lsnpeers" "px") (λ: <> "lsn",
+        "lsns" <-[slice.T uint64T] (SliceAppend uint64T (![slice.T uint64T] "lsns") "lsn"));;
+      util.Sort (![slice.T uint64T] "lsns");;
+      let: "lsn" := SliceGet uint64T (![slice.T uint64T] "lsns") ((slice.len (![slice.T uint64T] "lsns")) - ((struct.loadF Paxos "sc" "px") `quot` #2)) in
+      ("lsn", #true)).
 
 Definition Paxos__gttermc: val :=
   rec: "Paxos__gttermc" "px" "term" :=
@@ -261,7 +264,7 @@ Definition Paxos__GetConnection: val :=
 
 Definition Paxos__Connect: val :=
   rec: "Paxos__Connect" "px" "nid" :=
-    let: "addr" := SliceGet uint64T (struct.loadF Paxos "peers" "px") "nid" in
+    let: "addr" := Fst (MapGet (struct.loadF Paxos "addrpeers" "px") "nid") in
     let: "ret" := grove_ffi.Connect "addr" in
     (if: (~ (struct.get grove_ffi.ConnectRet "Err" "ret"))
     then

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

@@ -16,35 +16,4 @@ Definition Half: val :=
   rec: "Half" "n" :=
     ("n" + #1) `quot` #2.
 
-Definition swap: val :=
-  rec: "swap" "ns" "i" "j" :=
-    let: "tmp" := SliceGet uint64T "ns" "i" in
-    SliceSet uint64T "ns" "i" (SliceGet uint64T "ns" "j");;
-    SliceSet uint64T "ns" "j" "tmp";;
-    #().
-
-Definition sort: val :=
-  rec: "sort" "ns" :=
-    let: "i" := ref_to uint64T #1 in
-    Skip;;
-    (for: (λ: <>, (![uint64T] "i") < (slice.len "ns")); (λ: <>, Skip) := λ: <>,
-      let: "j" := ref_to uint64T (![uint64T] "i") in
-      Skip;;
-      (for: (λ: <>, (![uint64T] "j") > #0); (λ: <>, Skip) := λ: <>,
-        (if: (SliceGet uint64T "ns" ((![uint64T] "j") - #1)) ≤ (SliceGet uint64T "ns" (![uint64T] "j"))
-        then Break
-        else
-          swap "ns" ((![uint64T] "j") - #1) (![uint64T] "j");;
-          "j" <-[uint64T] ((![uint64T] "j") - #1);;
-          Continue));;
-      "i" <-[uint64T] ((![uint64T] "i") + #1);;
-      Continue);;
-    #().
-
-(* NB: Follow the proof of wrbuf.sortEntsByKey *)
-Definition Median: val :=
-  rec: "Median" "ns" :=
-    sort "ns";;
-    SliceGet uint64T "ns" ((slice.len "ns") `quot` #2).
-
 End code.

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

@@ -14,4 +14,29 @@ Definition NextAligned: val :=
     else "delta" <-[uint64T] (("interval" + "low") - "rem"));;
     std.SumAssumeNoOverflow "current" (![uint64T] "delta").
 
+Definition swap: val :=
+  rec: "swap" "ns" "i" "j" :=
+    let: "tmp" := SliceGet uint64T "ns" "i" in
+    SliceSet uint64T "ns" "i" (SliceGet uint64T "ns" "j");;
+    SliceSet uint64T "ns" "j" "tmp";;
+    #().
+
+Definition Sort: val :=
+  rec: "Sort" "ns" :=
+    let: "i" := ref_to uint64T #1 in
+    Skip;;
+    (for: (λ: <>, (![uint64T] "i") < (slice.len "ns")); (λ: <>, Skip) := λ: <>,
+      let: "j" := ref_to uint64T (![uint64T] "i") in
+      Skip;;
+      (for: (λ: <>, (![uint64T] "j") > #0); (λ: <>, Skip) := λ: <>,
+        (if: (SliceGet uint64T "ns" ((![uint64T] "j") - #1)) ≤ (SliceGet uint64T "ns" (![uint64T] "j"))
+        then Break
+        else
+          swap "ns" ((![uint64T] "j") - #1) (![uint64T] "j");;
+          "j" <-[uint64T] ((![uint64T] "j") - #1);;
+          Continue));;
+      "i" <-[uint64T] ((![uint64T] "i") + #1);;
+      Continue);;
+    #().
+
 End code.

src/program_proof/rsm/pure/list.v

@@ -99,6 +99,15 @@ Section lemma.
     by apply NoDup_app in Hl2 as [? _].
   Qed.
 
+  Lemma NoDup_suffix l1 l2 :
+    suffix l1 l2 ->
+    NoDup l2 ->
+    NoDup l1.
+  Proof.
+    intros [l Happ] Hl2. rewrite Happ in Hl2.
+    by apply NoDup_app in Hl2 as (_ & _ & ?).
+  Qed.
+
   Lemma not_elem_of_take l n x :
     NoDup l ->
     l !! n = Some x ->

src/program_proof/tulip/paxos/inv.v

@@ -1,7 +1,7 @@
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.program_proof.rsm Require Import big_sep.
 From Perennial.program_proof.rsm.pure Require Import quorum list extend.
-From Perennial.program_proof.tulip.paxos Require Import base res.
+From Perennial.program_proof.tulip.paxos Require Import base consistency res.
 
 Section inv.
   Context `{!heapGS Σ, !paxos_ghostG Σ}.
@@ -102,18 +102,47 @@ Section inv.
       "%Hquorum" ∷ ⌜cquorum nids nidsq⌝ ∗
       "%Hmember" ∷ ⌜nid ∈ nids⌝.
 
+  Lemma safe_ledger_in_weaken {γ nids t v} vlb :
+    prefix vlb v ->
+    safe_ledger_in γ nids t v -∗
+    safe_ledger_in γ nids t vlb.
+  Proof.
+    iIntros (Hprefix) "Hv".
+    iNamed "Hv".
+    iDestruct (accepted_proposal_lb_weaken vlb with "Hvacpt") as "Hvacpt'".
+    { apply Hprefix. }
+    set Ψ := λ nid, is_accepted_proposal_length_lb γ nid t (length vlb).
+    iDestruct (big_sepS_impl _ Ψ with "Hacpt []") as "Hacpt'".
+    { iIntros (nidx Hnidx) "!> Hlenlb".
+      iApply (accepted_proposal_length_lb_weaken (length vlb) with "Hlenlb").
+      by apply prefix_length.
+    }
+    iFrame "# %".
+  Qed.
+
   Definition safe_ledger γ nids v : iProp Σ :=
     ∃ t, safe_ledger_in γ nids t v.
 
   Definition safe_ledger_above γ nids t v : iProp Σ :=
     ∃ t', safe_ledger_in γ nids t' v ∗ ⌜(t' ≤ t)%nat⌝.
 
-  Lemma safe_ledger_above_mono {γ nids} t v t' :
+  Lemma safe_ledger_above_mono {γ nids} t t' v :
     (t ≤ t')%nat ->
     safe_ledger_above γ nids t v -∗
     safe_ledger_above γ nids t' v.
   Proof. iIntros (Hle) "(%p & Hsafe & %Hp)". iExists p. iFrame. iPureIntro. lia. Qed.
 
+  Lemma safe_ledger_above_weaken {γ nids t v} vlb :
+    prefix vlb v ->
+    safe_ledger_above γ nids t v -∗
+    safe_ledger_above γ nids t vlb.
+  Proof.
+    iIntros (Hprefix) "(%p & Hv & %Hplet)".
+    iDestruct (safe_ledger_in_weaken with "Hv") as "Hvlb".
+    { apply Hprefix. }
+    by iFrame "Hvlb".
+  Qed.
+
   Definition equal_latest_longest_proposal_nodedec (dssq : gmap u64 (list nodedec)) t v :=
     equal_latest_longest_proposal_with (mbind nodedec_to_ledger) dssq t v.
 
@@ -491,7 +520,7 @@ Section lemma.
     split; [done | lia].
   Qed.
 
-  Lemma node_inv_is_accepted_proposal_lb_impl_prefix γ bs nid1 nid2 t v1 v2 :
+  Lemma nodes_inv_is_accepted_proposal_lb_impl_prefix γ bs nid1 nid2 t v1 v2 :
     nid1 ∈ dom bs ->
     nid2 ∈ dom bs ->
     is_accepted_proposal_lb γ nid1 t v1 -∗
@@ -662,7 +691,7 @@ Section lemma.
     iNamed "Hinv".
     iIntros (t v Hv).
     iDestruct (big_sepM_lookup with "Hpsaubs") as (vlb) "[Hvub %Hprefix]"; first apply Hv.
-    iDestruct (proposal_prefix with "Hvub Hps") as %(vub & Hvub & Hprefixvlb).
+    iDestruct (proposals_prefix with "Hvub Hps") as %(vub & Hvub & Hprefixvlb).
     iPureIntro.
     exists vub.
     split; first apply Hvub.
@@ -763,6 +792,15 @@ Section lemma.
     by iFrame.
   Qed.
 
+  Lemma paxos_inv_impl_nodes_inv_psa γ nids :
+    paxos_inv γ nids -∗
+    ∃ bs, ([∗ map] nid ↦ psa ∈ bs, node_inv_psa γ nid psa) ∗ ⌜dom bs = nids⌝.
+  Proof.
+    iNamed 1.
+    rewrite -Hdomtermlm.
+    iApply (nodes_inv_impl_nodes_inv_psa with "Hnodes").
+  Qed.
+
   Lemma nodes_inv_safe_ledger_in_impl_chosen_in γ nids bs t v :
     dom bs = nids ->
     safe_ledger_in γ nids t v -∗
@@ -792,7 +830,7 @@ Section lemma.
     iDestruct (big_sepS_elem_of _ _ nid' with "Hacpt") as "Hvacpt'".
     { by apply map_lookup_filter_Some_1_2 in Hps. }
     iDestruct "Hvacpt'" as (v') "[Hvacpt' %Hlen]".
-    iDestruct (node_inv_is_accepted_proposal_lb_impl_prefix with "Hvacpt Hvacpt' Hinv") as %Hprefix.
+    iDestruct (nodes_inv_is_accepted_proposal_lb_impl_prefix with "Hvacpt Hvacpt' Hinv") as %Hprefix.
     { by rewrite -Hdombs in Hmember. }
     { apply elem_of_dom_2 in Hps.
       apply (elem_of_weaken _ (dom bsq)); first done.
@@ -852,5 +890,15 @@ Section lemma.
     iApply (prefix_growing_ledger_impl_prefix with "Hvub1 Hvub2").
   Qed.
 
+  Lemma nodes_inv_safe_ledger_impl_chosen γ nids bs v :
+    dom bs = nids ->
+    safe_ledger γ nids v -∗
+    ([∗ map] nid ↦ psa ∈ bs, node_inv_psa γ nid psa) -∗
+    ⌜chosen bs v⌝.
+  Proof.
+    iIntros (Hdombs) "[%t #Hsafe] Hinv".
+    iExists t.
+    by iApply (nodes_inv_safe_ledger_in_impl_chosen_in with "Hsafe Hinv").
+  Qed.
 
 End lemma.