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

isabelle-2021: update DRefine 

Signed-off-by: Gerwin Klein <kleing@unsw.edu.au>
This commit is contained in:
Gerwin Klein 2021-02-17 20:59:13 +11:00 committed by Gerwin Klein
parent 7edf5a6b37
commit ce9f9ffe60
11 changed files with 361 additions and 395 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
proof/drefine/Arch_DR.thy
View File

@ -216,7 +216,7 @@ proof -
have aligned_4_hd:
"\<And>r :: word32. is_aligned r 6 \<Longrightarrow> hd (map (\<lambda>x. x + r) [0 , 4 .e. 0x3C]) = r"
apply (subgoal_tac "r \<le> r + 0x3C")
apply (clarsimp simp: upto_enum_step_def less_def o_def | intro conjI)+
apply (clarsimp simp: upto_enum_step_def o_def | intro conjI)+
apply (subst hd_map)
apply (clarsimp simp:upto_enum_def)
apply (clarsimp simp:upto_enum_def hd_map)
@ -1270,6 +1270,7 @@ lemma store_pte_page_inv_entries_safe:
\<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_A.pte.InvalidPTE))
\<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)\<rbrace>"
including no_take_bit
apply (simp add:store_pte_def set_pt_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp:obj_at_def page_inv_entries_safe_def split:if_splits)
@ -1286,11 +1287,11 @@ lemma store_pte_page_inv_entries_safe:
apply simp
apply (subst (asm) is_aligned_shiftr_add)
apply (erule is_aligned_after_mask)
apply (simp add:pt_bits_def pageBits_def)+
apply (simp add:is_aligned_shiftl_self)
apply (rule shiftl_less_t2n)
apply (rule word_of_nat_less,simp)
apply simp+
apply (simp add:pt_bits_def pageBits_def)+
apply (simp add:is_aligned_shiftl_self)
apply (rule shiftl_less_t2n)
apply (rule word_of_nat_less,simp)
apply simp+
apply (subst (asm) ucast_add)
apply simp
apply simp
@ -1298,7 +1299,7 @@ lemma store_pte_page_inv_entries_safe:
apply simp
apply (rule word_of_nat_less)
apply simp
apply (simp add:ucast_of_nat_small of_nat_neq_0)
apply (simp add:ucast_of_nat_small of_nat_neq_0 del: word_of_nat_eq_0_iff)
apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def tl_map_simp
map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n image_def)
apply (simp add:field_simps)
@ -1312,13 +1313,13 @@ lemma store_pde_page_inv_entries_safe:
\<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_A.pde.InvalidPDE))
\<and> (\<forall>sl\<in>set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)\<rbrace>"
including no_take_bit
apply (simp add:store_pde_def set_pd_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp:obj_at_def page_inv_entries_safe_def split:if_splits)
apply (intro conjI impI)
apply (clarsimp simp:hd_map_simp upto_enum_def
upto_enum_step_def drop_map
tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n)
apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def drop_map
tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n)
apply (clarsimp simp add:field_simps)
apply (subst (asm) shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric])+
apply (subst (asm) and_mask_plus[where a = "of_nat slot << 2"])
@ -1328,11 +1329,11 @@ lemma store_pde_page_inv_entries_safe:
apply simp
apply (subst (asm) is_aligned_shiftr_add)
apply (erule is_aligned_after_mask)
apply (simp add:pd_bits_def pageBits_def)+
apply (simp add:is_aligned_shiftl_self)
apply (rule shiftl_less_t2n)
apply (rule word_of_nat_less,simp)
apply simp+
apply (simp add:pd_bits_def pageBits_def)+
apply (simp add:is_aligned_shiftl_self)
apply (rule shiftl_less_t2n)
apply (rule word_of_nat_less,simp)
apply simp+
apply (subst (asm) ucast_add)
apply simp
apply simp
@ -1340,7 +1341,7 @@ lemma store_pde_page_inv_entries_safe:
apply simp
apply (rule word_of_nat_less)
apply simp
apply (simp add:ucast_of_nat_small of_nat_neq_0)
apply (simp add:ucast_of_nat_small of_nat_neq_0 del: word_of_nat_eq_0_iff)
apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def tl_map_simp map_eq_Cons_conv
upt_eq_Cons_conv upto_0_to_n image_def)
apply (simp add: field_simps)
@ -1676,10 +1677,6 @@ proof -
apply (clarsimp simp:perform_asid_control_invocation_def)
apply (simp add:arch_invocation_relation_def translate_arch_invocation_def)
apply (cases asid_inv, clarsimp)
apply hypsubst_thin
apply (drule sym)
apply (drule sym)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated [OF _ delete_objects_dcorres])
apply (rule corres_symb_exec_r)

62
proof/drefine/CNode_DR.thy
View File

@ -916,7 +916,7 @@ lemma dcorres_ep_cancel_badge_sends:
apply (rule corres_guard_imp[OF filter_modify_empty_corres])
apply (clarsimp simp:invs_def)
apply (frule_tac epptr = epptr in get_endpoint_pick ,simp add:obj_at_def)
apply (cut_tac ep = epptr and s = "transform s'a" in is_thread_blocked_on_sth)
apply (cut_tac ep = epptr and s = "transform s'" in is_thread_blocked_on_sth)
apply (drule_tac x = x in eqset_imp_iff)
apply (clarsimp simp: valid_state_def valid_ep_abstract_def none_is_sending_ep_def
none_is_receiving_ep_def)
@ -940,7 +940,7 @@ lemma dcorres_ep_cancel_badge_sends:
apply (simp add:valid_ep_def)
apply (simp add:inj_on_def)
apply (simp add:is_thread_blocked_on_sth[simplified])
apply (subgoal_tac "valid_idle s' \<and> valid_etcbs s'")
apply (subgoal_tac "valid_idle s'a \<and> valid_etcbs s'a")
apply (clarsimp simp: ntfn_waiting_set_lift ep_waiting_set_send_lift
ep_waiting_set_recv_lift)
apply (subst ntfn_waiting_set_upd_kh)
@ -966,7 +966,7 @@ lemma dcorres_ep_cancel_badge_sends:
get_thread_state_def)
apply (rule_tac
Q'="\<lambda>s. valid_idle s \<and> valid_etcbs s \<and> not_idle_thread a s
\<and> idle_thread s = idle_thread s'a \<and>
\<and> idle_thread s = idle_thread s' \<and>
st_tcb_at (\<lambda>ts. \<exists>pl. ts = Structures_A.thread_state.BlockedOnSend epptr pl) a s"
in corres_guard_imp[where Q=\<top>])
apply (rule dcorres_absorb_gets_the)
@ -995,7 +995,7 @@ lemma dcorres_ep_cancel_badge_sends:
dest!: get_tcb_rev)
apply (rule ext)
apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp)
apply (case_tac "a=idle_thread s'", simp add: not_idle_thread_def)
apply (case_tac "a=idle_thread s'a", simp add: not_idle_thread_def)
apply (drule (2) transform_objects_tcb)
apply (clarsimp simp: transform_current_thread_def transform_def)
apply (clarsimp simp: not_idle_thread_def transform_tcb_def transform_def
@ -1004,7 +1004,7 @@ lemma dcorres_ep_cancel_badge_sends:
apply simp+
apply (clarsimp simp:bind_assoc not_idle_thread_def)
apply (wp sts_st_tcb_at_neq)
apply (rule_tac Q="\<lambda>r a. valid_idle a \<and> idle_thread a = idle_thread s'a \<and>
apply (rule_tac Q="\<lambda>r a. valid_idle a \<and> idle_thread a = idle_thread s' \<and>
st_tcb_at (\<lambda>ts. \<exists>pl. ts = Structures_A.thread_state.BlockedOnSend epptr pl) y a
\<and> y \<noteq> idle_thread a \<and> valid_etcbs a" in hoare_strengthen_post)
apply wp
@ -1132,6 +1132,7 @@ lemma set_asid_pool_empty'_helper:
"n < 1023 \<Longrightarrow>
(if x = ucast ((1 :: word32) + of_nat n) then None else if x \<le> of_nat n then None else ap x) =
(if (x :: 10 word) \<le> 1 + of_nat n then None else ap x)"
including no_take_bit
apply (frule of_nat_mono_maybe[where x="2^10 - 1" and 'a=10, simplified])
apply (subgoal_tac "ucast (1 + of_nat n :: word32) = (1 + of_nat n :: 10 word)")
prefer 2
@ -1273,8 +1274,8 @@ lemma dcorres_set_asid_pool_empty:
apply clarsimp
apply (clarsimp simp del:set_map simp: suffix_def)
apply (wp | clarsimp simp:swp_def)+
apply (clarsimp simp:list_all2_iff transform_asid_def asid_low_bits_def set_zip)
apply (clarsimp simp:unat_ucast upto_enum_def unat_of_nat)
apply (clarsimp simp:list_all2_iff transform_asid_def asid_low_bits_def set_zip)
apply (clarsimp simp: upto_enum_def take_bit_nat_eq_self)
done
declare fun_upd_apply[simp]
@ -1321,9 +1322,8 @@ lemma dcorres_clear_object_caps_asid_pool:
apply clarsimp
apply (clarsimp simp:invs_def valid_state_def valid_cap_def obj_at_def a_type_def
valid_pspace_def dest!: cte_wp_valid_cap)
apply (clarsimp split:Structures_A.kernel_object.split_asm
arch_kernel_obj.split_asm if_splits)
done
by (clarsimp split: Structures_A.kernel_object.split_asm
arch_kernel_obj.split_asm if_splits)
lemmas valid_idle_invs_strg = invs_valid_idle_strg
@ -1565,27 +1565,26 @@ lemma copy_global_mappings_dwp:
"is_aligned word pd_bits\<Longrightarrow> \<lbrace>\<lambda>ps. valid_idle (ps :: det_state) \<and> transform ps = cs\<rbrace> copy_global_mappings word \<lbrace>\<lambda>r s. transform s = cs\<rbrace>"
apply (simp add:copy_global_mappings_def)
apply wp
apply (rule_tac Q = "\<lambda>r s. valid_idle s \<and> transform s = cs" in hoare_strengthen_post)
apply (rule mapM_x_wp')
apply wp
apply (rule_tac Q="\<lambda>s. valid_idle s \<and> transform s = cs" in hoare_vcg_precond_imp)
apply (rule dcorres_to_wp)
apply (rule corres_guard_imp[OF store_pde_set_cap_corres])
apply (clarsimp simp:kernel_mapping_slots_def)
apply (simp add:ucast_def kernel_base_def pd_bits_def pageBits_def)
apply (simp add:mask_add_aligned)
apply (subst less_mask_eq,simp)
apply (simp add:shiftl_t2n)
apply (subst mult.commute)
apply (rule div_lt_mult,simp+,unat_arith,simp+)
apply (simp add:shiftl_shiftr1 word_size)
apply (subst less_mask_eq,simp)
apply unat_arith
apply (fold ucast_def)
apply (subst ucast_le_migrate[symmetric])
apply (simp add:word_size,unat_arith)
apply (simp add:word_size)+
apply (wp|clarsimp)+
apply (rule_tac Q = "\<lambda>r s. valid_idle s \<and> transform s = cs" in hoare_strengthen_post)
apply (rule mapM_x_wp')
apply wp
apply (rule_tac Q="\<lambda>s. valid_idle s \<and> transform s = cs" in hoare_vcg_precond_imp)
apply (rule dcorres_to_wp)
apply (rule corres_guard_imp[OF store_pde_set_cap_corres])
apply (clarsimp simp:kernel_mapping_slots_def)
apply (simp add: kernel_base_def pd_bits_def pageBits_def)
apply (simp add: mask_add_aligned)
apply (subst less_mask_eq,simp)
apply (simp add:shiftl_t2n)
apply (subst mult.commute)
apply (rule div_lt_mult,simp+,unat_arith,simp+)
apply (simp add:shiftl_shiftr1 word_size)
apply (subst less_mask_eq,simp)
apply unat_arith
apply (subst ucast_le_migrate[symmetric])
apply (simp add:word_size,unat_arith)
apply (simp add:word_size)+
apply (wp|clarsimp)+
done
lemma opt_cap_pd_not_None:
@ -1683,6 +1682,7 @@ lemma dcorres_clear_object_caps_pt:
"dcorres dc \<top> (invs and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageTableCap w option))) (a, b))
(clear_object_caps w)
(mapM_x (swp store_pte ARM_A.pte.InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])"
including no_take_bit
apply (clarsimp simp: 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'")

25
proof/drefine/Corres_D.thy
View File

@ -227,19 +227,20 @@ lemma dcorres_gets_the:
apply (simp add:gets_the_def)
apply (simp add: gets_def)
apply (subst bind_assoc)+
apply (rule corres_split_keep_pfx
[where r'="\<lambda>s s'. s = transform s'\<and> P s \<and> P' s'" and Q="\<lambda>x s. x = s" and Q'="\<lambda>x s. x = s "])
apply (clarsimp simp: corres_underlying_def get_def)
apply (rule corres_split_keep_pfx[where r'="\<lambda>s s'. s = transform s'\<and> P s \<and> P' s'"
and Q="\<lambda>x s. x = s" and Q'="\<lambda>x s. x = s "])
apply (clarsimp simp: corres_underlying_def get_def)
apply (simp add: assert_opt_def)
apply (case_tac "g' xa = None")
apply (clarsimp split:option.splits simp:corres_free_fail)
apply (subgoal_tac "\<exists>obj. g x \<noteq> None")
apply (clarsimp split:option.splits)
apply (rule_tac Q="(=)(transform xa)" and Q'="(=) xa" in corres_guard_imp)
apply (simp add: A)+
using B
apply (wp|clarsimp)+
done
apply (rename_tac x)
apply (case_tac "g' x = None")
apply (clarsimp split:option.splits simp:corres_free_fail)
apply (subgoal_tac "\<exists>obj. g (transform x) \<noteq> None")
apply (clarsimp split:option.splits)
apply (rule_tac Q="(=) (transform x)" and Q'="(=) x" in corres_guard_imp)
apply (simp add: A)+
using B
apply (wp|clarsimp)+
done
lemma wpc_helper_dcorres:
"dcorres r Q Q' f f'

477
proof/drefine/Finalise_DR.thy
View File

@ -866,13 +866,14 @@ lemma mask_pd_bits_less':
done
lemma mask_pd_bits_less:
"nat (uint ((y::word32) && mask pd_bits >> 2)) < 4096"
apply (clarsimp simp:pd_bits_def pageBits_def)
"unat ((y::word32) && mask pd_bits >> 2) < 4096"
apply (clarsimp simp:pd_bits_def pageBits_def simp del: nat_uint_eq)
apply (unfold unat_def)
apply (rule iffD2[OF nat_less_eq_zless[where z = 4096,simplified]])
apply (simp)
apply (simp)
using shiftr_less_t2n'[where m = 12 and x ="(y && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
apply (clarsimp simp:mask_twice)
done
done
lemma mask_pt_bits_less':
"uint (((ptr::word32) && mask pt_bits) >> 2)< 256"
@ -882,13 +883,14 @@ lemma mask_pt_bits_less':
done
lemma mask_pt_bits_less:
"nat (uint ((y::word32) && mask pt_bits >> 2)) < 256"
"unat ((y::word32) && mask pt_bits >> 2) < 256"
apply (clarsimp simp:pt_bits_def pageBits_def)
apply (unfold unat_def)
apply (rule iffD2[OF nat_less_eq_zless[where z = 256,simplified]])
apply (simp)
using shiftr_less_t2n'[where m = 8 and x ="(y && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]]
apply (clarsimp simp:mask_twice)
done
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>
@ -927,27 +929,21 @@ lemma slot_with_pt_frame_relation:
apply (frule(1) page_table_not_idle)
apply (clarsimp simp:slots_with_def transform_def transform_objects_def restrict_map_def)
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:transform_page_table_contents_def transform_pte_def unat_map_def)
apply (clarsimp simp:mask_pt_bits_less split:ARM_A.pte.split_asm)
done
done
lemma below_kernel_base:
"ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
\<Longrightarrow> kernel_pde_mask f (of_nat (unat (y && mask pd_bits >> 2)))
\<Longrightarrow> kernel_pde_mask f (ucast (y && mask pd_bits >> 2))
= f (of_nat (unat (y && mask pd_bits >> 2)))"
apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
apply (simp add:ucast_nat_def[symmetric] unat_def)
done
by (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
(* we need an int version for 2016 *)
lemma below_kernel_base_int:
"ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
\<Longrightarrow> kernel_pde_mask f (of_int (uint (y && mask pd_bits >> 2)))
= f (of_int (uint (y && mask pd_bits >> 2)))"
apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
apply (simp add:ucast_nat_def[symmetric] unat_def)
done
by (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def )
lemma slot_with_pd_pt_relation:
"\<lbrakk>valid_idle s; pd_pt_relation a b y s; ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
@ -960,10 +956,8 @@ lemma slot_with_pd_pt_relation:
apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def below_kernel_base)
apply (simp add:mask_pd_bits_less)
done
done
lemma slot_with_pd_section_relation:
"\<lbrakk>valid_idle s; pd_super_section_relation a b y s \<or> pd_section_relation a b y s;
@ -971,15 +965,14 @@ lemma slot_with_pd_section_relation:
(a, unat (y && mask pd_bits >> 2)) \<in>
(slots_with (\<lambda>x. \<exists>rights sz asid. x = cdl_cap.FrameCap False b rights sz Fake asid)) (transform s)"
apply (erule disjE)
apply (clarsimp simp :pd_super_section_relation_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def mask_pd_bits_less)
apply (clarsimp simp :pd_super_section_relation_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def)
apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (simp add: mask_pd_bits_less)
apply (clarsimp simp :pd_section_relation_def)
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
@ -987,67 +980,59 @@ lemma slot_with_pd_section_relation:
apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def)
apply (clarsimp simp:has_slots_def object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def)
apply (simp add:mask_pd_bits_less)
done
done
lemma opt_cap_page_table:"\<lbrakk>valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
(opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s))
= Some (cdl_cap.PageTableCap pt_id Fake None)"
apply (clarsimp simp:pd_pt_relation_def opt_cap_def transform_def unat_def slots_of_def)
lemma opt_cap_page_table:
"\<lbrakk> valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<rbrakk>
\<Longrightarrow> opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (cdl_cap.PageTableCap pt_id Fake None)"
apply (clarsimp simp :pd_pt_relation_def opt_cap_def transform_def slots_of_def)
apply (frule page_directory_at_rev)
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_def[symmetric] unat_map_def | rule conjI )+
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def)
apply (clarsimp simp:below_kernel_base)
apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] unat_def ucast_def)
apply (simp add:mask_pd_bits_less unat_def)
done
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 | rule conjI )+
apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_def below_kernel_base)
apply (simp add: mask_pd_bits_less )
done
lemma opt_cap_page:"\<lbrakk>valid_idle s;pt_page_relation a pg x S s \<rbrakk>\<Longrightarrow>
\<exists>f sz. (opt_cap (a, unat (x && mask pt_bits >> 2) ) (transform s))
= Some (cdl_cap.FrameCap False pg f sz Fake None)"
apply (clarsimp simp:pt_page_relation_def unat_def opt_cap_def transform_def slots_of_def)
apply (clarsimp simp: pt_page_relation_def opt_cap_def transform_def slots_of_def)
apply (frule page_table_at_rev)
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_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)
done
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_A.pte.split_asm | rule conjI )+
apply (clarsimp simp: transform_page_table_contents_def unat_map_def transform_pte_def)
apply (simp add: mask_pt_bits_less)+
apply (clarsimp simp: transform_page_table_contents_def unat_map_def transform_pte_def)
done
lemma opt_cap_section:
"\<lbrakk>valid_idle s;pd_section_relation a pg x s \<or> pd_super_section_relation a pg x s;
ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
\<exists>f sz. (opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s))
= Some (cdl_cap.FrameCap False pg f sz Fake None)"
unfolding unat_def
apply (erule disjE)
apply (clarsimp simp: pd_section_relation_def opt_cap_def transform_def slots_of_def)
apply (frule page_directory_at_rev)
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_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_int)
apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+
apply (simp add:mask_pd_bits_less)
apply (clarsimp simp:pd_super_section_relation_def opt_cap_def transform_def slots_of_def)
apply (clarsimp simp: pd_section_relation_def opt_cap_def transform_def slots_of_def)
apply (frule page_directory_at_rev)
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_A.pte.split_asm | rule conjI)+
apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_def below_kernel_base)
apply (simp add: mask_pd_bits_less)
apply (clarsimp simp: pd_super_section_relation_def opt_cap_def transform_def slots_of_def)
apply (frule page_directory_at_rev)
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_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_int)
apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+
apply (simp add:mask_pd_bits_less)
done
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_A.pte.split_asm | rule conjI)+
apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_def below_kernel_base)
apply (simp add: mask_pd_bits_less)
done
lemma opt_object_page_table:
"\<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk>
@ -1114,28 +1099,26 @@ lemma dcorres_set_pte_cap:
(KHeap_D.set_cap (a, unat (ptr && mask pt_bits >> 2)) pte_cap)
(KHeap_A.set_object a
(ArchObj (arch_kernel_obj.PageTable (fun(ucast (ptr && mask pt_bits >> 2) := a_pte)))))"
apply (simp add:KHeap_D.set_cap_def KHeap_A.set_object_def get_object_def gets_the_def gets_def bind_assoc unat_def)
apply (simp add: KHeap_D.set_cap_def KHeap_A.set_object_def get_object_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_r)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:obj_at_def opt_object_page_table assert_opt_def has_slots_def object_slots_def)
apply (clarsimp simp:KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def bind_def
corres_underlying_def update_slots_def return_def object_slots_def)
apply (clarsimp simp: obj_at_def opt_object_page_table assert_opt_def has_slots_def object_slots_def)
apply (clarsimp simp: KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def bind_def
corres_underlying_def update_slots_def return_def object_slots_def)
apply (rule sym)
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (clarsimp simp: transform_def transform_current_thread_def)
apply (rule ext)
apply (clarsimp | rule conjI)+
apply (frule page_table_at_rev)
apply (frule(1) page_table_not_idle)
apply (clarsimp simp:transform_objects_def not_idle_thread_def)
apply (rule ext)
apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def)
apply (clarsimp simp:word_of_int word_of_nat mask_pt_bits_less mask_pt_bits_less' ucast_def)
apply (subst (asm) word_of_int_inj)
apply (clarsimp simp:mask_pt_bits_less')+
apply (clarsimp simp:uint_nat)
apply clarify
apply (frule page_table_at_rev)
apply (frule(1) page_table_not_idle)
apply (clarsimp simp: transform_objects_def not_idle_thread_def)
apply (rule ext)
apply (clarsimp simp: transform_page_table_contents_def transform_pte_def unat_map_def)
apply (clarsimp simp: mask_pt_bits_less mask_pt_bits_less')
apply (simp only: ucast_nat_def[symmetric])
apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less)
apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def)
done
done
lemma dcorres_delete_cap_simple_set_pt:
"dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))
@ -1163,44 +1146,39 @@ lemma dcorres_delete_cap_simple_set_pt:
lemma transform_page_table_contents_upd:
"transform_page_table_contents fun(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte pte) =
transform_page_table_contents
(fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))"
transform_page_table_contents (fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))"
apply (rule ext)
apply (clarsimp simp:transform_page_table_contents_def unat_map_def )
apply (clarsimp simp:ucast_nat_def[symmetric])
apply (clarsimp simp: transform_page_table_contents_def unat_map_def)
apply (subgoal_tac "unat (y && mask pt_bits >> 2) < 256")
apply (rule conjI|clarsimp)+
apply (drule word_unat.Abs_eqD)
apply (simp add: unats_def)+
apply (rule conjI|clarsimp)+
apply (simp only: ucast_nat_def[symmetric])
apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less)
apply simp
apply (rule unat_less_helper)
apply (subst shiftr_div_2n_w)
apply (clarsimp simp:word_size)+
apply (rule word_div_mult,simp)
apply (clarsimp simp:pt_bits_def pageBits_def)
apply (rule and_mask_less_size[where n = 10,simplified],simp add:word_size)
done
done
lemma transform_page_directory_contents_upd:
"ucast ((ptr::word32) && mask pd_bits >> 2) \<notin> kernel_mapping_slots
\<Longrightarrow> transform_page_directory_contents f(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde)
= transform_page_directory_contents (f(ucast (ptr && mask pd_bits >> 2) := a_pde))"
apply (rule ext)
apply (simp (no_asm) add:transform_page_directory_contents_def unat_map_def)
apply (simp add:below_kernel_base)
apply (clarsimp simp: unat_def mask_pd_bits_less|rule conjI)+
apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def)
apply (clarsimp simp:ucast_nat_def[symmetric])
apply (drule sym)
apply (drule word_unat.Abs_eqD)
apply (simp add:unats_def unat_def[symmetric])+
apply (rule unat_less_helper)
apply (subst shiftr_div_2n_w,(simp add:word_size)+)
apply (rule word_div_mult,simp)
apply (clarsimp simp:pt_bits_def pd_bits_def pageBits_def)
apply (rule and_mask_less_size[where n = 14,simplified],simp add:word_size)
apply (simp add:word_of_int unat_def)
apply (clarsimp simp:ucast_def word_of_int_nat[OF uint_ge_0,simplified])
done
apply (simp (no_asm) add: transform_page_directory_contents_def unat_map_def)
apply (simp add: below_kernel_base)
apply (clarsimp simp: mask_pd_bits_less | rule conjI)+
apply (clarsimp simp: kernel_pde_mask_def kernel_mapping_slots_def)
apply (simp only: ucast_nat_def[symmetric])
apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less)
apply (rule unat_less_helper)
apply (subst shiftr_div_2n_w; simp add:word_size)
apply (rule word_div_mult, simp)
apply (clarsimp simp: pt_bits_def pd_bits_def pageBits_def)
apply (rule and_mask_less_size[where n = 14,simplified],simp add:word_size)
done
lemma dcorres_set_pde_cap:
"\<lbrakk> (x::word32) = (ptr && mask pd_bits >> 2);pde_cap = transform_pde a_pde; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow>
@ -1214,15 +1192,15 @@ lemma dcorres_set_pde_cap:
apply (clarsimp simp: KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def
bind_def corres_underlying_def update_slots_def object_slots_def return_def)
apply (clarsimp simp: transform_def transform_current_thread_def)
apply (rule ext)
apply (clarsimp | rule conjI)+
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp: transform_objects_def not_idle_thread_def)
apply (rule sym)
apply (erule transform_page_directory_contents_upd)
apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def)
done
apply (rule ext)
apply (clarsimp | rule conjI)+
apply (frule page_directory_at_rev)
apply (frule(1) page_directory_not_idle)
apply (clarsimp simp: transform_objects_def not_idle_thread_def)
apply (rule sym)
apply (erule transform_page_directory_contents_upd)
apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def)
done
lemma dcorres_delete_cap_simple_set_pde:
" ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
@ -1359,13 +1337,9 @@ lemma shiftl_inj_if:
done
lemma ucast_inj_mask:
"((ucast (x::'a::len word)) :: ('b::len word)) = ((ucast (y::'a::len word)) :: ('b::len word))
\<Longrightarrow> (x && mask (len_of TYPE('b))) = (y && mask (len_of TYPE('b)))"
apply (simp add:ucast_def)
apply (simp add:word_ubin.inverse_norm)
apply (simp add:word_ubin.eq_norm)
apply (simp add:and_mask_bintr)
done
"(ucast (x::'a::len word) :: 'b::len word) = (ucast (y::'a::len word) :: 'b::len word)
\<Longrightarrow> x && mask LENGTH('b) = y && mask LENGTH('b)"
by (metis ucast_ucast_mask)
lemma split_word_noteq_on_mask:
"(x \<noteq> y) = (x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k)"
@ -2356,138 +2330,135 @@ lemma dcorres_unmap_page:
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:valid_cap_def)
apply (case_tac vmpage_size)
\<comment> \<open>ARMSmallPage\<close>
apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot])
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply (simp add:transform_pt_slot_ref_def)
apply (rule dcorres_store_invalid_pte[where pg_id = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page)
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR)
apply ((wp check_mapping_pptr_pt_relation | wp (once) hoare_drop_imps)+)[1]
apply (simp | wp lookup_pt_slot_inv)+
apply (simp add: dc_def
| wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
| rule conjI | clarify)+
\<comment> \<open>ARMSmallPage\<close>
apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot])
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply (simp add:transform_pt_slot_ref_def)
apply (rule dcorres_store_invalid_pte[where pg_id = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page)
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR)
apply ((wp check_mapping_pptr_pt_relation | wp (once) hoare_drop_imps)+)[1]
apply (simp | wp lookup_pt_slot_inv)+
apply (simp add: dc_def
| wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
| rule conjI | clarify)+
\<comment> \<open>ARMLargePage\<close>
\<comment> \<open>ARMLargePage\<close>
apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot])
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule dcorres_symb_exec_rE)
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule_tac F = "is_aligned xa 6" in corres_gen_asm2)
apply (erule dcorres_unmap_large_page[where pg_id = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page[unfolded dc_def])
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR is_aligned_mask)
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation])
apply fastforce
apply (simp | wp lookup_pt_slot_inv)+
apply (simp add: ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot])
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule dcorres_symb_exec_rE)
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule_tac F = "is_aligned xa 6" in corres_gen_asm2)
apply (erule dcorres_unmap_large_page[where pg_id = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page[unfolded dc_def])
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR is_aligned_mask)
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation])
apply fastforce
apply (simp | wp lookup_pt_slot_inv)+
apply (simp add: dc_def
| wp lookup_pt_slot_inv hoare_drop_imps
find_pd_for_asid_kernel_mapping_help
| safe)+
| wp lookup_pt_slot_inv hoare_drop_imps find_pd_for_asid_kernel_mapping_help
| safe)+
\<comment> \<open>Section\<close>
apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule dcorres_delete_cap_simple_section[where oid = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page[unfolded dc_def])
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR)
apply ((wp check_mapping_pptr_section_relation | wp (once) hoare_drop_imps)+)[1]
apply (simp | wp lookup_pt_slot_inv)+
apply (simp add: dc_def
| wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
| safe)+
\<comment> \<open>SuperSection\<close>
apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
\<comment> \<open>Section\<close>
apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule dcorres_symb_exec_rE)
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule_tac F = "is_aligned pda 14" in corres_gen_asm2)
apply (erule(2) dcorres_unmap_large_section[where pg_id = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page[unfolded dc_def])
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR is_aligned_mask)
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation])
apply clarsimp
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule dcorres_delete_cap_simple_section[where oid = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page[unfolded dc_def])
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR)
apply ((wp check_mapping_pptr_section_relation | wp (once) hoare_drop_imps)+)[1]
apply (simp | wp lookup_pt_slot_inv)+
apply (simp add: dc_def
| wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
| safe)+
\<comment> \<open>SuperSection\<close>
apply (simp add: ARM_A.unmap_page_def bindE_assoc mapM_x_singleton
PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'"
in corres_split_catch [where f = dc and E = dc and E' =dc])
apply simp
apply (rule corres_guard_imp)
apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified])
apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib
pageBitsForSize_def bindE_assoc mapM_x_singleton)
apply (rule corres_splitEE[OF _ dcorres_might_throw])
apply (rule dcorres_symb_exec_rE)
apply (rule corres_dummy_returnOk_l)
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule_tac F = "is_aligned pd 14" in corres_gen_asm2)
apply (erule(2) dcorres_unmap_large_section[where pg_id = pg])
apply (simp add:liftE_distrib[symmetric] returnOk_liftE)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_flush_page[unfolded dc_def])
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR is_aligned_mask)
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_vcg_conj_lift)
apply (wp hoare_drop_imps)[1]
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation])
apply clarsimp
apply (simp add:is_aligned_mask[symmetric] dc_def
| wp lookup_pt_slot_inv hoare_drop_imps
find_pd_for_asid_kernel_mapping_help
| safe)+
done
| wp lookup_pt_slot_inv hoare_drop_imps find_pd_for_asid_kernel_mapping_help
| safe)+
done
lemma dcorres_delete_asid_none:

7
proof/drefine/Intent_DR.thy
View File

@ -59,15 +59,14 @@ lemma tcb_cap_casesE:
lemma tcb_cnode_index_def2:
"n < 8 \<Longrightarrow> tcb_cnode_index n = bin_to_bl 3 (int n)"
unfolding tcb_cnode_index_def to_bl_def
including no_take_bit
by (simp add: uint_nat unat_of_nat)
lemma bl_to_bin_tcb_cnode_index:
"n < 8 \<Longrightarrow> nat (bl_to_bin (tcb_cnode_index n)) = n"
unfolding tcb_cnode_index_def
apply simp
apply (fold unat_def)
apply (simp add: unat_of_nat)
done
including no_take_bit
by (simp add: unat_of_nat)
(* LIFT LEMMAS:
Lift the property from abstract spec to capdl model

104
proof/drefine/Ipc_DR.thy
View File

@ -1089,17 +1089,16 @@ lemma evalMonad_get_extra_cptrs:
done
lemma dcorres_symb_exec_r_evalMonad:
assumes wp:"\<And>sa. \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>"
assumes corres:"\<And>rv. evalMonad f s = Some rv \<Longrightarrow> dcorres r P ((=) s) h (g rv)"
shows "\<lbrakk>empty_when_fail f;weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> dcorres r P ((=) s) h (f>>=g)"
assumes wp:"\<And>sa. \<lbrace>(=) sa\<rbrace> f \<lbrace>\<lambda>r. (=) sa\<rbrace>"
assumes corres:"\<And>rv. evalMonad f s = Some rv \<Longrightarrow> dcorres r P ((=) s) h (g rv)"
shows "\<lbrakk> empty_when_fail f; weak_det_spec ((=) s) f \<rbrakk> \<Longrightarrow> dcorres r P ((=) s) h (f>>=g)"
apply (rule_tac Q'="\<lambda>r. (=) s and K_bind (evalMonad f s = Some r)" in corres_symb_exec_r)
apply (rule dcorres_expand_pfx)
using corres
apply (clarsimp simp:corres_underlying_def)
apply fastforce
apply (wp wp,simp,rule evalMonad_wp)
apply (simp add:wp)+
done
apply (rule dcorres_expand_pfx)
using corres
apply (clarsimp simp:corres_underlying_def)
apply (wp wp, simp, rule evalMonad_wp)
apply (simp add:wp)+
done
lemma dcorres_store_word_offs_spec:
"\<lbrakk>within_page buf (base + of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow>
@ -1477,19 +1476,19 @@ lemma get_ipc_buffer_words_receive_slots:
in is_aligned_weaken[OF is_aligned_after_mask])
apply (case_tac sz,simp_all add:msg_align_bits)
apply (simp add:mask_add_aligned)
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms)
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric])
apply (subst evalMonad_compose)
apply (simp add:empty_when_fail_loadWord weak_det_spec_loadWord)+
using loadWord_functional[unfolded functional_def,simplified]
apply fastforce
apply (simp add:evalMonad_loadWord word_size_def mask_add_aligned)
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms)
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric])
apply (subst evalMonad_compose)
apply (simp add:empty_when_fail_loadWord weak_det_spec_loadWord)+
using loadWord_functional[unfolded functional_def,simplified]
apply fastforce
apply (simp add:evalMonad_loadWord word_size_def mask_add_aligned)
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms)
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric])
done
(* FIXME: MOVE *)
@ -1705,54 +1704,51 @@ lemma dcorres_lookup_extra_caps:
(Ipc_A.lookup_extra_caps thread buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))"
apply (clarsimp simp:lookup_extra_caps_def liftE_bindE Endpoint_D.lookup_extra_caps_def)
apply (rule corres_symb_exec_r)
apply (rule_tac F = "evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv"
in corres_gen_asm2)
apply (rule corres_mapME[where S = "{(x,y). x = of_bl y \<and> length y = word_bits}"])
prefer 3
apply (rule_tac F = "evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv"
in corres_gen_asm2)
apply (rule corres_mapME[where S = "{(x,y). x = of_bl y \<and> length y = word_bits}"])
prefer 3
apply simp
apply (erule conjE)
apply (drule_tac t="of_bl y" in sym, simp)
apply (rule dcorres_lookup_cap_and_slot[simplified])
apply (clarsimp simp:transform_cap_list_def)+
apply wp
apply simp
apply (case_tac buffer)
apply clarsimp
apply (simp add:transform_full_intent_def Let_def)
apply (rule get_ipc_buffer_words_empty)
apply (simp add:obj_at_def)
apply (erule get_tcb_SomeD)
apply simp
apply (rule dcorres_lookup_cap_and_slot[simplified])
apply (clarsimp simp:transform_cap_list_def)+
apply wp
apply simp
apply (case_tac buffer)
apply clarsimp
apply (simp add:transform_full_intent_def Let_def)
apply (rule get_ipc_buffer_words_empty)
apply (simp add:obj_at_def)
apply (erule get_tcb_SomeD)
apply simp
apply clarify
apply (subst evalMonad_get_extra_cptrs)
apply simp+
apply (case_tac buffer)
apply simp+
apply (case_tac buffer)
apply clarsimp
apply clarify
apply (drule evalMonad_get_extra_cptrs)
apply (simp del:get_extra_cptrs.simps
add: zip_map_eqv[where g = "\<lambda>x. x",simplified])+
apply (simp add: word_bits_def del:get_extra_cptrs.simps)
apply (wp evalMonad_wp)
apply (case_tac buffer)
apply (simp add:get_extra_cptrs_def empty_when_fail_simps)+
apply (simp add:liftM_def)
apply (rule empty_when_fail_compose)
apply (simp add:empty_when_fail_simps)+
apply (rule empty_when_fail_mapM)
apply (simp add:weak_det_spec_load_word_offs empty_when_fail_load_word_offs)
apply (rule weak_det_spec_mapM)
apply (simp add:weak_det_spec_load_word_offs)
apply (case_tac buffer)
apply (simp add:get_extra_cptrs_def weak_det_spec_simps)+
apply clarify
apply (drule evalMonad_get_extra_cptrs)
apply (simp del:get_extra_cptrs.simps add: zip_map_eqv[where g = "\<lambda>x. x",simplified])+
apply (simp add: word_bits_def del:get_extra_cptrs.simps)
apply (wp evalMonad_wp)
apply (case_tac buffer)
apply (simp add:get_extra_cptrs_def empty_when_fail_simps)+
apply (simp add:liftM_def)
apply (rule empty_when_fail_compose)
apply (simp add:empty_when_fail_simps)+
apply (rule empty_when_fail_mapM)
apply (simp add:weak_det_spec_load_word_offs empty_when_fail_load_word_offs)
apply (rule weak_det_spec_mapM)
apply (simp add:weak_det_spec_load_word_offs)
apply (case_tac buffer)
apply (simp add:get_extra_cptrs_def weak_det_spec_simps)+
apply (simp add:liftM_def)
apply (rule weak_det_spec_compose)
apply (simp add:weak_det_spec_simps)
apply (simp add:weak_det_spec_simps)
apply (rule weak_det_spec_mapM)
apply (simp add:weak_det_spec_load_word_offs)
apply (clarsimp simp:valid_state_def valid_pspace_def cur_tcb_def)+
apply (wp|clarsimp)+
done
apply (clarsimp simp:valid_state_def valid_pspace_def cur_tcb_def)+
apply (wp|clarsimp)+
done
lemma dcorres_copy_mrs':
notes hoare_post_taut[wp] if_cong[cong]
@ -2680,7 +2676,7 @@ lemma send_sync_ipc_corres:
apply (rename_tac list)
apply (drule_tac s = "set list" in sym)
apply (clarsimp simp: bind_assoc neq_Nil_conv split del:if_split)
apply (rule_tac P1="\<top>" and P'="(=) s'a" and x1 = y
apply (rule_tac P1="\<top>" and P'="(=) s'" and x1 = y
in dcorres_absorb_pfx[OF select_pick_corres[OF dcorres_expand_pfx]])
defer
apply (simp+)[3]

12
proof/drefine/KHeap_DR.thy
View File

@ -270,6 +270,7 @@ lemma nat_to_bl_dest:
lemma bl_to_bin_tcb_cnode_index_le0:
"n < 8 \<Longrightarrow> (bl_to_bin (tcb_cnode_index n) \<le> 0) = (n = 0)"
including no_take_bit
by (simp add: tcb_cnode_index_def uint_nat unat_of_nat)
lemma nat_bl_to_bin_lt2p: "nat(bl_to_bin b) < 2 ^ length b"
@ -3095,7 +3096,7 @@ lemma branch_map_simp2:
apply (drule min.absorb2[where b = nata])
apply simp
apply (clarsimp simp: add.commute)
apply (simp add:unat_def)
apply (simp only: unat_def)
apply (rule iffD2[OF eq_nat_nat_iff])
apply (simp add:bl_to_bin_ge0 )+
apply (subst bl_to_bin_rep_F[symmetric])
@ -3177,8 +3178,9 @@ lemma resolve_address_bits_terminate_corres:
apply clarsimp
apply (rule_tac Q="\<lambda>x y. y = (transform s) \<and> x = (transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun))" in corres_symb_exec_l)
apply (rule dcorres_expand_pfx)
apply (simp add: unat_def split: nat.splits)
apply (simp split: nat.splits)
apply (clarsimp simp: returnOk_def return_def corres_underlying_def transform_cslot_ptr_def)
apply (simp only: unat_def)
apply (subst eq_nat_nat_iff)
apply (simp add:bl_to_bin_ge0)+
apply (subst to_bl_bin[symmetric])
@ -3287,7 +3289,7 @@ proof (induct n arbitrary: cref cap' cap)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits)
apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits)
apply (rename_tac word list nat "fun")
apply (rename_tac word nat list "fun")
apply (rule corres_guard_imp)
apply (rule_tac radix_bits = nat and guard = list and s = s' in resolve_address_bits_error_corres[where ref="[]",simplified])
apply ((simp add:transform_cap_def in_terminate_branch_def in_recursive_branch_def valid_cap_def obj_at_def is_cap_table_def)+)[10]
@ -3313,7 +3315,7 @@ next
apply (case_tac "\<not> in_recursive_branch cref cap'")
apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits)
apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits)
apply (rename_tac word list nat "fun")
apply (rename_tac word nat list "fun")
apply (rule corres_guard_imp)
apply (rule_tac s=s' and radix_bits = nat and guard = list in resolve_address_bits_error_corres)
apply (simp_all | rule conjI)+
@ -3323,7 +3325,7 @@ next
apply (subst KHeap_DR.resolve_address_bits.simps,subst resolve_address_bits_recursive_branch)
apply (clarsimp simp:cap_type_simps is_cap_simps)+
apply fastforce
apply (rename_tac word list nat "fun")
apply (rename_tac word nat list "fun")
apply (simp add:cap_type_simps)
apply (simp add:in_recursive_branch_def in_terminate_branch_def unlessE_def branch_map_simp1)
apply (clarsimp simp:get_cnode_def bind_assoc liftE_bindE)

1
proof/drefine/Schedule_DR.thy
View File

@ -404,7 +404,6 @@ lemma schedule_choose_new_thread_dcorres:
apply (wp hoare_drop_imp| simp | clarsimp simp: valid_sched_def)+
apply (frule max_set_not_empty, fastforce)
apply (wp hoare_drop_imp| simp)+
apply (clarsimp simp: valid_sched_def)
(* dom_t = 0 *)
apply (simp only: schedule_def_2)
apply (rule corres_guard_imp)

7
proof/drefine/StateTranslation_D.thy
View File

@ -453,7 +453,8 @@ lemma transform_intent_isnot_UntypedIntent:
apply(unfold transform_intent_untyped_retype_def)
apply (clarsimp split: list.split, safe, simp_all)[1]
apply (clarsimp simp: transform_type_def)
apply (simp add: linorder_not_less eval_nat_numeral le_Suc_eq unat_arith_simps)
apply (simp add: unat_arith_simps)
apply (simp add: eval_nat_numeral linorder_not_less le_Suc_eq)
apply(erule disjE)
apply(auto simp: transform_intent_def option_map_def
split: gen_invocation_labels.split invocation_label.split arch_invocation_label.split
@ -663,9 +664,7 @@ where
Some $ bin_to_bl bits (of_nat n)"
lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)"
apply (clarsimp simp: nat_to_bl_def to_bl_def)
apply (auto simp: uint_nat le_def word_size)
done
by (clarsimp simp: nat_to_bl_def to_bl_def le_def word_size)
(* FIXME: MOVE *)
definition

2
proof/drefine/Syscall_DR.thy
View File

@ -1393,6 +1393,7 @@ lemma handle_recv_corres:
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[OF _ get_cur_thread_corres])
apply (simp add:liftM_def select_f_get_register get_thread_def bind_assoc)
apply (rename_tac thread)
apply (rule_tac P=\<top> and P'="invs and valid_etcbs and (\<lambda>s. thread = cur_thread s
\<and> not_idle_thread thread s \<and> st_tcb_at active thread s)"
in dcorres_gets_the)
@ -1485,6 +1486,7 @@ lemma handle_reply_corres:
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated [OF _ get_cur_thread_corres])
apply simp
apply (rename_tac thread)
apply (rule_tac R="\<lambda>_. \<top>" and
R'="\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread
and not_idle_thread thread

22
proof/drefine/Untyped_DR.thy
View File

@ -668,7 +668,7 @@ lemma clearMemory_unused_corres_noop:
apply (simp add: within_page_def)
apply simp
apply (clarsimp simp: obj_at_def)
apply (subgoal_tac "y && ~~ mask (obj_bits_api ty us) = p")
apply (subgoal_tac "x && ~~ mask (obj_bits_api ty us) = p")
apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def ran_null_filter
split: cap.split_asm arch_cap.split_asm)
apply (cut_tac t="(t, tcb_cnode_index 4)" and P="(=) cap" for t cap
@ -943,7 +943,7 @@ lemma retype_transform_ref_subseteq_strong:
apply (clarsimp simp:range_cover_def)
apply (erule aligned_add_aligned[OF _ is_aligned_mult_triv2])
apply (simp add:range_cover_def)+
done
by (metis is_aligned_add is_aligned_mult_triv2 is_aligned_no_overflow_mask mask_2pm1)
qed
lemma generate_object_ids_exec:
@ -1271,6 +1271,7 @@ lemma reset_untyped_cap_corres:
and (\<lambda>s. descendants_of cref (cdt s) = {}))
(Untyped_D.reset_untyped_cap (transform_cslot_ptr cref))
(Retype_A.reset_untyped_cap cref)"
including no_take_bit
supply if_cong[cong]
apply (rule dcorres_expand_pfx)
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps)
@ -1284,7 +1285,8 @@ lemma reset_untyped_cap_corres:
apply (simp add: whenE_def if_flip split del: if_split)
apply (rule corres_if)
apply (clarsimp simp: is_cap_simps free_range_of_untyped_def
cap_aligned_def free_index_of_def)
cap_aligned_def free_index_of_def
simp del: word_of_nat_eq_0_iff)
apply (simp add: word_unat.Rep_inject[symmetric])
apply (subst unat_of_nat_eq, erule order_le_less_trans,
rule power_strict_increasing, simp_all add: word_bits_def bits_of_def)[1]
@ -1634,6 +1636,7 @@ lemma corres_whenE_throwError_split_rhs:
\<and> (\<not> G \<longrightarrow> corres_underlying sr nf nf' r P Q a b))"
by (simp add: whenE_bindE_throwError_to_if)
lemma nat_bl_to_bin_nat_to_cref:
assumes asms: "x < 2 ^ bits" "bits < word_bits"
shows "nat (bl_to_bin (nat_to_cref bits x)) = x"
@ -1651,11 +1654,8 @@ proof -
apply (insert asms word_bits_conv, simp)
done
show ?thesis using of_bl lt_bl lt_x
apply (simp add: of_bl_def word_of_nat)
apply (drule word_uint.Abs_eqD)
apply (simp add: uints_num bl_to_bin_ge0)
apply (simp add: uints_num)
apply simp
apply (simp add: of_bl_def)
apply (erule word_of_int_word_of_nat_eqD; simp add: bl_to_bin_ge0)
done
qed
@ -1717,7 +1717,7 @@ lemma descendants_of_empty_lift :
done
lemma alignUp_gt_0:
"\<lbrakk>is_aligned (x :: 'a :: len word) n; n < len_of TYPE('a); x \<noteq> 0 ; a \<le> x\<rbrakk> \<Longrightarrow> (0 < Word_Lib.alignUp a n) = (a \<noteq> 0)"
"\<lbrakk>is_aligned (x :: 'a :: len word) n; n < len_of TYPE('a); x \<noteq> 0 ; a \<le> x\<rbrakk> \<Longrightarrow> (0 < alignUp a n) = (a \<noteq> 0)"
apply (rule iffI)
apply (rule ccontr)
apply (clarsimp simp:not_less alignUp_def2 mask_def)
@ -1833,10 +1833,10 @@ lemma decode_untyped_corres:
apply (rule corres_guard_imp)
apply (rule_tac F="cap_aligned cnode_cap' \<and> is_cnode_cap cnode_cap'" in corres_gen_asm2)
apply (subgoal_tac "map (Pair (cap_object (transform_cap cnode_cap')))
[unat w4 ..< unat w4 + unat w5]
[unat w3 ..< unat w3 + unat w4]
= map (\<lambda>x. transform_cslot_ptr (obj_ref_of (cnode_cap'),
(nat_to_cref (bits_of cnode_cap') x)))
[unat w4 ..< unat w4 + unat w5]")
[unat w3 ..< unat w3 + unat w4]")
apply (simp del: map_eq_conv)
apply (simp add: mapME_x_map_simp)
apply (rule mapME_x_corres_inv)