arch_split: invariants: split DetSchedAux_AI [VER-602]
This commit is contained in:
Matthew Brecknell
parent
0448444776
commit
3e3baf7b49
|
|
@ -0,0 +1,134 @@
|
|||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
theory ArchDetSchedAux_AI
|
||||
imports "../DetSchedAux_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
named_theorems DetSchedAux_AI_assms
|
||||
|
||||
crunch exst[wp]: init_arch_objects "\<lambda>s. P (exst s)" (wp: crunch_wps)
|
||||
crunch ct[wp]: init_arch_objects "\<lambda>s. P (cur_thread s)" (wp: crunch_wps)
|
||||
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp')
|
||||
crunch valid_etcbs[wp, DetSchedAux_AI_assms]: init_arch_objects valid_etcbs (wp: valid_etcbs_lift)
|
||||
|
||||
lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
|
||||
"\<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
|
||||
apply (simp add: delete_objects_def)
|
||||
apply (wp)
|
||||
apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+
|
||||
done
|
||||
|
||||
lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]:
|
||||
"\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> "
|
||||
apply (cases ui)
|
||||
apply (simp add: mapM_x_def[symmetric])
|
||||
apply wp
|
||||
apply (wp retype_region_etcb_at mapM_x_wp' create_cap_no_pred_tcb_at
|
||||
hoare_convert_imp typ_at_pred_tcb_at_lift )
|
||||
apply simp
|
||||
done
|
||||
|
||||
crunch valid_blocked[wp, DetSchedAux_AI_assms]: init_arch_objects valid_blocked
|
||||
(wp: valid_blocked_lift set_cap_typ_at)
|
||||
|
||||
crunch ct[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (cur_thread s)"
|
||||
(wp: crunch_wps dxo_wp_weak simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym
|
||||
ignore: freeMemory ignore: retype_region_ext)
|
||||
|
||||
crunch ready_queues[wp, DetSchedAux_AI_assms]:
|
||||
invoke_untyped "\<lambda>s :: det_ext state. P (ready_queues s)"
|
||||
(wp: crunch_wps
|
||||
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
|
||||
crunch scheduler_action[wp, DetSchedAux_AI_assms]:
|
||||
invoke_untyped "\<lambda>s :: det_ext state. P (scheduler_action s)"
|
||||
(wp: crunch_wps
|
||||
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
|
||||
crunch cur_domain[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s :: det_ext state. P (cur_domain s)"
|
||||
(wp: crunch_wps
|
||||
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
|
||||
crunch idle_thread[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (idle_thread s)"
|
||||
(wp: crunch_wps dxo_wp_weak
|
||||
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory retype_region_ext)
|
||||
|
||||
lemma perform_asid_control_etcb_at:"\<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace>
|
||||
perform_asid_control_invocation aci
|
||||
\<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
|
||||
apply (simp add: perform_asid_control_invocation_def)
|
||||
apply (rule hoare_pre)
|
||||
apply ( wp | wpc | simp)+
|
||||
apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1]
|
||||
apply (rule hoare_drop_imps)
|
||||
apply (wp retype_region_etcb_at)
|
||||
apply simp
|
||||
done
|
||||
|
||||
crunch ct[wp]: perform_asid_control_invocation "\<lambda>s. P (cur_thread s)"
|
||||
|
||||
crunch idle_thread[wp]: perform_asid_control_invocation "\<lambda>s. P (idle_thread s)"
|
||||
|
||||
crunch valid_etcbs[wp]: perform_asid_control_invocation valid_etcbs (wp: static_imp_wp)
|
||||
|
||||
crunch valid_blocked[wp]: perform_asid_control_invocation valid_blocked (wp: static_imp_wp)
|
||||
|
||||
crunch schedact[wp]: perform_asid_control_invocation "\<lambda>s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
|
||||
|
||||
crunch rqueues[wp]: perform_asid_control_invocation "\<lambda>s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
|
||||
|
||||
crunch cur_domain[wp]: perform_asid_control_invocation "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
|
||||
|
||||
lemma perform_asid_control_invocation_valid_sched:
|
||||
"\<lbrace>ct_active and invs and valid_aci aci and valid_sched and valid_idle\<rbrace>
|
||||
perform_asid_control_invocation aci
|
||||
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (rule_tac I="invs and ct_active and valid_aci aci" in valid_sched_tcb_state_preservation)
|
||||
apply (wp perform_asid_control_invocation_st_tcb_at)
|
||||
apply simp
|
||||
apply (wp perform_asid_control_etcb_at)
|
||||
apply (rule hoare_strengthen_post, rule aci_invs)
|
||||
apply (simp add: invs_def valid_state_def)
|
||||
apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s"])
|
||||
apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_domain s"])
|
||||
apply (rule hoare_lift_Pf[where f="\<lambda>s. idle_thread s"])
|
||||
apply wp
|
||||
apply simp
|
||||
done
|
||||
|
||||
crunch valid_queues[wp]: init_arch_objects valid_queues (wp: valid_queues_lift)
|
||||
|
||||
crunch valid_sched_action[wp]: init_arch_objects valid_sched_action (wp: valid_sched_action_lift)
|
||||
|
||||
crunch valid_sched[wp]: init_arch_objects valid_sched (wp: valid_sched_lift)
|
||||
|
||||
end
|
||||
|
||||
global_interpretation DetSchedAux_AI_det_ext?: DetSchedAux_AI_det_ext
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?)
|
||||
qed
|
||||
|
||||
global_interpretation DetSchedAux_AI?: DetSchedAux_AI
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?)
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -12,6 +12,11 @@ theory DetSchedAux_AI
|
|||
imports DetSchedInvs_AI
|
||||
begin
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_facts
|
||||
invoke_untyped_st_tcb_at
|
||||
end
|
||||
|
||||
crunch_ignore (del:
|
||||
cap_swap_ext cap_move_ext cap_insert_ext empty_slot_ext create_cap_ext tcb_sched_action
|
||||
reschedule_required set_thread_state_ext switch_if_required_to
|
||||
|
|
@ -19,16 +24,11 @@ crunch_ignore (del:
|
|||
|
||||
crunch_ignore (add: do_extended_op)
|
||||
|
||||
|
||||
crunch ekheap[wp]: update_cdt_list "\<lambda>s. P (ekheap s)"
|
||||
crunch rqueues[wp]: update_cdt_list "\<lambda>s. P (ready_queues s)"
|
||||
crunch schedact[wp]: update_cdt_list "\<lambda>s. P (scheduler_action s)"
|
||||
crunch cur_domain[wp]: update_cdt_list "\<lambda>s. P (cur_domain s)"
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
crunch exst[wp]: init_arch_objects "\<lambda>s. P (exst s)" (wp: crunch_wps)
|
||||
end
|
||||
|
||||
crunch ekheap[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (ekheap s)" (wp: crunch_wps)
|
||||
|
||||
crunch rqueues[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (ready_queues s)" (wp: crunch_wps)
|
||||
|
|
@ -37,23 +37,13 @@ crunch schedact[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (sch
|
|||
|
||||
crunch cur_domain[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps)
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
crunch ct[wp]: init_arch_objects "\<lambda>s. P (cur_thread s)" (wp: crunch_wps)
|
||||
end
|
||||
|
||||
lemma create_cap_ct[wp]: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> create_cap a b c d \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>"
|
||||
apply (simp add: create_cap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp dxo_wp_weak | wpc | simp)+
|
||||
done
|
||||
|
||||
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp')
|
||||
|
||||
crunch valid_etcbs[wp]: create_cap,cap_insert,init_arch_objects,set_cap valid_etcbs (wp: valid_etcbs_lift set_cap_typ_at)
|
||||
end
|
||||
crunch valid_etcbs[wp]: create_cap,cap_insert,set_cap valid_etcbs (wp: valid_etcbs_lift set_cap_typ_at)
|
||||
|
||||
lemma valid_etcb_fold_update: "valid_etcbs_2 ekh kh \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<Longrightarrow> valid_etcbs_2
|
||||
(foldr (\<lambda>p ekh. ekh(p := default_ext type cdom))
|
||||
|
|
@ -191,11 +181,31 @@ lemma cap_insert_no_pred_tcb_at: "\<lbrace>\<lambda>s. \<not> pred_tcb_at proj P
|
|||
done
|
||||
|
||||
|
||||
lemma delete_objects_etcb_at[wp]: "\<lbrace>\<lambda>s. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
|
||||
apply (simp add: delete_objects_def)
|
||||
apply (wp)
|
||||
apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+
|
||||
done
|
||||
locale DetSchedAux_AI =
|
||||
fixes state_ext_t :: "'state_ext::state_ext itself"
|
||||
assumes invoke_untyped_ct[wp]:
|
||||
"\<And>P i. \<lbrace>\<lambda>s::'state_ext state. P (cur_thread s)\<rbrace> invoke_untyped i \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
|
||||
assumes invoke_untyped_idle_thread[wp]:
|
||||
"\<And>P i. \<lbrace>\<lambda>s::'state_ext state. P (idle_thread s)\<rbrace> invoke_untyped i \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>"
|
||||
|
||||
locale DetSchedAux_AI_det_ext = DetSchedAux_AI "TYPE(det_ext)" +
|
||||
assumes delete_objects_etcb_at[wp]:
|
||||
"\<And>P t a b. \<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
|
||||
assumes invoke_untyped_etcb_at:
|
||||
"\<And>P t ui.
|
||||
\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace>
|
||||
invoke_untyped ui
|
||||
\<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> "
|
||||
assumes init_arch_objects_valid_etcbs[wp]:
|
||||
"\<And>t r n sz refs. \<lbrace>valid_etcbs\<rbrace> init_arch_objects t r n sz refs \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
|
||||
assumes init_arch_objects_valid_blocked[wp]:
|
||||
"\<And>t r n sz refs. \<lbrace>valid_blocked\<rbrace> init_arch_objects t r n sz refs \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
|
||||
assumes invoke_untyped_cur_domain[wp]:
|
||||
"\<And>P i. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invoke_untyped i \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>"
|
||||
assumes invoke_untyped_ready_queues[wp]:
|
||||
"\<And>P i. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> invoke_untyped i \<lbrace>\<lambda>_ s. P (ready_queues s)\<rbrace>"
|
||||
assumes invoke_untyped_scheduler_action[wp]:
|
||||
"\<And>P i. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invoke_untyped i \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>"
|
||||
|
||||
lemma delete_objects_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> delete_objects a b \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
|
||||
apply (simp add: delete_objects_def)
|
||||
|
|
@ -207,16 +217,8 @@ lemma delete_objects_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> delete_obje
|
|||
apply (simp add: valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def)
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma invoke_untyped_etcb_at: "\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> "
|
||||
apply (cases ui)
|
||||
apply (simp add: mapM_x_def[symmetric])
|
||||
apply wp
|
||||
apply (wp retype_region_etcb_at mapM_x_wp' create_cap_no_pred_tcb_at
|
||||
hoare_convert_imp typ_at_pred_tcb_at_lift )
|
||||
apply simp
|
||||
done
|
||||
end
|
||||
|
||||
context DetSchedAux_AI_det_ext begin
|
||||
|
||||
lemma invoke_untyped_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_.valid_etcbs\<rbrace>"
|
||||
apply (cases ui)
|
||||
|
|
@ -225,11 +227,12 @@ lemma invoke_untyped_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> invoke_unty
|
|||
apply simp
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
crunch valid_blocked[wp]: create_cap,cap_insert,init_arch_objects,set_cap valid_blocked
|
||||
(wp: valid_blocked_lift set_cap_typ_at)
|
||||
end
|
||||
|
||||
|
||||
crunch valid_blocked[wp]: create_cap,cap_insert,set_cap valid_blocked
|
||||
(wp: valid_blocked_lift set_cap_typ_at)
|
||||
|
||||
lemma valid_blocked_fold_update: "valid_blocked_2 queues kh sa ct \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<Longrightarrow> valid_blocked_2
|
||||
queues
|
||||
(foldr (\<lambda>p kh. kh(p \<mapsto> default_object type o_bits))
|
||||
|
|
@ -263,6 +266,8 @@ lemma delete_objects_valid_blocked[wp]: "\<lbrace>valid_blocked\<rbrace> delete_
|
|||
apply (simp add: valid_blocked_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def)
|
||||
done
|
||||
|
||||
context DetSchedAux_AI_det_ext begin
|
||||
|
||||
lemma invoke_untyped_valid_blocked[wp]: "\<lbrace>valid_blocked\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_.valid_blocked\<rbrace>"
|
||||
apply (cases ui)
|
||||
apply (simp add: mapM_x_def[symmetric])
|
||||
|
|
@ -270,6 +275,8 @@ lemma invoke_untyped_valid_blocked[wp]: "\<lbrace>valid_blocked\<rbrace> invoke_
|
|||
apply simp
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
(*Leverages the fact that retype only clears out inactive tcbs under
|
||||
the invariants*)
|
||||
lemma valid_sched_tcb_state_preservation:
|
||||
|
|
@ -365,18 +372,6 @@ lemma valid_sched_tcb_state_preservation:
|
|||
|
||||
lemmas mapM_x_defsym = mapM_x_def[symmetric]
|
||||
|
||||
crunch ct[wp]: invoke_untyped "\<lambda>s. P (cur_thread s)" (wp: crunch_wps dxo_wp_weak simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym ignore: freeMemory ignore: retype_region_ext)
|
||||
|
||||
crunch ready_queues[wp]: invoke_untyped "\<lambda>s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory)
|
||||
|
||||
crunch scheduler_action[wp]: invoke_untyped "\<lambda>s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory)
|
||||
|
||||
crunch cur_domain[wp]: invoke_untyped "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory)
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
crunch idle_thread[wp]: invoke_untyped "\<lambda>s. P (idle_thread s)" (wp: crunch_wps dxo_wp_weak simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory retype_region_ext)
|
||||
end
|
||||
|
||||
lemma valid_idle_etcb_lift:
|
||||
assumes "\<And>P t. \<lbrace>\<lambda>s. etcb_at P t s\<rbrace> f \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
|
||||
shows "\<lbrace>valid_idle_etcb\<rbrace> f \<lbrace>\<lambda>r. valid_idle_etcb\<rbrace>"
|
||||
|
|
@ -385,81 +380,40 @@ lemma valid_idle_etcb_lift:
|
|||
done
|
||||
|
||||
|
||||
context DetSchedAux_AI_det_ext begin
|
||||
|
||||
lemma invoke_untyped_valid_sched:
|
||||
"\<lbrace>invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle \<rbrace>
|
||||
invoke_untyped ui
|
||||
\<lbrace> \<lambda>_ . valid_sched \<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (rule_tac I="invs and valid_untyped_inv ui and ct_active" in valid_sched_tcb_state_preservation)
|
||||
apply (wp invoke_untyped_st_tcb_at)
|
||||
apply simp
|
||||
apply (wp invoke_untyped_etcb_at)
|
||||
apply (wp invoke_untyped_st_tcb_at)
|
||||
apply simp
|
||||
apply (wp invoke_untyped_etcb_at)
|
||||
apply (rule hoare_strengthen_post)
|
||||
apply (wp invoke_untyp_invs, simp add: invs_def valid_state_def)
|
||||
apply (rule_tac f="\<lambda>s. P (scheduler_action s)" in hoare_lift_Pf)
|
||||
apply (rule_tac f="\<lambda>s. x (ready_queues s)" in hoare_lift_Pf)
|
||||
apply wp
|
||||
apply (wp invoke_untyp_invs, simp add: invs_def valid_state_def)
|
||||
apply (rule_tac f="\<lambda>s. P (scheduler_action s)" in hoare_lift_Pf)
|
||||
apply (rule_tac f="\<lambda>s. x (ready_queues s)" in hoare_lift_Pf)
|
||||
apply wp
|
||||
apply simp
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
|
||||
lemma hoare_imp_lift_something: "\<lbrakk>\<lbrace>\<lambda>s. \<not> P s \<rbrace> f \<lbrace>\<lambda>r s. \<not> P s\<rbrace>;\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>_.Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<longrightarrow> Q s\<rbrace> f \<lbrace>\<lambda>r s. P s \<longrightarrow> Q s\<rbrace>"
|
||||
apply (clarsimp simp add: valid_def)
|
||||
apply force
|
||||
done
|
||||
|
||||
context Arch begin global_naming ARM (*FIXME: arch_split*)
|
||||
crunch valid_queues[wp]: create_cap,cap_insert valid_queues
|
||||
(wp: valid_queues_lift)
|
||||
|
||||
lemma perform_asid_control_etcb_at:"\<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace>
|
||||
perform_asid_control_invocation aci
|
||||
\<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
|
||||
apply (simp add: perform_asid_control_invocation_def)
|
||||
apply (rule hoare_pre)
|
||||
apply ( wp | wpc | simp)+
|
||||
apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1]
|
||||
apply (rule hoare_drop_imps)
|
||||
apply (wp retype_region_etcb_at)
|
||||
apply simp
|
||||
done
|
||||
crunch valid_sched_action[wp]: create_cap,cap_insert valid_sched_action
|
||||
(wp: valid_sched_action_lift)
|
||||
|
||||
crunch ct[wp]: perform_asid_control_invocation "\<lambda>s. P (cur_thread s)"
|
||||
|
||||
crunch idle_thread[wp]: perform_asid_control_invocation "\<lambda>s. P (idle_thread s)"
|
||||
|
||||
crunch valid_etcbs[wp]: perform_asid_control_invocation valid_etcbs (wp: static_imp_wp)
|
||||
|
||||
crunch valid_blocked[wp]: perform_asid_control_invocation valid_blocked (wp: static_imp_wp)
|
||||
|
||||
crunch schedact[wp]: perform_asid_control_invocation "\<lambda>s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
|
||||
|
||||
crunch rqueues[wp]: perform_asid_control_invocation "\<lambda>s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
|
||||
|
||||
crunch cur_domain[wp]: perform_asid_control_invocation "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
|
||||
|
||||
lemma perform_asid_control_invocation_valid_sched: "\<lbrace>ct_active and invs and
|
||||
valid_aci aci and valid_sched and valid_idle\<rbrace>
|
||||
perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_sched\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (rule_tac I="invs and ct_active and valid_aci aci" in valid_sched_tcb_state_preservation)
|
||||
apply (wp perform_asid_control_invocation_st_tcb_at)
|
||||
apply simp
|
||||
apply (wp perform_asid_control_etcb_at)
|
||||
apply (rule hoare_strengthen_post, rule aci_invs)
|
||||
apply (simp add: invs_def valid_state_def)
|
||||
apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s"])
|
||||
apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_domain s"])
|
||||
apply (rule hoare_lift_Pf[where f="\<lambda>s. idle_thread s"])
|
||||
apply wp
|
||||
apply simp
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
crunch valid_queues[wp]: create_cap,cap_insert,init_arch_objects valid_queues (wp: valid_queues_lift)
|
||||
|
||||
crunch valid_sched_action[wp]: create_cap,cap_insert,init_arch_objects valid_sched_action (wp: valid_sched_action_lift)
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
crunch valid_sched[wp]: create_cap,cap_insert,init_arch_objects valid_sched (wp: valid_sched_lift)
|
||||
end
|
||||
crunch valid_sched[wp]: create_cap,cap_insert valid_sched
|
||||
(wp: valid_sched_lift)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@
|
|||
*)
|
||||
|
||||
theory DetSchedSchedule_AI
|
||||
imports DetSchedAux_AI
|
||||
imports "$L4V_ARCH/ArchDetSchedAux_AI"
|
||||
begin
|
||||
|
||||
lemma ethread_get_wp[wp]: "\<lbrace>\<lambda>s. etcb_at (\<lambda>t. P (f t) s) ptr s\<rbrace> ethread_get f ptr \<lbrace>P\<rbrace>"
|
||||
|
|
|
|||
Loading…
Reference in New Issue