Bounded subtyping.

theories/logrel/subtyping_rules.v

@@ -53,9 +53,13 @@ Section subtyping_rules.
   Qed.
 
   (** Term subtyping *)
-  Lemma lty_le_any A : ⊢ A <: any.
+  Lemma lty_le_bot A : ⊢ ⊥ <: A.
   Proof. by iIntros (v) "!> H". Qed.
-  Lemma lty_copyable_any : ⊢@{iPropI Σ} lty_copyable any.
+  Lemma lty_copyable_bot : ⊢@{iPropI Σ} lty_copyable ⊥.
+  Proof. iApply lty_le_bot. Qed.
+  Lemma lty_le_top A : ⊢ A <: ⊤.
+  Proof. by iIntros (v) "!> H". Qed.
+  Lemma lty_copyable_top : ⊢@{iPropI Σ} lty_copyable ⊤.
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
 
   Lemma lty_le_copy A B : A <: B -∗ copy A <: copy B.
@@ -133,32 +137,41 @@ Section subtyping_rules.
       try iModIntro; first [iLeft; by auto|iRight; by auto].
   Qed.
 
-  Lemma lty_le_forall C1 C2 :
-    ▷ (∀ A, C1 A <: C2 A) -∗
-    (∀ A, C1 A) <: (∀ A, C2 A).
+  Lemma lty_le_forall {k} (Mlow1 Mup1 Mlow2 Mup2 : lty Σ k) C1 C2 :
+    Mlow1 <: Mlow2 -∗ Mup2 <: Mup1 -∗
+    ▷ (∀ M, Mlow2 <: M -∗ M <: Mup2 -∗ C1 M <: C2 M) -∗
+    lty_forall Mlow1 Mup1 C1 <: lty_forall Mlow2 Mup2 C2.
   Proof.
-    iIntros "#Hle" (v) "!> H". iIntros (w).
-    iApply (wp_step_fupd); first done.
-    { iIntros "!>!>!>". iExact "Hle". }
-    iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
-    by iApply "Hle'".
+    iIntros "#Hlow #Hup #Hle" (v) "!> H". iIntros (M) "#Hlow' #Hup'".
+    iApply wp_step_fupd; first done.
+    { iIntros "!> !> !>". iExact "Hle". }
+    iApply (wp_wand with "(H [] [])").
+    { iApply (lty_le_trans with "Hlow Hlow'"). }
+    { iApply (lty_le_trans with "Hup' Hup"). }
+    iIntros (v') "H Hle' !>". by iApply "Hle'".
   Qed.
   (* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
 
-  Lemma lty_le_exist C1 C2 :
-    ▷ (∀ A, C1 A <: C2 A) -∗
-    (∃ A, C1 A) <: (∃ A, C2 A).
+  Lemma lty_le_exist {k} (Mlow1 Mup1 Mlow2 Mup2 : lty Σ k) C1 C2 :
+    Mlow2 <: Mlow1 -∗ Mup1 <: Mup2 -∗
+    ▷ (∀ M, Mlow1 <: M -∗ M <: Mup1 -∗ C1 M <: C2 M) -∗
+    lty_exist Mlow1 Mup1 C1 <: lty_exist Mlow2 Mup2 C2.
   Proof.
-    iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
+    iIntros "#Hlow #Hup #Hle" (v) "!>". iDestruct 1 as (M) "(#Hlow' & #Hup' & H)".
+    iExists M. iSplit; [|iSplit].
+    { iApply (lty_le_trans with "Hlow Hlow'"). }
+    { iApply (lty_le_trans with "Hup' Hup"). }
+    by iApply "Hle".
   Qed.
-  Lemma lty_le_exist_elim C B :
-    ⊢ C B <: ∃ A, C A.
-  Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
-  Lemma lty_le_exist_copy F :
-    ⊢ (∃ A, copy (F A)) <:> copy (∃ A, F A).
+  Lemma lty_le_exist_intro {k} (Mlow Mup : lty Σ k) C M :
+    Mlow <: M -∗ M <: Mup -∗
+    C M <: lty_exist Mlow Mup C.
+  Proof. iIntros "#Hlow #Hup !>" (v) "Hle". iExists M. auto. Qed.
+  Lemma lty_le_exist_copy {k} (Mlow Mup : lty Σ k) C :
+    ⊢ lty_exist Mlow Mup (λ M, copy (C M))%lty <:> copy (lty_exist Mlow Mup C).
   Proof.
-    iSplit; iIntros "!>" (v); iDestruct 1 as (A) "#Hv";
-      iExists A; repeat iModIntro; iApply "Hv".
+    iSplit; iIntros "!>" (v);
+      iDestruct 1 as (A) "#(Hlow & Hup & Hv)"; iExists A; auto.
   Qed.
 
   (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)

theories/logrel/term_types.v

@@ -4,7 +4,8 @@ From iris.heap_lang Require Export spin_lock.
 From actris.logrel Require Export subtyping.
 From actris.channel Require Export channel.
 
-Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
+Instance lty_bot {Σ} : Bottom (ltty Σ) := Ltty (λ w, False%I).
+Instance lty_top {Σ} : Top (ltty Σ) := Ltty (λ w, True%I).
 
 Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
 Definition lty_copy_inv {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
@@ -24,10 +25,11 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
   (∃ w1, ⌜w = InjLV w1⌝ ∗ ▷ ltty_car A1 w1) ∨
   (∃ w2, ⌜w = InjRV w2⌝ ∗ ▷ ltty_car A2 w2))%I.
 
-Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
-  Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I.
-Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
-  Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
+Definition lty_forall `{heapG Σ} {k} (Mlow Mup : lty Σ k)
+    (C : lty Σ k → ltty Σ) : ltty Σ :=
+  Ltty (λ w, ∀ M, Mlow <: M -∗ M <: Mup -∗ WP w #() {{ ltty_car (C M) }})%I.
+Definition lty_exist {Σ k} (Mlow Mup : lty Σ k) (C : lty Σ k → ltty Σ) : ltty Σ :=
+  Ltty (λ w, ∃ M, Mlow <: M ∗ M <: Mup ∗ ▷ ltty_car (C M) w)%I.
 
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
@@ -62,7 +64,6 @@ Instance: Params (@lty_mutex) 3 := {}.
 Instance: Params (@lty_mutexguard) 3 := {}.
 Instance: Params (@lty_chan) 3 := {}.
 
-Notation any := lty_any.
 Notation "()" := lty_unit : lty_scope.
 Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
 Notation "'copy-' A" := (lty_copy_inv A) (at level 10) : lty_scope.
@@ -73,10 +74,11 @@ Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
 Infix "*" := lty_prod : lty_scope.
 Infix "+" := lty_sum : lty_scope.
 
+(* TODO: Have nice notations for bounded quantifiers *)
 Notation "∀ A1 .. An , C" :=
-  (lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope.
+  (lty_forall ⊥ ⊤ (λ A1, .. (lty_forall ⊥ ⊤(λ An, C%lty)) ..)) : lty_scope.
 Notation "∃ A1 .. An , C" :=
-  (lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
+  (lty_exist ⊥ ⊤(λ A1, .. (lty_exist ⊥ ⊤(λ An, C%lty)) ..)) : lty_scope.
 
 Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
 Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
@@ -121,20 +123,25 @@ Section term_types.
   Proof. solve_proper. Qed.
 
   Global Instance lty_forall_contractive `{heapG Σ} k n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
+    Proper (dist n ==> dist n ==> pointwise_relation _ (dist_later n) ==> dist n)
+           (@lty_forall Σ _ k).
   Proof.
-    intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
-    apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
+    intros Ml Ml' Hl Mu Mu' Hu C C' HC w. apply Ltty_ne=> v. f_equiv=> M.
+    do 2 (f_equiv; [by f_equiv|]).
+    apply (wp_contractive _ _ _ _ _)=> u. specialize (HC M).
     by destruct n as [|n]; simpl.
   Qed.
   Global Instance lty_forall_ne `{heapG Σ} k n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
+    Proper (dist n ==> dist n ==> pointwise_relation _ (dist n) ==> dist n)
+           (@lty_forall Σ _ k).
   Proof. solve_proper. Qed.
   Global Instance lty_exist_contractive k n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
+    Proper (dist n ==> dist n ==> pointwise_relation _ (dist_later n) ==> dist n)
+           (@lty_exist Σ k).
   Proof. solve_contractive. Qed.
   Global Instance lty_exist_ne k n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
+    Proper (dist n ==> dist n ==> pointwise_relation _ (dist n) ==> dist n)
+           (@lty_exist Σ k).
   Proof. solve_proper. Qed.
 
   Global Instance lty_ref_mut_contractive `{heapG Σ} : Contractive lty_ref_mut.

theories/logrel/term_typing_rules.v

@@ -202,43 +202,39 @@ Section properties.
   Qed.
 
   (** Universal Properties *)
-  Lemma ltyped_tlam Γ e k (C : lty Σ k → ltty Σ) :
-    (∀ M, Γ ⊨ e : C M ⫤ ∅) -∗ Γ ⊨ (λ: <>, e) : ∀ M, C M ⫤ ∅.
+  Lemma ltyped_tlam Γ e k Mlow Mup (C : lty Σ k → ltty Σ) :
+    (∀ M, Mlow <: M -∗ M <: Mup -∗ Γ ⊨ e : C M ⫤ ∅) -∗
+    Γ ⊨ (λ: <>, e) : lty_forall Mlow Mup C ⫤ ∅.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
     iSplitL; last by iApply env_ltyped_empty.
-    iIntros (M) "/=". wp_pures.
-    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
+    iIntros (M) "/= Hlow Hup". wp_pures.
+    iApply (wp_wand with "(He Hlow Hup HΓ)"). iIntros (v) "[$ _]".
   Qed.
 
-  Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k → ltty Σ) M :
-    (Γ ⊨ e : ∀ M, C M ⫤ Γ2) -∗ Γ ⊨ e #() : C M ⫤ Γ2.
+  Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k → ltty Σ) Mlow Mup M :
+    Mlow <: M -∗ M <: Mup -∗
+    (Γ ⊨ e : lty_forall Mlow Mup C ⫤ Γ2) -∗
+    Γ ⊨ e #() : C M ⫤ Γ2.
   Proof.
-    iIntros "#He" (vs) "!> HΓ /=".
+    iIntros "#Hlow #Hup #He" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
-    iApply (wp_wand with "HB [HΓ]"). by iIntros (v) "$".
+    iApply (wp_wand with "(HB Hlow Hup) [HΓ]"). by iIntros (v) "$".
   Qed.
 
   (** Existential properties *)
-  Lemma ltyped_pack Γ e k (C : lty Σ k → ltty Σ) M :
-    (Γ ⊨ e : C M) -∗ Γ ⊨ e : ∃ M, C M.
-  Proof.
-    iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
-  Qed.
-
   Definition unpack : val := λ: "exist" "f", "f" #() "exist".
 
-  Lemma ltyped_unpack k (C : lty Σ k → ltty Σ) B :
-    ⊢ ∅ ⊨ unpack : (∃ M, C M) → (∀ M, C M ⊸ B) ⊸ B.
+  Lemma ltyped_unpack k (C : lty Σ k → ltty Σ) Mlow Mup B :
+    ⊢ ∅ ⊨ unpack : lty_exist Mlow Mup C → lty_forall Mlow Mup (λ M, C M ⊸ B)%lty ⊸ B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
     iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v). iDestruct 1 as (M) "Hv".
+    iIntros "!>" (v). iDestruct 1 as (M) "(Hlow & Hup & Hv)".
     rewrite /unpack. wp_pures.
     iIntros (fty) "Hfty". wp_pures.
     iSpecialize ("Hfty" $! M).
-    wp_bind (fty _). wp_apply (wp_wand with "Hfty").
+    wp_bind (fty _). wp_apply (wp_wand with "(Hfty Hlow Hup)").
     iIntros (f) "Hf".
     wp_apply (wp_wand with "(Hf [Hv //])").
     iIntros (w) "HB". iApply "HB".
@@ -264,7 +260,7 @@ Section properties.
   longer use the memory at the old location. *)
   Definition load : val := λ: "r", (!"r", "r").
   Lemma ltyped_load A :
-    ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut any.
+    ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut ⊤.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
     iSplitL; last by iApply env_ltyped_empty.