ghost state template

_CoqProject

@@ -111,6 +111,8 @@ theories/axiomatic/logrel/notation.v
 theories/axiomatic/logrel/persistent_pred.v
 theories/axiomatic/logrel/logrel.v
 theories/axiomatic/logrel/adequacy.v
+theories/axiomatic/logrel/ghost_state_lib.v
+theories/axiomatic/logrel/ghost_state.v
 
 
 

theories/axiomatic/logrel/ghost_state.v

+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import lang notation.
+From iris.base_logic.lib Require Import mono_nat.
+From semantics.axiomatic Require Import invariant_lib.
+From semantics.axiomatic.logrel Require notation syntactic logrel.
+From semantics.axiomatic Require Import ghost_state_lib.
+From semantics.axiomatic.heap_lang Require Import primitive_laws proofmode.
+From iris.prelude Require Import options.
+Set Default Proof Using "Type*".
+
+(** Update rules *)
+Check upd_return.
+Check upd_bind.
+Check upd_wp.
+
+(** Derived rules *)
+Section derived.
+  Context `{heapGS Σ}.
+  Implicit Types (P Q : iProp Σ).
+
+  Lemma upd_wand P Q :
+    (|==> P) -∗
+    (P -∗ Q) -∗
+    |==> Q.
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+
+  Lemma upd_mono P Q :
+    (P ⊢ Q) →
+    (|==> P) ⊢ |==> Q.
+  Proof.
+    (* FIXME exercise *)
+  Admitted.
+
+
+  Lemma upd_trans P :
+    (|==> |==> P) ⊢ |==> P.
+  Proof.
+    (* FIXME exercise *)
+  Admitted.
+
+
+  Lemma upd_frame P Q :
+    P -∗ (|==> Q) -∗ |==> (P ∗ Q).
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+End derived.
+
+(** ** The mono nat ghost theory *)
+Notation mono_nat_lb := mono_nat_lb_own.
+Check mono_nat_auth.
+Check mono_nat_lb.
+
+Check mono_nat_make_bound.
+Check mono_nat_use_bound.
+Check mono_nat_increase_val.
+Check mono_nat_new.
+
+(* The lb resource is persistent *)
+Check mono_nat_lb_own_persistent.
+(* Both resources are also timeless *)
+Check mono_nat_lb_own_timeless.
+Check mono_nat_auth_own_timeless.
+
+Section mono_derived.
+(** In addition to the known [heapGS] assumption, we now also need to assume that the ghost state for the theory of mono_nat has been registered with Iris, expressed through the [mono_natG] assumption.
+ *)
+  Context `{heapGS Σ} `{mono_natG Σ}.
+  Implicit Types (P Q : iProp Σ).
+
+  Lemma mono_nat_increase γ n m :
+    n ≤ m →
+    mono_nat_auth γ n -∗ |==> mono_nat_auth γ m.
+  Proof.
+    (* FIXME exercise *)
+  Admitted.
+
+  Lemma mono_nat_increase_wp γ n m e Φ :
+    n ≤ m →
+    (mono_nat_auth γ m -∗ WP e {{ Φ }}) -∗
+    (mono_nat_auth γ n -∗ WP e {{ Φ }}).
+  Proof.
+    iIntros (Hle) "He Hauth".
+    iApply upd_wp. iApply (upd_wand with "[Hauth]"); last iApply "He".
+    by iApply mono_nat_increase.
+  Qed.
+
+  Lemma mono_nat_new_wp e Φ n :
+    (∀ γ, mono_nat_auth γ n -∗ WP e {{ Φ }}) -∗ WP e {{ Φ }}.
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+End mono_derived.
+
+(** ** Updates in the IPM *)
+Section ipm.
+  Context `{heapGS Σ} `{mono_natG Σ}.
+  Implicit Types (P Q : iProp Σ).
+
+  Lemma update_ipm_1 γ n :
+    mono_nat_auth γ 0 -∗
+    |==> mono_nat_auth γ n.
+  Proof.
+    iIntros "Hauth".
+    (* [iMod] will eliminate an update modality in front of the hypothesis (using [upd_bind]) *)
+    iMod (mono_nat_increase _ _ n with "Hauth") as "Hauth"; first lia.
+    (* [iFrame] can also frame hypotheses below an update, using monotonicity *)
+    iFrame "Hauth". done.
+    Restart.
+    iIntros "Hauth".
+    iMod (mono_nat_increase with "Hauth") as "$"; [lia | done].
+  Abort.
+
+  Lemma update_ipm_2 γ n e Φ  :
+    mono_nat_auth γ 0 -∗
+    (mono_nat_auth γ n -∗ WP e {{ Φ }}) -∗
+    WP e {{ Φ }}.
+  Proof.
+    iIntros "Hauth He".
+    (* [iMod] will automatically apply [upd_wp] to eliminate updates at a WP *)
+    iMod (mono_nat_increase with "Hauth") as "Hauth"; first lia.
+    by iApply "He".
+  Abort.
+
+  Lemma update_ipm_3 n γ :
+    (|==> mono_nat_auth γ n) -∗ |==> mono_nat_auth γ (S n).
+  Proof.
+    (* the [>] intro pattern will eliminate an update when introducing an assumption *)
+    iIntros ">Hauth". by iApply mono_nat_increase_val.
+  Abort.
+End ipm.
+
+
+(** The Symbol ADT *)
+Section logrel_symbol.
+  Import logrel.notation syntactic logrel.
+  Context `{heapGS Σ} `{mono_natG Σ}.
+
+  Definition assert e := (if: e then #() else #0 #0)%E.
+
+  Definition symbolT : type := ∃: ((Unit → #0) × (#0 → Unit)).
+  Definition mk_symbol : expr :=
+    let: "c" := ref #0 in
+    pack (λ: <>, let: "x" := !"c" in "c" <- "x" + #1;; "x", λ: "y", assert ("y" ≤ !"c")).
+
+  Definition symbolN := nroot .@ "symbol".
+
+  Definition mono_nat_inv γ l : iProp Σ :=
+    ∃ n : nat, l ↦ #n ∗ mono_nat_auth γ n.
+  Definition mono_natT γ : semtypeO :=
+    mk_semtype (λ v, ∃ (n : nat), ⌜v = #n⌝ ∗ mono_nat_lb_own γ n)%I.
+
+  Lemma mk_symbol_semtyped :
+    TY 0; ∅ ⊨ mk_symbol : symbolT.
+  Proof using Type*.
+    iIntros (δ γ) "#Hctx".
+    iPoseProof (context_interp_dom_eq with "Hctx") as "%Hdom".
+    rewrite dom_empty_L in Hdom. symmetry in Hdom. apply dom_empty_iff_L in Hdom.
+    subst γ. rewrite subst_map_empty. unfold mk_symbol. simpl.
+    wp_alloc l as "Hl". wp_pures.
+    (* We allocate the ghost state + invariant *)
+    iMod (mono_nat_own_alloc 0) as "(%γ & Hauth & _)".
+    iApply (inv_alloc symbolN (mono_nat_inv γ l) with "[Hauth Hl]").
+    { unfold mono_nat_inv. eauto with iFrame. }
+    iIntros "#HInv".
+    iApply wp_value.
+    iExists _. iSplit; first done.
+    iExists (mono_natT γ), _, _. iSplit; first done. iSplit.
+    - (* mkSym *)
+      iIntros (w) "!> ->".
+      wp_pures. iApply (inv_open with "HInv"); first set_solver.
+      iIntros "(%n & >Hl & Hauth)".
+      wp_load. wp_store.
+      iPoseProof (mono_nat_make_bound with "Hauth") as "#Hbound".
+      iMod (mono_nat_increase _ _ (n + 1) with "Hauth") as "Hauth"; first lia.
+      iApply wp_value. simpl. iSplitL.
+      + unfold mono_nat_inv. iNext. iExists (n + 1). iFrame.
+        replace (Z.of_nat (n +1)%nat) with (n + 1)%Z by lia; done.
+      + eauto with iFrame.
+    - (* get *)
+      simpl. iIntros (w) "!> (%n & -> & Hlb)". wp_pures.
+      iApply (inv_open with "HInv"); first set_solver.
+      iIntros "(%m & >Hl & Hauth)".
+      wp_load.
+      iPoseProof (mono_nat_use_bound with "Hauth Hlb") as "%Hleq".
+      wp_pures.  rewrite bool_decide_eq_true_2; last lia.
+      wp_pures. iApply wp_value. unfold mono_nat_inv. eauto with iFrame.
+  Qed.
+End logrel_symbol.
+
+
+(** Exercise: Oneshot *)
+Section logrel_oneshot.
+  Import logrel.notation syntactic logrel.
+  Context `{heapGS Σ} `{oneshotG Σ nat}.
+
+
+  Check os_pending_alloc.
+  Check os_pending_shoot.
+  Check os_shot_persistent.
+  Check os_pending_shot_False.
+  Check os_pending_pending_False.
+  Check os_shot_agree.
+  Check os_shot_timeless.
+  Check os_pending_timeless.
+
+  Definition code : expr :=
+    let: "x" := ref #42 in
+    λ: "f", "x" <- #1337;;
+            "f" #();;
+            assert (!"x" = #1337).
+
+  Definition codeN := nroot .@ "oneshot".
+
+  Lemma code_safe :
+    TY 0; ∅ ⊨ code : ((TUnit → TUnit) → TUnit).
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+
+End logrel_oneshot.
+
+(** Exercise: Agreement *)
+Section logrel_ag.
+  Import logrel.notation syntactic logrel.
+  Context `{heapGS Σ} `{halvesG Σ Z}.
+
+  Check ghalves_alloc.
+  Check ghalves_agree.
+  Check ghalves_update.
+  Check ghalf_timeless.
+
+  Definition rec_code : expr :=
+    λ: "f",
+    let: "l" := ref #0 in
+    (rec: "loop" <> :=
+        let: "x" := !"l" in
+        if: "f" (λ: <>, !"l")
+        then
+          assert (!"l" = "x");;
+          "l" <- "x" + #1;;
+          "loop" #()
+        else !"l")
+      #().
+
+  Lemma rec_code_safe :
+    TY 0 ; ∅ ⊨ rec_code : (((TUnit → TInt) → TBool) → TInt).
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+End logrel_ag.
+
+(** Exercise: Red/blue *)
+
+Section logrel_redblue.
+  Import logrel.notation syntactic logrel.
+  Inductive colour := red | blue.
+
+  Context `{heapGS Σ} `{agmapG Σ nat colour}.
+
+  Check agmap_auth_alloc_empty.
+  Check agmap_auth_insert.
+  Check agmap_auth_lookup.
+  Check agmap_elem_agree.
+  Check agmap_elem_persistent.
+  Check agmap_elem_timeless.
+  Check agmap_auth_timeless.
+
+  Definition mkColourGen : expr :=
+    let: "c" := ref #0 in
+    (λ: <>, let: "red" := !"c" in "c" <- #1 + "red";; "red",
+     λ: <>, let: "blue" := !"c" in "c" <- #1 + "blue";; "blue",
+     λ: "red" "blue", assert ("red" ≠ "blue")).
+
+  Lemma mkColourGen_safe :
+    TY 0; ∅ ⊨ mkColourGen : (∃: ∃: ((TUnit → #0) × (TUnit → #1)) × (#0 → #1 → TUnit)).
+  Proof.
+    (* FIXME exercise *)
+  Admitted.
+End logrel_redblue.

theories/axiomatic/logrel/ghost_state_lib.v

+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import lang notation.
+From iris.base_logic.lib Require Import mono_nat ghost_var ghost_map.
+From semantics.axiomatic Require Import invariant_lib.
+From semantics.axiomatic.heap_lang Require Import primitive_laws proofmode.
+From iris.algebra Require Import csum excl agree.
+From iris.prelude Require Import options.
+
+Section updates.
+  Context `{heapGS Σ}.
+
+  Implicit Types (P Q : iProp Σ).
+
+  Lemma upd_return P :
+    P -∗ |==> P.
+  Proof.
+    by iIntros "$".
+  Qed.
+
+  Lemma upd_bind P Q :
+    (|==> P) -∗
+    (P -∗ |==> Q) -∗
+    |==> Q.
+  Proof.
+    iIntros ">HP HQ". by iApply "HQ".
+  Qed.
+
+  Lemma upd_wp e Φ :
+    (|==> WP e {{ Φ }}) -∗
+    WP e {{ Φ }}.
+  Proof.
+    iIntros ">$".
+  Qed.
+End updates.
+
+
+(** Some ghost theories are below *)
+
+(** MonoNat *)
+Section mononat.
+  Context `{heapGS Σ} `{mono_natG Σ}.
+
+  Definition mono_nat_auth γ n := mono_nat_auth_own γ 1%Qp n.
+  Notation mono_nat_lb := mono_nat_lb_own.
+
+  Lemma mono_nat_make_bound γ n :
+    mono_nat_auth γ n -∗ mono_nat_lb γ n.
+  Proof.
+    iApply mono_nat_lb_own_get.
+  Qed.
+
+  Lemma mono_nat_use_bound γ n m :
+    mono_nat_auth γ n -∗ mono_nat_lb γ m -∗ ⌜n ≥ m⌝.
+  Proof.
+    iIntros "Hauth Hlb". iPoseProof (mono_nat_lb_own_valid with "Hauth Hlb") as "(_ & $)".
+  Qed.
+
+  Lemma mono_nat_increase_val γ n :
+    mono_nat_auth γ n -∗ |==> mono_nat_auth γ (S n).
+  Proof.
+    iIntros "Hauth".
+    iMod (mono_nat_own_update with "Hauth") as "($ & _)"; eauto.
+  Qed.
+
+  Lemma mono_nat_new n :
+    ⊢ |==> ∃ γ, mono_nat_auth γ n.
+  Proof.
+    iMod (mono_nat_own_alloc n) as "(%γ & ? & _)"; eauto with iFrame.
+  Qed.
+End mononat.
+
+(** Half algebra: provides two halves *)
+Class halvesG Σ (A : Type) := HalvesG { halvesG_ghost_varG :> ghost_varG Σ A; }.
+Definition halvesΣ A : gFunctors := ghost_varΣ A.
+Global Instance subG_halvesΣ Σ A : subG (halvesΣ A) Σ → halvesG Σ A.
+Proof. solve_inG. Qed.
+Section half.
+  Context {A : Type}.
+  Context `{halvesG Σ A}.
+
+  Definition ghalf_def γ (a : A) := ghost_var γ (1/2)%Qp a.
+  Definition ghalf_aux : seal (@ghalf_def). Proof. by eexists. Qed.
+  Definition ghalf := ghalf_aux.(unseal).
+  Definition ghalf_eq : @ghalf = @ghalf_def := ghalf_aux.(seal_eq).
+
+  Lemma ghalves_alloc a :
+    ⊢ |==> ∃ γ, ghalf γ a ∗ ghalf γ a.
+  Proof.
+    iMod (ghost_var_alloc a) as "(%γ & H1 & H2)".
+    rewrite ghalf_eq; eauto with iFrame.
+  Qed.
+
+  Lemma ghalves_agree γ a b :
+    ghalf γ a -∗ ghalf γ b -∗ ⌜a = b⌝.
+  Proof.
+    rewrite !ghalf_eq. iApply ghost_var_agree.
+  Qed.
+
+  Lemma ghalves_update γ a b c :
+    ghalf γ a -∗ ghalf γ b -∗ |==> ghalf γ c ∗ ghalf γ c.
+  Proof.
+    rewrite !ghalf_eq /ghalf_def.
+    iIntros "H1 H2". iDestruct (ghost_var_agree with "H1 H2") as %->.
+    by iMod (ghost_var_update c with "[$H1 $H2]") as "[$ $]".
+  Qed.
+
+  Global Instance ghalf_timeless γ a : Timeless (ghalf γ a).
+  Proof. rewrite ghalf_eq. apply _. Qed.
+End half.
+
+Notation "'left'" := (ghalf) (only parsing).
+Notation "'right'" := (ghalf) (only parsing).
+
+(** One shot *)
+Class oneshotG Σ (A : Type) :=
+  OneShotG { oneshotG_inG :> inG Σ (csumR (exclR unitO) (agreeR (leibnizO A))); }.
+Definition oneshotΣ A : gFunctors := #[ GFunctor (csumR (exclR unitO) (agreeR (leibnizO A))) ].
+Global Instance subG_oneshotΣ Σ A : subG (oneshotΣ A) Σ → oneshotG Σ A.
+Proof. solve_inG. Qed.
+Section oneshot.
+  Context {A : Type}.
+  Context `{oneshotG Σ A}.
+
+  Definition os_pending_def γ := own γ (Cinl (Excl ())).
+  Definition os_pending_aux : seal (@os_pending_def). Proof. by eexists. Qed.
+  Definition os_pending := os_pending_aux.(unseal).
+  Definition os_pending_eq : @os_pending = @os_pending_def := os_pending_aux.(seal_eq).
+
+
+  Definition os_shot_def γ (a : A) := own γ (Cinr (to_agree (a : leibnizO A))).
+  Definition os_shot_aux : seal (@os_shot_def). Proof. by eexists. Qed.
+  Definition os_shot := os_shot_aux.(unseal).
+  Definition os_shot_eq : @os_shot = @os_shot_def := os_shot_aux.(seal_eq).
+
+  Lemma os_pending_alloc :
+    ⊢ |==> ∃ γ, os_pending γ.
+  Proof.
+    rewrite os_pending_eq. iApply own_alloc. done.
+  Qed.
+
+  Lemma os_pending_shoot γ a :
+    os_pending γ -∗ |==> os_shot γ a.
+  Proof.
+    rewrite os_pending_eq os_shot_eq.
+    apply own_update.
+    apply cmra_update_exclusive.
+    done.
+  Qed.
+
+  Global Instance os_shot_persistent γ a : Persistent (os_shot γ a).
+  Proof. rewrite os_shot_eq. apply _. Qed.
+
+  Lemma os_pending_shot_False γ a :
+    os_pending γ -∗ os_shot γ a -∗ False.
+  Proof.
+    iIntros "H1 H2". rewrite os_pending_eq os_shot_eq.
+    iDestruct (own_valid_2 with "H1 H2") as %Hv.
+    done.
+  Qed.
+
+  Lemma os_pending_pending_False γ :
+    os_pending γ -∗ os_pending γ -∗ False.
+  Proof.
+    iIntros "H1 H2". rewrite os_pending_eq.
+    iDestruct (own_valid_2 with "H1 H2") as %Hv.
+    done.
+  Qed.
+
+  Lemma os_shot_agree γ a b :
+    os_shot γ a -∗ os_shot γ b -∗ ⌜a = b⌝.
+  Proof.
+    iIntros "H1 H2". rewrite os_shot_eq.
+    iDestruct (own_valid_2 with "H1 H2") as %Hv.
+    iPureIntro. by apply to_agree_op_inv_L in Hv.
+  Qed.
+
+  Global Instance os_shot_timeless γ a : Timeless (os_shot γ a).
+  Proof. rewrite os_shot_eq. apply _. Qed.
+  Global Instance os_pending_timeless γ : Timeless (os_pending γ).
+  Proof. rewrite os_pending_eq. apply _. Qed.
+End oneshot.
+
+(** Agreement maps *)
+Class agmapG Σ (A B : Type) `{Countable A} :=
+  AgMapG { agmapG_inG :> ghost_mapG Σ A B; }.
+Definition agmapΣ A B `{Countable A} : gFunctors := ghost_mapΣ A B.
+Global Instance subG_agmapΣ Σ A B `{Countable A} : subG (agmapΣ A B) Σ → agmapG Σ A B.
+Proof. solve_inG. Qed.
+Section oneshot.
+  Context {A B : Type} `{Countable A}.
+  Context `{agmapG Σ A}.
+
+  Definition agmap_auth_def γ M := ghost_map_auth γ 1 M.
+  Definition agmap_auth_aux : seal (@agmap_auth_def). Proof. by eexists. Qed.
+  Definition agmap_auth := agmap_auth_aux.(unseal).
+  Definition agmap_auth_eq : @agmap_auth = @agmap_auth_def := agmap_auth_aux.(seal_eq).
+
+  Definition agmap_elem_def γ a b := ghost_map_elem γ a DfracDiscarded b.
+  Definition agmap_elem_aux : seal (@agmap_elem_def). Proof. by eexists. Qed.
+  Definition agmap_elem := agmap_elem_aux.(unseal).
+  Definition agmap_elem_eq : @agmap_elem = @agmap_elem_def := agmap_elem_aux.(seal_eq).
+
+  Lemma agmap_auth_alloc_empty :
+    ⊢ |==> ∃ γ, agmap_auth γ ∅.
+  Proof.
+    rewrite agmap_auth_eq. iApply ghost_map_alloc_empty.
+  Qed.
+
+  Lemma agmap_auth_insert {γ M} a b :
+    M !! a = None →
+    agmap_auth γ M -∗ |==>
+    agmap_auth γ (<[a := b]> M) ∗ agmap_elem γ a b.
+  Proof.
+    rewrite agmap_auth_eq agmap_elem_eq.
+    iIntros (?) "Hauth".
+    iMod (ghost_map_insert a b with "Hauth") as "($ & He)"; first done.
+    iApply (ghost_map_elem_persist with "He").
+  Qed.
+
+  Lemma agmap_auth_lookup {γ M} a b :
+    agmap_auth γ M -∗ agmap_elem γ a b -∗ ⌜M !! a = Some b⌝.
+  Proof.
+    rewrite agmap_auth_eq agmap_elem_eq.
+    iApply ghost_map_lookup.
+  Qed.
+
+  Lemma agmap_elem_agree γ k a b :
+    agmap_elem γ k a -∗ agmap_elem γ k b -∗ ⌜a = b⌝.
+  Proof.
+    rewrite agmap_elem_eq. iApply ghost_map_elem_agree.
+  Qed.
+
+  Global Instance agmap_elem_persistent γ a b : Persistent (agmap_elem γ a b).
+  Proof. rewrite agmap_elem_eq. apply _. Qed.
+  Global Instance agmap_elem_timeless γ a b : Timeless (agmap_elem γ a b).
+  Proof. rewrite agmap_elem_eq. apply _. Qed.
+  Global Instance agmap_auth_timeless γ M : Timeless (agmap_auth γ M).
+  Proof. rewrite agmap_auth_eq. apply _. Qed.
+End oneshot.