add headers to files

theories/logrel/environments.v

-From actris.logrel Require Export term_types.
+(** This file contains definitions related to type environments. The following
+relations on environments are defined:
+
+- [env_ltyped Γ vs]: This relation indicates that the value map [vs] contains a
+  value for each type in the semantic type environment [Γ].
+- [env_split Γ Γ1 Γ2]: The semantic type environment [Γ] can be split into
+  (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
+systems. *)
+From actris.logrel Require Export term_types subtyping.
 From iris.proofmode Require Import tactics.
 
 Notation "<![ b := x ]!>" :=

theories/logrel/examples/double.v

+(** This file contains a proof that the program
+
+  λ c, (recv c ||| recv c)
+
+can be assigned the semantic type
+
+  chan (?int.?int.end) ⊸ (int * int)
+
+This cannot be shown directly using the semantic typing rules, and therefore
+manual proof is used to show that the program is semantically well-typed. This
+demonstrates the extensibility of the type system. *)
 From iris.algebra Require Import frac auth excl updates.
 From iris.heap_lang.lib Require Export par spin_lock.
 From actris.channel Require Import proofmode.

theories/logrel/examples/pair.v

+(** This file contains shows that the program
+
+  λ c, (recv c, recv c)
+
+can be assigned the type
+
+  chan (?int.?int.end) ⊸ (int * int)
+
+by exclusively using the semantic typing rules. *)
 From actris.logrel Require Export term_typing_rules.
 From iris.proofmode Require Import tactics.
 

theories/logrel/kind_tele.v

+(** This file defines kinded telescopes, which are used for representing binders
+in session types. *)
 From stdpp Require Import base tactics telescopes.
 From actris.logrel Require Import model.
 Set Default Proof Using "Type".

theories/logrel/lib/mutex.v

+(** This file defines a new semantic type former [mutex A], which is the type of
+mutexes containing a value of type [A]. Mutexes are copyable, regardless of
+whether the type contained in them is copyable. This makes them very useful for
+sharing affine resources (such as channels) between multiple threads.
+Internally, mutexes are implemented using a spin lock and a mutable reference.
+The operations for spin locks that are used by the mutex are defined in Iris.
+
+The following operations are supported on mutexes:
+- [mutex_alloc]: Takes a value and wraps it in a mutex.
+- [mutex_acquire]: Acquire the mutex and return the value contained in it.
+- [mutex_release]: Release the mutex, storing a given value in it.
+
+The typing rules for these operations additionally contain a type
+[mutexguard A], which represents a mutex that has been acquired. The typing
+rules for the operations require the [mutex] or [mutexguard] to be in a variable
+(i.e., let-bound), and the type of this variable in the typing context changes
+as the mutex is acquired and released.
+
+It is only possible to release a mutex after it has been opened. The
+[mutexguard A] is not copyable, since that would allow a mutex to be released
+multiple times after acquiring it once.
+
+This type former is strongly inspired by the [Mutex] type in the standard
+library of Rust, which has also been semantically modelled in the LambdaRust
+project.
+*)
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Export spin_lock.
 From actris.logrel Require Export term_types term_typing_judgment subtyping.

theories/logrel/model.v

+(** This file contains the definition of what semantic term types and semantic
+session types are. A semantic term type is a unary (Iris) predicate on values,
+as is customary in a logical relation for type soundness. A semantic session
+type is essentially an Actris protocol.
+
+There is a single variant [lty Σ k], which contains either a term type or a
+session type, depending on the kind [k]. The reason for having a single type
+containing both term types and session types is that it allows for uniform
+definitions of polymorphic binders for term types and session types, instead of
+having duplicated definitions.
+
+This file also defines a COFE structure on semantic term types and session
+types, which is required in order to define recursive term types and session
+types. *)
 From iris.algebra Require Export ofe.
 From actris.channel Require Export channel.
 

theories/logrel/operators.v

+(** This file defines semantic typing lemmas for the operators of the language.
+*)
 From actris.logrel Require Export term_types.
 From iris.heap_lang Require Import proofmode.
 

theories/logrel/session_types.v

+(** This file defines the semantic interpretations of sesssion 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
+[model.v]. *)
 From iris.algebra Require Export gmap.
 From actris.logrel Require Export model kind_tele.
 From actris.channel Require Export channel.

theories/logrel/subtyping.v

-From actris.logrel Require Export model.
+(** 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]. *)
+From actris.logrel Require Export model term_types.
 
 Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
   match k with
@@ -15,6 +21,10 @@ Arguments lty_bi_le : simpl never.
 Infix "<:>" := lty_bi_le (at level 70) : bi_scope.
 Instance: Params (@lty_bi_le) 2 := {}.
 
+Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
+  tc_opaque (A <: lty_copy A)%I.
+Instance: Params (@lty_copyable) 1 := {}.
+
 Section subtyping.
   Context {Σ : gFunctors}.
 
@@ -31,4 +41,9 @@ Section subtyping.
   Proof. solve_proper. Qed.
   Global Instance lty_bi_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_bi_le Σ k).
   Proof. solve_proper. Qed.
+
+  Global Instance lty_copyable_plain A : Plain (@lty_copyable Σ A).
+  Proof. rewrite /lty_copyable /=. apply _. Qed.
+  Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
+  Proof. rewrite /lty_copyable /=. solve_proper. Qed.
 End subtyping.

theories/logrel/subtyping_rules.v

+(** This file defines all of the semantic subtyping rules for term types and
+session types. *)
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.proofmode Require Import tactics.

theories/logrel/term_types.v

+(** This file contains the definitions of the semantic interpretations of the
+term type formers of the type system. The semantic interpretation of a type
+(former) is a unary Iris predicate on values [val → iProp], which determines
+when a value belongs to a certain type.
+
+The following types are defined:
+
+- [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
+  only be invoked once, since they might have captured affine resources.
+- [A → B]: the type of non-affine (copyable) functions from [A] to [B]. These
+  can be invoked any number of times. This is simply syntactic sugar for [copy
+  (A ⊸ B)].
+- [A * B], [A + B], [∀ X, A], [∃ X, A]: products, sums, universal types,
+  existential types.
+- [copy A]: inhabited by those values in the type [A] which are copyable. In the
+  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
+  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_mut A]: the type of mutable (unique) references to a value of type [A].
+  Since the reference is guaranteed to be unique, it's 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 mutable (shared) references to a value of type [A].
+- [chan P]: the type of channels, governed by the session type [P].
+
+In addition, some important properties, such as contractivity and
+non-expansiveness of these type formers is proved. This is important in order to
+use these type formers to define recursive types. *)
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Export spin_lock.
-From actris.logrel Require Export subtyping kind_tele.
+From actris.logrel Require Export model kind_tele.
 From actris.channel Require Export channel.
 
-Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
-
-Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
-Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
-Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
-  tc_opaque (A <: lty_copy A)%I.
-
 Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, ⌜ w = #() ⌝%I).
 Definition lty_bool {Σ} : ltty Σ := Ltty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I.
 Definition lty_int {Σ} : ltty Σ := Ltty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I.
+Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
 
 Definition lty_arr `{heapG Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
   ∀ v, ▷ ltty_car A1 v -∗ WP w v {{ ltty_car A2 }})%I.
@@ -29,6 +59,9 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
 
+Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
+Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
+
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
 Definition ref_shrN := nroot .@ "shr_ref".
@@ -40,7 +73,6 @@ Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
 
 Instance: Params (@lty_copy) 1 := {}.
 Instance: Params (@lty_copy_minus) 1 := {}.
-Instance: Params (@lty_copyable) 1 := {}.
 Instance: Params (@lty_arr) 2 := {}.
 Instance: Params (@lty_prod) 1 := {}.
 Instance: Params (@lty_sum) 1 := {}.
@@ -80,10 +112,6 @@ Section term_types.
   Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ).
   Proof. solve_proper. Qed.
 
-  Global Instance lty_copyable_plain A : Plain (lty_copyable A).
-  Proof. rewrite /lty_copyable /=. apply _. Qed.
-  Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
-  Proof. rewrite /lty_copyable /=. solve_proper. Qed.
 
   Global Instance lty_arr_contractive `{heapG Σ} n :
     Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.

theories/logrel/term_typing_judgment.v

+(** This file contains the definitions of the semantic typing relation
+[Γ ⊨ 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.
+
+In addition, we use the adequacy of Iris in order to show type soundness:
+programs which satisfy the semantic typing relation are safe. That is,
+semantically well-typed programs do not get stuck. *)
 From iris.heap_lang Require Import metatheory adequacy.
 From actris.logrel Require Export term_types.
 From actris.logrel Require Import environments.

theories/logrel/term_typing_rules.v

+(** This file defines all of the semantic typing lemmas for term types. Most of
+these lemmas are semantic versions of the syntactic typing judgments typically
+found in a syntactic type system. *)
 From stdpp Require Import pretty.
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
@@ -255,8 +258,12 @@ Section properties.
     iIntros (w) "[$ HΓ3]". by iApply env_ltyped_delete.
   Qed.
 
+<<<<<<< HEAD
 
   (** Mutable Reference properties *)
+=======
+  (** Mutable Unique Reference properties *)
+>>>>>>> add headers to files
   Lemma ltyped_alloc Γ1 Γ2 e A :
     (Γ1 ⊨ e : A ⫤ Γ2) -∗
     (Γ1 ⊨ ref e : ref_mut A ⫤ Γ2).
@@ -307,7 +314,7 @@ Section properties.
     iFrame "HΓ'".
   Qed.
 
-  (** Shared Reference properties *)
+  (** Mutable Shared Reference properties *)
   Lemma ltyped_upgrade_shared  Γ Γ' e A :
     (Γ ⊨ e : ref_mut (copy A) ⫤ Γ') -∗
     Γ ⊨ e : ref_shr A ⫤ Γ'.
@@ -397,6 +404,7 @@ Section properties.
     Qed.
   End with_spawn.
 
+  (** Channel properties *)
   Section with_chan.
     Context `{chanG Σ}.