Theory Perm

theory Perm
imports Main Rat VHelper Lang
begin

This file contains a soundness proof for CSL with multiple resources and permissions.

(Adapted to Isabelle 2016-1 by Qin Yu and James Brotherston)

Permission model

Fractional permissions are rational numbers in the range (0,1].

typedef myfrac = {x::rat. 0 < x ∧ x ≤ 1}
by (rule_tac x=0.5 in exI, simp)

definition pfull ≜ Abs_myfrac 1 — Full permission

type_synonym pheap = (nat ⇀ nat * myfrac) — Permission heaps
type_synonym pstate = stack × pheap — Permission states

Definition when two permission heaps are composable.

definition
  pdisj :: pheap ⇒ pheap ⇒ bool
where
  pdisj h1 h2 ≜ (∀x. case h1 x of None ⇒ True | Some y1 ⇒
                      (case h2 x of None ⇒ True | Some y2 ⇒
                       fst y1 = fst y2 ∧
                       Rep_myfrac (snd y1) + Rep_myfrac (snd y2) ≤ 1))

Composition of two permission heaps.

definition
  padd :: pheap ⇒ pheap ⇒ pheap
where
  padd h1 h2 ≜
     (λx. case h1 x of None ⇒ h2 x | Some y1 ⇒
          (case h2 x of None ⇒ h1 x | Some y2 ⇒
           Some (fst y1, Abs_myfrac (Rep_myfrac (snd y1) + Rep_myfrac (snd y2)))))

Composition of two permission heaps, better for automation.

definition
  mypadd :: pheap option ⇒ pheap option ⇒ pheap option
  (infixr ⊕ 100)
where
  xo ⊕ yo ≜ case xo of None ⇒ None | Some x ⇒
             (case yo of None ⇒ None | Some y ⇒
              if pdisj x y then Some (padd x y) else None)

Full-permission domain of a permission heap

definition fpdom h ≜ {x. ∃v. h x = Some (v, pfull)}

Mapping from permission heaps to normal heaps

definition
  ptoheap :: pheap option ⇒ heap ⇒ bool
where
  ptoheap ho h ≜ case ho of None ⇒ False | Some ha ⇒
                  (∀x. case ha x of None ⇒ h x = None | Some y ⇒
                   snd y = pfull ∧ h x = Some (fst y))

Basic properties of fractions in the range (0,1]

lemmas rat_simps =
add_rat eq_rat one_rat zero_rat mult_rat le_rat minus_rat diff_rat

lemmas frac_simps =
Rep_myfrac_inverse Rep_myfrac Abs_myfrac_inverse Abs_myfrac_inject

lemma frac_contra[simp]:

¬ (Rep_myfrac pfull + Rep_myfrac b ≤ 1)

¬ (Rep_myfrac b + Rep_myfrac pfull ≤ 1)

by (case_tac b, auto simp add: pfull_def frac_simps)+

lemma frac_pos:

0 < Rep_myfrac x

by (case_tac x, simp add: frac_simps)

lemma frac_pos2[simp]:

0 < Rep_myfrac x + Rep_myfrac y

0 < Rep_myfrac x + (Rep_myfrac y + Rep_myfrac z)

by (case_tac x, (case_tac y)?, (case_tac z)?, simp add: frac_simps)+

Properties of permission-heaps

lemma pdisj_empty[simp]:

pdisj x Map.empty

pdisj Map.empty x

by (clarsimp simp add: pdisj_def split: option.splits)+

lemma pdisj_upd:

h x = Some (w, pfull)

pdisj (h(x ↦ (v, pfull))) h' = pdisj h h'

by (simp add: pdisj_def, rule iff_allI, auto split: option.splits)

lemma pdisj_comm:

pdisj h1 h2 = pdisj h2 h1

by (fastforce split: option.splits simp add: pdisj_def)

lemma padd_empty[simp]:

padd x Map.empty = x

padd Map.empty x = x

by (rule ext, clarsimp simp add: padd_def split: option.splits)+

lemma padd_comm[simp]:

pdisj x y

padd y x = padd x y

by (fastforce split: option.splits simp add: padd_def pdisj_def algebra_simps)

lemma pdisj_padd:

pdisj y z ; pdisj x (padd y z)

(pdisj x y ∧ pdisj x z)

apply (clarsimp simp add: pdisj_def padd_def all_conj_distrib [symmetric])
apply (drule_tac a=xa in allD)+
apply (auto split: option.splits simp add: algebra_simps frac_simps)
apply (cut_tac x=be in frac_pos, simp)
apply (cut_tac x=bd in frac_pos, simp)
done

lemma pdisjE[elim]:

pdisj x (padd y z) ; pdisj y z

pdisj x y

pdisj x (padd y z) ; pdisj y z

pdisj x z

by (drule (1) pdisj_padd, simp)+

lemma pdisj_padd_comm:

pdisj y (padd x z); pdisj x z

pdisj x (padd y z)

apply (clarsimp simp add: pdisj_def padd_def all_conj_distrib [symmetric])
apply (drule_tac a=xa in allD)+
apply (auto split: option.splits simp add: algebra_simps frac_simps)
apply (subst Abs_myfrac_inverse, simp add: frac_simps)
apply (cut_tac x=bf in frac_pos, simp)
apply (cut_tac x=bd in frac_pos, simp)
done

lemma pdisj_padd_expand:

pdisj x y

pdisj (padd x y) z = (pdisj x (padd y z) ∧ pdisj y z)

apply (simp add: pdisj_comm, rule iffI)
apply (frule (1) pdisj_padd_comm)
apply (drule (1) pdisj_padd, subst padd_comm, simp_all add: pdisj_comm)
apply (clarify, rule pdisj_padd_comm, simp_all add: pdisj_comm)
done

lemma padd_assoc:

pdisj x (padd y z) ; pdisj y z

padd (padd x y) z = padd x (padd y z)

apply (clarsimp simp add: pdisj_def padd_def all_conj_distrib [symmetric], rule ext)
apply (drule_tac a=xa in allD)+
apply (auto split: option.splits simp add: algebra_simps frac_simps)
apply (subst Abs_myfrac_inverse, simp_all add: frac_simps)
apply (cut_tac x=be in frac_pos, simp)
done

lemma padd_left_comm:

pdisj x (padd y z) ; pdisj y z

padd x (padd y z) = padd y (padd x z)

padd x y = padd x z ; pdisj x y; pdisj x z

y = z

apply (clarsimp simp add: pdisj_def padd_def all_conj_distrib [symmetric], rule ext)
apply (drule_tac a=xa in allD |drule_tac x=xa in fun_cong)+
apply (auto split: option.splits simp add: algebra_simps frac_simps)
apply (case_tac b, case_tac ba, clarsimp simp add: frac_simps)
apply (case_tac b, case_tac ba, clarsimp simp add: frac_simps)
apply (case_tac b, case_tac ba, clarsimp simp add: frac_simps)
done

lemma dom_padd[simp]:

dom (padd x y) = dom x ∪ dom y

by (rule set_eqI, simp add: padd_def dom_def split: option.splits)

lemma fpdom_padd[elim]:

pdisj h1 h2

fpdom h1 ⊆ fpdom (padd h1 h2)

pdisj h1 h2

fpdom h2 ⊆ fpdom (padd h1 h2)

apply (auto simp add: fpdom_def pdisj_def padd_def disjoint_def split: option.splits)
apply (drule_tac a=x in allD, fastforce)+
done

lemma pa_empty[simp]:

x ⊕ Some Map.empty = x

Some Map.empty ⊕ x = x

by (auto simp add: mypadd_def split: option.splits)

lemma pa_none[simp]:

x ⊕ None = None

None ⊕ x = None

by (auto simp add: mypadd_def split: option.splits)

lemma pa_comm:

y ⊕ x = x ⊕ y

by (auto simp add: mypadd_def pdisj_comm split: option.splits)

lemma pa_assoc:

(x ⊕ y) ⊕ z = x ⊕ y ⊕ z

apply (auto simp add: mypadd_def padd_assoc pdisj_padd_expand split: option.splits)
apply (erule notE, fast)
done

lemma pa_left_comm:

y ⊕ x ⊕ z = x ⊕ y ⊕ z

apply (auto simp add: mypadd_def padd_left_comm split: option.splits)
apply (erule_tac[!] notE, (erule (1) pdisj_padd_comm |erule (1) pdisjE)+)
done

lemma some_padd:

pdisj h1 h2

Some (padd h1 h2) = Some h1 ⊕ Some h2

by (simp add: mypadd_def)

lemmas pa_ac = pa_comm pa_assoc pa_left_comm some_padd

lemma pa_cancel:

x ⊕ y = x ⊕ z; x ⊕ y ≠ None

y = z

apply (simp add: mypadd_def split: option.splits if_splits)
apply (clarify, erule (2) padd_cancel)
done

lemma ptoD:

ptoheap x z; ptoheap y z

x = y

apply (clarsimp simp add: ptoheap_def split: option.splits)
apply (rule ext)
apply ((drule_tac a=xa in allD)+, auto)
apply (case_tac x2a xa, case_tac x2 xa, simp_all, fast+)
done

lemma pdisj_search1:

ptoheap (Some x ⊕ Some y) hh

pdisj x y

ptoheap (Some x ⊕ Some y ⊕ z) hh

pdisj x y

ptoheap (Some x ⊕ z ⊕ Some y) hh

pdisj x y

ptoheap (Some x ⊕ z ⊕ Some y ⊕ w) hh

pdisj x y

ptoheap (Some x ⊕ z ⊕ w ⊕ Some y) hh

pdisj x y

ptoheap (Some x ⊕ z ⊕ w ⊕ Some y ⊕ v) hh

pdisj x y

ptoheap (z ⊕ Some x ⊕ Some y) hh

pdisj x y

ptoheap (z ⊕ Some x ⊕ Some y ⊕ w) hh

pdisj x y

ptoheap (z ⊕ Some x ⊕ w ⊕ Some y) hh

pdisj x y

ptoheap (z ⊕ Some x ⊕ w ⊕ Some y ⊕ v) hh

pdisj x y

ptoheap (z ⊕ Some x ⊕ w ⊕ v ⊕ Some y) hh

pdisj x y

ptoheap (z ⊕ w ⊕ Some x ⊕ Some y) hh

pdisj x y

ptoheap (z ⊕ w ⊕ Some x ⊕ Some y ⊕ v) hh

pdisj x y

ptoheap (z ⊕ w ⊕ Some x ⊕ v ⊕ Some y) hh

pdisj x y

apply (simp_all add: ptoheap_def mypadd_def, case_tac[!] pdisj x y, simp_all)
apply (auto split: option.splits if_split_asm)
apply (erule notE | fast | erule pdisjE [rotated])+
done

lemma pdisj_comm_implies:

pdisj h1 h2

pdisj h2 h1

by (fastforce split: option.splits simp add: pdisj_def)

lemmas pdisj_search[elim] =
pdisj_search1 pdisj_search1[THEN pdisj_comm_implies]

Assertions with permissions

Separating conjunction of a finite list of assertions is just a derived assertion.

primrec
  Aistar :: assn list ⇒ assn
where
  Aistar [] = Aemp
| Aistar (P # Ps) = Astar P (Aistar Ps)

primrec
  sat :: pstate ⇒ assn ⇒ bool (infixl ⊨ 60)
where
  (σ ⊨ Aemp) = (snd σ = empty)
| (σ ⊨ Apsto k E E') = (dom (snd σ) = { edenot E (fst σ) } ∧ (snd σ) (edenot E (fst σ)) = Some (edenot E' (fst σ), k))
| (σ ⊨ P ** Q) = (∃h1 h2. (fst σ, h1) ⊨ P ∧ (fst σ, h2) ⊨ Q ∧ snd σ = padd h1 h2 ∧ pdisj h1 h2)
| (σ ⊨ Awand P Q) = (∀h. disjoint (dom (snd σ)) (dom h) ∧ (fst σ, h) ⊨ P ⟶ (fst σ, snd σ ++ h) ⊨ Q)
| (σ ⊨ Apure B) = bdenot B (fst σ)
| (σ ⊨ Aconj P Q) = (σ ⊨ P ∧ σ ⊨ Q)
| (σ ⊨ Adisj P Q) = (σ ⊨ P ∨ σ ⊨ Q)
| (σ ⊨ Aex PP) = (∃v. σ ⊨ PP v)

Shorthand for full permission

definition
Aptsto :: exp ⇒ exp ⇒ assn (infixl ⟼ 200)
where
E ⟼ E' ≜ Apsto pfull E E'

lemma sat_Aptsto[simp]:

(σ ⊨ E ⟼ E') = (dom (snd σ) = { edenot E (fst σ) }
∧ (snd σ) (edenot E (fst σ)) = Some (edenot E' (fst σ), pfull))

by (simp add: Aptsto_def)

definition
implies :: assn ⇒ assn ⇒ bool (infixl ⊑ 60)
where
P ⊑ Q ≜ (∀σ. σ ⊨ P ⟶ σ ⊨ Q)

lemma sat_istar_map_expand:

r ∈ set l

σ ⊨ Aistar (map f l)
⟷ (∃h1 h2. (fst σ, h1) ⊨ f r
∧ (fst σ, h2) ⊨ Aistar (map f (remove1 r l))
∧ snd σ = padd h1 h2 ∧ pdisj h1 h2)

apply (case_tac σ, rename_tac s h, clarify)
apply (induct l arbitrary: σ, simp_all, clarsimp, safe)
apply (intro exI conjI, simp+)
apply (drule pdisj_padd, simp, clarsimp)
apply (rule padd_left_comm, simp_all)
apply (rule pdisj_padd_comm, simp_all)

apply (intro exI conjI, simp+)
apply (drule pdisj_padd, simp, clarsimp)
apply (rule padd_left_comm, simp_all)
apply (rule pdisj_padd_comm, simp_all)
done

Precision

We say that an assertion is precise if for any given heap, there is at most one subheap that satisfies the formula. (The formal definition below says that if there are two such subheaps, they must be equal.)

definition
  precise :: assn ⇒ bool
where
  precise P ≜ ∀h1 h2 h1' h2' s. pdisj h1 h2 ∧ pdisj h1' h2'
                   ∧ padd h1 h2 = padd h1' h2' ∧ (s, h1) ⊨ P ∧ (s, h1') ⊨ P
               ⟶ h1 = h1'

A direct consequence of the definition that is more useful in Isabelle, because unfolding the definition slows down Isabelle's simplifier dramatically.

lemma preciseD:

precise P; (s, x) ⊨ P; (s, x') ⊨ P; padd x y = padd x' y';
pdisj x y; pdisj x' y'

x = x' ∧ y = y'

unfolding precise_def
by (drule all5_impD, (erule conjI)+, simp_all, drule padd_cancel)

The separating conjunction of precise assertions is precise:

lemma precise_istar:

∀x ∈ set l. precise x

precise (Aistar l)

apply (induct l, simp_all (no_asm) add: precise_def)
apply (clarsimp simp add: padd_assoc pdisj_padd_expand)
apply (drule (3) preciseD, simp_all, clarsimp)
apply (drule (3) preciseD, simp_all)
done

Auxiliary definition for resource environments

definition
envs :: ('a ⇒ assn) ⇒ 'a list ⇒ 'a list ⇒ assn
where
envs Γ l l' ≜ Aistar (map Γ (list_minus l l'))

lemma sat_envs_expand:

r ∈ set l; r ∉ set l'; distinct l

σ ⊨ envs Γ l l'
⟷ (∃h1 h2. (fst σ, h1) ⊨ Γ r
∧ (fst σ, h2) ⊨ envs Γ (removeAll r l) l'
∧ snd σ = padd h1 h2 ∧ pdisj h1 h2)

apply (simp add: envs_def distinct_remove1_removeAll [THEN sym] add: list_minus_remove1)
apply (subst sat_istar_map_expand [where f=Γ and r=r], simp_all)
done

lemma envs_upd:

r ∉ set l

envs (Γ(r := R)) l l' = envs Γ l l'

r ∈ set l'

envs (Γ(r := R)) l l' = envs Γ l l'

by (simp_all add: envs_def)

lemma envs_removeAll_irr:

r ∉ set l

envs Γ l (removeAll r l') = envs Γ l l'

by (simp add: envs_def list_minus_removeAll_irr)

lemma envs_removeAll2:

r ∈ set l'

envs Γ (removeAll r l) (removeAll r l') = envs Γ l l'

by (simp add: envs_def list_minus_removeAll2)

lemma envs_app:

disjoint (set x) (set z)

envs Γ (x @ z) (y @ z) = envs Γ x y

disjoint (set z) (set x)

envs Γ (z @ x) (z @ y) = envs Γ x y

by (simp_all add: envs_def list_minus_appl list_minus_appr)

Free variables and substitutions

primrec
  fvA :: assn ⇒ var set
where
  fvA (Aemp) = {}
| fvA (Apure B) = fvB B
| fvA (Apsto k e1 e2) = (fvE e1 ∪ fvE e2)
| fvA (P ** Q) = (fvA P ∪ fvA Q)
| fvA (Awand P Q) = (fvA P ∪ fvA Q)
| fvA (Aconj P Q) = (fvA P ∪ fvA Q)
| fvA (Adisj P Q) = (fvA P ∪ fvA Q)
| fvA (Aex P) = (⋃x. fvA (P x))

definition
  fvAs :: ('a ⇒ assn) ⇒ var set
where
  fvAs Γ = (⋃x. fvA (Γ x))

primrec
  subA :: var ⇒ exp ⇒ assn ⇒ assn
where
  subA x E (Aemp) = Aemp
| subA x E (Apure B) = Apure (subB x E B)
| subA x E (Apsto k e1 e2) = (Apsto k (subE x E e1) (subE x E e2))
| subA x E (P ** Q) = (subA x E P ** subA x E Q)
| subA x E (Awand P Q) = Awand (subA x E P) (subA x E Q)
| subA x E (Aconj P Q) = Aconj (subA x E P) (subA x E Q)
| subA x E (Adisj P Q) = Adisj (subA x E P) (subA x E Q)
| subA x E (Aex PP) = Aex (λn. subA x E (PP n))

lemma subAptsto[simp]:

subA x E (e1 ⟼ e2) = (subE x E e1 ⟼ subE x E e2)

by (simp add: Aptsto_def)

lemma subA_assign:

(s,h) ⊨ subA x E P ⟷ (s(x := edenot E s), h) ⊨ P

by (induct P arbitrary: h, simp_all add: subE_assign subB_assign fun_upd_def)

lemma fvA_istar[simp]:

fvA (Aistar Ps) = (⋃P ∈ set Ps. fvA P)

by (induct Ps, simp_all)

Proposition 4.2 for assertions

lemma assn_agrees:

agrees (fvA P) s s'

(s, h) ⊨ P ⟷ (s', h) ⊨ P

apply (induct P arbitrary: h, simp_all add: bexp_agrees)
apply (clarsimp, (subst exp_agrees, simp_all)+ )
apply (rule iff_exI, simp add: agrees_def)
done

Corollaries of Proposition 4.2, useful for automation.

lemma assns_agrees:

agrees (fvAs J) s s'

(s, h) ⊨ envs J l1 l2 ⟷ (s', h) ⊨ envs J l1 l2

apply (clarsimp simp add: envs_def, subst assn_agrees, simp_all)
apply (erule agrees_search, auto simp add: fvAs_def)
done

corollary assns_agreesE[elim]:

(s, h) ⊨ envs J l1 l2 ; agrees (fvAs J) s s'

(s',h) ⊨ envs J l1 l2

by (simp add: assns_agrees)

corollary assn_agrees2[simp]:

x ∉ fvA P

(s(x := v), h) ⊨ P ⟷ (s, h) ⊨ P

by (rule assn_agrees, simp add: agrees_def)

corollary assns_agrees2[simp]:

x ∉ fvAs J

(s(x := v), h) ⊨ envs J l l' ⟷ (s, h) ⊨ envs J l l'

by (rule assns_agrees, simp add: agrees_def)

Meaning of CSL judgments

Definition 5.1: Configuration safety.

primrec
  safe :: nat ⇒ cmd ⇒ stack ⇒ pheap ⇒ (rname ⇒ assn) ⇒ assn ⇒ bool
where
  safe 0 C s h Γ Q = True
| safe (Suc n) C s h Γ Q = (
            (C = Cskip ⟶ (s, h) ⊨ Q)
          ∧ (∀hF hh. ptoheap (Some h ⊕ hF) hh ⟶ ¬ aborts C (s, hh))
          ∧ accesses C s ⊆ dom h
          ∧ writes C s ⊆ fpdom h
          ∧ (∀hJ hF hh C' σ'.
                  red C (s, hh) C' σ'
                 ⟶ ptoheap (Some h ⊕ Some hJ ⊕ hF) hh
                 ⟶ (s, hJ) ⊨ envs Γ (llocked C') (llocked C)
                 ⟶ (∃h' hJ'.
                         ptoheap (Some h' ⊕ Some hJ' ⊕ hF) (snd σ')
                       ∧ (fst σ', hJ') ⊨ envs Γ (llocked C) (llocked C')
                       ∧ safe n C' (fst σ') h' Γ Q)))

The predicate safe n C s h Γ Q says that the command C and the logical state (s, h) are safe with respect to the resource environment Γ and the postcondition Q for n execution steps. Intuitively, any configuration is safe for zero steps. For n + 1 steps, it must (i) satisfy the postcondition if it is a terminal configuration, (ii) not abort, (iii) access memory only inside its footprint, and (iv) after any step it does, re-establish the resource invariant and be safe for another n steps.

Definition 5.2: The meaning of CSL judgements.

definition
  CSL :: (rname ⇒ assn) ⇒ assn ⇒ cmd ⇒ assn ⇒ bool
  (_ ⊢ { _ } _ { _ })
where
  Γ ⊢ {P} C {Q} ≜ (user_cmd C ∧ (∀n s h. (s, h) ⊨ P ⟶ safe n C s h Γ Q))

Basic properties of Definition 5.1

Proposition 4.3: Monotonicity with respect to the step number.

lemma safe_mon:

safe n C s h J Q; m ≤ n

safe m C s h J Q

apply (induct m arbitrary: C s n h l, simp)
apply (case_tac n, clarify)
apply (simp only: safe.simps, clarsimp)
apply (drule all5D, drule (2) all_imp2D, clarsimp)
apply (rule_tac x=h' in exI, rule_tac x=hJ' in exI, simp)
done

Proposition 4.4: Safety depends only the free variables of C, Q, and Γ.

lemma safe_agrees:

safe n C s h Γ Q ;
agrees (fvC C ∪ fvA Q ∪ fvAs Γ) s s'

safe n C s' h Γ Q

apply (induct n arbitrary: C s s' h bl, simp, simp only: safe.simps, clarify)
apply (rule conjI, clarsimp, subst assn_agrees, subst agreesC, assumption+)
apply (rule conjI, clarsimp)
apply (drule_tac aborts_agrees, simp, fast, simp, simp)
apply (rule conjI, subst (asm) accesses_agrees, simp_all)
apply (rule conjI, subst (asm) writes_agrees, simp_all)
apply (clarify, drule_tac X=fvC C ∪ fvAs Γ ∪ fvA Q in red_agrees,
simp (no_asm), fast, simp (no_asm), fast, clarify)
apply (drule allD, drule (1) all5_impD, clarsimp)
apply (drule imp2D, erule_tac[2] assns_agreesE, simp_all add: agreesC, clarify)
apply (rule_tac x=h'a and y=hJ' in ex2I, simp add: pa_ac)
apply (rule conjI, erule assns_agreesE, subst agreesC, assumption)
apply (erule (1) mall4_imp2D, simp add: agreesC)
apply (drule red_properties, auto)
done

Soundness of the proof rules

Skip

lemma safe_skip[intro!]:

(s,h) ⊨ Q

safe n Cskip s h J Q

by (induct n, simp_all)

theorem rule_skip:

Γ ⊢ {P} Cskip {P}

by (auto simp add: CSL_def)

Parallel composition

lemma disj_conv:

pdisj h1 h2

disjoint (fpdom h1) (dom h2)

pdisj h1 h2

disjoint (dom h1) (fpdom h2)

by (simp add: fpdom_def pdisj_def disjoint_def, rule set_eqI, drule_tac a=x in allD, clarsimp)+

lemma safe_par:

safe n C1 s h1 J Q1; safe n C2 s h2 J Q2;
wf_cmd (Cpar C1 C2);
pdisj h1 h2;
disjoint (fvC C1 ∪ fvA Q1 ∪ fvAs J) (wrC C2);
disjoint (fvC C2 ∪ fvA Q2 ∪ fvAs J) (wrC C1)

safe n (Cpar C1 C2) s (padd h1 h2) J (Q1 ** Q2)

apply (induct n arbitrary: C1 C2 s h1 h2 bl1 bl2, simp, clarsimp)
apply (rule conjI, clarify)
— no aborts
apply (erule aborts.cases, simp_all add: pa_ac)
   apply (clarify, drule_tac a=Some h2 ⊕ hF in all2_impD, simp add: pa_ac, clarsimp)
   apply (clarify, drule_tac a=Some h1 ⊕ hF in all2_impD, simp add: pa_ac, clarsimp)
— no races
apply (clarsimp, erule notE, (erule disjoint_search [rotated])+, erule disj_conv)+
— accesses
apply (rule conjI, erule order_trans, simp)+
apply (rule conjI, erule order_trans, erule fpdom_padd)+
— step
apply (clarsimp, erule red_par_cases, simp_all)
— C1 does a step
  apply (clarify, drule_tac a=hJ and b=Some h2 ⊕ hF in all2D, drule all4_impD,
         simp_all add: envs_app locked_eq, clarsimp simp add: pa_ac)
  apply (subgoal_tac pdisj h' h2, erule_tac[2] pdisj_search)
  apply (rule_tac x=padd h' h2 and y=hJ' in ex2I, simp add: pa_ac)
  apply (frule (1) red_wf_cmd, drule red_properties, clarsimp)
  apply (drule_tac a=C1' and b=C2 in mall2D, simp add: hsimps)
  apply (drule mall3_imp2D, erule_tac[3] mimp3D, simp_all add: hsimps)
  apply (rule_tac s=s in safe_agrees)
  apply (rule_tac n=Suc n in safe_mon, simp add: pa_ac, simp)
  apply (fastforce simp add: agreesC disjoint_commute)
  apply (intro conjI | erule (1) disjoint_search)+
— C2 does a step
  apply (clarify, drule_tac a=hJ and b=Some h1 ⊕ hF in all2D, drule all4_imp2D,
         simp_all add: hsimps envs_app pa_ac, clarsimp)
  apply (subgoal_tac pdisj h1 h', erule_tac[2] pdisj_search)
  apply (rule_tac x=padd h1 h' and y=hJ' in ex2I, simp add: pa_ac)
  apply (frule (1) red_wf_cmd, drule red_properties, clarsimp)
  apply (drule_tac a=C1 and b=C2' in mall2D, simp add: hsimps)
  apply (drule mall3_imp2D, erule_tac[3] mimp3D, simp_all add: hsimps)
  apply (rule_tac s=s in safe_agrees)
   apply (rule_tac n=Suc n in safe_mon, simp add: pa_ac, simp)
  apply (subst agreesC, bestsimp, bestsimp, bestsimp)
— Par skip skip
apply (clarify)
apply (rule_tac x=padd h1 h2 and y=hJ in ex2I, simp add: pa_ac)
apply (rule_tac safe_skip, simp, (rule exI, erule conjI)+, simp)
done

theorem rule_par:

Γ ⊢ {P1} C1 {Q1} ; Γ ⊢ {P2} C2 {Q2};
disjoint (fvC C1 ∪ fvA Q1 ∪ fvAs Γ) (wrC C2);
disjoint (fvC C2 ∪ fvA Q2 ∪ fvAs Γ) (wrC C1)

Γ ⊢ {P1 ** P2} (Cpar C1 C2) {Q1 ** Q2}

by (auto simp add: CSL_def intro!: safe_par)

Resource declaration

lemma safe_resource:

safe n C s h (Γ(r := R)) Q; wf_cmd C; disjoint (fvA R) (wrC C)

(∀hR. r ∉ locked C ⟶ pdisj h hR ⟶ (s,hR) ⊨ R ⟶ safe n (Cresource r C) s (padd h hR) Γ (Q ** R))
∧ (r ∈ locked C ⟶ safe n (Cresource r C) s h Γ (Q ** R))

apply (induct n arbitrary: C s h, simp, clarsimp simp add: pa_ac)
apply (rule conjI, clarify)
apply (rule conjI, clarify)
  — no aborts
  apply (erule aborts.cases, simp_all, clarsimp)
  apply (drule_tac a=Some hR ⊕ hF in all2_impD, simp add: pa_ac, simp)
— accesses
apply (rule conjI, erule order_trans, simp)
apply (rule conjI, erule order_trans, erule fpdom_padd)
— step
apply (clarify, frule red_properties, clarsimp)
apply (erule red.cases, simp_all, clarsimp, rename_tac C s hh C' s' hh')
— normal step
apply (subgoal_tac pdisj hR hJ, erule_tac[2] pdisj_search)
  apply (case_tac r ∈ set (llocked C'), simp_all add: locked_eq)
   apply (drule_tac a=padd hJ hR and b=hF and c=hh in all3D,
          drule_tac a=C' and b=s' and c=hh' in all3D, simp_all add: pa_ac)
   apply (drule impD, subst sat_envs_expand [where r=r], simp_all)
     apply (rule wf_cmd_distinct_locked, erule (1) red_wf_cmd)
    apply (intro exI conjI, simp, simp_all add: envs_upd)
   apply (clarsimp simp add: envs_removeAll_irr)
   apply (drule (1) mall3_imp2D, erule (1) red_wf_cmd)
   apply (drule mimpD, fast, clarsimp)
   apply (intro exI conjI, simp+)
  — r ∉ locked C'
  apply (drule_tac a=hJ and b=Some hR ⊕ hF and c=hh in all3D, drule_tac a=C' and b=s' and c=hh' in all3D,
         simp add: pa_ac)
  apply (clarsimp simp add: envs_upd)
  apply (drule (1) mall3_imp2D, erule (1) red_wf_cmd)
  apply (drule mimpD, fast, clarsimp)
  apply (subgoal_tac pdisj h' hR, erule_tac[2] pdisj_search)
  apply (rule_tac x=padd h' hR and y=hJ' in ex2I, simp add: pa_ac)
  apply (drule_tac a=hR in all_imp2D, simp_all add: hsimps)
  apply (subst assn_agrees, simp_all, fastforce)
— skip
apply (clarsimp simp add: envs_def)
apply (rule_tac x=padd h hR in exI, simp add: pa_ac, rule safe_skip, simp, fast)
— not user cmd
apply (clarsimp)
apply (rule conjI, clarsimp, erule aborts.cases, simp_all, clarsimp, clarsimp)
apply (frule red_properties, clarsimp)
apply (erule red.cases, simp_all, clarsimp, rename_tac C s hh C' s' hh')
apply (drule_tac a=hJ and b=hF and c=hh in all3D, drule_tac a=C' and b=s' and c=hh' in all3D,
       simp add: pa_ac)
apply (clarsimp simp add: envs_upd envs_removeAll2)
apply (drule (1) mall3_imp2D, erule (1) red_wf_cmd)
apply (drule mimpD, fast, clarsimp)
apply (case_tac r ∈ set (llocked C'), simp_all add: locked_eq envs_removeAll2 envs_upd)
apply (intro exI conjI, simp+)
apply (subst (asm) sat_envs_expand [where r=r], simp_all add: wf_cmd_distinct_locked,
       clarsimp simp add: pa_ac, rename_tac hR' hJ')
apply (subgoal_tac pdisj h' hR', erule_tac[2] pdisj_search)
apply (drule (2) all_imp2D, rule_tac x=padd h' hR' and y=hJ' in ex2I, simp add: pa_ac envs_upd)
done

theorem rule_resource:

Γ(r := R) ⊢ {P} C {Q} ; disjoint (fvA R) (wrC C)

Γ ⊢ {P ** R} (Cresource r C) {Q ** R}

by (clarsimp simp add: CSL_def, drule (1) all3_impD)
(auto simp add: locked_eq dest!: safe_resource)

Frame rule

The safety of the frame rule can be seen as a special case of the parallel composition rule taking one thread to be the empty command.

lemma safe_frame:

safe n C s h J Q;
pdisj h hR;
disjoint (fvA R) (wrC C);
(s,hR) ⊨ R

safe n C s (padd h hR) J (Q ** R)

apply (induct n arbitrary: C s h hR, simp, clarsimp simp add: pa_ac)
apply (rule conjI, clarify, fast)
apply (rule conjI, clarify)
— no aborts
apply (drule_tac a=Some hR ⊕ hF in all2_impD, simp add: pa_ac, simp)
— accesses
apply (rule conjI, erule order_trans, simp)
apply (rule conjI, erule order_trans, erule fpdom_padd)
— step
apply (clarify, frule red_properties, clarsimp)
apply (drule_tac a=hJ and b=Some hR ⊕ hF in all3D, simp add: pa_ac, drule (1) all3_impD, clarsimp)
apply (subgoal_tac pdisj h' hR, erule_tac[2] pdisj_search)
apply (rule_tac y=hJ' and x=padd h' hR in ex2I, clarsimp simp add: pa_ac)
apply (drule mall4D, erule mimp4D, simp_all add: hsimps)
apply (erule (1) disjoint_search)
apply (subst assn_agrees, simp_all, fastforce)
done

theorem rule_frame:

Γ ⊢ {P} C {Q} ; disjoint (fvA R) (wrC C)

Γ ⊢ {P ** R} C {Q ** R}

by (auto simp add: CSL_def intro: safe_frame)

Conditional critical regions

lemma safe_inwith:

safe n C s h Γ (Q ** Γ r); wf_cmd (Cinwith r C)

safe n (Cinwith r C) s h Γ Q

apply (induct n arbitrary: C s h, simp_all, clarify)
apply (rule conjI)
apply (clarify, erule aborts.cases, simp_all, clarsimp)
apply (clarify, erule_tac red.cases, simp_all, clarify)
apply (frule (1) red_wf_cmd)
apply (drule allD, drule (1) all5_imp2D, simp_all)
apply (simp add: envs_def list_minus_removeAll [THEN sym] locked_eq)+
apply fast
apply (clarsimp simp add: envs_def, rename_tac hQ hJ)
apply (rule_tac x=hQ and y=hJ in ex2I, simp add: pa_ac, fast)
done

theorem rule_with:

Γ ⊢ {Aconj (P ** Γ r) (Apure B)} C {Q ** Γ r}

Γ ⊢ {P} Cwith r B C {Q}

apply (clarsimp simp add: CSL_def)
apply (case_tac n, simp, clarsimp)
apply (rule conjI, clarify, erule aborts.cases, simp_all)
apply (clarify, erule red.cases, simp_all, clarsimp)
apply (subgoal_tac pdisj h hJ, erule_tac[2] pdisj_search)
apply (simp add: envs_def, rule_tac x=padd h hJ in exI, simp add: pa_ac)
apply (rule safe_inwith, erule all3_impD, auto dest: user_cmdD)
done

Sequential composition

lemma safe_seq:

safe n C s h J Q; user_cmd C2;
∀m s' h'. m ≤ n ∧ (s', h') ⊨ Q ⟶ safe m C2 s' h' J R

safe n (Cseq C C2) s h J R

apply (induct n arbitrary: C s h l, simp, clarsimp)
apply (rule conjI, clarsimp)
apply (erule aborts.cases, simp_all, clarsimp)
apply (clarsimp, erule red.cases, simp_all)
— Seq1
apply (clarify, rule_tac x=h and y=hJ in ex2I, simp)
— Seq2
apply (clarify, drule all3D, drule (2) all3_imp2D, clarsimp)
apply (drule (1) mall3_impD, rule_tac x=h' and y=hJ' in ex2I, simp)
done

theorem rule_seq:

Γ ⊢ {P} C1 {Q} ; Γ ⊢ {Q} C2 {R}

Γ ⊢ {P} Cseq C1 C2 {R}

by (auto simp add: CSL_def intro!: safe_seq)

Conditionals (if-then-else)

theorem rule_if:

Γ ⊢ {Aconj P (Apure B)} C1 {Q} ;
Γ ⊢ {Aconj P (Apure (Bnot B))} C2 {Q}

Γ ⊢ {P} Cif B C1 C2 {Q}

apply (clarsimp simp add: CSL_def)
apply (case_tac n, simp, clarsimp)
apply (intro conjI allI impI notI, erule aborts.cases, simp_all)
apply (erule red.cases, simp_all)
apply (clarsimp, intro exI, (rule conjI, simp)+, simp)+
done

While

lemma safe_while:

Γ ⊢ {Aconj P (Apure B)} C {P} ; (s, h) ⊨ P

safe n (Cwhile B C) s h Γ (Aconj P (Apure (Bnot B)))

apply (induct n arbitrary: s h, simp, clarsimp)
apply (intro conjI allI impI notI, erule aborts.cases, simp_all)
apply (erule red.cases, simp_all)
apply (clarsimp, intro exI, (rule conjI, simp)+)
apply (subgoal_tac ∀m s h. m ≤ n ∧ (s, h) ⊨ P ⟶ safe m (Cwhile B C) s h Γ (Aconj P (Apure (Bnot B))))
apply (case_tac n, simp, clarsimp)
apply (intro conjI allI impI notI, erule aborts.cases, simp_all)
apply (erule red.cases, simp_all)
apply (clarsimp, intro exI, (rule conjI, simp)+)
apply (clarsimp simp add: CSL_def, rule safe_seq, blast, simp, clarsimp)
apply (clarsimp, intro exI, (rule conjI, simp)+, rule safe_skip, simp)
apply (clarsimp, drule (1) mall2_impD, erule (1) safe_mon)
done

theorem rule_while:

Γ ⊢ {Aconj P (Apure B)} C {P}

Γ ⊢ {P} Cwhile B C {Aconj P (Apure (Bnot B))}

by (auto simp add: CSL_def intro: safe_while)

Local variable declaration

lemma safe_inlocal:

safe n C (s(x:=v)) h Γ Q ; x ∉ fvA Q ∪ fvAs Γ

safe n (Cinlocal x v C) s h Γ Q

apply (induct n arbitrary: s h v C, simp, clarsimp)
apply (intro conjI allI impI notI, erule aborts.cases, simp_all, clarsimp)
apply (erule red.cases, simp_all)
apply (clarsimp, drule allD, drule (1) all5_imp2D, simp)
apply (clarsimp, intro exI, (rule conjI, simp)+, simp)
apply (fastforce simp add: safe_skip)
done

theorem rule_local:

Γ ⊢ {Aconj P (Apure (Beq (Evar x) E))} C {Q} ;
x ∉ fvA P ∪ fvA Q ∪ fvAs Γ ∪ fvE E

Γ ⊢ {P} Clocal x E C {Q}

apply (auto simp add: CSL_def intro: safe_inlocal)
apply (case_tac n, simp_all)
apply (intro conjI allI impI notI, erule aborts.cases, simp_all)
apply (erule red.cases, simp_all, clarsimp)
apply (intro exI conjI, simp_all, rule safe_inlocal, simp_all)
done

Basic commands (Assign, Read, Write, Alloc, Free)

theorem rule_assign:

x ∉ fvAs Γ

Γ ⊢ {subA x E Q} Cassign x E {Q}

apply (clarsimp simp add: CSL_def)
apply (case_tac n, simp, clarsimp)
apply (rule conjI, clarsimp, erule aborts.cases, simp_all)
apply (clarsimp, erule red.cases, simp_all)
apply (rule_tac x=h in exI, rule_tac x=hJ in exI,
clarsimp simp add: subA_assign)
done

lemma ptoheap_read:

ptoheap (Some h ⊕ hF) hh; h x = Some (v, k)

hh x = Some v

apply (case_tac hF, (simp add: ptoheap_def mypadd_def split: if_split_asm)+)
apply (drule_tac a=x in allD, fastforce simp add: padd_def split: option.splits)
done

theorem rule_read:

x ∉ fvE E ∪ fvE E' ∪ fvAs Γ

Γ ⊢ {Apsto k E E'} Cread x E {Aconj (Apsto k E E') (Apure (Beq (Evar x) E'))}

apply (clarsimp simp add: CSL_def)
apply (case_tac n, simp, clarsimp, intro conjI allI impI notI)
apply (erule aborts.cases, simp_all, fastforce dest: ptoheap_read)
apply (erule red.cases, simp_all, fastforce dest: ptoheap_read)
done

lemma pdisj_upd2:

h x = Some (w, pfull)

pdisj (h(x ↦ (v, pfull))) h' = pdisj h h'

by (simp add: pdisj_def, rule iff_allI, auto split: option.splits)

lemma write_helper:

ptoheap (Some h ⊕ hF) hh; h x = Some (v, pfull)

ptoheap (Some (h(x↦ (w, pfull))) ⊕ hF) (hh(x↦w))

apply (case_tac hF, simp_all add: ptoheap_def mypadd_def split: if_split_asm)
apply (clarsimp simp add: pdisj_upd2, simp add: pdisj_def, (drule_tac a=xa in allD)+)
apply (clarsimp simp add: pdisj_def padd_def split: option.splits)
done

theorem rule_write:

Γ ⊢ {E ⟼ E0} Cwrite E E' {E ⟼ E'}

apply (clarsimp simp add: CSL_def)
apply (case_tac n, simp, clarsimp simp add: fpdom_def, intro conjI allI impI notI)
apply (erule aborts.cases, simp_all, fastforce dest: ptoheap_read)
apply (erule red.cases, simp_all, fastforce elim: write_helper)
done

lemma alloc_helper:

ptoheap h hh; x ∉ dom hh

ptoheap (Some [x ↦ (v, pfull)] ⊕ h) (hh(x ↦ v))

apply (auto simp add: ptoheap_def mypadd_def pdisj_def padd_def split: option.splits)
apply (drule_tac a=xa in allD, simp)
done

theorem rule_alloc:

x ∉ fvE E ∪ fvAs Γ

Γ ⊢ {Aemp} Calloc x E {Evar x ⟼ E}

apply (clarsimp simp add: CSL_def)
apply (case_tac n, simp, clarsimp, intro conjI allI impI notI)
apply (erule aborts.cases, simp_all)
apply (erule red.cases, simp_all, fastforce elim: alloc_helper)
done

lemma free_helper:

ptoheap (Some h ⊕ hF) hh; h x = Some (v, pfull)

ptoheap (Some (h(x:=None)) ⊕ hF) (hh(x:=None))

apply (case_tac hF, simp_all add: ptoheap_def mypadd_def split: if_split_asm)
apply (clarsimp simp add: pdisj_def, (drule_tac a=xa in allD)+)
apply (clarsimp simp add: padd_def split: option.splits)
done

theorem rule_free:

Γ ⊢ {E ⟼ E0} Cdispose E {Aemp}

Simple structural rules (Conseq, Disj, Ex)

lemma safe_conseq:

safe n C s h Γ Q ; Q ⊑ Q'

safe n C s h Γ Q'

apply (induct n arbitrary: C s h, simp, clarsimp simp add: implies_def)
apply (drule allD, drule (2) all5_imp2D, simp_all, clarsimp)
apply (drule (1) mall3_impD, rule_tac x=h' and y=hJ' in ex2I, simp)
done

theorem rule_conseq:

Γ ⊢ {P} C {Q} ; P' ⊑ P ; Q ⊑ Q'

Γ ⊢ {P'} C {Q'}

by (fastforce simp add: CSL_def implies_def elim!: safe_conseq)

theorem rule_disj:

Γ ⊢ {P1} C {Q1}; Γ ⊢ {P2} C {Q2}

Γ ⊢ {Adisj P1 P2} C {Adisj Q1 Q2}

by (clarsimp simp add: CSL_def, safe)
(rule safe_conseq, simp_all add: implies_def, drule (2) all3_impD, force)+

theorem rule_ex:

∀n. (Γ ⊢ {P n} C {Q n})

Γ ⊢ {Aex P} C {Aex Q}

by (clarsimp simp add: CSL_def, rule_tac Q = Q v in safe_conseq,
auto simp add: implies_def)

Conjunction rule

lemma safe_conj:

safe n C s h Γ Q1;
safe n C s h Γ Q2;
∀r. precise (Γ r)

safe n C s h Γ (Aconj Q1 Q2)

apply (induct n arbitrary: C s h, simp, clarsimp)
apply (drule allD, drule (2) all5_imp2D, clarsimp)+
apply (rule_tac x=h' and y=hJ' in ex2I, simp)
apply (erule mall3_imp2D, simp_all)
apply (subgoal_tac Some hJ' ⊕ Some h' = Some hJ'a ⊕ Some h'a)
apply (subst (asm) (8 9) mypadd_def, simp split: if_split_asm)
apply (erule_tac[2] notE, erule_tac[2] pdisj_search)
apply (drule_tac s=a and y=h' and y'=h'a in preciseD [rotated], simp_all
add: envs_def precise_istar, fast)
apply (case_tac hF, simp add: ptoheap_def, clarsimp, rename_tac hR)
apply (drule (1) ptoD, rule_tac x=Some hR in pa_cancel, simp add: pa_ac)
apply (rule notI, simp add: pa_ac ptoheap_def)
done

theorem rule_conj:

Γ ⊢ {P1} C {Q1};
Γ ⊢ {P2} C {Q2};
∀r. precise (Γ r)

Γ ⊢ {Aconj P1 P2} C {Aconj Q1 Q2}

by (auto simp add: CSL_def intro: safe_conj)

Auxiliary variables

lemma safe_aux:

safe n C s h Γ Q; disjoint X (fvC (rem_vars X C) ∪ fvA Q ∪ fvAs Γ)

safe n (rem_vars X C) s h Γ Q

apply (induct n arbitrary: C s h, simp_all)
apply (intro conjI impI allI, clarsimp)
apply (fastforce intro: aborts_remvars)
apply (elim conjE, erule order_trans [OF accesses_remvars])
apply (clarsimp, frule red_properties, drule aux_red, simp_all)
apply (drule_tac a=Some hJ ⊕ hF in allD, simp add: pa_ac)
apply (clarsimp, drule allD, drule (2) all5_imp2D, clarsimp)
apply (intro exI conjI, simp+)
apply (fastforce simp add: disjoint_commute agreesC)
apply (drule (1) mall3_imp2D, fast)
apply (erule safe_agrees, fastforce simp add: disjoint_commute agreesC)
done

The proof rule for eliminating auxiliary variables. Note that a set of variables, X, is auxiliary for a command C iff it disjoint from fvC (rem_vars X C).

theorem rule_aux:

Γ ⊢ {P} C {Q} ;
disjoint X (fvA P ∪ fvA Q ∪ fvAs Γ ∪ fvC (rem_vars X C))

Γ ⊢ {P} rem_vars X C {Q}

by (auto simp add: CSL_def safe_aux disjoint_commute)

end