From e27c687a36f17aa6e7ed12b5f48a0904b9569326 Mon Sep 17 00:00:00 2001 From: hehelego Date: Mon, 30 Mar 2026 18:52:50 +0200 Subject: [PATCH 01/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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.