Module ResourcesContinued

Set Implicit Arguments.
Require Import MyTactics.
Require Import Resources.
Require Import RawPrograms.
Require Import Types.
Require Import Store.

This definition is required for option raw_value to be an instance of the type class STAR. It can otherwise be ignored.

Instance inhabited_raw_value : Inhabited raw_value := { inhabitant := RawVUnit }.

-------------------------------------------------------------------------

Here is the structure of our resources. A resource is a pair of a region resource and a reference resource. A region resource is a map of regions to monotonic sets of raw values. (Recall that a monotonic set includes a permission flag and a predicate over raw values.) A reference resource is a map of locations to optional raw values, where the option is used to encode ownership. A reference resource can be viewed as a store fragment.

Both region resources and reference resources refer to raw values, as opposed to values, because we wish to support value reduction within regions (resp. within references) and pretend that value reduction does not alter the set of inhabitants of a region (resp. the content of a reference). This is required in order to prove that capabilities for regions (resp. the reference type) are covariant.

Definition region_resource :=
  aMap (mSet raw_value).

Definition reference_resource :=
  aMap (option raw_value).

Definition resource :=
  (region_resource * reference_resource)%type.

-------------------------------------------------------------------------

Accessors.

Definition reglimit (R : resource) : nat :=
  let (Rreg, _) := R in
  alimit Rreg.

Definition region_map (R : resource) (r : region) : raw_value -> Prop :=
  let (Rreg, _) := R in
  mset (amap Rreg r).

Definition permission_map (R : resource) (r : region) : option unit :=
  let (Rreg, _) := R in
  owned (amap Rreg r).

Definition reflimit (R : resource) : nat :=
  let (_, Rref) := R in
  alimit Rref.

Definition location_map (R : resource) (l : location) : option raw_value :=
  let (_, Rref) := R in
  amap Rref l.

-------------------------------------------------------------------------

We seem to need a special case of the relation rxo, where the store is unchanged. This relation is baptised fictitious, as it describes changes to the current resource that have no runtime effect.

Definition fictitious (R1 R2 : resource) :=
  let (Rreg1, Rref1) := R1 in
  let (Rreg2, Rref2) := R2 in
  rxo Rreg1 Rreg2 /\ Rref1 = Rref2.

-------------------------------------------------------------------------

A deconstruction tactic.

Ltac dr :=
  intros;
  repeat match goal with
  | R: resource |- _ => destruct R; dr
  | h: @star resource _ _ _ _ |- _ => destruct h as [ ? ? ]; dr
  | h: @rxo resource _ _ _ |- _ => destruct h as [ ? ? ]; dr
  | h: fictitious _ _ |- _ => destruct h as [ ? ? ]; dr
  | h: @rio resource _ _ _ |- _ => destruct h as [ ? ? ]; dr
  end;
  try subst.

-------------------------------------------------------------------------

Properties of fictitious.

Lemma fictitious_rxo:
  forall R1 R2,
  fictitious R1 R2 ->
  rxo R1 R2.
Proof.
  dr. econstructor; eauto using (@rxo_reflexive reference_resource).
Qed.

Lemma fictitious_star:
  forall R1a R1b R1 R2a,
  star R1a R1b R1 ->
  fictitious R1a R2a ->
  exists R2b R2,
  star R2a R2b R2 /\ rio R1b R2b /\ fictitious R1 R2.
Proof.
  intros [ RA1a RB1a ] [ RA1b RB1b ] [ RA1 RB1 ] [ RA2a RB2a ] [ hsa hsb ] [ hra hrb ]. subst.
  forwards [ RA2b [ RA2 [ ? [ ? ? ]]]]: (@rxo_star region_resource). eexact hsa. eexact hra.
  exists (RA2b, RB1b) (RA2, RB1).
  intuition (econstructor; eauto).
  eapply rio_reflexive.
Qed.

-------------------------------------------------------------------------

Symmetric versions of rxo_star and fictitious_star.

Lemma rxo_star_symmetric:
  forall (R1a R1b R1 R2a : resource),
  star R1b R1a R1 ->
  rxo R1a R2a ->
  exists R2b R2,
  star R2b R2a R2 /\ rio R1b R2b /\ rxo R1 R2.
Proof.
  intros. forwards: (@rxo_star resource). apply star_commutative. eassumption. eassumption. unpack.
  intuition eauto 7 using (@star_commutative resource).
Qed.

Lemma fictitious_star_symmetric:
  forall R1a R1b R1 R2a,
  star R1b R1a R1 ->
  fictitious R1a R2a ->
  exists R2b R2,
  star R2b R2a R2 /\ rio R1b R2b /\ fictitious R1 R2.
Proof.
  intros. forwards: fictitious_star. apply star_commutative. eassumption. eassumption. unpack.
  intuition eauto 7 using (@star_commutative resource).
Qed.

A tactic that applies one of the four rxo_star lemmas.

Ltac rxo_star :=
  match goal with
  | h1: star ?R1a ?R1b ?R1, h2: fictitious ?R1a ?R2a |- _ =>
      unpack (fictitious_star _ _ _ _ h1 h2)
  | h1: star ?R1a ?R1b ?R1, h2: rxo ?R1a ?R2a |- _ =>
      unpack (rxo_star h1 h2)
  | h1: star ?R1b ?R1a ?R1, h2: fictitious ?R1a ?R2a |- _ =>
      unpack (fictitious_star_symmetric _ _ _ _ h1 h2)
  | h1: star ?R1b ?R1a ?R1, h2: rxo ?R1a ?R2a |- _ =>
      unpack (rxo_star_symmetric h1 h2)
  end.

-------------------------------------------------------------------------

Consequences of the definitions.

Ltac specr :=
  repeat match goal with
  | h1: ?r < ?limit, h2: forall r, r < ?limit -> _ |- _ =>
      specializes h2 h1; unpack
  | r: region, h: forall r, _ |- _ =>
      specializes h r; unpack
  end.

Ltac resource_crunch :=
  intros;
  unfold star, rxo, rio, neutral in *;
  dr;
  simpl in *;
  unpack;
  subst;
  specr;
  try congruence;
  eauto with option_star_inversion.

Lemma reglimit_neutral:
  forall R1 R2 r,
  r < reglimit R1 ->
  neutral R1 = neutral R2 ->
  r < reglimit R2.
Proof.
  resource_crunch.
Qed.

Lemma reglimit_neutral_simplify:
  forall R r,
  r < reglimit R ->
  r < reglimit (neutral R).
Proof.
  resource_crunch.
Qed.

Lemma region_map_neutral_1:
  forall R r v,
  region_map (neutral R) r v ->
  region_map R r v.
Proof.
  resource_crunch.
Qed.

Lemma region_map_neutral_2:
  forall R r v,
  region_map R r v ->
  region_map (neutral R) r v.
Proof.
  resource_crunch.
Qed.

Lemma region_map_neutral:
  forall R1 R2 r v,
  region_map R1 r v ->
  neutral R1 = neutral R2 ->
  region_map R2 r v.
Proof.
  introv ? h. eapply region_map_neutral_1. rewrite <- h. eapply region_map_neutral_2. eassumption.
Qed.

Lemma reflimit_neutral:
  forall R1 R2 l,
  l < reflimit R1 ->
  neutral R1 = neutral R2 ->
  l < reflimit R2.
Proof.
  resource_crunch.
Qed.

Lemma star_owned_left:
  forall R1 R2 R r,
  star R1 R2 R ->
  permission_map R1 r = Some tt ->
  permission_map R r = Some tt.
Proof.
  resource_crunch.
Qed.

Lemma star_owned_exclusive:
  forall R1 R2 R r,
  star R1 R2 R ->
  permission_map R2 r = Some tt ->
  permission_map R1 r = (@None _).
Proof.
  resource_crunch.
Qed.

Lemma star_owned_left_locations:
  forall R1 R2 R l v,
  star R1 R2 R ->
  location_map R1 l = Some v ->
  location_map R l = Some v.
Proof.
  resource_crunch.
Qed.

Lemma star_owned_right_locations:
  forall R1 R2 R l v,
  star R1 R2 R ->
  location_map R2 l = Some v ->
  location_map R l = Some v.
Proof.
  resource_crunch.
Qed.

Implicit Arguments star_owned_left_locations [ R1 R2 R l v ].
Implicit Arguments star_owned_right_locations [ R1 R2 R l v ].

Ltac star_owned_locations :=
  repeat match goal with
  | h1: star ?R1 _ _, h2: location_map ?R1 ?l = Some _ |- _ =>
      generalize (star_owned_left_locations h1 h2); clear h2; intro
  | h1: star _ ?R1 _, h2: location_map ?R1 ?l = Some _ |- _ =>
      generalize (star_owned_right_locations h1 h2); clear h2; intro
  end.

Lemma star_owned_exclusive_locations:
  forall R1 R2 R r v,
  star R1 R2 R ->
  location_map R2 r = Some v ->
  location_map R1 r = (@None _).
Proof.
  resource_crunch.
Qed.

Lemma star_owned_exclusive_locations_symmetric:
  forall R1 R2 R r v,
  star R1 R2 R ->
  location_map R1 r = Some v ->
  location_map R2 r = (@None _).
Proof.
  intros. eapply star_owned_exclusive_locations. eapply star_commutative; eassumption. eassumption.
Qed.

Lemma reglimit_fictitious:
  forall R1 R2 r,
  fictitious R1 R2 ->
  r < reglimit R1 ->
  r < reglimit R2.
Proof.
  resource_crunch.
Qed.

Lemma region_map_fictitious:
  forall R1 R2 r rv,
  fictitious R1 R2 ->
  r < reglimit R1 ->
  region_map R1 r rv ->
  region_map R2 r rv.
Proof.
  resource_crunch.
Qed.

Lemma reglimit_rio:
  forall R1 R2,
  rio R1 R2 ->
  forall r,
  r < reglimit R1 ->
  r < reglimit R2.
Proof.
  resource_crunch.
Qed.

Lemma region_map_rio:
  forall R1 R2,
  rio R1 R2 ->
  forall r rv,
  r < reglimit R1 ->
  region_map R1 r rv ->
  region_map R2 r rv.
Proof.
  resource_crunch.
Qed.

Lemma region_map_rio_reverse:
  forall R1 R2 r v,
  permission_map R1 r = Some tt ->
  rio R1 R2 ->
  region_map R2 r v ->
  r < reglimit R1 ->
  region_map R1 r v.
Proof.
  resource_crunch.
Qed.

Lemma rio_owned_region:
  forall R1 R2 r,
  permission_map R1 r = Some tt ->
  rio R1 R2 ->
  r < reglimit R1 ->
  permission_map R2 r = Some tt.
Proof.
  resource_crunch.
Qed.

Lemma reflimit_rio:
  forall R1 R2,
  rio R1 R2 ->
  forall l,
  l < reflimit R1 ->
  l < reflimit R2.
Proof.
  resource_crunch.
Qed.

Lemma location_map_rio:
  forall R1 R2 l rv1 rv2,
  location_map R1 l = Some rv1 ->
  rv1 = rv2 ->
  rio R1 R2 ->
  l < reflimit R1 ->
  location_map R2 l = Some rv2.
Proof.
  resource_crunch.
Qed.

Lemma reflimit_reflimit_neutral:
  forall R1 R2 R,
  star R1 R2 R ->
  reflimit R = reflimit (neutral R1).
Proof.
  resource_crunch.
Qed.

Lemma duplicable_own_location:
  forall R l rv,
  duplicable R ->
  location_map R l = Some rv ->
  False.
Proof.
  resource_crunch.
  match goal with h1: forall l, option_star _ _ _,
                  h2: amap _ ?l = Some _ |- _ =>
    specializes h1 l;
    rewrite h2 in h1;
    inversion h1
  end.
Qed.

Lemma duplicable_own_region:
  forall R r,
  duplicable R ->
  permission_map R r = Some tt ->
  False.
Proof.
  resource_crunch.
  match goal with h1: option_star ?o ?o ?o,
                  h2: ?o = Some tt |- _ =>
    rewrite h2 in h1;
    inversion h1
  end.
Qed.

Hint Resolve (@star_neutral_map resource) (@rio_neutral resource)
reglimit_neutral reglimit_neutral_simplify region_map_neutral reflimit_neutral
star_owned_left star_owned_exclusive star_owned_exclusive_locations
star_owned_exclusive_locations_symmetric star_owned_left_locations
star_owned_right_locations reglimit_fictitious region_map_fictitious
reglimit_rio region_map_rio region_map_rio_reverse rio_owned_region
reflimit_rio location_map_rio reflimit_reflimit_neutral : resources.

-------------------------------------------------------------------------

Singleton region allocation.

Definition allocate_singleton (R : resource) (rv : raw_value) : resource :=
  let (Rreg, Rref) := R in
  (allocate Rreg (singleton_mset rv), Rref).

Lemma rxo_allocate_singleton:
  forall R rv,
  fictitious R (allocate_singleton R rv).
Proof.
  dr. split. eapply allocate_rxo. eauto.
Qed.

Lemma reglimit_allocate_singleton:
  forall R rv,
  reglimit R < reglimit (allocate_singleton R rv).
Proof.
  dr. eauto.
Qed.

Ltac bc :=
  simpl in *; by_cases; simpl in *; eauto.

Lemma region_map_allocate_singleton:
  forall R rv1 rv2,
  rv1 = rv2 ->
  region_map (allocate_singleton R rv1) (reglimit R) rv2.
Proof.
  dr. bc.
Qed.

Lemma region_map_allocate_singleton_uniqueness:
  forall R rv1 rv2,
  region_map (allocate_singleton R rv1) (reglimit R) rv2 ->
  rv1 = rv2.
Proof.
  dr. bc.
Qed.

Hint Resolve rxo_allocate_singleton reglimit_allocate_singleton
region_map_allocate_singleton region_map_allocate_singleton_uniqueness
: allocate_singleton.

We now explain how to split allocate_singleton R rv in two parts in order to apply the typing rule JVRegionCap. The component R1 represents the ownership of the new region only, while the component R2 represents the ownership of everything else.

Definition allocate_singleton_R1 (R : resource) (rv : raw_value) : resource :=
  let (Rreg, Rref) := R in
  (allocate (neutral Rreg) (singleton_mset rv), neutral Rref).

Definition allocate_singleton_R2 (R : resource) (rv : raw_value) : resource :=
  let (Rreg, Rref) := R in
  (allocate Rreg (neutral (singleton_mset rv)), Rref).

Lemma permission_map_allocate_singleton:
  forall R rv,
  permission_map (allocate_singleton_R1 R rv) (reglimit R) = Some tt.
Proof.
  dr. bc.
Qed.

Lemma star_allocate_singleton:
  forall R v,
  star
    (allocate_singleton_R1 R v)
    (allocate_singleton_R2 R v)
    (allocate_singleton R v).
Proof.
  dr.
  econstructor.
    eapply star_allocate. eapply star_commutative. eapply star_neutral. eapply star_neutral.
    eapply star_commutative. eapply star_neutral.
Qed.

Lemma rio_allocate_singleton:
  forall R v,
  rio R (allocate_singleton_R2 R v).
Proof.
  dr.
  econstructor.
    eapply allocate_rio.
    eapply rio_reflexive.
Qed.

Hint Resolve permission_map_allocate_singleton star_allocate_singleton
rio_allocate_singleton : allocate_singleton.

-------------------------------------------------------------------------

Group region allocation. Group regions are created empty.

Definition allocate_group (R : resource) : resource :=
  let (Rreg, Rref) := R in
  (allocate Rreg (@empty_mset raw_value), Rref).

Lemma rxo_allocate_group:
  forall R,
  fictitious R (allocate_group R).
Proof.
  dr. split. eapply allocate_rxo. eauto.
Qed.

Lemma reglimit_allocate_group:
  forall R,
  reglimit R < reglimit (allocate_group R).
Proof.
  dr. eauto.
Qed.

Lemma empty_allocate_group:
  forall R rv,
  region_map (allocate_group R) (reglimit R) rv ->
  False.
Proof.
  dr. bc.
Qed.

Lemma permission_map_allocate_group:
  forall R,
  permission_map (allocate_group R) (reglimit R) = Some tt.
Proof.
  dr. bc.
Qed.

Hint Resolve rxo_allocate_group reglimit_allocate_group
empty_allocate_group permission_map_allocate_group : allocate_group.

-------------------------------------------------------------------------

Group region extension, also known as adoption.

Definition extend_group (R : resource) (rv : raw_value) (r : region) : resource :=
  let (Rreg, Rref) := R in
  (update Rreg r (extend_mset (amap Rreg r) rv), Rref).

Lemma reglimit_extend_group:
  forall R rv r1 r2,
  r1 < reglimit R ->
  r1 < reglimit (extend_group R rv r2).
Proof.
  dr. eauto.
Qed.

Lemma star_extend_group:
  forall R1 R2 R rv r,
  star R1 R2 R ->
  star (extend_group R1 rv r) (extend_group R2 rv r) (extend_group R rv r).
Proof.
  dr.
  econstructor; eauto.
  eapply star_update; eauto.
  eapply star_extend_mset.
  eapply star_amap; eauto.
Qed.

Lemma rxo_extend_group:
  forall R rv r,
  permission_map R r = Some tt ->
  fictitious R (extend_group R rv r).
Proof.
  dr. split. eapply rxo_update. eauto using rxo_extend_mset. eauto.
Qed.

Lemma rio_extend_group:
  forall R rv r,
  permission_map R r = (@None _) ->
  rio R (extend_group R rv r).
Proof.
  dr.
  econstructor.
  eapply rio_update; eauto.
  eapply rio_extend_mset; eauto.
  eapply rio_reflexive.
Qed.

Lemma region_map_extend_group_1:
  forall R rv r,
  region_map (extend_group R rv r) r rv.
Proof.
  dr. bc.
Qed.

Lemma region_map_extend_group_2:
  forall R rv r rw,
  region_map R r rw ->
  region_map (extend_group R rv r) r rw.
Proof.
  dr. bc.
Qed.

Lemma region_map_extend_group_reverse:
  forall R rv1 rv2 r,
  region_map (extend_group R rv1 r) r rv2 ->
  rv2 = rv1 \/ region_map R r rv2.
Proof.
  dr. bc.
Qed.

Lemma permission_map_extend_group:
  forall R rv r,
  permission_map R r = Some tt ->
  permission_map (extend_group R rv r) r = Some tt.
Proof.
  dr. bc.
Qed.

Hint Resolve reglimit_extend_group star_extend_group rxo_extend_group
rio_extend_group region_map_extend_group_1 region_map_extend_group_2
permission_map_extend_group : extend_group.

-------------------------------------------------------------------------

Reference allocation.

Definition allocate_reference (R : resource) (rv : raw_value) : resource :=
  let (Rreg, Rref) := R in
  (Rreg, allocate Rref (Some rv)).

Definition allocate_reference_unowned (R : resource) : resource :=
  let (Rreg, Rref) := R in
  (Rreg, allocate Rref None).

Lemma star_allocate_reference_2:
  forall R1 R2 R rv,
  star R1 R2 R ->
  star
    (allocate_reference R1 rv)
    (allocate_reference_unowned R2)
    (allocate_reference R rv).
Proof.
  dr.
  econstructor; eauto.
  eapply star_allocate; eauto. econstructor.
Qed.

Lemma star_allocate_reference_1:
  forall R rv,
  star
    (allocate_reference (neutral R) rv)
    (allocate_reference_unowned R)
    (allocate_reference R rv).
Proof.
  intros. eapply star_allocate_reference_2. eapply star_commutative; eapply star_neutral.
Qed.

Lemma rxo_allocate_reference:
  forall R rv,
  rxo R (allocate_reference R rv).
Proof.
  dr.
  econstructor. eapply rxo_reflexive. eapply allocate_rxo.
Qed.

Lemma rio_allocate_reference_unowned:
  forall R,
  rio R (allocate_reference_unowned R).
Proof.
  dr.
  econstructor. eapply rio_reflexive. eapply allocate_rio.
Qed.

Lemma reflimit_allocate_reference_1:
  forall R rv,
  S (reflimit R) = reflimit (allocate_reference R rv).
Proof.
  dr. eauto.
Qed.

Lemma reflimit_allocate_reference_2:
  forall R l rv,
  (forall l', l' < l -> l' < reflimit R) ->
  l < reflimit (allocate_reference R rv).
Proof.
  introv h.
  assert (l <= reflimit R). destruct l. omega. specializes h l. omega.
  dr. simpl in *. omega.
Qed.

Lemma location_map_allocate_reference_1:
  forall R l rv,
  l = reflimit R ->
  location_map (allocate_reference R rv) l = Some rv.
Proof.
  dr. bc.
Qed.

Lemma location_map_allocate_reference_2:
  forall R l orv1 rv2,
  l < reflimit R ->
  orv1 = location_map R l ->
  orv1 = location_map (allocate_reference R rv2) l.
Proof.
  dr. bc.
Qed.

Hint Resolve star_allocate_reference_1 star_allocate_reference_2
rio_allocate_reference_unowned rxo_allocate_reference
reflimit_allocate_reference_1 reflimit_allocate_reference_2
location_map_allocate_reference_1 location_map_allocate_reference_2 :
allocate_reference.

-------------------------------------------------------------------------

Reference update.

Definition update_reference (R : resource) (l : location) (rv : raw_value) : resource :=
  let (Rreg, Rref) := R in
  (Rreg, update Rref l (Some rv)).

Lemma star_update_reference_preliminary:
  forall R1 R2 R l rv,
  star R1 R2 R ->
  location_map R2 l = None ->
  star (update_reference R1 l rv) R2 (update_reference R l rv).
Proof.
  dr.
  econstructor; eauto.
  eapply star_update_owned; eauto.
Qed.

Lemma star_update_reference:
  forall R1 R2 R l rv1 rv2,
  star R1 R2 R ->
  location_map R1 l = Some rv1 ->
  star (update_reference R1 l rv2) R2 (update_reference R l rv2).
Proof.
  intros. eapply star_update_reference_preliminary; eauto with resources.
Qed.

Lemma reflimit_update_reference_1:
  forall R l rv,
  reflimit R = reflimit (update_reference R l rv).
Proof.
  dr. eauto.
Qed.

Lemma reflimit_update_reference_2:
  forall R l1 l2 rv,
  l1 < reflimit R ->
  l1 < reflimit (update_reference R l2 rv).
Proof.
  intros. rewrite <- reflimit_update_reference_1. eauto.
Qed.

Lemma location_map_update_reference_1:
  forall R l rv,
  location_map (update_reference R l rv) l = Some rv.
Proof.
  dr. unfold update_reference. intros. eapply amap_update.
Qed.

Lemma location_map_update_reference_2:
  forall R l1 l2 orv1 rv2,
  orv1 = location_map R l1 ->
  l1 <> l2 ->
  orv1 = location_map (update_reference R l2 rv2) l1.
Proof.
  dr. bc.
Qed.

Hint Resolve star_update_reference reflimit_update_reference_1
reflimit_update_reference_2 location_map_update_reference_1
location_map_update_reference_2 : update_reference.

-------------------------------------------------------------------------

Make some definitions opaque, otherwise simpl expands them and chaos ensues.

Global Opaque star rxo rio fictitious neutral void.

-------------------------------------------------------------------------

This tactic exploits all star hypotheses to establish an equality of the form neutral R1 = neutral R2. It is very useful in conjunction with some of the above lemmas, such as reglimit_neutral, which generate such equalities as proof obligations.

Ltac neutral_eq :=
  repeat match goal with h: star _ _ _ |- _ =>
    generalize (compatible_implies_common_core _ _ _ h);
    generalize (compatible_implies_common_core _ _ _ (star_commutative _ _ _ h));
    clear h; intros
  end; congruence.

Hint Extern 1 (neutral _ = neutral _) => neutral_eq : resources.

Generated by coq2html