Massive refactoring/reorganization of the code

F_mu_ref_conc/fundamental_unary.v

-From iris_logrel.F_mu_ref_conc Require Export logrel_unary.
-From iris_logrel.F_mu_ref_conc Require Import rules.
-From iris.base_logic Require Export big_op invariants.
-From iris.proofmode Require Import tactics.
-
-Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs,
-  env_PersistentP Δ →
-  ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
-Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
-
-Section typed_interp.
-  Context `{heapG Σ}.
-  Notation D := (valC -n> iProp Σ).
-
-  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
-    iApply (wp_bind [ctx]);
-    iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
-    iIntros (v) Hv.
-
-  Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
-
-  Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ.
-  Proof.
-    induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
-    - (* var *)
-      iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
-      rewrite /env_subst. simplify_option_eq. by value_case.
-    - (* unit *) value_case; trivial.
-    - (* nat *) value_case; simpl; eauto.
-    - (* bool *) value_case; simpl; eauto.
-    - (* nat bin op *)
-      smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHtyped1.
-      smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHtyped2.
-      iDestruct "Hv" as (n) "%"; iDestruct "Hv'" as (n') "%"; simplify_eq/=.
-      iApply wp_nat_binop. iNext. iIntros "!>".
-      destruct op; simpl; try destruct eq_nat_dec;
-        try destruct le_dec; try destruct lt_dec; eauto 10.
-    - (* pair *)
-      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1.
-      smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
-      value_case; eauto.
-    - (* fst *)
-      smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
-      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
-      iApply wp_fst; eauto using to_of_val.
-    - (* snd *)
-      smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
-      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
-      iApply wp_snd; eauto using to_of_val.
-    - (* injl *)
-      smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
-      value_case; eauto.
-    - (* injr *)
-      smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn.
-      value_case; eauto.
-    - (* case *)
-      smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn.
-      iDestruct (interp_env_length with "HΓ") as %?.
-      iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
-      + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext.
-        erewrite typed_subst_head_simpl by naive_solver.
-        iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
-      + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext.
-        erewrite typed_subst_head_simpl by naive_solver.
-        iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
-    - (* If *)
-      smart_wp_bind (IfCtx _ _) v "#Hv" IHtyped1; cbn.
-      iDestruct "Hv" as ([]) "%"; subst; simpl;
-        [iApply wp_if_true| iApply wp_if_false]; iNext;
-      [iApply IHtyped2| iApply IHtyped3]; auto.
-    - (* Rec *)
-      value_case. simpl. iAlways. iLöb as "IH". iIntros (w) "#Hw".
-      iDestruct (interp_env_length with "HΓ") as %?.
-      iApply wp_rec; auto 1 using to_of_val. iNext.
-      asimpl. change (Rec _) with (of_val (RecV e.[upn 2 (env_subst vs)])) at 2.
-      erewrite typed_subst_head_simpl_2 by naive_solver.
-      iApply (IHtyped Δ (_ :: w :: vs)). 
-      iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
-    - (* app *)
-      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
-      smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
-      iApply wp_mono; [|iApply "Hv"]; auto.
-    - (* TLam *)
-      value_case.
-      iAlways; iIntros (τi) "%". iApply wp_tlam; iNext.
-      iApply IHtyped. by iApply interp_env_ren.
-    - (* TApp *)
-      smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
-      iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|]; cbn.
-      iIntros (w) "?". by iApply interp_subst.
-    - (* Fold *)
-      iApply (wp_bind [FoldCtx]);
-        iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto].
-      iIntros (v) "#Hv". value_case.
-      rewrite /= -interp_subst fixpoint_unfold /=.
-      iAlways; eauto.
-    - (* Unfold *)
-      iApply (wp_bind [UnfoldCtx]);
-        iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto].
-      iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
-      change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl.
-      iDestruct "Hv" as (w) "#[% Hw]"; subst.
-      iApply wp_fold; cbn; auto using to_of_val.
-      iNext; iModIntro. by iApply interp_subst.
-    - (* Pack *)
-      iApply (wp_bind [PackCtx]);
-      iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto].
-      iIntros (v) "#Hv". value_case.
-      rewrite /= -interp_subst /=.
-      iExists v. iSplit; eauto.
-      iAlways. iExists (⟦ τ' ⟧ Δ). iSplit; eauto.
-      iPureIntro. intro. by apply interp_persistent.
-    - (* Unpack *)
-      smart_wp_bind (UnpackLCtx (e2.[up (env_subst vs)])) v "#Hv" IHtyped1; cbn.
-      iDestruct "Hv" as (v') "[% #Hv']".
-      iDestruct "Hv'" as (τi) "[% Hv']".
-      subst. simpl. iApply wp_pack; eauto using to_of_val.
-      iNext. asimpl. 
-      rewrite /log_typed /interp_expr in IHtyped2.
-      iApply wp_wand_r. iSplitL.
-      + iDestruct (interp_env_length with "HΓ") as %?.
-        asimpl. erewrite typed_subst_head_simpl; eauto; last first.
-        { rewrite cons_length fmap_length. auto. }
-        iApply (IHtyped2 (τi :: Δ)).
-        iApply interp_env_cons. iFrame "Hv'".
-        iApply (interp_env_ren with "HΓ").
-      + (* remains to show the equivalence equivalence *)
-        replace (τi :: Δ) with ([] ++ [τi] ++ Δ); eauto.
-        iIntros (v) "H".
-        replace (⟦ τ2 ⟧ Δ v) with (⟦ τ2 ⟧ ([] ++ Δ) v); eauto.
-        iApply (interp_weaken [] [τi]). simpl.
-        rewrite upn0. iFrame.
-    - (* Fork *)
-      iApply wp_fork. iNext; iSplitL; trivial.
-      iApply wp_wand_l. iSplitL; [|iApply IHtyped; auto]; auto.
-    - (* Alloc *)
-      smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iApply wp_fupd.
-      iApply wp_alloc; auto 1 using to_of_val.
-      iNext; iIntros (l) "Hl".
-      iMod (inv_alloc _ with "[Hl]") as "HN";
-        [| iModIntro; iExists _; iSplit; trivial]; eauto.
-    - (* Load *)
-      smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
-      iDestruct "Hv" as (l) "[% #Hv]"; subst.
-      iApply wp_atomic; eauto.
-      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".      
-      iApply (wp_load with "Hw1"). 
-      iNext.
-      iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.      
-    - (* Store *)
-      smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
-      smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
-      iDestruct "Hv" as (l) "[% #Hv]"; subst.
-      iApply wp_atomic; eauto.
-      iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
-      iApply (wp_store with "Hz1"); auto using to_of_val. 
-      iNext.
-      iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
-    - (* CAS *)
-      smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHtyped1; cbn.
-      smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHtyped2; cbn.
-      smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHtyped3; cbn. iClear "HΓ".
-      iDestruct "Hv1" as (l) "[% Hv1]"; subst.
-      iApply wp_atomic; eauto.
-      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
-      destruct (decide (v2 = w)) as [|Hneq]; subst.
-      + iApply (wp_cas_suc with "Hw1"); auto using to_of_val.
-        iNext.
-        iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
-      + iApply (wp_cas_fail with "Hw1"); auto using to_of_val.
-        iNext.
-        iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
-  Qed.
-End typed_interp.

F_mu_ref_conc/hax.v

-(* the contents of this file sould belong elsewhere *)
-From iris.proofmode Require Import tactics.
-From iris_logrel.F_mu_ref_conc Require Import lang logrel_binary.
-
-Definition lamsubst (e : expr) (v : val) : expr :=
-  match e with
-  | Rec (BNamed f) x e' => lang.subst f e (subst' x (of_val v) e')
-  | Rec BAnon x e' => subst' x (of_val v) e'
-  | _ => e
-  end.
-
-Notation "e $/ v" := (lamsubst e%E v%V) (at level 71, left associativity) : expr_scope.
-(* ^ this should be left associative at a level lower than that of `bin_log_related` *)
-
-Section hax.
-  Context `{logrelG Σ}.
-  Notation D := (prodC valC valC -n> iProp Σ).
-  Implicit Types Δ : listC D.
-
-  Lemma weird_bind e Q :
-    WP App e tt {{ Q }} ⊢ WP e {{ v, WP (App v tt) {{ Q }} }}.
-  Proof.
-    (* ugh, turns out this is just the inverse bind:
-       Check (wp_bind_inv (fun v => App v #())). *)
-    iLöb as "IH" forall (e).
-    iIntros "wp".
-    rewrite (wp_unfold _ e) /wp_pre /=.
-    remember (to_val e) as eval. destruct eval.
-    - symmetry in Heqeval. rewrite -(of_to_val _ _ Heqeval). eauto.
-    - iIntros (σ1) "Hσ1".
-      rewrite wp_unfold /wp_pre /=.
-      iMod ("wp" $! σ1 with "Hσ1") as "[r wp]". iModIntro.
-      iDestruct "r" as %er.
-      assert (reducible e σ1).
-      { symmetry in Heqeval.
-        unfold reducible in er.
-        destruct er as (e2 & σ2 & efs & Hpst).
-        inversion Hpst; simpl in *; subst; clear Hpst.
-        admit. }
-      iSplitR; eauto.
-      iNext.
-      iIntros (e2 σ2 efs) "Hpst". iDestruct "Hpst" as %Hpst.
-      iSpecialize ("wp" $! (App e2 tt) σ2 efs).
-      iAssert (⌜prim_step (e (Lit tt))%E σ1 (e2 (Lit tt)%E) σ2 efs⌝)%I as "Hprim'".
-      { iPureIntro.
-        inversion Hpst; simpl in *; subst; clear Hpst.
-        eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (Lit tt)%E])); simpl; eauto.
-          by rewrite fill_app.
-          by rewrite fill_app. }
-      iMod ("wp" with "Hprim'") as "[$ [wp $]]". iModIntro.
-      by iApply "IH".
-  Abort.
-
-  (* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
-  (*   Closed ∅ (Lam x e) → *)
-  (*   to_val (lang.subst x (of_val v) e) = Some ev → *)
-  (*   Γ ⊨ (App (Lam x e) v) ≤log≤ t : τ *)
-  (*   ⊢ Γ ⊨ (lang.subst x (of_val v) e) ≤log≤ t : τ. *)
-  (* Proof. *)
-  (*   iIntros (??) "Hr". *)
-  (*   Transparent bin_log_related. *)
-  (*   iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". *)
-  (*   cbn-[subst_p].  *)
-  (*   (* assert (Closed ∅ (lang.subst x v e)). *) *)
-  (*   (* { eapply is_closed_subst_preserve; eauto. solve_closed. } *) *)
-  (*   rewrite /env_subst !Closed_subst_p_id. *)
-  (*   iSpecialize ("Hr" with "Hs []"). *)
-  (*   { iAlways. by iFrame. } *)
-  (*   rewrite /env_subst. erewrite (Closed_subst_p_id (fst <$> vvs)); last first. *)
-  (*   { rewrite /Closed. simpl. *)
-  (*     rewrite /Closed /= in H1. split_and; eauto; try solve_closed. } *)
-  (*   iMod ("Hr" with "Hj") as "Hr". *)
-  (*   iModIntro. simpl. *)
-  (*   rewrite {1}wp_unfold /wp_pre /=. *)
-  (*   iApply wp_value; eauto. *)
-  (*   iApply (wp_bind_inv in "Hr". *)
-End hax.

F_mu_ref_conc/logrel_unary.v

-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
-From iris_logrel.F_mu_ref_conc Require Export rules typing.
-From iris.algebra Require Import list.
-From iris.base_logic Require Import big_op namespaces invariants.
-Import uPred.
-
-Definition logN : namespace := nroot .@ "logN".
-
-(** interp : is a unary logical relation. *)
-Section logrel.
-  Context `{heapG Σ}.
-  Notation D := (valC -n> iProp Σ).
-  Implicit Types τi : D.
-  Implicit Types Δ : listC D.
-  Implicit Types interp : listC D → D.
-
-  Program Definition env_lookup (x : var) : listC D -n> D := λne Δ,
-    from_option id (cconst True)%I (Δ !! x).
-  Solve Obligations with solve_proper_alt.
-
-  Definition interp_unit : listC D -n> D := λne Δ w, ⌜w = ttV⌝%I.
-  Definition interp_nat : listC D -n> D := λne Δ w, ⌜∃ n, w = #nv n⌝%I.
-  Definition interp_bool : listC D -n> D := λne Δ w, ⌜∃ n, w = #♭v n⌝%I.
-
-  Program Definition interp_prod
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
-    (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
-  Solve Obligations with solve_proper.
-
-  Program Definition interp_sum
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
-    ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
-  Solve Obligations with solve_proper.
-
-  Program Definition interp_arrow
-      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
-    (□ ∀ v, interp1 Δ v → WP App (of_val w) (of_val v) {{ interp2 Δ }})%I.
-  Solve Obligations with solve_proper.
-
-  Program Definition interp_forall
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
-    (□ ∀ τi : D,
-      ⌜∀ v, PersistentP (τi v)⌝ → WP TApp (of_val w) {{ interp (τi :: Δ) }})%I.
-  Solve Obligations with solve_proper.
-
-  Program Definition interp_exists
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
-    (∃ v, ⌜w = PackV v⌝ ∧ □ ∃ τi : D, ⌜∀ v, PersistentP (τi v)⌝ ∧ interp (τi :: Δ) v)%I.
-  Solve Obligations with solve_proper.
-
-  Definition interp_rec1
-      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
-    (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
-
-  Global Instance interp_rec1_contractive
-    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
-  Proof. by solve_contractive. Qed.
-
-  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
-    fixpoint (interp_rec1 interp Δ).
-  Next Obligation. 
-    intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
-  Qed.
-
-  Program Definition interp_ref_inv (l : loc) : D -n> iProp Σ := λne τi,
-    (∃ v, l ↦ᵢ v ∗ τi v)%I.
-  Solve Obligations with solve_proper.
-
-  Program Definition interp_ref
-      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
-    (∃ l, ⌜w = LocV l⌝ ∧ inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
-  Solve Obligations with solve_proper.
-
-  Fixpoint interp (τ : type) : listC D -n> D :=
-    match τ return _ with
-    | TUnit => interp_unit
-    | TNat => interp_nat
-    | TBool => interp_bool
-    | TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
-    | TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2)
-    | TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
-    | TVar x => env_lookup x
-    | TForall τ' => interp_forall (interp τ')
-    | TExists τ' => interp_exists (interp τ')
-    | TRec τ' => interp_rec (interp τ')
-    | Tref τ' => interp_ref (interp τ')
-    end.
-  Notation "⟦ τ ⟧" := (interp τ).
-
-  Definition interp_env (Γ : list type)
-      (Δ : listC D) (vs : list val) : iProp Σ :=
-    (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
-  Notation "⟦ Γ ⟧*" := (interp_env Γ).
-
-  Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
-    WP e {{ ⟦ τ ⟧ Δ }}%I.
-
-  Class env_PersistentP Δ :=
-    env_persistentP : Forall (λ τi, ∀ v, PersistentP (τi v)) Δ.
-  Global Instance env_persistent_nil : env_PersistentP [].
-  Proof. by constructor. Qed.
-  Global Instance env_persistent_cons τi Δ :
-    (∀ v, PersistentP (τi v)) → env_PersistentP Δ → env_PersistentP (τi :: Δ).
-  Proof. by constructor. Qed.
-  Global Instance env_persistent_lookup Δ x v :
-    env_PersistentP Δ → PersistentP (env_lookup x Δ v).
-  Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
-  Global Instance interp_persistent τ Δ v :
-    env_PersistentP Δ → PersistentP (interp τ Δ v).
-  Proof.
-    revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
-    rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=.
-    by apply always_intro'.
-  Qed.
-  Global Instance interp_env_persistent Γ Δ vs :
-    env_PersistentP Δ → PersistentP (⟦ Γ ⟧* Δ vs) := _.
-
-  Lemma interp_weaken Δ1 Π Δ2 τ :
-    ⟦ τ.[upn (length Δ1) (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2)
-    ≡ ⟦ τ ⟧ (Δ1 ++ Δ2).
-  Proof.
-    revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
-    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
-    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
-    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
-    - apply fixpoint_proper=> τi w /=.
-      properness; auto. apply (IHτ (_ :: _)).
-    - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
-      { by rewrite !lookup_app_l. }
-      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
-    - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
-    - intros w; simpl; properness; auto. by apply (IHτ (_ :: _)).
-    - intros w; simpl; properness; auto. by apply IHτ. 
-  Qed.
-
-  Lemma interp_subst_up Δ1 Δ2 τ τ' :
-    ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2)
-    ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
-  Proof.
-    revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto.
-    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
-    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
-    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
-    - apply fixpoint_proper=> τi w /=.
-      properness; auto. apply (IHτ (_ :: _)).
-    - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
-      { by rewrite !lookup_app_l. }
-      rewrite !lookup_app_r; [|lia ..].
-      destruct (x - length Δ1) as [|n] eqn:?; simpl.
-      { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
-    - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
-    - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
-    - intros w; simpl; properness; auto. by apply IHτ.
-  Qed.
-
-  Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
-  Proof. apply (interp_subst_up []). Qed.
-
-  Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ ⌜length Γ = length vs⌝.
-  Proof. by iIntros "[% ?]". Qed.
-
-  Lemma interp_env_Some_l Δ Γ vs x τ :
-    Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, ⌜vs !! x = Some v⌝ ∧ ⟦ τ ⟧ Δ v.
-  Proof.
-    iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
-    destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
-    { by rewrite -Hlen; apply lookup_lt_Some with τ. }
-    iExists v; iSplit. done. iApply (big_sep_elem_of with "HΓ").
-    apply elem_of_list_lookup_2 with x.
-    rewrite lookup_zip_with; by simplify_option_eq.
-  Qed.
-
-  Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ [].
-  Proof. iIntros ""; iSplit; auto. Qed.
-  Lemma interp_env_cons Δ Γ vs τ v :
-    ⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
-  Proof.
-    rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜(_ = _)⌝%I) -assoc.
-    by apply sep_proper; [apply pure_proper; omega|].
-  Qed.
-
-  Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
-    ⟦ subst (ren (+1)) <$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs.
-  Proof.
-    apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
-    revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
-    apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
-  Qed.
-End logrel.
-
-Typeclasses Opaque interp_env.
-Notation "⟦ τ ⟧" := (interp τ).
-Notation "⟦ τ ⟧ₑ" := (interp_expr τ).
-Notation "⟦ Γ ⟧*" := (interp_env Γ).

F_mu_ref_conc/proofmode.v

-From iris_logrel.F_mu_ref_conc.proofmode Require Export tactics rel_tactics.

F_mu_ref_conc/soundness_unary.v

-From iris_logrel.F_mu_ref_conc Require Export fundamental_unary.
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import adequacy.
-From iris.base_logic Require Import auth.
-
-Class heapPreIG Σ := HeapPreIG {
-  heap_preG_iris :> invPreG Σ;
-  heap_preG_heap :> gen_heapPreG loc val Σ
-}.
-
-Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
-  (∀ `{heapG Σ}, [] ⊨ e : τ) →
-  rtc step ([e], σ) (thp, σ') → e' ∈ thp →
-  is_Some (to_val e') ∨ reducible e' σ'.
-Proof.
-  intros Hlog ??. cut (adequate e σ (λ _, True)); first (intros [_ ?]; eauto).
-  eapply (wp_adequacy Σ _). iIntros (Hinv). 
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
-  iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
-  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
-  iApply (wp_wand with "[]").
-  - rewrite -(empty_env_subst e).
-    iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
-  - eauto.
-Qed.
-
-Corollary type_soundness e τ e' thp σ σ' :
-  [] ⊢ₜ e : τ →
-  rtc step ([e], σ) (thp, σ') → e' ∈ thp →
-  is_Some (to_val e') ∨ reducible e' σ'.
-Proof.
-  intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
-  set (HG := HeapPreIG Σ _ _). 
-  eapply (soundness Σ); eauto using fundamental.
-Qed.

README.md

@@ -17,3 +17,21 @@ Make sure that all the dependencies are installed and run `make`.
 See [refman.md](docs/refman.md).
 
 Work in progress.
+
+# Structure
+
+- `logrel.v` - exports all the modules required to perform refinement proofs such as those in the `example/` folder
+- `F_mu_ref_conc` - definition of the object language
+- `examples` - example refinements
+- `logrel` contains modules related to the relational interpretation
+  + `threadpool.v` - definitions for the ghost threadpool RA
+  + `rules_threadpool.v` - symbolic execution in the threadpool
+  + `proofmode/tactics_threadpool.v` - tactics for preforming symbolic execution in the threadpool
+  + `semtypes.v` - interpretation of types/semantics in terms of values
+  + `logrel_binary.v` - interpretation of sequents/semantics in terms of open expressions
+  + `rules.v` - symbolic execution rules for the relational interpretation
+  + `proofmode/tactics_rel.v` - tactics for performing symbolic execution in the relational interpretation
+  + `fundamental_binary.v` - compatibility lemmas and the fundamental theorem of logical relations
+  + `contextual_refinement.v` - proof that logical relations are closed under contextual refinement
+  + `soundness_binary.v` - typesafety and contextual refinement proofs for terms in the relational interpretation  
+- `prelude` - some files shares by the whole development

_CoqProject

--Q . iris_logrel
+-Q theories iris_logrel
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-prelude/ds.v
-prelude/base.v
-F_mu_ref_conc/binder.v
-F_mu_ref_conc/lang.v
-F_mu_ref_conc/subst.v
-F_mu_ref_conc/hax.v
-F_mu_ref_conc/reflection.v
-F_mu_ref_conc/rules.v
-F_mu_ref_conc/typing.v
-# F_mu_ref_conc/logrel_unary.v
-# F_mu_ref_conc/fundamental_unary.v
-F_mu_ref_conc/relational_properties.v
-F_mu_ref_conc/rules_binary.v
-F_mu_ref_conc/logrel_binary.v
-F_mu_ref_conc/fundamental_binary.v
-# F_mu_ref_conc/soundness_unary.v
-F_mu_ref_conc/context_refinement.v
-F_mu_ref_conc/adequacy.v
-F_mu_ref_conc/soundness_binary.v
-F_mu_ref_conc/proofmode/classes.v
-F_mu_ref_conc/proofmode/tactics.v
-F_mu_ref_conc/proofmode/rel_tactics.v
-F_mu_ref_conc/proofmode.v
-F_mu_ref_conc/notation.v
-F_mu_ref_conc/examples/lock.v
-F_mu_ref_conc/examples/counter.v
-F_mu_ref_conc/examples/lateearlychoice.v
-F_mu_ref_conc/examples/par.v
-F_mu_ref_conc/examples/bit.v
-F_mu_ref_conc/examples/stack/stack_rules.v
-F_mu_ref_conc/examples/stack/CG_stack.v
-F_mu_ref_conc/examples/stack/FG_stack.v
-F_mu_ref_conc/examples/stack/refinement.v
-F_mu_ref_conc/examples/typetest.v
+theories/prelude/ds.v
+theories/prelude/base.v
+theories/prelude/hax.v
+theories/F_mu_ref_conc/binder.v
+theories/F_mu_ref_conc/lang.v
+theories/F_mu_ref_conc/notation.v
+theories/F_mu_ref_conc/subst.v
+theories/F_mu_ref_conc/reflection.v
+theories/F_mu_ref_conc/rules.v
+theories/F_mu_ref_conc/typing.v
+theories/F_mu_ref_conc/context_refinement.v
+theories/F_mu_ref_conc/adequacy.v
+theories/F_mu_ref_conc/pureexec.v
+theories/F_mu_ref_conc/tactics.v
+theories/logrel/threadpool.v
+theories/logrel/rules_threadpool.v
+theories/logrel/semtypes.v
+theories/logrel/logrel_binary.v
+theories/logrel/rules.v 
+theories/logrel/proofmode/tactics_threadpool.v
+theories/logrel/proofmode/tactics_rel.v
+theories/logrel/fundamental_binary.v
+theories/logrel/contextual_refinement.v
+theories/logrel/soundness_binary.v
+theories/logrel.v
+theories/examples/lock.v
+theories/examples/counter.v
+theories/examples/lateearlychoice.v
+theories/examples/par.v
+theories/examples/bit.v
+theories/examples/stack/stack_rules.v
+theories/examples/stack/CG_stack.v
+theories/examples/stack/FG_stack.v
+theories/examples/stack/refinement.v
+theories/examples/typetest.v

F_mu_ref_conc/adequacy.v → theories/F_mu_ref_conc/adequacy.v

 From iris.program_logic Require Export weakestpre adequacy.
-From iris_logrel.F_mu_ref_conc Require Export rules.
 From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics.
+From iris_logrel.F_mu_ref_conc Require Export rules.
 Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {

F_mu_ref_conc/binder.v → theories/F_mu_ref_conc/binder.v

 (* This module defines binders and liftings of all the necessary
 operations/lemmas. *)
-From iris_logrel.prelude Require Export base.
 From iris.algebra Require Export base.
+From iris_logrel.prelude Require Export base.
 
 Inductive binder := BAnon | BNamed : string → binder.
 Delimit Scope binder_scope with bind.

F_mu_ref_conc/lang.v → theories/F_mu_ref_conc/lang.v

+From iris.algebra Require Import ofe.
+From iris.program_logic Require Export language.
 From iris.program_logic Require Export ectx_language ectxi_language.
 From iris_logrel.prelude Require Export base.
 From iris_logrel.F_mu_ref_conc Require Export binder.
-From iris.algebra Require Export ofe.
+
 Module lang.
   (** * Syntax and syntactic categories *)
   Definition loc := positive.
@@ -340,6 +342,20 @@ Module lang.
      σ !! l = Some v1 →
      head_step (CAS (Loc l) e1 e2) σ (#♭ true) (<[l:=v2]>σ) [].
 
+  Definition is_atomic (e : expr) : Prop :=
+    match e with
+    | Alloc e => is_Some (to_val e)
+    | Load e =>  is_Some (to_val e)
+    | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
+    | CAS e0 e1 e2 => is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
+    | Fork _ => True
+    | _ => False
+    end.
+
+  Canonical Structure stateC := leibnizC state.
+  Canonical Structure valC := leibnizC val.
+  Canonical Structure exprC := leibnizC expr.
+
   Lemma fill_item_val Ki e :
     is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
   Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
@@ -369,10 +385,6 @@ Module lang.
     let l := fresh (dom _ σ) in
     to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) [].
   Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
-
-  Canonical Structure stateC := leibnizC state.
-  Canonical Structure valC := leibnizC val.
-  Canonical Structure exprC := leibnizC expr.
 End lang.
 
 (** Language instance for Iris *)
@@ -390,26 +402,21 @@ Canonical Structure lang := ectx_lang (lang.expr).