Require Import DeBruijn.
Require Import Coercions.
Require Import FocusPaths.
Require Import Programs.
Require Import Layers.
Require Import WellLayeredness.
Require Import Types.
Require Import TypeEquality.
Require Import TypeContexts.
Require Import Subtyping.
Require Import DerivedSubtyping.
Require Import DerivedTyping.
Require Import Environments.
Require Import Typing.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import AntiFrameSwitch.
Require Import RawPrograms.
Require Import Erasure.
In this file, we focus on an example: the encoding of weak references with
affine content in terms of strong references and the anti-frame rule. This
example is explained in the journal paper.
-------------------------------------------------------------------------
The primitive operation PReadCap is restricted to references whose
content is duplicable. For this reason, in order to be able to read a
reference whose content is affine, one must first ``focus'' on the content
of the reference. This changes the type of the content from T to TyAt
sigma, for a fresh region sigma, and creates a capability for this
region, of the form TyRegionCap Singleton sigma T.
In the code that follows, we need to perform this operation at a moment
where we have a pair of a value and a capability for the reference. Thus,
the ``focus'' operation must go down into the pair, into the capability,
into the reference, and focus on the content there. Thus, we need the
following ``focus path''.
Definition pair_cap_ref :
path :=
PathPairRight Physical Logical (
PathRegionCapSingleton (
PathRef PathRoot)
).
In order to simplify the type derivation that follows, let us give a
derived typing rule for the ``focus'' operation at this particular path.
Lemma focus_pair_cap_ref:
forall T T1 rho,
wf T ->
wf T1 ->
wf rho ->
jp
(
PFocus pair_cap_ref)
(
TyMixPair T1 (
TyRegionCap Singleton rho (
TyRef T)))
(
TyExists (
TyMixPair
(
TyMixPair
(
lift_ty 0
T1)
(
TyRegionCap Singleton (
lift_ty 0
rho) (
TyRef (
TyAt (
TyVar 0))))
)
(
TyRegionCap Singleton (
TyVar 0) (
lift_ty 0
T))
)).
Proof.
-------------------------------------------------------------------------
We now define the term of interest, in the instrumented calculus.
The main function is mkwref, which means ``make a weak reference''.
This function initializes a strong reference r, creates a closure
which has access to r, and hides r from the outside world.
The closure constructed by mkwref is swap. It is a weak reference
with affine content, viewed as an object that offers a single method,
namely swap.
Coq requires that we define swap first, but it makes sense to read
the definition of mkwref first.
The code must unfortunately be expressed in de Bruijn style. In order
to make slightly more readable, we use the following convention. When
a new variable is introduced, we mention its name in a comment. When
a variable is referred to, we mention its name, preceded with an
exclamation mark, in a comment.
The definition of swap implicitly assumes that two type variables are in
scope, namely alpha, the type of the content of the reference, and rho,
the region which the reference inhabits. The definition assumes that one
term variable is in scope, namely r, the reference. It assumes that r
has infinite multiplicity and has type TyAt rho.
Definition swap :=
swap is a duplicable function. Its argument newvc is a pair of
a new value newv and a capability c for the reference r.
VBang (
VAbs (
As announced above, we must focus on the content of the reference
before we are allowed to read it.
Technical/personal remark: it may seem surprising that we focus on the
content of the reference prior to destructuring the pair newvc. One
might wish to instead decompose the pair into newv and c, and apply
the focus operation to c alone. However, we cannot do this, because
of our overly restrictive well-layeredness rule for TPrimApp, whose
argument and result must be physical.
TLet (
TPrimApp (
PFocus pair_cap_ref) (
VVar 0 )) (
The focus operation has produced an existential package whose content
is a triple of the value newv, a capability c1 for the reference,
and a capability c2 for the content of the reference. Decompose all
this. We refer to the newly created singleton region as sigma.
TLetUnpack (
VVar 0 ) (
TLetMixPair (
VVar 0 ) (
TLetMixPair (
VVar 1 ) (
The capability c1 testifies that r is a reference who content has
type TyAt sigma. This is a duplicable type, as witnessed by the
coercion CoAtBang. Thus, the capability c1 allows reading r
via the primitive operation PReadCap. The result is a pair of the
current value of the reference, oldv, and an unchanged capability,
which we informally keep referring to as c1.
TLet
(
TPrimApp PReadCap (
VMixPair
(
VVar 7 )
(
VCoApp (
CoRegionCap (
CoRef CoAtBang)) (
VVar 0 ))
))
(
TLetMixPair (
VVar 0 ) (
The capability c1 allows us to write the value newv into r.
This produces a pair of a unit value u and an updated capability
for r, which we informally keep referring to as c1. This new
capability witnesses that r is now again a reference with affine
content.
TLet
(
TPrimApp PWriteCap (
VMixPair
(
VPhyPair (
VVar 10 ) (
VVar 4 ))
(
VVar 0 )
))
(
TLetMixPair (
VVar 0 ) (
There remains to return a pair of the value oldv and the capability
c1. We must be careful, however, because oldv currently has type
TyBang (TyAt sigma). We deal with this in two steps. First, we get
rid of the replication using dereliction. This allows us to view oldv
as a value of type TyAt sigma. Then, we focus again: since we have a
capability c2 for the region sigma, we bring these two pieces of
information together and forget about sigma.
TVal (
VMixPair
(
VCoApp
(
CoDefocus PathRoot)
(
VMixPair (
VCoApp CoDereliction (
VVar 4 )) (
VVar 8 ))
)
(
VVar 0 )
)))))))))
)).
mkwref is a closed value.
Definition mkwref :=
mkwref is a polymorphic, duplicable function. Its argument initv is
the initial value of the reference that must be created.
VTyAbs (
VBang (
VAbs (
First, we allocate a strong reference. This creates an existential
package of a fresh singleton region rho and of a pair rc of the
fresh reference and of the capability that controls it. We open up
this existential package.
TLet (
TPrimApp PNewCap (
VVar 0 )) (
TLetUnpack (
VVar 0 ) (
Next, we apply the anti-frame rule, so as to hide the existence of
r. The nature of the ``hidden invariant'' is not visible here
(because terms do not refer to types) but will be evident in the
type derivation.
In this particular case, we are fortunate that the code in the scope of
the hide construct naturally has exactly one free variable, namely
rc, so the fact that THide requires the code to have exactly one
free variable is not a problem. No superfluous tupling/untupling is
necessary.
THide (
VVar 0 ) (
Open up the pair of r and c.
TLetMixPair (
VVar 0 ) (
Because r has type TyAt rho, it is duplicable. The coercion CoAtBang
is a witness of this fact. Then, the TLetBang construct allows us to
assign multiplicity MInfinity to r. This is important, because swap
claims to be a duplicable function and would not be allowed to capture a
non-duplicable variable.
TLetBang (
VCoApp CoAtBang (
VVar 1 )) (
Now, construct a pair of the function swap and the capability c.
The function swap *is* the weak reference that we are constructing:
it is an object with one method, swap. The capability c proves
that the hidden invariant initially holds: its presence is required
by the anti-frame rule, which consumes it.
TVal (
VMixPair swap (
VVar 1 ))
)))))
))).
-------------------------------------------------------------------------
mkwref is well-layered.
Lemma mkwref_well_layered:
wlv nil mkwref Physical.
Proof.
repeat econstructor.
Qed.
-------------------------------------------------------------------------
Here is the invariant (the capability) that is hidden by the anti-frame
rule. The invariant is parameterized by rho and alpha. It basically
states that we own the singleton region rho, which contains a value of
type alpha. As usual, the invariant is recursive, so as to encode the
fact that the invariant preserves itself. In other words, if the naïve
intended invariant is N, then the actual invariant should satisfy the
equation I = TyTensor N I.
Notation invariant rho alpha :=
(
TyMu (
TyTensor
(
TyRegionCap Singleton (
TyVar (
S rho)) (
TyRef (
TyVar (
S alpha))))
(
TyVar 0 )
)).
The invariant satisfies the following two recursive equations.
The first equation is simply the characterization of a recursive type.
It is a consequence of the lemma tyeq_fold.
Lemma equation1:
forall rho alpha,
tyeq
(
TyTensor
(
TyRegionCap Singleton (
TyVar rho) (
TyRef (
TyVar alpha)))
(
invariant rho alpha)
)
(
invariant rho alpha)
.
Proof.
intros.
eapply tyeq_transitive; [ |
eapply tyeq_fold;
wf |
eauto using wf_unfold ].
unfold unfold.
simpl.
unfold subst_var.
simpl.
repeat match goal with |-
context[?
n - 0] =>
replace (
n - 0)
with n by omega end.
eapply tyeq_reflexive.
wf.
Qed.
The second equation is a variant of the previous one. We use the fact that
TyTensor commutes with TyRegionCap and with TyRef. This allows us to
push the tensor inside.
Lemma equation2:
forall rho alpha,
tyeq
(
TyRegionCap Singleton (
TyVar rho)
(
TyRef (
TyTensor (
TyVar alpha) (
invariant rho alpha)))
)
(
invariant rho alpha)
.
Proof.
-------------------------------------------------------------------------
The following tactics help clean up the goal (a typing judgement) by
abstracting away the type of a variable when this variable has zero
multiplicity.
These tactics are ugly. First, there is code duplication: I need at least
one tactic for each de Bruijn index. Second, the use of generalize T is
brittle: if the type T happens to occur elsewhere, every occurrence of
T is abstracted away, which is not desired. I work around this issue by
using generalize T at k, for some fixed k, but this is brittle.
Another approach would be to apply a weakening lemma (see TermSubstitution)
in order to get rid of the unused variables. In principle, it should work.
It might be a bit painful, though, and it will cause a renumbering of the
variables that will not help me understand what I am doing. So I am sticking
with the simple-minded approach.
Ltac cleanup1 :=
match goal with
|-
jt _ (
_ ::
MZero ::
_)%
list
(
_ :: ?
T ::
_)%
list
_ _ =>
generalize T
end;
let T :=
fresh "
T"
in
intro T.
Ltac cleanup1at1 :=
match goal with
|-
jt _ (
_ ::
MZero ::
_)%
list
(
_ :: ?
T ::
_)%
list
_ _ =>
generalize T at 1
end;
let T :=
fresh "
T"
in
intro T.
Ltac cleanup2 :=
match goal with
|-
jt _ (
_ ::
_ ::
MZero ::
_)%
list
(
_ ::
_ :: ?
T ::
_)%
list
_ _ =>
generalize T
end;
let T :=
fresh "
T"
in
intro T.
Ltac cleanup3 :=
match goal with
|-
jt _ (
_ ::
_ ::
_ ::
MZero ::
_)%
list
(
_ ::
_ ::
_ :: ?
T ::
_)%
list
_ _ =>
generalize T
end;
let T :=
fresh "
T"
in
intro T.
Ltac cleanup5 :=
match goal with
|-
jt _ (
_ ::
_ ::
_ ::
_ ::
_ ::
MZero ::
_)%
list
(
_ ::
_ ::
_ ::
_ ::
_ :: ?
T ::
_)%
list
_ _ =>
generalize T at 2
end;
let T :=
fresh "
T"
in
intro T.
-------------------------------------------------------------------------
swap is well-typed.
The type derivation for swap assumes that r has multiplicity
MInfinity and type TyAt rho. The type of swap is the tensor
of the duplicable function type alpha -> alpha by the invariant.
Lemma swap_well_typed:
forall M E,
duplicable M ->
jv void
(
MInfinity ::
M)%
list
(
TyAt (
TyVar 0 ) ::
E)%
list
swap
(
TyTensor
(
TyBang (
TyArrow (
TyVar 1 ) (
TyVar 1 )))
(
invariant 0 1 )
).
Proof.
-------------------------------------------------------------------------
mkwref is well-typed.
We use the resource void, which is used to type-check source programs.
The only property that is required of void is that void be duplicable.
The multiplicity environment and the type environment are empty.
The type of mkwref is forall a. a -> (a -> a), where the arrow denotes
a duplicable function type. In other words, when applied to an initial
value, mkwref produces a fresh reference with affine content, which is
an abstract object equipped with a swap method.
Lemma mkwref_well_typed:
anti_frame_enabled ->
jv
void
nil
nil
mkwref
(
TyForall
(
TyBang (
TyArrow (
TyVar 0 )
(
TyBang (
TyArrow (
TyVar 0 ) (
TyVar 0 )))
))
).
Proof.
intros.
VTyAbs
econstructor.
simpl.
VBang
econstructor.
do 2 (
rewrite <-
duplicable_implies_core; [ |
eauto using @
duplicable_void ]).
VAbs
econstructor; [ |
wf ].
TLet
eapply JTLet; [
eapply duplicable_void |
eauto |
wf |
eauto | ].
TLetUnpack
econstructor; [
eapply duplicable_void |
eauto |
eauto | ].
simpl;
unfold lift_var;
simpl.
THide
econstructor; [
assumption
|
eauto
|
|
eapply duplicable_void
|
wf
|
wf
|
instantiate (1 :=
invariant 0 1);
wf
].
TLetMixPair
TyTensor distributes over TyPair.
econstructor; [
eapply duplicable_void | |
eapply JVEq; [
eauto |
tyred_tyeq |
wf ] | ].
eauto.
TLetBang
econstructor.
eapply duplicable_void.
Focus 2.
VCoApp CoAtBang (VVar 1)
econstructor; [ |
eauto |
eauto ].
TyTensor distributes over TyAt.
eapply JVEq; [
eauto |
tyred_tyeq |
wf ].
Split.
eapply star_commutative.
eauto.
TVal
econstructor.
VMixPair
econstructor.
eapply duplicable_void.
Split.
eapply star_commutative.
eauto.
swap
eapply swap_well_typed;
eauto.
The second component of the pair proves that the invariant initially
holds. It is the capability c.
eapply JVEq; [
eauto using equation1 |
eauto |
wf ].
Qed.
-------------------------------------------------------------------------
We can now look at the erasure of mkwref and check (by visual inspection)
that this is the desired untyped code.
There is actually an extraneous beta-redex (a definition of the form let x
= x in ...) which remains after we erase the ``focus'' operation. I am
forced to introduce this let construct because TPrimApp is not a value
and cannot directly become the left-hand side of the TLetUnpack construct
that follows. It is a bit silly. Probably one could fix this, but I am not
going to attempt it...
Eval compute in (
erase_value mkwref).