Theory CSLsound

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.

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)
(subst (1 2) map_add_comm, auto simp add: disjoint_def)

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: map_add_assoc [THEN sym])
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 (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, 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

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 ⇒ 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}

by (auto simp add: CSL_def)

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 (subst map_add_commute, 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,
         simp_all add: hsimps envs_app, clarsimp)
  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 (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=hR ++ hF and c=C' and d=s' and e=hh in all5D, simp add: hsimps)
  apply (clarsimp simp add: envs_upd)
  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 (clarsimp simp add: envs_def)
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 (subst map_add_commute, 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 (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 (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 (clarsimp simp add: CSL_def)
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)
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 (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 (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

theorem rule_read:

x ∉ fvE E ∪ fvE E' ∪ fvAs Γ

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

apply (clarsimp simp add: CSL_def)
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 (clarsimp simp add: CSL_def)
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)
apply (subst map_add_assoc [THEN sym], subst map_add_commute, simp add: hsimps)
apply (subst map_add_upd [THEN sym], simp add: hsimps del: map_add_upd)
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)
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)
apply (clarsimp simp add: map_add_upd_left disjoint_def)
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 (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 (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+)
— Read
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)
apply (fastforce simp add: disjoint_def)
— 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)
apply (rule map_add_upd_left [THEN sym], fastforce simp add: disjoint_def)
apply (fastforce simp add: disjoint_def)
— 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+)
apply (rule map_add_upd_left [THEN sym], fastforce simp add: disjoint_def)
apply (fastforce simp add: disjoint_def)
— 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)
apply (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