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

arch_split: DRefine now builds

This commit is contained in:
Daniel Matichuk 2016-01-25 18:42:27 +11:00
parent 7aaa8ed774
commit a1f23e5b28
12 changed files with 215 additions and 269 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
proof/drefine/Arch_DR.thy
View File

@ -25,7 +25,7 @@ definition
definition
"transform_page_table_inv invok \<equiv> case invok of
ArchInvocation_A.PageTableMap cap slot pde slot' \<Rightarrow>
if (\<exists>oref attribs. pde = ARM_Structs_A.PageTablePDE (addrFromPPtr oref) attribs 0
if (\<exists>oref attribs. pde = Arch_Structs_A.PageTablePDE (addrFromPPtr oref) attribs 0
\<and> is_pt_cap cap \<and> oref \<in> obj_refs cap)
then Some (cdl_page_table_invocation.PageTableMap (transform_cap cap)
(make_arch_duplicate (transform_cap cap))
@ -156,7 +156,7 @@ lemma dcorres_lookup_pt_slot:
lookup_pt_slot_def liftE_bindE dcorres_lookup_pd_slot)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ dcorres_get_pde])
apply (rule_tac F = "case rv' of ARM_Structs_A.pde.PageTablePDE ptab x xa \<Rightarrow>
apply (rule_tac F = "case rv' of Arch_Structs_A.pde.PageTablePDE ptab x xa \<Rightarrow>
is_aligned (Platform.ptrFromPAddr ptab) 10 | _ \<Rightarrow> True"
in corres_gen_asm2)
apply (case_tac rv')
@ -176,7 +176,7 @@ lemma dcorres_lookup_pt_slot:
apply (rule hoare_strengthen_post[where Q = "\<lambda>r. valid_pde r and pspace_aligned"] )
apply (wp get_pde_valid)
apply (clarsimp simp:valid_pde_def dest!:pt_aligned
split:ARM_Structs_A.pde.splits)
split:Arch_Structs_A.pde.splits)
apply simp
apply auto
done
@ -195,7 +195,7 @@ lemma lookup_pt_slot_aligned_6':
apply wp
apply simp+
apply (clarsimp simp:valid_pde_def dest!:pt_aligned
split:ARM_Structs_A.pde.splits)
split:Arch_Structs_A.pde.splits)
apply (erule aligned_add_aligned)
apply (rule is_aligned_shiftl)
apply (rule is_aligned_andI1)
@ -223,7 +223,7 @@ lemma create_mapping_entries_dcorres:
proof -
have aligned_4_hd:
"\<And>r. is_aligned r 6 \<Longrightarrow> hd [r , r + 4 .e. r + 0x3C] = r"
"\<And>r :: word32. is_aligned r 6 \<Longrightarrow> hd [r , r + 4 .e. r + 0x3C] = r"
apply (subgoal_tac "r \<le> r + 0x3C")
apply (clarsimp simp: upto_enum_step_def less_def | intro conjI)+
apply fastforce
@ -373,7 +373,7 @@ proof -
apply (rule dcorres_injection_handler_rhs)
apply (simp add: lookup_pt_slot_def liftE_bindE)
apply (rule corres_symb_exec_r[OF _ get_pde_sp get_pde_inv], simp_all)[1]
apply (clarsimp simp add: corres_alternate2 split: ARM_Structs_A.pde.split)
apply (clarsimp simp add: corres_alternate2 split: Arch_Structs_A.pde.split)
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp select_wp | simp)+
@ -420,7 +420,7 @@ proof -
apply (rule dcorres_injection_handler_rhs)
apply (simp add: lookup_pt_slot_def liftE_bindE)
apply (rule corres_symb_exec_r[OF _ get_pde_sp get_pde_inv], simp_all)[1]
apply (clarsimp simp add: corres_alternate2 split: ARM_Structs_A.pde.split)
apply (clarsimp simp add: corres_alternate2 split: Arch_Structs_A.pde.split)
apply (rename_tac word1 set word2)
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
@ -521,7 +521,7 @@ qed
schematic_lemma get_master_pde_invalid_sp:
"\<lbrace>P\<rbrace> get_master_pde p
\<lbrace>\<lambda>pde s. pde = ARM_Structs_A.pde.InvalidPDE \<longrightarrow>
\<lbrace>\<lambda>pde s. pde = Arch_Structs_A.pde.InvalidPDE \<longrightarrow>
(\<exists>pd. ko_at (ArchObj (arch_kernel_obj.PageDirectory pd)) (?p && ~~ mask pd_bits) s \<and>
pde = pd (ucast (?p && mask pd_bits >> 2))) \<and> P s\<rbrace>"
apply (simp add:get_master_pde_def)
@ -549,6 +549,8 @@ lemma shiftl_mod:
*)
lemma decode_invocation_archcap_corres:
notes label_split_asm = invocation_label.split_asm arch_invocation_label.split_asm
shows
"\<lbrakk> Some intent = transform_intent (invocation_type label') args';
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
invoked_cap = transform_cap invoked_cap';
@ -573,7 +575,7 @@ proof (induct x)
apply (clarsimp simp: get_asid_pool_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def
decode_asid_pool_invocation_def
split del: split_if split: invocation_label.split_asm list.split_asm)
split del: split_if split: label_split_asm list.split_asm)
apply (simp add: split_beta corres_alternate2
liftE_bindE corres_symb_exec_in_gets
corres_whenE_throwError_split_rhs
@ -630,7 +632,7 @@ next
option_map_Some_eq2 throw_opt_def
decode_asid_control_invocation_def
transform_cnode_index_and_depth_def
split del: split_if split: invocation_label.split_asm list.split_asm)
split del: split_if split: label_split_asm list.split_asm)
apply (simp add: split_beta corres_alternate2
liftE_bindE corres_symb_exec_in_gets
corres_whenE_throwError_split_rhs
@ -691,7 +693,7 @@ next
decode_page_invocation_def
transform_intent_page_map_def
transform_intent_page_remap_def
split del: split_if split: invocation_label.split_asm list.split_asm,
split del: split_if split: label_split_asm list.split_asm,
simp_all add: split_beta corres_alternate2
liftE_bindE corres_symb_exec_in_gets
corres_whenE_throwError_split_rhs
@ -704,7 +706,7 @@ next
gets_the_def bind_assoc corres_symb_exec_in_gets
assert_opt_def)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPageFlush_def
opt_object_page_directory invs_valid_idle label_to_flush_type_def isPageFlushLabel_def
dest!: a_type_pdD)+
apply (rule_tac r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv x21 && ~~ mask pd_bits))" for I
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
@ -835,10 +837,10 @@ next
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (clarsimp simp: InvocationLabels_H.isPageFlush_def)+
apply (clarsimp simp: isPageFlushLabel_def)+
apply (rule corres_returnOk,clarsimp simp:arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def |
clarsimp simp: InvocationLabels_H.isPageFlush_def)+
clarsimp simp: isPageFlushLabel_def)+
done
next
case (PageTableCap ptr asid)
@ -851,7 +853,7 @@ next
decode_page_table_invocation_def
transform_intent_page_table_map_def
split del: split_if
split: invocation_label.split_asm list.split_asm)
split: label_split_asm list.split_asm)
apply (simp add: throw_on_none_def transform_cap_list_def
get_index_def split_beta alternative_refl
transform_mapping_def corres_whenE_throwError_split_rhs corres_alternate2
@ -909,14 +911,14 @@ next
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
get_page_directory_intent_def transform_intent_def
isPDFlush_def
isPDFlushLabel_def
split del: split_if)
apply (clarsimp simp: get_page_directory_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def decode_page_directory_invocation_def
split: invocation_label.split_asm cdl_intent.splits
InvocationLabels_H.invocation_label.splits)
split: label_split_asm cdl_intent.splits
InvocationLabels_H.invocation_label.splits arch_invocation_label.splits)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
Let_unfold opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPDFlush_def InvocationLabels_H.isPageFlush_def
Let_unfold opt_object_page_directory invs_valid_idle label_to_flush_type_def isPDFlushLabel_def isPageFlushLabel_def
dest!: a_type_pdD)+
apply (safe)
apply (simp_all add: Let_unfold)
@ -1357,7 +1359,7 @@ lemma store_pte_page_inv_entries_safe:
"\<lbrace>page_inv_entries_safe (Inl (ab, bb)) and valid_pdpt_objs\<rbrace>
store_pte (hd bb) ab
\<lbrace>\<lambda>rv s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (hd bb && ~~ mask pt_bits) s
\<and> (\<forall>slot\<in>set (tl bb). f (ucast (slot && mask pt_bits >> 2)) = ARM_Structs_A.pte.InvalidPTE))
\<and> (\<forall>slot\<in>set (tl bb). f (ucast (slot && mask pt_bits >> 2)) = Arch_Structs_A.pte.InvalidPTE))
\<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)\<rbrace>"
apply (simp add:store_pte_def set_pt_def set_object_def)
apply (wp get_object_wp)
@ -1401,7 +1403,7 @@ lemma store_pde_page_inv_entries_safe:
"\<lbrace>page_inv_entries_safe (Inr (ab, bb)) and valid_pdpt_objs\<rbrace>
store_pde (hd bb) ab
\<lbrace>\<lambda>rv s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (hd bb && ~~ mask pd_bits) s
\<and> (\<forall>slot\<in>set (tl bb). f (ucast (slot && mask pd_bits >> 2)) = ARM_Structs_A.pde.InvalidPDE))
\<and> (\<forall>slot\<in>set (tl bb). f (ucast (slot && mask pd_bits >> 2)) = Arch_Structs_A.pde.InvalidPDE))
\<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)\<rbrace>"
apply (simp add:store_pde_def set_pd_def set_object_def)
apply (wp get_object_wp)
@ -1561,7 +1563,7 @@ lemma pte_check_if_mapped_corres:
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (clarsimp split: Arch_Structs_A.pte.splits)
apply (simp_all add: get_pte_def get_pt_def get_object_def in_monad bind_assoc split: kernel_object.splits arch_kernel_obj.splits)
apply clarsimp
apply (case_tac y, simp_all add: in_monad)
@ -1580,7 +1582,7 @@ lemma pde_check_if_mapped_corres:
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (clarsimp split: ARM_Structs_A.pde.splits)
apply (clarsimp split: Arch_Structs_A.pde.splits)
apply (simp_all add: get_pde_def get_pd_def get_object_def in_monad bind_assoc)
apply clarsimp
apply (case_tac y, simp_all add: in_monad)
@ -1839,8 +1841,8 @@ proof -
"CSpaceAcc_A.descendants_of cref (cdt s') = {}"
"caps_of_state s' cref = Some cap"
"cap = cap.UntypedCap frame pageBits idx"
"is_aligned (base::word32) ARM_Structs_A.asid_low_bits"
"base < 2 ^ ARM_Structs_A.asid_bits"
"is_aligned (base::word32) Arch_Structs_A.asid_low_bits"
"base < 2 ^ Arch_Structs_A.asid_bits"
assume relation:"arch_invocation_relation (InvokeAsidControl asid_inv)
(arch_invocation.InvokeASIDControl (asid_control_invocation.MakePool frame cnode_ref cref base))"
assume asid_para: "asid_inv' = asid_control_invocation.MakePool frame cnode_ref cref base"

152
proof/drefine/CNode_DR.thy
View File

@ -1063,8 +1063,8 @@ lemma dcorres_ep_cancel_badge_sends:
lemma neq_CPSR:
"msg_info_register \<noteq> CPSR \<and> cap_register \<noteq> CPSR"
by (clarsimp simp:msg_info_register_def cap_register_def ARMMachineTypes.capRegister_def
ARMMachineTypes.msgInfoRegister_def register.simps )
by (clarsimp simp:msg_info_register_def cap_register_def MachineTypes.capRegister_def
MachineTypes.msgInfoRegister_def register.simps )
lemma transform_intent_invalid_invocation:
"transform_intent (invocation_type (mi_label (data_to_message_info 0))) = (\<lambda>x. None)"
@ -1157,7 +1157,7 @@ lemma set_asid_pool_empty':
done
lemma empty_pool:
"(\<lambda>x. if x \<le> 2 ^ ARM_Structs_A.asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty"
"(\<lambda>x. if x \<le> 2 ^ Arch_Structs_A.asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty"
apply (rule ext)
apply (cut_tac ptr=x and 'a=10 in word_up_bound)
apply (simp add:asid_low_bits_def)
@ -1177,8 +1177,8 @@ lemma get_set_asid_pool:
lemma set_asid_pool_empty:
"set_asid_pool a Map.empty \<equiv>
mapM_x (\<lambda>slot. get_asid_pool a >>= (\<lambda>pool. set_asid_pool a (pool(ucast slot:=None))))
[0 :: word32 .e. 2 ^ ARM_Structs_A.asid_low_bits - 1]"
using set_asid_pool_empty' [of "2 ^ ARM_Structs_A.asid_low_bits - 1" a]
[0 :: word32 .e. 2 ^ Arch_Structs_A.asid_low_bits - 1]"
using set_asid_pool_empty' [of "2 ^ Arch_Structs_A.asid_low_bits - 1" a]
apply -
apply (rule eq_reflection)
apply simp
@ -1240,7 +1240,7 @@ lemma dcorres_set_asid_pool_empty:
"dcorres dc \<top> (valid_idle and asid_pool_at a and
(\<lambda>s. mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s)))
(mapM_x PageTableUnmap_D.empty_slot
(map (Pair a) [0 .e. 2 ^ ARM_Structs_A.asid_low_bits - 1]))
(map (Pair a) [0 .e. 2 ^ Arch_Structs_A.asid_low_bits - 1]))
(set_asid_pool a Map.empty)"
apply (unfold set_asid_pool_empty)
apply (rule dcorres_list_all2_mapM_[where F="\<lambda>x y. snd x = snd (transform_asid y)"])
@ -1266,7 +1266,7 @@ lemma dcorres_set_asid_pool_empty:
apply (wp | clarsimp)+
apply simp
apply (wp get_asid_pool_triv | clarsimp simp:typ_at_eq_kheap_obj obj_at_def swp_def)+
apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ ARM_Structs_A.asid_low_bits])")
apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ Arch_Structs_A.asid_low_bits])")
apply (clarsimp simp:set_map)
apply (clarsimp simp del:set_map simp:suffixeq_def)
apply (wp | clarsimp simp:swp_def)+
@ -1468,6 +1468,9 @@ lemma dcorres_storeWord_mapM_x_cvt:
done
qed
lemmas upto_enum_step_shift_red =
upto_enum_step_shift_red[where 'a=32, simplified word_bits_def[symmetric]]
lemma dcorres_arch_recycle_cap_page_cap:
notes CSpace_D.finalise_cap.simps [simp del]
assumes cap: "cap = (arch_cap.PageCap buf fun sz option)"
@ -1540,7 +1543,7 @@ lemma dcorres_empty_pde_slot:"
ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
\<Longrightarrow> dcorres dc \<top> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s)))
(PageTableUnmap_D.empty_slot (y && ~~ mask pd_bits,unat (y && mask pd_bits >>2)))
(store_pde y ARM_Structs_A.pde.InvalidPDE)"
(store_pde y Arch_Structs_A.pde.InvalidPDE)"
apply (clarsimp simp:store_pde_def get_pd_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_def corres_free_fail split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
@ -1562,7 +1565,7 @@ ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
apply (rule ext)
apply (clarsimp simp: transform_page_directory_contents_def unat_map_def
kernel_pde_mask_def ucast_nat_def transform_pde_def
split: if_splits ARM_Structs_A.pte.split_asm)
split: if_splits Arch_Structs_A.pte.split_asm)
apply (clarsimp simp:)+
apply (rule corres_dummy_return_pr)
apply (rule_tac P'="\<lambda>r. op = s'" in corres_underlying_split[where r'=dc])
@ -1591,7 +1594,7 @@ ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
lemma dcorres_empty_pte_slot:
" dcorres dc \<top> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s)))
(PageTableUnmap_D.empty_slot (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)))
(store_pte y ARM_Structs_A.pte.InvalidPTE)"
(store_pte y Arch_Structs_A.pte.InvalidPTE)"
apply (clarsimp simp:store_pte_def get_pt_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_def corres_free_fail split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
@ -1612,7 +1615,7 @@ lemma dcorres_empty_pte_slot:
apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def)
apply (rule ext)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def ucast_nat_def
split: if_splits ARM_Structs_A.pte.split_asm)
split: if_splits Arch_Structs_A.pte.split_asm)
apply (clarsimp simp: )+
apply (rule corres_dummy_return_pr)
apply (rule_tac P'="\<lambda>r. op = s'" in corres_underlying_split[where r'=dc])
@ -1913,7 +1916,7 @@ lemma dcorres_recycle_pd_caps:
lemma dcorres_clear_object_caps_pt:
"dcorres dc \<top> (invs and cte_wp_at (op = (cap.ArchObjectCap (arch_cap.PageTableCap w option))) (a, b))
(clear_object_caps w)
(mapM_x (swp store_pte ARM_Structs_A.pte.InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])"
(mapM_x (swp store_pte Arch_Structs_A.pte.InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])"
apply (clarsimp simp:arch_recycle_cap_def clear_object_caps_def gets_def)
apply (rule dcorres_absorb_get_l)
apply (subgoal_tac "\<exists>ptx. (ko_at (ArchObj (arch_kernel_obj.PageTable ptx)) w) s'")
@ -2829,7 +2832,7 @@ lemma has_recycle_rights_eq [simp]:
"CNode_D.has_recycle_rights (transform_cap cap) =
CSpace_A.has_recycle_rights cap"
apply (simp add: CNode_D.has_recycle_rights_def CSpace_A.has_recycle_rights_def split: cap.splits)
apply (auto simp: transform_cap_def all_rights_def
apply (auto simp: transform_cap_def all_rights_def arch_has_recycle_rights_def
split: rights.splits arch_cap.splits)
done
@ -2887,6 +2890,19 @@ lemma corres_bindE_throwError:
done
lemma decode_cnode_corres:
notes defns = transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
transform_intent_cnode_mutate_def
transform_intent_cnode_mint_def
transform_intent_cnode_rotate_def
transform_cap_list_def get_index_def
throw_on_none_def
transform_cnode_index_and_depth_def and
splits = invocation_label.split_asm arch_invocation_label.split_asm list.split_asm
shows
"\<lbrakk> Some (CNodeIntent ui) = transform_intent (invocation_type label') args';
cap = transform_cap cap';
cap' = Structures_A.CNodeCap word n x;
@ -2899,16 +2915,7 @@ lemma decode_cnode_corres:
apply (drule_tac s="Some x" for x in sym)
apply (rule_tac label=label' and args=args' and exs="map fst excaps'"
in decode_cnode_cases2)
apply (clarsimp simp: transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
transform_intent_cnode_mint_def
transform_intent_cnode_mutate_def
transform_cap_list_def get_index_def
throw_on_none_def
split: invocation_label.split_asm list.split_asm)
apply (clarsimp simp: defns split: splits)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -3035,18 +3042,8 @@ lemma decode_cnode_corres:
apply (subgoal_tac "valid_mdb s")
apply (fastforce simp: valid_mdb_def mdb_cte_at_def)
apply fastforce
apply (clarsimp simp: transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
transform_intent_cnode_mint_def
transform_intent_cnode_mutate_def
transform_cap_list_def get_index_def
throw_on_none_def
transform_cnode_index_and_depth_def
split: invocation_label.split_asm list.split_asm)
apply (clarsimp simp: defns split: splits)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -3056,16 +3053,7 @@ lemma decode_cnode_corres:
apply wp[2]
apply simp
apply fastforce
apply (clarsimp simp: transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
transform_intent_cnode_mint_def
transform_intent_cnode_mutate_def
transform_cap_list_def get_index_def
throw_on_none_def transform_cnode_index_and_depth_def
split: invocation_label.split_asm list.split_asm)
apply (clarsimp simp: defns split: splits)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -3075,16 +3063,7 @@ lemma decode_cnode_corres:
apply wp[2]
apply simp
apply fastforce
apply (clarsimp simp: transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
transform_intent_cnode_mint_def
transform_intent_cnode_mutate_def
transform_cap_list_def get_index_def
throw_on_none_def transform_cnode_index_and_depth_def
split: invocation_label.split_asm list.split_asm)
apply (clarsimp simp: defns split: splits)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -3098,16 +3077,7 @@ lemma decode_cnode_corres:
apply (wp lsfco_not_idle)
apply simp
apply fastforce
apply (clarsimp simp: transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
transform_intent_cnode_mint_def
transform_intent_cnode_mutate_def
transform_cap_list_def get_index_def
throw_on_none_def transform_cnode_index_and_depth_def
split: invocation_label.split_asm list.split_asm)
apply (clarsimp simp: defns split: splits)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -3126,17 +3096,11 @@ lemma decode_cnode_corres:
apply (simp add: translate_cnode_invocation_def)
apply (wp lsfco_not_idle hoare_drop_imps|simp)+
apply fastforce
apply (clarsimp simp: transform_intent_def unlessE_whenE
CNode_D.decode_cnode_invocation_def
Decode_A.decode_cnode_invocation_def
transform_intent_cnode_copy_def
transform_intent_cnode_move_def
apply (clarsimp simp: defns
transform_intent_cnode_mint_def
transform_intent_cnode_mutate_def
transform_cap_list_def get_index_def
throw_on_none_def transform_cnode_index_and_depth_def
transform_intent_cnode_rotate_def
split: invocation_label.split_asm list.split_asm)
transform_intent_cnode_rotate_def
split: splits)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -3218,25 +3182,11 @@ lemma decode_cnode_corres:
apply (erule disjE)
apply (simp add: transform_intent_def upto_enum_def toEnum_def fromEnum_def
enum_invocation_label
split: invocation_label.splits)
split: invocation_label.splits arch_invocation_label.splits)
apply (erule disjE)
apply (simp add: transform_intent_def
enum_invocation_label transform_cnode_index_and_depth_def
transform_intent_cnode_copy_def
transform_intent_cnode_mint_def
transform_intent_cnode_move_def
transform_intent_cnode_mutate_def
transform_intent_cnode_rotate_def
split: invocation_label.splits)
apply (simp add: defns split: splits)
apply (erule disjE)
apply (simp add: transform_intent_def
enum_invocation_label transform_cnode_index_and_depth_def
transform_intent_cnode_copy_def
transform_intent_cnode_mint_def
transform_intent_cnode_move_def
transform_intent_cnode_mutate_def
transform_intent_cnode_rotate_def
split: invocation_label.splits)
apply (simp add: defns split: splits)
apply clarsimp
apply (erule disjE)
apply clarsimp
@ -3244,25 +3194,11 @@ lemma decode_cnode_corres:
apply clarsimp
apply (simp add: upto_enum_def toEnum_def fromEnum_def
enum_invocation_label)
apply (simp add: transform_intent_def
enum_invocation_label transform_cnode_index_and_depth_def
transform_intent_cnode_copy_def
transform_intent_cnode_mint_def
transform_intent_cnode_move_def
transform_intent_cnode_mutate_def
transform_intent_cnode_rotate_def
split: invocation_label.splits)
apply (simp add: defns split: splits)
apply clarsimp
apply (case_tac list)
apply clarsimp
apply (simp add: transform_intent_def upto_enum_def toEnum_def fromEnum_def
enum_invocation_label transform_cnode_index_and_depth_def
transform_intent_cnode_copy_def
transform_intent_cnode_mint_def
transform_intent_cnode_move_def
transform_intent_cnode_mutate_def
transform_intent_cnode_rotate_def
split: invocation_label.splits)
apply (simp add: defns split: splits)
apply clarsimp
apply (case_tac excaps', simp_all)[1]
apply (clarsimp simp: Decode_A.decode_cnode_invocation_def unlessE_whenE)

78
proof/drefine/Finalise_DR.thy
View File

@ -908,28 +908,28 @@ done
definition pd_pt_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_pt_relation pd pt offset s \<equiv>
\<exists>fun u v ref. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> page_table_at pt s \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_Structs_A.pde.PageTablePDE ref u v
\<and> page_table_at pt s \<and> fun (ucast (offset && mask pd_bits >> 2)) = Arch_Structs_A.pde.PageTablePDE ref u v
\<and> pt = Platform.ptrFromPAddr ref )"
definition pd_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_section_relation pd pt offset s \<equiv>
\<exists>fun u v ref1 ref2. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_Structs_A.pde.SectionPDE ref1 u ref2 v
\<and> fun (ucast (offset && mask pd_bits >> 2)) = Arch_Structs_A.pde.SectionPDE ref1 u ref2 v
\<and> pt = Platform.ptrFromPAddr ref1 )"
definition pd_super_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_super_section_relation pd pt offset s \<equiv>
\<exists>fun u v ref1. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_Structs_A.pde.SuperSectionPDE ref1 u v
\<and> fun (ucast (offset && mask pd_bits >> 2)) = Arch_Structs_A.pde.SuperSectionPDE ref1 u v
\<and> pt = Platform.ptrFromPAddr ref1 )"
definition pt_page_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>vmpage_size set\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pt_page_relation pt page offset S s \<equiv>
\<exists>fun. (kheap s pt = Some (ArchObj (arch_kernel_obj.PageTable fun)))
\<and> (case fun (ucast (offset && mask pt_bits >> 2)) of
ARM_Structs_A.pte.LargePagePTE ref fun1 fun2 \<Rightarrow>
Arch_Structs_A.pte.LargePagePTE ref fun1 fun2 \<Rightarrow>
page = Platform.ptrFromPAddr ref \<and> ARMLargePage \<in> S
| ARM_Structs_A.pte.SmallPagePTE ref fun1 fun2 \<Rightarrow>
| Arch_Structs_A.pte.SmallPagePTE ref fun1 fun2 \<Rightarrow>
page = Platform.ptrFromPAddr ref \<and> ARMSmallPage \<in> S
| _ \<Rightarrow> False)"
@ -944,7 +944,7 @@ lemma slot_with_pt_frame_relation:
apply (clarsimp simp:not_idle_thread_def has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] )
apply (clarsimp simp:mask_pt_bits_less split:ARM_Structs_A.pte.split_asm)
apply (clarsimp simp:mask_pt_bits_less split:Arch_Structs_A.pte.split_asm)
done
lemma below_kernel_base:
@ -1024,7 +1024,7 @@ lemma opt_cap_page:"\<lbrakk>valid_idle s;pt_page_relation a pg x S s \<rbrakk>\
apply (frule(1) page_table_not_idle)
apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
restrict_map_def object_slots_def)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:ARM_Structs_A.pte.split_asm | rule conjI )+
apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:Arch_Structs_A.pte.split_asm | rule conjI )+
apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ucast_def mask_pt_bits_less)+
apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def)
@ -1042,7 +1042,7 @@ lemma opt_cap_section:
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
restrict_map_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_Structs_A.pte.split_asm | rule conjI)+
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:Arch_Structs_A.pte.split_asm | rule conjI)+
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ucast_def unat_def mask_pt_bits_less)+
apply (simp add:mask_pd_bits_less)
@ -1051,7 +1051,7 @@ lemma opt_cap_section:
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle
restrict_map_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_Structs_A.pte.split_asm | rule conjI)+
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:Arch_Structs_A.pte.split_asm | rule conjI)+
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ucast_def unat_def mask_pt_bits_less)+
apply (simp add:mask_pd_bits_less)
@ -1150,7 +1150,7 @@ lemma dcorres_delete_cap_simple_set_pt:
and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV
and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageTable fun)) (ptr && ~~ mask pt_bits))
(delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)))
(set_pt (ptr && ~~ mask pt_bits) (fun(ucast (ptr && mask pt_bits >> 2) := ARM_Structs_A.pte.InvalidPTE)))"
(set_pt (ptr && ~~ mask pt_bits) (fun(ucast (ptr && mask pt_bits >> 2) := Arch_Structs_A.pte.InvalidPTE)))"
apply (simp add:delete_cap_simple_def set_pt_def gets_the_def gets_def bind_assoc get_object_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
@ -1242,7 +1242,7 @@ lemma dcorres_delete_cap_simple_set_pde:
or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr)
and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) (ptr && ~~ mask pd_bits))
(delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
(set_pd (ptr && ~~ mask pd_bits) (fun(ucast (ptr && mask pd_bits >> 2) := ARM_Structs_A.pde.InvalidPDE)))"
(set_pd (ptr && ~~ mask pd_bits) (fun(ucast (ptr && mask pd_bits >> 2) := Arch_Structs_A.pde.InvalidPDE)))"
apply (simp add:delete_cap_simple_def set_pd_def gets_the_def gets_def bind_assoc get_object_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
@ -1285,7 +1285,7 @@ lemma dcorres_delete_cap_simple_section:
"dcorres dc \<top> (invs and pd_section_relation (lookup_pd_slot pd v && ~~ mask pd_bits) oid
(lookup_pd_slot pd v) and K (is_aligned pd pd_bits \<and> v < kernel_base))
(delete_cap_simple (cdl_lookup_pd_slot pd v))
(store_pde (lookup_pd_slot pd v) ARM_Structs_A.pde.InvalidPDE)"
(store_pde (lookup_pd_slot pd v) Arch_Structs_A.pde.InvalidPDE)"
apply (clarsimp simp:store_pde_def transform_pd_slot_ref_def
lookup_pd_slot_def)
apply (rule corres_gen_asm2)
@ -1304,6 +1304,8 @@ lemma dcorres_delete_cap_simple_section:
done
lemma large_frame_range_helper:
fixes t :: word32
shows
"t \<in> set [0 , 4 .e. 0x3C] \<Longrightarrow> t < 0x40"
apply (clarsimp simp: upto_enum_step_def)
apply (subgoal_tac "x < 0x10")
@ -1330,6 +1332,8 @@ lemma zip_map_eqv:
done
lemma page_directory_address_eq:
fixes ptr :: word32
shows
"\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits"
apply (drule large_frame_range_helper)
using mask_lower_twice[where m = 14 and n = 6 and x= ptr,symmetric]
@ -1346,6 +1350,8 @@ lemma page_directory_address_eq:
done
lemma page_table_address_eq:
fixes ptr :: word32
shows
"\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr + t && ~~ mask pt_bits"
apply (drule large_frame_range_helper)
using mask_lower_twice[where m = 10 and n = 6 and x= ptr,symmetric]
@ -1520,7 +1526,7 @@ lemma remain_pd_either_section_relation:
"\<lbrakk>\<forall>y \<in> set ys. is_aligned y 2;ptr\<notin> set ys;is_aligned ptr 2\<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in> set ys. (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or>
pd_section_relation (y && ~~ mask pd_bits) pg_id y s) \<rbrace>
store_pde ptr ARM_Structs_A.pde.InvalidPDE
store_pde ptr Arch_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>r s. \<forall>y\<in>set ys.
(pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or>
pd_section_relation (y && ~~ mask pd_bits) pg_id y s)\<rbrace>"
@ -1578,7 +1584,7 @@ lemma dcorres_store_invalid_pde_super_section:
and invs
and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
(delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
(store_pde ptr ARM_Structs_A.pde.InvalidPDE)"
(store_pde ptr Arch_Structs_A.pde.InvalidPDE)"
apply simp
apply (rule corres_gen_asm2)
apply (rule corres_guard_imp)
@ -1594,7 +1600,7 @@ lemma dcorres_store_invalid_pte:
"dcorres dc \<top> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV
and invs )
(delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)))
(store_pte ptr ARM_Structs_A.pte.InvalidPTE)"
(store_pte ptr Arch_Structs_A.pte.InvalidPTE)"
apply (rule corres_guard_imp)
apply (simp add:store_pte_def)
apply (rule corres_symb_exec_r)
@ -1649,10 +1655,10 @@ lemma dcorres_store_pte_non_sense:
lemma store_pde_non_sense_wp:
"\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_Structs_A.pde.InvalidPDE)) \<rbrace>
store_pde x ARM_Structs_A.pde.InvalidPDE
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = Arch_Structs_A.pde.InvalidPDE)) \<rbrace>
store_pde x Arch_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_Structs_A.pde.InvalidPDE))\<rbrace>"
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = Arch_Structs_A.pde.InvalidPDE))\<rbrace>"
apply (simp add:store_pde_def get_object_def get_pde_def set_pd_def set_object_def)
apply wp
apply (clarsimp simp:obj_at_def split:Structures_A.kernel_object.splits arch_kernel_object.splits)
@ -1661,10 +1667,10 @@ lemma store_pde_non_sense_wp:
lemma dcorres_store_invalid_pde_tail_super_section:
"dcorres dc \<top> (valid_idle and
(\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
\<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pd_bits >> 2)) = ARM_Structs_A.pde.InvalidPDE))
\<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pd_bits >> 2)) = Arch_Structs_A.pde.InvalidPDE))
and K (\<forall>sl\<in> set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits))
(return a)
(mapM (swp store_pde ARM_Structs_A.pde.InvalidPDE) slots)"
(mapM (swp store_pde Arch_Structs_A.pde.InvalidPDE) slots)"
proof (induct slots arbitrary:a)
case Nil
show ?case
@ -1689,10 +1695,10 @@ qed
lemma store_pte_non_sense_wp:
"\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_Structs_A.pte.InvalidPTE)) \<rbrace>
store_pte x ARM_Structs_A.pte.InvalidPTE
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = Arch_Structs_A.pte.InvalidPTE)) \<rbrace>
store_pte x Arch_Structs_A.pte.InvalidPTE
\<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_Structs_A.pte.InvalidPTE))\<rbrace>"
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = Arch_Structs_A.pte.InvalidPTE))\<rbrace>"
apply (simp add:store_pte_def get_object_def
get_pte_def set_pt_def set_object_def)
apply wp
@ -1703,10 +1709,10 @@ lemma store_pte_non_sense_wp:
lemma dcorres_store_invalid_pte_tail_large_page:
"dcorres dc \<top> (valid_idle and
(\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
\<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pt_bits >> 2)) = ARM_Structs_A.pte.InvalidPTE))
\<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pt_bits >> 2)) = Arch_Structs_A.pte.InvalidPTE))
and K (\<forall>sl\<in> set slots. sl && ~~ mask pt_bits = slot && ~~ mask pt_bits))
(return a)
(mapM (swp store_pte ARM_Structs_A.pte.InvalidPTE) slots)"
(mapM (swp store_pte Arch_Structs_A.pte.InvalidPTE) slots)"
proof (induct slots arbitrary:a)
case Nil
show ?case
@ -1758,7 +1764,7 @@ lemma dcorres_unmap_large_section:
and (pd_super_section_relation ((lookup_pd_slot ptr v) && ~~ mask pd_bits)
pg_id (lookup_pd_slot ptr v)))
(delete_cap_simple (cdl_lookup_pd_slot ptr v))
(mapM (swp store_pde ARM_Structs_A.pde.InvalidPDE)
(mapM (swp store_pde Arch_Structs_A.pde.InvalidPDE)
(map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]))"
apply (subst mapM_Cons_split)
apply (simp add:upto_enum_step_def upto_enum_def)
@ -1866,14 +1872,14 @@ lemma dcorres_unmap_large_section:
lemma pt_page_relation_weaken:
"\<lbrakk> pt_page_relation a b c S s; S \<subseteq> T \<rbrakk> \<Longrightarrow> pt_page_relation a b c T s"
apply (clarsimp simp: pt_page_relation_def)
apply (auto split: ARM_Structs_A.pte.split)
apply (auto split: Arch_Structs_A.pte.split)
done
lemma pt_page_relation_univ:
"pt_page_relation a b c {ARMLargePage} s
\<Longrightarrow> pt_page_relation a b c UNIV s"
apply (clarsimp simp:pt_page_relation_def)
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (clarsimp split: Arch_Structs_A.pte.splits)
done
lemma dcorres_unmap_large_page:
@ -1881,7 +1887,7 @@ lemma dcorres_unmap_large_page:
\<Longrightarrow> dcorres dc \<top> (invs and valid_pdpt_objs
and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage})
(delete_cap_simple (transform_pt_slot_ref ptr))
(mapM (swp store_pte ARM_Structs_A.pte.InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]))"
(mapM (swp store_pte Arch_Structs_A.pte.InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]))"
apply (subst mapM_Cons_split)
apply (simp add:upto_enum_step_def upto_enum_def)
apply (simp add: PageTableUnmap_D.unmap_page_def)
@ -1959,7 +1965,7 @@ lemma dcorres_unmap_large_page:
apply simp
apply fastforce
apply (clarsimp split:if_splits
ARM_Structs_A.pte.split_asm)
Arch_Structs_A.pte.split_asm)
apply (rule ccontr)
apply (erule_tac x = "ucast (ptr + of_nat x * 4 && mask pt_bits >> 2)"
in in_empty_interE)
@ -2036,7 +2042,7 @@ lemma check_mapping_pptr_pt_relation:
apply (clarsimp simp: a_type_def pt_page_relation_def
split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm)
apply (simp split: ARM_Structs_A.pte.split_asm)
apply (simp split: Arch_Structs_A.pte.split_asm)
done
lemma check_mapping_pptr_section_relation:
@ -2050,7 +2056,7 @@ lemma check_mapping_pptr_section_relation:
apply (clarsimp simp: a_type_def pd_section_relation_def pd_super_section_relation_def
split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm
ARM_Structs_A.pde.split_asm)
Arch_Structs_A.pde.split_asm)
done
lemma check_mapping_pptr_super_section_relation:
@ -2063,7 +2069,7 @@ lemma check_mapping_pptr_super_section_relation:
apply (clarsimp simp: a_type_def pd_section_relation_def pd_super_section_relation_def
split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm
ARM_Structs_A.pde.split_asm)
Arch_Structs_A.pde.split_asm)
done
lemma lookup_pt_slot_aligned:
@ -2248,7 +2254,7 @@ lemma dcorres_unmap_page_table_store_pde:
and valid_idle and K (is_aligned pd 14 \<and> vptr < kernel_base)
and pd_pt_relation (lookup_pd_slot pd vptr && ~~ mask pd_bits) pt_id (lookup_pd_slot pd vptr) )
(delete_cap_simple (cdl_lookup_pd_slot pd vptr))
(store_pde (lookup_pd_slot pd vptr) ARM_Structs_A.pde.InvalidPDE)"
(store_pde (lookup_pd_slot pd vptr) Arch_Structs_A.pde.InvalidPDE)"
apply (rule corres_guard_imp)
apply (rule corres_gen_asm2)
apply (subst dcorres_lookup_pd_slot,assumption)
@ -2317,7 +2323,7 @@ lemma cleanCacheRange_PoU_underlying_memory[wp]:
done
lemma valid_pde_pt_at:
"\<lbrakk>valid_pde (ARM_Structs_A.pde.PageTablePDE word1 se word2) s \<and> pspace_aligned s\<rbrakk>
"\<lbrakk>valid_pde (Arch_Structs_A.pde.PageTablePDE word1 se word2) s \<and> pspace_aligned s\<rbrakk>
\<Longrightarrow> (ptrFromPAddr word1, unat ((vaddr >> 12) && 0xFF)) =
transform_pt_slot_ref (ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2))"
apply (clarsimp simp :transform_pt_slot_ref_def )
@ -3188,7 +3194,7 @@ lemma get_ipc_buffer_words_irq_state_independent[intro!, simp]:
apply (rule ext, rule ext)
apply (simp add: get_ipc_buffer_words_def)
apply (case_tac "tcb_ipcframe x", simp_all)
apply (clarsimp split: ARM_Structs_A.arch_cap.splits)
apply (clarsimp split: Arch_Structs_A.arch_cap.splits)
apply (rule arg_cong[where f=the])
apply (rule evalMonad_mapM_cong)
apply (simp add: evalMonad_def)

2
proof/drefine/Ipc_DR.thy
View File

@ -709,7 +709,7 @@ lemma receive_blocked_waiting_syncs:
apply (subst (asm) handy_enum_lemma3)+
apply clarsimp
apply (case_tac "x \<noteq> idle_thread s")
apply (clarsimp simp: transform_object_def split: Structures_A.kernel_object.splits ARM_Structs_A.arch_kernel_obj.splits option.splits nat.splits)
apply (clarsimp simp: transform_object_def split: Structures_A.kernel_object.splits Arch_Structs_A.arch_kernel_obj.splits option.splits nat.splits)
apply (frule_tac ptr=x in valid_etcbs_tcb_etcb, simp+)
apply (clarsimp simp add: transform_tcb_def tcb_pending_op_slot_def tcb_boundntfn_slot_def infer_tcb_bound_notification_def split: option.splits)
apply (frule_tac tcb="x2a" in bound_tcb_fold, simp)

4
proof/drefine/KHeap_DR.thy
View File

@ -447,7 +447,7 @@ shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<
clarsimp simp: unat_map_def transform_page_table_contents_def cap_counts_def
transform_page_directory_contents_def transform_asid_pool_contents_def
transform_pte_def transform_pde_def transform_asid_pool_entry_def
split:option.splits if_splits ARM_Structs_A.pte.splits ARM_Structs_A.pde.splits
split:option.splits if_splits Arch_Structs_A.pte.splits Arch_Structs_A.pde.splits
dest!:assms)+)
done
@ -1568,7 +1568,7 @@ lemma ntfn_bound_set_lift:
transform_tcb_def restrict_map_Some_iff tcb_slots
split: Structures_A.kernel_object.splits option.splits
Structures_A.thread_state.splits
ARM_Structs_A.arch_kernel_obj.splits| drule(1) valid_etcbs_tcb_etcb)+
Arch_Structs_A.arch_kernel_obj.splits| drule(1) valid_etcbs_tcb_etcb)+
apply (clarsimp simp: transform_def transform_object_def
transform_tcb_def transform_objects_def tcb_slots valid_idle_def obj_at_def
infer_tcb_bound_notification_def map_add_def restrict_map_Some_iff pred_tcb_at_def

6
proof/drefine/Schedule_DR.thy
View File

@ -587,12 +587,12 @@ lemma get_tcb_message_info_nextPC [simp]:
"get_tcb_message_info (tcb\<lparr>tcb_context := (tcb_context tcb)(LR_svc := pc)\<rparr>) =
get_tcb_message_info tcb"
by (simp add: get_tcb_message_info_def
msg_info_register_def ARMMachineTypes.msgInfoRegister_def)
msg_info_register_def MachineTypes.msgInfoRegister_def)
lemma map_msg_registers_nextPC [simp]:
"map ((tcb_context tcb)(LR_svc := pc)) msg_registers =
map (tcb_context tcb) msg_registers"
by (simp add: msg_registers_def ARMMachineTypes.msgRegisters_def
by (simp add: msg_registers_def MachineTypes.msgRegisters_def
upto_enum_red fromEnum_def toEnum_def enum_register)
lemma get_ipc_buffer_words_nextPC [simp]:
@ -609,7 +609,7 @@ lemma transform_tcb_LR_svc:
"transform_tcb m t (tcb\<lparr>tcb_context := (tcb_context tcb)(LR_svc := pc)\<rparr>)
= transform_tcb m t tcb"
by (auto simp add: transform_tcb_def transform_full_intent_def Let_def
cap_register_def ARMMachineTypes.capRegister_def)
cap_register_def MachineTypes.capRegister_def)
(*
* setNextPC in the tcb context is not observable on the capDL level.

12
proof/drefine/StateTranslationProofs_DR.thy
View File

@ -90,20 +90,20 @@ lemma get_tcb_mrs_update_state :
lemma msg_info_badge_register_no_overlap:
"badge_register \<noteq> msg_info_register"
by (clarsimp simp:badge_register_def msg_info_register_def
ARMMachineTypes.badgeRegister_def
ARMMachineTypes.msgInfoRegister_def)
MachineTypes.badgeRegister_def
MachineTypes.msgInfoRegister_def)
lemma badge_cap_register_overlap:
"badge_register = cap_register"
by (clarsimp simp:badge_register_def cap_register_def
ARMMachineTypes.badgeRegister_def
ARMMachineTypes.capRegister_def)
MachineTypes.badgeRegister_def
MachineTypes.capRegister_def)
lemma cap_msg_info_register_no_overlap:
"cap_register \<noteq> msg_info_register"
by (clarsimp simp:msg_info_register_def cap_register_def
ARMMachineTypes.msgInfoRegister_def
ARMMachineTypes.capRegister_def)
MachineTypes.msgInfoRegister_def
MachineTypes.capRegister_def)
lemmas register_overlap_check = msg_info_badge_register_no_overlap
cap_msg_info_register_no_overlap

148
proof/drefine/StateTranslation_D.thy
View File

@ -22,7 +22,7 @@ begin
type_synonym kernel_object = Structures_A.kernel_object
type_synonym tcb = Structures_A.tcb
type_synonym pte = ARM_Structs_A.pte
type_synonym pte = Arch_Structs_A.pte
(* Transform an abstract-spec cap ptr to a capDL one. This is currently
* a no-op; however, it is conceivable that the capDL cptr representation could
@ -264,7 +264,6 @@ where
* For malformed messages etc., we return None.
*)
definition
transform_intent :: "invocation_label \<Rightarrow> word32 list \<Rightarrow> cdl_intent option" where
"transform_intent label args \<equiv>
@ -331,31 +330,31 @@ definition
| IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent)
| IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent)
| IRQSetMode \<Rightarrow> option_map IrqHandlerIntent (transform_intent_irq_set_mode args)
| ARMPageTableMap \<Rightarrow>
map_option PageTableIntent
(transform_intent_page_table_map args)
| ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent)
| ARMPageMap \<Rightarrow>
map_option PageIntent
(transform_intent_page_map args)
| ARMPageRemap \<Rightarrow>
map_option PageIntent
(transform_intent_page_remap args)
| ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent)
| ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent )
| ARMPDClean_Data \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent )
| ARMPDInvalidate_Data \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent )
| ARMPDCleanInvalidate_Data \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent)
| ARMPDUnify_Instruction \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent )
| ARMASIDControlMakePool \<Rightarrow>
map_option AsidControlIntent
(transform_cnode_index_and_depth AsidControlMakePoolIntent args)
| ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent )
| Domainsetset \<Rightarrow> map_option DomainIntent (transform_intent_domain args)"
| ArchInvocationLabel ARMPageTableMap \<Rightarrow>
map_option PageTableIntent
(transform_intent_page_table_map args)
| ArchInvocationLabel ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent)
| ArchInvocationLabel ARMPageMap \<Rightarrow>
map_option PageIntent
(transform_intent_page_map args)
| ArchInvocationLabel ARMPageRemap \<Rightarrow>
map_option PageIntent
(transform_intent_page_remap args)
| ArchInvocationLabel ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent)
| ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent )
| ArchInvocationLabel ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent )
| ArchInvocationLabel ARMPDClean_Data \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent )
| ArchInvocationLabel ARMPDInvalidate_Data \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent )
| ArchInvocationLabel ARMPDCleanInvalidate_Data \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent)
| ArchInvocationLabel ARMPDUnify_Instruction \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent )
| ArchInvocationLabel ARMASIDControlMakePool \<Rightarrow>
map_option AsidControlIntent
(transform_cnode_index_and_depth AsidControlMakePoolIntent args)
| ArchInvocationLabel ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent )
| DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args)"
lemmas transform_intent_tcb_defs =
transform_intent_tcb_read_registers_def
@ -397,26 +396,26 @@ lemma transform_tcb_intent_invocation:
label \<noteq> IRQAckIRQ \<and>
label \<noteq> IRQSetIRQHandler \<and>
label \<noteq> IRQClearIRQHandler \<and>
label \<noteq> ARMPageTableMap \<and>
label \<noteq> ARMPageTableUnmap \<and>
label \<noteq> ARMPageMap \<and>
label \<noteq> ARMPageUnmap \<and>
label \<noteq> ARMPageClean_Data \<and>
label \<noteq> ARMPageInvalidate_Data \<and>
label \<noteq> ARMPageCleanInvalidate_Data \<and>
label \<noteq> ARMPageUnify_Instruction \<and>
label \<noteq> ARMPageGetAddress \<and>
label \<noteq> ARMPDClean_Data \<and>
label \<noteq> ARMPDInvalidate_Data \<and>
label \<noteq> ARMPDCleanInvalidate_Data \<and>
label \<noteq> ARMPDUnify_Instruction \<and>
label \<noteq> ARMASIDControlMakePool \<and>
label \<noteq> ArchInvocationLabel ARMPageTableMap \<and>
label \<noteq> ArchInvocationLabel ARMPageTableUnmap \<and>
label \<noteq> ArchInvocationLabel ARMPageMap \<and>
label \<noteq> ArchInvocationLabel ARMPageUnmap \<and>
label \<noteq> ArchInvocationLabel ARMPageClean_Data \<and>
label \<noteq> ArchInvocationLabel ARMPageInvalidate_Data \<and>
label \<noteq> ArchInvocationLabel ARMPageCleanInvalidate_Data \<and>
label \<noteq> ArchInvocationLabel ARMPageUnify_Instruction \<and>
label \<noteq> ArchInvocationLabel ARMPageGetAddress \<and>
label \<noteq> ArchInvocationLabel ARMPDClean_Data \<and>
label \<noteq> ArchInvocationLabel ARMPDInvalidate_Data \<and>
label \<noteq> ArchInvocationLabel ARMPDCleanInvalidate_Data \<and>
label \<noteq> ArchInvocationLabel ARMPDUnify_Instruction \<and>
label \<noteq> ArchInvocationLabel ARMASIDControlMakePool \<and>
label \<noteq> DomainSetSet)"
apply(intro conjI)
apply(rule iffI,
simp add: transform_intent_def transform_intent_tcb_defs split: list.split_asm,
simp add: transform_intent_def transform_intent_tcb_defs split: invocation_label.split_asm list.split_asm)+
apply(simp add: transform_intent_def transform_intent_tcb_defs split: invocation_label.split_asm)+
simp add: transform_intent_def transform_intent_tcb_defs split: invocation_label.split_asm arch_invocation_label.split_asm list.split_asm)+
apply(simp add: transform_intent_def transform_intent_tcb_defs split: invocation_label.split_asm arch_invocation_label.split_asm)+
done
lemma transform_intent_isnot_UntypedIntent:
@ -433,13 +432,13 @@ lemma transform_intent_isnot_UntypedIntent:
apply (clarsimp simp: transform_type_def)
apply (simp add: linorder_not_less eval_nat_numeral le_Suc_eq unat_arith_simps)
apply(erule disjE)
apply(auto simp: transform_intent_def option_map_def split: invocation_label.split option.split_asm)[1]
apply(auto simp: transform_intent_def option_map_def split: invocation_label.split arch_invocation_label.split option.split_asm)[1]
apply (erule disjE)
apply (auto simp: transform_intent_def transform_intent_untyped_retype_def
option_map_def split: invocation_label.split option.split_asm list.split)[1]
apply clarsimp
apply (clarsimp simp: transform_intent_def transform_type_def transform_intent_untyped_retype_def)
apply (clarsimp simp: option_map_def split: invocation_label.splits option.splits list.splits)
apply (clarsimp simp: option_map_def split: invocation_label.splits arch_invocation_label.splits option.splits list.splits)
apply (clarsimp simp: transform_type_def split: split_if_asm)
done
@ -462,6 +461,9 @@ lemmas transform_intent_cnode_defs =
transform_intent_cnode_mutate_def
transform_intent_cnode_rotate_def
method case_labels for label :: invocation_label =
(cases label, find_goal \<open>match premises in "label = ArchInvocationLabel x" for x \<Rightarrow> \<open>cases x\<close>\<close>)
lemma transform_intent_isnot_CNodeIntent:
"(\<not> (\<exists> ui. Some (CNodeIntent ui) = transform_intent label args))
= ((label = CNodeRevoke \<longrightarrow> length args < 2) \<and>
@ -483,7 +485,7 @@ lemma transform_intent_isnot_CNodeIntent:
split: list.split)
prefer 10
apply(clarify)
apply(case_tac label)
apply(case_labels label)
apply(clarsimp simp: transform_intent_def
option_map_def transform_intent_cnode_defs
split: list.split_asm option.split_asm)+
@ -506,15 +508,15 @@ lemma transform_intent_isnot_TcbIntent:
apply(rule iffI)
apply(erule contrapos_np)
apply(clarsimp simp: transform_intent_def)
apply(case_tac label)
apply(case_labels label)
apply(simp_all)
apply(fastforce simp: transform_intent_tcb_defs
option_map_def
split: list.split)+
apply(unfold transform_intent_def)
apply(case_tac label, simp_all add: option_map_def split: option.split)
apply (auto simp: transform_intent_tcb_defs
split: list.splits)
apply(case_labels label, simp_all add: option_map_def split: option.split)
apply (auto simp: transform_intent_tcb_defs
split: list.splits arch_invocation_label.splits)
done
(*
@ -600,15 +602,15 @@ where
| Structures_A.Zombie ptr _ _ \<Rightarrow>
Types_D.ZombieCap ptr
| Structures_A.ArchObjectCap arch_cap \<Rightarrow> (case arch_cap of
ARM_Structs_A.ASIDControlCap \<Rightarrow>
Arch_Structs_A.ASIDControlCap \<Rightarrow>
Types_D.AsidControlCap
| ARM_Structs_A.ASIDPoolCap ptr asid \<Rightarrow>
| Arch_Structs_A.ASIDPoolCap ptr asid \<Rightarrow>
Types_D.AsidPoolCap ptr (fst $ (transform_asid asid))
| ARM_Structs_A.PageCap ptr cap_rights_ sz mp \<Rightarrow>
| Arch_Structs_A.PageCap ptr cap_rights_ sz mp \<Rightarrow>
Types_D.FrameCap ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp)
| ARM_Structs_A.PageTableCap ptr mp \<Rightarrow>
| Arch_Structs_A.PageTableCap ptr mp \<Rightarrow>
Types_D.PageTableCap ptr Real (transform_mapping mp)
| ARM_Structs_A.PageDirectoryCap ptr mp \<Rightarrow>
| Arch_Structs_A.PageDirectoryCap ptr mp \<Rightarrow>
Types_D.PageDirectoryCap ptr Real (option_map transform_asid mp)
)
"
@ -820,19 +822,19 @@ declare transform_paddr_def[simp]
* This transforms the references to frames into frame caps.
*)
definition
transform_pte :: "ARM_Structs_A.pte \<Rightarrow> cdl_cap"
transform_pte :: "Arch_Structs_A.pte \<Rightarrow> cdl_cap"
where
"transform_pte pte \<equiv> case pte of
ARM_Structs_A.InvalidPTE \<Rightarrow> cdl_cap.NullCap
| ARM_Structs_A.LargePagePTE ref _ rights_ \<Rightarrow>
Arch_Structs_A.InvalidPTE \<Rightarrow> cdl_cap.NullCap
| Arch_Structs_A.LargePagePTE ref _ rights_ \<Rightarrow>
Types_D.FrameCap (transform_paddr ref) rights_
(pageBitsForSize ARMLargePage) Fake None
| ARM_Structs_A.SmallPagePTE ref _ rights_ \<Rightarrow>
| Arch_Structs_A.SmallPagePTE ref _ rights_ \<Rightarrow>
Types_D.FrameCap (transform_paddr ref) rights_
(pageBitsForSize ARMSmallPage) Fake None"
definition
transform_page_table_contents :: "(word8 \<Rightarrow> ARM_Structs_A.pte) \<Rightarrow> (nat \<Rightarrow> cdl_cap option)"
transform_page_table_contents :: "(word8 \<Rightarrow> Arch_Structs_A.pte) \<Rightarrow> (nat \<Rightarrow> cdl_cap option)"
where
"transform_page_table_contents M \<equiv> unat_map (Some o transform_pte o M)"
@ -842,27 +844,27 @@ where
* This transforms the references to frames into PageTable or Frame caps.
*)
definition
transform_pde :: "ARM_Structs_A.pde \<Rightarrow> cdl_cap"
transform_pde :: "Arch_Structs_A.pde \<Rightarrow> cdl_cap"
where
"transform_pde pde \<equiv> case pde of
ARM_Structs_A.InvalidPDE \<Rightarrow> cdl_cap.NullCap
| ARM_Structs_A.PageTablePDE ref _ _ \<Rightarrow>
Arch_Structs_A.InvalidPDE \<Rightarrow> cdl_cap.NullCap
| Arch_Structs_A.PageTablePDE ref _ _ \<Rightarrow>
Types_D.PageTableCap (transform_paddr ref) Fake None
| ARM_Structs_A.SectionPDE ref _ _ rights_ \<Rightarrow>
| Arch_Structs_A.SectionPDE ref _ _ rights_ \<Rightarrow>
Types_D.FrameCap (transform_paddr ref) rights_
(pageBitsForSize ARMSection) Fake None
| ARM_Structs_A.SuperSectionPDE ref _ rights_ \<Rightarrow>
| Arch_Structs_A.SuperSectionPDE ref _ rights_ \<Rightarrow>
Types_D.FrameCap (transform_paddr ref) rights_
(pageBitsForSize ARMSuperSection) Fake None"
definition
kernel_pde_mask :: "(12 word \<Rightarrow> ARM_Structs_A.pde) \<Rightarrow> (12 word \<Rightarrow> ARM_Structs_A.pde)"
kernel_pde_mask :: "(12 word \<Rightarrow> Arch_Structs_A.pde) \<Rightarrow> (12 word \<Rightarrow> Arch_Structs_A.pde)"
where
"kernel_pde_mask M \<equiv> \<lambda>x.
if (ucast (kernel_base >> 20)) \<le> x then ARM_Structs_A.InvalidPDE else M x"
if (ucast (kernel_base >> 20)) \<le> x then Arch_Structs_A.InvalidPDE else M x"
definition
transform_page_directory_contents :: "(12 word \<Rightarrow> ARM_Structs_A.pde) \<Rightarrow> (nat \<Rightarrow> cdl_cap option)"
transform_page_directory_contents :: "(12 word \<Rightarrow> Arch_Structs_A.pde) \<Rightarrow> (nat \<Rightarrow> cdl_cap option)"
where
"transform_page_directory_contents M \<equiv> unat_map (Some o transform_pde o kernel_pde_mask M)"
@ -883,17 +885,17 @@ definition
| Structures_A.TCB tcb \<Rightarrow> case opt_etcb of Some etcb \<Rightarrow> transform_tcb ms ref tcb etcb | None \<Rightarrow> undefined
| Structures_A.Endpoint _ \<Rightarrow> Types_D.Endpoint
| Structures_A.Notification _ \<Rightarrow> Types_D.Notification
| Structures_A.ArchObj (ARM_Structs_A.ASIDPool ap) \<Rightarrow>
| Structures_A.ArchObj (Arch_Structs_A.ASIDPool ap) \<Rightarrow>
Types_D.AsidPool \<lparr>cdl_asid_pool_caps = (transform_asid_pool_contents ap)\<rparr>
| Structures_A.ArchObj (ARM_Structs_A.PageTable ptx) \<Rightarrow>
| Structures_A.ArchObj (Arch_Structs_A.PageTable ptx) \<Rightarrow>
Types_D.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents ptx)\<rparr>
| Structures_A.ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
| Structures_A.ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
Types_D.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents pd)\<rparr>
| Structures_A.ArchObj (ARM_Structs_A.DataPage sz) \<Rightarrow>
| Structures_A.ArchObj (Arch_Structs_A.DataPage sz) \<Rightarrow>
Types_D.Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>"
lemmas transform_object_simps [simp] =
transform_object_def [split_simps Structures_A.kernel_object.split ARM_Structs_A.arch_kernel_obj.split]
transform_object_def [split_simps Structures_A.kernel_object.split Arch_Structs_A.arch_kernel_obj.split]
(* Lifts a map over a function, returning the empty map if that
function would be insufficiently injective *)

16
proof/drefine/Syscall_DR.thy
View File

@ -226,7 +226,7 @@ lemma decode_domain_corres:
(Decode_A.decode_domain_invocation label' args' excaps')"
apply (unfold Tcb_D.decode_domain_invocation_def Decode_A.decode_domain_invocation_def)
apply (unfold transform_cap_list_def)
apply (case_tac "invocation_type label'"; simp)
apply (case_labels "invocation_type label'"; simp)
apply (clarsimp simp: transform_intent_def option_map_def
split: option.splits)+
defer
@ -475,7 +475,7 @@ lemma transform_intent_arch_cap_None:
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply wp
apply (case_tac arch_cap)
apply (case_tac "invocation_type label")
apply (case_labels "invocation_type label")
apply (simp_all add:arch_decode_invocation_def split del:if_splits)
apply wp
apply (clarsimp split:if_splits | rule conjI)+
@ -483,14 +483,14 @@ lemma transform_intent_arch_cap_None:
apply (clarsimp split:cap.splits | rule conjI | wp)+
apply (clarsimp split:arch_cap.splits | rule conjI | wp)+
apply ((clarsimp simp:transform_intent_def | wp) +)[2]
apply (case_tac "invocation_type label")
apply (case_labels "invocation_type label")
apply (simp_all add:arch_decode_invocation_def split del:if_splits)
apply wp
apply (case_tac "excaps ! 0")
apply (clarsimp simp:transform_intent_def transform_cnode_index_and_depth_def split:list.split_asm)
apply wp
apply (case_tac "invocation_type label")
apply (simp_all add:arch_decode_invocation_def InvocationLabels_H.isPageFlush_def split del:if_splits)
apply (case_labels "invocation_type label")
apply (simp_all add:arch_decode_invocation_def isPageFlushLabel_def split del:if_splits)
apply (wp)
apply (clarsimp simp:transform_intent_def transform_intent_page_map_def split:list.split_asm )
apply wp
@ -499,7 +499,7 @@ lemma transform_intent_arch_cap_None:
apply (clarsimp simp:transform_intent_def
transform_intent_page_remap_def split:list.split_asm)
apply ((clarsimp simp:transform_intent_def | wp)+)
apply (case_tac "invocation_type label")
apply (case_labels "invocation_type label")
apply (simp_all)
apply (intro conjI impI | wp)+
apply (clarsimp | rule conjI)+
@ -510,8 +510,8 @@ lemma transform_intent_arch_cap_None:
apply ((clarsimp simp:transform_intent_def
split:list.split_asm
| wp)+)[1]
apply (case_tac "invocation_type label")
apply (simp_all add: isPDFlush_def)
apply (case_labels "invocation_type label")
apply (simp_all add: isPDFlushLabel_def)
apply (wp)
done

6
proof/drefine/Tcb_DR.thy
View File

@ -216,7 +216,7 @@ lemma decode_tcb_cap_label_not_match:
lemma is_cnode_cap_update_cap_data:
"Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a) \<Longrightarrow> is_cnode_cap a"
apply (case_tac a)
apply (clarsimp simp:update_cap_data_def is_arch_cap_def badge_update_def
apply (clarsimp simp:update_cap_data_def arch_update_cap_data_def is_arch_cap_def badge_update_def
is_cap_simps split:split_if_asm)+
done
@ -226,7 +226,7 @@ lemma update_cnode_cap_data:
apply (clarsimp simp:is_cap_simps)
apply (clarsimp split:if_splits)
apply (simp add:cdl_update_cnode_cap_data_def CSpace_D.update_cap_data_def)
apply (clarsimp simp: update_cap_data_def split:if_splits)
apply (clarsimp simp: update_cap_data_def arch_update_cap_data_def split:if_splits)
apply ((cases ab,simp_all add:badge_update_def)+)[2]
apply (clarsimp simp:is_cap_simps the_cnode_cap_def word_size split:split_if_asm simp:Let_def)
apply (clarsimp simp:cdl_update_cnode_cap_data_def WordSetup.word_bits_def of_drop_to_bl
@ -246,7 +246,7 @@ lemma decode_tcb_corres:
apply (drule sym, frule transform_tcb_intent_invocation)
apply (unfold transform_cap_def)
apply (unfold transform_cap_list_def)
apply(case_tac "invocation_type label'")
apply(case_labels "invocation_type label'")
apply(simp_all)
(* TCBReadRegisters *)
apply(clarsimp simp: decode_read_registers_def split: list.split)

6
proof/drefine/Untyped_DR.thy
View File

@ -410,10 +410,10 @@ lemma transform_default_tcb:
= Tcb (Types_D.default_tcb domain)"
apply (simp add: transform_tcb_def default_tcb_def Types_D.default_tcb_def)
apply (simp add: transform_full_intent_def Let_def new_context_def
cap_register_def ARMMachineTypes.capRegister_def
cap_register_def MachineTypes.capRegister_def
get_tcb_mrs_def
Suc_le_eq get_tcb_message_info_def msg_info_register_def
ARMMachineTypes.msgInfoRegister_def data_to_message_info_def
MachineTypes.msgInfoRegister_def data_to_message_info_def
get_ipc_buffer_words_def)
apply (simp add: transform_intent_def invocation_type_def fromEnum_def
enum_invocation_label toEnum_def)
@ -1789,7 +1789,7 @@ lemma decode_untyped_corres:
(Decode_A.decode_untyped_invocation label' args' slot' cap' (map fst excaps'))"
apply (simp add: transform_intent_def option_map_Some_eq2
transform_intent_untyped_retype_def
split: invocation_label.split_asm list.split_asm
split: invocation_label.split_asm arch_invocation_label.split_asm list.split_asm
option.split_asm)
apply (cases ui)
apply (drule transform_translate_type[where 'a=det_ext])

2
spec/capDL/Types_D.thy
View File

@ -17,7 +17,7 @@
theory Types_D
imports
"../abstract/ARM_VMRights_A"
"../abstract/$L4V_ARCH/ArchVMRights_A"
Intents_D
"../../lib/SplitRule"
begin