Skip to content

Instantly share code, notes, and snippets.

@JoJoDeveloping
Last active February 2, 2022 21:34
Show Gist options
  • Save JoJoDeveloping/aa68cda6d9bc228880eb2028d31d0d65 to your computer and use it in GitHub Desktop.
Save JoJoDeveloping/aa68cda6d9bc228880eb2028d31d0d65 to your computer and use it in GitHub Desktop.
Unique generator ghost state
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment