Library Heaps

Require Import HahnBase.
Require Import List.
Require Import Permissions.
Require Import PermSolver.
Require Import Permutation.
Require Import PermutationTactic.
Require Import Prelude.
Require Import Process.
Require Import QArith.
Require Import Qcanon.
Require Import Setoid.
Require Import Utf8.

Import ListNotations.

Set Implicit Arguments.

Heaps


Module Type Heaps(dom : Domains).
  Export dom.

Ordinary heaps


Definition Heap := Val -> option Val.

The identity heap is empty at every location:

Definition hIden : Heap := fun _ => None.

Update operation for heaps:

Definition hUpdate (h : Heap)(l : Val)(v : option Val) :=
  update val_eq_dec h l v.

Finiteness

A heap is finite if all mappings that are not free can be mapped to some finite structure, in this case a list.

Definition hFinite (h : Heap) : Prop :=
  exists xs : list Val, forall l, h l <> None -> In l xs.

Lemma hFinite_iden : hFinite hIden.

The most important property of finite heaps is that one can always find a free entry, as shown below.

Lemma hFinite_free :
  forall h, hFinite h -> exists l, h l = None.

Any heap update preserves finiteness.

Lemma hFinite_update :
  forall h l v,
  hFinite h -> hFinite (hUpdate h l v).

Permission heaps cells

The set PermHeapCell of permission heap cells is later used as the codomain of permission heaps.
Permission heap cells can be free, invalid or occupied. There are three kinds of occupied heap cells, which correspond to the three different heap ownership predicates in the logic.
Notice that action heap cells hold an extra value, which is a copy of the value at that heap location, made at the moment the action heap cell was created.

Inductive PermHeapCell :=
  | PHCfree
  | PHCstd(q : Qc)(v : Val)
  | PHCproc(q : Qc)(v : Val)
  | PHCact(q : Qc)(v v' : Val)
  | PHCinvalid.

Add Search Blacklist "PermHeapCell_rect".
Add Search Blacklist "PermHeapCell_ind".
Add Search Blacklist "PermHeapCell_rec".
Add Search Blacklist "PermHeapCell_sind".

Validity

Any permission heap cell phc is valid if phc is not (explicitly) invalid, and any underlying fractional permission is valid.

Definition phcValid (phc : PermHeapCell) : Prop :=
  match phc with
    | PHCfree => True
    | PHCstd q _
    | PHCproc q _
    | PHCact q _ _ => perm_valid q
    | PHCinvalid => False
  end.

Notation "√ phc" :=
  (phcValid phc)
  (only printing, at level 80).

Free cells are always valid, whereas invalid cells are never valid.

Lemma phcValid_free : phcValid PHCfree.

Lemma phcValid_contra :
  forall phc, phcValid phc -> phc <> PHCinvalid.

Hint Resolve phcValid_free phcValid_contra : core.

Disjointness

Any two permission heap cells are said to be disjoint if their underlying fractional permissions are disjoint, an all other components are equal apart from that.
Invalid heap cells are never disjoint with any other heap cell, while free heap cells are disjoint with other valid heap cells.

Definition phcDisj (phc1 phc2 : PermHeapCell) : Prop :=
  match phc1, phc2 with
    | PHCinvalid, _
    | _, PHCinvalid => False
    | PHCfree, PHCfree => True
    | PHCfree, phc
    | phc, PHCfree => phcValid phc
    | PHCstd q1 v1, PHCstd q2 v2 =>
        perm_disj q1 q2 /\ v1 = v2
    | PHCstd _ _, _
    | _, PHCstd _ _ => False
    | PHCproc q1 v1, PHCproc q2 v2 =>
        perm_disj q1 q2 /\ v1 = v2
    | PHCproc _ _, _
    | _, PHCproc _ _ => False
    | PHCact q1 v1 v1', PHCact q2 v2 v2' =>
        perm_disj q1 q2 /\ v1 = v2 /\ v1' = v2'
  end.

Notation "phc1 ⟂ phc2" :=
  (phcDisj phc1 phc2)
  (only printing, at level 80).

Heap cell disjointness is a symmetric relation

Global Instance phcDisj_symm : Symmetric phcDisj.

Below are the identity laws for disjointness:

Lemma phcDisj_free_l :
  forall phc, phcValid phc -> phcDisj phc PHCfree.
Lemma phcDisj_free_r :
  forall phc, phcValid phc -> phcDisj PHCfree phc.

Hint Resolve phcDisj_free_l phcDisj_free_r : core.

Below are some other useful properties of disjointness.

Lemma phcDisj_valid_l :
  forall phc1 phc2, phcDisj phc1 phc2 -> phcValid phc1.
Lemma phcDisj_valid_r :
  forall phc1 phc2, phcDisj phc1 phc2 -> phcValid phc2.
Lemma phcDisj_valid :
  forall phc1 phc2,
  phcDisj phc1 phc2 -> phcValid phc1 /\ phcValid phc2.

Union

The (disjoint) union of two permission heap cells is defined as the addition of their underlying fractional permissions.
PHCfree heap cells are neutral with respect to disjoint union, while PHCinvalid are absorbing.

Lemma val_pair_eq_dec :
  forall x y : Val * Val, {x = y} + {x <> y}.

Definition phcUnion (phc1 phc2 : PermHeapCell) : PermHeapCell :=
  match phc1, phc2 with
    | PHCinvalid, _
    | _, PHCinvalid => PHCinvalid
    | PHCfree, phc
    | phc, PHCfree => phc
    | PHCstd q1 v1, PHCstd q2 v2 =>
        if val_eq_dec v1 v2
        then PHCstd (q1 + q2) v1
        else PHCinvalid
    | PHCstd _ _, _
    | _, PHCstd _ _ => PHCinvalid
    | PHCproc q1 v1, PHCproc q2 v2 =>
        if val_eq_dec v1 v2
        then PHCproc (q1 + q2) v1
        else PHCinvalid
    | PHCproc _ _, _
    | _, PHCproc _ _ => PHCinvalid
    | PHCact q1 v1 v1', PHCact q2 v2 v2' =>
        if val_pair_eq_dec (v1, v1') (v2, v2')
        then PHCact (q1 + q2) v1 v1'
        else PHCinvalid
  end.

Notation "phc1 ⨄ phc2" :=
  (phcUnion phc1 phc2)
  (only printing, at level 80, right associativity).

The phcUnion relation is associative and commutative.

Lemma phcUnion_assoc :
  forall phc1 phc2 phc3,
  phcUnion phc1 (phcUnion phc2 phc3) =
  phcUnion (phcUnion phc1 phc2) phc3.

Lemma phcUnion_comm :
  forall phc1 phc2,
  phcUnion phc1 phc2 = phcUnion phc2 phc1.

Hint Resolve phcUnion_assoc phcUnion_comm : core.

The following lemmas show that PHCfree is neutral for union.

Lemma phcUnion_free_l :
  forall phc, phcUnion phc PHCfree = phc.
Lemma phcUnion_free_r :
  forall phc, phcUnion PHCfree phc = phc.

Hint Rewrite phcUnion_free_l phcUnion_free_r : core.

Below are various other useful properties of heap cell union.

Lemma phcUnion_valid :
  forall phc1 phc2,
  phcDisj phc1 phc2 -> phcValid (phcUnion phc1 phc2).

Lemma phcDisj_union_l :
  forall phc1 phc2 phc3,
  phcDisj phc1 phc2 ->
  phcDisj (phcUnion phc1 phc2) phc3 ->
  phcDisj phc2 phc3.
Lemma phcDisj_union_r :
  forall phc1 phc2 phc3,
  phcDisj phc2 phc3 ->
  phcDisj phc1 (phcUnion phc2 phc3) ->
  phcDisj phc1 phc2.

Lemma phcDisj_assoc_l :
  forall phc1 phc2 phc3,
  phcDisj phc1 phc2 ->
  phcDisj (phcUnion phc1 phc2) phc3 ->
  phcDisj phc1 (phcUnion phc2 phc3).
Lemma phcDisj_assoc_r :
  forall phc1 phc2 phc3,
  phcDisj phc2 phc3 ->
  phcDisj phc1 (phcUnion phc2 phc3) ->
  phcDisj (phcUnion phc1 phc2) phc3.

Lemma phcDisj_middle :
  forall phc1 phc2 phc3 phc4,
  phcDisj phc1 phc2 ->
  phcDisj phc3 phc4 ->
  phcDisj (phcUnion phc1 phc2) (phcUnion phc3 phc4) ->
  phcDisj phc2 phc3.

Lemma phcDisj_compat :
  forall phc1 phc2 phc3 phc4,
  phcDisj phc1 phc3 ->
  phcDisj phc2 phc4 ->
  phcDisj (phcUnion phc1 phc3) (phcUnion phc2 phc4) ->
  phcDisj (phcUnion phc1 phc2) (phcUnion phc3 phc4).

Lemma phcUnion_swap_l :
  forall phc1 phc2 phc3,
  phcUnion phc1 (phcUnion phc2 phc3) =
  phcUnion phc2 (phcUnion phc1 phc3).
Lemma phcUnion_swap_r :
  forall phc1 phc2 phc3,
  phcUnion (phcUnion phc1 phc2) phc3 =
  phcUnion (phcUnion phc1 phc3) phc2.

Lemma phcUnion_compat :
  forall phc1 phc2 phc3 phc4,
  phcUnion (phcUnion phc1 phc3) (phcUnion phc2 phc4) =
  phcUnion (phcUnion phc1 phc2) (phcUnion phc3 phc4).

Lemma phcUnion_free :
  forall phc1 phc2,
  phcUnion phc1 phc2 = PHCfree <-> phc1 = PHCfree /\ phc2 = PHCfree.

Lemma phcUnion_not_free :
  forall phc1 phc2,
  phcUnion phc1 phc2 <> PHCfree <-> phc1 <> PHCfree \/ phc2 <> PHCfree.

Orderings

The following (strict) partial order defines the 'less than' relation on permission heap cells.

Definition phcLt (phc1 phc2 : PermHeapCell) : Prop :=
  match phc1, phc2 with
    | PHCfree, PHCfree => False
    | PHCfree, _ => True
    | PHCstd q1 v1, PHCstd q2 v2
    | PHCproc q1 v1, PHCproc q2 v2 => q1 < q2 /\ v1 = v2
    | PHCact q1 v1 v1', PHCact q2 v2 v2' => q1 < q2 /\ v1 = v2 /\ v1' = v2'
    | _, _ => False
  end.

Notation "phc1 ≺ phc2" :=
  (phcLt phc1 phc2)
  (only printing, at level 80).

The phcLt relation is a strict partial order (i.e., irreflexive, asymmetric and transitive).

Global Instance phcLt_irrefl : Irreflexive phcLt.
Global Instance phcLt_trans : Transitive phcLt.
Global Instance phcLt_asymm : Asymmetric phcLt.
Global Instance phcLt_strictorder : StrictOrder phcLt.

Below are several other useful properties of phcLt.

Lemma phcLt_mono_pos :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcLt PHCfree phc2 ->
  phcLt phc1 (phcUnion phc1 phc2).

Lemma phcLt_mono_l :
  forall phc1 phc2 phc3,
  phcDisj phc3 phc2 ->
  phcLt phc1 phc2 ->
  phcLt (phcUnion phc3 phc1) (phcUnion phc3 phc2).
Lemma phcLt_mono_r :
  forall phc1 phc2 phc3,
  phcDisj phc2 phc3 ->
  phcLt phc1 phc2 ->
  phcLt (phcUnion phc1 phc3) (phcUnion phc2 phc3).

Lemma phcLt_diff :
  forall phc1 phc2,
  phcValid phc1 ->
  phcValid phc2 ->
  phcLt phc1 phc2 ->
  exists phc3, phcDisj phc1 phc3 /\ phcUnion phc1 phc3 = phc2.

Lemma phcDisj_lt :
  forall phc1 phc2 phc3,
  phcValid phc1 ->
  phcDisj phc2 phc3 ->
  phcLt phc1 phc2 ->
  phcDisj phc1 phc3.

The following partial order defines the 'less than or equal to' relation on permission heap cells.

Definition phcLe (phc1 phc2 : PermHeapCell) : Prop :=
  match phc1, phc2 with
    | PHCfree, _ => True
    | PHCstd q1 v1, PHCstd q2 v2
    | PHCproc q1 v1, PHCproc q2 v2 => q1 <= q2 /\ v1 = v2
    | PHCact q1 v1 v1', PHCact q2 v2 v2' => q1 <= q2 /\ v1 = v2 /\ v1' = v2'
    | PHCinvalid, PHCinvalid => True
    | _, _ => False
  end.

Notation "phc1 ≼ phc2" :=
  (phcLe phc1 phc2)
  (only printing, at level 80).

The phcLe relation is a non-strict partial order.

Global Instance phcLe_refl : Reflexive phcLe.

Hint Resolve phcLe_refl : core.

Lemma phcLt_le_weak :
  forall phc1 phc2,
  phcLt phc1 phc2 -> phcLe phc1 phc2.

Lemma phcLe_lt_or_eq :
  forall phc1 phc2,
  phcLe phc1 phc2 <->
  phc1 = phc2 \/ phcLt phc1 phc2.

Global Instance phcLe_antisym :
  Antisymmetric PermHeapCell eq phcLe.
Global Instance phcLe_trans : Transitive phcLe.
Global Instance phcLe_preorder : PreOrder phcLe.
Global Instance phcLe_partialorder : PartialOrder eq phcLe.

Below are various other useful properties of phcLe.

Lemma phcLe_valid :
  forall phc, phcLe PHCfree phc.

Lemma phcLe_lt_trans :
  forall phc1 phc2 phc3,
  phcLe phc1 phc2 ->
  phcLt phc2 phc3 ->
  phcLt phc1 phc3.

Lemma phcLt_le_trans :
  forall phc1 phc2 phc3,
  phcLt phc1 phc2 ->
  phcLe phc2 phc3 ->
  phcLt phc1 phc3.

Lemma phcLt_weaken :
  forall phc1 phc2 phc3,
  phcDisj phc2 phc3 ->
  phcLt phc1 phc2 ->
  phcLt phc1 (phcUnion phc2 phc3).

Lemma phcLe_weaken :
  forall phc1 phc2 phc3,
  phcDisj phc2 phc3 ->
  phcLe phc1 phc2 ->
  phcLe phc1 (phcUnion phc2 phc3).

Lemma phcLe_mono_l :
  forall phc1 phc2 phc3,
  phcDisj phc3 phc2 ->
  phcLe phc1 phc2 ->
  phcLe (phcUnion phc3 phc1) (phcUnion phc3 phc2).
Lemma phcLe_mono_r :
  forall phc1 phc2 phc3,
  phcDisj phc2 phc3 ->
  phcLe phc1 phc2 ->
  phcLe (phcUnion phc1 phc3) (phcUnion phc2 phc3).

Lemma phcLe_mono_pos :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcLe phc1 (phcUnion phc1 phc2).

Lemma phcLe_compat :
  forall phc1 phc2 phc3 phc4,
  phcDisj phc1 phc4 ->
  phcDisj phc3 phc4 ->
  phcLe phc1 phc3 ->
  phcLe phc2 phc4 ->
  phcLe (phcUnion phc1 phc2) (phcUnion phc3 phc4).

Lemma phcLe_diff :
  forall phc1 phc2,
  phcValid phc1 ->
  phcValid phc2 ->
  phcLe phc1 phc2 ->
  exists phc3, phcDisj phc1 phc3 /\ phcUnion phc1 phc3 = phc2.

Lemma phcDisj_le :
  forall phc1 phc2 phc3,
  phcValid phc1 ->
  phcDisj phc2 phc3 ->
  phcLe phc1 phc2 ->
  phcDisj phc1 phc3.

Entirety

Any permission heap cell phc is said to be entire if phc is occupied and holds a fractional permission perm_full.

Definition phcEntire (phc : PermHeapCell) : Prop :=
  match phc with
    | PHCfree
    | PHCinvalid => False
    | PHCstd q _
    | PHCproc q _
    | PHCact q _ _ => q = perm_full
  end.

Lemma phcEntire_union_l :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcEntire phc1 ->
  phcEntire (phcUnion phc1 phc2).
Lemma phcEntire_union_r :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcEntire phc2 ->
  phcEntire (phcUnion phc1 phc2).
Lemma phcEntire_union :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcEntire phc1 \/ phcEntire phc2 ->
  phcEntire (phcUnion phc1 phc2).

Lemma phcEntire_lt_neg :
  forall phc1 phc2,
  phcValid phc2 -> phcEntire phc1 -> ~ phcLt phc1 phc2.

Lemma phcEntire_le :
  forall phc1 phc2,
  phcLe phc1 phc2 ->
  phcValid phc2 ->
  phcEntire phc1 ->
  phcEntire phc2.

Lemma phcLe_entire_eq :
  forall phc1 phc2,
  phcValid phc2 ->
  phcEntire phc1 ->
  phcLe phc1 phc2 ->
  phc1 = phc2.

Lemma phcDisj_entire_free :
  forall phc1 phc2,
  phcDisj phc1 phc2 -> phcEntire phc1 -> phc2 = PHCfree.

Lemma phcLt_entire_free :
  forall phc,
  phcEntire phc -> phcLt PHCfree phc.

Concretisation

The concretisation of any permission heap cell phc is the underlying value of phc (thus removing all structure related to the context of the heap cell).

Definition phcConcr (phc : PermHeapCell) : option Val :=
  match phc with
    | PHCfree
    | PHCinvalid => None
    | PHCstd _ v
    | PHCproc _ v
    | PHCact _ v _ => Some v
  end.

Lemma phcConcr_lt_none :
  forall phc1 phc2,
  phcLt phc1 phc2 ->
  phcConcr phc2 = None ->
  phcConcr phc1 = None.
Lemma phcConcr_le_none :
  forall phc1 phc2,
  phcLe phc1 phc2 ->
  phcConcr phc2 = None ->
  phcConcr phc1 = None.

Lemma phcConcr_lt_some :
  forall phc1 phc2 v,
  phcLt phc1 phc2 ->
  phcConcr phc1 = Some v ->
  phcConcr phc2 = Some v.
Lemma phcConcr_le_some :
  forall phc1 phc2 v,
  phcLe phc1 phc2 ->
  phcConcr phc1 = Some v ->
  phcConcr phc2 = Some v.

Lemma phcConcr_none_free :
  forall phc,
  phcValid phc -> phcConcr phc = None -> phc = PHCfree.

Lemma phcConcr_union :
  forall phc1 phc2 v,
  phcDisj phc1 phc2 ->
  phcConcr phc1 = Some v ->
  phcConcr (phcUnion phc1 phc2) = Some v.

Lemma phcConcr_compat :
  forall phc1 phc2 phc3 phc4,
  phcDisj phc1 phc2 ->
  phcDisj phc3 phc4 ->
  phcConcr phc1 = phcConcr phc3 ->
  phcConcr phc2 = phcConcr phc4 ->
  phcConcr (phcUnion phc1 phc2) = phcConcr (phcUnion phc3 phc4).

Lemma phcConcr_disj_union_l :
  forall phc1 phc2 phc3,
  phcDisj phc1 phc3 ->
  phcDisj phc2 phc3 ->
  phcConcr phc1 = phcConcr phc2 ->
  phcConcr (phcUnion phc1 phc3) = phcConcr (phcUnion phc2 phc3).
Lemma phcConcr_disj_union_r :
  forall phc1 phc2 phc3,
  phcDisj phc1 phc3 ->
  phcDisj phc2 phc3 ->
  phcConcr phc1 = phcConcr phc2 ->
  phcConcr (phcUnion phc3 phc1) = phcConcr (phcUnion phc3 phc2).

Snapshots

The following operation extracts the snapshot value out of a given permission heap cell.

Definition phcSnapshot (phc : PermHeapCell) : option Val :=
  match phc with
    | PHCfree
    | PHCinvalid
    | PHCstd _ _ => None
    | PHCproc _ v
    | PHCact _ _ v => Some v
  end.

Below are several useful properties of snapshot extraction.

Lemma phcSnapshot_compat :
  forall phc1 phc2 phc3 phc4,
  phcDisj phc1 phc2 ->
  phcDisj phc3 phc4 ->
  phcSnapshot phc1 = phcSnapshot phc3 ->
  phcSnapshot phc2 = phcSnapshot phc4 ->
  phcSnapshot (phcUnion phc1 phc2) = phcSnapshot (phcUnion phc3 phc4).

Lemma phcConcr_snapshot_compat :
  forall phc1 phc2 phc3 phc4,
  phcDisj phc1 phc2 ->
  phcDisj phc3 phc4 ->
  phcConcr phc1 = phcSnapshot phc3 ->
  phcConcr phc2 = phcSnapshot phc4 ->
  phcConcr (phcUnion phc1 phc2) = phcSnapshot (phcUnion phc3 phc4).

Lemma phcSnapshot_disj_union_l :
  forall phc1 phc2 phc3,
  phcDisj phc1 phc3 ->
  phcDisj phc2 phc3 ->
  phcSnapshot phc1 = phcSnapshot phc2 ->
  phcSnapshot (phcUnion phc1 phc3) = phcSnapshot (phcUnion phc2 phc3).
Lemma phcSnapshot_disj_union_r :
  forall phc1 phc2 phc3,
  phcDisj phc1 phc3 ->
  phcDisj phc2 phc3 ->
  phcSnapshot phc1 = phcSnapshot phc2 ->
  phcSnapshot (phcUnion phc3 phc1) = phcSnapshot (phcUnion phc3 phc2).

Lemma phcSnapshot_lt_none :
  forall phc1 phc2,
  phcLt phc1 phc2 ->
  phcSnapshot phc2 = None ->
  phcSnapshot phc1 = None.
Lemma phcSnapshot_le_none :
  forall phc1 phc2,
  phcLe phc1 phc2 ->
  phcSnapshot phc2 = None ->
  phcSnapshot phc1 = None.

Lemma phcSnapshot_lt_some :
  forall phc1 phc2 v,
  phcLt phc1 phc2 ->
  phcSnapshot phc1 = Some v ->
  phcSnapshot phc2 = Some v.
Lemma phcSnapshot_le_some :
  forall phc1 phc2 v,
  phcLe phc1 phc2 ->
  phcSnapshot phc1 = Some v ->
  phcSnapshot phc2 = Some v.

Lemma phcSnapshot_union :
  forall phc1 phc2 v,
  phcDisj phc1 phc2 ->
  phcSnapshot phc1 = Some v ->
  phcSnapshot (phcUnion phc1 phc2) = Some v.

Heap cell conversion

Below are three operations for converting the type of permission heap cells, named phcConvStd, for converting to standard heap cells; phcConvProc, for converting to process heap cells; and phcConvAct, for converting to action heap cells.

Definition phcConvStd (phc : PermHeapCell) : PermHeapCell :=
  match phc with
    | PHCfree => PHCfree
    | PHCstd q v
    | PHCproc q v
    | PHCact q v _ => PHCstd q v
    | PHCinvalid => PHCinvalid
  end.

Notation "'std' { phc }" :=
  (phcConvStd phc)
  (only printing, at level 40).

Definition phcConvProc (phc : PermHeapCell) : PermHeapCell :=
  match phc with
    | PHCfree => PHCfree
    | PHCstd q v
    | PHCproc q v
    | PHCact q v _ => PHCproc q v
    | PHCinvalid => PHCinvalid
  end.

Notation "'proc' { phc }" :=
  (phcConvProc phc)
  (only printing, at level 40).

Definition phcConvAct (phc : PermHeapCell) : PermHeapCell :=
  match phc with
    | PHCfree => PHCfree
    | PHCstd q v
    | PHCproc q v => PHCact q v v
    | PHCact q v1 v2 => PHCact q v1 v2
    | PHCinvalid => PHCinvalid
  end.

Notation "'act' { phc }" :=
  (phcConvAct phc)
  (only printing, at level 40).

Converting any heap cell to its original types does not have any effect.

Lemma phc_std_conv :
  forall q v, PHCstd q v = phcConvStd (PHCstd q v).
Lemma phc_proc_conv :
  forall q v, PHCproc q v = phcConvProc (PHCproc q v).
Lemma phc_act_conv :
  forall q v v', PHCact q v v' = phcConvAct (PHCact q v v').

Heap cell conversion is idempotent.

Lemma phcConvStd_idemp :
  forall phc, phcConvStd (phcConvStd phc) = phcConvStd phc.
Lemma phcConvProc_idemp :
  forall phc, phcConvProc (phcConvProc phc) = phcConvProc phc.
Lemma phcConvAct_idemp :
  forall phc, phcConvAct (phcConvAct phc) = phcConvAct phc.

Free heap cells always convert to free heap cells.

Lemma phcConvStd_free :
  phcConvStd PHCfree = PHCfree.
Lemma phcConvProc_free :
  phcConvProc PHCfree = PHCfree.
Lemma phcConvAct_free :
  phcConvAct PHCfree = PHCfree.
Lemma phcConvStd_free2 :
  forall phc, phcConvStd phc = PHCfree <-> phc = PHCfree.
Lemma phcConvProc_free2 :
  forall phc, phcConvProc phc = PHCfree <-> phc = PHCfree.
Lemma phcConvAct_free2 :
  forall phc, phcConvAct phc = PHCfree <-> phc = PHCfree.

Invalid heap cells always convert to invalid heap cells.

Lemma phcConvStd_invalid :
  phcConvStd PHCinvalid = PHCinvalid.
Lemma phcConvProc_invalid :
  phcConvProc PHCinvalid = PHCinvalid.
Lemma phcConvAct_invalid :
  phcConvAct PHCinvalid = PHCinvalid.
Lemma phcConvStd_invalid2 :
  forall phc, phcConvStd phc = PHCinvalid <-> phc = PHCinvalid.
Lemma phcConvProc_invalid2 :
  forall phc, phcConvProc phc = PHCinvalid <-> phc = PHCinvalid.
Lemma phcConvAct_invalid2 :
  forall phc, phcConvAct phc = PHCinvalid <-> phc = PHCinvalid.

Heap cell conversion preserves validity.

Lemma phcConvStd_valid :
  forall phc, phcValid phc <-> phcValid (phcConvStd phc).
Lemma phcConvProc_valid :
  forall phc, phcValid phc <-> phcValid (phcConvProc phc).
Lemma phcConvAct_valid :
  forall phc, phcValid phc <-> phcValid (phcConvAct phc).

Heap cell conversion preserves disjointness.

Add Parametric Morphism : phcConvStd
  with signature phcDisj ==> phcDisj as phcConvStd_disj.
Add Parametric Morphism : phcConvProc
  with signature phcDisj ==> phcDisj as phcConvProc_disj.
Add Parametric Morphism : phcConvAct
  with signature phcDisj ==> phcDisj as phcConvAct_disj.

Heap cell conversion preserves entirety.

Lemma phcConvStd_entire :
  forall phc, phcEntire (phcConvStd phc) <-> phcEntire phc.
Lemma phcConvProc_entire :
  forall phc, phcEntire (phcConvProc phc) <-> phcEntire phc.
Lemma phcConvAct_entire :
  forall phc, phcEntire (phcConvAct phc) <-> phcEntire phc.

Below are several other properties of heap cell conversion for later convenience.
Note: in the following three lemmas, the validity condition is not neccessary for the right-to-left implication.

Lemma phcLt_conv_std_disj :
  forall phc2 phc3 q v,
  phcValid phc2 ->
  phcLt (PHCstd q v) phc2 ->
  phcDisj (phcConvStd phc2) phc3 <-> phcDisj phc2 phc3.
Lemma phcLt_conv_proc_disj :
  forall phc2 phc3 q v,
  phcValid phc2 ->
  phcLt (PHCproc q v) phc2 ->
  phcDisj (phcConvProc phc2) phc3 <-> phcDisj phc2 phc3.
Lemma phcLt_conv_act_disj :
  forall phc2 phc3 q v1 v2,
  phcValid phc2 ->
  phcLt (PHCact q v1 v2) phc2 ->
  phcDisj (phcConvAct phc2) phc3 <-> phcDisj phc2 phc3.

Lemma phcLe_conv_std_disj :
  forall phc2 phc3 q v,
  phcValid phc2 ->
  phcLe (PHCstd q v) phc2 ->
  phcDisj (phcConvStd phc2) phc3 <-> phcDisj phc2 phc3.
Lemma phcLe_conv_proc_disj :
  forall phc2 phc3 q v,
  phcValid phc2 ->
  phcLe (PHCproc q v) phc2 ->
  phcDisj (phcConvProc phc2) phc3 <->
  phcDisj phc2 phc3.
Lemma phcLe_conv_act_disj :
  forall phc2 phc3 q v v',
  phcValid phc2 ->
  phcLe (PHCact q v v') phc2 ->
  phcDisj (phcConvAct phc2) phc3 <-> phcDisj phc2 phc3.

Lemma phcConvStd_disj_entire :
  forall phc1 phc2,
  phcEntire phc1 ->
  phcDisj phc1 phc2 ->
  phcDisj (phcConvStd phc1) phc2.
Lemma phcConvProc_disj_entire :
  forall phc1 phc2,
  phcEntire phc1 ->
  phcDisj phc1 phc2 ->
  phcDisj (phcConvProc phc1) phc2.
Lemma phcConvAct_disj_entire :
  forall phc1 phc2,
  phcEntire phc1 ->
  phcDisj phc1 phc2 ->
  phcDisj (phcConvAct phc1) phc2.

Lemma phcConvStd_union :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcConvStd (phcUnion phc1 phc2) =
  phcUnion (phcConvStd phc1) (phcConvStd phc2).
Lemma phcConvProc_union :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcConvProc (phcUnion phc1 phc2) =
  phcUnion (phcConvProc phc1) (phcConvProc phc2).
Lemma phcConvAct_union :
  forall phc1 phc2,
  phcDisj phc1 phc2 ->
  phcConvAct (phcUnion phc1 phc2) =
  phcUnion (phcConvAct phc1) (phcConvAct phc2).

Lemma phcConvStd_lt :
  forall phc1 phc2,
  phcValid phc2 ->
  phcLt phc1 phc2 ->
  phcLt (phcConvStd phc1) (phcConvStd phc2).
Lemma phcConvProc_lt :
  forall phc1 phc2,
  phcValid phc2 ->
  phcLt phc1 phc2 ->
  phcLt (phcConvProc phc1) (phcConvProc phc2).
Lemma phcConvAct_lt :
  forall phc1 phc2,
  phcValid phc2 ->
  phcLt phc1 phc2 ->
  phcLt (phcConvAct phc1) (phcConvAct phc2).

Lemma phcConvStd_le :
  forall phc1 phc2,
  phcValid phc2 ->
  phcLe phc1 phc2 ->
  phcLe (phcConvStd phc1) (phcConvStd phc2).
Lemma phcConvProc_le :
  forall phc1 phc2,
  phcValid phc2 ->
  phcLe phc1 phc2 ->
  phcLe (phcConvProc phc1) (phcConvProc phc2).
Lemma phcConvAct_le :
  forall phc1 phc2,
  phcValid phc2 ->
  phcLe phc1 phc2 ->
  phcLe (phcConvAct phc1) (phcConvAct phc2).

Lemma phcConvStd_concr :
  forall phc, phcConcr (phcConvStd phc) = phcConcr phc.
Lemma phcConvProc_concr :
  forall phc, phcConcr (phcConvProc phc) = phcConcr phc.
Lemma phcConvAct_concr :
  forall phc, phcConcr (phcConvAct phc) = phcConcr phc.

Lemma phcSnapshot_conv_proc_occ :
  forall phc,
  phcSnapshot phc <> None ->
  phcSnapshot (phcConvProc phc) <> None.
Lemma phcSnapshot_conv_act_occ :
  forall phc,
  phcSnapshot phc <> None ->
  phcSnapshot (phcConvAct phc) <> None.

Lemma phcSnapshot_lt_conv_std :
  forall phc1 phc2,
  phcLt phc1 (phcConvStd phc2) ->
  phcSnapshot phc1 = phcSnapshot (phcConvStd phc1).
Lemma phcSnapshot_lt_conv_proc :
  forall phc1 phc2,
  phcLt phc1 (phcConvProc phc2) ->
  phcSnapshot phc1 = phcSnapshot (phcConvProc phc1).
Lemma phcSnapshot_lt_conv_act :
  forall phc1 phc2,
  phcLt phc1 (phcConvAct phc2) ->
  phcSnapshot phc1 = phcSnapshot (phcConvAct phc1).

Lemma phcSnapshot_conv_act_pres :
  forall phc v,
  phcSnapshot phc = Some v ->
  phcSnapshot (phcConvAct phc) = Some v.

Note: the following lemmas does not hold for process or action heap cell conversion.

Lemma phcConvStd_lt_eq :
  forall q v phc,
  phcLt (PHCstd q v) phc -> phc = phcConvStd phc.

Permission heaps

Permission heaps are defined as (total) mappings from values to permission heap cells.

Definition PermHeap := Val -> PermHeapCell.

The identity permission heap is free at every location

Definition phIden : PermHeap := fun _ => PHCfree.

An update operation for process maps:

Definition phUpdate (ph : PermHeap)(v : Val)(c : PermHeapCell) :=
  update val_eq_dec ph v c.

Validity

Any permission heap ph is defined to be valid if every entry of ph is valid.

Definition phValid (ph : PermHeap) : Prop :=
  forall l, phcValid (ph l).

Notation "√ ph" :=
  (phValid ph)
  (only printing, at level 80).

The identity permission heap is valid.

Lemma phValid_iden : phValid phIden.

Hint Resolve phValid_iden : core.

Updating a valid permission heap with a valid entry results in a valid permission heap.

Lemma phValid_update :
  forall ph phc l,
  phValid ph -> phcValid phc -> phValid (phUpdate ph l phc).

Disjointness

Any two permission heaps are said to be disjoint if all their entries are pairwise disjoint.

Definition phDisj : relation PermHeap :=
  pointwise_relation Val phcDisj.

Notation "ph1 ⟂ ph2" :=
  (phDisj ph1 ph2)
  (only printing, at level 80).

Permission heap disjointness is symmeric.

Global Instance phDisj_symm : Symmetric phDisj.

Permission heap disjointness implies validity.

Lemma phDisj_valid_l :
  forall ph1 ph2, phDisj ph1 ph2 -> phValid ph1.
Lemma phDisj_valid_r :
  forall ph1 ph2, phDisj ph1 ph2 -> phValid ph2.
Lemma phDisj_valid :
  forall ph1 ph2, phDisj ph1 ph2 -> phValid ph1 /\ phValid ph2.

Any valid permission heap is disjoint with the identity permission heap.

Lemma phDisj_iden_l :
  forall ph, phValid ph -> phDisj ph phIden.
Lemma phDisj_iden_r :
  forall ph, phValid ph -> phDisj phIden ph.

Hint Resolve phDisj_iden_l phDisj_iden_r : core.

Updating disjoint permission heaps with entries that are disjoint preserves heap disjointness.

Lemma phDisj_upd :
  forall ph1 ph2 phc1 phc2 l,
  phcDisj phc1 phc2 ->
  phDisj ph1 ph2 ->
  phDisj (phUpdate ph1 l phc1) (phUpdate ph2 l phc2).

Add Parametric Morphism : phUpdate
  with signature phDisj ==> eq ==> phcDisj ==> phDisj
    as phDisj_upd_mor.

Union

The (disjoint) union of two permission heaps is defined to be the pairwise disjoint union of their heap cells.

Definition phUnion (ph1 ph2 : PermHeap) : PermHeap :=
  fun l => phcUnion (ph1 l) (ph2 l).

Notation "ph1 ⨄ ph2" :=
  (phUnion ph1 ph2)
  (only printing, at level 80, right associativity).

Identity laws for disjoint union.

Lemma phUnion_iden_l :
  forall ph, phUnion ph phIden = ph.
Lemma phUnion_iden_r :
  forall ph, phUnion phIden ph = ph.

Hint Rewrite phUnion_iden_l phUnion_iden_r : core.

Disjoint union is associative and commutative.

Lemma phUnion_assoc :
  forall ph1 ph2 ph3,
  phUnion (phUnion ph1 ph2) ph3 = phUnion ph1 (phUnion ph2 ph3).

Lemma phUnion_comm :
  forall ph1 ph2, phUnion ph1 ph2 = phUnion ph2 ph1.

The union of any two disjoint permission heaps is valid.

Lemma phUnion_valid :
  forall ph1 ph2,
  phDisj ph1 ph2 -> phValid (phUnion ph1 ph2).

Hint Resolve phUnion_valid : core.

Below are various other useful properties of disjoint union.

Lemma phDisj_union_l :
  forall ph1 ph2 ph3,
  phDisj ph1 ph2 ->
  phDisj (phUnion ph1 ph2) ph3 ->
  phDisj ph2 ph3.
Lemma phDisj_union_r :
  forall ph1 ph2 ph3,
  phDisj ph2 ph3 ->
  phDisj ph1 (phUnion ph2 ph3) ->
  phDisj ph1 ph2.

Lemma phDisj_assoc_l :
  forall ph1 ph2 ph3,
  phDisj ph1 ph2 ->
  phDisj (phUnion ph1 ph2) ph3 ->
  phDisj ph1 (phUnion ph2 ph3).
Lemma phDisj_assoc_r :
  forall ph1 ph2 ph3,
  phDisj ph2 ph3 ->
  phDisj ph1 (phUnion ph2 ph3) ->
  phDisj (phUnion ph1 ph2) ph3.

Lemma phUnion_update :
  forall ph1 ph2 phc1 phc2 l,
  phUpdate (phUnion ph1 ph2) l (phcUnion phc1 phc2) =
  phUnion (phUpdate ph1 l phc1) (phUpdate ph2 l phc2).

Lemma phUnion_cell :
  forall ph1 ph2 l,
  phcUnion (ph1 l) (ph2 l) = phUnion ph1 ph2 l.

Lemma phDisj_middle :
  forall ph1 ph2 ph3 ph4,
  phDisj ph1 ph2 ->
  phDisj ph3 ph4 ->
  phDisj (phUnion ph1 ph2) (phUnion ph3 ph4) ->
  phDisj ph2 ph3.

Lemma phDisj_compat :
  forall ph1 ph2 ph3 ph4,
  phDisj ph1 ph3 ->
  phDisj ph2 ph4 ->
  phDisj (phUnion ph1 ph3) (phUnion ph2 ph4) ->
  phDisj (phUnion ph1 ph2) (phUnion ph3 ph4).

Lemma phUnion_swap_l :
  forall ph1 ph2 ph3,
  phUnion ph1 (phUnion ph2 ph3) =
  phUnion ph2 (phUnion ph1 ph3).
Lemma phUnion_swap_r :
  forall ph1 ph2 ph3,
  phUnion (phUnion ph1 ph2) ph3 =
  phUnion (phUnion ph1 ph3) ph2.

Lemma phUnion_compat :
  forall ph1 ph2 ph3 ph4,
  phUnion (phUnion ph1 ph3) (phUnion ph2 ph4) =
  phUnion (phUnion ph1 ph2) (phUnion ph3 ph4).

Lemma phUnion_update_free :
  forall ph1 ph2 phc l,
  ph2 l = PHCfree ->
  phUnion (phUpdate ph1 l phc) ph2 =
  phUpdate (phUnion ph1 ph2) l phc.

Concretisation

The concretisation of a permission heap ph is the heap that contains the concretisations of all heap cells of ph.

Definition phConcr (ph : PermHeap) : Heap :=
  fun l => phcConcr (ph l).

Lemma phConcr_update :
  forall ph l phc,
  phConcr (phUpdate ph l phc) =
  hUpdate (phConcr ph) l (phcConcr phc).

Lemma phConcr_disj_union_l :
  forall ph1 ph2 ph3,
  phDisj ph1 ph3 ->
  phDisj ph2 ph3 ->
  phConcr ph1 = phConcr ph2 ->
  phConcr (phUnion ph1 ph3) = phConcr (phUnion ph2 ph3).
Lemma phConcr_disj_union_r :
  forall ph1 ph2 ph3,
  phDisj ph1 ph3 ->
  phDisj ph2 ph3 ->
  phConcr ph1 = phConcr ph2 ->
  phConcr (phUnion ph3 ph1) = phConcr (phUnion ph3 ph2).

Snapshot

The snapshot of any permission heap ph is the heap constructed from the snapshots of all phs entries.

Definition phSnapshot (ph : PermHeap) : Heap :=
  fun l => phcSnapshot (ph l).

Several useful properties of permission heap snapshots:

Lemma phSnapshot_upd :
  forall ph l phc,
  phSnapshot (phUpdate ph l phc) =
  hUpdate (phSnapshot ph) l (phcSnapshot phc).

Lemma phSnapshot_disj_union_l :
  forall ph1 ph2 ph3,
  phDisj ph1 ph3 ->
  phDisj ph2 ph3 ->
  phSnapshot ph1 = phSnapshot ph2 ->
  phSnapshot (phUnion ph1 ph3) = phSnapshot (phUnion ph2 ph3).
Lemma phSnapshot_disj_union_r :
  forall ph1 ph2 ph3,
  phDisj ph1 ph3 ->
  phDisj ph2 ph3 ->
  phSnapshot ph1 = phSnapshot ph2 ->
  phSnapshot (phUnion ph3 ph1) = phSnapshot (phUnion ph3 ph2).

Finiteness

A permission heap is finite if all mappings that are not free can be mapped to some finite structure, in this case a list.

Definition phFinite (ph : PermHeap) : Prop :=
  exists xs : list Val, forall l, ph l <> PHCfree -> In l xs.

The main property of interest of finite permission heaps, is that one can always find a mapping that is free.

Lemma phFinite_free :
  forall ph,
  phFinite ph -> exists l, ph l = PHCfree.

Finiteness is preserved by any heap updates.

Lemma phFinite_update :
  forall ph l phc,
  phFinite ph -> phFinite (phUpdate ph l phc).

The disjoint union of two finite permission heaps is finite.

Lemma phFinite_union :
  forall ph1 ph2,
  phFinite (phUnion ph1 ph2) <-> phFinite ph1 /\ phFinite ph2.

Permission heap concretisation preserves finiteness.

Lemma phFinite_concr :
  forall ph,
  phValid ph -> phFinite ph <-> hFinite (phConcr ph).

Heap cell conversion

This section discusses tools to convert the types of heap cells in permission heaps.
The operations permheap_conv_std, permheap_conv_proc, and permheap_conv_act are used to convert the heap cell at location l in a given permission heap ph to a standard, process, or action heap cell, respectively. Later we define similar operations that work on sequences of heap locations.

Definition phConvStd (ph : PermHeap)(l : Val) : PermHeap :=
  phUpdate ph l (phcConvStd (ph l)).
Definition phConvProc (ph : PermHeap)(l : Val) : PermHeap :=
  phUpdate ph l (phcConvProc (ph l)).
Definition phConvAct (ph : PermHeap)(l : Val) : PermHeap :=
  phUpdate ph l (phcConvAct (ph l)).

Notation "'std' { ph ',' l }" := (phConvStd ph l).
Notation "'proc' { ph ',' l }" := (phConvProc ph l).
Notation "'act' { ph ',' l }" := (phConvAct ph l).

Heap cell conversion is idempotent.

Lemma phConvStd_idemp :
  forall ph l, phConvStd (phConvStd ph l) l = phConvStd ph l.
Lemma phConvProc_idemp :
  forall ph l, phConvProc (phConvProc ph l) l = phConvProc ph l.
Lemma phConvAct_idemp :
  forall ph l, phConvAct (phConvAct ph l) l = phConvAct ph l.

Heap cell conversion preserves validity.

Lemma phConvStd_valid :
  forall ph l,
  phValid ph <-> phValid (phConvStd ph l).
Lemma phConvProc_valid :
  forall ph l,
  phValid ph <-> phValid (phConvProc ph l).
Lemma phConvAct_valid :
  forall ph l,
  phValid ph <-> phValid (phConvAct ph l).

Heap cell conversion preserves disjointness.

Add Parametric Morphism : phConvStd
  with signature phDisj ==> eq ==> phDisj as phConvStd_disj.
Add Parametric Morphism : phConvProc
  with signature phDisj ==> eq ==> phDisj as phConvProc_disj.
Add Parametric Morphism : phConvAct
  with signature phDisj ==> eq ==> phDisj as phConvAct_disj.

Heap cell conversion preserves entirety.

Lemma phConvStd_entire :
  forall ph l l',
  phcEntire (phConvStd ph l l') <-> phcEntire (ph l').
Lemma phConvProc_entire :
  forall ph l l',
  phcEntire (phConvProc ph l l') <-> phcEntire (ph l').
Lemma phConvAct_entire :
  forall ph l l',
  phcEntire (phConvAct ph l l') <-> phcEntire (ph l').

Heap cell conversion preserves concretisations.

Lemma phConvStd_concr :
  forall ph l,
  phConcr (phConvStd ph l) = phConcr ph.
Lemma phConvProc_concr :
  forall ph l,
  phConcr (phConvProc ph l) = phConcr ph.
Lemma phConvAct_concr :
  forall ph l,
  phConcr (phConvAct ph l) = phConcr ph.

Heap cell conversion distributes over disjoint union.

Lemma phConvStd_union :
  forall ph1 ph2 l,
  phDisj ph1 ph2 ->
  phConvStd (phUnion ph1 ph2) l =
  phUnion (phConvStd ph1 l) (phConvStd ph2 l).
Lemma phConvProc_union :
  forall ph1 ph2 l,
  phDisj ph1 ph2 ->
  phConvProc (phUnion ph1 ph2) l =
  phUnion (phConvProc ph1 l) (phConvProc ph2 l).
Lemma phConvAct_union :
  forall ph1 ph2 l,
  phDisj ph1 ph2 ->
  phConvAct (phUnion ph1 ph2) l =
  phUnion (phConvAct ph1 l) (phConvAct ph2 l).

Free heap cells always convert to free heap cells.

Lemma phConvStd_free :
  forall ph l, ph l = PHCfree -> phConvStd ph l = ph.
Lemma phConvProc_free :
  forall ph l, ph l = PHCfree -> phConvProc ph l = ph.
Lemma phConvAct_free :
  forall ph l, ph l = PHCfree -> phConvAct ph l = ph.

Lemma phConvStd_free2 :
  forall ph l l',
  (phConvStd ph l) l' = PHCfree <-> ph l' = PHCfree.
Lemma phConvProc_free2 :
  forall ph l l',
  (phConvProc ph l) l' = PHCfree <-> ph l' = PHCfree.
Lemma phConvAct_free2 :
  forall ph l l',
  (phConvAct ph l) l' = PHCfree <-> ph l' = PHCfree.

Any heap cell that is not converted stays the same.

Lemma phConvStd_pres :
  forall ph l l', l <> l' -> ph l' = phConvStd ph l l'.
Lemma phConvProc_pres :
  forall ph l l', l <> l' -> ph l' = phConvProc ph l l'.
Lemma phConvAct_pres :
  forall ph l l', l <> l' -> ph l' = phConvAct ph l l'.

Requesting any converted heap cell gives the converted heap cell.

Lemma phConvStd_apply :
  forall ph l, phConvStd ph l l = phcConvStd (ph l).
Lemma phConvProc_apply :
  forall ph l, phConvProc ph l l = phcConvProc (ph l).
Lemma phConvAct_apply :
  forall ph l, phConvAct ph l l = phcConvAct (ph l).

Below are various other useful properties of heap cell conversion.

Lemma phConvStd_disj_entire :
  forall ph1 ph2 l,
  phcEntire (ph1 l) -> phDisj ph1 ph2 -> phDisj (phConvStd ph1 l) ph2.
Lemma phConvProc_disj_entire :
  forall ph1 ph2 l,
  phcEntire (ph1 l) -> phDisj ph1 ph2 -> phDisj (phConvProc ph1 l) ph2.
Lemma phConvAct_disj_entire :
  forall ph1 ph2 l,
  phcEntire (ph1 l) -> phDisj ph1 ph2 -> phDisj (phConvAct ph1 l) ph2.

Lemma phConvProc_snapshot_occ :
  forall ph l l',
  phSnapshot ph l' <> None ->
  phSnapshot (phConvProc ph l) l' <> None.
Lemma phConvAct_snapshot_occ :
  forall ph l l',
  phSnapshot ph l' <> None ->
  phSnapshot (phConvAct ph l) l' <> None.

Lemma phConvAct_snapshot_pres :
  forall ph l l' v,
  phSnapshot ph l' = Some v ->
  phSnapshot (phConvAct ph l) l' = Some v.

Heap cell batch conversions

The following operations are for converting a sequence (or set) of heap locations (i.e., for converting a batch or bulk of locations).

Fixpoint phConvStdMult (ph : PermHeap)(xs : list Val) : PermHeap :=
  match xs with
    | nil => ph
    | l :: xs' => phConvStd (phConvStdMult ph xs') l
  end.
Fixpoint phConvProcMult (ph : PermHeap)(xs : list Val) : PermHeap :=
  match xs with
    | nil => ph
    | l :: xs' => phConvProc (phConvProcMult ph xs') l
  end.
Fixpoint phConvActMult (ph : PermHeap)(xs : list Val) : PermHeap :=
  match xs with
    | nil => ph
    | l :: xs' => phConvAct (phConvActMult ph xs') l
  end.

Notation "'std' { ph ';' xs }" := (phConvStdMult ph xs).
Notation "'proc' { ph ';' xs }" := (phConvProcMult ph xs).
Notation "'act' { ph ';' xs }" := (phConvActMult ph xs).

Converting an empty batch of locations leaves the heap unchanged.

Lemma phConvStdMult_nil :
  forall ph, ph = phConvStdMult ph nil.
Lemma phConvProcMult_nil :
  forall ph, ph = phConvProcMult ph nil.
Lemma phConvActMult_nil :
  forall ph, ph = phConvActMult ph nil.

Properties related to converting a single heap cell:

Lemma phConvStdMult_single :
  forall ph l, phConvStd ph l = phConvStdMult ph [l].
Lemma phConvProcMult_single :
  forall ph l, phConvProc ph l = phConvProcMult ph [l].
Lemma phConvActMult_single :
  forall ph l, phConvAct ph l = phConvActMult ph [l].

Conversions of a non-empty batch of locations can be unfolded.

Lemma phConvStdMult_cons :
  forall xs l ph,
  phConvStdMult ph (l :: xs) = phConvStd (phConvStdMult ph xs) l.
Lemma phConvProcMult_cons :
  forall xs l ph,
  phConvProcMult ph (l :: xs) = phConvProc (phConvProcMult ph xs) l.
Lemma phConvActMult_cons :
  forall xs l ph,
  phConvActMult ph (l :: xs) = phConvAct (phConvActMult ph xs) l.

Conversion of two batches of locations can be appended into a single batch.

Lemma phConvStdMult_app :
  forall xs ys ph,
  phConvStdMult ph (xs ++ ys) = phConvStdMult (phConvStdMult ph ys) xs.
Lemma phConvProcMult_app :
  forall xs ys ph,
  phConvProcMult ph (xs ++ ys) = phConvProcMult (phConvProcMult ph ys) xs.
Lemma phConvActMult_app :
  forall xs ys ph,
  phConvActMult ph (xs ++ ys) = phConvActMult (phConvActMult ph ys) xs.

Batch conversions are closed under permutations.

Lemma phConvStdMult_permut :
  forall ph xs ys,
  Permutation xs ys -> phConvStdMult ph xs = phConvStdMult ph ys.
Lemma phConvProcMult_permut :
  forall ph xs ys,
  Permutation xs ys -> phConvProcMult ph xs = phConvProcMult ph ys.
Lemma phConvActMult_permut :
  forall ph xs ys,
  Permutation xs ys -> phConvActMult ph xs = phConvActMult ph ys.

Add Parametric Morphism : phConvStdMult
  with signature eq ==> @Permutation Val ==> eq
    as phConvStdMult_permut_mor.
Add Parametric Morphism : phConvProcMult
  with signature eq ==> @Permutation Val ==> eq
    as phConvProcMult_permut_mor.
Add Parametric Morphism : phConvActMult
  with signature eq ==> @Permutation Val ==> eq
    as phConvActMult_permut_mor.

Batch conversions are idempotent.

Lemma phConvStdMult_idemp :
  forall xs ph,
  phConvStdMult (phConvStdMult ph xs) xs = phConvStdMult ph xs.
Lemma phConvProcMult_idemp :
  forall xs ph,
  phConvProcMult (phConvProcMult ph xs) xs = phConvProcMult ph xs.
Lemma phConvActMult_idemp :
  forall xs ph,
  phConvActMult (phConvActMult ph xs) xs = phConvActMult ph xs.

Any duplicate conversions in a batch are subsumed.

Lemma phConvStdMult_subsume :
  forall xs l ph,
  In l xs -> phConvStdMult ph (l :: xs) = phConvStdMult ph xs.
Lemma phConvProcMult_subsume :
  forall xs l ph,
  In l xs -> phConvProcMult ph (l :: xs) = phConvProcMult ph xs.
Lemma phConvActMult_subsume :
  forall xs l ph,
  In l xs -> phConvActMult ph (l :: xs) = phConvActMult ph xs.

Batch conversions preserve heap validity.

Lemma phConvStdMult_valid :
  forall xs ph, phValid ph <-> phValid (phConvStdMult ph xs).
Lemma phConvProcMult_valid :
  forall xs ph, phValid ph <-> phValid (phConvProcMult ph xs).
Lemma phConvActMult_valid :
  forall xs ph, phValid ph <-> phValid (phConvActMult ph xs).

Converting a batch of only free locations does not change the heap.

Lemma phConvStdMult_free :
  forall xs ph,
  (forall l, In l xs -> ph l = PHCfree) ->
  phConvStdMult ph xs = ph.
Lemma phConvProcMult_free :
  forall xs ph,
  (forall l, In l xs -> ph l = PHCfree) ->
  phConvProcMult ph xs = ph.
Lemma phConvActMult_free :
  forall xs ph,
  (forall l, In l xs -> ph l = PHCfree) ->
  phConvActMult ph xs = ph.

Lemma phConvStdMult_free2 :
  forall xs ph l,
  phConvStdMult ph xs l = PHCfree <-> ph l = PHCfree.
Lemma phConvProcMult_free2 :
  forall xs ph l,
  phConvProcMult ph xs l = PHCfree <-> ph l = PHCfree.
Lemma phConvActMult_free2 :
  forall xs ph l,
  phConvActMult ph xs l = PHCfree <-> ph l = PHCfree.

Batch conversions preserve heap disjointness.

Lemma phConvStdMult_disj :
  forall xs ph1 ph2,
  phDisj ph1 ph2 -> phDisj (phConvStdMult ph1 xs) (phConvStdMult ph2 xs).
Lemma phConvProcMult_disj :
  forall xs ph1 ph2,
  phDisj ph1 ph2 -> phDisj (phConvProcMult ph1 xs) (phConvProcMult ph2 xs).
Lemma phConvActMult_disj :
  forall xs ph1 ph2,
  phDisj ph1 ph2 -> phDisj (phConvActMult ph1 xs) (phConvActMult ph2 xs).

Add Parametric Morphism : phConvStdMult
  with signature phDisj ==> @Permutation Val ==> phDisj
    as phConvStdMult_disj_mor.
Add Parametric Morphism : phConvProcMult
  with signature phDisj ==> @Permutation Val ==> phDisj
    as phConvProcMult_disj_mor.
Add Parametric Morphism : phConvActMult
  with signature phDisj ==> @Permutation Val ==> phDisj
    as phConvActMult_disj_mor.

Batch conversions preserve entirety.

Lemma phConvStdMult_entire:
  forall xs ph l,
  phcEntire (phConvStdMult ph xs l) <-> phcEntire (ph l).
Lemma phConvProcMult_entire:
  forall xs ph l,
  phcEntire (phConvProcMult ph xs l) <-> phcEntire (ph l).
Lemma phConvActMult_entire:
  forall xs ph l,
  phcEntire (phConvActMult ph xs l) <-> phcEntire (ph l).

Batch conversions distribute over disjoint union.

Lemma phConvStdMult_union :
  forall xs ph1 ph2,
  phDisj ph1 ph2 ->
  phConvStdMult (phUnion ph1 ph2) xs =
  phUnion (phConvStdMult ph1 xs) (phConvStdMult ph2 xs).
Lemma phConvProcMult_union :
  forall xs ph1 ph2,
  phDisj ph1 ph2 ->
  phConvProcMult (phUnion ph1 ph2) xs =
  phUnion (phConvProcMult ph1 xs) (phConvProcMult ph2 xs).
Lemma phConvActMult_union :
  forall xs ph1 ph2,
  phDisj ph1 ph2 ->
  phConvActMult (phUnion ph1 ph2) xs =
  phUnion (phConvActMult ph1 xs) (phConvActMult ph2 xs).

Batch conversions preserve heap concretisation.

Lemma phConvStdMult_concr :
  forall xs ph, phConcr (phConvStdMult ph xs) = phConcr ph.
Lemma phConvProcMult_concr :
  forall xs ph, phConcr (phConvProcMult ph xs) = phConcr ph.
Lemma phConvActMult_concr :
  forall xs ph, phConcr (phConvActMult ph xs) = phConcr ph.

Any location that is not in the conversion batch is not affected by batch conversion.

Lemma phConvStdMult_pres :
  forall xs l ph, ~ In l xs -> ph l = phConvStdMult ph xs l.
Lemma phConvProcMult_pres :
  forall xs l ph, ~ In l xs -> ph l = phConvProcMult ph xs l.
Lemma phConvActMult_pres :
  forall xs l ph, ~ In l xs -> ph l = phConvActMult ph xs l.

Any location in the conversion batch is indeed converted.

Lemma phConvStdMult_apply :
  forall xs l ph,
  In l xs -> phConvStdMult ph xs l = phcConvStd (ph l).
Lemma phConvProcMult_apply :
  forall xs l ph,
  In l xs -> phConvProcMult ph xs l = phcConvProc (ph l).
Lemma phConvActMult_apply :
  forall xs l ph,
  In l xs -> phConvActMult ph xs l = phcConvAct (ph l).

Batch conversions preserve occupied snapshots.

Lemma phConvProcMult_snapshot_occ :
  forall xs ph l,
  phSnapshot ph l <> None ->
  phSnapshot (phConvProcMult ph xs) l <> None.
Lemma phConvActMult_snapshot_occ :
  forall xs ph l,
  phSnapshot ph l <> None ->
  phSnapshot (phConvActMult ph xs) l <> None.

Lemma phConvActMult_snapshot_pres :
  forall xs ph l v,
  phSnapshot ph l = Some v ->
  phSnapshot (phConvActMult ph xs) l = Some v.

Below are various other useful properties of batch conversions.

Lemma phConvStdMult_disj_entire :
  forall xs ph1 ph2,
  (forall l, In l xs -> phcEntire (ph1 l)) ->
  phDisj ph1 ph2 ->
  phDisj (phConvStdMult ph1 xs) ph2.
Lemma phConvProcMult_disj_entire :
  forall xs ph1 ph2,
  (forall l, In l xs -> phcEntire (ph1 l)) ->
  phDisj ph1 ph2 ->
  phDisj (phConvProcMult ph1 xs) ph2.
Lemma phConvActMult_disj_entire :
  forall xs ph1 ph2,
  (forall l, In l xs -> phcEntire (ph1 l)) ->
  phDisj ph1 ph2 ->
  phDisj (phConvActMult ph1 xs) ph2.

End Heaps.