Start using own_crash_ex for a paxos ghost resource.

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".

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 := {}.

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)".

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".

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".

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 "!> _".

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".

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) ∗

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 :