Theory TypeSystem
section ‹Type System for Ensuring SIFUM-Security of Commands›
theory TypeSystem
imports Compositionality Language
begin
subsection ‹Typing Rules›
text ‹
Types now depend on memories. To see why, consider an assignment in which some variable
@{term x} for which we have a @{term AsmNoReadOrWrite} assumption is assigned the value in
variable @{term input}, but where @{term input}'s classification depends on some control
variable. Then the new type of @{term x} depends on memory. If we were to just take the
upper bound of @{term input}'s classification, this would likely give us @{term High} as
@{term x}'s type, but that would prevent us from treating @{term x} as @{term Low}
if we later learn @{term input}'s original classification.
Instead we need to make @{term x}'s type explicitly depend on memory so later on, once we
learn @{term input}'s classification, we can resolve @{term x}'s type to a concrete
security level.
We choose to deeply embed types as sets of boolean expressions. If any expression in the
set evaluates to @{term True}, the type is @{term High}; otherwise it is @{term Low}.
›
type_synonym 'BExp Type = "'BExp set"
text ‹
We require @{term Γ} to track all stable (i.e. @{term AsmNoWrite} or @{term AsmNoReadOrWrite}),
non-@{term 𝒞} variables.
This differs from Mantel a bit. Mantel would exclude from @{term Γ}, variables
whose classification (according to @{term dma}) is @{term Low} for which we have only
an @{term AsmNoWrite} assumption.
We decouple the requirement for inclusion in @{term Γ} from a variable's classification
so that we don't need to be updating @{term Γ} each time we alter a control variable.
Even if we tried to keep @{term Γ} up-to-date in that case, we may not be able to
precisely compute the new classification of each variable after the modification anyway.
›
type_synonym ('Var,'BExp) TyEnv = "'Var ⇀ 'BExp Type"
text ‹
This records which variables are \emph{stable} in that we have an assumption
implying that their value won't change. It duplicates a bit of info in
@{term Γ} above but I haven't yet thought of a way to remove that duplication
cleanly.
The first component of the pair records variables for which we have
@{term AsmNoWrite}; the second component is for @{term AsmNoReadOrWrite}.
The reason we want to distinguish the different kinds of assumptions is to know whether
a variable should remain in @{term Γ} when we drop an assumption on it. If we drop
e.g. @{term AsmNoWrite} but also have @{term AsmNoReadOrWrite} then if we didn't track
stability info this way we wouldn't know whether we had to remove the variable from
@{term Γ} or not.
›
type_synonym 'Var Stable = "('Var set × 'Var set)"
text ‹
We track a set of predicates on memories as we execute. If we evaluate a boolean expression
all of whose variables are stable, then we enrich this set predicate with that one.
If we assign to a stable variable, then we enrich this predicate also.
If we release an assumption making a variable unstable, we need to remove all predicates that
pertain to it from this set.
This needs to be deeply embedded (i.e. it cannot be stored as a predicate of type
@{typ "('Var,'Val) Mem ⇒ bool"} or even @{typ "('Var,'Val) Mem set"}), because we need to be
able to identify each individual predicate and for each predicate identify all of the
variables in it, so we can discard the right predicates each time a variable becomes unstable.
›
type_synonym 'bexp preds = "'bexp set"
context sifum_lang_no_dma begin
definition
pred :: "'BExp preds ⇒ ('Var,'Val) Mem ⇒ bool"
where
"pred P ≡ λmem. (∀p∈P. eval⇩B mem p)"
end
locale sifum_types =
sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars + sifum_security dma 𝒞_vars 𝒞 eval⇩w undefined
for ev⇩A :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
and ev⇩B :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
and aexp_vars :: "'AExp ⇒ 'Var set"
and bexp_vars :: "'BExp ⇒ 'Var set"
and dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
and 𝒞_vars :: "'Var ⇒ 'Var set"
and 𝒞 :: "'Var set" +
fixes bexp_neg :: "'BExp ⇒ 'BExp"
assumes bexp_neg_negates: "⋀mem e. (ev⇩B mem (bexp_neg e)) = (¬ (ev⇩B mem e))"
fixes assign_post :: "'BExp preds ⇒ 'Var ⇒ 'AExp ⇒ 'BExp preds"
assumes assign_post_valid: "⋀mem. pred P mem ⟹ pred (assign_post P x e) (mem(x := ev⇩A mem e))"
fixes dma_type :: "'Var ⇒ 'BExp set"
assumes dma_correct:
"dma mem x = (if (∀e∈dma_type x. ev⇩B mem e) then Low else High)"
assumes 𝒞_vars_correct:
"𝒞_vars x = (⋃(bexp_vars ` dma_type x))"
fixes pred_False :: 'BExp
assumes pred_False_is_False: "¬ ev⇩B mem pred_False"
assumes bexp_vars_pred_False: "bexp_vars pred_False = {}"
locale sifum_types_assign =
sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars + sifum_security dma 𝒞_vars 𝒞 eval⇩w undefined
for ev⇩A :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
and ev⇩B :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
and aexp_vars :: "'AExp ⇒ 'Var set"
and bexp_vars :: "'BExp ⇒ 'Var set"
and dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
and 𝒞_vars :: "'Var ⇒ 'Var set"
and 𝒞 :: "'Var set" +
fixes bexp_neg :: "'BExp ⇒ 'BExp"
assumes bexp_neg_negates: "⋀mem e. (ev⇩B mem (bexp_neg e)) = (¬ (ev⇩B mem e))"
fixes dma_type :: "'Var ⇒ 'BExp set"
assumes dma_correct:
"dma mem x = (if (∀e∈dma_type x. ev⇩B mem e) then Low else High)"
assumes 𝒞_vars_correct:
"𝒞_vars x = (⋃(bexp_vars ` dma_type x))"
fixes pred_False :: 'BExp
assumes pred_False_is_False: "¬ ev⇩B mem pred_False"
assumes bexp_vars_pred_False: "bexp_vars pred_False = {}"
fixes bexp_assign :: "'Var ⇒ 'AExp ⇒ 'BExp"
assumes bexp_assign_eval: "⋀mem e x. (ev⇩B mem (bexp_assign x e)) = (mem x = (ev⇩A mem e))"
assumes bexp_assign_vars: "⋀e x. (bexp_vars (bexp_assign x e)) = aexp_vars e ∪ {x}"
context sifum_lang_no_dma begin
definition
stable :: "'Var Stable ⇒ 'Var ⇒ bool"
where
"stable 𝒮 x ≡ x ∈ (fst 𝒮 ∪ snd 𝒮)"
definition
add_pred :: "'BExp preds ⇒ 'Var Stable ⇒ 'BExp ⇒ 'BExp preds" ("_ +⇩_ _" [120, 120, 120] 1000)
where
"P +⇩𝒮 e ≡ (if (∀x∈bexp_vars e. stable 𝒮 x) then P ∪ {e} else P)"
lemma add_pred_subset:
"P ⊆ P +⇩𝒮 p"
apply(clarsimp simp: add_pred_def)
done
definition
restrict_preds_to_vars :: "'BExp preds ⇒ 'Var set ⇒ 'BExp preds" ("_ |` _" [120, 120] 1000)
where
"P |` V ≡ {e. e ∈ P ∧ bexp_vars e ⊆ V}"
end
context sifum_types_assign begin
text ‹
the most simple assignment postcondition transformer
›
definition
assign_post :: "'BExp preds ⇒ 'Var ⇒ 'AExp ⇒ 'BExp preds"
where
"assign_post P x e ≡
(if x ∈ (aexp_vars e) then
(restrict_preds_to_vars P (-{x}))
else
(restrict_preds_to_vars P (-{x})) ∪ {bexp_assign x e})"
end
sublocale sifum_types_assign ⊆ sifum_types _ _ _ _ _ _ _ _ assign_post
apply(unfold_locales)
using bexp_neg_negates apply blast
apply(clarsimp simp: assign_post_def pred_def | safe)+
using eval_vars_det⇩B
unfolding restrict_preds_to_vars_def
apply (metis (mono_tags, lifting) ComplD fun_upd_other mem_Collect_eq singletonI subset_eq)
unfolding bexp_assign_eval
using eval_vars_det⇩A
apply fastforce
using eval_vars_det⇩B
apply (metis (mono_tags, lifting) ComplD fun_upd_other mem_Collect_eq singletonI subset_eq)
using dma_correct apply blast
using 𝒞_vars_correct pred_False_is_False bexp_vars_pred_False apply blast+
done
context sifum_types
begin
abbreviation
mm_equiv_abv2 :: "(_, _, _) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
(infix "≈" 60)
where
"mm_equiv_abv2 c c' ≡ mm_equiv_abv c c'"
abbreviation
eval_abv2 :: "(_, 'Var, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
(infixl "↝" 70)
where
"x ↝ y ≡ (x, y) ∈ eval⇩w"
abbreviation
eval_plus_abv :: "(_, 'Var, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
(infixl "↝⇧+" 70)
where
"x ↝⇧+ y ≡ (x, y) ∈ eval⇩w⇧+"
abbreviation
no_eval_abv :: "(_, 'Var, 'Val) LocalConf ⇒ bool"
("_ ↝ ⊥")
where
"x ↝ ⊥ ≡ ∀ y. (x, y) ∉ eval⇩w"
abbreviation
low_indistinguishable_abv :: "'Var Mds ⇒ ('Var, 'AExp, 'BExp) Stmt ⇒ (_, _, _) Stmt ⇒ bool"
("_ ∼ı _" [100, 100] 80)
where
"c ∼⇘mds⇙ c' ≡ low_indistinguishable mds c c'"
abbreviation
vars_of_type :: "'BExp Type ⇒ 'Var set"
where
"vars_of_type t ≡ ⋃(bexp_vars ` t)"
definition
type_wellformed :: "'BExp Type ⇒ bool"
where
"type_wellformed t ≡ vars_of_type t ⊆ 𝒞"
lemma dma_type_wellformed [simp]:
"type_wellformed (dma_type x)"
apply(clarsimp simp: type_wellformed_def 𝒞_def | safe)+
using 𝒞_vars_correct apply blast
done
definition
to_total :: "('Var,'BExp) TyEnv ⇒ 'Var ⇒ 'BExp Type"
where
"to_total Γ ≡ λv. if v ∈ dom Γ then the (Γ v) else dma_type v"
definition
types_wellformed :: "('Var,'BExp) TyEnv ⇒ bool"
where
"types_wellformed Γ ≡ ∀x∈dom Γ. type_wellformed (the (Γ x))"
lemma to_total_type_wellformed:
"types_wellformed Γ ⟹
type_wellformed (to_total Γ x)"
by(auto simp: to_total_def types_wellformed_def)
lemma Un_type_wellformed:
"∀t∈ts. type_wellformed t ⟹ type_wellformed (⋃ ts)"
apply(clarsimp simp: type_wellformed_def | safe)+
by(fastforce simp: 𝒞_def elim!: subsetCE)
inductive
type_aexpr :: "('Var,'BExp) TyEnv ⇒ 'AExp ⇒ 'BExp Type ⇒ bool" ("_ ⊢⇩a _ ∈ _" [120, 120, 120] 1000)
where
type_aexpr [intro!]: "Γ ⊢⇩a e ∈ ⋃ (image (λ x. to_total Γ x) (aexp_vars e))"
lemma type_aexprI:
"t = ⋃ (image (λ x. to_total Γ x) (aexp_vars e)) ⟹ Γ ⊢⇩a e ∈ t"
apply(erule ssubst)
apply(rule type_aexpr.intros)
done
lemma type_aexpr_type_wellformed:
"types_wellformed Γ ⟹ Γ ⊢⇩a e ∈ t ⟹ type_wellformed t"
apply(erule type_aexpr.cases)
apply(erule ssubst, rule Un_type_wellformed)
apply clarsimp
apply(blast intro: to_total_type_wellformed)
done
inductive_cases type_aexpr_elim [elim]: "Γ ⊢⇩a e ∈ t"
inductive
type_bexpr :: "('Var,'BExp) TyEnv ⇒ 'BExp ⇒ 'BExp Type ⇒ bool" ("_ ⊢⇩b _ ∈ _ " [120, 120, 120] 1000)
where
type_bexpr [intro!]: "Γ ⊢⇩b e ∈ ⋃ (image (λ x. to_total Γ x) (bexp_vars e))"
lemma type_bexprI:
"t = ⋃ (image (λ x. to_total Γ x) (bexp_vars e)) ⟹ Γ ⊢⇩b e ∈ t"
apply(erule ssubst)
apply(rule type_bexpr.intros)
done
lemma type_bexpr_type_wellformed:
"types_wellformed Γ ⟹ Γ ⊢⇩b e ∈ t ⟹ type_wellformed t"
apply(erule type_bexpr.cases)
apply(erule ssubst, rule Un_type_wellformed)
apply clarsimp
apply(blast intro: to_total_type_wellformed)
done
inductive_cases type_bexpr_elim [elim]: "Γ ⊢⇩b e ∈ t"
text ‹
Define a sufficient condition for a type to be stable, assuming the type is wellformed.
We need this because there is no point tracking the fact that e.g. variable @{term x}'s data has
a classification that depends on some control variable @{term c} (where @{term c} might be
the control variable for some other variable @{term y} whose value we've just assigned to
@{term x}) if @{term c} can then go and be modified, since now the classification of
the data in @{term x} no longer depends on the value of @{term c}, instead it depends on
@{term c}'s \emph{old} value, which has now been lost.
Therefore, if a type depends on @{term c}, then @{term c} had better be stable.
›
abbreviation
pred_stable :: "'Var Stable ⇒ 'BExp ⇒ bool"
where
"pred_stable 𝒮 p ≡ ∀x∈bexp_vars p. stable 𝒮 x"
abbreviation
type_stable :: "'Var Stable ⇒ 'BExp Type ⇒ bool"
where
"type_stable 𝒮 t ≡ (∀p∈t. pred_stable 𝒮 p)"
lemma type_stable_is_sufficient:
"⟦type_stable 𝒮 t⟧ ⟹
∀mem mem'. (∀x. stable 𝒮 x ⟶ mem x = mem' x) ⟶ (ev⇩B mem) ` t = (ev⇩B mem') ` t"
apply(clarsimp simp: type_wellformed_def image_def)
apply safe
using eval_vars_det⇩B apply blast+
done
definition
mds_consistent :: "'Var Mds ⇒ ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ bool"
where
"mds_consistent mds Γ 𝒮 P ≡
(𝒮 = (mds AsmNoWrite, mds AsmNoReadOrWrite)) ∧
(dom Γ = {x. x ∉ 𝒞 ∧ stable 𝒮 x}) ∧
(∀p ∈ P. pred_stable 𝒮 p)"
fun
add_anno_dom :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'Var ModeUpd ⇒ 'Var set"
where
"add_anno_dom Γ 𝒮 (Acq v AsmNoReadOrWrite) = (if v ∉ 𝒞 then dom Γ ∪ {v} else dom Γ)" |
"add_anno_dom Γ 𝒮 (Acq v AsmNoWrite) = (if v ∉ 𝒞 then dom Γ ∪ {v} else dom Γ)" |
"add_anno_dom Γ 𝒮 (Acq v _) = dom Γ" |
"add_anno_dom Γ 𝒮 (Rel v AsmNoReadOrWrite) = (if v ∉ fst 𝒮 then dom Γ - {v} else dom Γ)" |
"add_anno_dom Γ 𝒮 (Rel v AsmNoWrite) = (if v ∉ snd 𝒮 then dom Γ - {v} else dom Γ)" |
"add_anno_dom Γ 𝒮 (Rel v _) = dom Γ"
definition
add_anno :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'Var ModeUpd ⇒ ('Var,'BExp) TyEnv" ("_ ⊕⇩_ _" [120, 120, 120] 1000)
where
"Γ ⊕⇩𝒮 upd = restrict_map (λx. Some (to_total Γ x)) (add_anno_dom Γ 𝒮 upd)"
lemma add_anno_acq_AsmNoReadOrWrite_idemp [simp]:
"v ∈ dom Γ ∨ v ∈ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoReadOrWrite) = Γ"
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(rule ext)
apply(clarsimp simp: restrict_map_def | safe)+
apply(case_tac "Γ x", fastforce+)[5]
apply(rule ext)
apply(clarsimp simp: restrict_map_def | safe)+
apply(case_tac "Γ x", fastforce+)
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(rule ext)
apply(clarsimp simp: restrict_map_def | safe)+
apply(case_tac "Γ x", fastforce+)
done
lemma add_anno_rel_AsmNoReadOrWrite_idemp [simp]:
"⟦v ∉ dom Γ; v ∉ fst 𝒮⟧ ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoReadOrWrite) = Γ"
apply(subgoal_tac "v ∉ dom Γ")
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(clarsimp simp: restrict_map_def | safe)+
apply(erule_tac P="(λx. if x ∈ dom Γ ∧ x ≠ v
then Some (if x ∈ dom Γ then the (Γ x) else dma_type x) else None) = Γ" in notE)
apply(rule ext)
apply(case_tac "Γ x", fastforce+)
done
lemma add_anno_acq_AsmNoReadOrWrite [simp]:
assumes notin [simp]: "v ∉ dom Γ"
shows "v ∉ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoReadOrWrite) = (Γ(v ↦ dma_type v))"
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(clarsimp simp: restrict_map_def | safe)+
apply(rule ext)
apply(auto intro: sym)
done
lemma add_anno_rel_AsmNoReadOrWrite [simp]:
assumes isin [simp]: "v ∈ dom Γ"
shows "v ∉ fst 𝒮 ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoReadOrWrite) = restrict_map Γ ((dom Γ) - {v})"
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(clarsimp simp: restrict_map_def | safe)+
apply(rule ext)
apply(auto intro: sym)
done
lemma add_anno_acq_AsmNoWrite_idemp [simp]:
"v ∈ dom Γ ∨ v ∈ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoWrite) = Γ"
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(rule ext)
apply(clarsimp simp: restrict_map_def | safe)+
apply(case_tac "Γ x", fastforce+)[5]
apply(rule ext)
apply(clarsimp simp: restrict_map_def | safe)+
apply(case_tac "Γ x", fastforce+)
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(rule ext)
apply(clarsimp simp: restrict_map_def | safe)+
apply(case_tac "Γ x", fastforce+)
done
lemma add_anno_rel_AsmNoWrite_idemp [simp]:
"⟦v ∉ dom Γ; v ∉ snd 𝒮⟧ ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoWrite) = Γ"
apply(subgoal_tac "v ∉ dom Γ")
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(clarsimp simp: restrict_map_def | safe)+
apply(erule_tac P="(λx. if x ∈ dom Γ ∧ x ≠ v
then Some (if x ∈ dom Γ then the (Γ x) else dma_type x) else None) = Γ" in notE)
apply(rule ext)
apply(case_tac "Γ x", fastforce+)
done
lemma add_anno_acq_AsmNoWrite [simp]:
assumes notin [simp]: "v ∉ dom Γ"
shows "v ∉ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoWrite) = (Γ(v ↦ dma_type v))"
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(clarsimp simp: restrict_map_def | safe)+
apply(rule ext)
apply(auto intro: sym)
done
lemma add_anno_rel_AsmNoWrite [simp]:
assumes isin [simp]: "v ∈ dom Γ"
shows "v ∉ snd 𝒮 ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoWrite) = restrict_map Γ ((dom Γ) - {v})"
apply(safe | clarsimp simp: add_anno_def to_total_def)+
apply(clarsimp simp: restrict_map_def | safe)+
apply(rule ext)
apply(auto intro: sym)
done
fun
add_anno_stable :: "'Var Stable ⇒ 'Var ModeUpd ⇒ 'Var Stable"
where
"add_anno_stable 𝒮 (Acq v AsmNoReadOrWrite) = (fst 𝒮, snd 𝒮 ∪ {v})" |
"add_anno_stable 𝒮 (Acq v AsmNoWrite) = (fst 𝒮 ∪ {v}, snd 𝒮)" |
"add_anno_stable 𝒮 (Acq v _) = 𝒮" |
"add_anno_stable 𝒮 (Rel v AsmNoReadOrWrite) = (fst 𝒮, snd 𝒮 - {v})" |
"add_anno_stable 𝒮 (Rel v AsmNoWrite) = (fst 𝒮 - {v}, snd 𝒮)" |
"add_anno_stable 𝒮 (Rel v _) = 𝒮"
definition
pred_entailment :: "'BExp preds ⇒ 'BExp preds ⇒ bool" (infix "⊢" 70)
where
"P ⊢ P' ≡ ∀mem. pred P mem ⟶ pred P' mem"
text ‹
We give a predicate interpretation of subtype and then prove it has the correct
semantic property.
›
definition
subtype :: "'BExp Type ⇒ 'BExp preds ⇒ 'BExp Type ⇒ bool" ("_ ≤:⇩_ _" [120, 120, 120] 1000)
where
"t ≤:⇩P t' ≡ (P ∪ t') ⊢ t"
definition
type_max :: "'BExp Type ⇒ ('Var,'Val) Mem ⇒ Sec"
where
"type_max t mem ≡ if (∀p∈t. ev⇩B mem p) then Low else High"
lemma type_stable_is_sufficient':
"⟦type_stable 𝒮 t⟧ ⟹
∀mem mem'. (∀x. stable 𝒮 x ⟶ mem x = mem' x) ⟶ type_max t mem = type_max t mem'"
using type_stable_is_sufficient
unfolding type_max_def image_def
by (metis (no_types, lifting) eval_vars_det⇩B)
lemma subtype_sound:
"t ≤:⇩P t' ⟹ ∀mem. pred P mem ⟶ type_max t mem ≤ type_max t' mem"
apply(fastforce simp: subtype_def pred_entailment_def pred_def type_max_def less_eq_Sec_def)
done
lemma subtype_complete:
assumes a: "⋀mem. pred P mem ⟹ type_max t mem ≤ type_max t' mem"
shows "t ≤:⇩P t'"
unfolding subtype_def pred_entailment_def
proof (clarify)
fix mem
assume p: "pred (P ∪ t') mem"
hence "pred P mem"
unfolding pred_def by blast
with a have tmax: "type_max t mem ≤ type_max t' mem" by blast
from p have t': "pred t' mem"
unfolding pred_def by blast
from t' have "type_max t' mem = Low"
unfolding type_max_def pred_def by force
with tmax have "type_max t mem ≤ Low"
by simp
hence "type_max t mem = Low"
unfolding less_eq_Sec_def by blast
thus "pred t mem"
unfolding type_max_def pred_def by (auto split: if_splits)
qed
lemma subtype_correct:
"(t ≤:⇩P t') = (∀mem. pred P mem ⟶ type_max t mem ≤ type_max t' mem)"
apply(rule iffI)
apply(simp add: subtype_sound)
apply(simp add: subtype_complete)
done
definition
type_equiv :: "'BExp Type ⇒ 'BExp preds ⇒ 'BExp Type ⇒ bool" ("_ =:⇩_ _" [120, 120, 120] 1000)
where
"t =:⇩P t' ≡ t ≤:⇩P t' ∧ t' ≤:⇩P t"
lemma subtype_refl [simp]:
"t ≤:⇩P t"
by(simp add: subtype_def pred_entailment_def pred_def)
lemma type_equiv_refl [simp]:
"t =:⇩P t"
by (simp add: type_equiv_def)
definition
anno_type_stable :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'Var ModeUpd ⇒ bool"
where
"anno_type_stable Γ 𝒮 upd ≡ (case upd of (Rel v m) ⇒
(v ∈ 𝒞 ∧ v ∉ add_anno_dom Γ 𝒮 upd) ⟶
(∀x∈dom Γ. v ∉ vars_of_type (the (Γ x)))
| (Acq v m) ⇒
(v ∉ 𝒞 ∧ v∈add_anno_dom Γ 𝒮 upd - dom Γ) ⟶
(∀x∈𝒞_vars v. stable 𝒮 x))"
definition
anno_type_sec :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ 'Var ModeUpd ⇒ bool"
where
"anno_type_sec Γ 𝒮 P upd ≡ (case upd of (Rel v AsmNoReadOrWrite) ⇒
(v ∈ add_anno_dom Γ 𝒮 upd ⟶ (the (Γ v)) ≤:⇩P (dma_type v))
| _ ⇒ True)"
definition
types_stable :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ bool"
where
"types_stable Γ 𝒮 ≡ ∀x∈dom Γ. type_stable 𝒮 (the (Γ x))"
definition
tyenv_wellformed :: "'Var Mds ⇒ ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ bool"
where
"tyenv_wellformed mds Γ 𝒮 P ≡
mds_consistent mds Γ 𝒮 P ∧
types_wellformed Γ ∧ types_stable Γ 𝒮"
lemma subset_entailment:
"P' ⊆ P ⟹ P ⊢ P'"
apply(auto simp: pred_entailment_def pred_def)
done
lemma pred_entailment_refl [simp]:
"P ⊢ P"
by(simp add: pred_entailment_def)
lemma pred_entailment_mono:
"P ⊢ P' ⟹ P ⊆ P'' ⟹ P'' ⊢ P'"
by(auto simp: pred_entailment_def pred_def)
lemma type_equiv_subset:
"type_equiv t P t' ⟹ P ⊆ P' ⟹ type_equiv t P' t'"
apply(auto simp: type_equiv_def subtype_def intro: pred_entailment_mono)
done
definition
context_equiv :: "('Var,'BExp) TyEnv ⇒ 'BExp preds ⇒ ('Var,'BExp) TyEnv ⇒ bool" ("_ =:⇩_ _" [120, 120, 120] 1000)
where
"Γ =:⇩P Γ' ≡ dom Γ = dom Γ' ∧
(∀x∈dom Γ'. type_equiv (the (Γ x)) P (the (Γ' x)))"
lemma context_equiv_refl[simp]:
"context_equiv Γ P Γ"
by(simp add: context_equiv_def)
lemma context_equiv_subset:
"context_equiv Γ P Γ' ⟹ P ⊆ P' ⟹ context_equiv Γ P' Γ'"
apply(auto simp: context_equiv_def intro: type_equiv_subset)
done
lemma pred_entailment_trans:
"P ⊢ P' ⟹ P' ⊢ P'' ⟹ P ⊢ P''"
by(auto simp: pred_entailment_def)
lemma pred_un [simp]:
"pred (P ∪ P') mem = (pred P mem ∧ pred P' mem)"
apply(auto simp: pred_def)
done
lemma pred_entailment_un:
"P ⊢ P' ⟹ P ⊢ P'' ⟹ P ⊢ (P' ∪ P'')"
apply(subst pred_entailment_def)
apply clarsimp
apply(fastforce simp: pred_entailment_def)
done
lemma pred_entailment_mono_un:
"P ⊢ P' ⟹ (P ∪ P'') ⊢ (P' ∪ P'')"
apply(auto simp: pred_entailment_def pred_def)
done
lemma subtype_trans:
"t ≤:⇩P t' ⟹ t' ≤:⇩P' t'' ⟹ P ⊢ P' ⟹ t ≤:⇩P t''"
"t ≤:⇩P' t' ⟹ t' ≤:⇩P t'' ⟹ P ⊢ P' ⟹ t ≤:⇩P t''"
apply(clarsimp simp: subtype_def)
apply(rule pred_entailment_trans)
prefer 2
apply assumption
apply(rule pred_entailment_un)
apply(blast intro: subset_entailment)
apply(rule pred_entailment_trans)
prefer 2
apply assumption
apply(blast intro: pred_entailment_mono_un)
apply(clarsimp simp: subtype_def)
apply(rule pred_entailment_trans)
prefer 2
apply assumption
apply(rule pred_entailment_un)
apply(blast intro: pred_entailment_mono)
apply(blast intro: subset_entailment)
done
lemma type_equiv_trans:
"type_equiv t P t' ⟹ type_equiv t' P' t'' ⟹ P ⊢ P' ⟹ type_equiv t P t''"
apply(auto simp: type_equiv_def intro: subtype_trans)
done
lemma context_equiv_trans:
"context_equiv Γ P Γ' ⟹ context_equiv Γ' P' Γ'' ⟹ P ⊢ P' ⟹ context_equiv Γ P Γ''"
apply(force simp: context_equiv_def intro: type_equiv_trans)
done
lemma un_pred_entailment_mono:
"(P ∪ P') ⊢ P'' ⟹ P''' ⊢ P ⟹ (P''' ∪ P') ⊢ P''"
unfolding pred_entailment_def pred_def
apply blast
done
lemma subtype_entailment:
"t ≤:⇩P t' ⟹ P' ⊢ P ⟹ t ≤:⇩P' t'"
apply(auto simp: subtype_def intro: un_pred_entailment_mono)
done
lemma type_equiv_entailment:
"type_equiv t P t' ⟹ P' ⊢ P ⟹ type_equiv t P' t'"
apply(auto simp: type_equiv_def intro: subtype_entailment)
done
lemma context_equiv_entailment:
"context_equiv Γ P Γ' ⟹ P' ⊢ P ⟹ context_equiv Γ P' Γ'"
apply(auto simp: context_equiv_def intro: type_equiv_entailment)
done
inductive
has_type :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ ('Var, 'AExp, 'BExp) Stmt ⇒ ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ bool"
("⊢ _,_,_ {_} _,_,_" [120, 120, 120, 120, 120, 120, 120] 1000)
where
stop_type [intro]: "⊢ Γ,𝒮,P {Stop} Γ,𝒮,P" |
skip_type [intro] : "⊢ Γ,𝒮,P {Skip} Γ,𝒮,P" |
assign⇩𝒞 :
"⟦x ∈ 𝒞; Γ ⊢⇩a e ∈ t; P ⊢ t; (∀v∈dom Γ. x ∉ vars_of_type (the (Γ v)));
P' = restrict_preds_to_vars (assign_post P x e) {v. stable 𝒮 v};
∀v. x ∈ 𝒞_vars v ∧ v ∉ snd 𝒮 ⟶ P ⊢ (to_total Γ v) ∧
(to_total Γ v) ≤:⇩P' (dma_type v) ⟧ ⟹
⊢ Γ,𝒮,P {x ← e} Γ,𝒮,P'" |
assign⇩1 :
"⟦ x ∉ dom Γ ; x ∉ 𝒞; Γ ⊢⇩a e ∈ t; t ≤:⇩P (dma_type x);
P' = restrict_preds_to_vars (assign_post P x e) {v. stable 𝒮 v} ⟧ ⟹
⊢ Γ,𝒮,P {x ← e} Γ,𝒮,P'" |
assign⇩2 :
"⟦ x ∈ dom Γ ; Γ ⊢⇩a e ∈ t; type_stable 𝒮 t; P' = restrict_preds_to_vars (assign_post P x e) {v. stable 𝒮 v};
x ∉ snd 𝒮 ⟶ t ≤:⇩P' (dma_type x) ⟧ ⟹
has_type Γ 𝒮 P (x ← e) (Γ (x := Some t)) 𝒮 P'" |
if_type [intro]:
"⟦ Γ ⊢⇩b e ∈ t; P ⊢ t;
⊢ Γ,𝒮,(P +⇩𝒮 e) { c⇩1 } Γ',𝒮',P'; ⊢ Γ,𝒮,(P +⇩𝒮 (bexp_neg e)) { c⇩2 } Γ'',𝒮',P'';
context_equiv Γ' P' Γ'''; context_equiv Γ'' P'' Γ'''; P' ⊢ P'''; P'' ⊢ P''';
∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ''' 𝒮' P''';
∀mds. tyenv_wellformed mds Γ'' 𝒮' P'' ⟶ tyenv_wellformed mds Γ''' 𝒮' P''' ⟧ ⟹
⊢ Γ,𝒮,P { If e c⇩1 c⇩2 } Γ''',𝒮',P'''" |
while_type [intro]: "⟦ Γ ⊢⇩b e ∈ t ; P ⊢ t; ⊢ Γ,𝒮,(P +⇩𝒮 e) { c } Γ,𝒮,P ⟧ ⟹ ⊢ Γ,𝒮,P { While e c } Γ,𝒮,P" |
anno_type [intro]: "⟦ Γ' = Γ ⊕⇩𝒮 upd ; 𝒮' = add_anno_stable 𝒮 upd; P' = restrict_preds_to_vars P {v. stable 𝒮' v};
⊢ Γ',𝒮',P' { c } Γ'',𝒮'',P'' ; c ≠ Stop ;
(⋀ x. (to_total Γ x) ≤:⇩P' (to_total Γ' x));
anno_type_stable Γ 𝒮 upd; anno_type_sec Γ 𝒮 P upd⟧ ⟹ ⊢ Γ,𝒮,P { c@[upd] } Γ'',𝒮'',P''" |
seq_type [intro]: "⟦ ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P' ; ⊢ Γ',𝒮',P' { c⇩2 } Γ'',𝒮'',P'' ⟧ ⟹ ⊢ Γ,𝒮,P { c⇩1 ;; c⇩2 } Γ'',𝒮'',P''" |
sub : "⟦ ⊢ Γ⇩1,𝒮,P⇩1 { c } Γ⇩1',𝒮',P⇩1' ; context_equiv Γ⇩2 P⇩2 Γ⇩1 ; (∀mds. tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1);
(∀mds. tyenv_wellformed mds Γ⇩1' 𝒮' P⇩1' ⟶ tyenv_wellformed mds Γ⇩2' 𝒮' P⇩2'); context_equiv Γ⇩1' P⇩1' Γ⇩2'; P⇩2 ⊢ P⇩1; P⇩1' ⊢ P⇩2' ⟧ ⟹ ⊢ Γ⇩2,𝒮,P⇩2 { c } Γ⇩2',𝒮',P⇩2'" |
await_type [intro]:
"⟦ Γ ⊢⇩b e ∈ t; P ⊢ t;
⊢ Γ,𝒮,(P +⇩𝒮 e) { c } Γ',𝒮',P' ⟧ ⟹
⊢ Γ,𝒮,P { Await e c } Γ',𝒮',P'"
lemma sub':
"⟦ context_equiv Γ⇩2 P⇩2 Γ⇩1 ;
(∀mds. tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1);
(∀mds. tyenv_wellformed mds Γ⇩1' 𝒮' P⇩1' ⟶ tyenv_wellformed mds Γ⇩2' 𝒮' P⇩2');
context_equiv Γ⇩1' P⇩1' Γ⇩2';
P⇩2 ⊢ P⇩1;
P⇩1' ⊢ P⇩2';
⊢ Γ⇩1,𝒮,P⇩1 { c } Γ⇩1',𝒮',P⇩1' ⟧ ⟹
⊢ Γ⇩2,𝒮,P⇩2 { c } Γ⇩2',𝒮',P⇩2'"
by(rule sub)
lemma assign⇩2_helper:
"⟦Γ x = Some t; has_type Γ 𝒮 P (x ← e) (Γ(x ↦ t)) 𝒮 P'⟧ ⟹ has_type Γ 𝒮 P (x ← e) Γ 𝒮 P'"
by (simp add:map_upd_triv)
lemma conc':
"⟦ ⊢ Γ⇩1,𝒮,P { c } Γ',𝒮',P';
Γ⇩1 = (Γ⇩2(x ↦ t));
x ∈ dom Γ⇩2;
type_equiv (the (Γ⇩2 x)) P t;
type_wellformed t;
type_stable 𝒮 t ⟧ ⟹
⊢ Γ⇩2,𝒮,P { c } Γ',𝒮',P'"
apply(erule sub)
apply(fastforce simp: context_equiv_def)
apply(clarsimp simp: tyenv_wellformed_def mds_consistent_def)
apply(rule conjI)
apply fastforce
apply(rule conjI)
apply(fastforce simp: types_wellformed_def)
apply(fastforce simp: types_stable_def)
apply blast
apply simp+
done
lemma tyenv_wellformed_subset:
"tyenv_wellformed mds Γ 𝒮 P ⟹ P' ⊆ P ⟹ tyenv_wellformed mds Γ 𝒮 P'"
apply(auto simp: tyenv_wellformed_def mds_consistent_def)
done
lemma if_type':
"⟦ Γ ⊢⇩b e ∈ t;
P ⊢ t;
⊢ Γ,𝒮,(P +⇩𝒮 e) { c⇩1 } Γ',𝒮',P';
⊢ Γ,𝒮,(P +⇩𝒮 (bexp_neg e)) { c⇩2 } Γ',𝒮',P'';
P''' ⊆ P' ∩ P'' ⟧ ⟹
⊢ Γ,𝒮,P { If e c⇩1 c⇩2 } Γ',𝒮',P'''"
apply(erule (3) if_type)
apply(rule context_equiv_refl)
apply(rule context_equiv_refl)
apply(blast intro: subset_entailment)+
apply(blast intro: tyenv_wellformed_subset)+
done
lemma skip_type':
"⟦Γ = Γ'; 𝒮 = 𝒮'; P = P'⟧ ⟹ ⊢ Γ,𝒮,P {Skip} Γ',𝒮',P'"
using skip_type by simp
text ‹
Some helper lemmas to discharge the assumption of the @{thm anno_type} rule.
›
lemma anno_type_helpers [simp]:
"(to_total Γ x) ≤:⇩P (to_total (add_anno Γ 𝒮 (buffer +=⇩m AsmNoWrite)) x)"
"(to_total Γ x) ≤:⇩P (to_total (add_anno Γ 𝒮 (buffer +=⇩m AsmNoReadOrWrite)) x)"
apply(auto simp: to_total_def add_anno_def subtype_def intro: subset_entailment)
done
subsection ‹Typing Soundness›
text ‹The following predicate is needed to exclude some pathological
cases, that abuse the @{term Stop} command which is not allowed to
occur in actual programs.›
inductive_cases has_type_elim: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
inductive_cases has_type_stop_elim: "⊢ Γ,𝒮,P { Stop } Γ',𝒮',P'"
definition tyenv_eq :: "('Var,'BExp) TyEnv ⇒ ('Var, 'Val) Mem ⇒ ('Var, 'Val) Mem ⇒ bool"
(infix "=ı" 60)
where "mem⇩1 =⇘Γ⇙ mem⇩2 ≡ ∀ x. (type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x)"
lemma type_max_dma_type [simp]:
"type_max (dma_type x) mem = dma mem x"
using dma_correct unfolding type_max_def apply auto
done
text ‹
This result followed trivially for Mantel et al., but we need to know that the
type environment is wellformed.
›
lemma tyenv_eq_sym':
"dom Γ ∩ 𝒞 = {} ⟹ types_wellformed Γ ⟹ mem⇩1 =⇘Γ⇙ mem⇩2 ⟹ mem⇩2 =⇘Γ⇙ mem⇩1"
proof(clarsimp simp: tyenv_eq_def)
fix x
assume a: "∀x. type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x"
assume b: "dom Γ ∩ 𝒞 = {}"
from a b have eq_𝒞: "∀x∈𝒞. mem⇩1 x = mem⇩2 x"
by (fastforce simp: to_total_def 𝒞_Low type_max_dma_type split: if_splits)
hence "dma mem⇩1 = dma mem⇩2"
by (rule dma_𝒞)
hence dma_type_eq: "type_max (dma_type x) mem⇩1 = type_max (dma_type x) mem⇩2"
by(simp)
assume c: "types_wellformed Γ"
assume d: "type_max (to_total Γ x) mem⇩2 = Low"
show "mem⇩2 x = mem⇩1 x"
proof(cases "x ∈ dom Γ")
assume in_dom: "x ∈ dom Γ"
from this obtain t where t: "Γ x = Some t" by blast
from this in_dom c have "type_wellformed t" by (force simp: types_wellformed_def)
hence "∀x∈vars_of_type t. mem⇩1 x = mem⇩2 x"
using eq_𝒞 unfolding type_wellformed_def by blast
hence t_eq: "type_max t mem⇩1 = type_max t mem⇩2"
unfolding type_max_def using eval_vars_det⇩B
by fastforce
with in_dom t have "to_total Γ x = t"
by (auto simp: to_total_def)
with t_eq have "type_max (to_total Γ x) mem⇩2 = type_max (to_total Γ x) mem⇩1" by simp
with d have "type_max (to_total Γ x) mem⇩1 = Low" by simp
with a show ?thesis by (metis sym)
next
assume "x ∉ dom Γ"
hence "to_total Γ x = dma_type x"
by (auto simp: to_total_def)
with dma_type_eq have "type_max (to_total Γ x) mem⇩2 = type_max (to_total Γ x) mem⇩1" by simp
with d have "type_max (to_total Γ x) mem⇩1 = Low" by simp
with a show ?thesis by (metis sym)
qed
qed
lemma tyenv_eq_sym:
"tyenv_wellformed mds Γ 𝒮 P ⟹ mem⇩1 =⇘Γ⇙ mem⇩2 ⟹ mem⇩2 =⇘Γ⇙ mem⇩1"
apply(rule tyenv_eq_sym')
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
apply(simp add: tyenv_wellformed_def)
by assumption
inductive_set ℛ⇩1 :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
and ℛ⇩1_abv :: "
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
bool" ("_ ℛ⇧1⇘_,_,_⇙ _" [120, 120, 120, 120, 120] 1000)
for Γ' :: "('Var,'BExp) TyEnv"
and 𝒮' :: "'Var Stable"
and P' :: "'BExp preds"
where
"x ℛ⇧1⇘Γ,𝒮,P⇙ y ≡ (x, y) ∈ ℛ⇩1 Γ 𝒮 P" |
intro [intro!] : "⟦ ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ; tyenv_wellformed mds Γ 𝒮 P ; mem⇩1 =⇘Γ⇙ mem⇩2;
pred P mem⇩1; pred P mem⇩2; ∀x∈dom Γ. x∉mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x⟧ ⟹
⟨c, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c, mds, mem⇩2⟩"
inductive ℛ⇩3_aux :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
bool" ("_ ℛ⇧3⇘_,_,_⇙ _" [120, 120, 120, 120, 120] 1000)
and ℛ⇩3 :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
where
"ℛ⇩3 Γ' 𝒮' P' ≡ {(lc⇩1, lc⇩2). ℛ⇩3_aux lc⇩1 Γ' 𝒮' P' lc⇩2}" |
intro⇩1 [intro] : "⟦ ⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩; ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ⟧ ⟹
⟨Seq c⇩1 c, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨Seq c⇩2 c, mds, mem⇩2⟩" |
intro⇩3 [intro] : "⟦ ⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩; ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ⟧ ⟹
⟨Seq c⇩1 c, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨Seq c⇩2 c, mds, mem⇩2⟩"
definition
weak_bisim :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel ⇒
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel ⇒ bool"
where
"weak_bisim 𝒯⇩1 𝒯 ≡ ∀ c⇩1 c⇩2 mds mem⇩1 mem⇩2 c⇩1' mds' mem⇩1'.
((⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ 𝒯⇩1 ∧
(⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩)) ⟶
(∃ c⇩2' mem⇩2'. ⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
(⟨c⇩1', mds', mem⇩1'⟩, ⟨c⇩2', mds', mem⇩2'⟩) ∈ 𝒯)"
inductive_set ℛ :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
and ℛ_abv :: "
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
bool" ("_ ℛ⇧u⇘_,_,_⇙ _" [120, 120, 120, 120, 120] 1000)
for Γ :: "('Var,'BExp) TyEnv"
and 𝒮 :: "'Var Stable"
and P :: "'BExp preds"
where
"x ℛ⇧u⇘Γ,𝒮,P⇙ y ≡ (x, y) ∈ ℛ Γ 𝒮 P" |
intro⇩1: "lc ℛ⇧1⇘Γ,𝒮,P⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ 𝒮 P" |
intro⇩3: "lc ℛ⇧3⇘Γ,𝒮,P⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ 𝒮 P"
inductive_cases ℛ⇩1_elim [elim]: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩"
inductive_cases ℛ⇩3_elim [elim]: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩"
inductive_cases ℛ_elim [elim]: "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ ℛ Γ 𝒮 P"
inductive_cases ℛ_elim': "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds⇩2, mem⇩2⟩) ∈ ℛ Γ 𝒮 P"
inductive_cases ℛ⇩1_elim' : "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds⇩2, mem⇩2⟩"
inductive_cases ℛ⇩3_elim' : "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds⇩2, mem⇩2⟩"
lemma ℛ⇩1_mem_eq: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ mem⇩1 =⇘mds⇙⇧l mem⇩2"
proof (erule ℛ⇩1_elim)
fix Γ 𝒮 P
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
hence mds_consistent: "mds_consistent mds Γ 𝒮 P"
unfolding tyenv_wellformed_def by blast
assume tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
assume leq: "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x"
assume pred: "pred P mem⇩1"
show "mem⇩1 =⇘mds⇙⇧l mem⇩2"
unfolding low_mds_eq_def
proof(clarify)
fix x
assume is_Low: "dma mem⇩1 x = Low"
assume is_readable: "x ∈ 𝒞 ∨ x ∉ mds AsmNoReadOrWrite"
show "mem⇩1 x = mem⇩2 x"
proof(cases "x ∈ dom Γ")
assume in_dom: "x ∈ dom Γ"
with mds_consistent have "x ∉ 𝒞"
unfolding mds_consistent_def by blast
with is_readable have "x ∉ mds AsmNoReadOrWrite"
by blast
with in_dom leq have "type_max (to_total Γ x) mem⇩1 ≤ dma mem⇩1 x"
unfolding to_total_def
by auto
with is_Low have "type_max (to_total Γ x) mem⇩1 = Low"
by(simp add: less_eq_Sec_def)
with tyenv_eq show ?thesis
unfolding tyenv_eq_def by blast
next
assume nin_dom: "x ∉ dom Γ"
with is_Low have "type_max (to_total Γ x) mem⇩1 = Low"
unfolding to_total_def
by simp
with tyenv_eq show ?thesis
unfolding tyenv_eq_def by blast
qed
qed
qed
lemma ℛ⇩1_dma_eq:
"⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ dma mem⇩1 = dma mem⇩2"
apply(drule ℛ⇩1_mem_eq)
apply(erule low_mds_eq_dma)
done
lemma bisim_simple_ℛ⇩1:
"⟨c, mds, mem⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c', mds', mem'⟩ ⟹ c = c'"
apply(cases rule: ℛ⇩1.cases, simp+)
done
lemma bisim_simple_ℛ⇩3:
"lc ℛ⇧3⇘Γ,𝒮,P⇙ lc' ⟹ (fst (fst lc)) = (fst (fst lc'))"
apply(induct rule: ℛ⇩3_aux.induct)
using bisim_simple_ℛ⇩1 apply clarsimp
apply simp
done
lemma bisim_simple_ℛ⇩u:
"lc ℛ⇧u⇘Γ,𝒮,P⇙ lc' ⟹ (fst (fst lc)) = (fst (fst lc'))"
apply(induct rule: ℛ.induct)
apply clarsimp
apply(cases rule: ℛ⇩1.cases, simp+)
apply(cases rule: ℛ⇩3_aux.cases, simp+)
apply blast
using bisim_simple_ℛ⇩3 apply clarsimp
done
lemma 𝒞_eq_type_max_eq:
assumes wf: "type_wellformed t"
assumes 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩2 x"
shows "type_max t mem⇩1 = type_max t mem⇩2"
proof -
have "∀x∈vars_of_type t. mem⇩1 x = mem⇩2 x"
using wf 𝒞_eq unfolding type_wellformed_def by blast
thus ?thesis
unfolding type_max_def using eval_vars_det⇩B by fastforce
qed
lemma vars_of_type_eq_type_max_eq:
assumes mem_eq: "∀x∈vars_of_type t. mem⇩1 x = mem⇩2 x"
shows "type_max t mem⇩1 = type_max t mem⇩2"
proof -
from assms show ?thesis
unfolding type_max_def using eval_vars_det⇩B by fastforce
qed
lemma ℛ⇩1_sym: "sym (ℛ⇩1 Γ' 𝒮' P')"
unfolding sym_def
proof clarsimp
fix c mds mem c' mds' mem'
assume in_ℛ⇩1: "⟨c, mds, mem⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c', mds', mem'⟩"
then obtain Γ 𝒮 P where
stuff: "c' = c" "mds' = mds" "⊢ Γ,𝒮,P {c} Γ',𝒮',P'" "tyenv_wellformed mds Γ 𝒮 P"
"mem =⇘Γ⇙ mem'" "pred P mem" "pred P mem'"
"∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem ≤ dma mem x"
using ℛ⇩1_elim' by blast+
from stuff have stuff': "mem' =⇘Γ⇙ mem"
by (metis tyenv_eq_sym)
have "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem' ≤ dma mem' x"
proof -
from in_ℛ⇩1 have "dma mem = dma mem'"
using ℛ⇩1_dma_eq stuff by metis
moreover have "∀x∈dom Γ. type_max (the (Γ x)) mem = type_max (the (Γ x)) mem'"
proof
fix x
assume "x ∈ dom Γ"
hence "type_wellformed (the (Γ x))"
using ‹tyenv_wellformed mds Γ 𝒮 P›
by(auto simp: tyenv_wellformed_def types_wellformed_def)
moreover have "∀x∈𝒞. mem x = mem' x"
using in_ℛ⇩1 ℛ⇩1_mem_eq 𝒞_Low stuff
unfolding low_mds_eq_def by auto
ultimately
show "type_max (the (Γ x)) mem = type_max (the (Γ x)) mem'"
using 𝒞_eq_type_max_eq by blast
qed
ultimately show ?thesis
using stuff(8) by fastforce
qed
with stuff stuff'
show "⟨c', mds', mem'⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c, mds, mem⟩"
by (metis (no_types) ℛ⇩1.intro)
qed
lemma ℛ⇩3_sym: "sym (ℛ⇩3 Γ 𝒮 P)"
unfolding sym_def
proof (clarify)
fix c⇩1 mds mem⇩1 c⇩2 mds' mem⇩2
assume asm: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds', mem⇩2⟩"
hence [simp]: "mds' = mds"
using ℛ⇩3_elim' by blast
from asm show "⟨c⇩2, mds', mem⇩2⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩1, mds, mem⇩1⟩"
apply auto
apply (induct rule: ℛ⇩3_aux.induct)
apply (metis (lifting) ℛ⇩1_sym ℛ⇩3_aux.intro⇩1 symD)
by (metis (lifting) ℛ⇩3_aux.intro⇩3)
qed
lemma ℛ_mds [simp]: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2, mds', mem⇩2⟩ ⟹ mds = mds'"
apply (rule ℛ_elim')
apply (auto)
apply (metis ℛ⇩1_elim')
apply (insert ℛ⇩3_elim')
by blast
lemma ℛ_sym: "sym (ℛ Γ 𝒮 P)"
unfolding sym_def
proof (clarify)
fix c⇩1 mds mem⇩1 c⇩2 mds⇩2 mem⇩2
assume asm: "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds⇩2, mem⇩2⟩) ∈ ℛ Γ 𝒮 P"
with ℛ_mds have [simp]: "mds⇩2 = mds"
by blast
from asm show "(⟨c⇩2, mds⇩2, mem⇩2⟩, ⟨c⇩1, mds, mem⇩1⟩) ∈ ℛ Γ 𝒮 P"
using ℛ.intro⇩1 [of Γ 𝒮 P] and ℛ.intro⇩3 [of _ Γ 𝒮 P]
using ℛ⇩1_sym [of Γ] and ℛ⇩3_sym [of Γ]
apply simp
apply (erule ℛ_elim)
by (auto simp: sym_def)
qed
lemma ℛ⇩1_closed_glob_consistent: "closed_glob_consistent (ℛ⇩1 Γ' 𝒮' P')"
unfolding closed_glob_consistent_def
proof (clarify)
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 A
assume R1: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
hence [simp]: "c⇩2 = c⇩1" by blast
assume A_updates_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
assume A_updates_dma: "∀x. dma mem⇩1 [∥⇩1 A] x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
assume A_updates_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
from R1 obtain Γ 𝒮 P where Γ_props: "⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P'" "mem⇩1 =⇘Γ⇙ mem⇩2" "tyenv_wellformed mds Γ 𝒮 P"
"pred P mem⇩1" "pred P mem⇩2"
"∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x"
by force
from Γ_props(3) have stable_not_written: "∀x. stable 𝒮 x ⟶ var_asm_not_written mds x"
by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def var_asm_not_written_def)
with A_updates_vars have stable_unchanged⇩1: "∀x. stable 𝒮 x ⟶ (mem⇩1 [∥⇩1 A]) x = mem⇩1 x" and
stable_unchanged⇩2: "∀x. stable 𝒮 x ⟶ (mem⇩2 [∥⇩2 A]) x = mem⇩2 x"
by(auto simp: apply_adaptation_def split: option.splits)
from stable_not_written A_updates_dma
have stable_unchanged_dma⇩1: "∀x. stable 𝒮 x ⟶ dma (mem⇩1 [∥⇩1 A]) x = dma mem⇩1 x"
by(blast)
have tyenv_eq': "mem⇩1 [∥⇩1 A] =⇘Γ⇙ mem⇩2 [∥⇩2 A]"
proof(clarsimp simp: tyenv_eq_def)
fix x
assume a: "type_max (to_total Γ x) mem⇩1 [∥⇩1 A] = Low"
show "mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
proof(cases "x ∈ dom Γ")
assume in_dom: "x ∈ dom Γ"
with Γ_props(3) have "var_asm_not_written mds x"
by(auto simp: tyenv_wellformed_def mds_consistent_def var_asm_not_written_def stable_def)
hence [simp]: "mem⇩1 [∥⇩1 A] x = mem⇩1 x" and [simp]: "mem⇩2 [∥⇩2 A] x = mem⇩2 x"
using A_updates_vars by(auto simp: apply_adaptation_def split: option.splits)
from in_dom a obtain t⇩x where Γ⇩x: "Γ x = Some t⇩x" and t⇩x_Low': "type_max t⇩x (mem⇩1 [∥⇩1 A]) = Low"
by(auto simp: to_total_def)
have t⇩x_unchanged: "type_max t⇩x (mem⇩1 [∥⇩1 A]) = type_max t⇩x mem⇩1"
proof -
from Γ⇩x Γ_props(3) have t⇩x_stable: "type_stable 𝒮 t⇩x" and t⇩x_wellformed: "type_wellformed t⇩x"
by(force simp: tyenv_wellformed_def types_stable_def types_wellformed_def)+
from t⇩x_stable t⇩x_wellformed stable_unchanged⇩1 show ?thesis
using type_stable_is_sufficient'
by blast
qed
with t⇩x_Low' have t⇩x_Low: "type_max t⇩x mem⇩1 = Low" by simp
with Γ⇩x Γ_props(2) have "mem⇩1 x = mem⇩2 x"
by(force simp: tyenv_eq_def to_total_def split: if_splits)
thus ?thesis by simp
next
assume nin_dom: "x ∉ dom Γ"
with a have is_Low': "dma (mem⇩1[∥⇩1 A]) x = Low"
by(simp add: to_total_def)
show ?thesis
proof(cases "x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞")
assume "x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞"
with is_Low' show ?thesis
using A_updates_sec by blast
next
assume "¬ (x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞)"
hence "x ∈ mds AsmNoReadOrWrite" and "x ∉ 𝒞"
by auto
with nin_dom Γ_props(3) have "False"
by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def)
thus ?thesis by blast
qed
qed
qed
have sec': "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) (mem⇩1 [∥⇩1 A]) ≤ dma (mem⇩1 [∥⇩1 A]) x"
proof(intro ballI impI)
fix x
assume readable: "x ∉ mds AsmNoReadOrWrite"
assume in_dom: "x ∈ dom Γ"
with Γ_props(3) have "var_asm_not_written mds x"
by(auto simp: tyenv_wellformed_def mds_consistent_def var_asm_not_written_def stable_def)
hence [simp]: "dma mem⇩1 [∥⇩1 A] x = dma mem⇩1 x"
using A_updates_dma by(auto simp: apply_adaptation_def split: option.splits)
from in_dom obtain t⇩x where Γ⇩x: "Γ x = Some t⇩x"
by(auto simp: to_total_def)
have t⇩x_unchanged: "type_max t⇩x (mem⇩1 [∥⇩1 A]) = type_max t⇩x mem⇩1"
proof -
from Γ⇩x Γ_props(3) have t⇩x_stable: "type_stable 𝒮 t⇩x" and t⇩x_wellformed: "type_wellformed t⇩x"
by(force simp: tyenv_wellformed_def types_stable_def types_wellformed_def)+
from t⇩x_stable t⇩x_wellformed stable_unchanged⇩1 show ?thesis
using type_stable_is_sufficient'
by blast
qed
with Γ⇩x have [simp]:"type_max (the (Γ x)) (mem⇩1 [∥⇩1 A]) = type_max (the (Γ x)) mem⇩1"
by simp
show "type_max (the (Γ x)) mem⇩1 [∥⇩1 A] ≤ dma mem⇩1 [∥⇩1 A] x "
apply simp
using in_dom readable Γ_props by metis
qed
from stable_unchanged⇩1 stable_unchanged⇩2 Γ_props(3) have "∀p∈P. ev⇩B (mem⇩1 [∥⇩1 A]) p = ev⇩B mem⇩1 p ∧ ev⇩B (mem⇩2 [∥⇩2 A]) p = ev⇩B mem⇩2 p"
apply(intro ballI)
apply(rule conjI)
by(rule eval_vars_det⇩B,force simp: tyenv_wellformed_def mds_consistent_def stable_def)+
hence "pred P (mem⇩1 [∥⇩1 A]) = pred P mem⇩1" and
"pred P (mem⇩2 [∥⇩2 A]) = pred P mem⇩2"
by(simp add: pred_def)+
with Γ_props tyenv_eq' sec'
show "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩"
by auto
qed
lemma ℛ⇩3_closed_glob_consistent:
"closed_glob_consistent (ℛ⇩3 Γ' 𝒮' P')"
unfolding closed_glob_consistent_def
proof(clarsimp)
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 A
assume in_ℛ⇩3: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
assume A_modifies_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
assume A_modifies_dma: "∀x. dma mem⇩1 [∥⇩1 A] x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
assume A_modifies_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∈ mds AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
define lc⇩1 where "lc⇩1 ≡ ⟨c⇩1, mds, mem⇩1⟩"
define lc⇩2 where "lc⇩2 ≡ ⟨c⇩2, mds, mem⇩2⟩"
from lc⇩1_def lc⇩2_def in_ℛ⇩3 have "lc⇩1 ℛ⇧3⇘Γ',𝒮',P'⇙ lc⇩2" by simp
from this lc⇩1_def lc⇩2_def A_modifies_vars A_modifies_dma A_modifies_sec
show "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩"
proof(induct arbitrary: c⇩1 mds mem⇩1 c⇩2 mds mem⇩2 rule: ℛ⇩3_aux.induct)
case (intro⇩1 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
show ?case
apply (rule ℛ⇩3_aux.intro⇩1[OF _ intro⇩1(2)])
using ℛ⇩1_closed_glob_consistent intro⇩1
unfolding closed_glob_consistent_def by blast
next
case (intro⇩3 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
show ?case
apply(rule ℛ⇩3_aux.intro⇩3)
apply(rule intro⇩3(2))
using intro⇩3 apply simp+
done
qed
qed
lemma ℛ_closed_glob_consistent: "closed_glob_consistent (ℛ Γ' 𝒮' P')"
unfolding closed_glob_consistent_def
proof (clarify, erule ℛ_elim, simp_all)
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 A
assume R1: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
and A_modifies_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
and A_modifies_dma: "∀x. dma (mem⇩1 [∥⇩1 A]) x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
and A_modifies_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∈ mds AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
show
"⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩"
apply(rule intro⇩1)
apply clarify
using ℛ⇩1_closed_glob_consistent unfolding closed_glob_consistent_def
using R1 A_modifies_vars A_modifies_dma A_modifies_sec
by blast
next
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 x A
assume R3: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
and A_modifies_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
and A_modifies_dma: "∀x. dma (mem⇩1 [∥⇩1 A]) x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
and A_modifies_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∈ mds AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
show "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩ "
apply(rule intro⇩3)
using ℛ⇩3_closed_glob_consistent unfolding closed_glob_consistent_def
using R3 A_modifies_vars A_modifies_dma A_modifies_sec
by blast
qed
lemma mode_update_add_anno:
"mds_consistent mds Γ 𝒮 P ⟹
mds_consistent (update_modes upd mds)
(Γ ⊕⇩𝒮 upd)
(add_anno_stable 𝒮 upd)
(P |` {v. stable (add_anno_stable 𝒮 upd) v})"
apply(case_tac upd)
apply(rename_tac v m)
apply(case_tac m)
apply((clarsimp simp: add_anno_def mds_consistent_def stable_def restrict_preds_to_vars_def | safe | fastforce)+)[4]
apply(rename_tac v m)
apply(case_tac m)
apply((clarsimp simp: add_anno_def mds_consistent_def stable_def restrict_preds_to_vars_def | safe | fastforce)+)[4]
done
lemma add_anno_acq_GuarNoReadOrWrite [simp]:
"Γ ⊕⇩𝒮 (v +=⇩m GuarNoReadOrWrite) = Γ"
apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
apply(rule ext)
apply(clarsimp | safe)+
by (metis option.collapse prod.collapse)
lemma add_anno_rel_GuarNoReadOrWrite [simp]:
"Γ ⊕⇩𝒮 (v -=⇩m GuarNoReadOrWrite) = Γ"
apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
apply(rule ext)
apply(clarsimp | safe)+
by (metis option.collapse)
lemma add_anno_acq_GuarNoWrite [simp]:
"Γ ⊕⇩𝒮 (v +=⇩m GuarNoWrite) = Γ"
apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
apply(rule ext)
apply(clarsimp | safe)+
by (metis option.collapse prod.collapse)
lemma add_anno_rel_GuarNoWrite [simp]:
"Γ ⊕⇩𝒮 (v -=⇩m GuarNoWrite) = Γ"
apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
apply(rule ext)
apply(clarsimp | safe)+
by (metis option.collapse)
lemma dom_add_anno_rel:
"∀x∈dom (Γ ⊕⇩𝒮 (v -=⇩m m)). (Γ ⊕⇩𝒮 (v -=⇩m m)) x = Γ x"
apply(clarsimp simp: add_anno_def to_total_def restrict_map_def split: if_splits)
apply(case_tac m)
apply(auto split: if_splits)
done
lemma types_wellformed_mode_update:
"types_wellformed Γ ⟹
types_wellformed (Γ ⊕⇩𝒮 upd)"
apply(clarsimp simp: types_wellformed_def)
apply(case_tac upd)
apply(rename_tac v t v' m)
apply(case_tac m)
apply clarsimp
apply(case_tac "v' ∈ dom Γ ∨ v' ∈ 𝒞")
apply(clarsimp, force)
apply(simp split: if_splits)
apply(drule sym, fastforce)
apply(clarsimp | force )+
apply(case_tac "v' ∈ dom Γ ∨ v' ∈ 𝒞")
apply clarsimp
apply force
apply(simp split: if_splits)
apply(drule sym, fastforce)
apply(clarsimp | force)+
using dom_add_anno_rel[THEN bspec, OF domI]
apply (metis domI option.sel)
done
lemma types_stable_mode_update:
"types_stable Γ 𝒮 ⟹ types_wellformed Γ ⟹ anno_type_stable Γ 𝒮 upd
⟹ types_stable (Γ ⊕⇩𝒮 upd) (add_anno_stable 𝒮 upd)"
apply(clarsimp simp: types_stable_def)
apply(rename_tac x c f C)
apply(case_tac upd)
apply(rename_tac v m)
apply(case_tac m)
apply clarsimp
apply(case_tac "v ∈ dom Γ ∨ v ∈ 𝒞")
apply clarsimp
apply(force simp: stable_def)
apply(simp split: if_splits)
using 𝒞_vars_correct
apply(fastforce simp: anno_type_stable_def stable_def)
apply(force simp: stable_def)
apply clarsimp
apply(case_tac "v ∈ dom Γ ∨ v ∈ 𝒞")
apply clarsimp
apply(force simp: stable_def)
apply(simp split: if_splits)
using 𝒞_vars_correct
apply(fastforce simp: anno_type_stable_def stable_def)
apply(force simp: stable_def)
apply(force simp: stable_def)
apply(force simp: stable_def)
apply(rename_tac v m)
apply(subgoal_tac "Γ x = Some (C)")
prefer 2
using dom_add_anno_rel
apply (metis domI)
apply(case_tac m)
apply(clarsimp simp: anno_type_stable_def split: if_splits)
apply(clarsimp simp: stable_def types_wellformed_def type_wellformed_def)
using 𝒞_vars_correct
apply (metis (mono_tags, lifting) UN_I contra_subsetD domI option.sel)
apply(clarsimp simp: stable_def types_wellformed_def type_wellformed_def)
using 𝒞_vars_correct
apply (metis (mono_tags, lifting) UN_I contra_subsetD domI option.sel)
apply(clarsimp simp: anno_type_stable_def split: if_splits)
apply(clarsimp simp: stable_def types_wellformed_def type_wellformed_def)
apply (metis (mono_tags, lifting) UN_I contra_subsetD domI option.sel)
apply(clarsimp simp: stable_def)
apply (metis (no_types, lifting) domI option.sel snd_conv subsetD type_wellformed_def types_wellformed_def)
apply(clarsimp simp: anno_type_stable_def split: if_splits)
apply(clarsimp simp: stable_def)
apply (metis (no_types, lifting) domI option.sel snd_conv subsetD type_wellformed_def types_wellformed_def)
apply(clarsimp simp: stable_def)
apply (metis (no_types, lifting) domI option.sel snd_conv subsetD type_wellformed_def types_wellformed_def)
done
lemma tyenv_wellformed_mode_update:
"tyenv_wellformed mds Γ 𝒮 P ⟹ anno_type_stable Γ 𝒮 upd ⟹
tyenv_wellformed (update_modes upd mds)
(Γ ⊕⇩𝒮 upd)
(add_anno_stable 𝒮 upd)
(P |` {v. stable (add_anno_stable 𝒮 upd) v})"
apply(clarsimp simp: tyenv_wellformed_def)
apply(rule conjI)
apply(blast intro: mode_update_add_anno)
apply(rule conjI)
apply(blast intro: types_wellformed_mode_update)
apply(blast intro: types_stable_mode_update)
done
lemma stop_cxt :
"⟦ ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ; c = Stop ⟧ ⟹
context_equiv Γ P Γ' ∧ 𝒮' = 𝒮 ∧ P ⊢ P' ∧ (∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ' 𝒮 P')"
apply (induct rule: has_type.induct)
apply (auto intro: context_equiv_trans context_equiv_entailment pred_entailment_trans)
done
lemma tyenv_wellformed_preds_update:
"P' = P'' |` {v. stable 𝒮 v} ⟹
tyenv_wellformed mds Γ 𝒮 P ⟹ tyenv_wellformed mds Γ 𝒮 P'"
apply(clarsimp simp: tyenv_wellformed_def)
apply(clarsimp simp: mds_consistent_def)
apply(auto simp: restrict_preds_to_vars_def add_pred_def split: if_splits)
done
lemma mds_consistent_preds_tyenv_update:
"P' = P'' |` {v. stable 𝒮 v} ⟹ v ∈ dom Γ ⟹
mds_consistent mds Γ 𝒮 P ⟹ mds_consistent mds (Γ(v ↦ t)) 𝒮 P'"
apply(clarsimp simp: mds_consistent_def)
apply(auto simp: restrict_preds_to_vars_def add_pred_def split: if_splits)
done
lemma pred_preds_update:
assumes mem'_def: "mem' = mem (x := ev⇩A mem e)"
assumes P'_def: "P' = (assign_post P x e) |` {v. stable 𝒮 v}"
assumes pred_P: "pred P mem"
shows "pred P' mem'"
proof -
from P'_def have P'_def': "P' ⊆ assign_post P x e"
by(auto simp: restrict_preds_to_vars_def add_pred_def split: if_splits)
have "pred (assign_post P x e) mem'"
using assign_post_valid pred_P mem'_def by blast
with P'_def' show ?thesis
unfolding pred_def by blast
qed
lemma types_wellformed_update:
"types_wellformed Γ ⟹ type_wellformed t ⟹ types_wellformed (Γ(x ↦ t))"
by(auto simp: types_wellformed_def)
lemma types_stable_update:
"types_stable Γ 𝒮 ⟹ type_stable 𝒮 t ⟹ types_stable (Γ(x ↦ t)) 𝒮"
by(auto simp: types_stable_def)
lemma tyenv_wellformed_sub:
"⟦P⇩1 ⊆ P⇩2;
Γ⇩2 = Γ⇩1; tyenv_wellformed mds Γ⇩2 𝒮 P⇩2⟧ ⟹
tyenv_wellformed mds Γ⇩1 𝒮 P⇩1"
apply(clarsimp simp: tyenv_wellformed_def | safe)+
apply(fastforce simp: mds_consistent_def)
done
abbreviation
tyenv_sec :: "'Var Mds ⇒ ('Var,'BExp) TyEnv ⇒ ('Var,'Val) Mem ⇒ bool"
where
"tyenv_sec mds Γ mem ≡ ∀x∈dom Γ. x∉mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem ≤ dma mem x"
lemma tyenv_sec_mode_update:
"(∀x. (to_total Γ x) ≤:⇩P'' (to_total Γ'' x)) ⟹ pred P'' mem ⟹ 𝒮 = (mds AsmNoWrite, mds AsmNoReadOrWrite) ⟹
anno_type_sec Γ 𝒮 P upd ⟹ 𝒮'' = add_anno_stable 𝒮 upd ⟹ (∀p∈P. ∀v∈bexp_vars p. stable 𝒮 v) ⟹
P'' = P |` {v. stable 𝒮'' v} ⟹
Γ'' = Γ ⊕⇩𝒮 upd ⟹ tyenv_sec mds Γ mem ⟹ tyenv_sec (update_modes upd mds) Γ'' mem"
apply(case_tac upd)
apply(rename_tac v m)
apply(case_tac m)
apply(auto simp: add_anno_def to_total_def)[4]
apply(rename_tac v m)
apply(case_tac m)
apply(subgoal_tac "v ∈ mds AsmNoWrite ⟶ P'' = P")
by(auto simp: add_anno_def to_total_def dest: subtype_sound split: if_splits simp: anno_type_sec_def restrict_preds_to_vars_def stable_def)
lemma tyenv_sec_eq:
"∀x∈𝒞. mem x = mem' x ⟹ types_wellformed Γ ⟹ tyenv_sec mds Γ mem = tyenv_sec mds Γ mem'"
apply(rule ball_cong[OF HOL.refl])
apply(rename_tac x)
apply(rule imp_cong[OF HOL.refl])
apply(subgoal_tac "type_max (the (Γ x)) mem = type_max (the (Γ x)) mem'")
using dma_𝒞 apply fastforce
apply(force intro: 𝒞_eq_type_max_eq simp: types_wellformed_def)
done
lemma context_equiv_tyenv_sec:
"context_equiv Γ⇩2 P⇩2 Γ⇩1 ⟹
pred P⇩2 mem ⟹ tyenv_sec mds Γ⇩2 mem ⟹ tyenv_sec mds Γ⇩1 mem"
apply(clarsimp simp: context_equiv_def type_equiv_def)
apply(rename_tac x y)
apply(rule_tac y="type_max (the (Γ⇩2 x)) mem" in order_trans)
apply(rule subtype_sound[rule_format])
apply force
apply assumption
apply force
done
lemma add_pred_entailment:
"P +⇩𝒮 p ⊢ P"
apply(rule subset_entailment)
apply(rule add_pred_subset)
done
lemma preservation_no_await:
"⟦⊢ Γ,𝒮,P { c } Γ',𝒮',P';
⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩;
no_await c⟧ ⟹
∃ Γ'' 𝒮'' P''. (⊢ Γ'',𝒮'',P'' { c' } Γ',𝒮',P') ∧
(tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶
tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧
pred P'' mem' ∧
tyenv_sec mds' Γ'' mem')"
proof (induct arbitrary: c' mds rule: has_type.induct)
case (anno_type Γ'' Γ 𝒮 upd 𝒮'' P'' P c⇩1 Γ' 𝒮' P')
hence step: "⟨c⇩1, update_modes upd mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
by (metis upd_elim)
from ‹no_await (c⇩1@[upd])› no_await.cases have "no_await c⇩1" by fast
with step anno_type(5) obtain Γ''' 𝒮''' P''' where
"⊢ Γ''',𝒮''',P''' { c' } Γ',𝒮',P' ∧
(tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P'' ∧ pred P'' mem ∧ tyenv_sec (update_modes upd mds) Γ'' mem ⟶
tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
by blast
moreover
have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P''"
using anno_type
apply auto
by (metis tyenv_wellformed_mode_update)
moreover
have pred: "pred P mem ⟶ pred P'' mem"
using anno_type
by (auto simp: pred_def restrict_preds_to_vars_def)
moreover
have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec (update_modes upd mds) Γ'' mem"
apply(rule impI)
apply(rule tyenv_sec_mode_update)
using anno_type apply fastforce
using anno_type pred apply fastforce
using anno_type apply fastforce
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply fastforce
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
by simp
ultimately show ?case
by blast
next
case stop_type
with stop_no_eval show ?case by auto
next
case skip_type
hence "c' = Stop ∧ mds' = mds ∧ mem' = mem"
by (metis skip_elim)
thus ?case
by (metis stop_type)
next
case (assign⇩1 x Γ e t P P' 𝒮 c' mds)
hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
by (metis assign_elim)
from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
by auto
from upd have " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
by (metis stop_type)
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩1 by metis
moreover have "pred P mem ⟶ pred P' mem'"
using pred_preds_update assign⇩1 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec mds Γ mem'"
using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
unfolding tyenv_wellformed_def by blast
ultimately show ?case
by (metis upd)
next
case (assign⇩2 x Γ e t 𝒮 P' P c' mds)
hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
by (metis assign_elim)
let ?Γ' = "Γ (x ↦ t)"
from upd have ty: " ⊢ ?Γ',𝒮,P' {c'} ?Γ',𝒮,P'"
by (metis stop_type)
have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
proof
assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
hence wf: "types_wellformed Γ"
unfolding tyenv_wellformed_def by blast
hence "type_wellformed t"
using assign⇩2(2) type_aexpr_type_wellformed
by blast
with wf have wf': "types_wellformed ?Γ'"
using types_wellformed_update by metis
from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
using types_stable_update
assign⇩2(3)
unfolding tyenv_wellformed_def by blast
have m: "mds_consistent mds Γ 𝒮 P"
using tyenv_wf unfolding tyenv_wellformed_def by blast
from assign⇩2(4) assign⇩2(1)
have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
apply(rule mds_consistent_preds_tyenv_update)
using upd m by simp
from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
unfolding tyenv_wellformed_def by blast
qed
have p: "pred P mem ⟶ pred P' mem'"
using pred_preds_update assign⇩2 upd by metis
have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem ⟹ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' ?Γ' mem'"
proof(clarify)
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem"
assume sec: "tyenv_sec mds Γ mem"
from pred p have pred': "pred P' mem'" by blast
fix v t'
assume Γv: "(Γ(x ↦ t)) v = Some t'"
assume "v ∉ mds' AsmNoReadOrWrite"
show "type_max (the ((Γ(x ↦ t)) v)) mem' ≤ dma mem' v"
proof(cases "v = x")
assume [simp]: "v = x"
hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
using Γv by auto
from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
with pred' show ?thesis
using type_max_dma_type subtype_correct
by fastforce
next
assume neq: "v ≠ x"
hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
by simp
with Γv have Γv: "Γ v = Some t'" by simp
with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem ≤ dma mem v"
by auto
have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
hence dma_eq: "dma mem = dma mem'"
by(rule dma_𝒞)
have f_eq: "type_max t' mem = type_max t' mem'"
apply(rule 𝒞_eq_type_max_eq)
using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
by(rule 𝒞_eq)
from neq Γv f_leq dma_eq f_eq show ?thesis
by simp
qed
qed
from ty wf p sec show ?case
by blast
next
case (assign⇩𝒞 x Γ e t P P' 𝒮 c' mds)
hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
by (metis assign_elim)
hence " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
by (metis stop_type)
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
moreover have "pred P mem ⟶ pred P' mem'"
using pred_preds_update assign⇩𝒞 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' Γ mem'"
proof(clarify)
fix v t'
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem"
hence pred': "pred P' mem'" using ‹pred P mem ⟶ pred P' mem'› by blast
assume sec: "tyenv_sec mds Γ mem"
assume Γv: "Γ v = Some t'"
assume readable': "v ∉ mds' AsmNoReadOrWrite"
with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
show "type_max (the (Γ v)) mem' ≤ dma mem' v"
proof(cases "x ∈ 𝒞_vars v")
assume "x ∈ 𝒞_vars v"
with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
from pred' Γv subtype_correct this show ?thesis
using type_max_dma_type by(auto simp: to_total_def split: if_splits)
next
assume "x ∉ 𝒞_vars v"
hence "∀v'∈𝒞_vars v. mem v' = mem' v'"
using upd by auto
hence dma_eq: "dma mem v = dma mem' v"
by(rule dma_𝒞_vars)
from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
have "type_wellformed t'"
using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem = type_max t' mem'"
using vars_of_type_eq_type_max_eq by fastforce
from sec Γv readable have "type_max t' mem ≤ dma mem v"
by auto
with f_eq dma_eq Γv show ?thesis
by simp
qed
qed
ultimately show ?case
by (metis)
next
case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''' c' mds)
from if_type(13)
show ?case
proof(rule if_elim)
assume [simp]: "ev⇩B mem e" and [simp]: "c' = th" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
from if_type(3) have " ⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ',𝒮',P'" by simp
hence "⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ''',𝒮',P'''"
apply(rule sub)
apply simp+
using if_type apply blast
using if_type apply blast
apply simp
using if_type apply(blast intro: pred_entailment_trans)
done
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 e)"
by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
moreover have "pred P mem ⟶ pred (P +⇩𝒮 e) mem'"
by(auto simp: pred_def add_pred_def)
moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
by(simp)
ultimately show ?case by blast
next
assume [simp]: "¬ ev⇩B mem e" and [simp]: "c' = el" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
from if_type(5) have " ⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ'',𝒮',P''" by simp
hence "⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ''',𝒮',P'''"
apply(rule sub)
apply simp+
using if_type apply blast
using if_type apply blast
apply simp
using if_type apply(blast intro: pred_entailment_trans)
done
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 bexp_neg e)"
by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
moreover have "pred P mem ⟶ pred (P +⇩𝒮 bexp_neg e) mem'"
by(auto simp: pred_def add_pred_def bexp_neg_negates)
moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
by(simp)
ultimately show ?case by blast
qed
next
case (while_type Γ e t P 𝒮 c c' mds)
hence [simp]: "mds' = mds ∧ c' = If e (c ;; While e c) Stop ∧ mem' = mem"
by (metis while_elim)
have " ⊢ Γ,𝒮,P {c'} Γ,𝒮,P"
apply simp
apply(rule if_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule seq_type)
apply(rule while_type(3))
apply(rule has_type.while_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule while_type(3))
apply(rule stop_type)
apply simp
apply simp
apply simp
apply(rule add_pred_entailment)
apply simp+
by(blast intro!: tyenv_wellformed_subset add_pred_subset)
thus ?case
by fastforce
next
case (seq_type Γ 𝒮 P c⇩1 Γ⇩1 𝒮⇩1 P⇩1 c⇩2 Γ⇩2 𝒮⇩2 P⇩2 c' mds)
thus ?case
proof (cases "c⇩1 = Stop")
assume [simp]: "c⇩1 = Stop"
with seq_type have [simp]: "mds' = mds" and [simp]: "c' = c⇩2" and [simp]: "mem' = mem"
by (metis seq_stop_elim)+
have context_eq: "context_equiv Γ P Γ⇩1" and [simp]: "𝒮⇩1 = 𝒮" and entail: "P ⊢ P⇩1" and
wf_imp: "∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1"
using stop_cxt seq_type(1) by simp+
have "⊢ Γ,𝒮,P {c⇩2} Γ⇩2,𝒮⇩2,P⇩2"
apply(rule sub)
using seq_type(3) apply simp
apply(rule context_eq)
apply(rule wf_imp)
apply simp+
apply(rule entail)
apply(rule pred_entailment_refl)
done
thus ?case
by fastforce
next
assume "c⇩1 ≠ Stop"
then obtain c⇩1' where step: "⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = (c⇩1' ;; c⇩2)"
by (metis seq_elim seq_type.prems)
then have "no_await c⇩1" using ‹no_await (c⇩1 ;; c⇩2)› no_await.cases by blast
then obtain Γ''' 𝒮''' P''' where "⊢ Γ''',𝒮''',P''' {c⇩1'} Γ⇩1,𝒮⇩1,P⇩1 ∧
(tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶
tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
using step seq_type(2)
by blast
moreover
from seq_type have "⊢ Γ⇩1,𝒮⇩1,P⇩1 {c⇩2} Γ⇩2,𝒮⇩2,P⇩2" by auto
moreover
ultimately show ?case
apply (rule_tac x = Γ''' in exI)
using ‹⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = c⇩1' ;; c⇩2› by blast
qed
next
case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' c' mds)
then obtain Γ'' 𝒮'' P'' where stuff: "⊢ Γ'',𝒮'',P'' { c' } Γ⇩1',𝒮',P⇩1' ∧
(tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem ⟶
tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem')"
by force
have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem ∧ tyenv_sec mds Γ⇩2 mem ⟹
tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem"
apply(rule conjI)
using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
apply blast
apply(rule conjI)
using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast
show ?case
apply (rule_tac x = Γ'' in exI, rule_tac x = "𝒮''" in exI, rule_tac x="P''" in exI)
apply (rule conjI)
apply(rule has_type.sub)
apply(rule stuff[THEN conjunct1])
apply simp+
apply(rule sub(5))
apply(rule sub(6))
apply simp
using sub apply blast
using imp stuff apply blast
done
next
case (await_type Γ e t P 𝒮 c Γ' 𝒮' P' c' mds)
show ?case using no_await_no_await await_type.prems by blast
qed
lemma preservation_no_await_plus:
"⟦⟨c, mds, mem⟩ ↝⇧+ ⟨c', mds', mem'⟩;
⊢ Γ,𝒮,P { c } Γ',𝒮',P';
no_await c⟧ ⟹
no_await c' ∧ (∃ Γ'' 𝒮'' P''. (⊢ Γ'',𝒮'',P'' { c' } Γ',𝒮',P') ∧
(tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶
tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem'))"
apply (induct arbitrary: Γ 𝒮 P rule: my_trancl_step_induct3)
using preservation_no_await no_await_trans apply fast
using preservation_no_await no_await_trans by metis
lemma preservation:
assumes typed: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
assumes eval: "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
shows "∃ Γ'' 𝒮'' P''. (⊢ Γ'',𝒮'',P'' { c' } Γ',𝒮',P') ∧
(tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶
tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem')"
using typed eval
proof (induct arbitrary: c' mds rule: has_type.induct)
case (anno_type Γ'' Γ 𝒮 upd 𝒮'' P'' P c⇩1 Γ' 𝒮' P')
hence "⟨c⇩1, update_modes upd mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
by (metis upd_elim)
with anno_type(5) obtain Γ''' 𝒮''' P''' where
"⊢ Γ''',𝒮''',P''' { c' } Γ',𝒮',P' ∧
(tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P'' ∧ pred P'' mem ∧ tyenv_sec (update_modes upd mds) Γ'' mem ⟶
tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
by blast
moreover
have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P''"
using anno_type
apply auto
by (metis tyenv_wellformed_mode_update)
moreover
have pred: "pred P mem ⟶ pred P'' mem"
using anno_type
by (auto simp: pred_def restrict_preds_to_vars_def)
moreover
have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec (update_modes upd mds) Γ'' mem"
apply(rule impI)
apply(rule tyenv_sec_mode_update)
using anno_type apply fastforce
using anno_type pred apply fastforce
using anno_type apply fastforce
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply fastforce
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
by simp
ultimately show ?case
by blast
next
case stop_type
with stop_no_eval show ?case ..
next
case skip_type
hence "c' = Stop ∧ mds' = mds ∧ mem' = mem"
by (metis skip_elim)
thus ?case
by (metis stop_type)
next
case (assign⇩1 x Γ e t P P' 𝒮 c' mds)
hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
by (metis assign_elim)
from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
by auto
from upd have " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
by (metis stop_type)
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩1 by metis
moreover have "pred P mem ⟶ pred P' mem'"
using pred_preds_update assign⇩1 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec mds Γ mem'"
using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
unfolding tyenv_wellformed_def by blast
ultimately show ?case
by (metis upd)
next
case (assign⇩2 x Γ e t 𝒮 P' P c' mds)
hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
by (metis assign_elim)
let ?Γ' = "Γ (x ↦ t)"
from upd have ty: " ⊢ ?Γ',𝒮,P' {c'} ?Γ',𝒮,P'"
by (metis stop_type)
have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
proof
assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
hence wf: "types_wellformed Γ"
unfolding tyenv_wellformed_def by blast
hence "type_wellformed t"
using assign⇩2(2) type_aexpr_type_wellformed
by blast
with wf have wf': "types_wellformed ?Γ'"
using types_wellformed_update by metis
from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
using types_stable_update
assign⇩2(3)
unfolding tyenv_wellformed_def by blast
have m: "mds_consistent mds Γ 𝒮 P"
using tyenv_wf unfolding tyenv_wellformed_def by blast
from assign⇩2(4) assign⇩2(1)
have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
apply(rule mds_consistent_preds_tyenv_update)
using upd m by simp
from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
unfolding tyenv_wellformed_def by blast
qed
have p: "pred P mem ⟶ pred P' mem'"
using pred_preds_update assign⇩2 upd by metis
have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem ⟹ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' ?Γ' mem'"
proof(clarify)
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem"
assume sec: "tyenv_sec mds Γ mem"
from pred p have pred': "pred P' mem'" by blast
fix v t'
assume Γv: "(Γ(x ↦ t)) v = Some t'"
assume "v ∉ mds' AsmNoReadOrWrite"
show "type_max (the ((Γ(x ↦ t)) v)) mem' ≤ dma mem' v"
proof(cases "v = x")
assume [simp]: "v = x"
hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
using Γv by auto
from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
with pred' show ?thesis
using type_max_dma_type subtype_correct
by fastforce
next
assume neq: "v ≠ x"
hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
by simp
with Γv have Γv: "Γ v = Some t'" by simp
with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem ≤ dma mem v"
by auto
have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
hence dma_eq: "dma mem = dma mem'"
by(rule dma_𝒞)
have f_eq: "type_max t' mem = type_max t' mem'"
apply(rule 𝒞_eq_type_max_eq)
using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
by(rule 𝒞_eq)
from neq Γv f_leq dma_eq f_eq show ?thesis
by simp
qed
qed
from ty wf p sec show ?case
by blast
next
case (assign⇩𝒞 x Γ e t P P' 𝒮 c' mds)
hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
by (metis assign_elim)
hence " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
by (metis stop_type)
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
moreover have "pred P mem ⟶ pred P' mem'"
using pred_preds_update assign⇩𝒞 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' Γ mem'"
proof(clarify)
fix v t'
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem"
hence pred': "pred P' mem'" using ‹pred P mem ⟶ pred P' mem'› by blast
assume sec: "tyenv_sec mds Γ mem"
assume Γv: "Γ v = Some t'"
assume readable': "v ∉ mds' AsmNoReadOrWrite"
with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
show "type_max (the (Γ v)) mem' ≤ dma mem' v"
proof(cases "x ∈ 𝒞_vars v")
assume "x ∈ 𝒞_vars v"
with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
from pred' Γv subtype_sound[OF this] show ?thesis
using type_max_dma_type by(auto simp: to_total_def split: if_splits)
next
assume "x ∉ 𝒞_vars v"
hence "∀v'∈𝒞_vars v. mem v' = mem' v'"
using upd by auto
hence dma_eq: "dma mem v = dma mem' v"
by(rule dma_𝒞_vars)
from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
have "type_wellformed t'"
using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem = type_max t' mem'"
using vars_of_type_eq_type_max_eq by fastforce
from sec Γv readable have "type_max t' mem ≤ dma mem v"
by auto
with f_eq dma_eq Γv show ?thesis
by simp
qed
qed
ultimately show ?case
by (metis stop_type)
next
case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''' c' mds)
from if_type(13)
show ?case
proof(rule if_elim)
assume [simp]: "ev⇩B mem e" and [simp]: "c' = th" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
from if_type(3) have " ⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ',𝒮',P'" by simp
hence "⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ''',𝒮',P'''"
apply(rule sub)
apply simp+
using if_type apply blast
using if_type apply blast
apply simp
using if_type apply(blast intro: pred_entailment_trans)
done
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 e)"
by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
moreover have "pred P mem ⟶ pred (P +⇩𝒮 e) mem'"
by(auto simp: pred_def add_pred_def)
moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
by(simp)
ultimately show ?case by blast
next
assume [simp]: "¬ ev⇩B mem e" and [simp]: "c' = el" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
from if_type(5) have " ⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ'',𝒮',P''" by simp
hence "⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ''',𝒮',P'''"
apply(rule sub)
apply simp+
using if_type apply blast
using if_type apply blast
apply simp
using if_type apply(blast intro: pred_entailment_trans)
done
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 bexp_neg e)"
by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
moreover have "pred P mem ⟶ pred (P +⇩𝒮 bexp_neg e) mem'"
by(auto simp: pred_def add_pred_def bexp_neg_negates)
moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
by(simp)
ultimately show ?case by blast
qed
next
case (while_type Γ e t P 𝒮 c c' mds)
hence [simp]: "mds' = mds ∧ c' = If e (c ;; While e c) Stop ∧ mem' = mem"
by (metis while_elim)
have " ⊢ Γ,𝒮,P {c'} Γ,𝒮,P"
apply simp
apply(rule if_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule seq_type)
apply(rule while_type(3))
apply(rule has_type.while_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule while_type(3))
apply(rule stop_type)
apply simp
apply simp
apply simp
apply(rule add_pred_entailment)
apply simp+
by(blast intro!: tyenv_wellformed_subset add_pred_subset)
thus ?case
by fastforce
next
case (seq_type Γ 𝒮 P c⇩1 Γ⇩1 𝒮⇩1 P⇩1 c⇩2 Γ⇩2 𝒮⇩2 P⇩2 c' mds)
thus ?case
proof (cases "c⇩1 = Stop")
assume [simp]: "c⇩1 = Stop"
with seq_type have [simp]: "mds' = mds" and [simp]: "c' = c⇩2" and [simp]: "mem' = mem"
by (metis seq_stop_elim)+
have context_eq: "context_equiv Γ P Γ⇩1" and [simp]: "𝒮⇩1 = 𝒮" and entail: "P ⊢ P⇩1" and
wf_imp: "∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1"
using stop_cxt seq_type(1) by simp+
have "⊢ Γ,𝒮,P {c⇩2} Γ⇩2,𝒮⇩2,P⇩2"
apply(rule sub)
using seq_type(3) apply simp
apply(rule context_eq)
apply(rule wf_imp)
apply simp+
apply(rule entail)
apply(rule pred_entailment_refl)
done
thus ?case
by fastforce
next
assume "c⇩1 ≠ Stop"
then obtain c⇩1' where "⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = (c⇩1' ;; c⇩2)"
by (metis seq_elim seq_type.prems)
then obtain Γ''' 𝒮''' P''' where "⊢ Γ''',𝒮''',P''' {c⇩1'} Γ⇩1,𝒮⇩1,P⇩1 ∧
(tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶
tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
using seq_type(2)
by force
moreover
from seq_type have "⊢ Γ⇩1,𝒮⇩1,P⇩1 {c⇩2} Γ⇩2,𝒮⇩2,P⇩2" by auto
moreover
ultimately show ?case
apply (rule_tac x = Γ''' in exI)
using ‹⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = c⇩1' ;; c⇩2› by blast
qed
next
case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' c' mds)
then obtain Γ'' 𝒮'' P'' where stuff: "⊢ Γ'',𝒮'',P'' { c' } Γ⇩1',𝒮',P⇩1' ∧
(tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem ⟶
tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem')"
by force
have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem ∧ tyenv_sec mds Γ⇩2 mem ⟹
tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem"
apply(rule conjI)
using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
apply blast
apply(rule conjI)
using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast
show ?case
apply (rule_tac x = Γ'' in exI, rule_tac x = "𝒮''" in exI, rule_tac x="P''" in exI)
apply (rule conjI)
apply(rule has_type.sub)
apply(rule stuff[THEN conjunct1])
apply simp+
apply(rule sub(5))
apply(rule sub(6))
apply simp
using sub apply blast
using imp stuff apply blast
done
next
case (await_type Γ e t P 𝒮 c Γ' 𝒮' P' c' mds)
from this show ?case
apply simp
apply (drule await_elim, clarsimp)
apply (drule preservation_no_await_plus[of c mds mem c' mds' mem' Γ 𝒮 "P +⇩𝒮 e" Γ' 𝒮' P'], assumption+)
apply (subgoal_tac "⟦ tyenv_wellformed mds Γ 𝒮 P ⟧ ⟹ tyenv_wellformed mds Γ 𝒮 P +⇩𝒮 e") defer
apply (unfold add_pred_def)[1]
apply (case_tac "pred_stable 𝒮 e", clarsimp)
apply (unfold tyenv_wellformed_def, clarsimp)[1]
apply (unfold mds_consistent_def, clarsimp)[1]
apply clarsimp
apply (subgoal_tac "pred P mem ⟹ pred P +⇩𝒮 e mem") defer
apply (unfold add_pred_def)[1]
apply (case_tac "pred_stable 𝒮 e", clarsimp)
apply (unfold pred_def, clarsimp)[1]
apply clarsimp
apply clarsimp
using has_type.sub by (metis context_equiv_refl pred_entailment_refl)
qed
inductive_cases await_type_elim: "⊢ Γ,𝒮,P {Await b ca} Γ',𝒮',P'"
fun bisim_helper :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒ bool"
where
"bisim_helper ⟨c⇩1, mds, mem⇩1⟩ ⟨c⇩2, mds⇩2, mem⇩2⟩ = mem⇩1 =⇘mds⇙⇧l mem⇩2"
lemma ℛ⇩3_mem_eq: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ mem⇩1 =⇘mds⇙⇧l mem⇩2"
apply (subgoal_tac "bisim_helper ⟨c⇩1, mds, mem⇩1⟩ ⟨c⇩2, mds, mem⇩2⟩")
apply simp
apply (induct rule: ℛ⇩3_aux.induct)
by (auto simp: ℛ⇩1_mem_eq)
lemma ev⇩A_eq:
assumes tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
assumes pred: "pred P mem⇩1"
assumes e_type: "Γ ⊢⇩a e ∈ t"
assumes subtype: "t ≤:⇩P (dma_type v)"
assumes is_Low: "dma mem⇩1 v = Low"
shows "ev⇩A mem⇩1 e = ev⇩A mem⇩2 e"
proof(rule eval_vars_det⇩A, clarify)
fix x
assume in_vars: "x ∈ aexp_vars e"
have "type_max (to_total Γ x) mem⇩1 = Low"
proof -
from subtype_sound[OF subtype] pred have "type_max t mem⇩1 ≤ dma mem⇩1 v"
by(auto)
with is_Low have "type_max t mem⇩1 = Low" by(auto simp: less_eq_Sec_def)
with e_type in_vars show ?thesis
apply -
apply(erule type_aexpr.cases)
using Sec.exhaust by(auto simp: type_max_def split: if_splits)
qed
thus "mem⇩1 x = mem⇩2 x"
using tyenv_eq unfolding tyenv_eq_def by blast
qed
lemma ev⇩A_eq':
assumes tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
assumes pred: "pred P mem⇩1"
assumes e_type: "Γ ⊢⇩a e ∈ t"
assumes subtype: "P ⊢ t"
shows "ev⇩A mem⇩1 e = ev⇩A mem⇩2 e"
proof(rule eval_vars_det⇩A, clarify)
fix x
assume in_vars: "x ∈ aexp_vars e"
have "type_max (to_total Γ x) mem⇩1 = Low"
proof -
from subtype pred have "type_max t mem⇩1 ≤ Low"
by(auto simp: type_max_def pred_entailment_def pred_def)
hence "type_max t mem⇩1 = Low" by(auto simp: less_eq_Sec_def)
with e_type in_vars show ?thesis
apply -
apply(erule type_aexpr.cases)
using Sec.exhaust by(auto simp: type_max_def split: if_splits)
qed
thus "mem⇩1 x = mem⇩2 x"
using tyenv_eq unfolding tyenv_eq_def by blast
qed
lemma ev⇩B_eq':
assumes tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
assumes pred: "pred P mem⇩1"
assumes e_type: "Γ ⊢⇩b e ∈ t"
assumes subtype: "P ⊢ t"
shows "ev⇩B mem⇩1 e = ev⇩B mem⇩2 e"
proof(rule eval_vars_det⇩B, clarify)
fix x
assume in_vars: "x ∈ bexp_vars e"
have "type_max (to_total Γ x) mem⇩1 = Low"
proof -
from subtype pred have "type_max t mem⇩1 ≤ Low"
by(auto simp: type_max_def pred_entailment_def pred_def)
hence "type_max t mem⇩1 = Low" by(auto simp: less_eq_Sec_def)
with e_type in_vars show ?thesis
apply -
apply(erule type_bexpr.cases)
using Sec.exhaust by(auto simp: type_max_def split: if_splits)
qed
thus "mem⇩1 x = mem⇩2 x"
using tyenv_eq unfolding tyenv_eq_def by blast
qed
lemma R1_equiv_entailment:
"⟨c, mds, mem⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c', mds', mem'⟩ ⟹
context_equiv Γ' P' Γ'' ⟹ P' ⊢ P'' ⟹
∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ'' 𝒮' P'' ⟹
⟨c, mds, mem⟩ ℛ⇧1⇘Γ'',𝒮',P''⇙ ⟨c', mds', mem'⟩"
apply(induct rule: ℛ⇩1.induct)
apply(rule ℛ⇩1.intro)
apply(blast intro: sub context_equiv_refl pred_entailment_refl)+
done
lemma R3_equiv_entailment:
"⟨c, mds, mem⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c', mds', mem'⟩ ⟹
context_equiv Γ' P' Γ'' ⟹ P' ⊢ P'' ⟹
∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ'' 𝒮' P'' ⟹
⟨c, mds, mem⟩ ℛ⇧3⇘Γ'',𝒮',P''⇙ ⟨c', mds', mem'⟩"
apply(induct rule: ℛ⇩3_aux.induct)
apply(erule ℛ⇩3_aux.intro⇩1)
apply(blast intro: sub context_equiv_refl tyenv_wellformed_subset subset_entailment)
apply(erule ℛ⇩3_aux.intro⇩3)
apply(blast intro: sub context_equiv_refl tyenv_wellformed_subset subset_entailment)
done
lemma R_equiv_entailment:
"lc⇩1 ℛ⇧u⇘Γ',𝒮',P'⇙ lc⇩2 ⟹
context_equiv Γ' P' Γ'' ⟹ P' ⊢ P'' ⟹
∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ'' 𝒮' P'' ⟹
lc⇩1 ℛ⇧u⇘Γ'',𝒮',P''⇙ lc⇩2"
apply(induct rule: ℛ.induct)
apply clarsimp
apply(rule ℛ.intro⇩1)
apply(fastforce intro: R1_equiv_entailment)
apply(rule ℛ.intro⇩3)
apply(fastforce intro: R3_equiv_entailment)
done
lemma context_equiv_tyenv_eq:
"tyenv_eq Γ mem mem' ⟹ context_equiv Γ P Γ' ⟹ pred P mem ⟹ tyenv_eq Γ' mem mem'"
apply(clarsimp simp: tyenv_eq_def to_total_def context_equiv_def split: if_splits simp: type_equiv_def)
using subtype_trans subtype_sound
by (metis domI less_eq_Sec_def option.sel)
lemma ℛ_typed_step_no_await:
"⟦ ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P' ;
tyenv_wellformed mds Γ 𝒮 P; mem⇩1 =⇘Γ⇙ mem⇩2; pred P mem⇩1;
pred P mem⇩2; tyenv_sec mds Γ mem⇩1;
⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩; no_await c⇩1 ⟧ ⟹
(∃ c⇩2' mem⇩2'. ⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
proof (induct arbitrary: mds c⇩1' rule: has_type.induct)
case (seq_type Γ 𝒮 P c⇩1 Γ'' 𝒮'' P'' c⇩2 Γ' 𝒮' P' mds)
show ?case
proof (cases "c⇩1 = Stop")
assume "c⇩1 = Stop"
hence [simp]: "c⇩1' = c⇩2" "mds' = mds" "mem⇩1' = mem⇩1"
using seq_type
by (auto simp: seq_stop_elim)
from seq_type ‹c⇩1 = Stop› have "context_equiv Γ P Γ''" and "𝒮 = 𝒮''" and "P ⊢ P''" and
"(∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ'' 𝒮 P'')"
by (metis stop_cxt)+
hence "⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'"
apply -
apply(rule sub)
using seq_type(3) apply simp
by auto
have "⟨c⇩2, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
apply (rule ℛ⇩1.intro [of Γ])
apply(rule ‹⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'›)
using seq_type by auto
thus ?case
using ℛ.intro⇩1
apply clarify
apply (rule_tac x = c⇩2 in exI)
apply (rule_tac x = mem⇩2 in exI)
by (auto simp: ‹c⇩1 = Stop› seq_stop_eval⇩w ℛ.intro⇩1)
next
assume "c⇩1 ≠ Stop"
with ‹⟨c⇩1 ;; c⇩2, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› obtain c⇩1'' where c⇩1''_props:
"⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = c⇩1'' ;; c⇩2"
by (metis seq_elim)
with ‹no_await (c⇩1 ;; c⇩2)› have "no_await c⇩1" using no_await.cases by blast
with seq_type(2) ‹no_await c⇩1› obtain c⇩2'' mem⇩2' where c⇩2''_props:
"⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩ ∧ ⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
using seq_type.prems(1) seq_type.prems(2) seq_type.prems(3) seq_type.prems(4) seq_type.prems(5) c⇩1''_props
by blast
hence "⟨c⇩1'' ;; c⇩2, mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
apply (rule conjE)
apply (erule ℛ_elim, auto)
apply (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩1 seq_type(3))
by (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩3 seq_type(3))
moreover
from c⇩2''_props have "⟨c⇩1 ;; c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
by (metis eval⇩w.seq)
ultimately show ?case
by (metis c⇩1''_props)
qed
next
case (anno_type Γ' Γ 𝒮 upd 𝒮' P' P c Γ'' 𝒮'' P'' mds)
have "mem⇩1 =⇘Γ'⇙ mem⇩2"
proof(clarsimp simp: tyenv_eq_def)
fix x
assume a: "type_max (to_total Γ' x) mem⇩1 = Low"
hence "type_max (to_total Γ x) mem⇩1 = Low"
proof -
from ‹pred P mem⇩1› have "pred P' mem⇩1"
using anno_type.hyps(3)
by(auto simp: restrict_preds_to_vars_def pred_def)
with subtype_correct anno_type.hyps(7) a
show ?thesis
using less_eq_Sec_def by metis
qed
thus " mem⇩1 x = mem⇩2 x"
using anno_type.prems(2)
unfolding tyenv_eq_def by blast
qed
have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ' 𝒮' P'"
using anno_type
apply auto
by (metis tyenv_wellformed_mode_update)
moreover
have pred: "pred P mem⇩1 ⟶ pred P' mem⇩1"
using anno_type
by (auto simp: pred_def restrict_preds_to_vars_def)
moreover
have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟶
tyenv_sec (update_modes upd mds) Γ' mem⇩1"
apply(rule impI)
apply(rule tyenv_sec_mode_update)
using anno_type apply fastforce
using anno_type pred apply fastforce
using anno_type apply fastforce
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply fastforce
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
by simp
from ‹no_await (c@[upd])› have "no_await c" using no_await.cases by blast
ultimately obtain c⇩2' mem⇩2' where "(⟨c, update_modes upd mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
using anno_type
apply auto
using ‹mem⇩1 =⇘Γ'⇙ mem⇩2› local.pred_def restrict_preds_to_vars_def upd_elim ‹no_await c›
using ‹tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ (∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x) ⟶ (∀x∈dom Γ'. x ∉ update_modes upd mds AsmNoReadOrWrite ⟶ type_max (the (Γ' x)) mem⇩1 ≤ dma mem⇩1 x)› mem_Collect_eq by fastforce try0
thus ?case
apply (rule_tac x = c⇩2' in exI)
apply (rule_tac x = mem⇩2' in exI)
apply auto
by (metis cxt_to_stmt.simps(1) eval⇩w.decl)
next
case stop_type
with stop_no_eval show ?case by auto
next
case (skip_type Γ 𝒮 P mds)
moreover
with skip_type have [simp]: "mds' = mds" "c⇩1' = Stop" "mem⇩1' = mem⇩1"
using skip_elim
by (metis, metis, metis)
with skip_type have "⟨Stop, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨Stop, mds, mem⇩2⟩"
by auto
thus ?case
using ℛ.intro⇩1 and unannotated [where c = Skip and E = "[]"]
apply auto
by (metis (mono_tags, lifting) ℛ.intro⇩1 old.prod.case skip_eval⇩w)
next
case (assign⇩1 x Γ e t P P' 𝒮 mds)
hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
using assign_elim
by (auto, metis)
from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
by auto
have dma_eq [simp]: "dma mem⇩1 = dma mem⇩1'"
using dma_𝒞 assign⇩1(2) by simp
have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
unfolding tyenv_eq_def
proof(clarify)
fix v
assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
proof(cases "v ∈ dom Γ")
assume [simp]: "v ∈ dom Γ"
then obtain t' where [simp]: "Γ v = Some t'" by force
hence [simp]: "(to_total Γ v) = t'"
unfolding to_total_def by (auto split: if_splits)
have "type_max t' mem⇩1 = type_max t' mem⇩1'"
apply(rule 𝒞_eq_type_max_eq)
using ‹Γ v = Some t'› assign⇩1(6)
unfolding tyenv_wellformed_def types_wellformed_def
apply (metis ‹v ∈ dom Γ› option.sel)
using assign⇩1(2) apply simp
done
with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
by simp
from assign⇩1(1) ‹v ∈ dom Γ› have "x ≠ v" by auto
thus ?thesis
apply simp
using is_Low assign⇩1(7) unfolding tyenv_eq_def by auto
next
assume "v ∉ dom Γ"
hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
unfolding to_total_def by simp
with is_Low' have "dma mem⇩1' v = Low" by simp
with dma_eq have dma_v_Low: "dma mem⇩1 v = Low" by simp
hence is_Low: "type_max (to_total Γ v) mem⇩1 = Low" by simp
show ?thesis
proof(cases "x = v")
assume "x ≠ v"
thus ?thesis
apply simp
using is_Low assign⇩1(7) unfolding tyenv_eq_def by blast
next
assume "x = v"
thus ?thesis
apply simp
apply(rule ev⇩A_eq)
apply(rule assign⇩1(7))
apply(rule assign⇩1(8))
apply(rule assign⇩1(3))
apply(rule assign⇩1(4))
using dma_v_Low by simp
qed
qed
qed
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩1 by metis
moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
using pred_preds_update assign⇩1 upd by metis
moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
using pred_preds_update assign⇩1 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ tyenv_sec mds Γ mem⇩1 ⟶ tyenv_sec mds Γ mem⇩1'"
using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
unfolding tyenv_wellformed_def by blast
ultimately have ℛ':
"⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
apply -
apply (rule ℛ.intro⇩1, auto simp: assign⇩1 simp del: dma_eq)
done
have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)
from ℛ' a show ?case
using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
by blast
next
case (assign⇩𝒞 x Γ e t P P' 𝒮 mds)
hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
using assign_elim
by (auto, metis)
have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
unfolding tyenv_eq_def
proof(clarify)
fix v
assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
proof(cases "v ∈ dom Γ")
assume in_dom [simp]: "v ∈ dom Γ"
then obtain t' where Γv [simp]: "Γ v = Some t'" by force
hence [simp]: "(to_total Γ v) = t'"
unfolding to_total_def by (auto split: if_splits)
from assign⇩𝒞(4) have x_nin_C: "x ∉ vars_of_type t'"
using in_dom Γv
by (metis option.sel snd_conv)
have Γv_wf: "type_wellformed t'"
using in_dom Γv assign⇩𝒞(7) unfolding tyenv_wellformed_def types_wellformed_def
by (metis option.sel)
with x_nin_C have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
using vars_of_type_eq_type_max_eq by simp
with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
by simp
from assign⇩𝒞(1) ‹v ∈ dom Γ› assign⇩𝒞(7) have "x ≠ v"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
thus ?thesis
apply simp
using is_Low assign⇩𝒞(8) unfolding tyenv_eq_def by auto
next
assume nin_dom: "v ∉ dom Γ"
hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
unfolding to_total_def by simp
with is_Low' have "dma mem⇩1' v = Low" by simp
show ?thesis
proof(cases "x = v")
assume "x = v"
thus ?thesis
apply simp
apply(rule ev⇩A_eq')
apply(rule assign⇩𝒞(8))
apply(rule assign⇩𝒞(9))
apply(rule assign⇩𝒞(2))
by(rule assign⇩𝒞(3))
next
assume [simp]: "x ≠ v"
show ?thesis
proof(cases "x ∈ 𝒞_vars v")
assume in_𝒞_vars: "x ∈ 𝒞_vars v"
hence "v ∉ 𝒞"
using 𝒞_vars_𝒞 by auto
with nin_dom have "v ∉ snd 𝒮"
using assign⇩𝒞(7)
by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def)
with in_𝒞_vars have "P ⊢ (to_total Γ v)"
using assign⇩𝒞(6) by blast
with assign⇩𝒞(9) have "type_max (to_total Γ v) mem⇩1 = Low"
by(auto simp: type_max_def pred_def pred_entailment_def)
thus ?thesis
using not_sym[OF ‹x ≠ v›]
apply simp
using assign⇩𝒞(8)
unfolding tyenv_eq_def by auto
next
assume "x ∉ 𝒞_vars v"
with is_Low' have "dma mem⇩1 v = Low"
using dma_𝒞_vars ‹⋀mem. type_max (to_total Γ v) mem = dma mem v›
by (metis fun_upd_other)
thus ?thesis
using not_sym[OF ‹x ≠ v›]
apply simp
using assign⇩𝒞(8)
unfolding tyenv_eq_def by auto
qed
qed
qed
qed
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
using pred_preds_update assign⇩𝒞 upd by metis
moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
using pred_preds_update assign⇩𝒞 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' Γ mem⇩1'"
proof(clarify)
fix v t'
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem⇩1"
hence pred': "pred P' mem⇩1'" using ‹pred P mem⇩1 ⟶ pred P' mem⇩1'› by blast
assume sec: "tyenv_sec mds Γ mem⇩1"
assume Γv: "Γ v = Some t'"
assume readable': "v ∉ mds' AsmNoReadOrWrite"
with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
show "type_max (the (Γ v)) mem⇩1' ≤ dma mem⇩1' v"
proof(cases "x ∈ 𝒞_vars v")
assume "x ∈ 𝒞_vars v"
with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
from pred' Γv subtype_correct this show ?thesis
using type_max_dma_type by(auto simp: to_total_def split: if_splits)
next
assume "x ∉ 𝒞_vars v"
hence "∀v'∈𝒞_vars v. mem⇩1 v' = mem⇩1' v'"
using upd by auto
hence dma_eq: "dma mem⇩1 v = dma mem⇩1' v"
by(rule dma_𝒞_vars)
from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
have "type_wellformed t'"
using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
using vars_of_type_eq_type_max_eq by fastforce
from sec Γv readable have "type_max t' mem⇩1 ≤ dma mem⇩1 v"
by auto
with f_eq dma_eq Γv show ?thesis
by simp
qed
qed
ultimately have ℛ':
"⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
apply -
apply (rule ℛ.intro⇩1, auto simp: assign⇩𝒞)
done
have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)
from ℛ' a show ?case
using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
by blast
next
case (assign⇩2 x Γ e t 𝒮 P' P mds)
have upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
using assign_elim[OF assign⇩2(11)]
by auto
from ‹x ∈ dom Γ› ‹tyenv_wellformed mds Γ 𝒮 P›
have x_nin_𝒞: "x ∉ 𝒞"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
hence dma_eq [simp]: "dma mem⇩1' = dma mem⇩1"
using dma_𝒞 assign⇩2
by auto
let ?Γ' = "Γ (x ↦ t)"
have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
using assign⇩2
by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.assign eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
moreover
have tyenv_eq': "mem⇩1(x := ev⇩A mem⇩1 e) =⇘Γ(x ↦ t)⇙ mem⇩2(x := ev⇩A mem⇩2 e)"
unfolding tyenv_eq_def
proof(clarify)
fix v
assume is_Low': "type_max (to_total (Γ(x ↦ t)) v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
proof(cases "v = x")
assume neq: "v ≠ x"
hence "type_max (to_total Γ v) mem⇩1 = Low"
proof(cases "v ∈ dom Γ")
assume "v ∈ dom Γ"
then obtain t' where [simp]: "Γ v = Some t'" by force
hence [simp]: "(to_total Γ v) = t'"
unfolding to_total_def by (auto split: if_splits)
hence [simp]: "(to_total ?Γ' v) = t'"
using neq by(auto simp: to_total_def)
have "type_max t' mem⇩1 = type_max t' mem⇩1'"
apply(rule 𝒞_eq_type_max_eq)
using assign⇩2(6)
apply(clarsimp simp: tyenv_wellformed_def types_wellformed_def)
using ‹v ∈ dom Γ› ‹Γ v = Some t'› apply(metis option.sel)
using x_nin_𝒞 by simp
from this is_Low' neq neq[THEN not_sym] show "type_max (to_total Γ v) mem⇩1 = Low"
by auto
next
assume "v ∉ dom Γ"
with is_Low' neq
have "dma mem⇩1' v = Low"
by(auto simp: to_total_def split: if_splits)
with dma_eq ‹v ∉ dom Γ› show ?thesis
by(auto simp: to_total_def split: if_splits)
qed
with neq assign⇩2(7) show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
by(auto simp: tyenv_eq_def)
next
assume eq[simp]: "v = x"
with is_Low' ‹x ∈ dom Γ› have t_Low': "type_max t mem⇩1' = Low"
by(auto simp: to_total_def split: if_splits)
have wf_t: "type_wellformed t"
using type_aexpr_type_wellformed assign⇩2(2) assign⇩2(6)
by(fastforce simp: tyenv_wellformed_def)
with t_Low' ‹x ∉ 𝒞› have t_Low: "type_max t mem⇩1 = Low"
using 𝒞_eq_type_max_eq
by (metis (no_types, lifting) fun_upd_other upd(3))
show ?thesis
proof(simp, rule eval_vars_det⇩A, clarify)
fix y
assume in_vars: "y ∈ aexp_vars e"
have "type_max (to_total Γ y) mem⇩1 = Low"
proof -
from t_Low in_vars assign⇩2(2) show ?thesis
apply -
apply(erule type_aexpr.cases)
using Sec.exhaust by(auto simp: type_max_def split: if_splits)
qed
thus "mem⇩1 y = mem⇩2 y"
using assign⇩2 unfolding tyenv_eq_def by blast
qed
qed
qed
from upd have ty: " ⊢ ?Γ',𝒮,P' {c⇩1'} ?Γ',𝒮,P'"
by (metis stop_type)
have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
proof
assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
hence wf: "types_wellformed Γ"
unfolding tyenv_wellformed_def by blast
hence "type_wellformed t"
using assign⇩2(2) type_aexpr_type_wellformed
by blast
with wf have wf': "types_wellformed ?Γ'"
using types_wellformed_update by metis
from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
using types_stable_update
assign⇩2(3)
unfolding tyenv_wellformed_def by blast
have m: "mds_consistent mds Γ 𝒮 P"
using tyenv_wf unfolding tyenv_wellformed_def by blast
from assign⇩2(4) assign⇩2(1)
have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
apply(rule mds_consistent_preds_tyenv_update)
using upd m by simp
from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
unfolding tyenv_wellformed_def by blast
qed
have p: "pred P mem⇩1 ⟶ pred P' mem⇩1'"
using pred_preds_update assign⇩2 upd by metis
have p⇩2: "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
using pred_preds_update assign⇩2 upd by metis
have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem⇩1 ⟹ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' ?Γ' mem⇩1'"
proof(clarify)
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem⇩1"
assume sec: "tyenv_sec mds Γ mem⇩1"
from pred p have pred': "pred P' mem⇩1'" by blast
fix v t'
assume Γv: "(Γ(x ↦ t)) v = Some t'"
assume "v ∉ mds' AsmNoReadOrWrite"
show "type_max (the ((Γ(x ↦ t)) v)) mem⇩1' ≤ dma mem⇩1' v"
proof(cases "v = x")
assume [simp]: "v = x"
hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
using Γv by auto
from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
with pred' show ?thesis
using type_max_dma_type subtype_correct
by fastforce
next
assume neq: "v ≠ x"
hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
by simp
with Γv have Γv: "Γ v = Some t'" by simp
with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem⇩1 ≤ dma mem⇩1 v"
by auto
have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
hence dma_eq: "dma mem⇩1 = dma mem⇩1'"
by(rule dma_𝒞)
have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
apply(rule 𝒞_eq_type_max_eq)
using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
by(rule 𝒞_eq)
from neq Γv f_leq dma_eq f_eq show ?thesis
by simp
qed
qed
have "⟨Stop, mds, mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧1⇘?Γ',𝒮,P'⇙ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
apply(rule ℛ⇩1.intro)
apply blast
using wf assign⇩2 apply fastforce
apply(rule tyenv_eq')
using p assign⇩2 apply fastforce
using p⇩2 assign⇩2 apply fastforce
using sec assign⇩2
using upd(2) upd(3) by blast
ultimately have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
"⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ(x ↦ t),𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
using ℛ.intro⇩1
by auto
thus ?case
using ‹mds' = mds› ‹c⇩1' = Stop› ‹mem⇩1' = mem⇩1(x := ev⇩A mem⇩1 e)›
by blast
next
case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''')
let ?P = "if (ev⇩B mem⇩1 e) then P +⇩𝒮 e else P +⇩𝒮 (bexp_neg e)"
from ‹⟨Stmt.If e th el, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› have ty: "⊢ Γ,𝒮,?P {c⇩1'} Γ''',𝒮',P'''"
proof (rule if_elim)
assume "c⇩1' = th" "mem⇩1' = mem⇩1" "mds' = mds" "ev⇩B mem⇩1 e"
with if_type(3)
show ?thesis
apply simp
apply(erule sub)
using if_type apply simp+
done
next
assume "c⇩1' = el" "mem⇩1' = mem⇩1" "mds' = mds" "¬ ev⇩B mem⇩1 e"
with if_type(5)
show ?thesis
apply simp
apply(erule sub)
using if_type apply simp+
done
qed
have ev⇩B_eq [simp]: "ev⇩B mem⇩1 e = ev⇩B mem⇩2 e"
apply(rule ev⇩B_eq')
apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)
apply(rule ‹pred P mem⇩1›)
apply(rule ‹Γ ⊢⇩b e ∈ t›)
by(rule ‹ P ⊢ t›)
have "(⟨c⇩1', mds, mem⇩1⟩, ⟨c⇩1', mds, mem⇩2⟩) ∈ ℛ Γ''' 𝒮' P'''"
apply (rule intro⇩1)
apply clarify
apply (rule ℛ⇩1.intro [where Γ = Γ and Γ' = Γ''' and 𝒮 = 𝒮 and P = ?P])
apply(rule ty)
using ‹tyenv_wellformed mds Γ 𝒮 P›
apply(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)[1]
apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)
using ‹pred P mem⇩1› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
using ‹pred P mem⇩2› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
by(rule ‹tyenv_sec mds Γ mem⇩1›)
show ?case
proof -
from ev⇩B_eq if_type(13) have "(⟨If e th el, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩)"
apply (cases "ev⇩B mem⇩1 e")
apply (subgoal_tac "c⇩1' = th")
apply clarify
apply (metis cxt_to_stmt.simps(1) eval⇩w_simplep.if_true eval⇩wp.unannotated eval⇩wp_eval⇩w_eq if_type(8))
using if_type.prems(6) apply blast
apply (subgoal_tac "c⇩1' = el")
apply (metis (opaque_lifting, mono_tags) cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.if_false if_type(8))
using if_type.prems(6) by blast
with ‹⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ''',𝒮',P'''⇙ ⟨c⇩1', mds, mem⇩2⟩› show ?thesis
by (metis if_elim if_type.prems(6))
qed
next
case (while_type Γ e t P 𝒮 c)
hence [simp]: "c⇩1' = (If e (c ;; While e c) Stop)" and
[simp]: "mds' = mds" and
[simp]: "mem⇩1' = mem⇩1"
by (auto simp: while_elim)
with while_type have "⟨While e c, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩"
by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.while eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
moreover have ty: " ⊢ Γ,𝒮,P {c⇩1'} Γ,𝒮,P"
apply simp
apply(rule if_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule seq_type)
apply(rule while_type(3))
apply(rule has_type.while_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule while_type(3))
apply(rule stop_type)
apply simp+
apply(rule add_pred_entailment)
apply simp
apply(blast intro!: add_pred_subset tyenv_wellformed_subset)
done
moreover
have "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
apply (rule ℛ⇩1.intro [where Γ = Γ])
apply(rule ty)
using while_type apply simp+
done
hence "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
using ℛ.intro⇩1 by auto
ultimately show ?case
by fastforce
next
case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' mds c⇩1')
have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem⇩1 ∧ pred P⇩2 mem⇩2 ∧ tyenv_sec mds Γ⇩2 mem⇩1 ⟹
tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem⇩1 ∧ pred P⇩1 mem⇩2 ∧ tyenv_sec mds Γ⇩1 mem⇩1"
apply(rule conjI)
using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
apply blast
apply(rule conjI)
using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
apply(rule conjI)
using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast
have tyenv_eq: "mem⇩1 =⇘Γ⇩1⇙ mem⇩2"
using context_equiv_tyenv_eq sub by blast
from imp tyenv_eq obtain c⇩2' mem⇩2' where c⇩2'_props: "⟨c, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩"
"⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ⇩1',𝒮',P⇩1'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
using sub by blast
with R_equiv_entailment ‹P⇩1' ⊢ P⇩2'› show ?case
using sub.hyps(6) sub.hyps(5) by blast
next case (await_type Γ e t P 𝒮 c Γ' 𝒮' P' Γ'' P'')
from this show ?case using no_await_no_await by blast
qed
lemma is_final_ℛ⇩u_is_final:
"⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ is_final c⇩1 ⟹ is_final c⇩2"
by (fastforce dest: bisim_simple_ℛ⇩u)
lemma pred_plus_impl:
"pred P mem ⟹ ev⇩B mem e ⟹ pred P +⇩S e mem"
unfolding add_pred_def pred_def by simp
lemma my_ℛ⇩3_aux_induct [consumes 1, case_names intro⇩1 intro⇩3]:
"⟦⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩;
⋀c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P'.
⟦⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩;
⊢ Γ,𝒮,P {c} Γ',𝒮',P'⟧ ⟹
Q (c⇩1 ;; c) mds mem⇩1 Γ' 𝒮' P' (c⇩2 ;; c) mds mem⇩2;
⋀c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P'.
⟦⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩;
Q c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mds mem⇩2;
⊢ Γ,𝒮,P {c} Γ',𝒮',P'⟧ ⟹
Q (c⇩1 ;; c) mds mem⇩1 Γ' 𝒮' P' (c⇩2 ;; c) mds mem⇩2⟧ ⟹
Q c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mds mem⇩2"
using ℛ⇩3_aux.induct[where
?x1.0 = "⟨c⇩1, mds, mem⇩1⟩" and
?x2.0 = Γ and
?x3.0 = 𝒮 and
?x4.0 = P and
?x5.0 = "⟨c⇩2, mds, mem⇩2⟩" and
?P = "λctx⇩1 Γ 𝒮 P ctx⇩2. Q (fst (fst ctx⇩1)) (snd (fst ctx⇩1)) (snd ctx⇩1) Γ 𝒮 P (fst (fst ctx⇩2)) (snd (fst ctx⇩2)) (snd ctx⇩2)"]
by force
lemma ℛ_typed_step_plus:
"⟦⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1', mds', mem⇩1'⟩;
⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P';
no_await c⇩1;
tyenv_wellformed mds Γ 𝒮 P;
mem⇩1 =⇘Γ⇙ mem⇩2;
pred P mem⇩1;
pred P mem⇩2;
tyenv_sec mds Γ mem⇩1 ⟧ ⟹
(∃ c⇩2' mem⇩2'. ⟨c⇩1, mds, mem⇩2⟩ ↝⇧+ ⟨c⇩2', mds', mem⇩2'⟩ ∧
⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
proof (induct arbitrary: Γ 𝒮 P mem⇩2 rule: my_trancl_big_step_induct3)
case (base c⇩1 mds mem⇩1 c⇩1' mds' mem⇩1')
from this show ?case using ℛ_typed_step_no_await bisim_simple_ℛ⇩u by fast
next
case (step c⇩1 mds mem⇩1 c⇩1' mds' mem⇩1' c⇩1'' mds'' mem⇩1'')
from this obtain mem⇩2' where step⇩2': "⟨c⇩1, mds, mem⇩2⟩ ↝⇧+ ⟨c⇩1', mds', mem⇩2'⟩" and
rel⇩2': "⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩1', mds', mem⇩2'⟩"
using bisim_simple_ℛ⇩u by (metis fst_conv)
from rel⇩2' show ?case
proof(cases rule: ℛ.cases)
case (intro⇩1)
from this obtain Γ'' 𝒮'' P'' where
"⊢ Γ'',𝒮'',P'' {c⇩1'} Γ',𝒮',P'"
"tyenv_wellformed mds' Γ'' 𝒮'' P''"
"mem⇩1' =⇘Γ''⇙ mem⇩2'"
"pred P'' mem⇩1'"
"pred P'' mem⇩2'"
"∀x∈dom Γ''. x ∉ mds' AsmNoReadOrWrite ⟶ type_max (the (Γ'' x)) mem⇩1' ≤ dma mem⇩1' x"
using ℛ⇩1.cases by auto
from step⇩2' ‹no_await c⇩1› step.hyps(1) step.hyps(4) this obtain mem⇩2'' where
step⇩2'': "⟨c⇩1', mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩" and
rel⇩2'': "⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
using no_await_trancl bisim_simple_ℛ⇩u by (metis fst_conv)
from this step⇩2' show ?thesis using trancl_trans by fast
next
case (intro⇩3)
from intro⇩3 step.prems step.hyps(1) step.hyps(3) step.hyps(4) obtain mem⇩2'' where
step'': "⟨c⇩1', mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩" and
rel'': "⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
proof (induct arbitrary: rule: my_ℛ⇩3_aux_induct)
case (intro⇩1 c⇩1'1' mds' mem⇩1' Γ''' 𝒮''' P''' c⇩1'1 mem⇩2' c⇩1'2 Γ'' 𝒮'' P'')
from intro⇩1(1) obtain Γv 𝒮v Pv where pre_props:
"⊢ Γv,𝒮v,Pv {c⇩1'1} Γ''',𝒮''',P'''"
"tyenv_wellformed mds' Γv 𝒮v Pv"
"mem⇩1' =⇘Γv⇙ mem⇩2'"
"pred Pv mem⇩1'"
"pred Pv mem⇩2'"
"c⇩1'1 = c⇩1'1'"
"∀x∈dom Γv. x ∉ mds' AsmNoReadOrWrite ⟶ type_max (the (Γv x)) mem⇩1' ≤ dma mem⇩1' x"
using ℛ⇩1.cases by blast
from this intro⇩1 have typed: "⊢ Γv,𝒮v,Pv {c⇩1'1 ;; c⇩1'2} Γ'',𝒮'',P''"
using has_type.seq_type by blast
from this pre_props ‹no_await c⇩1› ‹⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩1'⟩› intro⇩1(13)
obtain mem⇩2'' where
step: "⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩ ∧
⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
using no_await_trancl bisim_simple_ℛ⇩u by (metis fst_conv)
from this intro⇩1(3) show ?case using no_await_trancl bisim_simple_ℛ⇩u by blast
next
case (intro⇩3 c⇩1'1' mds' mem⇩1' Γ''' 𝒮''' P''' c⇩1'1 mem⇩2' c⇩1'2 Γ'' 𝒮'' P'')
from intro⇩3(1) obtain Γv 𝒮v Pv where pre_props:
"⊢ Γv,𝒮v,Pv {c⇩1'1} Γ''',𝒮''',P'''"
"tyenv_wellformed mds' Γv 𝒮v Pv"
"mem⇩1' =⇘Γv⇙ mem⇩2'"
"pred Pv mem⇩1'"
"pred Pv mem⇩2'"
"c⇩1'1 = c⇩1'1'"
"∀x∈dom Γv. x ∉ mds' AsmNoReadOrWrite ⟶ type_max (the (Γv x)) mem⇩1' ≤ dma mem⇩1' x"
by (induct arbitrary: rule: my_ℛ⇩3_aux_induct)
(blast elim: ℛ⇩1.cases, blast)
from this intro⇩1 have typed: "⊢ Γv,𝒮v,Pv {c⇩1'1 ;; c⇩1'2} Γ'',𝒮'',P''"
using has_type.seq_type intro⇩3.hyps(3) by blast
from this pre_props ‹no_await c⇩1› ‹⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩1'⟩› intro⇩3
obtain mem⇩2'' where
step: "⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩ ∧
⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
proof -
assume a1: "⋀mem⇩2''. ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩ ∧
⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩1'', mds'', mem⇩2''⟩ ⟹ thesis"
thus ?thesis using intro⇩3.prems(11)
using a1 by (metis (no_types) pre_props(2-)
‹⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩1'⟩› ‹no_await c⇩1›
bisim_simple_ℛ⇩u fst_conv no_await_trancl typed)
qed
from this intro⇩3 show ?case using no_await_trancl bisim_simple_ℛ⇩u by blast
qed
thus ?thesis
by (meson step⇩2' trancl_trans)
qed
qed
lemma ℛ_typed_step:
"⟦ ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P' ;
tyenv_wellformed mds Γ 𝒮 P; mem⇩1 =⇘Γ⇙ mem⇩2; pred P mem⇩1;
pred P mem⇩2; tyenv_sec mds Γ mem⇩1;
⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩ ⟧ ⟹
(∃ c⇩2' mem⇩2'. ⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
proof (induct arbitrary: mds c⇩1' rule: has_type.induct)
case (seq_type Γ 𝒮 P c⇩1 Γ'' 𝒮'' P'' c⇩2 Γ' 𝒮' P' mds)
show ?case
proof (cases "c⇩1 = Stop")
assume "c⇩1 = Stop"
hence [simp]: "c⇩1' = c⇩2" "mds' = mds" "mem⇩1' = mem⇩1"
using seq_type
by (auto simp: seq_stop_elim)
from seq_type ‹c⇩1 = Stop› have "context_equiv Γ P Γ''" and "𝒮 = 𝒮''" and "P ⊢ P''" and
"(∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ'' 𝒮 P'')"
by (metis stop_cxt)+
hence "⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'"
apply -
apply(rule sub)
using seq_type(3) apply simp
by auto
have "⟨c⇩2, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
apply (rule ℛ⇩1.intro [of Γ])
apply(rule ‹⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'›)
using seq_type by auto
thus ?case
using ℛ.intro⇩1
apply clarify
apply (rule_tac x = c⇩2 in exI)
apply (rule_tac x = mem⇩2 in exI)
by (auto simp: ‹c⇩1 = Stop› seq_stop_eval⇩w ℛ.intro⇩1)
next
assume "c⇩1 ≠ Stop"
with ‹⟨c⇩1 ;; c⇩2, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› obtain c⇩1'' where c⇩1''_props:
"⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = c⇩1'' ;; c⇩2"
by (metis seq_elim)
with seq_type(2) obtain c⇩2'' mem⇩2' where c⇩2''_props:
"⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩ ∧ ⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
using seq_type.prems(1) seq_type.prems(2) seq_type.prems(3) seq_type.prems(4) seq_type.prems(5) by presburger
hence "⟨c⇩1'' ;; c⇩2, mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
apply (rule conjE)
apply (erule ℛ_elim, auto)
apply (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩1 seq_type(3))
by (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩3 seq_type(3))
moreover
from c⇩2''_props have "⟨c⇩1 ;; c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
by (metis eval⇩w.seq)
ultimately show ?case
by (metis c⇩1''_props)
qed
next
case (anno_type Γ' Γ 𝒮 upd 𝒮' P' P c Γ'' 𝒮'' P'' mds)
have "mem⇩1 =⇘Γ'⇙ mem⇩2"
proof(clarsimp simp: tyenv_eq_def)
fix x
assume a: "type_max (to_total Γ' x) mem⇩1 = Low"
hence "type_max (to_total Γ x) mem⇩1 = Low"
proof -
from ‹pred P mem⇩1› have "pred P' mem⇩1"
using anno_type.hyps(3)
by(auto simp: restrict_preds_to_vars_def pred_def)
with subtype_sound[OF anno_type.hyps(7)] a
show ?thesis
using less_eq_Sec_def by metis
qed
thus " mem⇩1 x = mem⇩2 x"
using anno_type.prems(2)
unfolding tyenv_eq_def by blast
qed
have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ' 𝒮' P'"
using anno_type
apply auto
by (metis tyenv_wellformed_mode_update)
moreover
have pred: "pred P mem⇩1 ⟶ pred P' mem⇩1"
using anno_type
by (auto simp: pred_def restrict_preds_to_vars_def)
moreover
have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟶
tyenv_sec (update_modes upd mds) Γ' mem⇩1"
apply(rule impI)
apply(rule tyenv_sec_mode_update)
using anno_type apply fastforce
using anno_type pred apply fastforce
using anno_type apply fastforce
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply fastforce
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
by simp
ultimately obtain c⇩2' mem⇩2' where "(⟨c, update_modes upd mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
using anno_type
apply auto
using ‹mem⇩1 =⇘Γ'⇙ mem⇩2› local.pred_def restrict_preds_to_vars_def upd_elim by fastforce
thus ?case
apply (rule_tac x = c⇩2' in exI)
apply (rule_tac x = mem⇩2' in exI)
apply auto
by (metis cxt_to_stmt.simps(1) eval⇩w.decl)
next
case stop_type
with stop_no_eval show ?case by auto
next
case (skip_type Γ 𝒮 P mds)
moreover
with skip_type have [simp]: "mds' = mds" "c⇩1' = Stop" "mem⇩1' = mem⇩1"
using skip_elim
by (metis, metis, metis)
with skip_type have "⟨Stop, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨Stop, mds, mem⇩2⟩"
by auto
thus ?case
using ℛ.intro⇩1 and unannotated [where c = Skip and E = "[]"]
apply auto
by (metis (mono_tags, lifting) ℛ.intro⇩1 old.prod.case skip_eval⇩w)
next
case (assign⇩1 x Γ e t P P' 𝒮 mds)
hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
using assign_elim
by (auto, metis)
from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
by auto
have dma_eq [simp]: "dma mem⇩1 = dma mem⇩1'"
using dma_𝒞 assign⇩1(2) by simp
have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
unfolding tyenv_eq_def
proof(clarify)
fix v
assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
proof(cases "v ∈ dom Γ")
assume [simp]: "v ∈ dom Γ"
then obtain t' where [simp]: "Γ v = Some t'" by force
hence [simp]: "(to_total Γ v) = t'"
unfolding to_total_def by (auto split: if_splits)
have "type_max t' mem⇩1 = type_max t' mem⇩1'"
apply(rule 𝒞_eq_type_max_eq)
using ‹Γ v = Some t'› assign⇩1(6)
unfolding tyenv_wellformed_def types_wellformed_def
apply (metis ‹v ∈ dom Γ› option.sel)
using assign⇩1(2) apply simp
done
with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
by simp
from assign⇩1(1) ‹v ∈ dom Γ› have "x ≠ v" by auto
thus ?thesis
apply simp
using is_Low assign⇩1(7) unfolding tyenv_eq_def by auto
next
assume "v ∉ dom Γ"
hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
unfolding to_total_def by simp
with is_Low' have "dma mem⇩1' v = Low" by simp
with dma_eq have dma_v_Low: "dma mem⇩1 v = Low" by simp
hence is_Low: "type_max (to_total Γ v) mem⇩1 = Low" by simp
show ?thesis
proof(cases "x = v")
assume "x ≠ v"
thus ?thesis
apply simp
using is_Low assign⇩1(7) unfolding tyenv_eq_def by blast
next
assume "x = v"
thus ?thesis
apply simp
apply(rule ev⇩A_eq)
apply(rule assign⇩1(7))
apply(rule assign⇩1(8))
apply(rule assign⇩1(3))
apply(rule assign⇩1(4))
using dma_v_Low by simp
qed
qed
qed
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩1 by metis
moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
using pred_preds_update assign⇩1 upd by metis
moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
using pred_preds_update assign⇩1 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ tyenv_sec mds Γ mem⇩1 ⟶ tyenv_sec mds Γ mem⇩1'"
using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
unfolding tyenv_wellformed_def by blast
ultimately have ℛ':
"⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
apply -
apply (rule ℛ.intro⇩1, auto simp: assign⇩1 simp del: dma_eq)
done
have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)
from ℛ' a show ?case
using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
by blast
next
case (assign⇩𝒞 x Γ e t P P' 𝒮 mds)
hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
using assign_elim
by (auto, metis)
have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
unfolding tyenv_eq_def
proof(clarify)
fix v
assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
proof(cases "v ∈ dom Γ")
assume in_dom [simp]: "v ∈ dom Γ"
then obtain t' where Γv [simp]: "Γ v = Some t'" by force
hence [simp]: "(to_total Γ v) = t'"
unfolding to_total_def by (auto split: if_splits)
from assign⇩𝒞(4) have x_nin_C: "x ∉ vars_of_type t'"
using in_dom Γv
by (metis option.sel snd_conv)
have Γv_wf: "type_wellformed t'"
using in_dom Γv assign⇩𝒞(7) unfolding tyenv_wellformed_def types_wellformed_def
by (metis option.sel)
with x_nin_C have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
using vars_of_type_eq_type_max_eq by simp
with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
by simp
from assign⇩𝒞(1) ‹v ∈ dom Γ› assign⇩𝒞(7) have "x ≠ v"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
thus ?thesis
apply simp
using is_Low assign⇩𝒞(8) unfolding tyenv_eq_def by auto
next
assume nin_dom: "v ∉ dom Γ"
hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
unfolding to_total_def by simp
with is_Low' have "dma mem⇩1' v = Low" by simp
show ?thesis
proof(cases "x = v")
assume "x = v"
thus ?thesis
apply simp
apply(rule ev⇩A_eq')
apply(rule assign⇩𝒞(8))
apply(rule assign⇩𝒞(9))
apply(rule assign⇩𝒞(2))
by(rule assign⇩𝒞(3))
next
assume [simp]: "x ≠ v"
show ?thesis
proof(cases "x ∈ 𝒞_vars v")
assume in_𝒞_vars: "x ∈ 𝒞_vars v"
hence "v ∉ 𝒞"
using 𝒞_vars_𝒞 by auto
with nin_dom have "v ∉ snd 𝒮"
using assign⇩𝒞(7)
by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def)
with in_𝒞_vars have "P ⊢ (to_total Γ v)"
using assign⇩𝒞(6) by blast
with assign⇩𝒞(9) have "type_max (to_total Γ v) mem⇩1 = Low"
by(auto simp: type_max_def pred_def pred_entailment_def)
thus ?thesis
using not_sym[OF ‹x ≠ v›]
apply simp
using assign⇩𝒞(8)
unfolding tyenv_eq_def by auto
next
assume "x ∉ 𝒞_vars v"
with is_Low' have "dma mem⇩1 v = Low"
using dma_𝒞_vars ‹⋀mem. type_max (to_total Γ v) mem = dma mem v›
by (metis fun_upd_other)
thus ?thesis
using not_sym[OF ‹x ≠ v›]
apply simp
using assign⇩𝒞(8)
unfolding tyenv_eq_def by auto
qed
qed
qed
qed
moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
using pred_preds_update assign⇩𝒞 upd by metis
moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
using pred_preds_update assign⇩𝒞 upd by metis
moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' Γ mem⇩1'"
proof(clarify)
fix v t'
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem⇩1"
hence pred': "pred P' mem⇩1'" using ‹pred P mem⇩1 ⟶ pred P' mem⇩1'› by blast
assume sec: "tyenv_sec mds Γ mem⇩1"
assume Γv: "Γ v = Some t'"
assume readable': "v ∉ mds' AsmNoReadOrWrite"
with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
show "type_max (the (Γ v)) mem⇩1' ≤ dma mem⇩1' v"
proof(cases "x ∈ 𝒞_vars v")
assume "x ∈ 𝒞_vars v"
with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
from pred' Γv subtype_sound[OF this] show ?thesis
using type_max_dma_type by(auto simp: to_total_def split: if_splits)
next
assume "x ∉ 𝒞_vars v"
hence "∀v'∈𝒞_vars v. mem⇩1 v' = mem⇩1' v'"
using upd by auto
hence dma_eq: "dma mem⇩1 v = dma mem⇩1' v"
by(rule dma_𝒞_vars)
from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
have "type_wellformed t'"
using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
using vars_of_type_eq_type_max_eq by fastforce
from sec Γv readable have "type_max t' mem⇩1 ≤ dma mem⇩1 v"
by auto
with f_eq dma_eq Γv show ?thesis
by simp
qed
qed
ultimately have ℛ':
"⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
apply -
apply (rule ℛ.intro⇩1, auto simp: assign⇩𝒞)
done
have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)
from ℛ' a show ?case
using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
by blast
next
case (assign⇩2 x Γ e t 𝒮 P' P mds)
have upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
using assign_elim[OF assign⇩2(11)]
by auto
from ‹x ∈ dom Γ› ‹tyenv_wellformed mds Γ 𝒮 P›
have x_nin_𝒞: "x ∉ 𝒞"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
hence dma_eq [simp]: "dma mem⇩1' = dma mem⇩1"
using dma_𝒞 assign⇩2
by auto
let ?Γ' = "Γ (x ↦ t)"
have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
using assign⇩2
by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.assign eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
moreover
have tyenv_eq': "mem⇩1(x := ev⇩A mem⇩1 e) =⇘Γ(x ↦ t)⇙ mem⇩2(x := ev⇩A mem⇩2 e)"
unfolding tyenv_eq_def
proof(clarify)
fix v
assume is_Low': "type_max (to_total (Γ(x ↦ t)) v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
proof(cases "v = x")
assume neq: "v ≠ x"
hence "type_max (to_total Γ v) mem⇩1 = Low"
proof(cases "v ∈ dom Γ")
assume "v ∈ dom Γ"
then obtain t' where [simp]: "Γ v = Some t'" by force
hence [simp]: "(to_total Γ v) = t'"
unfolding to_total_def by (auto split: if_splits)
hence [simp]: "(to_total ?Γ' v) = t'"
using neq by(auto simp: to_total_def)
have "type_max t' mem⇩1 = type_max t' mem⇩1'"
apply(rule 𝒞_eq_type_max_eq)
using assign⇩2(6)
apply(clarsimp simp: tyenv_wellformed_def types_wellformed_def)
using ‹v ∈ dom Γ› ‹Γ v = Some t'› apply(metis option.sel)
using x_nin_𝒞 by simp
from this is_Low' neq neq[THEN not_sym] show "type_max (to_total Γ v) mem⇩1 = Low"
by auto
next
assume "v ∉ dom Γ"
with is_Low' neq
have "dma mem⇩1' v = Low"
by(auto simp: to_total_def split: if_splits)
with dma_eq ‹v ∉ dom Γ› show ?thesis
by(auto simp: to_total_def split: if_splits)
qed
with neq assign⇩2(7) show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
by(auto simp: tyenv_eq_def)
next
assume eq[simp]: "v = x"
with is_Low' ‹x ∈ dom Γ› have t_Low': "type_max t mem⇩1' = Low"
by(auto simp: to_total_def split: if_splits)
have wf_t: "type_wellformed t"
using type_aexpr_type_wellformed assign⇩2(2) assign⇩2(6)
by(fastforce simp: tyenv_wellformed_def)
with t_Low' ‹x ∉ 𝒞› have t_Low: "type_max t mem⇩1 = Low"
using 𝒞_eq_type_max_eq
by (metis (no_types, lifting) fun_upd_other upd(3))
show ?thesis
proof(simp, rule eval_vars_det⇩A, clarify)
fix y
assume in_vars: "y ∈ aexp_vars e"
have "type_max (to_total Γ y) mem⇩1 = Low"
proof -
from t_Low in_vars assign⇩2(2) show ?thesis
apply -
apply(erule type_aexpr.cases)
using Sec.exhaust by(auto simp: type_max_def split: if_splits)
qed
thus "mem⇩1 y = mem⇩2 y"
using assign⇩2 unfolding tyenv_eq_def by blast
qed
qed
qed
from upd have ty: " ⊢ ?Γ',𝒮,P' {c⇩1'} ?Γ',𝒮,P'"
by (metis stop_type)
have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
proof
assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
hence wf: "types_wellformed Γ"
unfolding tyenv_wellformed_def by blast
hence "type_wellformed t"
using assign⇩2(2) type_aexpr_type_wellformed
by blast
with wf have wf': "types_wellformed ?Γ'"
using types_wellformed_update by metis
from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
using types_stable_update
assign⇩2(3)
unfolding tyenv_wellformed_def by blast
have m: "mds_consistent mds Γ 𝒮 P"
using tyenv_wf unfolding tyenv_wellformed_def by blast
from assign⇩2(4) assign⇩2(1)
have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
apply(rule mds_consistent_preds_tyenv_update)
using upd m by simp
from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
unfolding tyenv_wellformed_def by blast
qed
have p: "pred P mem⇩1 ⟶ pred P' mem⇩1'"
using pred_preds_update assign⇩2 upd by metis
have p⇩2: "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
using pred_preds_update assign⇩2 upd by metis
have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem⇩1 ⟹ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' ?Γ' mem⇩1'"
proof(clarify)
assume wf: "tyenv_wellformed mds Γ 𝒮 P"
assume pred: "pred P mem⇩1"
assume sec: "tyenv_sec mds Γ mem⇩1"
from pred p have pred': "pred P' mem⇩1'" by blast
fix v t'
assume Γv: "(Γ(x ↦ t)) v = Some t'"
assume "v ∉ mds' AsmNoReadOrWrite"
show "type_max (the ((Γ(x ↦ t)) v)) mem⇩1' ≤ dma mem⇩1' v"
proof(cases "v = x")
assume [simp]: "v = x"
hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
using Γv by auto
from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
by(auto simp: tyenv_wellformed_def mds_consistent_def)
with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
with pred' show ?thesis
using type_max_dma_type subtype_sound
by fastforce
next
assume neq: "v ≠ x"
hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
by simp
with Γv have Γv: "Γ v = Some t'" by simp
with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem⇩1 ≤ dma mem⇩1 v"
by auto
have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
hence dma_eq: "dma mem⇩1 = dma mem⇩1'"
by(rule dma_𝒞)
have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
apply(rule 𝒞_eq_type_max_eq)
using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
by(rule 𝒞_eq)
from neq Γv f_leq dma_eq f_eq show ?thesis
by simp
qed
qed
have "⟨Stop, mds, mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧1⇘?Γ',𝒮,P'⇙ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
apply(rule ℛ⇩1.intro)
apply blast
using wf assign⇩2 apply fastforce
apply(rule tyenv_eq')
using p assign⇩2 apply fastforce
using p⇩2 assign⇩2 apply fastforce
using sec assign⇩2
using upd(2) upd(3) by blast
ultimately have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
"⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ(x ↦ t),𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
using ℛ.intro⇩1
by auto
thus ?case
using ‹mds' = mds› ‹c⇩1' = Stop› ‹mem⇩1' = mem⇩1(x := ev⇩A mem⇩1 e)›
by blast
next
case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''')
let ?P = "if (ev⇩B mem⇩1 e) then P +⇩𝒮 e else P +⇩𝒮 (bexp_neg e)"
from ‹⟨Stmt.If e th el, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› have ty: "⊢ Γ,𝒮,?P {c⇩1'} Γ''',𝒮',P'''"
proof (rule if_elim)
assume "c⇩1' = th" "mem⇩1' = mem⇩1" "mds' = mds" "ev⇩B mem⇩1 e"
with if_type(3)
show ?thesis
apply simp
apply(erule sub)
using if_type apply simp+
done
next
assume "c⇩1' = el" "mem⇩1' = mem⇩1" "mds' = mds" "¬ ev⇩B mem⇩1 e"
with if_type(5)
show ?thesis
apply simp
apply(erule sub)
using if_type apply simp+
done
qed
have ev⇩B_eq [simp]: "ev⇩B mem⇩1 e = ev⇩B mem⇩2 e"
apply(rule ev⇩B_eq')
apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)
apply(rule ‹pred P mem⇩1›)
apply(rule ‹Γ ⊢⇩b e ∈ t›)
by(rule ‹ P ⊢ t›)
have "(⟨c⇩1', mds, mem⇩1⟩, ⟨c⇩1', mds, mem⇩2⟩) ∈ ℛ Γ''' 𝒮' P'''"
apply (rule intro⇩1)
apply clarify
apply (rule ℛ⇩1.intro [where Γ = Γ and Γ' = Γ''' and 𝒮 = 𝒮 and P = ?P])
apply(rule ty)
using ‹tyenv_wellformed mds Γ 𝒮 P›
apply(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)[1]
apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)
using ‹pred P mem⇩1› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
using ‹pred P mem⇩2› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
by(rule ‹tyenv_sec mds Γ mem⇩1›)
show ?case
proof -
from ev⇩B_eq if_type(13) have "(⟨If e th el, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩)"
apply (cases "ev⇩B mem⇩1 e")
apply (subgoal_tac "c⇩1' = th")
apply clarify
apply (metis cxt_to_stmt.simps(1) eval⇩w_simplep.if_true eval⇩wp.unannotated eval⇩wp_eval⇩w_eq if_type(8))
using if_type.prems(6) apply blast
apply (subgoal_tac "c⇩1' = el")
apply (metis (opaque_lifting, mono_tags) cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.if_false if_type(8))
using if_type.prems(6) by blast
with ‹⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ''',𝒮',P'''⇙ ⟨c⇩1', mds, mem⇩2⟩› show ?thesis
by (metis if_elim if_type.prems(6))
qed
next
case (while_type Γ e t P 𝒮 c)
hence [simp]: "c⇩1' = (If e (c ;; While e c) Stop)" and
[simp]: "mds' = mds" and
[simp]: "mem⇩1' = mem⇩1"
by (auto simp: while_elim)
with while_type have "⟨While e c, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩"
by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.while eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
moreover have ty: " ⊢ Γ,𝒮,P {c⇩1'} Γ,𝒮,P"
apply simp
apply(rule if_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule seq_type)
apply(rule while_type(3))
apply(rule has_type.while_type)
apply(rule while_type(1))
apply(rule while_type(2))
apply(rule while_type(3))
apply(rule stop_type)
apply simp+
apply(rule add_pred_entailment)
apply simp
apply(blast intro!: add_pred_subset tyenv_wellformed_subset)
done
moreover
have "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
apply (rule ℛ⇩1.intro [where Γ = Γ])
apply(rule ty)
using while_type apply simp+
done
hence "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
using ℛ.intro⇩1 by auto
ultimately show ?case
by fastforce
next
case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' mds c⇩1')
have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem⇩1 ∧ pred P⇩2 mem⇩2 ∧ tyenv_sec mds Γ⇩2 mem⇩1 ⟹
tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem⇩1 ∧ pred P⇩1 mem⇩2 ∧ tyenv_sec mds Γ⇩1 mem⇩1"
apply(rule conjI)
using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
apply blast
apply(rule conjI)
using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
apply(rule conjI)
using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast
have tyenv_eq: "mem⇩1 =⇘Γ⇩1⇙ mem⇩2"
using context_equiv_tyenv_eq sub by blast
from imp tyenv_eq obtain c⇩2' mem⇩2' where c⇩2'_props: "⟨c, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩"
"⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ⇩1',𝒮',P⇩1'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
using sub by blast
with R_equiv_entailment ‹P⇩1' ⊢ P⇩2'› show ?case
using sub.hyps(6) sub.hyps(5) by blast
next case (await_type Γ e t P 𝒮 c Γ' 𝒮' P')
from await_type.prems have "ev⇩B mem⇩1 e" "no_await c" "is_final c⇩1'" and step: "⟨c, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1', mds', mem⇩1'⟩"
using await_elim by simp+
from await_type.prems ‹Γ ⊢⇩b e ∈ t› ‹P ⊢ t› have "pred P +⇩𝒮 e mem⇩1" "pred P +⇩𝒮 e mem⇩2" "ev⇩B mem⇩2 e"
using pred_plus_impl ‹ev⇩B mem⇩1 e› ‹pred P mem⇩1› ev⇩B_eq'
by blast+
from await_type.prems ‹Γ ⊢⇩b e ∈ t› ‹P ⊢ t› have wellformed: "tyenv_wellformed mds Γ 𝒮 P +⇩𝒮 e"
apply (unfold add_pred_def)[1]
apply (case_tac "pred_stable 𝒮 e", clarsimp)
apply (unfold tyenv_wellformed_def, clarsimp)[1]
apply (unfold mds_consistent_def, clarsimp)[1]
by clarsimp
from step ‹is_final c⇩1'› ‹no_await c› ‹tyenv_wellformed mds Γ 𝒮 P +⇩𝒮 e› await_type.prems ‹pred P +⇩𝒮 e mem⇩1› ‹pred P +⇩𝒮 e mem⇩2›
obtain c⇩2' mem⇩2' where step: "⟨c, mds, mem⇩2⟩ ↝⇧+ ⟨c⇩2', mds', mem⇩2'⟩" and
rel: "⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩" "is_final c⇩2'"
using ℛ_typed_step_plus await_type.hyps(3) is_final_ℛ⇩u_is_final by meson
from wellformed ‹is_final c⇩2'› ‹ev⇩B mem⇩2 e› ‹no_await c› ‹Γ ⊢⇩b e ∈ t› ‹P ⊢ t› ‹pred P +⇩𝒮 e mem⇩2› step rel show ?case
using eval⇩w.intros(4) by blast
qed
lemma ℛ⇩1_weak_bisim:
"weak_bisim (ℛ⇩1 Γ' 𝒮' P') (ℛ Γ' 𝒮' P')"
unfolding weak_bisim_def
apply clarsimp
apply(erule ℛ⇩1_elim)
apply(blast intro: ℛ_typed_step)
done
lemma ℛ_to_ℛ⇩3: "⟦ ⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩ ; ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ⟧ ⟹
⟨c⇩1 ;; c, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2 ;; c, mds, mem⇩2⟩"
apply (erule ℛ_elim)
by auto
lemma ℛ⇩3_weak_bisim:
"weak_bisim (ℛ⇩3 Γ' 𝒮' P') (ℛ Γ' 𝒮' P')"
proof -
{
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 c⇩1' mds' mem⇩1'
assume case3: "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ ℛ⇩3 Γ' 𝒮' P'"
assume eval: "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩"
have "∃ c⇩2' mem⇩2'. ⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧ ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
using case3 eval
apply simp
proof (induct arbitrary: c⇩1' rule: ℛ⇩3_aux.induct)
case (intro⇩1 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
hence [simp]: "c⇩2 = c⇩1"
by (metis (lifting) ℛ⇩1_elim)
thus ?case
proof (cases "c⇩1 = Stop")
assume [simp]: "c⇩1 = Stop"
from intro⇩1(1) show ?thesis
apply (rule ℛ⇩1_elim)
apply simp
apply (rule_tac x = c in exI)
apply (rule_tac x = mem⇩2 in exI)
apply (rule conjI)
apply (metis ‹c⇩1 = Stop› cxt_to_stmt.simps(1) eval⇩w_simplep.seq_stop eval⇩wp.unannotated eval⇩wp_eval⇩w_eq intro⇩1.prems seq_stop_elim)
apply (rule ℛ.intro⇩1, clarify)
apply (subgoal_tac "c⇩1' = c")
apply simp
apply (rule ℛ⇩1.intro)
apply(rule intro⇩1(2))
apply (metis (no_types, lifting) ‹c⇩1 = Stop› intro⇩1.prems seq_stop_elim stop_cxt tyenv_wellformed_sub)
using ‹c⇩1 = Stop› intro⇩1.prems seq_stop_elim stop_cxt context_equiv_tyenv_eq
apply metis
using ‹c⇩1 = Stop› intro⇩1.prems pred_entailment_def seq_stop_elim stop_cxt apply blast
using pred_entailment_def stop_cxt apply blast
apply (metis (no_types, lifting) ‹c⇩1 = Stop› context_equiv_def intro⇩1.prems less_eq_Sec_def seq_stop_elim stop_cxt subtype_sound type_equiv_def)
using intro⇩1.prems seq_stop_elim by auto
next
assume "c⇩1 ≠ Stop"
from intro⇩1
obtain c⇩1'' where "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = (c⇩1'' ;; c)"
by (metis ‹c⇩1 ≠ Stop› intro⇩1.prems seq_elim)
with intro⇩1
obtain c⇩2'' mem⇩2' where "⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩" "⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
using ℛ⇩1_weak_bisim and weak_bisim_def
by blast
thus ?thesis
using intro⇩1(2) ℛ_to_ℛ⇩3
apply (rule_tac x = "c⇩2'' ;; c" in exI)
apply (rule_tac x = mem⇩2' in exI)
apply (rule conjI)
apply (metis eval⇩w.seq)
apply auto
apply (rule ℛ.intro⇩3)
by (simp add: ℛ_to_ℛ⇩3 ‹⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = c⇩1'' ;; c›)
qed
next
case (intro⇩3 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
thus ?case
apply (cases "c⇩1 = Stop")
apply blast
proof -
assume "c⇩1 ≠ Stop"
then obtain c⇩1'' where "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩" "c⇩1' = (c⇩1'' ;; c)"
by (metis intro⇩3.prems seq_elim)
then obtain c⇩2'' mem⇩2' where "⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩" "⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
using intro⇩3(2) by metis
thus ?thesis
apply (rule_tac x = "c⇩2'' ;; c" in exI)
apply (rule_tac x = mem⇩2' in exI)
apply (rule conjI)
apply (metis eval⇩w.seq)
apply (erule ℛ_elim)
apply simp_all
apply (metis ℛ.intro⇩3 ℛ_to_ℛ⇩3 ‹⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩› ‹c⇩1' = c⇩1'' ;; c› intro⇩3(3))
apply (metis (lifting) ℛ.intro⇩3 ℛ_to_ℛ⇩3 ‹⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩› ‹c⇩1' = c⇩1'' ;; c› intro⇩3(3))
done
qed
qed
}
thus ?thesis
unfolding weak_bisim_def
by auto
qed
lemma ℛ_bisim: "strong_low_bisim_mm (ℛ Γ' 𝒮' P')"
unfolding strong_low_bisim_mm_def
proof (auto)
from ℛ_sym show "sym (ℛ Γ' 𝒮' P')" .
next
from ℛ_closed_glob_consistent show "closed_glob_consistent (ℛ Γ' 𝒮' P')" .
next
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2
assume "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
thus "mem⇩1 =⇘mds⇙⇧l mem⇩2"
apply (rule ℛ_elim)
by (auto simp: ℛ⇩1_mem_eq ℛ⇩3_mem_eq)
next
fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 c⇩1' mds' mem⇩1'
assume eval: "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩"
assume R: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
from R show "∃ c⇩2' mem⇩2'. ⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
apply (rule ℛ_elim)
apply (insert ℛ⇩1_weak_bisim ℛ⇩3_weak_bisim eval weak_bisim_def)
apply auto
done
qed
lemma Typed_in_ℛ:
assumes typeable: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
assumes wf: "tyenv_wellformed mds Γ 𝒮 P"
assumes mem_eq: "∀ x. type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x"
assumes pred⇩1: "pred P mem⇩1"
assumes pred⇩2: "pred P mem⇩2"
assumes tyenv_sec: "tyenv_sec mds Γ mem⇩1"
shows "⟨c, mds, mem⇩1⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c, mds, mem⇩2⟩"
apply (rule ℛ.intro⇩1 [of Γ'])
apply clarify
apply (rule ℛ⇩1.intro [of Γ])
apply(rule typeable)
apply(rule wf)
using mem_eq apply(fastforce simp: tyenv_eq_def)
using assms by simp+
theorem type_soundness:
assumes well_typed: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
assumes wf: "tyenv_wellformed mds Γ 𝒮 P"
assumes mem_eq: "∀ x. type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x"
assumes pred⇩1: "pred P mem⇩1"
assumes pred⇩2: "pred P mem⇩2"
assumes tyenv_sec: "tyenv_sec mds Γ mem⇩1"
shows "⟨c, mds, mem⇩1⟩ ≈ ⟨c, mds, mem⇩2⟩"
using ℛ_bisim Typed_in_ℛ
by (metis assms mem_eq mm_equiv.simps well_typed)
definition
Γ_of_mds :: "'Var Mds ⇒ ('Var,'BExp) TyEnv"
where
"Γ_of_mds mds ≡ (λx. if x ∉ 𝒞 ∧ x ∈ mds AsmNoWrite ∪ mds AsmNoReadOrWrite then
if x ∈ mds AsmNoReadOrWrite then
Some ({pred_False})
else
Some (dma_type x)
else None)"
definition
𝒮_of_mds :: "'Var Mds ⇒ 'Var Stable"
where
"𝒮_of_mds mds ≡ (mds AsmNoWrite, mds AsmNoReadOrWrite)"
definition
mds_yields_stable_types :: "'Var Mds ⇒ bool"
where
"mds_yields_stable_types mds ≡ ∀x. x ∈ mds AsmNoWrite ∪ mds AsmNoReadOrWrite ⟶
(∀v∈𝒞_vars x. v ∈ mds AsmNoWrite ∪ mds AsmNoReadOrWrite)"
inductive
type_global :: "(('Var, 'AExp, 'BExp) Stmt × 'Var Mds) list ⇒ bool"
("⊢ _" [120] 1000)
where
"⟦ list_all (λ (c,m). (∃ Γ' 𝒮' P'. ⊢ (Γ_of_mds m),(𝒮_of_mds m),{} { c } Γ',𝒮',P') ∧ mds_yields_stable_types m) cs ;
∀ mem. sound_mode_use (cs, mem)
⟧ ⟹
type_global cs"
inductive_cases type_global_elim: "⊢ cs"
lemma of_mds_tyenv_wellformed: "mds_yields_stable_types m ⟹ tyenv_wellformed m (Γ_of_mds m) (𝒮_of_mds m) {}"
apply(auto simp: tyenv_wellformed_def Γ_of_mds_def 𝒮_of_mds_def mds_consistent_def stable_def
types_wellformed_def types_stable_def mds_yields_stable_types_def
type_wellformed_def dma_𝒞_vars 𝒞_def bexp_vars_pred_False 𝒞_vars_correct
split: if_splits)
done
lemma Γ_of_mds_tyenv_sec:
"tyenv_sec m (Γ_of_mds m) mem⇩1"
apply(auto simp: Γ_of_mds_def)
done
lemma type_max_pred_False [simp]:
"type_max {pred_False} mem = High"
apply(simp add: type_max_def pred_False_is_False)
done
lemma typed_secure:
"⟦ ⊢ (Γ_of_mds m),(𝒮_of_mds m),{} { c } Γ',𝒮',P'; mds_yields_stable_types m ⟧ ⟹ com_sifum_secure (c,m)"
apply (clarsimp simp: com_sifum_secure_def low_indistinguishable_def)
apply (erule type_soundness)
apply(erule of_mds_tyenv_wellformed)
apply(auto simp: to_total_def split: if_split simp: Γ_of_mds_def low_mds_eq_def)[1]
apply(fastforce simp: pred_def type_max_def)
apply(fastforce simp: pred_def)
by(rule Γ_of_mds_tyenv_sec)
lemma list_all_set: "∀ x ∈ set xs. P x ⟹ list_all P xs"
by (metis (lifting) list_all_iff)
theorem type_soundness_global:
assumes typeable: "⊢ cs"
shows "prog_sifum_secure_cont cs"
using typeable
apply (rule type_global_elim)
apply (subgoal_tac "∀ c ∈ set cs. com_sifum_secure c")
apply(rule sifum_compositionality_cont)
using list_all_set apply fastforce
apply fastforce
apply(drule list_all_iff[THEN iffD1])
apply clarsimp
apply(rename_tac c m)
apply(drule_tac x="(c,m)" in bspec)
apply assumption
apply clarsimp
using typed_secure by blast
end
end