Commit 0c4b9da9 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc tweaks.

parent a15377fd
Pipeline #27943 passed with stage
in 6 minutes and 12 seconds
......@@ -7,8 +7,8 @@ relations on environments are defined:
(semantically disjoint) [Γ1] and [Γ2].
- [env_copy Γ Γ']: [Γ'] is a copyable sub-environment of [Γ].
In addition, some lemmas about these definitions are proved, corresponding to
the syntactic typing rules that are typically found in linear/affine type
In addition, some lemmas/rules about these definitions are proved, corresponding
to the syntactic typing rules that are typically found in substructural type
systems. *)
From actris.logrel Require Export term_types subtyping.
From iris.proofmode Require Import tactics.
......
(** This file demonstrates how Löb induction can be used to prove subtyping
of recursive protocols that combine polymorphism and asynchornous subtyping.
In pseudo syntax, the subtyping we show is:
μ rec. ! (X,Y:★) (X ⊸ Y). !X. ?Y. rec
<: μ rec. ! (X1,X2:★) (X1 ⊸ bool). !X1. !(X2 ⊸ int). !X2. ?bool. ?int. rec
*)
From actris.channel Require Import proofmode proto channel.
From actris.logrel Require Import subtyping_rules.
From iris.proofmode Require Import tactics.
......@@ -5,32 +12,30 @@ From iris.proofmode Require Import tactics.
Section basics.
Context `{heapG Σ, chanG Σ}.
Definition prot1_aux : (lsty Σ lsty Σ) :=
λ rec, (<!!X Y> TY (X Y)%lty ; <!!> TY X;
<??> TY Y; rec)%lty.
Definition prot1_aux (rec : lsty Σ) : lsty Σ :=
<!! X Y> TY (X Y); <!!> TY X; <??> TY Y; rec.
Instance prot1_aux_contractive : Contractive prot1_aux.
Proof. solve_proto_contractive. Qed.
Definition prot1 := lty_rec prot1_aux.
Definition prot1'_aux : (lsty Σ lsty Σ) :=
λ rec, (<!!X Y> TY (X Y)%lty ; <!!> TY X;
<??> TY Y;
<!!X Y> TY (X Y)%lty ; <!!> TY X;
<??> TY Y; rec)%lty.
Definition prot1'_aux (rec : lsty Σ) : lsty Σ :=
<!! X Y> TY (X Y); <!!> TY X;
<??> TY Y;
<!! X Y> TY (X Y); <!!> TY X;
<??> TY Y; rec.
Instance prot1'_aux_contractive : Contractive prot1'_aux.
Proof. solve_proto_contractive. Qed.
Definition prot1' := lty_rec prot1'_aux.
Definition prot2_aux : (lsty Σ lsty Σ) :=
λ rec, (<!!X> TY (X lty_bool)%lty ; <!!> TY X;
<!!Y> TY (Y lty_int)%lty ; <!!> TY Y;
<??> TY lty_bool; <??> TY lty_int; rec)%lty.
Definition prot2_aux (rec : lsty Σ) : lsty Σ :=
<!! X> TY (X lty_bool); <!!> TY X;
<!! Y> TY (Y lty_int); <!!> TY Y;
<??> TY lty_bool; <??> TY lty_int; rec.
Instance prot2_aux_contractive : Contractive prot2_aux.
Proof. solve_proto_contractive. Qed.
Definition prot2 := lty_rec prot2_aux.
Lemma rec_swap_example :
prot1 <: prot2.
Lemma rec_swap_example : prot1 <: prot2.
Proof.
iApply (lty_le_trans _ prot1').
{ iLöb as "IH".
......@@ -41,22 +46,16 @@ Section basics.
iIntros (X Y). iExists X, Y. do 3 iModIntro.
iApply (lty_le_trans with "H1").
iIntros (X' Y'). iExists X', Y'. do 3 iModIntro.
iApply "IH".
}
iApply "IH". }
iApply lty_le_rec.
iIntros (M1 M2) "#Hrec".
iIntros (X). iExists X, lty_bool. iModIntro. iModIntro.
iIntros (Y).
iApply (lty_le_trans _ (<??> TY lty_bool ; <!!> TY Y lty_int ;
<!!> TY Y ; <??> TY lty_int ; M2)); last first.
{
iApply (lty_le_trans _ (<!!> TY Y lty_int ; <??> TY lty_bool ;
<!!> TY Y ; <??> TY lty_int ; M2)).
iIntros (S1 S2) "#Hrec".
iIntros (X). iExists X, lty_bool. iIntros "!> !>" (Y).
iApply (lty_le_trans _ (<??> TY lty_bool; <!!> TY Y lty_int;
<!!> TY Y; <??> TY lty_int; S2)); last first.
{ iApply (lty_le_trans _ (<!!> TY Y lty_int; <??> TY lty_bool;
<!!> TY Y; <??> TY lty_int; S2)).
{ iApply lty_le_swap_recv_send. }
iModIntro. iApply lty_le_swap_recv_send.
}
iModIntro. iExists Y, lty_int.
by do 3 iModIntro.
iModIntro. iApply lty_le_swap_recv_send. }
iModIntro. iExists Y, lty_int. by do 3 iModIntro.
Qed.
End basics.
(** This file defines semantic typing lemmas for the operators of the language.
*)
(** This file defines semantic typing judgments and typing lemmas for the
operators of the language. The typing judgments for operators are expressed
using type classes, so they can easily be solved automatically. *)
From actris.logrel Require Export term_types.
From iris.heap_lang Require Import proofmode.
......@@ -21,7 +22,7 @@ Section operators.
Context {Σ : gFunctors}.
Implicit Types A B : ltty Σ.
(* Unboxed types *)
(** Rules for unboxed types *)
Global Instance lty_unit_unboxed : LTyUnboxed (Σ:=Σ) ().
Proof. by iIntros (v ->). Qed.
Global Instance lty_bool_unboxed : LTyUnboxed (Σ:=Σ) lty_bool.
......@@ -33,7 +34,7 @@ Section operators.
Global Instance lty_ref_shr_unboxed `{heapG Σ} A : LTyUnboxed (ref_shr A).
Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
(* Operator typing *)
(** Rules for operator typing *)
Global Instance lty_un_op_int op : LTyUnOp (Σ:=Σ) op lty_int lty_int.
Proof. iIntros (?). iDestruct 1 as (i) "->". destruct op; eauto. Qed.
Global Instance lty_un_op_bool : LTyUnOp (Σ:=Σ) NegOp lty_bool lty_bool.
......
(** This file defines the semantic interpretations of session types as Actris
protocols. It includes session types for sending and receiving with session
polymorphism, as well as n-ary choice. Recursive protocols are defined in
the model.v file. *)
the [model.v] file. *)
From iris.algebra Require Export gmap.
From actris.logrel Require Export model telescopes.
From actris.channel Require Export channel.
......@@ -10,15 +10,15 @@ Definition lmsg Σ := iMsg Σ.
Delimit Scope lmsg_scope with lmsg.
Bind Scope lmsg_scope with lmsg.
Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
( v, MSG v {{ ltty_car A v}} ; (lsty_car S))%msg.
Definition lty_msg_exist {Σ} {k} (M : lty Σ k lmsg Σ) : lmsg Σ :=
( X, M X)%msg.
Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys Σ kt lmsg Σ) : lmsg Σ :=
ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M).
Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
( v, MSG v {{ ltty_car A v}} ; (lsty_car S))%msg.
Definition lty_end {Σ} : lsty Σ := Lsty END.
Definition lty_message {Σ} (a : action) (M : lmsg Σ) : lsty Σ :=
......@@ -93,8 +93,7 @@ Section session_types.
Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
Proof. solve_proper. Qed.
Global Instance lty_message_proper a :
Proper (() ==> ()) (@lty_message Σ a).
Global Instance lty_message_proper a : Proper (() ==> ()) (@lty_message Σ a).
Proof. apply ne_proper, _. Qed.
Global Instance lty_choice_ne a : NonExpansive (@lty_choice Σ a).
......
(** This file contains the definition of the semantic subtyping relation
[A <: B], where [A] and [B] can be either term types or session types, as
well as a semantic type equivalence relation [A <:> B], which is essentially
equivalent to having both [A <: B] and [B <: A]. Finally, the notion of a
*copyable type* is defined in terms of subtyping: a type [A] is copyable
when [A <: copy A]. *)
well as a semantic type equivalence relation [A <:> B], which is equivalent to
having both [A <: B] and [B <: A]. Finally, the notion of a *copyable type* is
defined in terms of subtyping: a type [A] is copyable when [A <: copy A]. *)
From actris.logrel Require Export model term_types.
Definition lsty_le_def {Σ} (P1 P2 : lsty Σ) :=
......
......@@ -105,8 +105,8 @@ Section subtyping_rules.
(A21 <: A11) - (A12 <: A22) -
(A11 A12) <: (A21 A22).
Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_le_arr. Qed.
(* This rule is really trivial, since → is syntactic sugar for copy (... ⊸ ...),
but we include it anyway for completeness' sake. *)
(** This rule is really trivial, since [A → B] is syntactic sugar for
[copy (A ⊸ B)], but we include it anyway for completeness' sake. *)
Lemma lty_copyable_arr_copy A B : @{iPropI Σ} lty_copyable (A B).
Proof. iApply lty_copyable_copy. Qed.
......@@ -198,20 +198,17 @@ Section subtyping_rules.
iApply lty_le_exist. iApply "Hle".
Qed.
(* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)
(* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
(* TODO(COPY): Commuting rule for recursive types, allowing [copy] to move
outside the recursive type. This rule should be derivable using Löb
induction. *)
Lemma lty_copyable_rec C `{!Contractive C} :
( A, lty_copyable A - lty_copyable (C A)) - lty_copyable (lty_rec C).
Proof.
iIntros "#Hcopy".
iLöb as "IH".
iIntros (v) "!> Hv".
rewrite /lty_rec.
rewrite {2}fixpoint_unfold.
iSpecialize ("Hcopy" with "IH").
iSpecialize ("Hcopy" with "Hv").
iDestruct "Hcopy" as "#Hcopy".
rewrite /lty_rec {2}fixpoint_unfold.
iDestruct ("Hcopy" with "IH Hv") as "{Hcopy} #Hcopy".
iModIntro.
iEval (rewrite fixpoint_unfold).
iApply "Hcopy".
......@@ -269,7 +266,7 @@ Section subtyping_rules.
Lemma lty_le_exist_elim_l k (M : lty Σ k lmsg Σ) S :
( (A : lty Σ k), (<??> M A) <: S) -
((<?? (A : lty Σ k)> M A) <: S).
(<?? (A : lty Σ k)> M A) <: S.
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto.
......@@ -277,7 +274,7 @@ Section subtyping_rules.
Lemma lty_le_exist_elim_r k (M : lty Σ k lmsg Σ) S :
( (A : lty Σ k), S <: (<!!> M A)) -
(S <: (<!! (A : lty Σ k)> M A)).
S <: (<!! (A : lty Σ k)> M A).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto.
......
......@@ -4,7 +4,7 @@ term type formers of the type system. The semantic interpretation of a type
when a value belongs to a certain type.
The following types are defined:
- [unit], [bool], [int]: basic types for unit, boolean and integer values,
- [unit], [bool], [int]: basic types for unit, Boolean and integer values,
respectively.
- [any]: inhabited by all values.
- [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can
......@@ -18,12 +18,12 @@ The following types are defined:
case of functions, for instance, functions (closures) which capture affine
resources are not copyable, whereas functions that do not capture resources are.
- [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have
that [copy- (copy A) <:> A]. This type is used to indicate the results of
that [copy- (copy A) :> A]. This type is used to indicate the results of
operations that might consume a resource, but do not always do so, depending
on whether the type [A] is copyable. Such operations result in a [copy- A],
which can be turned into an [A] using subtyping when [A] is copyable.
- [ref_uniq A]: the type of uniquely-owned mutable references to a value of type [A].
Since the reference is guaranteed to be unique, it's possible for the type [A]
Since the reference is guaranteed to be unique, it is possible for the type [A]
contained in the reference to change to a different type [B] by assigning to
the reference.
- [ref_shr A]: the type of shared mutable references to a value of type [A].
......
(** This file contains the definitions of the semantic typing relation
(** This file contains the definitions of the semantic typing judgment
[Γ ⊨ e : A ⫤ Γ'], indicating that in context [Γ], the expression [e] has type
[A], producing a new context [Γ']. The context is allowed to change to
accomodate things like changing the type of a channel after a receive.
......@@ -11,7 +11,7 @@ From actris.logrel Require Export term_types.
From actris.logrel Require Import environments.
From iris.proofmode Require Import tactics.
(* The semantic typing judgement *)
(** The semantic typing judgment *)
Definition ltyped `{!heapG Σ}
(Γ Γ' : gmap string (ltty Σ)) (e : expr) (A : ltty Σ) : iProp Σ :=
( vs, env_ltyped Γ vs -
......
......@@ -160,7 +160,7 @@ Section properties.
Lemma ltyped_snd Γ A1 A2 (x : string) :
Γ !! x = Some (A1 * A2)%lty
Γ Snd x : A2 <[x := (A1 * copy- A2)%lty]> Γ.
Γ Snd x : A2 <[x:=(A1 * copy- A2)%lty]> Γ.
Proof.
iIntros (Hx vs) "!> HΓ /=".
iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
......@@ -480,21 +480,19 @@ Section properties.
Qed.
Definition select : val := λ: "c" "i", send "c" "i".
Lemma ltyped_select Γ (c : string) (i : Z) (S : lsty Σ) Ss :
Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
Ss !! i = Some S
<[c := (chan (lty_select Ss))%lty]>Γ select c #i : ()
<[c := (chan S)%lty]>Γ.
<[x:=(chan (lty_select Ss))%lty]>Γ select x #i : ()
<[x:=(chan S)%lty]>Γ.
Proof.
iIntros (Hin).
iIntros "!>" (vs) "HΓ /=".
iIntros (Hin); iIntros "!>" (vs) "HΓ /=".
iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
{ by apply lookup_insert. }
rewrite Heq /select.
wp_send with "[]".
{ eauto. }
iSplitR; first done.
iDestruct (env_ltyped_insert _ _ c (chan _) with "[Hc //] HΓ")
as "HΓ'"=> /=.
iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
rewrite insert_delete insert_insert (insert_id vs)=> //.
by rewrite lookup_total_alt Hin.
Qed.
......@@ -538,14 +536,14 @@ Section properties.
rewrite assoc_L. iApply ("H" with "[$HA $HAs]").
Qed.
Definition chanbranch (xs : list Z) : val := λ: "c",
Definition branch (xs : list Z) : val := λ: "c",
switch_lams "f" 0 (length xs) $
let: "y" := recv "c" in
switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) "c".
Lemma ltyped_chanbranch Ss A xs :
Lemma ltyped_branch Ss A xs :
( x, x xs is_Some (Ss !! x))
chanbranch xs : chan (lty_branch Ss)
branch xs : chan (lty_branch Ss)
lty_arr_list ((λ x, (chan (Ss !!! x) A)%lty) <$> xs) A.
Proof.
iIntros (Hdom) "!>". iIntros (vs) "Hvs".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment