diff --git a/_CoqProject b/_CoqProject index e8cf1c7..4ef1b32 100644 --- a/_CoqProject +++ b/_CoqProject @@ -16,7 +16,6 @@ vendor/Binding/Resolver.v theories/prelude.v theories/lang_generic.v -theories/lang_affine.v theories/gitree/core.v theories/gitree/subofe.v @@ -29,22 +28,23 @@ theories/gitree.v theories/program_logic.v -theories/input_lang_callcc/lang.v -theories/input_lang_callcc/interp.v -theories/input_lang_callcc/hom.v -theories/input_lang_callcc/logrel.v - -theories/input_lang/lang.v -theories/input_lang/interp.v -theories/input_lang/logpred.v -theories/input_lang/logrel.v - -theories/affine_lang/lang.v -theories/affine_lang/logrel1.v -theories/affine_lang/logrel2.v - -theories/examples/store.v -theories/examples/pairs.v -theories/examples/while.v -theories/examples/factorial.v -theories/examples/iter.v +theories/examples/input_lang_callcc/lang.v +theories/examples/input_lang_callcc/interp.v +theories/examples/input_lang_callcc/hom.v +theories/examples/input_lang_callcc/logrel.v + +theories/examples/input_lang/lang.v +theories/examples/input_lang/interp.v +theories/examples/input_lang/logpred.v +theories/examples/input_lang/logrel.v + +theories/examples/affine_lang/lang.v +theories/examples/affine_lang/logrel1.v +theories/examples/affine_lang/logrel2.v + +theories/effects/store.v + +theories/lib/pairs.v +theories/lib/while.v +theories/lib/factorial.v +theories/lib/iter.v diff --git a/theories/affine_lang/logrel1.v b/theories/affine_lang/logrel1.v deleted file mode 100644 index b5757b3..0000000 --- a/theories/affine_lang/logrel1.v +++ /dev/null @@ -1,493 +0,0 @@ -(** Unary (Kripke) logical relation for the affine lang *) -From Equations Require Import Equations. -From gitrees Require Export lang_affine gitree program_logic. -From gitrees.affine_lang Require Import lang. -From gitrees.examples Require Import store pairs. -Require Import iris.algebra.gmap. - -Local Notation tyctx := (tyctx ty). - -Inductive typed : forall {S}, tyctx S → expr S → ty → Prop := -(** functions *) -| typed_Var {S} (Ω : tyctx S) (τ : ty) (v : var S) : - typed_var Ω v τ → - typed Ω (Var v) τ -| typed_Lam {S} (Ω : tyctx S) (τ1 τ2 : ty) (e : expr (()::S) ) : - typed (consC τ1 Ω) e τ2 → - typed Ω (Lam e) (tArr τ1 τ2) -| typed_App {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 : ty) e1 e2 : - typed Ω1 e1 (tArr τ1 τ2) → - typed Ω2 e2 τ1 → - typed (tyctx_app Ω1 Ω2) (App e1 e2) τ2 -(** pairs *) -| typed_Pair {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 : ty) e1 e2 : - typed Ω1 e1 τ1 → - typed Ω2 e2 τ2 → - typed (tyctx_app Ω1 Ω2) (EPair e1 e2) (tPair τ1 τ2) -| typed_Destruct {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 τ : ty) - (e1 : expr S1) (e2 : expr (()::()::S2)) : - typed Ω1 e1 (tPair τ1 τ2) → - typed (consC τ1 (consC τ2 Ω2)) e2 τ → - typed (tyctx_app Ω1 Ω2) (EDestruct e1 e2) τ -(** references *) -| typed_Alloc {S} (Ω : tyctx S) τ e : - typed Ω e τ → - typed Ω (Alloc e) (tRef τ) -| typed_Replace {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 : ty) e1 e2 : - typed Ω1 e1 (tRef τ1) → - typed Ω2 e2 τ2 → - typed (tyctx_app Ω1 Ω2) (Replace e1 e2) (tPair τ1 (tRef τ2)) -| typed_Dealloc {S} (Ω : tyctx S) e τ : - typed Ω e (tRef τ) → - typed Ω (Dealloc e) tUnit -(** literals *) -| typed_Nat {S} (Ω : tyctx S) n : - typed Ω (LitNat n) tInt -| typed_Bool {S} (Ω : tyctx S) b : - typed Ω (LitBool b) tBool -| typed_Unit {S} (Ω : tyctx S) : - typed Ω LitUnit tUnit -. - -Section logrel. - Context {sz : nat}. - Variable rs : gReifiers NotCtxDep sz. - Context `{!subReifier reify_store rs}. - Context `{!subReifier input_lang.interp.reify_io rs}. - Notation F := (gReifiers_ops NotCtxDep rs). - Context {R} `{!Cofe R}. - Context `{!SubOfe natO R}. - Context `{!SubOfe unitO R}. - Context `{!SubOfe locO R}. - Notation IT := (IT F R). - Notation ITV := (ITV F R). - Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}. - Notation iProp := (iProp Σ). - - (* parameters for the kripke logical relation *) - Variable s : stuckness. - Context `{A:ofe}. - Variable (P : A -n> iProp). - Local Notation expr_pred := (expr_pred s rs P). - - (* interpreting tys *) - Program Definition protected (Φ : ITV -n> iProp) : ITV -n> iProp := λne αv, - (WP@{rs} Force (IT_of_V αv) @ s {{ Φ }})%I. - Solve All Obligations with solve_proper_please. - Program Definition interp_tbool : ITV -n> iProp := λne αv, - (αv ≡ RetV 0 ∨ αv ≡ RetV 1)%I. - Solve All Obligations with solve_proper_please. - Program Definition interp_tnat : ITV -n> iProp := λne αv, - (∃ n : nat, αv ≡ RetV n)%I. - Solve All Obligations with solve_proper_please. - Program Definition interp_tunit : ITV -n> iProp := λne αv, - (αv ≡ RetV ())%I. - Solve All Obligations with solve_proper_please. - Program Definition interp_tpair (Φ1 Φ2 : ITV -n> iProp) : ITV -n> iProp := λne αv, - (∃ β1v β2v, IT_of_V αv ≡ pairITV (IT_of_V β1v) (IT_of_V β2v) ∗ - Φ1 β1v ∗ Φ2 β2v)%I. - Solve All Obligations with solve_proper_please. - Program Definition interp_tarr (Φ1 Φ2 : ITV -n> iProp) : ITV -n> iProp := λne αv, - (∀ βv, Φ1 βv -∗ expr_pred ((IT_of_V αv) ⊙ (Thunk (IT_of_V βv))) Φ2)%I. - Solve All Obligations with solve_proper_please. - - Program Definition interp_ref (Φ : ITV -n> iProp) : ITV -n> iProp := λne αv, - (∃ (l : loc) βv, αv ≡ RetV l ∗ pointsto l (IT_of_V βv) ∗ Φ βv)%I. - Solve All Obligations with solve_proper_please. - - Fixpoint interp_ty (τ : ty) : ITV -n> iProp := - match τ with - | tBool => interp_tbool - | tUnit => interp_tunit - | tInt => interp_tnat - | tPair τ1 τ2 => interp_tpair (interp_ty τ1) (interp_ty τ2) - | tArr τ1 τ2 => interp_tarr (interp_ty τ1) (interp_ty τ2) - | tRef τ => interp_ref (interp_ty τ) - end. - - Definition ssubst_valid {S} (Ω : tyctx S) ss := - lang_affine.ssubst_valid rs (λ τ, protected (interp_ty τ)) Ω ss. - - Definition valid1 {S} (Ω : tyctx S) (α : interp_scope S -n> IT) (τ : ty) : iProp := - ∀ ss, heap_ctx -∗ ssubst_valid Ω ss -∗ expr_pred (α (interp_ssubst ss)) (interp_ty τ). - - Lemma compat_pair {S1 S2} (Ω1: tyctx S1) (Ω2:tyctx S2) α β τ1 τ2 : - ⊢ valid1 Ω1 α τ1 -∗ - valid1 Ω2 β τ2 -∗ - valid1 (tyctx_app Ω1 Ω2) (interp_pair α β ◎ interp_scope_split) (tPair τ1 τ2). - Proof. - Opaque pairITV. - iIntros "H1 H2". - iIntros (αs) "#Hctx Has". - cbn-[interp_pair]. - unfold ssubst_valid. - rewrite ssubst_valid_app. - rewrite interp_scope_ssubst_split. - iDestruct "Has" as "[Ha1 Ha2]". cbn-[interp_app]. - iSpecialize ("H1" with "Hctx Ha1"). - iSpecialize ("H2" with "Hctx Ha2"). - iApply (expr_pred_bind with "H2"). - iIntros (βv) "Hb". simpl. - rewrite -> get_val_ITV. simpl. - iApply (expr_pred_bind with "H1"). - iIntros (αv) "Ha". simpl. - rewrite -> get_val_ITV. simpl. - iApply expr_pred_ret. - iExists _,_. iFrame. done. - Qed. - - Lemma compat_destruct {S1 S2} (Ω1: tyctx S1) (Ω2:tyctx S2) α β τ1 τ2 τ : - ⊢ valid1 Ω1 α (tPair τ1 τ2) -∗ - valid1 (consC τ1 $ consC τ2 Ω2) β τ -∗ - valid1 (tyctx_app Ω1 Ω2) (interp_destruct α β ◎ interp_scope_split) τ. - Proof. - Opaque pairITV thunked thunkedV projIT1 projIT2. - iIntros "H1 H2". - iIntros (αs) "#Hctx Has". - cbn-[interp_destruct]. - unfold ssubst_valid. - rewrite ssubst_valid_app. - rewrite interp_scope_ssubst_split. - iDestruct "Has" as "[Ha1 Ha2]". - iSpecialize ("H1" with "Hctx Ha1"). - simpl. iApply (expr_pred_bind (LETCTX _) with "H1"). - iIntros (αv) "Ha". unfold LETCTX. simpl. - rewrite LET_Val/=. - iDestruct "Ha" as (β1 β2) "[#Ha [Hb1 Hb2]]". - iIntros (x) "Hx". - iApply wp_let. - { solve_proper. } - iApply (wp_Thunk with "Hctx"). - { solve_proper_please. } - iNext. iIntros (l1) "Hl1". simpl. - iApply wp_let. - { solve_proper. } - iApply (wp_Thunk with "Hctx"). - { solve_proper_please. } - iNext. iIntros (l2) "Hl2". simpl. - iSpecialize ("H2" $! (cons_ssubst (thunkedV (projIT1 (IT_of_V αv)) l1) - $ cons_ssubst (thunkedV (projIT2 (IT_of_V αv)) l2) (ssubst_split αs).2) - with "Hctx [-Hx] Hx"). - { unfold ssubst_valid. rewrite !ssubst_valid_cons. - iFrame. Transparent thunkedV thunked. - iSplitL "Hb1 Hl1". - - simpl. iApply wp_lam. simpl. iNext. - iApply (wp_bind _ (IFSCtx _ _)). - iApply (wp_read with "Hctx Hl1"). - iNext. iNext. iIntros "Hl1". - iApply wp_val. iModIntro. unfold IFSCtx. - rewrite IF_False; last lia. - iApply wp_seq. - { solve_proper. } - iApply (wp_write with "Hctx Hl1"). - iNext. iNext. iIntros "Hl1". - iRewrite "Ha". - rewrite projIT1_pairV. simpl. - repeat iApply wp_tick. - repeat iNext. iApply wp_val. done. - - simpl. iApply wp_lam. simpl. iNext. - iApply (wp_bind _ (IFSCtx _ _)). - iApply (wp_read with "Hctx Hl2"). - iNext. iNext. iIntros "Hl2". - iApply wp_val. iModIntro. unfold IFSCtx. - rewrite IF_False; last lia. - iApply wp_seq. - { solve_proper. } - iApply (wp_write with "Hctx Hl2"). - iNext. iNext. iIntros "Hl2". - iRewrite "Ha". - rewrite projIT2_pairV. simpl. - repeat iApply wp_tick. - repeat iNext. iApply wp_val. done. - } - simp interp_ssubst. - iApply "H2". - Qed. - - Lemma compat_alloc {S} (Ω : tyctx S) α τ: - ⊢ valid1 Ω α τ -∗ - valid1 Ω (interp_alloc α) (tRef τ). - Proof. - iIntros "H". - iIntros (αs) "#Hctx Has". - iSpecialize ("H" with "Hctx Has"). - simpl. iApply (expr_pred_bind (LETCTX _) with "H"). - iIntros (αv) "Hav". unfold LETCTX. simpl. - rewrite LET_Val/=. - iApply expr_pred_frame. - iApply (wp_alloc with "Hctx"). - iNext. iNext. iIntros (l) "Hl". - iApply wp_val. iModIntro. simpl. - eauto with iFrame. - Qed. - - Lemma compat_replace {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) α β τ τ' : - ⊢ valid1 Ω1 α (tRef τ) -∗ - valid1 Ω2 β τ' -∗ - valid1 (tyctx_app Ω1 Ω2) (interp_replace α β ◎ interp_scope_split) (tPair τ (tRef τ')). - Proof. - Opaque pairITV. - iIntros "H1 H2". - iIntros (αs) "#Hctx Has". - cbn-[interp_replace]. - unfold ssubst_valid. - rewrite ssubst_valid_app. - rewrite interp_scope_ssubst_split. - iDestruct "Has" as "[Ha1 Ha2]". cbn-[interp_app]. - iSpecialize ("H1" with "Hctx Ha1"). - iSpecialize ("H2" with "Hctx Ha2"). - iApply (expr_pred_bind (LETCTX _) with "H2"). - iIntros (βv) "Hb". unfold LETCTX. simpl. - rewrite LET_Val/=. - iApply (expr_pred_bind with "H1"). - iIntros (αv) "Ha". simpl. - iDestruct "Ha" as (l γ) "[Ha [Hl Hg]]". - iApply expr_pred_frame. - iRewrite "Ha". simpl. - rewrite IT_of_V_Ret. - rewrite -> get_ret_ret; simpl. - iApply wp_let. - { solve_proper. } - iApply (wp_read with "Hctx Hl"). - iNext. iNext. iIntros "Hl". - iApply wp_val. iModIntro. - simpl. iApply wp_seq. - { solve_proper. } - iApply (wp_write with "Hctx Hl"). - iNext. iNext. iIntros "Hl". - rewrite get_val_ITV. simpl. - rewrite get_val_ITV. simpl. - iApply wp_val. iModIntro. - iExists γ,(RetV l). - iSplit; first done. - iFrame. eauto with iFrame. - Qed. - - Lemma compat_dealloc {S} (Ω : tyctx S) α τ: - ⊢ valid1 Ω α (tRef τ) -∗ - valid1 Ω (interp_dealloc α) tUnit. - Proof. - iIntros "H". - iIntros (αs) "#Hctx Has". - iSpecialize ("H" with "Hctx Has"). - iApply (expr_pred_bind with "H"). - iIntros (αv) "Ha /=". - iDestruct "Ha" as (l βv) "[Ha [Hl Hb]]". - iRewrite "Ha". iApply expr_pred_frame. simpl. - rewrite IT_of_V_Ret. rewrite -> get_ret_ret. simpl. - iApply (wp_dealloc with "Hctx Hl"). - iNext. iNext. eauto with iFrame. - Qed. - - Lemma compat_bool {S} b (Ω : tyctx S) : - ⊢ valid1 Ω (interp_litbool b) tBool. - Proof. - iIntros (αs) "#Hctx Has". - iApply expr_pred_ret. - destruct b; simpl; eauto. - Qed. - Lemma compat_nat {S} n (Ω : tyctx S) : - ⊢ valid1 Ω (interp_litnat n) tInt. - Proof. - iIntros (αs) "#Hctx Has". - iApply expr_pred_ret. eauto with iFrame. - Qed. - Lemma compat_unit {S} (Ω : tyctx S) : - ⊢ valid1 Ω interp_litunit tUnit. - Proof. - iIntros (αs) "#Hctx Has". - iApply expr_pred_ret. eauto with iFrame. - Qed. - Lemma compat_var {S} Ω τ (v : var S) : - typed_var Ω v τ → - ⊢ valid1 Ω (Force ◎ interp_var v) τ. - Proof. - iIntros (Hv ss) "#Hctx Has". - iApply expr_pred_frame. - unfold ssubst_valid. - iInduction Hv as [|? ? ? Ω v] "IH" forall (ss); simpl. - - dependent elimination ss as [cons_ssubst αv ss]. - rewrite ssubst_valid_cons. - simp interp_var. simpl. - iDestruct "Has" as "[H _]". - simp interp_ssubst. simpl. done. - - dependent elimination ss as [cons_ssubst αv ss]. - rewrite ssubst_valid_cons. - simp interp_var. simpl. - iDestruct "Has" as "[_ H]". - simp interp_ssubst. simpl. - by iApply ("IH" with "H"). - Qed. - - Lemma compat_app {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) - α β τ1 τ2 : - ⊢ valid1 Ω1 α (tArr τ1 τ2) -∗ - valid1 Ω2 β τ1 -∗ - valid1 (tyctx_app Ω1 Ω2) (interp_app α β ◎ interp_scope_split) τ2. - Proof. - iIntros "H1 H2". - iIntros (αs) "#Hctx Has". - iEval(cbn-[interp_app]). - unfold ssubst_valid. - rewrite ssubst_valid_app. - rewrite interp_scope_ssubst_split. - iDestruct "Has" as "[Ha1 Ha2]". cbn-[interp_app]. - iSpecialize ("H1" with "Hctx Ha1"). - iSpecialize ("H2" with "Hctx Ha2"). - Local Opaque Thunk. - iSimpl. - iApply (expr_pred_bind (LETCTX _) with "H2"). - iIntros (βv) "H2". unfold LETCTX. iSimpl. - rewrite LET_Val/=. - iApply (expr_pred_bind (LETCTX _) with "H1"). - iIntros (αv) "H1". unfold LETCTX. iSimpl. - rewrite LET_Val/=. - by iApply "H1". - Qed. - - Lemma compat_lam {S} (Ω : tyctx S) τ1 τ2 α : - ⊢ valid1 (consC τ1 Ω) α τ2 -∗ - valid1 Ω (interp_lam α) (tArr τ1 τ2). - Proof. - iIntros "H". - iIntros (αs) "#Hctx Has". - iIntros (x) "Hx". - iApply wp_val. - iModIntro. simpl. - iExists _; iFrame. - iIntros (βv) "Hb". clear x. - iIntros (x) "Hx". - iApply (wp_bind _ (AppRSCtx _)). - { solve_proper. } - Local Transparent Thunk. - Local Opaque thunked thunkedV. - iSimpl. iApply (wp_alloc with "Hctx"). - { solve_proper. } - iNext. iNext. iIntros (l) "Hl". - iApply wp_val. iModIntro. - unfold AppRSCtx. - iApply wp_lam. iNext. - iEval(cbn-[thunked]). - iSpecialize ("H" $! (cons_ssubst (thunkedV (IT_of_V βv) l) αs) - with "Hctx [-Hx] Hx"). - { unfold ssubst_valid. - rewrite ssubst_valid_cons. iFrame. - Local Transparent thunked thunkedV. - iApply wp_lam. iNext. simpl. - iApply (wp_bind _ (IFSCtx _ _)). - iApply (wp_read with "Hctx Hl"). - iNext. iNext. iIntros "Hl". - iApply wp_val. iModIntro. - unfold IFSCtx. simpl. - rewrite IF_False; last lia. - iApply wp_seq. - { solve_proper. } - iApply (wp_write with "Hctx Hl"). - iNext. iNext. iIntros "Hl". - iApply wp_val. iModIntro. - iApply "Hb". } - simp interp_ssubst. - iApply "H". - Qed. - - Lemma fundamental_affine {S} (Ω : tyctx S) (e : expr S) τ : - typed Ω e τ → - ⊢ valid1 Ω (interp_expr _ e) τ. - Proof. - induction 1; simpl. - - by iApply compat_var. - - by iApply compat_lam. - - by iApply compat_app. - - by iApply compat_pair. - - by iApply compat_destruct. - - by iApply compat_alloc. - - by iApply compat_replace. - - by iApply compat_dealloc. - - by iApply compat_nat. - - by iApply compat_bool. - - by iApply compat_unit. - Qed. - -End logrel. - -Arguments interp_tarr {_ _ _ _ _ _ _ _ _ _ _ _ _} Φ1 Φ2. -Arguments interp_tbool {_ _ _ _ _ _}. -Arguments interp_tnat {_ _ _ _ _ _}. -Arguments interp_tunit {_ _ _ _ _ _}. -Arguments interp_ty {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _} τ. - -Local Definition rs : gReifiers NotCtxDep 2 := - gReifiers_cons NotCtxDep reify_store (gReifiers_cons NotCtxDep input_lang.interp.reify_io (gReifiers_nil NotCtxDep)). - -Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. - -Lemma logrel1_adequacy cr Σ R `{!Cofe R, !SubOfe natO R, !SubOfe unitO R, !SubOfe locO R} `{!invGpreS Σ} - `{!statePreG rs R Σ} `{!heapPreG rs R Σ} τ - (α : unitO -n> IT (gReifiers_ops NotCtxDep rs) R) (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : - (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ}, - (£ cr ⊢ valid1 rs notStuck (λne _: unitO, True)%I empC α τ)%I) → - ssteps (gReifiers_sReifier NotCtxDep rs) (α ()) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) - ∨ (∃ βv, IT_of_V βv ≡ β). -Proof. - intros Hlog Hst. - destruct (IT_to_V β) as [βv|] eqn:Hb. - { right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. } - left. - cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) - ∨ (∃ e, β ≡ Err e ∧ notStuck e)). - { intros [?|He]; first done. - destruct He as [? [? []]]. } - eapply (wp_safety (S cr)); eauto. - { apply Hdisj. } - { by rewrite Hb. } - intros H1 H2. - exists (λ _, True)%I. split. - { apply _. } - iIntros "[[Hone Hcr] Hst]". - pose (σ := st.1). - pose (ios := st.2.1). - iMod (new_heapG rs σ) as (H3) "H". - iAssert (has_substate σ ∗ has_substate ios)%I with "[Hst]" as "[Hs Hio]". - { unfold has_substate, has_full_state. - assert (of_state NotCtxDep rs (IT (gReifiers_ops NotCtxDep rs) _) st ≡ - of_idx NotCtxDep rs (IT (gReifiers_ops NotCtxDep rs) _) sR_idx (sR_state σ) - ⋅ of_idx NotCtxDep rs (IT (gReifiers_ops NotCtxDep rs) _) sR_idx (sR_state ios)) as ->; last first. - { rewrite -own_op. done. } - unfold sR_idx. simpl. - intro j. - rewrite discrete_fun_lookup_op. - inv_fin j. - { unfold of_state, of_idx. simpl. - erewrite (eq_pi _ _ _ (@eq_refl _ 0%fin)). done. } - intros j. inv_fin j. - { unfold of_state, of_idx. simpl. - erewrite (eq_pi _ _ _ (@eq_refl _ 1%fin)). done. } - intros i. inversion i. } - iApply fupd_wp. - iMod (inv_alloc (nroot.@"storeE") _ (∃ σ, £ 1 ∗ has_substate σ ∗ own (heapG_name rs) (●V σ))%I with "[-Hcr]") as "#Hinv". - { iNext. iExists _. iFrame. } - simpl. - iPoseProof (@Hlog _ _ _ with "Hcr") as "Hlog". - iSpecialize ("Hlog" $! emp_ssubst with "Hinv []"). - { iApply ssubst_valid_nil. } - iSpecialize ("Hlog" $! tt with "[//]"). - iModIntro. - iApply (wp_wand with "Hlog"). - eauto with iFrame. -Qed. - -Definition R := sumO locO (sumO unitO natO). - -Lemma logrel1_safety e τ (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : - typed empC e τ → - ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ()) st β st' k → - (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) - ∨ (∃ βv, IT_of_V βv ≡ β). -Proof. - intros Hty Hst. - pose (Σ:=#[invΣ;stateΣ rs R;heapΣ rs R]). - eapply (logrel1_adequacy 0 Σ); eauto; try apply _. - iIntros (? ? ?) "_". - by iApply fundamental_affine. -Qed. diff --git a/theories/examples/store.v b/theories/effects/store.v similarity index 99% rename from theories/examples/store.v rename to theories/effects/store.v index 490ad68..6b72ad6 100644 --- a/theories/examples/store.v +++ b/theories/effects/store.v @@ -1,4 +1,3 @@ -From Equations Require Import Equations. From iris.algebra Require Import gmap excl auth gmap_view. From iris.proofmode Require Import classes tactics. From iris.base_logic Require Import algebra. diff --git a/theories/affine_lang/lang.v b/theories/examples/affine_lang/lang.v similarity index 69% rename from theories/affine_lang/lang.v rename to theories/examples/affine_lang/lang.v index 9616cb1..3e5505f 100644 --- a/theories/affine_lang/lang.v +++ b/theories/examples/affine_lang/lang.v @@ -1,6 +1,7 @@ From gitrees Require Export lang_generic gitree program_logic. -From gitrees.input_lang Require Import lang interp. -From gitrees.examples Require Import store pairs. +From gitrees.examples.input_lang Require Import lang interp. +From gitrees.effects Require Import store. +From gitrees.lib Require Import pairs. (* for namespace sake *) Module io_lang. @@ -14,15 +15,13 @@ Module io_lang. input_lang.interp.interp_expr rs e (ı_scope rs). End io_lang. -From gitrees Require Export lang_affine. +Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. Inductive ty := tBool | tInt | tUnit | tArr (τ1 τ2 : ty) | tPair (τ1 τ2 : ty) | tRef (τ : ty). -Local Notation tyctx := (tyctx ty). - Inductive ty_conv : ty → io_lang.ty → Type := | ty_conv_bool : ty_conv tBool Tnat | ty_conv_int : ty_conv tInt Tnat @@ -32,19 +31,19 @@ Inductive ty_conv : ty → io_lang.ty → Type := ty_conv (tArr τ1 τ2) (Tarr (Tarr Tnat t1) t2) . -Inductive expr : scope → Type := -| LitBool (b : bool) {S} : expr S -| LitNat (n : nat) {S} : expr S -| LitUnit {S} : expr S -| Lam {S} : expr (tt::S) → expr S -| Var {S} : var S → expr S -| App {S1 S2} : expr S1 → expr S2 → expr (S1++S2) -| EPair {S1 S2} : expr S1 → expr S2 → expr (S1++S2) -| EDestruct {S1 S2} : expr S1 → expr (()::()::S2) → expr (S1++S2) -| Alloc {S} : expr S → expr S -| Replace {S1 S2} : expr S1 → expr S2 → expr (S1++S2) -| Dealloc {S} : expr S → expr S -| EEmbed {τ1 τ1' S} : io_lang.expr Empty_set → ty_conv τ1 τ1' → expr S +Inductive expr : ∀ (S : Set), Type := +| LitBool {S : Set} (b : bool) : expr S +| LitNat {S : Set} (n : nat) : expr S +| LitUnit {S : Set} : expr S +| Lam {S : Set} : expr (inc S) → expr S +| Var {S : Set} : S → expr S +| App {S1 S2 : Set} : expr S1 → expr S2 → expr (sum S1 S2) +| EPair {S1 S2 : Set} : expr S1 → expr S2 → expr (sum S1 S2) +| EDestruct {S1 S2 : Set} : expr S1 → expr (inc (inc S2)) → expr (sum S1 S2) +| Alloc {S : Set} : expr S → expr S +| Replace {S1 S2 : Set} : expr S1 → expr S2 → expr (sum S1 S2) +| Dealloc {S : Set} : expr S → expr S +| EEmbed {S : Set} {τ1 τ1'} : io_lang.expr Empty_set → ty_conv τ1 τ1' → expr S . Section affine. @@ -64,9 +63,11 @@ Section affine. λit _, IF (READ ℓ) (Err OtherError) (SEQ (WRITE ℓ (Ret 1)) e). Solve All Obligations with first [solve_proper|solve_proper_please]. + Program Definition thunkedV : IT -n> locO -n> ITV := λne e ℓ, FunV $ Next (λne _, IF (READ ℓ) (Err OtherError) (SEQ (WRITE ℓ (Ret 1)) e)). Solve All Obligations with first [solve_proper|solve_proper_please]. + #[export] Instance thunked_into_val e l : IntoVal (thunked e l) (thunkedV e l). Proof. unfold IntoVal. simpl. f_equiv. f_equiv. intro. done. @@ -75,45 +76,52 @@ Section affine. Program Definition Thunk : IT -n> IT := λne e, ALLOC (Ret 0) (thunked e). Solve All Obligations with first [solve_proper|solve_proper_please]. + Program Definition Force : IT -n> IT := λne e, e ⊙ (Ret 0). Local Open Scope type. Definition interp_litbool {A} (b : bool) : A -n> IT := λne _, - Ret (if b then 1 else 0). + Ret (if b then 1 else 0). + Definition interp_litnat {A} (n : nat) : A -n> IT := λne _, - Ret n. + Ret n. + Definition interp_litunit {A} : A -n> IT := λne _, Ret tt. + Program Definition interp_pair {A1 A2} (t1 : A1 -n> IT) (t2 : A2 -n> IT) - : A1*A2 -n> IT := λne env, + : A1 * A2 -n> IT := λne env, pairIT (t1 env.1) (t2 env.2). (* we don't need to evaluate the pair here, i.e. lazy pairs? *) Next Obligation. solve_proper_please. Qed. - Program Definition interp_lam {A : ofe} (b : (IT * A) -n> IT) : A -n> IT := λne env, - λit x, b (x,env). - Solve All Obligations with solve_proper_please. + + Program Definition interp_lam {S : Set} (b : @interp_scope F R _ (inc S) -n> IT) : @interp_scope F R _ S -n> IT := λne env, (λit x, (b (@extend_scope F R _ _ env x))). + Next Obligation. + intros; repeat intro; repeat f_equiv; assumption. + Qed. + Next Obligation. + intros; repeat intro; repeat f_equiv; intro; simpl; + f_equiv; intro z; simpl. + destruct z; done. + Qed. + Program Definition interp_app {A1 A2 : ofe} (t1 : A1 -n> IT) (t2 : A2 -n> IT) : A1*A2 -n> IT := λne env, LET (t2 env.2) $ λne x, LET (t1 env.1) $ λne f, APP' f (Thunk x). Solve All Obligations with solve_proper_please. - Program Definition interp_destruct {A1 A2 : ofe} - (ps : A1 -n> IT) (t : IT*(IT*A2) -n> IT) - : A1*A2 -n> IT := λne env, - LET (ps env.1) $ λne ps, - LET (Thunk (projIT1 ps)) $ λne x, - LET (Thunk (projIT2 ps)) $ λne y, - t (x, (y, env.2)). - Solve All Obligations with solve_proper_please. + Program Definition interp_alloc {A} (α : A -n> IT) : A -n> IT := λne env, LET (α env) $ λne α, ALLOC α Ret. Solve All Obligations with solve_proper_please. + Program Definition interp_replace {A1 A2} (α : A1 -n> IT) (β : A2 -n> IT) : A1*A2 -n> IT := λne env, LET (β env.2) $ λne β, flip get_ret (α env.1) $ λne (l : loc), LET (READ l) $ λne γ, SEQ (WRITE l β) (pairIT γ (Ret l)). Solve All Obligations with solve_proper_please. + Program Definition interp_dealloc {A} (α : A -n> IT) : A -n> IT := λne env, get_ret DEALLOC (α env). Solve All Obligations with solve_proper_please. @@ -154,6 +162,35 @@ Section affine. | ty_conv_fun conv1 conv2 => glue_from_affine_fun (glue_from_affine conv2) (glue_to_affine conv1) end. + Program Definition interp_destruct {S1 S2 : Set} + (ps : @interp_scope F R _ S1 -n> IT) + (t : (@interp_scope F R _ (inc (inc S2)) -n> IT)) + : (@interp_scope F R _ S1 * @interp_scope F R _ S2) -n> IT + := λne env, + LET (ps env.1) $ λne z, + LET (Thunk (projIT1 z)) $ λne x, + LET (Thunk (projIT2 z)) $ λne y, + (t (@extend_scope F R _ _ (@extend_scope F R _ _ env.2 y) x)). + Next Obligation. + intros; repeat intro; repeat f_equiv; assumption. + Qed. + Next Obligation. + intros; repeat intro; repeat f_equiv; intro; simpl; f_equiv; intro A; simpl. + destruct A as [| [|]]; [assumption | reflexivity | reflexivity]. + Qed. + Next Obligation. + intros; repeat intro; repeat f_equiv; first assumption. + intro; simpl; f_equiv; intro; simpl. + repeat f_equiv; intro; simpl; repeat f_equiv; intro; simpl. + repeat f_equiv; assumption. + Qed. + Next Obligation. + intros; repeat intro; repeat f_equiv; first assumption. + intro; simpl; f_equiv; intro; simpl. + repeat f_equiv; intro; simpl; repeat f_equiv; intro A; simpl. + destruct A as [| [|]]; [reflexivity | reflexivity |]. + repeat f_equiv; assumption. + Qed. Fixpoint interp_expr {S} (e : expr S) : interp_scope S -n> IT := match e with @@ -162,12 +199,16 @@ Section affine. | LitUnit => interp_litunit | Var v => Force ◎ interp_var v | Lam e => interp_lam (interp_expr e) - | App e1 e2 => interp_app (interp_expr e1) (interp_expr e2) ◎ interp_scope_split - | EPair e1 e2 => interp_pair (interp_expr e1) (interp_expr e2) ◎ interp_scope_split - | EDestruct e1 e2 => interp_destruct (interp_expr e1) (interp_expr e2) ◎ interp_scope_split + | App e1 e2 => + interp_app (interp_expr e1) (interp_expr e2) ◎ interp_scope_split + | EPair e1 e2 => + interp_pair (interp_expr e1) (interp_expr e2) ◎ interp_scope_split + | EDestruct e1 e2 => + interp_destruct (interp_expr e1) (interp_expr e2) ◎ interp_scope_split | Alloc e => interp_alloc (interp_expr e) | Dealloc e => interp_dealloc (interp_expr e) - | Replace e1 e2 => interp_replace (interp_expr e1) (interp_expr e2) ◎ interp_scope_split + | Replace e1 e2 => + interp_replace (interp_expr e1) (interp_expr e2) ◎ interp_scope_split | EEmbed e tconv => constO $ glue_to_affine tconv (io_lang.interp_closed _ e) end. diff --git a/theories/examples/affine_lang/logrel1.v b/theories/examples/affine_lang/logrel1.v new file mode 100644 index 0000000..50b2fcd --- /dev/null +++ b/theories/examples/affine_lang/logrel1.v @@ -0,0 +1,931 @@ +(** Unary (Kripke) logical relation for the affine lang *) +From gitrees Require Export gitree program_logic. +From gitrees.examples.affine_lang Require Import lang. +From gitrees.effects Require Import store. +From gitrees.lib Require Import pairs. +Require Import iris.algebra.gmap. +Require Import stdpp.finite. + +Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. + +Lemma fin_to_set_sum {S1 S2 : Set} `{EqDecision S1} `{EqDecision S2} `{EqDecision (S1 + S2)} + `{Finite S1} `{Finite S2} `{Finite (S1 + S2)} + `{Countable S1} `{Countable S2} `{Countable (S1 + S2)} + : let A1 : gset S1 := (fin_to_set S1) in + let A2 : gset (S1 + S2) := set_map (inl : S1 → S1 + S2) A1 in + let B1 : gset S2 := (fin_to_set S2) in + let B2 : gset (S1 + S2) := set_map (inr : S2 → S1 + S2) B1 in + let C : gset (S1 + S2) := fin_to_set (S1 + S2) in + C = A2 ∪ B2. +Proof. + apply set_eq. + intros [x|x]; simpl; split; intros _. + - apply elem_of_union; left. + apply elem_of_map_2. + apply elem_of_fin_to_set. + - apply elem_of_fin_to_set. + - apply elem_of_union; right. + apply elem_of_map_2. + apply elem_of_fin_to_set. + - apply elem_of_fin_to_set. +Qed. + +Lemma fin_to_set_empty : + let A : gset ∅ := fin_to_set ∅ in + let B : gset ∅ := empty in + A = B. +Proof. + apply set_eq; intros []. +Qed. + +Section InstSum. + Global Instance EqDecisionLeft {S1 S2 : Set} {H : EqDecision (S1 + S2)} : EqDecision S1. + Proof. + intros x y. + destruct (decide (inl x = inl y)) as [G | G]; + [left; by inversion G | right; intros C; by subst]. + Qed. + + Global Instance EqDecisionRight {S1 S2 : Set} {H : EqDecision (S1 + S2)} : EqDecision S2. + Proof. + intros x y. + destruct (decide (inr x = inr y)) as [G | G]; + [left; by inversion G | right; intros C; by subst]. + Qed. + + Global Instance FiniteLeft {S1 S2 : Set} `{EqDecision S1} + `{EqDecision (S1 + S2)} `{Finite (S1 + S2)} + : Finite S1. + Proof. + unshelve econstructor. + - apply (foldr (λ x acc, match x with + | inl x => x :: acc + | inr _ => acc + end) [] (enum (S1 + S2))). + - set (l := enum (S1 + S2)). + assert (NoDup l) as K; first apply NoDup_enum. + clearbody l. + induction l as [| a l IH]; first constructor. + destruct a as [a | a]; simpl. + + constructor. + * intros C. + assert (inl a ∈ l) as C'. + { + clear -C. + induction l as [| b l IH]; first inversion C. + destruct b as [b | b]; simpl. + - rewrite foldr_cons in C. + rewrite elem_of_cons in C. + destruct C as [-> | C]. + + apply elem_of_cons. + by left. + + right. + apply IH. + apply C. + - apply elem_of_cons. + right. + rewrite foldr_cons in C. + apply IH. + apply C. + } + by inversion K. + * apply IH. + by inversion K. + + apply IH. + by inversion K. + - intros x. + set (l := enum (S1 + S2)). + assert (inl x ∈ l) as K; first apply elem_of_enum. + clearbody l. + induction l as [| a l IH]; first inversion K. + destruct a as [a | a]; simpl. + + rewrite elem_of_cons in K. + destruct K as [K | K]. + * inversion K; subst. + apply elem_of_cons; by left. + * apply elem_of_cons; right; by apply IH. + + rewrite elem_of_cons in K. + destruct K as [K | K]; first inversion K. + by apply IH. + Qed. + + Global Instance FiniteRight {S1 S2 : Set} `{EqDecision S2} + `{EqDecision (S1 + S2)} `{H : Finite (S1 + S2)} + : Finite S2. + Proof. + unshelve econstructor. + - apply (foldr (λ x acc, match x with + | inl _ => acc + | inr x => x :: acc + end) [] (enum (S1 + S2))). + - set (l := enum (S1 + S2)). + assert (NoDup l) as K; first apply NoDup_enum. + clearbody l. + induction l as [| a l IH]; first constructor. + destruct a as [a | a]; simpl. + + apply IH. + by inversion K. + + constructor. + * intros C. + assert (inr a ∈ l) as C'. + { + clear -C. + induction l as [| b l IH]; first inversion C. + destruct b as [b | b]; simpl. + - apply elem_of_cons. + right. + rewrite foldr_cons in C. + apply IH. + apply C. + - rewrite foldr_cons in C. + rewrite elem_of_cons in C. + destruct C as [-> | C]. + + apply elem_of_cons. + by left. + + right. + apply IH. + apply C. + } + by inversion K. + * apply IH. + by inversion K. + - intros x. + set (l := enum (S1 + S2)). + assert (inr x ∈ l) as K; first apply elem_of_enum. + clearbody l. + induction l as [| a l IH]; first inversion K. + destruct a as [a | a]; simpl. + + rewrite elem_of_cons in K. + destruct K as [K | K]; first inversion K. + by apply IH. + + rewrite elem_of_cons in K. + destruct K as [K | K]. + * inversion K; subst. + apply elem_of_cons; by left. + * apply elem_of_cons; right; by apply IH. + Qed. + +End InstSum. + +Section InstInc. + Context (S : Set). + + Global Instance EqDecisionIncN {HS : EqDecision S} (n : nat) : EqDecision (Init.Nat.iter n inc S). + Proof using S. + induction n; simpl. + - apply _. + - intros [|x] [|y]. + + by left. + + by right. + + by right. + + destruct (decide (x = y)) as [-> |]; first by left. + right; by inversion 1. + Qed. + + Global Instance EqDecisionInc {HS : EqDecision S} : EqDecision (inc S). + Proof using S. + assert (inc S = Init.Nat.iter 1 inc S) as ->; first done. + by apply EqDecisionIncN. + Qed. + + Global Instance FiniteIncN {HS : EqDecision S} (HF : Finite S) (n : nat) {HS' : EqDecision (Init.Nat.iter n inc S)} : Finite (Init.Nat.iter n inc S). + Proof using S. + induction n. + - apply (@surjective_finite S HS HF _ _ id). + apply _. + - simpl. + unshelve eapply (@surjective_finite (option (Init.Nat.iter n inc S))); simpl in *. + + intros [x |]. + * apply (VS x). + * apply VZ. + + apply _. + + intros [| x]; simpl. + * exists None; reflexivity. + * exists (Some x); reflexivity. + Qed. + + Global Instance FiniteInc {HS : EqDecision S} (HF : Finite S) (HE : EqDecision (inc S)) : Finite (inc S). + Proof using S. + assert (J : @Finite (Init.Nat.iter 1 inc S) HE). + { apply FiniteIncN, HF. } + simpl in J. + apply J. + Qed. + +End InstInc. + +Definition sum_map' {A B C : Set} (f : A → C) (g : B → C) : sum A B → C := + λ x, match x with | inl x' => f x' | inr x' => g x' end. + +Inductive typed : forall {S : Set}, (S → ty) → expr S → ty → Prop := +(** functions *) +| typed_Var {S : Set} (Ω : S → ty) (v : S) : + typed Ω (Var v) (Ω v) +| typed_Lam {S : Set} (Ω : S → ty) (τ1 τ2 : ty) (e : expr (inc S) ) : + typed (Ω ▹ τ1) e τ2 → + typed Ω (Lam e) (tArr τ1 τ2) +| typed_App {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 : ty) e1 e2 : + typed Ω1 e1 (tArr τ1 τ2) → + typed Ω2 e2 τ1 → + typed (sum_map' Ω1 Ω2) (App e1 e2) τ2 +(** pairs *) +| typed_Pair {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 : ty) e1 e2 : + typed Ω1 e1 τ1 → + typed Ω2 e2 τ2 → + typed (sum_map' Ω1 Ω2) (EPair e1 e2) (tPair τ1 τ2) +| typed_Destruct {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 τ : ty) + (e1 : expr S1) (e2 : expr (inc (inc S2))) : + typed Ω1 e1 (tPair τ1 τ2) → + typed ((Ω2 ▹ τ2) ▹ τ1) e2 τ → + typed (sum_map' Ω1 Ω2) (EDestruct e1 e2) τ +(** references *) +| typed_Alloc {S : Set} (Ω : S → ty) τ e : + typed Ω e τ → + typed Ω (Alloc e) (tRef τ) +| typed_Replace {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 : ty) e1 e2 : + typed Ω1 e1 (tRef τ1) → + typed Ω2 e2 τ2 → + typed (sum_map' Ω1 Ω2) (Replace e1 e2) (tPair τ1 (tRef τ2)) +| typed_Dealloc {S : Set} (Ω : S → ty) e τ : + typed Ω e (tRef τ) → + typed Ω (Dealloc e) tUnit +(** literals *) +| typed_Nat {S : Set} (Ω : S → ty) n : + typed Ω (LitNat n) tInt +| typed_Bool {S : Set} (Ω : S → ty) b : + typed Ω (LitBool b) tBool +| typed_Unit {S : Set} (Ω : S → ty) : + typed Ω LitUnit tUnit +. + +Section logrel. + Context {sz : nat}. + Variable rs : gReifiers NotCtxDep sz. + Context `{!subReifier reify_store rs}. + Context `{!subReifier input_lang.interp.reify_io rs}. + Notation F := (gReifiers_ops NotCtxDep rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R}. + Context `{!SubOfe unitO R}. + Context `{!SubOfe locO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}. + Notation iProp := (iProp Σ). + + (* parameters for the kripke logical relation *) + Variable s : stuckness. + Context `{A:ofe}. + Variable (P : A -n> iProp). + Local Notation expr_pred := (expr_pred s rs P). + + (* interpreting tys *) + Program Definition protected (Φ : ITV -n> iProp) : ITV -n> iProp := λne αv, + (WP@{rs} Force (IT_of_V αv) @ s {{ Φ }})%I. + Solve All Obligations with solve_proper_please. + Program Definition interp_tbool : ITV -n> iProp := λne αv, + (αv ≡ RetV 0 ∨ αv ≡ RetV 1)%I. + Solve All Obligations with solve_proper_please. + Program Definition interp_tnat : ITV -n> iProp := λne αv, + (∃ n : nat, αv ≡ RetV n)%I. + Solve All Obligations with solve_proper_please. + Program Definition interp_tunit : ITV -n> iProp := λne αv, + (αv ≡ RetV ())%I. + Solve All Obligations with solve_proper_please. + Program Definition interp_tpair (Φ1 Φ2 : ITV -n> iProp) : ITV -n> iProp := λne αv, + (∃ β1v β2v, IT_of_V αv ≡ pairITV (IT_of_V β1v) (IT_of_V β2v) ∗ + Φ1 β1v ∗ Φ2 β2v)%I. + Solve All Obligations with solve_proper_please. + Program Definition interp_tarr (Φ1 Φ2 : ITV -n> iProp) : ITV -n> iProp := λne αv, + (∀ βv, Φ1 βv -∗ expr_pred ((IT_of_V αv) ⊙ (Thunk (IT_of_V βv))) Φ2)%I. + Solve All Obligations with solve_proper_please. + + Program Definition interp_ref (Φ : ITV -n> iProp) : ITV -n> iProp := λne αv, + (∃ (l : loc), αv ≡ RetV l ∗ ∃ βv, pointsto l (IT_of_V βv) ∗ Φ βv)%I. + Solve All Obligations with solve_proper_please. + + Fixpoint interp_ty (τ : ty) : ITV -n> iProp := + match τ with + | tBool => interp_tbool + | tUnit => interp_tunit + | tInt => interp_tnat + | tPair τ1 τ2 => interp_tpair (interp_ty τ1) (interp_ty τ2) + | tArr τ1 τ2 => interp_tarr (interp_ty τ1) (interp_ty τ2) + | tRef τ => interp_ref (interp_ty τ) + end. + + Program Definition ssubst_valid {S : Set} `{!EqDecision S} `{!Finite S} + (Ω : S → ty) (ss : interp_scope S) : iProp + := ([∗ set] x ∈ (fin_to_set S), + (expr_pred (ss x) (protected (interp_ty (Ω x))))%I). + + Definition valid1 {S : Set} `{!EqDecision S} `{!Finite S} (Ω : S → ty) + (α : interp_scope S -n> IT) (τ : ty) : iProp := + ∀ ss, heap_ctx + -∗ (ssubst_valid Ω ss) + -∗ expr_pred (α ss) (interp_ty τ). + + Lemma ssubst_valid_empty (αs : interp_scope ∅) : + ⊢ ssubst_valid □ αs. + Proof. + iStartProof. + unfold ssubst_valid. + match goal with + | |- context G [big_opS ?a ?b ?c] => assert (c = empty) as -> + end. + { apply set_eq; intros []. } + by iApply big_sepS_empty. + Qed. + + Lemma ssubst_valid_app + {S1 S2 : Set} `{!EqDecision S1} `{!Finite S1} + `{!EqDecision S2} `{!Finite S2} + `{!EqDecision (S1 + S2)} `{!Finite (S1 + S2)} + (Ω1 : S1 → ty) (Ω2 : S2 → ty) + (αs : interp_scope (sum S1 S2)) : + (ssubst_valid (sum_map' Ω1 Ω2) αs) ⊢ + (ssubst_valid Ω1 (interp_scope_split αs).1) + ∗ (ssubst_valid Ω2 (interp_scope_split αs).2). + Proof. + iIntros "H". + rewrite /ssubst_valid fin_to_set_sum big_sepS_union; first last. + { + apply elem_of_disjoint. + intros [x | x]. + - rewrite !elem_of_list_to_set. + intros _ H2. + apply elem_of_list_fmap_2 in H2. + destruct H2 as [y [H2 H2']]; inversion H2. + - rewrite !elem_of_list_to_set. + intros H1 _. + apply elem_of_list_fmap_2 in H1. + destruct H1 as [y [H1 H1']]; inversion H1. + } + iDestruct "H" as "(H1 & H2)". + iSplitL "H1". + - rewrite big_opS_list_to_set; first last. + { + apply NoDup_fmap. + - intros ??; by inversion 1. + - apply NoDup_elements. + } + rewrite big_sepL_fmap /=. + rewrite big_sepS_elements. + iFrame "H1". + - rewrite big_opS_list_to_set; first last. + { + apply NoDup_fmap. + - intros ??; by inversion 1. + - apply NoDup_elements. + } + rewrite big_sepL_fmap /=. + rewrite big_sepS_elements. + iFrame "H2". + Qed. + + Lemma ssubst_valid_cons {S : Set} `{!EqDecision S} `{!Finite S} + (Ω : S → ty) (αs : interp_scope S) τ t : + ssubst_valid Ω αs ∗ expr_pred t (protected (interp_ty τ)) ⊢ ssubst_valid (Ω ▹ τ) (extend_scope αs t). + Proof. + iIntros "(H & G)". + rewrite /ssubst_valid. + pose (Y := let A := {[VZ]} : @gset (leibnizO (inc S)) _ finite_countable in + let B := fin_to_set (leibnizO S) : gset (leibnizO S) in + let C := set_map (VS : S → inc S) B + : gset (inc S) in A ∪ C). + assert (fin_to_set (inc S) = Y) as ->. + { + subst Y; simpl. + apply set_eq. + intros [| x]. + - split. + + intros _; apply elem_of_union; left. + by apply elem_of_singleton. + + intros _; apply elem_of_fin_to_set. + - split. + + intros _; apply elem_of_union; right. + apply elem_of_map_2, elem_of_fin_to_set. + + intros H. + apply elem_of_fin_to_set. + } + subst Y; simpl. + rewrite big_sepS_union; first last. + { + apply elem_of_disjoint. + intros [| x]. + - rewrite !elem_of_list_to_set. + intros _ H2. + apply elem_of_list_fmap_2 in H2. + destruct H2 as [y [H2 H2']]; inversion H2. + - rewrite !elem_of_list_to_set. + intros H1 _. + apply elem_of_singleton_1 in H1. + inversion H1. + } + iSplitL "G". + - rewrite big_opS_singleton. + iFrame "G". + - erewrite big_opS_set_map. + + iFrame "H". + + intros ?? H; by inversion H. + Qed. + + Lemma ssubst_valid_lookup {S : Set} `{!EqDecision S} `{!Finite S} + (Ω : S → ty) (αs : interp_scope S) x : + ssubst_valid Ω αs ⊢ expr_pred (αs x) (protected (interp_ty (Ω x))). + Proof. + iIntros "H". + iDestruct (big_sepS_elem_of_acc _ _ x with "H") as "($ & _)"; + first apply elem_of_fin_to_set. + Qed. + + Lemma compat_pair {S1 S2 : Set} + `{!EqDecision S1} `{!Finite S1} + `{!EqDecision S2} `{!Finite S2} + `{!EqDecision (S1 + S2)} `{!Finite (S1 + S2)} + (Ω1 : S1 → ty) (Ω2 : S2 → ty) α β τ1 τ2 : + ⊢ valid1 Ω1 α τ1 -∗ + valid1 Ω2 β τ2 -∗ + valid1 (sum_map' Ω1 Ω2) (interp_pair α β ◎ interp_scope_split) (tPair τ1 τ2). + Proof. + Opaque pairITV. + iIntros "H1 H2". + iIntros (αs) "#Hctx Has". + cbn-[interp_pair]. + rewrite ssubst_valid_app. + iDestruct "Has" as "[Ha1 Ha2]". cbn-[interp_app]. + iSpecialize ("H1" with "Hctx Ha1"). + iSpecialize ("H2" with "Hctx Ha2"). + iApply (expr_pred_bind with "H2"). + iIntros (βv) "Hb". simpl. + rewrite -> get_val_ITV. simpl. + iApply (expr_pred_bind with "H1"). + iIntros (αv) "Ha". simpl. + rewrite -> get_val_ITV. simpl. + iApply expr_pred_ret. + simpl. + iExists _,_. + by iFrame. + Qed. + + Lemma compat_destruct {S1 S2 : Set} + `{!EqDecision S1} `{!Finite S1} + `{!EqDecision S2} `{!Finite S2} + `{!EqDecision (S1 + S2)} `{!Finite (S1 + S2)} + (Ω1 : S1 → ty) (Ω2 : S2 → ty) + α β τ1 τ2 τ : + ⊢ valid1 Ω1 α (tPair τ1 τ2) + -∗ valid1 (Ω2 ▹ τ2 ▹ τ1) β τ + -∗ valid1 (sum_map' Ω1 Ω2) (interp_destruct α β ◎ interp_scope_split) τ. + Proof. + Opaque pairITV thunked thunkedV projIT1 projIT2. + iIntros "H1 H2". + iIntros (αs) "#Hctx Has". + cbn-[interp_destruct]. + rewrite ssubst_valid_app. + iDestruct "Has" as "[Ha1 Ha2]". + iSpecialize ("H1" with "Hctx Ha1"). + iApply (expr_pred_bind (LETCTX _) with "H1"). + iIntros (αv) "Ha". unfold LETCTX. simpl. + rewrite LET_Val/=. + iDestruct "Ha" as (β1 β2) "[#Ha [Hb1 Hb2]]". + iIntros (x) "Hx". + iApply wp_let. + iApply (wp_Thunk with "Hctx"). + { + repeat intro; simpl. + repeat f_equiv. + intro; simpl. + f_equiv. + intro B; simpl. + destruct B as [| [|]]; [by f_equiv | reflexivity | reflexivity]. + } + iNext. iIntros (l1) "Hl1". simpl. + iApply wp_let. + { solve_proper. } + iApply (wp_Thunk with "Hctx"). + { + repeat intro; simpl. + repeat f_equiv. + intro B; simpl. + destruct B as [| [|]]; [reflexivity | by f_equiv | reflexivity]. + } + iNext. iIntros (l2) "Hl2". simpl. + pose (ss' := (extend_scope + (extend_scope + (interp_scope_split αs).2 + (IT_of_V (thunkedV (projIT2 (IT_of_V αv)) l2))) + (IT_of_V (thunkedV (projIT1 (IT_of_V αv)) l1)))). + iSpecialize ("H2" $! ss' + with "Hctx [-Hx] Hx"). + { + iApply ssubst_valid_cons. + iSplitR "Hl1 Hb1". + - iApply ssubst_valid_cons. + iSplitL "Ha2"; first done. + Transparent thunkedV thunked. + simpl. + iIntros (z) "Hz". + simpl. + iApply wp_val. + iModIntro. + iExists z; iFrame. + iApply wp_lam. + iNext. + simpl. + iApply (wp_bind _ (IFSCtx _ _)). + iApply (wp_read with "Hctx Hl2"). + iNext. iNext. iIntros "Hl2". + iApply wp_val. iModIntro. + unfold IFSCtx. simpl. + rewrite IF_False; last lia. + iApply wp_seq. + { solve_proper. } + iApply (wp_write with "Hctx Hl2"). + iNext. iNext. iIntros "Hl2". + iRewrite "Ha". + simpl. + rewrite projIT2_pairV. + do 3 (iApply wp_tick; iNext). + iApply wp_val. iModIntro. + iApply "Hb2". + - Transparent thunkedV thunked. + simpl. + iIntros (z) "Hz". + simpl. + iApply wp_val. + iModIntro. + iExists z; iFrame. + iApply wp_lam. + iNext. + simpl. + iApply (wp_bind _ (IFSCtx _ _)). + iApply (wp_read with "Hctx Hl1"). + iNext. iNext. iIntros "Hl1". + iApply wp_val. iModIntro. + unfold IFSCtx. simpl. + rewrite IF_False; last lia. + iApply wp_seq. + { solve_proper. } + iApply (wp_write with "Hctx Hl1"). + iNext. iNext. iIntros "Hl1". + iRewrite "Ha". + simpl. + rewrite projIT1_pairV. + do 3 (iApply wp_tick; iNext). + iApply wp_val. iModIntro. + iApply "Hb1". + } + iApply "H2". + Qed. + + Lemma compat_alloc {S : Set} + `{!EqDecision S} `{!Finite S} + (Ω : S → ty) α τ: + ⊢ valid1 Ω α τ -∗ + valid1 Ω (interp_alloc α) (tRef τ). + Proof. + iIntros "H". + iIntros (αs) "#Hctx Has". + iSpecialize ("H" with "Hctx Has"). + simpl. iApply (expr_pred_bind (LETCTX _) with "H"). + iIntros (αv) "Hav". unfold LETCTX. simpl. + rewrite LET_Val/=. + iApply expr_pred_frame. + iApply (wp_alloc with "Hctx"). + iNext. iNext. iIntros (l) "Hl". + iApply wp_val. iModIntro. simpl. + iExists l. + iSplit; first done. + iExists αv. + iFrame "Hl". + iFrame. + Qed. + + Lemma compat_replace {S1 S2 : Set} + `{!EqDecision S1} `{!Finite S1} + `{!EqDecision S2} `{!Finite S2} + `{!EqDecision (S1 + S2)} `{!Finite (S1 + S2)} + (Ω1 : S1 → ty) (Ω2 : S2 → ty) α β τ τ' : + ⊢ valid1 Ω1 α (tRef τ) -∗ + valid1 Ω2 β τ' -∗ + valid1 (sum_map' Ω1 Ω2) (interp_replace α β ◎ interp_scope_split) (tPair τ (tRef τ')). + Proof. + Opaque pairITV. + iIntros "H1 H2". + iIntros (αs) "#Hctx Has". + cbn-[interp_replace]. + rewrite ssubst_valid_app. + iDestruct "Has" as "[Ha1 Ha2]". cbn-[interp_app]. + iSpecialize ("H1" with "Hctx Ha1"). + iSpecialize ("H2" with "Hctx Ha2"). + iApply (expr_pred_bind (LETCTX _) with "H2"). + iIntros (βv) "Hb". unfold LETCTX. simpl. + rewrite LET_Val/=. + iApply (expr_pred_bind with "H1"). + iIntros (αv) "Ha". simpl. + iDestruct "Ha" as (l) "[Ha Ha']". + iDestruct "Ha'" as (γ) "[Hl Hg]". + iApply expr_pred_frame. + iRewrite "Ha". simpl. + rewrite IT_of_V_Ret. + rewrite -> get_ret_ret; simpl. + iApply wp_let. + { solve_proper. } + iApply (wp_read with "Hctx Hl"). + iNext. iNext. iIntros "Hl". + iApply wp_val. iModIntro. + simpl. iApply wp_seq. + { solve_proper. } + iApply (wp_write with "Hctx Hl"). + iNext. iNext. iIntros "Hl". + rewrite get_val_ITV. simpl. + rewrite get_val_ITV. simpl. + iApply wp_val. iModIntro. + iExists γ, (RetV l). + iSplit; first done. + iFrame. eauto with iFrame. + Qed. + + Lemma compat_dealloc {S : Set} + `{!EqDecision S} `{!Finite S} + (Ω : S → ty) α τ: + ⊢ valid1 Ω α (tRef τ) -∗ + valid1 Ω (interp_dealloc α) tUnit. + Proof. + iIntros "H". + iIntros (αs) "#Hctx Has". + iSpecialize ("H" with "Hctx Has"). + iApply (expr_pred_bind with "H"). + iIntros (αv) "Ha /=". + iDestruct "Ha" as (l) "[Ha Ha']". + iDestruct "Ha'" as (βv) "[Hl Hb]". + iRewrite "Ha". iApply expr_pred_frame. simpl. + rewrite IT_of_V_Ret. rewrite -> get_ret_ret. simpl. + iApply (wp_dealloc with "Hctx Hl"). + iNext. iNext. eauto with iFrame. + Qed. + + Lemma compat_bool {S : Set} + `{!EqDecision S} `{!Finite S} + b (Ω : S → ty) : + ⊢ valid1 Ω (interp_litbool b) tBool. + Proof. + iIntros (αs) "#Hctx Has". + iApply expr_pred_ret. + destruct b; simpl; eauto. + Qed. + + Lemma compat_nat {S : Set} + `{!EqDecision S} `{!Finite S} + n (Ω : S → ty) : + ⊢ valid1 Ω (interp_litnat n) tInt. + Proof. + iIntros (αs) "#Hctx Has". + iApply expr_pred_ret. eauto with iFrame. + Qed. + + Lemma compat_unit {S : Set} + `{!EqDecision S} `{!Finite S} + (Ω : S → ty) : + ⊢ valid1 Ω interp_litunit tUnit. + Proof. + iIntros (αs) "#Hctx Has". + iApply expr_pred_ret. eauto with iFrame. + Qed. + + Lemma compat_var {S : Set} + `{!EqDecision S} `{!Finite S} + Ω (v : S) : + ⊢ valid1 Ω (Force ◎ interp_var v) (Ω v). + Proof. + iIntros (ss) "#Hctx Has". + iIntros (x) "Hx". + unfold Force. + simpl. + iApply (wp_bind rs (AppRSCtx (ss v))). + { solve_proper. } + iApply wp_val. + iModIntro. + unfold AppRSCtx. + iApply (wp_bind rs (AppLSCtx (IT_of_V (RetV 0)))). + { solve_proper. } + unfold AppLSCtx. + simpl. + unfold ssubst_valid. + iDestruct (ssubst_valid_lookup _ _ v with "Has Hx") as "Has". + iApply (wp_wand with "Has"). + iIntros (w) "(%y & Hw1 & Hw2)"; simpl. + iModIntro. + rewrite IT_of_V_Ret. + iApply (wp_wand with "Hw1 [Hw2]"). + iIntros (z) "Hz". + iModIntro. + iExists y. + iFrame. + Qed. + + Lemma compat_app {S1 S2 : Set} + `{!EqDecision S1} `{!Finite S1} + `{!EqDecision S2} `{!Finite S2} + `{!EqDecision (S1 + S2)} `{!Finite (S1 + S2)} + (Ω1 : S1 → ty) (Ω2 : S2 → ty) + α β τ1 τ2 : + ⊢ valid1 Ω1 α (tArr τ1 τ2) -∗ + valid1 Ω2 β τ1 -∗ + valid1 (sum_map' Ω1 Ω2) (interp_app α β ◎ interp_scope_split) τ2. + Proof. + iIntros "H1 H2". + iIntros (αs) "#Hctx Has". + iEval(cbn-[interp_app]). + rewrite ssubst_valid_app. + iDestruct "Has" as "[Ha1 Ha2]". cbn-[interp_app]. + iSpecialize ("H1" with "Hctx Ha1"). + iSpecialize ("H2" with "Hctx Ha2"). + Local Opaque Thunk. + iSimpl. + iApply (expr_pred_bind (LETCTX _) with "H2"). + iIntros (βv) "H2". unfold LETCTX. iSimpl. + rewrite LET_Val/=. + iApply (expr_pred_bind (LETCTX _) with "H1"). + iIntros (αv) "H1". unfold LETCTX. iSimpl. + rewrite LET_Val/=. + by iApply "H1". + Qed. + + Lemma compat_lam {S : Set} + `{!EqDecision S} `{!Finite S} + (Ω : S → ty) τ1 τ2 α : + ⊢ valid1 (Ω ▹ τ1) α τ2 -∗ + valid1 Ω (interp_lam α) (tArr τ1 τ2). + Proof. + iIntros "H". + iIntros (αs) "#Hctx Has". + iIntros (x) "Hx". + iApply wp_val. + iModIntro. simpl. + iExists _; iFrame. + iIntros (βv) "Hb". clear x. + iIntros (x) "Hx". + iApply (wp_bind _ (AppRSCtx _)). + Local Transparent Thunk. + Local Opaque thunked thunkedV. + iSimpl. iApply (wp_alloc with "Hctx"). + { solve_proper. } + iNext. iNext. iIntros (l) "Hl". + iApply wp_val. iModIntro. + unfold AppRSCtx. + iApply wp_lam. iNext. + iEval(cbn-[thunked]). + pose (ss' := extend_scope αs (IT_of_V (thunkedV (IT_of_V βv) l))). + iSpecialize ("H" $! ss' + with "Hctx [-Hx] Hx"). + { + iApply ssubst_valid_cons. + iFrame "Has". + Local Transparent thunked thunkedV. + simpl. + iIntros (x') "Hx". + iApply wp_val. + iModIntro. + iExists x'. + iFrame "Hx". + iApply wp_lam. + iNext. + iApply (wp_bind _ (IFSCtx _ _)). + iApply (wp_read with "Hctx Hl"). + iNext. iNext. iIntros "Hl". + iApply wp_val. iModIntro. + unfold IFSCtx. simpl. + rewrite IF_False; last lia. + iApply wp_seq. + { solve_proper. } + iApply (wp_write with "Hctx Hl"). + iNext. iNext. iIntros "Hl". + iApply wp_val. iModIntro. + iApply "Hb". + } + iApply "H". + Qed. + + Lemma fundamental_affine (S : Set) + {HE : EqDecision S} {HF : Finite S} + (Ω : S → ty) + (e : expr S) τ : + typed Ω e τ → + ⊢ valid1 Ω (interp_expr _ e) τ. + Proof. + intros H. + induction H. + - by iApply compat_var. + - iApply compat_lam; + iApply IHtyped. + - iApply (@compat_app S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply (@compat_pair S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply (@compat_destruct S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply compat_alloc; + iApply IHtyped. + - iApply (@compat_replace S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply compat_dealloc; + iApply IHtyped. + - by iApply compat_nat. + - by iApply compat_bool. + - by iApply compat_unit. + Qed. + +End logrel. + +Arguments interp_tarr {_ _ _ _ _ _ _ _ _ _ _ _ _} Φ1 Φ2. +Arguments interp_tbool {_ _ _ _ _ _}. +Arguments interp_tnat {_ _ _ _ _ _}. +Arguments interp_tunit {_ _ _ _ _ _}. +Arguments interp_ty {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _} τ. + +Local Definition rs : gReifiers NotCtxDep 2 := + gReifiers_cons NotCtxDep reify_store (gReifiers_cons NotCtxDep input_lang.interp.reify_io (gReifiers_nil NotCtxDep)). + +Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. + +Require Import gitrees.gitree.greifiers. + +Program Definition ı_scope R `{!Cofe R} : @interp_scope (gReifiers_ops NotCtxDep rs) R _ Empty_set := λne (x : ∅), match x with end. + +Lemma logrel1_adequacy cr Σ R `{!Cofe R, !SubOfe natO R, !SubOfe unitO R, !SubOfe locO R} `{!invGpreS Σ} + `{!statePreG rs R Σ} `{!heapPreG rs R Σ} τ + (α : interp_scope ∅ -n> IT (gReifiers_ops NotCtxDep rs) R) (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : + (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ}, + (£ cr ⊢ valid1 rs notStuck (λne _: unitO, True)%I □ α τ)%I) → + ssteps (gReifiers_sReifier NotCtxDep rs) (α (ı_scope _)) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ∨ (∃ βv, IT_of_V βv ≡ β). +Proof. + intros Hlog Hst. + destruct (IT_to_V β) as [βv|] eqn:Hb. + { right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. } + left. + cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ∨ (∃ e, β ≡ Err e ∧ notStuck e)). + { intros [?|He]; first done. + destruct He as [? [? []]]. } + eapply (wp_safety (S cr)); eauto. + { apply Hdisj. } + { by rewrite Hb. } + intros H1 H2. + exists (λ _, True)%I. split. + { apply _. } + iIntros "[[Hone Hcr] Hst]". + pose (σ := st.1). + pose (ios := st.2.1). + iMod (new_heapG rs σ) as (H3) "H". + iAssert (has_substate σ ∗ has_substate ios)%I with "[Hst]" as "[Hs Hio]". + { unfold has_substate, has_full_state. + assert (of_state NotCtxDep rs (IT (gReifiers_ops NotCtxDep rs) _) st ≡ + of_idx NotCtxDep rs (IT (gReifiers_ops NotCtxDep rs) _) sR_idx (sR_state σ) + ⋅ of_idx NotCtxDep rs (IT (gReifiers_ops NotCtxDep rs) _) sR_idx (sR_state ios)) as ->; last first. + { rewrite -own_op. done. } + unfold sR_idx. simpl. + intro j. + rewrite discrete_fun_lookup_op. + inv_fin j. + { unfold of_state, of_idx. simpl. + erewrite (eq_pi _ _ _ (@eq_refl _ 0%fin)). done. } + intros j. inv_fin j. + { unfold of_state, of_idx. simpl. + erewrite (eq_pi _ _ _ (@eq_refl _ 1%fin)). done. } + intros i. inversion i. } + iApply fupd_wp. + iMod (inv_alloc (nroot.@"storeE") _ (∃ σ, £ 1 ∗ has_substate σ ∗ own (heapG_name rs) (●V σ))%I with "[-Hcr]") as "#Hinv". + { iNext. iExists _. iFrame. } + simpl. + iPoseProof (@Hlog _ _ _ with "Hcr") as "Hlog". + iSpecialize ("Hlog" $! (ı_scope _) with "Hinv []"). + { iApply ssubst_valid_empty. } + iSpecialize ("Hlog" $! tt with "[//]"). + iModIntro. + iApply (wp_wand with "Hlog"). + eauto with iFrame. +Qed. + +Definition R := sumO locO (sumO unitO natO). + +Lemma logrel1_safety e τ (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : + typed □ e τ → + ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e (ı_scope _)) st β st' k → + (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) + ∨ (∃ βv, IT_of_V βv ≡ β). +Proof. + intros Hty Hst. + pose (Σ:=#[invΣ;stateΣ rs R;heapΣ rs R]). + eapply (logrel1_adequacy 0 Σ); eauto; try apply _. + iIntros (? ? ?) "_". + iApply (fundamental_affine rs notStuck (λne _ : unitO, True)%I). + apply Hty. +Qed. diff --git a/theories/affine_lang/logrel2.v b/theories/examples/affine_lang/logrel2.v similarity index 77% rename from theories/affine_lang/logrel2.v rename to theories/examples/affine_lang/logrel2.v index a45dac8..0c1cba4 100644 --- a/theories/affine_lang/logrel2.v +++ b/theories/examples/affine_lang/logrel2.v @@ -1,59 +1,57 @@ -From Equations Require Import Equations. From iris.base_logic.lib Require Import na_invariants. -From gitrees Require Export lang_affine gitree program_logic. -From gitrees.input_lang Require Import lang interp logpred. -From gitrees.affine_lang Require Import lang logrel1. -From gitrees.examples Require Import store pairs. +From gitrees Require Export gitree program_logic. +From gitrees.examples.input_lang Require Import lang interp logpred. +From gitrees.examples.affine_lang Require Import lang logrel1. +From gitrees.effects Require Import store. +From gitrees.lib Require Import pairs. Require Import iris.algebra.gmap. +Require Import stdpp.finite. Require Import Binding.Lib Binding.Set Binding.Env. -Local Notation tyctx := (tyctx ty). - -Inductive typed_glued : forall {S}, tyctx S → expr S → ty → Type := +Inductive typed_glued : forall {S : Set}, (S → ty) → expr S → ty → Type := (** FFI *) -| typed_Glue {S} (Ω : tyctx S) τ' τ e +| typed_Glue {S : Set} (Ω : S → ty) τ' τ e (tconv : ty_conv τ τ') : io_lang.typed □ e τ' → typed_glued Ω (EEmbed e tconv) τ (** functions *) -| typed_VarG {S} (Ω : tyctx S) (τ : ty) (v : var S) : - typed_var Ω v τ → - typed_glued Ω (Var v) τ -| typed_LamG {S} (Ω : tyctx S) (τ1 τ2 : ty) (e : expr (()::S) ) : - typed_glued (consC τ1 Ω) e τ2 → +| typed_VarG {S : Set} (Ω : S → ty) (τ : ty) (v : S) : + typed_glued Ω (Var v) (Ω v) +| typed_LamG {S : Set} (Ω : S → ty) (τ1 τ2 : ty) (e : expr (inc S) ) : + typed_glued (Ω ▹ τ1) e τ2 → typed_glued Ω (Lam e) (tArr τ1 τ2) -| typed_AppG {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 : ty) e1 e2 : +| typed_AppG {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 : ty) e1 e2 : typed_glued Ω1 e1 (tArr τ1 τ2) → typed_glued Ω2 e2 τ1 → - typed_glued (tyctx_app Ω1 Ω2) (App e1 e2) τ2 + typed_glued (sum_map' Ω1 Ω2) (App e1 e2) τ2 (** pairs *) -| typed_PairG {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 : ty) e1 e2 : +| typed_PairG {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 : ty) e1 e2 : typed_glued Ω1 e1 τ1 → typed_glued Ω2 e2 τ2 → - typed_glued (tyctx_app Ω1 Ω2) (EPair e1 e2) (tPair τ1 τ2) -| typed_DestructG {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 τ : ty) - (e1 : expr S1) (e2 : expr (()::()::S2)) : + typed_glued (sum_map' Ω1 Ω2) (EPair e1 e2) (tPair τ1 τ2) +| typed_DestructG {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 τ : ty) + (e1 : expr S1) (e2 : expr (inc (inc S2))) : typed_glued Ω1 e1 (tPair τ1 τ2) → - typed_glued (consC τ1 (consC τ2 Ω2)) e2 τ → - typed_glued (tyctx_app Ω1 Ω2) (EDestruct e1 e2) τ + typed_glued ((Ω2 ▹ τ2) ▹ τ1) e2 τ → + typed_glued (sum_map' Ω1 Ω2) (EDestruct e1 e2) τ (** references *) -| typed_AllocG {S} (Ω : tyctx S) τ e : +| typed_AllocG {S : Set} (Ω : S → ty) τ e : typed_glued Ω e τ → typed_glued Ω (Alloc e) (tRef τ) -| typed_ReplaceG {S1 S2} (Ω1 : tyctx S1) (Ω2 : tyctx S2) (τ1 τ2 : ty) e1 e2 : +| typed_ReplaceG {S1 S2 : Set} (Ω1 : S1 → ty) (Ω2 : S2 → ty) (τ1 τ2 : ty) e1 e2 : typed_glued Ω1 e1 (tRef τ1) → typed_glued Ω2 e2 τ2 → - typed_glued (tyctx_app Ω1 Ω2) (Replace e1 e2) (tPair τ1 (tRef τ2)) -| typed_DeallocG {S} (Ω : tyctx S) e τ : + typed_glued (sum_map' Ω1 Ω2) (Replace e1 e2) (tPair τ1 (tRef τ2)) +| typed_DeallocG {S : Set} (Ω : S → ty) e τ : typed_glued Ω e (tRef τ) → typed_glued Ω (Dealloc e) tUnit (** literals *) -| typed_NatG {S} (Ω : tyctx S) n : +| typed_NatG {S : Set} (Ω : S → ty) n : typed_glued Ω (LitNat n) tInt -| typed_BoolG {S} (Ω : tyctx S) b : +| typed_BoolG {S : Set} (Ω : S → ty) b : typed_glued Ω (LitBool b) tBool -| typed_UnitG {S} (Ω : tyctx S) : +| typed_UnitG {S : Set} (Ω : S → ty) : typed_glued Ω LitUnit tUnit . @@ -75,17 +73,19 @@ Section glue. Definition s : stuckness := λ e, e = OtherError. Variable p : na_inv_pool_name. - Definition valid2 {S} (Ω : tyctx S) (α : interp_scope (E:=F) S -n> IT) (τ : ty) : iProp := + Definition valid2 {S : Set} `{HE : EqDecision S} `{!Finite S} (Ω : S → ty) (α : interp_scope (E:=F) S -n> IT) + (τ : ty) : iProp := valid1 rs s (λne σ, has_substate σ ∗ na_own p ⊤)%I Ω α τ. - Definition io_valid {S : Set} (Γ : S → io_lang.ty) α (τ' : io_lang.ty) : iProp := + Definition io_valid {S : Set} (Γ : S → io_lang.ty) α (τ' : io_lang.ty) + : iProp := input_lang.logpred.valid1 rs s (λne _ : unitO, na_own p ⊤) Γ α τ'. Local Opaque thunked thunkedV Thunk. Program Definition ı_scope : @lang_generic.interp_scope (gReifiers_ops NotCtxDep rs) R _ Empty_set := λne (x : ∅), match x with end. - Lemma compat_glue_to_affine_bool {S} (Ω : tyctx S) α : + Lemma compat_glue_to_affine_bool {S : Set} `{HE : EqDecision S} `{!Finite S} (Ω : S → ty) α : io_valid □ α Tnat ⊢ valid2 Ω (constO (glue2_bool _ (α ı_scope))) tBool. Proof. @@ -97,7 +97,7 @@ Section glue. iIntros ([]). } iSpecialize ("H" $! tt with "Hp"). - simp interp_ssubst. simpl. + simpl. iApply (wp_bind _ (IFSCtx _ _)). { solve_proper. } iApply (wp_wand with "H"). @@ -112,7 +112,8 @@ Section glue. * rewrite IF_True ; last lia. iApply wp_val; eauto with iFrame. Qed. - Lemma compat_glue_to_affine_nat {S} (Ω : tyctx S) α : + + Lemma compat_glue_to_affine_nat {S : Set} `{HE : EqDecision S} `{!Finite S} (Ω : S → ty) α : io_valid □ α Tnat ⊢ valid2 Ω (constO (α ı_scope)) tInt. Proof. @@ -124,32 +125,23 @@ Section glue. iIntros ([]). } iSpecialize ("H" $! tt with "Hp"). - simp interp_ssubst. simpl. + simpl. iApply (wp_wand with "H"). iIntros (αv). iDestruct 1 as (_) "[Ha Hp]". iDestruct "Ha" as (σ') "[Ha Hs]". iModIntro. eauto with iFrame. Qed. - Lemma IT_move_from_affine (α : @interp_scope (@gReifiers_ops NotCtxDep sz rs) R _ [] -n> IT) - : @lang_generic.interp_scope (@gReifiers_ops NotCtxDep sz rs) R _ ∅ -n> IT. - Proof. - unshelve econstructor. - - intros g. apply α. - constructor. - - repeat intro. - f_equiv. - Defined. - Lemma compat_glue_from_affine_bool α : - valid2 empC α tBool ⊢ - heap_ctx -∗ io_valid □ (IT_move_from_affine α) Tnat. + valid2 □ α tBool ⊢ + heap_ctx -∗ io_valid □ α Tnat. Proof. iIntros "H #Hctx". iIntros (σ ss) "Hs Hss". iIntros (?) "Hp". - iSpecialize ("H" $! emp_ssubst with "Hctx [] [$Hs $Hp]"). - { iApply ssubst_valid_nil. } + iSpecialize ("H" $! ss with "Hctx [] [$Hs $Hp]"). + { iApply ssubst_valid_empty. } + simpl. iApply (wp_wand with "H"). iIntros (αv) "Ha". iDestruct "Ha" as (σ') "[Ha [Hs Hp]]". iModIntro. simpl. iFrame. iExists tt,_; iFrame. @@ -157,22 +149,22 @@ Section glue. Qed. Lemma compat_glue_from_affine_nat α : - valid2 empC α tInt ⊢ - heap_ctx -∗ io_valid □ (IT_move_from_affine α) Tnat. + valid2 □ α tInt ⊢ + heap_ctx -∗ io_valid □ α Tnat. Proof. iIntros "H #Hctx". iIntros (σ ss) "Hs Hss". iIntros (?) "Hp". - iSpecialize ("H" $! emp_ssubst with "Hctx [] [$Hs $Hp]"). - { iApply ssubst_valid_nil. } + iSpecialize ("H" $! ss with "Hctx [] [$Hs $Hp]"). + { iApply ssubst_valid_empty. } iApply (wp_wand with "H"). iIntros (αv) "Ha". iDestruct "Ha" as (σ') "[Ha [Hs Hp]]". iModIntro. iExists tt. eauto with iFrame. Qed. Lemma compat_glue_from_affine_unit α : - valid2 empC α tUnit ⊢ - heap_ctx -∗ io_valid □ (constO (glue_from_affine _ ty_conv_unit (α ()))) Tnat. + valid2 □ α tUnit ⊢ + heap_ctx -∗ io_valid □ (constO (glue_from_affine _ ty_conv_unit (α ı_scope))) Tnat. Proof. iIntros "H #Hctx". iIntros (σ ss) "Hs Hss". @@ -187,10 +179,10 @@ Section glue. Lemma compat_glue_from_affine_fun (τ1 τ2 : ty) (τ1' τ2' : io_lang.ty) α (glue_to_affine glue_from_affine : IT -n> IT) : (∀ α, io_valid □ α τ1' - ⊢ valid2 empC (constO (glue_to_affine (α ı_scope))) τ1) → - (∀ α, valid2 empC (constO α) τ2 + ⊢ valid2 □ (constO (glue_to_affine (α ı_scope))) τ1) → + (∀ α, valid2 □ (constO α) τ2 ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine α)) τ2') → - valid2 empC (constO α) (tArr τ1 τ2) + valid2 □ (constO α) (tArr τ1 τ2) ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine_fun _ glue_from_affine glue_to_affine α)) @@ -203,8 +195,8 @@ Section glue. iIntros (σ ss) "Hs ?". simpl. iIntros (?) "Hp". - iSpecialize ("H" $! emp_ssubst with "Hctx [] [$Hs $Hp]"). - { iApply ssubst_valid_nil. } + iSpecialize ("H" $! ss with "Hctx [] [$Hs $Hp]"). + { iApply ssubst_valid_empty. } simpl. iApply wp_let. { solve_proper. } iApply (wp_wand with "H"). @@ -274,8 +266,8 @@ Section glue. iSpecialize ("G1" with "[Hg]"). { iIntros (σ0 ss0) "Hs Has". simpl. iApply expr_pred_ret. simpl. eauto with iFrame. } - iSpecialize ("G1" $! emp_ssubst with "Hctx [] [$Hst $Hp]"). - { iApply ssubst_valid_nil. } + iSpecialize ("G1" $! ss with "Hctx [] [$Hst $Hp]"). + { iApply ssubst_valid_empty. } iApply (wp_wand with "G1"). clear βv σ'. iIntros (βv). iDestruct 1 as (σ') "[Hb [Hst Hp]]". @@ -298,11 +290,11 @@ Section glue. iApply ("G1" $! tt with "Hp"). Qed. - Lemma compat_glue_to_affine_fun {S} (Ω : tyctx S) (τ1 τ2 : ty) + Lemma compat_glue_to_affine_fun {S : Set} `{HE : EqDecision S} `{!Finite S} (Ω : S → ty) (τ1 τ2 : ty) (τ1' τ2' : io_lang.ty) α (glue_to_affine glue_from_affine : IT -n> IT) : (∀ α, io_valid □ α τ2' ⊢ valid2 Ω (constO (glue_to_affine (α ı_scope))) τ2) → - (∀ α, valid2 empC (constO α) τ1 + (∀ α, valid2 □ (constO α) τ1 ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine α)) τ1') → io_valid □ α (Tarr (Tarr Tnat τ1') τ2') ⊢ valid2 Ω @@ -314,11 +306,9 @@ Section glue. iIntros (αs) "#Hctx Has". iIntros (σ) "[Hs Hp]". simpl. iSpecialize ("H" $! _ ı_scope with "Hs []"). - { - iIntros ([]). - } + { iIntros ([]). } iSpecialize ("H" $! tt with "Hp"). - simp interp_ssubst. simpl. + simpl. iApply wp_let. { solve_proper. } iApply (wp_wand with "H"). @@ -332,7 +322,6 @@ Section glue. iSimpl. clear σ σ'. iIntros (σ) "[Hs Hp]". iApply (wp_bind _ (AppRSCtx _)). - { solve_proper. } iApply (wp_Thunk with "Hctx"). { solve_proper. } iNext. iIntros (l) "Hl". @@ -435,20 +424,20 @@ Section glue. simpl. done. Qed. - Lemma glue_to_affine_compatibility {S} (Ω : tyctx S) (τ1 : ty) (τ1' : io_lang.ty) + Lemma glue_to_affine_compatibility {S : Set} `{HE : EqDecision S} `{!Finite S} (Ω : S → ty) (τ1 : ty) (τ1' : io_lang.ty) (Hconv : ty_conv τ1 τ1') α : io_valid □ α τ1' ⊢ valid2 Ω (constO (glue_to_affine _ Hconv (α ı_scope))) τ1 with glue_from_affine_compatibility (τ1 : ty) (τ1' : io_lang.ty) (Hconv : ty_conv τ1 τ1') (α : IT) : - valid2 empC (constO α) τ1 ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine _ Hconv α)) τ1'. + valid2 □ (constO α) τ1 ⊢ heap_ctx -∗ io_valid □ (constO (glue_from_affine _ Hconv α)) τ1'. Proof. - destruct Hconv. - + by iApply compat_glue_to_affine_bool. - + by iApply compat_glue_to_affine_nat. + + by iApply (@compat_glue_to_affine_bool). + + by iApply (@compat_glue_to_affine_nat). + iIntros "_". simpl. iApply compat_unit. - + simpl. iApply compat_glue_to_affine_fun. - * apply glue_to_affine_compatibility. + + simpl. iApply (@compat_glue_to_affine_fun). + * by apply glue_to_affine_compatibility. * apply glue_from_affine_compatibility. - destruct Hconv. + iApply compat_glue_from_affine_bool. @@ -459,7 +448,7 @@ Section glue. * apply glue_from_affine_compatibility. Qed. - Lemma fundamental_affine_glued {S} (Ω : tyctx S) (e : expr S) τ : + Lemma fundamental_affine_glued {S : Set} `{HE : EqDecision S} `{!Finite S} (Ω : S → ty) (e : expr S) τ : typed_glued Ω e τ → ⊢ valid2 Ω (interp_expr _ e) τ. Proof. @@ -467,13 +456,24 @@ Section glue. - iApply glue_to_affine_compatibility. by iApply fundamental. - by iApply compat_var. - - by iApply compat_lam. - - by iApply compat_app. - - by iApply compat_pair. - - by iApply compat_destruct. - - by iApply compat_alloc. - - by iApply compat_replace. - - by iApply compat_dealloc. + - iApply compat_lam. + iApply IHtyped. + - iApply (@compat_app _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply (@compat_pair _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply (@compat_destruct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply compat_alloc. + iApply IHtyped. + - iApply (@compat_replace _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ S1 S2 EqDecisionLeft FiniteLeft EqDecisionRight FiniteRight). + + iApply IHtyped1. + + iApply IHtyped2. + - iApply compat_dealloc. + iApply IHtyped. - by iApply compat_nat. - by iApply compat_bool. - by iApply compat_unit. @@ -491,10 +491,10 @@ Require Import gitrees.gitree.greifiers. Lemma logrel2_adequacy (cr : nat) R `{!Cofe R, !SubOfe locO R, !SubOfe natO R, !SubOfe unitO R} Σ `{!invGpreS Σ}`{!statePreG rs R Σ} `{!heapPreG rs R Σ} `{!na_invG Σ} - (τ : ty) (α : unitO -n> IT (gReifiers_ops NotCtxDep rs) R) (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : + (τ : ty) (α : interp_scope Empty_set -n> IT (gReifiers_ops NotCtxDep rs) R) (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ} p, - (£ cr ⊢ valid2 rs p empC α τ)%I) → - ssteps (gReifiers_sReifier NotCtxDep rs) (α ()) st β st' k → + (£ cr ⊢ valid2 rs p □ α τ)%I) → + ssteps (gReifiers_sReifier NotCtxDep rs) (α (ı_scope rs)) st β st' k → (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) ∨ (β ≡ Err OtherError) ∨ (∃ βv, IT_of_V βv ≡ β). @@ -538,11 +538,11 @@ Proof. simpl. iMod na_alloc as (p) "Hp". iPoseProof (@Hlog _ _ _ p with "Hcr") as "Hlog". - iSpecialize ("Hlog" $! emp_ssubst with "Hinv []"). - { iApply ssubst_valid_nil. } + iSpecialize ("Hlog" $! (ı_scope _) with "Hinv []"). + { iApply ssubst_valid_empty. } unfold expr_pred. simpl. iSpecialize ("Hlog" $! ios with "[$Hio $Hp]"). - iModIntro. simp interp_ssubst. + iModIntro. simpl. iApply (wp_wand with "Hlog"). eauto with iFrame. Qed. @@ -550,8 +550,8 @@ Qed. Definition R := sumO locO (sumO natO unitO). Lemma logrel2_safety e τ (β : IT (gReifiers_ops NotCtxDep rs) R) st st' k : - typed_glued empC e τ → - ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ()) st β st' k → + typed_glued □ e τ → + ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e (ı_scope _)) st β st' k → (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1) ∨ (β ≡ Err OtherError) ∨ (∃ βv, IT_of_V βv ≡ β). diff --git a/theories/input_lang/interp.v b/theories/examples/input_lang/interp.v similarity index 99% rename from theories/input_lang/interp.v rename to theories/examples/input_lang/interp.v index 41bf8af..c0ae876 100644 --- a/theories/input_lang/interp.v +++ b/theories/examples/input_lang/interp.v @@ -1,5 +1,5 @@ From gitrees Require Import gitree lang_generic. -From gitrees.input_lang Require Import lang. +From gitrees.examples.input_lang Require Import lang. Require Import Binding.Lib. Require Import Binding.Set. diff --git a/theories/input_lang/lang.v b/theories/examples/input_lang/lang.v similarity index 100% rename from theories/input_lang/lang.v rename to theories/examples/input_lang/lang.v diff --git a/theories/input_lang/logpred.v b/theories/examples/input_lang/logpred.v similarity index 99% rename from theories/input_lang/logpred.v rename to theories/examples/input_lang/logpred.v index ea1b802..b548bc9 100644 --- a/theories/input_lang/logpred.v +++ b/theories/examples/input_lang/logpred.v @@ -1,6 +1,6 @@ (** Unary (Kripke) logical relation for the IO lang *) From gitrees Require Import gitree program_logic lang_generic. -From gitrees.input_lang Require Import lang interp. +From gitrees.examples.input_lang Require Import lang interp. Require Import Binding.Lib Binding.Set Binding.Env. Section io_lang. diff --git a/theories/input_lang/logrel.v b/theories/examples/input_lang/logrel.v similarity index 99% rename from theories/input_lang/logrel.v rename to theories/examples/input_lang/logrel.v index a1f0017..53f9756 100644 --- a/theories/input_lang/logrel.v +++ b/theories/examples/input_lang/logrel.v @@ -1,6 +1,6 @@ (** Logical relation for adequacy for the IO lang *) From gitrees Require Import gitree lang_generic. -From gitrees.input_lang Require Import lang interp. +From gitrees.examples.input_lang Require Import lang interp. Require Import Binding.Lib Binding.Set Binding.Env. Section logrel. diff --git a/theories/input_lang_callcc/hom.v b/theories/examples/input_lang_callcc/hom.v similarity index 98% rename from theories/input_lang_callcc/hom.v rename to theories/examples/input_lang_callcc/hom.v index 16d7ad0..3e4f03e 100644 --- a/theories/input_lang_callcc/hom.v +++ b/theories/examples/input_lang_callcc/hom.v @@ -1,5 +1,5 @@ From gitrees Require Import gitree. -From gitrees.input_lang_callcc Require Import lang interp. +From gitrees.examples.input_lang_callcc Require Import lang interp. Require Import gitrees.lang_generic. Require Import Binding.Lib Binding.Set Binding.Env. diff --git a/theories/input_lang_callcc/interp.v b/theories/examples/input_lang_callcc/interp.v similarity index 99% rename from theories/input_lang_callcc/interp.v rename to theories/examples/input_lang_callcc/interp.v index ae97290..8e41b93 100644 --- a/theories/input_lang_callcc/interp.v +++ b/theories/examples/input_lang_callcc/interp.v @@ -1,5 +1,5 @@ From gitrees Require Import gitree. -From gitrees.input_lang_callcc Require Import lang. +From gitrees.examples.input_lang_callcc Require Import lang. Require Import gitrees.lang_generic. Require Import Binding.Lib. diff --git a/theories/input_lang_callcc/lang.v b/theories/examples/input_lang_callcc/lang.v similarity index 100% rename from theories/input_lang_callcc/lang.v rename to theories/examples/input_lang_callcc/lang.v diff --git a/theories/input_lang_callcc/logrel.v b/theories/examples/input_lang_callcc/logrel.v similarity index 99% rename from theories/input_lang_callcc/logrel.v rename to theories/examples/input_lang_callcc/logrel.v index b88fac4..89d9c44 100644 --- a/theories/input_lang_callcc/logrel.v +++ b/theories/examples/input_lang_callcc/logrel.v @@ -1,6 +1,6 @@ (** Logical relation for adequacy for the IO lang *) From gitrees Require Import gitree. -From gitrees.input_lang_callcc Require Import lang interp hom. +From gitrees.examples.input_lang_callcc Require Import lang interp hom. Require Import gitrees.lang_generic. Require Import Binding.Lib Binding.Set Binding.Env. diff --git a/theories/lang_affine.v b/theories/lang_affine.v deleted file mode 100644 index b13c0be..0000000 --- a/theories/lang_affine.v +++ /dev/null @@ -1,245 +0,0 @@ -From gitrees Require Import prelude. -From gitrees Require Import gitree. -From Equations Require Import Equations. -Require Import List. -Import ListNotations. - -(** XXX: We /NEED/ this line for [Equations Derive] to work, *) -(* this flag is globally unset by std++, but Equations need obligations to be transparent. *) -Set Transparent Obligations. - -Derive NoConfusion NoConfusionHom for list. - -Definition scope := (list unit). - -(** Variables in a context *) -Inductive var : scope → Type := -| Vz : forall {S : scope} {s}, var (s::S) -| Vs : forall {S : scope} {s}, var S -> var (s::S) -. -Derive Signature NoConfusion for var. - -Inductive tyctx (ty : Type) : scope → Type := -| empC : tyctx ty [] -| consC : forall{Γ}, ty → tyctx ty Γ → tyctx ty (()::Γ) -. -Arguments empC {_}. -Arguments consC {_ _} _ _. - -Equations list_of_tyctx {S ty} (Γ : tyctx ty S) : list ty := - list_of_tyctx empC := []; - list_of_tyctx (consC τ Γ') := τ::list_of_tyctx Γ'. - -Equations tyctx_app {S1 S2 ty} (c1 : tyctx ty S1) (c2 : tyctx ty S2) : tyctx ty (S1++S2) := - tyctx_app empC c2 := c2; - tyctx_app (consC τ c1) c2 := consC τ (tyctx_app c1 c2). - -Inductive typed_var {ty : Type}: forall {S}, tyctx ty S → var S → ty → Prop := -| typed_var_Z S (τ : ty) (Γ : tyctx ty S) : - typed_var (consC τ Γ) Vz τ -| typed_var_S S (τ τ' : ty) (Γ : tyctx ty S) v : - typed_var Γ v τ → - typed_var (consC τ' Γ) (Vs v) τ -. - -Section interp. - Local Open Scope type. - Context {E: opsInterp}. - Context {R} `{!Cofe R}. - Notation IT := (IT E R). - Notation ITV := (ITV E R). - - Fixpoint interp_scope (S : scope) : ofe := - match S with - | [] => unitO - | τ::Sc => prodO IT (interp_scope Sc) - end. - - Instance interp_scope_cofe S : Cofe (interp_scope S). - Proof. induction S; simpl; apply _. Qed. - - Instance interp_scope_inhab S : Inhabited (interp_scope S). - Proof. induction S; simpl; apply _. Defined. - - Equations interp_var {S : scope} (v : var S) : interp_scope S -n> IT := - interp_var (S:=(_::_)) Vz := fstO; - interp_var (S:=(_::Sc)) (Vs v) := interp_var v ◎ sndO. - - Instance interp_var_ne S (v : var S) : NonExpansive (@interp_var S v). - Proof. - intros n D1 D2 HD12. induction v; simp interp_var. - - by f_equiv. - - eapply IHv. by f_equiv. - Qed. - - Global Instance interp_var_proper S (v : var S) : Proper ((≡) ==> (≡)) (interp_var v). - Proof. apply ne_proper. apply _. Qed. - - Definition interp_scope_split {S1 S2} : - interp_scope (S1 ++ S2) -n> interp_scope S1 * interp_scope S2. - Proof. - induction S1 as [|? S1]; simpl. - - simple refine (λne x, (tt, x)). - solve_proper. - - simple refine (λne xy, let ss := IHS1 xy.2 in ((xy.1, ss.1), ss.2)). - solve_proper. - Defined. - - (** scope substituions *) - Inductive ssubst : scope → Type := - | emp_ssubst : ssubst [] - | cons_ssubst {S} : ITV → ssubst S → ssubst (tt::S) - . - - Equations interp_ssubst {S} (ss : ssubst S) : interp_scope S := - interp_ssubst emp_ssubst := tt; - interp_ssubst (cons_ssubst αv ss) := (IT_of_V αv, interp_ssubst ss). - - Equations list_of_ssubst {S} (ss : ssubst S) : list ITV := - list_of_ssubst emp_ssubst := []; - list_of_ssubst (cons_ssubst αv ss) := αv::(list_of_ssubst ss). - - Equations ssubst_split {S1 S2} (αs : ssubst (S1++S2)) : ssubst S1 * ssubst S2 := - ssubst_split (S1:=[]) αs := (emp_ssubst,αs); - ssubst_split (S1:=u::_) (cons_ssubst αv αs) := - (cons_ssubst αv (ssubst_split αs).1, (ssubst_split αs).2). - Lemma interp_scope_ssubst_split {S1 S2} (αs : ssubst (S1++S2)) : - interp_scope_split (interp_ssubst αs) ≡ - (interp_ssubst (ssubst_split αs).1, interp_ssubst (ssubst_split αs).2). - Proof. - induction S1 as [|u S1]; simpl. - - simp ssubst_split. simpl. - simp interp_ssubst. done. - - dependent elimination αs as [cons_ssubst αv αs]. - simp ssubst_split. simpl. - simp interp_ssubst. repeat f_equiv; eauto; simpl. - + rewrite IHS1//. - + rewrite IHS1//. - Qed. - -End interp. - -(* Common definitions and lemmas for Kripke logical relations *) -Section kripke_logrel. - Variable s : stuckness. - - Context {sz : nat} {a : is_ctx_dep}. - Variable rs : gReifiers a sz. - Context {R} `{!Cofe R}. - - Notation F := (gReifiers_ops a rs). - Notation IT := (IT F R). - Notation ITV := (ITV F R). - Context `{!invGS Σ, !stateG rs R Σ}. - Notation iProp := (iProp Σ). - - Context {A:ofe}. (* The type & predicate for the explicit Kripke worlds *) - Variable (P : A -n> iProp). - - Implicit Types α β : IT. - Implicit Types αv βv : ITV. - Implicit Types Φ Ψ : ITV -n> iProp. - - Program Definition expr_pred (α : IT) (Φ : ITV -n> iProp) : iProp := - (∀ x : A, P x -∗ WP@{rs} α @ s {{ v, ∃ y : A, Φ v ∗ P y }}). - #[export] Instance expr_pred_ne : NonExpansive2 expr_pred. - Proof. solve_proper. Qed. - #[export] Instance expr_pred_proper : Proper ((≡) ==> (≡) ==> (≡)) expr_pred . - Proof. solve_proper. Qed. - - Definition ssubst_valid {ty} (interp_ty : ty → ITV -n> iProp) {S} (Γ : tyctx ty S) (ss : ssubst S) : iProp := - ([∗ list] τx ∈ zip (list_of_tyctx Γ) (list_of_ssubst (E:=F) ss), - interp_ty (τx.1) (τx.2))%I. - - Lemma ssubst_valid_nil {ty} (interp_ty : ty → ITV -n> iProp) : - ⊢ ssubst_valid interp_ty empC emp_ssubst. - Proof. - unfold ssubst_valid. - by simp list_of_tyctx list_of_ssubst. - Qed. - - Lemma ssubst_valid_cons {ty} (interp_ty : ty → ITV -n> iProp) {S} - (Γ : tyctx ty S) (ss : ssubst S) τ αv : - ssubst_valid interp_ty (consC τ Γ) (cons_ssubst αv ss) - ⊣⊢ interp_ty τ αv ∗ ssubst_valid interp_ty Γ ss. - Proof. - unfold ssubst_valid. - by simp list_of_tyctx list_of_ssubst. - Qed. - - Lemma ssubst_valid_app {ty} (interp_ty : ty → ITV -n> iProp) - {S1 S2} (Ω1 : tyctx ty S1) (Ω2 : tyctx ty S2) αs : - ssubst_valid interp_ty (tyctx_app Ω1 Ω2) αs ⊢ - ssubst_valid interp_ty Ω1 (ssubst_split αs).1 - ∗ ssubst_valid interp_ty Ω2 (ssubst_split αs).2. - Proof. - iInduction Ω1 as [|τ Ω1] "IH" forall (Ω2); simp tyctx_app ssubst_split. - - simpl. iIntros "$". iApply ssubst_valid_nil. - - iIntros "H". - rewrite {4 5}/ssubst_valid. - simpl in αs. - dependent elimination αs as [cons_ssubst αv αs]. - simp ssubst_split. simpl. - simp list_of_ssubst list_of_tyctx. - simpl. iDestruct "H" as "[$ H]". - by iApply "IH". - Qed. - - Lemma expr_pred_ret α αv Φ `{!IntoVal α αv} : - Φ αv ⊢ expr_pred α Φ. - Proof. - iIntros "H". - iIntros (x) "Hx". iApply wp_val. - eauto with iFrame. - Qed. - - Lemma expr_pred_frame α Φ : - WP@{rs} α @ s {{ Φ }} ⊢ expr_pred α Φ. - Proof. - iIntros "H". - iIntros (x) "Hx". - iApply (wp_wand with "H"). - eauto with iFrame. - Qed. -End kripke_logrel. - -Section kripke_logrel_ctx_indep. - Variable s : stuckness. - - Context {sz : nat}. - Variable rs : gReifiers NotCtxDep sz. - Context {R} `{!Cofe R}. - - Notation F := (gReifiers_ops NotCtxDep rs). - Notation IT := (IT F R). - Notation ITV := (ITV F R). - Context `{!invGS Σ, !stateG rs R Σ}. - Notation iProp := (iProp Σ). - - Context {A : ofe}. - Variable (P : A -n> iProp). - - Implicit Types α β : IT. - Implicit Types αv βv : ITV. - Implicit Types Φ Ψ : ITV -n> iProp. - - Local Notation expr_pred := (expr_pred s rs P). - - Lemma expr_pred_bind f `{!IT_hom f} α Φ Ψ `{!NonExpansive Φ} - : expr_pred α Ψ ⊢ - (∀ αv, Ψ αv -∗ expr_pred (f (IT_of_V αv)) Φ) - -∗ expr_pred (f α) Φ. - Proof. - iIntros "H1 H2". - iIntros (x) "Hx". - iApply wp_bind. - { solve_proper. } - iSpecialize ("H1" with "Hx"). - iApply (wp_wand with "H1"). - iIntros (βv). iDestruct 1 as (y) "[Hb Hy]". - iModIntro. - iApply ("H2" with "Hb Hy"). - Qed. -End kripke_logrel_ctx_indep. - -Arguments expr_pred_bind {_ _ _ _ _ _ _ _ _ _} f {_ _}. diff --git a/theories/examples/factorial.v b/theories/lib/factorial.v similarity index 97% rename from theories/examples/factorial.v rename to theories/lib/factorial.v index 3d2cc4e..259395e 100644 --- a/theories/examples/factorial.v +++ b/theories/lib/factorial.v @@ -1,7 +1,7 @@ -From Equations Require Import Equations. From gitrees Require Import gitree program_logic. -From gitrees.input_lang Require Import lang interp. -From gitrees.examples Require Import store while. +From gitrees.examples.input_lang Require Import lang interp. +From gitrees.effects Require Import store. +From gitrees.lib Require Import while. Section fact. Definition rs : gReifiers NotCtxDep 2 := diff --git a/theories/examples/iter.v b/theories/lib/iter.v similarity index 100% rename from theories/examples/iter.v rename to theories/lib/iter.v diff --git a/theories/examples/pairs.v b/theories/lib/pairs.v similarity index 100% rename from theories/examples/pairs.v rename to theories/lib/pairs.v diff --git a/theories/examples/while.v b/theories/lib/while.v similarity index 100% rename from theories/examples/while.v rename to theories/lib/while.v