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
(λ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)

pdisj x y

pdisj y z ; pdisj x (padd y z)
(pdisj x y ∧ pdisj x z)
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

pdisj y (padd x z); pdisj x z
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

pdisj x y
pdisj (padd x y) z = (pdisj x (padd y z) ∧ pdisj y z)
apply (simp add: pdisj_comm, rule iffI)
done

pdisj x (padd y z) ; pdisj y z
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

pdisj x (padd y z) ; pdisj y z
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=bf in frac_pos, simp)
done

padd x y = padd x z ; pdisj x y; pdisj x z
y = z
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

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

pdisj h1 h2
fpdom h1 ⊆ fpdom (padd h1 h2)
pdisj h1 h2
fpdom h2 ⊆ fpdom (padd h1 h2)
apply (drule_tac a=x in allD, fastforce)+
done

lemma pa_empty[simp]:
x ⊕ Some Map.empty = x
Some Map.empty ⊕ x = x

lemma pa_none[simp]:
x ⊕ None = None
None ⊕ x = None

lemma pa_comm:
y ⊕ x = x ⊕ y

lemma pa_assoc:
(x ⊕ y) ⊕ z = x ⊕ y ⊕ z
apply (erule notE, fast)
done

lemma pa_left_comm:
y ⊕ x ⊕ z = x ⊕ y ⊕ z
apply (erule_tac[!] notE, (erule (1) pdisj_padd_comm |erule (1) pdisjE)+)
done

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

lemmas pa_ac = pa_comm pa_assoc pa_left_comm some_padd

lemma pa_cancel:
x ⊕ y = x ⊕ z; x ⊕ y ≠ None
y = z
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 (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

datatype assn =
Aemp — Empty heap
| Apsto myfrac exp exp — Singleton heap
| Astar assn assn (infixl ** 100) — Separating conjunction
| Awand assn assn — Separating implication
| Apure bexp — Pure assertion
| Aconj assn assn — Conjunction
| Adisj assn assn — Disjunction
| Aex (nat ⇒ assn) — Existential quantification

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))

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 (intro exI conjI, simp+)
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 (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 (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'

lemma envs_removeAll_irr:
r ∉ set l
envs Γ l (removeAll r l') = envs Γ l l'

lemma envs_removeAll2:
r ∈ set l'
envs Γ (removeAll r l) (removeAll r l') = envs Γ l l'

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)

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

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}

### 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,
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 (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,
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 (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,
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 (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 (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 (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)
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 (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,
done

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

x ∉ fvE E ∪ fvE E' ∪ fvAs Γ
Γ ⊢ {Apsto k E E'} Cread x E {Aconj (Apsto k E E') (Apure (Beq (Evar x) E'))}
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 (clarsimp simp add: pdisj_upd2, simp add: pdisj_def, (drule_tac a=xa in allD)+)
done

theorem rule_write:
Γ ⊢ {E ⟼ E0} Cwrite E E' {E ⟼ E'}
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 (drule_tac a=xa in allD, simp)
done

theorem rule_alloc:
x ∉ fvE E ∪ fvAs Γ
Γ ⊢ {Aemp} Calloc x E {Evar x ⟼ E}
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 (clarsimp simp add: pdisj_def, (drule_tac a=xa in allD)+)
done

theorem rule_free:
Γ ⊢ {E ⟼ E0} Cdispose E {Aemp}
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: free_helper dom_eqD)
done

### 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}
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,

### 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
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
Imprint | Data protection | HTML version generated by isa2html.