diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
index e4ab014ffc7ff48944c583362306d0d9d6e4a316..dfff320e49f842d29455464fd5e0f094089f8a06 100644
--- a/theories/logrel/environments.v
+++ b/theories/logrel/environments.v
@@ -1,4 +1,16 @@
-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 ]!>" :=
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index 333e5b69c0b4e39eb50376b8dcb858ed6d5428d8..ff514a1c925890a844c3380ff3f1a9ac166c28c8 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -1,3 +1,14 @@
+(** 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.
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 427c357259b1aa52a5bf5388582bef2970348695..ed65db36397c40a7a5f8283e219bc1fc1e32e2c4 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -1,3 +1,12 @@
+(** 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.
diff --git a/theories/logrel/kind_tele.v b/theories/logrel/kind_tele.v
index 2cd61549e76adeef69eb7d863648e0d7a769e4ba..5be0264c4b393b6c2d6d2720f2d78fa2739d69e5 100644
--- a/theories/logrel/kind_tele.v
+++ b/theories/logrel/kind_tele.v
@@ -1,3 +1,5 @@
+(** 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".
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index 95a8249089c7a6f0f9bbb2d379ac7a169220c0e7..b2ca4e94ce10ab5fca77fdf67008b78359e56d77 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -1,3 +1,29 @@
+(** 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.
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index a44e55ead02807c1cb82ac60a9d4dc6be7d80609..d38d587f00340fd33fb98bbfcbf4561f5f599f8f 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -1,3 +1,17 @@
+(** 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.
diff --git a/theories/logrel/operators.v b/theories/logrel/operators.v
index 6fd2d18c1fe9d272ae7c972f626ed13e09c2342b..ab7b5316662b00ac9f0034b20dd006c8cdb13602 100644
--- a/theories/logrel/operators.v
+++ b/theories/logrel/operators.v
@@ -1,3 +1,5 @@
+(** 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.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index f83f644eefa4e86bb445c402960c1f4652252fb7..d4dff05e7e5835b05810e1ebecf525229d8d42f4 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -1,3 +1,7 @@
+(** 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.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 5567d38d5ca8cded3931a5a4b6c838fb6b551495..428b13a2443ecf2cfdc07fcf28537c75fe179d20 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -1,4 +1,10 @@
-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.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 2715f374499420f08a5ef2a7e22ca8c34e573b12..9666ca087ef8db0ccaa0dc5b7f99f2192159ae4b 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -1,3 +1,5 @@
+(** 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.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index b69d653d7f06c18f548b41d1b3c2641084f48170..0a6cf4c680b6f13863e5ba5534b531c178012050 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -1,19 +1,49 @@
+(** 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.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 17c7797e4d8cdd7805c4b8a4fd3d1781aab61a73..0daef109783f17a9836fd391f1aa4197d4c04dcd 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -1,3 +1,11 @@
+(** 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.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 383be7e69ef5db2d8d4607f4069a7339769f0aa5..933148de1318d7c05b1de50b32ea5b1317d1247d 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -1,3 +1,6 @@
+(** 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 Σ}.