From e27c687a36f17aa6e7ed12b5f48a0904b9569326 Mon Sep 17 00:00:00 2001 From: hehelego Date: Mon, 30 Mar 2026 18:52:50 +0200 Subject: [PATCH 01/21] pseudo random number generator effect currently implemented as a linear congruence generator with fixed parameter --- theories/effects/prng.v | 457 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 457 insertions(+) create mode 100644 theories/effects/prng.v diff --git a/theories/effects/prng.v b/theories/effects/prng.v new file mode 100644 index 0000000..fc35e27 --- /dev/null +++ b/theories/effects/prng.v @@ -0,0 +1,457 @@ +(** pseudo random number generator effect *) +From iris.algebra Require Import gmap excl auth gmap_view list. +From iris.proofmode Require Import classes tactics. +From iris.base_logic Require Import algebra. +From iris.heap_lang Require Export locations. +From gitrees Require Import prelude. +From gitrees Require Import gitree. +From gitrees.lib Require Import eq. + +Section prng_effect. + +Opaque laterO_map. + +Canonical Structure locO := leibnizO loc. + +(* + TODO: keep track of the state update and read out functions represented as GIT + [stateF : oFunctor := (gmapOF locO ((▶ ∙) * (▶ ∙)))%OF;] + [Ins := ((▶ ∙) * (▶ ∙))%OF;] + *) +(* finite map of PRNG states: [Some seed] or [None] for deleted or unallocated. *) +Definition state := gmap loc nat. +Definition stateO : ofe := state. +Definition stateF : oFunctor := constOF state. + +Definition read_lcg : natO -n> natO := λne n, n. +Definition update_lcg : natO -n> natO := λne n, (13 * n + 7) mod 23. +#[global] Opaque read_lcg update_lcg. + +Definition state_new (σ : state) := let l := Loc.fresh (dom σ) in Some (l, <[l := 0]> σ). +Definition state_del (σ : state) (l : loc) := _ ← σ !! l; Some ((), delete l σ). +Definition state_gen (σ : state) (l : loc) := n ← σ !! l; Some (read_lcg n, <[l := update_lcg n]> σ). +Definition state_seed (σ : state) (l : loc) (sd : nat) := _ ← σ !! l; Some ((), <[l := sd]> σ). + +Definition lift_post {A B} : option (A * state) -> option (A * state * list B) + := option_map (fun '(a,st) => (a,st,[])). + +Instance state_inhabited `{Cofe X} : Inhabited (stateF ♯ X). +Proof. + constructor. + constructor. + constructor. +Qed. +Instance state_cofe `{Cofe X} : Cofe (stateF ♯ X). +Proof. + apply gmap_cofe. +Qed. + +Program Definition NewPrngE : opInterp := {| + Ins := unitO; + Outs := locO; +|}. +Definition reify_new X `{Cofe X} + : (Ins NewPrngE ♯ X) * (stateF ♯ X) + → option (Outs NewPrngE ♯ X * (stateF ♯ X) * listO (laterO X)) + := λ '((),s), lift_post $ state_new s. +#[export] Instance reify_new_ne X `{!Cofe X} : + NonExpansive (reify_new X : prodO (Ins NewPrngE ♯ X) (stateF ♯ X) + → optionO (Outs NewPrngE ♯ X * (stateF ♯ X) * listO (laterO X))%type). +Proof. solve_proper. Qed. + + +Program Definition DelPrngE : opInterp := {| + Ins := locO; + Outs := unitO; +|}. +Definition reify_del X `{Cofe X} + : (Ins DelPrngE ♯ X) * (stateF ♯ X) + → option (Outs DelPrngE ♯ X * (stateF ♯ X) * listO (laterO X)) + := λ '(l,s), lift_post $ state_del s l. +#[export] Instance reify_del_ne X `{!Cofe X} : + NonExpansive (reify_del X : prodO (Ins DelPrngE ♯ X) (stateF ♯ X) + → optionO (Outs DelPrngE ♯ X * (stateF ♯ X) * listO (laterO X))%type). +Proof. solve_proper. Qed. + + +Program Definition GenPrngE : opInterp := {| + Ins := locO; + Outs := natO; +|}. +Definition reify_gen X `{Cofe X} + : (Ins GenPrngE ♯ X) * (stateF ♯ X) + → option (Outs GenPrngE ♯ X * (stateF ♯ X) * listO (laterO X)) + := λ '(l,s), lift_post $ state_gen s l. +#[export] Instance reify_gen_ne X `{!Cofe X} : + NonExpansive (reify_gen X : prodO (Ins GenPrngE ♯ X) (stateF ♯ X) + → optionO (Outs GenPrngE ♯ X * (stateF ♯ X) * listO (laterO X))%type). +Proof. solve_proper. Qed. + +Program Definition SeedPrngE : opInterp := {| + Ins := locO * natO; + Outs := unitO; +|}. +Definition reify_seed X `{Cofe X} + : (Ins SeedPrngE ♯ X) * (stateF ♯ X) + → option (Outs SeedPrngE ♯ X * (stateF ♯ X) * listO (laterO X)) + := λ '((l,n),s), lift_post $ state_seed s l n. +#[export] Instance reify_seed_ne X `{!Cofe X} : + NonExpansive (reify_seed X : prodO (Ins SeedPrngE ♯ X) (stateF ♯ X) + → optionO (Outs SeedPrngE ♯ X * (stateF ♯ X) * listO (laterO X))%type). +Proof. solve_proper. Qed. + + +Definition prngE : opsInterp := @[NewPrngE;DelPrngE;GenPrngE;SeedPrngE]. +Program Canonical Structure reify_prng : sReifier NotCtxDep := + Build_sReifier NotCtxDep prngE stateF _ _ _. +Next Obligation. + intros X HX op. + destruct op as [| [| [| [| []]]]]; simpl. + - simple refine (OfeMor (reify_new X)). + - simple refine (OfeMor (reify_del X)). + - simple refine (OfeMor (reify_gen X)). + - simple refine (OfeMor (reify_seed X)). +Defined. + +End prng_effect. + +Section prng_combinators. + Context {E : opsInterp}. + Context `{!subEff prngE E}. + Context {R} `{!Cofe R}. + Context `{Base_nat : !SubOfe natO R} `{Base_unit : !SubOfe unitO R}. + Notation IT := (IT E R). + Notation ITV := (ITV E R). + + Notation opid_new := (inl ()). + Notation opid_del := (inr opid_new). + Notation opid_gen := (inr opid_del). + Notation opid_seed := (inr opid_gen). + + Program Definition PRNG_NEW : (locO -n> IT) -n> IT := + λne k, Vis (E:=E) (subEff_opid opid_new) + (subEff_ins (F:=prngE) (op:=opid_new) ()) + (NextO ◎ k ◎ (subEff_outs (op:=opid_new) ^-1)). + (* XXX: we have to specify [op] otherwise a weird proof obligation will be generated. *) + Solve Obligations with solve_proper. + + Program Definition PRNG_DEL : locO -n> IT := + λne l, Vis (E:=E) (subEff_opid opid_del) + (subEff_ins (F:=prngE) (op:=opid_del) l) + (λne _, Next (Ret ())). + + Program Definition PRNG_GEN : locO -n> IT := + λne l, Vis (E:=E) (subEff_opid $ opid_gen) + (subEff_ins (F:=prngE) (op:=opid_gen) l) + (NextO ◎ Ret ◎ (subEff_outs ^-1)). + + Program Definition PRNG_SEED : locO -n> natO -n> IT := + λne l n, Vis (E:=E) (subEff_opid $ opid_seed) + (subEff_ins (F:=prngE) (op:=opid_seed) (l, n)) + (λne _, Next (Ret ())). + + Lemma hom_NEW k f `{!IT_hom f} : f (PRNG_NEW k) ≡ PRNG_NEW (OfeMor f ◎ k). + Proof. + unfold PRNG_NEW. + rewrite hom_vis/=. repeat f_equiv. + intro x. cbn-[laterO_map]. rewrite laterO_map_Next. + done. + Qed. +End prng_combinators. + +Section wp. + Context {grs_sz : nat}. + Context {a : is_ctx_dep}. + Variable (rs : gReifiers a grs_sz). + Context {R} {CR : Cofe R}. + Context {SO : SubOfe unitO R} {SN : SubOfe natO R}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Notation stateO := (stateF ♯ IT). + + (* TODO: what exactly is this CMRA? Can we get rid of the authoratative RA? *) + Definition istate := gmap_viewR loc natO. + Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ istate }. + Class prngG Σ := PrngG { + prngG_inG :: inG Σ istate; + prngG_name : gname; + }. + Definition prngΣ : gFunctors := GFunctor istate. + #[export] Instance subG_prngΣ {Σ} : subG prngΣ Σ → prngPreG Σ. + Proof. solve_inG. Qed. + + Lemma new_prngG σ `{!prngPreG Σ} : + (⊢ |==> ∃ `{!prngG Σ}, own prngG_name (●V σ): iProp Σ)%I. + Proof. + iMod (own_alloc (●V σ)) as (γ) "H". + { apply gmap_view_auth_valid. } + pose (sg := {| prngG_inG := _; prngG_name := γ |}). + iModIntro. iExists sg. by iFrame. + Qed. + + Context `{!subReifier (sReifier_NotCtxDep_min reify_prng a) rs}. + Context `{!gitreeGS_gen rs R Σ}. + Notation iProp := (iProp Σ). + + Context `{!prngG Σ}. + + Program Definition prng_ctx := + inv (nroot.@"prngE") + (∃ σ, £ 1 ∗ has_substate σ ∗ own prngG_name (●V σ))%I. + + Program Definition has_prng_state (l : loc) (s : nat) : iProp := + own prngG_name $ gmap_view_frag l (DfracOwn 1) s. + Global Instance has_state_proper l : Proper ((≡) ==> (≡)) (has_prng_state l). + Proof. solve_proper. Qed. + Global Instance has_state_ne l : NonExpansive (has_prng_state l). + Proof. solve_proper. Qed. + + Lemma istate_alloc n l σ : + σ !! l = None → + own prngG_name (●V σ) ==∗ own prngG_name (●V (<[l:=n]>σ)) + ∗ has_prng_state l n. + Proof. + iIntros (Hl) "H". + iMod (own_update with "H") as "[$ $]". + { by apply (gmap_view_alloc _ l (DfracOwn 1) n); eauto. } + done. + Qed. + + Lemma istate_read l n σ : + own prngG_name (●V σ) -∗ has_prng_state l n + -∗ (σ !! l) ≡ Some n. + Proof. + iIntros "Ha Hf". + iPoseProof (own_valid_2 with "Ha Hf") as "H". + rewrite gmap_view_both_validI. + iDestruct "H" as "[%H [Hval HEQ]]". + done. + Qed. + + Lemma istate_loc_dom l n σ : + own prngG_name (●V σ) -∗ has_prng_state l n -∗ ⌜is_Some (σ !! l)⌝. + Proof. + iIntros "Hinv Hloc". + iPoseProof (istate_read with "Hinv Hloc") as "Hl". + destruct (σ !! l) ; eauto. + by rewrite option_equivI. + Qed. + + Lemma istate_write l n n' σ : + own prngG_name (●V σ) -∗ has_prng_state l n + ==∗ own prngG_name (●V <[l:=n']>σ) + ∗ has_prng_state l n'. + Proof. + iIntros "H Hl". + iMod (own_update_2 with "H Hl") as "[$ $]"; last done. + by apply gmap_view_replace. + Qed. + + Lemma istate_delete l n σ : + own prngG_name (●V σ) -∗ has_prng_state l n ==∗ own prngG_name (●V delete l σ). + Proof. + iIntros "H Hl". + iMod (own_update_2 with "H Hl") as "$". + { apply gmap_view_delete. } + done. + Qed. + + (* TODO: Piecing together proofs in [store.v]. Review the proof. Understand the mask changes. *) + Lemma wp_gen_hom (l : loc) (n : nat) s Φ (κ : IT -n> IT) `{!IT_hom κ} : + prng_ctx -∗ + ▷ has_prng_state l n -∗ + ▷▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} κ (Ret $ read_lcg n) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_GEN l) @ s {{ Φ }}. + Proof. + iIntros "#Hctx Hp Ha". + unfold PRNG_GEN; simpl. + rewrite hom_vis. + iApply wp_subreify_ctx_indep_lift''. + iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". + simpl. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + (* current state, reification results, new state, continuation, thread pool additions *) + iExists σ,(read_lcg n),(<[l:=update_lcg n]>σ),(κ (Ret $ read_lcg n)),[]. + iFrame "Hs". + iSplit. + { + iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". + unfold lift_post, state_gen. + by rewrite Hread. + } + iSplit; first by rewrite ofe_iso_21 later_map_Next. + iNext. + iMod (istate_write l n (update_lcg n) σ with "Hh Hp") as "[Hh Hp]". + iIntros "Hlc Hs". + iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". + { iExists _. iFrame. } + iModIntro. + iSplit. + - by iApply "Ha". + - by iFrame. + Qed. + + Lemma wp_gen (l : loc) (n : nat) s Φ : + prng_ctx -∗ + ▷ has_prng_state l n -∗ + ▷ ▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} (Ret $ read_lcg n) @ s {{ Φ }}) -∗ + WP@{rs} PRNG_GEN l @ s {{ Φ }}. + Proof. + iIntros "#Hcxt Hp Ha". + iApply (wp_gen_hom _ _ _ _ idfun with "Hcxt Hp Ha"). + Qed. + + Lemma wp_seed_hom (l : loc) (n n' : nat) s Φ (κ : IT -n> IT) `{!IT_hom κ} : + prng_ctx -∗ + ▷ has_prng_state l n -∗ + ▷▷ (has_prng_state l n' -∗ WP@{rs} κ (Ret ()) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_SEED l n') @ s {{ Φ }}. + Proof. + iIntros "#Hctx Hp Ha". + unfold PRNG_SEED; simpl. + rewrite hom_vis. + iApply wp_subreify_ctx_indep_lift''. + iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". + simpl. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + (* current state, reification results, new state, continuation, thread pool additions *) + iExists σ,(),(<[l:=n']>σ),(κ (Ret ())),[]. + iFrame "Hs". + iSplit. + { + iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". + unfold lift_post, state_seed. + by rewrite Hread. + } + iSplit; first by rewrite later_map_Next. + iNext. + iMod (istate_write l n n' σ with "Hh Hp") as "[Hh Hp]". + iIntros "Hlc Hs". + iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". + { iExists _. iFrame. } + iModIntro. + iSplit. + - by iApply "Ha". + - by iFrame. + Qed. + + Lemma wp_seed (l : loc) (n n' : nat) s Φ : + prng_ctx -∗ + ▷ has_prng_state l n -∗ + ▷▷ (has_prng_state l n' -∗ Φ (RetV ())) -∗ + WP@{rs} PRNG_SEED l n' @ s {{ Φ }}. + Proof. + iIntros "#Hctx Hp Ha". + iApply (wp_seed_hom _ _ _ _ _ idfun with "Hctx Hp [Ha]"). + do 2 iNext. + iIntros "H". + iDestruct ("Ha" with "H") as "G". + iApply wp_val. + by iModIntro. + Qed. + + Lemma wp_new_hom (k : locO -n> IT) s Φ `{!NonExpansive Φ} + (κ : IT -n> IT) `{!IT_hom κ} : + prng_ctx -∗ + ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} κ (k l) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_NEW k) @ s {{ Φ }}. + Proof. + iIntros "#Hctx Ha". + unfold PRNG_NEW; simpl. + rewrite hom_vis. + iApply wp_subreify_ctx_indep_lift''. + iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". + simpl. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + set (l:=Loc.fresh (dom σ)). + (* current state, reification results, new state, continuation, thread pool additions *) + iExists σ,l,(<[l:=0]>σ),(κ $ k l),[]. + iFrame "Hs". + iSplit; first done. + iSplit; first by rewrite later_map_Next ofe_iso_21. + iNext. + iMod (istate_alloc 0 l with "Hh") as "[Hh Hp]". + { + apply (not_elem_of_dom_1 (M:=gmap loc)). + rewrite -(Loc.add_0 l). + apply Loc.fresh_fresh. + lia. + } + iIntros "Hlc Hs". + iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". + { iExists _. iFrame. } + iModIntro. + iSplit. + - by iApply "Ha". + - by iFrame. + Qed. + + Lemma wp_new (k : locO -n> IT) s Φ `{!NonExpansive Φ} : + prng_ctx -∗ + ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} k l @ s {{ Φ }}) -∗ + WP@{rs} PRNG_NEW k @ s {{ Φ }}. + Proof. + iIntros "Hh H". + iApply (wp_new_hom _ _ _ idfun with "Hh H"). + Qed. + + Lemma wp_del_hom (l : loc) n s Φ (κ : IT -n> IT) `{!IT_hom κ} : + prng_ctx -∗ + ▷ has_prng_state l n -∗ + ▷ ▷ WP@{rs} κ (Ret ()) @ s {{ β, Φ β }} -∗ + WP@{rs} κ (PRNG_DEL l) @ s {{ Φ }}. + Proof. + iIntros "#Hctx Hp Ha". + unfold PRNG_DEL; simpl. + rewrite hom_vis. + iApply wp_subreify_ctx_indep_lift''. + iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". + simpl. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom". + { iApply (istate_loc_dom with "Hh Hp"). } + destruct Hdom as [x Hx]. + (* current state, reification results, new state, continuation, thread pool additions *) + iExists σ,(),(delete l σ),(κ $ Ret ()),[]. + iFrame "Hs". + iSplit. + { + iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". + unfold lift_post, state_del. + by rewrite Hread. + } + iSplit; first by rewrite later_map_Next. + iNext. + iMod (istate_delete l n σ with "Hh Hp") as "Hh". + iIntros "Hlc Hs". + iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". + { iExists _. iFrame. } + iModIntro. + iSplit. + - by iApply "Ha". + - by iFrame. + Qed. + + Lemma wp_del (l : loc) n s Φ : + prng_ctx -∗ + ▷ has_prng_state l n -∗ + ▷ ▷ Φ (RetV ()) -∗ + WP@{rs} PRNG_DEL l @ s {{ Φ }}. + Proof. + iIntros "#Hctx Hl H". + iApply (wp_del_hom _ _ _ _ idfun with "Hctx Hl [H]"). + do 2 iNext. + iApply wp_val. + iModIntro. done. + Qed. +End wp. + +Arguments prng_ctx {_ _} rs {_ _ _ _ _ _}. +Arguments has_prng_state {_ _} _ _. +#[global] Opaque PRNG_NEW PRNG_DEL PRNG_GEN PRNG_SEED. + From 107d9b74270372b38402b412ca938b92f9df05c8 Mon Sep 17 00:00:00 2001 From: hehelego Date: Mon, 30 Mar 2026 19:04:45 +0200 Subject: [PATCH 02/21] update `_CoqProject` to include the PRNG effect reifier and the PRNG-lang --- _CoqProject | 6 + theories/examples/prng_lang/interp.v | 0 theories/examples/prng_lang/lang.v | 667 ++++++++++++++++++++++++++ theories/examples/prng_lang/logpred.v | 0 theories/examples/prng_lang/logrel.v | 0 5 files changed, 673 insertions(+) create mode 100644 theories/examples/prng_lang/interp.v create mode 100644 theories/examples/prng_lang/lang.v create mode 100644 theories/examples/prng_lang/logpred.v create mode 100644 theories/examples/prng_lang/logrel.v diff --git a/_CoqProject b/_CoqProject index 86e368c..288aad2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -39,6 +39,7 @@ theories/effects/exceptions.v theories/effects/delim.v theories/effects/fork.v theories/effects/coroutines.v +theories/effects/prng.v theories/lib/pairs.v theories/lib/sums.v @@ -87,6 +88,11 @@ theories/examples/heap_lang/notation.v theories/examples/heap_lang/pretty.v theories/examples/heap_lang/tactics.v +theories/examples/prng_lang/lang.v +theories/examples/prng_lang/interp.v +theories/examples/prng_lang/logpred.v +theories/examples/prng_lang/logrel.v + theories/utils/finite_sets.v theories/utils/clwp.v theories/utils/wbwp.v diff --git a/theories/examples/prng_lang/interp.v b/theories/examples/prng_lang/interp.v new file mode 100644 index 0000000..e69de29 diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v new file mode 100644 index 0000000..fb3e8ac --- /dev/null +++ b/theories/examples/prng_lang/lang.v @@ -0,0 +1,667 @@ +From gitrees Require Export prelude effects.prng. +Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. +From stdpp Require gmap. + +Inductive nat_op := Add | Sub | Mult | Div | Mod | Pow. + +Inductive expr {X : Set} : Type := + (* Values *) +| Val (v : val) : expr +| Var (x : X) : expr +(* Base lambda calculus *) +| App (e₁ : expr) (e₂ : expr) : expr +(* Base types and their operations *) +| NatOp (op : nat_op) (e₁ : expr) (e₂ : expr) : expr +| If (e₁ : expr) (e₂ : expr) (e₃ : expr) : expr +(* The effects *) +| NewPrng : expr +| DelPrng (e : expr) : expr +| Seed (e₁ : expr) (e₂ : expr) : expr +| Rand (e : expr) : expr +with val {X : Set} := +| UnitV : val +| LitV (n : nat) : val +| LitPrng (l : loc) : val +| RecV (e : @expr (inc (inc X))) : val +with ectx {X : Set} := +| EmptyK : ectx +| DelPrngK (K : ectx) : ectx +| SeedKl (K : ectx) (e : expr) : ectx +| SeedKs (e : expr) (K : ectx) : ectx +| RandK (K : ectx) : ectx +| IfK (K : ectx) (e₁ : expr) (e₂ : expr) : ectx +| AppLK (K : ectx) (v : val) : ectx +| AppRK (e : expr) (K : ectx) : ectx +| NatOpRK (op : nat_op) (e : expr) (K : ectx) : ectx +| NatOpLK (op : nat_op) (K : ectx) (v : val) : ectx. + +Arguments val X%_bind : clear implicits. +Arguments expr X%_bind : clear implicits. +Arguments ectx X%_bind : clear implicits. + +Local Open Scope bind_scope. + +Fixpoint emap {A B : Set} (f : A [→] B) (e : expr A) : expr B := + match e with + | Val v => Val (vmap f v) + | Var x => Var (f x) + | App e₁ e₂ => App (emap f e₁) (emap f e₂) + | NatOp o e₁ e₂ => NatOp o (emap f e₁) (emap f e₂) + | If e₁ e₂ e₃ => If (emap f e₁) (emap f e₂) (emap f e₃) + | NewPrng => NewPrng + | DelPrng e => DelPrng (emap f e) + | Seed e₁ e₂ => Seed (emap f e₁) (emap f e₂) + | Rand e => Rand (emap f e) + end +with vmap {A B : Set} (f : A [→] B) (v : val A) : val B := + match v with + | UnitV => UnitV + | LitV n => LitV n + | LitPrng l => LitPrng l + | RecV e => RecV (emap ((f ↑) ↑) e) + end. +Fixpoint kmap {A B : Set} (f : A [→] B) (K : ectx A) : ectx B := + match K with + | EmptyK => EmptyK + | DelPrngK K => DelPrngK (kmap f K) + | SeedKl K s => SeedKl (kmap f K) (emap f s) + | SeedKs l K => SeedKs (emap f l) (kmap f K) + | RandK K => RandK (kmap f K) + | IfK K e₁ e₂ => IfK (kmap f K) (emap f e₁) (emap f e₂) + | AppLK K v => AppLK (kmap f K) (vmap f v) + | AppRK e K => AppRK (emap f e) (kmap f K) + | NatOpRK op e K => NatOpRK op (emap f e) (kmap f K) + | NatOpLK op K v => NatOpLK op (kmap f K) (vmap f v) + end. +#[export] Instance FMap_expr : FunctorCore expr := @emap. +#[export] Instance FMap_val : FunctorCore val := @vmap. +#[export] Instance FMap_ectx : FunctorCore ectx := @kmap. + +#[export] Instance SPC_expr : SetPureCore expr := @Var. + +Fixpoint ebind {A B : Set} (f : A [⇒] B) (e : expr A) : expr B := + match e with + | Val v => Val (vbind f v) + | Var x => f x + | App e₁ e₂ => App (ebind f e₁) (ebind f e₂) + | NatOp o e₁ e₂ => NatOp o (ebind f e₁) (ebind f e₂) + | If e₁ e₂ e₃ => If (ebind f e₁) (ebind f e₂) (ebind f e₃) + | NewPrng => NewPrng + | DelPrng e => DelPrng (ebind f e) + | Seed e₁ e₂ => Seed (ebind f e₁) (ebind f e₂) + | Rand e => Rand (ebind f e) + end +with vbind {A B : Set} (f : A [⇒] B) (v : val A) : val B := + match v with + | UnitV => UnitV + | LitV n => LitV n + | LitPrng l => LitPrng l + | RecV e => RecV (ebind ((f ↑) ↑) e) + end. +Fixpoint kbind {A B : Set} (f : A [⇒] B) (K : ectx A) : ectx B := + match K with + | EmptyK => EmptyK + | DelPrngK K => DelPrngK (kbind f K) + | SeedKl K s => SeedKl (kbind f K) (ebind f s) + | SeedKs l K => SeedKs (ebind f l) (kbind f K) + | RandK K => RandK (kbind f K) + | IfK K e₁ e₂ => IfK (kbind f K) (ebind f e₁) (ebind f e₂) + | AppLK K v => AppLK (kbind f K) (vbind f v) + | AppRK e K => AppRK (ebind f e) (kbind f K) + | NatOpRK op e K => NatOpRK op (ebind f e) (kbind f K) + | NatOpLK op K v => NatOpLK op (kbind f K) (vbind f v) + end. + +#[export] Instance BindCore_expr : BindCore expr := @ebind. +#[export] Instance BindCore_val : BindCore val := @vbind. +#[export] Instance BindCore_ectx : BindCore ectx := @kbind. + +#[export] Instance IP_typ : SetPure expr. +Proof. + split; intros; reflexivity. +Qed. + +Fixpoint vmap_id X (δ : X [→] X) (v : val X) : δ ≡ ı → fmap δ v = v +with emap_id X (δ : X [→] X) (e : expr X) : δ ≡ ı → fmap δ e = e +with kmap_id X (δ : X [→] X) (e : ectx X) : δ ≡ ı → fmap δ e = e. +Proof. + - auto_map_id. + - auto_map_id. + - auto_map_id. +Qed. + +Fixpoint vmap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (v : val A) : + f ∘ g ≡ h → fmap f (fmap g v) = fmap h v +with emap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (e : expr A) : + f ∘ g ≡ h → fmap f (fmap g e) = fmap h e +with kmap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (e : ectx A) : + f ∘ g ≡ h → fmap f (fmap g e) = fmap h e. +Proof. + - auto_map_comp. + - auto_map_comp. + - auto_map_comp. +Qed. + +#[export] Instance Functor_val : Functor val. +Proof. + split; [exact vmap_id | exact vmap_comp]. +Qed. +#[export] Instance Functor_expr : Functor expr. +Proof. + split; [exact emap_id | exact emap_comp]. +Qed. +#[export] Instance Functor_ectx : Functor ectx. +Proof. + split; [exact kmap_id | exact kmap_comp]. +Qed. + +Fixpoint vmap_vbind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (v : val A) : + f ̂ ≡ g → fmap f v = bind g v +with emap_ebind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (e : expr A) : + f ̂ ≡ g → fmap f e = bind g e +with kmap_kbind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (e : ectx A) : + f ̂ ≡ g → fmap f e = bind g e. +Proof. + - auto_map_bind_pure. + erewrite emap_ebind_pure; [reflexivity |]. + intros [| [| x]]; term_simpl; [reflexivity | reflexivity |]. + rewrite <-(EQ x). + reflexivity. + - auto_map_bind_pure. + - auto_map_bind_pure. +Qed. + +#[export] Instance BindMapPure_val : BindMapPure val. +Proof. + split; intros; now apply vmap_vbind_pure. +Qed. +#[export] Instance BindMapPure_expr : BindMapPure expr. +Proof. + split; intros; now apply emap_ebind_pure. +Qed. +#[export] Instance BindMapPure_ectx : BindMapPure ectx. +Proof. + split; intros; now apply kmap_kbind_pure. +Qed. + +Fixpoint vmap_vbind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (v : val A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ v) = fmap f₁ (bind g₁ v) +with emap_ebind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (e : expr A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ e) = fmap f₁ (bind g₁ e) +with kmap_kbind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (e : ectx A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ e) = fmap f₁ (bind g₁ e). +Proof. + - auto_map_bind_comm. + erewrite emap_ebind_comm; [reflexivity |]. + erewrite lift_comm; [reflexivity |]. + erewrite lift_comm; [reflexivity | assumption]. + - auto_map_bind_comm. + - auto_map_bind_comm. +Qed. + +#[export] Instance BindMapComm_val : BindMapComm val. +Proof. + split; intros; now apply vmap_vbind_comm. +Qed. +#[export] Instance BindMapComm_expr : BindMapComm expr. +Proof. + split; intros; now apply emap_ebind_comm. +Qed. +#[export] Instance BindMapComm_ectx : BindMapComm ectx. +Proof. + split; intros; now apply kmap_kbind_comm. +Qed. + +Fixpoint vbind_id (A : Set) (f : A [⇒] A) (v : val A) : + f ≡ ı → bind f v = v +with ebind_id (A : Set) (f : A [⇒] A) (e : expr A) : + f ≡ ı → bind f e = e +with kbind_id (A : Set) (f : A [⇒] A) (e : ectx A) : + f ≡ ı → bind f e = e. +Proof. + - auto_bind_id. + rewrite ebind_id; [reflexivity |]. + apply lift_id, lift_id; assumption. + - auto_bind_id. + - auto_bind_id. +Qed. + +Fixpoint vbind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (v : val A) : + f ∘ g ≡ h → bind f (bind g v) = bind h v +with ebind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (e : expr A) : + f ∘ g ≡ h → bind f (bind g e) = bind h e +with kbind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (e : ectx A) : + f ∘ g ≡ h → bind f (bind g e) = bind h e. +Proof. + - auto_bind_comp. + erewrite ebind_comp; [reflexivity |]. + erewrite lift_comp; [reflexivity |]. + erewrite lift_comp; [reflexivity | assumption]. + - auto_bind_comp. + - auto_bind_comp. +Qed. + +#[export] Instance Bind_val : Bind val. +Proof. + split; intros; [now apply vbind_id | now apply vbind_comp]. +Qed. +#[export] Instance Bind_expr : Bind expr. +Proof. + split; intros; [now apply ebind_id | now apply ebind_comp]. +Qed. +#[export] Instance Bind_ectx : Bind ectx. +Proof. + split; intros; [now apply kbind_id | now apply kbind_comp]. +Qed. + +Definition to_val {S} (e : expr S) : option (val S) := + match e with + | Val v => Some v + | _ => None + end. + +Definition do_natop (op : nat_op) (x y : nat) : nat := + match op with + | Add => plus x y + | Sub => minus x y + | Mult => mult x y + | Div => fst $ Nat.divmod x y 0 0 + | Mod => snd $ Nat.divmod x y 0 0 + | Pow => Nat.pow x y + end. + +Definition nat_op_interp {S} (n : nat_op) (x y : val S) : option (val S) := + match x, y with + | LitV x, LitV y => Some $ LitV $ do_natop n x y + | _,_ => None + end. + +Fixpoint fill {X : Set} (K : ectx X) (e : expr X) : expr X := + match K with + | EmptyK => e + | DelPrngK K => DelPrng (fill K e) + | SeedKl K s => Seed (fill K e) s + | SeedKs l K => Seed l (fill K e) + | RandK K => Rand (fill K e) + | IfK K e₁ e₂ => If (fill K e) e₁ e₂ + | AppLK K v => App (fill K e) (Val v) + | AppRK e' K => App e' (fill K e) + | NatOpRK op e' K => NatOp op e' (fill K e) + | NatOpLK op K v => NatOp op (fill K e) (Val v) + end. + +Lemma fill_emap {X Y : Set} (f : X [→] Y) (K : ectx X) (e : expr X) + : fmap f (fill K e) = fill (fmap f K) (fmap f e). +Proof. + revert f. + induction K as [| ?? IH + | ?? IH + | ??? IH + | ?? IH + | ?? IH + | ?? IH + | ??? IH + | ???? IH + | ??? IH]; + intros f; term_simpl; first done; rewrite IH; reflexivity. +Qed. + +(*** Operational semantics *) + +(* counter: (unfold ticks, pure/effect) *) +Inductive head_step {S} : expr S → state → expr S → state → nat*nat → Prop := +| BetaS e1 v2 σ : + head_step (App (Val $ RecV e1) (Val v2)) σ (subst (Inc := inc) ((subst (F := expr) (Inc := inc) e1) (Val (shift (Inc := inc) v2))) (Val (RecV e1))) σ (1,0) +| NewPrngS σ l σ' : + state_new σ = Some (l,σ') → + head_step NewPrng σ (Val $ LitPrng l) σ' (1,1) +| DelPrngS σ l σ' : + state_del σ l = Some ((),σ') → + head_step (DelPrng (Val $ LitPrng l)) σ (Val $ UnitV) σ' (1,1) +| RandS σ l n σ' : + state_gen σ l = Some (n, σ') → + head_step (Rand $ Val $ LitPrng l) σ (Val $ LitV n) σ' (1,1) +| SeedS σ l n σ' : + state_seed σ l n = Some ((), σ') → + head_step (Seed (Val $ LitPrng l) (Val $ LitV n)) σ (Val $ UnitV) σ' (1,1) +| IfTrueS n e1 e2 σ : + n > 0 → + head_step (If (Val (LitV n)) e1 e2) σ + e1 σ (0,0) +| IfFalseS n e1 e2 σ : + n = 0 → + head_step (If (Val (LitV n)) e1 e2) σ + e2 σ (0,0) +. + +Lemma head_step_prng_01 {S} (e1 e2 : expr S) σ1 σ2 n m : + head_step e1 σ1 e2 σ2 (n,m) → m = 0 ∨ m = 1. +Proof. inversion 1; eauto. Qed. +Lemma head_step_unfold_01 {S} (e1 e2 : expr S) σ1 σ2 n m : + head_step e1 σ1 e2 σ2 (n,m) → n = 0 ∨ n = 1. +Proof. inversion 1; eauto. Qed. +Lemma head_step_pure {S} (e1 e2 : expr S) σ1 σ2 n : + head_step e1 σ1 e2 σ2 (n,0) → σ1 = σ2. +Proof. inversion 1; eauto. Qed. + +(** Carbonara from heap lang *) +Global Instance fill_item_inj {S} (Ki : ectx S) : Inj (=) (=) (fill Ki). +Proof. + induction Ki; intros ???; simplify_eq/=; auto with f_equal. +Qed. + +Lemma fill_item_val {S} Ki (e : expr S) : + is_Some (to_val (fill Ki e)) → is_Some (to_val e). +Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed. + +Lemma val_head_stuck {S} (e1 : expr S) σ1 e2 σ2 m : head_step e1 σ1 e2 σ2 m → to_val e1 = None. +Proof. destruct 1; naive_solver. Qed. + +Fixpoint ectx_compose {S} (K1 K2 : ectx S) : ectx S + := match K1 with + | EmptyK => K2 + | DelPrngK K => DelPrngK (ectx_compose K K2) + | SeedKl K s => SeedKl (ectx_compose K K2) s + | SeedKs l K => SeedKs l (ectx_compose K K2) + | RandK K => RandK (ectx_compose K K2) + | IfK K e₁ e₂ => IfK (ectx_compose K K2) e₁ e₂ + | AppLK K v => AppLK (ectx_compose K K2) v + | AppRK e K => AppRK e (ectx_compose K K2) + | NatOpRK op e K => NatOpRK op e (ectx_compose K K2) + | NatOpLK op K v => NatOpLK op (ectx_compose K K2) v + end. + +Lemma fill_app {S} (K1 K2 : ectx S) e : fill (ectx_compose K1 K2) e = fill K1 (fill K2 e). +Proof. + revert K2. + revert e. + induction K1 as [| ?? IH + | ?? IH + | ??? IH + | ?? IH + | ?? IH + | ?? IH + | ??? IH + | ???? IH + | ??? IH]; + simpl; first done; intros e' K2; rewrite IH; reflexivity. +Qed. + +Lemma fill_val : ∀ {S} K (e : expr S), is_Some (to_val (fill K e)) → is_Some (to_val e). +Proof. + intros S K. + induction K as [| ?? IH + | ?? IH + | ??? IH + | ?? IH + | ?? IH + | ?? IH + | ??? IH + | ???? IH + | ??? IH]=> e' //=; + inversion 1 as [? HH]; inversion HH. +Qed. + +Lemma fill_not_val : ∀ {S} K (e : expr S), to_val e = None → to_val (fill K e) = None. +Proof. + intros S K e. rewrite !eq_None_not_Some. + eauto using fill_val. +Qed. + +Lemma fill_empty {S} (e : expr S) : fill EmptyK e = e. +Proof. reflexivity. Qed. +Lemma fill_comp {S} K1 K2 (e : expr S) : fill K2 (fill K1 e) = fill (ectx_compose K2 K1) e. +Proof. by rewrite fill_app. Qed. +Global Instance fill_inj {S} (K : ectx S) : Inj (=) (=) (fill K). +Proof. + induction K as [| ?? IH + | ?? IH + | ??? IH + | ?? IH + | ?? IH + | ?? IH + | ??? IH + | ???? IH + | ??? IH]; + rewrite /Inj; naive_solver. +Qed. + +Inductive prim_step {S} (e1 : expr S) (σ1 : state) + (e2 : expr S) (σ2 : state) (n : nat*nat) : Prop:= + Ectx_step (K : ectx S) e1' e2' : + e1 = fill K e1' → e2 = fill K e2' → + head_step e1' σ1 e2' σ2 n → prim_step e1 σ1 e2 σ2 n. + +Lemma prim_step_pure {S} (e1 e2 : expr S) σ1 σ2 n : + prim_step e1 σ1 e2 σ2 (n,0) → σ1 = σ2. +Proof. + inversion 1; simplify_eq/=. + inversion H2; eauto. +Qed. + +Inductive prim_steps {S} : expr S → state → expr S → state → nat*nat → Prop := +| prim_steps_zero e σ : + prim_steps e σ e σ (0,0) +| prim_steps_abit e1 σ1 e2 σ2 e3 σ3 n1 m1 n2 m2 : + prim_step e1 σ1 e2 σ2 (n1,m1) → + prim_steps e2 σ2 e3 σ3 (n2,m2) → + prim_steps e1 σ1 e3 σ3 (n1+n2,m1+m2) +. + +Lemma Ectx_step' {S} (K : ectx S) e1 σ1 e2 σ2 efs : + head_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs. +Proof. econstructor; eauto. Qed. + +Lemma prim_step_ctx {S} (K : ectx S) e1 σ1 e2 σ2 efs : + prim_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs. +Proof. + destruct 1 as [K2 u1 u2 HK2]. + subst e1 e2. rewrite -!fill_app. + by econstructor; eauto. +Qed. + +Lemma prim_steps_ctx {S} (K : ectx S) e1 σ1 e2 σ2 efs : + prim_steps e1 σ1 e2 σ2 efs → prim_steps (fill K e1) σ1 (fill K e2) σ2 efs. +Proof. + induction 1; econstructor; eauto using prim_step_ctx. +Qed. + +Lemma prim_steps_app {S} nm1 nm2 (e1 e2 e3 : expr S) σ1 σ2 σ3 : + prim_steps e1 σ1 e2 σ2 nm1 → prim_steps e2 σ2 e3 σ3 nm2 → + prim_steps e1 σ1 e3 σ3 (nm1.1 + nm2.1, nm1.2 + nm2.2). +Proof. + intros Hst. revert nm2. + induction Hst; intros [n' m']; simplify_eq/=; first done. + rewrite -!Nat.add_assoc. intros Hsts. + econstructor; eauto. + by apply (IHHst (n',m')). +Qed. + +Lemma prim_step_steps {S} nm (e1 e2 : expr S) σ1 σ2 : + prim_step e1 σ1 e2 σ2 nm → prim_steps e1 σ1 e2 σ2 nm. +Proof. + destruct nm as [n m]. intro Hs. + rewrite -(Nat.add_0_r n). + rewrite -(Nat.add_0_r m). + econstructor; eauto. + by constructor. +Qed. + + +(*** Type system *) + + +Inductive ty := Tnat | Tunit | Tprng | Tarr : ty → ty → ty. + +Inductive typed {S : Set} (Γ : S -> ty) : expr S → ty → Prop := +| typed_Val (τ : ty) (v : val S) : + typed_val Γ v τ → + typed Γ (Val v) τ +| typed_Var (τ : ty) (v : S) : + Γ v = τ → + typed Γ (Var v) τ +| typed_App (τ1 τ2 : ty) e1 e2 : + typed Γ e1 (Tarr τ1 τ2) → + typed Γ e2 τ1 → + typed Γ (App e1 e2) τ2 +| typed_NatOp e1 e2 op : + typed Γ e1 Tnat → + typed Γ e2 Tnat → + typed Γ (NatOp op e1 e2) Tnat +| typed_If e0 e1 e2 τ : + typed Γ e0 Tnat → + typed Γ e1 τ → + typed Γ e2 τ → + typed Γ (If e0 e1 e2) τ +| typed_NewPrng : + typed Γ NewPrng Tprng +| typed_DelPrng e : + typed Γ e Tprng → + typed Γ (DelPrng e) Tunit +| typed_Rand e : + typed Γ e Tprng → + typed Γ (Rand e) Tnat +| typed_Seed el es : + typed Γ el Tprng → + typed Γ es Tnat → + typed Γ (Seed el es) Tunit +with typed_val {S : Set} (Γ : S -> ty) : val S → ty → Prop := +| typed_Unit : + typed_val Γ UnitV Tunit +| typed_Lit n : + typed_val Γ (LitV n) Tnat +| typed_Loc l : + typed_val Γ (LitPrng l) Tprng +| typed_RecV (τ1 τ2 : ty) (e : expr (inc (inc S))) : + typed (Γ ▹ (Tarr τ1 τ2) ▹ τ1) e τ2 → + typed_val Γ (RecV e) (Tarr τ1 τ2) +. + +Declare Scope syn_scope. +Delimit Scope syn_scope with syn. + +Coercion Val : val >-> expr. + +Coercion App : expr >-> Funclass. +Coercion AppLK : ectx >-> Funclass. +Coercion AppRK : expr >-> Funclass. + +(* XXX: We use these typeclasses to share the notaiton between the +expressions and the evaluation contexts, for readability. It will be +good to also share the notation between different languages. *) + +Class AsSynExpr (F : Set -> Type) := { __asSynExpr : ∀ S, F S -> expr S }. + +Arguments __asSynExpr {_} {_} {_}. + +Global Instance AsSynExprValue : AsSynExpr val := { + __asSynExpr _ v := Val v + }. +Global Instance AsSynExprExpr : AsSynExpr expr := { + __asSynExpr _ e := e + }. + +Class OpNotation (A B C D : Type) := { __op : A -> B -> C -> D }. + +Global Instance OpNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : OpNotation (F S) nat_op (G S) (expr S) := { + __op e₁ op e₂ := NatOp op (__asSynExpr e₁) (__asSynExpr e₂) + }. + +Global Instance OpNotationLK {S : Set} : OpNotation (ectx S) (nat_op) (val S) (ectx S) := { + __op K op v := NatOpLK op K v + }. + +Global Instance OpNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : OpNotation (F S) (nat_op) (ectx S) (ectx S) := { + __op e op K := NatOpRK op (__asSynExpr e) K + }. + +Class IfNotation (A B C D : Type) := { __if : A -> B -> C -> D }. + +Global Instance IfNotationExpr {S : Set} {F G H : Set -> Type} `{AsSynExpr F, AsSynExpr G, AsSynExpr H} : IfNotation (F S) (G S) (H S) (expr S) := { + __if e₁ e₂ e₃ := If (__asSynExpr e₁) (__asSynExpr e₂) (__asSynExpr e₃) + }. + +Global Instance IfNotationK {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : IfNotation (ectx S) (F S) (G S) (ectx S) := { + __if K e₂ e₃ := IfK K (__asSynExpr e₂) (__asSynExpr e₃) + }. + +Class AppNotation (A B C : Type) := { __app : A -> B -> C }. + +Global Instance AppNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : AppNotation (F S) (G S) (expr S) := { + __app e₁ e₂ := App (__asSynExpr e₁) (__asSynExpr e₂) + }. + +Global Instance AppNotationLK {S : Set} : AppNotation (ectx S) (val S) (ectx S) := { + __app K v := AppLK K v + }. + +Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (ectx S) (ectx S) := { + __app e K := AppRK (__asSynExpr e) K + }. + +Class DelNotation (A B : Type) := { __del : A -> B }. +Global Instance DelNotationExpr {S : Set} {F : Set -> Type} `{AsSynExpr F} +: DelNotation (F S) (expr S) := { __del e := DelPrng (__asSynExpr e) }. +Global Instance DelNotationK {S : Set} +: DelNotation (ectx S) (ectx S) := { __del K := DelPrngK K }. + +Class RandNotation (A B : Type) := { __rand : A -> B }. +Global Instance RandNotationExpr {S : Set} {F : Set -> Type} `{AsSynExpr F} +: RandNotation (F S) (expr S) := { __rand e := Rand (__asSynExpr e) }. +Global Instance RandNotationK {S : Set} +: RandNotation (ectx S) (ectx S) := { __rand K := RandK K }. + +Class SeedNotation (A B C : Type) := { __seed : A -> B -> C }. +Global Instance SeedNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} +: SeedNotation (F S) (G S) (expr S) := { __seed el es := Seed (__asSynExpr el) (__asSynExpr es) }. +Global Instance SeedNotationLK {S : Set} +: SeedNotation (ectx S) (val S) (ectx S) := { __seed K v := SeedKl K v }. +Global Instance SeedNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} +: SeedNotation (F S) (ectx S) (ectx S) := { __seed e K := SeedKs (__asSynExpr e) K }. + +Notation of_val := Val (only parsing). + +Notation "'newprng'" := (NewPrng) : syn_scope. +Notation "'delprng' x" := (__del x%syn) (at level 60) : syn_scope. +Notation "'rand' x" := (__rand x%syn) (at level 60) : syn_scope. +Notation "'seed' x y" := (__seed x%syn y%syn) (at level 50) : syn_scope. + +Notation "x '⋆' y" := (__app x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope. +Notation "x '+' y" := (__op x%syn Add y%syn) : syn_scope. +Notation "x '-' y" := (__op x%syn Sub y%syn) : syn_scope. +Notation "x '*' y" := (__op x%syn Mult y%syn) : syn_scope. +Notation "'if' x 'then' y 'else' z" := (__if x%syn y%syn z%syn) : syn_scope. +Notation "'#' '()'" := (UnitV) (at level 60) : syn_scope. +Notation "'#' n" := (LitV n) (at level 60) : syn_scope. +Notation "'rec' e" := (RecV e%syn) (at level 60) : syn_scope. +Notation "'$' fn" := (set_pure_resolver fn) (at level 60) : syn_scope. +Notation "□" := (EmptyK) : syn_scope. +Notation "K '⟪' e '⟫'" := (fill K%syn e%syn) (at level 60) : syn_scope. + +Definition LamV {S : Set} (e : expr (inc S)) : val S := + RecV (shift e). + +Notation "'λ' . e" := (LamV e%syn) (at level 60) : syn_scope. + +Definition LetE {S : Set} (e : expr S) (e' : expr (inc S)) : expr S := + App (LamV e') (e). + +Notation "'let_' e₁ 'in' e₂" := (LetE e₁%syn e₂%syn) (at level 60, right associativity) : syn_scope. + +Definition SeqE {S : Set} (e e' : expr S) : expr S := + App (LamV (shift e)) e'. + +Notation "e₁ ';;' e₂" := (SeqE e₁%syn e₂%syn) : syn_scope. + +Declare Scope typ_scope. +Delimit Scope typ_scope with typ. + +Notation "'𝟙'" := (Tunit) (at level 1) : typ_scope. +Notation "'ℕ'" := (Tnat) (at level 1) : typ_scope. +Notation "A →ₜ B" := (Tarr A%typ B%typ) + (right associativity, at level 60) : typ_scope. + +(* TODO: add some example PRNG-lang programs *) diff --git a/theories/examples/prng_lang/logpred.v b/theories/examples/prng_lang/logpred.v new file mode 100644 index 0000000..e69de29 diff --git a/theories/examples/prng_lang/logrel.v b/theories/examples/prng_lang/logrel.v new file mode 100644 index 0000000..e69de29 From a7612d6106ca15e2cd13ee75df2ceea5a0c6da94 Mon Sep 17 00:00:00 2001 From: hehelego Date: Thu, 2 Apr 2026 16:33:15 +0200 Subject: [PATCH 03/21] fix PRNG lang evaluation order `SEED rng seed` should evaluate `rng` first then evaluate `seed` --- theories/examples/prng_lang/lang.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v index fb3e8ac..560675d 100644 --- a/theories/examples/prng_lang/lang.v +++ b/theories/examples/prng_lang/lang.v @@ -27,7 +27,7 @@ with ectx {X : Set} := | EmptyK : ectx | DelPrngK (K : ectx) : ectx | SeedKl (K : ectx) (e : expr) : ectx -| SeedKs (e : expr) (K : ectx) : ectx +| SeedKs (v : val) (K : ectx) : ectx | RandK (K : ectx) : ectx | IfK (K : ectx) (e₁ : expr) (e₂ : expr) : ectx | AppLK (K : ectx) (v : val) : ectx @@ -65,7 +65,7 @@ Fixpoint kmap {A B : Set} (f : A [→] B) (K : ectx A) : ectx B := | EmptyK => EmptyK | DelPrngK K => DelPrngK (kmap f K) | SeedKl K s => SeedKl (kmap f K) (emap f s) - | SeedKs l K => SeedKs (emap f l) (kmap f K) + | SeedKs l K => SeedKs (vmap f l) (kmap f K) | RandK K => RandK (kmap f K) | IfK K e₁ e₂ => IfK (kmap f K) (emap f e₁) (emap f e₂) | AppLK K v => AppLK (kmap f K) (vmap f v) @@ -103,7 +103,7 @@ Fixpoint kbind {A B : Set} (f : A [⇒] B) (K : ectx A) : ectx B := | EmptyK => EmptyK | DelPrngK K => DelPrngK (kbind f K) | SeedKl K s => SeedKl (kbind f K) (ebind f s) - | SeedKs l K => SeedKs (ebind f l) (kbind f K) + | SeedKs l K => SeedKs (vbind f l) (kbind f K) | RandK K => RandK (kbind f K) | IfK K e₁ e₂ => IfK (kbind f K) (ebind f e₁) (ebind f e₂) | AppLK K v => AppLK (kbind f K) (vbind f v) @@ -284,7 +284,7 @@ Fixpoint fill {X : Set} (K : ectx X) (e : expr X) : expr X := | EmptyK => e | DelPrngK K => DelPrng (fill K e) | SeedKl K s => Seed (fill K e) s - | SeedKs l K => Seed l (fill K e) + | SeedKs l K => Seed (Val l) (fill K e) | RandK K => Rand (fill K e) | IfK K e₁ e₂ => If (fill K e) e₁ e₂ | AppLK K v => App (fill K e) (Val v) @@ -617,10 +617,10 @@ Global Instance RandNotationK {S : Set} Class SeedNotation (A B C : Type) := { __seed : A -> B -> C }. Global Instance SeedNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : SeedNotation (F S) (G S) (expr S) := { __seed el es := Seed (__asSynExpr el) (__asSynExpr es) }. -Global Instance SeedNotationLK {S : Set} +Global Instance SeedNotationKloc {S : Set} : SeedNotation (ectx S) (val S) (ectx S) := { __seed K v := SeedKl K v }. -Global Instance SeedNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} -: SeedNotation (F S) (ectx S) (ectx S) := { __seed e K := SeedKs (__asSynExpr e) K }. +Global Instance SeedNotationKseed {S : Set} {F : Set -> Type} `{AsSynExpr F} +: SeedNotation (val S) (ectx S) (ectx S) := { __seed v K := SeedKs v K }. Notation of_val := Val (only parsing). From 1e29f6d467e7610d85ed74b9128c8c9764001397 Mon Sep 17 00:00:00 2001 From: hehelego Date: Thu, 2 Apr 2026 17:16:29 +0200 Subject: [PATCH 04/21] fix add back the missing head reduction for nat op expressions --- theories/examples/prng_lang/lang.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v index 560675d..d858023 100644 --- a/theories/examples/prng_lang/lang.v +++ b/theories/examples/prng_lang/lang.v @@ -335,6 +335,10 @@ Inductive head_step {S} : expr S → state → expr S → state → nat*nat → n = 0 → head_step (If (Val (LitV n)) e1 e2) σ e2 σ (0,0) +| NatOpS op v1 v2 v3 σ : + nat_op_interp op v1 v2 = Some v3 → + head_step (NatOp op (Val v1) (Val v2)) σ + (Val v3) σ (0,0) . Lemma head_step_prng_01 {S} (e1 e2 : expr S) σ1 σ2 n m : From cf94b0f41f8fde4b0a504060bb5b689c5ecf972e Mon Sep 17 00:00:00 2001 From: hehelego Date: Fri, 3 Apr 2026 14:49:37 +0200 Subject: [PATCH 05/21] PRNG gitree combinators with continunation --- theories/effects/prng.v | 207 +++++++++++++++++++++------------------- 1 file changed, 111 insertions(+), 96 deletions(-) diff --git a/theories/effects/prng.v b/theories/effects/prng.v index fc35e27..d136d53 100644 --- a/theories/effects/prng.v +++ b/theories/effects/prng.v @@ -128,35 +128,51 @@ Section prng_combinators. Notation opid_gen := (inr opid_del). Notation opid_seed := (inr opid_gen). + (* XXX: we have to specify [op] otherwise a weird proof obligation will be generated. *) Program Definition PRNG_NEW : (locO -n> IT) -n> IT := λne k, Vis (E:=E) (subEff_opid opid_new) (subEff_ins (F:=prngE) (op:=opid_new) ()) (NextO ◎ k ◎ (subEff_outs (op:=opid_new) ^-1)). - (* XXX: we have to specify [op] otherwise a weird proof obligation will be generated. *) Solve Obligations with solve_proper. - Program Definition PRNG_DEL : locO -n> IT := - λne l, Vis (E:=E) (subEff_opid opid_del) - (subEff_ins (F:=prngE) (op:=opid_del) l) - (λne _, Next (Ret ())). + Program Definition PRNG_DEL_k : locO -n> (unitO -n> IT) -n> IT := + λne l k, Vis (E:=E) (subEff_opid opid_del) + (subEff_ins (F:=prngE) (op:=opid_del) l) + (NextO ◎ k ◎ (subEff_outs (op:=opid_del) ^-1)). + Solve Obligations with solve_proper. + Definition PRNG_DEL := λne l, PRNG_DEL_k l Ret. - Program Definition PRNG_GEN : locO -n> IT := - λne l, Vis (E:=E) (subEff_opid $ opid_gen) - (subEff_ins (F:=prngE) (op:=opid_gen) l) - (NextO ◎ Ret ◎ (subEff_outs ^-1)). + Program Definition PRNG_GEN_k : locO -n> (natO -n> IT) -n> IT := + λne l k, Vis (E:=E) (subEff_opid $ opid_gen) + (subEff_ins (F:=prngE) (op:=opid_gen) l) + (NextO ◎ k ◎ (subEff_outs (op:=opid_gen)^-1)). + Solve Obligations with solve_proper. + Definition PRNG_GEN := λne l, PRNG_GEN_k l Ret. - Program Definition PRNG_SEED : locO -n> natO -n> IT := - λne l n, Vis (E:=E) (subEff_opid $ opid_seed) - (subEff_ins (F:=prngE) (op:=opid_seed) (l, n)) - (λne _, Next (Ret ())). + Program Definition PRNG_SEED_k : locO -n> natO -n> (unitO -n> IT) -n> IT := + λne l n k, Vis (E:=E) (subEff_opid $ opid_seed) + (subEff_ins (F:=prngE) (op:=opid_seed) (l, n)) + (NextO ◎ k ◎ (subEff_outs (op:=opid_seed) ^-1)). + Solve Obligations with solve_proper. + Definition PRNG_SEED := λne l n, PRNG_SEED_k l n Ret. - Lemma hom_NEW k f `{!IT_hom f} : f (PRNG_NEW k) ≡ PRNG_NEW (OfeMor f ◎ k). - Proof. - unfold PRNG_NEW. - rewrite hom_vis/=. repeat f_equiv. - intro x. cbn-[laterO_map]. rewrite laterO_map_Next. + Ltac solve_hom_easy symbol := + unfold symbol; + rewrite hom_vis/=; repeat f_equiv; + intro x; cbn-[laterO_map]; rewrite laterO_map_Next; done. - Qed. + + Lemma hom_NEW k f `{!IT_hom f} : f (PRNG_NEW k) ≡ PRNG_NEW (OfeMor f ◎ k). + Proof. solve_hom_easy PRNG_NEW. Qed. + + Lemma hom_DEL_k l k f `{!IT_hom f} : f (PRNG_DEL_k l k) ≡ PRNG_DEL_k l (OfeMor f ◎ k). + Proof. solve_hom_easy PRNG_DEL_k. Qed. + + Lemma hom_GEN_k l k f `{!IT_hom f} : f (PRNG_GEN_k l k) ≡ PRNG_GEN_k l (OfeMor f ◎ k). + Proof. solve_hom_easy PRNG_GEN_k. Qed. + + Lemma hom_SEED_k l n k f `{!IT_hom f} : f (PRNG_SEED_k l n k) ≡ PRNG_SEED_k l n (OfeMor f ◎ k). + Proof. solve_hom_easy PRNG_SEED_k. Qed. End prng_combinators. Section wp. @@ -170,7 +186,6 @@ Section wp. Notation ITV := (ITV F R). Notation stateO := (stateF ♯ IT). - (* TODO: what exactly is this CMRA? Can we get rid of the authoratative RA? *) Definition istate := gmap_viewR loc natO. Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ istate }. Class prngG Σ := PrngG { @@ -257,33 +272,34 @@ Section wp. done. Qed. - (* TODO: Piecing together proofs in [store.v]. Review the proof. Understand the mask changes. *) - Lemma wp_gen_hom (l : loc) (n : nat) s Φ (κ : IT -n> IT) `{!IT_hom κ} : + + Lemma wp_new_hom (k : locO -n> IT) s Φ `{!NonExpansive Φ} (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} κ (Ret $ read_lcg n) @ s {{ Φ }}) -∗ - WP@{rs} κ (PRNG_GEN l) @ s {{ Φ }}. + ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} κ (k l) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_NEW k) @ s {{ Φ }}. Proof. - iIntros "#Hctx Hp Ha". - unfold PRNG_GEN; simpl. + iIntros "#Hctx Ha". + unfold PRNG_NEW; simpl. rewrite hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". simpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. + set (l:=Loc.fresh (dom σ)). (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,(read_lcg n),(<[l:=update_lcg n]>σ),(κ (Ret $ read_lcg n)),[]. + iExists σ,l,(<[l:=0]>σ),(κ $ k l),[]. iFrame "Hs". - iSplit. + iSplit; first done. + iSplit; first by rewrite later_map_Next ofe_iso_21. + iNext. + iMod (istate_alloc 0 l with "Hh") as "[Hh Hp]". { - iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". - unfold lift_post, state_gen. - by rewrite Hread. + apply (not_elem_of_dom_1 (M:=gmap loc)). + rewrite -(Loc.add_0 l). + apply Loc.fresh_fresh. + lia. } - iSplit; first by rewrite ofe_iso_21 later_map_Next. - iNext. - iMod (istate_write l n (update_lcg n) σ with "Hh Hp") as "[Hh Hp]". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } @@ -293,42 +309,44 @@ Section wp. - by iFrame. Qed. - Lemma wp_gen (l : loc) (n : nat) s Φ : + Lemma wp_new (k : locO -n> IT) s Φ `{!NonExpansive Φ} : prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷ ▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} (Ret $ read_lcg n) @ s {{ Φ }}) -∗ - WP@{rs} PRNG_GEN l @ s {{ Φ }}. + ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} k l @ s {{ Φ }}) -∗ + WP@{rs} PRNG_NEW k @ s {{ Φ }}. Proof. - iIntros "#Hcxt Hp Ha". - iApply (wp_gen_hom _ _ _ _ idfun with "Hcxt Hp Ha"). + iIntros "Hh H". + iApply (wp_new_hom _ _ _ idfun with "Hh H"). Qed. - Lemma wp_seed_hom (l : loc) (n n' : nat) s Φ (κ : IT -n> IT) `{!IT_hom κ} : + Lemma wp_del_k_hom (l : loc) (cont : unitO -n> IT) n s Φ (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ ▷ has_prng_state l n -∗ - ▷▷ (has_prng_state l n' -∗ WP@{rs} κ (Ret ()) @ s {{ Φ }}) -∗ - WP@{rs} κ (PRNG_SEED l n') @ s {{ Φ }}. + ▷▷ WP@{rs} κ (cont ()) @ s {{ β, Φ β }} -∗ + WP@{rs} κ (PRNG_DEL_k l cont) @ s {{ Φ }}. Proof. iIntros "#Hctx Hp Ha". - unfold PRNG_SEED; simpl. + unfold PRNG_DEL_k; simpl. rewrite hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". simpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. + iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom". + { iApply (istate_loc_dom with "Hh Hp"). } + destruct Hdom as [x Hx]. (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,(),(<[l:=n']>σ),(κ (Ret ())),[]. + iExists σ,(),(delete l σ),(κ $ cont ()),[]. iFrame "Hs". iSplit. { iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". - unfold lift_post, state_seed. + unfold lift_post, state_del. by rewrite Hread. } - iSplit; first by rewrite later_map_Next. + iSplit; first by rewrite later_map_Next ofe_iso_21. iNext. - iMod (istate_write l n n' σ with "Hh Hp") as "[Hh Hp]". + iMod (istate_delete l n σ with "Hh Hp") as "Hh". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } @@ -338,49 +356,45 @@ Section wp. - by iFrame. Qed. - Lemma wp_seed (l : loc) (n n' : nat) s Φ : + Lemma wp_del (l : loc) n s Φ : prng_ctx -∗ ▷ has_prng_state l n -∗ - ▷▷ (has_prng_state l n' -∗ Φ (RetV ())) -∗ - WP@{rs} PRNG_SEED l n' @ s {{ Φ }}. + ▷ ▷ Φ (RetV ()) -∗ + WP@{rs} PRNG_DEL l @ s {{ Φ }}. Proof. - iIntros "#Hctx Hp Ha". - iApply (wp_seed_hom _ _ _ _ _ idfun with "Hctx Hp [Ha]"). + iIntros "#Hctx Hl H". + iApply (wp_del_k_hom _ _ _ _ _ idfun with "Hctx Hl [H]"). do 2 iNext. - iIntros "H". - iDestruct ("Ha" with "H") as "G". iApply wp_val. - by iModIntro. + iModIntro. done. Qed. - Lemma wp_new_hom (k : locO -n> IT) s Φ `{!NonExpansive Φ} - (κ : IT -n> IT) `{!IT_hom κ} : + Lemma wp_gen_k_hom (l : loc) (cont : natO -n> IT) n s Φ (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ - ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} κ (k l) @ s {{ Φ }}) -∗ - WP@{rs} κ (PRNG_NEW k) @ s {{ Φ }}. + ▷ has_prng_state l n -∗ + ▷▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} κ (cont $ read_lcg n) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_GEN_k l cont) @ s {{ Φ }}. Proof. - iIntros "#Hctx Ha". - unfold PRNG_NEW; simpl. + iIntros "#Hctx Hp Ha". + unfold PRNG_GEN_k; simpl. rewrite hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". simpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. - set (l:=Loc.fresh (dom σ)). (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,l,(<[l:=0]>σ),(κ $ k l),[]. + iExists σ,(read_lcg n),(<[l:=update_lcg n]>σ),(κ (cont $ read_lcg n)),[]. iFrame "Hs". - iSplit; first done. - iSplit; first by rewrite later_map_Next ofe_iso_21. - iNext. - iMod (istate_alloc 0 l with "Hh") as "[Hh Hp]". + iSplit. { - apply (not_elem_of_dom_1 (M:=gmap loc)). - rewrite -(Loc.add_0 l). - apply Loc.fresh_fresh. - lia. + iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". + unfold lift_post, state_gen. + by rewrite Hread. } + iSplit; first by rewrite ofe_iso_21 later_map_Next. + iNext. + iMod (istate_write l n (update_lcg n) σ with "Hh Hp") as "[Hh Hp]". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } @@ -390,44 +404,42 @@ Section wp. - by iFrame. Qed. - Lemma wp_new (k : locO -n> IT) s Φ `{!NonExpansive Φ} : + Lemma wp_gen (l : loc) (n : nat) s Φ : prng_ctx -∗ - ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} k l @ s {{ Φ }}) -∗ - WP@{rs} PRNG_NEW k @ s {{ Φ }}. + ▷ has_prng_state l n -∗ + ▷ ▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} (Ret $ read_lcg n) @ s {{ Φ }}) -∗ + WP@{rs} PRNG_GEN l @ s {{ Φ }}. Proof. - iIntros "Hh H". - iApply (wp_new_hom _ _ _ idfun with "Hh H"). + iIntros "#Hcxt Hp Ha". + iApply (wp_gen_k_hom l Ret _ _ _ idfun with "Hcxt Hp Ha"). Qed. - Lemma wp_del_hom (l : loc) n s Φ (κ : IT -n> IT) `{!IT_hom κ} : + Lemma wp_seed_k_hom (l : loc) n (cont : unitO -n> IT) n' s Φ (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ ▷ has_prng_state l n -∗ - ▷ ▷ WP@{rs} κ (Ret ()) @ s {{ β, Φ β }} -∗ - WP@{rs} κ (PRNG_DEL l) @ s {{ Φ }}. + ▷▷ (has_prng_state l n' -∗ WP@{rs} κ (cont ()) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_SEED_k l n' cont) @ s {{ Φ }}. Proof. iIntros "#Hctx Hp Ha". - unfold PRNG_DEL; simpl. + unfold PRNG_SEED_k; simpl. rewrite hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". simpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. - iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom". - { iApply (istate_loc_dom with "Hh Hp"). } - destruct Hdom as [x Hx]. (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,(),(delete l σ),(κ $ Ret ()),[]. + iExists σ,(),(<[l:=n']>σ),(κ (cont ())),[]. iFrame "Hs". iSplit. { iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". - unfold lift_post, state_del. + unfold lift_post, state_seed. by rewrite Hread. } - iSplit; first by rewrite later_map_Next. + iSplit; first by rewrite ofe_iso_21 later_map_Next. iNext. - iMod (istate_delete l n σ with "Hh Hp") as "Hh". + iMod (istate_write l n n' σ with "Hh Hp") as "[Hh Hp]". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } @@ -437,21 +449,24 @@ Section wp. - by iFrame. Qed. - Lemma wp_del (l : loc) n s Φ : + Lemma wp_seed (l : loc) n n' s Φ : prng_ctx -∗ ▷ has_prng_state l n -∗ - ▷ ▷ Φ (RetV ()) -∗ - WP@{rs} PRNG_DEL l @ s {{ Φ }}. + ▷▷ (has_prng_state l n' -∗ Φ (RetV ())) -∗ + WP@{rs} PRNG_SEED l n' @ s {{ Φ }}. Proof. - iIntros "#Hctx Hl H". - iApply (wp_del_hom _ _ _ _ idfun with "Hctx Hl [H]"). + iIntros "#Hctx Hp Ha". + iApply (wp_seed_k_hom l n Ret _ _ _ idfun with "Hctx Hp [Ha]"). do 2 iNext. + iIntros "H". + iDestruct ("Ha" with "H") as "G". iApply wp_val. - iModIntro. done. + by iModIntro. Qed. + End wp. Arguments prng_ctx {_ _} rs {_ _ _ _ _ _}. Arguments has_prng_state {_ _} _ _. -#[global] Opaque PRNG_NEW PRNG_DEL PRNG_GEN PRNG_SEED. +#[global] Opaque PRNG_NEW PRNG_DEL_k PRNG_GEN_k PRNG_SEED_k. From 4d898cbbc5f893fc141fe8ef2a5c1d96e5959f9f Mon Sep 17 00:00:00 2001 From: hehelego Date: Sat, 4 Apr 2026 12:05:23 +0200 Subject: [PATCH 06/21] fix PRNG SEED unfold tick counting --- theories/examples/prng_lang/lang.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v index d858023..28a97f3 100644 --- a/theories/examples/prng_lang/lang.v +++ b/theories/examples/prng_lang/lang.v @@ -326,7 +326,7 @@ Inductive head_step {S} : expr S → state → expr S → state → nat*nat → head_step (Rand $ Val $ LitPrng l) σ (Val $ LitV n) σ' (1,1) | SeedS σ l n σ' : state_seed σ l n = Some ((), σ') → - head_step (Seed (Val $ LitPrng l) (Val $ LitV n)) σ (Val $ UnitV) σ' (1,1) + head_step (Seed (Val $ LitPrng l) (Val $ LitV n)) σ (Val $ UnitV) σ' (3,1) | IfTrueS n e1 e2 σ : n > 0 → head_step (If (Val (LitV n)) e1 e2) σ @@ -345,7 +345,7 @@ Lemma head_step_prng_01 {S} (e1 e2 : expr S) σ1 σ2 n m : head_step e1 σ1 e2 σ2 (n,m) → m = 0 ∨ m = 1. Proof. inversion 1; eauto. Qed. Lemma head_step_unfold_01 {S} (e1 e2 : expr S) σ1 σ2 n m : - head_step e1 σ1 e2 σ2 (n,m) → n = 0 ∨ n = 1. + head_step e1 σ1 e2 σ2 (n,m) → n = 0 ∨ n = 1 ∨ n = 3. Proof. inversion 1; eauto. Qed. Lemma head_step_pure {S} (e1 e2 : expr S) σ1 σ2 n : head_step e1 σ1 e2 σ2 (n,0) → σ1 = σ2. From 438b309d2f564dc2028e57c2773245ac1b1ebcda Mon Sep 17 00:00:00 2001 From: hehelego Date: Thu, 2 Apr 2026 17:17:06 +0200 Subject: [PATCH 07/21] WIP: denotational interpretation of PRNG lang --- theories/examples/prng_lang/interp.v | 768 +++++++++++++++++++++++++++ 1 file changed, 768 insertions(+) diff --git a/theories/examples/prng_lang/interp.v b/theories/examples/prng_lang/interp.v index e69de29..257cef8 100644 --- a/theories/examples/prng_lang/interp.v +++ b/theories/examples/prng_lang/interp.v @@ -0,0 +1,768 @@ +From gitrees Require Import gitree lang_generic. +From gitrees.effects Require Export prng. +From gitrees.examples.prng_lang Require Import lang. + +Require Import Binding.Lib Binding.Set. + +Section interp. + Context {sz : nat}. + Variable (rs : gReifiers NotCtxDep sz). + Context {subR : subReifier reify_prng rs}. + Context {R} `{CR : !Cofe R}. + Context `{!SubOfe natO R} `{!SubOfe locO R} `{!SubOfe unitO R}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + + Global Instance denot_cont_ne (κ : IT -n> IT) : + NonExpansive (λ x : IT, Tau (laterO_map κ (Next x))). + Proof. + solve_proper. + Qed. + + (** Interpreting individual operators *) + (* TODO: these interpretation might be unsound. + Problems with evaluation order. + Problems with "going under Tau/Vis constructor" + *) + Program Definition interp_new {A} : A -n> IT := + λne env, PRNG_NEW Ret. + Program Definition interp_del {A} (l : A -n> IT) : A -n> IT := + λne env, get_ret PRNG_DEL (l env). + Program Definition interp_rand {A} (l : A -n> IT) : A -n> IT := + λne env, get_ret (PRNG_GEN) (l env). + + Program Definition SEED_FUN : IT -n> IT -n> IT := + λne s, get_ret (λne vLoc : locO, get_ret (PRNG_SEED vLoc) s). + Solve All Obligations with solve_proper_please. + Program Definition SEED_IT : IT := λit s l, SEED_FUN s l. + Solve All Obligations with solve_proper_please. + + (* NOTE: + 1. The interpretation should be a homomorphism in both arguments. + 2. The PRNG location should be evaluated first. + + APP is left-associative. + *) + Program Definition interp_seed {A} (l s : A -n> IT) : A -n> IT := + λne env, SEED_IT ⊙ (s env) ⊙ (l env). + Solve All Obligations with solve_proper_please. + + Lemma seed_it_app_ret_ret (l : locO) (s : natO) : + SEED_IT ⊙ (Ret s) ⊙ (Ret l) ≡ Tick_n 2 $ PRNG_SEED l s. + Proof. + rewrite (APP'_Ret_r (SEED_IT ⊙ (Ret s))). + rewrite (APP'_Ret_r SEED_IT). + rewrite APP_Fun. + rewrite APP_Tick. + rewrite APP_Fun. + simpl. + f_equiv. + rewrite get_ret_ret. + simpl. + rewrite get_ret_ret. + simpl. + done. + Qed. + + Program Definition interp_natop {A} (op : nat_op) (t1 t2 : A -n> IT) : A -n> IT := + λne env, NATOP (do_natop op) (t1 env) (t2 env). + Solve All Obligations with solve_proper_please. + + Global Instance interp_natop_ne A op : NonExpansive2 (@interp_natop A op). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_natop. + + Opaque laterO_map. + Program Definition interp_rec_pre {S : Set} (body : interp_scope (inc (inc S)) -n> IT) + : laterO (interp_scope S -n> IT) -n> interp_scope S -n> IT := + λne self env, Fun $ laterO_map (λne (self : interp_scope S -n> IT) (a : IT), + body (extend_scope (extend_scope env (self env)) a)) self. + Next Obligation. + intros. + solve_proper_prepare. + f_equiv; intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros ??????? H. + solve_proper_prepare. + f_equiv; intros [| [| y']]; simpl; [done | apply H | done]. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + f_equiv. + apply laterO_map_ne. + intros ??; simpl; f_equiv; + intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + by do 2 f_equiv. + Qed. + + Program Definition interp_rec {S : Set} + (body : interp_scope (inc (inc S)) -n> IT) : + interp_scope S -n> IT := + mmuu (interp_rec_pre body). + + Program Definition ir_unf {S : Set} + (body : interp_scope (inc (inc S)) -n> IT) env : IT -n> IT := + λne a, body (extend_scope + (extend_scope env (interp_rec body env)) + a). + Next Obligation. + intros. + solve_proper_prepare. + f_equiv. intros [| [| y']]; simpl; solve_proper. + Qed. + + Lemma interp_rec_unfold {S : Set} (body : interp_scope (inc (inc S)) -n> IT) env : + interp_rec body env ≡ Fun $ Next $ ir_unf body env. + Proof. + trans (interp_rec_pre body (Next (interp_rec body)) env). + { f_equiv. rewrite /interp_rec. apply mmuu_unfold. } + simpl. rewrite laterO_map_Next. repeat f_equiv. + simpl. unfold ir_unf. intro. simpl. reflexivity. + Qed. + + Program Definition interp_app {A} (t1 t2 : A -n> IT) : A -n> IT := + λne env, APP' (t1 env) (t2 env). + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + Global Instance interp_app_ne A : NonExpansive2 (@interp_app A). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_app. + + Program Definition interp_if {A} (t0 t1 t2 : A -n> IT) : A -n> IT := + λne env, IF_nat.IF (t0 env) (t1 env) (t2 env). + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + Global Instance interp_if_ne A n : + Proper ((dist n) ==> (dist n) ==> (dist n) ==> (dist n)) (@interp_if A). + Proof. solve_proper. Qed. + + Program Definition interp_unit {A} : A -n> IT := + λne env, Ret (). + Program Definition interp_nat (n : nat) {A} : A -n> IT := + λne env, Ret n. + Program Definition interp_loc (l : loc) {A} : A -n> IT := + λne env, Ret l. + + Program Definition interp_applk {A} + (K : A -n> (IT -n> IT)) + (q : A -n> IT) + : A -n> (IT -n> IT) := + λne env t, interp_app (λne env, K env t) q env. + Solve All Obligations with solve_proper. + + Program Definition interp_apprk {A} + (q : A -n> IT) + (K : A -n> (IT -n> IT)) + : A -n> (IT -n> IT) := + λne env t, interp_app q (λne env, K env t) env. + Solve All Obligations with solve_proper. + + Program Definition interp_natoprk {A} (op : nat_op) + (q : A -n> IT) + (K : A -n> (IT -n> IT)) : A -n> (IT -n> IT) := + λne env t, interp_natop op q (λne env, K env t) env. + Solve All Obligations with solve_proper. + + Program Definition interp_natoplk {A} (op : nat_op) + (K : A -n> (IT -n> IT)) + (q : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_natop op (λne env, K env t) q env. + Solve All Obligations with solve_proper. + + Program Definition interp_ifk {A} (K : A -n> (IT -n> IT)) (q : A -n> IT) + (p : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_if (λne env, K env t) q p env. + Solve All Obligations with solve_proper. + + + Program Definition interp_delk {A} (K : A -n> (IT -n> IT)) : A -n> (IT -n> IT) := + λne env t, interp_del (λne env, K env t) env. + Program Definition interp_seedkl {A} (K : A -n> (IT -n> IT)) (eSeed : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_seed (λne env, K env t) eSeed env. + Program Definition interp_seedks {A} (vprng : A -n> IT) (K : A -n> (IT -n> IT)) : A -n> (IT -n> IT) := + λne env t, interp_seed vprng (λne env, K env t) env. + Program Definition interp_randk {A} (K : A -n> (IT -n> IT)) : A -n> (IT -n> IT) := + λne env t, interp_rand (λne env, K env t) env. + Solve All Obligations with solve_proper_please. + + + (** Interpretation for all the syntactic categories: values, expressions, contexts *) + Fixpoint interp_val {S} (v : val S) : interp_scope S -n> IT := + match v with + | UnitV => interp_unit + | LitV n => interp_nat n + | LitPrng l => interp_loc l + | RecV e => interp_rec (interp_expr e) + end + with interp_expr {S} (e : expr S) : interp_scope S -n> IT := + match e with + | Val v => interp_val v + | Var x => interp_var x + | App e1 e2 => interp_app (interp_expr e1) (interp_expr e2) + | NatOp op e1 e2 => interp_natop op (interp_expr e1) (interp_expr e2) + | If e e1 e2 => interp_if (interp_expr e) (interp_expr e1) (interp_expr e2) + | NewPrng => interp_new + | DelPrng e => interp_del (interp_expr e) + | Seed el es => interp_seed (interp_expr el) (interp_expr es) + | Rand e => interp_rand (interp_expr e) + end. + Fixpoint interp_ectx {S} (K : ectx S) : interp_scope S -n> (IT -n> IT) := + match K with + | EmptyK => λne env, idfun + | AppRK e1 K => interp_apprk (interp_expr e1) (interp_ectx K) + | AppLK K v2 => interp_applk (interp_ectx K) (interp_val v2) + | NatOpRK op e1 K => interp_natoprk op (interp_expr e1) (interp_ectx K) + | NatOpLK op K v2 => interp_natoplk op (interp_ectx K) (interp_val v2) + | IfK K e1 e2 => interp_ifk (interp_ectx K) (interp_expr e1) (interp_expr e2) + | DelPrngK K => interp_delk (interp_ectx K) + | SeedKl K es => interp_seedkl (interp_ectx K) (interp_expr es) + | SeedKs vl K => interp_seedks (interp_val vl) (interp_ectx K) + | RandK K => interp_randk (interp_ectx K) + end. + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + + Global Instance interp_val_asval {S} {D : interp_scope S} (v : val S) + : AsVal (interp_val v D). + Proof. + destruct v; simpl. + - apply _. + - apply _. + - apply _. + - rewrite interp_rec_unfold. apply _. + Qed. + + Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) := + fun f g => ∀ x, f x = g x. + + Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) := + fun n => fun f g => ∀ x, f x ≡{n}≡ g x. + + Global Instance ren_scope_proper {S S'} : + Proper ((≡) ==> (≡) ==> (≡)) (@ren_scope F _ CR S S'). + Proof. + intros D D' HE s1 s2 Hs. + intros x; simpl. + f_equiv. + - apply Hs. + - apply HE. + Qed. + + Lemma interp_expr_ren {S S'} env + (δ : S [→] S') (e : expr S) : + interp_expr (fmap δ e) env ≡ interp_expr e (ren_scope δ env) + with interp_val_ren {S S'} env + (δ : S [→] S') (e : val S) : + interp_val (fmap δ e) env ≡ interp_val e (ren_scope δ env) + with interp_ectx_ren {S S'} env + (δ : S [→] S') (e : ectx S) : + interp_ectx (fmap δ e) env ≡ interp_ectx e (ren_scope δ env). + Proof. + - destruct e; simpl. + + by apply interp_val_ren. + + reflexivity. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + - destruct e; simpl. + + reflexivity. + + reflexivity. + + reflexivity. + + clear -interp_expr_ren. + apply bi.siProp.internal_eq_soundness. + iLöb as "IH". + rewrite {2}interp_rec_unfold. + rewrite {2}(interp_rec_unfold (interp_expr e)). + do 1 iApply f_equivI. iNext. + iApply internal_eq_pointwise. + rewrite /ir_unf. iIntros (x). simpl. + rewrite interp_expr_ren. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (y'). + destruct y' as [| [| y]]; simpl; first done. + * by iRewrite - "IH". + * done. + - destruct e; simpl; intros ?; simpl. + + reflexivity. + + repeat f_equiv; by apply interp_ectx_ren. + + repeat f_equiv; [by apply interp_expr_ren | by apply interp_ectx_ren]. + + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_val_ren]. + + repeat f_equiv; by apply interp_ectx_ren. + + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_expr_ren | by apply interp_expr_ren]. + + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_val_ren]. + + repeat f_equiv; [by apply interp_expr_ren | by apply interp_ectx_ren]. + + repeat f_equiv; [by apply interp_expr_ren | by apply interp_ectx_ren]. + + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_val_ren]. + Qed. + + Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : ectx S): + interp_expr (fill K e) env ≡ (interp_ectx K) env ((interp_expr e) env). + Proof. + revert env. + induction K; simpl; intros env; first reflexivity; try (by rewrite IHK). + Qed. + + Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') + : interp_scope S := λne x, interp_expr (δ x) env. + + Global Instance SubEquiv {A B : Set} : Equiv (A [⇒] B) := fun f g => ∀ x, f x = g x. + + Global Instance sub_scope_proper {S S'} : + Proper ((≡) ==> (≡) ==> (≡)) (@sub_scope S S'). + Proof. + intros D D' HE s1 s2 Hs. + intros x; simpl. + f_equiv. + - f_equiv. + apply HE. + - apply Hs. + Qed. + + Lemma interp_expr_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_expr (bind δ e) env ≡ interp_expr e (sub_scope δ env) + with interp_val_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env) + with interp_ectx_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_ectx (bind δ e) env ≡ interp_ectx e (sub_scope δ env). + Proof. + - destruct e; simpl. + + by apply interp_val_subst. + + term_simpl. + reflexivity. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + f_equiv. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + - destruct e; simpl. + + reflexivity. + + reflexivity. + + reflexivity. + + clear -interp_expr_subst. + apply bi.siProp.internal_eq_soundness. + iLöb as "IH". + rewrite {2}interp_rec_unfold. + rewrite {2}(interp_rec_unfold (interp_expr e)). + do 1 iApply f_equivI. iNext. + iApply internal_eq_pointwise. + rewrite /ir_unf. iIntros (x). simpl. + rewrite interp_expr_subst. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (y'). + destruct y' as [| [| y]]; simpl; first done. + * by iRewrite - "IH". + * do 2 rewrite interp_expr_ren. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (z). + done. + - destruct e; simpl; intros ?; simpl. + + reflexivity. + + repeat f_equiv; by apply interp_ectx_subst. + + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst]. + + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. + + repeat f_equiv; by apply interp_ectx_subst. + + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_expr_subst | by apply interp_expr_subst]. + + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. + + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst]. + + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst]. + + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. + Qed. + + (** ** Interpretation of evaluation contexts induces homomorphism *) + + #[local] Instance interp_ectx_hom_emp {S} env : + IT_hom (interp_ectx (EmptyK : ectx S) env). + Proof. + simple refine (IT_HOM _ _ _ _ _); intros; auto. + simpl. fold (@idfun IT). f_equiv. intro. simpl. + by rewrite laterO_map_id. + Qed. + + + #[local] Instance interp_ectx_hom_del {S} (K : ectx S) env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (DelPrngK K) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. + f_equiv. intro. simpl. rewrite -laterO_map_compose. + do 2 f_equiv. by intro. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_ectx_hom_rand {S} (K : ectx S) env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (RandK K) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. + f_equiv. intro. simpl. rewrite -laterO_map_compose. + do 2 f_equiv. by intro. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_ectx_hom_seedkl {S} (K : ectx S) (eSeed : expr S) env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (SeedKl K eSeed) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. + f_equiv. intro. simpl. rewrite -laterO_map_compose. + do 2 f_equiv. by intro. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_ectx_hom_seedks {S} (vprng : val S) (K : ectx S) env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (SeedKs vprng K) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite !hom_tick. + erewrite APP'_Tick_l; first done. + by apply interp_val_asval. + - rewrite hom_vis. + rewrite APP'_Vis_r. + rewrite APP'_Vis_l. + f_equiv. + intros ?. simpl. by rewrite -laterO_map_compose. + - rewrite hom_err. + rewrite APP'_Err_r. + rewrite APP'_Err_l. + done. + Qed. + + + #[local] Instance interp_ectx_hom_if {S} + (K : ectx S) (e1 e2 : expr S) env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (IfK K e1 e2) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite -IF_nat.IF_Tick. f_equiv. apply hom_tick. + - assert ((interp_ectx K env (Vis op i ko)) ≡ + (Vis op i (laterO_map (λne y, interp_ectx K env y) ◎ ko))). + { by rewrite hom_vis. } + trans (IF_nat.IF (Vis op i (laterO_map (λne y : IT, interp_ectx K env y) ◎ ko)) + (interp_expr e1 env) (interp_expr e2 env)). + { f_equiv. by rewrite hom_vis. } + rewrite IF_nat.IF_Vis. f_equiv. simpl. + intro. simpl. by rewrite -laterO_map_compose. + - trans (IF_nat.IF (Err e) (interp_expr e1 env) (interp_expr e2 env)). + { repeat f_equiv. apply hom_err. } + apply IF_nat.IF_Err. + Qed. + + #[local] Instance interp_ectx_hom_appr {S} (K : ectx S) + (e : expr S) env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (AppRK e K) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. f_equiv. intro x. simpl. + by rewrite laterO_map_compose. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_ectx_hom_appl {S} (K : ectx S) + (v : val S) (env : interp_scope S) : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (AppLK K v) env). + Proof. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite -APP'_Tick_l. f_equiv. apply hom_tick. + - trans (APP' (Vis op i (laterO_map (interp_ectx K env) ◎ ko)) + (interp_val v env)). + + f_equiv. rewrite hom_vis. do 3 f_equiv. by intro. + + rewrite APP'_Vis_l. f_equiv. intro x. simpl. + by rewrite -laterO_map_compose. + - trans (APP' (Err e) (interp_val v env)). + { f_equiv. apply hom_err. } + apply APP'_Err_l, interp_val_asval. + Qed. + + #[local] Instance interp_ectx_hom_natopr {S} (K : ectx S) + (e : expr S) op env : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (NatOpRK op e K) env). + Proof. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. f_equiv. intro x. simpl. + by rewrite laterO_map_compose. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_ectx_hom_natopl {S} (K : ectx S) + (v : val S) op (env : interp_scope S) : + IT_hom (interp_ectx K env) -> + IT_hom (interp_ectx (NatOpLK op K v) env). + Proof. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite -NATOP_ITV_Tick_l. f_equiv. apply hom_tick. + - trans (NATOP (do_natop op) + (Vis op0 i (laterO_map (interp_ectx K env) ◎ ko)) + (interp_val v env)). + { f_equiv. rewrite hom_vis. f_equiv. by intro. } + rewrite NATOP_ITV_Vis_l. f_equiv. intro x. simpl. + by rewrite -laterO_map_compose. + - trans (NATOP (do_natop op) (Err e) (interp_val v env)). + + f_equiv. apply hom_err. + + by apply NATOP_Err_l, interp_val_asval. + Qed. + + #[global] Instance interp_ectx_hom {S} (K : ectx S) env : + IT_hom (interp_ectx K env). + Proof. + induction K; apply _. + Qed. + + (** ** Finally, preservation of reductions *) + Lemma interp_expr_head_step {S : Set} (env : interp_scope S) (e : expr S) e' σ σ' n : + head_step e σ e' σ' (n, 0) → + interp_expr e env ≡ Tick_n n $ interp_expr e' env. + Proof. + inversion 1; cbn-[IF_nat.IF APP' Tick]. + - (* app lemma *) + subst. + erewrite APP_APP'_ITV; last apply _. + trans (APP (Fun (Next (ir_unf (interp_expr e1) env))) (Next $ interp_val v2 env)). + { repeat f_equiv. apply interp_rec_unfold. } + rewrite APP_Fun. simpl. rewrite Tick_eq. do 2 f_equiv. + simplify_eq. + rewrite !interp_expr_subst. + f_equiv. + intros [| [| x]]; simpl; [| reflexivity | reflexivity]. + rewrite interp_val_ren. + f_equiv. + intros ?; simpl; reflexivity. + - rewrite IF_nat.IF_True; last lia. + reflexivity. + - rewrite IF_nat.IF_False; last lia. + reflexivity. + - (* the natop stuff *) + simplify_eq. + destruct v1,v2; try naive_solver. simpl in *. + rewrite NATOP_Ret. + destruct op; simplify_eq/=; done. + Qed. + + Lemma interp_expr_fill_no_reify {S} K (env : interp_scope S) (e e' : expr S) σ σ' n : + head_step e σ e' σ' (n, 0) → + interp_expr (fill K e) env + ≡ + Tick_n n $ interp_expr (fill K e') env. + Proof. + intros He. + rewrite !interp_comp. + erewrite <-hom_tick_n. + - apply (interp_expr_head_step env) in He. + rewrite He. + reflexivity. + - apply _. + Qed. + + Opaque PRNG_NEW PRNG_DEL PRNG_SEED PRNG_GEN. + Opaque extend_scope. + Opaque Ret. + + (* from [prng.v] *) + Notation opid_new := (inl ()). + Notation opid_del := (inr opid_new). + Notation opid_gen := (inr opid_del). + Notation opid_seed := (inr opid_gen). + + (* TODO: streamline the repetitive proof script *) + Lemma interp_expr_fill_yes_reify {S} K env (e e' : expr S) + (σ σ' : stateO) (σr : gState_rest sR_idx rs ♯ IT) n : + head_step e σ e' σ' (n, 1) → + reify (gReifiers_sReifier rs) + (interp_expr (fill K e) env) (gState_recomp σr (sR_state σ)) + ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env, []). + Proof. + intros Hst. + trans (reify (gReifiers_sReifier rs) (interp_ectx K env (interp_expr e env)) + (gState_recomp σr (sR_state σ))). + { f_equiv. by rewrite interp_comp. } + inversion Hst; simplify_eq; cbn-[gState_recomp]. + - trans (reify (gReifiers_sReifier rs) (PRNG_NEW (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). + { + repeat f_equiv; eauto. + rewrite hom_NEW. + do 2 f_equiv. by intro. + } + rewrite reify_vis_eq_ctx_indep //; first last. + { + epose proof (@subReifier_reify sz NotCtxDep reify_prng rs _ IT _ opid_new () l σ σ' σr []) as H. + simpl in H. + simpl. + erewrite <-H; last first. + - unfold state_new in H4. + inversion H4. + reflexivity. + - f_equiv; + solve_proper. + } + repeat f_equiv; last done. rewrite Tick_eq/=. repeat f_equiv. + rewrite interp_comp. + rewrite ofe_iso_21. + simpl. + reflexivity. + - trans (reify (gReifiers_sReifier rs) (PRNG_DEL_k l (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). + { + repeat f_equiv. + rewrite get_ret_ret. + rewrite hom_DEL_k. + f_equiv; f_equiv. + by intro. + } + rewrite reify_vis_eq_ctx_indep //; last first. + { + epose proof (@subReifier_reify sz NotCtxDep reify_prng rs _ IT _ opid_del l () σ σ' σr []) as H. + simpl in H. + rewrite H4 in H. + simpl. + erewrite <-H; last reflexivity. + f_equiv. + } + repeat f_equiv; last done. rewrite Tick_eq/=. repeat f_equiv. + rewrite interp_comp. + by rewrite ofe_iso_21. + - trans (reify (gReifiers_sReifier rs) (PRNG_GEN_k l (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). + { + repeat f_equiv. + rewrite get_ret_ret. + rewrite hom_GEN_k. + f_equiv; f_equiv. + by intro. + } + rewrite reify_vis_eq_ctx_indep //; last first. + { + epose proof (@subReifier_reify sz NotCtxDep reify_prng rs _ IT _ opid_gen l n0 σ σ' σr []) as H. + simpl in H. + rewrite H4 in H. + simpl. + erewrite <-H; last reflexivity. + f_equiv. + } + repeat f_equiv; last done. rewrite Tick_eq/=. repeat f_equiv. + rewrite interp_comp. + by rewrite ofe_iso_21. + - trans (reify (gReifiers_sReifier rs) (Tick_n 2 $ PRNG_SEED_k l n0 (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). + { + f_equiv; last done; f_equiv. + rewrite seed_it_app_ret_ret. + rewrite !hom_tick. + rewrite hom_SEED_k. + simpl; do 4 f_equiv. + intro; simpl; done. + } + trans (reify (gReifiers_sReifier rs) + (PRNG_SEED_k l n0 (Tick ◎ Tick ◎ interp_ectx K env ◎ Ret)) + (gState_recomp σr (sR_state σ))). + { + do 2 f_equiv. + (* FIXME: maybe this interpretation of [Seed] does not work ?? *) + admit. + } + rewrite reify_vis_eq_ctx_indep //; last first. + { + epose proof (@subReifier_reify sz NotCtxDep reify_prng rs _ IT _ opid_seed (l,n0) () σ σ' σr []) as H. + simpl in H. + rewrite H4 in H. + simpl. + rewrite <-H; last reflexivity. + f_equiv; solve_proper. + } + repeat f_equiv; last done. rewrite Tick_eq/=. repeat f_equiv. + rewrite interp_comp. + by rewrite ofe_iso_21. + Admitted. + + Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : + prim_step e1 σ1 e2 σ2 (n,m) → + external_steps (gReifiers_sReifier rs) + (interp_expr e1 env) (gState_recomp σr (sR_state σ1)) + (interp_expr e2 env) (gState_recomp σr (sR_state σ2)) [] n. + Proof. + Opaque gState_decomp gState_recomp. + inversion 1; simplify_eq/=. + destruct (head_step_prng_01 _ _ _ _ _ _ H2); subst. + - assert (σ1 = σ2) as ->. + { eapply head_step_pure; eauto. } + unshelve eapply (interp_expr_fill_no_reify K) in H2; first apply env. + rewrite H2. + rewrite interp_comp. + eapply external_steps_tick_n. + - inversion H2; subst. + + eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. + rewrite interp_comp. + rewrite hom_NEW. + change 1 with (Nat.add 1 0). econstructor; last first. + { constructor; reflexivity. } + 2:{ rewrite app_nil_r; reflexivity. } + eapply external_step_reify. + { Transparent PRNG_NEW. unfold PRNG_NEW. simpl. + f_equiv. reflexivity. } + simpl in H2. + rewrite -H2. + repeat f_equiv; eauto. + rewrite interp_comp hom_NEW. + eauto. + + eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. + rewrite interp_comp. simpl. + rewrite get_ret_ret. + rewrite hom_DEL_k. + change 1 with (Nat.add 1 0). econstructor; last first. + { constructor; reflexivity. } + 2:{ rewrite app_nil_r; reflexivity. } + eapply external_step_reify. + { Transparent PRNG_DEL_k. unfold PRNG_DEL_k. simpl. + f_equiv. reflexivity. } + simpl in H2. + rewrite -H2. + repeat f_equiv; eauto. + Opaque PRNG_DEL_k. + rewrite interp_comp /= get_ret_ret hom_DEL_k. + eauto. + + eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. + rewrite interp_comp. simpl. + rewrite get_ret_ret. + rewrite hom_GEN_k. + change 1 with (Nat.add 1 0). econstructor; last first. + { constructor; reflexivity. } + 2:{ rewrite app_nil_r; reflexivity. } + eapply external_step_reify. + { Transparent PRNG_GEN_k. unfold PRNG_GEN_k. simpl. + f_equiv. reflexivity. } + simpl in H2. + rewrite -H2. + repeat f_equiv; eauto. + Opaque PRNG_GEN_k. + rewrite interp_comp /= get_ret_ret hom_GEN_k. + eauto. + + eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. + rewrite interp_comp. simpl. + rewrite seed_it_app_ret_ret; rewrite !Tick_n_S Tick_n_O. + Admitted. +End interp. +#[global] Opaque PRNG_NEW PRNG_DEL_k PRNG_GEN_k PRNG_SEED_k. From 82366218e1d38cfbea54ffefca5867d53779ab00 Mon Sep 17 00:00:00 2001 From: hehelego Date: Sat, 4 Apr 2026 23:01:49 +0200 Subject: [PATCH 08/21] GIT combinators for PRNG-SEED operator --- _CoqProject | 1 + .../examples/prng_lang/prng_seed_combinator.v | 148 ++++++++++++++++++ 2 files changed, 149 insertions(+) create mode 100644 theories/examples/prng_lang/prng_seed_combinator.v diff --git a/_CoqProject b/_CoqProject index 288aad2..431aa96 100644 --- a/_CoqProject +++ b/_CoqProject @@ -88,6 +88,7 @@ theories/examples/heap_lang/notation.v theories/examples/heap_lang/pretty.v theories/examples/heap_lang/tactics.v +theories/examples/prng_lang/prng_seed_combinator.v theories/examples/prng_lang/lang.v theories/examples/prng_lang/interp.v theories/examples/prng_lang/logpred.v diff --git a/theories/examples/prng_lang/prng_seed_combinator.v b/theories/examples/prng_lang/prng_seed_combinator.v new file mode 100644 index 0000000..9967c7b --- /dev/null +++ b/theories/examples/prng_lang/prng_seed_combinator.v @@ -0,0 +1,148 @@ +From iris.prelude Require Import options. +From iris.base_logic Require Import base_logic. +From gitrees Require Import prelude hom greifiers. +From gitrees.gitree Require Import core subofe reify. +From gitrees.effects Require Import prng. + +Section get_ret2_generalized. + Local Opaque laterO_ap. + Context {Σ : opsInterp}. + Context `{!Cofe A, !Cofe B, !Cofe R}. + Context `{!SubOfe A R, !SubOfe B R}. + Notation IT := (IT Σ R). + + Program Definition get_ret2 (f : A -n> B -n> IT) : IT -n> IT -n> IT := λne x y, + get_ret (λne x, get_ret (λne y, f x y) y) x. + Solve All Obligations with solve_proper_please. + Global Instance get_ret2_ne n : Proper ((dist n) ==> (dist n)) get_ret2. + Proof. + intros f1 f2 Hf. unfold get_ret2. + intros x y. simpl. apply get_ret_ne. + clear x. intros x. simpl. apply get_ret_ne. + clear y. intros y. simpl. apply Hf. + Qed. + Global Instance get_ret2_proper : Proper ((≡) ==> (≡)) get_ret2. + Proof. + intros f1 f2 Hf. unfold get_ret2. + intros x y. simpl. apply get_ret_proper. + clear x. intros x. simpl. apply get_ret_proper. + clear y. intros y. simpl. apply Hf. + Qed. +End get_ret2_generalized. + +Section prng_seed_workaround. + Context {sz : nat}. + Locate NotCtxDep. + Variable (rs : gReifiers NotCtxDep sz). + Context {subR : subReifier reify_prng rs}. + Context {R} `{CR : !Cofe R}. + Context `{!SubOfe natO R} `{!SubOfe locO R} `{!SubOfe unitO R}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + + Program Definition SeedGit_ne : IT -n> IT -n> IT := λne tloc tseed, + get_val (λne vloc, + get_val (λne vseed, + get_ret2 PRNG_SEED vloc vseed) tseed) tloc. + Solve All Obligations with solve_proper_please. + Definition SeedGit tloc tseed := SeedGit_ne tloc tseed. + Global Instance SEEDOP_Proper + : Proper ((≡) ==> (≡) ==> (≡)) (SeedGit). + Proof. rewrite /SeedGit; solve_proper_please. Qed. + Global Instance SeedGit_NonExp : NonExpansive2 (SeedGit). + Proof. rewrite /SeedGit; solve_proper_please. Qed. + + Lemma SeedGit_ErrS β e : AsVal β → SeedGit β (Err e) ≡ Err e. + Proof. + intros ?. simpl. + rewrite /SeedGit /SeedGit_ne //= get_val_ITV /= get_val_err //. + Qed. + Lemma SeedGit_ErrL e tseed : SeedGit (Err e) tseed ≡ Err e. + Proof. simpl. by rewrite /SeedGit /SeedGit_ne //= get_val_err. Qed. + Lemma SeedGit_Ret loc seed : + SeedGit (Ret loc) (Ret seed) ≡ PRNG_SEED loc seed. + Proof. + simpl. + rewrite /SeedGit /SeedGit_ne /= get_val_ret/= get_val_ret/=. + rewrite !get_ret_ret. simpl. + rewrite !get_ret_ret. simpl. + done. + Qed. + Lemma SeedGit_TickL tloc tseed: + SeedGit (Tick tloc) tseed ≡ Tick $ SeedGit tloc tseed. + Proof. + simpl. rewrite /SeedGit /SeedGit_ne /= get_val_tick//. + Qed. + Lemma SeedGit_TickL_n tloc tseed n : + SeedGit (Tick_n n tloc) tseed ≡ Tick_n n $ SeedGit tloc tseed. + Proof. + induction n; eauto. rewrite SeedGit_TickL. + rewrite IHn. done. + Qed. + Lemma SeedGit_ITV_TickS tseed β : + AsVal β → + SeedGit β (Tick tseed) ≡ Tick $ SeedGit β tseed. + Proof. + intros ?. simpl. rewrite /SeedGit /SeedGit_ne /= get_val_ITV/=. + rewrite get_val_tick. f_equiv. + rewrite get_val_ITV. done. + Qed. + Lemma SeedGit_ITV_TickS_n tseed β n : + AsVal β → + SeedGit β (Tick_n n tseed) ≡ Tick_n n $ SeedGit β tseed. + Proof. + intros Hb. + induction n; eauto. rewrite SeedGit_ITV_TickS. + rewrite IHn. done. + Qed. + Lemma SeedGit_ITV_VisS op i k β : + AsVal β → + SeedGit β (Vis op i k) ≡ + Vis op i (laterO_map (SeedGit_ne β) ◎ k). + Proof. + intros ?. simpl. rewrite /SeedGit /SeedGit_ne /= get_val_ITV/=. + rewrite get_val_vis. repeat f_equiv. + intro y. simpl. rewrite get_val_ITV//. + Qed. + Lemma SeedGit_VisL tseed op i k : + SeedGit (Vis op i k) tseed ≡ Vis op i (laterO_map (flipO SeedGit_ne tseed) ◎ k). + Proof. + simpl. rewrite /SeedGit /SeedGit_ne /= get_val_vis. f_equiv. solve_proper. + Qed. + + Opaque SeedGit. + Definition SeedGitCtxL β holeL := SeedGit holeL β. + Definition SeedGitCtxS βval holeS := SeedGit βval holeS. + + #[local] Instance SeedGitCtxL_ne (β : IT) : NonExpansive (SeedGitCtxL β). + Proof. + intro n. unfold SeedGitCtxL. + repeat intro. repeat f_equiv; eauto. + Qed. + #[local] Instance SeedGitCtxS_ne (β : IT) : NonExpansive (SeedGitCtxS β). + Proof. + intro n. unfold SeedGitCtxS. + solve_proper. + Qed. + #[export] Instance SeedGitCtxS_hom (β : IT) `{!AsVal β} : IT_hom (SeedGitCtxS β). + Proof. + unfold SeedGitCtxS. + simple refine (IT_HOM _ _ _ _ _). + - intro a. simpl. rewrite SeedGit_ITV_TickS//. + - intros op' i k. simpl. rewrite SeedGit_ITV_VisS//. + repeat f_equiv. intro. reflexivity. + - intros e. simpl. rewrite SeedGit_ErrS//. + Qed. + #[export] Instance SeedGitCtxL_hom (β : IT) : IT_hom (SeedGitCtxL β). + Proof. + unfold SeedGitCtxL. + simple refine (IT_HOM _ _ _ _ _). + - intro a. simpl. rewrite SeedGit_TickL//. + - intros op' i k. simpl. rewrite SeedGit_VisL//. + repeat f_equiv. intro. reflexivity. + - intros e. simpl. rewrite SeedGit_ErrL//. + Qed. +End prng_seed_workaround. + +#[global] Opaque SeedGit. From d7b709387ff0fb0a94344c36e8440f1c8f8f1bb8 Mon Sep 17 00:00:00 2001 From: hehelego Date: Sat, 4 Apr 2026 23:37:52 +0200 Subject: [PATCH 09/21] Revert "fix PRNG SEED unfold tick counting" This reverts commit 4d898cbbc5f893fc141fe8ef2a5c1d96e5959f9f. --- theories/examples/prng_lang/lang.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v index 28a97f3..d858023 100644 --- a/theories/examples/prng_lang/lang.v +++ b/theories/examples/prng_lang/lang.v @@ -326,7 +326,7 @@ Inductive head_step {S} : expr S → state → expr S → state → nat*nat → head_step (Rand $ Val $ LitPrng l) σ (Val $ LitV n) σ' (1,1) | SeedS σ l n σ' : state_seed σ l n = Some ((), σ') → - head_step (Seed (Val $ LitPrng l) (Val $ LitV n)) σ (Val $ UnitV) σ' (3,1) + head_step (Seed (Val $ LitPrng l) (Val $ LitV n)) σ (Val $ UnitV) σ' (1,1) | IfTrueS n e1 e2 σ : n > 0 → head_step (If (Val (LitV n)) e1 e2) σ @@ -345,7 +345,7 @@ Lemma head_step_prng_01 {S} (e1 e2 : expr S) σ1 σ2 n m : head_step e1 σ1 e2 σ2 (n,m) → m = 0 ∨ m = 1. Proof. inversion 1; eauto. Qed. Lemma head_step_unfold_01 {S} (e1 e2 : expr S) σ1 σ2 n m : - head_step e1 σ1 e2 σ2 (n,m) → n = 0 ∨ n = 1 ∨ n = 3. + head_step e1 σ1 e2 σ2 (n,m) → n = 0 ∨ n = 1. Proof. inversion 1; eauto. Qed. Lemma head_step_pure {S} (e1 e2 : expr S) σ1 σ2 n : head_step e1 σ1 e2 σ2 (n,0) → σ1 = σ2. From fbbd2ef0d0741c42fb68ab3b2019227617dec944 Mon Sep 17 00:00:00 2001 From: hehelego Date: Sat, 4 Apr 2026 23:47:35 +0200 Subject: [PATCH 10/21] fix PRNG-lang interpretation and soundness proof --- theories/examples/prng_lang/interp.v | 134 ++++++++++++--------------- 1 file changed, 58 insertions(+), 76 deletions(-) diff --git a/theories/examples/prng_lang/interp.v b/theories/examples/prng_lang/interp.v index 257cef8..1c97c8b 100644 --- a/theories/examples/prng_lang/interp.v +++ b/theories/examples/prng_lang/interp.v @@ -1,6 +1,7 @@ From gitrees Require Import gitree lang_generic. From gitrees.effects Require Export prng. From gitrees.examples.prng_lang Require Import lang. +From gitrees.examples.prng_lang Require Import prng_seed_combinator. Require Import Binding.Lib Binding.Set. @@ -14,6 +15,10 @@ Section interp. Notation IT := (IT F R). Notation ITV := (ITV F R). + Definition SeedGit' : IT -> IT -> IT := SeedGit rs. + Definition SeedGitCtxL' : IT -> IT -> IT := SeedGitCtxL rs. + Definition SeedGitCtxS' : IT -> IT -> IT := SeedGitCtxS rs. + Global Instance denot_cont_ne (κ : IT -n> IT) : NonExpansive (λ x : IT, Tau (laterO_map κ (Next x))). Proof. @@ -21,10 +26,6 @@ Section interp. Qed. (** Interpreting individual operators *) - (* TODO: these interpretation might be unsound. - Problems with evaluation order. - Problems with "going under Tau/Vis constructor" - *) Program Definition interp_new {A} : A -n> IT := λne env, PRNG_NEW Ret. Program Definition interp_del {A} (l : A -n> IT) : A -n> IT := @@ -32,38 +33,17 @@ Section interp. Program Definition interp_rand {A} (l : A -n> IT) : A -n> IT := λne env, get_ret (PRNG_GEN) (l env). - Program Definition SEED_FUN : IT -n> IT -n> IT := - λne s, get_ret (λne vLoc : locO, get_ret (PRNG_SEED vLoc) s). - Solve All Obligations with solve_proper_please. - Program Definition SEED_IT : IT := λit s l, SEED_FUN s l. - Solve All Obligations with solve_proper_please. - (* NOTE: 1. The interpretation should be a homomorphism in both arguments. 2. The PRNG location should be evaluated first. - - APP is left-associative. *) Program Definition interp_seed {A} (l s : A -n> IT) : A -n> IT := - λne env, SEED_IT ⊙ (s env) ⊙ (l env). + λne env, SeedGit' (l env) (s env). Solve All Obligations with solve_proper_please. - Lemma seed_it_app_ret_ret (l : locO) (s : natO) : - SEED_IT ⊙ (Ret s) ⊙ (Ret l) ≡ Tick_n 2 $ PRNG_SEED l s. - Proof. - rewrite (APP'_Ret_r (SEED_IT ⊙ (Ret s))). - rewrite (APP'_Ret_r SEED_IT). - rewrite APP_Fun. - rewrite APP_Tick. - rewrite APP_Fun. - simpl. - f_equiv. - rewrite get_ret_ret. - simpl. - rewrite get_ret_ret. - simpl. - done. - Qed. + Global Instance interp_seed_ne A : NonExpansive2 (@interp_seed A). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_seed. Program Definition interp_natop {A} (op : nat_op) (t1 t2 : A -n> IT) : A -n> IT := λne env, NATOP (do_natop op) (t1 env) (t2 env). @@ -294,8 +274,8 @@ Section interp. - destruct e; simpl; intros ?; simpl. + reflexivity. + repeat f_equiv; by apply interp_ectx_ren. - + repeat f_equiv; [by apply interp_expr_ren | by apply interp_ectx_ren]. - + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_val_ren]. + + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_expr_ren]. + + repeat f_equiv; [by apply interp_val_ren | by apply interp_ectx_ren]. + repeat f_equiv; by apply interp_ectx_ren. + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_expr_ren | by apply interp_expr_ren]. + repeat f_equiv; [by apply interp_ectx_ren | by apply interp_val_ren]. @@ -308,7 +288,7 @@ Section interp. interp_expr (fill K e) env ≡ (interp_ectx K) env ((interp_expr e) env). Proof. revert env. - induction K; simpl; intros env; first reflexivity; try (by rewrite IHK). + induction K; simpl; intros env; first reflexivity; rewrite IHK //. Qed. Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') @@ -374,8 +354,8 @@ Section interp. - destruct e; simpl; intros ?; simpl. + reflexivity. + repeat f_equiv; by apply interp_ectx_subst. - + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst]. - + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. + + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_expr_subst]. + + repeat f_equiv; [by apply interp_val_subst | by apply interp_ectx_subst]. + repeat f_equiv; by apply interp_ectx_subst. + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_expr_subst | by apply interp_expr_subst]. + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. @@ -423,31 +403,26 @@ Section interp. IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (SeedKl K eSeed) env). Proof. - intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by rewrite !hom_tick. - - rewrite !hom_vis. + intros. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick /SeedGit' SeedGit_TickL. + - rewrite hom_vis /SeedGit' SeedGit_VisL. f_equiv. intro. simpl. rewrite -laterO_map_compose. do 2 f_equiv. by intro. - - by rewrite !hom_err. + - by rewrite hom_err /SeedGit' SeedGit_ErrL. Qed. #[local] Instance interp_ectx_hom_seedks {S} (vprng : val S) (K : ectx S) env : IT_hom (interp_ectx K env) -> IT_hom (interp_ectx (SeedKs vprng K) env). Proof. + pose proof (@interp_val_asval S env vprng) as Hval. intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite !hom_tick. - erewrite APP'_Tick_l; first done. - by apply interp_val_asval. - - rewrite hom_vis. - rewrite APP'_Vis_r. - rewrite APP'_Vis_l. - f_equiv. - intros ?. simpl. by rewrite -laterO_map_compose. - - rewrite hom_err. - rewrite APP'_Err_r. - rewrite APP'_Err_l. - done. + - by rewrite !hom_tick. + - rewrite hom_vis /SeedGit' SeedGit_ITV_VisS. + f_equiv. intro. simpl. rewrite -laterO_map_compose. + do 2 f_equiv. by intro. + - by rewrite hom_err /SeedGit' SeedGit_ErrS. Qed. @@ -667,22 +642,12 @@ Section interp. repeat f_equiv; last done. rewrite Tick_eq/=. repeat f_equiv. rewrite interp_comp. by rewrite ofe_iso_21. - - trans (reify (gReifiers_sReifier rs) (Tick_n 2 $ PRNG_SEED_k l n0 (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). + - trans (reify (gReifiers_sReifier rs) (PRNG_SEED_k l n0 (interp_ectx K env ◎ Ret)) (gState_recomp σr (sR_state σ))). { - f_equiv; last done; f_equiv. - rewrite seed_it_app_ret_ret. - rewrite !hom_tick. + repeat f_equiv. + rewrite /SeedGit' SeedGit_Ret. rewrite hom_SEED_k. - simpl; do 4 f_equiv. - intro; simpl; done. - } - trans (reify (gReifiers_sReifier rs) - (PRNG_SEED_k l n0 (Tick ◎ Tick ◎ interp_ectx K env ◎ Ret)) - (gState_recomp σr (sR_state σ))). - { - do 2 f_equiv. - (* FIXME: maybe this interpretation of [Seed] does not work ?? *) - admit. + f_equiv; first done. by intro. } rewrite reify_vis_eq_ctx_indep //; last first. { @@ -695,8 +660,8 @@ Section interp. } repeat f_equiv; last done. rewrite Tick_eq/=. repeat f_equiv. rewrite interp_comp. - by rewrite ofe_iso_21. - Admitted. + rewrite ofe_iso_21 //. + Qed. Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : prim_step e1 σ1 e2 σ2 (n,m) → @@ -721,8 +686,10 @@ Section interp. { constructor; reflexivity. } 2:{ rewrite app_nil_r; reflexivity. } eapply external_step_reify. - { Transparent PRNG_NEW. unfold PRNG_NEW. simpl. - f_equiv. reflexivity. } + { + Transparent PRNG_NEW. unfold PRNG_NEW. Opaque PRNG_NEW. + simpl. by f_equiv. + } simpl in H2. rewrite -H2. repeat f_equiv; eauto. @@ -736,12 +703,13 @@ Section interp. { constructor; reflexivity. } 2:{ rewrite app_nil_r; reflexivity. } eapply external_step_reify. - { Transparent PRNG_DEL_k. unfold PRNG_DEL_k. simpl. - f_equiv. reflexivity. } + { + Transparent PRNG_DEL_k. unfold PRNG_DEL_k. Opaque PRNG_DEL_k. + simpl. by f_equiv. + } simpl in H2. rewrite -H2. repeat f_equiv; eauto. - Opaque PRNG_DEL_k. rewrite interp_comp /= get_ret_ret hom_DEL_k. eauto. + eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. @@ -752,17 +720,31 @@ Section interp. { constructor; reflexivity. } 2:{ rewrite app_nil_r; reflexivity. } eapply external_step_reify. - { Transparent PRNG_GEN_k. unfold PRNG_GEN_k. simpl. - f_equiv. reflexivity. } + { + Transparent PRNG_GEN_k. unfold PRNG_GEN_k. Opaque PRNG_GEN_k. + simpl. by f_equiv. + } simpl in H2. rewrite -H2. repeat f_equiv; eauto. - Opaque PRNG_GEN_k. rewrite interp_comp /= get_ret_ret hom_GEN_k. eauto. + eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. rewrite interp_comp. simpl. - rewrite seed_it_app_ret_ret; rewrite !Tick_n_S Tick_n_O. - Admitted. + rewrite /SeedGit' SeedGit_Ret. + rewrite hom_SEED_k. + change 1 with (Nat.add 1 0). econstructor; last first. + { constructor; reflexivity. } + 2:{ rewrite app_nil_r; reflexivity. } + eapply external_step_reify. + { + Transparent PRNG_SEED_k. unfold PRNG_SEED_k. Opaque PRNG_SEED_k. + simpl. by f_equiv. + } + simpl in H2. + rewrite -H2. + repeat f_equiv; eauto. + rewrite interp_comp /= /SeedGit' SeedGit_Ret hom_SEED_k //. + Qed. End interp. #[global] Opaque PRNG_NEW PRNG_DEL_k PRNG_GEN_k PRNG_SEED_k. From 52b9d2e11a88c8225b02f1fdbfa176dbdd17d2b4 Mon Sep 17 00:00:00 2001 From: hehelego Date: Sun, 5 Apr 2026 17:18:47 +0200 Subject: [PATCH 11/21] fix forbid the creation of PRNG location statically --- theories/examples/prng_lang/lang.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v index d858023..da263e9 100644 --- a/theories/examples/prng_lang/lang.v +++ b/theories/examples/prng_lang/lang.v @@ -537,11 +537,11 @@ with typed_val {S : Set} (Γ : S -> ty) : val S → ty → Prop := typed_val Γ UnitV Tunit | typed_Lit n : typed_val Γ (LitV n) Tnat -| typed_Loc l : - typed_val Γ (LitPrng l) Tprng | typed_RecV (τ1 τ2 : ty) (e : expr (inc (inc S))) : typed (Γ ▹ (Tarr τ1 τ2) ▹ τ1) e τ2 → typed_val Γ (RecV e) (Tarr τ1 τ2) + (* NOTE: PRNG location literals cannot be statically created *) + (* | typed_Loc l : typed_val Γ (LitPrng l) Tprng *) . Declare Scope syn_scope. From f999caa31ba39addf68b4797c6563b126f3540ee Mon Sep 17 00:00:00 2001 From: hehelego Date: Sun, 5 Apr 2026 17:20:28 +0200 Subject: [PATCH 12/21] WIP: unary logical relation for safety and adeqaucy for PRNG lang --- theories/examples/prng_lang/logpred.v | 451 ++++++++++++++++++++++++++ 1 file changed, 451 insertions(+) diff --git a/theories/examples/prng_lang/logpred.v b/theories/examples/prng_lang/logpred.v index e69de29..e0aa121 100644 --- a/theories/examples/prng_lang/logpred.v +++ b/theories/examples/prng_lang/logpred.v @@ -0,0 +1,451 @@ +(** Unary (Kripke) logical relation for the PRNG lang *) +(** Type safety and adequacy of the GIT interptation *) +From gitrees Require Import gitree program_logic lang_generic. +From gitrees.examples.prng_lang Require Import lang interp prng_seed_combinator. +From gitrees.effects Require Import prng. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Import IF_nat. + +Section prng_logrel. + Context {sz : nat}. + Variable rs : gReifiers NotCtxDep sz. + Context `{!subReifier reify_prng rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R} `{!SubOfe locO R} `{!SubOfe unitO R} . + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!prngG Σ, !gitreeGS_gen rs R Σ, !na_invG Σ}. + Notation iProp := (iProp Σ). + + (* stuckness and the freely-adjoined kripke frame *) + Variable s : stuckness. + Context {A : ofe}. + Variable (P : A -n> iProp). + + (* expr_pred: gitree value predicate -> gitree predicate *) + Local Notation expr_pred := (expr_pred s rs P). + + Program Definition val_nat : ITV -n> iProp := λne αv, + (∃ (n : nat), αv ≡ RetV n)%I. + Program Definition val_unit : ITV -n> iProp := λne αv, + (αv ≡ RetV ())%I. + Program Definition val_prng : ITV -n> iProp := λne αv, + (∃ (l : loc) (n : nat), αv ≡ RetV l ∗ has_prng_state l n)%I. + Solve All Obligations with solve_proper. + + Program Definition val_arr (Φ1 Φ2 : ITV -n> iProp) := λne αv, + (□ ∀ βv, Φ1 βv -∗ expr_pred ((IT_of_V αv) ⊙ (IT_of_V βv)) Φ2)%I. + Solve All Obligations with solve_proper. + + Fixpoint val_pred (τ : ty) : ITV -n> iProp := + match τ with + | Tunit => val_unit + | Tnat => val_nat + | Tprng => val_prng + | Tarr τ1 τ2 => val_arr (val_pred τ1) (val_pred τ2) + end. + + (* subst_valid: (S : Names) (Γ : Context S) -> interptation of Γ -> iProp *) + Notation ssubst_valid := (ssubst_valid1 rs ty val_pred expr_pred). + + (*[Tprng] is not persistent*) + #[global] Instance prng_lang_val_pred_persist τ βv : Persistent (val_pred τ βv). + Proof. induction τ; try apply _. Abort. + + Program Definition valid1 {S : Set} (Γ : S → ty) (α : interp_scope S -n> IT) (τ : ty) : iProp := + (∀ ss, prng_ctx rs + -∗ ssubst_valid Γ ss + -∗ expr_pred (α ss) (λne v, val_pred τ v))%I. + Solve Obligations with solve_proper. + + Lemma compat_unit {S : Set} (Γ : S → ty) : + ⊢ valid1 Γ (interp_unit rs) Tunit. + Proof. + iIntros (αs) "#Hctx Has". + by iApply expr_pred_ret. + Qed. + + Lemma compat_nat {S : Set} (Γ : S → ty) (n : nat) : + ⊢ valid1 Γ (interp_nat rs n) Tnat. + Proof. + iIntros (αs) "#Hctx Has". + iApply expr_pred_ret. + by iExists n. + Qed. + + Lemma compat_var {S : Set} (Γ : S → ty) (v : S) : + ⊢ valid1 Γ (interp_var v) (Γ v). + Proof. + iIntros (ss) "#Hctx Has". + iIntros (x) "HP". + iSimpl. + iSpecialize ("Has" $! v x with "HP"). + iApply (wp_wand with "Has"). + iIntros (v') "HH". + iDestruct "HH" as "(%y & HH & HP')". + iModIntro. + iExists y. + iFrame. + Qed. + + Lemma compat_if {S : Set} (Γ : S → ty) τ α β1 β2 : + ⊢ valid1 Γ α Tnat -∗ + valid1 Γ β1 τ -∗ + valid1 Γ β2 τ -∗ + valid1 Γ (interp_if rs α β1 β2) τ. + Proof. + iIntros "H0 H1 H2". + iIntros (ss) "#Hctx #Has". + iSpecialize ("H0" with "Hctx Has"). + iApply (expr_pred_bind (IFSCtx _ _) with "H0"). + iIntros (αv) "Ha/=". + iDestruct "Ha" as (n) "Hn". + unfold IFSCtx. iIntros (x) "Hx". + iRewrite "Hn". + destruct n as [|n]. + - rewrite IF_False; last lia. + iApply ("H2" with "Hctx Has Hx"). + - rewrite IF_True; last lia. + iApply ("H1" with "Hctx Has Hx"). + Qed. + + + Lemma val_prng_loc_literal {S : Set} (Γ : S → ty) (l : loc) (n : nat) : + ⊢ has_prng_state l n -∗ + valid1 Γ (interp_loc rs l) Tprng. + Proof. + iIntros "Hstate" (αs) "#Hctx Has". + iApply expr_pred_ret. + iExists l,n. + by iFrame. + Qed. + + (* TODO: use the derived WP rules to prove that the effect interpretations are semantically well-typed *) + + (* [typed_NewPrng] *) + Lemma compat_NewPrng {S : Set} {Γ : S → ty} : + ⊢ valid1 Γ (interp_new rs) Tprng. + Proof. + iIntros (ss) "#Hctx #Has". + iApply expr_pred_frame. + iApply (wp_new rs Ret s with "Hctx"). + iIntros (l). + iIntros "!> !> Hrng". + iApply wp_val. + iExists l,0. + by iFrame. + Qed. + + (* [typed_DelPrng] *) + Lemma compat_DelPrng {S : Set} {Γ : S → ty} α : + ⊢ valid1 Γ α Tprng -∗ + valid1 Γ (interp_del rs α) Tunit. + Proof. + iIntros "H1" (ss) "#Hctx #Has". + iSpecialize ("H1" $! ss with "Hctx Has"). + iApply (expr_pred_bind (get_ret PRNG_DEL) with "H1"). + iIntros (αv) "(%l & %n & Heq & Hprng) /=". + iRewrite "Heq". + iApply expr_pred_frame. + rewrite IT_of_V_Ret get_ret_ret. + iApply (wp_del rs l n s with "Hctx Hprng"). + done. + Qed. + + (* [typed_Rand] *) + Lemma compat_Rand {S : Set} {Γ : S → ty} α : + ⊢ valid1 Γ α Tprng -∗ + valid1 Γ (interp_rand rs α) Tnat. + Proof. + iIntros "H1" (ss) "#Hctx #Has". + iSpecialize ("H1" $! ss with "Hctx Has"). + iApply (expr_pred_bind (get_ret PRNG_GEN) with "H1"). + iIntros (αv) "(%l & %n & Heq & Hprng) /=". + iRewrite "Heq". + iApply expr_pred_frame. + rewrite IT_of_V_Ret get_ret_ret. + iApply (wp_gen rs l n s with "Hctx Hprng"). + iIntros "!> !> Hprng'". + iApply wp_val. + by iExists (read_lcg n). + Qed. + + (* [typed_Seed] *) + Lemma compat_Seed {S : Set} {Γ : S → ty} α β : + ⊢ valid1 Γ α Tprng -∗ + valid1 Γ β Tnat -∗ + valid1 Γ (interp_seed rs α β) Tunit. + Proof. + iIntros "H1 H2" (ss) "#Hctx #Has". simpl. + iSpecialize ("H1" $! ss with "Hctx Has"). + iSpecialize ("H2" $! ss with "Hctx Has"). + iApply (expr_pred_bind (SeedGitCtxL rs (β ss)) with "H1"). + iIntros (αv) "(%l & %n & Heq & Hprng) /=". + iRewrite "Heq"; rewrite IT_of_V_Ret. + iApply (expr_pred_bind (SeedGitCtxS rs (Ret l)) with "H2"). + iIntros (βv) "(%sd & Heq)". + iRewrite "Heq"; rewrite IT_of_V_Ret /SeedGitCtxS SeedGit_Ret. + iApply expr_pred_frame. + iApply (wp_seed rs l n sd with "Hctx Hprng"). + iIntros "!> !> Hprng'". + done. + Qed. + + Lemma compat_app {S : Set} (Γ : S → ty) α β τ1 τ2 : + ⊢ valid1 Γ α (Tarr τ1 τ2) -∗ + valid1 Γ β τ1 -∗ + valid1 Γ (interp_app rs α β) τ2. + Proof. + iIntros "H1 H2". + iIntros (ss) "#Hctx #Has". simpl. + iSpecialize ("H2" with "Hctx Has"). + iApply (expr_pred_bind (AppRSCtx _) with "H2"). + iIntros (βv) "Hb/=". + unfold AppRSCtx. + iSpecialize ("H1" with "Hctx Has"). + iApply (expr_pred_bind (AppLSCtx (IT_of_V βv)) with "H1"). + iIntros (αv) "Ha". + unfold AppLSCtx. + iApply ("Ha" with "Hb"). + Qed. + + Lemma compat_rec {S : Set} (Γ : S → ty) τ1 τ2 α : + ⊢ □ valid1 (Γ ▹ (Tarr τ1 τ2) ▹ τ1) α τ2 -∗ + valid1 Γ (interp_rec rs α) (Tarr τ1 τ2). + Proof. + iIntros "#H". iIntros (ss) "#Hctx #Hss". + term_simpl. + pose (f := (ir_unf rs α ss)). + iAssert (interp_rec rs α ss ≡ IT_of_V $ FunV (Next f))%I as "Hf". + { iPureIntro. apply interp_rec_unfold. } + iRewrite "Hf". iApply expr_pred_ret. simpl. + iModIntro. + iLöb as "IH". iSimpl. + iIntros (βv) "Hw". + iIntros (x) "Hx". + iApply wp_lam. + iIntros "!> Hcl". + pose (ss' := (extend_scope (extend_scope ss (interp_rec rs α ss)) (IT_of_V βv))). + iSpecialize ("H" $! ss' with "Hctx [Hw]"). + { + unfold ssubst_valid. + iIntros ([| [|]]); term_simpl. + - iModIntro. + iApply expr_pred_ret. + (* FIXME: [Hw : val_pred τ1 βv] is not persistent + + a PRNG state cannot be shared easily. + PRNG state update is not an atomic operator. + *) + admit. + - iModIntro. + iRewrite "Hf". + iIntros (x') "Hx". + iApply wp_val. + iModIntro. + iExists x'. + iFrame "Hx". + iModIntro. + iApply "IH". + - iApply "Hss". + } + unfold f. + by iApply "H". + Admitted. + + Lemma compat_natop {S : Set} (Γ : S → ty) op α β : + ⊢ valid1 Γ α Tnat -∗ + valid1 Γ β Tnat -∗ + valid1 Γ (interp_natop _ op α β) Tnat. + Proof. + iIntros "H1 H2". + iIntros (ss) "#Hctx #Has". simpl. + iSpecialize ("H2" with "Hctx Has"). + iApply (expr_pred_bind (NatOpRSCtx _ _) with "H2"). + iIntros (βv) "Hb/=". + unfold NatOpRSCtx. + iSpecialize ("H1" with "Hctx Has"). + iApply (expr_pred_bind (NatOpLSCtx _ (IT_of_V βv)) with "H1"). + iIntros (αv) "Ha". + unfold NatOpLSCtx. + iDestruct "Hb" as (n1) "Hb". + iDestruct "Ha" as (n2) "Ha". + iRewrite "Hb". iRewrite "Ha". + simpl. iApply expr_pred_frame. + rewrite NATOP_Ret. iApply wp_val. simpl. + eauto with iFrame. + Qed. + + Lemma fundamental {S : Set} (Γ : S → ty) e τ : + typed Γ e τ → ⊢ valid1 Γ (interp_expr rs e) τ + with fundamental_val {S : Set} (Γ : S → ty) v τ : + typed_val Γ v τ → ⊢ valid1 Γ (interp_val rs v) τ. + Proof. + - destruct 1. + + by iApply fundamental_val. + + subst. by iApply compat_var. + + iApply compat_app; iApply fundamental; eauto. + + iApply compat_natop; iApply fundamental; eauto. + + iApply compat_if; iApply fundamental; eauto. + + iApply compat_NewPrng. + + iApply compat_DelPrng; iApply fundamental; eauto. + + iApply compat_Rand; iApply fundamental; eauto. + + iApply compat_Seed; iApply fundamental; eauto. + - destruct 1. + + iApply compat_unit. + + iApply compat_nat. + + iApply compat_rec; iApply fundamental; eauto. + Qed. + + Lemma fundmanetal_closed (e : expr ∅) (τ : ty) : + typed □ e τ → + ⊢ valid1 □ (interp_expr rs e) τ. + Proof. apply fundamental. Qed. + +End prng_logrel. + +Arguments val_pred {_ _ _ _ _ _ _ _ _ _ _ _ _} τ. +Arguments val_arr {_ _ _ _ _ _ _ _ _} Φ1 Φ2. + +(* Closed typed PRNG lang programs are safety to executed. + We prove this by the safety of GIT interpretation (of typed closed programs) and adequacy + *) +Section safety_adeqaucy. + +Local Definition rs : gReifiers NotCtxDep _ := gReifiers_cons reify_prng gReifiers_nil. + +#[local] Parameter Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. + +Program Definition InputLangGitreeGS {R} `{!Cofe R} + {a : is_ctx_dep} {n} (rs : gReifiers a n) + (Σ : gFunctors) + (H1 : invGS Σ) (H2 : stateG rs R Σ) + : gitreeGS_gen rs R Σ := + GitreeG rs R Σ H1 H2 + (λ _ σ, @state_interp _ _ rs R _ _ H2 σ) + (λ _, True%I) + (λ _, True%I) + _ + (λ x, x) + _ + _ + _. +Next Obligation. + intros; simpl. + iIntros "?". by iModIntro. +Qed. +Next Obligation. + intros; simpl. iSplit; iIntros "H". + - by iFrame "H". + - by iDestruct "H" as "(_ & ?)". +Qed. + +(* TODO: adeequacy and safety proof for the PRNG lang + adapt the proofs for input-lang. +*) + +(* +Lemma logpred_adequacy cr Σ R + `{!Cofe R, !SubOfe natO R, !SubOfe logO R, !SubOfe unitO R} + `{!invGpreS Σ} `{!statePreG rs R Σ} `{!prngPreG Σ} + (τ : ty) + (α : interp_scope ∅ -n> IT (gReifiers_ops rs) R) + (β : IT (gReifiers_ops rs) R) st st' k : + (∀ `{H1 : !gitreeGS_gen rs R Σ}, + (£ cr ⊢ valid1 rs notStuck (λne _ : unitO, True)%I □ α τ)%I) → + external_steps (gReifiers_sReifier rs) (α ı_scope) st β st' [] k → + is_Some (IT_to_V β) + ∨ (∃ β1 st1 l, external_step (gReifiers_sReifier rs) β st' β1 st1 l) + ∨ (∃ e : errorO, β ≡ Err e ∧ notStuck e). +Proof. + intros Hlog Hst. + eapply (wp_progress_gen Σ 1 NotCtxDep rs (S cr) (λ x, x) notStuck + [] k (α ı_scope) β st st' Hdisj Hst). + intros H1 H2. + pose H3 : gitreeGS_gen rs R Σ := InputLangGitreeGS rs Σ H1 H2. + simpl in H3. + exists (val_pred (s:=notStuck) (P:=(λne _:unitO, True)) τ)%I. split. + { apply _. } + iExists (@state_interp_fun _ _ rs _ _ _ H3). + iExists (@aux_interp_fun _ _ rs _ _ _ H3). + iExists (@fork_post _ _ rs _ _ _ H3). + iExists (@fork_post_ne _ _ rs _ _ _ H3). + iExists (@state_interp_fun_mono _ _ rs _ _ _ H3). + iExists (@state_interp_fun_ne _ _ rs _ _ _ H3). + iExists (@state_interp_fun_decomp _ _ rs _ _ _ H3). + simpl. + iAssert (True%I) as "G"; first done; iFrame "G"; iClear "G". + iModIntro. iIntros "((Hone & Hcr) & Hst)". + iPoseProof (Hlog H3 with "Hcr") as "Hlog". + destruct st as [σ []]. + iAssert (has_substate σ) with "[Hst]" as "Hs". + { + unfold has_substate, has_full_state. + assert (of_state rs (IT (gReifiers_ops rs) _) (σ,()) ≡ + of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)) as ->; last done. + intro j. unfold sR_idx. simpl. + unfold of_state, of_idx. + destruct decide as [Heq|]; last first. + { + inv_fin j; first done. + intros i. inversion i. + } + inv_fin j; last done. + intros Heq. + rewrite (eq_pi _ _ Heq eq_refl)//. + } + iApply fupd_wp. + iMod (inv_alloc (nroot.@"ioE") _ + (∃ σ, + £ 1 ∗ has_substate (σ : oFunctor_car + (sReifier_state reify_io) + (IT (sReifier_ops (gReifiers_sReifier rs)) R) + (IT (sReifier_ops (gReifiers_sReifier rs)) R)))%I + with "[Hone Hs]") as "#Hinv". + { + iNext. iExists σ. + iFrame "Hone Hs". + } + iSpecialize ("Hlog" with "Hinv []"). + { + iIntros (x). + destruct x. + } + iSpecialize ("Hlog" $! tt with "[//]"). + iApply (wp_wand with"Hlog"). + iModIntro. + iIntros ( βv). simpl. iDestruct 1 as (_) "[H _]". + by iFrame. +Qed. + +Lemma prng_lang_safety e τ σ st' (β : IT (sReifier_ops (gReifiers_sReifier rs)) natO) k : + typed □ e τ → + external_steps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) (σ, ()) β st' [] k → + is_Some (IT_to_V β) + ∨ (∃ β1 st1 l, external_step (gReifiers_sReifier rs) β st' β1 st1 l). +Proof. + intros Htyped Hsteps. + cut (is_Some (IT_to_V β) + ∨ (∃ β1 st1 l, external_step (gReifiers_sReifier rs) β st' β1 st1 l) + ∨ (∃ e : errorO, β ≡ Err e ∧ notStuck e)). + { + intros [H | [H | [? [? H]]]]. + - by left. + - by right. + - done. + } + pose (Σ:=#[invΣ;stateΣ rs natO]). + assert (invGpreS Σ). + { apply _. } + assert (statePreG rs natO Σ). + { apply _. } + eapply (logpred_adequacy 0 Σ); eauto. + intros ?. iIntros "_". + by iApply fundamental. +Qed. + +*) +End safety_adeqaucy. From 5ae59ad54f657888c7674ae883e273f9e9312a60 Mon Sep 17 00:00:00 2001 From: hehelego Date: Mon, 6 Apr 2026 08:25:25 +0200 Subject: [PATCH 13/21] make prng location value relation persistent --- theories/examples/prng_lang/logpred.v | 72 +++++++++++++-------------- 1 file changed, 36 insertions(+), 36 deletions(-) diff --git a/theories/examples/prng_lang/logpred.v b/theories/examples/prng_lang/logpred.v index e0aa121..d7aaa63 100644 --- a/theories/examples/prng_lang/logpred.v +++ b/theories/examples/prng_lang/logpred.v @@ -25,6 +25,8 @@ Section prng_logrel. Context {A : ofe}. Variable (P : A -n> iProp). + Definition prng_logrel_NS : namespace := nroot .@ "prng-logrel". + (* expr_pred: gitree value predicate -> gitree predicate *) Local Notation expr_pred := (expr_pred s rs P). @@ -33,7 +35,7 @@ Section prng_logrel. Program Definition val_unit : ITV -n> iProp := λne αv, (αv ≡ RetV ())%I. Program Definition val_prng : ITV -n> iProp := λne αv, - (∃ (l : loc) (n : nat), αv ≡ RetV l ∗ has_prng_state l n)%I. + (∃ (l : loc), αv ≡ RetV l ∗ inv (prng_logrel_NS .@ l) (∃ (n : nat), has_prng_state l n))%I. Solve All Obligations with solve_proper. Program Definition val_arr (Φ1 Φ2 : ITV -n> iProp) := λne αv, @@ -51,9 +53,9 @@ Section prng_logrel. (* subst_valid: (S : Names) (Γ : Context S) -> interptation of Γ -> iProp *) Notation ssubst_valid := (ssubst_valid1 rs ty val_pred expr_pred). - (*[Tprng] is not persistent*) + (* we made [Tprng] persistent by wrapping the [pointsto]/[has_prng_state] predicate in an invariant *) #[global] Instance prng_lang_val_pred_persist τ βv : Persistent (val_pred τ βv). - Proof. induction τ; try apply _. Abort. + Proof. induction τ; try apply _. Qed. Program Definition valid1 {S : Set} (Γ : S → ty) (α : interp_scope S -n> IT) (τ : ty) : iProp := (∀ ss, prng_ctx rs @@ -113,18 +115,6 @@ Section prng_logrel. Qed. - Lemma val_prng_loc_literal {S : Set} (Γ : S → ty) (l : loc) (n : nat) : - ⊢ has_prng_state l n -∗ - valid1 Γ (interp_loc rs l) Tprng. - Proof. - iIntros "Hstate" (αs) "#Hctx Has". - iApply expr_pred_ret. - iExists l,n. - by iFrame. - Qed. - - (* TODO: use the derived WP rules to prove that the effect interpretations are semantically well-typed *) - (* [typed_NewPrng] *) Lemma compat_NewPrng {S : Set} {Γ : S → ty} : ⊢ valid1 Γ (interp_new rs) Tprng. @@ -133,12 +123,18 @@ Section prng_logrel. iApply expr_pred_frame. iApply (wp_new rs Ret s with "Hctx"). iIntros (l). - iIntros "!> !> Hrng". + iIntros "!> !> Hprng". + iAssert ((∃ n, has_prng_state l n)%I) with "[Hprng]" as "HprngEx"; + first by iExists 0. + iMod (inv_alloc (prng_logrel_NS .@ l) with "HprngEx") as "#HprngInv". iApply wp_val. - iExists l,0. - by iFrame. + iModIntro. + iExists l. + by iSplit. Qed. + (* TODO: invariant open problem *) + (* [typed_DelPrng] *) Lemma compat_DelPrng {S : Set} {Γ : S → ty} α : ⊢ valid1 Γ α Tprng -∗ @@ -147,13 +143,17 @@ Section prng_logrel. iIntros "H1" (ss) "#Hctx #Has". iSpecialize ("H1" $! ss with "Hctx Has"). iApply (expr_pred_bind (get_ret PRNG_DEL) with "H1"). - iIntros (αv) "(%l & %n & Heq & Hprng) /=". - iRewrite "Heq". + iIntros (αv) "(%l & Heq & HprngInv) /=". + iRewrite "Heq". rewrite IT_of_V_Ret get_ret_ret. iApply expr_pred_frame. - rewrite IT_of_V_Ret get_ret_ret. - iApply (wp_del rs l n s with "Hctx Hprng"). - done. - Qed. + (* FIXME: deleting a potentially shared PRNG state is generally unsafe. + it is only safe to delete with exclusive ownership. + + let rng := new_prng in + let rng_share := rng in + delete rng; rand rng_share + *) + Admitted. (* [typed_Rand] *) Lemma compat_Rand {S : Set} {Γ : S → ty} α : @@ -163,15 +163,17 @@ Section prng_logrel. iIntros "H1" (ss) "#Hctx #Has". iSpecialize ("H1" $! ss with "Hctx Has"). iApply (expr_pred_bind (get_ret PRNG_GEN) with "H1"). - iIntros (αv) "(%l & %n & Heq & Hprng) /=". - iRewrite "Heq". + iIntros (αv) "(%l & Heq & HprngInv) /=". + iRewrite "Heq". rewrite IT_of_V_Ret get_ret_ret. iApply expr_pred_frame. - rewrite IT_of_V_Ret get_ret_ret. + (* iApply (wp_gen rs l n s with "Hctx Hprng"). iIntros "!> !> Hprng'". iApply wp_val. by iExists (read_lcg n). Qed. + *) + Admitted. (* [typed_Seed] *) Lemma compat_Seed {S : Set} {Γ : S → ty} α β : @@ -183,16 +185,19 @@ Section prng_logrel. iSpecialize ("H1" $! ss with "Hctx Has"). iSpecialize ("H2" $! ss with "Hctx Has"). iApply (expr_pred_bind (SeedGitCtxL rs (β ss)) with "H1"). - iIntros (αv) "(%l & %n & Heq & Hprng) /=". + iIntros (αv) "(%l & Heq & HprngInv) /=". iRewrite "Heq"; rewrite IT_of_V_Ret. iApply (expr_pred_bind (SeedGitCtxS rs (Ret l)) with "H2"). iIntros (βv) "(%sd & Heq)". iRewrite "Heq"; rewrite IT_of_V_Ret /SeedGitCtxS SeedGit_Ret. iApply expr_pred_frame. + (* iApply (wp_seed rs l n sd with "Hctx Hprng"). iIntros "!> !> Hprng'". done. Qed. + *) + Admitted. Lemma compat_app {S : Set} (Γ : S → ty) α β τ1 τ2 : ⊢ valid1 Γ α (Tarr τ1 τ2) -∗ @@ -224,7 +229,7 @@ Section prng_logrel. iRewrite "Hf". iApply expr_pred_ret. simpl. iModIntro. iLöb as "IH". iSimpl. - iIntros (βv) "Hw". + iIntros (βv) "#Hw". iIntros (x) "Hx". iApply wp_lam. iIntros "!> Hcl". @@ -235,12 +240,7 @@ Section prng_logrel. iIntros ([| [|]]); term_simpl. - iModIntro. iApply expr_pred_ret. - (* FIXME: [Hw : val_pred τ1 βv] is not persistent - - a PRNG state cannot be shared easily. - PRNG state update is not an atomic operator. - *) - admit. + iExact "Hw". - iModIntro. iRewrite "Hf". iIntros (x') "Hx". @@ -254,7 +254,7 @@ Section prng_logrel. } unfold f. by iApply "H". - Admitted. + Qed. Lemma compat_natop {S : Set} (Γ : S → ty) op α β : ⊢ valid1 Γ α Tnat -∗ From 9bd28cd295eb5276588993cc05cba5499c10acfe Mon Sep 17 00:00:00 2001 From: hehelego Date: Mon, 6 Apr 2026 21:54:34 +0200 Subject: [PATCH 14/21] prevent delete PRNG location as it is generally unsafe --- theories/examples/prng_lang/lang.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/examples/prng_lang/lang.v b/theories/examples/prng_lang/lang.v index da263e9..fc8d728 100644 --- a/theories/examples/prng_lang/lang.v +++ b/theories/examples/prng_lang/lang.v @@ -522,9 +522,8 @@ Inductive typed {S : Set} (Γ : S -> ty) : expr S → ty → Prop := typed Γ (If e0 e1 e2) τ | typed_NewPrng : typed Γ NewPrng Tprng -| typed_DelPrng e : - typed Γ e Tprng → - typed Γ (DelPrng e) Tunit + (* NOTE: PRNG location can be duplicated/shared through function application. It is unsafe to delete except for exclusive ownership *) + (* | typed_DelPrng e : typed Γ e Tprng → typed Γ (DelPrng e) Tunit *) | typed_Rand e : typed Γ e Tprng → typed Γ (Rand e) Tnat From 13e1f0a05b91c943d2f7b0e6b330d57846337eed Mon Sep 17 00:00:00 2001 From: hehelego Date: Tue, 7 Apr 2026 12:28:52 +0200 Subject: [PATCH 15/21] new ghost theory and Hoare triples for PRNG effects (deletion is not allowed) --- theories/effects/prng.v | 246 +++++++++++++++------------------------- 1 file changed, 92 insertions(+), 154 deletions(-) diff --git a/theories/effects/prng.v b/theories/effects/prng.v index d136d53..650ca7d 100644 --- a/theories/effects/prng.v +++ b/theories/effects/prng.v @@ -1,5 +1,5 @@ (** pseudo random number generator effect *) -From iris.algebra Require Import gmap excl auth gmap_view list. +From iris.algebra Require Import gmap gmap_view excl auth. From iris.proofmode Require Import classes tactics. From iris.base_logic Require Import algebra. From iris.heap_lang Require Export locations. @@ -175,6 +175,7 @@ Section prng_combinators. Proof. solve_hom_easy PRNG_SEED_k. Qed. End prng_combinators. +(* NOTE: we cannot give a spec to delete *) Section wp. Context {grs_sz : nat}. Context {a : is_ctx_dep}. @@ -186,23 +187,31 @@ Section wp. Notation ITV := (ITV F R). Notation stateO := (stateF ♯ IT). - Definition istate := gmap_viewR loc natO. - Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ istate }. + Definition entryR := prodR (agreeR unit) (optionR (exclR nat)). + Definition prngR := gmap_viewR loc entryR. + + Definition owner_entry n : entryR := (to_agree (), Some (Excl n)). + Definition borrow_entry : entryR := (to_agree (), None). + Definition owner_store (m : gmapR loc nat) := owner_entry <$> m. + + Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ prngR }. Class prngG Σ := PrngG { - prngG_inG :: inG Σ istate; + prngG_inG :: inG Σ prngR; prngG_name : gname; }. - Definition prngΣ : gFunctors := GFunctor istate. + Definition prngΣ : gFunctors := GFunctor prngR. #[export] Instance subG_prngΣ {Σ} : subG prngΣ Σ → prngPreG Σ. Proof. solve_inG. Qed. - Lemma new_prngG σ `{!prngPreG Σ} : + Lemma new_storeG σ `{!prngPreG Σ} : (⊢ |==> ∃ `{!prngG Σ}, own prngG_name (●V σ): iProp Σ)%I. Proof. iMod (own_alloc (●V σ)) as (γ) "H". - { apply gmap_view_auth_valid. } - pose (sg := {| prngG_inG := _; prngG_name := γ |}). - iModIntro. iExists sg. by iFrame. + { + apply gmap_view_auth_valid. + } + set {| prngG_inG := PrngPreG_inG; prngG_name := γ |} as sg. + by iExists sg. Qed. Context `{!subReifier (sReifier_NotCtxDep_min reify_prng a) rs}. @@ -211,76 +220,59 @@ Section wp. Context `{!prngG Σ}. - Program Definition prng_ctx := - inv (nroot.@"prngE") - (∃ σ, £ 1 ∗ has_substate σ ∗ own prngG_name (●V σ))%I. + Notation own := (own prngG_name). + Definition has_prngs (σ : gmapR loc nat) := + own $ gmap_view_auth (DfracOwn 1) (owner_store σ). + Definition known_prng (l : loc) := + own $ gmap_view_frag l DfracDiscarded borrow_entry. + Definition prng_ctx := inv (nroot.@"prngE") (∃ σ, £ 1 ∗ has_substate σ ∗ has_prngs σ)%I. - Program Definition has_prng_state (l : loc) (s : nat) : iProp := - own prngG_name $ gmap_view_frag l (DfracOwn 1) s. - Global Instance has_state_proper l : Proper ((≡) ==> (≡)) (has_prng_state l). - Proof. solve_proper. Qed. - Global Instance has_state_ne l : NonExpansive (has_prng_state l). - Proof. solve_proper. Qed. + (* TODO: find some library functions for proving frame preserving updates of gmap fragmental view weakening *) - Lemma istate_alloc n l σ : + Lemma istate_alloc (n : nat) l σ : σ !! l = None → - own prngG_name (●V σ) ==∗ own prngG_name (●V (<[l:=n]>σ)) - ∗ has_prng_state l n. + has_prngs σ ==∗ has_prngs (<[l:=n]> σ) ∗ known_prng l. Proof. iIntros (Hl) "H". - iMod (own_update with "H") as "[$ $]". - { by apply (gmap_view_alloc _ l (DfracOwn 1) n); eauto. } - done. - Qed. - - Lemma istate_read l n σ : - own prngG_name (●V σ) -∗ has_prng_state l n - -∗ (σ !! l) ≡ Some n. + iMod (own_update with "H") as "[Hauth Hfrag]". + { + apply (gmap_view_alloc (owner_store σ) l (DfracOwn 1) (owner_entry n)). + - rewrite lookup_fmap Hl //. + - done. + - done. + } + iSplitL "Hauth"; first rewrite /has_prngs /owner_store fmap_insert //. + iMod (own_update with "Hfrag") as "$". + Admitted. + + Lemma istate_read l σ : + has_prngs σ + -∗ known_prng l + -∗ ∃ n, (σ !! l) ≡ Some n. Proof. iIntros "Ha Hf". iPoseProof (own_valid_2 with "Ha Hf") as "H". - rewrite gmap_view_both_validI. - iDestruct "H" as "[%H [Hval HEQ]]". - done. - Qed. - - Lemma istate_loc_dom l n σ : - own prngG_name (●V σ) -∗ has_prng_state l n -∗ ⌜is_Some (σ !! l)⌝. - Proof. - iIntros "Hinv Hloc". - iPoseProof (istate_read with "Hinv Hloc") as "Hl". - destruct (σ !! l) ; eauto. - by rewrite option_equivI. - Qed. - - Lemma istate_write l n n' σ : - own prngG_name (●V σ) -∗ has_prng_state l n - ==∗ own prngG_name (●V <[l:=n']>σ) - ∗ has_prng_state l n'. + rewrite gmap_view_both_dfrac_validI. + iDestruct "H" as (n dq Hvalid1 Hlookup Hvalid2 OtherPart) "%Heq". + rewrite lookup_fmap in Hlookup. + Admitted. + + Lemma istate_write l n' σ : + has_prngs σ + -∗ known_prng l + ==∗ has_prngs (<[l:=n']> σ) ∗ known_prng l. Proof. iIntros "H Hl". iMod (own_update_2 with "H Hl") as "[$ $]"; last done. - by apply gmap_view_replace. - Qed. - - Lemma istate_delete l n σ : - own prngG_name (●V σ) -∗ has_prng_state l n ==∗ own prngG_name (●V delete l σ). - Proof. - iIntros "H Hl". - iMod (own_update_2 with "H Hl") as "$". - { apply gmap_view_delete. } - done. - Qed. - + Admitted. Lemma wp_new_hom (k : locO -n> IT) s Φ `{!NonExpansive Φ} (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ - ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} κ (k l) @ s {{ Φ }}) -∗ + ▷▷ (∀ l, known_prng l -∗ WP@{rs} κ (k l) @ s {{ Φ }}) -∗ WP@{rs} κ (PRNG_NEW k) @ s {{ Φ }}. Proof. iIntros "#Hctx Ha". - unfold PRNG_NEW; simpl. - rewrite hom_vis. + rewrite /PRNG_NEW hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". simpl. @@ -291,7 +283,7 @@ Section wp. iExists σ,l,(<[l:=0]>σ),(κ $ k l),[]. iFrame "Hs". iSplit; first done. - iSplit; first by rewrite later_map_Next ofe_iso_21. + iSplit; first rewrite later_map_Next ofe_iso_21 //. iNext. iMod (istate_alloc 0 l with "Hh") as "[Hh Hp]". { @@ -311,135 +303,81 @@ Section wp. Lemma wp_new (k : locO -n> IT) s Φ `{!NonExpansive Φ} : prng_ctx -∗ - ▷▷ (∀ l, has_prng_state l 0 -∗ WP@{rs} k l @ s {{ Φ }}) -∗ + ▷▷ (∀ l, known_prng l -∗ WP@{rs} k l @ s {{ Φ }}) -∗ WP@{rs} PRNG_NEW k @ s {{ Φ }}. Proof. iIntros "Hh H". iApply (wp_new_hom _ _ _ idfun with "Hh H"). Qed. - Lemma wp_del_k_hom (l : loc) (cont : unitO -n> IT) n s Φ (κ : IT -n> IT) `{!IT_hom κ} : - prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷▷ WP@{rs} κ (cont ()) @ s {{ β, Φ β }} -∗ - WP@{rs} κ (PRNG_DEL_k l cont) @ s {{ Φ }}. - Proof. - iIntros "#Hctx Hp Ha". - unfold PRNG_DEL_k; simpl. - rewrite hom_vis. - iApply wp_subreify_ctx_indep_lift''. - iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". - simpl. - iApply (lc_fupd_elim_later with "Hlc"). - iNext. - iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom". - { iApply (istate_loc_dom with "Hh Hp"). } - destruct Hdom as [x Hx]. - (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,(),(delete l σ),(κ $ cont ()),[]. - iFrame "Hs". - iSplit. - { - iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". - unfold lift_post, state_del. - by rewrite Hread. - } - iSplit; first by rewrite later_map_Next ofe_iso_21. - iNext. - iMod (istate_delete l n σ with "Hh Hp") as "Hh". - iIntros "Hlc Hs". - iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". - { iExists _. iFrame. } - iModIntro. - iSplit. - - by iApply "Ha". - - by iFrame. - Qed. - - Lemma wp_del (l : loc) n s Φ : - prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷ ▷ Φ (RetV ()) -∗ - WP@{rs} PRNG_DEL l @ s {{ Φ }}. - Proof. - iIntros "#Hctx Hl H". - iApply (wp_del_k_hom _ _ _ _ _ idfun with "Hctx Hl [H]"). - do 2 iNext. - iApply wp_val. - iModIntro. done. - Qed. - - Lemma wp_gen_k_hom (l : loc) (cont : natO -n> IT) n s Φ (κ : IT -n> IT) `{!IT_hom κ} : + Lemma wp_gen_k_hom (l : loc) (cont : natO -n> IT) s Φ (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} κ (cont $ read_lcg n) @ s {{ Φ }}) -∗ + ▷ known_prng l -∗ + ▷▷ (known_prng l -∗ ∀ n : nat, WP@{rs} κ (cont n) @ s {{ Φ }}) -∗ WP@{rs} κ (PRNG_GEN_k l cont) @ s {{ Φ }}. Proof. iIntros "#Hctx Hp Ha". - unfold PRNG_GEN_k; simpl. - rewrite hom_vis. + rewrite /PRNG_GEN_k hom_vis. iApply wp_subreify_ctx_indep_lift''. + iSimpl. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". - simpl. + iSimpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. + iPoseProof (istate_read l σ with "Hh Hp") as (m) "%Hread". (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,(read_lcg n),(<[l:=update_lcg n]>σ),(κ (cont $ read_lcg n)),[]. + iExists σ,(read_lcg m),(<[l:=update_lcg m]>σ),(κ (cont $ read_lcg m)),[]. iFrame "Hs". - iSplit. - { - iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". - unfold lift_post, state_gen. - by rewrite Hread. - } - iSplit; first by rewrite ofe_iso_21 later_map_Next. + iSplit; first rewrite /lift_post /state_gen Hread //. + iSplit; first rewrite ofe_iso_21 later_map_Next //. iNext. - iMod (istate_write l n (update_lcg n) σ with "Hh Hp") as "[Hh Hp]". + iMod (istate_write l (update_lcg m) σ with "Hh Hp") as "[Hh Hp]". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } iModIntro. iSplit. - - by iApply "Ha". + - iApply ("Ha" with "Hp"). - by iFrame. Qed. - Lemma wp_gen (l : loc) (n : nat) s Φ : + Lemma wp_gen (l : loc) s Φ : prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷ ▷ (has_prng_state l (update_lcg n) -∗ WP@{rs} (Ret $ read_lcg n) @ s {{ Φ }}) -∗ + ▷ known_prng l -∗ + ▷▷ (known_prng l -∗ ∀ n : nat, Φ (RetV n)) -∗ WP@{rs} PRNG_GEN l @ s {{ Φ }}. Proof. iIntros "#Hcxt Hp Ha". - iApply (wp_gen_k_hom l Ret _ _ _ idfun with "Hcxt Hp Ha"). + iApply (wp_gen_k_hom _ _ _ _ idfun with "Hcxt Hp"). + iIntros "!> !> Hl %n". + iApply wp_val. + iApply ("Ha" with "Hl"). Qed. - Lemma wp_seed_k_hom (l : loc) n (cont : unitO -n> IT) n' s Φ (κ : IT -n> IT) `{!IT_hom κ} : + Lemma wp_seed_k_hom (l : loc) (cont : unitO -n> IT) m s Φ (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷▷ (has_prng_state l n' -∗ WP@{rs} κ (cont ()) @ s {{ Φ }}) -∗ - WP@{rs} κ (PRNG_SEED_k l n' cont) @ s {{ Φ }}. + ▷ known_prng l -∗ + ▷▷ (known_prng l -∗ WP@{rs} κ (cont ()) @ s {{ Φ }}) -∗ + WP@{rs} κ (PRNG_SEED_k l m cont) @ s {{ Φ }}. Proof. iIntros "#Hctx Hp Ha". - unfold PRNG_SEED_k; simpl. - rewrite hom_vis. + rewrite /PRNG_SEED_k hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". - simpl. + iSimpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. (* current state, reification results, new state, continuation, thread pool additions *) - iExists σ,(),(<[l:=n']>σ),(κ (cont ())),[]. + iExists σ,(),(<[l:=m]>σ),(κ (cont ())),[]. iFrame "Hs". iSplit. { - iPoseProof (istate_read l n σ with "Hh Hp") as "%Hread". - unfold lift_post, state_seed. - by rewrite Hread. + iPoseProof (istate_read l σ with "Hh Hp") as (?) "%Hread". + rewrite /lift_post /state_seed Hread //. } - iSplit; first by rewrite ofe_iso_21 later_map_Next. + iSplit; first rewrite ofe_iso_21 later_map_Next //. iNext. - iMod (istate_write l n n' σ with "Hh Hp") as "[Hh Hp]". + iMod (istate_write l m σ with "Hh Hp") as "[Hh Hp]". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } @@ -449,14 +387,14 @@ Section wp. - by iFrame. Qed. - Lemma wp_seed (l : loc) n n' s Φ : + Lemma wp_seed (l : loc) m s Φ : prng_ctx -∗ - ▷ has_prng_state l n -∗ - ▷▷ (has_prng_state l n' -∗ Φ (RetV ())) -∗ - WP@{rs} PRNG_SEED l n' @ s {{ Φ }}. + ▷ known_prng l -∗ + ▷▷ (known_prng l -∗ Φ (RetV ())) -∗ + WP@{rs} PRNG_SEED l m @ s {{ Φ }}. Proof. iIntros "#Hctx Hp Ha". - iApply (wp_seed_k_hom l n Ret _ _ _ idfun with "Hctx Hp [Ha]"). + iApply (wp_seed_k_hom l _ _ _ _ idfun with "Hctx Hp [Ha]"). do 2 iNext. iIntros "H". iDestruct ("Ha" with "H") as "G". @@ -467,6 +405,6 @@ Section wp. End wp. Arguments prng_ctx {_ _} rs {_ _ _ _ _ _}. -Arguments has_prng_state {_ _} _ _. +Arguments known_prng {_ _} _. #[global] Opaque PRNG_NEW PRNG_DEL_k PRNG_GEN_k PRNG_SEED_k. From 1e7ef202f473b6490258e8767939a5f3bd15c41b Mon Sep 17 00:00:00 2001 From: hehelego Date: Tue, 7 Apr 2026 12:29:33 +0200 Subject: [PATCH 16/21] fundamental lemma for PRNG lang logical relation --- theories/examples/prng_lang/logpred.v | 63 ++++++++++----------------- 1 file changed, 22 insertions(+), 41 deletions(-) diff --git a/theories/examples/prng_lang/logpred.v b/theories/examples/prng_lang/logpred.v index d7aaa63..a158491 100644 --- a/theories/examples/prng_lang/logpred.v +++ b/theories/examples/prng_lang/logpred.v @@ -35,7 +35,7 @@ Section prng_logrel. Program Definition val_unit : ITV -n> iProp := λne αv, (αv ≡ RetV ())%I. Program Definition val_prng : ITV -n> iProp := λne αv, - (∃ (l : loc), αv ≡ RetV l ∗ inv (prng_logrel_NS .@ l) (∃ (n : nat), has_prng_state l n))%I. + (∃ (l : loc), αv ≡ RetV l ∗ known_prng l )%I. Solve All Obligations with solve_proper. Program Definition val_arr (Φ1 Φ2 : ITV -n> iProp) := λne αv, @@ -122,38 +122,26 @@ Section prng_logrel. iIntros (ss) "#Hctx #Has". iApply expr_pred_frame. iApply (wp_new rs Ret s with "Hctx"). - iIntros (l). - iIntros "!> !> Hprng". - iAssert ((∃ n, has_prng_state l n)%I) with "[Hprng]" as "HprngEx"; - first by iExists 0. - iMod (inv_alloc (prng_logrel_NS .@ l) with "HprngEx") as "#HprngInv". + iIntros (l) "!> !> Hprng". iApply wp_val. - iModIntro. iExists l. - by iSplit. + by iFrame. Qed. - (* TODO: invariant open problem *) + (* [typed_DelPrng] has been removed. + Deleting a potentially shared PRNG state is generally unsafe. + it is only safe to delete with exclusive ownership. - (* [typed_DelPrng] *) - Lemma compat_DelPrng {S : Set} {Γ : S → ty} α : - ⊢ valid1 Γ α Tprng -∗ - valid1 Γ (interp_del rs α) Tunit. - Proof. - iIntros "H1" (ss) "#Hctx #Has". - iSpecialize ("H1" $! ss with "Hctx Has"). - iApply (expr_pred_bind (get_ret PRNG_DEL) with "H1"). - iIntros (αv) "(%l & Heq & HprngInv) /=". - iRewrite "Heq". rewrite IT_of_V_Ret get_ret_ret. - iApply expr_pred_frame. - (* FIXME: deleting a potentially shared PRNG state is generally unsafe. - it is only safe to delete with exclusive ownership. + Consider the following counterexample program. + + let rng := new_prng in + let rng_share := rng in + delete rng; rand rng_share - let rng := new_prng in - let rng_share := rng in - delete rng; rand rng_share - *) - Admitted. + We have to make a choice. + Either be affine and lose the ability of manual deallocation + or be linear and restrict sharing. + *) (* [typed_Rand] *) Lemma compat_Rand {S : Set} {Γ : S → ty} α : @@ -163,17 +151,13 @@ Section prng_logrel. iIntros "H1" (ss) "#Hctx #Has". iSpecialize ("H1" $! ss with "Hctx Has"). iApply (expr_pred_bind (get_ret PRNG_GEN) with "H1"). - iIntros (αv) "(%l & Heq & HprngInv) /=". + iIntros (αv) "(%l & Heq & #Hprng) /=". iRewrite "Heq". rewrite IT_of_V_Ret get_ret_ret. iApply expr_pred_frame. - (* - iApply (wp_gen rs l n s with "Hctx Hprng"). - iIntros "!> !> Hprng'". - iApply wp_val. - by iExists (read_lcg n). + iApply (wp_gen rs l with "Hctx Hprng"). + iIntros "!> !> Hprng' %n". + by iExists n. Qed. - *) - Admitted. (* [typed_Seed] *) Lemma compat_Seed {S : Set} {Γ : S → ty} α β : @@ -185,19 +169,16 @@ Section prng_logrel. iSpecialize ("H1" $! ss with "Hctx Has"). iSpecialize ("H2" $! ss with "Hctx Has"). iApply (expr_pred_bind (SeedGitCtxL rs (β ss)) with "H1"). - iIntros (αv) "(%l & Heq & HprngInv) /=". + iIntros (αv) "(%l & Heq & #Hprng) /=". iRewrite "Heq"; rewrite IT_of_V_Ret. iApply (expr_pred_bind (SeedGitCtxS rs (Ret l)) with "H2"). iIntros (βv) "(%sd & Heq)". iRewrite "Heq"; rewrite IT_of_V_Ret /SeedGitCtxS SeedGit_Ret. iApply expr_pred_frame. - (* - iApply (wp_seed rs l n sd with "Hctx Hprng"). + iApply (wp_seed rs l with "Hctx Hprng"). iIntros "!> !> Hprng'". done. Qed. - *) - Admitted. Lemma compat_app {S : Set} (Γ : S → ty) α β τ1 τ2 : ⊢ valid1 Γ α (Tarr τ1 τ2) -∗ @@ -291,7 +272,7 @@ Section prng_logrel. + iApply compat_natop; iApply fundamental; eauto. + iApply compat_if; iApply fundamental; eauto. + iApply compat_NewPrng. - + iApply compat_DelPrng; iApply fundamental; eauto. + (* + iApply compat_DelPrng; iApply fundamental; eauto. *) + iApply compat_Rand; iApply fundamental; eauto. + iApply compat_Seed; iApply fundamental; eauto. - destruct 1. From ce149c9ddbb3a34df0c9102bea0e4efb0ed93f26 Mon Sep 17 00:00:00 2001 From: hehelego Date: Tue, 7 Apr 2026 22:23:45 +0200 Subject: [PATCH 17/21] WIP: PRNG ghost theory PRNG state update is incomplete --- theories/effects/prng.v | 121 +++++++++++++++++++++++++++------------- 1 file changed, 82 insertions(+), 39 deletions(-) diff --git a/theories/effects/prng.v b/theories/effects/prng.v index 650ca7d..7f0abe7 100644 --- a/theories/effects/prng.v +++ b/theories/effects/prng.v @@ -1,5 +1,5 @@ (** pseudo random number generator effect *) -From iris.algebra Require Import gmap gmap_view excl auth. +From iris.algebra Require Import gmap gset gmap_view excl agree auth. From iris.proofmode Require Import classes tactics. From iris.base_logic Require Import algebra. From iris.heap_lang Require Export locations. @@ -187,28 +187,37 @@ Section wp. Notation ITV := (ITV F R). Notation stateO := (stateF ♯ IT). - Definition entryR := prodR (agreeR unit) (optionR (exclR nat)). - Definition prngR := gmap_viewR loc entryR. + (* + an insert-only store with anonymous pointsto predicate - Definition owner_entry n : entryR := (to_agree (), Some (Excl n)). - Definition borrow_entry : entryR := (to_agree (), None). - Definition owner_store (m : gmapR loc nat) := owner_entry <$> m. + pointsto l -∗ pointsto l ∗ pointsto l + store σ ∗ pointsto l -∗ ∃ n, σ !! l ≡ Some n + store σ ∗ pointsto l ==∗ <[l:=v]> σ ∗ pointsto l + *) - Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ prngR }. + Definition entryUR := prodUR (optionUR (agreeR unit)) (optionUR (exclR natO)). + Definition prngUR := authUR (gmapUR loc entryUR). + + Definition owner_entry n : entryUR := (Some (to_agree ()), Excl' n). + Definition borrow_entry : entryUR := (Some (to_agree ()), None). + Definition owner_store σ : prngUR := ● (owner_entry <$> σ). + Definition borrow_store l : prngUR := ◯ {[l := borrow_entry]}. + + Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ prngUR }. Class prngG Σ := PrngG { - prngG_inG :: inG Σ prngR; + prngG_inG :: inG Σ prngUR; prngG_name : gname; }. - Definition prngΣ : gFunctors := GFunctor prngR. + Definition prngΣ : gFunctors := GFunctor prngUR. #[export] Instance subG_prngΣ {Σ} : subG prngΣ Σ → prngPreG Σ. Proof. solve_inG. Qed. - Lemma new_storeG σ `{!prngPreG Σ} : - (⊢ |==> ∃ `{!prngG Σ}, own prngG_name (●V σ): iProp Σ)%I. + Lemma new_storeG `{!prngPreG Σ} : + (⊢ |==> ∃ `{!prngG Σ}, own prngG_name (owner_store ∅): iProp Σ)%I. Proof. - iMod (own_alloc (●V σ)) as (γ) "H". + iMod (own_alloc (owner_store ∅)) as (γ) "H1". { - apply gmap_view_auth_valid. + rewrite /owner_store auth_auth_valid //. } set {| prngG_inG := PrngPreG_inG; prngG_name := γ |} as sg. by iExists sg. @@ -222,13 +231,11 @@ Section wp. Notation own := (own prngG_name). Definition has_prngs (σ : gmapR loc nat) := - own $ gmap_view_auth (DfracOwn 1) (owner_store σ). + own $ owner_store σ. Definition known_prng (l : loc) := - own $ gmap_view_frag l DfracDiscarded borrow_entry. + own $ borrow_store l. Definition prng_ctx := inv (nroot.@"prngE") (∃ σ, £ 1 ∗ has_substate σ ∗ has_prngs σ)%I. - (* TODO: find some library functions for proving frame preserving updates of gmap fragmental view weakening *) - Lemma istate_alloc (n : nat) l σ : σ !! l = None → has_prngs σ ==∗ has_prngs (<[l:=n]> σ) ∗ known_prng l. @@ -236,34 +243,70 @@ Section wp. iIntros (Hl) "H". iMod (own_update with "H") as "[Hauth Hfrag]". { - apply (gmap_view_alloc (owner_store σ) l (DfracOwn 1) (owner_entry n)). - - rewrite lookup_fmap Hl //. - - done. - - done. + apply (auth_update_alloc (owner_entry <$> σ) (owner_entry <$> <[l:=n]> σ) {[l := owner_entry n]}). + rewrite fmap_insert. + apply alloc_local_update; last done. + rewrite lookup_fmap Hl //. } - iSplitL "Hauth"; first rewrite /has_prngs /owner_store fmap_insert //. - iMod (own_update with "Hfrag") as "$". - Admitted. + unfold has_prngs, owner_store, borrow_store, known_prng. + iMod (own_update with "Hauth") as "[$ $]"; last done. + { + apply auth_update_dfrac_alloc. + { + apply gmap_core_id. + intros i x H. + rewrite lookup_singleton_Some in H. + destruct H as [<- <-]. + rewrite /CoreId /borrow_entry //. + } + apply singleton_included_l. + exists (owner_entry n). + rewrite lookup_fmap lookup_insert. + split; first done. + apply Some_included_mono. + exists (owner_entry n). + unfold owner_entry, borrow_entry. + rewrite -pair_op -Some_op. + split; cbn; trivial. + by rewrite agree_idemp. + } + Qed. Lemma istate_read l σ : has_prngs σ -∗ known_prng l - -∗ ∃ n, (σ !! l) ≡ Some n. + -∗ has_prngs σ ∗ ∃ n, (σ !! l) ≡ Some n. Proof. iIntros "Ha Hf". - iPoseProof (own_valid_2 with "Ha Hf") as "H". - rewrite gmap_view_both_dfrac_validI. - iDestruct "H" as (n dq Hvalid1 Hlookup Hvalid2 OtherPart) "%Heq". - rewrite lookup_fmap in Hlookup. - Admitted. + iPoseProof (own_valid_2 with "Ha Hf") as "%H". + iFrame. + rewrite /owner_store /borrow_store auth_both_valid_discrete in H. + destruct H as [H _]. + apply singleton_included_l in H. + destruct H as ([] & H1 & H2). + rewrite lookup_fmap in H1. + destruct (σ !! l) as [x|] eqn:Hlookup. + - by iExists x. + - rewrite Hlookup in H1. + simpl in H1. + inversion H1. + Qed. Lemma istate_write l n' σ : has_prngs σ -∗ known_prng l - ==∗ has_prngs (<[l:=n']> σ) ∗ known_prng l. + ==∗ has_prngs (<[l:=n']> σ). Proof. - iIntros "H Hl". - iMod (own_update_2 with "H Hl") as "[$ $]"; last done. + iIntros "H #Hl". + iPoseProof (istate_read l σ with "H Hl") as "(H & [%n %Hlookup])". + iMod (own_update_2 with "H Hl") as "[$ _]"; last done. + unfold owner_store, borrow_store. + rewrite fmap_insert. + apply auth_update. + eapply singleton_local_update. + - rewrite lookup_fmap Hlookup //. + - unfold owner_entry, borrow_entry. + apply prod_local_update; simpl. Admitted. Lemma wp_new_hom (k : locO -n> IT) s Φ `{!NonExpansive Φ} (κ : IT -n> IT) `{!IT_hom κ} : @@ -316,7 +359,7 @@ Section wp. ▷▷ (known_prng l -∗ ∀ n : nat, WP@{rs} κ (cont n) @ s {{ Φ }}) -∗ WP@{rs} κ (PRNG_GEN_k l cont) @ s {{ Φ }}. Proof. - iIntros "#Hctx Hp Ha". + iIntros "#Hctx #Hp Ha". rewrite /PRNG_GEN_k hom_vis. iApply wp_subreify_ctx_indep_lift''. iSimpl. @@ -324,14 +367,14 @@ Section wp. iSimpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. - iPoseProof (istate_read l σ with "Hh Hp") as (m) "%Hread". + iPoseProof (istate_read l σ with "Hh Hp") as "(Hh & %m & %Hread)". (* current state, reification results, new state, continuation, thread pool additions *) iExists σ,(read_lcg m),(<[l:=update_lcg m]>σ),(κ (cont $ read_lcg m)),[]. iFrame "Hs". iSplit; first rewrite /lift_post /state_gen Hread //. iSplit; first rewrite ofe_iso_21 later_map_Next //. iNext. - iMod (istate_write l (update_lcg m) σ with "Hh Hp") as "[Hh Hp]". + iMod (istate_write l (update_lcg m) σ with "Hh Hp") as "Hh". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } @@ -360,7 +403,7 @@ Section wp. ▷▷ (known_prng l -∗ WP@{rs} κ (cont ()) @ s {{ Φ }}) -∗ WP@{rs} κ (PRNG_SEED_k l m cont) @ s {{ Φ }}. Proof. - iIntros "#Hctx Hp Ha". + iIntros "#Hctx #Hp Ha". rewrite /PRNG_SEED_k hom_vis. iApply wp_subreify_ctx_indep_lift''. iInv (nroot.@"prngE") as (σ) "[>Hlc [Hs Hh]]" "Hcl". @@ -372,12 +415,12 @@ Section wp. iFrame "Hs". iSplit. { - iPoseProof (istate_read l σ with "Hh Hp") as (?) "%Hread". + iPoseProof (istate_read l σ with "Hh Hp") as "(Hh & %mm & %Hread)". rewrite /lift_post /state_seed Hread //. } iSplit; first rewrite ofe_iso_21 later_map_Next //. iNext. - iMod (istate_write l m σ with "Hh Hp") as "[Hh Hp]". + iMod (istate_write l m σ with "Hh Hp") as "Hh". iIntros "Hlc Hs". iMod ("Hcl" with "[Hlc Hh Hs]") as "Hemp". { iExists _. iFrame. } From 3bca8ad89e04b1677992082c9b96f9bab21be785 Mon Sep 17 00:00:00 2001 From: hehelego Date: Fri, 10 Apr 2026 01:06:05 +0200 Subject: [PATCH 18/21] finish PRNG ghost theory --- theories/effects/prng.v | 143 ++++++++++++++++++++-------------------- 1 file changed, 71 insertions(+), 72 deletions(-) diff --git a/theories/effects/prng.v b/theories/effects/prng.v index 7f0abe7..1baabdc 100644 --- a/theories/effects/prng.v +++ b/theories/effects/prng.v @@ -1,5 +1,5 @@ (** pseudo random number generator effect *) -From iris.algebra Require Import gmap gset gmap_view excl agree auth. +From iris.algebra Require Import gmap gset mono_nat gmap_view excl agree auth. From iris.proofmode Require Import classes tactics. From iris.base_logic Require Import algebra. From iris.heap_lang Require Export locations. @@ -195,32 +195,36 @@ Section wp. store σ ∗ pointsto l ==∗ <[l:=v]> σ ∗ pointsto l *) - Definition entryUR := prodUR (optionUR (agreeR unit)) (optionUR (exclR natO)). - Definition prngUR := authUR (gmapUR loc entryUR). + Definition storeR := exclR (gmapUR loc nat). + Definition locR := authR (gsetR loc). - Definition owner_entry n : entryUR := (Some (to_agree ()), Excl' n). - Definition borrow_entry : entryUR := (Some (to_agree ()), None). - Definition owner_store σ : prngUR := ● (owner_entry <$> σ). - Definition borrow_store l : prngUR := ◯ {[l := borrow_entry]}. - - Class prngPreG Σ := PrngPreG { PrngPreG_inG :: inG Σ prngUR }. + Class prngPreG Σ := PrngPreG { + PrngPreG_V_inG :: inG Σ storeR; + PrngPreG_K_inG :: inG Σ locR; + }. Class prngG Σ := PrngG { - prngG_inG :: inG Σ prngUR; - prngG_name : gname; + prngG_V_inG :: inG Σ storeR; + prngG_K_inG :: inG Σ locR; + prngG_nameV : gname; + prngG_nameK : gname; }. - Definition prngΣ : gFunctors := GFunctor prngUR. + Definition prngΣ : gFunctors := #[GFunctor storeR; GFunctor locR]. #[export] Instance subG_prngΣ {Σ} : subG prngΣ Σ → prngPreG Σ. Proof. solve_inG. Qed. Lemma new_storeG `{!prngPreG Σ} : - (⊢ |==> ∃ `{!prngG Σ}, own prngG_name (owner_store ∅): iProp Σ)%I. + ⊢ |==> ∃ `{!prngG Σ}, own prngG_nameV (Excl ∅) + ∗ own prngG_nameK (● ∅ ⋅ ◯ ∅). Proof. - iMod (own_alloc (owner_store ∅)) as (γ) "H1". - { - rewrite /owner_store auth_auth_valid //. - } - set {| prngG_inG := PrngPreG_inG; prngG_name := γ |} as sg. - by iExists sg. + iMod (own_alloc (Excl ∅)) as (gn1) "H1"; first done. + iMod (own_alloc (● ∅ ⋅ ◯ ∅)) as (gn2) "H2"; first by apply auth_both_valid. + iModIntro. + set {| + prngG_V_inG := PrngPreG_V_inG; prngG_nameV := gn1; + prngG_K_inG := PrngPreG_K_inG; prngG_nameK := gn2; + |} as sg. + iExists sg. + iFrame. Qed. Context `{!subReifier (sReifier_NotCtxDep_min reify_prng a) rs}. @@ -229,47 +233,32 @@ Section wp. Context `{!prngG Σ}. - Notation own := (own prngG_name). - Definition has_prngs (σ : gmapR loc nat) := - own $ owner_store σ. - Definition known_prng (l : loc) := - own $ borrow_store l. + Notation ownV := (own prngG_nameV). + Notation ownK := (own prngG_nameK). + Definition has_prngs (σ : gmap loc nat) : iProp := ownV (Excl σ) ∗ ownK (● (dom σ)). + Definition known_prng (l : loc) := ownK (◯ {[ l ]}). Definition prng_ctx := inv (nroot.@"prngE") (∃ σ, £ 1 ∗ has_substate σ ∗ has_prngs σ)%I. Lemma istate_alloc (n : nat) l σ : σ !! l = None → has_prngs σ ==∗ has_prngs (<[l:=n]> σ) ∗ known_prng l. Proof. - iIntros (Hl) "H". - iMod (own_update with "H") as "[Hauth Hfrag]". + iIntros (Hl) "[HV HK]". + + iMod (own_update _ _ (Excl $ <[l:=n]>σ) with "HV") as "$". { - apply (auth_update_alloc (owner_entry <$> σ) (owner_entry <$> <[l:=n]> σ) {[l := owner_entry n]}). - rewrite fmap_insert. - apply alloc_local_update; last done. - rewrite lookup_fmap Hl //. + by intros ?[[]|][]. } - unfold has_prngs, owner_store, borrow_store, known_prng. - iMod (own_update with "Hauth") as "[$ $]"; last done. + rewrite dom_insert. + iMod (own_update with "HK") as "[$ HK']". { - apply auth_update_dfrac_alloc. - { - apply gmap_core_id. - intros i x H. - rewrite lookup_singleton_Some in H. - destruct H as [<- <-]. - rewrite /CoreId /borrow_entry //. - } - apply singleton_included_l. - exists (owner_entry n). - rewrite lookup_fmap lookup_insert. - split; first done. - apply Some_included_mono. - exists (owner_entry n). - unfold owner_entry, borrow_entry. - rewrite -pair_op -Some_op. - split; cbn; trivial. - by rewrite agree_idemp. + apply auth_update_alloc. + apply gset_local_update. + apply union_subseteq_r. } + assert ({[l]} ∪ dom σ ≡ {[l]} ⋅ dom σ) as -> by done. + iDestruct "HK'" as "[? ?]". + by iFrame. Qed. Lemma istate_read l σ : @@ -277,19 +266,23 @@ Section wp. -∗ known_prng l -∗ has_prngs σ ∗ ∃ n, (σ !! l) ≡ Some n. Proof. - iIntros "Ha Hf". - iPoseProof (own_valid_2 with "Ha Hf") as "%H". + iIntros "[HV HK] Hf". + iPoseProof (own_valid_2 with "HK Hf") as "%H". iFrame. - rewrite /owner_store /borrow_store auth_both_valid_discrete in H. - destruct H as [H _]. - apply singleton_included_l in H. - destruct H as ([] & H1 & H2). - rewrite lookup_fmap in H1. - destruct (σ !! l) as [x|] eqn:Hlookup. - - by iExists x. - - rewrite Hlookup in H1. - simpl in H1. - inversion H1. + iPureIntro. + apply auth_both_valid_discrete in H. + destruct H as [[] _]. + assert (l ∈ dom σ) as Hin. + { + rewrite H. + apply elem_of_union_l. + apply elem_of_singleton. + done. + } + pose proof (elem_of_dom σ l) as [Hlk _]. + pose proof (Hlk Hin) as [? ?]. + exists x0. + by rewrite H0. Qed. Lemma istate_write l n' σ : @@ -298,16 +291,22 @@ Section wp. ==∗ has_prngs (<[l:=n']> σ). Proof. iIntros "H #Hl". - iPoseProof (istate_read l σ with "H Hl") as "(H & [%n %Hlookup])". - iMod (own_update_2 with "H Hl") as "[$ _]"; last done. - unfold owner_store, borrow_store. - rewrite fmap_insert. - apply auth_update. - eapply singleton_local_update. - - rewrite lookup_fmap Hlookup //. - - unfold owner_entry, borrow_entry. - apply prod_local_update; simpl. - Admitted. + iPoseProof (istate_read l σ with "H Hl") as "([HV HK] & [%n %Hlookup])". + unfold has_prngs. + + iMod (own_update _ _ (Excl $ <[l:=n']>σ) with "HV") as "$". + { + by intros ?[[]|][]. + } + rewrite dom_insert. + iMod (own_update with "HK") as "[$ HK']". + { + apply auth_update_alloc. + apply gset_local_update. + apply union_subseteq_r. + } + done. + Qed. Lemma wp_new_hom (k : locO -n> IT) s Φ `{!NonExpansive Φ} (κ : IT -n> IT) `{!IT_hom κ} : prng_ctx -∗ From c44c6cf3428958023bc1306f852d9a76b84e4044 Mon Sep 17 00:00:00 2001 From: hehelego Date: Fri, 10 Apr 2026 22:38:34 +0200 Subject: [PATCH 19/21] complete the adequacy and safety proofs for the PRNG lang --- _CoqProject | 1 - theories/effects/prng.v | 10 ++-- theories/examples/prng_lang/logpred.v | 84 ++++++++++++++------------- 3 files changed, 50 insertions(+), 45 deletions(-) diff --git a/_CoqProject b/_CoqProject index 431aa96..874af82 100644 --- a/_CoqProject +++ b/_CoqProject @@ -92,7 +92,6 @@ theories/examples/prng_lang/prng_seed_combinator.v theories/examples/prng_lang/lang.v theories/examples/prng_lang/interp.v theories/examples/prng_lang/logpred.v -theories/examples/prng_lang/logrel.v theories/utils/finite_sets.v theories/utils/clwp.v diff --git a/theories/effects/prng.v b/theories/effects/prng.v index 1baabdc..30af304 100644 --- a/theories/effects/prng.v +++ b/theories/effects/prng.v @@ -212,12 +212,12 @@ Section wp. #[export] Instance subG_prngΣ {Σ} : subG prngΣ Σ → prngPreG Σ. Proof. solve_inG. Qed. - Lemma new_storeG `{!prngPreG Σ} : - ⊢ |==> ∃ `{!prngG Σ}, own prngG_nameV (Excl ∅) - ∗ own prngG_nameK (● ∅ ⋅ ◯ ∅). + Lemma new_prngG σ `{!prngPreG Σ} : + ⊢ |==> ∃ `{!prngG Σ}, own prngG_nameV (Excl σ) + ∗ own prngG_nameK (● dom σ). Proof. - iMod (own_alloc (Excl ∅)) as (gn1) "H1"; first done. - iMod (own_alloc (● ∅ ⋅ ◯ ∅)) as (gn2) "H2"; first by apply auth_both_valid. + iMod (own_alloc (Excl σ)) as (gn1) "H1"; first done. + iMod (own_alloc (● dom σ)) as (gn2) "H2"; first by apply auth_auth_valid. iModIntro. set {| prngG_V_inG := PrngPreG_V_inG; prngG_nameV := gn1; diff --git a/theories/examples/prng_lang/logpred.v b/theories/examples/prng_lang/logpred.v index a158491..0b6146b 100644 --- a/theories/examples/prng_lang/logpred.v +++ b/theories/examples/prng_lang/logpred.v @@ -25,8 +25,6 @@ Section prng_logrel. Context {A : ofe}. Variable (P : A -n> iProp). - Definition prng_logrel_NS : namespace := nroot .@ "prng-logrel". - (* expr_pred: gitree value predicate -> gitree predicate *) Local Notation expr_pred := (expr_pred s rs P). @@ -53,7 +51,6 @@ Section prng_logrel. (* subst_valid: (S : Names) (Γ : Context S) -> interptation of Γ -> iProp *) Notation ssubst_valid := (ssubst_valid1 rs ty val_pred expr_pred). - (* we made [Tprng] persistent by wrapping the [pointsto]/[has_prng_state] predicate in an invariant *) #[global] Instance prng_lang_val_pred_persist τ βv : Persistent (val_pred τ βv). Proof. induction τ; try apply _. Qed. @@ -300,7 +297,7 @@ Local Definition rs : gReifiers NotCtxDep _ := gReifiers_cons reify_prng gReifie #[local] Parameter Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. -Program Definition InputLangGitreeGS {R} `{!Cofe R} +Program Definition PrngLangGitreeGS {R} `{!Cofe R} {a : is_ctx_dep} {n} (rs : gReifiers a n) (Σ : gFunctors) (H1 : invGS Σ) (H2 : stateG rs R Σ) @@ -324,18 +321,16 @@ Next Obligation. - by iDestruct "H" as "(_ & ?)". Qed. -(* TODO: adeequacy and safety proof for the PRNG lang - adapt the proofs for input-lang. -*) +(* XXX: need this command to typecheck [β ≡ Err e] *) +Open Scope stdpp. -(* -Lemma logpred_adequacy cr Σ R - `{!Cofe R, !SubOfe natO R, !SubOfe logO R, !SubOfe unitO R} +Lemma logpred_adequacy (cr : nat) Σ R + `{!Cofe R, !SubOfe natO R, !SubOfe unitO R, !SubOfe locO R} `{!invGpreS Σ} `{!statePreG rs R Σ} `{!prngPreG Σ} (τ : ty) (α : interp_scope ∅ -n> IT (gReifiers_ops rs) R) (β : IT (gReifiers_ops rs) R) st st' k : - (∀ `{H1 : !gitreeGS_gen rs R Σ}, + (∀ `{H1 : !gitreeGS_gen rs R Σ} `{H2 : !prngG Σ}, (£ cr ⊢ valid1 rs notStuck (λne _ : unitO, True)%I □ α τ)%I) → external_steps (gReifiers_sReifier rs) (α ı_scope) st β st' [] k → is_Some (IT_to_V β) @@ -346,9 +341,10 @@ Proof. eapply (wp_progress_gen Σ 1 NotCtxDep rs (S cr) (λ x, x) notStuck [] k (α ı_scope) β st st' Hdisj Hst). intros H1 H2. - pose H3 : gitreeGS_gen rs R Σ := InputLangGitreeGS rs Σ H1 H2. + pose H3 : gitreeGS_gen rs R Σ := PrngLangGitreeGS rs Σ H1 H2. simpl in H3. - exists (val_pred (s:=notStuck) (P:=(λne _:unitO, True)) τ)%I. split. + exists (λ _, True)%I. split. + (*exists (val_pred (s:=notStuck) (P:=(λne _:unitO, True)) τ)%I. split.*) { apply _. } iExists (@state_interp_fun _ _ rs _ _ _ H3). iExists (@aux_interp_fun _ _ rs _ _ _ H3). @@ -360,7 +356,6 @@ Proof. simpl. iAssert (True%I) as "G"; first done; iFrame "G"; iClear "G". iModIntro. iIntros "((Hone & Hcr) & Hst)". - iPoseProof (Hlog H3 with "Hcr") as "Hlog". destruct st as [σ []]. iAssert (has_substate σ) with "[Hst]" as "Hs". { @@ -379,32 +374,44 @@ Proof. rewrite (eq_pi _ _ Heq eq_refl)//. } iApply fupd_wp. - iMod (inv_alloc (nroot.@"ioE") _ - (∃ σ, + iMod (new_prngG σ) as (H4) "Hprng". + iMod (inv_alloc (nroot.@"prngE") _ + (∃ σ : state, £ 1 ∗ has_substate (σ : oFunctor_car - (sReifier_state reify_io) + (sReifier_state reify_prng) (IT (sReifier_ops (gReifiers_sReifier rs)) R) - (IT (sReifier_ops (gReifiers_sReifier rs)) R)))%I - with "[Hone Hs]") as "#Hinv". - { - iNext. iExists σ. - iFrame "Hone Hs". - } - iSpecialize ("Hlog" with "Hinv []"). + (IT (sReifier_ops (gReifiers_sReifier rs)) R)) + ∗ has_prngs σ)%I + with "[Hone Hs Hprng]") as "#Hinv". { - iIntros (x). - destruct x. + iNext. iExists σ. iFrame. } - iSpecialize ("Hlog" $! tt with "[//]"). - iApply (wp_wand with"Hlog"). + iSimpl in "Hinv". + iPoseProof (Hlog H3 with "Hcr") as "Hlog". + iSpecialize ("Hlog" $! ı_scope). + iSpecialize ("Hlog" with "Hinv"). + iAssert (ssubst_valid1 rs ty val_pred + (expr_pred notStuck rs (λne _ : unitO, True)%I) □ ı_scope) as "Hvalid". + { + by iIntros "%Hempty". + } + iSpecialize ("Hlog" with "Hvalid"). + iSpecialize ("Hlog" $! () I). + iApply (wp_wand with "Hlog"). iModIntro. - iIntros ( βv). simpl. iDestruct 1 as (_) "[H _]". - by iFrame. + iIntros (βv) "_". + done. Qed. -Lemma prng_lang_safety e τ σ st' (β : IT (sReifier_ops (gReifiers_sReifier rs)) natO) k : +Let R := sumO natO (sumO unitO locO). +Let sRef := gReifiers_sReifier rs. +Let sOps := sReifier_ops sRef. +Let IT := IT sOps R. +Let fullState := sReifier_state sRef ♯ IT. + +Lemma prng_lang_safety e τ (st st' : fullState) (β : IT) k : typed □ e τ → - external_steps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) (σ, ()) β st' [] k → + external_steps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) st β st' [] k → is_Some (IT_to_V β) ∨ (∃ β1 st1 l, external_step (gReifiers_sReifier rs) β st' β1 st1 l). Proof. @@ -418,15 +425,14 @@ Proof. - by right. - done. } - pose (Σ:=#[invΣ;stateΣ rs natO]). - assert (invGpreS Σ). - { apply _. } - assert (statePreG rs natO Σ). - { apply _. } + pose (Σ:=#[invΣ;stateΣ rs R;prngΣ]). + assert (invGpreS Σ) by apply _. + assert (statePreG rs R Σ) by apply _. + assert (prngPreG Σ) by apply _. eapply (logpred_adequacy 0 Σ); eauto. - intros ?. iIntros "_". + intros ??. iIntros "_". by iApply fundamental. Qed. -*) End safety_adeqaucy. +Print Assumptions prng_lang_safety. From a3156ebcf0ebb180d8e39f4ac620ee122f88767c Mon Sep 17 00:00:00 2001 From: hehelego Date: Sat, 11 Apr 2026 20:37:04 +0200 Subject: [PATCH 20/21] add an example GIT program with PRNG and its safety proof --- _CoqProject | 1 + theories/examples/prng_lang/prng_examples.v | 97 +++++++++++++++++++++ 2 files changed, 98 insertions(+) create mode 100644 theories/examples/prng_lang/prng_examples.v diff --git a/_CoqProject b/_CoqProject index 874af82..990b006 100644 --- a/_CoqProject +++ b/_CoqProject @@ -89,6 +89,7 @@ theories/examples/heap_lang/pretty.v theories/examples/heap_lang/tactics.v theories/examples/prng_lang/prng_seed_combinator.v +theories/examples/prng_lang/prng_examples.v theories/examples/prng_lang/lang.v theories/examples/prng_lang/interp.v theories/examples/prng_lang/logpred.v diff --git a/theories/examples/prng_lang/prng_examples.v b/theories/examples/prng_lang/prng_examples.v new file mode 100644 index 0000000..933c3ee --- /dev/null +++ b/theories/examples/prng_lang/prng_examples.v @@ -0,0 +1,97 @@ +(* + Examples demonstrating programming and reasoning with the PRNG effect. + Randomized algorithms and their partial correctness. + *) +From gitrees Require Import gitree program_logic. +From gitrees.effects Require Import prng store. +From gitrees.lib Require Import while. + +Section prng_examples. + Context {sz : nat} (rs : gReifiers NotCtxDep sz). + Context `{!subReifier reify_store rs}. + Context `{!subReifier reify_prng rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R, !SubOfe unitO R, !SubOfe locO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + + Context `{!gitreeGS_gen rs R Σ}. + Context `{!heapG rs R Σ} `{prngG Σ}. + Notation iProp := (iProp Σ). + + Notation wp_new := (wp_new rs). + Notation wp_seed := (wp_seed rs). + Notation wp_gen := (wp_gen rs). + Notation wp_alloc := (wp_alloc rs). + Notation wp_read := (wp_read rs). + Notation wp_write := (wp_write rs). + Notation wp_bind := (wp_bind rs). + + Definition neg_bool : IT -> IT := NATOP Nat.sub (Ret 1). + + Definition las_vegas_ITF (sd : nat) (init : nat) (test : IT) : IT := + PRNG_NEW $ λne r, + ALLOC (Ret init) $ λne s, + SEQ (PRNG_SEED r sd) $ + SEQ (WHILE + (neg_bool (test ⊙ (READ s))) + (LET (PRNG_GEN r) (WRITE s))) $ + READ s. + + Lemma wp_las_vegas_ITF (f : nat -> bool) (fIT : IT) (sd : nat) (init : nat) : + heap_ctx rs + -∗ prng_ctx rs + -∗ □ (∀ n, WP@{rs} fIT ⊙ (Ret n) {{ β, β ≡ RetV (if f n then 1 else 0) }}) + -∗ WP@{rs} las_vegas_ITF sd init fIT {{ β, ∃ n, β ≡ RetV n ∧ f n ≡ true }}. + Proof with (try solve_proper). + (* preamble *) + rewrite /las_vegas_ITF. + iIntros "#Hheap #Hprng #Hf". + iApply (wp_new with "Hprng")... + iIntros "!>!> %r #Hr /=". + iApply (wp_alloc with "Hheap")... + iIntros "!>!> %s Hl /=". + iApply wp_seq... + iApply (wp_seed with "Hprng Hr"). + iIntros "!>!> _ /=". + (* repeated retry *) + iApply (wp_bind (SEQCtx _) _)... + iLöb as "IH" forall (init). + rewrite {2}(WHILE_eq _ _). + iApply (wp_bind (IFSCtx _ _) _)... + iApply (wp_bind neg_bool _)... + iApply (wp_bind (AppRSCtx fIT) _)... + iApply (wp_read with "Hheap Hl"). + iIntros "!>!> Hl /=". + iApply wp_val; iModIntro. + iPoseProof ("Hf" $! init) as "Hf0". + rewrite /AppRSCtx IT_of_V_Ret. + iApply (wp_wand with "Hf0"). + iIntros "%v Hv !>". + iRewrite "Hv". + rewrite /IFSCtx IT_of_V_Ret. + destruct (f init) eqn:Hdec; + rewrite /neg_bool NATOP_Ret /=; + iApply wp_val; iModIntro; + rewrite IT_of_V_Ret. + - rewrite IF_False; last lia. + iApply wp_val; iModIntro. + rewrite /SEQCtx IT_of_V_Ret SEQ_Val. + iApply (wp_read with "Hheap Hl"). + iIntros "!>!> _". + iApply wp_val; iModIntro. + by iExists init. + - rewrite IF_True; last lia. + iApply (wp_bind (SEQCtx _) _)... + iApply wp_let... + iApply (wp_gen with "Hprng Hr"). + iIntros "!>!> _ %n". + iApply (wp_write with "Hheap Hl"). + iIntros "!>!> Hl". + rewrite /SEQCtx !IT_of_V_Ret SEQ_Val. + iApply wp_tick. + iIntros "!> _". + iApply ("IH" $! n with "Hl"). + Qed. +End prng_examples. From c9a412d51c05dff97d7861ec70d5220bac3b8fc7 Mon Sep 17 00:00:00 2001 From: hehelego Date: Tue, 14 Apr 2026 11:23:44 +0200 Subject: [PATCH 21/21] PRNG lang gitree denotational semantics adequacy with respect to the operational semantics --- _CoqProject | 1 + theories/effects/prng.v | 115 ++++- theories/examples/prng_lang/logrel.v | 603 +++++++++++++++++++++++++++ 3 files changed, 714 insertions(+), 5 deletions(-) diff --git a/_CoqProject b/_CoqProject index 990b006..ab16f99 100644 --- a/_CoqProject +++ b/_CoqProject @@ -93,6 +93,7 @@ theories/examples/prng_lang/prng_examples.v theories/examples/prng_lang/lang.v theories/examples/prng_lang/interp.v theories/examples/prng_lang/logpred.v +theories/examples/prng_lang/logrel.v theories/utils/finite_sets.v theories/utils/clwp.v diff --git a/theories/effects/prng.v b/theories/effects/prng.v index 30af304..08b41bb 100644 --- a/theories/effects/prng.v +++ b/theories/effects/prng.v @@ -264,7 +264,7 @@ Section wp. Lemma istate_read l σ : has_prngs σ -∗ known_prng l - -∗ has_prngs σ ∗ ∃ n, (σ !! l) ≡ Some n. + -∗ ∃ n, (σ !! l) ≡ Some n. Proof. iIntros "[HV HK] Hf". iPoseProof (own_valid_2 with "HK Hf") as "%H". @@ -291,9 +291,9 @@ Section wp. ==∗ has_prngs (<[l:=n']> σ). Proof. iIntros "H #Hl". - iPoseProof (istate_read l σ with "H Hl") as "([HV HK] & [%n %Hlookup])". + iPoseProof (istate_read l σ with "H Hl") as "[%n %Hlk]". unfold has_prngs. - + iDestruct "H" as "[HV HK]". iMod (own_update _ _ (Excl $ <[l:=n']>σ) with "HV") as "$". { by intros ?[[]|][]. @@ -366,7 +366,7 @@ Section wp. iSimpl. iApply (lc_fupd_elim_later with "Hlc"). iNext. - iPoseProof (istate_read l σ with "Hh Hp") as "(Hh & %m & %Hread)". + iPoseProof (istate_read l σ with "Hh Hp") as "(%m & %Hread)". (* current state, reification results, new state, continuation, thread pool additions *) iExists σ,(read_lcg m),(<[l:=update_lcg m]>σ),(κ (cont $ read_lcg m)),[]. iFrame "Hs". @@ -414,7 +414,7 @@ Section wp. iFrame "Hs". iSplit. { - iPoseProof (istate_read l σ with "Hh Hp") as "(Hh & %mm & %Hread)". + iPoseProof (istate_read l σ with "Hh Hp") as "(%mm & %Hread)". rewrite /lift_post /state_seed Hread //. } iSplit; first rewrite ofe_iso_21 later_map_Next //. @@ -444,6 +444,111 @@ Section wp. by iModIntro. Qed. + (* [wp_new_state], [wp_gen_state], and [wp_seed_state] are proof rules with explict and exclusive state ownership *) + + Lemma wp_new_state (k : locO -n> IT) s σ Φ `{!NonExpansive Φ} : + let l:=Loc.fresh (dom σ) in + has_substate σ -∗ + has_prngs σ -∗ + ▷▷ (has_substate (<[l := 0]>σ) -∗ + has_prngs (<[l := 0]>σ) -∗ + known_prng l -∗ + WP@{rs} k l @ s {{ Φ }}) -∗ + WP@{rs} PRNG_NEW k @ s {{ Φ }}. + Proof. + iIntros (l) "Hs Hp Ha". + iApply wp_subreify_ctx_indep_lift''. + iExists σ,l,(<[l:=0]>σ),_,[]. + iFrame "Hs". + iModIntro. + iSplit; first done. + iSplit; first done. + iNext. + iMod (istate_alloc 0 l with "Hp") as "[Hp Hl]". + { + apply not_elem_of_dom_1. + rewrite -(Loc.add_0 l). + by apply Loc.fresh_fresh. + } + iIntros "Hlc Hs". + iModIntro. + iSplit. + { + rewrite ofe_iso_21. + iApply fupd_wp. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + iApply ("Ha" with "Hs Hp Hl"). + } + by cbn. + Qed. + + Lemma wp_gen_state l n s σ Φ : + let n' := update_lcg n in + σ !! l = Some n → + has_substate σ -∗ + has_prngs σ -∗ + known_prng l -∗ + ▷▷ (has_substate (<[l := n']>σ) -∗ + has_prngs (<[l := n']>σ) -∗ + known_prng l -∗ + Φ (RetV $ read_lcg n)) -∗ + WP@{rs} PRNG_GEN l @ s {{ Φ }}. + Proof. + iIntros (n' Hlk) "Hs Hp #Hl Ha". + iApply wp_subreify_ctx_indep_lift''. + iExists σ,(read_lcg n),(<[l:=n']>σ),_,[]. + iFrame "Hs". + iModIntro. + iSplit; first rewrite /= /state_gen Hlk //. + iSplit; first done. + iNext. + iIntros "Hlc Hs". + iMod (istate_write l (update_lcg n) σ with "Hp Hl") as "Hp". + iModIntro. + iSplit. + { + rewrite ofe_iso_21. + iApply wp_val. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + iApply ("Ha" with "Hs Hp Hl"). + } + by cbn. + Qed. + + Lemma wp_seed_state l m s σ Φ : + has_substate σ -∗ + has_prngs σ -∗ + known_prng l -∗ + ▷▷ (has_substate (<[l := m]>σ) -∗ + has_prngs (<[l := m]>σ) -∗ + known_prng l -∗ + Φ (RetV ())) -∗ + WP@{rs} PRNG_SEED l m @ s {{ Φ }}. + Proof. + iIntros "Hs Hp #Hl Ha". + iPoseProof (istate_read l σ with "Hp Hl") as "(%n & %Hread)". + iApply wp_subreify_ctx_indep_lift''. + iExists σ,(),(<[l:=m]>σ),_,[]. + iFrame "Hs". + iModIntro. + iSplit; first rewrite /= /state_seed Hread //. + iSplit; first done. + iNext. + iIntros "Hlc Hs". + iMod (istate_write l m σ with "Hp Hl") as "Hp". + iModIntro. + iSplit. + { + rewrite ofe_iso_21. + iApply wp_val. + iApply (lc_fupd_elim_later with "Hlc"). + iNext. + iApply ("Ha" with "Hs Hp Hl"). + } + by cbn. + Qed. End wp. Arguments prng_ctx {_ _} rs {_ _ _ _ _ _}. diff --git a/theories/examples/prng_lang/logrel.v b/theories/examples/prng_lang/logrel.v index e69de29..591ed2c 100644 --- a/theories/examples/prng_lang/logrel.v +++ b/theories/examples/prng_lang/logrel.v @@ -0,0 +1,603 @@ +(* Adequacy of the gitrees denotational semantics with respect to the operational semantics for the PRNG language. + gitree interpretation steps implies PRNG operational semantics steps. + + Soundness, the converse, that PRNG operational semantics steps implies gitree interpretation steps, is already proved [prng_lang/interp.v] + *) +From gitrees Require Import gitree program_logic lang_generic. +From gitrees.examples.prng_lang Require Import lang interp prng_seed_combinator. +From gitrees.effects Require Import prng. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Import IF_nat. + +Section prng_logrel. + Context {sz : nat}. + Variable rs : gReifiers NotCtxDep sz. + Context `{!subReifier reify_prng rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R} `{!SubOfe locO R} `{!SubOfe unitO R} . + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!prngG Σ, !gitreeGS_gen rs R Σ, !na_invG Σ}. + Notation iProp := (iProp Σ). + Variable s : stuckness. + + Notation wp_wand := (wp_wand rs). + Notation wp_bind := (wp_bind rs). + Notation wp_new := (wp_new_state rs). + Notation wp_seed := (wp_seed_state rs). + Notation wp_gen := (wp_gen_state rs). + + Canonical Structure exprO S := leibnizO (expr S). + Canonical Structure valO S := leibnizO (val S). + Canonical Structure stateO := prng.stateO. + + (* (state, gitree program) steps to (post-state, gitree value) + implies + (state, PL program) steps (post-state, PL value) + such that the gitree values is related to the PL value *) + Definition expr_rel {S} (Φ : ITV → val S → iProp) (α : IT) (e : expr S) : iProp := + ∀ (σ : prng.state), has_substate σ -∗ has_prngs σ -∗ + WP@{rs} α @ s {{ βv, ∃ m v σ', ⌜prim_steps e σ (Val v) σ' m⌝ + ∗ has_substate σ' + ∗ has_prngs σ' + ∗ Φ βv v }}. + + #[export] Instance expr_rel_ne {S} (V : ITV → val S → iProp) : + NonExpansive2 V → NonExpansive2 (expr_rel V). + Proof. + unfold expr_rel. + intros ????????. + f_equiv. + intros ?; simpl. + f_equiv. + f_equiv. + f_equiv; first done. + intros ?; simpl. + f_equiv. + intros ?; simpl. + solve_proper. + Qed. + + Lemma rel_ret_val {S} α αv (v : val S) Φ `{!IntoVal α αv} : + Φ αv v ⊢ expr_rel Φ α v. + Proof. + iIntros "H %σ Hs Hp". + iApply wp_val; iModIntro. + iExists (0,0), v, σ. + iFrame. + iPureIntro. + constructor. + Qed. + + Definition val_nat {S} (αv : ITV) (vn : val S) : iProp := + ∃ (n : nat), αv ≡ RetV n ∧ vn ≡ LitV n. + Definition val_unit {S} (αv : ITV) (vu : val S) : iProp := + αv ≡ RetV () ∧ vu ≡ UnitV. + Definition val_prng {S} (αv : ITV) (vp : val S) : iProp := + ∃ (l : loc), αv ≡ RetV l ∗ vp ≡ LitPrng l ∗ known_prng l. + Definition val_func {S} (Φ1 Φ2 : ITV → val S → iProp) (αv : ITV) (vf : val S) : iProp := + ∃ f, IT_of_V αv ≡ Fun f + ∧ □ ∀ (βv : ITV) (xv : val S), + Φ1 βv xv -∗ expr_rel Φ2 + (Fun f ⊙ (IT_of_V βv)) + (App (Val vf) (Val xv)). + + Fixpoint val_rel (τ : ty) {S} : ITV → val S → iProp := + match τ with + | Tunit => val_unit + | Tnat => val_nat + | Tprng => val_prng + | Tarr τ1 τ2 => val_func (val_rel τ1) (val_rel τ2) + end. + + Definition logrel (τ : ty) {S} := expr_rel (val_rel τ (S:=S)). + + #[global] Instance prng_lang_val_rel_persist' τ {S} v_git v_pl : Persistent (val_rel τ v_git v_pl (S:=S)). + Proof. induction τ; apply _. Qed. + + #[export] Program Instance prng_adequacy_val_nat_ne {S} : NonExpansive2 (@val_nat S). + #[export] Program Instance prng_adequacy_val_unit_ne {S} : NonExpansive2 (@val_unit S). + #[export] Program Instance prng_adequacy_val_prng_ne {S} : NonExpansive2 (@val_prng S). + #[export] Program Instance prng_adequacy_val_func_ne {S} Vdom Vcodom + : NonExpansive2 Vdom → NonExpansive2 Vcodom → NonExpansive2 (@val_func S Vdom Vcodom). + #[export] Program Instance prng_adequacy_val_nat_proper {S} : Proper ((≡) ==> (≡) ==> (≡)) (@val_nat S). + #[export] Program Instance prng_adequacy_val_unit_proper {S} : Proper ((≡) ==> (≡) ==> (≡)) (@val_unit S). + #[export] Program Instance prng_adequacy_val_prng_proper {S} : Proper ((≡) ==> (≡) ==> (≡)) (@val_prng S). + #[export] Program Instance prng_adequacy_val_func_proper {S} Vdom Vcodom : + Proper ((≡) ==> (≡) ==> (≡)) Vdom → + Proper ((≡) ==> (≡) ==> (≡)) Vcodom → + Proper ((≡) ==> (≡) ==> (≡)) (@val_func S Vdom Vcodom). + #[export] Program Instance prng_adequacy_expr_rel_proper {S} (V : ITV → val S → iProp) : + Proper ((≡) ==> (≡) ==> (≡)) V → + Proper ((≡) ==> (≡) ==> (≡)) (expr_rel V). + + Solve All Obligations with solve_proper. + + #[export] Instance prng_adequacy_val_rel_ne {S} τ: + NonExpansive2 (@val_rel τ S). + Proof. induction τ; simpl; solve_proper. Qed. + #[export] Instance prng_adequacy_val_rel_proper {S} τ: + Proper ((≡) ==> (≡) ==> (≡)) (val_rel τ (S:=S)). + Proof. induction τ; simpl; solve_proper. Qed. + #[export] Instance prng_adequacy_logrel_proper {S} τ: + Proper ((≡) ==> (≡) ==> (≡)) (logrel τ (S:=S)). + Proof. solve_proper. Qed. + + + Lemma rel_bind {S} (f : IT → IT) (K : ectx S) Ψ Φ `{!NonExpansive2 Φ} `{!IT_hom f} α e : + ⊢ expr_rel Ψ α e -∗ + (∀ αv v, Ψ αv v -∗ + expr_rel Φ (f (IT_of_V αv)) (fill K (Val v))) -∗ + expr_rel Φ (f α) (fill K e). + Proof. + iIntros "Hrel Hbind". + iLöb as "IH" forall (α e). + iIntros (σ) "Hs Hp". + iApply wp_bind. { solve_proper. } + iSpecialize ("Hrel" with "Hs Hp"). + iApply (wp_wand with "Hrel"). + iIntros (αv). iDestruct 1 as ([m m'] v σ' Hsteps) "(Hs & Hp & Hrel)". + apply (prim_steps_ctx K) in Hsteps. + iSpecialize ("Hbind" with "Hrel Hs Hp"). + iApply (wp_wand with "Hbind"). iModIntro. + iIntros (βv). iDestruct 1 as ([m2 m2'] v2 σ2' Hsteps2) "[H2 Hs]". + iExists (m + m2, m' + m2'),v2,σ2'. iFrame "H2 Hs". + iPureIntro. eapply (prim_steps_app (m,m') (m2,m2')); eauto. + Qed. + + (* subject expansion, on PL expression side *) + Lemma rel_pure_expansion {S} (e e' : expr S) n Φ `{!NonExpansive2 Φ} α : + (∀ σ, prim_step e σ e' σ (n, 0)) → + ⊢ expr_rel Φ α e' -∗ expr_rel Φ α e. + Proof. + intros Hsteps. + iIntros "Hrel %σ Hs Hp". + specialize (Hsteps σ). + iSpecialize ("Hrel" $! σ with "Hs Hp"). + iApply (wp_wand with "Hrel"). + iIntros (αv) "H". + iDestruct "H" as ([m1 m2] v σ' Hsteps') "[Hs Hp]". + iModIntro. + iExists (n+m1,m2), v, σ'. + iFrame. + iPureIntro. + eapply (prim_steps_app (n,0) (m1,m2)); eauto. + eapply prim_step_steps; eauto. + Qed. + + + (* Context Γ, gitree values indexed Γ, cloesd program values indexed by Γ. + gitree i ~(Γ i)~ program_value i *) + Definition env_valid {S : Set} + (Γ : S -> ty) + (tvs : interp_scope S) + (evs : S [⇒] Empty_set) : iProp := + (∀ x, □ logrel (Γ x) (tvs x) (evs x))%I. + + Definition valid1 {S : Set} (Γ : S → ty) (α : interp_scope S -n> IT) (e : expr S) (τ : ty) : iProp := + ∀ tvs evs, env_valid Γ tvs evs -∗ logrel τ (α tvs) (bind evs e). + + + Lemma compat_unit {S : Set} (Γ : S → ty) : + ⊢ valid1 Γ (interp_unit rs) (Val UnitV) Tunit. + Proof. + iIntros (tvs evs) "#Henv". + by iApply rel_ret_val. + Qed. + + Lemma compat_nat {S : Set} (Γ : S → ty) (n : nat) : + ⊢ valid1 Γ (interp_nat rs n) (LitV n) Tnat. + Proof. + iIntros (tvs evs) "#Henv". + iApply rel_ret_val. + by iExists n. + Qed. + + Lemma compat_var {S : Set} (Γ : S → ty) (x : S) : + ⊢ valid1 Γ (interp_var x) (Var x) (Γ x). + Proof. + iIntros (tvs evs) "#Henv". + iApply "Henv". + Qed. + + Lemma compat_if {S : Set} (Γ : S → ty) τ α β1 β2 a b1 b2: + ⊢ valid1 Γ α a Tnat -∗ + valid1 Γ β1 b1 τ -∗ + valid1 Γ β2 b2 τ -∗ + valid1 Γ (interp_if rs α β1 β2) (if a then b1 else b2)%syn τ. + Proof. + iIntros "H0 H1 H2". + iIntros (tvs evs) "#Henv". + iSpecialize ("H0" $! tvs evs with "Henv"); + iSpecialize ("H1" $! tvs evs with "Henv"); + iSpecialize ("H2" $! tvs evs with "Henv"). + iApply (rel_bind (IFSCtx (β1 tvs) (β2 tvs)) (bind evs $ IfK EmptyK b1 b2) (val_rel Tnat) with "H0"). + iIntros (αv v) "(%n & HeqIT & HeqEV)". + iRewrite "HeqIT"; iRewrite "HeqEV". + rewrite /IFSCtx IT_of_V_Ret. + destruct n as [|n]. + - rewrite IF_False; last lia. + iApply (rel_pure_expansion _ (bind evs b2) 0 with "H2"). + intros ?. apply (Ectx_step' EmptyK). + econstructor; eauto. + - rewrite IF_True; last lia. + iApply (rel_pure_expansion _ (bind evs b1) 0 with "H1"). + intros ?. apply (Ectx_step' EmptyK). + econstructor; eauto. + lia. + Qed. + + (* [typed_NewPrng] *) + Lemma compat_NewPrng {S : Set} {Γ : S → ty} : + ⊢ valid1 Γ (interp_new rs) NewPrng Tprng. + Proof. + iIntros (tvs evs) "#Henv". + iIntros (σ) "Hs Hp /=". + iApply (wp_new with "Hs Hp"). { solve_proper. } + iIntros "!>!> Hs Hp Hl". + iApply wp_val. + iModIntro. + iExists (1,1),(LitPrng $ Loc.fresh $ dom σ),_. + iFrame. + iSplit; last done. + iPureIntro. + apply prim_step_steps. + apply (Ectx_step' EmptyK). + by constructor. + Qed. + + (* [typed_Rand] *) + Lemma compat_Rand {S : Set} {Γ : S → ty} α e : + ⊢ valid1 Γ α e Tprng -∗ + valid1 Γ (interp_rand rs α) (Rand e) Tnat. + Proof. + iIntros "H". + iIntros (tvs evs) "#Henv". + iIntros (σ) "Hs Hp /=". + iSpecialize ("H" $! tvs evs with "Henv"). + iApply (rel_bind (λ l, get_ret PRNG_GEN l) (bind evs $ RandK EmptyK) (val_rel Tprng) with "H [] Hs Hp"). + iIntros (αlv lv) "Hrel". + iDestruct "Hrel" as (l) "(Heq & -> & Hl)". + iRewrite "Heq". + iSimpl. + (* XXX: this definitional unfold is for typeclass resolution ... *) + change (val_nat) with (val_rel Tnat (S:=Empty_set)). + rewrite IT_of_V_Ret get_ret_ret. + iIntros (σ0) "Hs Hp". + iPoseProof (istate_read l with "Hp Hl") as "(%n & %Hlk)". + iApply (wp_gen l n with "Hs Hp Hl"); first done. + iIntros "!>!> Hs Hp Hl". + iExists (1,1),(LitV $ read_lcg n),_. + iFrame. + iSplit; last by iExists _. + iPureIntro. + apply prim_step_steps. + apply (Ectx_step' EmptyK). + constructor. + rewrite /state_gen Hlk //. + Qed. + + (* [typed_Seed] *) + Lemma compat_Seed {S : Set} {Γ : S → ty} α β el es : + ⊢ valid1 Γ α el Tprng -∗ + valid1 Γ β es Tnat -∗ + valid1 Γ (interp_seed rs α β) (Seed el es) Tunit. + Proof. + iIntros "H1 H2". + iIntros (tvs evs) "#Henv". + iIntros (σ) "Hs Hp /=". + iSpecialize ("H1" $! tvs evs with "Henv"). + iApply (rel_bind (SeedGitCtxL rs (β tvs)) (bind evs $ SeedKl EmptyK es) (val_rel Tprng) with "H1 [H2] Hs Hp"). + iIntros (αlv lv) "(%l & Heq & -> & Hl)". + iRewrite "Heq"; iSimpl. + iIntros (σ0) "Hs Hp /=". + iSpecialize ("H2" $! tvs evs with "Henv"). + iApply (rel_bind (SeedGitCtxS rs (IT_of_V (RetV l))) (bind evs $ SeedKs (LitPrng l) EmptyK) (val_rel Tnat) with "H2 [Hl] Hs Hp"). + iIntros (αsv sv) "(%m & Heq & ->)". + iRewrite "Heq"; iSimpl. + (* XXX: this definitional unfold is for typeclass resolution ... *) + change (val_unit) with (val_rel Tunit (S:=Empty_set)). + rewrite /SeedGitCtxS !IT_of_V_Ret SeedGit_Ret. + iIntros (σ1) "Hs Hp". + iPoseProof (istate_read l with "Hp Hl") as "(%n & %Hlk)". + iApply (wp_seed l m with "Hs Hp Hl"). + iIntros "!>!> Hs Hp Hl". + iExists (1,1),UnitV,_. + iFrame. + iSplit; last done. + iPureIntro. + apply prim_step_steps. + apply (Ectx_step' EmptyK). + constructor. + rewrite /state_seed Hlk //. + Qed. + + Lemma compat_app {S : Set} (Γ : S → ty) φ υ f u τ1 τ2 : + ⊢ valid1 Γ φ f (Tarr τ1 τ2) -∗ + valid1 Γ υ u τ1 -∗ + valid1 Γ (interp_app rs φ υ) (App f u) τ2. + Proof. + iIntros "H1 H2". + iIntros (tvs evs) "#Henv". + iIntros (σ) "Hs Hp". + iSpecialize ("H2" $! tvs evs with "Henv"). + iApply (rel_bind (AppRSCtx (φ tvs)) (AppRK (bind evs f) EmptyK) (val_rel τ1) with "H2 [H1] Hs Hp"). + iIntros (υv uv) "H2". + iIntros (σ0) "Hs Hp". + iSpecialize ("H1" $! tvs evs with "Henv"). + iApply (rel_bind (AppLSCtx (IT_of_V υv)) (AppLK EmptyK uv) (val_rel (Tarr τ1 τ2)) with "H1 [H2] Hs Hp"). + iIntros (φv fv) "(%φ' & Heq & H1)". + fold val_rel. + iRewrite "Heq". + iApply ("H1" with "H2"). + Qed. + + Lemma compat_rec {S : Set} (Γ : S → ty) τ1 τ2 α e : + ⊢ □ valid1 (Γ ▹ (Tarr τ1 τ2) ▹ τ1) α e τ2 -∗ + valid1 Γ (interp_rec rs α) (Val $ RecV e) (Tarr τ1 τ2). + Proof. + iIntros "#H". + iIntros (tvs evs) "#Henv". + rewrite interp_rec_unfold. + iApply rel_ret_val. + fold @ebind. + iExists _. + fold val_rel. + iSplit; first done. + iLöb as "IH". + iModIntro. + iIntros (βv bv) "#H1". + rewrite APP_APP'_ITV APP_Fun laterO_map_Next -Tick_eq. + set (tvs' := (extend_scope (extend_scope tvs (interp_rec rs α tvs)) (IT_of_V βv))). + set (evs' := ((mk_subst (Val (rec bind ((evs ↑) ↑)%bind e)%syn)) + ∘ ((mk_subst (shift (Val bv))) ∘ ((evs ↑) ↑)))%bind). + iApply (rel_pure_expansion _ ((bind evs' e)%syn) 1). + { + intros ?. + eapply (Ectx_step' EmptyK). + term_simpl. + rewrite -!bind_bind_comp'. + apply BetaS. + } + iIntros (σ) "Hs Hp". + iApply wp_tick. iNext. iIntros "Hlc". + iAssert (env_valid (Γ ▹ (τ1 →ₜ τ2)%typ ▹ τ1) tvs' evs') as "Henv'". + { + rewrite /evs' /tvs'. + iIntros (x'); destruct x' as [| [| x']]; term_simpl; iModIntro. + { (* ext 0 *) + iApply (rel_ret_val with "H1"). + } + { (* ext 1 *) + iApply rel_ret_val. + { + rewrite interp_rec_unfold. + apply intoval_fun. + } + iExists (Next (ir_unf rs α tvs)). + fold @val_rel. + iSplit; first done. + iApply "IH". + } + { (* index in env. already known related *) + iApply "Henv". + } + } + iApply ("H" with "Henv' Hs Hp"). + Qed. + + Lemma compat_natop {S : Set} (Γ : S → ty) op α1 α2 e1 e2 : + ⊢ valid1 Γ α1 e1 Tnat -∗ + valid1 Γ α2 e2 Tnat -∗ + valid1 Γ (interp_natop _ op α1 α2) (NatOp op e1 e2) Tnat. + Proof. + iIntros "H1 H2". + iIntros (tvs evs) "#Henv". + iIntros (σ) "Hs Hp /=". + iSpecialize ("H2" $! tvs evs with "Henv"). + iApply (rel_bind (NatOpRSCtx (do_natop op) (α1 tvs)) (NatOpRK op (bind evs e1) EmptyK) (val_rel Tnat) with "H2 [H1] Hs Hp"). + iIntros (β2 v2) "(%n2 & Ht2 & ->)". + iRewrite "Ht2". + change (val_nat) with (val_rel Tnat (S:=Empty_set)). + rewrite IT_of_V_Ret. + iIntros (σ1) "Hs Hp /=". + iSpecialize ("H1" $! tvs evs with "Henv"). + iApply (rel_bind (NatOpLSCtx (do_natop op) (Ret n2)) (NatOpLK op EmptyK (LitV n2)) with "H1 [] Hs Hp"). + iIntros (β1 v1) "(%n1 & Ht1 & ->)". + iRewrite "Ht1". + change (val_nat) with (val_rel Tnat (S:=Empty_set)). + rewrite /NatOpLSCtx IT_of_V_Ret NATOP_Ret /=. + iApply (rel_pure_expansion _ (LitV $ do_natop op n1 n2) 0). + { + intros ?. apply (Ectx_step' EmptyK). + by constructor. + } + by iApply compat_nat. + Qed. + + Lemma fundamental {S : Set} (Γ : S → ty) e τ : + typed Γ e τ → ⊢ valid1 Γ (interp_expr rs e) e τ + with fundamental_val {S : Set} (Γ : S → ty) v τ : + typed_val Γ v τ → ⊢ valid1 Γ (interp_val rs v) v τ. + Proof. + - destruct 1. + + by iApply fundamental_val. + + subst. by iApply compat_var. + + iApply compat_app; iApply fundamental; eauto. + + iApply compat_natop; iApply fundamental; eauto. + + iApply compat_if; iApply fundamental; eauto. + + iApply compat_NewPrng. + (* + iApply compat_DelPrng; iApply fundamental; eauto. *) + + iApply compat_Rand; iApply fundamental; eauto. + + iApply compat_Seed; iApply fundamental; eauto. + - destruct 1. + + iApply compat_unit. + + iApply compat_nat. + + iApply compat_rec; iApply fundamental; eauto. + Qed. + + Lemma fundmanetal_closed (e : expr ∅) (τ : ty) : + typed □ e τ → + ⊢ valid1 □ (interp_expr rs e) e τ. + Proof. apply fundamental. Qed. +End prng_logrel. + +Section reduction_correspondence_adeqaucy. + +Local Definition rs : gReifiers NotCtxDep _ := gReifiers_cons reify_prng gReifiers_nil. + +#[local] Parameter Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. + +Program Definition PrngLangGitreeGS {R} `{!Cofe R} + {a : is_ctx_dep} {n} (rs : gReifiers a n) + (Σ : gFunctors) + (H1 : invGS Σ) (H2 : stateG rs R Σ) + : gitreeGS_gen rs R Σ := + GitreeG rs R Σ H1 H2 + (λ _ σ, @state_interp _ _ rs R _ _ H2 σ) + (λ _, True%I) + (λ _, True%I) + _ + (λ x, x) + _ + _ + _. +Next Obligation. + intros; simpl. + iIntros "?". by iModIntro. +Qed. +Next Obligation. + intros; simpl. iSplit; iIntros "H". + - by iFrame "H". + - by iDestruct "H" as "(_ & ?)". +Qed. + +Let R := sumO natO (sumO unitO locO). +Let sRef := gReifiers_sReifier rs. +Let sOps := sReifier_ops sRef. +Let IT := IT sOps R. +Let ITV := ITV sOps R. +Let fullState := sReifier_state sRef ♯ IT. + +Definition κ {S} : ITV → val S := λ x, + match x with + | core.RetV v => match v with + | inl n => LitV n + | inr (inl ()) => UnitV + | inr (inr l) => LitPrng l + end + | _ => LitV 0 + end. +Lemma κ_Ret {S} n : κ ((RetV n) : ITV) = (LitV n : val S). +Proof. + Transparent RetV. unfold RetV. simpl. done. Opaque RetV. +Qed. + +Lemma logrel_nat_adequacy Σ `{!invGpreS Σ}`{!statePreG rs R Σ} `{!prngPreG Σ} {S} + (α : IT) (e : expr S) n (σ : prng.state) (σ' : fullState) k : + (∀ `{H1 : !gitreeGS_gen rs R Σ} `{H2 : !prngG Σ}, + (True ⊢ logrel rs notStuck Tnat α e)%I) → + external_steps sRef α (σ,()) (Ret n) σ' [] k → + ∃ m σ', prim_steps e σ (Val $ LitV n) σ' m. +Proof. + intros Hlog Hst. + pose (ϕ := λ (βv : ITV), ∃ m σ', prim_steps e σ (Val $ κ βv) σ' m). + cut (ϕ (RetV n)). + { + destruct 1 as ( m' & σ2 & Hm). + exists m', σ2. revert Hm. by rewrite κ_Ret. + } + + eapply (wp_adequacy 0 (λ x, x) 1 NotCtxDep rs Σ α (σ,()) (Ret n) σ' notStuck k). + + intros Hinv1 Hst1. + pose H3 : gitreeGS_gen rs R Σ := PrngLangGitreeGS rs Σ Hinv1 Hst1. + simpl in H3. + iExists (@state_interp_fun _ _ rs _ _ _ H3). + iExists (@aux_interp_fun _ _ rs _ _ _ H3). + iExists (@fork_post _ _ rs _ _ _ H3). + iExists (@fork_post_ne _ _ rs _ _ _ H3). + iMod (new_prngG σ) as (H4) "Hprng". + pose (Φ := (λ (βv : ITV), ∃ n, val_rel rs notStuck Tnat (Σ:=Σ) (S:=S) βv (LitV n) + ∗ ⌜∃ m σ', prim_steps e σ (Val $ LitV n) σ' m⌝)%I). + assert (NonExpansive Φ). + { + unfold Φ. + intros l a1 a2 Ha. repeat f_equiv. done. + } + iExists Φ, _. + iExists (@state_interp_fun_mono _ _ rs _ _ _ H3). + iExists (@state_interp_fun_ne _ _ rs _ _ _ H3). + iExists (@state_interp_fun_decomp _ _ rs _ _ _ H3). + simpl. + iPoseProof (external_steps_internal_steps _ _ _ _ _ _ _ Hst) as "J1". + iFrame "J1"; iClear "J1". + iAssert (True%I) as "G"; first done; iFrame "G"; iClear "G". + iModIntro. + iSplitL "Hprng". + - iIntros "(_ & Hst)". + iPoseProof (Hlog _ with "[//]") as "Hlog". + iAssert (has_substate (σ : oFunctor_car (sReifier_state reify_prng) IT IT)) with "[Hst]" as "Hst". + { + unfold has_substate, has_full_state. + fold sRef sOps IT. + assert (of_state rs IT (σ, ()) ≡ of_idx rs IT 0 σ)%stdpp as ->; last done. + intro j. unfold sR_idx. simpl. + unfold of_state, of_idx. + destruct decide as [Heq|]; last first. + { inv_fin j; first done. + intros i. inversion i. } + inv_fin j; last done. + intros Heq. + rewrite (eq_pi _ _ Heq eq_refl)//. + } + iSpecialize ("Hlog" $! σ with "Hst Hprng"). + iApply (wp_wand with "Hlog"). + iIntros ( βv). iIntros "H". + iDestruct "H" as (m' v σ1' Hsts) "(Hst & Hprng & Hrel)". + unfold Φ. iDestruct "Hrel" as (n0) "[Hβ %]". simplify_eq/=. + iExists n0. iModIntro. iSplit; eauto. + iExists n0. iSplit; eauto. + - iIntros "Hst HΦ Hstuck". + iAssert ((IT_to_V (Ret n)) ≡ Some (RetV n))%I as "HEQ". + { by rewrite IT_to_V_Ret. } + iDestruct (internal_eq_rewrite _ _ + (λ x, from_option Φ True%I x) + with "HEQ HΦ") + as "HΦ". + { solve_proper. } + iClear "HEQ". + iSimpl in "HΦ". + iDestruct "HΦ" as (n') "[(%p & J1 & %J2) %J3]". + rewrite J2 in J3; clear J2. + iEval (subst ϕ; simpl). + rewrite κ_Ret. + iPoseProof (RetV_inj with "J1") as "->". + iApply fupd_mask_intro; first done. + iIntros "H". + by iPureIntro. +Qed. + +Theorem prng_adequacy_nat (e : expr ∅) (k : nat) σ σ' n : + typed □ e Tnat → + external_steps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) (σ,()) (Ret k : IT) σ' [] n → + ∃ mm σ', prim_steps e σ (Val $ LitV k) σ' mm. +Proof. + intros Htyped Hsteps. + pose (Σ:=#[invΣ;stateΣ rs R;prngΣ]). + eapply (logrel_nat_adequacy Σ (interp_expr rs e ı_scope)); last eassumption. + intros ? ?. + iIntros "_". + iPoseProof (fundamental rs notStuck □ e Tnat Htyped) as "H". + iSpecialize ("H" $! ı_scope ı%bind with "[]"). + { iIntros (x); destruct x. } + rewrite ebind_id; last done. + iApply "H". +Qed. + +End reduction_correspondence_adeqaucy. + +