Unique generator ghost state

generated.v

From iris.base_logic Require Import invariants.
From iris.base_logic.lib Require Import mono_nat.
From iris.heap_lang Require Import lang primitive_laws notation.
From iris.prelude Require Import options.
From iris.proofmode Require Import tactics.
(* You might need to uncomment resource_algebras in your _CoqMakefile *)
From semantics.axiomatic Require Import invariant_lib ghost_state_lib hoare_lib ra_lib ipm resource_algebras.
From semantics.axiomatic.heap_lang Require Import adequacy proofmode primitive_laws.
From semantics.axiomatic.program_logic Require Import notation.


Set Default Proof Using "Type*".

Section Generated.
  Context (A : Type).
  Context {ED : EqDecision A}.
  Context {C : Countable A}.
  
  Inductive generated := Error | OK (p : option (gset A) * gset A).

  Instance generated_valid_instance : Valid generated := λ x, match x with
       Error => False
     | OK (Some g,l) => subseteq l g
     | OK (None,l) => True end.
  Instance generated_unit_instance : Unit generated := OK (None, ∅).
  Instance generated_pcore_instance : PCore generated := λ x, Some (OK (None, ∅)).

  Instance generated_op_instance : Op generated :=
    λ n m, match (n,m) with
      | (Error,_) => Error
      | (_,Error) => Error
      | (OK (Some _,_), OK (Some _,_)) => Error
      | (OK (Some gl,ll), OK  (None,rr)) =>
        if gset_eq_dec (ll ∩ rr) ∅ then
          OK (Some gl, ll ∪ rr)
        else Error
      | (OK (None,ll), OK  (gr,rr)) =>
        if gset_eq_dec (ll ∩ rr) ∅ then
          OK (gr, ll ∪ rr)
        else Error end.

  Lemma generated_op (x y : generated) :
    x ⋅ y = generated_op_instance x y.
  Proof.
    reflexivity.
  Qed.

  Lemma generated_op_1 g1 g2 :
    OK (Some g1, ∅) ⋅ OK (None, g2) = OK (Some g1, g2).
  Proof.
    unfold op, generated_op_instance.
    destruct gset_eq_dec; [ do 2 f_equal |]; set_solver.
  Qed.

  Lemma generated_op_2 g1 g2 g3:
    g2 ∩ g3 = ∅ ->
    OK (Some g1, g2) ⋅ OK (None, g3) = OK (Some g1, g2 ∪ g3).
  Proof.
    unfold op, generated_op_instance.
    destruct gset_eq_dec; [ do 2 f_equal | set_solver ].
  Qed.

  Lemma generated_lra_mixin :
    LRAMixin generated.
  Proof.
    constructor; eauto.
    - intros [|[[x1|] x2]] [|[[y1|] y2]] [|[[z1|] z2]].
      all: repeat rewrite generated_op; cbn; try done.
      all: repeat destruct gset_eq_dec; try done.
      all: try (do 2 f_equal; set_solver).
    - intros [|[[x1|] x2]] [|[[y1|] y2]]; eauto.
      all: repeat rewrite generated_op; cbn; repeat destruct gset_eq_dec.
      all: f_equal; f_equal; set_solver.
    - intros [|[[a1|] a2]] cx [= <-]; eauto.
      all: repeat rewrite generated_op; cbn.
      all: destruct gset_eq_dec; [ do 2 f_equal | ]; set_solver.  
    - intros [|[[a1|] a2]] y cx [x ->] [= <-].
      all: eexists; split; first reflexivity.
      all: exists (OK (None, ∅)); cbn.
      all: destruct gset_eq_dec; [ do 2 f_equal | ]; set_solver.
    - intros [|[[a1|] a2]] [|[[b1|] b2]]; eauto.
      all: repeat rewrite generated_op; cbn; try done.
      destruct gset_eq_dec; cbn; set_solver.
  Qed.
  Canonical Structure generatedR : lra := Lra generated generated_lra_mixin.

  Lemma generated_ulra_mixin :
    ULRAMixin generated.
  Proof.
    constructor; try done.
    intros [|[[a1|] a2]]; cbn; eauto.
    all: destruct gset_eq_dec; try set_solver.
    all: do 2 f_equal; set_solver.
  Qed.
  Canonical Structure generatedUR : ulra := Ulra generated generated_lra_mixin generated_ulra_mixin.
End Generated.

Canonical Structure generatedO A ED C := leibnizO (@generated A ED C).
Canonical Structure generatedCR A ED C : cmra := cmra_of_lra (@generated A ED C) (@generated_lra_mixin A ED C).

(**
  We need this to register the ghost state we setup with Iris.
*)
Class generatedG Σ A ED C := OneShotG {
  oneshotG_inG :> inG Σ (@generatedCR A ED C);
}.

Definition generatedΣ A ED C : gFunctors :=
  #[ GFunctor ((@generatedCR A ED C)) ].

Global Instance subG_generatedΣ Σ A ED C :
  subG (generatedΣ A ED C) Σ → generatedG Σ A ED C.
Proof.
  solve_inG.
Qed.

Section generated.
  Context (A : Type).
  Context {ED : EqDecision A}.
  Context {C : Countable A}.
  (**
    We now assume that the generated ghost state we
    have just defined is registered with Iris.
  *)
  Context `{@generatedG Σ A ED C}.

  Definition generated_auth γ g :=
    (own γ (OK A (Some g, ∅))).
  
  Definition generated_gen γ v :=
    (own γ (OK A (None, singleton v))).

  Lemma generated_use_gen γ v1 v2 :
    generated_gen γ v1 -∗ generated_gen γ v2 -∗ ⌜v1 ≠ v2⌝.
  Proof.
    iIntros "Hfrag1 Hfrag2".
    iDestruct (own_valid_2 with "Hfrag1 Hfrag2") as %Hv.
    iPureIntro. do 8 red in Hv.
    destruct gset_eq_dec; set_solver.
  Qed.

  Lemma generate_update γ g v :
    ⌜v ∉ g⌝ -∗ generated_auth γ g -∗ |==> generated_auth γ (g ∪ {[v]}) ∗ generated_gen γ v.
  Proof.
    unfold generated_auth, generated_gen.
    iIntros "%H1 H2". rewrite <- own_op.
    iApply (own_lra_update with "H2").
    intros [[|[[c1|] c2]]|] Hc; cbn in *; try done.
    + rewrite generated_op_1 in Hc. do 3 red in Hc.
      rewrite generated_op_1 generated_op_2; set_solver.
    + rewrite generated_op_1. do 3 red. set_solver.
  Qed.

  Lemma generate_auth γ g v : 
    ⊢ generated_auth γ g -∗ generated_gen γ v -∗ ⌜v ∈ g⌝.
  Proof.
    iIntros "H1 H2".
    iDestruct (own_valid_2 with "H1 H2") as %Hv.
    iPureIntro.
    rewrite generated_op_1 in Hv. do 4 red in Hv.
    set_solver.
  Qed.

  Lemma generate_new g :
    ⊢ |==> ∃ γ, generated_auth γ g.
  Proof.
    iApply own_alloc. do 4 red.
    set_solver.
  Qed.
End generated.


Section generated_derived.
  (* The two placeholders let Coq infer EqDecision and Countable for val. Works for many other "canonical" types as well *)
  Context `{heapGS Σ} `{@generatedG Σ val _ _}. 


  Definition mk_generator : expr :=
      let: "l" := ref #0 in
      λ: <>,
        let: "x" := !"l" in
        "l" <- "x" + #1;; "x".


  Definition generator_inv (γ : gname) (l : loc) : iProp Σ := 
   ∃ (c:nat) (g:gset val), l ↦ #c ∗ generated_auth val γ g ∗ ⌜forall (n:nat), (#n) ∈ g -> n < c⌝.

  Definition generatorN := nroot .@ "generator".

  Lemma generator_correct :
    ⊢ □ (WP mk_generator {{ v, ∃ γ, □ (WP of_val v #() {{ w, generated_gen val γ w }}) }}).
  Proof.
  iIntros "!>". unfold mk_generator.
  wp_pures. wp_alloc l as "Hl".
  iPoseProof (generate_new val ∅) as "> (%γ & Hγ)".
  iApply (invariant_lib.inv_alloc generatorN (generator_inv γ l) with "[Hγ Hl]").
  1: { iExists 0. iExists ∅. iFrame. iPureIntro. intros n. set_solver. } 
  iIntros "#Hinv".
  wp_pures. wp_apply wp_value.
  iExists γ. iIntros "!>".
  iApply (inv_open with "Hinv"); first set_solver.
  iIntros "Hinv'". wp_pures. iDestruct "Hinv'" as "(%c & %g & Hl & Hγ & %Hcg)".
  wp_pures. wp_load. wp_pures. wp_store.
  iPoseProof (generate_update val γ g #c with "[] Hγ") as ">[Hγ Hgen]".
  1: { iPureIntro. intros Hc. pose proof (Hcg c) as HL. specialize (HL Hc). lia. }
  wp_apply wp_value. iFrame.
  iModIntro. iExists (c+1). iExists ((g ∪ {[#c]})).
  rewrite Nat2Z.inj_add. iFrame. iPureIntro. intros n. rewrite elem_of_union. intros [Hl|Hr].
  - pose proof (Hcg n) as Hll. specialize (Hll Hl). lia.
  - assert (#n = #c) as Heq by set_solver.
    assert (Z.of_nat n = Z.of_nat c)%Z as Heq2 by congruence. lia.
  Qed.

End generated_derived.