adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

SELFOUR-444: CRefine proof for preemptible retype.

This commit is contained in:
Thomas Sewell 2016-09-21 10:33:03 +10:00
parent dcd7fd8c17
commit 86731939f2
24 changed files with 3104 additions and 1658 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/SIMPL_Lemmas.thy
View File

@ -227,7 +227,8 @@ lemma Guard_Seq_semantic_equiv:
lemma exec_Seq_cong:
"\<lbrakk> \<And>s''. \<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> s'' = \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s'';
\<And>s''. \<Gamma> \<turnstile> \<langle>b, Normal s''\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>d, Normal s''\<rangle> \<Rightarrow> s' \<rbrakk>
\<And>s''. \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal s''
\<Longrightarrow> \<Gamma> \<turnstile> \<langle>b, Normal s''\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>d, Normal s''\<rangle> \<Rightarrow> s' \<rbrakk>
\<Longrightarrow> \<Gamma> \<turnstile> \<langle>a ;; b, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>c ;; d, Normal s\<rangle> \<Rightarrow> s'"
apply (rule iffI)
apply (erule exec_Normal_elim_cases)

19
lib/clib/Corres_UL_C.thy
View File

@ -1598,4 +1598,23 @@ lemma ccorres_cond_seq:
apply assumption
done
lemma ccorres_assume_pre:
assumes "\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (P and (\<lambda>s'. s' = s)) P' hs H C"
shows "ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C"
apply (clarsimp simp: ccorres_underlying_def)
apply (frule assms)
apply (simp add: ccorres_underlying_def)
apply blast
done
lemma ccorres_name_pre:
"(\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C)
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C"
apply (rule ccorres_assume_pre)
apply (rule ccorres_guard_imp)
apply fastforce
apply simp
apply simp
done
end

233
lib/clib/Ctac.thy
View File

@ -11,8 +11,8 @@
(* Automation framework for general C refinement *)
theory Ctac
imports
Corres_C
imports
Corres_C
"../XPres"
begin
@ -360,8 +360,8 @@ lemma semantic_equiv_While_cong:
done
lemma semantic_equiv_Seq_cong:
assumes sea: "\<And>s s'. semantic_equiv Gamma s s' a a'"
and seb: "\<And>s s'. semantic_equiv Gamma s s' b b'"
assumes sea: "\<And>s'. semantic_equiv Gamma s s' a a'"
and seb: "\<And>s. semantic_equiv Gamma s s' b b'"
shows "semantic_equiv Gamma s s' (a ;; b) (a' ;; b')"
using sea seb
apply (simp add: semantic_equiv_def2)
@ -399,8 +399,8 @@ lemma semantic_equiv_refl:
by (rule semantic_equivI, simp)
lemma semantic_equiv_trans:
assumes sea: "\<And>s s'. semantic_equiv Gamma s s' a b"
and seb: "\<And>s s'. semantic_equiv Gamma s s' b c"
assumes sea: "semantic_equiv Gamma s s' a b"
and seb: "semantic_equiv Gamma s s' b c"
shows "semantic_equiv Gamma s s' a c"
using sea seb
by (simp add: semantic_equiv_def2)
@ -1049,8 +1049,8 @@ lemmas ceqv_rules = ceqv_refl [where xf' = xfdc] -- "Any ceqv with xfdc should b
ceqv_refl [where c = catchbrk_C]
definition
ceqv_xpres :: "(int \<rightharpoonup> ('s, int, strictc_errortype) com) \<Rightarrow> ('s \<Rightarrow> 'a) \<Rightarrow> 'a
\<Rightarrow> bool \<Rightarrow> ('s, int, strictc_errortype) com \<Rightarrow> bool \<Rightarrow> ('s, int, strictc_errortype) com \<Rightarrow> bool"
ceqv_xpres :: "('p \<rightharpoonup> ('s, 'p, 'x) com) \<Rightarrow> ('s \<Rightarrow> 'a) \<Rightarrow> 'a
\<Rightarrow> bool \<Rightarrow> ('s, 'p, 'x) com \<Rightarrow> bool \<Rightarrow> ('s, 'p, 'x) com \<Rightarrow> bool"
where
"ceqv_xpres \<Gamma> xf v pres c pres' c'
\<equiv> \<forall>s s' s''. (pres \<longrightarrow> xf s = v)
@ -1335,6 +1335,223 @@ lemma ceqv_xpres_eq_If_rules:
"ceqv_xpres_eq_If True x y x"
by (simp add: ceqv_xpres_eq_If_def)+
definition
"simpl_sequence f xs
= foldr (Seq) (map f xs) Skip"
lemma simpl_sequence_Cons:
"simpl_sequence f (x # xs) = Seq (f x) (simpl_sequence f xs)"
by (simp add: simpl_sequence_def)
fun(sequential)
simpl_final_basic_opts :: "('s, 'p, 'x) com \<Rightarrow> ('s \<Rightarrow> 's) option"
where
"simpl_final_basic_opts (x ;; y)
= (case (simpl_final_basic_opts y) of None \<Rightarrow> simpl_final_basic_opts x
| Some v \<Rightarrow> Some v)"
| "simpl_final_basic_opts (Basic f) = Some f"
| "simpl_final_basic_opts (Guard E F c) = simpl_final_basic_opts c"
| "simpl_final_basic_opts Skip = None"
| "simpl_final_basic_opts Throw = None"
| "simpl_final_basic_opts c = Some id"
definition
"simpl_final_basic c = (case simpl_final_basic_opts c
of Some v \<Rightarrow> v | None \<Rightarrow> id)"
lemmas simpl_final_basic_simps[simp]
= simpl_final_basic_def[where c="Seq c c'" for c c']
simpl_final_basic_def[where c="Basic f" for f]
simpl_final_basic_def[where c="Guard E F c" for E F c]
lemma simpl_final_basic_opts_exec[OF _ refl refl]:
"\<Gamma> \<turnstile> \<langle>c, xs\<rangle> \<Rightarrow> xs' \<Longrightarrow> xs = Normal t \<Longrightarrow> xs' = Normal t'
\<Longrightarrow> (case simpl_final_basic_opts c of None \<Rightarrow> t' = t
| Some f \<Rightarrow> \<exists>s. t' = f s)"
apply (induct arbitrary: t t' rule: exec.induct, simp_all)
apply metis
apply atomize
apply clarsimp
apply (case_tac s')
apply (auto split: option.split_asm)[1]
apply (auto elim!: exec_elim_cases)
done
lemma simpl_final_basic_exec:
"\<Gamma> \<turnstile> \<langle>c, Normal t\<rangle> \<Rightarrow> Normal t'
\<Longrightarrow> \<exists>s. t' = simpl_final_basic c s"
apply (frule simpl_final_basic_opts_exec)
apply (simp add: simpl_final_basic_def split: option.split_asm)
done
lemma ceqv_xpres_to_simpl_sequence:
fixes v :: "'a :: ring_1"
assumes c: "\<And>v. ceqv_xpres \<Gamma> xf' v True c pres (c' v)"
and v: "\<And>v s. xf' (simpl_final_basic (c' v) s) - v = offs"
shows "\<not> CP (v + of_nat n * offs)
\<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False
(simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0 ..< n])))"
(is "_ \<Longrightarrow> ceqv_xpres _ _ _ _ (While ?S _) _ _")
proof (induct n arbitrary: v)
case 0
show ?case using c[where v=v] 0
apply (simp add: simpl_sequence_def)
apply (simp add: ceqv_xpres_eq_imp ceqv_def)
apply (auto elim!: exec_Normal_elim_cases intro: exec.intros)[1]
done
next
case (Suc n)
have foo: "\<And>t t'. (\<Gamma> \<turnstile> \<langle>c' v, Normal t\<rangle> \<Rightarrow> Normal t') \<longrightarrow> xf' t' = v + offs"
using v
by (clarsimp simp: field_simps dest!: simpl_final_basic_exec)
show ?case using c[where v=v] Suc.hyps[where v="v + offs"] Suc.prems
apply (subst upt_conv_Cons, simp)
apply (simp only: map_Suc_upt[symmetric] list.simps)
apply (cases "CP v")
apply (simp add: o_def field_simps simpl_sequence_Cons
ceqv_xpres_eq_imp)
apply (clarsimp, rule ceqv_trans[where c'="c ;; While ?S c"])
apply (simp add: ceqv_def)
apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq exec.WhileTrue)[1]
apply (rule ceqv_trans[where c'="c' v ;; While ?S c"])
apply (simp add: ceqv_def)
apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq)[1]
apply (simp add: ceqv_def)
apply (intro impI exec_Seq_cong refl)
apply (simp add: foo)
apply (simp add: simpl_sequence_def field_simps)
apply (simp add: ceqv_xpres_eq_imp ceqv_def)
apply (auto intro: exec.WhileFalse exec.Skip elim!: exec_Normal_elim_cases)[1]
done
qed
lemma ceqv_xpres_While_simpl_sequence:
fixes v :: "'a :: ring_1"
assumes c: "\<And>v. ceqv_xpres \<Gamma> xf' v True c pres (c' v)"
shows "ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False
(if \<exists>n offs. (\<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs)) \<and> \<not> CP (v + of_nat n * offs)
then simpl_sequence c' (map (\<lambda>x. v + of_nat x
* (THE offs. \<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs)))
[0 ..< (LEAST n. \<not> CP (v + of_nat n
* (THE offs. \<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs))))])
else While {s. CP (xf' s)} c)"
apply (split split_if, simp add: ceqv_xpres_def[where c=c and c'=c for c])
apply (clarsimp simp: ceqv_xpres_eq_ceqv)
apply (rule ceqv_trans)
apply (rule_tac n="LEAST n. \<not> CP (v + of_nat n * offs)"
in ceqv_xpres_to_simpl_sequence[simplified ceqv_xpres_eq_ceqv, rule_format])
apply (rule c)
apply simp
apply simp
apply (rule LeastI_ex)
apply blast
apply (subst takeWhile_eq_all_conv[THEN iffD2])
apply (clarsimp dest!: not_less_Least)
apply (simp add: ceqv_def)
done
lemma ccorres_underlying_name_seq_bound:
"(\<not> CP n \<and> (\<forall>n' < n. CP n'))
\<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m
(simpl_sequence c' (map f [0 ..< n]))
\<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf
G G' hs m (if \<exists>n. \<not> CP n
then simpl_sequence c' (map f [0 ..< (LEAST n. \<not> CP n)])
else c)"
apply (subst if_P, blast)
apply (subst Least_equality[where x=n], simp_all)
apply (rule ccontr, simp add: linorder_not_le)
done
lemma sequenceE_simpl_sequence_nth_corres':
"\<lbrakk> length xs = length ys;
\<And>zs. length zs < length xs \<Longrightarrow>
ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (prev_xs @ zs @ [rv]) rv')) xf'
(inl_rrel arrel) axf
(P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs
(xs ! length zs) (f (ys ! length zs));
\<And>s \<sigma>. s \<in> Q \<Longrightarrow> P \<sigma> \<Longrightarrow>
(\<sigma>, s) \<in> sr \<Longrightarrow> \<forall>y \<in> set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} (f y) Q,UNIV;
\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -
\<rbrakk>
\<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (prev_xs @ rv) rv')) xf'
(inl_rrel arrel) axf
(\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs
(sequenceE xs)
(simpl_sequence f ys)"
proof (induct xs ys arbitrary: prev_xs rule: list_induct2)
case Nil
show ?case
apply (simp add: sequenceE_def simpl_sequence_def)
apply (rule ccorres_guard_imp2, rule ccorres_returnOk_skip)
apply simp
done
next
case (Cons x xs y ys)
show ?case
apply (simp add: simpl_sequence_Cons sequenceE_Cons)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_splitE)
apply (simp add: inl_rrel_inl_rrel)
apply (rule Cons.prems(1)[where zs=Nil, simplified])
apply (rule ceqv_refl)
apply (simp add: liftME_def[symmetric] liftME_liftM)
apply (rule ccorres_rel_imp2, rule Cons.hyps(2)[where prev_xs="prev_xs @ [rv]" for rv])
apply (rule ccorres_guard_imp2, rule ccorres_rel_imp2,
rule Cons.prems(1)[where zs="z # zs" for z zs, simplified])
apply simp+
apply (blast dest: Cons.prems[simplified])
apply simp
apply (cut_tac n="Suc n" in Cons.prems(3), simp, simp)
apply (clarsimp elim!: inl_inrE)
apply assumption
apply (clarsimp elim!: inl_inrE)
apply simp
apply (rule hoare_vcg_const_imp_lift_R)
apply (rule hoare_gen_asmE)
apply (erule Cons.prems(3)[where n=0, simplified])
apply (rule_tac P="Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}"
in HoarePartial.conseq_exploit_pre)
apply (clarsimp, rule conseqPost, rule Cons.prems(2)[simplified, THEN conjunct1],
simp+)
apply (clarsimp simp: ccHoarePost_def elim!: inl_inrE)
apply simp
apply auto
done
qed
lemmas sequenceE_simpl_sequence_nth_corres
= sequenceE_simpl_sequence_nth_corres'[where prev_xs=Nil, simplified]
lemma mapME_x_simpl_sequence_fun_related:
"\<lbrakk> ys = map yf xs;
\<And>n x. x \<in> set xs \<Longrightarrow>
ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf
(P and F n (n < length xs) x) Q hs
(f x) (f' (yf x));
\<And>s \<sigma>. s \<in> Q \<Longrightarrow> P \<sigma> \<Longrightarrow>
(\<sigma>, s) \<in> sr \<Longrightarrow> \<forall>x \<in> set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} (f' (yf x)) Q,UNIV;
\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F n True (xs ! n)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. P and F (Suc n) (Suc n < length xs) (xs ! Suc n)\<rbrace>, -
\<rbrakk>
\<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc
(inl_rrel arrel) axf
(P and F 0 (xs \<noteq> []) (xs ! 0)) Q hs
(mapME_x f xs)
(simpl_sequence f' ys)"
apply (simp add: mapME_x_sequenceE liftME_def[symmetric]
liftME_liftM)
apply (rule ccorres_rel_imp2, rule ccorres_guard_imp2,
rule sequenceE_simpl_sequence_nth_corres[where r'=dc and xf'=xfdc
and P=P and F="\<lambda>i. F i (i < length xs) (xs ! i)" and Q=Q and arrel=arrel and axf=axf];
clarsimp elim!: inl_inrE)
apply (erule_tac x="length zs" in meta_allE
| erule_tac x="xs ! length zs" in meta_allE)+
apply (simp add: dc_def)
done
lemmas mapME_x_simpl_sequence_same
= mapME_x_simpl_sequence_fun_related[where yf=id, simplified]
lemma call_ignore_cong:
"call i f g r = call i f g r" by (rule refl)

17
lib/clib/ctac-method.ML
View File

@ -123,6 +123,10 @@ val ctac_post_del = Thm.declaration_attribute
(fn thm =>
(ctac_post.map (Thm.del_thm thm)));
val ceqv_simpl_sequence_pair = Attrib.config_bool
@{binding ceqv_simpl_sequence} (K false)
fun ceqv_simpl_seq ctxt = Config.get ctxt (fst ceqv_simpl_sequence_pair)
val setup =
Attrib.setup @{binding "corres"} (Attrib.add_del ctac_add ctac_del)
"correspondence rules"
@ -131,7 +135,8 @@ val setup =
"correspondence preprocessing rules"
#> Attrib.setup @{binding "corres_post"}
(Attrib.add_del ctac_post_add ctac_post_del)
"correspondence postprocessing rules";
"correspondence postprocessing rules"
#> snd ceqv_simpl_sequence_pair;
(* tacticals *)
@ -327,14 +332,20 @@ val ceqv_xpres_eq_If_rules = @{thms ceqv_xpres_eq_If_rules};
val apply_ceqv_xpres_rules_trace = ref @{term True};
fun apply_ceqv_xpres_rules ctxt _ n = DETERM
(resolve_tac ctxt ceqv_xpres_rules n
fun apply_ceqv_xpres_rules1 ctxt rules _ n = DETERM
(resolve_tac ctxt rules n
ORELSE (SUBGOAL (fn (t, n) =>
(warning ("apply_ceqv_xpres_rules: no rule applied"
^ " - see CtacImpl.apply_ceqv_xpres_rules_trace");
apply_ceqv_xpres_rules_trace := t;
resolve_tac ctxt [ceqv_xpres_FalseI] n)) n));
fun apply_ceqv_xpres_rules ctxt = let
val seq = ceqv_simpl_seq ctxt
val ex_rules = if seq then [@{thm ceqv_xpres_While_simpl_sequence}]
else []
in apply_ceqv_xpres_rules1 ctxt (ex_rules @ ceqv_xpres_rules) end
fun addcongs thms ss = foldl (uncurry Simplifier.add_cong) ss thms
fun delsplits thms ss = foldl (uncurry Splitter.del_split) ss thms

68
proof/crefine/ADT_C.thy
View File

@ -1440,12 +1440,45 @@ lemma cbitmap_L2_to_H_correct:
apply clarsimp
done
definition
mk_gsUntypedZeroRanges
where
"mk_gsUntypedZeroRanges s
= ran (untypedZeroRange \<circ>\<^sub>m (option_map cteCap o map_to_ctes (cstate_to_pspace_H s)))"
lemma cpspace_user_data_relation_user_mem'[simp]:
"\<lbrakk>pspace_aligned' as;pspace_distinct' as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
= cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)"
by (simp add: cmap_relation_def)
lemma cpspace_device_data_relation_user_mem'[simp]:
"cpspace_device_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
= cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)"
apply (clarsimp simp: cmap_relation_def cuser_user_data_device_relation_def heap_to_device_data_def)
apply (rule_tac arg_cong[where f = "%x. x = y" for y])
by auto
lemma (in kernel) mk_gsUntypedZeroRanges_correct:
assumes valid: "valid_state' as"
assumes cstate_rel: "cstate_relation as cs"
shows "mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as"
using assms
apply (clarsimp simp: valid_state'_def untyped_ranges_zero_inv_def
mk_gsUntypedZeroRanges_def cteCaps_of_def)
apply (subst cstate_to_pspace_H_correct[where c=cs], simp_all)
apply (clarsimp simp: cstate_relation_def Let_def)
apply (subst cstate_to_machine_H_correct, assumption, simp_all)
apply (clarsimp simp: cpspace_relation_def)+
apply (clarsimp simp: observable_memory_def valid_pspace'_def)
done
definition (in state_rel)
cstate_to_H :: "globals \<Rightarrow> kernel_state"
where
"cstate_to_H s \<equiv>
\<lparr>ksPSpace = cstate_to_pspace_H s,
gsUserPages = fst (ghost'state_' s), gsCNodes = fst (snd (ghost'state_' s)),
gsUntypedZeroRanges = mk_gsUntypedZeroRanges s,
gsMaxObjectSize = (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' s))
in if v = 0 then card (UNIV :: word32 set) else v),
ksDomScheduleIdx = unat (ksDomScheduleIdx_' s),
@ -1468,36 +1501,25 @@ where
lemma trivial_eq_conj: "B = C \<Longrightarrow> (A \<and> B) = (A \<and> C)"
by simp
lemma cpspace_user_data_relation_user_mem'[simp]:
"\<lbrakk>pspace_aligned' as;pspace_distinct' as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
= cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)"
by (simp add: cmap_relation_def)
lemma cpspace_device_data_relation_user_mem'[simp]:
"cpspace_device_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
= cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)"
apply (clarsimp simp: cmap_relation_def cuser_user_data_device_relation_def heap_to_device_data_def)
apply (rule_tac arg_cong[where f = "%x. x = y" for y])
by auto
lemma (in kernel_m) cstate_to_H_correct:
assumes valid: "valid_state' as"
assumes cstate_rel: "cstate_relation as cs"
shows "cstate_to_H cs = as \<lparr>ksMachineState:= observable_memory (ksMachineState as) (user_mem' as)\<rparr>"
apply (subgoal_tac "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)")
apply (rule kernel_state.equality, simp_all add: cstate_to_H_def)
apply (rule cstate_to_pspace_H_correct)
using valid
apply (simp add: valid_state'_def)
using cstate_rel valid
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
observable_memory_def valid_state'_def
valid_pspace'_def)
apply (rule cstate_to_pspace_H_correct)
using valid
apply (simp add: valid_state'_def)
using cstate_rel valid
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
observable_memory_def valid_state'_def
valid_pspace'_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
using cstate_rel
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
using cstate_rel
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
using valid cstate_rel
apply (rule mk_gsUntypedZeroRanges_correct)
using cstate_rel
apply (fastforce simp: cstate_relation_def cpspace_relation_def
Let_def ghost_size_rel_def unat_eq_0

108
proof/crefine/Arch_C.thy
View File

@ -88,9 +88,10 @@ lemma performPageTableInvocationUnmap_ccorres:
apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap_ArchObject)
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule rev_bexI)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
typ_heap_simps')
apply (rule conjI)
apply (clarsimp simp: cpspace_relation_def)
apply (clarsimp simp: cpspace_relation_def typ_heap_simps')
apply (subst setCTE_tcb_case, assumption+)
apply (clarsimp dest!: ksPSpace_update_eq_ExD)
apply (erule cmap_relation_updI, assumption)
@ -106,7 +107,7 @@ lemma performPageTableInvocationUnmap_ccorres:
cap_page_table_cap_lift_def)
apply simp
apply (clarsimp simp: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff
typ_heap_simps'
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
dest!: ksPSpace_update_eq_ExD)
apply (simp add: cte_wp_at_ctes_of)
@ -146,6 +147,7 @@ lemma createObjects_asidpool_ccorres:
shows "ccorres dc xfdc
((\<lambda>s. \<exists>p. cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap isdev frame pageBits idx ) p s)
and pspace_aligned' and pspace_distinct' and valid_objs'
and ret_zero frame (2 ^ pageBits)
and valid_global_refs' and pspace_no_overlap' frame pageBits)
({s. region_actually_is_bytes frame (2^pageBits) s})
hs
@ -156,6 +158,7 @@ proof -
have helper: "\<forall>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<and> is_aligned frame pageBits \<and> frame \<noteq> 0
\<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma>
\<and> pspace_no_overlap' frame pageBits \<sigma>
\<and> ret_zero frame (2 ^ pageBits) \<sigma>
\<and> region_actually_is_bytes frame (2 ^ pageBits) x
\<and> {frame ..+ 2 ^ pageBits} \<inter> kernel_data_refs = {}
\<longrightarrow>
@ -178,9 +181,10 @@ proof -
hence rf: "(\<sigma>, x) \<in> rf_sr" and al: "is_aligned frame pageBits" and ptr0: "frame \<noteq> 0"
and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>"
and pno: "pspace_no_overlap' frame pageBits \<sigma>"
and zro: "ret_zero frame (2 ^ pageBits) \<sigma>"
and actually: "region_actually_is_bytes frame (2 ^ pageBits) x"
and kdr: "{frame ..+ 2 ^ pageBits} \<inter> kernel_data_refs = {}"
by (simp_all)
by simp_all
note empty = region_actually_is_bytes[OF actually]
@ -307,7 +311,7 @@ proof -
apply (rule relrl)
done
thus ?thesis using rf empty kdr
thus ?thesis using rf empty kdr zro
apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name
ko_def[symmetric])
apply (simp add: carch_state_relation_def cmachine_state_relation_def)
@ -316,6 +320,7 @@ proof -
kernel_data_refs_domain_eq_rotate
cvariable_array_ptr_retyps[OF szo]
foldr_upd_app_if [folded data_map_insert_def]
zero_ranges_ptr_retyps
rl empty projectKOs)
done
qed
@ -425,17 +430,31 @@ shows
apply (rule ccorres_Guard_Seq[where S=UNIV])?
apply (rule deleteObjects_ccorres)
apply ceqv
apply (rule ccorres_move_c_guard_cte)
apply csymbr
apply (rule ccorres_rhs_assoc2)
apply (rule ccorres_abstract_cleanup)
apply (rule ccorres_symb_exec_l)
apply (rule_tac P = "rva = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm)
apply (simp add: hrs_htd_update del:fun_upd_apply)
apply (rule ccorres_move_Guard_Seq_strong[OF c_guard_abs_cte])
apply (ctac add:update_freeIndex)
apply (rule ccorres_split_nothrow)
apply (rule_tac cap'="UntypedCap isdev frame pageBits idx" in updateFreeIndex_ccorres)
apply (rule allI, rule conseqPre, vcg)
apply (rule subsetI, clarsimp simp: typ_heap_simps' pageBits_def isCap_simps)
apply (frule ccte_relation_ccap_relation, clarsimp)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: isCap_simps cap_lift_untyped_cap
cap_to_H_simps cap_untyped_cap_lift_def
ccap_relation_def modify_map_def
fun_eq_iff
dest!: word_unat.Rep_inverse' split: split_if)
apply (rule exI, strengthen refl)
apply (case_tac cte', simp add: cap_lift_untyped_cap max_free_index_def mask_def)
apply (simp add: mex_def meq_def del: split_paired_Ex)
apply blast
apply ceqv
apply ccorres_remove_UNIV_guard
apply (rule ccorres_Guard_Seq[where F=ShiftError])+
apply (ctac (c_lines 2) add:createObjects_asidpool_ccorres
apply (ctac (c_lines 2) add:createObjects_asidpool_ccorres[where idx="max_free_index pageBits"]
pre del: ccorres_Guard_Seq)
apply csymbr
apply (ctac (no_vcg) add: cteInsert_ccorres)
@ -471,15 +490,16 @@ shows
apply vcg
apply (clarsimp simp:conj_comms objBits_simps archObjSize_def |
strengthen valid_pspace_mdb' vp_strgs' invs_valid_pspace'
valid_pspace_valid_objs' invs_valid_global')+
valid_pspace_valid_objs' invs_valid_global'
invs_urz)+
apply (wp updateFreeIndex_forward_invs'
updateFreeIndex_caps_no_overlap''[where cap = "UntypedCap isdev frame pageBits idx",simplified]
updateFreeIndex_pspace_no_overlap'[where cap = "UntypedCap isdev frame pageBits idx",simplified]
updateFreeIndex_caps_overlap_reserved'[where cap = "UntypedCap isdev frame pageBits idx",simplified])
apply (rule_tac P1 = "\<lambda>x. x = UntypedCap isdev frame pageBits (max_free_index pageBits)"
in hoare_strengthen_post[OF updateCap_weak_cte_wp_at[where p = parent]])
apply (rule exI)
apply assumption
updateFreeIndex_caps_no_overlap''[where sz=pageBits]
updateFreeIndex_pspace_no_overlap'[where sz=pageBits]
updateFreeIndex_caps_overlap_reserved
updateFreeIndex_cte_wp_at
)
apply (strengthen exI[where x=parent])
apply (wp updateFreeIndex_cte_wp_at)
apply clarsimp
apply vcg
apply wp
@ -496,19 +516,23 @@ shows
pageBits_def max_free_index_def asid_low_bits_def)
apply (case_tac cte,clarsimp simp:invs_valid_pspace')
apply (frule(1) ctes_of_valid_cap'[OF _ invs_valid_objs'])
apply (clarsimp simp:valid_cap'_def asid_low_bits_def)
apply (clarsimp simp:valid_cap'_def asid_low_bits_def invs_urz)
apply (strengthen descendants_range_in_subseteq'[mk_strg I E] refl)
apply simp
apply (intro conjI)
apply (simp add:is_aligned_def)
apply (simp add:is_aligned_def)
apply (rule descendants_range_caps_no_overlapI'[where d=isdev and cref = parent])
apply simp
apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq)
apply (clarsimp simp:is_aligned_neg_mask_eq)
apply (rule le_m1_iff_lt[THEN iffD1,THEN iffD1])
apply (simp add:asid_bits_def)
apply (simp add:mask_def)
apply simp
apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq)
apply (clarsimp simp:is_aligned_neg_mask_eq)
apply (rule le_m1_iff_lt[THEN iffD1,THEN iffD1])
apply (simp add:asid_bits_def)
apply (simp add:mask_def)
apply (clarsimp dest!: upto_intvl_eq)
apply (wp deleteObjects_cte_wp_at'[where d=isdev and idx = idx and p = parent]
deleteObjects_descendants[where d=isdev and p = parent and idx = idx]
deleteObjects_invs'[where d=isdev and p = parent and idx = idx]
Detype_R.deleteObjects_descendants[where p = parent and idx = idx]
deleteObjects_ct_active'[where d=isdev and cref = parent and idx = idx])
apply clarsimp
apply vcg
@ -516,7 +540,7 @@ shows
apply (frule cte_wp_at_valid_objs_valid_cap', fastforce)
apply (clarsimp simp:valid_cap'_def capAligned_def cte_wp_at_ctes_of
descendants_range'_def2 empty_descendants_range_in')
apply (intro conjI)
apply (intro conjI; (rule refl)?)
apply clarsimp
apply (drule(1) cte_cap_in_untyped_range[where ptr = frame])
apply (fastforce simp: cte_wp_at_ctes_of)
@ -532,18 +556,15 @@ shows
apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap dest!: ccte_relation_ccap_relation)
apply (clarsimp simp: is_aligned_mask max_free_index_def pageBits_def
gen_framesize_to_H_def)
apply (rule conjI, rule UNIV_I)?
apply clarsimp?
apply (erule_tac s = sa in rf_sr_ctes_of_cliftE)
apply assumption
apply (frule_tac s = sa in rf_sr_cte_relation)
apply simp+
apply (clarsimp simp:typ_heap_simps' )
apply (rule context_conjI)
apply (rule cap_get_tag_isCap_unfolded_H_cap)
apply (fastforce dest!:ccte_relation_ccap_relation)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (intro conjI)
apply ((drule cap_get_tag_UntypedCap,
clarsimp simp:unat32_eq_of_nat word_bits_conv)+)[2]
apply (clarsimp simp:typ_heap_simps' region_is_bytes'_def[where sz=0])
apply (frule ccte_relation_ccap_relation)
apply (clarsimp simp: cap_get_tag_isCap)
apply (clarsimp simp: hrs_htd_update_def split_def
pageBits_def
split: split_if)
@ -553,18 +574,19 @@ shows
apply assumption
apply (simp add: ghost_assertion_data_get_gs_clear_region[unfolded o_def])
apply (drule valid_global_refsD_with_objSize, clarsimp)+
apply clarsimp+
apply (clarsimp simp: isCap_simps dest!: ccte_relation_ccap_relation)
apply (cut_tac ptr=frame and bits=12 and s="globals_update (t_hrs_'_update (hrs_htd_update
(typ_region_bytes frame 12))) s'" in typ_region_bytes_actually_is_bytes)
apply (simp add: hrs_htd_update)
apply clarsimp
apply (intro conjI)
apply (clarsimp elim!:is_aligned_weaken)
apply (simp add:is_aligned_def)
apply (erule is_aligned_no_wrap',simp)
apply (drule region_actually_is_bytes_dom_s[OF _ order_refl])
apply (simp add: hrs_htd_update_def split_def)
apply (clarsimp simp: region_actually_is_bytes_def hrs_htd_def
hrs_htd_update_def split_def)
apply (clarsimp simp: region_actually_is_bytes_def hrs_htd_update)
apply (simp add: hrs_htd_def hrs_htd_update_def split_def)
apply (clarsimp simp: ccap_relation_def)
apply (clarsimp simp: cap_asid_pool_cap_lift)
apply (clarsimp simp: cap_to_H_def)
@ -860,7 +882,8 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (clarsimp simp: rf_sr_ksCurThread "StrictC'_thread_state_defs"
mask_eq_iff_w2p word_size
ct_in_state'_def st_tcb_at'_def
word_sle_def word_sless_def)
word_sle_def word_sless_def
typ_heap_simps')
apply (clarsimp simp: cap_get_tag_isCap_ArchObject isCap_simps
word_sle_def word_sless_def
word_less_nat_alt)
@ -3703,7 +3726,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (case_tac st,simp+)
apply (frule cap_get_tag_isCap_unfolded_H_cap(15))
apply (clarsimp simp: cap_lift_page_directory_cap hd_conv_nth
cap_lift_page_table_cap
cap_lift_page_table_cap typ_heap_simps'
cap_to_H_def cap_page_directory_cap_lift_def
to_bool_def cap_page_table_cap_lift_def
typ_heap_simps' shiftl_t2n[where n=2] field_simps
@ -3711,7 +3734,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (intro conjI impI allI)
apply (clarsimp simp:ThreadState_Restart_def less_mask_eq rf_sr_ksCurThread
resolve_ret_rel_def framesize_from_to_H framesize_from_H_mask2
to_option_def rel_option_alt_def to_bool_def
to_option_def rel_option_alt_def to_bool_def typ_heap_simps'
split:option.splits if_splits
| fastforce simp: mask_def
| rule flushtype_relation_triv,simp add:isPageFlush_def isPDFlushLabel_def
@ -3727,6 +3750,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (clarsimp simp:ThreadState_Restart_def less_mask_eq rf_sr_ksCurThread
resolve_ret_rel_def framesize_from_to_H framesize_from_H_mask2
to_option_def rel_option_alt_def to_bool_def
typ_heap_simps'
split:option.splits if_splits
| fastforce simp: mask_def
| rule flushtype_relation_triv,simp add:isPageFlush_def isPDFlushLabel_def
@ -3742,6 +3766,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (clarsimp simp:ThreadState_Restart_def less_mask_eq rf_sr_ksCurThread
resolve_ret_rel_def framesize_from_to_H framesize_from_H_mask2
to_option_def rel_option_alt_def to_bool_def
typ_heap_simps'
split:option.splits if_splits
| fastforce simp: mask_def
| rule flushtype_relation_triv,simp add:isPageFlush_def isPDFlushLabel_def
@ -3757,6 +3782,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
by (clarsimp simp:ThreadState_Restart_def less_mask_eq rf_sr_ksCurThread
resolve_ret_rel_def framesize_from_to_H framesize_from_H_mask2
to_option_def rel_option_alt_def to_bool_def
typ_heap_simps'
split:option.splits if_splits
| fastforce simp: mask_def
| rule flushtype_relation_triv,simp add:isPageFlush_def isPDFlushLabel_def

395
proof/crefine/CSpace_C.thy
View File

@ -638,7 +638,8 @@ lemma ccorres_updateMDB_set_mdbNext [corres]:
apply (erule bexI [rotated])
apply (clarsimp simp add: rf_sr_def cstate_relation_def
Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"])
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps')
apply (rule conjI)
apply (erule (2) cspace_cte_relation_upd_mdbI)
apply (simp add: cmdbnode_relation_def)
@ -685,7 +686,8 @@ lemma ccorres_updateMDB_set_mdbPrev [corres]:
apply (erule bexI [rotated])
apply (clarsimp simp add: rf_sr_def cstate_relation_def
Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"])
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps')
apply (rule conjI)
apply (erule (2) cspace_cte_relation_upd_mdbI)
apply (simp add: cmdbnode_relation_def)
@ -693,7 +695,7 @@ lemma ccorres_updateMDB_set_mdbPrev [corres]:
subgoal for _ s' by (cases "v_' s' = 0"; simp)
apply (erule_tac t = s'a in ssubst)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff)
h_t_valid_clift_Some_iff typ_heap_simps')
apply (erule (1) setCTE_tcb_case)
apply clarsimp
@ -1935,48 +1937,6 @@ done
(************************************************************************)
(*-------------------------------------------------------------------------------------*)
(* redefining Haskell definition of emptySlot so that it corresponds to the C code ----*)
(*-------------------------------------------------------------------------------------*)
lemma emptySlot_def:
"emptySlot slot irq = (do
newCTE \<leftarrow> getCTE slot;
(if ((cteCap newCTE) \<noteq> NullCap)
then (do
mdbNode \<leftarrow> return ( cteMDBNode newCTE);
prev \<leftarrow> return ( mdbPrev mdbNode);
next \<leftarrow> return ( mdbNext mdbNode);
updateMDB prev (\<lambda> mdb. mdb \<lparr> mdbNext := next \<rparr>);
updateMDB next (\<lambda> mdb. mdb \<lparr>
mdbPrev := prev,
mdbFirstBadged :=
mdbFirstBadged mdb \<or> mdbFirstBadged mdbNode \<rparr>);
updateCap slot NullCap;
updateMDB slot (const nullMDBNode);
(case irq of
Some irq \<Rightarrow> deletedIRQHandler irq
| None \<Rightarrow> return ()
)
od)
else return ()
)
od)"
apply (simp add: emptySlot_def)
apply (rule bind_eqI)
apply (rule ext)
apply (case_tac "cteCap newCTE")
apply (simp_all add: bind_assoc)
done
declare split_if [split del]
@ -2070,6 +2030,7 @@ lemma emptySlot_helper:
apply (erule_tac t = s' in ssubst)
apply (simp add: carch_state_relation_def cmachine_state_relation_def h_t_valid_clift_Some_iff
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps'
cong: lifth_update)
apply (erule (1) setCTE_tcb_case)
@ -2100,6 +2061,7 @@ lemma emptySlot_helper:
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps'
cong: lifth_update)
apply (erule (1) setCTE_tcb_case)
@ -2124,7 +2086,7 @@ lemma emptySlot_helper:
apply (rule ccorres_return_Skip)
apply simp
apply (clarsimp simp: cmdbnode_relation_def)
done
done
@ -2358,78 +2320,256 @@ ML_command {*show_abbrevs true*}
ML_command {*show_abbrevs false*}
*)
lemmas ccorres_split_noop_lhs
= ccorres_split_nothrow[where c=Skip, OF _ ceqv_refl _ _ hoarep.Skip,
simplified ccorres_seq_skip]
(* FIXME: to SR_Lemmas *)
lemma region_is_bytes_subset:
"region_is_bytes' ptr sz htd
\<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
\<Longrightarrow> region_is_bytes' ptr' sz' htd"
by (auto simp: region_is_bytes'_def)
lemma intvl_both_le:
"\<lbrakk> a \<le> x; unat x + y \<le> unat a + b \<rbrakk>
\<Longrightarrow> {x ..+ y} \<le> {a ..+ b}"
apply (rule order_trans[OF _ intvl_sub_offset[where x="x - a"]])
apply (simp, rule order_refl)
apply unat_arith
done
lemma untypedZeroRange_idx_forward_helper:
"isUntypedCap cap
\<Longrightarrow> capFreeIndex cap \<le> idx
\<Longrightarrow> idx \<le> 2 ^ capBlockSize cap
\<Longrightarrow> valid_cap' cap s
\<Longrightarrow> (case (untypedZeroRange cap, untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap))
of (Some (a, b), Some (a', b')) \<Rightarrow> {a' ..+ unat (b' + 1 - a')} \<subseteq> {a ..+ unat (b + 1 - a)}
| _ \<Rightarrow> True)"
apply (clarsimp split: option.split)
apply (clarsimp simp: untypedZeroRange_def max_free_index_def Let_def
isCap_simps valid_cap_simps' capAligned_def
split: split_if_asm)
apply (erule subsetD[rotated], rule intvl_both_le)
apply (clarsimp simp: getFreeRef_def)
apply (rule word_plus_mono_right)
apply (rule PackedTypes.of_nat_mono_maybe_le)
apply (erule order_le_less_trans, rule power_strict_increasing, simp_all)
apply (erule is_aligned_no_wrap')
apply (rule word_of_nat_less, simp)
apply (simp add: getFreeRef_def)
apply (simp add: unat_plus_simple[THEN iffD1, OF is_aligned_no_wrap']
word_of_nat_less)
apply (simp add: word_of_nat_le unat_sub
order_le_less_trans[OF _ power_strict_increasing]
unat_of_nat_eq[where 'a=32, folded word_bits_def])
done
lemma intvl_close_Un:
"y = x + of_nat n
\<Longrightarrow> ({x ..+ n} \<union> {y ..+ m}) = {x ..+ n + m}"
apply ((simp add: intvl_def, safe, simp_all,
simp_all only: of_nat_add[symmetric]); (rule exI, strengthen refl))
apply simp_all
apply (rule ccontr)
apply (drule_tac x="k - n" in spec)
apply simp
done
lemma untypedZeroRange_idx_backward_helper:
"isUntypedCap cap
\<Longrightarrow> idx \<le> capFreeIndex cap
\<Longrightarrow> idx \<le> 2 ^ capBlockSize cap
\<Longrightarrow> valid_cap' cap s
\<Longrightarrow> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap)
of None \<Rightarrow> True | Some (a', b') \<Rightarrow>
{a' ..+ unat (b' + 1 - a')} \<subseteq> {capPtr cap + of_nat idx ..+ (capFreeIndex cap - idx)}
\<union> (case untypedZeroRange cap
of Some (a, b) \<Rightarrow> {a ..+ unat (b + 1 - a)}
| None \<Rightarrow> {})
)"
apply (clarsimp split: option.split, intro impI conjI allI)
apply (rule intvl_both_le; clarsimp simp: untypedZeroRange_def
max_free_index_def Let_def
isCap_simps valid_cap_simps' capAligned_def
split: split_if_asm)
apply (clarsimp simp: getFreeRef_def)
apply (clarsimp simp: getFreeRef_def)
apply (simp add: word_of_nat_le unat_sub
order_le_less_trans[OF _ power_strict_increasing]
unat_of_nat_eq[where 'a=32, folded word_bits_def])
apply (subst intvl_close_Un)
apply (clarsimp simp: untypedZeroRange_def
max_free_index_def Let_def
getFreeRef_def
split: split_if_asm)
apply (clarsimp simp: untypedZeroRange_def
max_free_index_def Let_def
getFreeRef_def isCap_simps valid_cap_simps'
split: split_if_asm)
apply (simp add: word_of_nat_le unat_sub capAligned_def
order_le_less_trans[OF _ power_strict_increasing]
order_le_less_trans[where x=idx]
unat_of_nat_eq[where 'a=32, folded word_bits_def])
done
lemma ctes_of_untyped_zero_rf_sr_case:
"\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
untyped_ranges_zero' s \<rbrakk>
\<Longrightarrow> case untypedZeroRange (cteCap cte)
of None \<Rightarrow> True
| Some (start, end) \<Rightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
by (simp split: option.split add: ctes_of_untyped_zero_rf_sr)
lemma gsUntypedZeroRanges_update_helper:
"(\<sigma>, s) \<in> rf_sr
\<Longrightarrow> (zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s))
\<longrightarrow> zero_ranges_are_zero (f (gsUntypedZeroRanges \<sigma>)) (t_hrs_' (globals s)))
\<Longrightarrow> (gsUntypedZeroRanges_update f \<sigma>, s) \<in> rf_sr"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
lemma heap_list_zero_Ball_intvl:
"heap_list_is_zero hmem ptr n = (\<forall>x \<in> {ptr ..+ n}. hmem x = 0)"
apply safe
apply (erule heap_list_h_eq_better)
apply (simp add: heap_list_rpbs)
apply (rule trans[OF heap_list_h_eq2 heap_list_rpbs])
apply simp
done
lemma untypedZeroRange_not_device:
"untypedZeroRange cap = Some r
\<Longrightarrow> \<not> capIsDevice cap"
by (clarsimp simp: untypedZeroRange_def)
lemma updateTrackedFreeIndex_noop_ccorres:
"ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap
\<and> idx \<le> 2 ^ capBlockSize cap
\<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) o cteCap) slot
and valid_objs' and untyped_ranges_zero')
{s. \<not> capIsDevice cap' \<longrightarrow> region_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs
(updateTrackedFreeIndex slot idx) Skip"
(is "ccorres dc xfdc ?P ?P' _ _ _")
apply (simp add: updateTrackedFreeIndex_def getSlotCap_def)
apply (rule ccorres_guard_imp)
apply (rule ccorres_pre_getCTE[where P="\<lambda>rv.
cte_wp_at' (op = rv) slot and ?P" and P'="K ?P'"])
apply (rule ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (frule(1) ctes_of_valid')
apply (frule(2) ctes_of_untyped_zero_rf_sr_case)
apply (clarsimp simp: simpler_modify_def bind_def cte_wp_at_ctes_of)
apply (erule gsUntypedZeroRanges_update_helper)
apply (clarsimp simp: zero_ranges_are_zero_def
split: split_if)
apply (case_tac "(a, b) \<in> gsUntypedZeroRanges \<sigma>")
apply (drule(1) bspec, simp)
apply (erule disjE_L)
apply (frule(3) untypedZeroRange_idx_forward_helper)
apply (clarsimp simp: isCap_simps valid_cap_simps')
apply (case_tac "untypedZeroRange (cteCap cte)")
apply (clarsimp simp: untypedZeroRange_def
valid_cap_simps'
max_free_index_def Let_def
split: split_if_asm)
apply clarsimp
apply (thin_tac "\<not> capIsDevice cap' \<longrightarrow> P" for P)
apply (clarsimp split: option.split_asm)
apply (subst region_is_bytes_subset, simp+)
apply (subst heap_list_is_zero_mono2, simp+)
apply (frule untypedZeroRange_idx_backward_helper[where idx=idx],
simp+)
apply (clarsimp simp: isCap_simps valid_cap_simps')
apply (clarsimp split: option.split_asm)
apply (clarsimp dest!: untypedZeroRange_not_device)
apply (subst region_is_bytes_subset, simp+)
apply (subst heap_list_is_zero_mono2, simp+)
apply (simp add: region_is_bytes'_def heap_list_zero_Ball_intvl)
apply (clarsimp dest!: untypedZeroRange_not_device)
apply blast
apply (clarsimp simp: cte_wp_at_ctes_of)
apply clarsimp
done
lemma updateTrackedFreeIndex_forward_noop_ccorres:
"ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap
\<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) o cteCap) slot
and valid_objs' and untyped_ranges_zero') UNIV hs
(updateTrackedFreeIndex slot idx) Skip"
(is "ccorres dc xfdc ?P UNIV _ _ _")
apply (rule ccorres_name_pre)
apply (rule ccorres_guard_imp2,
rule_tac cap'="cteCap (the (ctes_of s slot))" in updateTrackedFreeIndex_noop_ccorres)
apply (clarsimp simp: cte_wp_at_ctes_of region_is_bytes'_def)
done
lemma clearUntypedFreeIndex_noop_ccorres:
"ccorres dc xfdc (valid_objs' and untyped_ranges_zero') UNIV hs
(clearUntypedFreeIndex p) Skip"
apply (simp add: clearUntypedFreeIndex_def getSlotCap_def)
apply (rule ccorres_guard_imp)
apply (rule ccorres_pre_getCTE[where P="\<lambda>rv. cte_wp_at' (op = rv) p
and valid_objs' and untyped_ranges_zero'" and P'="K UNIV"])
apply (case_tac "cteCap cte", simp_all add: ccorres_guard_imp[OF ccorres_return_Skip])[1]
apply (rule ccorres_guard_imp, rule updateTrackedFreeIndex_forward_noop_ccorres)
apply (clarsimp simp: cte_wp_at_ctes_of max_free_index_def)
apply (frule(1) Finalise_R.ctes_of_valid')
apply (clarsimp simp: valid_cap_simps')
apply simp
apply (clarsimp simp: cte_wp_at_ctes_of)
apply simp
done
lemma emptySlot_ccorres:
"ccorres dc xfdc
(valid_mdb' and pspace_aligned')
(valid_mdb' and valid_objs' and pspace_aligned'
and untyped_ranges_zero')
(UNIV \<inter> {s. slot_' s = Ptr slot}
\<inter> {s. irq_opt_relation irq (irq_' s)} )
[]
(emptySlot slot irq)
(Call emptySlot_'proc)"
apply (cinit lift: slot_' irq_' simp del: return_bind)
apply (cinit lift: slot_' irq_' simp: case_Null_If)
-- "***Main goal***"
apply (unfold emptySlot_def) -- "unfolding the new definition"
-- "--- handle the clearUntypedFreeIndex"
apply (rule ccorres_split_noop_lhs, rule clearUntypedFreeIndex_noop_ccorres)
-- "--- instruction: newCTE \<leftarrow> getCTE slot; ---"
apply (rule ccorres_pre_getCTE)
apply (rule ccorres_pre_getCTE)
-- "--- instruction: CALL on C side"
(* apply (rule ccorres_Guard_Seq) *)
apply (rule ccorres_move_c_guard_cte)
apply csymbr
apply (rule ccorres_move_c_guard_cte)
apply csymbr
apply (rule ccorres_abstract_cleanup)
apply (rename_tac cap_tag)
apply (rule_tac P="(cap_tag = scast cap_null_cap)
= (cteCap newCTE = NullCap)" in ccorres_gen_asm2)
apply (simp del: Collect_const)
-- "--- instruction: if-then-else / IF-THEN-ELSE "
apply (rule ccorres_guard_imp2)
-- "*** Main Goal ***"
apply (rule ccorres_cond2)
-- "--- instruction: if-then-else / IF-THEN-ELSE "
apply (rule ccorres_cond2'[where R=\<top>])
-- "*** link between abstract and concrete conditionals ***"
apply clarsimp
apply (subgoal_tac "\<exists> cap'. ret__unsigned = cap_get_tag cap'
\<and> ccap_relation (cteCap rv) cap' ")
apply (insert not_NullCap_eq_not_cap_null_cap)[1]
subgoal by (clarsimp)
apply assumption
(* apply clarsimp
apply (subgoal_tac "\<exists> cap'. ret__unsigned_long = cap_get_tag cap'
\<and> ccap_relation (cteCap newCTE) cap' ")
prefer 2 apply assumption
apply clarsimp
apply (simp add: not_NullCap_eq_not_cap_null_cap)*)
apply (clarsimp split: split_if)
-- "*** proof for the 'else' branch (return () and SKIP) ***"
prefer 2
apply (ctac add: ccorres_return_Skip)
apply (ctac add: ccorres_return_Skip[unfolded dc_def])
-- "*** proof for the 'then' branch ***"
-- "---instructions: multiple undefined on C side"
-- "---instructions: multiple on C side, including mdbNode fetch"
apply (rule ccorres_rhs_assoc)+
-- "we have to do it here because the first assoc did not apply inside the then block"
apply csymbr
apply csymbr
apply csymbr
apply (rule ccorres_move_c_guard_cte | csymbr)+
apply (rule ccorres_symb_exec_r)
apply (rule_tac xf'="mdbNode_'" in ccorres_abstract, ceqv)
apply (rename_tac "cmdbNode")
apply (rule_tac P="cmdbnode_relation (cteMDBNode newCTE) cmdbNode"
in ccorres_gen_asm2)
apply csymbr+
-- "--- instruction : mdbNode \<leftarrow> return (cteMDBNode rv)"
apply ctac
-- "*** Main goal ***"
-- "--- instruction: CALL on C side"
apply csymbr
-- "--- instruction: prev \<leftarrow> return (mdbPrev mdbNode); ---"
-- "--- next \<leftarrow> return (mdbNext mdbNode); ---"
apply (simp del: Collect_const) -- "to simplify the returns and replace them in the rest\<dots>"
-- "--- instruction: assignements on C side"
apply csymbr
apply (erule_tac t = ret__unsigned in ssubst)
apply csymbr
apply (erule_tac t = ret__unsigned in ssubst)
apply csymbr
-- "--- instruction: updateMDB (mdbPrev rva) (mdbNext_update \<dots>) but with Ptr\<dots>\<noteq> NULL on C side"
apply (simp only:Ptr_not_null_pointer_not_zero) --"replaces Ptr p \<noteq> NULL with p\<noteq>0"
@ -2439,7 +2579,7 @@ lemma emptySlot_ccorres:
-- "here ctac alone does not apply because the subgoal generated
by the rule are not solvable by simp"
-- "so we have to use (no_simp) (or apply (rule ccorres_split_nothrow))"
apply (simp add: cmdbnode_relation_def)
apply (simp add: cmdbnode_relation_def)
apply assumption
-- "*** Main goal ***"
-- "--- instruction: updateMDB (mdbNext rva)
@ -2476,61 +2616,32 @@ lemma emptySlot_ccorres:
-- "C pre/post for the two nested updates "
apply (simp add: Collect_const_mem ccap_relation_NullCap_iff)
-- "Haskell pre/post for (updateMDB (mdbPrev rva) (mdbNext_update (\<lambda>_. mdbNext rva)))"
apply wp
apply (simp, wp)
-- "C pre/post for (updateMDB (mdbPrev rva) (mdbNext_update (\<lambda>_. mdbNext rva)))"
apply simp+
-- "Haskell pre/post for mdbNode \<leftarrow> return (cteMDBNode rv)"
apply wp
-- "C pre/post for mdbNode \<leftarrow> return (cteMDBNode rv)"
apply vcg
-- "*************************************************************"
-- "*** generalised precondition for ccorres_cond application ***"
-- "*************************************************************"
-- "from here, really big goals"
apply (clarsimp simp: typ_heap_simps Collect_const_mem split del: split_if)
-- "instantiating the Haskell precondition that has been generalised"
apply (subgoal_tac "ctes_of s slot = Some rv \<and> (cte_at' slot and valid_mdb' and pspace_aligned') s")
prefer 2
apply assumption
apply clarsimp
-- "instantiating the C precondition that has been generalised"
apply (subgoal_tac "s' \<in> UNIV")
prefer 2
apply assumption
-- "generating cslift"
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp: typ_heap_simps)
-- "generating the hypotheses regarding validity, c_guard and cslift for Prev and Next"
apply (intro conjI)
apply (rule_tac x="cte_C.cap_C cte'" in exI)
apply (drule (2) rf_sr_cte_relation)
apply (drule ccte_relation_ccap_relation, simp)
apply (frule (2) is_aligned_3_next)
apply (frule (2) is_aligned_3_prev)
apply vcg
apply (rule conseqPre, vcg)
apply clarsimp
prefer 2
apply (clarsimp, rule refl)
apply simp
apply (clarsimp simp: cte_wp_at_ctes_of)
done
apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift)
-- "final precondition proof"
apply (clarsimp simp: typ_heap_simps Collect_const_mem
cte_wp_at_ctes_of
split del: split_if)
apply (rule conjI)
-- "Haskell side"
apply (simp add: is_aligned_3_prev is_aligned_3_next)
-- "C side"
apply (clarsimp simp: map_comp_Some_iff typ_heap_simps)
apply (subst cap_get_tag_isCap)
apply (rule ccte_relation_ccap_relation)
apply (simp add: ccte_relation_def c_valid_cte_def
cl_valid_cte_def c_valid_cap_def)
apply simp
done
(************************************************************************)

29
proof/crefine/Detype_C.thy
View File

@ -1137,24 +1137,6 @@ lemma tcb_ptr_to_ctcb_ptr_comp:
apply (simp add: tcb_ptr_to_ctcb_ptr_def)
done
lemma ccorres_assume_pre:
assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C"
shows "ccorres r xf P P' hs H C"
apply (clarsimp simp: ccorres_underlying_def)
apply (frule assms)
apply (simp add: ccorres_underlying_def)
apply blast
done
lemma ccorres_name_pre:
"(\<And>s. P s \<Longrightarrow> ccorresG rf_sr \<Gamma> r xf (\<lambda>s'. s' = s) P' hs H C) \<Longrightarrow> ccorresG rf_sr \<Gamma> r xf P P' hs H C"
apply (rule ccorres_assume_pre)
apply (rule ccorres_guard_imp)
apply fastforce
apply simp
apply simp
done
lemma tcb_ptr_to_ctcb_ptr_to_Ptr:
"tcb_ptr_to_ctcb_ptr ` {p..+b} = Ptr ` {p + ctcb_offset..+b}"
apply (simp add: tcb_ptr_to_ctcb_ptr_comp image_comp [symmetric])
@ -1631,6 +1613,14 @@ lemma cvariable_array_map_relation_detype:
apply (simp add: h_t_array_valid_typ_region_bytes)
done
lemma zero_ranges_are_zero_typ_region_bytes:
"zero_ranges_are_zero rs hrs
\<Longrightarrow> zero_ranges_are_zero rs (hrs_htd_update (typ_region_bytes ptr bits) hrs)"
apply (clarsimp simp: zero_ranges_are_zero_def)
apply (drule(1) bspec)
apply (clarsimp simp: region_is_bytes'_def typ_region_bytes_def hrs_htd_update)
done
lemma deleteObjects_ccorres':
notes if_cong[cong]
shows
@ -2091,7 +2081,8 @@ proof -
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
psu_restrict cpspace_relation_def
carch_state_relation_def cmachine_state_relation_def
hrs_htd_update htd_safe_typ_region_bytes)
hrs_htd_update htd_safe_typ_region_bytes
zero_ranges_are_zero_typ_region_bytes)
qed
abbreviation (input)

164
proof/crefine/Fastpath_C.thy
View File

@ -1196,9 +1196,10 @@ lemma thread_state_ptr_set_tsType_np_spec:
tsType_CL (thread_state_lift thread_state) = tsType_' s \<and>
tcbQueued_CL (thread_state_lift thread_state)
= tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift s (ptr s))))) \<and>
cslift t = cslift s(ptr s \<mapsto> the (cslift s (ptr s))\<lparr>tcbState_C := thread_state\<rparr>))
\<and> types_proofs.cslift_all_but_tcb_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
(the (cslift s (ptr s))\<lparr>tcbState_C := thread_state\<rparr>))
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: ptr_def)
apply (clarsimp simp: h_t_valid_clift_Some_iff)
@ -1224,9 +1225,10 @@ lemma thread_state_ptr_mset_blockingObject_tsType_spec:
\<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' s
\<and> tcbQueued_CL (thread_state_lift thread_state)
= tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift s (ptr s)))))
\<and> cslift t = cslift s(ptr s \<mapsto> the (cslift s (ptr s))\<lparr>tcbState_C := thread_state\<rparr>))
\<and> types_proofs.cslift_all_but_tcb_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
(the (cslift s (ptr s))\<lparr>tcbState_C := thread_state\<rparr>))
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: ptr_def)
apply (frule h_t_valid_c_guard_cparent, simp+)
@ -1253,9 +1255,10 @@ lemma mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_spec:
mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))
\<lparr> mdbNext_CL := mdbNext___unsigned_long_' s, mdbRevocable_CL := mdbRevocable___unsigned_long_' s,
mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' s \<rparr>
\<and> cslift t = cslift s(ptr s \<mapsto> the (cslift s (ptr s)) \<lparr> cteMDBNode_C := mdb_node \<rparr>))
\<and> types_proofs.cslift_all_but_cte_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
(the (cslift s (ptr s)) \<lparr> cteMDBNode_C := mdb_node \<rparr>))
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: ptr_def)
apply (clarsimp simp: h_t_valid_clift_Some_iff)
@ -1280,9 +1283,10 @@ lemma mdb_node_ptr_set_mdbPrev_np_spec:
{t. (\<exists>mdb_node.
mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))
\<lparr> mdbPrev_CL := mdbPrev___unsigned_long_' s \<rparr>
\<and> cslift t = cslift s(ptr s \<mapsto> the (cslift s (ptr s)) \<lparr> cteMDBNode_C := mdb_node \<rparr>))
\<and> types_proofs.cslift_all_but_cte_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
(the (cslift s (ptr s)) \<lparr> cteMDBNode_C := mdb_node \<rparr>))
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: ptr_def)
apply (clarsimp simp: h_t_valid_clift_Some_iff)
@ -1305,9 +1309,10 @@ lemma cap_reply_cap_ptr_new_np_spec2:
{t. (\<exists>cap.
cap_lift cap = Some (Cap_reply_cap \<lparr> capReplyMaster_CL = capReplyMaster___unsigned_long_' s,
capTCBPtr_CL = capTCBPtr___unsigned_long_' s \<rparr>)
\<and> cslift t = cslift s(ptr s \<mapsto> the (cslift s (ptr s)) \<lparr> cte_C.cap_C := cap \<rparr>))
\<and> types_proofs.cslift_all_but_cte_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
(the (cslift s (ptr s)) \<lparr> cte_C.cap_C := cap \<rparr>))
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: ptr_def)
apply (clarsimp simp: h_t_valid_clift_Some_iff word_sle_def)
@ -1331,9 +1336,10 @@ lemma endpoint_ptr_mset_epQueue_tail_state_spec:
{t. (\<exists>endpoint.
endpoint_lift endpoint = endpoint_lift (the (cslift s (ep_ptr_' s)))
\<lparr> endpoint_CL.state_CL := state_' s, epQueue_tail_CL := epQueue_tail_' s \<rparr>
\<and> cslift t = cslift s(ep_ptr_' s \<mapsto> endpoint))
\<and> types_proofs.cslift_all_but_endpoint_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ep_ptr_' s)
endpoint)
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: h_t_valid_clift_Some_iff typ_heap_simps'
word_sle_def word_sless_def)
@ -1350,9 +1356,10 @@ lemma endpoint_ptr_set_epQueue_head_np_spec:
{t. (\<exists>endpoint.
endpoint_lift endpoint = endpoint_lift (the (cslift s (ep_ptr_' s)))
\<lparr> epQueue_head_CL := epQueue_head_' s \<rparr>
\<and> cslift t = cslift s(ep_ptr_' s \<mapsto> endpoint))
\<and> types_proofs.cslift_all_but_endpoint_C t s
\<and> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))}"
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ep_ptr_' s)
endpoint)
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: h_t_valid_clift_Some_iff typ_heap_simps'
word_sless_def word_sle_def)
@ -1675,19 +1682,22 @@ lemma fastpath_dequeue_ccorres:
typ_heap_simps' endpoint_state_defs)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
apply (rule conjI)
apply (clarsimp simp: cpspace_relation_def update_ep_map_tos)
apply (clarsimp simp: cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (erule(1) cpspace_relation_ep_update_ep2)
apply (simp add: cendpoint_relation_def endpoint_state_defs)
apply simp
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff update_ep_map_tos)
h_t_valid_clift_Some_iff update_ep_map_tos
typ_heap_simps')
apply (clarsimp simp: neq_Nil_conv cendpoint_relation_def Let_def
isRecvEP_endpoint_case tcb_queue_relation'_def
typ_heap_simps' endpoint_state_defs)
apply (clarsimp simp: is_aligned_weaken[OF is_aligned_tcb_ptr_to_ctcb_ptr]
tcb_at_not_NULL)
apply (drule(1) obj_at_cslift_tcb)+
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
typ_heap_simps' tcb_at_not_NULL[OF obj_at'_weakenE, OF _ TrueI])
apply (rule conjI)
apply (clarsimp simp: cpspace_relation_def update_ep_map_tos
update_tcb_map_tos typ_heap_simps')
@ -1978,21 +1988,21 @@ lemma ccorres_updateCap [corres]:
apply clarsimp
done
lemma setCTE_rf_sr:
"\<lbrakk> (\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte'';
cslift s' = ((cslift s)(cte_Ptr ptr \<mapsto> cte'));
t_hrs_' (globals s') = hrs_mem_update
(heap_update (cte_Ptr ptr) cte')
(t_hrs_' (globals s));
ccte_relation cte cte';
types_proofs.cslift_all_but_cte_C s' s;
hrs_htd (t_hrs_' (globals s')) = hrs_htd (t_hrs_' (globals s));
(globals s')\<lparr> t_hrs_' := undefined \<rparr>
= (globals s)\<lparr> t_hrs_' := undefined \<rparr> \<rbrakk>
\<Longrightarrow>
\<exists>x\<in>fst (setCTE ptr cte \<sigma>).
(snd x, s') \<in> rf_sr"
apply (rule fst_setCTE[OF ctes_of_cte_at], assumption)
apply (erule rev_bexI)
apply clarsimp
apply (frule(1) rf_sr_ctes_of_clift)
apply (subgoal_tac "\<exists>hrs. globals s' = globals s
\<lparr> t_hrs_' := hrs \<rparr>")
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
@ -2012,10 +2022,10 @@ lemma setCTE_rf_sr:
lemma getCTE_setCTE_rf_sr:
"\<lbrakk> (\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte;
cslift s' = ((cslift s)(cte_Ptr ptr \<mapsto> cte'));
t_hrs_' (globals s') = hrs_mem_update
(heap_update (cte_Ptr ptr) cte')
(t_hrs_' (globals s));
ccte_relation (f cte) cte';
types_proofs.cslift_all_but_cte_C s' s;
hrs_htd (t_hrs_' (globals s')) = hrs_htd (t_hrs_' (globals s));
(globals s')\<lparr> t_hrs_' := undefined \<rparr>
= (globals s)\<lparr> t_hrs_' := undefined \<rparr> \<rbrakk>
@ -2310,7 +2320,6 @@ lemma fastpath_call_ccorres:
done
show ?thesis
using [[goals_limit = 3]]
apply (cinit lift: cptr_' msgInfo_')
apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
unifyFailure_catch_If catch_liftE
@ -2568,10 +2577,10 @@ lemma fastpath_call_ccorres:
apply (simp add: ctcb_relation_def cthread_state_relation_def)
apply simp
apply (rule conjI, erule cready_queues_relation_not_queue_ptrs)
apply (rule ext, simp split: split_if)
apply (rule ext, simp split: split_if)
apply (rule ext, simp split: split_if add: typ_heap_simps')
apply (rule ext, simp split: split_if add: typ_heap_simps')
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff map_comp_update projectKO_opt_tcb
typ_heap_simps' map_comp_update projectKO_opt_tcb
cvariable_relation_upd_const ko_at_projectKO_opt)
apply ceqv
apply (rule ccorres_abstract_ksCurThread, ceqv)
@ -2679,7 +2688,7 @@ lemma fastpath_call_ccorres:
apply (rule ext, simp split: split_if)
apply (rule ext, simp split: split_if)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff map_comp_update projectKO_opt_tcb
typ_heap_simps' map_comp_update projectKO_opt_tcb
cvariable_relation_upd_const ko_at_projectKO_opt)
apply ceqv
apply (simp only: bind_assoc[symmetric])
@ -3076,7 +3085,7 @@ lemma fastpath_reply_recv_ccorres:
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply simp
apply (rule ccorres_split_throws)
apply (rule ccorres_split_throws)
apply (fold dc_def)[1]
apply (rule ccorres_call_hSkip)
apply (rule slowpath_ccorres)
@ -3324,7 +3333,7 @@ lemma fastpath_reply_recv_ccorres:
apply (rule ext, simp split: split_if)
apply (rule ext, simp split: split_if)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff map_comp_update projectKO_opt_tcb
typ_heap_simps' map_comp_update projectKO_opt_tcb
cvariable_relation_upd_const ko_at_projectKO_opt)
apply ceqv
apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2)
@ -3377,7 +3386,8 @@ lemma fastpath_reply_recv_ccorres:
apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+)
apply (clarsimp simp: typ_heap_simps' split_def tcbCallerSlot_def
tcb_cnode_index_defs tcb_ptr_to_ctcb_ptr_mask
cte_level_bits_def size_of_def)
cte_level_bits_def size_of_def
packed_heap_update_collapse_hrs)
apply (rule setCTE_rf_sr, simp_all add: typ_heap_simps')[1]
apply (clarsimp simp: ccte_relation_eq_ccap_relation makeObject_cte
mdb_node_to_H_def nullMDBNode_def
@ -3402,7 +3412,7 @@ lemma fastpath_reply_recv_ccorres:
apply (rule ext, simp split: split_if)
apply (rule ext, simp split: split_if)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff map_comp_update projectKO_opt_tcb
typ_heap_simps' map_comp_update projectKO_opt_tcb
cvariable_relation_upd_const ko_at_projectKO_opt)
apply ceqv
apply (simp only: bind_assoc[symmetric])
@ -5101,11 +5111,24 @@ lemma updateMDB_isolatable:
(wp | simp)+)
done
lemma clearUntypedFreeIndex_isolatable:
"thread_actions_isolatable idx (clearUntypedFreeIndex slot)"
apply (simp add: clearUntypedFreeIndex_def getSlotCap_def)
apply (rule thread_actions_isolatable_bind)
apply (rule getCTE_isolatable)
apply (simp split: capability.split, safe intro!: thread_actions_isolatable_return)
apply (simp add: updateTrackedFreeIndex_def getSlotCap_def)
apply (intro thread_actions_isolatable_bind getCTE_isolatable
modify_isolatable)
apply (wp | simp)+
done
lemma emptySlot_isolatable:
"thread_actions_isolatable idx (emptySlot slot None)"
apply (simp add: emptySlot_def updateCap_def
apply (simp add: emptySlot_def updateCap_def case_Null_If
cong: if_cong)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
clearUntypedFreeIndex_isolatable
thread_actions_isolatable_if
getCTE_isolatable setCTE_isolatable
thread_actions_isolatable_return
@ -5825,6 +5848,36 @@ lemma setEndpoint_updateCap_pivot[unfolded K_bind_def]:
setEndpoint_getCTE_pivot
setEndpoint_setCTE_pivot)
lemma modify_setEndpoint_pivot[unfolded K_bind_def]:
"\<lbrakk> \<And>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s) \<rbrakk>
\<Longrightarrow> (do modify sf; setEndpoint p val; f od) =
(do setEndpoint p val; modify sf; f od)"
apply (subgoal_tac "\<forall>s. ep_at' p (sf s) = ep_at' p s")
apply (simp add: setEndpoint_def setObject_modify_assert
bind_assoc fun_eq_iff
exec_gets exec_modify assert_def
split: split_if)
apply atomize
apply clarsimp
apply (drule_tac x="\<lambda>_. ksPSpace s" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac f="ksPSpace" in arg_cong)
apply simp
apply (metis obj_at'_pspaceI)
done
lemma setEndpoint_clearUntypedFreeIndex_pivot[unfolded K_bind_def]:
"do setEndpoint p val; v <- clearUntypedFreeIndex slot; f od
= do v <- clearUntypedFreeIndex slot; setEndpoint p val; f od"
by (simp add: clearUntypedFreeIndex_def bind_assoc
getSlotCap_def
setEndpoint_getCTE_pivot
updateTrackedFreeIndex_def
modify_setEndpoint_pivot
split: capability.split
| rule bind_cong[OF refl] allI impI
bind_apply_cong[OF refl])+
lemma emptySlot_setEndpoint_pivot[unfolded K_bind_def]:
"(do emptySlot slot None; setEndpoint p val; f od) =
(do setEndpoint p val; emptySlot slot None; f od)"
@ -5833,6 +5886,8 @@ lemma emptySlot_setEndpoint_pivot[unfolded K_bind_def]:
setEndpoint_getCTE_pivot
setEndpoint_updateCap_pivot
setEndpoint_updateMDB_pivot
case_Null_If
setEndpoint_clearUntypedFreeIndex_pivot
split: split_if
| rule bind_apply_cong[OF refl])+
done
@ -5907,12 +5962,29 @@ lemma setCTE_updateCapMDB:
apply (auto simp: mask_out_sub_mask)
done
lemma clearUntypedFreeIndex_simple_rewrite:
"monadic_rewrite True False
(cte_wp_at' (Not o isUntypedCap o cteCap) slot)
(clearUntypedFreeIndex slot) (return ())"
apply (simp add: clearUntypedFreeIndex_def getSlotCap_def)
apply (rule monadic_rewrite_name_pre)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (rule monadic_rewrite_imp)
apply (rule_tac rv=cte in monadic_rewrite_symb_exec_l_known, wp)
apply (simp split: capability.split,
strengthen monadic_rewrite_refl, simp)
apply clarsimp
apply (wp getCTE_wp')
apply (clarsimp simp: cte_wp_at_ctes_of)
done
lemma emptySlot_replymaster_rewrite[OF refl]:
"mdbn = cteMDBNode cte \<Longrightarrow>
monadic_rewrite True False
((\<lambda>_. mdbNext mdbn = 0 \<and> mdbPrev mdbn \<noteq> 0)
and ((\<lambda>_. cteCap cte \<noteq> NullCap)
and (cte_wp_at' (op = cte) slot
and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot
and cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte))
(mdbPrev mdbn)
and (\<lambda>s. reply_masters_rvk_fb (ctes_of s))
@ -5926,8 +5998,12 @@ lemma emptySlot_replymaster_rewrite[OF refl]:
apply (rule monadic_rewrite_imp)
apply (rule_tac P="slot \<noteq> 0" in monadic_rewrite_gen_asm)
apply (clarsimp simp: emptySlot_def setCTE_updateCapMDB)
apply (rule monadic_rewrite_trans)
apply (rule monadic_rewrite_bind_head)
apply (rule clearUntypedFreeIndex_simple_rewrite)
apply simp
apply (rule_tac rv=cte in monadic_rewrite_symb_exec_l_known, wp empty_fail_getCTE)
apply (simp add: updateMDB_def Let_def bind_assoc makeObject_cte)
apply (simp add: updateMDB_def Let_def bind_assoc makeObject_cte case_Null_If)
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_bind)
apply (rule_tac P="mdbFirstBadged (cteMDBNode ctea) \<and> mdbRevocable (cteMDBNode ctea)"
@ -5938,7 +6014,7 @@ lemma emptySlot_replymaster_rewrite[OF refl]:
apply (rule monadic_rewrite_refl)
apply (wp getCTE_wp')
apply (clarsimp simp: cte_wp_at_ctes_of reply_masters_rvk_fb_def)
apply fastforce
apply (fastforce simp: isCap_simps)
done
(* FIXME: Move *)

29
proof/crefine/Finalise_C.thy
View File

@ -340,7 +340,7 @@ lemma cancelAllIPC_ccorres:
Let_def carch_state_relation_def carch_globals_def
cmachine_state_relation_def)
apply (clarsimp simp: cpspace_relation_def
update_ep_map_tos)
update_ep_map_tos typ_heap_simps')
apply (erule(2) cpspace_relation_ep_update_ep)
subgoal by (simp add: cendpoint_relation_def endpoint_state_defs)
subgoal by simp
@ -389,7 +389,7 @@ lemma cancelAllIPC_ccorres:
apply (clarsimp simp: rf_sr_def cstate_relation_def
Let_def carch_state_relation_def carch_globals_def
cmachine_state_relation_def)
apply (clarsimp simp: cpspace_relation_def
apply (clarsimp simp: cpspace_relation_def typ_heap_simps'
update_ep_map_tos)
apply (erule(2) cpspace_relation_ep_update_ep)
subgoal by (simp add: cendpoint_relation_def endpoint_state_defs)
@ -476,7 +476,7 @@ lemma cancelAllSignals_ccorres:
apply (clarsimp simp: rf_sr_def cstate_relation_def
Let_def carch_state_relation_def carch_globals_def
cmachine_state_relation_def)
apply (clarsimp simp: cpspace_relation_def
apply (clarsimp simp: cpspace_relation_def typ_heap_simps'
update_ntfn_map_tos)
apply (erule(2) cpspace_relation_ntfn_update_ntfn)
subgoal by (simp add: cnotification_relation_def notification_state_defs Let_def)
@ -668,7 +668,8 @@ lemma doUnbindNotification_ccorres:
apply (clarsimp simp: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
cpspace_relation_def update_ntfn_map_tos)
typ_heap_simps'
cpspace_relation_def update_ntfn_map_tos)
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -676,7 +677,7 @@ lemma doUnbindNotification_ccorres:
apply (clarsimp simp: cnotification_relation_def Let_def
mask_def [where n=2] NtfnState_Waiting_def)
apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4])
subgoal by (simp add: carch_state_relation_def)
subgoal by (simp add: carch_state_relation_def typ_heap_simps')
subgoal by (simp add: cmachine_state_relation_def)
subgoal by (simp add: h_t_valid_clift_Some_iff)
subgoal by (simp add: objBits_simps)
@ -690,7 +691,7 @@ lemma doUnbindNotification_ccorres:
apply vcg
apply simp
apply (erule(1) rf_sr_tcb_update_no_queue2)
apply (simp add: typ_heap_simps)+
apply (simp add: typ_heap_simps')+
apply (simp add: tcb_cte_cases_def)
apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
apply (simp add: invs'_def valid_state'_def)
@ -715,7 +716,8 @@ lemma doUnbindNotification_ccorres':
apply (clarsimp simp: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
cpspace_relation_def update_ntfn_map_tos)
typ_heap_simps'
cpspace_relation_def update_ntfn_map_tos)
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -725,7 +727,7 @@ lemma doUnbindNotification_ccorres':
apply (fold_subgoals (prefix))[2]
subgoal premises prems using prems
by (case_tac "ntfnObj ntfn", (simp add: option_to_ctcb_ptr_def)+)
subgoal by (simp add: carch_state_relation_def)
subgoal by (simp add: carch_state_relation_def typ_heap_simps')
subgoal by (simp add: cmachine_state_relation_def)
subgoal by (simp add: h_t_valid_clift_Some_iff)
subgoal by (simp add: objBits_simps)
@ -739,7 +741,7 @@ lemma doUnbindNotification_ccorres':
apply vcg
apply simp
apply (erule(1) rf_sr_tcb_update_no_queue2)
apply (simp add: typ_heap_simps)+
apply (simp add: typ_heap_simps')+
apply (simp add: tcb_cte_cases_def)
apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
apply (simp add: invs'_def valid_state'_def)
@ -1221,7 +1223,7 @@ lemma deleteASID_ccorres:
simp_all add: objBits_simps archObjSize_def pageBits_def)[1]
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps)
apply (rule conjI)
apply (clarsimp simp: cpspace_relation_def typ_heap_simps
apply (clarsimp simp: cpspace_relation_def typ_heap_simps'
update_asidpool_map_tos
update_asidpool_map_to_asidpools)
apply (rule cmap_relation_updI, simp_all)[1]
@ -1234,7 +1236,7 @@ lemma deleteASID_ccorres:
subgoal by (simp add: asid_low_bits_def)
subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
carch_globals_def update_asidpool_map_tos
typ_heap_simps)
typ_heap_simps')
apply (rule ccorres_pre_getCurThread)
apply (ctac add: setVMRoot_ccorres)
apply (simp add: cur_tcb'_def[symmetric])
@ -1746,8 +1748,9 @@ lemma cteDeleteOne_ccorres:
apply (simp add: dc_def[symmetric])
apply (ctac add: emptySlot_ccorres)
apply (simp add: pred_conj_def finaliseCapTrue_standin_simple_def)
apply (strengthen invs_mdb_strengthen')
apply (wp typ_at_lifts isFinalCapability_inv)
apply (strengthen invs_mdb_strengthen' invs_urz)
apply (wp typ_at_lifts isFinalCapability_inv
| strengthen invs_valid_objs')+
apply (clarsimp simp: from_bool_def true_def irq_opt_relation_def
invs_pspace_aligned' cte_wp_at_ctes_of)
apply (erule(1) cmap_relationE1 [OF cmap_relation_cte])

1306
proof/crefine/Invoke_C.thy
View File

File diff suppressed because it is too large Load Diff

188
proof/crefine/IpcCancel_C.thy
View File

@ -115,6 +115,17 @@ lemma ntfn_ptr_get_queue_spec:
declare td_names_word8[simp]
abbreviation
"cslift_all_but_tcb_C s t \<equiv> (cslift s :: cte_C typ_heap) = cslift t
\<and> (cslift s :: endpoint_C typ_heap) = cslift t
\<and> (cslift s :: notification_C typ_heap) = cslift t
\<and> (cslift s :: asid_pool_C typ_heap) = cslift t
\<and> (cslift s :: pte_C typ_heap) = cslift t
\<and> (cslift s :: pde_C typ_heap) = cslift t
\<and> (cslift s :: user_data_C typ_heap) = cslift t
\<and> (cslift s :: user_data_device_C typ_heap) = cslift t
"
lemma tcbEPDequeue_spec:
"\<forall>s queue. \<Gamma> \<turnstile> \<lbrace>s. \<exists>t. (t, s) \<in> rf_sr
\<and> (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<and> distinct queue
@ -136,7 +147,10 @@ lemma tcbEPDequeue_spec:
(cslift s |` (- tcb_ptr_to_ctcb_ptr ` set queue))
\<and> option_map tcb_null_ep_ptrs \<circ> (cslift t) =
option_map tcb_null_ep_ptrs \<circ> (cslift s))
\<and> cslift_all_but_tcb_C t s \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
\<and> cslift_all_but_tcb_C t s
\<and> (\<forall>rs. zero_ranges_are_zero rs (\<^bsup>t\<^esup>t_hrs)
= zero_ranges_are_zero rs (\<^bsup>s\<^esup>t_hrs))
\<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
apply (intro allI)
apply (rule conseqPre)
apply vcg
@ -177,11 +191,11 @@ lemma ntfn_ptr_set_queue_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>ntfnPtr\<rbrace> Call ntfn_ptr_set_queue_'proc
{t. (\<exists>ntfn'. notification_lift ntfn' =
(notification_lift (the (cslift s (\<^bsup>s\<^esup>ntfnPtr))))\<lparr> ntfnQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4,
ntfnQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4 \<rparr> \<and>
(cslift t :: notification_C typ_heap) = (cslift s)(\<^bsup>s\<^esup>ntfnPtr \<mapsto> ntfn'))
\<and> cslift_all_but_notification_C t s \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
apply vcg
apply (auto simp: split_def h_t_valid_clift_Some_iff)
ntfnQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>ntfn_queue) && ~~ mask 4 \<rparr>
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>ntfnPtr) ntfn')
(t_hrs_' (globals s)))}"
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: packed_heap_update_collapse_hrs typ_heap_simps')
done
lemma cancelSignal_ccorres_helper:
@ -230,7 +244,9 @@ lemma cancelSignal_ccorres_helper:
apply simp
apply (simp add: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def cpspace_relation_def update_ntfn_map_tos)
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -249,13 +265,15 @@ lemma cancelSignal_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def carch_globals_def)
apply (simp add: carch_state_relation_def carch_globals_def
typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
apply assumption
-- "non empty case"
apply (frule tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel])
apply (rule ballI, erule bspec)
@ -264,7 +282,9 @@ lemma cancelSignal_ccorres_helper:
apply (simp add: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (frule (1) st_tcb_at_h_t_valid)
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def cpspace_relation_def update_ntfn_map_tos)
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -291,7 +311,8 @@ lemma cancelSignal_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def carch_globals_def)
apply (simp add: carch_state_relation_def carch_globals_def
typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -299,6 +320,8 @@ lemma cancelSignal_ccorres_helper:
apply assumption
done
lemmas rf_sr_tcb_update_no_queue_gen
= rf_sr_tcb_update_no_queue[where t="t''\<lparr> globals := gs \<lparr> t_hrs_' := th \<rparr>\<rparr>" for th, simplified]
lemma threadSet_tcbState_simple_corres:
"ccorres dc xfdc (tcb_at' thread)
@ -308,10 +331,10 @@ lemma threadSet_tcbState_simple_corres:
apply (rule threadSet_corres_lemma)
apply (rule thread_state_ptr_set_tsType_spec)
apply (rule thread_state_ptr_set_tsType_modifies)
apply clarsimp
apply (frule (1) obj_at_cslift_tcb)
apply clarsimp
apply (rule rf_sr_tcb_update_no_queue, assumption+, simp_all)
apply (frule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps')
apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all)
apply (rule ball_tcb_cte_casesI, simp_all)
apply (frule cmap_relation_tcb)
apply (frule (1) cmap_relation_ko_atD)
@ -321,7 +344,6 @@ lemma threadSet_tcbState_simple_corres:
apply (clarsimp simp: typ_heap_simps)
done
lemma ko_at_obj_congD':
"\<lbrakk>ko_at' k p s; ko_at' k' p s\<rbrakk> \<Longrightarrow> k = k'"
apply (erule obj_atE')+
@ -643,7 +665,7 @@ lemma threadSet_queued_ccorres [corres]:
apply clarsimp
apply (frule (1) obj_at_cslift_tcb)
apply clarsimp
apply (rule rf_sr_tcb_update_no_queue, assumption+, simp_all)
apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all)
apply (rule ball_tcb_cte_casesI, simp_all)
apply (simp add: ctcb_relation_def cthread_state_relation_def)
apply (case_tac "tcbState ko", simp_all add: Word_Lemmas.from_bool_mask_simp)[1]
@ -699,6 +721,8 @@ lemma state_relation_queue_update_helper':
option_map tcb_null_sched_ptrs \<circ> cslift t
= option_map tcb_null_sched_ptrs \<circ> cslift s';
cslift_all_but_tcb_C t s';
zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s')))
= zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s'));
hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
prio' = cready_queues_index_to_C qdom prio;
\<forall>x \<in> S. obj_at' (inQ qdom prio) x s
@ -770,6 +794,8 @@ lemma state_relation_queue_update_helper:
option_map tcb_null_sched_ptrs \<circ> cslift t
= option_map tcb_null_sched_ptrs \<circ> cslift s';
cslift_all_but_tcb_C t s';
zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s')))
= zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s'));
hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
prio' = cready_queues_index_to_C qdom prio;
\<forall>x \<in> S. obj_at' (inQ qdom prio) x s
@ -781,7 +807,7 @@ lemma state_relation_queue_update_helper:
\<Longrightarrow> (s \<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr"
apply (subgoal_tac "\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
\<and> distinct(ksReadyQueues s (d, p))")
apply (erule(12) state_relation_queue_update_helper')
apply (erule(5) state_relation_queue_update_helper', simp_all)
apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def)
apply (drule_tac x=d in spec)
apply (drule_tac x=p in spec)
@ -1160,6 +1186,7 @@ proof -
simp_all add: valid_queues_valid_q)[1]
apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
apply (erule(1) state_relation_queue_update_helper[where S="{t}"],
(simp | rule globals.equality)+,
simp_all add: cready_queues_index_to_C_def2 numPriorities_def
t_hrs_ksReadyQueues_upd_absorb upd_unless_null_def
typ_heap_simps)[1]
@ -1202,6 +1229,7 @@ proof -
apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D])
apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper,
(simp | rule globals.equality)+,
simp_all add: typ_heap_simps if_Some_helper numPriorities_def
cready_queues_index_to_C_def2 upd_unless_null_def
cong: if_cong split del: split_if
@ -1559,7 +1587,8 @@ proof -
apply (clarsimp simp: h_t_valid_c_guard [OF h_t_valid_field, OF h_t_valid_clift]
h_t_valid_field[OF h_t_valid_clift] h_t_valid_clift)
apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
in state_relation_queue_update_helper', assumption,
in state_relation_queue_update_helper',
(simp | rule globals.equality)+,
simp_all add: clift_field_update if_Some_helper numPriorities_def
cready_queues_index_to_C_def2 typ_heap_simps
maxDom_to_H maxPrio_to_H
@ -1567,14 +1596,14 @@ proof -
apply (fold_subgoals (prefix))[2]
subgoal premises prems using prems by (fastforce simp: tcb_null_sched_ptrs_def)+
apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
in state_relation_queue_update_helper', assumption,
in state_relation_queue_update_helper',
(simp | rule globals.equality)+,
simp_all add: clift_field_update if_Some_helper numPriorities_def
cready_queues_index_to_C_def2
maxDom_to_H maxPrio_to_H
cong: if_cong split del: split_if)[1]
subgoal by (fastforce simp: typ_heap_simps)
subgoal by (fastforce simp: tcb_null_sched_ptrs_def)
subgoal by (simp add: typ_heap_simps)
cong: if_cong split del: split_if,
simp_all add: typ_heap_simps')[1]
subgoal by (fastforce simp: tcb_null_sched_ptrs_def)
subgoal by fastforce
apply clarsimp
@ -1587,7 +1616,8 @@ proof -
elim: obj_at'_weaken)+
apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
in state_relation_queue_update_helper', assumption,
in state_relation_queue_update_helper',
(simp | rule globals.equality)+,
simp_all add: clift_field_update if_Some_helper numPriorities_def
cready_queues_index_to_C_def2
maxDom_to_H maxPrio_to_H
@ -1656,14 +1686,16 @@ proof -
apply (clarsimp simp: typ_heap_simps)
apply (rule conjI; clarsimp simp: typ_heap_simps)
apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
in state_relation_queue_update_helper', assumption,
in state_relation_queue_update_helper',
(simp | rule globals.equality)+,
simp_all add: clift_field_update if_Some_helper numPriorities_def
cready_queues_index_to_C_def2
maxDom_to_H maxPrio_to_H
cong: if_cong split del: split_if)[1]
apply (fastforce simp: typ_heap_simps tcb_null_sched_ptrs_def)+
apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
in state_relation_queue_update_helper', assumption,
in state_relation_queue_update_helper',
(simp | rule globals.equality)+,
simp_all add: clift_field_update if_Some_helper numPriorities_def
cready_queues_index_to_C_def2
maxDom_to_H maxPrio_to_H
@ -1683,12 +1715,13 @@ proof -
apply (fold_subgoals (prefix))[2]
subgoal premises prems using prems by (fastforce elim: obj_at'_weaken)+
apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))"
in state_relation_queue_update_helper', assumption,
in state_relation_queue_update_helper',
(simp | rule globals.equality)+,
simp_all add: clift_field_update if_Some_helper numPriorities_def
cready_queues_index_to_C_def2 typ_heap_simps
maxDom_to_H maxPrio_to_H
cong: if_cong split del: split_if)[1]
apply (fold_subgoals (prefix))[3]
apply (fold_subgoals (prefix))[2]
subgoal premises prems using prems
by (fastforce simp: typ_heap_simps tcb_null_sched_ptrs_def)+
apply (simp add: guard_is_UNIV_def)
@ -1857,6 +1890,7 @@ proof -
apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption)
apply (fastforce intro: cbitmap_L1_relation_bit_set cbitmap_L2_relation_bit_set)+
apply (erule(1) state_relation_queue_update_helper[where S="{t}"],
(simp | rule globals.equality)+,
simp_all add: cready_queues_index_to_C_def2 numPriorities_def
t_hrs_ksReadyQueues_upd_absorb upd_unless_null_def
typ_heap_simps)[1]
@ -1897,6 +1931,7 @@ proof -
apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D])
apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper,
(simp | rule globals.equality)+,
simp_all add: typ_heap_simps if_Some_helper numPriorities_def
cready_queues_index_to_C_def2 upd_unless_null_def
cong: if_cong split del: split_if
@ -2487,11 +2522,12 @@ lemma ep_ptr_set_queue_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> Call ep_ptr_set_queue_'proc
{t. (\<exists>ep'. endpoint_lift ep' =
(endpoint_lift (the (cslift s (\<^bsup>s\<^esup>epptr))))\<lparr> epQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>queue) && ~~ mask 4,
epQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>queue) && ~~ mask 4 \<rparr> \<and>
(cslift t :: endpoint_C typ_heap) = (cslift s)(\<^bsup>s\<^esup>epptr \<mapsto> ep'))
\<and> cslift_all_but_endpoint_C t s \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
epQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>queue) && ~~ mask 4 \<rparr>
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>epptr) ep')
(t_hrs_' (globals s)))}"
apply vcg
apply (auto simp: split_def h_t_valid_clift_Some_iff)
apply (auto simp: split_def h_t_valid_clift_Some_iff
typ_heap_simps packed_heap_update_collapse_hrs)
done
lemma valid_ep_blockedD:
@ -2724,7 +2760,8 @@ lemma cancelIPC_ccorres_helper:
subgoal by simp
apply (simp add: setEndpoint_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def cpspace_relation_def update_ep_map_tos)
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ep_map_tos typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -2744,7 +2781,8 @@ lemma cancelIPC_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
subgoal by (clarsimp simp: comp_def)
subgoal by (simp add: carch_state_relation_def carch_globals_def)
subgoal by (simp add: carch_state_relation_def carch_globals_def
typ_heap_simps')
subgoal by (simp add: cmachine_state_relation_def)
subgoal by (simp add: h_t_valid_clift_Some_iff)
subgoal by (simp add: objBits_simps)
@ -2759,7 +2797,8 @@ lemma cancelIPC_ccorres_helper:
apply (simp add: setEndpoint_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (frule (1) st_tcb_at_h_t_valid)
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def cpspace_relation_def update_ep_map_tos)
apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ep_map_tos typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -2786,7 +2825,8 @@ lemma cancelIPC_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
subgoal by (clarsimp simp: comp_def)
subgoal by (simp add: carch_state_relation_def carch_globals_def)
subgoal by (simp add: carch_state_relation_def carch_globals_def
typ_heap_simps')
subgoal by (simp add: cmachine_state_relation_def)
subgoal by (simp add: h_t_valid_clift_Some_iff)
subgoal by (simp add: objBits_simps)
@ -2813,6 +2853,8 @@ lemma getThreadState_ccorres_foo:
apply (clarsimp simp: ctcb_relation_def obj_at'_def)
done
(*
thm cancelIPC_body_def
lemma cancelIPC_ccorres_reply_helper:
assumes cteDeleteOne_ccorres:
"\<And>w slot. ccorres dc xfdc
@ -2833,7 +2875,10 @@ lemma cancelIPC_ccorres_reply_helper:
cteDeleteOne callerCap
od)
od)
(CALL fault_null_fault_ptr_new(Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbFault_C'']));;
(\<acute>ret__struct_fault_C :== CALL fault_null_fault_new();;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s}
(Basic (\<lambda>s. s \<lparr> (\<acute>t_hrs :== (hrs_mem_update (heap_update
(Ptr &(\<acute>tptr\<rightarrow>[''tcbFault_C''])) \<acute>ret__struct_fault_C)));;
(Guard MemorySafety
\<lbrace>ptr_add_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr thread) && 0xFFFFFE00))
(sint Kernel_C.tcbReply) False (hrs_htd \<acute>t_hrs)\<rbrace>
@ -2900,6 +2945,7 @@ lemma cancelIPC_ccorres_reply_helper:
Kernel_C.tcbReply_def mask_def tcbCNodeEntries_def)
apply (fastforce simp: pred_tcb_at' inQ_def tcb_aligned'[OF pred_tcb_at'])
done
*)
lemma ep_blocked_in_queueD_recv:
"\<lbrakk>st_tcb_at' (op = (Structures_H.thread_state.BlockedOnReceive x)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep'"
@ -2971,10 +3017,60 @@ lemma cancelIPC_ccorres1:
apply csymbr
apply csymbr
apply (unfold comp_def)[1]
apply (rule ccorres_Guard ccorres_Guard_Seq)+
apply (clarsimp simp del: dc_simp simp: of_int_sint)
apply ccorres_remove_UNIV_guard
apply (rule cancelIPC_ccorres_reply_helper [OF cteDeleteOne_ccorres])
apply csymbr
apply (rule ccorres_move_c_guard_tcb)+
apply (rule ccorres_split_nothrow_novcg)
apply (rule_tac P=\<top> in threadSet_ccorres_lemma2)
apply vcg
apply (clarsimp simp: typ_heap_simps')
apply (erule(1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps')+)[1]
apply (rule ball_tcb_cte_casesI, simp_all)[1]
apply (clarsimp simp: ctcb_relation_def fault_lift_null_fault
cfault_rel_def cthread_state_relation_def)
apply (case_tac "tcbState tcb", simp_all add: is_cap_fault_def)[1]
apply ceqv
apply ccorres_remove_UNIV_guard
apply (rule ccorres_move_array_assertion_tcb_ctes)
apply (rule_tac P="tcb_at' thread" in ccorres_cross_over_guard)
apply (simp add: getThreadReplySlot_def)
apply ctac
apply (simp only: liftM_def bind_assoc return_bind del: Collect_const)
apply (rule ccorres_pre_getCTE)
apply (rename_tac slot slot' cte)
apply (rule ccorres_move_c_guard_cte)
apply (rule_tac xf'=ret__unsigned_' and val="mdbNext (cteMDBNode cte)"
and R="cte_wp_at' (op = cte) slot and invs'"
in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
apply vcg
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
apply (clarsimp simp: typ_heap_simps)
apply (clarsimp simp: ccte_relation_def map_option_Some_eq2)
apply ceqv
apply csymbr
apply (rule ccorres_Cond_rhs)
apply (simp add: nullPointer_def when_def)
apply (rule ccorres_symb_exec_l[OF _ _ _ empty_fail_stateAssert])
apply (simp only: dc_def[symmetric])
apply (rule ccorres_symb_exec_r)
apply (ctac add: cteDeleteOne_ccorres[where w1="scast cap_reply_cap"])
apply vcg
apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def
gs_set_assn_Delete_cstate_relation[unfolded o_def])
apply (wp | simp)+
apply (simp add: when_def nullPointer_def dc_def[symmetric])
apply (rule ccorres_return_Skip)
apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
ghost_assertion_data_set_def cap_tag_defs)
apply (simp add: locateSlot_conv, wp)
apply vcg
apply (rule_tac Q="\<lambda>rv. tcb_at' thread and invs'" in hoare_post_imp)
apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def
cap_get_tag_isCap ucast_id)
apply (wp threadSet_invs_trivial | simp)+
apply (clarsimp simp add: guard_is_UNIV_def tcbReplySlot_def
Kernel_C.tcbReply_def tcbCNodeEntries_def)
-- "BlockedOnNotification"
apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong)
apply (rule ccorres_symb_exec_r)
@ -3046,11 +3142,15 @@ lemma cancelIPC_ccorres1:
cthread_state_relation_def sch_act_wf_weak valid_ep'_def
dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits endpoint.splits)
apply (rule conjI)
apply (clarsimp simp: isBlockedOnReply_def pred_tcb_at'_def obj_at'_def)
apply (rule conjI, clarsimp)
apply (clarsimp simp: inQ_def)
apply (rule conjI)
apply clarsimp
apply clarsimp
apply (rule conjI)
subgoal by (auto simp: pred_tcb_at'_def isBlockedOnReceive_def isBlockedOnSend_def obj_at'_def projectKOs split: thread_state.splits)[1]
subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
isTS_defs cte_wp_at_ctes_of
cthread_state_relation_def sch_act_wf_weak valid_ep'_def
dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits)
apply clarsimp
apply (rule conjI)
subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def
@ -3066,7 +3166,7 @@ lemma cancelIPC_ccorres1:
dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits endpoint.splits)[1]
apply (auto simp: isTS_defs cthread_state_relation_def typ_heap_simps weak_sch_act_wf_def)
apply (case_tac ts,
auto simp: isTS_defs cthread_state_relation_def typ_heap_simps)
auto simp: isTS_defs cthread_state_relation_def typ_heap_simps)
done
end

247
proof/crefine/Ipc_C.thy
View File

@ -3532,6 +3532,7 @@ lemma handleFaultReply_ccorres [corres]:
message_info_to_H_def
split: split_if)
apply unat_arith
apply clarsimp
apply (vcg spec=TrueI)
apply clarsimp
apply wp
@ -3616,6 +3617,7 @@ lemma handleFaultReply_ccorres [corres]:
min_def message_info_to_H_def word_of_nat_less
split: split_if)
apply unat_arith
apply clarsimp
apply (vcg spec=TrueI)
apply clarsimp
apply wp
@ -3728,27 +3730,6 @@ lemma handleFaultReply_ccorres [corres]:
apply (clarsimp simp: obj_at'_def n_msgRegisters_def)
done
lemma fault_null_fault_ptr_new_ccorres [corres]:
"ccorres dc xfdc (tcb_at' receiver) UNIV hs
(threadSet (tcbFault_update empty) receiver)
(CALL fault_null_fault_ptr_new(Ptr
&(tcb_ptr_to_ctcb_ptr receiver\<rightarrow>[''tcbFault_C''])))"
apply (rule ccorres_from_vcg)
apply (rule allI)
apply (rule conseqPre, vcg)
apply clarsimp
apply (frule(1) obj_at_cslift_tcb)
apply (rule conjI)
apply (clarsimp simp: typ_heap_simps)
apply clarsimp
apply (rule rev_bexI [OF threadSet_eq], assumption)
apply clarsimp
apply (erule(2) rf_sr_tcb_update_no_queue, simp_all add: tcb_cte_cases_def)
apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def
fault_lift_def cfault_rel_def)
apply (case_tac "tcbState ko", simp_all add: is_cap_fault_def)
done
(* FIXME: move *)
lemma cancelAllIPC_sch_act_wf:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
@ -3795,58 +3776,20 @@ lemma setCTE_tcbFault:
apply (rule setObject_cte_obj_at_tcb', simp_all)
done
(* FIXME: move *)
lemma emptySlot_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
emptySlot slot irq
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: emptySlot_def)
apply (wp setCTE_tcbFault getCTE_wp' hoare_drop_imps
| wpc
| simp add: updateMDB_def updateCap_def Let_def
| rule conjI impI)+
done
crunch tcbFault: emptySlot, tcbSchedEnqueue, rescheduleRequired
"obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
(wp: threadSet_obj_at'_strongish crunch_wps
simp: crunch_simps unless_def)
(* FIXME: move *)
lemmas threadSet_obj_at' = threadSet_obj_at'_strongish
(* FIXME: move *)
lemma tcbSchedEnqueue_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
tcbSchedEnqueue t'
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: tcbSchedEnqueue_def unless_when)
apply (wp threadSet_obj_at' hoare_drop_imps threadGet_wp
|simp split: split_if)+
done
lemma rescheduleRequired_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
rescheduleRequired
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: rescheduleRequired_def)
apply (wp tcbSchedEnqueue_tcbFault | wpc)+
apply simp
done
crunch tcbFault: setThreadState, cancelAllIPC, cancelAllSignals
"obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
(wp: threadSet_obj_at'_strongish crunch_wps)
(* FIXME: move *)
lemma sts_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
setThreadState st t'
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: setThreadState_def)
apply (wp threadSet_obj_at' rescheduleRequired_tcbFault | simp)+
done
(* FIXME: move *)
lemma setEndpoint_tcb:
"\<lbrace>obj_at' (\<lambda>tcb::tcb. P tcb) t\<rbrace>
setEndpoint ep e
\<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
apply (simp add: setEndpoint_def)
apply (rule obj_at_setObject2)
apply (clarsimp simp: updateObject_default_def in_monad)
done
lemmas setEndpoint_tcb = KHeap_R.setEndpoint_obj_at'_tcb
(* FIXME: move *)
lemma setNotification_tcb:
@ -3858,30 +3801,6 @@ lemma setNotification_tcb:
apply (clarsimp simp: updateObject_default_def in_monad)
done
(* FIXME: move *)
lemma cancelAllIPC_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
cancelAllIPC ep
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: cancelAllIPC_def)
apply (rule order_refl |
wp mapM_x_wp tcbSchedEnqueue_tcbFault sts_tcbFault
setEndpoint_tcb getEndpoint_wp rescheduleRequired_tcbFault |
wpc | simp)+
done
(* FIXME: move *)
lemma cancelAllSignals_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
cancelAllSignals ep
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: cancelAllSignals_def)
apply (rule order_refl |
wp mapM_x_wp tcbSchedEnqueue_tcbFault sts_tcbFault
setNotification_tcb getNotification_wp rescheduleRequired_tcbFault |
wpc | simp)+
done
lemma sbn_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
setBoundNotification st t'
@ -4061,9 +3980,19 @@ proof -
where xf'=restart_'])
apply simp_all[3]
apply ceqv
apply (rule ccorres_move_c_guard_tcb)
apply csymbr
apply (rule ccorres_split_nothrow_novcg)
apply (rule fault_null_fault_ptr_new_ccorres)
apply (rule threadSet_ccorres_lemma2[where P=\<top>])
apply vcg
apply (clarsimp simp: typ_heap_simps')
apply (erule(1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps')+, simp_all?)[1]
apply (rule ball_tcb_cte_casesI, simp+)
apply (clarsimp simp: ctcb_relation_def
fault_lift_null_fault
cfault_rel_def is_cap_fault_def
cthread_state_relation_def)
apply (case_tac "tcbState tcb", simp_all add: is_cap_fault_def)[1]
apply ceqv
apply (rule_tac R=\<top> in ccorres_cond2)
apply (clarsimp simp: to_bool_def Collect_const_mem)
@ -4256,7 +4185,8 @@ lemma sendIPC_dequeue_ccorres_helper:
apply (rule conjI)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -4276,7 +4206,7 @@ lemma sendIPC_dequeue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -4295,7 +4225,8 @@ lemma sendIPC_dequeue_ccorres_helper:
apply (rule bexI [OF _ setObject_eq])
apply (frule(1) st_tcb_at_h_t_valid)
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -4323,7 +4254,7 @@ lemma sendIPC_dequeue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -4332,6 +4263,18 @@ lemma sendIPC_dequeue_ccorres_helper:
apply (clarsimp simp: cendpoint_relation_def Let_def tcb_queue_relation'_def)
done
lemma rf_sr_tcb_update_twice:
"h_t_valid (hrs_htd hrs) c_guard ptr
\<Longrightarrow> ((s, s'\<lparr>globals := globals s''\<lparr>t_hrs_' :=
hrs_mem_update (heap_update (ptr :: tcb_C ptr) v)
(hrs_mem_update (heap_update ptr v') hrs)\<rparr>\<rparr>) \<in> rf_sr)
= ((s, s'\<lparr>globals := globals s''\<lparr>t_hrs_' :=
hrs_mem_update (heap_update (ptr :: tcb_C ptr) v) hrs\<rparr>\<rparr>) \<in> rf_sr)"
by (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def typ_heap_simps'
carch_state_relation_def
cmachine_state_relation_def)
lemma sendIPC_block_ccorres_helper:
"ccorres dc xfdc (tcb_at' thread and valid_queues and valid_objs' and
sch_act_not thread and ep_at' epptr and
@ -4377,9 +4320,10 @@ lemma sendIPC_block_ccorres_helper:
apply clarsimp
apply (frule(1) tcb_at_h_t_valid)
apply (frule h_t_valid_c_guard)
apply (clarsimp simp: typ_heap_simps)
apply (erule(1) rf_sr_tcb_update_no_queue)
apply (simp add: typ_heap_simps')+
apply (clarsimp simp: typ_heap_simps'
rf_sr_tcb_update_twice)
apply (erule(1) rf_sr_tcb_update_no_queue_gen,
(simp add: typ_heap_simps')+)[1]
apply (simp add: tcb_cte_cases_def)
apply (simp add: ctcb_relation_def cthread_state_relation_def
ThreadState_BlockedOnSend_def mask_def
@ -4515,7 +4459,9 @@ lemma tcbEPAppend_spec:
((ctcb_ptr_to_tcb_ptr \<^bsup>s\<^esup>tcb) # queue)))
\<and> option_map tcb_null_ep_ptrs \<circ> (cslift t) =
option_map tcb_null_ep_ptrs \<circ> (cslift s)
\<and> cslift_all_but_tcb_C t s \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
\<and> cslift_all_but_tcb_C t s \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)
\<and> (\<forall>rs. zero_ranges_are_zero rs (\<^bsup>s\<^esup>t_hrs)
\<longrightarrow> zero_ranges_are_zero rs (\<^bsup>t\<^esup>t_hrs))}"
apply (intro allI)
apply (rule conseqPre, vcg)
apply (clarsimp split del: split_if)
@ -4536,13 +4482,13 @@ lemma tcbEPAppend_spec:
apply assumption+
apply (drule tcb_at_not_NULL, simp)
apply (unfold upd_unless_null_def)
apply (simp add: typ_heap_simps)
apply (intro impI conjI allI)
apply simp
apply simp
apply (rule ext)
apply (clarsimp simp add: typ_heap_simps tcb_null_ep_ptrs_def
split: split_if)
apply (clarsimp split: split_if_asm)
apply (simp add: typ_heap_simps')
apply (rule ext)
apply (clarsimp simp add: typ_heap_simps tcb_null_ep_ptrs_def
split: split_if)
apply (simp add: typ_heap_simps')
apply (intro conjI)
apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff)
apply (erule iffD1 [OF tcb_queue_relation'_cong, OF refl refl refl, rotated -1])
apply (clarsimp split: split_if)
@ -4634,7 +4580,8 @@ lemma sendIPC_enqueue_ccorres_helper:
apply (simp add: setEndpoint_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def init_def Let_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -4660,9 +4607,9 @@ lemma sendIPC_enqueue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: typ_heap_simps')
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
apply assumption
@ -4672,7 +4619,8 @@ lemma sendIPC_enqueue_ccorres_helper:
apply (simp add: setEndpoint_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -4700,7 +4648,7 @@ lemma sendIPC_enqueue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -4998,9 +4946,8 @@ lemma receiveIPC_block_ccorres_helper:
apply clarsimp
apply (frule(1) tcb_at_h_t_valid)
apply (frule h_t_valid_c_guard)
apply (clarsimp simp: typ_heap_simps)
apply (erule(1) rf_sr_tcb_update_no_queue)
apply (simp add: typ_heap_simps)+
apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice)
apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps)+)
apply (simp add: tcb_cte_cases_def)
apply (simp add: ctcb_relation_def cthread_state_relation_def
ThreadState_BlockedOnReceive_def mask_def
@ -5069,7 +5016,8 @@ lemma receiveIPC_enqueue_ccorres_helper:
apply (simp add: setEndpoint_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -5097,7 +5045,7 @@ lemma receiveIPC_enqueue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -5109,7 +5057,8 @@ lemma receiveIPC_enqueue_ccorres_helper:
apply (simp add: setEndpoint_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def init_def Let_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -5134,9 +5083,9 @@ lemma receiveIPC_enqueue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: typ_heap_simps')
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
apply assumption
@ -5198,7 +5147,8 @@ lemma receiveIPC_dequeue_ccorres_helper:
apply (rule conjI)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -5218,9 +5168,9 @@ lemma receiveIPC_dequeue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: typ_heap_simps')
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
apply assumption
@ -5237,7 +5187,8 @@ lemma receiveIPC_dequeue_ccorres_helper:
apply (rule bexI [OF _ setObject_eq])
apply (frule(1) st_tcb_at_h_t_valid)
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ep_map_tos)
cpspace_relation_def update_ep_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -5265,9 +5216,9 @@ lemma receiveIPC_dequeue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: typ_heap_simps')
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
apply assumption
@ -5335,13 +5286,13 @@ lemma completeSignal_ccorres:
apply (clarsimp simp: typ_heap_simps setNotification_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def update_ntfn_map_tos
cpspace_relation_def)
cpspace_relation_def typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def mask_def)
apply simp
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -5772,7 +5723,8 @@ lemma sendSignal_dequeue_ccorres_helper:
apply (rule conjI)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -5792,7 +5744,7 @@ lemma sendSignal_dequeue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -5813,7 +5765,8 @@ lemma sendSignal_dequeue_ccorres_helper:
apply (rule bexI [OF _ setObject_eq])
apply (frule(1) st_tcb_at_h_t_valid)
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -5841,7 +5794,7 @@ lemma sendSignal_dequeue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -5868,7 +5821,7 @@ lemma ntfn_set_active_ccorres:
apply (rule cmap_relation_ko_atE [OF cmap_relation_ntfn], assumption+)
apply (clarsimp simp: typ_heap_simps)
apply (rule bexI[OF _ setObject_eq], simp_all)
apply (clarsimp simp: typ_heap_simps rf_sr_def cstate_relation_def Let_def
apply (clarsimp simp: typ_heap_simps' rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos
carch_state_relation_def cmachine_state_relation_def)
apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
@ -5977,14 +5930,15 @@ lemma sendSignal_ccorres [corres]:
apply (clarsimp simp: typ_heap_simps)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
apply (simp add: cnotification_relation_def Let_def
NtfnState_Active_def mask_def word_bw_comms)
apply simp
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -6067,9 +6021,9 @@ lemma receiveSignal_block_ccorres_helper:
apply clarsimp
apply (frule(1) tcb_at_h_t_valid)
apply (frule h_t_valid_c_guard)
apply (clarsimp simp: typ_heap_simps)
apply (erule(1) rf_sr_tcb_update_no_queue)
apply (simp add: typ_heap_simps)+
apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice)
apply (erule(1) rf_sr_tcb_update_no_queue_gen,
(simp add: typ_heap_simps')+)
apply (simp add: tcb_cte_cases_def)
apply (simp add: ctcb_relation_def cthread_state_relation_def
ThreadState_BlockedOnNotification_def mask_def
@ -6191,7 +6145,8 @@ lemma receiveSignal_enqueue_ccorres_helper:
apply (simp add: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -6219,7 +6174,7 @@ lemma receiveSignal_enqueue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
subgoal by (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -6231,7 +6186,8 @@ lemma receiveSignal_enqueue_ccorres_helper:
apply (simp add: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def init_def Let_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -6258,7 +6214,7 @@ lemma receiveSignal_enqueue_ccorres_helper:
-- "queue relation"
apply (rule cready_queues_relation_null_queue_ptrs, assumption+)
apply (clarsimp simp: comp_def)
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -6352,14 +6308,15 @@ lemma receiveSignal_ccorres [corres]:
apply (clarsimp simp: typ_heap_simps setNotification_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
apply (simp add: cnotification_relation_def Let_def
NtfnState_Idle_def mask_def)
apply simp
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)

118
proof/crefine/Recycle_C.thy
View File

@ -194,6 +194,31 @@ lemma flex_user_data_at_rf_sr_dom_s:
apply simp
done
lemma hrs_mem_update_fold_eq:
"hrs_mem_update (fold f xs)
= fold (hrs_mem_update o f) xs"
apply (rule sym, induct xs)
apply (simp add: hrs_mem_update_def)
apply (simp add: hrs_mem_update_def fun_eq_iff)
done
lemma power_user_page_foldl_zero_ranges:
" \<forall>p<2 ^ (pageBitsForSize sz - pageBits).
hrs_htd hrs \<Turnstile>\<^sub>t (Ptr (ptr + of_nat p * 0x1000) :: user_data_C ptr)
\<Longrightarrow> zero_ranges_are_zero rngs hrs
\<Longrightarrow> zero_ranges_are_zero rngs
(hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (Ptr x) (user_data_C (arr x)) s) s
(map (\<lambda>n. ptr + of_nat n * 0x1000) [0..<2 ^ (pageBitsForSize sz - pageBits)]))
hrs)"
apply (simp add: foldl_conv_fold hrs_mem_update_fold_eq)
apply (rule conjunct1)
apply (rule fold_invariant[where P="\<lambda>hrs'. zero_ranges_are_zero rngs hrs'
\<and> hrs_htd hrs' = hrs_htd hrs"
and xs=xs and Q="\<lambda>x. x \<in> set xs" for xs], simp_all)
apply (subst zero_ranges_are_zero_update, simp_all)
apply clarsimp
done
lemma heap_to_device_data_disj_mdf':
"\<lbrakk>is_aligned ptr (pageBitsForSize sz); ksPSpace \<sigma> a = Some obj; objBitsKO obj = pageBits; pspace_aligned' \<sigma>;
pspace_distinct' \<sigma>; pspace_no_overlap' ptr (pageBitsForSize sz) \<sigma>\<rbrakk>
@ -291,6 +316,7 @@ lemma clearMemory_PageCap_ccorres:
carch_state_relation_def
cmachine_state_relation_def
foldl_fun_upd_const[unfolded fun_upd_def]
power_user_page_foldl_zero_ranges
dom_heap_to_device_data)
apply (rule conjI[rotated])
apply (simp add:pageBitsForSize_mess_multi)
@ -1409,7 +1435,8 @@ lemma cancelBadgedSends_ccorres:
cmachine_state_relation_def
)
apply (clarsimp simp: cpspace_relation_def
update_ep_map_tos)
update_ep_map_tos
typ_heap_simps')
apply (erule(1) cpspace_relation_ep_update_ep2)
apply (simp add: cendpoint_relation_def endpoint_state_defs)
subgoal by simp
@ -1447,7 +1474,7 @@ lemma cancelBadgedSends_ccorres:
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
carch_state_relation_def
cmachine_state_relation_def
cpspace_relation_def
cpspace_relation_def typ_heap_simps'
update_ep_map_tos)
apply (erule(1) cpspace_relation_ep_update_ep2)
subgoal by (simp add: cendpoint_relation_def Let_def)
@ -1459,7 +1486,7 @@ lemma cancelBadgedSends_ccorres:
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
carch_state_relation_def
cmachine_state_relation_def
cpspace_relation_def
cpspace_relation_def typ_heap_simps'
update_ep_map_tos)
apply (erule(1) cpspace_relation_ep_update_ep2)
apply (simp add: cendpoint_relation_def Let_def)
@ -1936,6 +1963,91 @@ lemma cteRecycle_ccorres:
apply (clarsimp simp: from_bool_def true_def exception_defs cintr_def)
done
lemma cte_lift_ccte_relation:
"cte_lift cte' = Some ctel'
\<Longrightarrow> c_valid_cte cte'
\<Longrightarrow> ccte_relation (cte_to_H ctel') cte'"
by (simp add: ccte_relation_def)
lemma updateFreeIndex_ccorres:
"\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte'
\<and> cteCap cte = cap' \<and> ccte_relation cte cte'})
c
{t. \<exists>cap. cap_untyped_cap_lift cap = (cap_untyped_cap_lift
(cte_C.cap_C (the (cslift s (cte_Ptr srcSlot)))))
\<lparr> cap_untyped_cap_CL.capFreeIndex_CL := ((of_nat idx') >> 4) \<rparr>
\<and> cap_get_tag cap = scast cap_untyped_cap
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot)
(cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot)))))
(t_hrs_' (globals s))
\<and> t may_only_modify_globals s in [t_hrs]
}
\<Longrightarrow> ccorres dc xfdc
(valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte)
\<and> cap' = (cteCap cte)) srcSlot
and untyped_ranges_zero'
and (\<lambda>_. is_aligned (of_nat idx' :: word32) 4 \<and> idx' \<le> 2 ^ (capBlockSize cap')))
{s. \<not> capIsDevice cap'
\<longrightarrow> region_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs
(updateFreeIndex srcSlot idx') c"
(is "_ \<Longrightarrow> ccorres dc xfdc (valid_objs' and ?cte_wp_at' and _ and _) ?P' hs ?a c")
apply (rule ccorres_gen_asm)
apply (simp add: updateFreeIndex_def getSlotCap_def updateCap_def)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_split_noop_lhs, rule_tac cap'=cap' in updateTrackedFreeIndex_noop_ccorres)
apply (rule ccorres_pre_getCTE)+
apply (rename_tac cte cte2)
apply (rule_tac P = "\<lambda>s. ?cte_wp_at' s \<and> cte2 = cte \<and> cte_wp_at' (op = cte) srcSlot s"
and P'="{s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte'
\<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> ?P'" in ccorres_from_vcg)
apply (rule allI, rule HoarePartial.conseq_exploit_pre, clarify)
apply (drule_tac x=s in spec, rule conseqPre, erule conseqPost)
defer
apply clarsimp
apply clarsimp
apply (simp add: cte_wp_at_ctes_of)
apply wp
apply (clarsimp simp: isCap_simps cte_wp_at_ctes_of)
apply (frule(1) rf_sr_ctes_of_clift)
apply clarsimp
apply (frule(1) cte_lift_ccte_relation)
apply (rule exI, intro conjI[rotated], assumption, simp_all)[1]
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (erule(1) rf_sr_ctes_of_cliftE)
apply (frule(1) rf_sr_ctes_of_clift)
apply clarsimp
apply (subgoal_tac "ccap_relation (capFreeIndex_update (\<lambda>_. idx')
(cteCap (the (ctes_of \<sigma> srcSlot)))) cap")
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule bexI [rotated])
apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
isCap_simps)
apply (simp add:cpspace_relation_def)
apply (clarsimp simp:typ_heap_simps' modify_map_def mex_def meq_def)
apply (rule conjI)
apply (rule cpspace_cte_relation_upd_capI, assumption+)
apply (rule conjI)
apply (rule setCTE_tcb_case, assumption+)
apply (case_tac s', clarsimp)
subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps')
apply (clarsimp simp: isCap_simps)
apply (drule(1) cte_lift_ccte_relation,
drule ccte_relation_ccap_relation)
apply (simp add: cte_to_H_def)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: ccap_relation_def cap_lift_untyped_cap
cap_to_H_simps cap_untyped_cap_lift_def
is_aligned_shiftr_shiftl
dest!: ccte_relation_ccap_relation)
apply (rule unat_of_nat_eq unat_of_nat_eq[symmetric],
erule order_le_less_trans,
rule power_strict_increasing, simp_all)
apply (rule unat_less_helper, rule order_le_less_trans[OF word_and_le1], simp)
done
end
(* FIXME: Move *)

1394
proof/crefine/Retype_C.thy
View File

File diff suppressed because it is too large Load Diff

81
proof/crefine/SR_lemmas_C.thy
View File

@ -1668,6 +1668,35 @@ lemma heap_to_device_data_cong [cong]:
\<Longrightarrow> heap_to_device_data ks bhp = heap_to_device_data ks' bhp'"
unfolding heap_to_device_data_def by simp
lemma map_leD:
"\<lbrakk> map_le m m'; m x = Some y \<rbrakk> \<Longrightarrow> m' x = Some y"
by (simp add: map_le_def dom_def)
lemma region_is_bytes_disjoint:
assumes cleared: "region_is_bytes' p n (hrs_htd hrs)"
and not_byte: "typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)"
shows "hrs_htd hrs \<Turnstile>\<^sub>t (p' :: 'a ptr)
\<Longrightarrow> {p ..+ n} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {}"
apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
apply (clarsimp simp: set_eq_iff dest!: intvlD[where p="ptr_val p'"])
apply (drule_tac x="of_nat k" in spec, clarsimp simp: size_of_def)
apply (cut_tac m=k in typ_slice_t_self[where td="typ_uinfo_t TYPE('a)"])
apply (clarsimp simp: in_set_conv_nth)
apply (drule_tac x=i in map_leD, simp)
apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def)
done
lemma zero_ranges_are_zero_update[simp]:
"h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr)
\<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)
\<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update ptr v) hrs)
= zero_ranges_are_zero rs hrs"
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update
intro!: ball_cong[OF refl] conj_cong[OF refl])
apply (drule(2) region_is_bytes_disjoint)
apply (simp add: heap_update_def heap_list_update_disjoint_same Int_commute)
done
lemma inj_tcb_ptr_to_ctcb_ptr [simp]:
"inj tcb_ptr_to_ctcb_ptr"
apply (rule injI)
@ -2197,6 +2226,58 @@ lemma page_table_at_rf_sr:
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def page_table_at_carray_map_relation)
lemma gsUntypedZeroRanges_rf_sr:
"\<lbrakk> (start, end) \<in> gsUntypedZeroRanges s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
zero_ranges_are_zero_def)
apply (drule(1) bspec)
apply clarsimp
done
lemma ctes_of_untyped_zero_rf_sr:
"\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
untyped_ranges_zero' s;
untypedZeroRange (cteCap cte) = Some (start, end) \<rbrakk>
\<Longrightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
apply (erule gsUntypedZeroRanges_rf_sr[rotated])
apply (clarsimp simp: untyped_ranges_zero_inv_def)
apply (rule_tac a=p in ranI)
apply (simp add: map_comp_def cteCaps_of_def)
done
lemma heap_list_is_zero_mono:
"heap_list_is_zero hmem p n \<Longrightarrow> n' \<le> n
\<Longrightarrow> heap_list_is_zero hmem p n'"
apply (induct n arbitrary: n' p)
apply simp
apply clarsimp
apply (case_tac n', simp_all)
done
lemma heap_list_h_eq_better:
"\<And>p. \<lbrakk> x \<in> {p..+q}; heap_list h q p = heap_list h' q p \<rbrakk>
\<Longrightarrow> h x = h' x"
proof (induct q)
case 0 thus ?case by simp
next
case (Suc n) thus ?case by (force dest: intvl_neq_start)
qed
lemma heap_list_is_zero_mono2:
"heap_list_is_zero hmem p n
\<Longrightarrow> {p' ..+ n'} \<le> {p ..+ n}
\<Longrightarrow> heap_list_is_zero hmem p' n'"
using heap_list_h_eq2[where h'="\<lambda>_. 0"]
heap_list_h_eq_better[where h'="\<lambda>_. 0"]
apply (simp(no_asm_use) add: heap_list_rpbs)
apply blast
done
lemma invs_urz[elim!]:
"invs' s \<Longrightarrow> untyped_ranges_zero' s"
by (clarsimp simp: invs'_def valid_state'_def)
end
end

6
proof/crefine/Schedule_C.thy
View File

@ -818,11 +818,7 @@ proof -
apply (frule_tac t=t in valid_queues_no_bitmap_objD)
apply (blast intro: cons_set_intro)
apply (simp add: lookupBitmapPriority_def)
apply normalise_obj_at'
apply (rule valid_queues_queued_runnable[simplified valid_queues_def])
apply simp
apply (simp add: invs_no_cicd'_def)
apply (clarsimp simp add: inQ_def obj_at'_def)
apply (clarsimp simp: obj_at'_def st_tcb_at'_def)
apply (fold lookupBitmapPriority_def)
apply (drule invs_no_cicd'_queues)

26
proof/crefine/StateRelation_C.thy
View File

@ -672,6 +672,31 @@ where
end
definition
region_is_bytes' :: "word32 \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"
where
"region_is_bytes' ptr sz htd \<equiv> \<forall>z\<in>{ptr ..+ sz}. \<forall> td. td \<noteq> typ_uinfo_t TYPE (word8) \<longrightarrow>
(\<forall>n b. snd (htd z) n \<noteq> Some (td, b))"
abbreviation
region_is_bytes :: "word32 \<Rightarrow> nat \<Rightarrow> globals myvars \<Rightarrow> bool"
where
"region_is_bytes ptr sz s \<equiv> region_is_bytes' ptr sz (hrs_htd (t_hrs_' (globals s)))"
abbreviation(input)
"heap_list_is_zero hp ptr n \<equiv> heap_list hp n ptr = replicate n 0"
abbreviation
"region_is_zero_bytes ptr n x \<equiv> region_is_bytes ptr n x
\<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr n"
definition
zero_ranges_are_zero
where
"zero_ranges_are_zero rs hrs
= (\<forall>(start, end) \<in> rs. region_is_bytes' start (unat ((end + 1) - start)) (hrs_htd hrs)
\<and> heap_list_is_zero (hrs_mem hrs) start (unat ((end + 1) - start)))"
definition (in state_rel)
cstate_relation :: "KernelStateData_H.kernel_state \<Rightarrow> globals \<Rightarrow> bool"
where
@ -682,6 +707,7 @@ where
cready_queues_relation (clift cheap)
(ksReadyQueues_' cstate)
(ksReadyQueues astate) \<and>
zero_ranges_are_zero (gsUntypedZeroRanges astate) cheap \<and>
cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cstate) (ksReadyQueuesL1Bitmap astate) \<and>
cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cstate) (ksReadyQueuesL2Bitmap astate) \<and>
ksCurThread_' cstate = (tcb_ptr_to_ctcb_ptr (ksCurThread astate)) \<and>

52
proof/crefine/StoreWord_C.thy
View File

@ -624,6 +624,30 @@ proof (intro allI impI)
apply (simp add: typ_heap_simps clift_heap_update_same)
done
have subset: "{ptr..+ 2 ^ 2} \<subseteq> {ptr && ~~ mask pageBits ..+ 2 ^ pageBits}"
apply (simp only: upto_intvl_eq al is_aligned_neg_mask2)
apply (cut_tac ptr="ptr && ~~ mask pageBits" and x="ptr && mask pageBits"
in aligned_range_offset_subset, rule is_aligned_neg_mask2)
apply (rule is_aligned_andI1[OF al])
apply (simp add: pageBits_def)
apply (rule and_mask_less', simp add: pageBits_def)
apply (erule order_trans[rotated])
apply (simp add: mask_out_sub_mask)
done
hence zr: "\<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s)))
= zero_ranges_are_zero rs (t_hrs_' (globals s))"
using page
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
heap_update_def
intro!: ball_cong[OF refl] conj_cong[OF refl])
apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift])
apply simp
apply (subst heap_list_update_disjoint_same, simp_all)
apply ((subst Int_commute)?, erule disjoint_subset2[rotated])
apply (simp add: pageBits_def)
done
have cmap_relation_heap_cong:
"\<And>as cs cs' f rel. \<lbrakk> cmap_relation as cs f rel; cs = cs' \<rbrakk> \<Longrightarrow> cmap_relation as cs' f rel"
by simp
@ -664,7 +688,7 @@ proof (intro allI impI)
thus ?thesis using rf
apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name)
apply (simp add: carch_state_relation_def cmachine_state_relation_def carch_globals_def)
apply (simp add: rl' tag_disj_via_td_name)
apply (simp add: rl' tag_disj_via_td_name zr)
done
qed
@ -908,6 +932,30 @@ proof (intro allI impI)
apply (simp add: typ_heap_simps clift_heap_update_same)
done
have subset: "{ptr..+ 2 ^ 2} \<subseteq> {ptr && ~~ mask pageBits ..+ 2 ^ pageBits}"
apply (simp only: upto_intvl_eq al is_aligned_neg_mask2)
apply (cut_tac ptr="ptr && ~~ mask pageBits" and x="ptr && mask pageBits"
in aligned_range_offset_subset, rule is_aligned_neg_mask2)
apply (rule is_aligned_andI1[OF al])
apply (simp add: pageBits_def)
apply (rule and_mask_less', simp add: pageBits_def)
apply (erule order_trans[rotated])
apply (simp add: mask_out_sub_mask)
done
hence zr: "\<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s)))
= zero_ranges_are_zero rs (t_hrs_' (globals s))"
using page
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
heap_update_def
intro!: ball_cong[OF refl] conj_cong[OF refl])
apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift])
apply simp
apply (subst heap_list_update_disjoint_same, simp_all)
apply ((subst Int_commute)?, erule disjoint_subset2[rotated])
apply (simp add: pageBits_def)
done
have cmap_relation_heap_cong:
"\<And>as cs cs' f rel. \<lbrakk> cmap_relation as cs f rel; cs = cs' \<rbrakk> \<Longrightarrow> cmap_relation as cs' f rel"
by simp
@ -948,7 +996,7 @@ proof (intro allI impI)
thus ?thesis using rf
apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name)
apply (simp add: carch_state_relation_def cmachine_state_relation_def carch_globals_def)
apply (simp add: rl' tag_disj_via_td_name)
apply (simp add: rl' tag_disj_via_td_name zr)
done
qed

29
proof/crefine/Syscall_C.thy
View File

@ -574,7 +574,22 @@ lemma threadGet_tcbFaultHandler_ccorres [corres]:
apply (clarsimp simp: obj_at'_def ctcb_relation_def)
done
lemma rf_sr_tcb_update_twice:
"h_t_valid (hrs_htd (hrs2 (globals s') (t_hrs_' (gs2 (globals s'))))) c_guard
(ptr (t_hrs_' (gs2 (globals s'))) (globals s'))
\<Longrightarrow> ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths.
hrs_mem_update (heap_update (ptr ths gs :: tcb_C ptr) (v ths gs))
(hrs_mem_update (heap_update (ptr ths gs) (v' ths gs)) (hrs2 gs ths))) (gs2 gs)) s') \<in> rf_sr)
= ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths.
hrs_mem_update (heap_update (ptr ths gs) (v ths gs)) (hrs2 gs ths)) (gs2 gs)) s') \<in> rf_sr)"
by (simp add: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def typ_heap_simps'
carch_state_relation_def
cmachine_state_relation_def)
lemma hrs_mem_update_use_hrs_mem:
"hrs_mem_update f = (\<lambda>hrs. (hrs_mem_update $ (\<lambda>_. f (hrs_mem hrs))) hrs)"
by (simp add: hrs_mem_update_def hrs_mem_def fun_eq_iff)
lemma sendFaultIPC_ccorres:
"ccorres (cfault_rel2 \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -635,21 +650,21 @@ lemma sendFaultIPC_ccorres:
(lookup_fault_lift(original_lookup_fault_' s)))}"
in threadSet_ccorres_lemma4)
apply vcg
apply (clarsimp simp: typ_heap_simps')
apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice)
apply (intro conjI allI impI)
apply (simp add: typ_heap_simps rf_sr_def)
apply (simp add: typ_heap_simps' rf_sr_def)
apply (rule rf_sr_tcb_update_no_queue2[unfolded rf_sr_def, simplified],
assumption+)
apply (simp add: typ_heap_simps)+
assumption+, (simp add: typ_heap_simps')+)
apply (rule ball_tcb_cte_casesI, simp+)
apply (simp add: ctcb_relation_def cthread_state_relation_def )
apply (case_tac "tcbState tcb", simp+)
apply (simp add: rf_sr_def)
apply (rule rf_sr_tcb_update_no_queue2[unfolded rf_sr_def, simplified],
assumption+)
apply (simp add: typ_heap_simps)+
assumption+, (simp add: typ_heap_simps' | simp only: hrs_mem_update_use_hrs_mem)+)
apply (rule ball_tcb_cte_casesI, simp+)
apply (simp add: ctcb_relation_def cthread_state_relation_def )
apply (clarsimp simp: typ_heap_simps')
apply (simp add: ctcb_relation_def cthread_state_relation_def)
apply (rule conjI)
apply (case_tac "tcbState tcb", simp+)
apply (simp add: cfault_rel_def)

21
proof/crefine/TcbQueue_C.thy
View File

@ -1108,9 +1108,8 @@ lemma cvariable_relation_upd_const:
lemma rf_sr_tcb_update_no_queue:
"\<lbrakk> (s, s') \<in> rf_sr; ko_at' tcb thread s;
(cslift t :: tcb_C typ_heap) = (cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> ctcb);
cslift_all_but_tcb_C t s';
hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
t_hrs_' (globals t) = hrs_mem_update (heap_update
(tcb_ptr_to_ctcb_ptr thread) ctcb) (t_hrs_' (globals s'));
tcbEPNext_C ctcb = tcbEPNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread)));
tcbEPPrev_C ctcb = tcbEPPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread)));
tcbSchedNext_C ctcb = tcbSchedNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread)));
@ -1125,7 +1124,8 @@ lemma rf_sr_tcb_update_no_queue:
apply (frule (1) cmap_relation_ko_atD)
apply (erule obj_atE')
apply (clarsimp simp: projectKOs)
apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const)
apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const
typ_heap_simps')
apply (intro conjI)
subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq)
apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1])
@ -1141,7 +1141,7 @@ lemma rf_sr_tcb_update_no_queue:
apply (erule cready_queues_relation_not_queue_ptrs)
subgoal by (clarsimp intro!: ext)
subgoal by (clarsimp intro!: ext)
subgoal by (simp add: carch_state_relation_def)
subgoal by (simp add: carch_state_relation_def typ_heap_simps')
by (simp add: cmachine_state_relation_def)
lemma rf_sr_tcb_update_no_queue_helper:
@ -1161,9 +1161,8 @@ lemma tcb_queue_relation_not_in_q:
lemma rf_sr_tcb_update_not_in_queue:
"\<lbrakk> (s, s') \<in> rf_sr; ko_at' tcb thread s;
(cslift t :: tcb_C typ_heap) = (cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> ctcb);
cslift_all_but_tcb_C t s';
hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
t_hrs_' (globals t) = hrs_mem_update (heap_update
(tcb_ptr_to_ctcb_ptr thread) ctcb) (t_hrs_' (globals s'));
\<not> live' (KOTCB tcb); invs' s;
(\<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x);
ctcb_relation tcb' ctcb \<rbrakk>
@ -1175,7 +1174,8 @@ lemma rf_sr_tcb_update_not_in_queue:
apply (frule (1) cmap_relation_ko_atD)
apply (erule obj_atE')
apply (clarsimp simp: projectKOs)
apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const)
apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const
typ_heap_simps')
apply (subgoal_tac "\<forall>rf. \<not> ko_wp_at' (\<lambda>ko. rf \<in> refs_of' ko) thread s")
prefer 2
apply (auto simp: obj_at'_def ko_wp_at'_def)[1]
@ -1205,7 +1205,8 @@ lemma rf_sr_tcb_update_not_in_queue:
apply (drule valid_queues_obj_at'D, clarsimp)
apply (clarsimp simp: obj_at'_def projectKOs inQ_def)
subgoal by simp
subgoal by (simp add: carch_state_relation_def carch_globals_def)
subgoal by (simp add: carch_state_relation_def carch_globals_def
typ_heap_simps')
by (simp add: cmachine_state_relation_def)
lemmas rf_sr_tcb_update_not_in_queue2

31
proof/crefine/Tcb_C.thy
View File

@ -428,8 +428,7 @@ lemma setPriority_ccorres:
apply vcg
apply clarsimp
apply (erule(1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps)+, simp_all)[1]
apply (subst heap_update_field_hrs | fastforce intro: typ_heap_simps)+
(simp add: typ_heap_simps')+, simp_all?)[1]
apply (rule ball_tcb_cte_casesI, simp+)
apply (simp add: ctcb_relation_def cast_simps)
apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down)
@ -484,14 +483,12 @@ lemma setMCPriority_ccorres:
apply vcg
apply clarsimp
apply (erule(1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps)+, simp_all)[1]
apply (subst heap_update_field_hrs | fastforce intro: typ_heap_simps)+
(simp add: typ_heap_simps')+)[1]
apply (rule ball_tcb_cte_casesI, simp+)
apply (simp add: ctcb_relation_def cast_simps)
apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down)
done
lemma ccorres_subgoal_tailE:
"\<lbrakk> ccorres rvr xf Q Q' hs (b ()) d;
ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d) \<rbrakk>
@ -655,10 +652,7 @@ lemma invokeTCB_ThreadControl_ccorres:
apply vcg
apply clarsimp
apply (erule(1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps)+, simp_all)[1]
apply (subst heap_update_field_hrs
| simp add: typ_heap_simps
| fastforce intro: typ_heap_simps)+
(simp add: typ_heap_simps')+, simp_all?)[1]
apply (rule ball_tcb_cte_casesI, simp+)
apply (clarsimp simp: ctcb_relation_def option_to_0_def)
apply (rule ceqv_refl)
@ -943,7 +937,8 @@ lemma setupReplyMaster_ccorres:
apply (rule fst_setCTE[OF ctes_of_cte_at], assumption)
apply (rule rev_bexI, assumption)
apply (clarsimp simp: rf_sr_def cstate_relation_def
cpspace_relation_def Let_def)
cpspace_relation_def Let_def
typ_heap_simps')
apply (subst setCTE_tcb_case, assumption+)
apply (rule_tac r="s'" in KernelStateData_H.kernel_state.cases)
apply clarsimp
@ -960,7 +955,7 @@ lemma setupReplyMaster_ccorres:
apply (simp add: true_def mask_def to_bool_def)
apply simp
apply (simp add: cmachine_state_relation_def
h_t_valid_clift_Some_iff
typ_heap_simps'
carch_state_relation_def carch_globals_def
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"])
apply (wp | simp)+
@ -1392,7 +1387,6 @@ lemma asUser_sysargs_rel:
apply (wp asUser_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+
done
lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
notes static_imp_wp [wp]
shows
@ -1455,6 +1449,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
frame_gp_registers_convs word_less_nat_alt)
apply (simp add: unat_of_nat32 word_bits_def)
apply arith
apply clarsimp
apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
exspec=sanitiseRegister_modifies)
apply clarsimp
@ -1484,6 +1479,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
word_less_nat_alt word_bits_def
less_diff_conv)
apply (simp add: unat_word_ariths cong: conj_cong)
apply clarsimp
apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
exspec=sanitiseRegister_modifies)
apply clarsimp
@ -3545,7 +3541,8 @@ lemma bindNotification_ccorres:
apply (clarsimp simp: setNotification_def split_def)
apply (rule bexI [OF _ setObject_eq])
apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
cpspace_relation_def update_ntfn_map_tos)
cpspace_relation_def update_ntfn_map_tos
typ_heap_simps')
apply (elim conjE)
apply (intro conjI)
-- "tcb relation"
@ -3556,7 +3553,7 @@ lemma bindNotification_ccorres:
apply ((clarsimp simp: option_to_ctcb_ptr_def
tcb_ptr_to_ctcb_ptr_def ctcb_offset_def obj_at'_def projectKOs
objBitsKO_def bindNTFN_alignment_junk)+)[4]
apply (simp add: carch_state_relation_def)
apply (simp add: carch_state_relation_def typ_heap_simps')
apply (simp add: cmachine_state_relation_def)
apply (simp add: h_t_valid_clift_Some_iff)
apply (simp add: objBits_simps)
@ -3568,8 +3565,8 @@ lemma bindNotification_ccorres:
apply (rule_tac P'=\<top> and P=\<top> in threadSet_ccorres_lemma3[unfolded dc_def])
apply vcg
apply simp
apply (erule (1) rf_sr_tcb_update_no_queue2)
apply (simp add: typ_heap_simps)+
apply (erule (1) rf_sr_tcb_update_no_queue2,
(simp add: typ_heap_simps')+, simp_all?)[1]
apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
apply simp
apply (wp get_ntfn_ko'| simp add: guard_is_UNIV_def)+

7
proof/crefine/VSpace_C.thy
View File

@ -712,8 +712,8 @@ lemma generic_frame_cap_ptr_set_capFMappedAddress_spec:
{t. (\<exists>cte' cap'.
generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift s \<^bsup>s\<^esup>cap_ptr))) \<^bsup>s\<^esup>asid \<^bsup>s\<^esup>addr = Some cap' \<and>
cte_lift cte' = option_map (cap_CL_update (K cap')) (cte_lift (the (cslift s cte_slot))) \<and>
cslift t = cslift s(cte_slot \<mapsto> cte')) \<and> cslift_all_but_cte_C t s
\<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}"
t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte')
(t_hrs_' (globals s)))}"
apply vcg
apply (clarsimp simp: typ_heap_simps)
apply (subgoal_tac "cap_lift ret__struct_cap_C \<noteq> None")
@ -721,9 +721,8 @@ lemma generic_frame_cap_ptr_set_capFMappedAddress_spec:
apply (clarsimp simp: generic_frame_cap_set_capFMappedAddress_CL_def split: cap_CL.splits)
apply (clarsimp simp: clift_ptr_safe2 typ_heap_simps)
apply (rule_tac x="cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y" in exI)
apply simp
apply (case_tac y)
apply (clarsimp simp: cte_lift_def)
apply (clarsimp simp: cte_lift_def typ_heap_simps')
done
lemma lookupPDSlot_spec:

191
proof/drefine/Untyped_DR.thy
View File

@ -1256,6 +1256,33 @@ lemma mapME_x_append:
apply (simp add: mapME_x_Cons bindE_assoc)
done
lemma hd_filter_eq:
"P (hd xs) \<Longrightarrow> hd (filter P xs) = hd xs"
by (cases xs, simp_all)
lemma free_range_of_untyped_subset'[rule_format]:
assumes al: "is_aligned ptr sz"
and sz: "sz < size (ptr)"
shows "a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr"
proof -
note no_ov = is_aligned_no_overflow'[OF al]
note mono = word_plus_mono_right[OF _ no_ov, simplified field_simps]
note sz_len = sz[unfolded word_size]
(*
note sz_simp[simp] = unat_2p_sub_1[OF sz_len] unat_power_lower[OF sz_len]
*)
show ?thesis using sz
apply (intro impI psubsetI)
apply (rule free_range_of_untyped_subseteq', simp_all add: al)
apply (clarsimp simp:free_range_of_untyped_def)
apply (strengthen mono word_of_nat_le)+
apply (simp add: sz_len unat_2p_sub_1)
apply (intro conjI impI; (clarsimp dest!: le_p2_minus_1)?)
apply (drule word_unat.Abs_eqD, simp_all add: unats_def word_size
less_trans[OF _ power_strict_increasing[OF sz_len]])
done
qed
lemma reset_untyped_cap_corres:
"dcorres (dc \<oplus> dc) \<top> (invs and valid_etcbs and ct_active
and cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> free_index_of cap = idx) cref
@ -1271,14 +1298,28 @@ lemma reset_untyped_cap_corres:
apply (rule_tac F="is_untyped_cap capa \<and> cap_aligned capa
\<and> bits_of capa > 2 \<and> free_index_of capa \<le> 2 ^ bits_of capa"
in corres_gen_asm2)
apply (simp add: whenE_def if_flip split del: split_if)
apply (rule corres_if)
apply (clarsimp simp: is_cap_simps free_range_of_untyped_def
cap_aligned_def free_index_of_def)
apply (simp add: word_unat.Rep_inject[symmetric])
apply (subst unat_of_nat_eq, erule order_le_less_trans,
rule power_strict_increasing, simp_all add: word_bits_def bits_of_def)[1]
apply (rule corres_trivial, rule corres_returnOk, simp)
apply (rule_tac F="free_index_of capa \<noteq> 0" in corres_gen_asm2)
apply (rule corres_split_nor)
prefer 2
apply (rule delete_objects_dcorres)
apply (clarsimp simp: is_cap_simps bits_of_def)
apply (rule corres_if_rhs)
apply (rule_tac x=0 in select_pick_corres_asm)
apply simp
apply (simp add: mapME_x_Nil)
apply (rule_tac x="[cap_objects (transform_cap capa)]" in select_pick_corres_asm)
apply (clarsimp simp: is_cap_simps cap_aligned_def free_index_of_def)
apply (rule order_less_le_trans, rule free_range_of_untyped_subset'[where a=0],
simp_all)[1]
apply (simp add: word_size word_bits_def)
apply (simp add: free_range_of_untyped_def)
apply (simp add: mapME_x_Nil mapME_x_Cons liftE_def bind_assoc)
apply (rule corres_add_noop_lhs)
apply (rule corres_split_nor)
prefer 2
@ -1288,96 +1329,80 @@ lemma reset_untyped_cap_corres:
apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def)
apply (clarsimp simp: is_cap_simps cap_aligned_def bits_of_def)
apply (rule corres_trivial, simp)
apply (rule set_cap_corres)
apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def)
apply simp
apply (wp | simp add: unless_def)+
apply (rule_tac x="length xs" for xs in select_pick_corres_asm)
apply simp
apply (simp add: mapME_x_upt_length_ys)
apply (rule corres_dummy_returnOk_r)
apply (rule corres_splitEE)
prefer 2
apply (rule_tac P="\<top>\<top>" and P'="\<lambda>_. valid_objs
apply (rule corres_split_nor)
apply (rule corres_alternate1)
apply (rule corres_trivial, simp add: returnOk_def)
apply (rule set_cap_corres)
apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def)
apply simp
apply (wp | simp add: unless_def)+
apply (rule_tac F="\<not> (is_device_untyped_cap capa \<or> bits_of capa < reset_chunk_bits)
\<and> (\<exists>s. s \<turnstile> capa)"
in corres_gen_asm2)
apply (rule_tac x="map (\<lambda>i. free_range_of_untyped (i * 2 ^ reset_chunk_bits)
(bits_of capa) (obj_ref_of capa)) xs" for xs
in select_pick_corres_asm)
prefer 2
apply (simp add: mapME_x_map_simp o_def)
apply (rule_tac P="\<top>\<top>" and P'="\<lambda>_. valid_objs
and valid_etcbs and pspace_no_overlap (untyped_range capa)
and valid_idle and (\<lambda>s. idle_thread s \<noteq> fst cref)
and cte_wp_at (\<lambda>cp. \<exists>idx. cp = free_index_update (\<lambda>_. idx) capa) cref"
in mapME_x_corres_same_xs[OF _ _ _ refl])
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs)
apply (rule corres_split_nor[OF _ clearMemory_corres_noop[OF refl]])
apply (rule_tac x="available_range (transform_cap
(free_index_update (\<lambda>_. x * 2 ^ reset_chunk_bits) capa))"
in select_pick_corres_asm)
apply (clarsimp simp: is_cap_simps bits_of_def free_index_of_def)
apply (strengthen free_range_of_untyped_subseteq')
apply (strengthen order_trans[OF free_range_of_untyped_subseteq'[where a=0]])
apply (simp add: cap_aligned_def free_range_of_untyped_def
word_bits_def word_size)
apply (rule corres_split[OF _ set_cap_corres])
apply (subst alternative_com)
apply (rule throw_or_return_preemption_corres[where P=\<top> and P'=\<top>])
apply (clarsimp simp: is_cap_simps bits_of_def)
apply simp
apply wp
apply (clarsimp simp add: is_cap_simps cap_aligned_def bits_of_def
aligned_add_aligned is_aligned_shiftl)
apply (simp add: reset_chunk_bits_def)
apply (simp add: reset_chunk_bits_def word_bits_def)
apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
preemption_point_inv' set_cap_no_overlap
update_untyped_cap_valid_objs set_cap_idle
| simp)+
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def)
apply (erule pspace_no_overlap_subset)
apply (rule aligned_range_offset_subset, simp_all add: is_aligned_shiftl)[1]
apply (rule shiftl_less_t2n[OF word_of_nat_less])
apply simp
apply (simp add: word_bits_def)
apply (rule hoare_pre, wp)
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs)
apply (rule corres_split_nor[OF _ clearMemory_corres_noop[OF refl]])
apply (rule corres_split[OF _ set_cap_corres])
apply (subst alternative_com)
apply (rule throw_or_return_preemption_corres[where P=\<top> and P'=\<top>])
apply (clarsimp simp: is_cap_simps bits_of_def)
apply simp
apply wp
apply (clarsimp simp add: is_cap_simps cap_aligned_def bits_of_def
aligned_add_aligned is_aligned_shiftl)
apply (simp add: reset_chunk_bits_def)
apply (simp add: reset_chunk_bits_def word_bits_def)
apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
preemption_point_inv' set_cap_no_overlap
update_untyped_cap_valid_objs set_cap_idle
| simp)+
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def)
apply (erule pspace_no_overlap_subset)
apply (rule aligned_range_offset_subset, simp_all add: is_aligned_shiftl)[1]
apply (rule shiftl_less_t2n[OF word_of_nat_less])
apply simp
apply (rule hoare_pre)
apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
update_untyped_cap_valid_objs set_cap_no_overlap
set_cap_idle preemption_point_inv'
set_cap_cte_wp_at
| simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state exI
is_cap_simps bits_of_def)
apply (frule(1) cte_wp_at_valid_objs_valid_cap[OF caps_of_state_cteD])
apply (clarsimp simp: valid_cap_simps cap_aligned_def
valid_untyped_pspace_no_overlap
free_index_of_def)
apply (simp add: returnOk_liftE)
apply (rule monadic_rewrite_corres_rhs,
rule_tac cap="free_index_update (\<lambda>_. 0) capa"
and p=cref in monadic_set_cap_id2)
apply (rule set_cap_corres[unfolded dc_def])
apply (clarsimp simp: is_cap_simps free_range_of_untyped_def)
apply (simp add: word_bits_def)
apply (rule hoare_pre, wp)
apply simp
apply wp
apply (rule_tac P="valid_etcbs
and valid_idle and (\<lambda>s. idle_thread s \<noteq> fst cref)
and cte_wp_at (op = capa) cref"
in hoare_trivE_R)
apply (case_tac "free_index_of capa = 0")
apply (simp add: mapME_x_Nil)
apply wp
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps
apply (rule hoare_pre)
apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
update_untyped_cap_valid_objs set_cap_no_overlap
set_cap_idle preemption_point_inv'
set_cap_cte_wp_at
| simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state exI
is_cap_simps bits_of_def)
apply (frule(1) cte_wp_at_valid_objs_valid_cap[OF caps_of_state_cteD])
apply (clarsimp simp: valid_cap_simps cap_aligned_def
valid_untyped_pspace_no_overlap
free_index_of_def)
apply (subst upt_conv_Cons)
apply simp
apply (simp add: mapME_x_append mapME_x_Cons mapME_x_Nil bindE_assoc)
apply (rule hoare_pre)
apply (wp preemption_point_inv' set_cap_idle
set_cap_cte_wp_at | simp
| (wp_once mapME_x_inv_wp, rule hoare_pre))+
apply (clarsimp simp: is_cap_simps bits_of_def cte_wp_at_caps_of_state)
apply (simp del: hoare_TrueI)
apply (clarsimp simp: is_cap_simps bits_of_def)
apply (strengthen order_trans[OF free_range_of_untyped_subseteq'[where a=0]]
free_range_of_untyped_subset')
apply (clarsimp simp: conj_comms)
apply (clarsimp simp: filter_empty_conv bexI[where x=0]
last_rev hd_map hd_filter_eq
is_cap_simps bits_of_def cap_aligned_def
word_bits_def word_size exI
rev_map[symmetric])
apply (clarsimp simp: free_index_of_def free_range_of_untyped_def)
apply wp
apply clarsimp
apply (wp add: hoare_vcg_const_imp_lift get_cap_wp
| simp
| strengthen invs_valid_objs invs_valid_idle)+
| strengthen invs_valid_objs invs_valid_idle
| rule impI)+
apply (clarsimp simp: cte_wp_at_caps_of_state
descendants_range_def2)
apply (cases cref, simp)