Add extistential types to F_mu_ref_conc

F_mu_ref_conc/fundamental_binary.v

@@ -287,6 +287,60 @@ Section fundamental.
     iNext; iModIntro. iExists _; iFrame. by rewrite -interp_subst. 
   Qed.
 
+  Lemma bin_log_related_pack Γ e e' τ τ'
+      (IHHtyped : Γ ⊨ e ≤log≤ e' : τ.[τ'/]) :
+    Γ ⊨ Pack e ≤log≤ Pack e' : TExists τ.
+  Proof.
+    iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iApply (wp_bind [PackCtx]); iApply wp_wand_l; iSplitR;
+        [|iApply ('IHHtyped _ _ _ j (K ++ [PackCtx]));
+          rewrite ?fill_app; simpl; repeat iSplitR; trivial].
+    iIntros (v). iDestruct 1 as (v') "[Hw #Hiw]"; rewrite fill_app /=.
+    value_case.
+    iExists (PackV v'). simpl. iFrame.
+    iExists (v, v'). simpl; iSplit; eauto.
+    iAlways. rewrite -interp_subst. iExists (⟦ τ' ⟧ Δ).
+    iSplit; eauto. iPureIntro. apply _.
+  Qed.
+
+  (* TODO: can we get rid of typing information? *)
+  Lemma bin_log_related_unpack Γ e1 e1' e2 e2' τ τ2
+      (ActualTyped1 : τ :: (subst (ren (+1)) <$> Γ) ⊢ₜ e2 : (subst (ren (+1)) τ2))
+      (ActualTyped2 : τ :: (subst (ren (+1)) <$> Γ) ⊢ₜ e2' : (subst (ren (+1)) τ2))
+      (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : TExists τ)
+      (IHHtyped2 : τ :: (subst (ren (+1)) <$> Γ) ⊨ e2 ≤log≤ e2' : (subst (ren (+1)) τ2)) :
+    Γ ⊨ Unpack e1 e2 ≤log≤ Unpack e1' e2' : τ2.
+  Proof.
+    iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    smart_wp_bind (UnpackLCtx (e2.[up (env_subst (vvs.*1))])) v v' "[Hj #Hv]"
+      ('IHHtyped1 _ _ _ j (K ++ [UnpackLCtx _])); cbn.
+    iDestruct "Hv" as ([w w']) "[% #Hτi]"; simplify_eq/=.
+    iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
+    iApply wp_pack; eauto. iNext.
+    iMod (step_Pack _ _ j K with "[-]") as "Hz"; eauto. 
+    iApply wp_wand_r. iSplitL.
+    iDestruct (interp_env_length with "HΓ") as "%".
+    replace (e2.[up (env_subst (vvs.*1))].[of_val w/])
+       with (e2.[(env_subst (((w,w')::vvs).*1))]); eauto.
+    replace (e2'.[up (env_subst (vvs.*2))].[of_val w'/])
+       with (e2'.[(env_subst (((w,w')::vvs).*2))]); eauto.
+    iApply ('IHHtyped2 (τi :: Δ) _ _ j K).
+    { iFrame. iFrame "Hs".
+      iApply interp_env_cons; auto.
+      rewrite interp_env_ren. iFrame "HΓ". iFrame "Hτi". }
+    Focus 3.
+    iIntros (v) "Hv'". iDestruct "Hv'" as (v') "[Hv Hτ2]".
+    iExists v'.
+    replace (⟦ τ2 ⟧ Δ) with (⟦ τ2 ⟧ ([] ++ Δ)); eauto.
+    rewrite (interp_weaken [] [τi] Δ τ2). iFrame.
+
+    asimpl. erewrite typed_subst_head_simpl; eauto.
+    simpl. repeat rewrite fmap_length; eauto.
+
+    asimpl. erewrite typed_subst_head_simpl; eauto.
+    simpl. repeat rewrite fmap_length; eauto.
+  Qed.
+  
   Lemma bin_log_related_fork Γ e e'
       (IHHtyped : Γ ⊨ e ≤log≤ e' : TUnit) :
     Γ ⊨ Fork e ≤log≤ Fork e' : TUnit.
@@ -423,6 +477,8 @@ Section fundamental.
     - eapply bin_log_related_tapp; eauto.
     - eapply bin_log_related_fold; eauto.
     - eapply bin_log_related_unfold; eauto.
+    - eapply bin_log_related_pack; eauto.
+    - eapply bin_log_related_unpack; eauto.      
     - eapply bin_log_related_fork; eauto.
     - eapply bin_log_related_alloc; eauto.
     - eapply bin_log_related_load; eauto.

F_mu_ref_conc/fundamental_unary.v

@@ -102,6 +102,34 @@ Section typed_interp.
       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.

F_mu_ref_conc/lang.v

@@ -38,6 +38,9 @@ Module lang.
   (* Polymorphic Types *)
   | TLam (e : expr)
   | TApp (e : expr)
+  (* Existential types *)
+  | Pack (e : expr)
+  | Unpack (e : expr) (e : {bind 1 of expr})
   (* Concurrency *)
   | Fork (e : expr)
   (* Reference Types *)
@@ -70,6 +73,7 @@ Module lang.
   | InjLV (v : val)
   | InjRV (v : val)
   | FoldV (v : val)
+  | PackV (v : val)
   | LocV (l : loc).
 
   (* Notation for bool and nat *)
@@ -101,6 +105,7 @@ Module lang.
     | InjLV v => InjL (of_val v)
     | InjRV v => InjR (of_val v)
     | FoldV v => Fold (of_val v)
+    | PackV v => Pack (of_val v)
     | LocV l => Loc l
     end.
 
@@ -115,6 +120,7 @@ Module lang.
     | InjL e => InjLV <$> to_val e
     | InjR e => InjRV <$> to_val e
     | Fold e => v ← to_val e; Some (FoldV v)
+    | Pack e => v ← to_val e; Some (PackV v)
     | Loc l => Some (LocV l)
     | _ => None
     end.
@@ -136,6 +142,8 @@ Module lang.
   | IfCtx (e1 : {bind expr}) (e2 : {bind expr})
   | FoldCtx
   | UnfoldCtx
+  | PackCtx
+  | UnpackLCtx (e2 : expr)
   | AllocCtx
   | LoadCtx
   | StoreLCtx (e2 : expr)
@@ -161,6 +169,8 @@ Module lang.
     | IfCtx e1 e2 => If e e1 e2
     | FoldCtx => Fold e
     | UnfoldCtx => Unfold e
+    | PackCtx => Pack e
+    | UnpackLCtx e2 => Unpack e e2  
     | AllocCtx => Alloc e
     | LoadCtx => Load e
     | StoreLCtx e2 => Store e e2
@@ -206,6 +216,10 @@ Module lang.
   (* Polymorphic Types *)
   | TBeta e σ :
       head_step (TApp (TLam e)) σ e σ []
+  (* Existential types *)
+  | Unpack_Pack e1 v e2 σ :
+      to_val e1 = Some v →
+      head_step (Unpack (Pack e1) e2) σ e2.[e1/] σ []
   (* Concurrency *)
   | ForkS e σ:
       head_step (Fork e) σ Unit σ [e]

F_mu_ref_conc/logrel_binary.v

@@ -84,6 +84,12 @@ Section logrel.
             interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
   Solve Obligations with solve_proper.
 
+  Program Definition interp_exists
+      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
+    (∃ vv, ⌜ww = (PackV (vv.1), PackV (vv.2))⌝ 
+     ∧ □ ∃ τi : D, ⌜∀ ww, PersistentP (τi ww)⌝ ∧ interp (τi :: Δ) vv)%I.
+  Solve Obligations with solve_proper.
+
   Program Definition interp_rec1
       (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
     (□ ∃ vv, ⌜ww = (FoldV (vv.1), FoldV (vv.2))⌝ ∧ ▷ interp (τi :: Δ) vv)%I.
@@ -119,6 +125,7 @@ Section logrel.
     | TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
     | TVar x => ctx_lookup x
     | TForall τ' => interp_forall (interp τ')
+    | TExists τ' => interp_exists (interp τ')
     | TRec τ' => interp_rec (interp τ')
     | Tref τ' => interp_ref (interp τ')
     end.
@@ -165,6 +172,7 @@ Section logrel.
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
     - unfold interp_expr.
       intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
+    - intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
     - intros ww; simpl; properness; auto. by apply IHτ.
   Qed.
 
@@ -187,6 +195,7 @@ Section logrel.
       rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
     - unfold interp_expr.
       intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
+    - intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
     - intros ww; simpl; properness; auto. by apply IHτ.
   Qed.
 

F_mu_ref_conc/logrel_unary.v

@@ -44,6 +44,11 @@ Section logrel.
       ⌜∀ 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.
@@ -77,6 +82,7 @@ Section logrel.
     | 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.
@@ -124,7 +130,8 @@ Section logrel.
       { 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τ (_ :: _)).
+    - intros w; simpl; properness; auto. by apply IHτ. 
   Qed.
 
   Lemma interp_subst_up Δ1 Δ2 τ τ' :
@@ -144,6 +151,7 @@ Section logrel.
       { 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.
 

F_mu_ref_conc/rules.v

@@ -140,6 +140,15 @@ Section lang_rules.
     intros; inv_head_step; eauto.
   Qed.
 
+  Lemma wp_pack E e1 e2 v Φ :
+    to_val e1 = Some v →
+    ▷ WP e2.[e1/] @ E {{ Φ }} ⊢ WP Unpack (Pack e1) e2 @ E {{ Φ }}.
+  Proof.
+    intros <-%of_to_val. 
+    rewrite -(wp_lift_pure_det_head_step_no_fork (Unpack _ _) e2.[of_val v/]); eauto.
+    intros; inv_head_step; eauto.
+  Qed.
+
   Lemma wp_fst E e1 v1 e2 v2 Φ :
     to_val e1 = Some v1 → to_val e2 = Some v2 →
     ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.

F_mu_ref_conc/rules_binary.v

@@ -286,6 +286,12 @@ Section cfg.
     spec_ctx ρ ∗ j ⤇ fill K (Unfold (Fold e)) ={E}=∗ j ⤇ fill K e.
   Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
 
+  Lemma step_Pack E ρ j K e1 e2 v :
+    to_val e1 = Some v → nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K (Unpack (Pack e1) e2)
+    ={E}=∗ j ⤇ fill K e2.[e1/].
+  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
+
   Lemma step_fst E ρ j K e1 v1 e2 v2 :
     to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ j ⤇ fill K e1.

F_mu_ref_conc/typing.v

@@ -10,6 +10,7 @@ Inductive type :=
   | TRec (τ : {bind 1 of type})
   | TVar (x : var)
   | TForall (τ : {bind 1 of type})
+  | TExists (τ : {bind 1 of type})
   | Tref (τ : type).
 
 Instance Ids_type : Ids type. derive. Defined.
@@ -58,6 +59,10 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
   | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ → Γ ⊢ₜ TApp e : τ.[τ'/]
   | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜ Fold e : TRec τ
   | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ Unfold e : τ.[TRec τ/]
+  | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ Pack e : TExists τ
+  | TUnpack e1 e2 τ τ2 : Γ ⊢ₜ e1 : TExists τ →
+      τ :: (subst (ren (+1)) <$> Γ) ⊢ₜ e2 : (subst (ren (+1)) τ2) →
+      Γ ⊢ₜ Unpack e1 e2 : τ2                                                        
   | TFork e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
   | TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ
   | TLoad e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ
@@ -109,6 +114,10 @@ Proof.
     + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
     + intros [|x] H2; [by cbv |].
       asimpl; rewrite H1; auto with omega.
+  - apply (IHe0 (S m)); eauto. 
+    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+    + intros [|x] Hx. reflexivity.
+      asimpl. rewrite H1; eauto with omega.
 Qed.
 
 Definition env_subst (vs : list val) (x : var) : expr :=
@@ -120,6 +129,7 @@ Proof.
   - apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
   - f_equal. apply IHtyped.
   - by f_equal; rewrite map_length in IHtyped.
+  - f_equal. apply IHtyped1. rewrite map_length in IHtyped2. auto.
 Qed.
 
 Lemma n_closed_subst_head_simpl n e w ws :
@@ -180,6 +190,11 @@ Proof.
     asimpl in *. rewrite ?map_length in IHtyped.
     repeat rewrite fmap_app. apply IHtyped.
     by repeat rewrite fmap_app.
+  - econstructor; eauto. 
+    specialize (IHtyped2 (τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
+    repeat rewrite fmap_app.
+    asimpl in IHtyped2. asimpl. rewrite ?map_length in IHtyped2. apply IHtyped2.
+    by repeat rewrite fmap_app.
 Qed.
 
 Lemma context_weakening ξ Γ e τ :

_CoqProject

@@ -40,4 +40,4 @@ F_mu_ref_conc/examples/counter.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
\ No newline at end of file
+F_mu_ref_conc/examples/stack/refinement.v