mirror of https://github.com/seL4/l4v.git
lib+refine: rename Corres_Method to CorresK_Method
This also renames most of the corres* methods to corresK* methods, including corressimp -> corresKsimp. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
parent
1f06802350
commit
c1fe4ad10f
|
|
@ -7,12 +7,12 @@
|
|||
|
||||
theory CorresK_Lemmas
|
||||
imports
|
||||
"Lib.Corres_Method"
|
||||
"Lib.CorresK_Method"
|
||||
"ExecSpec.Syscall_H"
|
||||
"ASpec.Syscall_A"
|
||||
begin
|
||||
|
||||
lemma corres_throwError_str [corres_concrete_rER]:
|
||||
lemma corres_throwError_str [corresK_concrete_rER]:
|
||||
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)"
|
||||
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)"
|
||||
by (simp add: corres_underlyingK_def)+
|
||||
|
|
@ -41,7 +41,7 @@ lemma mapME_x_corresK_inv:
|
|||
show ?case
|
||||
apply (simp add: mapME_x_def sequenceE_x_def)
|
||||
apply (fold mapME_x_def sequenceE_x_def dc_def)
|
||||
apply (corressimp corresK: x IH wp: y)
|
||||
apply (corresKsimp corresK: x IH wp: y)
|
||||
done
|
||||
qed
|
||||
done
|
||||
|
|
@ -141,7 +141,7 @@ lemma corresK_mapM_list_all2:
|
|||
lemma corresK_discard_rv:
|
||||
assumes A[corresK]: "corres_underlyingK sr nf nf' F r' P P' a c"
|
||||
shows "corres_underlyingK sr nf nf' F dc P P' (do x \<leftarrow> a; return () od) (do x \<leftarrow> c; return () od)"
|
||||
by corressimp
|
||||
by corresKsimp
|
||||
|
||||
lemma corresK_mapM_mapM_x:
|
||||
assumes "corres_underlyingK sr nf nf' F r' P P' (mapM f as) (mapM f' cs)"
|
||||
|
|
@ -163,12 +163,12 @@ lemma corresK_subst_both: "g' = f' \<Longrightarrow> g = f \<Longrightarrow>
|
|||
|
||||
lemma if_fun_true: "(if A then B else (\<lambda>_. True)) = (\<lambda>s. (A \<longrightarrow> B s))" by simp
|
||||
|
||||
lemmas corresK_whenE [corres_splits] =
|
||||
lemmas corresK_whenE [corresK_splits] =
|
||||
corresK_if[THEN
|
||||
corresK_subst_both[OF whenE_def[THEN meta_eq_to_obj_eq] whenE_def[THEN meta_eq_to_obj_eq]],
|
||||
OF _ corresK_returnOk[where r="f \<oplus> dc" for f], simplified, simplified if_fun_true]
|
||||
|
||||
lemmas corresK_head_splits[corres_splits] =
|
||||
lemmas corresK_head_splits[corresK_splits] =
|
||||
corresK_split[where d="return", simplified]
|
||||
corresK_splitE[where d="returnOk", simplified]
|
||||
corresK_split[where b="return", simplified]
|
||||
|
|
@ -192,7 +192,7 @@ lemmas [corresK] =
|
|||
corresK_Id[where nf'=True and r="(=)", simplified]
|
||||
corresK_Id[where nf'=True, simplified]
|
||||
|
||||
lemma corresK_unit_rv_eq_any[corres_concrete_r]:
|
||||
lemma corresK_unit_rv_eq_any[corresK_concrete_r]:
|
||||
"corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
|
||||
corres_underlyingK sr nf nf' F
|
||||
(\<lambda>(x :: unit) (y :: unit). x = y) P P' f f'"
|
||||
|
|
@ -201,7 +201,7 @@ lemma corresK_unit_rv_eq_any[corres_concrete_r]:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma corresK_unit_rv_dc_any[corres_concrete_r]:
|
||||
lemma corresK_unit_rv_dc_any[corresK_concrete_r]:
|
||||
"corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
|
||||
corres_underlyingK sr nf nf' F
|
||||
(\<lambda>(x :: unit) (y :: unit). dc x y) P P' f f'"
|
||||
|
|
|
|||
|
|
@ -4,11 +4,20 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*)
|
||||
|
||||
theory Corres_Method
|
||||
theory CorresK_Method
|
||||
imports Corres_Cases SpecValid_R
|
||||
begin
|
||||
|
||||
chapter \<open>Corres Methods\<close>
|
||||
(* Advanced Eisbach example for automating corres proofs via a new corresK calculus that improves
|
||||
on some of properties that are problematic for automation in the original corres calculus.
|
||||
|
||||
See also section 7.3 in
|
||||
|
||||
Daniel Matichuk: Automation for proof engineering: Machine-checked proofs at scale,
|
||||
PhD thesis, UNSW 2018. https://trustworthy.systems/publications/papers/Matichuk%3Aphd.abstract
|
||||
*)
|
||||
|
||||
chapter \<open>CorresK Methods\<close>
|
||||
|
||||
section \<open>Boilerplate\<close>
|
||||
|
||||
|
|
@ -112,7 +121,7 @@ private definition "my_false s \<equiv> False"
|
|||
private
|
||||
lemma corres_my_falseE: "my_false x \<Longrightarrow> P" by (simp add: my_false_def)
|
||||
|
||||
method no_schematic_prems = (fails \<open>erule corres_my_falseE\<close>)
|
||||
private method no_schematic_prems = (fails \<open>erule corres_my_falseE\<close>)
|
||||
|
||||
private lemma hoare_pre: "\<lbrace>my_false\<rbrace> f \<lbrace>Q\<rbrace>" by (simp add: valid_def my_false_def)
|
||||
private lemma hoareE_pre: "\<lbrace>my_false\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>Q'\<rbrace>" by (simp add: validE_def valid_def my_false_def)
|
||||
|
|
@ -134,7 +143,7 @@ private
|
|||
by (auto simp add: corres_my_false corres_underlyingK_def)
|
||||
|
||||
|
||||
method corres_raw_pre =
|
||||
method corresK_raw_pre =
|
||||
(check_corres, (fails \<open>rule corres_my_false\<close>, rule corresK_start)?)
|
||||
|
||||
lemma corresK_weaken_states:
|
||||
|
|
@ -156,7 +165,7 @@ method corresK_pre =
|
|||
((succeeds \<open>rule corresK_my_falseF\<close>, rule corresK_weaken_states) |
|
||||
rule corresK_weaken)))
|
||||
|
||||
method corres_pre' = (corres_raw_pre | corresK_pre)?
|
||||
method corresK_pre' = (corresK_raw_pre | corresK_pre)?
|
||||
|
||||
lemma corresK_weakenK:
|
||||
"corres_underlyingK sr nf nf' F' r P P' f f' \<Longrightarrow> (F \<Longrightarrow> F') \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f f'"
|
||||
|
|
@ -165,7 +174,7 @@ lemma corresK_weakenK:
|
|||
(* Special corres rules which should only be applied when the return value relation is
|
||||
concrete, to avoid bare schematics. *)
|
||||
|
||||
named_theorems corres_concrete_r and corres_concrete_rER
|
||||
named_theorems corresK_concrete_r and corresK_concrete_rER
|
||||
|
||||
private lemma corres_r_False:
|
||||
"False \<Longrightarrow> corres_underlyingK sr nf nf' F (\<lambda>_. my_false) P P' f f'"
|
||||
|
|
@ -179,18 +188,18 @@ private lemma corres_r_FalseE':
|
|||
"False \<Longrightarrow> corres_underlyingK sr nf nf' F (r \<oplus> (\<lambda>_. my_false)) P P' f f'"
|
||||
by simp
|
||||
|
||||
method corres_concrete_r declares corres_concrete_r corres_concrete_rER =
|
||||
(fails \<open>rule corres_r_False corres_r_FalseE corres_r_FalseE'\<close>, determ \<open>rule corres_concrete_r\<close>)
|
||||
| (fails \<open>rule corres_r_FalseE\<close>, determ \<open>rule corres_concrete_rER\<close>)
|
||||
method corresK_concrete_r declares corresK_concrete_r corresK_concrete_rER =
|
||||
(fails \<open>rule corres_r_False corres_r_FalseE corres_r_FalseE'\<close>, determ \<open>rule corresK_concrete_r\<close>)
|
||||
| (fails \<open>rule corres_r_FalseE\<close>, determ \<open>rule corresK_concrete_rER\<close>)
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
||||
section \<open>Corresc - Corres over case statements\<close>
|
||||
section \<open>CorresKc - Corres over case statements\<close>
|
||||
|
||||
text
|
||||
\<open>Based on wpc, corresc examines the split rule for top-level case statements on the left
|
||||
\<open>Based on wpc, corresKc examines the split rule for top-level case statements on the left
|
||||
and right hand sides, propagating backwards the stateless and left/right preconditions.\<close>
|
||||
|
||||
definition
|
||||
|
|
@ -232,7 +241,7 @@ text \<open>
|
|||
context
|
||||
begin
|
||||
|
||||
private method corresc_body for B :: bool uses helper =
|
||||
private method corresKc_body for B :: bool uses helper =
|
||||
determ \<open>(rule wpc2_helperI,
|
||||
repeat_new \<open>rule wpc2_conj_process wpc2_all_process wpc2_imp_process[where B=B]\<close> ; (rule helper))\<close>
|
||||
|
||||
|
|
@ -241,20 +250,20 @@ lemma wpc2_helper_corres_left:
|
|||
wpc2_helper (P, P') (Q, Q') (\<lambda>_. PP,PP') (\<lambda>_. QQ,QQ') (corres_underlyingK sr nf nf' PP r P A f f')"
|
||||
by (clarsimp simp: wpc2_helper_def corres_underlyingK_def elim!: corres_guard_imp)
|
||||
|
||||
private method corresc_left_raw =
|
||||
private method corresKc_left_raw =
|
||||
determ \<open>(match conclusion in "corres_underlyingK sr nf nf' F r P P' f f'" for sr nf nf' F r P P' f f'
|
||||
\<Rightarrow> \<open>apply_split f "\<lambda>f. corres_underlyingK sr nf nf' F r P P' f f'"\<close>,
|
||||
corresc_body False helper: wpc2_helper_corres_left)\<close>
|
||||
corresKc_body False helper: wpc2_helper_corres_left)\<close>
|
||||
|
||||
lemma wpc2_helper_corres_right:
|
||||
"corres_underlyingK sr nf nf' QQ r A Q f f' \<Longrightarrow>
|
||||
wpc2_helper (P, P') (Q, Q') (\<lambda>_. PP,PP') (\<lambda>_. QQ,QQ') (corres_underlyingK sr nf nf' PP r A P f f')"
|
||||
by (clarsimp simp: wpc2_helper_def corres_underlyingK_def elim!: corres_guard_imp)
|
||||
|
||||
private method corresc_right_raw =
|
||||
private method corresKc_right_raw =
|
||||
determ \<open>(match conclusion in "corres_underlyingK sr nf nf' F r P P' f f'" for sr nf nf' F r P P' f f'
|
||||
\<Rightarrow> \<open>apply_split f' "\<lambda>f'. corres_underlyingK sr nf nf' F r P P' f f'"\<close>,
|
||||
corresc_body True helper: wpc2_helper_corres_right)\<close>
|
||||
corresKc_body True helper: wpc2_helper_corres_right)\<close>
|
||||
|
||||
definition
|
||||
"corres_protect r = (r :: bool)"
|
||||
|
|
@ -267,13 +276,13 @@ lemma wpc2_corres_protect:
|
|||
"wpc2_protect B Q \<Longrightarrow> corres_protect Q"
|
||||
by (simp add: wpc2_protect_def corres_protect_def)
|
||||
|
||||
method corresc_left = (corresc_left_raw; (drule wpc2_corres_protect[where B=False]))
|
||||
method corresc_right = (corresc_right_raw; (drule wpc2_corres_protect[where B=True]))
|
||||
method corresKc_left = (corresKc_left_raw; (drule wpc2_corres_protect[where B=False]))
|
||||
method corresKc_right = (corresKc_right_raw; (drule wpc2_corres_protect[where B=True]))
|
||||
|
||||
named_theorems corresc_simp
|
||||
named_theorems corresKc_simp
|
||||
|
||||
declare wpc2_protect_def[corresc_simp]
|
||||
declare corres_protect_def[corresc_simp]
|
||||
declare wpc2_protect_def[corresKc_simp]
|
||||
declare corres_protect_def[corresKc_simp]
|
||||
|
||||
lemma corresK_false_guard_instantiate:
|
||||
"False \<Longrightarrow> corres_underlyingK sr nf nf' True r P P' f f'"
|
||||
|
|
@ -284,22 +293,22 @@ lemma
|
|||
"wpc2_protect False (A = B) \<Longrightarrow> wpc2_protect True (A = C) \<Longrightarrow> B \<noteq> C \<Longrightarrow> P"
|
||||
by (auto simp: wpc2_protect_def)
|
||||
|
||||
method corresc declares corresc_simp =
|
||||
(check_corresK, corresc_left_raw; corresc_right_raw;
|
||||
method corresKc declares corresKc_simp =
|
||||
(check_corresK, corresKc_left_raw; corresKc_right_raw;
|
||||
((solves \<open>rule corresK_false_guard_instantiate,
|
||||
determ \<open>(erule (1) wpc_contr_helper)?\<close>, simp add: corresc_simp\<close>)
|
||||
determ \<open>(erule (1) wpc_contr_helper)?\<close>, simp add: corresKc_simp\<close>)
|
||||
| (drule wpc2_corres_protect[where B=False], drule wpc2_corres_protect[where B=True])))[1]
|
||||
|
||||
end
|
||||
|
||||
section \<open>Corres_rv\<close>
|
||||
section \<open>CorresK_rv\<close>
|
||||
|
||||
text \<open>Corres_rv is used to propagate backwards the stateless precondition (F) from corres_underlyingK.
|
||||
It's main purpose is to defer the decision of where each condition should go: either continue
|
||||
text \<open>CorresK_rv is used to propagate backwards the stateless precondition (F) from corres_underlyingK.
|
||||
Its main purpose is to defer the decision of where each condition should go: either continue
|
||||
through the stateless precondition, or be pushed into the left/right side as a hoare triple.\<close>
|
||||
|
||||
|
||||
(*Don't unfold the definition. Use corres_rv method or associated rules. *)
|
||||
(*Don't unfold the definition. Use corresK_rv method or associated rules. *)
|
||||
definition corres_rv :: "bool \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('t \<Rightarrow> bool)
|
||||
\<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('t, 'b) nondet_monad \<Rightarrow>
|
||||
('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
|
|
@ -308,7 +317,7 @@ definition corres_rv :: "bool \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> b
|
|||
F \<longrightarrow> (\<forall>s s'. P s \<longrightarrow> P' s' \<longrightarrow>
|
||||
(\<forall>sa rv. (rv, sa) \<in> fst (f s) \<longrightarrow> (\<forall>sa' rv'. (rv', sa') \<in> fst (f' s') \<longrightarrow> r rv rv' \<longrightarrow> Q rv rv')))"
|
||||
|
||||
(*Don't unfold the definition. Use corres_rv method or associated rules. *)
|
||||
(*Don't unfold the definition. Use corresK_rv method or associated rules. *)
|
||||
definition "corres_rvE_R F r P P' f f' Q \<equiv>
|
||||
corres_rv F (\<lambda>_ _. True) P P' f f'
|
||||
(\<lambda>rvE rvE'. case (rvE,rvE') of (Inr rv, Inr rv') \<Rightarrow> r rv rv' \<longrightarrow> Q rv rv' | _ \<Rightarrow> True)"
|
||||
|
|
@ -403,9 +412,9 @@ lemma corres_rvE_R_conj_lift:
|
|||
corres_rvE_R (F \<and> F') r (\<lambda>s. P s \<and> P' s) (\<lambda>s'. PP s' \<and> PP' s') f g (\<lambda>rv rv'. Q rv rv' \<and> Q' rv rv')"
|
||||
by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits)
|
||||
|
||||
subsection \<open>Corres_rv method\<close>
|
||||
subsection \<open>CorresK_rv method\<close>
|
||||
|
||||
text \<open>This method propagate corres_rv obligations into each precondition according to the following
|
||||
text \<open>This method propagate corresK_rv obligations into each precondition according to the following
|
||||
heuristic:
|
||||
For each conjunct in the obligation:
|
||||
|
||||
|
|
@ -475,7 +484,7 @@ lemmas corres_rv_lifts =
|
|||
lemmas corres_rv_prove_simple =
|
||||
corres_rv_proveT[# \<open>thin_tac _, thin_tac _\<close>, simplified]
|
||||
|
||||
method corres_rv =
|
||||
method corresK_rv =
|
||||
(((repeat_new \<open>rule corres_rv_trivials corres_rv_lifts\<close>)?);
|
||||
((rule corres_rv_trivials corres_rv_defers corres_rv_noops |
|
||||
(succeeds \<open>rule corres_rv_defer_left corres_rvE_R_defer_left\<close>,
|
||||
|
|
@ -491,7 +500,7 @@ section \<open>CorresK Split rules\<close>
|
|||
text \<open>
|
||||
The corresK split allows preconditions to be propagated backward via the extra stateless precondition
|
||||
(here given as @{term F}. The head function is propagated backward directly, while the tail
|
||||
is propagated via corres_rv. Using the corres_rv method, this condition is then decomposed and
|
||||
is propagated via corres_rv. Using the corresK_rv method, this condition is then decomposed and
|
||||
pushed into the stateless, left, and right preconditions as appropriate.
|
||||
|
||||
The return value relation is now almost never needed directly, and so it is wrapped in corres_protect
|
||||
|
|
@ -531,7 +540,7 @@ lemma corresK_split:
|
|||
apply clarsimp
|
||||
done
|
||||
|
||||
section \<open>Corres_inst\<close>
|
||||
section \<open>CorresK_inst\<close>
|
||||
|
||||
text \<open>Handles rare in-place subgoals generated by corres rules which need to be solved immediately
|
||||
in order to instantiate a schematic.
|
||||
|
|
@ -544,19 +553,19 @@ lemma corres_inst_eqI[wp]: "corres_inst_eq x x" by (simp add: corres_inst_eq_def
|
|||
|
||||
lemma corres_inst_test: "False \<Longrightarrow> corres_inst_eq x y" by simp
|
||||
|
||||
method corres_inst =
|
||||
method corresK_inst =
|
||||
(succeeds \<open>rule corres_inst_test\<close>, fails \<open>rule TrueI\<close>,
|
||||
(rule corres_inst_eqI |
|
||||
(clarsimp simp: corres_protect_def split del: if_split, rule corres_inst_eqI)
|
||||
| (clarsimp simp: corres_protect_def split del: if_split,
|
||||
fastforce intro!: corres_inst_eqI)))[1]
|
||||
|
||||
section \<open>Corres Method\<close>
|
||||
section \<open>CorresK Method\<close>
|
||||
|
||||
text \<open>Handles structured decomposition of corres goals\<close>
|
||||
|
||||
named_theorems
|
||||
corres_splits and (* rules that, one applied, must
|
||||
corresK_splits and (* rules that, one applied, must
|
||||
eventually yield a successful corres or corresK rule application*)
|
||||
corres_simp_del and (* bad simp rules that break everything *)
|
||||
corres and (* solving terminal corres subgoals *)
|
||||
|
|
@ -564,15 +573,15 @@ named_theorems
|
|||
|
||||
context begin
|
||||
|
||||
lemma corres_fold_dc:
|
||||
lemma corresK_fold_dc:
|
||||
"corres_underlyingK sr nf nf' F dc P P' f f' \<Longrightarrow> corres_underlyingK sr nf nf' F (\<lambda>_ _. True) P P' f f'"
|
||||
by (simp add: dc_def[abs_def])
|
||||
|
||||
private method corres_fold_dc =
|
||||
private method corresK_fold_dc =
|
||||
(match conclusion in
|
||||
"corres_underlyingK _ _ _ _ (\<lambda>_ _. True) _ _ _ _" \<Rightarrow> \<open>rule corres_fold_dc\<close>)
|
||||
"corres_underlyingK _ _ _ _ (\<lambda>_ _. True) _ _ _ _" \<Rightarrow> \<open>rule corresK_fold_dc\<close>)
|
||||
|
||||
section \<open>Corres_apply method\<close>
|
||||
section \<open>CorresK_apply method\<close>
|
||||
|
||||
text \<open>This is a private method that performs an in-place rewrite of corres rules into
|
||||
corresK rules. This is primarily for backwards-compatibility with the existing corres proofs.
|
||||
|
|
@ -594,45 +603,45 @@ private lemma guard_collect: "guard_collect F \<Longrightarrow> F"
|
|||
private lemma has_guard: "maybe_guard F" by (simp add: maybe_guard_def)
|
||||
private lemma no_guard: "maybe_guard True" by (simp add: maybe_guard_def)
|
||||
|
||||
private method corres_apply =
|
||||
private method corresK_apply =
|
||||
(rule corresK_assume_guard_guarded,
|
||||
(determ \<open>rule corres\<close>, safe_fold_subgoals)[1],
|
||||
#break "corres_apply",
|
||||
((focus_concl \<open>(atomize (full))?\<close>, erule guard_collect, rule has_guard) | rule no_guard))[1]
|
||||
|
||||
private method corres_alternate = corres_inst | corres_rv
|
||||
private method corresK_alternate = corresK_inst | corresK_rv
|
||||
|
||||
|
||||
|
||||
method corres_once declares corres_splits corres corresK corresc_simp =
|
||||
method corresK_once declares corresK_splits corres corresK corresKc_simp =
|
||||
(no_schematic_concl,
|
||||
(corres_alternate |
|
||||
(corres_fold_dc?,
|
||||
(corres_pre',
|
||||
(corresK_alternate |
|
||||
(corresK_fold_dc?,
|
||||
(corresK_pre',
|
||||
#break "corres",
|
||||
( (check_corresK, determ \<open>rule corresK\<close>)
|
||||
| corres_apply
|
||||
| corres_concrete_r
|
||||
| corresc
|
||||
| (rule corres_splits, corres_once)
|
||||
| corresK_apply
|
||||
| corresK_concrete_r
|
||||
| corresKc
|
||||
| (rule corresK_splits, corresK_once)
|
||||
)))))
|
||||
|
||||
|
||||
method corres declares corres_splits corres corresK corresc_simp =
|
||||
(corres_once+)[1]
|
||||
method corresK declares corresK_splits corres corresK corresKc_simp =
|
||||
(corresK_once+)[1]
|
||||
|
||||
text \<open>Unconditionally try applying split rules. Useful for determining why corres is not applying
|
||||
in a given proof.\<close>
|
||||
|
||||
method corres_unsafe_split declares corres_splits corres corresK corresc_simp =
|
||||
((rule corres_splits | corres_pre' | corres_once)+)[1]
|
||||
method corresK_unsafe_split declares corresK_splits corres corresK corresKc_simp =
|
||||
((rule corresK_splits | corresK_pre' | corresK_once)+)[1]
|
||||
|
||||
end
|
||||
|
||||
lemmas [corres_splits] =
|
||||
lemmas [corresK_splits] =
|
||||
corresK_split
|
||||
|
||||
lemma corresK_when [corres_splits]:
|
||||
lemma corresK_when [corresK_splits]:
|
||||
"\<lbrakk>corres_protect G \<Longrightarrow> corres_protect G' \<Longrightarrow> corres_underlyingK sr nf nf' F dc P P' a c\<rbrakk>
|
||||
\<Longrightarrow> corres_underlyingK sr nf nf' ((G = G') \<and> F) dc ((\<lambda>x. G \<longrightarrow> P x)) (\<lambda>x. G' \<longrightarrow> P' x) (when G a) (when G' c)"
|
||||
apply (simp add: corres_underlying_def corres_underlyingK_def corres_protect_def)
|
||||
|
|
@ -652,7 +661,7 @@ lemma corres_lift_to_K:
|
|||
corres_underlyingK sra nfa nf'a F ra Pa P'a fa f'a \<longrightarrow> corres_underlyingK sr nf nf' F r P P' f f'"
|
||||
by (simp add: corres_underlyingK_def)
|
||||
|
||||
lemmas [THEN iffD2, atomized, THEN corresK_lift_rule, rule_format, simplified o_def, corres_splits] =
|
||||
lemmas [THEN iffD2, atomized, THEN corresK_lift_rule, rule_format, simplified o_def, corresK_splits] =
|
||||
corres_liftE_rel_sum
|
||||
corres_liftM_simp
|
||||
corres_liftM2_simp
|
||||
|
|
@ -670,28 +679,28 @@ lemma corresK_subst_right: "g' = f' \<Longrightarrow>
|
|||
corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
|
||||
corres_underlyingK sr nf nf' F r P P' f g'" by simp
|
||||
|
||||
lemmas corresK_fun_app_left[corres_splits] = corresK_subst_left[OF fun_app_def[THEN meta_eq_to_obj_eq]]
|
||||
lemmas corresK_fun_app_right[corres_splits] = corresK_subst_right[OF fun_app_def[THEN meta_eq_to_obj_eq]]
|
||||
lemmas corresK_fun_app_left[corresK_splits] = corresK_subst_left[OF fun_app_def[THEN meta_eq_to_obj_eq]]
|
||||
lemmas corresK_fun_app_right[corresK_splits] = corresK_subst_right[OF fun_app_def[THEN meta_eq_to_obj_eq]]
|
||||
|
||||
lemmas corresK_Let_left[corres_splits] = corresK_subst_left[OF Let_def[THEN meta_eq_to_obj_eq]]
|
||||
lemmas corresK_Let_right[corres_splits] = corresK_subst_right[OF Let_def[THEN meta_eq_to_obj_eq]]
|
||||
lemmas corresK_Let_left[corresK_splits] = corresK_subst_left[OF Let_def[THEN meta_eq_to_obj_eq]]
|
||||
lemmas corresK_Let_right[corresK_splits] = corresK_subst_right[OF Let_def[THEN meta_eq_to_obj_eq]]
|
||||
|
||||
lemmas corresK_return_bind_left[corres_splits] = corresK_subst_left[OF return_bind]
|
||||
lemmas corresK_return_bind_right[corres_splits] = corresK_subst_right[OF return_bind]
|
||||
lemmas corresK_return_bind_left[corresK_splits] = corresK_subst_left[OF return_bind]
|
||||
lemmas corresK_return_bind_right[corresK_splits] = corresK_subst_right[OF return_bind]
|
||||
|
||||
lemmas corresK_liftE_bindE_left[corres_splits] = corresK_subst_left[OF liftE_bindE]
|
||||
lemmas corresK_liftE_bindE_right[corres_splits] = corresK_subst_right[OF liftE_bindE]
|
||||
lemmas corresK_liftE_bindE_left[corresK_splits] = corresK_subst_left[OF liftE_bindE]
|
||||
lemmas corresK_liftE_bindE_right[corresK_splits] = corresK_subst_right[OF liftE_bindE]
|
||||
|
||||
lemmas corresK_K_bind_left[corres_splits] =
|
||||
lemmas corresK_K_bind_left[corresK_splits] =
|
||||
corresK_subst_left[where g="K_bind f rv" and f="f" for f rv, # \<open>simp\<close>]
|
||||
|
||||
lemmas corresK_K_bind_right[corres_splits] =
|
||||
lemmas corresK_K_bind_right[corresK_splits] =
|
||||
corresK_subst_right[where g'="K_bind f' rv" and f'="f'" for f' rv, # \<open>simp\<close>]
|
||||
|
||||
|
||||
section \<open>Corres Search - find symbolic execution path that allows a given rule to be applied\<close>
|
||||
section \<open>CorresK Search - find symbolic execution path that allows a given rule to be applied\<close>
|
||||
|
||||
lemma corresK_if [corres_splits]:
|
||||
lemma corresK_if [corresK_splits]:
|
||||
"\<lbrakk>(corres_protect G \<Longrightarrow> corres_protect G' \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' a c);
|
||||
(corres_protect (\<not>G) \<Longrightarrow> corres_protect (\<not>G') \<Longrightarrow> corres_underlyingK sr nf nf' F' r Q Q' b d)\<rbrakk>
|
||||
\<Longrightarrow> corres_underlyingK sr nf nf' ((G = G') \<and> (G \<longrightarrow> F) \<and> (\<not>G \<longrightarrow> F')) r (if G then P else Q) (if G' then P' else Q') (if G then a else b)
|
||||
|
|
@ -707,9 +716,9 @@ lemma corresK_if_rev:
|
|||
|
||||
|
||||
|
||||
named_theorems corres_symb_exec_ls and corres_symb_exec_rs
|
||||
named_theorems corresK_symb_exec_ls and corresK_symb_exec_rs
|
||||
|
||||
lemma corresK_symb_exec_l_search[corres_symb_exec_ls]:
|
||||
lemma corresK_symb_exec_l_search[corresK_symb_exec_ls]:
|
||||
fixes x :: "'b \<Rightarrow> 'a \<Rightarrow> ('d \<times> 'a) set \<times> bool"
|
||||
notes [simp] = corres_noop_def
|
||||
shows
|
||||
|
|
@ -743,10 +752,10 @@ lemma corresK_symb_exec_l_search[corres_symb_exec_ls]:
|
|||
done
|
||||
|
||||
|
||||
lemmas corresK_symb_exec_liftME_l_search[corres_symb_exec_ls] =
|
||||
lemmas corresK_symb_exec_liftME_l_search[corresK_symb_exec_ls] =
|
||||
corresK_symb_exec_l_search[where 'd="'x + 'y", folded liftE_bindE]
|
||||
|
||||
lemma corresK_symb_exec_r_search[corres_symb_exec_rs]:
|
||||
lemma corresK_symb_exec_r_search[corresK_symb_exec_rs]:
|
||||
fixes y :: "'b \<Rightarrow> 'a \<Rightarrow> ('e \<times> 'a) set \<times> bool"
|
||||
assumes X: "\<And>s. \<lbrace>PP' s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
|
||||
assumes corres: "\<And>rv. corres_underlyingK sr nf nf' (F rv) r P (Q' rv) x (y rv)"
|
||||
|
|
@ -781,12 +790,12 @@ lemma corresK_symb_exec_r_search[corres_symb_exec_rs]:
|
|||
apply (rule no_failD[OF nf],simp+)
|
||||
done
|
||||
|
||||
lemmas corresK_symb_exec_liftME_r_search[corres_symb_exec_rs] =
|
||||
lemmas corresK_symb_exec_liftME_r_search[corresK_symb_exec_rs] =
|
||||
corresK_symb_exec_r_search[where 'e="'x + 'y", folded liftE_bindE]
|
||||
|
||||
context begin
|
||||
|
||||
private method corres_search_wp = solves \<open>((wp | wpc | simp)+)[1]\<close>
|
||||
private method corresK_search_wp = solves \<open>((wp | wpc | simp)+)[1]\<close>
|
||||
|
||||
text \<open>
|
||||
Depth-first search via symbolic execution of both left and right hand
|
||||
|
|
@ -802,14 +811,14 @@ text \<open>
|
|||
\<close>
|
||||
|
||||
|
||||
private method corres_search_frame methods m uses search =
|
||||
(#break "corres_search",
|
||||
((corres?, corres_once corres: search corresK:search)
|
||||
| (corresc, find_goal \<open>m\<close>)[1]
|
||||
private method corresK_search_frame methods m uses search =
|
||||
(#break "corresK_search",
|
||||
((corresK?, corresK_once corres: search corresK:search)
|
||||
| (corresKc, find_goal \<open>m\<close>)[1]
|
||||
| (rule corresK_if, find_goal \<open>m\<close>)[1]
|
||||
| (rule corresK_if_rev, find_goal \<open>m\<close>)[1]
|
||||
| (rule corres_symb_exec_ls, corres_search_wp, m)
|
||||
| (rule corres_symb_exec_rs, corres_search_wp, m)))
|
||||
| (rule corresK_symb_exec_ls, corresK_search_wp, m)
|
||||
| (rule corresK_symb_exec_rs, corresK_search_wp, m)))
|
||||
|
||||
text \<open>
|
||||
Set up local context where we make sure we don't know how to
|
||||
|
|
@ -817,11 +826,11 @@ text \<open>
|
|||
make corres progress once we add our rule back in
|
||||
\<close>
|
||||
|
||||
method corres_search uses search
|
||||
declares corres corres_symb_exec_ls corres_symb_exec_rs =
|
||||
(corres_pre',
|
||||
use search[corres del] search[corresK del] search[corres_splits del] in
|
||||
\<open>use in \<open>corres_search_frame \<open>corres_search search: search\<close> search: search\<close>\<close>)[1]
|
||||
method corresK_search uses search
|
||||
declares corres corresK_symb_exec_ls corresK_symb_exec_rs =
|
||||
(corresK_pre',
|
||||
use search[corres del] search[corresK del] search[corresK_splits del] in
|
||||
\<open>use in \<open>corresK_search_frame \<open>corresK_search search: search\<close> search: search\<close>\<close>)[1]
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -838,15 +847,15 @@ lemma corres_stateAssert_implied_frame:
|
|||
shows
|
||||
"corres_underlyingK sr nf nf' (F \<and> F') r (P and P') (Q and Q') f (stateAssert A [] >>= g)"
|
||||
apply (clarsimp simp: bind_assoc stateAssert_def)
|
||||
apply (corres_search search: C[THEN corresK_unlift])
|
||||
apply (corresK_search search: C[THEN corresK_unlift])
|
||||
apply (wp corres_rv_defer | simp add: A)+
|
||||
done
|
||||
|
||||
lemma corresK_return [corres_concrete_r]:
|
||||
lemma corresK_return [corresK_concrete_r]:
|
||||
"corres_underlyingK sr nf nf' (r a b) r \<top> \<top> (return a) (return b)"
|
||||
by (simp add: corres_underlyingK_def)
|
||||
|
||||
lemma corres_throwError_str [corres_concrete_rER]:
|
||||
lemma corres_throwError_str [corresK_concrete_rER]:
|
||||
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)"
|
||||
by (simp add: corres_underlyingK_def)+
|
||||
|
||||
|
|
@ -854,7 +863,7 @@ section \<open>Error Monad\<close>
|
|||
|
||||
|
||||
|
||||
lemma corresK_splitE [corres_splits]:
|
||||
lemma corresK_splitE [corresK_splits]:
|
||||
assumes x: "corres_underlyingK sr nf nf' F (f \<oplus> r') P P' a c"
|
||||
assumes y: "\<And>rv rv'. corres_protect (r' rv rv') \<Longrightarrow> corres_underlyingK sr nf nf' (F' rv rv') (f \<oplus> r) (R rv) (R' rv') (b rv) (d rv')"
|
||||
assumes c: "corres_rvE_R F'' r' PP PP' a c F'"
|
||||
|
|
@ -885,7 +894,7 @@ lemma corresK_splitE [corres_splits]:
|
|||
apply (insert z)
|
||||
by ((fastforce simp: valid_def validE_def validE_R_def split: sum.splits)+)
|
||||
|
||||
lemma corresK_returnOk [corres_concrete_r]:
|
||||
lemma corresK_returnOk [corresK_concrete_r]:
|
||||
"corres_underlyingK sr nf nf' (r (Inr a) (Inr b)) r \<top> \<top> (returnOk a) (returnOk b)"
|
||||
by (simp add: returnOk_def corres_underlyingK_def)
|
||||
|
||||
|
|
@ -893,7 +902,7 @@ lemma corres_assertE_str[corresK]:
|
|||
"corres_underlyingK sr nf nf' ((nf' \<longrightarrow> Q) \<and> P) (f \<oplus> dc) \<top> \<top> (assertE P) (assertE Q)"
|
||||
by (auto simp add: corres_underlying_def corres_underlyingK_def returnOk_def return_def assertE_def fail_def)
|
||||
|
||||
lemmas corres_symb_exec_whenE_l_search[corres_symb_exec_ls] =
|
||||
lemmas corres_symb_exec_whenE_l_search[corresK_symb_exec_ls] =
|
||||
corresK_symb_exec_l_search[where 'd="'x + 'y", folded liftE_bindE]
|
||||
|
||||
lemmas corres_returnOk_liftEs
|
||||
|
|
@ -913,7 +922,7 @@ lemma corresK_fail_no_fail'[corresK]:
|
|||
apply (simp add: corres_underlyingK_def)
|
||||
by (fastforce intro!: corres_fail)
|
||||
|
||||
section \<open>Correswp\<close>
|
||||
section \<open>CorresKwp\<close>
|
||||
|
||||
text
|
||||
\<open>This method wraps up wp and wpc to ensure that they don't accidentally generate schematic
|
||||
|
|
@ -925,40 +934,40 @@ text
|
|||
To solve this, instead of meta-implication in the wp_comb rules we use corres_inst_eq, which
|
||||
can only be solved by reflexivity. In most cases these comb rules are either never applied or
|
||||
solved trivially. If users manually apply corres_rv rules to create postconditions with
|
||||
inaccessible meta-variables (@{method corres_rv} will never do this), then these rules will
|
||||
be used. Since @{method corres_inst} has access to the protected return-value relation, it has a chance
|
||||
inaccessible meta-variables (@{method corresK_rv} will never do this), then these rules will
|
||||
be used. Since @{method corresK_inst} has access to the protected return-value relation, it has a chance
|
||||
to unify the generated precondition with the original schematic one.\<close>
|
||||
|
||||
named_theorems correswp_wp_comb and correswp_wp_comb_del
|
||||
named_theorems corresKwp_wp_comb and corresKwp_wp_comb_del
|
||||
|
||||
lemma corres_inst_eq_imp:
|
||||
"corres_inst_eq A B \<Longrightarrow> A \<longrightarrow> B" by (simp add: corres_inst_eq_def)
|
||||
|
||||
lemmas corres_hoare_pre = hoare_pre[# \<open>-\<close> \<open>atomize (full), rule allI, rule corres_inst_eq_imp\<close>]
|
||||
|
||||
method correswp uses wp =
|
||||
method corresKwp uses wp =
|
||||
(determ \<open>
|
||||
(fails \<open>schematic_hoare_pre\<close>, (wp add: wp | wpc))
|
||||
| (schematic_hoare_pre,
|
||||
(use correswp_wp_comb [wp_comb]
|
||||
correswp_wp_comb_del[wp_comb del]
|
||||
(use corresKwp_wp_comb [wp_comb]
|
||||
corresKwp_wp_comb_del[wp_comb del]
|
||||
hoare_pre[wp_pre del]
|
||||
corres_hoare_pre[wp_pre]
|
||||
in
|
||||
\<open>use in \<open>wp add: wp | wpc\<close>\<close>))\<close>)
|
||||
|
||||
lemmas [correswp_wp_comb_del] =
|
||||
lemmas [corresKwp_wp_comb_del] =
|
||||
hoare_vcg_precond_imp
|
||||
hoare_vcg_precond_impE
|
||||
hoare_vcg_precond_impE_R
|
||||
|
||||
lemma corres_inst_conj_lift[correswp_wp_comb]:
|
||||
lemma corres_inst_conj_lift[corresKwp_wp_comb]:
|
||||
"\<lbrakk>\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. corres_inst_eq (R s) (P s)\<rbrakk> \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
|
||||
by (rule hoare_vcg_conj_lift; simp add: valid_def corres_inst_eq_def)
|
||||
|
||||
lemmas [correswp_wp_comb] =
|
||||
correswp_wp_comb_del[# \<open>-\<close> \<open>atomize (full), rule allI, rule corres_inst_eq_imp\<close>]
|
||||
lemmas [corresKwp_wp_comb] =
|
||||
corresKwp_wp_comb_del[# \<open>-\<close> \<open>atomize (full), rule allI, rule corres_inst_eq_imp\<close>]
|
||||
valid_validE_R
|
||||
hoare_vcg_R_conj[OF valid_validE_R]
|
||||
hoare_vcg_E_elim[OF valid_validE_E]
|
||||
|
|
@ -969,10 +978,10 @@ lemmas [correswp_wp_comb] =
|
|||
hoare_vcg_E_conj
|
||||
hoare_vcg_conj_lift
|
||||
|
||||
declare hoare_post_comb_imp_conj[correswp_wp_comb_del]
|
||||
declare hoare_post_comb_imp_conj[corresKwp_wp_comb_del]
|
||||
|
||||
section \<open>Corressimp\<close>
|
||||
text \<open>Combines corres, wp and clarsimp\<close>
|
||||
section \<open>CorresKsimp\<close>
|
||||
text \<open>Combines corresK, wp and clarsimp\<close>
|
||||
|
||||
text
|
||||
\<open>If clarsimp solves a terminal subgoal, its preconditions are left uninstantiated. We can
|
||||
|
|
@ -995,14 +1004,14 @@ lemmas corresK_True_inst =
|
|||
|
||||
lemmas calculus_True_insts = hoare_True_inst corres_rv_True_inst corresK_True_inst
|
||||
|
||||
method corressimp uses simp cong search wp
|
||||
declares corres corresK corres_splits corresc_simp =
|
||||
method corresKsimp uses simp cong search wp
|
||||
declares corres corresK corresK_splits corresKc_simp =
|
||||
((no_schematic_concl,
|
||||
(corres corresc_simp: simp
|
||||
| correswp wp: wp
|
||||
(corresK corresKc_simp: simp
|
||||
| corresKwp wp: wp
|
||||
| (rule calculus_True_insts, solves \<open>clarsimp cong: cong simp: simp corres_protect_def\<close>)
|
||||
| clarsimp cong: cong simp: simp simp del: corres_simp_del split del: if_split
|
||||
| (match search in _ \<Rightarrow> \<open>corres_search search: search\<close>)))+)[1]
|
||||
| (match search in _ \<Rightarrow> \<open>corresK_search search: search\<close>)))+)[1]
|
||||
|
||||
declare corres_return[corres_simp_del]
|
||||
|
||||
|
|
@ -1060,7 +1069,7 @@ lemma use_corresK_frame_E_R:
|
|||
lemma K_True: "K True = (\<lambda>_. True)" by simp
|
||||
lemma True_And: "((\<lambda>_. True) and P) = P" by simp
|
||||
|
||||
method use_corres uses frame =
|
||||
method use_corresK uses frame =
|
||||
(corresK_convert?, drule use_corresK_frame use_corresK_frame_E_R, rule frame,
|
||||
(solves \<open>wp\<close> | defer_tac), (solves \<open>wp\<close> | defer_tac), (simp only: True_And K_True)?)
|
||||
|
||||
|
|
@ -1073,18 +1082,18 @@ experiment
|
|||
frameA: "\<forall>s s' rv rv'. (s,s') \<in> sr \<longrightarrow> r rv rv' \<longrightarrow> Q rv s \<longrightarrow> Q' rv' s' \<longrightarrow> QQ' rv' s'"
|
||||
begin
|
||||
|
||||
lemmas f_Q' = f_corres[atomized, @\<open>use_corres frame: frameA\<close>]
|
||||
lemmas f_Q' = f_corres[atomized, @\<open>use_corresK frame: frameA\<close>]
|
||||
|
||||
lemma "G \<Longrightarrow> F \<Longrightarrow> corres_underlying sr False True dc (P and PP) (P' and PP')
|
||||
(g >>= (K (f >>= K (assert True)))) (g' >>= (K (f' >>= (\<lambda>rv'. (stateAssert (QQ' rv') [])))))"
|
||||
apply (simp only: stateAssert_def K_def)
|
||||
apply corres
|
||||
apply (corres_search search: corresK_assert)
|
||||
apply corres_rv
|
||||
apply (correswp | simp)+
|
||||
apply corres_rv
|
||||
apply (correswp wp: f_Q' | simp)+
|
||||
apply corressimp+
|
||||
apply corresK
|
||||
apply (corresK_search search: corresK_assert)
|
||||
apply corresK_rv
|
||||
apply (corresKwp | simp)+
|
||||
apply corresK_rv
|
||||
apply (corresKwp wp: f_Q' | simp)+
|
||||
apply corresKsimp+
|
||||
by auto
|
||||
|
||||
end
|
||||
|
|
@ -42,7 +42,7 @@ text \<open>
|
|||
section \<open>Helper functions and definitions\<close>
|
||||
|
||||
(* The following three definitions are originally by Dan Matichuck from the Eisbach
|
||||
Corres_Method example *)
|
||||
CorresK_Method example *)
|
||||
|
||||
(* Retrieve a split rule for a target term that is expected to be a case statement. *)
|
||||
ML \<open>
|
||||
|
|
|
|||
4
lib/ROOT
4
lib/ROOT
|
|
@ -58,7 +58,7 @@ session Lib (lib) = Word_Lib +
|
|||
DataMap
|
||||
FastMap
|
||||
RangeMap
|
||||
Corres_Method
|
||||
CorresK_Method
|
||||
DetWPLib
|
||||
Guess_ExI
|
||||
GenericTag
|
||||
|
|
@ -125,7 +125,7 @@ session LibTest (lib) in test = Refine +
|
|||
MonadicRewrite_Test
|
||||
(* use virtual memory function as an example, only makes sense on ARM: *)
|
||||
theories [condition = "L4V_ARCH_IS_ARM"]
|
||||
Corres_Test
|
||||
CorresK_Test
|
||||
|
||||
session SepTactics (lib) in Hoare_Sep_Tactics = Sep_Algebra +
|
||||
theories
|
||||
|
|
|
|||
|
|
@ -8,15 +8,15 @@
|
|||
Test proofs for corres methods. Builds on AInvs image.
|
||||
*)
|
||||
|
||||
theory Corres_Test
|
||||
imports "Refine.VSpace_R" "Lib.Corres_Method"
|
||||
theory CorresK_Test
|
||||
imports "Refine.VSpace_R" "Lib.CorresK_Method"
|
||||
begin
|
||||
|
||||
chapter \<open>The Corres Method\<close>
|
||||
|
||||
section \<open>Introduction\<close>
|
||||
|
||||
text \<open>The @{method corres} method tries to do for corres-style refinement proofs what
|
||||
text \<open>The @{method corresK} method tries to do for corres-style refinement proofs what
|
||||
@{method wp} did for hoare logic proofs. The intention is to automate the application
|
||||
of corres calculational rules, so that the bulk of the manual proof is now handling
|
||||
a verification condition. In general refinement proofs are difficult to automate, so here we
|
||||
|
|
@ -83,16 +83,16 @@ of the functions. In essence, it states the given functions will establish @{ter
|
|||
assuming the given return-value relation @{term r} holds, along with the given stateless precondition
|
||||
@{term F} and left/right preconditions @{term P} and @{term P'}.
|
||||
|
||||
The assumption in general is that corres_rv rules should never be written, instead corres_rv obligations
|
||||
The assumption in general is that corresK_rv rules should never be written, instead corresK_rv obligations
|
||||
should be propagated into either the stateless precondition (@{term F} from @{term corres_underlyingK}),
|
||||
the left precondition (@{term P}) or the right precondition @{term P'}. This is implicitly handled
|
||||
by @{method corres_rv} (called from @{method corres}) by applying one of the following rules to each conjunct:\<close>
|
||||
by @{method corresK_rv} (called from @{method corresK}) by applying one of the following rules to each conjunct:\<close>
|
||||
|
||||
thm corres_rv_defer
|
||||
thm corres_rv_wp_left
|
||||
thm corres_rv_wp_right
|
||||
|
||||
text \<open>If none of these rules can be safely applied, then @{method corres_rv} will leave the
|
||||
text \<open>If none of these rules can be safely applied, then @{method corresK_rv} will leave the
|
||||
obligation untouched. The user can manually apply one of them if desired, but this is liable to
|
||||
create unsolvable proof obligations. In the worst case, the user may manually solve the goal in-place.\<close>
|
||||
|
||||
|
|
@ -105,7 +105,7 @@ text \<open>The core algorithm of the corres method is simple:
|
|||
2) apply a known @{thm corres} or @{thm corresK} rule (see next section)
|
||||
3) if unsuccessful, apply a split rule (i.e. @{thm corresK_split}) and go to 2
|
||||
|
||||
Importantly, @{method corres} will not split a goal if it ultimately is not able to apply at least
|
||||
Importantly, @{method corresK} will not split a goal if it ultimately is not able to apply at least
|
||||
one @{thm corres} or @{thm corresK} rule.
|
||||
\<close>
|
||||
|
||||
|
|
@ -125,45 +125,45 @@ thm corres
|
|||
|
||||
subsection \<open>The corresc method\<close>
|
||||
|
||||
text \<open>Similar to @{method wpc}, @{method corresc} can handle case statements in @{const corres_underlyingK}
|
||||
proof goals. Importantly, however, it is split into two sub-methods @{method corresc_left} and
|
||||
@{method corresc_right}, which perform case-splitting on each side respectively. The combined method
|
||||
@{method corresc}, however, attempts to discharge the contradictions that arise from the quadratic
|
||||
text \<open>Similar to @{method wpc}, @{method corresKc} can handle case statements in @{const corres_underlyingK}
|
||||
proof goals. Importantly, however, it is split into two sub-methods @{method corresKc_left} and
|
||||
@{method corresKc_right}, which perform case-splitting on each side respectively. The combined method
|
||||
@{method corresKc}, however, attempts to discharge the contradictions that arise from the quadratic
|
||||
blowup of a case analysis on both the left and right sides.\<close>
|
||||
|
||||
subsection \<open>corres_concrete_r, corres_concrete_rE\<close>
|
||||
|
||||
text \<open>Some @{thm corresK} rules should only be applied if certain variables are concrete
|
||||
(i.e. not schematic) in the goal. These are classified separately with the named_theorems
|
||||
@{thm corres_concrete_r} and @{thm corres_concrete_rER}. The first
|
||||
@{thm corresK_concrete_r} and @{thm corresK_concrete_rER}. The first
|
||||
indicates that the return value relation of the goal must be concrete, the second indicates that
|
||||
only the left side of the error relation must be concrete.\<close>
|
||||
|
||||
thm corres_concrete_r
|
||||
thm corres_concrete_rER
|
||||
thm corresK_concrete_r
|
||||
thm corresK_concrete_rER
|
||||
|
||||
subsection \<open>The corres_search method\<close>
|
||||
subsection \<open>The corresK_search method\<close>
|
||||
|
||||
text \<open>The purpose of @{method corres_search} is to address cases where there is non-trivial control flow.
|
||||
text \<open>The purpose of @{method corresK_search} is to address cases where there is non-trivial control flow.
|
||||
In particular: in the case where there is an "if" statement or either side needs to be symbolically
|
||||
executed. The core idea is that corres_search should be provided with a "search" rule that acts
|
||||
executed. The core idea is that corresK_search should be provided with a "search" rule that acts
|
||||
as an anchoring point. Symbolic execution and control flow is decomposed until either the given
|
||||
rule is successfully applied or all search branches are exhausted.\<close>
|
||||
|
||||
subsubsection \<open>Symbolic Execution\<close>
|
||||
|
||||
text \<open>Symbolic execution is handled by two named theorems:
|
||||
@{thm corres_symb_exec_ls} and @{thm corres_symb_exec_rs}, which perform symbolic execution on
|
||||
@{thm corresK_symb_exec_ls} and @{thm corresK_symb_exec_rs}, which perform symbolic execution on
|
||||
the left and right hand sides of a corres goal.\<close>
|
||||
|
||||
thm corres_symb_exec_ls
|
||||
thm corres_symb_exec_rs
|
||||
thm corresK_symb_exec_ls
|
||||
thm corresK_symb_exec_rs
|
||||
|
||||
text \<open>A function may be symbolically executed if it does not modify the state, i.e. its only purpose
|
||||
is to compute some value and return it. After being symbolically executed,
|
||||
this value can only be discussed by the precondition of the associated side or the stateless
|
||||
precondition of corresK. The resulting @{const corres_rv} goal has @{const corres_noop} as the
|
||||
function on the alternate side. This gives @{method corres_rv} a hint that the resulting obligation
|
||||
function on the alternate side. This gives @{method corresK_rv} a hint that the resulting obligation
|
||||
should be aggressively re-written into a hoare triple over @{term m} if it can't be propagated
|
||||
back statelessly safely.
|
||||
\<close>
|
||||
|
|
@ -198,7 +198,7 @@ lemma invalidateASIDEntry_corres:
|
|||
apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def)
|
||||
apply_debug (trace) (* apply_trace between steps *)
|
||||
(tags "corres") (* break at breakpoints labelled "corres" *)
|
||||
corres (* weaken precondition *)
|
||||
corresK (* weaken precondition *)
|
||||
continue (* split *)
|
||||
continue (* solve load_hw_asid *)
|
||||
continue (* split *)
|
||||
|
|
@ -207,7 +207,7 @@ lemma invalidateASIDEntry_corres:
|
|||
continue (* invalidate _hw_asid_entry *)
|
||||
finish (* invalidate_asid *)
|
||||
|
||||
apply (corressimp wp: load_hw_asid_wp)+
|
||||
apply (corresKsimp wp: load_hw_asid_wp)+
|
||||
apply (fastforce simp: pd_at_asid_uniq)
|
||||
done
|
||||
|
||||
|
|
@ -246,7 +246,7 @@ lemma delete_asid_corresb:
|
|||
apply (simp add: delete_asid_def deleteASID_def)
|
||||
apply_debug (trace) (* apply_trace between steps *)
|
||||
(tags "corres") (* break at breakpoints labelled "corres" *)
|
||||
corres (* weaken precondition *)
|
||||
corresK (* weaken precondition *)
|
||||
continue (* split *)
|
||||
continue (* gets rule *)
|
||||
continue (* corresc *)
|
||||
|
|
@ -278,7 +278,7 @@ lemma delete_asid_corresb:
|
|||
continue (* getCurThread_corres *)
|
||||
continue (* setVMRoot_corres *)
|
||||
finish (* backtracking? *)
|
||||
apply (corressimp simp: mask_asid_low_bits_ucast_ucast
|
||||
apply (corresKsimp simp: mask_asid_low_bits_ucast_ucast
|
||||
| fold cur_tcb_def | wps)+
|
||||
apply (frule arm_asid_table_related,clarsimp)
|
||||
apply (rule conjI)
|
||||
|
|
@ -343,7 +343,7 @@ lemma setVMRootForFlush_corres:
|
|||
(setVMRootForFlush pd asid)"
|
||||
apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
|
||||
apply corres
|
||||
apply_debug (trace) (tags "corres_search") (corres_search search: armv_contextSwitch_corres)
|
||||
apply_debug (trace) (tags "corresK_search") (corresK_search search: armv_contextSwitch_corres)
|
||||
continue (* step left *)
|
||||
continue (* if rule *)
|
||||
continue (* failed corres on first subgoal, trying next *)
|
||||
|
|
@ -351,7 +351,7 @@ lemma setVMRootForFlush_corres:
|
|||
continue (* can't make corres progress here, trying other goal *)
|
||||
finish (* successful goal discharged by corres *)
|
||||
|
||||
apply (corressimp wp: get_cap_wp getSlotCap_wp)+
|
||||
apply (corresKsimp wp: get_cap_wp getSlotCap_wp)+
|
||||
apply (rule context_conjI)
|
||||
subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def
|
||||
tcbVTableSlot_def to_bl_1 cte_level_bits_def)
|
||||
|
|
@ -368,7 +368,7 @@ lemma setVMRootForFlush_corres:
|
|||
apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation)
|
||||
done
|
||||
|
||||
text \<open>Note we can wrap it all up in corressimp\<close>
|
||||
text \<open>Note we can wrap it all up in corresKsimp\<close>
|
||||
|
||||
lemma setVMRootForFlush_corres':
|
||||
notes [corres] = getCurThread_corres getSlotCap_corres
|
||||
|
|
@ -385,7 +385,7 @@ lemma setVMRootForFlush_corres':
|
|||
(set_vm_root_for_flush pd asid)
|
||||
(setVMRootForFlush pd asid)"
|
||||
apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
|
||||
apply (corressimp search: armv_contextSwitch_corres
|
||||
apply (corresKsimp search: armv_contextSwitch_corres
|
||||
wp: get_cap_wp getSlotCap_wp
|
||||
simp: isCap_simps)
|
||||
apply (rule context_conjI)
|
||||
|
|
@ -721,7 +721,7 @@ lemma lookupPTSlot_corres:
|
|||
\<top>
|
||||
(gets_the (pt_lookup_slot pt vptr \<circ> ptes_of)) (lookupPTSlot pt vptr)"
|
||||
unfolding lookupPTSlot_def pt_lookup_slot_def
|
||||
by (corressimp corres: lookupPTSlotFromLevel_corres)
|
||||
by (corresKsimp corres: lookupPTSlotFromLevel_corres)
|
||||
|
||||
(* FIXME AARCH64: pt_lookup_from_level also returns a level on AARCH64, but lookupPTFromLevel doesn't
|
||||
there is no point fixing this lemma until we see what's needed in
|
||||
|
|
@ -801,7 +801,7 @@ next
|
|||
apply (simp add: unlessE_whenE not_less)
|
||||
apply (rule corres_gen_asm, simp)
|
||||
apply (rule corres_initial_splitE[where r'=dc])
|
||||
apply (corressimp simp: lookup_failure_map_def)
|
||||
apply (corresKsimp simp: lookup_failure_map_def)
|
||||
apply (rule corres_splitEE[where r'=pte_relation'])
|
||||
apply (simp, rule getObject_PTE_corres)
|
||||
apply (rule whenE_throwError_corres)
|
||||
|
|
|
|||
|
|
@ -843,14 +843,14 @@ lemma decodeARMVCPUInvocation_corres:
|
|||
apply (frule list_all2_Cons)
|
||||
apply clarsimp
|
||||
apply (case_tac a; clarsimp simp add: cap_relation_def)
|
||||
apply (corres corres: corres_returnOkTT)
|
||||
apply (corresK corres: corres_returnOkTT)
|
||||
apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def)
|
||||
(* inject_irq *)
|
||||
apply (simp add: decode_vcpu_inject_irq_def decodeVCPUInjectIRQ_def isVCPUCap_def)
|
||||
apply (cases args; clarsimp)
|
||||
apply (clarsimp simp add: rangeCheck_def range_check_def unlessE_whenE)
|
||||
apply (clarsimp simp: shiftL_nat whenE_bindE_throwError_to_if)
|
||||
apply (corressimp wp: get_vcpu_wp)
|
||||
apply (corresKsimp wp: get_vcpu_wp)
|
||||
apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def ucast_id
|
||||
valid_cap'_def valid_cap_def isVIRQActive_def is_virq_active_def
|
||||
virqType_def virq_type_def
|
||||
|
|
@ -1089,7 +1089,7 @@ lemma invokeVCPUInjectIRQ_corres:
|
|||
apply (clarsimp simp: bind_assoc)
|
||||
(* FIXME AARCH64 old proof worked with:
|
||||
|
||||
apply (corressimp corres: getObject_vcpu_corres setObject_VCPU_corres wp: get_vcpu_wp)
|
||||
apply (corresKsimp corres: getObject_vcpu_corres setObject_VCPU_corres wp: get_vcpu_wp)
|
||||
apply clarsimp
|
||||
|
||||
but now it doesn't, and not clear why
|
||||
|
|
@ -1107,8 +1107,8 @@ lemma invokeVCPUReadReg_corres:
|
|||
(invokeVCPUReadReg v r)"
|
||||
unfolding invoke_vcpu_read_register_def invokeVCPUReadReg_def read_vcpu_register_def readVCPUReg_def
|
||||
apply (rule corres_discard_r)
|
||||
sorry (* FIXME AARCH64 unclear why corressimp is failing
|
||||
apply (corressimp corres: getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
sorry (* FIXME AARCH64 unclear why corresKsimp is failing
|
||||
apply (corresKsimp corres: getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
apply (clarsimp simp: vcpu_relation_def split: option.splits)
|
||||
apply (wpsimp simp: getCurThread_def)+
|
||||
done *)
|
||||
|
|
@ -1122,8 +1122,8 @@ lemma invokeVCPUWriteReg_corres:
|
|||
unfolding invokeVCPUWriteReg_def invoke_vcpu_write_register_def write_vcpu_register_def
|
||||
writeVCPUReg_def
|
||||
apply (rule corres_discard_r)
|
||||
sorry (* FIXME AARCH64 unclear why corressimp is failing
|
||||
apply (corressimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
sorry (* FIXME AARCH64 unclear why corresKsimp is failing
|
||||
apply (corresKsimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
subgoal by (auto simp: vcpu_relation_def split: option.splits)
|
||||
apply (wpsimp simp: getCurThread_def)+
|
||||
done *)
|
||||
|
|
@ -1159,8 +1159,8 @@ lemma associateVCPUTCB_corres:
|
|||
(associateVCPUTCB v t)"
|
||||
unfolding associate_vcpu_tcb_def associateVCPUTCB_def
|
||||
apply (clarsimp simp: bind_assoc)
|
||||
sorry (* FIXME AARCH64 unclear why corressimp is failing
|
||||
apply (corressimp search: getObject_vcpu_corres setObject_VCPU_corres vcpuSwitch_corres''
|
||||
sorry (* FIXME AARCH64 unclear why corresKsimp is failing
|
||||
apply (corresKsimp search: getObject_vcpu_corres setObject_VCPU_corres vcpuSwitch_corres''
|
||||
wp: get_vcpu_wp getVCPU_wp hoare_vcg_imp_lift'
|
||||
simp: vcpu_relation_def)
|
||||
apply (rule_tac Q="\<lambda>_. invs and tcb_at t" in hoare_strengthen_post)
|
||||
|
|
@ -1181,7 +1181,7 @@ lemma associateVCPUTCB_corres:
|
|||
apply (simp add: valid_vcpu'_def typ_at_tcb')
|
||||
apply (clarsimp simp: typ_at_to_obj_at_arches obj_at'_def)
|
||||
apply (fastforce simp: typ_at_to_obj_at_arches obj_at'_def)
|
||||
apply (corressimp wp: arch_thread_get_wp getObject_tcb_wp
|
||||
apply (corresKsimp wp: arch_thread_get_wp getObject_tcb_wp
|
||||
simp: archThreadGet_def)+
|
||||
apply (simp add: vcpu_relation_def)
|
||||
apply (intro allI conjI impI;
|
||||
|
|
@ -1207,7 +1207,7 @@ lemma invokeVCPUAckVPPI_corres:
|
|||
(invokeVCPUAckVPPI vcpu vppi)"
|
||||
unfolding invokeVCPUAckVPPI_def invoke_vcpu_ack_vppi_def write_vcpu_register_def
|
||||
writeVCPUReg_def
|
||||
by (corressimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
by (corresKsimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
(auto simp: vcpu_relation_def split: option.splits)
|
||||
|
||||
lemma performARMVCPUInvocation_corres:
|
||||
|
|
|
|||
|
|
@ -1513,8 +1513,8 @@ lemma arch_postCapDeletion_corres:
|
|||
lemma postCapDeletion_corres:
|
||||
"cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')"
|
||||
apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def)
|
||||
apply (corressimp corres: deletedIRQHandler_corres)
|
||||
by (corressimp corres: arch_postCapDeletion_corres)
|
||||
apply (corresKsimp corres: deletedIRQHandler_corres)
|
||||
by (corresKsimp corres: arch_postCapDeletion_corres)
|
||||
|
||||
lemma set_cap_trans_state:
|
||||
"((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))"
|
||||
|
|
|
|||
|
|
@ -1410,7 +1410,7 @@ lemma archThreadGet_corres:
|
|||
corres (=) (tcb_at t and pspace_aligned and pspace_distinct) \<top>
|
||||
(arch_thread_get f t) (archThreadGet f' t)"
|
||||
unfolding arch_thread_get_def archThreadGet_def
|
||||
apply (corressimp corres: getObject_TCB_corres)
|
||||
apply (corresKsimp corres: getObject_TCB_corres)
|
||||
apply (clarsimp simp: tcb_relation_def)
|
||||
done
|
||||
|
||||
|
|
@ -1440,7 +1440,7 @@ lemma corres_gets_current_vcpu[corres]:
|
|||
lemma vcpuInvalidateActive_corres[corres]:
|
||||
"corres dc \<top> no_0_obj' vcpu_invalidate_active vcpuInvalidateActive"
|
||||
unfolding vcpuInvalidateActive_def vcpu_invalidate_active_def
|
||||
apply (corressimp corres: vcpuDisable_corres
|
||||
apply (corresKsimp corres: vcpuDisable_corres
|
||||
corresK: corresK_modifyT
|
||||
simp: modifyArchState_def)
|
||||
apply (clarsimp simp: state_relation_def arch_state_relation_def)
|
||||
|
|
@ -1455,7 +1455,7 @@ lemma archThreadSet_corres:
|
|||
corres dc (tcb_at t and pspace_aligned and pspace_distinct) \<top>
|
||||
(arch_thread_set f t) (archThreadSet f' t)"
|
||||
apply (simp add: arch_thread_set_def archThreadSet_def)
|
||||
apply (corres corres: getObject_TCB_corres setObject_update_TCB_corres')
|
||||
apply (corresK corres: getObject_TCB_corres setObject_update_TCB_corres')
|
||||
apply wpsimp+
|
||||
sorry (* FIXME AARCH64
|
||||
apply (auto simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+
|
||||
|
|
@ -1482,7 +1482,7 @@ lemma asUser_sanitiseRegister_corres[corres]:
|
|||
setRegister CPSR (sanitiseRegister b' CPSR cpsr)
|
||||
od))"
|
||||
unfolding sanitiseRegister_def sanitise_register_def
|
||||
apply (corressimp corresK: corresK_as_user')
|
||||
apply (corresKsimp corresK: corresK_as_user')
|
||||
done *)
|
||||
|
||||
crunch typ_at'[wp]: vcpuInvalidateActive "\<lambda>s. P (typ_at' T p s)"
|
||||
|
|
@ -1504,14 +1504,14 @@ lemma dissociateVCPUTCB_corres [@lift_corres_args, corres]:
|
|||
(dissociate_vcpu_tcb v t) (dissociateVCPUTCB v t)"
|
||||
unfolding dissociate_vcpu_tcb_def dissociateVCPUTCB_def
|
||||
apply (clarsimp simp: bind_assoc when_fail_assert opt_case_when)
|
||||
apply (corressimp corres: getObject_vcpu_corres setObject_VCPU_corres getObject_TCB_corres)
|
||||
apply (corresKsimp corres: getObject_vcpu_corres setObject_VCPU_corres getObject_TCB_corres)
|
||||
sorry (* FIXME AARCH64 also cross tcb_at'
|
||||
apply (wpsimp wp: arch_thread_get_wp
|
||||
simp: archThreadSet_def tcb_ko_at' tcb_at_typ_at'
|
||||
| strengthen imp_drop_strg[where Q="tcb_at t s" for s]
|
||||
imp_drop_strg[where Q="vcpu_at' v s \<and> typ_at' TCBT t s" for s]
|
||||
| corres_rv)+
|
||||
apply (corressimp wp: get_vcpu_wp getVCPU_wp getObject_tcb_wp arch_thread_get_wp corres_rv_wp_left
|
||||
| corresK_rv)+
|
||||
apply (corresKsimp wp: get_vcpu_wp getVCPU_wp getObject_tcb_wp arch_thread_get_wp corres_rv_wp_left
|
||||
simp: archThreadGet_def tcb_ko_at')+
|
||||
apply (clarsimp simp: typ_at_tcb' typ_at_to_obj_at_arches)
|
||||
apply normalise_obj_at'
|
||||
|
|
@ -1545,7 +1545,7 @@ lemma prepareThreadDelete_corres:
|
|||
(prepare_thread_delete t) (prepareThreadDelete t)"
|
||||
apply (simp add: prepare_thread_delete_def prepareThreadDelete_def)
|
||||
sorry (* FIXME AARCH64 this is the ARM_HYP proof, FPU makes it more complicated
|
||||
apply (corressimp simp: tcb_vcpu_relation)
|
||||
apply (corresKsimp simp: tcb_vcpu_relation)
|
||||
apply (wp arch_thread_get_wp)
|
||||
apply (wpsimp wp: getObject_tcb_wp simp: archThreadGet_def)
|
||||
apply clarsimp
|
||||
|
|
|
|||
|
|
@ -1804,7 +1804,7 @@ lemma arch_getSanitiseRegisterInfo_corres:
|
|||
unfolding arch_get_sanitise_register_info_def getSanitiseRegisterInfo_def
|
||||
apply (fold archThreadGet_def)
|
||||
sorry (*
|
||||
by (corressimp corres: archThreadGet_VCPU_corres) *)
|
||||
by (corresKsimp corres: archThreadGet_VCPU_corres) *)
|
||||
|
||||
crunch tcb_at'[wp]: getSanitiseRegisterInfo "tcb_at' t"
|
||||
|
||||
|
|
|
|||
|
|
@ -1039,8 +1039,8 @@ lemma setEndpoint_corres:
|
|||
corres dc (ep_at ptr) (ep_at' ptr)
|
||||
(set_endpoint ptr e) (setEndpoint ptr e')"
|
||||
apply (simp add: set_simple_ko_def setEndpoint_def is_ep_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ep obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma setNotification_corres:
|
||||
|
|
@ -1048,8 +1048,8 @@ lemma setNotification_corres:
|
|||
corres dc (ntfn_at ptr) (ntfn_at' ptr)
|
||||
(set_notification ptr ae) (setNotification ptr ae')"
|
||||
apply (simp add: set_simple_ko_def setNotification_def is_ntfn_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ntfn obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma no_fail_getNotification [wp]:
|
||||
|
|
|
|||
|
|
@ -799,7 +799,7 @@ lemma arch_switchToIdleThread_corres:
|
|||
arch_switch_to_idle_thread Arch.switchToIdleThread"
|
||||
apply (simp add: arch_switch_to_idle_thread_def
|
||||
AARCH64_H.switchToIdleThread_def)
|
||||
apply (corressimp corres: getIdleThread_corres setVMRoot_corres
|
||||
apply (corresKsimp corres: getIdleThread_corres setVMRoot_corres
|
||||
vcpuSwitch_corres[where vcpu=None, simplified])
|
||||
sorry (* FIXME AARCH64 need to deal with setGlobalUserVSpace_corres
|
||||
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb
|
||||
|
|
|
|||
|
|
@ -1962,7 +1962,7 @@ lemma handleHypervisorFault_corres:
|
|||
and st_tcb_at' simple' thread and ex_nonz_cap_to' thread)
|
||||
(handle_hypervisor_fault thread fault) (handleHypervisorFault thread fault)"
|
||||
apply (cases fault; clarsimp simp add: handleHypervisorFault_def returnOk_def2)
|
||||
apply (corres corres: handleFault_corres)
|
||||
apply (corresK corres: handleFault_corres)
|
||||
apply (clarsimp simp: valid_fault_def)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -2017,7 +2017,7 @@ lemma decodeSetPriority_corres:
|
|||
clarsimp simp: decode_set_priority_def decodeSetPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2035,7 +2035,7 @@ lemma decodeSetMCPriority_corres:
|
|||
clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2150,7 +2150,7 @@ lemma decodeSetSchedParams_corres:
|
|||
apply (clarsimp split: list.split simp: list_all2_Cons2)
|
||||
apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less)
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_split_norE[OF checkPrio_corres])
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
|
|
|
|||
|
|
@ -462,18 +462,18 @@ lemma vcpuUpdate_corres[corres]:
|
|||
"\<forall>v1 v2. vcpu_relation v1 v2 \<longrightarrow> vcpu_relation (f v1) (f' v2) \<Longrightarrow>
|
||||
corres dc (vcpu_at v) (vcpu_at' v)
|
||||
(vcpu_update v f) (vcpuUpdate v f')"
|
||||
by (corressimp corres: getObject_vcpu_corres setObject_VCPU_corres
|
||||
by (corresKsimp corres: getObject_vcpu_corres setObject_VCPU_corres
|
||||
simp: vcpu_update_def vcpuUpdate_def vcpu_relation_def)
|
||||
|
||||
lemma vgicUpdate_corres[corres]:
|
||||
"\<forall>vgic vgic'. vgic_map vgic = vgic' \<longrightarrow> vgic_map (f vgic) = (f' vgic')
|
||||
\<Longrightarrow> corres dc (vcpu_at v) (vcpu_at' v) (vgic_update v f) (vgicUpdate v f')"
|
||||
by (corressimp simp: vgic_update_def vgicUpdate_def vcpu_relation_def)
|
||||
by (corresKsimp simp: vgic_update_def vgicUpdate_def vcpu_relation_def)
|
||||
|
||||
lemma vgicUpdateLR_corres[corres]:
|
||||
"corres dc (vcpu_at v) (vcpu_at' v)
|
||||
(vgic_update_lr v idx val) (vgicUpdateLR v idx val)"
|
||||
by (corressimp simp: vgic_update_lr_def vgicUpdateLR_def vgic_map_def)
|
||||
by (corresKsimp simp: vgic_update_lr_def vgicUpdateLR_def vgic_map_def)
|
||||
|
||||
lemma vcpuReadReg_corres[corres]:
|
||||
"corres (=) (vcpu_at v) (vcpu_at' v and no_0_obj')
|
||||
|
|
@ -1678,7 +1678,7 @@ proof -
|
|||
(do globalPT <- gets (armKSGlobalUserVSpace \<circ> ksArchState);
|
||||
doMachineOp (setVSpaceRoot (addrFromKPPtr globalPT) 0)
|
||||
od)" for P Q
|
||||
apply (corressimp corres: corres_gets_global_pt corres_machine_op)
|
||||
apply (corresKsimp corres: corres_gets_global_pt corres_machine_op)
|
||||
done
|
||||
|
||||
show ?thesis
|
||||
|
|
@ -1729,7 +1729,7 @@ proof -
|
|||
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
|
||||
apply (rule whenE_throwError_corres; simp add: lookup_failure_map_def)
|
||||
apply (rule corres_machine_op)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply fastforce
|
||||
apply simp
|
||||
apply wpsimp+
|
||||
|
|
@ -1793,7 +1793,7 @@ lemma no_fail_hwAIDFlush[intro!, wp, simp]:
|
|||
|
||||
lemma hwASIDFlush_corres[corres]:
|
||||
"corres dc \<top> \<top> (do_machine_op (hwASIDFlush x)) (doMachineOp (hwASIDFlush x))"
|
||||
by (corressimp corres: corres_machine_op) *)
|
||||
by (corresKsimp corres: corres_machine_op) *)
|
||||
|
||||
lemma deleteASID_corres [corres]:
|
||||
assumes "asid' = ucast asid" "pm' = pm"
|
||||
|
|
|
|||
|
|
@ -199,7 +199,7 @@ lemma setObject_ASIDPool_corres [corres]:
|
|||
corres dc (asid_pool_at p and valid_etcbs) (asid_pool_at' p')
|
||||
(set_asid_pool p a) (setObject p' a')"
|
||||
apply (simp add: set_asid_pool_def)
|
||||
apply (corressimp search: setObject_other_corres[where P="\<lambda>_. True"]
|
||||
apply (corresKsimp search: setObject_other_corres[where P="\<lambda>_. True"]
|
||||
wp: get_object_ret get_object_wp)
|
||||
apply (simp add: other_obj_relation_def asid_pool_relation_def)
|
||||
apply (clarsimp simp: obj_at_simps )
|
||||
|
|
@ -1032,7 +1032,7 @@ lemma lookupPTSlot_corres [@lift_corres_args, corres]:
|
|||
(pspace_aligned' and pspace_distinct')
|
||||
(lookup_pt_slot pd vptr) (lookupPTSlot pd vptr)"
|
||||
unfolding lookup_pt_slot_def lookupPTSlot_def lookupPTSlotFromPT_def
|
||||
apply (corressimp simp: pde_relation_aligned_def lookup_failure_map_def
|
||||
apply (corresKsimp simp: pde_relation_aligned_def lookup_failure_map_def
|
||||
ptBits_def pdeBits_def pageBits_def pteBits_def mask_def
|
||||
wp: get_pde_wp_valid getPDE_wp)
|
||||
by (auto simp: lookup_failure_map_def obj_at_def)
|
||||
|
|
@ -1131,7 +1131,7 @@ lemma createMappingEntries_corres [corres]:
|
|||
(create_mapping_entries base vptr pgsz vm_rights attrib pd)
|
||||
(createMappingEntries base' vptr' pgsz' vm_rights' attrib' pd')"
|
||||
unfolding createMappingEntries_def mapping_map_def
|
||||
by (cases pgsz; corressimp simp: vmattributes_map_def less_kernel_base_mapping_slots
|
||||
by (cases pgsz; corresKsimp simp: vmattributes_map_def less_kernel_base_mapping_slots
|
||||
largePagePTEOffsets_def
|
||||
largePagePTE_offsets_def
|
||||
superSectionPDEOffsets_def
|
||||
|
|
@ -1168,7 +1168,7 @@ lemma ensureSafeMapping_corres [corres]:
|
|||
unfolding mapping_map_def ensureSafeMapping_def
|
||||
apply (cases m; cases m'; simp;
|
||||
match premises in "(_ \<otimes> (=)) p p'" for p p' \<Rightarrow> \<open>cases "fst p"; cases "fst p'"\<close>; clarsimp)
|
||||
by (corressimp corresK: mapME_x_corresK_inv
|
||||
by (corresKsimp corresK: mapME_x_corresK_inv
|
||||
wp: get_master_pte_wp get_master_pde_wp getPTE_wp getPDE_wp;
|
||||
auto simp add: valid_mapping_entries_def)+
|
||||
|
||||
|
|
@ -1201,7 +1201,7 @@ lemma find_pd_for_asid_corres [corres]:
|
|||
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
||||
(find_pd_for_asid asid) (findPDForASID asid')"
|
||||
apply (simp add: find_pd_for_asid_def findPDForASID_def liftME_def bindE_assoc)
|
||||
apply (corressimp simp: liftE_bindE assertE_assert mask_asid_low_bits_ucast_ucast
|
||||
apply (corresKsimp simp: liftE_bindE assertE_assert mask_asid_low_bits_ucast_ucast
|
||||
lookup_failure_map_def
|
||||
wp: getPDE_wp getASID_wp
|
||||
search: checkPDAt_corres corres_gets_asid)
|
||||
|
|
|
|||
|
|
@ -325,7 +325,7 @@ lemma getSlotCap_corres:
|
|||
(getSlotCap cte_ptr')"
|
||||
apply (simp add: getSlotCap_def)
|
||||
apply (subst bind_return [symmetric])
|
||||
apply (corressimp)
|
||||
apply (corresKsimp)
|
||||
done
|
||||
|
||||
lemma maskCapRights [simp]:
|
||||
|
|
@ -604,7 +604,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
|
|||
apply (simp add: Let_def unlessE_whenE)
|
||||
apply (simp add: caps isCap_defs Let_def whenE_bindE_throwError_to_if)
|
||||
apply (subst cnode_cap_case_if)
|
||||
apply (corressimp search: getSlotCap_corres IH
|
||||
apply (corresKsimp search: getSlotCap_corres IH
|
||||
wp: get_cap_wp getSlotCap_valid no_fail_stateAssert
|
||||
simp: locateSlot_conv)
|
||||
apply (simp add: drop_postfix_eq)
|
||||
|
|
|
|||
|
|
@ -1467,13 +1467,13 @@ lemma deletedIRQHandler_corres:
|
|||
|
||||
lemma arch_postCapDeletion_corres:
|
||||
"acap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (arch_post_cap_deletion cap) (ARM_H.postCapDeletion cap')"
|
||||
by (corressimp simp: arch_post_cap_deletion_def ARM_H.postCapDeletion_def)
|
||||
by (corresKsimp simp: arch_post_cap_deletion_def ARM_H.postCapDeletion_def)
|
||||
|
||||
lemma postCapDeletion_corres:
|
||||
"cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')"
|
||||
apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def)
|
||||
apply (corressimp corres: deletedIRQHandler_corres)
|
||||
by (corressimp corres: arch_postCapDeletion_corres)
|
||||
apply (corresKsimp corres: deletedIRQHandler_corres)
|
||||
by (corresKsimp corres: arch_postCapDeletion_corres)
|
||||
|
||||
lemma set_cap_trans_state:
|
||||
"((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))"
|
||||
|
|
|
|||
|
|
@ -970,8 +970,8 @@ lemma setEndpoint_corres [corres]:
|
|||
corres dc (ep_at ptr) (ep_at' ptr)
|
||||
(set_endpoint ptr e) (setEndpoint ptr e')"
|
||||
apply (simp add: set_simple_ko_def setEndpoint_def is_ep_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ep obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma setNotification_corres [corres]:
|
||||
|
|
@ -979,8 +979,8 @@ lemma setNotification_corres [corres]:
|
|||
corres dc (ntfn_at ptr) (ntfn_at' ptr)
|
||||
(set_notification ptr ae) (setNotification ptr ae')"
|
||||
apply (simp add: set_simple_ko_def setNotification_def is_ntfn_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ntfn obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma no_fail_getNotification [wp]:
|
||||
|
|
|
|||
|
|
@ -766,7 +766,7 @@ lemma arch_switchToIdleThread_corres:
|
|||
Arch.switchToIdleThread"
|
||||
apply (simp add: arch_switch_to_idle_thread_def
|
||||
ARM_H.switchToIdleThread_def)
|
||||
apply (corressimp corres: getIdleThread_corres setVMRoot_corres[@lift_corres_args])
|
||||
apply (corresKsimp corres: getIdleThread_corres setVMRoot_corres[@lift_corres_args])
|
||||
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb obj_at'_def)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -2097,7 +2097,7 @@ lemma decodeSetPriority_corres:
|
|||
clarsimp simp: decode_set_priority_def decodeSetPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2116,7 +2116,7 @@ lemma decodeSetMCPriority_corres:
|
|||
clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2227,7 +2227,7 @@ lemma decodeSetSchedParams_corres:
|
|||
apply (clarsimp split: list.split simp: list_all2_Cons2)
|
||||
apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less)
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_split_norE[OF checkPrio_corres])
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
|
|
|
|||
|
|
@ -230,7 +230,7 @@ lemma setObject_ASIDPool_corres [corres]:
|
|||
corres dc (asid_pool_at p and valid_etcbs) (asid_pool_at' p)
|
||||
(set_asid_pool p a) (setObject p a')"
|
||||
apply (simp add: set_asid_pool_def)
|
||||
apply (corressimp search: setObject_other_corres[where P="\<lambda>_. True"]
|
||||
apply (corresKsimp search: setObject_other_corres[where P="\<lambda>_. True"]
|
||||
wp: get_object_ret get_object_wp)
|
||||
apply (simp add: other_obj_relation_def asid_pool_relation_def)
|
||||
apply (clarsimp simp: obj_at_simps )
|
||||
|
|
@ -1216,7 +1216,7 @@ lemma lookupPTSlot_corres [corres]:
|
|||
(pspace_aligned' and pspace_distinct')
|
||||
(lookup_pt_slot pd vptr) (lookupPTSlot pd vptr)"
|
||||
unfolding lookup_pt_slot_def lookupPTSlot_def lookupPTSlotFromPT_def
|
||||
apply (corressimp simp: pde_relation_aligned_def lookup_failure_map_def
|
||||
apply (corresKsimp simp: pde_relation_aligned_def lookup_failure_map_def
|
||||
wp: get_pde_wp_valid getPDE_wp)
|
||||
by (auto simp: lookup_failure_map_def obj_at_def)
|
||||
|
||||
|
|
@ -1321,7 +1321,7 @@ lemma createMappingEntries_corres [corres]:
|
|||
(create_mapping_entries base vptr pgsz vm_rights attrib pd)
|
||||
(createMappingEntries base vptr pgsz vm_rights' attrib' pd)"
|
||||
unfolding createMappingEntries_def mapping_map_def
|
||||
by (cases pgsz; corressimp simp: vmattributes_map_def)
|
||||
by (cases pgsz; corresKsimp simp: vmattributes_map_def)
|
||||
|
||||
lemma pte_relation'_Invalid_inv [simp]:
|
||||
"pte_relation' x ARM_HYP_H.pte.InvalidPTE = (x = ARM_A.pte.InvalidPTE)"
|
||||
|
|
@ -1354,7 +1354,7 @@ lemma createMappingEntries_valid_slots' [wp]:
|
|||
apply (auto elim: is_aligned_weaken)
|
||||
done
|
||||
|
||||
lemmas [corresc_simp] = master_pte_relation_def master_pde_relation_def
|
||||
lemmas [corresKc_simp] = master_pte_relation_def master_pde_relation_def
|
||||
|
||||
lemma ensureSafeMapping_corres [corres]:
|
||||
"mapping_map m m' \<Longrightarrow>
|
||||
|
|
@ -1365,7 +1365,7 @@ lemma ensureSafeMapping_corres [corres]:
|
|||
unfolding mapping_map_def ensureSafeMapping_def
|
||||
apply (cases m; cases m'; simp;
|
||||
match premises in "(_ \<otimes> (=)) p p'" for p p' \<Rightarrow> \<open>cases "fst p"; cases "fst p'"\<close>; clarsimp)
|
||||
by (corressimp corresK: mapME_x_corresK_inv
|
||||
by (corresKsimp corresK: mapME_x_corresK_inv
|
||||
wp: get_master_pte_wp get_master_pde_wp getPTE_wp getPDE_wp;
|
||||
auto simp add: valid_mapping_entries_def)+
|
||||
|
||||
|
|
@ -1397,7 +1397,7 @@ lemma find_pd_for_asid_corres [@lift_corres_args, corres]:
|
|||
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
||||
(find_pd_for_asid asid) (findPDForASID asid)"
|
||||
apply (simp add: find_pd_for_asid_def findPDForASID_def liftME_def bindE_assoc)
|
||||
apply (corressimp simp: liftE_bindE assertE_assert mask_asid_low_bits_ucast_ucast lookup_failure_map_def
|
||||
apply (corresKsimp simp: liftE_bindE assertE_assert mask_asid_low_bits_ucast_ucast lookup_failure_map_def
|
||||
wp: getPDE_wp getASID_wp
|
||||
search: checkPDAt_corres corres_gets_asid)
|
||||
subgoal premises prems for s s'
|
||||
|
|
|
|||
|
|
@ -843,14 +843,14 @@ lemma decodeARMVCPUInvocation_corres:
|
|||
apply (frule list_all2_Cons)
|
||||
apply clarsimp
|
||||
apply (case_tac a; clarsimp simp add: cap_relation_def)
|
||||
apply (corres corres: corres_returnOkTT)
|
||||
apply (corresK corres: corres_returnOkTT)
|
||||
apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def)
|
||||
(* inject_irq *)
|
||||
apply (simp add: decode_vcpu_inject_irq_def decodeVCPUInjectIRQ_def isVCPUCap_def)
|
||||
apply (cases args; clarsimp)
|
||||
apply (case_tac list; clarsimp simp add: rangeCheck_def range_check_def unlessE_whenE)
|
||||
apply (clarsimp simp: shiftL_nat whenE_bindE_throwError_to_if)
|
||||
apply (corressimp wp: get_vcpu_wp)
|
||||
apply (corresKsimp wp: get_vcpu_wp)
|
||||
apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def ucast_id
|
||||
valid_cap'_def valid_cap_def
|
||||
make_virq_def makeVIRQ_def split:if_split)
|
||||
|
|
@ -1251,7 +1251,7 @@ lemma invokeVCPUInjectIRQ_corres:
|
|||
(invokeVCPUInjectIRQ v index virq)"
|
||||
unfolding invokeVCPUInjectIRQ_def invoke_vcpu_inject_irq_def
|
||||
apply (clarsimp simp: bind_assoc)
|
||||
apply (corressimp corres: getObject_vcpu_corres setObject_VCPU_corres wp: get_vcpu_wp)
|
||||
apply (corresKsimp corres: getObject_vcpu_corres setObject_VCPU_corres wp: get_vcpu_wp)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
|
|
@ -1264,7 +1264,7 @@ lemma invokeVCPUReadReg_corres:
|
|||
(invokeVCPUReadReg v r)"
|
||||
unfolding invoke_vcpu_read_register_def invokeVCPUReadReg_def read_vcpu_register_def readVCPUReg_def
|
||||
apply (rule corres_discard_r)
|
||||
apply (corressimp corres: getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
apply (corresKsimp corres: getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
apply (clarsimp simp: vcpu_relation_def split: option.splits)
|
||||
apply (wpsimp simp: getCurThread_def)+
|
||||
done
|
||||
|
|
@ -1279,7 +1279,7 @@ lemma invokeVCPUWriteReg_corres:
|
|||
unfolding invokeVCPUWriteReg_def invoke_vcpu_write_register_def write_vcpu_register_def
|
||||
writeVCPUReg_def
|
||||
apply (rule corres_discard_r)
|
||||
apply (corressimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
apply (corresKsimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
subgoal by (auto simp: vcpu_relation_def split: option.splits)
|
||||
apply (wpsimp simp: getCurThread_def)+
|
||||
done
|
||||
|
|
@ -1314,7 +1314,7 @@ lemma associateVCPUTCB_corres:
|
|||
(associateVCPUTCB v t)"
|
||||
unfolding associate_vcpu_tcb_def associateVCPUTCB_def
|
||||
apply (clarsimp simp: bind_assoc)
|
||||
apply (corressimp search: getObject_vcpu_corres setObject_VCPU_corres vcpuSwitch_corres''
|
||||
apply (corresKsimp search: getObject_vcpu_corres setObject_VCPU_corres vcpuSwitch_corres''
|
||||
wp: get_vcpu_wp getVCPU_wp hoare_vcg_imp_lift'
|
||||
simp: vcpu_relation_def)
|
||||
apply (rule_tac Q="\<lambda>_. invs and tcb_at t" in hoare_strengthen_post)
|
||||
|
|
@ -1335,7 +1335,7 @@ lemma associateVCPUTCB_corres:
|
|||
apply (simp add: valid_vcpu'_def typ_at_tcb')
|
||||
apply (clarsimp simp: typ_at_to_obj_at_arches obj_at'_def)
|
||||
apply (fastforce simp: typ_at_to_obj_at_arches obj_at'_def)
|
||||
apply (corressimp wp: arch_thread_get_wp getObject_tcb_wp
|
||||
apply (corresKsimp wp: arch_thread_get_wp getObject_tcb_wp
|
||||
simp: archThreadGet_def)+
|
||||
apply (simp add: vcpu_relation_def)
|
||||
apply (intro allI conjI impI;
|
||||
|
|
@ -1361,7 +1361,7 @@ lemma invokeVCPUAckVPPI_corres:
|
|||
(invokeVCPUAckVPPI vcpu vppi)"
|
||||
unfolding invokeVCPUAckVPPI_def invoke_vcpu_ack_vppi_def write_vcpu_register_def
|
||||
writeVCPUReg_def
|
||||
by (corressimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
by (corresKsimp corres: setObject_VCPU_corres getObject_vcpu_corres wp: get_vcpu_wp)
|
||||
(auto simp: vcpu_relation_def split: option.splits)
|
||||
|
||||
lemma performARMVCPUInvocation_corres:
|
||||
|
|
|
|||
|
|
@ -482,7 +482,7 @@ lemma constOnFailure_wp :
|
|||
apply (wp|simp)+
|
||||
done
|
||||
|
||||
lemma corres_throwError_str [corres_concrete_rER]:
|
||||
lemma corres_throwError_str [corresK_concrete_rER]:
|
||||
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)"
|
||||
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)"
|
||||
by (simp add: corres_underlyingK_def)+
|
||||
|
|
|
|||
|
|
@ -325,7 +325,7 @@ lemma getSlotCap_corres:
|
|||
(getSlotCap cte_ptr')"
|
||||
apply (simp add: getSlotCap_def)
|
||||
apply (subst bind_return [symmetric])
|
||||
apply (corressimp)
|
||||
apply (corresKsimp)
|
||||
done
|
||||
|
||||
lemma maskCapRights [simp]:
|
||||
|
|
@ -607,7 +607,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
|
|||
apply (simp add: Let_def unlessE_whenE)
|
||||
apply (simp add: caps isCap_defs Let_def whenE_bindE_throwError_to_if)
|
||||
apply (subst cnode_cap_case_if)
|
||||
apply (corressimp search: getSlotCap_corres IH
|
||||
apply (corresKsimp search: getSlotCap_corres IH
|
||||
wp: get_cap_wp getSlotCap_valid no_fail_stateAssert
|
||||
simp: locateSlot_conv)
|
||||
apply (simp add: drop_postfix_eq)
|
||||
|
|
|
|||
|
|
@ -1473,13 +1473,13 @@ lemma deletedIRQHandler_corres:
|
|||
|
||||
lemma arch_postCapDeletion_corres:
|
||||
"acap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (arch_post_cap_deletion cap) (ARM_HYP_H.postCapDeletion cap')"
|
||||
by (corressimp simp: arch_post_cap_deletion_def ARM_HYP_H.postCapDeletion_def)
|
||||
by (corresKsimp simp: arch_post_cap_deletion_def ARM_HYP_H.postCapDeletion_def)
|
||||
|
||||
lemma postCapDeletion_corres:
|
||||
"cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')"
|
||||
apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def)
|
||||
apply (corressimp corres: deletedIRQHandler_corres)
|
||||
by (corressimp corres: arch_postCapDeletion_corres)
|
||||
apply (corresKsimp corres: deletedIRQHandler_corres)
|
||||
by (corresKsimp corres: arch_postCapDeletion_corres)
|
||||
|
||||
lemma set_cap_trans_state:
|
||||
"((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))"
|
||||
|
|
@ -3844,7 +3844,7 @@ lemma sym_refs_vcpu_tcb:
|
|||
lemma vcpuFinalise_corres [corres]:
|
||||
"corres dc (invs and vcpu_at vcpu) (invs' and vcpu_at' vcpu) (vcpu_finalise vcpu) (vcpuFinalise vcpu)"
|
||||
unfolding vcpuFinalise_def vcpu_finalise_def
|
||||
apply (corressimp corres: getObject_vcpu_corres simp: vcpu_relation_def)
|
||||
apply (corresKsimp corres: getObject_vcpu_corres simp: vcpu_relation_def)
|
||||
apply (wpsimp wp: get_vcpu_wp getVCPU_wp)+
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
|
|
@ -3888,7 +3888,7 @@ lemma arch_finaliseCap_corres:
|
|||
elim!: is_aligned_weaken invs_valid_asid_map)[2]
|
||||
apply (rule corres_guard_imp, rule deleteASID_corres)
|
||||
apply (auto elim!: invs_valid_asid_map simp: mask_def valid_cap_def)[2]
|
||||
apply corres
|
||||
apply corresK
|
||||
apply (clarsimp simp: valid_cap_def valid_cap'_def)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -1040,7 +1040,7 @@ lemma handleInterrupt_corres:
|
|||
apply wp+
|
||||
apply clarsimp
|
||||
apply clarsimp
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
done
|
||||
|
||||
lemma threadSet_ksDomainTime[wp]:
|
||||
|
|
|
|||
|
|
@ -1457,7 +1457,7 @@ lemma archThreadGet_corres:
|
|||
"(\<And>a a'. arch_tcb_relation a a' \<Longrightarrow> f a = f' a') \<Longrightarrow>
|
||||
corres (=) (tcb_at t) (tcb_at' t) (arch_thread_get f t) (archThreadGet f' t)"
|
||||
unfolding arch_thread_get_def archThreadGet_def
|
||||
apply (corressimp corres: get_tcb_corres)
|
||||
apply (corresKsimp corres: get_tcb_corres)
|
||||
apply (clarsimp simp: tcb_relation_def)
|
||||
done
|
||||
|
||||
|
|
@ -1486,7 +1486,7 @@ lemma corres_gets_current_vcpu[corres]:
|
|||
lemma vcpuInvalidateActive_corres[corres]:
|
||||
"corres dc \<top> no_0_obj' vcpu_invalidate_active vcpuInvalidateActive"
|
||||
unfolding vcpuInvalidateActive_def vcpu_invalidate_active_def
|
||||
apply (corressimp corres: vcpuDisable_corres
|
||||
apply (corresKsimp corres: vcpuDisable_corres
|
||||
corresK: corresK_modifyT
|
||||
simp: modifyArchState_def)
|
||||
apply (clarsimp simp: state_relation_def arch_state_relation_def)
|
||||
|
|
@ -1500,7 +1500,7 @@ lemma archThreadSet_corres:
|
|||
"(\<And>a a'. arch_tcb_relation a a' \<Longrightarrow> arch_tcb_relation (f a) (f' a')) \<Longrightarrow>
|
||||
corres dc (tcb_at t) (tcb_at' t) (arch_thread_set f t) (archThreadSet f' t)"
|
||||
apply (simp add: arch_thread_set_def archThreadSet_def)
|
||||
apply (corres corres: get_tcb_corres setObject_update_TCB_corres')
|
||||
apply (corresK corres: get_tcb_corres setObject_update_TCB_corres')
|
||||
apply wpsimp+
|
||||
apply (auto simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+
|
||||
done
|
||||
|
|
@ -1531,7 +1531,7 @@ lemma asUser_sanitiseRegister_corres[corres]:
|
|||
setRegister CPSR (sanitiseRegister b' CPSR cpsr)
|
||||
od))"
|
||||
unfolding sanitiseRegister_def sanitise_register_def
|
||||
apply (corressimp corresK: corresK_as_user')
|
||||
apply (corresKsimp corresK: corresK_as_user')
|
||||
done
|
||||
|
||||
crunch typ_at'[wp]: vcpuInvalidateActive "\<lambda>s. P (typ_at' T p s)"
|
||||
|
|
@ -1553,13 +1553,13 @@ lemma dissociateVCPUTCB_corres [@lift_corres_args, corres]:
|
|||
(dissociate_vcpu_tcb v t) (dissociateVCPUTCB v t)"
|
||||
unfolding dissociate_vcpu_tcb_def dissociateVCPUTCB_def
|
||||
apply (clarsimp simp: bind_assoc when_fail_assert opt_case_when)
|
||||
apply (corressimp corres: getObject_vcpu_corres setObject_VCPU_corres get_tcb_corres)
|
||||
apply (corresKsimp corres: getObject_vcpu_corres setObject_VCPU_corres get_tcb_corres)
|
||||
apply (wpsimp wp: arch_thread_get_wp
|
||||
simp: archThreadSet_def tcb_ko_at' tcb_at_typ_at'
|
||||
| strengthen imp_drop_strg[where Q="tcb_at t s" for s]
|
||||
imp_drop_strg[where Q="vcpu_at' v s \<and> typ_at' TCBT t s" for s]
|
||||
| corres_rv)+
|
||||
apply (corressimp wp: get_vcpu_wp getVCPU_wp getObject_tcb_wp arch_thread_get_wp corres_rv_wp_left
|
||||
| corresK_rv)+
|
||||
apply (corresKsimp wp: get_vcpu_wp getVCPU_wp getObject_tcb_wp arch_thread_get_wp corres_rv_wp_left
|
||||
simp: archThreadGet_def tcb_ko_at')+
|
||||
apply (clarsimp simp: typ_at_tcb' typ_at_to_obj_at_arches)
|
||||
apply normalise_obj_at'
|
||||
|
|
@ -1582,7 +1582,7 @@ lemma prepareThreadDelete_corres:
|
|||
"corres dc (invs and tcb_at t) (valid_objs' and tcb_at' t and no_0_obj')
|
||||
(prepare_thread_delete t) (prepareThreadDelete t)"
|
||||
apply (simp add: prepare_thread_delete_def prepareThreadDelete_def)
|
||||
apply (corressimp simp: tcb_vcpu_relation)
|
||||
apply (corresKsimp simp: tcb_vcpu_relation)
|
||||
apply (wp arch_thread_get_wp)
|
||||
apply (wpsimp wp: getObject_tcb_wp simp: archThreadGet_def)
|
||||
apply clarsimp
|
||||
|
|
|
|||
|
|
@ -1866,7 +1866,7 @@ lemma arch_getSanitiseRegisterInfo_corres:
|
|||
(getSanitiseRegisterInfo t)"
|
||||
unfolding arch_get_sanitise_register_info_def getSanitiseRegisterInfo_def
|
||||
apply (fold archThreadGet_def)
|
||||
by (corressimp corres: archThreadGet_VCPU_corres)
|
||||
by (corresKsimp corres: archThreadGet_VCPU_corres)
|
||||
|
||||
crunch tcb_at'[wp]: getSanitiseRegisterInfo "tcb_at' t"
|
||||
|
||||
|
|
|
|||
|
|
@ -1061,8 +1061,8 @@ lemma setEndpoint_corres [corres]:
|
|||
corres dc (ep_at ptr) (ep_at' ptr)
|
||||
(set_endpoint ptr e) (setEndpoint ptr e')"
|
||||
apply (simp add: set_simple_ko_def setEndpoint_def is_ep_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ep obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma setNotification_corres [corres]:
|
||||
|
|
@ -1070,8 +1070,8 @@ lemma setNotification_corres [corres]:
|
|||
corres dc (ntfn_at ptr) (ntfn_at' ptr)
|
||||
(set_notification ptr ae) (setNotification ptr ae')"
|
||||
apply (simp add: set_simple_ko_def setNotification_def is_ntfn_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ntfn obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma no_fail_getNotification [wp]:
|
||||
|
|
|
|||
|
|
@ -792,7 +792,7 @@ lemma arch_switchToIdleThread_corres:
|
|||
arch_switch_to_idle_thread
|
||||
Arch.switchToIdleThread"
|
||||
unfolding arch_switch_to_idle_thread_def ARM_HYP_H.switchToIdleThread_def
|
||||
apply (corressimp corres: getIdleThread_corres setVMRoot_corres[@lift_corres_args] vcpuSwitch_corres[where vcpu=None, simplified]
|
||||
apply (corresKsimp corres: getIdleThread_corres setVMRoot_corres[@lift_corres_args] vcpuSwitch_corres[where vcpu=None, simplified]
|
||||
wp: tcb_at_idle_thread_lift tcb_at'_ksIdleThread_lift vcpuSwitch_it')
|
||||
apply (clarsimp simp: invs_valid_objs invs_arch_state invs_valid_asid_map invs_valid_vs_lookup
|
||||
invs_psp_aligned invs_distinct invs_unique_refs invs_vspace_objs)
|
||||
|
|
|
|||
|
|
@ -1979,7 +1979,7 @@ lemma handleHypervisorFault_corres:
|
|||
(handle_hypervisor_fault thread fault)
|
||||
(handleHypervisorFault thread fault)"
|
||||
apply (cases fault; clarsimp simp add: handleHypervisorFault_def returnOk_def2)
|
||||
apply (corres corres: handleFault_corres)
|
||||
apply (corresK corres: handleFault_corres)
|
||||
apply (simp add: ucast_id)
|
||||
apply (clarsimp simp: valid_fault_def)
|
||||
done
|
||||
|
|
|
|||
|
|
@ -2075,7 +2075,7 @@ lemma decodeSetPriority_corres:
|
|||
clarsimp simp: decode_set_priority_def decodeSetPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2094,7 +2094,7 @@ lemma decodeSetMCPriority_corres:
|
|||
clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2211,7 +2211,7 @@ lemma decodeSetSchedParams_corres:
|
|||
apply (clarsimp split: list.split simp: list_all2_Cons2)
|
||||
apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less)
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_split_norE[OF checkPrio_corres])
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
|
|
|
|||
|
|
@ -804,18 +804,18 @@ lemma vcpuUpdate_corres[corres]:
|
|||
"\<forall>v1 v2. vcpu_relation v1 v2 \<longrightarrow> vcpu_relation (f v1) (f' v2) \<Longrightarrow>
|
||||
corres dc (vcpu_at v) (vcpu_at' v)
|
||||
(vcpu_update v f) (vcpuUpdate v f')"
|
||||
by (corressimp corres: getObject_vcpu_corres setObject_VCPU_corres
|
||||
by (corresKsimp corres: getObject_vcpu_corres setObject_VCPU_corres
|
||||
simp: vcpu_update_def vcpuUpdate_def vcpu_relation_def)
|
||||
|
||||
lemma vgicUpdate_corres[corres]:
|
||||
"\<forall>vgic vgic'. vgic_map vgic = vgic' \<longrightarrow> vgic_map (f vgic) = (f' vgic')
|
||||
\<Longrightarrow> corres dc (vcpu_at v) (vcpu_at' v) (vgic_update v f) (vgicUpdate v f')"
|
||||
by (corressimp simp: vgic_update_def vgicUpdate_def vcpu_relation_def)
|
||||
by (corresKsimp simp: vgic_update_def vgicUpdate_def vcpu_relation_def)
|
||||
|
||||
lemma vgicUpdateLR_corres[corres]:
|
||||
"corres dc (vcpu_at v) (vcpu_at' v)
|
||||
(vgic_update_lr v idx val) (vgicUpdateLR v idx val)"
|
||||
by (corressimp simp: vgic_update_lr_def vgicUpdateLR_def vgic_map_def)
|
||||
by (corresKsimp simp: vgic_update_lr_def vgicUpdateLR_def vgic_map_def)
|
||||
|
||||
lemma vcpuReadReg_corres[corres]:
|
||||
"corres (=) (vcpu_at v) (vcpu_at' v and no_0_obj')
|
||||
|
|
|
|||
|
|
@ -681,7 +681,7 @@ lemma lookupPTSlot_corres:
|
|||
\<top>
|
||||
(gets_the (pt_lookup_slot pt vptr \<circ> ptes_of)) (lookupPTSlot pt vptr)"
|
||||
unfolding lookupPTSlot_def pt_lookup_slot_def
|
||||
by (corressimp corres: lookupPTSlotFromLevel_corres)
|
||||
by (corresKsimp corres: lookupPTSlotFromLevel_corres)
|
||||
|
||||
lemma lookupPTFromLevel_corres:
|
||||
"\<lbrakk> level' = size level; pt' = pt \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -756,7 +756,7 @@ next
|
|||
apply (simp add: unlessE_whenE not_less)
|
||||
apply (rule corres_gen_asm, simp)
|
||||
apply (rule corres_initial_splitE[where r'=dc])
|
||||
apply (corressimp simp: lookup_failure_map_def)
|
||||
apply (corresKsimp simp: lookup_failure_map_def)
|
||||
apply (rule corres_splitEE[where r'=pte_relation'])
|
||||
apply (simp, rule getObject_PTE_corres)
|
||||
apply (rule whenE_throwError_corres)
|
||||
|
|
@ -843,10 +843,10 @@ lemma copy_global_mappings_corres [@lift_corres_args, corres]:
|
|||
(copy_global_mappings pt)
|
||||
(copyGlobalMappings pt)" (is "corres _ ?apre _ _ _")
|
||||
unfolding copy_global_mappings_def copyGlobalMappings_def objBits_simps archObjSize_def pptr_base_def
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule_tac P="pt_at global_pt and ?apre" and P'="\<top>"
|
||||
in corresK_mapM_x[OF order_refl])
|
||||
apply (corressimp simp: objBits_def mask_def wp: get_pte_wp getPTE_wp)+
|
||||
apply (corresKsimp simp: objBits_def mask_def wp: get_pte_wp getPTE_wp)+
|
||||
apply (drule valid_global_arch_objs_pt_at)
|
||||
apply (clarsimp simp: ptIndex_def ptBitsLeft_def maxPTLevel_def ptTranslationBits_def pageBits_def
|
||||
pt_index_def pt_bits_left_def level_defs)
|
||||
|
|
|
|||
|
|
@ -1527,8 +1527,8 @@ lemma arch_postCapDeletion_corres:
|
|||
lemma postCapDeletion_corres:
|
||||
"cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')"
|
||||
apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def)
|
||||
apply (corressimp corres: deletedIRQHandler_corres)
|
||||
by (corressimp corres: arch_postCapDeletion_corres)
|
||||
apply (corresKsimp corres: deletedIRQHandler_corres)
|
||||
by (corresKsimp corres: arch_postCapDeletion_corres)
|
||||
|
||||
lemma set_cap_trans_state:
|
||||
"((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))"
|
||||
|
|
|
|||
|
|
@ -995,8 +995,8 @@ lemma setEndpoint_corres:
|
|||
corres dc (ep_at ptr) (ep_at' ptr)
|
||||
(set_endpoint ptr e) (setEndpoint ptr e')"
|
||||
apply (simp add: set_simple_ko_def setEndpoint_def is_ep_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ep obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma setNotification_corres:
|
||||
|
|
@ -1004,8 +1004,8 @@ lemma setNotification_corres:
|
|||
corres dc (ntfn_at ptr) (ntfn_at' ptr)
|
||||
(set_notification ptr ae) (setNotification ptr ae')"
|
||||
apply (simp add: set_simple_ko_def setNotification_def is_ntfn_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ntfn obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma no_fail_getNotification [wp]:
|
||||
|
|
|
|||
|
|
@ -658,7 +658,7 @@ lemma arch_switchToIdleThread_corres:
|
|||
arch_switch_to_idle_thread Arch.switchToIdleThread"
|
||||
apply (simp add: arch_switch_to_idle_thread_def
|
||||
RISCV64_H.switchToIdleThread_def)
|
||||
apply (corressimp corres: getIdleThread_corres setVMRoot_corres)
|
||||
apply (corresKsimp corres: getIdleThread_corres setVMRoot_corres)
|
||||
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb
|
||||
valid_arch_state_asid_table valid_arch_state_global_arch_objs)
|
||||
done
|
||||
|
|
|
|||
|
|
@ -2009,7 +2009,7 @@ lemma decodeSetPriority_corres:
|
|||
clarsimp simp: decode_set_priority_def decodeSetPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2027,7 +2027,7 @@ lemma decodeSetMCPriority_corres:
|
|||
clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2142,7 +2142,7 @@ lemma decodeSetSchedParams_corres:
|
|||
apply (clarsimp split: list.split simp: list_all2_Cons2)
|
||||
apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less)
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_split_norE[OF checkPrio_corres])
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
|
|
|
|||
|
|
@ -85,7 +85,7 @@ proof -
|
|||
(do globalPT <- gets (riscvKSGlobalPT \<circ> ksArchState);
|
||||
doMachineOp (setVSpaceRoot (addrFromKPPtr globalPT) 0)
|
||||
od)" for P Q
|
||||
apply (corressimp corres: corres_gets_global_pt corres_machine_op)
|
||||
apply (corresKsimp corres: corres_gets_global_pt corres_machine_op)
|
||||
apply fastforce
|
||||
apply (simp add: addrFromKPPtr_def)
|
||||
done
|
||||
|
|
@ -137,7 +137,7 @@ proof -
|
|||
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
|
||||
apply (rule whenE_throwError_corres; simp add: lookup_failure_map_def)
|
||||
apply (rule corres_machine_op)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply fastforce
|
||||
apply simp
|
||||
apply wpsimp+
|
||||
|
|
@ -192,7 +192,7 @@ lemma no_fail_hwAIDFlush[intro!, wp, simp]:
|
|||
|
||||
lemma hwASIDFlush_corres[corres]:
|
||||
"corres dc \<top> \<top> (do_machine_op (hwASIDFlush x)) (doMachineOp (hwASIDFlush x))"
|
||||
by (corressimp corres: corres_machine_op)
|
||||
by (corresKsimp corres: corres_machine_op)
|
||||
|
||||
lemma deleteASID_corres [corres]:
|
||||
assumes "asid' = ucast asid" "pm' = pm"
|
||||
|
|
|
|||
|
|
@ -1411,11 +1411,11 @@ lemma copy_global_mappings_corres [@lift_corres_args, corres]:
|
|||
(copyGlobalMappings pm)" (is "corres _ ?apre _ _ _")
|
||||
unfolding copy_global_mappings_def copyGlobalMappings_def objBits_simps archObjSize_def pptr_base_def
|
||||
apply (fold word_size_bits_def)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule_tac P="page_map_l4_at global_pm and ?apre" and
|
||||
P'="page_map_l4_at' skimPM and page_map_l4_at' pm"
|
||||
in corresK_mapM_x[OF order_refl])
|
||||
apply (corressimp simp: objBits_def mask_def wp: get_pde_wp getPDE_wp)+
|
||||
apply (corresKsimp simp: objBits_def mask_def wp: get_pde_wp getPDE_wp)+
|
||||
apply(rule conjI)
|
||||
subgoal by (auto intro!: page_map_l4_pml4e_atI page_map_l4_pml4e_atI'
|
||||
simp: page_bits_def le_less_trans ptTranslationBits_def)
|
||||
|
|
|
|||
|
|
@ -1321,7 +1321,7 @@ lemma perform_port_inv_corres:
|
|||
apply (clarsimp simp: perform_io_port_invocation_def performX64PortInvocation_def
|
||||
archinv_relation_def ioport_invocation_map_def)
|
||||
apply (case_tac x; clarsimp)
|
||||
apply (corressimp corres: port_in_corres simp: ioport_data_relation_def)
|
||||
apply (corresKsimp corres: port_in_corres simp: ioport_data_relation_def)
|
||||
by (auto simp: no_fail_in8 no_fail_in16 no_fail_in32
|
||||
no_fail_out8 no_fail_out16 no_fail_out32)
|
||||
|
||||
|
|
|
|||
|
|
@ -1646,8 +1646,8 @@ lemma arch_postCapDeletion_corres:
|
|||
lemma postCapDeletion_corres:
|
||||
"cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')"
|
||||
apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def)
|
||||
apply (corressimp corres: deletedIRQHandler_corres)
|
||||
by (corressimp corres: arch_postCapDeletion_corres)
|
||||
apply (corresKsimp corres: deletedIRQHandler_corres)
|
||||
by (corresKsimp corres: arch_postCapDeletion_corres)
|
||||
|
||||
lemma set_cap_trans_state:
|
||||
"((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))"
|
||||
|
|
|
|||
|
|
@ -1019,8 +1019,8 @@ lemma setEndpoint_corres:
|
|||
corres dc (ep_at ptr) (ep_at' ptr)
|
||||
(set_endpoint ptr e) (setEndpoint ptr e')"
|
||||
apply (simp add: set_simple_ko_def setEndpoint_def is_ep_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ep obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma setNotification_corres:
|
||||
|
|
@ -1028,8 +1028,8 @@ lemma setNotification_corres:
|
|||
corres dc (ntfn_at ptr) (ntfn_at' ptr)
|
||||
(set_notification ptr ae) (setNotification ptr ae')"
|
||||
apply (simp add: set_simple_ko_def setNotification_def is_ntfn_def[symmetric])
|
||||
apply (corres_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corressimp wp: get_object_ret get_object_wp)+
|
||||
apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"])
|
||||
apply (corresKsimp wp: get_object_ret get_object_wp)+
|
||||
by (fastforce simp: is_ntfn obj_at_simps objBits_defs partial_inv_def)
|
||||
|
||||
lemma no_fail_getNotification [wp]:
|
||||
|
|
|
|||
|
|
@ -5545,7 +5545,7 @@ lemma corres_retype_region_createNewCaps:
|
|||
APIType_map2_def arch_default_cap_def)
|
||||
apply fastforce+
|
||||
\<comment> \<open>PML4\<close>
|
||||
apply (corressimp corres: corres_retype[where ty="Inr PML4Object" and 'a=pml4e and sz=sz,
|
||||
apply (corresKsimp corres: corres_retype[where ty="Inr PML4Object" and 'a=pml4e and sz=sz,
|
||||
simplified, folded retype_region2_retype_region_PML4Obj]
|
||||
corresK: corresK_mapM_x_list_all2[where I="\<lambda>xs s. valid_arch_state s \<and> pspace_aligned s
|
||||
\<and> valid_etcbs s \<and>
|
||||
|
|
|
|||
|
|
@ -715,7 +715,7 @@ lemma arch_switchToIdleThread_corres:
|
|||
arch_switch_to_idle_thread Arch.switchToIdleThread"
|
||||
apply (simp add: arch_switch_to_idle_thread_def
|
||||
X64_H.switchToIdleThread_def)
|
||||
apply (corressimp corres: getIdleThread_corres setVMRoot_corres)
|
||||
apply (corresKsimp corres: getIdleThread_corres setVMRoot_corres)
|
||||
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb obj_at'_def)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -2035,7 +2035,7 @@ lemma decodeSetPriority_corres:
|
|||
clarsimp simp: decode_set_priority_def decodeSetPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2054,7 +2054,7 @@ lemma decodeSetMCPriority_corres:
|
|||
clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def)
|
||||
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
|
||||
|
|
@ -2171,7 +2171,7 @@ lemma decodeSetSchedParams_corres:
|
|||
apply (clarsimp split: list.split simp: list_all2_Cons2)
|
||||
apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less)
|
||||
apply (rule corres_split_eqrE)
|
||||
apply corressimp
|
||||
apply corresKsimp
|
||||
apply (rule corres_split_norE[OF checkPrio_corres])
|
||||
apply (rule corres_splitEE[OF checkPrio_corres])
|
||||
apply (rule corres_returnOkTT)
|
||||
|
|
|
|||
|
|
@ -546,7 +546,7 @@ lemma invalidatePageStructureCacheASID_corres' [corres]:
|
|||
"corres dc \<top> \<top>
|
||||
(invalidate_page_structure_cache_asid vspace asid)
|
||||
(X64_H.invalidatePageStructureCacheASID vspace' asid')"
|
||||
by (corressimp simp: invalidate_page_structure_cache_asid_def
|
||||
by (corresKsimp simp: invalidate_page_structure_cache_asid_def
|
||||
X64_H.invalidatePageStructureCacheASID_def
|
||||
invalidateLocalPageStructureCacheASID_def
|
||||
assms ucast_id
|
||||
|
|
|
|||
Loading…
Reference in New Issue