From 61eea858cb9b2c20748d0534b181fd538ef5cae7 Mon Sep 17 00:00:00 2001 From: Yun-Sheng Chang Date: Wed, 4 Dec 2024 00:26:46 -0500 Subject: [PATCH] Define and prove consensus resources --- src/program_proof/rsm/pure/misc.v | 26 ++++++ src/program_proof/tulip/base.v | 13 ++- src/program_proof/tulip/paxos/base.v | 15 ++-- src/program_proof/tulip/paxos/inv.v | 4 +- src/program_proof/tulip/paxos/res.v | 88 ++++++++++++++----- .../tulip/program/txnlog/txnlog.v | 2 - src/program_proof/tulip/res.v | 77 ++++++++++++---- 7 files changed, 177 insertions(+), 48 deletions(-) diff --git a/src/program_proof/rsm/pure/misc.v b/src/program_proof/rsm/pure/misc.v index b586a46bf..24f1b06c8 100644 --- a/src/program_proof/rsm/pure/misc.v +++ b/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. diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v index 14aa8a12b..f9b779679 100644 --- a/src/program_proof/tulip/base.v +++ b/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; diff --git a/src/program_proof/tulip/paxos/base.v b/src/program_proof/tulip/paxos/base.v index 4e23b099a..eb447a9a0 100644 --- a/src/program_proof/tulip/paxos/base.v +++ b/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; diff --git a/src/program_proof/tulip/paxos/inv.v b/src/program_proof/tulip/paxos/inv.v index ab695df4d..0d2fd857a 100644 --- a/src/program_proof/tulip/paxos/inv.v +++ b/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). diff --git a/src/program_proof/tulip/paxos/res.v b/src/program_proof/tulip/paxos/res.v index 9fde6809b..28990f96d 100644 --- a/src/program_proof/tulip/paxos/res.v +++ b/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. diff --git a/src/program_proof/tulip/program/txnlog/txnlog.v b/src/program_proof/tulip/program/txnlog/txnlog.v index bd073ccd6..f93815f05 100644 --- a/src/program_proof/tulip/program/txnlog/txnlog.v +++ b/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. *) diff --git a/src/program_proof/tulip/res.v b/src/program_proof/tulip/res.v index 740d7940a..4a31f685b 100644 --- a/src/program_proof/tulip/res.v +++ b/src/program_proof/tulip/res.v @@ -433,22 +433,22 @@ Section res. (** Consensus resource with transaction semantics. One half owned by the group invariant, the other half by the txnlog invariant. *) - Definition own_txn_log_half γ (gid : u64) (log : dblog) : iProp Σ. - Admitted. + Definition own_txn_log_half γ (gid : u64) (log : dblog) : iProp Σ := + own γ.(txn_log) {[ gid := mono_list_auth (DfracOwn (1 / 2)) log ]}. - Definition is_txn_log_lb γ (gid : u64) (log : dblog) : iProp Σ. - Admitted. + Definition is_txn_log_lb γ (gid : u64) (log : dblog) : iProp Σ := + own γ.(txn_log) {[ gid := mono_list_lb log ]}. #[global] Instance is_txn_log_lb_persistent γ gid log : Persistent (is_txn_log_lb γ gid log). - Admitted. + Proof. apply _. Defined. Definition is_txn_log_lbs γ (logs : gmap u64 dblog) : iProp Σ := [∗ map] gid ↦ log ∈ logs, is_txn_log_lb γ gid log. - Definition own_txn_cpool_half γ (gid : u64) (cpool : gset ccommand) : iProp Σ. - Admitted. + Definition own_txn_cpool_half γ (gid : u64) (cpool : gset ccommand) : iProp Σ := + own γ.(txn_cpool) {[ gid := to_dfrac_agree (DfracOwn (1 / 2)) cpool ]}. Definition own_txn_consensus_half γ (gid : u64) (log : dblog) (cpool : gset ccommand) : iProp Σ := @@ -457,37 +457,65 @@ Section res. Lemma txn_log_witness γ gid log : own_txn_log_half γ gid log -∗ is_txn_log_lb γ gid log. - Admitted. + Proof. + iApply own_mono. + rewrite singleton_included_total. + apply mono_list_included. + Qed. Lemma txn_log_prefix γ gid log logp : own_txn_log_half γ gid log -∗ is_txn_log_lb γ gid logp -∗ ⌜prefix logp log⌝. - Admitted. + Proof. + iIntros "Hauth Hlb". + iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid. + rewrite singleton_op singleton_valid in Hvalid. + by apply mono_list_both_dfrac_valid_L in Hvalid as [_ ?]. + Qed. Lemma txn_log_agree γ gid log1 log2 : own_txn_log_half γ gid log1 -∗ own_txn_log_half γ gid log2 -∗ ⌜log2 = log1⌝. - Admitted. + Proof. + iIntros "Hauth1 Hauth2". + iDestruct (own_valid_2 with "Hauth1 Hauth2") as %Hvalid. + rewrite singleton_op singleton_valid in Hvalid. + by apply mono_list_auth_dfrac_op_valid_L in Hvalid as [_ ?]. + Qed. Lemma txn_log_lb_prefix γ gid logp1 logp2 : is_txn_log_lb γ gid logp1 -∗ is_txn_log_lb γ gid logp2 -∗ ⌜prefix logp1 logp2 ∨ prefix logp2 logp1⌝. - Admitted. + Proof. + iIntros "Hlb1 Hlb2". + iDestruct (own_valid_2 with "Hlb1 Hlb2") as %Hvalid. + by rewrite singleton_op singleton_valid mono_list_lb_op_valid_L in Hvalid. + Qed. Lemma txn_log_lb_weaken {γ gid} logp1 logp2 : prefix logp1 logp2 -> is_txn_log_lb γ gid logp2 -∗ is_txn_log_lb γ gid logp1. - Admitted. + Proof. + intros Hprefix. + iApply own_mono. + rewrite singleton_included_total. + by apply mono_list_lb_mono. + Qed. Lemma txn_cpool_agree γ gid cpool1 cpool2 : own_txn_cpool_half γ gid cpool1 -∗ own_txn_cpool_half γ gid cpool2 -∗ ⌜cpool2 = cpool1⌝. - Admitted. + Proof. + iIntros "Hauth1 Hauth2". + iDestruct (own_valid_2 with "Hauth1 Hauth2") as %Hvalid. + rewrite singleton_op singleton_valid in Hvalid. + by apply dfrac_agree_op_valid_L in Hvalid as [_ ?]. + Qed. Definition txn_cpool_subsume_log (cpool : gset ccommand) (log : list ccommand) := Forall (λ c, c ∈ cpool) log. @@ -497,15 +525,32 @@ Section res. own_txn_log_half γ gid log ==∗ own_txn_log_half γ gid (log ++ logext) ∗ own_txn_log_half γ gid (log ++ logext). - Admitted. + Proof. + iIntros "Hauth1 Hauth2". + iCombine "Hauth1 Hauth2" as "Hauth". + rewrite -own_op singleton_op. + iApply (own_update with "Hauth"). + apply singleton_update. + rewrite -mono_list_auth_dfrac_op dfrac_op_own Qp.half_half. + apply mono_list_update. + by apply prefix_app_r. + Qed. + (* TODO: the ⊆ is not required *) Lemma txn_cpool_update {γ gid cpool} cpool' : - cpool ⊆ cpool' -> own_txn_cpool_half γ gid cpool -∗ own_txn_cpool_half γ gid cpool ==∗ own_txn_cpool_half γ gid cpool' ∗ own_txn_cpool_half γ gid cpool'. - Admitted. + Proof. + iIntros "Hauth1 Hauth2". + iCombine "Hauth1 Hauth2" as "Hauth". + rewrite -own_op singleton_op. + iApply (own_update with "Hauth"). + apply singleton_update. + apply dfrac_agree_update_2. + by rewrite dfrac_op_own Qp.half_half. + Qed. End txn_consensus.