x64: AInvs now done except ArchAInvsPre and KernelInit_AI
This commit is contained in:
Joel Beeren
parent
c45e14c383
commit
67daaea42a
|
|
@ -3106,219 +3106,6 @@ assumes rewrite: "\<And>s. Q s \<Longrightarrow> f s = t s"
|
|||
done
|
||||
|
||||
|
||||
lemma commute_grab_asm:
|
||||
"(F \<Longrightarrow> monad_commute P f g) \<Longrightarrow> (monad_commute (P and (K F)) f g)"
|
||||
by (clarsimp simp: monad_commute_def)
|
||||
|
||||
lemma bexEI: "\<lbrakk>\<exists>x\<in>S. Q x; \<And>x. \<lbrakk>x \<in> S; Q x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. P x" by blast
|
||||
|
||||
lemma monad_eq_split:
|
||||
assumes "\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
|
||||
"\<lbrace>P\<rbrace> g \<lbrace>\<lambda>r s. Q r s\<rbrace>"
|
||||
"P s"
|
||||
shows "(g >>= f) s = (g >>= f') s"
|
||||
proof -
|
||||
have pre: "\<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s)\<rbrakk> \<Longrightarrow> f rv s' = f' rv s'"
|
||||
using assms unfolding valid_def
|
||||
by (erule_tac x=s in allE) auto
|
||||
show ?thesis
|
||||
apply (simp add: bind_def image_def)
|
||||
apply (intro conjI)
|
||||
apply (rule set_eqI)
|
||||
apply (clarsimp simp: Union_eq)
|
||||
apply (rule iffI; elim exEI conjE; simp; elim exEI bexEI; clarsimp simp: pre)
|
||||
apply (rule iffI; cases "snd (g s)"; simp; elim exEI bexEI; clarsimp simp: pre)
|
||||
done
|
||||
qed
|
||||
|
||||
lemma monad_eq_split2:
|
||||
assumes eq: " g' s = g s"
|
||||
assumes tail:"\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
|
||||
and hoare: "\<lbrace>P\<rbrace>g\<lbrace>\<lambda>r s. Q r s\<rbrace>" "P s"
|
||||
shows "(g>>=f) s = (g'>>= f') s"
|
||||
proof -
|
||||
have pre: "\<And>aa bb. \<lbrakk>(aa, bb) \<in> fst (g s)\<rbrakk> \<Longrightarrow> Q aa bb"
|
||||
using hoare by (auto simp: valid_def)
|
||||
show ?thesis
|
||||
apply (simp add:bind_def eq split_def image_def)
|
||||
apply (rule conjI)
|
||||
apply (rule set_eqI)
|
||||
apply (clarsimp simp:Union_eq)
|
||||
apply (metis pre surjective_pairing tail)
|
||||
apply (metis pre surjective_pairing tail)
|
||||
done
|
||||
qed
|
||||
|
||||
lemma monad_eq_split_tail:
|
||||
"\<lbrakk>f = g;a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)"
|
||||
by (simp add:bind_def)
|
||||
|
||||
definition monad_commute where
|
||||
"monad_commute P a b \<equiv>
|
||||
(\<forall>s. (P s \<longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; return (x, y) od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; return (x, y) od) s)))"
|
||||
|
||||
|
||||
lemma monad_eq:
|
||||
"a s = b s \<Longrightarrow> (a >>= g) s = (b >>= g) s"
|
||||
by (auto simp:bind_def)
|
||||
|
||||
lemma monad_commute_simple:
|
||||
"\<lbrakk>monad_commute P a b;P s\<rbrakk> \<Longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; g x y od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; g x y od) s)"
|
||||
apply (clarsimp simp:monad_commute_def)
|
||||
apply (drule spec)
|
||||
apply (erule(1) impE)
|
||||
apply (drule_tac g = "(\<lambda>t. g (fst t) (snd t))" in monad_eq)
|
||||
apply (simp add:bind_assoc)
|
||||
done
|
||||
|
||||
lemma commute_commute:
|
||||
"monad_commute P f h \<Longrightarrow> monad_commute P h f"
|
||||
apply (simp (no_asm) add: monad_commute_def)
|
||||
apply (clarsimp)
|
||||
apply (erule monad_commute_simple[symmetric])
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma assert_commute: "monad_commute (K G) (assert G) f"
|
||||
by (clarsimp simp:assert_def monad_commute_def)
|
||||
|
||||
lemma cond_fail_commute: "monad_commute (K (\<not>G)) (when G fail) f"
|
||||
by (clarsimp simp:when_def fail_def monad_commute_def)
|
||||
|
||||
lemma return_commute: "monad_commute \<top> (return a) f"
|
||||
by (clarsimp simp: return_def bind_def monad_commute_def)
|
||||
|
||||
lemma monad_commute_guard_imp:
|
||||
"\<lbrakk>monad_commute P f h; \<And>s. Q s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> monad_commute Q f h"
|
||||
by (clarsimp simp:monad_commute_def)
|
||||
|
||||
lemma monad_commute_split:
|
||||
"\<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h;
|
||||
\<lbrace>P'\<rbrace> h \<lbrace>\<lambda>r. Q r\<rbrace>\<rbrakk>
|
||||
\<Longrightarrow> monad_commute (P and P') f (h>>=g)"
|
||||
apply (simp (no_asm) add:monad_commute_def)
|
||||
apply (clarsimp simp:bind_assoc)
|
||||
apply (subst monad_commute_simple)
|
||||
apply simp+
|
||||
apply (rule_tac Q = "(\<lambda>x. Q x)" in monad_eq_split)
|
||||
apply (subst monad_commute_simple[where a = f])
|
||||
apply assumption
|
||||
apply simp+
|
||||
done
|
||||
|
||||
lemma monad_commute_get:
|
||||
assumes hf: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>"
|
||||
and hg: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>"
|
||||
and eptyf: "empty_fail f" "empty_fail g"
|
||||
shows "monad_commute \<top> f g"
|
||||
proof -
|
||||
have fsame: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s"
|
||||
by (drule use_valid[OF _ hf],auto)
|
||||
have gsame: "\<And>a b s. (a,b) \<in> fst (g s) \<Longrightarrow> b = s"
|
||||
by (drule use_valid[OF _ hg],auto)
|
||||
note ef = empty_fail_not_snd[OF _ eptyf(1)]
|
||||
note eg = empty_fail_not_snd[OF _ eptyf(2)]
|
||||
show ?thesis
|
||||
apply (simp add:monad_commute_def)
|
||||
apply (clarsimp simp:bind_def split_def return_def)
|
||||
apply (intro conjI)
|
||||
apply (rule set_eqI)
|
||||
apply (rule iffI)
|
||||
apply (clarsimp simp:Union_eq dest!: singletonD)
|
||||
apply (frule fsame)
|
||||
apply clarsimp
|
||||
apply (frule gsame)
|
||||
apply (metis fst_conv snd_conv)
|
||||
apply (clarsimp simp:Union_eq dest!: singletonD)
|
||||
apply (frule gsame)
|
||||
apply clarsimp
|
||||
apply (frule fsame)
|
||||
apply clarsimp
|
||||
apply (metis fst_conv snd_conv)
|
||||
apply (rule iffI)
|
||||
apply (erule disjE)
|
||||
apply (clarsimp simp:image_def)
|
||||
apply (metis fsame)
|
||||
apply (clarsimp simp:image_def)
|
||||
apply (drule eg)
|
||||
apply clarsimp
|
||||
apply (rule bexI [rotated], assumption)
|
||||
apply (frule gsame)
|
||||
apply clarsimp
|
||||
apply (erule disjE)
|
||||
apply (clarsimp simp:image_def dest!:gsame)
|
||||
apply (clarsimp simp:image_def)
|
||||
apply (drule ef)
|
||||
apply clarsimp
|
||||
apply (frule fsame)
|
||||
apply (erule bexI[rotated])
|
||||
apply simp
|
||||
done
|
||||
qed
|
||||
|
||||
lemma mapM_x_commute:
|
||||
assumes commute:
|
||||
"\<And>r. monad_commute (P r) a (b r)"
|
||||
and single:
|
||||
"\<And>r x. \<lbrace>P r and K (f r \<noteq> f x) and P x\<rbrace> b x \<lbrace>\<lambda>v. P r \<rbrace>"
|
||||
shows
|
||||
"monad_commute (\<lambda>s. (distinct (map f list)) \<and> (\<forall>r\<in> set list. P r s)) a (mapM_x b list)"
|
||||
apply (induct list)
|
||||
apply (clarsimp simp:mapM_x_Nil return_def bind_def monad_commute_def)
|
||||
apply (clarsimp simp:mapM_x_Cons)
|
||||
apply (rule monad_commute_guard_imp)
|
||||
apply (rule monad_commute_split)
|
||||
apply assumption
|
||||
apply (rule monad_commute_guard_imp[OF commute])
|
||||
apply assumption
|
||||
apply (wp hoare_vcg_ball_lift)
|
||||
apply (rule single)
|
||||
apply (clarsimp simp: image_def)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma commute_name_pre_state:
|
||||
assumes "\<And>s. P s \<Longrightarrow> monad_commute (op = s) f g"
|
||||
shows "monad_commute P f g"
|
||||
using assms
|
||||
by (clarsimp simp:monad_commute_def)
|
||||
|
||||
lemma commute_rewrite:
|
||||
assumes rewrite: "\<And>s. Q s \<Longrightarrow> f s = t s"
|
||||
and hold : "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>x. Q\<rbrace>"
|
||||
shows "monad_commute R t g \<Longrightarrow> monad_commute (P and Q and R) f g"
|
||||
apply (clarsimp simp:monad_commute_def bind_def split_def return_def)
|
||||
apply (drule_tac x = s in spec)
|
||||
apply (clarsimp simp:rewrite[symmetric])
|
||||
apply (intro conjI)
|
||||
apply (rule set_eqI)
|
||||
apply (rule iffI)
|
||||
apply clarsimp
|
||||
apply (rule bexI[rotated],assumption)
|
||||
apply (subst rewrite)
|
||||
apply (rule use_valid[OF _ hold])
|
||||
apply simp+
|
||||
apply (erule bexI[rotated],simp)
|
||||
apply clarsimp
|
||||
apply (rule bexI[rotated],assumption)
|
||||
apply (subst rewrite[symmetric])
|
||||
apply (rule use_valid[OF _ hold])
|
||||
apply simp+
|
||||
apply (erule bexI[rotated],simp)
|
||||
apply (intro iffI)
|
||||
apply clarsimp
|
||||
apply (rule bexI[rotated],assumption)
|
||||
apply simp
|
||||
apply (subst rewrite)
|
||||
apply (erule(1) use_valid[OF _ hold])
|
||||
apply simp
|
||||
apply (clarsimp)
|
||||
apply (drule bspec,assumption)
|
||||
apply clarsimp
|
||||
apply (metis rewrite use_valid[OF _ hold])
|
||||
done
|
||||
|
||||
|
||||
lemma commute_grab_asm:
|
||||
"(F \<Longrightarrow> monad_commute P f g) \<Longrightarrow> (monad_commute (P and (K F)) f g)"
|
||||
by (clarsimp simp: monad_commute_def)
|
||||
|
|
|
|||
|
|
@ -49,6 +49,11 @@ session AInvs = ASpec +
|
|||
"invariant-abstract/KernelInit_AI"
|
||||
"invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI"
|
||||
|
||||
session AInvsQD = ASpec +
|
||||
theories [quick_and_dirty]
|
||||
"invariant-abstract/AInvs"
|
||||
"invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI"
|
||||
|
||||
|
||||
(*
|
||||
* C Refinement proof.
|
||||
|
|
@ -172,7 +177,7 @@ session AutoLevity = AutoLevity_Base +
|
|||
theories
|
||||
"../lib/autolevity_buckets/AutoLevity_Top"
|
||||
|
||||
session AutoLevity_Base = Word_Lib +
|
||||
session AutoLevity_Base = Word_Lib +
|
||||
theories
|
||||
"../lib/autolevity_buckets/AutoLevity_Base"
|
||||
|
||||
|
|
|
|||
|
|
@ -261,7 +261,7 @@ end
|
|||
interpretation AInvsPre?: AInvsPre
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_asms)?)
|
||||
case 1 show ?case apply (intro_locales; (unfold_locales, fact AInvsPre_asms)?) sorry
|
||||
qed
|
||||
|
||||
requalify_facts
|
||||
|
|
|
|||
|
|
@ -504,8 +504,8 @@ lemma update_aobj_pred_tcb_at[wp]:
|
|||
apply (clarsimp simp: pred_tcb_at_def obj_at_def a_type_def)
|
||||
done
|
||||
|
||||
lemma update_aobj_cur [wp]:
|
||||
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
|
||||
lemma update_object_cur_thread [wp]:
|
||||
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> update_object ptr obj \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
|
||||
unfolding update_object_def by (wp get_object_wp) simp
|
||||
|
||||
lemma update_aobj_cur_tcb [wp]:
|
||||
|
|
@ -1242,19 +1242,19 @@ end
|
|||
|
||||
context begin
|
||||
|
||||
method finish =
|
||||
method hammer =
|
||||
(simp?; erule is_aligned_weaken[rotated]; simp add: is_aligned_def pptrBase_def)
|
||||
|
||||
lemma is_aligned_addrFromPPtr_eq: "n \<le> 39 \<Longrightarrow> is_aligned (addrFromPPtr p) n = is_aligned p n"
|
||||
apply (simp add: addrFromPPtr_def; rule iffI)
|
||||
apply (drule aligned_sub_aligned[where y="-pptrBase"]; finish)
|
||||
apply (erule aligned_sub_aligned; finish)
|
||||
apply (drule aligned_sub_aligned[where y="-pptrBase"]; hammer)
|
||||
apply (erule aligned_sub_aligned; hammer)
|
||||
done
|
||||
|
||||
lemma is_aligned_ptrFromPAddr_eq: "n \<le> 39 \<Longrightarrow> is_aligned (ptrFromPAddr p) n = is_aligned p n"
|
||||
apply (simp add: ptrFromPAddr_def; rule iffI)
|
||||
apply (drule aligned_add_aligned[where y="-pptrBase"]; finish)
|
||||
apply (erule aligned_add_aligned; finish)
|
||||
apply (drule aligned_add_aligned[where y="-pptrBase"]; hammer)
|
||||
apply (erule aligned_add_aligned; hammer)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -125,6 +125,9 @@ lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fau
|
|||
apply (simp | wp)+
|
||||
done
|
||||
|
||||
lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
|
||||
by (cases b) wpsimp
|
||||
|
||||
lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
|
||||
apply (cases e)
|
||||
apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
|
||||
|
|
|
|||
|
|
@ -467,6 +467,7 @@ lemma zombie_is_cap_toE_pre[CNodeInv_AI_assms]:
|
|||
apply (simp add: nat_to_cref_def word_bits_conv)
|
||||
done
|
||||
|
||||
crunch st_tcb_at_halted[wp]: prepare_thread_delete "st_tcb_at halted t"
|
||||
|
||||
lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
|
||||
"\<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s)
|
||||
|
|
@ -513,6 +514,11 @@ lemma nat_to_cref_0_replicate [CNodeInv_AI_assms]:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma prepare_thread_delete_thread_cap [CNodeInv_AI_assms]:
|
||||
"\<lbrace>\<lambda>s. caps_of_state s x = Some (cap.ThreadCap p)\<rbrace>
|
||||
prepare_thread_delete t
|
||||
\<lbrace>\<lambda>rv s. caps_of_state s x = Some (cap.ThreadCap p)\<rbrace>"
|
||||
by (wpsimp simp: prepare_thread_delete_def)
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,84 @@
|
|||
(*
|
||||
* Copyright 2016, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_GPL)
|
||||
*)
|
||||
|
||||
theory ArchDetSchedDomainTime_AI
|
||||
imports "../DetSchedDomainTime_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
named_theorems DetSchedDomainTime_AI_assms
|
||||
|
||||
lemma flush_table_domain_list_inv[wp]: "\<lbrace>\<lambda>s. P (domain_list s)\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
lemma flush_table_domain_time_inv[wp]: "\<lbrace>\<lambda>s. P (domain_time s)\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]: arch_finalise_cap "\<lambda>s. P (domain_list s)"
|
||||
(wp: hoare_drop_imps mapM_wp mapM_x_wp' subset_refl simp: crunch_simps)
|
||||
|
||||
crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]:
|
||||
arch_activate_idle_thread, arch_switch_to_thread, arch_switch_to_idle_thread,
|
||||
handle_arch_fault_reply, init_arch_objects, arch_tcb_set_ipc_buffer,
|
||||
arch_invoke_irq_control, handle_vm_fault,
|
||||
prepare_thread_delete, handle_hypervisor_fault
|
||||
"\<lambda>s. P (domain_list s)"
|
||||
|
||||
crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]: arch_perform_invocation "\<lambda>s. P (domain_list s)"
|
||||
(wp: crunch_wps check_cap_inv)
|
||||
|
||||
crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: arch_finalise_cap "\<lambda>s. P (domain_time s)"
|
||||
(wp: hoare_drop_imps mapM_wp subset_refl simp: crunch_simps)
|
||||
|
||||
crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]:
|
||||
arch_activate_idle_thread, arch_switch_to_thread, arch_switch_to_idle_thread,
|
||||
handle_arch_fault_reply, init_arch_objects, arch_tcb_set_ipc_buffer,
|
||||
arch_invoke_irq_control, handle_vm_fault,
|
||||
prepare_thread_delete, handle_hypervisor_fault
|
||||
"\<lambda>s. P (domain_time s)"
|
||||
|
||||
crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: arch_perform_invocation "\<lambda>s. P (domain_time s)"
|
||||
(wp: crunch_wps check_cap_inv)
|
||||
|
||||
crunch exst[wp]: do_machine_op "\<lambda>s. P (exst s)"
|
||||
|
||||
crunch inv[wp]: get_irq_slot P
|
||||
|
||||
lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
|
||||
"\<lbrace>\<lambda>s :: det_ext state. 0 < domain_time s \<rbrace> handle_interrupt i
|
||||
\<lbrace>\<lambda>rv s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread \<rbrace>"
|
||||
apply (unfold handle_interrupt_def)
|
||||
apply (case_tac "maxIRQ < i"; simp)
|
||||
subgoal by (wp hoare_false_imp, simp)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp do_machine_op_exst | simp | wpc)+
|
||||
apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
|
||||
apply wp
|
||||
apply (wp get_cap_wp)
|
||||
apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
|
||||
apply wp+
|
||||
apply simp (* dxo_eq *)
|
||||
apply (clarsimp simp: timer_tick_def num_domains_def)
|
||||
apply (wp reschedule_required_valid_domain_time
|
||||
| simp add: handle_reserved_irq_def
|
||||
| wp_once hoare_drop_imp)+
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
global_interpretation DetSchedDomainTime_AI?: DetSchedDomainTime_AI
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact DetSchedDomainTime_AI_assms)?)
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,310 @@
|
|||
(*
|
||||
* Copyright 2016, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_GPL)
|
||||
*)
|
||||
|
||||
theory ArchDetSchedSchedule_AI
|
||||
imports "../DetSchedSchedule_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
named_theorems DetSchedSchedule_AI_assms
|
||||
|
||||
crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_switch_to_idle_thread, arch_switch_to_thread valid_etcbs
|
||||
(simp: whenE_def ignore: )
|
||||
|
||||
crunch valid_queues [wp, DetSchedSchedule_AI_assms]:
|
||||
switch_to_idle_thread, switch_to_thread valid_queues
|
||||
(simp: whenE_def ignore: set_tcb_queue tcb_sched_action )
|
||||
|
||||
crunch weak_valid_sched_action [wp, DetSchedSchedule_AI_assms]:
|
||||
switch_to_idle_thread, switch_to_thread "weak_valid_sched_action"
|
||||
(simp: whenE_def ignore: )
|
||||
|
||||
lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_queues and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
|
||||
apply (simp add: switch_to_idle_thread_def)
|
||||
apply wp
|
||||
apply (simp add: arch_switch_to_idle_thread_def)
|
||||
apply wp+
|
||||
apply (fastforce simp: valid_queues_def ct_not_in_q_def not_queued_def
|
||||
valid_idle_def pred_tcb_at_def obj_at_def)
|
||||
done
|
||||
|
||||
lemma switch_to_idle_thread_valid_sched_action [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_sched_action and valid_idle\<rbrace>
|
||||
switch_to_idle_thread
|
||||
\<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
|
||||
apply (simp add: switch_to_idle_thread_def)
|
||||
apply wp
|
||||
apply (simp add: arch_switch_to_idle_thread_def do_machine_op_def split_def)
|
||||
apply wp+
|
||||
apply (clarsimp simp: valid_sched_action_def valid_idle_def is_activatable_def
|
||||
pred_tcb_at_def obj_at_def)
|
||||
done
|
||||
|
||||
lemma switch_to_idle_thread_ct_in_cur_domain [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>"
|
||||
by (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def do_machine_op_def
|
||||
split_def ct_in_cur_domain_def
|
||||
| wp)+
|
||||
|
||||
crunch ct_not_in_q [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread ct_not_in_q
|
||||
(simp: whenE_def ignore: )
|
||||
|
||||
crunch is_activatable [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread "is_activatable t"
|
||||
(simp: whenE_def ignore: )
|
||||
|
||||
crunch valid_sched_action [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread valid_sched_action
|
||||
(simp: whenE_def ignore: )
|
||||
|
||||
crunch valid_sched [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread valid_sched
|
||||
(simp: whenE_def ignore: )
|
||||
|
||||
crunch exst[wp]: set_vm_root "\<lambda>s. P (exst s)"
|
||||
(wp: crunch_wps hoare_whenE_wp simp: crunch_simps)
|
||||
|
||||
crunch ct_in_cur_domain_2[wp]: set_vm_root
|
||||
"\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)"
|
||||
(simp: whenE_def)
|
||||
|
||||
crunch ct_in_cur_domain_2 [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread
|
||||
"\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)"
|
||||
(simp: whenE_def)
|
||||
|
||||
crunch valid_blocked[wp]: set_vm_root valid_blocked
|
||||
(simp: crunch_simps)
|
||||
|
||||
crunch ct_in_q[wp]: set_vm_root ct_in_q
|
||||
(simp: crunch_simps)
|
||||
|
||||
crunch etcb_at [wp, DetSchedSchedule_AI_assms]: switch_to_thread "etcb_at P t"
|
||||
|
||||
crunch valid_idle [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_switch_to_idle_thread "valid_idle :: det_ext state \<Rightarrow> bool"
|
||||
|
||||
crunch etcb_at [wp, DetSchedSchedule_AI_assms]: arch_switch_to_idle_thread "etcb_at P t"
|
||||
|
||||
crunch scheduler_action [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_switch_to_idle_thread, next_domain "\<lambda>s. P (scheduler_action s)"
|
||||
(simp: Let_def)
|
||||
|
||||
lemma set_vm_root_valid_blocked_ct_in_q [wp]:
|
||||
"\<lbrace>valid_blocked and ct_in_q\<rbrace> set_vm_root p \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>"
|
||||
by (wp | wpc | auto)+
|
||||
|
||||
lemma arch_switch_to_thread_valid_blocked [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_blocked and ct_in_q\<rbrace> arch_switch_to_thread thread \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>"
|
||||
apply (simp add: arch_switch_to_thread_def)
|
||||
apply wp
|
||||
done
|
||||
|
||||
lemma switch_to_idle_thread_ct_not_queued [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_queues and valid_etcbs and valid_idle\<rbrace>
|
||||
switch_to_idle_thread
|
||||
\<lbrace>\<lambda>rv s. not_queued (cur_thread s) s\<rbrace>"
|
||||
apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def
|
||||
tcb_sched_action_def | wp)+
|
||||
apply (fastforce simp: valid_sched_2_def valid_queues_2_def valid_idle_def
|
||||
pred_tcb_at_def obj_at_def not_queued_def)
|
||||
done
|
||||
|
||||
lemma switch_to_idle_thread_valid_blocked [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_blocked and ct_in_q\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. valid_blocked\<rbrace>"
|
||||
apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def do_machine_op_def | wp | wpc)+
|
||||
apply clarsimp
|
||||
apply (drule(1) ct_in_q_valid_blocked_ct_upd)
|
||||
apply simp
|
||||
done
|
||||
|
||||
crunch exst [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread "\<lambda>s. P (exst s :: det_ext)"
|
||||
(ignore: )
|
||||
|
||||
lemma stit_activatable' [DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>"
|
||||
apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def do_machine_op_def split_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: valid_idle_def ct_in_state_def pred_tcb_at_def obj_at_def)
|
||||
done
|
||||
|
||||
lemma switch_to_idle_thread_cur_thread_idle_thread [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_ s. cur_thread s = idle_thread s\<rbrace>"
|
||||
by (wp | simp add:switch_to_idle_thread_def arch_switch_to_idle_thread_def)+
|
||||
|
||||
lemma set_pm_valid_etcbs[wp]:
|
||||
"\<lbrace>valid_etcbs\<rbrace> set_pml4 ptr pm \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_etcbs_lift del: set_pml4_typ_at | simp add: set_pml4_def)+
|
||||
|
||||
lemma set_pdpt_valid_etcbs[wp]:
|
||||
"\<lbrace>valid_etcbs\<rbrace> set_pdpt ptr pd \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_etcbs_lift del: set_pdpt_typ_at | simp add: set_pdpt_def)+
|
||||
|
||||
lemma set_pd_valid_etcbs[wp]:
|
||||
"\<lbrace>valid_etcbs\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_etcbs_lift del: set_pd_typ_at | simp add: set_pd_def)+
|
||||
|
||||
lemma set_pt_valid_etcbs[wp]:
|
||||
"\<lbrace>valid_etcbs\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_etcbs_lift | simp add: set_pt_def)+
|
||||
|
||||
lemma set_asid_pool_valid_etcbs[wp]:
|
||||
"\<lbrace>valid_etcbs\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_asid_pool_def)+
|
||||
|
||||
lemma set_pt_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp hoare_drop_imps valid_sched_lift | simp add: set_pt_def)+
|
||||
|
||||
lemma set_pm_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> set_pml4 ptr pm \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_sched_lift del: set_pml4_typ_at | simp add: set_pml4_def)+
|
||||
|
||||
lemma set_pdpt_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> set_pdpt ptr pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_sched_lift del: set_pdpt_typ_at | simp add: set_pdpt_def)+
|
||||
|
||||
lemma set_pd_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_sched_lift del: set_pd_typ_at | simp add: set_pd_def)+
|
||||
|
||||
lemma set_asid_pool_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp hoare_drop_imps valid_sched_lift | simp add: set_asid_pool_def)+
|
||||
|
||||
crunch ct_not_in_q[wp]: update_object ct_not_in_q
|
||||
(wp: crunch_wps hoare_drop_imps hoare_unless_wp select_inv mapM_wp
|
||||
subset_refl if_fun_split simp: crunch_simps ignore: tcb_sched_action)
|
||||
|
||||
lemma flush_table_ct_not_in_q[wp]: "\<lbrace>ct_not_in_q\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. ct_not_in_q\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
crunch ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_finalise_cap, prepare_thread_delete ct_not_in_q
|
||||
(wp: crunch_wps hoare_drop_imps hoare_unless_wp select_inv mapM_wp
|
||||
subset_refl if_fun_split simp: crunch_simps ignore: tcb_sched_action)
|
||||
|
||||
lemma flush_table_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
lemma update_object_valid_etcbs[wp]:
|
||||
"\<lbrace>valid_etcbs\<rbrace> update_object f tptr \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
|
||||
by (wp hoare_drop_imps valid_etcbs_lift | simp add: update_object_def)+
|
||||
|
||||
crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_finalise_cap, prepare_thread_delete valid_etcbs
|
||||
(wp: hoare_drop_imps hoare_unless_wp select_inv mapM_x_wp mapM_wp subset_refl
|
||||
if_fun_split simp: crunch_simps ignore: update_object set_object thread_set)
|
||||
|
||||
lemma flush_table_simple_sched_action[wp]: "\<lbrace>simple_sched_action\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_finalise_cap, prepare_thread_delete simple_sched_action
|
||||
(wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl crunch_wps
|
||||
simp: unless_def if_fun_split crunch_simps)
|
||||
|
||||
lemma flush_table_valid_sched[wp]: "\<lbrace>valid_sched\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
lemma store_pte_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> store_pte pter pte \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp hoare_drop_imps valid_sched_lift | simp add: store_pte_def)+
|
||||
|
||||
lemma store_pm_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> store_pml4e pter pm \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_sched_lift del: store_pml4e_typ_at | simp add: store_pml4e_def)+
|
||||
|
||||
lemma store_pdepte_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> store_pdpte pter pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_sched_lift del: store_pdpte_typ_at | simp add: store_pdpte_def)+
|
||||
|
||||
lemma store_pde_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> store_pde pter pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp add: hoare_drop_imps valid_sched_lift del: store_pde_typ_at | simp add: store_pde_def)+
|
||||
|
||||
crunch valid_sched [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_tcb_set_ipc_buffer, arch_finalise_cap, prepare_thread_delete valid_sched
|
||||
(ignore: set_object update_object wp: crunch_wps subset_refl simp: if_fun_split crunch_simps)
|
||||
|
||||
lemma activate_thread_valid_sched [DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>valid_sched\<rbrace> activate_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>"
|
||||
apply (simp add: activate_thread_def)
|
||||
apply (wp set_thread_state_runnable_valid_sched gts_wp | wpc | simp add: arch_activate_idle_thread_def)+
|
||||
apply (force elim: st_tcb_weakenE)
|
||||
done
|
||||
|
||||
lemma store_asid_pool_entry_valid_sched[wp]:
|
||||
"\<lbrace>valid_sched\<rbrace> store_asid_pool_entry ptr pool a \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
|
||||
by (wp hoare_drop_imps valid_sched_lift | simp add: store_asid_pool_entry_def)+
|
||||
|
||||
crunch valid_sched[wp]:
|
||||
perform_page_invocation, perform_page_table_invocation, perform_asid_pool_invocation,
|
||||
perform_page_directory_invocation, perform_io_port_invocation, perform_pdpt_invocation
|
||||
valid_sched
|
||||
(wp: mapM_x_wp' mapM_wp')
|
||||
|
||||
lemma arch_perform_invocation_valid_sched [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>invs and valid_sched and ct_active and valid_arch_inv a\<rbrace>
|
||||
arch_perform_invocation a
|
||||
\<lbrace>\<lambda>_.valid_sched\<rbrace>"
|
||||
apply (cases a, simp_all add: arch_perform_invocation_def)
|
||||
apply (wp perform_asid_control_invocation_valid_sched | wpc |
|
||||
simp add: valid_arch_inv_def invs_valid_idle)+
|
||||
done
|
||||
|
||||
crunch valid_sched [wp, DetSchedSchedule_AI_assms]:
|
||||
handle_arch_fault_reply, handle_vm_fault valid_sched
|
||||
(ignore: )
|
||||
|
||||
crunch not_queued [wp, DetSchedSchedule_AI_assms]:
|
||||
handle_vm_fault, handle_arch_fault_reply "not_queued t"
|
||||
(ignore: )
|
||||
|
||||
crunch sched_act_not [wp, DetSchedSchedule_AI_assms]:
|
||||
handle_arch_fault_reply, handle_vm_fault "scheduler_act_not t"
|
||||
(ignore: )
|
||||
|
||||
lemma hvmf_st_tcb_at [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace>st_tcb_at P t' \<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at P t' \<rbrace>"
|
||||
by (cases w, simp_all) ((wp | simp)+)
|
||||
|
||||
lemma handle_vm_fault_st_tcb_cur_thread [wp, DetSchedSchedule_AI_assms]:
|
||||
"\<lbrace> \<lambda>s. st_tcb_at P (cur_thread s) s \<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_ s. st_tcb_at P (cur_thread s) s \<rbrace>"
|
||||
apply (fold ct_in_state_def)
|
||||
apply (rule ct_in_state_thread_state_lift)
|
||||
apply (cases f)
|
||||
apply (wp|simp)+
|
||||
done
|
||||
|
||||
crunch valid_sched [wp, DetSchedSchedule_AI_assms]: arch_invoke_irq_control "valid_sched"
|
||||
|
||||
crunch valid_list [wp, DetSchedSchedule_AI_assms]:
|
||||
arch_activate_idle_thread, arch_switch_to_thread, arch_switch_to_idle_thread "valid_list"
|
||||
|
||||
crunch cur_tcb [wp, DetSchedSchedule_AI_assms]: handle_arch_fault_reply, handle_vm_fault cur_tcb
|
||||
|
||||
crunch valid_sched [wp, DetSchedSchedule_AI_assms]: handle_hypervisor_fault valid_sched
|
||||
(ignore:)
|
||||
|
||||
crunch not_queued [wp, DetSchedSchedule_AI_assms]: handle_hypervisor_fault "not_queued t"
|
||||
(ignore:)
|
||||
|
||||
crunch sched_act_not [wp, DetSchedSchedule_AI_assms]: handle_hypervisor_fault "scheduler_act_not t"
|
||||
(ignore:)
|
||||
|
||||
end
|
||||
|
||||
global_interpretation DetSchedSchedule_AI?: DetSchedSchedule_AI
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact DetSchedSchedule_AI_assms)?)
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -93,7 +93,8 @@ crunch valid_list[wp]: perform_invocation valid_list
|
|||
crunch valid_list[wp, Deterministic_AI_assms]: handle_invocation valid_list
|
||||
(wp: crunch_wps syscall_valid simp: crunch_simps ignore: without_preemption)
|
||||
|
||||
crunch valid_list[wp, Deterministic_AI_assms]: handle_recv, handle_yield, handle_call valid_list
|
||||
crunch valid_list[wp, Deterministic_AI_assms]: handle_recv, handle_yield, handle_call,
|
||||
handle_hypervisor_fault valid_list
|
||||
(wp: crunch_wps simp: crunch_simps)
|
||||
|
||||
lemma handle_vm_fault_valid_list[wp, Deterministic_AI_assms]:
|
||||
|
|
|
|||
|
|
@ -352,6 +352,8 @@ lemma deleting_irq_handler_final [Finalise_AI_asms]:
|
|||
apply simp
|
||||
done
|
||||
|
||||
crunch is_final_cap'[wp]: prepare_thread_delete "is_final_cap' cap"
|
||||
|
||||
lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
|
||||
"\<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s
|
||||
\<and> cte_wp_at (op = cap) slot s\<rbrace>
|
||||
|
|
@ -385,10 +387,17 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
|
|||
apply (wp | wpc | simp only: simp_thms)+
|
||||
done
|
||||
|
||||
crunch typ_at_arch[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (typ_at T p s)"
|
||||
crunch typ_at_arch[wp,Finalise_AI_asms]: arch_finalise_cap, prepare_thread_delete "\<lambda>s. P (typ_at T p s)"
|
||||
(wp: crunch_wps simp: crunch_simps unless_def assertE_def
|
||||
ignore: maskInterrupt )
|
||||
|
||||
crunch valid_cap[wp]: prepare_thread_delete "valid_cap cap"
|
||||
crunch tcb_at[wp]: prepare_thread_delete "tcb_at p"
|
||||
crunch cte_wp_at[wp, Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (cte_wp_at P' p s)"
|
||||
crunch irq_node[wp, Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (interrupt_irq_node s)"
|
||||
crunch invs[wp]: prepare_thread_delete invs
|
||||
crunch caps_of_state[wp, Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (caps_of_state s)"
|
||||
|
||||
lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]:
|
||||
"\<lbrace>valid_cap cap\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv. valid_cap (fst rv)\<rbrace>"
|
||||
apply (cases cap, simp_all)
|
||||
|
|
@ -529,7 +538,7 @@ lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
|
|||
unbind_notification_valid_objs
|
||||
| clarsimp simp: o_def dom_tcb_cap_cases_lt_ARCH
|
||||
ran_tcb_cap_cases is_cap_simps
|
||||
cap_range_def
|
||||
cap_range_def prepare_thread_delete_def
|
||||
can_fast_finalise_def
|
||||
obj_irq_refs_subset
|
||||
vs_cap_ref_def unat_of_bl_length
|
||||
|
|
|
|||
|
|
@ -0,0 +1,400 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
(* Kernel init refinement. Currently axiomatised.
|
||||
*)
|
||||
|
||||
theory ArchKernelInit_AI
|
||||
imports
|
||||
"../ADT_AI"
|
||||
"../Tcb_AI"
|
||||
"../Arch_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64 (*FIXME: arch_split*)
|
||||
|
||||
text {*
|
||||
Showing that there is a state that satisfies the abstract invariants.
|
||||
*}
|
||||
|
||||
lemma [simp]: "is_aligned (0x1000 :: word32) 9" by (simp add: is_aligned_def)
|
||||
lemma [simp]: "is_aligned (0x2000 :: word32) 9" by (simp add: is_aligned_def)
|
||||
|
||||
lemmas ptr_defs = init_tcb_ptr_def idle_thread_ptr_def init_irq_node_ptr_def
|
||||
init_globals_frame_def init_global_pd_def
|
||||
lemmas state_defs = init_A_st_def init_kheap_def init_arch_state_def ptr_defs
|
||||
|
||||
lemma [simp]: "is_tcb (TCB t)" by (simp add: is_tcb_def)
|
||||
|
||||
lemma [simp]: "ran (empty_cnode n) = {Structures_A.NullCap}"
|
||||
apply (auto simp: ran_def empty_cnode_def)
|
||||
apply (rule_tac x="replicate n False" in exI)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma empty_cnode_apply[simp]:
|
||||
"(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = Structures_A.NullCap)"
|
||||
by (auto simp add: empty_cnode_def)
|
||||
|
||||
lemma valid_cs_size_empty[simp]:
|
||||
"valid_cs_size n (empty_cnode n) = (n < word_bits - cte_level_bits)"
|
||||
apply (simp add: valid_cs_size_def)
|
||||
apply (insert wf_empty_bits [of n])
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
lemma init_cdt [simp]:
|
||||
"cdt init_A_st = init_cdt"
|
||||
by (simp add: state_defs)
|
||||
|
||||
lemma mdp_parent_empty [simp]:
|
||||
"\<not>empty \<Turnstile> x \<rightarrow> y"
|
||||
apply clarsimp
|
||||
apply (drule tranclD)
|
||||
apply (clarsimp simp: cdt_parent_of_def)
|
||||
done
|
||||
|
||||
lemma descendants_empty [simp]:
|
||||
"descendants_of x empty = {}"
|
||||
by (clarsimp simp: descendants_of_def)
|
||||
|
||||
lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"
|
||||
by (simp add: is_reply_cap_def)
|
||||
|
||||
lemma [simp]: "cap_range Structures_A.NullCap = {}"
|
||||
by (simp add: cap_range_def)
|
||||
|
||||
lemma pde_mapping_bits_shift:
|
||||
fixes x :: "12 word"
|
||||
shows "x \<noteq> 0 \<Longrightarrow> 2 ^ pde_mapping_bits - 1 < (ucast x << pde_mapping_bits :: word32)"
|
||||
apply (simp only:shiftl_t2n pde_mapping_bits_def)
|
||||
apply (unfold word_less_alt)
|
||||
apply simp
|
||||
apply (unfold word_mult_def)
|
||||
apply simp
|
||||
apply (subst int_word_uint)
|
||||
apply (subst mod_pos_pos_trivial)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (subst uint_up_ucast)
|
||||
apply (simp add: is_up_def source_size_def target_size_def word_size)
|
||||
apply (cut_tac 'a = "12" and x = x in uint_lt2p)
|
||||
apply simp
|
||||
apply (rule order_less_le_trans)
|
||||
prefer 2
|
||||
apply (rule pos_mult_pos_ge)
|
||||
apply (subst uint_up_ucast)
|
||||
apply (simp add: is_up_def source_size_def target_size_def word_size)
|
||||
apply (simp add: word_neq_0_conv word_less_alt)
|
||||
apply simp
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma mask_pde_mapping_bits:
|
||||
"mask 20 = 2^pde_mapping_bits - 1"
|
||||
by (simp add: mask_def pde_mapping_bits_def)
|
||||
|
||||
|
||||
|
||||
lemma init_irq_ptrs_ineqs:
|
||||
"init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
|
||||
"init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
|
||||
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
|
||||
"init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
|
||||
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
|
||||
proof -
|
||||
have P: "ucast irq < (2 ^ (14 - cte_level_bits) :: word32)"
|
||||
apply (rule order_le_less_trans[OF
|
||||
ucast_le_ucast[where 'a=10 and 'b=32,simplified,THEN iffD2, OF word_n1_ge]])
|
||||
apply (simp add: cte_level_bits_def minus_one_norm)
|
||||
done
|
||||
show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
|
||||
apply (rule is_aligned_no_wrap'[where sz=14])
|
||||
apply (simp add: is_aligned_def init_irq_node_ptr_def kernel_base_def)
|
||||
apply (rule shiftl_less_t2n[OF P])
|
||||
apply simp
|
||||
done
|
||||
show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
|
||||
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
|
||||
apply (simp only: add_diff_eq[symmetric] add.assoc)
|
||||
apply (rule word_add_le_mono2)
|
||||
apply (simp only: trans [OF shiftl_t2n mult.commute])
|
||||
apply (rule nasty_split_lt[OF P])
|
||||
apply (simp_all add: cte_level_bits_def
|
||||
word_bits_def kernel_base_def init_irq_node_ptr_def)
|
||||
done
|
||||
show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
|
||||
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
|
||||
apply (simp only: add_diff_eq[symmetric])
|
||||
apply (rule word_add_le_mono2)
|
||||
apply (rule minus_one_helper3, rule shiftl_less_t2n[OF P])
|
||||
apply simp
|
||||
apply (simp add: kernel_base_def
|
||||
cte_level_bits_def word_bits_def init_irq_node_ptr_def)
|
||||
done
|
||||
qed
|
||||
|
||||
lemmas init_irq_ptrs_less_ineqs
|
||||
= init_irq_ptrs_ineqs(1)[THEN order_less_le_trans[rotated]]
|
||||
init_irq_ptrs_ineqs(2-3)[THEN order_le_less_trans]
|
||||
|
||||
lemmas init_irq_ptrs_all_ineqs[unfolded init_irq_node_ptr_def cte_level_bits_def]
|
||||
= init_irq_ptrs_ineqs(1)[THEN order_trans[rotated]]
|
||||
init_irq_ptrs_ineqs(2-3)[THEN order_trans]
|
||||
init_irq_ptrs_less_ineqs
|
||||
init_irq_ptrs_less_ineqs[THEN less_imp_neq]
|
||||
init_irq_ptrs_less_ineqs[THEN less_imp_neq, THEN not_sym]
|
||||
|
||||
lemmas ucast_le_ucast_10_32 = ucast_le_ucast[where 'a=10 and 'b=32,simplified]
|
||||
lemma init_irq_ptrs_eq:
|
||||
"((ucast (irq :: irq) << cte_level_bits)
|
||||
= (ucast (irq' :: irq) << cte_level_bits :: word32))
|
||||
= (irq = irq')"
|
||||
apply safe
|
||||
apply (rule ccontr)
|
||||
apply (erule_tac bnd="ucast (max_word :: irq) + 1"
|
||||
in shift_distinct_helper[rotated 3],
|
||||
safe intro!: plus_one_helper2,
|
||||
simp_all add: ucast_le_ucast_10_32 up_ucast_inj_eq,
|
||||
simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq
|
||||
max_word_def)
|
||||
done
|
||||
|
||||
lemma in_kernel_base:
|
||||
"\<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF\<rbrakk> \<Longrightarrow> (\<forall>y\<in>{kernel_base + m .. n + kernel_base}.
|
||||
kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)"
|
||||
apply (clarsimp simp:)
|
||||
apply (intro conjI)
|
||||
apply (rule ccontr,simp add:not_le)
|
||||
apply (drule(1) le_less_trans)
|
||||
apply (cut_tac is_aligned_no_wrap'[where ptr = kernel_base and off = m
|
||||
and sz = 28,simplified])
|
||||
apply (drule(1) less_le_trans)
|
||||
apply simp
|
||||
apply (simp add:kernel_base_def is_aligned_def)
|
||||
apply (rule ccontr,simp add:not_less)
|
||||
apply (drule less_le_trans[where z = "0x10000000"])
|
||||
apply simp
|
||||
apply simp
|
||||
apply (erule order_trans)
|
||||
apply (simp add:field_simps)
|
||||
apply (rule word_plus_mono_right)
|
||||
apply simp
|
||||
apply (simp add:kernel_base_def)
|
||||
done
|
||||
|
||||
lemma pspace_aligned_init_A:
|
||||
"pspace_aligned init_A_st"
|
||||
apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
|
||||
dom_if_Some cte_level_bits_def)
|
||||
apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
|
||||
simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
|
||||
done
|
||||
|
||||
lemma pspace_distinct_init_A:
|
||||
"pspace_distinct init_A_st"
|
||||
apply (clarsimp simp: pspace_distinct_def state_defs pageBits_def
|
||||
empty_cnode_bits kernel_base_def
|
||||
cte_level_bits_def linorder_not_le cong: if_cong)
|
||||
apply (safe,
|
||||
simp_all add: init_irq_ptrs_all_ineqs
|
||||
[simplified kernel_base_def, simplified])[1]
|
||||
apply (cut_tac x="init_irq_node_ptr + (ucast irq << cte_level_bits)"
|
||||
and y="init_irq_node_ptr + (ucast irqa << cte_level_bits)"
|
||||
and sz=cte_level_bits in aligned_neq_into_no_overlap)
|
||||
apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
|
||||
apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
|
||||
apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
|
||||
kernel_base_def)
|
||||
apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
|
||||
apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
|
||||
kernel_base_def)
|
||||
apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def
|
||||
linorder_not_le)
|
||||
done
|
||||
|
||||
lemma caps_of_state_init_A_st_Null:
|
||||
"caps_of_state (init_A_st::'z::state_ext state) x
|
||||
= (if cte_at x (init_A_st::'z::state_ext state) then Some cap.NullCap else None)"
|
||||
apply (subgoal_tac "\<not> cte_wp_at (op \<noteq> cap.NullCap) x init_A_st")
|
||||
apply (auto simp add: cte_wp_at_caps_of_state)[1]
|
||||
apply (clarsimp, erule cte_wp_atE)
|
||||
apply (auto simp add: state_defs tcb_cap_cases_def split: if_split_asm)
|
||||
done
|
||||
|
||||
lemmas cte_wp_at_caps_of_state_eq
|
||||
= cte_wp_at_caps_of_state[where P="op = cap" for cap]
|
||||
|
||||
declare ptrFormPAddr_addFromPPtr[simp]
|
||||
|
||||
lemma pspace_respects_device_region_init[simp]:
|
||||
"pspace_respects_device_region init_A_st"
|
||||
apply (clarsimp simp: pspace_respects_device_region_def init_A_st_def init_machine_state_def device_mem_def
|
||||
in_device_frame_def obj_at_def init_kheap_def a_type_def)
|
||||
apply (rule ext)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma cap_refs_respects_device_region_init[simp]:
|
||||
"cap_refs_respects_device_region init_A_st"
|
||||
apply (clarsimp simp: cap_refs_respects_device_region_def)
|
||||
apply (frule cte_wp_at_caps_of_state[THEN iffD1])
|
||||
apply clarsimp
|
||||
apply (subst(asm) caps_of_state_init_A_st_Null)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_respects_device_region_def)
|
||||
done
|
||||
|
||||
lemma invs_A:
|
||||
"invs init_A_st"
|
||||
|
||||
apply (simp add: invs_def)
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (simp add: cur_tcb_def state_defs obj_at_def)
|
||||
apply (simp add: valid_state_def)
|
||||
apply (rule conjI)
|
||||
apply (simp add: valid_pspace_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: kernel_base_def valid_objs_def state_defs
|
||||
valid_obj_def valid_vm_rights_def vm_kernel_only_def
|
||||
dom_if_Some cte_level_bits_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
|
||||
valid_cap_def obj_at_def valid_tcb_state_def
|
||||
cap_aligned_def word_bits_def valid_ipc_buffer_cap_simps)+
|
||||
apply (clarsimp simp: valid_cs_def word_bits_def cte_level_bits_def
|
||||
init_irq_ptrs_all_ineqs valid_tcb_def
|
||||
split: if_split_asm)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
|
||||
dom_if_Some cte_level_bits_def)
|
||||
apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
|
||||
simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
|
||||
apply (rule conjI)
|
||||
apply (simp add:pspace_distinct_init_A)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: if_live_then_nonz_cap_def obj_at_def state_defs)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: zombies_final_def cte_wp_at_cases state_defs
|
||||
tcb_cap_cases_def is_zombie_def)
|
||||
apply (clarsimp simp: sym_refs_def state_refs_of_def state_defs)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_mdb_def init_cdt_def no_mloop_def
|
||||
mdb_cte_at_def)
|
||||
apply (clarsimp simp: untyped_mdb_def caps_of_state_init_A_st_Null
|
||||
untyped_inc_def ut_revocable_def
|
||||
irq_revocable_def reply_master_revocable_def
|
||||
reply_mdb_def reply_caps_mdb_def
|
||||
reply_masters_mdb_def)
|
||||
apply (simp add:descendants_inc_def)
|
||||
apply (rule conjI)
|
||||
apply (simp add: valid_ioc_def init_A_st_def init_ioc_def cte_wp_at_cases2)
|
||||
apply (intro allI impI, elim exE conjE)
|
||||
apply (case_tac obj, simp_all add: cap_of_def)
|
||||
apply (clarsimp simp: init_kheap_def split: if_split_asm)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def state_defs)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def state_defs)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: if_unsafe_then_cap_def caps_of_state_init_A_st_Null)
|
||||
apply (clarsimp simp: valid_reply_caps_def unique_reply_caps_def
|
||||
has_reply_cap_def pred_tcb_at_def obj_at_def
|
||||
caps_of_state_init_A_st_Null
|
||||
cte_wp_at_caps_of_state_eq
|
||||
valid_reply_masters_def valid_global_refs_def
|
||||
valid_refs_def[unfolded cte_wp_at_caps_of_state])
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_arch_state_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_asid_table_def state_defs)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs
|
||||
a_type_def)
|
||||
apply (rule conjI)
|
||||
apply (simp add: valid_global_pts_def state_defs)
|
||||
apply (simp add: state_defs is_inv_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
|
||||
is_cap_table_def wf_empty_bits
|
||||
init_irq_ptrs_all_ineqs cte_level_bits_def
|
||||
init_irq_ptrs_eq[unfolded cte_level_bits_def])
|
||||
apply (intro conjI)
|
||||
apply (rule inj_onI)
|
||||
apply (simp add: init_irq_ptrs_eq[unfolded cte_level_bits_def])
|
||||
apply clarsimp
|
||||
defer
|
||||
apply (simp add: valid_irq_handlers_def caps_of_state_init_A_st_Null
|
||||
ran_def cong: rev_conj_cong)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_irq_states_def init_A_st_def init_machine_state_def valid_irq_masks_def init_irq_masks_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_machine_state_def init_A_st_def
|
||||
init_machine_state_def init_underlying_memory_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_arch_objs_def obj_at_def state_defs)
|
||||
apply (clarsimp simp: vs_lookup_def vs_asid_refs_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_arch_caps_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_vs_lookup_def)
|
||||
apply (clarsimp simp: vs_lookup_pages_def state_defs vs_asid_refs_def)
|
||||
apply (clarsimp simp: valid_table_caps_def caps_of_state_init_A_st_Null
|
||||
unique_table_caps_def unique_table_refs_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_global_objs_def state_defs)
|
||||
apply (clarsimp simp: valid_ao_at_def obj_at_def empty_table_def pde_ref_def
|
||||
valid_pde_mappings_def)
|
||||
apply (simp add: kernel_base_def kernel_mapping_slots_def
|
||||
Platform.ARM.addrFromPPtr_def physMappingOffset_def
|
||||
kernelBase_addr_def physBase_def pageBits_def is_aligned_def)
|
||||
apply (rule conjI)
|
||||
apply (simp add: valid_kernel_mappings_def state_defs
|
||||
valid_kernel_mappings_if_pd_def pde_ref_def
|
||||
ran_def)
|
||||
apply (auto simp: pde_ref_def split: if_split_asm)[1]
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: equal_kernel_mappings_def state_defs obj_at_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_asid_map_def state_defs)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_global_vspace_mappings_def obj_at_def state_defs
|
||||
valid_pd_kernel_mappings_def mask_pde_mapping_bits)
|
||||
apply (simp add: valid_pde_kernel_mappings_def kernel_base_def)
|
||||
apply (rule conjI)
|
||||
apply (fastforce simp:pde_mapping_bits_def)
|
||||
apply (intro ballI impI)
|
||||
apply (clarsimp simp:pde_mapping_bits_def)
|
||||
apply word_bitwise
|
||||
apply clarsimp
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pspace_in_kernel_window_def state_defs mask_def)
|
||||
apply (intro conjI impI)
|
||||
apply (rule in_kernel_base|simp)+
|
||||
apply (erule exE,drule sym,simp add:field_simps)
|
||||
apply (rule in_kernel_base[simplified add.commute])
|
||||
apply (rule word_less_add_right,simp add:cte_level_bits_def)
|
||||
apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
|
||||
apply simp
|
||||
apply (simp add:cte_level_bits_def field_simps)
|
||||
apply (subst add.commute)
|
||||
apply (rule le_plus')
|
||||
apply simp+
|
||||
apply (rule less_imp_le)
|
||||
apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
|
||||
apply (rule in_kernel_base|simp)+
|
||||
apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
|
||||
valid_refs_def[unfolded cte_wp_at_caps_of_state])
|
||||
apply word_bitwise
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -93,6 +93,11 @@ crunch cur_thread[wp,Syscall_AI_assms]: handle_arch_fault_reply "\<lambda>s. P (
|
|||
crunch valid_objs[wp,Syscall_AI_assms]: handle_arch_fault_reply "valid_objs"
|
||||
crunch cte_wp_at[wp,Syscall_AI_assms]: handle_arch_fault_reply "\<lambda>s. P (cte_wp_at P' p s)"
|
||||
|
||||
|
||||
lemma hh_invs[wp, Syscall_AI_assms]:
|
||||
"\<lbrace>invs and ct_active\<rbrace> handle_hypervisor_fault thread fault \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
by (cases fault) wpsimp
|
||||
|
||||
end
|
||||
|
||||
global_interpretation Syscall_AI?: Syscall_AI
|
||||
|
|
|
|||
|
|
@ -720,7 +720,7 @@ lemma handle_invocation_valid_vspace_objs[wp]:
|
|||
done
|
||||
|
||||
|
||||
crunch valid_vspace_objs[wp]: activate_thread,switch_to_thread,
|
||||
crunch valid_vspace_objs[wp]: activate_thread,switch_to_thread, handle_hypervisor_fault,
|
||||
switch_to_idle_thread, handle_call, handle_recv, handle_reply,
|
||||
handle_send, handle_yield, handle_interrupt "valid_vspace_objs"
|
||||
(simp: crunch_simps wp: crunch_wps alternative_valid select_wp OR_choice_weak_wp select_ext_weak_wp
|
||||
|
|
|
|||
Loading…
Reference in New Issue