tlsomers
Actris

Repository



ACTRIS COQ DEVELOPMENT
This repository contains:

The Coq mechanization of the Actris framework, first presented in the paper
Actris: Session Type Based Reasoning in Separation Logic
at POPL'20
The logical relations model for a semantic session type system, first presented in
the paper
Machine-Checked Semantic Session Typing


It has been built and tested with the following dependencies

Coq 8.15.1
The version of Iris in the opam file


In order to build, install the above dependencies and then run
make -j [num CPU cores] to compile Actris.

Theory of Actris
The theory of Actris (semantics of channels, the model, and the proof rules)
can be found in the directory theories/channel.
The individual types contain the following:


theories/channel/proto_model.v: The
construction of the model of dependent separation protocols as the solution of
a recursive domain equation.

theories/channel/proto.v: The instantiation of
protocols with the Iris logic, definition of iProto_own for channel endpoint
ownership, and lemmas corresponding to the Actris proof rules.
The relevant definitions and proof rules are as follows:


iProto Σ: The type of protocols.

iProto_message: The constructor for sends and receives.

iProto_end: The constructor for terminated protocols.

iProto_le: The subprotocol relation for protocols (notation ⊑).


theories/channel/channel.v: The encoding of
bidirectional channels in terms of Iris's HeapLang language, with specifications
defined in terms of the dependent separation protocols.
The relevant definitions and proof rules are as follows:


iProto_mapsto: endpoint ownership (notation ↣).

new_chan_spec, send_spec and recv_spec: proof rule for new_chan,
send, and recv.

select_spec and branch_spec: proof rule for the derived (binary)
select and branch operations.


Notation
The following table gives a mapping between the notation in literature
and the Coq mechanization:
Dependent Separation Protocols:


POPL20 paper
Coq mechanization


Send
! x_1 .. x_n <v>{ P }. prot
<! x_1 .. x_n> MSG v {{ P }}; prot


Recv
? x_1 .. x_n <v>{ P }. prot
<? x_1 .. x_n> MSG v {{ P }}; prot


End
end
END


Select
prot_1 {Q_1}⊕{Q_2} prot_2
prot_1 <{Q_1}+{Q_2}> prot_2


Branch
prot_1 {Q_1}&{Q_2} prot_2
prot_1 <{Q_1}&{Q_2}> prot_2


Append
prot_1 · prot_2
prot_1 <++> prot_2


Dual
An overlined protocol
No notation


This notation is additionally used for the LMCS submission.
Semantic Session Types:


CPP21 submission
Coq mechanization


Send
!_{X_1 .. X_n} A . S
<!! X_1 .. X_n> TY A ; S


Recv
?_{X_1 .. X_n} A . S
<?? X_1 .. X_n> TY A ; S


End
end
END


Select
(+){ Ss }
lty_choice SEND Ss


Branch
&{ Ss }
lty_choice RECV Ss


Dual
An overlined type
No notation


N-append
S^n
lty_napp S n


Coq tactics
In order to prove programs using Actris, one can make use of a combination of
Iris's symbolic execution tactics for HeapLang programs and
Actris's symbolic execution tactics for message passing. The
Actris tactics are as follows:


wp_send (t1 .. tn) with "selpat": symbolically execute send c v by looking
up ownership of a send protocol H : c ↣ <!> y1 .. yn, MSG v; {{ P }}; prot
in the proof mode context. The tactic instantiates the variables y1 .. yn
using the terms t1 .. tn and uses selpat to prove P. If fewer terms
t are given than variables y, they will be instantiated using existential
variables (evars). The tactic will put H : c ↣ prot back into the context.

wp_recv (x1 .. xn) as "ipat": symbolically execute recv c by looking up
H : c ↣  <?> y1 .. yn, MSG v; {{ P }}; prot in the proof mode context. The
variables y1 .. yn are introduced as x1 .. xn, and the predicate P is
introduced using the introduction pattern ipat. The tactic will put
H : c ↣ prot back into the context.

wp_select with "selpat": symbolically execute select c b by looking up
H : c ↣  prot1 {Q1}<+>{Q2} prot2 in the proof mode context. The selection
pattern selpat is used to resolve either Q1 or Q2, based on the chosen
branch b. The tactic will put H : c ↣  prot1 or H : c ↣ prot2 back
into the context based on the chosen branch b.

wp_branch as ipat1 | ipat2: symbolically execute branch c e1 e2 by looking
up H : c ↣ prot1 {Q1}<&>{Q2} prot2 in the proof mode context. The result of
the tactic involves two subgoals, in which Q1 and Q2 are introduced using
the introduction patterns ipat1 and ipat2, respectively. The tactic will
put H : c ↣ prot1 and H : c ↣ prot2 back into the contexts of the two
respectively goals.

The above tactics implicitly perform normalization of the protocol prot in
the hypothesis H : c ↣ prot. For example, wp_send also works if there is a
channel with the protocol iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot).
Concretely, the normalization performs the following actions:

It re-associates appends (<++>), and removes left-identities (END) of it.
It moves appends (<++>) into sends (<!>), receives (<?>), selections
(<+>) and branches (<&>).
It distributes duals (iProto_dual) over append (<++>).
It unfolds prot1 into prot2 if there is an instance of the type class
ProtoUnfold prot1 prot2. When defining a recursive protocol, it is
useful to define a ProtoUnfold instance to obtain automatic unfolding
of the recursive protocol. For example, see sort_protocol_br_unfold in
theories/examples/sort_br_del.v.


Semantic Session Type System
The logical relation for type safety of a semantic session type system is contained
in the directory theories/logrel.
The logical relation is defined across the following files:


theories/logrel/model.v: Definition of the
notions of a semantic term type and a semantic session type in terms of
unary Iris predicates (on values) and Actris protocols, respectively. Also
provides the required Coq definitions for creating recursive term/session
types.

theories/logrel/term_types.v: Definitions
of the following semantic term types: basic types (integers, booleans, unit),
sums, products, copyable/affine functions, universally and existentially
quantified types, unique/shared references, and session-typed channels.

theories/logrel/session_types.v:
Definitions of the following semantic session types: sending and receiving
with session polymorphism, n-ary choice. Session type duality is also
defined here. Recursive session types can be defined using the mechanism
defined in theories/logrel/model.v.

theories/logrel/operators.v:
Type definitions of unary and binary operators.

theories/logrel/contexts.v:
Definition of the semantic type contexts, which is used in the semantic
typing relation. This also contains the rules for updating the context,
which is used for distributing affine resources across the
various parts of the proofs inside the typing rules.

theories/logrel/term_typing_judgment.v:
Definition of the semantic typing relation, as well as the proof of type
soundness, showing that semantically well-typed programs do not get stuck.

theories/logrel/subtyping.v:
Definition of the semantic subtyping relation for both term and session types.
This file also defines the notion of copyability of types in terms of subtyping.

theories/logrel/subtyping_rules.v:
Subtyping rules for term types and session types.

theories/logrel/term_typing_rules.v:
Semantic typing lemmas (typing rules) for the semantic term types.

theories/logrel/session_typing_rules.v:
Semantic typing lemmas (typing rules) for the semantic session types.

theories/logrel/napp.v:
Definition of session types iteratively being appended to themselves a finite
number of times, with support for swapping e.g. a send over an arbitrary number
of receives.

An extension to the basic type system is given in
theories/logrel/lib/mutex.v, which defines
mutexes as a type-safe abstraction. Mutexes are implemented using spin locks
and allow one to gain exclusive ownership of resources shared between multiple
threads. An encoding of a list type is found in
theories/logrel/lib/mutex.v, along with axillary
lemmas, and a weakest precondition for llength,
that converts ownership of a list type into a list reference predicate, with
the values of the list made explicit.

Paper-specific remarks
For remarks about the paper-specific submissions, see

papers/POPL20.md
papers/CPP21.md
papers/LMCS.md