From 16bdc4e0d2f72337284f905daf0e5b3062aeb273 Mon Sep 17 00:00:00 2001 From: Joseph Tassarotti Date: Fri, 29 Nov 2024 17:25:14 -0500 Subject: [PATCH] Start using own_crash_ex for a paxos ghost resource. --- src/program_logic/own_crash_inv.v | 2 +- src/program_proof/tulip/paxos/base.v | 3 +++ src/program_proof/tulip/paxos/program/mk_paxos.v | 5 ++++- src/program_proof/tulip/paxos/program/paxos_accept.v | 4 ++++ src/program_proof/tulip/paxos/program/paxos_ascend.v | 2 ++ src/program_proof/tulip/paxos/program/paxos_stepdown.v | 2 ++ src/program_proof/tulip/paxos/program/paxos_submit.v | 2 ++ src/program_proof/tulip/paxos/program/repr.v | 5 ++++- src/program_proof/tulip/paxos/res.v | 4 ++++ 9 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/program_logic/own_crash_inv.v b/src/program_logic/own_crash_inv.v index 755280447..11dc33ed7 100644 --- a/src/program_logic/own_crash_inv.v +++ b/src/program_logic/own_crash_inv.v @@ -1,5 +1,5 @@ From iris.proofmode Require Import base tactics classes. -From Perennial.base_logic Require Export invariants. +From Perennial.base_logic Require Import invariants. From Perennial.program_logic Require Import invariants_mutable staged_invariant_alt. From Perennial.base_logic.lib Require Import wsat. Set Default Proof Using "Type". diff --git a/src/program_proof/tulip/paxos/base.v b/src/program_proof/tulip/paxos/base.v index 9ff973543..0f854c9ae 100644 --- a/src/program_proof/tulip/paxos/base.v +++ b/src/program_proof/tulip/paxos/base.v @@ -368,4 +368,7 @@ Qed. Class paxos_ghostG (Σ : gFunctors). +Instance stagedG_paxos_ghostG Σ : paxos_ghostG Σ → stagedG Σ. +Proof. Admitted. + Record paxos_names := {}. diff --git a/src/program_proof/tulip/paxos/program/mk_paxos.v b/src/program_proof/tulip/paxos/program/mk_paxos.v index 1983bd91c..db2e420c8 100644 --- a/src/program_proof/tulip/paxos/program/mk_paxos.v +++ b/src/program_proof/tulip/paxos/program/mk_paxos.v @@ -17,7 +17,7 @@ Section mk_paxos. know_paxos_network_inv γ addrm -∗ {{{ own_slice logP stringT (DfracOwn 1) log ∗ own_map addrmP (DfracOwn 1) addrm ∗ - own_current_term_half γ nidme (uint.nat termc) ∗ + own_crash_ex paxoscrashNS (own_current_term_half γ nidme) (uint.nat termc) ∗ own_ledger_term_half γ nidme (uint.nat terml) ∗ own_committed_lsn_half γ nidme (uint.nat lsnc) ∗ own_node_ledger_half γ nidme log @@ -146,6 +146,8 @@ Section mk_paxos. iDestruct (accepted_proposal_lookup with "Hacpt Hpsa") as %Hlogn. by iApply (big_sepM_lookup with "Hpsalbs"). } + iMod (own_crash_ex_open with "HtermcX") as "(>HtermcX&Hclose_termcX)". + { solve_ndisj. } iAssert (if decide (termc = terml) then True else past_nodedecs_latest_before γ nidme (uint.nat termc) (uint.nat terml) log)%I @@ -211,6 +213,7 @@ Section mk_paxos. iPureIntro. clear -Hltlog. word. } + iMod ("Hclose_termcX" with "HtermcX"). iMod ("HinvC" with "HinvO") as "_". iAssert (own_paxos px nidme nids γ ∗ own_paxos_comm px addrm γ)%I with "[-HΦ Hfree]" as "(Hpx & Hcomm)". diff --git a/src/program_proof/tulip/paxos/program/paxos_accept.v b/src/program_proof/tulip/paxos/program/paxos_accept.v index 358c8e2f4..a2dd794f6 100644 --- a/src/program_proof/tulip/paxos/program/paxos_accept.v +++ b/src/program_proof/tulip/paxos/program/paxos_accept.v @@ -103,6 +103,7 @@ Section accept. iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]". { apply Hnidme. } iNamed "Hnodefile". + iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. iApply ncfupd_mask_intro; first solve_ndisj. iIntros "Hmask". iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->. @@ -126,6 +127,7 @@ Section accept. iDestruct ("HinvfileO" with "[Hfile Hwalfile]") as "HinvfileO". { iFrame "∗ # %". } iMod "Hmask" as "_". + iMod ("Hclose_termc" with "Htermc") as "Htermc". iMod ("HinvfileC" with "HinvfileO") as "_". iMod ("HinvC" with "HinvO") as "_". iIntros "!> Hents". @@ -250,6 +252,7 @@ Section accept. iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]". { apply Hnidme. } iNamed "Hnodefile". + iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. iApply ncfupd_mask_intro; first solve_ndisj. iIntros "Hmask". iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->. @@ -266,6 +269,7 @@ Section accept. iDestruct ("HinvfileO" with "[Hfile Hwalfile]") as "HinvfileO". { iFrame "∗ # %". } iMod "Hmask" as "_". + iMod ("Hclose_termc" with "Htermc") as "Htermc". iMod ("HinvfileC" with "HinvfileO") as "_". iMod ("HinvC" with "HinvO") as "_". iIntros "!> Hents". diff --git a/src/program_proof/tulip/paxos/program/paxos_ascend.v b/src/program_proof/tulip/paxos/program/paxos_ascend.v index 1a4091fab..40f08d525 100644 --- a/src/program_proof/tulip/paxos/program/paxos_ascend.v +++ b/src/program_proof/tulip/paxos/program/paxos_ascend.v @@ -78,6 +78,7 @@ Section ascend. iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]". { apply Hnidme. } iNamed "Hnodefile". + iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. iApply ncfupd_mask_intro; first solve_ndisj. iIntros "Hmask". iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->. @@ -109,6 +110,7 @@ Section ascend. iDestruct ("HinvfileO" with "[Hfile Hwalfile]") as "HinvfileO". { iFrame "∗ # %". } iMod "Hmask" as "_". + iMod ("Hclose_termc" with "Htermc") as "Htermc". iMod ("HinvfileC" with "HinvfileO") as "_". iMod ("HinvC" with "HinvO") as "_". iIntros "!> Hents". diff --git a/src/program_proof/tulip/paxos/program/paxos_stepdown.v b/src/program_proof/tulip/paxos/program/paxos_stepdown.v index 2a19ad164..e6af73970 100644 --- a/src/program_proof/tulip/paxos/program/paxos_stepdown.v +++ b/src/program_proof/tulip/paxos/program/paxos_stepdown.v @@ -49,6 +49,7 @@ Section stepdown. iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]". { apply Hnidme. } iNamed "Hnodefile". + iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. iApply ncfupd_mask_intro; first solve_ndisj. iIntros "Hmask". iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->. @@ -63,6 +64,7 @@ Section stepdown. iDestruct ("HinvfileO" with "[Hfile Hwalfile]") as "HinvfileO". { iFrame "∗ # %". } iMod "Hmask" as "_". + iMod ("Hclose_termc" with "Htermc") as "Htermc". iMod ("HinvfileC" with "HinvfileO") as "_". iMod ("HinvC" with "HinvO") as "_". iIntros "!> _". diff --git a/src/program_proof/tulip/paxos/program/paxos_submit.v b/src/program_proof/tulip/paxos/program/paxos_submit.v index 33548b170..fe4cd3c86 100644 --- a/src/program_proof/tulip/paxos/program/paxos_submit.v +++ b/src/program_proof/tulip/paxos/program/paxos_submit.v @@ -83,6 +83,7 @@ Section submit. iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]". { apply Hnidme. } iNamed "Hnodefile". + iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. iApply ncfupd_mask_intro; first solve_ndisj. iIntros "Hmask". iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->. @@ -97,6 +98,7 @@ Section submit. iDestruct ("HinvfileO" with "[Hfile Hwalfile]") as "HinvfileO". { by iFrame "∗ # %". } iMod "Hmask" as "_". + iMod ("Hclose_termc" with "Htermc") as "Htermc". iMod ("HinvfileC" with "HinvfileO") as "_". iMod ("HinvC" with "HinvO") as "_". iIntros "!> Hents". diff --git a/src/program_proof/tulip/paxos/program/repr.v b/src/program_proof/tulip/paxos/program/repr.v index fbd724e13..0b8820d6d 100644 --- a/src/program_proof/tulip/paxos/program/repr.v +++ b/src/program_proof/tulip/paxos/program/repr.v @@ -1,4 +1,5 @@ From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_logic Require Export own_crash_inv. From Goose.github_com.mit_pdos.tulip Require Import paxos. Section repr. @@ -61,6 +62,8 @@ Section repr. (*@ // @*) (*@ conns map[uint64]grove_ffi.Connection @*) (*@ } @*) + Definition paxoscrashNS := nroot.@"paxos_crash". + Definition is_paxos_addrm (paxos : loc) (addrm : gmap u64 chan) : iProp Σ := ∃ (addrmP : loc), "#HaddrmP" ∷ readonly (paxos ↦[Paxos :: "addrm"] #addrmP) ∗ @@ -167,7 +170,7 @@ Section repr. ∃ (hb : bool) (logP : Slice.t), "HhbP" ∷ paxos ↦[Paxos :: "hb"] #hb ∗ "HtermcP" ∷ paxos ↦[Paxos :: "termc"] #termc ∗ - "Htermc" ∷ own_current_term_half γ nidme (uint.nat termc) ∗ + "Htermc" ∷ own_crash_ex paxoscrashNS (own_current_term_half γ nidme) (uint.nat termc) ∗ "HtermlP" ∷ paxos ↦[Paxos :: "terml"] #terml ∗ "Hterml" ∷ own_ledger_term_half γ nidme (uint.nat terml) ∗ "HlogP" ∷ paxos ↦[Paxos :: "log"] (to_val logP) ∗ diff --git a/src/program_proof/tulip/paxos/res.v b/src/program_proof/tulip/paxos/res.v index 345e24627..487ca61fd 100644 --- a/src/program_proof/tulip/paxos/res.v +++ b/src/program_proof/tulip/paxos/res.v @@ -364,6 +364,10 @@ Section res. (** Type class instances. *) + #[global] + Instance own_current_term_timeless γ nid t : Timeless (own_current_term_half γ nid t). + Proof. admit. Admitted. + (** Rules. *) Lemma current_term_update {γ nid t1} t2 :