ACTRIS COQ DEVELOPMENT
This directory contains the Coq mechanization of the Actris framework, first presented in the paper Actris: Session Type Based Reasoning in Separation Logic at POPL'20.
It has been built and tested with the following dependencies
- Coq 8.12.0
- 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
andrecv_spec
: proof rule fornew_chan
,send
, andrecv
. -
select_spec
andbranch_spec
: proof rule for the derived (binary)select
andbranch
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 executesend c v
by looking up ownership of a send protocolH : c ↣ <!> y1 .. yn, MSG v; {{ P }}; prot
in the proof mode context. The tactic instantiates the variablesy1 .. yn
using the termst1 .. tn
and usesselpat
to proveP
. If fewer termst
are given than variablesy
, they will be instantiated using existential variables (evars). The tactic will putH : c ↣ prot
back into the context. -
wp_recv (x1 .. xn) as "ipat"
: symbolically executerecv c
by looking upH : c ↣ <?> y1 .. yn, MSG v; {{ P }}; prot
in the proof mode context. The variablesy1 .. yn
are introduced asx1 .. xn
, and the predicateP
is introduced using the introduction patternipat
. The tactic will putH : c ↣ prot
back into the context. -
wp_select with "selpat"
: symbolically executeselect c b
by looking upH : c ↣ prot1 {Q1}<+>{Q2} prot2
in the proof mode context. The selection patternselpat
is used to resolve eitherQ1
orQ2
, based on the chosen branchb
. The tactic will putH : c ↣ prot1
orH : c ↣ prot2
back into the context based on the chosen branchb
. -
wp_branch as ipat1 | ipat2
: symbolically executebranch c e1 e2
by looking upH : c ↣ prot1 {Q1}<&>{Q2} prot2
in the proof mode context. The result of the tactic involves two subgoals, in whichQ1
andQ2
are introduced using the introduction patternsipat1
andipat2
, respectively. The tactic will putH : c ↣ prot1
andH : 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
intoprot2
if there is an instance of the type classProtoUnfold prot1 prot2
. When defining a recursive protocol, it is useful to define aProtoUnfold
instance to obtain automatic unfolding of the recursive protocol. For example, seesort_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 CPP21 submission, see papers/POPL20.md. papers/CPP21.md. papers/LMCS.md.