Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Layers.
Require Import Types.
Require Import Store.
Require Import RawPrograms.
Require Import Programs.
Require Import Typing.
Require Import DerivedTyping.
Require Import Environments.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Monotonicity.
Require Import RegionAllocation.
Require Import Erasure.
Require Import InversionClassification.
Require Import LittleFacts.
Require Import ResourcesReconfiguration.
Require Import Sigma.
Require Import ValueLists.
-------------------------------------------------------------------------
Subject reduction for writing to a reference.
Lemma reference_write:
forall R1 m1 limit,
jsto R1 (
Store limit m1) ->
forall R1a R1b,
star R1a R1b R1 ->
forall l v1,
m1 l =
Some v1 ->
forall v2 w,
forall T1 T2,
jv R1a nil nil (
VPhyPair (
VLoc l w)
v2) (
TyPhyPair (
TyRef T1)
T2) ->
exists R2a R2b R2,
jt R2a nil nil (
TVal (
VLoc l v2)) (
TyRef T2) /\
jsto R2 (
Store limit (
extend m1 l v2)) /\
rio R1b R2b /\
star R2a R2b R2.
Proof.
unfold jsto.
introv [ ? ? ]
hstar hm1l hjv.
classify_and_invert.
Exhibit appropriate witnesses.
exists
R2a :=
(
update_reference R1a l (
erase_value v2))
R2b :=
R1b
R2 :=
(
update_reference R1 l (
erase_value v2)).
splits.
Sub-goal 1: check that the new reference is well-typed.
econstructor.
econstructor;
eauto 3
with resources update_reference.
Sub-goal 2: check that the new store is well-typed.
simpl.
intuition eauto with update_reference.
rewrite transform_extend.
unfold extend,
patch.
by_cases.
subst;
symmetry;
eauto with update_reference.
eauto with update_reference.
Sub-goal 3.
eapply rio_reflexive.
Sub-goal 4.
eauto with resources update_reference.
Qed.
-------------------------------------------------------------------------
Subject reduction for writing to a reference that is controlled by a
capability.
Lemma controlled_reference_write:
forall R1 m1 limit,
jsto R1 (
Store limit m1) ->
forall R1a R1b,
star R1a R1b R1 ->
forall l v1,
m1 l =
Some v1 ->
forall v'1
v2 w,
forall sigma T1 T2,
jv R1a nil nil (
VMixPair (
VPhyPair (
VInhabitant v'1)
v2) (
VRegionCap (
VCons (
VLoc l w)
VNil)))
(
TyMixPair (
TyPhyPair (
TyAt sigma)
T2) (
TyRegionCap Singleton sigma (
TyRef T1))) ->
exists R2a R2b R2,
jt R2a nil nil (
TVal (
VMixPair VPhyUnit (
VRegionCap (
VCons (
VLoc l v2)
VNil))))
(
TyMixPair TyPhyUnit (
TyRegionCap Singleton sigma (
TyRef T2))) /\
jsto R2 (
Store limit (
extend m1 l v2)) /\
rio R1b R2b /\
star R2a R2b R2.
Proof.
intros.
jv_inversion.
jv_inversion.
match goal with h:
jv _ nil nil (
VPhyPair _ _)
_ |-
_ =>
generalize h;
clear h;
intro h end.
jv_inversion.
pair_inhabitant.
Reconfigure the resource tree.
match goal with
h1:
jv ?
Rl _ _ (
VLoc _ _)
_,
h2:
jv ?
Rv2 _ _ v2 _,
h3:
permission_map ?
Rsigma _ =
Some _
|-
_ =>
reconfigure R1 (
Node (
Node (
Leaf Rl) (
Leaf Rv2)) (
Node (
Leaf Rsigma) (
Leaf R1b)))
end.
Apply the previous result.
forwards:
reference_write.
eassumption.
eassumption.
eassumption.
econstructor;
eauto.
unpack.
inversion_tval.
The resource that combines Rsigma and R1b has evolved along rio,
so each of Rsigma and R1b has evolved along rio as well.
rio_star.
forwards:
rio_owned_region.
eassumption.
eassumption.
eauto with resources.
Reconfigure again, and exhibit (two of) the witnesses.
match goal with
h1:
jv ?
Rl _ _ (
VLoc _ _)
_,
h2:
permission_map ?
Rsigma _ =
Some _,
h3:
rio R1b ?
R2b,
h4:
jsto ?
R2 _
|-
_ =>
reconfigure R2 (
Node (
Node (
Leaf Rsigma) (
Leaf Rl)) (
Leaf R2b));
eexists;
exists R2b R2
end.
Check that the goal holds.
intuition (
try eassumption).
econstructor.
eapply JVPairDupLeft.
eauto.
eapply JVRegionCap_flexible_singleton;
eauto with resources.
Qed.