clutch.gen_prob_lang.spec.spec_ra
Resources required to track a gen_prob_lang spec configuration.
Generalized from prob_lang: the per-distribution tape ghost maps
(tapes / tapes_laplace / …) collapse into a single generic stape map.
From Stdlib Require Import Reals.
From iris.algebra Require Import auth excl.
From iris.base_logic.lib Require Import invariants ghost_map.
From iris.prelude Require Import options.
From iris.proofmode Require Import proofmode.
From clutch.base_logic Require Export spec_update.
From clutch.common Require Import language ectxi_language.
From clutch.gen_prob_lang Require Import lang.
Definition progUR : ucmra := optionUR (exclR exprO).
Definition cfgO : ofe := prodO exprO stateO.
From iris.algebra Require Import auth excl.
From iris.base_logic.lib Require Import invariants ghost_map.
From iris.prelude Require Import options.
From iris.proofmode Require Import proofmode.
From clutch.base_logic Require Export spec_update.
From clutch.common Require Import language ectxi_language.
From clutch.gen_prob_lang Require Import lang.
Definition progUR : ucmra := optionUR (exclR exprO).
Definition cfgO : ofe := prodO exprO stateO.
The CMRA for the spec cfg.
Class specG_prob_lang Σ := SpecGS {
#[local] specG_prob_lang_prog_inG :: inG Σ (authR progUR);
specG_prob_lang_prog_name : gname;
#[local] specG_prob_lang_heap :: ghost_mapG Σ loc val;
#[local] specG_prob_lang_tapes :: ghost_mapG Σ loc stape;
specG_prob_lang_heap_name : gname;
specG_prob_lang_tapes_name : gname;
}.
Class specGpreS Σ := SpecGPreS {
specGpreS_prog_inG :: inG Σ (authR progUR);
specGpreS_heap :: ghost_mapG Σ loc val;
specGpreS_tapes :: ghost_mapG Σ loc stape;
}.
Definition specΣ : gFunctors :=
#[ghost_mapΣ loc val;
ghost_mapΣ loc stape;
GFunctor (authUR progUR)].
#[global] Instance subG_clutchGPreS {Σ} : subG specΣ Σ → specGpreS Σ.
Proof. solve_inG. Qed.
Section resources.
Context `{!specG_prob_lang Σ}.
Definition spec_prog_auth e :=
own specG_prob_lang_prog_name (● (Excl' e : progUR)).
Definition spec_heap_auth `{specG_prob_lang Σ} :=
@ghost_map_auth _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name 1.
Definition spec_tapes_auth `{specG_prob_lang Σ} :=
@ghost_map_auth _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name 1.
Definition spec_auth (ρ : cfg) : iProp Σ :=
spec_prog_auth (ρ.1) ∗
spec_heap_auth (ρ.2.(heap)) ∗
spec_tapes_auth (ρ.2.(stapes)).
Definition spec_prog_frag (e : expr) : iProp Σ :=
own specG_prob_lang_prog_name (◯ (Excl' e : progUR)).
Definition spec_heap_frag (l : loc) v dq: iProp Σ :=
(@ghost_map_elem _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name l dq v).
Definition spec_tapes_frag (l : loc) v dq: iProp Σ :=
(@ghost_map_elem _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name l dq v).
End resources.
#[local] specG_prob_lang_prog_inG :: inG Σ (authR progUR);
specG_prob_lang_prog_name : gname;
#[local] specG_prob_lang_heap :: ghost_mapG Σ loc val;
#[local] specG_prob_lang_tapes :: ghost_mapG Σ loc stape;
specG_prob_lang_heap_name : gname;
specG_prob_lang_tapes_name : gname;
}.
Class specGpreS Σ := SpecGPreS {
specGpreS_prog_inG :: inG Σ (authR progUR);
specGpreS_heap :: ghost_mapG Σ loc val;
specGpreS_tapes :: ghost_mapG Σ loc stape;
}.
Definition specΣ : gFunctors :=
#[ghost_mapΣ loc val;
ghost_mapΣ loc stape;
GFunctor (authUR progUR)].
#[global] Instance subG_clutchGPreS {Σ} : subG specΣ Σ → specGpreS Σ.
Proof. solve_inG. Qed.
Section resources.
Context `{!specG_prob_lang Σ}.
Definition spec_prog_auth e :=
own specG_prob_lang_prog_name (● (Excl' e : progUR)).
Definition spec_heap_auth `{specG_prob_lang Σ} :=
@ghost_map_auth _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name 1.
Definition spec_tapes_auth `{specG_prob_lang Σ} :=
@ghost_map_auth _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name 1.
Definition spec_auth (ρ : cfg) : iProp Σ :=
spec_prog_auth (ρ.1) ∗
spec_heap_auth (ρ.2.(heap)) ∗
spec_tapes_auth (ρ.2.(stapes)).
Definition spec_prog_frag (e : expr) : iProp Σ :=
own specG_prob_lang_prog_name (◯ (Excl' e : progUR)).
Definition spec_heap_frag (l : loc) v dq: iProp Σ :=
(@ghost_map_elem _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name l dq v).
Definition spec_tapes_frag (l : loc) v dq: iProp Σ :=
(@ghost_map_elem _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name l dq v).
End resources.
Spec program
Spec heap
Notation "l ↦ₛ{ dq } v" := (@ghost_map_elem _ _ _ _ _ specG_prob_lang_heap specG_prob_lang_heap_name l dq v)
(at level 20, format "l ↦ₛ{ dq } v") : bi_scope.
Notation "l ↦ₛ□ v" := (l ↦ₛ{ DfracDiscarded } v)%I
(at level 20, format "l ↦ₛ□ v") : bi_scope.
Notation "l ↦ₛ{# q } v" := (l ↦ₛ{ DfracOwn q } v)%I
(at level 20, format "l ↦ₛ{# q } v") : bi_scope.
Notation "l ↦ₛ v" := (l ↦ₛ{ DfracOwn 1 } v)%I
(at level 20, format "l ↦ₛ v") : bi_scope.
(at level 20, format "l ↦ₛ{ dq } v") : bi_scope.
Notation "l ↦ₛ□ v" := (l ↦ₛ{ DfracDiscarded } v)%I
(at level 20, format "l ↦ₛ□ v") : bi_scope.
Notation "l ↦ₛ{# q } v" := (l ↦ₛ{ DfracOwn q } v)%I
(at level 20, format "l ↦ₛ{# q } v") : bi_scope.
Notation "l ↦ₛ v" := (l ↦ₛ{ DfracOwn 1 } v)%I
(at level 20, format "l ↦ₛ v") : bi_scope.
Spec tapes (one generic tape map)
Notation "l ↪ₛ{ dq } v" := (@ghost_map_elem _ _ _ _ _ specG_prob_lang_tapes specG_prob_lang_tapes_name l dq v)
(at level 20, format "l ↪ₛ{ dq } v") : bi_scope.
Notation "l ↪ₛ□ v" := (l ↪ₛ{ DfracDiscarded } v)%I
(at level 20, format "l ↪ₛ□ v") : bi_scope.
Notation "l ↪ₛ{# q } v" := (l ↪ₛ{ DfracOwn q } v)%I
(at level 20, format "l ↪ₛ{# q } v") : bi_scope.
Notation "l ↪ₛ v" := (l ↪ₛ{ DfracOwn 1 } v)%I
(at level 20, format "l ↪ₛ v") : bi_scope.
Section theory.
Context `{!specG_prob_lang Σ}.
Lemma spec_auth_prog_agree e1 σ1 e2 :
spec_auth (e1, σ1) -∗ ⤇ e2 -∗ ⌜e1 = e2⌝.
Proof.
iIntros "[Ha _] Hf".
iDestruct (own_valid_2 with "Ha Hf") as
%[Hexcl ?]%auth_both_valid_discrete.
rewrite Excl_included in Hexcl.
by apply leibniz_equiv in Hexcl.
Qed.
Lemma spec_update_prog e3 e1 σ1 e2 :
spec_auth (e1, σ1) -∗ ⤇ e2 ==∗ spec_auth (e3, σ1) ∗ ⤇ e3.
Proof.
iIntros "Ha Hf".
iDestruct (spec_auth_prog_agree with "Ha Hf") as %->.
iDestruct "Ha" as "[Ha Hb]".
iMod (own_update_2 with "Ha Hf") as "[Ha Hf]".
{ by eapply auth_update, option_local_update,
(exclusive_local_update _ (Excl e3)). }
by iFrame.
Qed.
(at level 20, format "l ↪ₛ{ dq } v") : bi_scope.
Notation "l ↪ₛ□ v" := (l ↪ₛ{ DfracDiscarded } v)%I
(at level 20, format "l ↪ₛ□ v") : bi_scope.
Notation "l ↪ₛ{# q } v" := (l ↪ₛ{ DfracOwn q } v)%I
(at level 20, format "l ↪ₛ{# q } v") : bi_scope.
Notation "l ↪ₛ v" := (l ↪ₛ{ DfracOwn 1 } v)%I
(at level 20, format "l ↪ₛ v") : bi_scope.
Section theory.
Context `{!specG_prob_lang Σ}.
Lemma spec_auth_prog_agree e1 σ1 e2 :
spec_auth (e1, σ1) -∗ ⤇ e2 -∗ ⌜e1 = e2⌝.
Proof.
iIntros "[Ha _] Hf".
iDestruct (own_valid_2 with "Ha Hf") as
%[Hexcl ?]%auth_both_valid_discrete.
rewrite Excl_included in Hexcl.
by apply leibniz_equiv in Hexcl.
Qed.
Lemma spec_update_prog e3 e1 σ1 e2 :
spec_auth (e1, σ1) -∗ ⤇ e2 ==∗ spec_auth (e3, σ1) ∗ ⤇ e3.
Proof.
iIntros "Ha Hf".
iDestruct (spec_auth_prog_agree with "Ha Hf") as %->.
iDestruct "Ha" as "[Ha Hb]".
iMod (own_update_2 with "Ha Hf") as "[Ha Hf]".
{ by eapply auth_update, option_local_update,
(exclusive_local_update _ (Excl e3)). }
by iFrame.
Qed.
Heap
Lemma spec_auth_lookup_heap e1 σ1 l v dq:
spec_auth (e1, σ1) -∗ l ↦ₛ{dq} v -∗ ⌜σ1.(heap) !! l = Some v⌝.
Proof. iIntros "(_&H&_) H'/=". iApply (ghost_map_lookup with "H H'"). Qed.
Lemma spec_auth_heap_alloc e σ v :
spec_auth (e, σ) ==∗
spec_auth (e, state_upd_heap <[ fresh_loc σ.(heap) := v ]> σ) ∗ fresh_loc σ.(heap) ↦ₛ v.
Proof.
iIntros "(? & Hheap & ?) /=".
iMod (ghost_map_insert (fresh_loc σ.(heap)) with "Hheap") as "[Hheap Hl]".
{ apply not_elem_of_dom, fresh_loc_is_fresh. }
by iFrame.
Qed.
Lemma spec_auth_update_heap w e1 σ1 l v :
spec_auth (e1, σ1) -∗ l ↦ₛ{#1} v ==∗
spec_auth (e1, state_upd_heap <[l:=w]> σ1) ∗ l ↦ₛ{#1} w.
Proof.
iIntros "(?&H&?) H' /=".
iMod (ghost_map_update with "H H'") as "?".
iModIntro. by iFrame.
Qed.
spec_auth (e1, σ1) -∗ l ↦ₛ{dq} v -∗ ⌜σ1.(heap) !! l = Some v⌝.
Proof. iIntros "(_&H&_) H'/=". iApply (ghost_map_lookup with "H H'"). Qed.
Lemma spec_auth_heap_alloc e σ v :
spec_auth (e, σ) ==∗
spec_auth (e, state_upd_heap <[ fresh_loc σ.(heap) := v ]> σ) ∗ fresh_loc σ.(heap) ↦ₛ v.
Proof.
iIntros "(? & Hheap & ?) /=".
iMod (ghost_map_insert (fresh_loc σ.(heap)) with "Hheap") as "[Hheap Hl]".
{ apply not_elem_of_dom, fresh_loc_is_fresh. }
by iFrame.
Qed.
Lemma spec_auth_update_heap w e1 σ1 l v :
spec_auth (e1, σ1) -∗ l ↦ₛ{#1} v ==∗
spec_auth (e1, state_upd_heap <[l:=w]> σ1) ∗ l ↦ₛ{#1} w.
Proof.
iIntros "(?&H&?) H' /=".
iMod (ghost_map_update with "H H'") as "?".
iModIntro. by iFrame.
Qed.
Tapes
Lemma spec_auth_lookup_tape e1 σ1 l v dq :
spec_auth (e1, σ1) -∗ l ↪ₛ{dq} v -∗ ⌜σ1.(stapes) !! l = Some v⌝.
Proof. iIntros "(_&_&H) H'/=". iApply (ghost_map_lookup with "H H'"). Qed.
Lemma spec_auth_update_tape w e1 σ1 l v :
spec_auth (e1, σ1) -∗ l ↪ₛ{#1} v ==∗
spec_auth (e1, state_upd_stapes <[l:=w]> σ1) ∗ l ↪ₛ{#1} w.
Proof.
iIntros "(?&?&H) H'/=".
iMod (ghost_map_update with "H H'") as "?".
iModIntro. by iFrame.
Qed.
Lemma spec_auth_tape_alloc e σ (t : stape) :
spec_auth (e, σ) ==∗
spec_auth (e, state_upd_stapes <[fresh_loc σ.(stapes) := t]> σ) ∗ fresh_loc σ.(stapes) ↪ₛ t.
Proof.
iIntros "(? & ? & Htapes) /=".
iMod (ghost_map_insert (fresh_loc σ.(stapes)) with "Htapes") as "[H Hl]".
{ apply not_elem_of_dom, fresh_loc_is_fresh. }
by iFrame.
Qed.
End theory.
Lemma spec_ra_init e σ `{specGpreS Σ} :
⊢ |==> ∃ _ : specG_prob_lang Σ,
spec_auth (e, σ) ∗ ⤇ e ∗
([∗ map] l ↦ v ∈ σ.(heap), l ↦ₛ v) ∗
([∗ map] α ↦ t ∈ σ.(stapes), α ↪ₛ t).
Proof.
iMod (own_alloc ((● (Excl' e)) ⋅ (◯ (Excl' e)))) as "(%γp & Hprog_auth & Hprog_frag)".
{ by apply auth_both_valid_discrete. }
iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh Hls]]".
iMod (ghost_map_alloc σ.(stapes)) as "[%γT [Ht Hαs]]".
iExists (SpecGS _ _ γp _ _ γH γT).
by iFrame.
Qed.
#[global] Instance spec_rules_spec_updateGS `{!specG_prob_lang Σ} (S : Sig) :
spec_updateGS (lang_markov (gen_lang S)) Σ.
Proof. constructor. exact spec_auth. Defined.
spec_auth (e1, σ1) -∗ l ↪ₛ{dq} v -∗ ⌜σ1.(stapes) !! l = Some v⌝.
Proof. iIntros "(_&_&H) H'/=". iApply (ghost_map_lookup with "H H'"). Qed.
Lemma spec_auth_update_tape w e1 σ1 l v :
spec_auth (e1, σ1) -∗ l ↪ₛ{#1} v ==∗
spec_auth (e1, state_upd_stapes <[l:=w]> σ1) ∗ l ↪ₛ{#1} w.
Proof.
iIntros "(?&?&H) H'/=".
iMod (ghost_map_update with "H H'") as "?".
iModIntro. by iFrame.
Qed.
Lemma spec_auth_tape_alloc e σ (t : stape) :
spec_auth (e, σ) ==∗
spec_auth (e, state_upd_stapes <[fresh_loc σ.(stapes) := t]> σ) ∗ fresh_loc σ.(stapes) ↪ₛ t.
Proof.
iIntros "(? & ? & Htapes) /=".
iMod (ghost_map_insert (fresh_loc σ.(stapes)) with "Htapes") as "[H Hl]".
{ apply not_elem_of_dom, fresh_loc_is_fresh. }
by iFrame.
Qed.
End theory.
Lemma spec_ra_init e σ `{specGpreS Σ} :
⊢ |==> ∃ _ : specG_prob_lang Σ,
spec_auth (e, σ) ∗ ⤇ e ∗
([∗ map] l ↦ v ∈ σ.(heap), l ↦ₛ v) ∗
([∗ map] α ↦ t ∈ σ.(stapes), α ↪ₛ t).
Proof.
iMod (own_alloc ((● (Excl' e)) ⋅ (◯ (Excl' e)))) as "(%γp & Hprog_auth & Hprog_frag)".
{ by apply auth_both_valid_discrete. }
iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh Hls]]".
iMod (ghost_map_alloc σ.(stapes)) as "[%γT [Ht Hαs]]".
iExists (SpecGS _ _ γp _ _ γH γT).
by iFrame.
Qed.
#[global] Instance spec_rules_spec_updateGS `{!specG_prob_lang Σ} (S : Sig) :
spec_updateGS (lang_markov (gen_lang S)) Σ.
Proof. constructor. exact spec_auth. Defined.