theory CSLsound
imports Main VHelper Lang
begin

This file contains a soundness proof for CSL (with multiple resources) as presented by O'Hearn and Brookes including the data-race freedom property of CSL. For simplicity, there is a slight difference regarding variable side-conditions: we do not allow resource-owned variables.

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

## Separation logic assertions

A deep embedding of separation logic assertions.

datatype assn =
Aemp — Empty heap
| Apointsto exp exp (infixl ⟼ 200) — 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 :: state ⇒ assn ⇒ bool (infixl ⊨ 60)
where
(σ ⊨ Aemp) = (snd σ = empty)
| (σ ⊨ E ⟼ E') = (dom (snd σ) = { edenot E (fst σ) } ∧ (snd σ) (edenot E (fst σ)) = Some (edenot E' (fst σ)))
| (σ ⊨ P ** Q) = (∃h1 h2. (fst σ, h1) ⊨ P ∧ (fst σ, h2) ⊨ Q ∧ snd σ = (h1 ++ h2) ∧ disjoint (dom h1) (dom 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)

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 σ = (h1 ++ h2)
∧ disjoint (dom h1) (dom h2))
apply (case_tac σ, rename_tac s h, clarify)
apply (induction l arbitrary: σ, auto)
apply (intro exI conjI, (simp add: hsimps)+)+
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. disjoint (dom h1) (dom h2) ∧ disjoint (dom h1') (dom h2')
∧ h1 ++ h2 = 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; x ++ y = x' ++ y';
disjoint (dom x) (dom y); disjoint (dom x') (dom y')
x = x' ∧ y = y'
unfolding precise_def
by (drule all5_impD, (erule conjI)+, simp_all, rule map_add_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?)+
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 σ = h1 ++ h2 ∧ disjoint (dom h1) (dom 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, substitutions

primrec
fvA :: assn ⇒ var set
where
fvA (Aemp) = {}
| fvA (Apure B) = fvB B
| fvA (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 (e1 ⟼ e2) = (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 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 ⇒ heap ⇒ (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. disjoint (dom h) (dom hF) ⟶ ¬ aborts C (s, h ++ hF))
∧ accesses C s ⊆ dom h
∧ (∀hJ hF C' σ'.
red C (s,h ++ hJ ++ hF) C' σ'
⟶ (s, hJ) ⊨ envs Γ (llocked C') (llocked C)
⟶ (disjoint (dom h) (dom hJ) ∧ disjoint (dom h) (dom hF) ∧ disjoint (dom hJ) (dom hF))
⟶ (∃h' hJ'.
snd σ' = h' ++ hJ' ++ hF
∧ disjoint (dom h') (dom hJ') ∧ disjoint (dom h') (dom hF) ∧ disjoint (dom hJ') (dom hF)
∧ (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) imp3D, simp, 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 (clarify, drule_tac X=fvC C ∪ fvAs Γ ∪ fvA Q in red_agrees,
simp (no_asm), fast, simp (no_asm), fast, clarify)
apply (drule (1) all5_impD, clarsimp)
apply (drule impD, erule assns_agreesE, simp add: agreesC, clarify)
apply (rule_tac x=h' and y=hJ' in ex2I, simp add: hsimps)
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 safe_par:
safe n C1 s h1 J Q1; safe n C2 s h2 J Q2;
wf_cmd (Cpar C1 C2);
disjoint (dom h1) (dom 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 (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: hsimps)
apply (clarify, drule_tac a=h2 ++ hF in all_impD, simp_all add: hsimps)
apply (clarify, drule_tac allD, drule_tac a=h1 ++ hF in all_impD, simp_all add: hsimps)
— no races
apply (clarsimp, erule notE, erule disjoint_search [rotated], erule disjoint_search,
erule order_trans [OF writes_accesses])+
— accesses
apply (rule conjI, erule order_trans, simp)+
— step
apply (clarsimp, erule red_par_cases)
— C1 does a step
apply (clarify, drule_tac a=hJ and b=h2 ++ hF in all2D, drule all3_impD,
simp_all add: hsimps envs_app locked_eq, clarsimp)
apply (rule_tac x=h' ++ h2 in exI, rule_tac x=hJ' in exI, simp add: hsimps)
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: hsimps, 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=h1 ++ hF in all2D, drule all3_imp2D,
apply (rule_tac x=h1 ++ h' in exI, rule_tac x=hJ' in exI, simp add: hsimps)
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: hsimps, simp)
apply (subst agreesC, fastforce, fastforce, fastforce)
— Par skip skip
apply (clarify)
apply (rule_tac x=h1 ++ h2 in exI, rule_tac x=hJ in exI, simp add: hsimps)
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 ⟶ disjoint (dom h) (dom hR) ⟶ (s,hR) ⊨ R ⟶ safe n (Cresource r C) s (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)
apply (rule conjI, clarify)
apply (rule conjI, clarify)
— no aborts
apply (erule aborts.cases, simp_all, clarsimp)
apply (drule_tac a=hR ++ hF in all_impD, simp, simp add: hsimps)
— accesses
apply (rule conjI, erule order_trans, simp)
— step
apply (clarify, frule red_properties, clarsimp)
apply (erule red.cases, simp_all, clarsimp, rename_tac C s C' s' hh)
— normal step
apply (case_tac r ∈ set (llocked C'), simp_all add: locked_eq)
apply (drule_tac a=hJ ++ hR and b=hF and c=C' and d=s' and e=hh in all5D, simp add: hsimps)
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=hR ++ hF and c=C' and d=s' and e=hh in all5D, simp add: hsimps)
apply (drule (1) mall3_imp2D, erule (1) red_wf_cmd)
apply (drule mimpD, fast, clarsimp)
apply (rule_tac x=h' ++ hR and y=hJ' in ex2I, simp add: hsimps)
apply (drule_tac a=hR in all_imp2D, simp_all add: hsimps)
apply (subst assn_agrees, simp_all, fastforce)
— skip
apply (rule_tac x=h ++ hR in exI, simp add: hsimps, 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 C' s' hh)
apply (drule_tac a=hJ and b=hF and c=C' and d=s' and e=hh in all5D, simp add: hsimps)
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, rename_tac hR' hJ')
apply (drule (2) all_imp2D, rule_tac x=h' ++ hR' and y=hJ' in ex2I, simp add: hsimps 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;
disjoint (dom h) (dom hR);
disjoint (fvA R) (wrC C);
(s,hR) ⊨ R
safe n C s (h ++ hR) J (Q ** R)
apply (induct n arbitrary: C s h hR, simp, clarsimp)
apply (rule conjI, clarify, fast)
apply (rule conjI, clarify)
— no aborts
apply (drule_tac a=hR ++ hF in all_impD, simp, simp add: hsimps)
— accesses
apply (rule conjI, erule order_trans, simp)
— step
apply (clarify, frule red_properties, clarsimp)
apply (drule_tac a=hJ and b=hR ++ hF in all3D, simp add: hsimps, drule (1) all2_impD, clarsimp)
apply (rule_tac y=hJ' and x=h' ++ hR in ex2I, clarsimp simp add: hsimps)
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 (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: hsimps, 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 (simp add: envs_def, rule_tac x=h ++ hJ in exI, simp)
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 (1) all5_impD, 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 (elim conjE)
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 (elim conjE, 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 (elim conjE, 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 (elim conjE, erule red.cases, simp_all)
apply (clarsimp, 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 (elim conjE, 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

x ∉ fvE E ∪ fvE E' ∪ fvAs Γ
Γ ⊢ {E ⟼ E'} Cread x E {Aconj (E ⟼ E') (Apure (Beq (Evar x) E'))}
apply (case_tac n, simp, clarsimp)
apply (rule conjI)
apply (clarsimp, erule aborts.cases, simp_all, clarsimp simp add: dom_def)
apply (clarify, erule red.cases, simp_all, elim exE conjE, hypsubst)
apply (rule_tac x=h in exI, rule_tac x=hJ in exI, clarsimp)
apply (simp add: disjoint_def, clarsimp, elim disjE, clarsimp+)
done

theorem rule_write:
Γ ⊢ {E ⟼ E0} Cwrite E E' {E ⟼ E'}
apply (case_tac n, simp, clarsimp)
apply (rule conjI)
apply (clarsimp, erule aborts.cases, simp_all, clarsimp simp add: dom_def)
apply (clarify, erule red.cases, simp_all, clarsimp)
apply (rule_tac x=h(edenot E sa ↦ edenot E' sa) in exI, rule_tac x=hJ in exI, simp)
apply (rule conjI [rotated], clarsimp)
done

theorem rule_alloc:
x ∉ fvE E ∪ fvAs Γ
Γ ⊢ {Aemp} Calloc x E {Evar x ⟼ E}
apply (case_tac n, simp, clarsimp)
apply (rule conjI, clarsimp, erule aborts.cases, simp_all)
apply (clarify)
apply (erule red.cases, simp_all)
apply (rule_tac x=Map.empty(v ↦ edenot E s) in exI, rule_tac x=hJ in exI, simp)
apply (elim conjE, hypsubst, simp, elim conjE)
done

theorem rule_free:
Γ ⊢ {E ⟼ E0} Cdispose E {Aemp}
apply (case_tac n, simp, clarsimp)
apply (rule conjI)
apply (clarsimp, erule aborts.cases, simp_all, clarsimp simp add: dom_def)
apply (clarify, erule red.cases, simp_all, clarsimp)
apply (rule_tac x=h(edenot E sa := None) in exI, rule_tac x=hJ in exI, simp)
apply (clarsimp, rule ext, simp, clarify, erule dom_eqD, simp)
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 (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 (1) all5_impD, clarsimp)+
apply (rule_tac x=h' and y=hJ' in ex2I, simp)
apply (erule mall3_imp2D, simp_all, drule map_add_cancel, simp_all)
apply (drule_tac s=a and y=h' and y'=h'a in preciseD [rotated], simp_all add: hsimps)
apply (auto simp add: envs_def precise_istar)
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=hJ ++ hF in allD, simp add: hsimps)
apply (clarsimp, 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)

## Alternative definition of configuration safety

Here is an alternative definition of safety monotonicity that does not quantify over the frame hF.

primrec
safe_weak :: nat ⇒ cmd ⇒ stack ⇒ heap ⇒ (rname ⇒ assn) ⇒ assn ⇒ bool
where
safe_weak 0 C s h Γ Q = True
| safe_weak (Suc n) C s h Γ Q = (
(C = Cskip ⟶ (s, h) ⊨ Q)
∧ ¬ aborts C (s, h)
∧ accesses C s ⊆ dom h
∧ (∀hJ C' σ'.
red C (s,h ++ hJ) C' σ'
⟶ (s, hJ) ⊨ envs Γ (llocked C') (llocked C)
⟶ (disjoint (dom h) (dom hJ))
⟶ (∃h' hJ'.
snd σ' = h' ++ hJ'
∧ disjoint (dom h') (dom hJ')
∧ (fst σ', hJ') ⊨ envs Γ (llocked C) (llocked C')
∧ safe_weak n C' (fst σ') h' Γ Q)))

It is easy to show that the alternative definition is weaker than the one with the quantification:

lemma safe_weakI:
safe n C s h Γ Q
safe_weak n C s h Γ Q
apply (induct n arbitrary: C s h, simp, clarsimp)
apply (rule conjI, drule_tac a=empty in allD, simp)
apply (clarify, drule_tac b=empty in all5D, simp, drule (2) imp2D, fast)
done

If, however, the operational semantics satisfies the safety monotonicity and frame properties (which it does), then the two definitions are equivalent. We first prove that the operational semantics satisfies these two properties, and then using these properties, we show that the alternative definition of configuration safety implies the original one.

[A] Safety monotonicity:

lemma safety_monotonicity_helper[rule_format]:
aborts C σ ⟹ ∀s h hF. σ = (s, h ++ hF) ⟶ disjoint (dom h) (dom hF) ⟶ aborts C (s, h)
by (erule aborts.induct, auto)

lemma safety_monotonicity:
aborts C (s, h ++ hF); disjoint (dom h) (dom hF)
aborts C (s, h)
by (erule safety_monotonicity_helper, simp_all)

[B] Frame property:

lemma frame_property_helper[rule_format]:
red C σ C' σ' ⟹ ∀s h hF s' h''. σ = (s, h ++ hF) ⟶ σ' = (s', h'')
⟶ disjoint (dom h) (dom hF)
⟶ ¬ aborts C (s, h)
⟶ (∃h'. red C (s, h) C' (s', h') ∧ h'' = h' ++ hF ∧ disjoint (dom h') (dom hF))
apply (erule red.induct, fastforce+)
apply (clarsimp, rename_tac h hF)
apply (case_tac h (edenot E s), erule notE, fastforce)
apply (intro exI conjI red_Read, fast+, simp_all)
— Write
apply (clarsimp, rename_tac h hF)
apply (case_tac h (edenot E s), erule notE, fastforce)
apply (rule_tac x=h(edenot E s ↦ edenot E' s) in exI, intro conjI, fast)
— Alloc
apply (clarsimp, rename_tac h hF)
apply (rule_tac x=h(v ↦ edenot E s) in exI, intro conjI)
apply (rule_tac v=v in red_Alloc, fast+)
— Dispose
apply (clarsimp, rename_tac h hF)
apply (case_tac h (edenot E s), erule notE, fastforce)
apply (rule_tac x=h(edenot E s := None) in exI, intro conjI, fast)
apply (subgoal_tac hF(edenot E s := None) = hF, simp, rule ext, fastforce simp add: disjoint_def)
done

lemma frame_property:
red C (s, h ++ hF) C' (s', h''); disjoint (dom h) (dom hF); ¬ aborts C (s, h)
∃h'. red C (s, h) C' (s', h') ∧ h'' = h' ++ hF ∧ disjoint (dom h') (dom hF)
by (erule frame_property_helper, simp_all)

Finally, using safety monotonicity and the frame property, we conclude that safe_weak n C s h Γ Q implies safe n C s h Γ Q.

lemma safe_weakE:
safe_weak n C s h Γ Q
safe n C s h Γ Q
apply (induct n arbitrary: C s h, simp, clarsimp)
apply (rule conjI, clarify)
apply (erule notE, erule (1) safety_monotonicity)
apply (clarify, drule frame_property, simp)
apply (erule contrapos_nn, erule (1) safety_monotonicity, clarify)
apply (drule (2) all4_imp2D, clarsimp, fast)
done

end
Imprint | Data protection | HTML version generated by isa2html.