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

arch_split: AInvs checking?

This commit is contained in:
Daniel Matichuk 2016-04-19 14:27:07 +10:00
parent ee48e33253
commit 3f4c8cb188
12 changed files with 172 additions and 143 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
proof/invariant-abstract/AInvs.thy
View File

@ -15,7 +15,7 @@ The main theorem
theory AInvs
imports PDPTEntries_AI ADT_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
lemma st_tcb_at_nostate_upd:
"\<lbrakk> get_tcb t s = Some y; tcb_state y = tcb_state y' \<rbrakk> \<Longrightarrow>
st_tcb_at P t' (s \<lparr>kheap := kheap s(t \<mapsto> TCB y')\<rparr>) = st_tcb_at P t' s"
@ -118,7 +118,7 @@ lemma some_get_page_info_kmapsD:
kernel_mappings_slots_eq
split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits
Arch_Structs_A.pde.splits Arch_Structs_A.pte.splits)
pde.splits pte.splits)
apply (rule conjI, rule_tac x=ARMLargePage in exI, simp)
apply (simp add: valid_pde_kernel_mappings_def obj_at_def
valid_pt_kernel_mappings_def)
@ -159,20 +159,21 @@ lemma get_pd_of_thread_reachable:
cap.splits arch_cap.splits)
lemma is_aligned_ptrFromPAddrD:
"\<lbrakk>is_aligned (Platform.ptrFromPAddr b) a; a \<le> 24\<rbrakk> \<Longrightarrow> is_aligned b a"
apply (clarsimp simp:Platform.ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
"\<lbrakk>is_aligned (ptrFromPAddr b) a; a \<le> 24\<rbrakk> \<Longrightarrow> is_aligned b a"
apply (clarsimp simp:ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
apply (erule is_aligned_addD2)
apply (rule is_aligned_weaken[where x = 24])
apply (simp add:is_aligned_def)
apply simp
done
lemma some_get_page_info_umapsD:
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
(\<exists>\<rhd> pd_ref) s; p \<notin> kernel_mappings; valid_arch_objs s; pspace_aligned s;
valid_asid_table (arm_asid_table (arch_state s)) s; valid_objs s\<rbrakk>
\<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and>
typ_at (AArch (AIntData sz)) (Platform.ptrFromPAddr b) s)"
typ_at (AArch (AIntData sz)) (ptrFromPAddr b) s)"
apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
kernel_mappings_slots_eq
split: option.splits Structures_A.kernel_object.splits
@ -181,12 +182,12 @@ lemma some_get_page_info_umapsD:
apply (simp add: obj_at_def)
apply (simp add: valid_arch_obj_def)
apply (drule bspec, simp)
apply (simp split: Arch_Structs_A.pde.splits)
apply (simp split: pde.splits)
apply (rename_tac rs pd pt_ref rights w)
apply (subgoal_tac
"((rs, pd_ref) \<rhd>1
(VSRef (ucast (ucast (p >> 20))) (Some APageDirectory) # rs,
Platform.ptrFromPAddr pt_ref)) s")
ptrFromPAddr pt_ref)) s")
prefer 2
apply (rule vs_lookup1I[rotated 2], simp)
apply (simp add: obj_at_def)
@ -199,24 +200,24 @@ lemma some_get_page_info_umapsD:
apply (simp add: get_pt_info_def get_pt_entry_def)
apply (drule_tac x="(ucast ((p >> 12) && mask 8))" in spec)
apply (clarsimp simp: obj_at_def valid_arch_obj_def
split: Arch_Structs_A.pte.splits)
split: pte.splits)
apply (clarsimp simp: pspace_aligned_def)
apply (drule_tac x = "(Platform.ptrFromPAddr b)" in bspec, fastforce)
apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce)
apply (drule is_aligned_ptrFromPAddrD)
apply simp
apply (clarsimp simp:a_type_simps)
apply (clarsimp simp: pspace_aligned_def)
apply (drule_tac x = "(Platform.ptrFromPAddr b)" in bspec, fastforce)
apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce)
apply (drule is_aligned_ptrFromPAddrD)
apply simp
apply (clarsimp simp:a_type_simps)
apply (clarsimp simp: pspace_aligned_def obj_at_def)
apply (drule_tac x = "(Platform.ptrFromPAddr b)" in bspec, fastforce)
apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce)
apply (drule is_aligned_ptrFromPAddrD)
apply simp
apply (clarsimp simp:a_type_simps)
apply (clarsimp simp: pspace_aligned_def obj_at_def)
apply (drule_tac x = "(Platform.ptrFromPAddr b)" in bspec, fastforce)
apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce)
apply (drule is_aligned_ptrFromPAddrD)
apply simp
apply (clarsimp simp:a_type_simps)
@ -248,7 +249,7 @@ lemma ptable_rights_imp_user_frame:
apply (frule is_aligned_add_helper[OF _ and_mask_less',
THEN conjunct2, of _ _ x])
apply (simp only: pbfs_less_wb'[simplified word_bits_def])
apply (clarsimp simp: Platform.ptrFromPAddr_def Platform.ARM.addrFromPPtr_def
apply (clarsimp simp: ptrFromPAddr_def Platform.ARM.addrFromPPtr_def
field_simps)
apply (rule_tac x=sz in exI)
apply (subst add.assoc[symmetric])
@ -275,3 +276,4 @@ lemma do_user_op_invs:
done
end
end

6
proof/invariant-abstract/ARM/ArchADT_AI.thy
View File

@ -77,9 +77,9 @@ lemma VSRef_AASIDPool_in_vs_refs:
apply (simp_all add: asid_low_bits_def)
done
context begin
declare vs_refs_arch_def[simp del]
context
notes vs_refs_arch_def[simp del]
begin
lemma get_pd_of_thread_def2:
"get_pd_of_thread khp astate tcb_ref \<equiv>

8
proof/invariant-abstract/BCorres2_AI.thy
View File

@ -14,6 +14,7 @@ imports
"../../lib/BCorres_UL"
CNodeInv_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
definition all_but_exst where
"all_but_exst P \<equiv> (\<lambda>s. P (kheap s) (cdt s) (is_original_cap s)
@ -92,13 +93,13 @@ lemma dxo_ex: "((),x :: det_ext state) \<in> fst (do_extended_op f s) \<Longrigh
wrap_ext_op_det_ext_ext_def)
apply force
done
end
locale is_extended' =
fixes f :: "'a det_ext_monad"
assumes a: "(\<And>P. \<lbrace>all_but_exst P\<rbrace> f \<lbrace>\<lambda>_. all_but_exst P\<rbrace>)"
begin
interpretation ARM . (*FIXME: arch_split*)
lemmas v = use_valid[OF _ a, OF _ all_but_obvious,simplified all_but_exst_def, THEN bluh]
lemma ex_st: "(a,x :: det_ext state) \<in> fst (f s) \<Longrightarrow>
@ -309,7 +310,7 @@ lemma cap_revoke_s_bcorres:
qed
lemmas cap_revoke_bcorres = use_sbcorres_underlying[OF cap_revoke_s_bcorres]
context begin interpretation ARM . (*FIXME: arch_split*)
crunch (bcorres)bcorres[wp]: invoke_cnode truncate_state (simp: swp_def ignore: clearMemory without_preemption filterM ethread_set recycle_cap_ext)
crunch (bcorres)bcorres[wp]: "Tcb_A.restart",as_user,option_update_thread truncate_state (simp: gets_the_def ignore: clearMemory check_cap_at gets_the getRegister setRegister getRestartPC setNextPC)
@ -673,3 +674,4 @@ lemma schedule_bcorres[wp]: "bcorres (schedule :: (unit,det_ext) s_monad) schedu
*)
end
end

32
proof/invariant-abstract/DetSchedAux_AI.thy
View File

@ -19,12 +19,14 @@ 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 ARM . (*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)
@ -33,9 +35,9 @@ crunch rqueues[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (read
crunch schedact[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps)
crunch cur_domain[wp]: create_cap, cap_insert "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps)
context begin interpretation ARM . (*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)
@ -45,11 +47,11 @@ lemma create_cap_ct[wp]: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> create_
context begin interpretation ARM . (*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
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))
@ -202,7 +204,7 @@ lemma delete_objects_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> delete_obje
apply (wp|wpc)+
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 ARM . (*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])
@ -211,17 +213,17 @@ lemma invoke_untyped_etcb_at: "\<lbrace>(\<lambda>s :: det_ext state. etcb_at P
hoare_convert_imp typ_at_pred_tcb_at_lift )
apply simp
done
end
lemma invoke_untyped_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_.valid_etcbs\<rbrace>"
apply (cases ui)
apply (simp add: mapM_x_def[symmetric])
apply (wp mapM_x_wp')
apply simp
done
context begin interpretation ARM . (*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
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))
@ -364,9 +366,9 @@ crunch ready_queues[wp]: invoke_untyped "\<lambda>s :: det_ext state. P (ready_q
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 ARM . (*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>"
@ -396,7 +398,7 @@ lemma hoare_imp_lift_something: "\<lbrakk>\<lbrace>\<lambda>s. \<not> P s \<rbra
apply (clarsimp simp add: valid_def)
apply force
done
context begin interpretation ARM . (*FIXME: arch_split*)
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>"
@ -440,11 +442,11 @@ perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_sched\<rbrace>"
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 ARM . (*FIXME: arch_split*)
crunch valid_sched[wp]: create_cap,cap_insert,init_arch_objects valid_sched (wp: valid_sched_lift)
end
end

3
proof/invariant-abstract/DetSchedSchedule_AI.thy
View File

@ -11,7 +11,7 @@
theory DetSchedSchedule_AI
imports DetSchedAux_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
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>"
apply (simp add: ethread_get_def)
apply wp
@ -3002,3 +3002,4 @@ lemma call_kernel_valid_sched:
done
end
end

17
proof/invariant-abstract/Deterministic_AI.thy
View File

@ -3920,9 +3920,9 @@ lemma reply_cancel_ipc_valid_list[wp]: "\<lbrace>valid_list\<rbrace> reply_cance
apply (wp select_wp hoare_drop_imps thread_set_mdb | simp)+
done
context begin interpretation ARM . (*FIXME: arch_split*)
crunch valid_list[wp]: cap_swap_for_delete,set_cap,finalise_cap valid_list (wp: crunch_wps simp: unless_def crunch_simps)
end
lemmas rec_del_valid_list[wp] = rec_del_preservation[OF cap_swap_for_delete_valid_list set_cap_valid_list empty_slot_valid_list finalise_cap_valid_list]
@ -3978,9 +3978,9 @@ interpretation recycle_cap_ext_extended: is_extended "recycle_cap_ext a"
apply (unfold_locales)
apply wp
done
context begin interpretation ARM . (*FIXME: arch_split*)
crunch valid_list[wp]: cap_recycle valid_list (wp: crunch_wps preemption_point_inv' simp: crunch_simps filterM_mapM unless_def ignore: without_preemption filterM recycle_cap_ext)
end
lemma invoke_cnode_valid_list[wp]: "\<lbrace>valid_list\<rbrace>
invoke_cnode ci
\<lbrace>\<lambda>_.valid_list\<rbrace>"
@ -4065,7 +4065,7 @@ interpretation retype_region_ext_extended: is_extended "retype_region_ext a b"
apply (unfold_locales)
apply wp
done
context begin interpretation ARM . (*FIXME: arch_split*)
crunch valid_list[wp]: invoke_untyped valid_list (wp: crunch_wps simp: mapM_x_def_bak)
crunch valid_list[wp]: invoke_irq_control valid_list
@ -4084,14 +4084,14 @@ lemma perform_page_invocation_valid_list[wp]:
apply (cases a,simp_all)
apply (wp mapM_x_wp' mapM_wp' crunch_wps | intro impI conjI allI | wpc | simp add: set_message_info_def set_mrs_def split: cap.splits arch_cap.splits option.splits sum.splits)+
done
end
crunch valid_list[wp]: attempt_switch_to "valid_list"
interpretation attempt_switch_to_extended: is_extended "attempt_switch_to a"
apply (simp add: attempt_switch_to_def)
apply (unfold_locales)
done
context begin interpretation ARM . (*FIXME: arch_split*)
crunch valid_list[wp]: perform_invocation valid_list (wp: crunch_wps simp: crunch_simps ignore: without_preemption)
crunch valid_list[wp]: handle_invocation valid_list (wp: crunch_wps syscall_valid simp: crunch_simps ignore: without_preemption)
@ -4110,7 +4110,7 @@ crunch all_but_exst[wp]: timer_tick "all_but_exst P" (simp: ethread_get_def crun
crunch (empty_fail)empty_fail[wp]: timer_tick
(simp: thread_state.splits)
end
interpretation timer_tick_extended: is_extended "timer_tick"
apply (unfold_locales)
apply wp
@ -5395,3 +5395,4 @@ lemma next_sib_def2:
done
end

38
proof/invariant-abstract/EmptyFail_AI.thy
View File

@ -9,9 +9,9 @@
*)
theory EmptyFail_AI
imports Tcb_AI
imports Tcb_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
lemmas [wp] = empty_fail_bind empty_fail_bindE empty_fail_get empty_fail_modify
empty_fail_whenEs empty_fail_when empty_fail_gets empty_fail_assertE
empty_fail_error_bits empty_fail_mapM_x empty_fail_mapM empty_fail_sequence_x
@ -133,17 +133,31 @@ lemma without_preemption_empty_fail[wp]:
lemma put_empty_fail[wp]:
"empty_fail (put f)"
by (simp add: put_def empty_fail_def)
end
crunch_ignore (empty_fail)
(add: bind bindE lift liftE liftM "when" whenE unless unlessE return fail assert_opt
mapM mapM_x sequence_x catch handleE invalidateTLB_ASID_impl
invalidateTLB_VAASID_impl cleanByVA_impl cleanByVA_PoU_impl invalidateByVA_impl
invalidateByVA_I_impl invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl
mapM mapM_x sequence_x catch handleE do_extended_op
cap_insert_ext empty_slot_ext create_cap_ext cap_swap_ext cap_move_ext
reschedule_required switch_if_required_to attempt_switch_to set_thread_state_ext
OR_choice OR_choiceE set_priority timer_tick)
context ARM begin
crunch_ignore (empty_fail)
(add: invalidateTLB_ASID_impl invalidateTLB_VAASID_impl cleanByVA_impl
cleanByVA_PoU_impl invalidateByVA_impl invalidateByVA_I_impl
invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl
clean_D_PoU_impl cleanInvalidate_D_PoC_impl cleanInvalidateL2Range_impl
invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl writeContextID_impl
isb_impl dsb_impl dmb_impl setHardwareASID_impl writeTTBR0_impl do_extended_op
cacheRangeOp)
invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl
writeContextID_impl isb_impl dsb_impl dmb_impl setHardwareASID_impl
writeTTBR0_impl cacheRangeOp)
end
context begin interpretation ARM . (*FIXME: arch_split*)
crunch (empty_fail) empty_fail[wp]: set_object, gets_the, get_register, get_cap
(simp: split_def kernel_object.splits)
@ -245,10 +259,7 @@ lemma get_extra_cptrs_empty_fail[wp]:
apply (simp | wp)+
done
crunch_ignore (empty_fail)
(add: cap_insert_ext empty_slot_ext create_cap_ext cap_swap_ext cap_move_ext
reschedule_required switch_if_required_to attempt_switch_to set_thread_state_ext
OR_choice OR_choiceE set_priority timer_tick)
crunch (empty_fail) empty_fail[wp]: storeWord, set_register, lookup_slot_for_cnode_op,
getRestartPC, decode_untyped_invocation, get_mrs, range_check,
@ -478,3 +489,4 @@ lemma call_kernel_empty_fail': "empty_fail ((call_kernel a) :: (unit,unit) s_mon
done
end
end

11
proof/invariant-abstract/Interrupt_AI.thy
View File

@ -15,7 +15,7 @@ Refinement for interrupt controller operations
theory Interrupt_AI
imports Ipc_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
definition
interrupt_derived :: "cap \<Rightarrow> cap \<Rightarrow> bool"
where
@ -172,15 +172,15 @@ lemma real_cte_emptyable_strg:
"real_cte_at p s \<longrightarrow> emptyable p s"
by (clarsimp simp: emptyable_def obj_at_def is_tcb is_cap_table)
context begin interpretation ARM . (*FIXME: arch_split*)
lemma is_derived_use_interrupt:
"(is_ntfn_cap cap \<and> interrupt_derived cap cap') \<longrightarrow> (is_derived m p cap cap')"
apply (clarsimp simp: is_cap_simps)
apply (clarsimp simp: interrupt_derived_def is_derived_def)
apply (clarsimp simp: cap_master_cap_def split: cap.split_asm)
apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def)
done
apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def is_derived_arch_def)
done (* FIXME: arch_split *)
end
lemma cap_delete_one_cte_cap_to[wp]:
"\<lbrace>ex_cte_cap_wp_to P ptr\<rbrace> cap_delete_one ptr' \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P ptr\<rbrace>"
@ -383,3 +383,4 @@ lemma handle_interrupt_invs[wp]:
done
end
end

3
proof/invariant-abstract/KernelInit_AI.thy
View File

@ -14,7 +14,7 @@
theory KernelInit_AI
imports ADT_AI Tcb_AI Arch_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
text {*
Showing that there is a state that satisfies the abstract invariants.
*}
@ -373,6 +373,7 @@ lemma invs_A:
valid_refs_def[unfolded cte_wp_at_caps_of_state])
apply word_bitwise
done
end
axiomatization where
akernel_init_invs: "\<forall>((tc,s),m,e) \<in> Init_A. invs s \<and> ct_running s"

164
proof/invariant-abstract/PDPTEntries_AI.thy
View File

@ -11,38 +11,43 @@
theory PDPTEntries_AI
imports Syscall_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
lemma a_type_pdD:
"a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)"
by (clarsimp)
primrec
pde_range_sz :: "Arch_Structs_A.pde \<Rightarrow> nat"
pde_range_sz :: "pde \<Rightarrow> nat"
where
"pde_range_sz (Arch_Structs_A.InvalidPDE) = 0"
| "pde_range_sz (Arch_Structs_A.SectionPDE ptr x y z) = 0"
| "pde_range_sz (Arch_Structs_A.SuperSectionPDE ptr x z) = 4"
| "pde_range_sz (Arch_Structs_A.PageTablePDE ptr x z) = 0"
"pde_range_sz (InvalidPDE) = 0"
| "pde_range_sz (SectionPDE ptr x y z) = 0"
| "pde_range_sz (SuperSectionPDE ptr x z) = 4"
| "pde_range_sz (PageTablePDE ptr x z) = 0"
primrec
pte_range_sz :: "Arch_Structs_A.pte \<Rightarrow> nat"
pte_range_sz :: "pte \<Rightarrow> nat"
where
"pte_range_sz (Arch_Structs_A.InvalidPTE) = 0"
| "pte_range_sz (Arch_Structs_A.LargePagePTE ptr x y) = 4"
| "pte_range_sz (Arch_Structs_A.SmallPagePTE ptr x y) = 0"
"pte_range_sz (InvalidPTE) = 0"
| "pte_range_sz (LargePagePTE ptr x y) = 4"
| "pte_range_sz (SmallPagePTE ptr x y) = 0"
primrec
pde_range :: "Arch_Structs_A.pde \<Rightarrow> 12 word \<Rightarrow> 12 word set"
pde_range :: "pde \<Rightarrow> 12 word \<Rightarrow> 12 word set"
where
"pde_range (Arch_Structs_A.InvalidPDE) p = {}"
| "pde_range (Arch_Structs_A.SectionPDE ptr x y z) p = {p}"
| "pde_range (Arch_Structs_A.SuperSectionPDE ptr x z) p =
"pde_range (InvalidPDE) p = {}"
| "pde_range (SectionPDE ptr x y z) p = {p}"
| "pde_range (SuperSectionPDE ptr x z) p =
(if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})"
| "pde_range (Arch_Structs_A.PageTablePDE ptr x z) p = {p}"
| "pde_range (PageTablePDE ptr x z) p = {p}"
primrec
pte_range :: "Arch_Structs_A.pte \<Rightarrow> word8 \<Rightarrow> word8 set"
pte_range :: "pte \<Rightarrow> word8 \<Rightarrow> word8 set"
where
"pte_range (Arch_Structs_A.InvalidPTE) p = {}"
| "pte_range (Arch_Structs_A.LargePagePTE ptr x y) p =
"pte_range (InvalidPTE) p = {}"
| "pte_range (LargePagePTE ptr x y) p =
(if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})"
| "pte_range (Arch_Structs_A.SmallPagePTE ptr x y) p = {p}"
| "pte_range (SmallPagePTE ptr x y) p = {p}"
definition valid_entries :: " ('b \<Rightarrow> ('a::len) word \<Rightarrow> 'c set) \<Rightarrow> (('a::len) word \<Rightarrow> 'b) \<Rightarrow> bool"
where "valid_entries \<equiv> \<lambda>range fun. \<forall>x y. x \<noteq> y \<longrightarrow> range (fun x) x \<inter> range (fun y) y = {}"
@ -223,11 +228,11 @@ lemma mapM_x_store_pte_updates:
lemma valid_pt_entries_invalid[simp]:
"valid_pt_entries (\<lambda>x. Arch_Structs_A.pte.InvalidPTE)"
"valid_pt_entries (\<lambda>x. pte.InvalidPTE)"
by (simp add:valid_entries_def)
lemma valid_pd_entries_invalid[simp]:
"valid_pd_entries (\<lambda>x. Arch_Structs_A.pde.InvalidPDE)"
"valid_pd_entries (\<lambda>x. pde.InvalidPDE)"
by (simp add:valid_entries_def)
lemma entries_align_pte_update:
@ -257,7 +262,7 @@ lemma valid_pdpt_objs_ptD:
lemma mapM_x_store_invalid_pte_valid_pdpt:
"\<lbrace>valid_pdpt_objs and K (is_aligned p 6) \<rbrace>
mapM_x (\<lambda>x. store_pte (x + p) Arch_Structs_A.InvalidPTE) [0, 4 .e. 0x3C]
mapM_x (\<lambda>x. store_pte (x + p) InvalidPTE) [0, 4 .e. 0x3C]
\<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule hoare_pre, rule_tac p="p && ~~ mask pt_bits" in mapM_x_store_pte_updates)
@ -320,7 +325,7 @@ lemma mapM_x_store_pde_updates:
lemma mapM_x_store_pde_valid_pdpt_objs:
"\<lbrace>valid_pdpt_objs and K (is_aligned p 6)\<rbrace>
mapM_x (\<lambda>x. store_pde (x + p) Arch_Structs_A.InvalidPDE) [0, 4 .e. 0x3C]
mapM_x (\<lambda>x. store_pde (x + p) InvalidPDE) [0, 4 .e. 0x3C]
\<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule hoare_pre, rule_tac p="p && ~~ mask pd_bits" in mapM_x_store_pde_updates)
@ -361,7 +366,7 @@ lemma valid_entriesD:
lemma store_invalid_pde_valid_pdpt:
"\<lbrace>valid_pdpt_objs and
(\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
\<longrightarrow> pde = Arch_Structs_A.InvalidPDE)\<rbrace>
\<longrightarrow> pde = InvalidPDE)\<rbrace>
store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (simp add: store_pde_def set_pd_def, wp get_object_wp)
apply (clarsimp simp: obj_at_def)
@ -403,7 +408,7 @@ lemma store_pde_non_master_valid_pdpt:
lemma store_invalid_pte_valid_pdpt:
"\<lbrace>valid_pdpt_objs and
(\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s
\<longrightarrow> pte = Arch_Structs_A.InvalidPTE)\<rbrace>
\<longrightarrow> pte = InvalidPTE)\<rbrace>
store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (simp add: store_pte_def set_pt_def, wp get_object_wp)
apply (clarsimp simp: obj_at_def)
@ -652,7 +657,7 @@ lemma shiftr_eq_neg_mask_eq:
lemma mapM_x_store_pte_valid_pdpt2:
"\<lbrace>valid_pdpt_objs and K (is_aligned ptr pt_bits)\<rbrace>
mapM_x (\<lambda>x. store_pte x Arch_Structs_A.pte.InvalidPTE) [ptr, ptr + 4 .e. ptr + 2 ^ pt_bits - 1]
mapM_x (\<lambda>x. store_pte x pte.InvalidPTE) [ptr, ptr + 4 .e. ptr + 2 ^ pt_bits - 1]
\<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule mapM_x_wp')
@ -673,7 +678,7 @@ lemma mapM_x_store_pte_valid_pdpt2:
lemma mapM_x_store_pde_valid_pdpt2:
"\<lbrace>valid_pdpt_objs and K (is_aligned pd pd_bits)\<rbrace>
mapM_x (\<lambda>x. store_pde ((x << 2) + pd) Arch_Structs_A.pde.InvalidPDE)
mapM_x (\<lambda>x. store_pde ((x << 2) + pd) pde.InvalidPDE)
[0.e.(kernel_base >> 20) - 1]
\<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)
@ -694,12 +699,12 @@ lemma mapM_x_store_pde_valid_pdpt2:
done
lemma non_invalid_in_pde_range:
"pde \<noteq> Arch_Structs_A.pde.InvalidPDE
"pde \<noteq> pde.InvalidPDE
\<Longrightarrow> x \<in> pde_range pde x"
by (case_tac pde,simp_all)
lemma non_invalid_in_pte_range:
"pte \<noteq> Arch_Structs_A.pte.InvalidPTE
"pte \<noteq> pte.InvalidPTE
\<Longrightarrow> x \<in> pte_range pte x"
by (case_tac pte,simp_all)
@ -859,8 +864,8 @@ lemma invoke_untyped_valid_pdpt[wp]:
have cte_at: "cte_wp_at (op = (cap.UntypedCap (ptr && ~~ mask sz) sz idx)) (cref,oref) s" (is "?cte_cond s")
using cte_wp_at by (simp add:cte_wp_at_caps_of_state)
assume desc_range: "ptr = ptr && ~~ mask sz \<longrightarrow> descendants_range_in {ptr..ptr + 2 ^ sz - 1} (cref,oref) s"
assume misc : "distinct slots" "tp = Invariants_AI.CapTableObject \<longrightarrow> 0 < (us::nat)"
" tp = Invariants_AI.Untyped \<longrightarrow> 4 \<le> (us::nat)"
assume misc : "distinct slots" "tp = CapTableObject \<longrightarrow> 0 < (us::nat)"
" tp = Untyped \<longrightarrow> 4 \<le> (us::nat)"
" idx \<le> unat (ptr && mask sz) \<or> ptr = ptr && ~~ mask sz"
" invs s" "tp \<noteq> ArchObject ASIDPoolObj"
" \<forall>slot\<in>set slots. cte_wp_at (op = cap.NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s"
@ -1155,13 +1160,13 @@ crunch valid_pdpt_objs[wp]: perform_asid_pool_invocation,
abbreviation (input)
"safe_pt_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt)
\<and> (\<forall>x\<in>set (tl slots). pt (ucast (x && mask pt_bits >> 2))
= Arch_Structs_A.pte.InvalidPTE))
= pte.InvalidPTE))
(hd slots && ~~ mask pt_bits) s"
abbreviation (input)
"safe_pd_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd)
\<and> (\<forall>x\<in>set (tl slots). pd (ucast (x && mask pd_bits >> 2))
= Arch_Structs_A.pde.InvalidPDE))
= pde.InvalidPDE))
(hd slots && ~~ mask pd_bits) s"
definition
@ -1180,8 +1185,8 @@ definition
(hd slots && ~~ mask pd_bits)
and K (pde_range_sz pde = 0)
else (\<lambda>s. (\<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0, 4 .e. 0x3C])))
and K (case entries of Inl (pte,slots) \<Rightarrow> pte \<noteq> Arch_Structs_A.InvalidPTE
| Inr (pde,slots) \<Rightarrow> pde \<noteq> Arch_Structs_A.InvalidPDE)"
and K (case entries of Inl (pte,slots) \<Rightarrow> pte \<noteq> InvalidPTE
| Inr (pde,slots) \<Rightarrow> pde \<noteq> InvalidPDE)"
definition
"page_inv_entries_safe entries \<equiv>
@ -1206,15 +1211,15 @@ definition
definition
"page_inv_duplicates_valid iv \<equiv> case iv of
ArchInvocation_A.PageMap asid cap ct_slot entries \<Rightarrow>
PageMap asid cap ct_slot entries \<Rightarrow>
page_inv_entries_safe entries
| ArchInvocation_A.page_invocation.PageRemap asid entries \<Rightarrow>
| PageRemap asid entries \<Rightarrow>
page_inv_entries_safe entries
| _ \<Rightarrow> \<top>"
lemma pte_range_interD:
"pte_range pte p \<inter> pte_range pte' p' \<noteq> {}
\<Longrightarrow> pte \<noteq> Arch_Structs_A.InvalidPTE \<and> pte' \<noteq> Arch_Structs_A.InvalidPTE
\<Longrightarrow> pte \<noteq> InvalidPTE \<and> pte' \<noteq> InvalidPTE
\<and> p && ~~ mask 4 = p' && ~~ mask 4"
apply (drule WordLemmaBucket.int_not_emptyD)
apply (case_tac pte,simp_all split:if_splits)
@ -1226,7 +1231,7 @@ lemma pte_range_interD:
lemma pde_range_interD:
"pde_range pde p \<inter> pde_range pde' p' \<noteq> {}
\<Longrightarrow> pde \<noteq> Arch_Structs_A.InvalidPDE \<and> pde' \<noteq> Arch_Structs_A.InvalidPDE
\<Longrightarrow> pde \<noteq> InvalidPDE \<and> pde' \<noteq> InvalidPDE
\<and> p && ~~ mask 4 = p' && ~~ mask 4"
apply (drule WordLemmaBucket.int_not_emptyD)
apply (case_tac pde,simp_all split:if_splits)
@ -1307,7 +1312,7 @@ lemma store_pte_valid_pdpt:
apply (clarsimp simp:store_pte_def set_pt_def)
apply (wp get_pt_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:Arch_Structs_A.pte.splits arch_kernel_obj.splits)
split:pte.splits arch_kernel_obj.splits)
apply (rule conjI)
apply (drule(1) valid_pdpt_objs_ptD)
apply (rule valid_entries_overwrite_0)
@ -1324,7 +1329,7 @@ lemma store_pte_valid_pdpt:
apply (clarsimp simp:store_pte_def set_pt_def)
apply (wp get_pt_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:Arch_Structs_A.pte.splits arch_kernel_obj.splits)
split:pte.splits arch_kernel_obj.splits)
apply (drule(1) valid_pdpt_objs_ptD)
apply (rule conjI)
apply (rule valid_entries_overwrite_0)
@ -1392,7 +1397,7 @@ lemma store_pde_valid_pdpt:
apply (clarsimp simp:store_pde_def set_pd_def)
apply (wp get_pd_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:Arch_Structs_A.pde.splits arch_kernel_obj.splits)
split:pde.splits arch_kernel_obj.splits)
apply (drule(1) valid_pdpt_objs_pdD)
apply (rule conjI)
apply (rule valid_entries_overwrite_0)
@ -1409,7 +1414,7 @@ lemma store_pde_valid_pdpt:
apply (clarsimp simp:store_pde_def set_pd_def)
apply (wp get_pd_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:Arch_Structs_A.pde.splits arch_kernel_obj.splits)
split:pde.splits arch_kernel_obj.splits)
apply (drule(1) valid_pdpt_objs_pdD)
apply (rule conjI)
apply (rule valid_entries_overwrite_0)
@ -1498,22 +1503,22 @@ lemma perform_page_valid_pdpt[wp]:
apply (wp store_pte_valid_pdpt store_pde_valid_pdpt get_master_pte_wp get_master_pde_wp
store_pte_non_master_valid_pdpt store_pde_non_master_valid_pdpt
mapM_x_wp'[OF store_invalid_pte_valid_pdpt
[where pte=Arch_Structs_A.pte.InvalidPTE, simplified]]
[where pte=pte.InvalidPTE, simplified]]
mapM_x_wp'[OF store_invalid_pde_valid_pdpt
[where pde=Arch_Structs_A.pde.InvalidPDE, simplified]]
[where pde=pde.InvalidPDE, simplified]]
set_cap_page_inv_entries_safe
hoare_vcg_imp_lift[OF set_cap_arch_obj_neg] hoare_vcg_all_lift
| clarsimp simp: valid_page_inv_def cte_wp_at_weakenE[OF _ TrueI] obj_at_def
pte_range_sz_def pde_range_sz_def swp_def valid_page_inv_def
valid_slots_def page_inv_entries_safe_def pte_check_if_mapped_def
pde_check_if_mapped_def
split: Arch_Structs_A.pte.splits Arch_Structs_A.pde.splits
split: pte.splits pde.splits
| wp_once hoare_drop_imps)+
done
definition
"pti_duplicates_valid iv \<equiv>
case iv of ArchInvocation_A.PageTableMap cap ct_slot pde pd_slot
case iv of PageTableMap cap ct_slot pde pd_slot
\<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd)
\<and> pd (ucast (pd_slot && mask pd_bits >> 2) && ~~ mask 4)
= pde \<and> pde_range_sz pde = 0)
@ -1533,7 +1538,7 @@ lemma perform_page_table_valid_pdpt[wp]:
"\<lbrace>valid_pdpt_objs and valid_pti pinv and pti_duplicates_valid pinv\<rbrace>
perform_page_table_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (simp add: perform_page_table_invocation_def split_def
cong: ArchInvocation_A.page_table_invocation.case_cong
cong: page_table_invocation.case_cong
option.case_cong cap.case_cong arch_cap.case_cong)
apply (rule hoare_pre)
apply (wp store_pde_non_master_valid_pdpt hoare_vcg_ex_lift
@ -1703,19 +1708,19 @@ lemma mask_out_same_pd:
done
lemma ensure_safe_mapping_ensures[wp]:
"\<lbrace>valid_pdpt_objs and (case entries of (Inl (Arch_Structs_A.SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (Arch_Structs_A.SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (Arch_Structs_A.LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (Arch_Structs_A.SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
"\<lbrace>valid_pdpt_objs and (case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
| _ \<Rightarrow> page_inv_entries_pre entries)\<rbrace>
ensure_safe_mapping entries
\<lbrace>\<lambda>rv. page_inv_entries_safe entries\<rbrace>,-"
proof -
have [simp]:
"\<And>s a. page_inv_entries_pre (Inl (Arch_Structs_A.pte.InvalidPTE, a)) s \<Longrightarrow>
page_inv_entries_safe (Inl (Arch_Structs_A.pte.InvalidPTE, a)) s"
"\<And>s a. page_inv_entries_pre (Inl (pte.InvalidPTE, a)) s \<Longrightarrow>
page_inv_entries_safe (Inl (pte.InvalidPTE, a)) s"
apply (clarsimp simp:page_inv_entries_pre_def page_inv_entries_safe_def
split:if_splits)
done
@ -1729,13 +1734,13 @@ lemma ensure_safe_mapping_ensures[wp]:
"\<And>a m n. a && ~~ mask m && mask n = a && mask n && ~~ mask m"
by (simp add:word_bw_comms word_bw_lcs)
have align_entry_ptD:
"\<And>pt m x xb xc. \<lbrakk>pt m = Arch_Structs_A.pte.LargePagePTE x xb xc; entries_align pte_range_sz pt\<rbrakk>
"\<And>pt m x xb xc. \<lbrakk>pt m = pte.LargePagePTE x xb xc; entries_align pte_range_sz pt\<rbrakk>
\<Longrightarrow> is_aligned m 4"
apply (simp add:entries_align_def)
apply (drule_tac x = m in spec,simp)
done
have align_entry_pdD:
"\<And>pd m x xb xc. \<lbrakk>pd m = Arch_Structs_A.pde.SuperSectionPDE x xb xc; entries_align pde_range_sz pd\<rbrakk>
"\<And>pd m x xb xc. \<lbrakk>pd m = pde.SuperSectionPDE x xb xc; entries_align pde_range_sz pd\<rbrakk>
\<Longrightarrow> is_aligned m 4"
apply (simp add:entries_align_def)
apply (drule_tac x = m in spec,simp)
@ -1817,16 +1822,16 @@ lemma ensure_safe_mapping_ensures[wp]:
done
have invalid_pteI:
"\<And>a pt x y z. \<lbrakk>valid_pt_entries pt; (a && ~~ mask 4) \<noteq> a;
pt (a && ~~ mask 4) = Arch_Structs_A.pte.LargePagePTE x y z \<rbrakk>
\<Longrightarrow> pt a = Arch_Structs_A.pte.InvalidPTE"
pt (a && ~~ mask 4) = pte.LargePagePTE x y z \<rbrakk>
\<Longrightarrow> pt a = pte.InvalidPTE"
apply (drule(1) valid_entriesD[rotated])
apply (case_tac "pt a"; simp add:mask_lower_twice is_aligned_neg_mask split:if_splits)
apply fastforce
done
have invalid_pdeI:
"\<And>a pd x y z. \<lbrakk>valid_pd_entries pd; (a && ~~ mask 4) \<noteq> a;
pd (a && ~~ mask 4) = Arch_Structs_A.pde.SuperSectionPDE x y z \<rbrakk>
\<Longrightarrow> pd a = Arch_Structs_A.pde.InvalidPDE"
pd (a && ~~ mask 4) = pde.SuperSectionPDE x y z \<rbrakk>
\<Longrightarrow> pd a = pde.InvalidPDE"
apply (drule(1) valid_entriesD[rotated])
apply (case_tac "pd a",
simp_all add:mask_lower_twice is_aligned_neg_mask
@ -1856,7 +1861,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply wp
apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set slots. obj_at
(\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and>
pt (ucast (x && mask pt_bits >> 2)) = Arch_Structs_A.pte.InvalidPTE)
pt (ucast (x && mask pt_bits >> 2)) = pte.InvalidPTE)
(hd (slot # slots) && ~~ mask pt_bits) s" in hoare_post_imp_R)
apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] )
apply (wp get_master_pte_wp| wpc | simp)+
@ -1871,7 +1876,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (frule_tac x = z in mask_out_same_pt)
apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
apply (clarsimp simp:field_simps obj_at_def
split:Arch_Structs_A.pte.splits)
split:pte.splits)
apply (intro conjI impI)
apply (clarsimp)
apply (drule(1) valid_pdpt_objs_ptD)
@ -1896,7 +1901,7 @@ lemma ensure_safe_mapping_ensures[wp]:
| wp | intro conjI impI)+
apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
apply (wp get_master_pte_wp |wpc | simp)+
apply (clarsimp simp:obj_at_def split:Arch_Structs_A.pte.splits)
apply (clarsimp simp:obj_at_def split:pte.splits)
apply (clarsimp simp:page_inv_entries_safe_def split:list.splits)
apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
apply (case_tac b,case_tac a)
@ -1907,7 +1912,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
apply (wp get_master_pde_wp | wpc | simp)+
apply (clarsimp simp:obj_at_def page_inv_entries_safe_def
split:Arch_Structs_A.pde.splits)
split:pde.splits)
apply (simp split:list.splits if_splits
add:page_inv_entries_pre_def Let_def page_inv_entries_safe_def)
apply (elim conjE exE)
@ -1916,7 +1921,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply wp
apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set x22. obj_at
(\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and>
pd (ucast (x && mask pd_bits >> 2)) = Arch_Structs_A.pde.InvalidPDE)
pd (ucast (x && mask pd_bits >> 2)) = pde.InvalidPDE)
(hd (x21 # x22) && ~~ mask pd_bits) s" in hoare_post_imp_R)
apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] )
apply (wp get_master_pde_wp| wpc | simp)+
@ -1931,7 +1936,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (frule_tac x = z in mask_out_same_pd)
apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
apply (clarsimp simp:field_simps obj_at_def
split:Arch_Structs_A.pde.splits)
split:pde.splits)
apply (drule(1) valid_pdpt_objs_pdD)
apply (intro conjI impI)
apply clarsimp
@ -1962,12 +1967,12 @@ lemma create_mapping_entries_safe[wp]:
and valid_arch_objs and pspace_aligned and
(\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))\<rbrace>
create_mapping_entries ptr vptr sz rights attrib pd
\<lbrace>\<lambda>entries. case entries of (Inl (Arch_Structs_A.SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (Arch_Structs_A.SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (Arch_Structs_A.LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
\<lbrace>\<lambda>entries. case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
| (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
| _ \<Rightarrow> page_inv_entries_pre entries\<rbrace>,-"
apply (cases sz, simp_all)
defer 2
@ -2008,12 +2013,12 @@ lemma create_mapping_entries_safe[wp]:
apply (clarsimp simp:not_less[symmetric])
apply (subgoal_tac
"(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2))
= Arch_Structs_A.pde.PageTablePDE x xa xb)
\<longrightarrow> is_aligned (Platform.ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6")
= pde.PageTablePDE x xa xb)
\<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6")
apply clarsimp
apply (subgoal_tac "
Platform.ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) \<le>
Platform.ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C")
ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) \<le>
ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C")
apply (clarsimp simp:not_less[symmetric])
apply (erule is_aligned_no_wrap')
apply simp
@ -2151,8 +2156,8 @@ lemma set_thread_state_duplicates_valid[wp]:
Let_def
dest!: get_tcb_SomeD
split: Invocations_A.invocation.split arch_invocation.split_asm
ArchInvocation_A.page_table_invocation.split
ArchInvocation_A.page_invocation.split sum.split
page_table_invocation.split
page_invocation.split sum.split
)
apply (auto simp add: obj_at_def page_inv_entries_safe_def)
done
@ -2195,3 +2200,4 @@ lemma call_kernel_valid_pdpt[wp]:
done
end
end

4
proof/invariant-abstract/Syscall_AI.thy
View File

@ -19,7 +19,7 @@ imports
Arch_AI
Interrupt_AI
begin
context begin interpretation ARM . (*FIXME: arch_split*)
lemma schedule_invs[wp]: "\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: Schedule_A.schedule_def)
@ -1258,5 +1258,5 @@ lemma he_invs[wp]:
fastforce simp: tcb_at_invs ct_in_state_def valid_fault_def
elim!: st_tcb_ex_cap)+
done
end
end

1
proof/invariant-abstract/Tcb_AI.thy
View File

@ -1594,4 +1594,5 @@ lemma unbind_notification_sym_refs[wp]:
intro!: ntfn_q_refs_no_NTFNBound)
done
end