From 828ab2e67d200574c3b5b04e55393b6fc3cf55fb Mon Sep 17 00:00:00 2001 From: Yun-Sheng Chang Date: Sat, 16 Nov 2024 14:42:26 -0500 Subject: [PATCH] Prove replica applier --- .../Goose/github_com/mit_pdos/tulip/replica.v | 29 +- src/program_proof/rsm/pure/list.v | 10 + src/program_proof/tulip/base.v | 6 + src/program_proof/tulip/cmd.v | 11 +- src/program_proof/tulip/inv_group.v | 69 ++ .../tulip/invariance/execute_commit.v | 4 +- .../tulip/invariance/learn_commit.v | 25 +- src/program_proof/tulip/program/prelude.v | 4 +- .../tulip/program/replica/replica.v | 888 +++++++++++++++++- src/program_proof/tulip/program/tuple/tuple.v | 27 +- 10 files changed, 1009 insertions(+), 64 deletions(-) diff --git a/external/Goose/github_com/mit_pdos/tulip/replica.v b/external/Goose/github_com/mit_pdos/tulip/replica.v index dc30fbd9c..a0dc666b6 100644 --- a/external/Goose/github_com/mit_pdos/tulip/replica.v +++ b/external/Goose/github_com/mit_pdos/tulip/replica.v @@ -35,15 +35,15 @@ Definition Replica := struct.decl [ Return values: @terminated: Whether txn @ts has terminated (committed or aborted). *) -Definition Replica__queryTxnTermination: val := - rec: "Replica__queryTxnTermination" "rp" "ts" := +Definition Replica__terminated: val := + rec: "Replica__terminated" "rp" "ts" := let: (<>, "terminated") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in "terminated". Definition Replica__QueryTxnTermination: val := rec: "Replica__QueryTxnTermination" "rp" "ts" := Mutex__Lock (struct.loadF Replica "mu" "rp");; - let: "terminated" := Replica__queryTxnTermination "rp" "ts" in + let: "terminated" := Replica__terminated "rp" "ts" in Mutex__Unlock (struct.loadF Replica "mu" "rp");; "terminated". @@ -444,7 +444,7 @@ Definition Replica__release: val := Definition Replica__applyCommit: val := rec: "Replica__applyCommit" "rp" "ts" "pwrs" := - let: "committed" := Replica__queryTxnTermination "rp" "ts" in + let: "committed" := Replica__terminated "rp" "ts" in (if: "committed" then #() else @@ -460,7 +460,7 @@ Definition Replica__applyCommit: val := Definition Replica__applyAbort: val := rec: "Replica__applyAbort" "rp" "ts" := - let: "aborted" := Replica__queryTxnTermination "rp" "ts" in + let: "aborted" := Replica__terminated "rp" "ts" in (if: "aborted" then #() else @@ -475,24 +475,23 @@ Definition Replica__applyAbort: val := Definition Replica__apply: val := rec: "Replica__apply" "rp" "cmd" := - (if: (struct.get txnlog.Cmd "Kind" "cmd") = #0 - then #() + (if: (struct.get txnlog.Cmd "Kind" "cmd") = #1 + then + Replica__applyCommit "rp" (struct.get txnlog.Cmd "Timestamp" "cmd") (struct.get txnlog.Cmd "PartialWrites" "cmd");; + #() else - (if: (struct.get txnlog.Cmd "Kind" "cmd") = #1 + (if: (struct.get txnlog.Cmd "Kind" "cmd") = #2 then - Replica__applyCommit "rp" (struct.get txnlog.Cmd "Timestamp" "cmd") (struct.get txnlog.Cmd "PartialWrites" "cmd");; - #() - else Replica__applyAbort "rp" (struct.get txnlog.Cmd "Timestamp" "cmd");; - #())). + #() + else #())). Definition Replica__Start: val := rec: "Replica__Start" "rp" := Mutex__Lock (struct.loadF Replica "mu" "rp");; Skip;; (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>, - let: "lsn" := std.SumAssumeNoOverflow (struct.loadF Replica "lsna" "rp") #1 in - let: ("cmd", "ok") := txnlog.TxnLog__Lookup (struct.loadF Replica "txnlog" "rp") "lsn" in + let: ("cmd", "ok") := txnlog.TxnLog__Lookup (struct.loadF Replica "txnlog" "rp") (struct.loadF Replica "lsna" "rp") in (if: (~ "ok") then Mutex__Unlock (struct.loadF Replica "mu" "rp");; @@ -501,7 +500,7 @@ Definition Replica__Start: val := Continue else Replica__apply "rp" "cmd";; - struct.storeF Replica "lsna" "rp" "lsn";; + struct.storeF Replica "lsna" "rp" (std.SumAssumeNoOverflow (struct.loadF Replica "lsna" "rp") #1);; Continue));; #(). diff --git a/src/program_proof/rsm/pure/list.v b/src/program_proof/rsm/pure/list.v index e6021f30d..b71a262de 100644 --- a/src/program_proof/rsm/pure/list.v +++ b/src/program_proof/rsm/pure/list.v @@ -171,4 +171,14 @@ Section lemma. (l ++ [x]) !! n = Some x. Proof. intros ->. apply lookup_snoc_length. Qed. + Lemma prefix_singleton l x : + l !! O = Some x -> + prefix [x] l. + Proof. + intros Hx. + destruct l as [| x' l']; first done. + inv Hx. + apply prefix_cons, prefix_nil. + Qed. + End lemma. diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v index 11c359d67..53bb7c293 100644 --- a/src/program_proof/tulip/base.v +++ b/src/program_proof/tulip/base.v @@ -211,6 +211,12 @@ Definition valid_wrs (wrs : dbmap) := dom wrs ⊆ keys_all. Definition valid_key (key : dbkey) := key ∈ keys_all. +Definition valid_ccommand gid (c : ccommand) := + match c with + | CmdCommit ts pwrs => valid_ts ts ∧ valid_pwrs gid pwrs + | CmdAbort ts => valid_ts ts + end. + Class tulip_ghostG (Σ : gFunctors). Record tulip_names := {}. diff --git a/src/program_proof/tulip/cmd.v b/src/program_proof/tulip/cmd.v index 5c853a94d..8f145acca 100644 --- a/src/program_proof/tulip/cmd.v +++ b/src/program_proof/tulip/cmd.v @@ -265,13 +265,18 @@ Section apply_cmds. Definition not_stuck st := st ≠ Stuck. + Definition safe_extension (ts : nat) (pwrs : dbmap) (histm : gmap dbkey dbhist) := + map_Forall (λ _ l, (length l ≤ ts)%nat) (filter (λ x, x.1 ∈ dom pwrs) histm). + Definition apply_commit st (tid : nat) (pwrs : dbmap) := match st with - | State cm hists => + | State cm histm => match cm !! tid with | Some true => st | Some false => Stuck - | _ => State (<[tid := true]> cm) (multiwrite tid pwrs hists) + | _ => if decide (safe_extension tid pwrs histm) + then State (<[tid := true]> cm) (multiwrite tid pwrs histm) + else Stuck end | Stuck => Stuck end. @@ -341,7 +346,7 @@ Section apply_cmds. destruct x eqn:Hx; rewrite /apply_cmds foldl_snoc apply_cmds_unfold Hrsm1 /= in Hrsm. { (* Case [CmdCommit]. *) destruct (stm1 !! tid) as [st |]; last first. - { inv Hrsm. apply multiwrite_dom. } + { case_decide; last done. inv Hrsm. apply multiwrite_dom. } by destruct st; inv Hrsm. } { (* Case [CmdAbort]. *) diff --git a/src/program_proof/tulip/inv_group.v b/src/program_proof/tulip/inv_group.v index 2381fac66..ec6303187 100644 --- a/src/program_proof/tulip/inv_group.v +++ b/src/program_proof/tulip/inv_group.v @@ -167,6 +167,19 @@ Section inv. ⌜valid_ts ts⌝. Proof. iIntros "Hsafe". by iDestruct "Hsafe" as (?) "(_ & ? & _ & _ & _)". Qed. + Lemma safe_txn_pwrs_impl_valid_wrs γ gid ts pwrs : + safe_txn_pwrs γ gid ts pwrs -∗ + ⌜valid_wrs pwrs⌝. + Proof. + iIntros "Hsafe". + iDestruct "Hsafe" as (?) "(_ & _ & %Hvw & _ & %Hpwrs)". + iPureIntro. + rewrite Hpwrs. + rewrite /valid_wrs. + etrans; last apply Hvw. + apply subseteq_dom, map_filter_subseteq. + Qed. + (** The [StAborted] branch says that a transaction is aborted globally if it is aborted locally on some group (the other direction is encoded in [safe_submit]). This gives contradiction when learning a commit command under @@ -197,6 +210,7 @@ Section inv. Definition safe_commit γ gid ts pwrs : iProp Σ := ∃ wrs, is_txn_committed γ ts wrs ∗ is_txn_wrs γ ts wrs ∗ + ⌜valid_ts ts⌝ ∗ ⌜pwrs = wrs_group gid wrs⌝ ∗ ⌜gid ∈ ptgroups (dom wrs)⌝ ∗ ⌜valid_wrs wrs⌝. @@ -375,6 +389,61 @@ Section lemma. apply Hprefixh. Qed. + Definition group_histm_lbs_from_log γ gid log : iProp Σ := + match apply_cmds log with + | State _ histm => ([∗ map] k ↦ h ∈ filter_group gid histm, is_repl_hist_lb γ k h) + | _ => False + end. + + #[global] + Instance group_histm_lbs_from_log_persistent γ gid log : + Persistent (group_histm_lbs_from_log γ gid log). + Proof. rewrite /group_histm_lbs_from_log. destruct (apply_cmds log); apply _. Defined. + + Lemma group_inv_witness_group_histm_lbs_from_log {γ gid} loglb : + is_txn_log_lb γ gid loglb -∗ + group_inv γ gid -∗ + group_histm_lbs_from_log γ gid loglb. + Proof. + iIntros "#Hloglb Hgroup". + rewrite /group_histm_lbs_from_log. + destruct (apply_cmds loglb) as [cmlb histmlb |] eqn:Happly; last first. + { do 2 iNamed "Hgroup". + iDestruct (txn_log_prefix with "Hlog Hloglb") as %Hprefix. + unshelve epose proof (apply_cmds_not_stuck loglb _ Hprefix _) as Hns. + { by rewrite Hrsm. } + done. + } + iApply big_sepM_forall. + iIntros (k h Hh). + apply map_lookup_filter_Some in Hh as [Hh Hgid]. + iApply (group_inv_witness_repl_hist with "Hloglb Hgroup"). + { pose proof (apply_cmds_dom _ _ _ Happly) as Hdom. + apply elem_of_dom_2 in Hh. + set_solver. + } + { done. } + { by rewrite /hist_from_log Happly. } + Qed. + + Lemma group_inv_impl_valid_ccommand_cpool {γ gid} cpool : + group_inv_no_cpool γ gid cpool -∗ + ⌜set_Forall (valid_ccommand gid) cpool⌝. + Proof. + iIntros "Hgroup". + do 2 iNamed "Hgroup". + iIntros (c Hc). + iDestruct (big_sepS_elem_of with "Hsafecp") as "Hsafec"; first apply Hc. + destruct c; simpl. + { iDestruct "Hsafec" as (wrs) "(_ & _ & %Hvts & %Hwg & %Hgid & %Hvw)". + iPureIntro. + split; first done. + rewrite /valid_pwrs Hwg wrs_group_keys_group_dom. + set_solver. + } + { by iDestruct "Hsafec" as "[_ %Hvts]". } + Qed. + Lemma group_inv_extract_log_expose_cpool {γ} gid : group_inv γ gid -∗ ∃ log cpool, diff --git a/src/program_proof/tulip/invariance/execute_commit.v b/src/program_proof/tulip/invariance/execute_commit.v index 3074ea130..05af9fec8 100644 --- a/src/program_proof/tulip/invariance/execute_commit.v +++ b/src/program_proof/tulip/invariance/execute_commit.v @@ -35,7 +35,7 @@ Section execute_commit. set_solver. } iDestruct (big_sepS_elem_of with "Hsafecp") as "Hsafec"; first apply Hin. - iDestruct "Hsafec" as (wrs) "(_ & Hwrs & %Hpwrs & %Hgid & %Hvwrs)". + iDestruct "Hsafec" as (wrs) "(_ & Hwrs & _ & %Hpwrs & %Hgid & %Hvwrs)". assert (Hdompwrs : dom pwrs ⊆ keys_all). { rewrite Hpwrs wrs_group_keys_group_dom. set_solver. } iFrame "Hwrs %". @@ -110,6 +110,7 @@ Section execute_commit. rewrite Hvl. destruct (vl !! t) as [b |] eqn:Hvlt; last done. destruct b; last done. + clear Hns. case_decide as Ht; last done. destruct Ht as (Hgelen & Hnz). assert (is_Some (ptsm !! k)) as [pts Hpts]. @@ -186,6 +187,7 @@ Section execute_commit. rewrite (multiwrite_modified Hv Hh). destruct (vl !! t) as [b |] eqn:Hvlt; last done. destruct b; last done. + clear Hns. case_decide as Ht; last done. destruct Ht as [Hgelen Hnepts]. iSpecialize ("Hgabt" $! k t). diff --git a/src/program_proof/tulip/invariance/learn_commit.v b/src/program_proof/tulip/invariance/learn_commit.v index 1841c7279..87950edf0 100644 --- a/src/program_proof/tulip/invariance/learn_commit.v +++ b/src/program_proof/tulip/invariance/learn_commit.v @@ -105,7 +105,7 @@ Section inv. (* Obtain proof that [ts] has committed. *) iDestruct (big_sepS_elem_of with "Hsafecp") as "Hc"; first apply Hc. simpl. - iDestruct "Hc" as (wrs) "(Hcmt & Hwrs & %Hpwrs & %Hgid)". + iDestruct "Hc" as (wrs) "(Hcmt & Hwrs & _ & %Hpwrs & %Hgid)". rewrite /group_inv_no_log_with_cpool. destruct (stm !! ts) as [st |] eqn:Hdup; last first. { (* Case: Empty state; contradiction---no prepare before commit. *) @@ -213,6 +213,27 @@ Section inv. iDestruct (keys_inv_committed with "Hcmt Hkeys Htxnsys") as "[Hkeys Htxnsys]". { apply Hdomhistmg. } { rewrite Hpwrs. apply map_filter_subseteq. } + (* Prove safe extension used later to re-establish the RSM invariant. *) + iAssert (⌜safe_extension ts pwrs hists⌝)%I as %Hsafeext. + { iIntros (k h Hh). + apply map_lookup_filter_Some in Hh as [Hh Hk]. simpl in Hk. + assert (Hhistmk : histm !! k = Some h). + { clear -Hinclhistmg Hdomhistmg Hh Hk. + rewrite -Hdomhistmg elem_of_dom in Hk. + destruct Hk as [h' Hh']. + unshelve epose proof (lookup_weaken_inv _ _ _ _ _ Hh' _ Hh) as ->. + { etrans; [apply Hinclhistmg | apply map_filter_subseteq]. } + done. + } + apply elem_of_dom in Hk as [v Hpwrsk]. + iDestruct (big_sepM2_lookup with "Hkeys") as "Hkey". + { apply Hhistmk. } + { apply Hpwrsk. } + do 3 iNamed "Hkey". + iPureIntro. + rewrite /ext_by_cmtd Hv in Hdiffc. + by destruct Hdiffc as [_ ?]. + } (* Re-establish keys invariant w.r.t. updated tuples. *) iDestruct (keys_inv_learn_commit with "Hkeys") as "Hkeys". (* Put ownership of tuples back to keys invariant. *) @@ -251,7 +272,7 @@ Section inv. { iFrame "Hcmt". } iFrame "∗ # %". iPureIntro. - split; first done. + split; first by case_decide. split. { rewrite dom_insert_L. apply (map_Forall_impl _ _ _ Hpmstm). diff --git a/src/program_proof/tulip/program/prelude.v b/src/program_proof/tulip/program/prelude.v index d78183d44..63adf1272 100644 --- a/src/program_proof/tulip/program/prelude.v +++ b/src/program_proof/tulip/program/prelude.v @@ -76,8 +76,8 @@ Defined. Definition ccommand_to_val (pwrsS : Slice.t) (c : ccommand) : val := match c with - | CmdCommit ts _ => (#(U64 0), (#(U64 ts), (to_val pwrsS, (zero_val stringT, #())))) - | CmdAbort ts => (#(U64 1), (#(U64 ts), (Slice.nil, (zero_val stringT, #())))) + | CmdCommit ts _ => (#(U64 1), (#(U64 ts), (to_val pwrsS, (zero_val stringT, #())))) + | CmdAbort ts => (#(U64 2), (#(U64 ts), (Slice.nil, (zero_val stringT, #())))) end. Section def. diff --git a/src/program_proof/tulip/program/replica/replica.v b/src/program_proof/tulip/program/replica/replica.v index 3a3bd47c7..c16a09c8a 100644 --- a/src/program_proof/tulip/program/replica/replica.v +++ b/src/program_proof/tulip/program/replica/replica.v @@ -1,4 +1,5 @@ -From Perennial.program_proof.tulip.invariance Require Import validate execute accept. +From Perennial.program_proof.tulip.invariance Require Import validate execute accept learn. +From Perennial.program_proof Require Import std_proof. From Perennial.program_proof.tulip.program Require Import prelude. From Perennial.program_proof.tulip.program.replica Require Import replica_repr replica_accept replica_acquire replica_bump_key replica_finalized @@ -11,15 +12,18 @@ From Perennial.program_proof.tulip.program.index Require Import index. Section replica. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Definition own_replica (rp : loc) (gid rid : u64) γ α : iProp Σ := - ∃ (lsna : u64) (cm : gmap nat bool) (histm : gmap dbkey dbhist) + Definition own_replica_histm (rp : loc) (histm : gmap dbkey dbhist) α : iProp Σ := + ([∗ map] k ↦ h ∈ histm, own_phys_hist_half α k h). + + Definition own_replica_with_cloga_no_lsna + (rp : loc) (cloga : dblog) (gid rid : u64) γ α : iProp Σ := + ∃ (cm : gmap nat bool) (histm : gmap dbkey dbhist) (cpm : gmap nat dbmap) (ptgsm : gmap nat (gset u64)) (sptsm ptsm : gmap dbkey nat) (psm : gmap nat (nat * bool)) (rkm : gmap nat nat) - (clog cloga : dblog) (ilog : list (nat * icommand)), + (clog : dblog) (ilog : list (nat * icommand)), let log := merge_clog_ilog cloga ilog in - "Hlsna" ∷ rp ↦[Replica :: "lsna"] #lsna ∗ "Hcm" ∷ own_replica_cm rp cm ∗ - "Hphistm" ∷ ([∗ map] k ↦ h ∈ histm, own_phys_hist_half α k h) ∗ + "Hhistm" ∷ own_replica_histm rp histm α ∗ "Hcpm" ∷ own_replica_cpm rp cpm ∗ "Hptsmsptsm" ∷ own_replica_ptsm_sptsm rp ptsm sptsm ∗ "Hpsmrkm" ∷ own_replica_psm_rkm rp psm rkm ∗ @@ -30,18 +34,798 @@ Section replica. "#Hclogalb" ∷ is_txn_log_lb γ gid cloga ∗ "%Hdompsmrkm" ∷ ⌜dom psm = dom rkm⌝ ∗ "%Hcloga" ∷ ⌜prefix clog cloga⌝ ∗ + "%Hvcpm" ∷ ⌜map_Forall (λ _ m, valid_wrs m) cpm⌝ ∗ + "%Hvicmds" ∷ ⌜Forall (λ nc, (nc.1 <= length cloga)%nat) ilog⌝ ∗ "%Hexec" ∷ ⌜execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm psm rkm⌝. - Definition is_replica (rp : loc) : iProp Σ := - ∃ (mu : loc) (txnlog : loc) (idx : loc) (gid rid : u64) γ α, - "#HmuP" ∷ readonly (rp ↦[Replica :: "mu"] #mu) ∗ - "#Hlock" ∷ is_lock tulipNS #mu (own_replica rp gid rid γ α) ∗ + Definition own_replica (rp : loc) (gid rid : u64) γ α : iProp Σ := + ∃ (cloga : dblog) (lsna : u64), + "Hrp" ∷ own_replica_with_cloga_no_lsna rp cloga gid rid γ α ∗ + "Hlsna" ∷ rp ↦[Replica :: "lsna"] #lsna ∗ + "%Hlencloga" ∷ ⌜length cloga = uint.nat lsna⌝. + + Definition is_replica_txnlog (rp : loc) gid γ : iProp Σ := + ∃ (txnlog : loc), "#HtxnlogP" ∷ readonly (rp ↦[Replica :: "txnlog"] #txnlog) ∗ - "#Htxnlog" ∷ is_txnlog txnlog gid γ ∗ - "#HidxP" ∷ readonly (rp ↦[Replica :: "idx"] #idx) ∗ - "#Hidx" ∷ is_index idx α ∗ - "%Hgid" ∷ ⌜gid ∈ gids_all⌝. + "#Htxnlog" ∷ is_txnlog txnlog gid γ. + + Definition is_replica_idx (rp : loc) α : iProp Σ := + ∃ (idx : loc), + "#HidxP" ∷ readonly (rp ↦[Replica :: "idx"] #idx) ∗ + "#Hidx" ∷ is_index idx α. + + Definition is_replica (rp : loc) : iProp Σ := + ∃ (mu : loc) (gid rid : u64) γ α, + "#HmuP" ∷ readonly (rp ↦[Replica :: "mu"] #mu) ∗ + "#Hlock" ∷ is_lock tulipNS #mu (own_replica rp gid rid γ α) ∗ + "#Htxnlog" ∷ is_replica_txnlog rp gid γ ∗ + "#Hidx" ∷ is_replica_idx rp α ∗ + "#Hinv" ∷ know_tulip_inv γ ∗ + "%Hgid" ∷ ⌜gid ∈ gids_all⌝. + + Theorem wp_Replica__multiwrite rp (tsW : u64) pwrsS pwrsL pwrs histm gid γ α : + let ts := uint.nat tsW in + let histm' := multiwrite ts pwrs histm in + valid_pwrs gid pwrs -> + dom histm = keys_all -> + safe_extension ts pwrs histm -> + ([∗ map] k ↦ h ∈ filter_group gid histm', is_repl_hist_lb γ k h) -∗ + is_replica_idx rp α -∗ + {{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_histm rp histm α }}} + Replica__multiwrite #rp #tsW (to_val pwrsS) + {{{ RET #(); + own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_histm rp histm' α + }}}. + Proof. + iIntros (ts histm' Hvw Hdomhistm Hlenhistm) "#Hrlbs #Hidx". + iIntros (Φ) "!> [[HpwrsS %Hpwrs] Hhistm] HΦ". + wp_rec. + + (*@ func (rp *Replica) multiwrite(ts uint64, pwrs []tulip.WriteEntry) { @*) + (*@ for _, ent := range pwrs { @*) + (*@ key := ent.Key @*) + (*@ value := ent.Value @*) + (*@ tpl := rp.idx.GetTuple(key) @*) + (*@ if value.Present { @*) + (*@ tpl.AppendVersion(ts, value.Content) @*) + (*@ } else { @*) + (*@ tpl.KillVersion(ts) @*) + (*@ } @*) + (*@ } @*) + (*@ } @*) + iDestruct (own_slice_sz with "HpwrsS") as %Hlenpwrs. + iDestruct (own_slice_small_acc with "HpwrsS") as "[HpwrsS HpwrsC]". + set P := (λ (i : u64), + let pwrs' := list_to_map (take (uint.nat i) pwrsL) in + own_replica_histm rp (multiwrite ts pwrs' histm) α)%I. + wp_apply (wp_forSlice P with "[] [$HpwrsS Hhistm]"); last first; first 1 last. + { (* Loop entry. *) + subst P. simpl. + rewrite uint_nat_W64_0 take_0 list_to_map_nil. + by rewrite multiwrite_empty. + } + { (* Loop body. *) + clear Φ. + iIntros (i [k v]) "!>". + iIntros (Φ) "(Hhistm & %Hbound & %Hi) HΦ". + subst P. simpl. + iNamed "Hidx". + wp_loadField. + (* Prove [k] in the domain of [pwrs] and in [keys_all]. *) + apply elem_of_list_lookup_2 in Hi as Hpwrsv. + rewrite -Hpwrs elem_of_map_to_list in Hpwrsv. + apply elem_of_dom_2 in Hpwrsv as Hdompwrs. + assert (Hvk : k ∈ keys_all). + { clear -Hvw Hdompwrs. set_solver. } + wp_apply (wp_Index__GetTuple with "Hidx"); first apply Hvk. + iIntros (tpl) "#Htpl". + (* Obtain proof that the current key [k] has not been written. *) + pose proof (NoDup_fst_map_to_list pwrs) as Hnd. + rewrite Hpwrs in Hnd. + pose proof (list_lookup_fmap fst pwrsL (uint.nat i)) as Hk. + rewrite Hi /= in Hk. + pose proof (not_elem_of_take _ _ _ Hnd Hk) as Htake. + rewrite -fmap_take in Htake. + apply not_elem_of_list_to_map_1 in Htake as Hnone. + (* Adjust the goal. *) + rewrite uint_nat_word_add_S; last by word. + rewrite (take_S_r _ _ _ Hi) list_to_map_snoc; last done. + set pwrs' := (list_to_map _) in Hnone *. + assert (is_Some (histm !! k)) as [h Hh]. + { by rewrite -elem_of_dom Hdomhistm. } + (* Obtain the length constraint. *) + rewrite /safe_extension in Hlenhistm. + set histmwr := filter _ _ in Hlenhistm. + assert (Hhistmwrk : histmwr !! k = Some h). + { by apply map_lookup_filter_Some_2. } + specialize (Hlenhistm _ _ Hhistmwrk). simpl in Hlenhistm. + (* Obtain the replicated history lb. *) + assert (Hh' : histm' !! k = Some (last_extend ts h ++ [v])). + { by rewrite (multiwrite_modified Hpwrsv Hh). } + iDestruct (big_sepM_lookup _ _ k with "Hrlbs") as "Hrlb". + { apply map_lookup_filter_Some_2; first apply Hh'. simpl. + clear -Hdompwrs Hvw. set_solver. + } + (* Take the physical history out. *) + iDestruct (big_sepM_delete with "Hhistm") as "[Hh Hhistm]". + { rewrite multiwrite_unmodified; [apply Hh | apply Hnone]. } + destruct v as [s |]; wp_pures. + { (* Case: [@AppendVersion]. *) + wp_apply (wp_Tuple__AppendVersion with "Hrlb Htpl Hh"). + { apply Hlenhistm. } + iIntros "Hh". + iDestruct (big_sepM_insert_2 with "Hh Hhistm") as "Hhistm". + rewrite insert_delete_insert /multiwrite. + erewrite insert_merge_l; last first. + { by rewrite Hh. } + iApply "HΦ". + iFrame "∗ #". + } + { (* Case: [@KillVersion]. *) + wp_apply (wp_Tuple__KillVersion with "Hrlb Htpl Hh"). + { apply Hlenhistm. } + iIntros "Hh". + iDestruct (big_sepM_insert_2 with "Hh Hhistm") as "Hhistm". + rewrite insert_delete_insert /multiwrite. + erewrite insert_merge_l; last first. + { by rewrite Hh. } + iApply "HΦ". + iFrame "∗ #". + } + } + iIntros "[Hhistm HpwrsS]". subst P. simpl. + iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS". + wp_pures. + iApply "HΦ". + rewrite -Hlenpwrs firstn_all -Hpwrs list_to_map_to_list. + by iFrame. + Qed. + + Theorem wp_Replica__terminated rp (tsW : u64) cm : + let ts := uint.nat tsW in + {{{ own_replica_cm rp cm }}} + Replica__terminated #rp #tsW + {{{ RET #(bool_decide (ts ∈ dom cm)); own_replica_cm rp cm }}}. + Proof. + iIntros (ts Φ) "Hcm HΦ". + wp_rec. + (*@ func (rp *Replica) terminated(ts uint64) bool { @*) + (*@ _, terminated := rp.txntbl[ts] @*) + (*@ return terminated @*) + (*@ } @*) + iNamed "Hcm". + wp_loadField. + wp_apply (wp_MapGet with "Htxntbl"). + iIntros (v ok) "[%Hok Htxntbl]". + wp_pures. + case_bool_decide as Hts. + { destruct ok; last first. + { exfalso. + apply map_get_false in Hok as [Hnone _]. + apply elem_of_dom in Hts as [b Hb]. + symmetry in Hcmabs. + pose proof (lookup_kmap_eq_None _ _ _ _ _ Hcmabs Hnone) as Hcontra. + specialize (Hcontra ts). + unshelve epose proof (Hcontra _) as Hcmts; first word. + by rewrite Hb in Hcmts. + } + iApply "HΦ". by iFrame "∗ %". + } + { destruct ok. + { exfalso. + apply map_get_true in Hok. + apply not_elem_of_dom in Hts. + pose proof (lookup_kmap_eq_None _ _ _ _ _ Hcmabs Hts) as Hcontra. + specialize (Hcontra tsW). + unshelve epose proof (Hcontra _) as Hcmts; first word. + by rewrite Hok in Hcmts. + } + iApply "HΦ". by iFrame "∗ %". + } + Qed. + + Theorem wp_Replica__release rp pwrsS pwrsL pwrs ptsm sptsm : + valid_wrs pwrs -> + {{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}} + Replica__release #rp (to_val pwrsS) + {{{ RET #(); + own_dbmap_in_slice pwrsS pwrsL pwrs ∗ + own_replica_ptsm_sptsm rp (release pwrs ptsm) sptsm + }}}. + Proof. + iIntros (Hvw Φ) "[[HpwrsS %Hpwrs] Hrp] HΦ". + wp_rec. + iDestruct (own_replica_ptsm_sptsm_dom with "Hrp") as %[Hdomptsm Hdomsptsm]. + + (*@ func (rp *Replica) release(pwrs []tulip.WriteEntry) { @*) + (*@ for _, ent := range pwrs { @*) + (*@ key := ent.Key @*) + (*@ rp.releaseKey(key) @*) + (*@ } @*) + (*@ } @*) + iDestruct (own_slice_sz with "HpwrsS") as %Hlenpwrs. + iDestruct (own_slice_small_acc with "HpwrsS") as "[HpwrsS HpwrsC]". + set P := (λ (i : u64), + let pwrs' := list_to_map (take (uint.nat i) pwrsL) in + own_replica_ptsm_sptsm rp (release pwrs' ptsm) sptsm)%I. + wp_apply (wp_forSlice P with "[] [$HpwrsS Hrp]"); last first; first 1 last. + { (* Loop entry. *) + subst P. simpl. + rewrite uint_nat_W64_0 take_0 list_to_map_nil. + by rewrite release_empty. + } + { (* Loop body. *) + clear Φ. + iIntros (i [k v]) "!>". + iIntros (Φ) "(Hrp & %Hbound & %Hi) HΦ". + subst P. simpl. + wp_pures. + wp_apply (wp_Replica__releaseKey with "Hrp"). + iIntros "Hrp". + iApply "HΦ". + (* Obtain proof that the current key [k] has not been written. *) + pose proof (NoDup_fst_map_to_list pwrs) as Hnd. + rewrite Hpwrs in Hnd. + pose proof (list_lookup_fmap fst pwrsL (uint.nat i)) as Hk. + rewrite Hi /= in Hk. + pose proof (not_elem_of_take _ _ _ Hnd Hk) as Htake. + rewrite -fmap_take in Htake. + (* Adjust the goal. *) + rewrite uint_nat_word_add_S; last by word. + rewrite (take_S_r _ _ _ Hi) list_to_map_snoc; last apply Htake. + set pwrs' := list_to_map _. + rewrite /release setts_insert; last first. + { rewrite -Hpwrs in Hi. + apply elem_of_list_lookup_2, elem_of_map_to_list, elem_of_dom_2 in Hi. + clear -Hvw Hi Hdomptsm. set_solver. + } + done. + } + iIntros "[Hrp HpwrsS]". + subst P. simpl. + rewrite -Hlenpwrs firstn_all -Hpwrs list_to_map_to_list. + iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS". + wp_pures. + iApply "HΦ". + by iFrame. + Qed. + + Theorem wp_Replica__applyCommit + rp (tsW : u64) pwrsS pwrsL pwrs cloga gid rid γ α : + let ts := uint.nat tsW in + let cloga' := cloga ++ [CmdCommit ts pwrs] in + valid_pwrs gid pwrs -> + group_histm_lbs_from_log γ gid cloga' -∗ + is_txn_log_lb γ gid cloga' -∗ + is_replica_idx rp α -∗ + {{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ + own_replica_with_cloga_no_lsna rp cloga gid rid γ α + }}} + Replica__applyCommit #rp #tsW (to_val pwrsS) + {{{ RET #(); + own_dbmap_in_slice pwrsS pwrsL pwrs ∗ + own_replica_with_cloga_no_lsna rp cloga' gid rid γ α + }}}. + Proof. + iIntros (ts cloga' Hvpwrs) "#Hhistmlb #Hlb' #Hidx". + iIntros (Φ) "!> [Hpwrs Hrp] HΦ". + wp_rec. + (* First establish that applying this commit results does not get stuck. *) + rewrite /group_histm_lbs_from_log. + destruct (apply_cmds cloga') as [cm' histm' |] eqn:Happly'; last done. + (* Also establish connection between executing entire log vs. consistent log. *) + iNamed "Hrp". + unshelve epose proof (execute_cmds_apply_cmds cloga ilog cm histm _) as Happly. + { by eauto 10. } + + (*@ func (rp *Replica) applyCommit(ts uint64, pwrs []tulip.WriteEntry) { @*) + (*@ // Query the transaction table. Note that if there's an entry for @ts in @*) + (*@ // @txntbl, then transaction @ts can only be committed. That's why we're not @*) + (*@ // even reading the value of entry. @*) + (*@ committed := rp.terminated(ts) @*) + (*@ if committed { @*) + (*@ return @*) + (*@ } @*) + (*@ @*) + wp_apply (wp_Replica__terminated with "Hcm"). + iIntros "Hcm". + case_bool_decide as Hterm; wp_pures. + { iApply "HΦ". + apply elem_of_dom in Hterm as [b Hb]. + iFrame "∗ # %". + iPureIntro. simpl. + exists ptgsm. + split. + { by apply prefix_app_r. } + rewrite merge_clog_ilog_snoc_clog; last apply Hvicmds. + split. + { eapply Forall_impl; first apply Hvicmds. simpl. + intros nc Hnc. + rewrite length_app /=. + clear -Hnc. lia. + } + rewrite /execute_cmds foldl_snoc /= execute_cmds_unfold Hexec /= Hb. + destruct b; first done. + by rewrite /apply_cmds foldl_snoc /= apply_cmds_unfold /apply_commit Happly Hb in Happly'. + } + apply not_elem_of_dom in Hterm. + rewrite /apply_cmds foldl_snoc /= apply_cmds_unfold Happly /= Hterm in Happly'. + case_decide as Hsafeext; last done. + symmetry in Happly'. inv Happly'. + + (*@ rp.multiwrite(ts, pwrs) @*) + (*@ @*) + wp_apply (wp_Replica__multiwrite with "Hhistmlb Hidx [$Hpwrs $Hhistm]"). + { apply Hvpwrs. } + { by eapply apply_cmds_dom. } + { apply Hsafeext. } + iIntros "[Hpwrs Hhistm]". + + (*@ rp.txntbl[ts] = true @*) + (*@ @*) + iNamed "Hcm". + wp_loadField. + wp_apply (wp_MapInsert with "Htxntbl"); first done. + iIntros "Htxntbl". + + (*@ // With PCR, a replica might receive a commit even if it is not prepared on @*) + (*@ // this replica. @*) + (*@ _, prepared := rp.prepm[ts] @*) + (*@ @*) + iNamed "Hcpm". + wp_loadField. + wp_apply (wp_MapGet with "HprepmS"). + iIntros (prepS prepared) "[%Hprepared HprepmS]". + wp_pures. + + (*@ if prepared { @*) + (*@ rp.release(pwrs) @*) + (*@ delete(rp.prepm, ts) @*) + (*@ } @*) + (*@ } @*) + destruct prepared; wp_pures. + { wp_apply (wp_Replica__release with "[$Hpwrs $Hptsmsptsm]"). + { clear -Hvpwrs. set_solver. } + iIntros "[Hpwrs Hptsmsptsm]". + wp_loadField. + wp_apply (wp_MapDelete with "HprepmS"). + iIntros "HprepmS". + wp_pures. + iApply "HΦ". + apply map_get_true in Hprepared. + iDestruct (big_sepM2_delete_l with "Hprepm") as (m) "(%Hm & _ & Hprepm)". + { apply Hprepared. } + iAssert ([∗ set] t ∈ dom (delete ts cpm), is_replica_validated_ts γ gid rid t)%I + as "#Hrpvds'". + { rewrite dom_delete_L. + iDestruct (big_sepS_delete _ _ ts with "Hrpvds") as "[_ ?]"; last done. + symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hcpmabs Hm) as (ts' & Hts' & Hcpmts). + assert (ts' = ts) as -> by word. + by apply elem_of_dom. + } + iClear "Hrpvds". + iFrame "∗ # %". + iPureIntro. simpl. + exists (<[ts := true]> cm), (delete ts ptgsm). + split. + { rewrite 2!kmap_insert. f_equal; [word | done]. } + split. + { rewrite 2!kmap_delete. f_equal; [word | done]. } + split. + { by apply prefix_app_r. } + { rewrite merge_clog_ilog_snoc_clog; last apply Hvicmds. + split. + { by apply map_Forall_delete. } + split. + { eapply Forall_impl; first apply Hvicmds. simpl. + intros nc Hnc. + rewrite length_app /=. + clear -Hnc. lia. + } + symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hcpmabs Hm) as (ts' & Hts' & Hcpmts). + assert (ts' = ts) as -> by word. + by rewrite /execute_cmds foldl_snoc /= execute_cmds_unfold Hexec /= Hterm Hcpmts. + } + } + iDestruct (big_sepM2_dom with "Hprepm") as %Hdomprepm. + iApply "HΦ". + iFrame "∗ # %". + iPureIntro. simpl. + exists (<[ts := true]> cm), ptgsm. + split. + { rewrite 2!kmap_insert. f_equal; [word | done]. } + split. + { by apply prefix_app_r. } + { rewrite merge_clog_ilog_snoc_clog; last apply Hvicmds. + split. + { eapply Forall_impl; first apply Hvicmds. simpl. + intros nc Hnc. + rewrite length_app /=. + clear -Hnc. lia. + } + apply map_get_false in Hprepared as [Hnone _]. + rewrite -not_elem_of_dom Hdomprepm not_elem_of_dom in Hnone. + symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_None _ _ _ _ _ Hcpmabs Hnone) as Hcpmnone. + specialize (Hcpmnone ts). + unshelve epose proof (Hcpmnone _) as Hcpmts; first word. + by rewrite /execute_cmds foldl_snoc /= execute_cmds_unfold Hexec /= Hterm Hcpmts. + } + Qed. + + Theorem wp_Replica__applyAbort rp (tsW : u64) cloga gid rid γ α : + let ts := uint.nat tsW in + let cloga' := cloga ++ [CmdAbort ts] in + not_stuck (apply_cmds cloga') -> + is_txn_log_lb γ gid cloga' -∗ + {{{ own_replica_with_cloga_no_lsna rp cloga gid rid γ α }}} + Replica__applyAbort #rp #tsW + {{{ RET #(); own_replica_with_cloga_no_lsna rp cloga' gid rid γ α }}}. + Proof. + iIntros (ts cloga' Hns) "#Hlb'". + iIntros (Φ) "!> Hrp HΦ". + wp_rec. + (* First establish that applying this commit results does not get stuck. *) + destruct (apply_cmds cloga') as [cm' histm' |] eqn:Happly'; last done. + (* Also establish connection between executing entire log vs. consistent log. *) + iNamed "Hrp". + unshelve epose proof (execute_cmds_apply_cmds cloga ilog cm histm _) as Happly. + { by eauto 10. } + + (*@ func (rp *Replica) applyAbort(ts uint64) { @*) + (*@ // Query the transaction table. Note that if there's an entry for @ts in @*) + (*@ // @txntbl, then transaction @ts can only be aborted. That's why we're not @*) + (*@ // even reading the value of entry. @*) + (*@ aborted := rp.terminated(ts) @*) + (*@ if aborted { @*) + (*@ return @*) + (*@ } @*) + (*@ @*) + wp_apply (wp_Replica__terminated with "Hcm"). + iIntros "Hcm". + case_bool_decide as Hterm; wp_pures. + { iApply "HΦ". + apply elem_of_dom in Hterm as [b Hb]. + iFrame "∗ # %". + iPureIntro. simpl. + exists ptgsm. + split. + { by apply prefix_app_r. } + rewrite merge_clog_ilog_snoc_clog; last apply Hvicmds. + split. + { eapply Forall_impl; first apply Hvicmds. simpl. + intros nc Hnc. + rewrite length_app /=. + clear -Hnc. lia. + } + rewrite /execute_cmds foldl_snoc /= execute_cmds_unfold Hexec /= Hb. + destruct b; last done. + by rewrite /apply_cmds foldl_snoc /= apply_cmds_unfold /apply_abort Happly Hb in Happly'. + } + apply not_elem_of_dom in Hterm. + (* rewrite /apply_cmds foldl_snoc /= apply_cmds_unfold Happly /= Hterm in Happly'. *) + (* symmetry in Happly'. inv Happly'. *) + + (*@ rp.txntbl[ts] = false @*) + (*@ @*) + iNamed "Hcm". + wp_loadField. + wp_apply (wp_MapInsert with "Htxntbl"); first done. + iIntros "Htxntbl". + + (*@ // Tuples lock are held iff @prepm[ts] contains something (and so we should @*) + (*@ // release them by calling @abort). @*) + (*@ pwrs, prepared := rp.prepm[ts] @*) + (*@ @*) + iNamed "Hcpm". + wp_loadField. + wp_apply (wp_MapGet with "HprepmS"). + iIntros (prepS prepared) "[%Hprepared HprepmS]". + wp_pures. + + (*@ if prepared { @*) + (*@ rp.release(pwrs) @*) + (*@ delete(rp.prepm, ts) @*) + (*@ } @*) + (*@ } @*) + iDestruct (big_sepM2_dom with "Hprepm") as %Hdomprepm. + destruct prepared; wp_pures. + { apply map_get_true in Hprepared. + assert (is_Some (prepm !! tsW)) as [pwrs Hpwrs]. + { by rewrite -elem_of_dom -Hdomprepm elem_of_dom. } + iDestruct (big_sepM2_delete with "Hprepm") as "[Hpwrs Hprepm]". + { apply Hprepared. } + { apply Hpwrs. } + iDestruct "Hpwrs" as (pwrsL) "Hpwrs". + wp_apply (wp_Replica__release with "[$Hpwrs $Hptsmsptsm]"). + { symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hcpmabs Hpwrs) as (ts' & Hts' & Hcpmts). + assert (ts' = ts) as -> by word. + by specialize (Hvcpm _ _ Hcpmts). + } + iIntros "[Hpwrs Hptsmsptsm]". + wp_loadField. + wp_apply (wp_MapDelete with "HprepmS"). + iIntros "HprepmS". + wp_pures. + iApply "HΦ". + iAssert ([∗ set] t ∈ dom (delete ts cpm), is_replica_validated_ts γ gid rid t)%I + as "#Hrpvds'". + { rewrite dom_delete_L. + iDestruct (big_sepS_delete _ _ ts with "Hrpvds") as "[_ ?]"; last done. + symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hcpmabs Hpwrs) as (ts' & Hts' & Hcpmts). + assert (ts' = ts) as -> by word. + by apply elem_of_dom. + } + iClear "Hrpvds". + iFrame "∗ # %". + iPureIntro. simpl. + exists (<[ts := false]> cm), (delete ts ptgsm). + split. + { rewrite 2!kmap_insert. f_equal; [word | done]. } + split. + { rewrite 2!kmap_delete. f_equal; [word | done]. } + split. + { by apply prefix_app_r. } + { rewrite merge_clog_ilog_snoc_clog; last apply Hvicmds. + split. + { by apply map_Forall_delete. } + split. + { eapply Forall_impl; first apply Hvicmds. simpl. + intros nc Hnc. + rewrite length_app /=. + clear -Hnc. lia. + } + symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_Some _ _ _ _ _ _ Hcpmabs Hpwrs) as (ts' & Hts' & Hcpmts). + assert (ts' = ts) as -> by word. + by rewrite /execute_cmds foldl_snoc /= execute_cmds_unfold Hexec /= Hterm Hcpmts. + } + } + iApply "HΦ". + iFrame "∗ # %". + iPureIntro. simpl. + exists (<[ts := false]> cm), ptgsm. + split. + { rewrite 2!kmap_insert. f_equal; [word | done]. } + split. + { by apply prefix_app_r. } + { rewrite merge_clog_ilog_snoc_clog; last apply Hvicmds. + split. + { eapply Forall_impl; first apply Hvicmds. simpl. + intros nc Hnc. + rewrite length_app /=. + clear -Hnc. lia. + } + apply map_get_false in Hprepared as [Hnone _]. + rewrite -not_elem_of_dom Hdomprepm not_elem_of_dom in Hnone. + symmetry in Hcpmabs. + pose proof (lookup_kmap_eq_None _ _ _ _ _ Hcpmabs Hnone) as Hcpmnone. + specialize (Hcpmnone ts). + unshelve epose proof (Hcpmnone _) as Hcpmts; first word. + by rewrite /execute_cmds foldl_snoc /= execute_cmds_unfold Hexec /= Hterm Hcpmts. + } + Qed. + + Theorem wp_Replica__apply + rp cmd pwrsS cloga gid rid γ α : + let cloga' := cloga ++ [cmd] in + valid_ccommand gid cmd -> + group_histm_lbs_from_log γ gid cloga' -∗ + is_txn_log_lb γ gid cloga' -∗ + is_replica_idx rp α -∗ + {{{ own_pwrs_slice pwrsS cmd ∗ + own_replica_with_cloga_no_lsna rp cloga gid rid γ α + }}} + Replica__apply #rp (ccommand_to_val pwrsS cmd) + {{{ RET #(); + own_pwrs_slice pwrsS cmd ∗ + own_replica_with_cloga_no_lsna rp cloga' gid rid γ α + }}}. + Proof. + iIntros (cloga' Hvcmd) "#Hsafe #Hlb' #Hidx". + iIntros (Φ) "!> [Hpwrs Hrp] HΦ". + wp_rec. + + (*@ func (rp *Replica) apply(cmd txnlog.Cmd) { @*) + (*@ if cmd.Kind == 1 { @*) + (*@ rp.applyCommit(cmd.Timestamp, cmd.PartialWrites) @*) + (*@ } else if cmd.Kind == 2 { @*) + (*@ rp.applyAbort(cmd.Timestamp) @*) + (*@ } @*) + (*@ } @*) + wp_pures. + destruct cmd eqn:Hcmd; wp_pures. + { (* Case: CmdCommit. *) + destruct Hvcmd as [Hvts Hvpwrs]. + iDestruct "Hpwrs" as (pwrsL) "Hpwrs". + wp_apply (wp_Replica__applyCommit with "[Hsafe] [Hlb'] Hidx [$Hpwrs $Hrp]"). + { apply Hvpwrs. } + { rewrite uint_nat_W64_of_nat; first done. rewrite /valid_ts in Hvts. word. } + { rewrite uint_nat_W64_of_nat; first done. rewrite /valid_ts in Hvts. word. } + iIntros "[Hpwrs Hrp]". + wp_pures. + iApply "HΦ". + rewrite uint_nat_W64_of_nat; last first. + { rewrite /valid_ts in Hvts. word. } + by iFrame. + } + { (* Case: CmdAbort. *) + simpl in Hvcmd. + rewrite /group_histm_lbs_from_log. + destruct (apply_cmds cloga') as [cpm histm |] eqn:Happly; last done. + wp_apply (wp_Replica__applyAbort with "[Hlb'] Hrp"). + { rewrite uint_nat_W64_of_nat; first by rewrite Happly. rewrite /valid_ts in Hvcmd. word. } + { rewrite uint_nat_W64_of_nat; first done. rewrite /valid_ts in Hvcmd. word. } + iIntros "Hrp". + wp_pures. + iApply "HΦ". + rewrite uint_nat_W64_of_nat; last first. + { rewrite /valid_ts in Hvcmd. word. } + by iFrame. + } + Qed. + + Theorem wp_Replica__Start rp : + is_replica rp -∗ + {{{ True }}} + Replica__Start #rp + {{{ RET #(); True }}}. + Proof. + iIntros "#Hrp" (Φ) "!> _ HΦ". + wp_rec. + + (*@ func (rp *Replica) Start() { @*) + (*@ rp.mu.Lock() @*) + (*@ @*) + iNamed "Hrp". + wp_loadField. + wp_apply (wp_Mutex__Lock with "Hlock"). + iIntros "[Hlocked Hrp]". + wp_pures. + + (*@ for { @*) + (*@ // TODO: a more efficient interface would return multiple safe commands @*) + (*@ // at once (so as to reduce the frequency of acquiring Paxos mutex). @*) + (*@ // Ghost action: Learn a list of new commands. @*) + (*@ cmd, ok := rp.txnlog.Lookup(rp.lsna) @*) + (*@ @*) + set P := (λ b : bool, own_replica rp gid rid γ α ∗ locked #mu)%I. + wp_apply (wp_forBreak P with "[] [$Hrp $Hlocked]"); last first. + { (* Get out of an infinite loop. *) + iIntros "Hrp". wp_pures. by iApply "HΦ". + } + clear Φ. iIntros "!>" (Φ) "[Hrp Hlocked] HΦ". + wp_rec. + do 2 iNamed "Hrp". + wp_loadField. + + (*@ cmd, ok := rp.txnlog.Lookup(lsn) @*) + (*@ @*) + iNamed "Htxnlog". + wp_loadField. + wp_apply (wp_TxnLog__Lookup with "Htxnlog"). + iInv "Hinv" as "> HinvO" "HinvC". + iApply ncfupd_mask_intro; first set_solver. + iIntros "Hmask". + iNamed "HinvO". + (* Take the required group invariant. *) + iDestruct (big_sepS_elem_of_acc with "Hgroups") as "[Hgroup HgroupsC]"; first apply Hgid. + (* Separate out the ownership of the Paxos log from others. *) + iDestruct (group_inv_extract_log_expose_cpool with "Hgroup") as (paxos cpool) "[Hpaxos Hgroup]". + (* Obtain validity of command input on cpool. *) + iDestruct (group_inv_impl_valid_ccommand_cpool with "[Hgroup Hpaxos]") as %Hvcmds. + { iNamed "Hgroup". iFrame. } + (* Obtain a lower bound before passing it to Paxos. *) + iDestruct (txn_log_witness with "Hpaxos") as "#Hlb". + iExists paxos. iFrame. + iIntros (paxos') "Hpaxos". + (* Obtain prefix between the old and new logs. *) + iDestruct (txn_log_prefix with "Hpaxos Hlb") as %Hpaxos. + destruct Hpaxos as [cmds Hpaxos]. + (* Obtain inclusion between the command pool and the log. *) + iAssert (⌜cpool_subsume_log cpool paxos'⌝)%I as %Hincl. + { iNamed "Hgroup". + by iDestruct (txn_log_cpool_incl with "Hpaxos Hcpool") as %?. + } + (* Transfer validity of command input on cpool to log; used when executing @apply. *) + pose proof (set_Forall_Forall_subsume _ _ _ Hvcmds Hincl) as Hvc. + (* Obtain prefix between the applied log and the new log; needed later. *) + iDestruct (txn_log_prefix with "Hpaxos Hclogalb") as %Hloga. + (* Obtain a witness of the new log; needed later. *) + iDestruct (txn_log_witness with "Hpaxos") as "#Hlbnew". + subst paxos'. + + (*@ // Ghost action: Learn a list of new commands. @*) + (*@ @*) + iMod (group_inv_learn with "Htxnsys Hkeys Hgroup") as "(Htxnsys & Hkeys & Hgroup)". + { apply Hincl. } + iDestruct (group_inv_merge_log_hide_cpool with "Hpaxos Hgroup") as "Hgroup". + (* Put back the group invariant. *) + iDestruct ("HgroupsC" with "Hgroup") as "Hgroups". + (* Close the entire invariant. *) + iMod "Hmask" as "_". + iMod ("HinvC" with "[$Htxnsys $Hkeys $Hgroups $Hrgs]") as "_". + iIntros "!>" (cmd ok pwrsS) "[HpwrsS %Hcmd]". + wp_pures. + + (*@ if !ok { @*) + (*@ // Sleep for 1 ms. @*) + (*@ rp.mu.Unlock() @*) + (*@ primitive.Sleep(1 * 1000000) @*) + (*@ rp.mu.Lock() @*) + (*@ continue @*) + (*@ } @*) + (*@ @*) + destruct ok; wp_pures; last first. + { (* Have applied all the commands known to be committed. *) + wp_loadField. + iClear "Hlb Hlbnew". + wp_apply (wp_Mutex__Unlock with "[-HΦ $Hlock $Hlocked]"); first by iFrame "∗ # %". + wp_apply wp_Sleep. + wp_loadField. + wp_apply (wp_Mutex__Lock with "Hlock"). + iIntros "[Hlocked Hrp]". + wp_pures. + iApply "HΦ". + by iFrame. + } + (* Obtain a witness for the newly applied log. *) + iClear "Hlb". + (* Prove the newly applied log is a prefix of the new log. *) + assert (Hprefix : prefix (cloga ++ [cmd]) (paxos ++ cmds)). + { clear -Hloga Hcmd Hlencloga. + destruct Hloga as [l Hl]. + rewrite Hl. + apply prefix_app, prefix_singleton. + rewrite Hl lookup_app_r in Hcmd; last lia. + by rewrite Hlencloga /= Nat.sub_diag in Hcmd. + } + iDestruct (txn_log_lb_weaken (cloga ++ [cmd]) with "Hlbnew") as "#Hlb"; first apply Hprefix. + (* Obtain lbs of replicated history over the new history map. *) + iApply fupd_wp. + iInv "Hinv" as "> HinvO" "HinvC". + (* Take the required group invariant. *) + iNamed "HinvO". + iDestruct (big_sepS_elem_of_acc with "Hgroups") as "[Hgroup HgroupsC]"; first apply Hgid. + iDestruct (group_inv_witness_group_histm_lbs_from_log with "Hlb Hgroup") as "#Hhistmlb". + iDestruct ("HgroupsC" with "Hgroup") as "Hgroups". + iMod ("HinvC" with "[$Htxnsys $Hkeys $Hgroups $Hrgs]") as "_". + iModIntro. + + (*@ rp.apply(cmd) @*) + (*@ @*) + iAssert (own_replica_with_cloga_no_lsna rp cloga gid rid γ α)%I + with "[Hcm Hhistm Hcpm Hptsmsptsm Hpsmrkm Hclog Hilog]" as "Hrp". + { iFrame "∗ # %". } + wp_apply (wp_Replica__apply with "Hhistmlb Hlb Hidx [$HpwrsS $Hrp]"). + { rewrite Forall_forall in Hvc. + apply Hvc. + by apply elem_of_list_lookup_2 in Hcmd. + } + iIntros "[HpwrsS Hrp]". + + + (*@ rp.lsna = std.SumAssumeNoOverflow(rp.lsna, 1) @*) + (*@ @*) + wp_loadField. + wp_apply wp_SumAssumeNoOverflow. + iIntros (Hnoof). + wp_storeField. + + (*@ } @*) + (*@ } @*) + iApply "HΦ". + iFrame. + iPureIntro. + rewrite uint_nat_word_add_S; last word. + rewrite length_app /= Hlencloga. + lia. + Qed. Definition finalized_outcome γ ts res : iProp Σ := match res with @@ -79,7 +863,7 @@ Section replica. (*@ } @*) (*@ } @*) (*@ @*) - iNamed "Hrp". iNamed "Hcm". + do 2 iNamed "Hrp". iNamed "Hcm". wp_loadField. wp_apply (wp_MapGet with "Htxntbl"). iIntros (cmted bdone) "[%Hcmted Htxntbl]". @@ -106,9 +890,9 @@ Section replica. pose proof (apply_cmds_mono_cm Hprefix Hrsm Happly) as Hcmrp. pose proof (lookup_weaken _ _ _ _ Hcmrpts Hcmrp) as Hcmts. rewrite Hcm lookup_omap_Some in Hcmts. - destruct Hcmts as (st & Hstcmted & Hst). - destruct st; [done | | done]. - by iDestruct (big_sepM_lookup with "Hsafestm") as "Hcmted"; first apply Hst. + destruct Hcmts as (status & Hstcmted & Hstatus). + destruct status; [done | | done]. + by iDestruct (big_sepM_lookup with "Hsafestm") as "Hcmted"; first apply Hstatus. } iMod ("HinvC" with "HinvO") as "_". by iFrame "∗ # %". @@ -133,9 +917,9 @@ Section replica. pose proof (apply_cmds_mono_cm Hprefix Hrsm Happly) as Hcmrp. pose proof (lookup_weaken _ _ _ _ Hcmrpts Hcmrp) as Hcmts. rewrite Hcm lookup_omap_Some in Hcmts. - destruct Hcmts as (st & Hstabted & Hst). - destruct st; [done | done |]. - by iDestruct (big_sepM_lookup with "Hsafestm") as "Habted"; first apply Hst. + destruct Hcmts as (status & Hstabted & Hstatus). + destruct status; [done | done |]. + by iDestruct (big_sepM_lookup with "Hsafestm") as "Habted"; first apply Hstatus. } iMod ("HinvC" with "HinvO") as "_". by iFrame "∗ # %". @@ -208,7 +992,7 @@ Section replica. (*@ return tulip.REPLICA_OK @*) (*@ } @*) (*@ @*) - iNamed "Hrp". iNamed "Hcpm". + do 2 iNamed "Hrp". iNamed "Hcpm". iDestruct (big_sepM2_dom with "Hprepm") as %Hdomprepm. wp_loadField. wp_apply (wp_MapGet with "HprepmS"). @@ -297,6 +1081,7 @@ Section replica. iApply (big_sepS_insert_2 ts with "Hvd Hrpvds"). } iClear "Hrpvds". + iDestruct (safe_txn_pwrs_impl_valid_wrs with "Hsafepwrs") as %Hvw. iFrame "∗ # %". iModIntro. iPureIntro. simpl. @@ -305,7 +1090,17 @@ Section replica. { rewrite 2!kmap_insert. f_equal; [word | done]. } split; first done. rewrite merge_clog_ilog_snoc_ilog; last done. - by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. + split. + { by apply map_Forall_insert_2. } + split. + { rewrite Forall_forall. + intros [n c] Hilog. simpl. + apply elem_of_app in Hilog as [Hilog | Hnewc]. + { rewrite Forall_forall in Hvicmds. by specialize (Hvicmds _ Hilog). } + rewrite elem_of_list_singleton in Hnewc. + by inv Hnewc. + } + { by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. } Qed. Definition try_accept_outcome γ gid rid ts rank pdec res : iProp Σ := @@ -370,7 +1165,7 @@ Section replica. (*@ return tulip.REPLICA_STALE_COORDINATOR @*) (*@ } @*) (*@ @*) - iNamed "Hrp". + do 2 iNamed "Hrp". wp_apply (wp_Replica__lowestRank with "Hpsmrkm"). iIntros (rankl ok) "[Hpsmrkm %Hok]". wp_pures. @@ -408,7 +1203,7 @@ Section replica. iMod (replica_inv_accept ts rank dec with "[Hgpsl] Hclog Hilog Hrp") as "(Hclog & Hilog & Hrp & #Hacc)". { apply Hexec. } - { simpl. + { rewrite /accept_requirement. destruct ok; rewrite Hok; last done. apply Classical_Prop.not_and_or in Hcase. destruct Hcase as [? | Hge]; first done. @@ -436,7 +1231,15 @@ Section replica. { by rewrite 2!dom_insert_L Hdompsmrkm. } split; first done. rewrite merge_clog_ilog_snoc_ilog; last done. - by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. + split. + { rewrite Forall_forall. + intros [n c] Hilog. simpl. + apply elem_of_app in Hilog as [Hilog | Hnewc]. + { rewrite Forall_forall in Hvicmds. by specialize (Hvicmds _ Hilog). } + rewrite elem_of_list_singleton in Hnewc. + by inv Hnewc. + } + { by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. } Qed. Theorem wp_Replica__logFastPrepare (rp : loc) (ts : u64) (pwrs : Slice.t) (ptgs : Slice.t) : @@ -511,7 +1314,7 @@ Section replica. (*@ return tulip.REPLICA_OK @*) (*@ } @*) (*@ @*) - iNamed "Hrp". + do 2 iNamed "Hrp". wp_apply (wp_Replica__lastProposal with "Hpsmrkm"). iIntros (rank dec ok) "[Hpsmrkm %Hok]". wp_pures. @@ -593,7 +1396,7 @@ Section replica. iMod (replica_inv_accept ts O false with "[] Hclog Hilog Hrp") as "(Hclog & Hilog & Hrp & #Hacc)". { apply Hexec. } - { simpl. + { rewrite /accept_requirement. destruct (rkm !! ts) as [r |] eqn:Hr; last done. apply elem_of_dom_2 in Hr. by rewrite -not_elem_of_dom Hdompsmrkm in Hok. @@ -618,7 +1421,15 @@ Section replica. { by rewrite 2!dom_insert_L Hdompsmrkm. } split; first done. rewrite merge_clog_ilog_snoc_ilog; last done. - by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. + split. + { rewrite Forall_forall. + intros [n c] Hilog. simpl. + apply elem_of_app in Hilog as [Hilog | Hnewc]. + { rewrite Forall_forall in Hvicmds. by specialize (Hvicmds _ Hilog). } + rewrite elem_of_list_singleton in Hnewc. + by inv Hnewc. + } + { by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. } } iDestruct "Hptsmsptsm" as "(Hptsmsptsm & %Hvptsm & %Hvsptsm)". @@ -662,7 +1473,7 @@ Section replica. { rewrite merge_clog_ilog_snoc_ilog; last done. by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. } - { simpl. + { rewrite /accept_requirement. destruct (rkm !! ts) as [r |] eqn:Hr; last done. apply elem_of_dom_2 in Hr. by rewrite -not_elem_of_dom Hdompsmrkm in Hok. @@ -691,6 +1502,7 @@ Section replica. iFrame "Hvd Hacc". } iClear "Hfpw". + iDestruct (safe_txn_pwrs_impl_valid_wrs with "Hsafepwrs") as %Hvw. iFrame "∗ # %". iPureIntro. simpl. exists (<[ts := ∅]> ptgsm). @@ -701,7 +1513,21 @@ Section replica. split; first done. do 2 (rewrite merge_clog_ilog_snoc_ilog; last done). rewrite /execute_cmds foldl_snoc execute_cmds_unfold. - by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. + split. + { by apply map_Forall_insert_2. } + split. + { rewrite Forall_forall. + intros [n c] Hilog. simpl. + apply elem_of_app in Hilog as [Hilog | Hnewc]. + { apply elem_of_app in Hilog as [Hilog | Hnewc]. + { rewrite Forall_forall in Hvicmds. by specialize (Hvicmds _ Hilog). } + rewrite elem_of_list_singleton in Hnewc. + by inv Hnewc. + } + rewrite elem_of_list_singleton in Hnewc. + by inv Hnewc. + } + { by rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=. } Qed. End replica. diff --git a/src/program_proof/tulip/program/tuple/tuple.v b/src/program_proof/tulip/program/tuple/tuple.v index 084e8e662..4ecbcd412 100644 --- a/src/program_proof/tulip/program/tuple/tuple.v +++ b/src/program_proof/tulip/program/tuple/tuple.v @@ -19,29 +19,36 @@ Section program. Persistent (is_tuple tuple key α). Admitted. - Theorem wp_Tuple__AppendVersion (tuple : loc) (tid : u64) (val : string) key hist α : - (length hist ≤ uint.nat tid)%nat -> + Theorem wp_Tuple__AppendVersion (tuple : loc) (tsW : u64) (value : string) key hist γ α : + let ts := uint.nat tsW in + let hist' := last_extend ts hist ++ [Some value] in + (length hist ≤ ts)%nat -> + is_repl_hist_lb γ key hist' -∗ is_tuple tuple key α -∗ {{{ own_phys_hist_half α key hist }}} - Tuple__AppendVersion #tuple #tid #(LitString val) - {{{ RET #(); own_phys_hist_half α key (last_extend (uint.nat tid) hist ++ [Some val]) }}}. + Tuple__AppendVersion #tuple #tsW #(LitString value) + {{{ RET #(); own_phys_hist_half α key hist' }}}. Proof. Admitted. - Theorem wp_Tuple__KillVersion (tuple : loc) (tid : u64) key hist α : - (length hist ≤ uint.nat tid)%nat -> + Theorem wp_Tuple__KillVersion (tuple : loc) (tsW : u64) key hist γ α : + let ts := uint.nat tsW in + let hist' := last_extend ts hist ++ [None] in + (length hist ≤ ts)%nat -> + is_repl_hist_lb γ key hist' -∗ is_tuple tuple key α -∗ {{{ own_phys_hist_half α key hist }}} - Tuple__KillVersion #tuple #tid - {{{ RET #(); own_phys_hist_half α key (last_extend (uint.nat tid) hist ++ [None]) }}}. + Tuple__KillVersion #tuple #tsW + {{{ RET #(); own_phys_hist_half α key hist' }}}. Proof. Admitted. (* TODO *) - Theorem wp_Tuple__ReadVersion (tuple : loc) (tid : u64) key α : + Theorem wp_Tuple__ReadVersion (tuple : loc) (tsW : u64) key α : + let ts := uint.nat tsW in is_tuple tuple key α -∗ {{{ True }}} - Tuple__ReadVersion #tuple #tid + Tuple__ReadVersion #tuple #tsW {{{ (v : dbval) (ok : bool), RET (dbval_to_val v, #ok); True }}}. Proof. Admitted.