Library Soundness

Require Import Assertions.
Require Import HahnBase.
Require Import Heaps.
Require Import HeapSolver.
Require Import List.
Require Import Permissions.
Require Import PermSolver.
Require Import Permutation.
Require Import PermutationTactic.
Require Import Prelude.
Require Import Process.
Require Import ProcMap.
Require Import ProcMapSolver.
Require Import Programs.
Require Import QArith Qcanon.

Import ListNotations.

Set Implicit Arguments.

Soundness

Module Type Soundness
  (domains : Domains)
  (heaps : Heaps domains)
  (hsolver : HeapSolver domains heaps)
  (procs : Processes domains)
  (procmaps : ProcMaps domains heaps procs)
  (progs : Programs domains heaps procs procmaps)
  (pmsolver : ProcMapSolver domains heaps procs procmaps)
  (assns : Assertions domains heaps hsolver procs procmaps progs pmsolver).

Export domains heaps hsolver procs procmaps pmsolver progs assns.

Process environments

The remaining theory assumes an environment of process definitions, which assigns to each (defined) process its precondition.

Note that processes do not have postconditions (any longer). Instead, processes have the Passert (or HPassert) constructors to specify that a certain property should hold at that point.

So we define process environments simply as a total function precondition that maps any process to its precondition.

Parameter precondition : HProc -> HCond.

Moreover, the remaining theory requires that all defined processes are safe (with respect to psafe).

Parameter precondition_safe :
  forall P s ps,
    pcond_eval (cDehybridise (precondition P) s) ps = true ->
    psafe (pDehybridise P s) ps.

Adequacy of process maps

The following definition captures what it means for a process map entry c to be safe (with respect to some heap h).

In particular this means that, if c is occupied, then the underlying process in c is safe with respect to any process store that corresponds with h. This correspondence is needed to connect process-algebraic state to shared program state.

Definition pmeSafe (h : Heap)(c : ProcMapEntry) : Prop :=
  match c with
    | PEelem _ P xs f =>
        forall ps,
          (forall x, In x xs -> h (f x) = Some (ps x)) ->
        psafe P ps
    | PEfree => True
    | PEinvalid => False
  end.

Safety of process map entries is preserved by bisimilarity.

Lemma pmeSafe_bisim :
  forall h c1 c2,
  pmeBisim c1 c2 -> pmeSafe h c1 -> pmeSafe h c2.
Add Parametric Morphism : pmeSafe
  with signature eq ==> pmeBisim ==> iff
    as pmeSafe_bisim_mor.

Free entries are trivially safe.

Lemma pmeSafe_iden :
forall h, pmeSafe h PEfree.

Safety of process map entries c is stable under replacing heaps that agree on all locations covered by c.

Lemma pmeSafe_heap_acc :
  forall h1 h2 c,
    (forall l, In l (pmeProj c) -> h1 l = h2 l) ->
  pmeSafe h1 c ->
  pmeSafe h2 c.

Safety of process map entries is stable under extending (snapshot) heaps.

Lemma pmeSafe_subheap :
  forall h1 h2 c,
  (forall l v, h2 l = Some v -> h1 l = Some v) ->
  pmeSafe h1 c ->
  pmeSafe h2 c.

Lemma pmeSafe_weaken_snapshot_l :
  forall ph1 ph2 c,
  phDisj ph1 ph2 ->
  pmeSafe (phSnapshot (phUnion ph1 ph2)) c ->
  pmeSafe (phSnapshot ph1) c.

Lemma pmeSafe_weaken_snapshot_r :
  forall ph1 ph2 c,
  phDisj ph1 ph2 ->
  pmeSafe (phSnapshot (phUnion ph1 ph2)) c ->
  pmeSafe (phSnapshot ph2) c.

Removing entry information does not invalidate safety.

Lemma pmeSafe_weaken_l :
  forall h c1 c2,
  pmeSafe h (pmeUnion c1 c2) ->
  pmeSafe h c1.

Lemma pmeSafe_weaken_r :
  forall h c1 c2,
  pmeSafe h (pmeUnion c1 c2) ->
  pmeSafe h c2.

Any process map is defined to be safe (with respect to some heap) if all its entries are safe with respect to pmeSafe.

Definition pmSafe (h : Heap)(pm : ProcMap) : Prop :=
forall pid, pmeSafe h (pm pid).

The identity process map is trivially safe.

Lemma pmSafe_iden :
forall h, pmSafe h pmIden.

Bisimilarity preserves safety.

Lemma pmSafe_bisim :
  forall h pm1 pm2,
  pmBisim pm1 pm2 -> pmSafe h pm1 -> pmSafe h pm2.
Add Parametric Morphism : pmSafe
  with signature eq ==> pmBisim ==> iff
    as pmSafe_bisim_mor.

Process map safety is stable under extensions of the (snapshot) heap.

Lemma pmSafe_subheap :
  forall h1 h2 pm,
    (forall l v, h2 l = Some v -> h1 l = Some v) ->
  pmSafe h1 pm ->
  pmSafe h2 pm.

Lemma pmSafe_weaken_snapshot_l :
  forall ph1 ph2 pm,
  phDisj ph1 ph2 ->
  pmSafe (phSnapshot (phUnion ph1 ph2)) pm ->
  pmSafe (phSnapshot ph1) pm.

Lemma pmSafe_weaken_snapshot_r :
  forall ph1 ph2 pm,
  phDisj ph1 ph2 ->
  pmSafe (phSnapshot (phUnion ph1 ph2)) pm ->
  pmSafe (phSnapshot ph2) pm.

Removing process map information does not invalidate safety.

Lemma pmSafe_weaken_l :
  forall h pm1 pm2,
  pmSafe h (pmUnion pm1 pm2) ->
  pmSafe h pm1.

Lemma pmSafe_weaken_r :
  forall h pm1 pm2,
  pmSafe h (pmUnion pm1 pm2) ->
  pmSafe h pm2.

Well-structured process maps

A process map pm is defined to be well-structured if every heap location l is accessed by at most one entry of pm. This definition therefore implies that all the entries of pm access different heap locations (i.e., disjoint parts of the heap).

This definition is important in the soundness argument, since every heap location can be subject to at most one "active process", and we need to make this fact explicit, which we do via pmWs.

Definition pmWs (pm : ProcMap) : Prop :=
forall p1 p2 l,
In l (pmeProj (pm p1)) -> In l (pmeProj (pm p2)) -> p1 = p2.

Bisimilarity preserves well-structuredness of process maps.

Lemma pmWs_bisim :
  forall pm1 pm2,
  pmBisim pm1 pm2 -> pmWs pm1 -> pmWs pm2.
Add Parametric Morphism : pmWs
  with signature pmBisim ==> iff as pmWs_mor.

The identity process map is trivially well-structured.

Lemma pmWs_iden : pmWs pmIden.

Process map agreement preserves well-structuredness.

Lemma pmWs_agree :
  forall pm1 pm2,
  pmAgree pm1 pm2 -> pmWs pm1 -> pmWs pm2.
Add Parametric Morphism : pmWs
  with signature pmAgree ==> iff as pmWs_agree_mor.

Below are several other useful properties of well-structuredness.

Lemma pmWs_update :
  forall pm p c,
    (forall p' l, p <> p' -> In l (pmeProj c) -> ~ In l (pmeProj (pm p'))) ->
  pmWs pm ->
  pmWs (pmUpdate pm p c).

Adequacy

The auxiliary predicate invariant_sat determines whether a resource invariant J is satisfied by the given model in the context of the given program C. If the program is locked, we allow the resource invariant to be arbitrary (as in the proof system the resource invariant then becomes Atrue), but otherwise the model should hold with respect to J.

Definition invariant_sat (ph : PermHeap)(pm : ProcMap)(s g : Store)(C : GhostCmd)(J : Assn) : Prop :=
  ~ cmd_locked C -> sat ph pm s g J.

Fixpoint safe (n : nat)(basic : Prop)(C : GhostCmd)(ph : PermHeap)(pm : ProcMap)(s g : Store)(J A : Assn) : Prop :=
  match n with
    | O => True
    | S m =>

        (C = Cskip -> sat ph pm s g A) /\

      (forall phF pmF,
        phDisj ph phF ->
        pmDisj pm pmF ->
      let h := phConcr (phUnion ph phF) in
      let pm' := pmUnion pm pmF in
        hFinite h ->
        pmFinite pm' ->
        ~ gfault h pm' s g C) /\

      (forall l, cmd_acc C s l -> phcLt PHCfree (ph l)) /\

      (forall l, cmd_writes C s l -> phcEntire (ph l)) /\

      (forall phJ phF pmJ pmF pmC h' s' C',
        phDisj ph phJ ->
        phDisj (phUnion ph phJ) phF ->
        pmDisj pm pmJ ->
        pmDisj (pmUnion pm pmJ) pmF ->
        pmBisim (pmUnion (pmUnion pm pmJ) pmF) pmC ->
        pmFinite pmC ->
        pmWs pmC ->
        invariant_sat phJ pmJ s g C J ->
      let h := phConcr (phUnion (phUnion ph phJ) phF) in
      let hs := phSnapshot (phUnion (phUnion ph phJ) phF) in
        hFinite h ->
        pmCovers pmC hs ->
        pmSafe hs pmC ->
        step h s (plain C) h' s' C' ->
      exists ph' phJ',
        phDisj ph' phJ' /\
        phDisj (phUnion ph' phJ') phF /\
        phConcr (phUnion (phUnion ph' phJ') phF) = h' /\
        hFinite h' /\
        (basic -> phJ = phJ' /\ phSnapshot ph = phSnapshot ph') /\
      exists pm' pmJ' pmC',
        pmDisj pm' pmJ' /\
        pmDisj (pmUnion pm' pmJ') pmF /\
        pmBisim (pmUnion (pmUnion pm' pmJ') pmF) pmC' /\
        pmFinite pmC' /\
        pmWs pmC' /\
        (basic -> pmBisim pm pm' /\ pmBisim pmJ pmJ') /\
      let hs' := phSnapshot (phUnion (phUnion ph' phJ') phF) in
        pmCovers pmC' hs' /\
        pmSafe hs' pmC' /\
      exists g' C'',
        plain C'' = C' /\
        gstep h pmC s g C h' pmC' s' g' C'' /\
        invariant_sat phJ' pmJ' s' g' C'' J /\
        safe m basic C'' ph' pm' s' g' J A)
  end.

Safety is stable under replacing process maps by bisimilar ones.

Lemma safe_pmBisim :
  forall n basic C ph pm1 pm2 s g J A,
  pmBisim pm1 pm2 ->
  safe n basic C ph pm1 s g J A ->
  safe n basic C ph pm2 s g J A.

Safety is stable under replacing resource invariants by equivalent ones.

Lemma safe_aEquiv_inv :
  forall n basic C ph pm s g R1 R2 A,
  aEquiv R1 R2 ->
  safe n basic C ph pm s g R1 A ->
  safe n basic C ph pm s g R2 A.

Safety is stable under replacing postconditions by equivalent ones.

Lemma safe_aEquiv_post :
  forall n basic C ph pm s g R A1 A2,
  phValid ph ->
  pmValid pm ->
  aEquiv A1 A2 ->
  safe n basic C ph pm s g R A1 ->
  safe n basic C ph pm s g R A2.

Add Parametric Morphism : safe
  with signature eq ==> eq ==> eq ==> eq ==> pmBisim ==> eq ==> eq ==> aEquiv ==> eq ==> iff
    as safe_bisim_mor.

Adequacy is monotonic in the number of computation steps.

That is, if any configuration is safe for n steps, it must also be safe for less than n steps.

Open Scope nat_scope.

Lemma safe_mono :
  forall m n basic C ph pm s g J A,
  m <= n ->
  safe n basic C ph pm s g J A ->
  safe m basic C ph pm s g J A.

Close Scope nat_scope.

The Cskip program being safe in a certain state means that the postcondition holds in that state.

Lemma safe_skip :
  forall n basic ph pm s g J A,
  safe (S n) basic Cskip ph pm s g J A ->
  sat ph pm s g A.

Lemma safe_done :
  forall n basic ph pm s g J A,
  sat ph pm s g A ->
  safe n basic Cskip ph pm s g J A.

Any (ghost) store can be replaced by one that agrees on the values of all free variables in the program, resource invariant, and the postcondition.

Lemma safe_agree :
  forall n basic C ph pm s1 s2 g J A,
  sAgree (assn_fv A) s1 s2 ->
  sAgree (assn_fv J) s1 s2 ->
  sAgree (cmd_fv C) s1 s2 ->
  safe n basic C ph pm s1 g J A ->
  safe n basic C ph pm s2 g J A.
Lemma safe_agree_ghost :
  forall n basic C ph pm s g1 g2 J A,
  sAgree (assn_fv A) g1 g2 ->
  sAgree (assn_fv J) g1 g2 ->
  sAgree (cmd_fv C) g1 g2 ->
  safe n basic C ph pm s g1 J A ->
  safe n basic C ph pm s g2 J A.

Disjuncts in postconditions can always be introduced.

Lemma safe_disj_weaken :
  forall n basic C ph pm s g R A1 A2,
  safe n basic C ph pm s g R A1 ->
  safe n basic C ph pm s g R (Adisj A1 A2).

Soundness of the proof rules

The meaning of Hoare triples is given by the following definition.

Intuitively csl b J A C A' holds if C is a user program, and moreover that C is safe for any number of reduction steps.

The extra basic parameter is purely for technical reasons. Recall that basic programs exclude certain language features such as specification-only commands. It later helps if we explicitly administer whether a csl judgement is used in the context of a basic program. The extra basic parameter is used for just that.

Definition csl (basic : Prop)(J : Assn)(A1 : Assn)(C : GhostCmd)(A2 : Assn) : Prop :=
  cmd_user C /\
  forall n ph pm s g,
    phValid ph ->
    pmValid pm ->
    pmSafe (phSnapshot ph) pm ->
    cmd_wf C ->
    sat ph pm s g A1 ->
    safe n basic C ph pm s g J A2.

Any assertion (pre- or postcondition, or resource invariant) can always be replaced by an equivalent one.

Add Parametric Morphism : csl
with signature eq ==> aEquiv ==> aEquiv ==> eq ==> aEquiv ==> iff
as csl_aEquiv_mor.

Any program judgement with an unsatisfiable precondition trivially holds.

Lemma csl_trivial :
forall basic J C A,
cmd_user C -> csl basic J Afalse C A.

Skip rule

Theorem rule_skip :
forall basic J A,
csl basic J A Cskip A.

Sequential composition

Open Scope nat_scope.

Lemma safe_seq :
  forall n basic C1 C2 J A1 A2 ph pm s g,
  phValid ph ->
  pmValid pm ->
  pmSafe (phSnapshot ph) pm ->
  safe n basic C1 ph pm s g J A1 ->
  (forall m ph' pm' s' g',
    m <= n ->
    phValid ph' ->
    pmValid pm' ->
    pmSafe (phSnapshot ph') pm' ->
    sat ph' pm' s' g' A1 ->
    safe m basic C2 ph' pm' s' g' J A2) ->
  safe n basic (Cseq C1 C2) ph pm s g J A2.

Close Scope nat_scope.

Theorem rule_seq :
  forall basic J A1 A2 A3 C1 C2,
  csl basic J A1 C1 A2 ->
  csl basic J A2 C2 A3 ->
  csl basic J A1 (Cseq C1 C2) A3.

If-then-else rule

Lemma safe_ite :
  forall n basic J A1 A2 B C1 C2 ph pm s g,
  sat ph pm s g A1 ->
    (sat ph pm s g (Astar A1 (Aplain B)) -> safe n basic C1 ph pm s g J A2) ->
    (sat ph pm s g (Astar A1 (Aplain (Bnot B))) -> safe n basic C2 ph pm s g J A2) ->
  safe n basic (Cite B C1 C2) ph pm s g J A2.

Theorem rule_ite :
  forall basic J A1 A2 B C1 C2,
  csl basic J (Astar A1 (Aplain B)) C1 A2 ->
  csl basic J (Astar A1 (Aplain (Bnot B))) C2 A2 ->
  csl basic J A1 (Cite B C1 C2) A2.

While rule

Lemma safe_while :
  forall n basic B C ph pm s g J A,
  csl basic J (Astar A (Aplain B)) C A ->
  sat ph pm s g A ->
  cmd_wf C ->
  safe n basic (Cwhile B C) ph pm s g J (Astar A (Aplain (Bnot B))).

Theorem rule_while :
  forall basic J A B C,
  csl basic J (Astar A (Aplain B)) C A ->
  csl basic J A (Cwhile B C) (Astar A (Aplain (Bnot B))).

Assign rule

Lemma safe_assign :
  forall n basic J A x E ph pm s g,
  ~ assn_fv J x ->
  sat ph pm s g (assn_subst x E A) ->
  safe n basic (Cass x E) ph pm s g J A.

Theorem rule_assign :
  forall basic J A x E,
  ~ assn_fv J x ->
  csl basic J (assn_subst x E A) (Cass x E) A.

Rule of consequence

Lemma safe_conseq :
  forall n basic C ph pm s g J A1 A2,
  phValid ph ->
  pmValid pm ->
  pmSafe (phSnapshot ph) pm ->
  aEntails A1 A2 ->
  safe n basic C ph pm s g J A1 ->
  safe n basic C ph pm s g J A2.
Theorem rule_conseq :
  forall basic J A1 A2 A1' A2' C,
  aEntails A1 A1' ->
  aEntails A2' A2 ->
  csl basic J A1' C A2' ->
  csl basic J A1 C A2.

Disjunction rule

Theorem rule_disj :
  forall basic J A1 A2 A1' A2' C,
  csl basic J A1 C A1' ->
  csl basic J A2 C A2' ->
  csl basic J (Adisj A1 A2) C (Adisj A1' A2').

Corollary rule_disj_l :
  forall basic J A1 A2 A3 C,
  csl basic J A2 C A1 ->
  csl basic J A3 C A1 ->
  csl basic J (Adisj A2 A3) C A1.

Corollary rule_disj_r :
  forall basic J A1 A2 A3 C,
  csl basic J A1 C A2 ->
  csl basic J A1 C A3 ->
  csl basic J A1 C (Adisj A2 A3).

Lemma rule_disj_weaken :
  forall basic J A1 A2 A3 C,
  csl basic J A1 C A2 ->
  csl basic J A1 C (Adisj A2 A3).

Frame rule

Lemma safe_frame :
  forall n basic C ph1 ph2 pm1 pm2 s g J A1 A2,
  phDisj ph1 ph2 ->
  pmDisj pm1 pm2 ->
  pmSafe (phSnapshot ph1) pm1 ->
  disjoint (assn_fv A2) (cmd_mod C) ->
  sat ph2 pm2 s g A2 ->
  safe n basic C ph1 pm1 s g J A1 ->
  safe n basic C (phUnion ph1 ph2) (pmUnion pm1 pm2) s g J (Astar A1 A2).
Theorem rule_frame :
  forall basic J A1 A2 A3 C,
  disjoint (assn_fv A3) (cmd_mod C) ->
  csl basic J A1 C A2 ->
  csl basic J (Astar A1 A3) C (Astar A2 A3).

Heap reading

Lemma rule_lookup_std :
  forall basic x E1 q E2 J A,
  ~ In x (expr_fv E1) ->
  ~ In x (expr_fv E2) ->
  ~ assn_fv J x ->
  csl basic J (Astar (assn_subst x E2 A) (Apointsto PTTstd q E1 E2)) (Cread x E1) (Astar A (Apointsto PTTstd q E1 E2)).

Lemma rule_lookup_proc :
  forall basic x E1 q E2 J A,
  ~ In x (expr_fv E1) ->
  ~ In x (expr_fv E2) ->
  ~ assn_fv J x ->
  csl basic J (Astar (assn_subst x E2 A) (Apointsto PTTproc q E1 E2)) (Cread x E1) (Astar A (Apointsto PTTproc q E1 E2)).

Lemma rule_lookup_act :
  forall basic x E1 q E2 J A,
  ~ In x (expr_fv E1) ->
  ~ In x (expr_fv E2) ->
  ~ assn_fv J x ->
  csl basic J (Astar (assn_subst x E2 A) (Apointsto PTTact q E1 E2)) (Cread x E1) (Astar A (Apointsto PTTact q E1 E2)).

Theorem rule_lookup :
  forall basic x E1 q E2 J A t,
  ~ In x (expr_fv E1) ->
  ~ In x (expr_fv E2) ->
  ~ assn_fv J x ->
  csl basic J (Astar (assn_subst x E2 A) (Apointsto t q E1 E2)) (Cread x E1) (Astar A (Apointsto t q E1 E2)).

Heap writing

Soundness of the rules for heap writing. In the paper these rules are presented as a single rule (for presentational convenience), but here we handle heap writing via two separate rules -- one for handling points-to ownership predicates of type PTTstd, and one for PTTact.

Theorem rule_write_std :
  forall basic J E1 E2 E3,
  csl basic J (Apointsto PTTstd 1 E1 E3) (Cwrite E1 E2) (Apointsto PTTstd 1 E1 E2).
Theorem rule_write_act :
  forall basic J E1 E2 E3,
  csl basic J (Apointsto PTTact 1 E1 E3) (Cwrite E1 E2) (Apointsto PTTact 1 E1 E2).

Heap allocation

Theorem rule_alloc :
  forall basic x E J,
  ~ In x (expr_fv E) ->
  ~ assn_fv J x ->
  csl basic J Atrue (Calloc x E) (Apointsto PTTstd perm_full (Evar x) E).

Heap disposal

Theorem rule_dispose :
forall basic E1 E2 J,
csl basic J (Apointsto PTTstd perm_full E1 E2) (Cdispose E1) Atrue.

Parallel composition

Lemma safe_par :
  forall n basic C1 C2 ph1 ph2 pm1 pm2 s g J A1 A2,
  phDisj ph1 ph2 ->
  pmDisj pm1 pm2 ->
  pmSafe (phSnapshot ph1) pm1 ->
  pmSafe (phSnapshot ph2) pm2 ->
  cmd_wf (Cpar C1 C2) ->
  disjoint (cmd_fv C1) (cmd_mod C2) ->
  disjoint (assn_fv A1) (cmd_mod C2) ->
  disjoint (assn_fv J) (cmd_mod C2) ->
  disjoint (cmd_fv C2) (cmd_mod C1) ->
  disjoint (assn_fv A2) (cmd_mod C1) ->
  disjoint (assn_fv J) (cmd_mod C1) ->
  safe n basic C1 ph1 pm1 s g J A1 ->
  safe n basic C2 ph2 pm2 s g J A2 ->
  safe n basic (Cpar C1 C2) (phUnion ph1 ph2) (pmUnion pm1 pm2) s g J (Astar A1 A2).
Theorem rule_par :
  forall basic C1 C2 J A1 A2 A1' A2',
  disjoint (cmd_fv C1) (cmd_mod C2) ->
  disjoint (assn_fv A1') (cmd_mod C2) ->
  disjoint (assn_fv J) (cmd_mod C2) ->
  disjoint (cmd_fv C2) (cmd_mod C1) ->
  disjoint (assn_fv A2') (cmd_mod C1) ->
  disjoint (assn_fv J) (cmd_mod C1) ->
  csl basic J A1 C1 A1' ->
  csl basic J A2 C2 A2' ->
  csl basic J (Astar A1 A2) (Cpar C1 C2) (Astar A1' A2').

Existential quantification

Theorem rule_ex :
  forall basic C J (A1 A2 : Val -> Assn),
    (forall x, csl basic J (A1 x) C (A2 x)) ->
  csl basic J (Aex A1) C (Aex A2).

Share rule

Lemma safe_share :
  forall n C ph1 ph2 pm1 pm2 s g J A1 A2,
  phDisj ph1 ph2 ->
  pmDisj pm1 pm2 ->
  pmSafe (phSnapshot ph1) pm1 ->
  pmSafe (phSnapshot ph2) pm2 ->
  invariant_sat ph2 pm2 s g C A2 ->
  safe n False C ph1 pm1 s g (Astar J A2) A1 ->
  safe n False C (phUnion ph1 ph2) (pmUnion pm1 pm2) s g J (Astar A1 A2).
Theorem rule_share :
  forall C J A1 A2 A3,
  csl False (Astar J A3) A1 C A2 ->
  csl False J (Astar A1 A3) C (Astar A2 A3).

Atomic rule

Lemma safe_atom :
  forall n C ph pm s g J A,
  safe n False C ph pm s g Atrue (Astar A J) ->
  safe n False (Cinatom C) ph pm s g J A.

Theorem rule_atom :
  forall C J A1 A2,
  csl False Atrue (Astar A1 J) C (Astar A2 J) ->
  csl False J A1 (Catomic C) A2.

Process init rule

Theorem rule_proc_init :
  forall Pf E J (x : Var)(xs : list ProcVar)(f1 f2 : ProcVar -> Expr),
  let HP := Pf E in
  let b := precondition HP in
  let B := hcond_convert b f2 in
  let fq := fun _ => perm_full in
    (forall y, In y (hcond_fpv b) -> In y xs) ->
  ~ assn_fv J x ->
  ~ (exists y : ProcVar, In y xs /\ In x (expr_fv (f1 y))) ->
  ~ (exists y : ProcVar, In y xs /\ In x (expr_fv (f2 y))) ->
  csl False J
    (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTstd)) (Aplain B))
    (Cproc x Pf E xs f1)
    (Astar (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aproc x perm_full HP xs f1)) (Aplain B)).

Process finish rule

Theorem rule_proc_finish :
  forall HP J (x : Var)(xs : list ProcVar)(f1 f2 : ProcVar -> Expr),
  let fq := fun _ => perm_full in
  csl False J
    (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aproc x perm_full (HPalt HP HPepsilon) xs f1))
    (Cendproc x)
    (Aiter (ApointstoIter xs fq f1 f2 PTTstd)).

Action rule

The soundness proof of the action rule requires some extra auxiliary definitions and properties, in particular that the metadata that is stored in Cinact commands actually makes sense with respect to the rest of the state that is maintained. The central definition that helps with is is metadata_agree.

Lemma phcConcr_snapshot_none :
  forall pme, phcConcr pme = None -> phcSnapshot pme = None.

Definition metadata_agree (pid : Val)(a : Act)(v : Val)(xs : list ProcVar)(f : ProcVar -> Val)(h hs : Heap)(pm : ProcMap) : Prop :=

  exists (q : Qc)(P : Proc),
    pmeBisim (pm pid) (PEelem q P xs f) /\

    (forall x : ProcVar, In x (act_fv a v) -> In x xs) /\

    (forall x : ProcVar, In x xs -> h (f x) = hs (f x)) /\

    exists ps : ProcStore,
      (forall x : ProcVar, In x xs -> h (f x) = Some (ps x)) /\
        pcond_eval (guard a v) ps = true.

Lemma metadata_agree_pmBisim :
  forall pid a v xs f h hs pm1 pm2,
  pmBisim pm1 pm2 ->
  metadata_agree pid a v xs f h hs pm1 ->
  metadata_agree pid a v xs f h hs pm2.

Add Parametric Morphism : metadata_agree
  with signature eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> pmBisim ==> iff
    as metadata_agree_pmBisim_mor.

Lemma metadata_agree_F :
  forall pid a v xs F1 F2 h hs pm,
    (forall x : ProcVar, In x xs -> F1 x = F2 x) ->
  metadata_agree pid a v xs F1 h hs pm ->
  metadata_agree pid a v xs F2 h hs pm.

Now to the actual soundness result, which can be proven using the following (rather involved) key lemma:

Lemma safe_action :
  forall n C ph pm pm' (s g : Store) x hs q E HP HQ (xs ys1 ys2 : list ProcVar) a (fq : ProcVar -> Qc)(f1 f2 : ProcVar -> Expr)(J A : Assn),
  let B2 := hcond_convert (heffect a E) f2 in
  let F1 := expr_eval_map f1 s : ProcVar -> Val in
  let v := expr_eval E s in
  metadata_agree (g x) a v xs F1 hs (phSnapshot ph) pm' ->
  Permutation xs (ys1 ++ ys2) ->
  (forall y : ProcVar, In y ys1 -> fq y <> perm_full) ->
  (forall y : ProcVar, In y ys2 -> fq y = perm_full) ->
  (forall y : ProcVar, In y xs -> perm_valid (fq y)) ->
  (forall y : ProcVar, disjoint (expr_fv (f1 y)) (cmd_mod C)) ->
  disjoint (expr_fv E) (cmd_mod C) ->
  disjoint (hproc_fv HP) (cmd_mod C) ->
  disjoint (hproc_fv HQ) (cmd_mod C) ->
  ~ cmd_mod C x ->
  cmd_basic C ->
  pmDisj pm pm' ->
  sat phIden pm' s g (Aproc x q (HPalt (HPseq (HPact a E) HP) HQ) xs f1) ->
  safe n True C ph pm s g J (Astar (Astar (Aiter (ApointstoIter_procact xs fq f1 f2)) (Aplain B2)) A) ->
  safe n False (Cinact (GMdata (g x) a v hs) C) ph (pmUnion pm pm') s g J (Astar (Astar (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aproc x q HP xs f1)) (Aplain B2)) A).
Theorem rule_act :
  forall x a E C xs J q HP HQ (f1 f2 f2' : ProcVar -> Expr)(fq : ProcVar -> Qc) A1 A2,
  let B1 := hcond_convert (hguard a E) f2 in
  let B2 := hcond_convert (heffect a E) f2' in
  (forall y v, In y (act_fv a v) -> In y xs) ->
  (forall y : ProcVar, In y xs -> perm_valid (fq y)) ->
  (forall y : ProcVar, disjoint (expr_fv (f1 y)) (cmd_mod C)) ->
  disjoint (expr_fv E) (cmd_mod C) ->
  disjoint (hproc_fv HP) (cmd_mod C) ->
  disjoint (hproc_fv HQ) (cmd_mod C) ->
  ~ cmd_mod C x ->
  csl True J (Astar (Astar (Aiter (ApointstoIter_procact xs fq f1 f2)) (Aplain B1)) A1) C (Astar (Astar (Aiter (ApointstoIter_procact xs fq f1 f2')) (Aplain B2)) A2) ->
  csl False J
    (Astar (Astar (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aproc x q (HPalt (HPseq (HPact a E) HP) HQ) xs f1)) (Aplain B1)) A1)
    (Cact x a E C)
    (Astar (Astar (Astar (Aiter (ApointstoIter xs fq f1 f2' PTTproc)) (Aproc x q HP xs f1)) (Aplain B2)) A2).

Query rule

We use the following small helper definition (only for technical reasons).

Definition DisjWrapper (P Q : Prop) := P \/ Q.

Lemma wrap : forall P Q, P \/ Q -> DisjWrapper P Q.
Lemma unwrap : forall P Q, DisjWrapper P Q -> P \/ Q.

And now the actual rule.

Theorem rule_query :
  forall x HB HP HQ q (xs : list ProcVar)(f1 f2 : ProcVar -> Expr)(fq : ProcVar -> Qc) J A,
  (forall y : ProcVar, In y (hcond_fpv HB) -> In y xs) ->
  (forall y : ProcVar, In y xs -> perm_valid (fq y)) ->
  let B := hcond_convert HB f2 in
  csl False J
    (Astar (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aproc x q (HPalt (HPseq (HPassert HB) HP) HQ) xs f1)) A)
    (Cquery x)
    (Astar (Astar (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aproc x q HP xs f1)) (Aplain B)) A).
End Soundness.