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

arch_splitting, fixing sorries, some more invariants

This commit is contained in:
Miki Tanaka 2017-02-27 20:27:16 +11:00 committed by Alejandro Gomez-Londono
parent d3a226b867
commit eb0ec4dcd0
19 changed files with 460 additions and 330 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -367,7 +367,7 @@ lemma vspace_objs':
"valid_vspace_objs s \<Longrightarrow> valid_vspace_objs s'"
using ko
apply (clarsimp simp: valid_vspace_objs_def vs_lookup')
(* apply (fastforce simp: obj_at_def)*)
(* apply (fastforce simp: obj_at_def split: arch_kernel_obj.splits) *)
sorry
lemma caps_of_state_s':
@ -646,7 +646,7 @@ lemma cap_insert_ap_invs:
apply (auto simp: obj_at_def is_tcb_def is_cap_table_def a_type_def
valid_cap_def [where c="cap.Zombie a b x" for a b x]
dest: obj_ref_is_tcb obj_ref_is_cap_table split: option.splits)
(* apply (clarsimp simp: obj_at_def a_type_def)*)
(* apply (fastforce simp: obj_at_def a_type_def)*)
sorry
@ -1035,7 +1035,6 @@ lemma shiftr_irrelevant:
apply simp
done
lemma create_mapping_entries_parent_for_refs:
"\<lbrace>invs and \<exists>\<rhd> pd and page_directory_at pd
and K (is_aligned pd pd_bits) and K (vmsz_aligned vptr pgsz)
@ -1044,7 +1043,7 @@ lemma create_mapping_entries_parent_for_refs:
rights attribs pd
\<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -"
apply (rule hoare_gen_asmE)+
apply (cases pgsz, simp_all add: vmsz_aligned_def)
apply (cases pgsz, simp_all add: vmsz_aligned_def largePagePTE_offsets_def superSectionPDE_offsets_def)
apply (rule hoare_pre)
apply wp
apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to)
@ -1055,22 +1054,28 @@ lemma create_mapping_entries_parent_for_refs:
apply wp
apply (rule hoare_post_imp_R)
apply (rule lookup_pt_slot_cap_to_multiple1)
apply (simp only: add.commute)
apply (elim conjE exEI cte_wp_at_weakenE)
apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
subset_iff p_0x3C_shift vspace_bits_defs largePagePTE_offsets_def
split: ARM_A.arch_cap.splits)
(* apply (rule hoare_pre, wp)
apply_trace (simp add: pte_bits_def del: set_map cap_asid_simps not_None_eq)
apply_trace (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
subset_iff p_0x3C_shift
simp del: cap_asid_simps set_map del: imageE)
apply (erule_tac x=t in allE)
apply (subgoal_tac "map (op + r) [0 , 8 .e. 0x78] = [r , r + 8 .e. r + 0x78]", simp)
defer
apply simp
apply (rule hoare_pre, wp)
apply (clarsimp dest!:vs_lookup_pages_vs_lookupI)
apply (drule valid_vs_lookupD, clarsimp)
apply (simp, elim exEI)
apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
lookup_pd_slot_def Let_def)
apply (subst pd_shifting, simp add: pd_bits_def pageBits_def)
apply (clarsimp simp: vs_cap_ref_def
apply (subst pd_shifting, simp add: vspace_bits_defs)
apply (clarsimp simp: vs_cap_ref_def simp del: cap_asid_simps
split: cap.split_asm arch_cap.split_asm option.split_asm)
apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def
dest!: caps_of_state_valid_cap)[3]
apply (frule(1) caps_of_state_valid)
(* apply (frule(1) caps_of_state_valid)
apply (clarsimp simp:valid_cap_def obj_at_def)
apply (simp add:is_cap_simps)
apply (rule hoare_pre, wp)

16
proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy
View File

@ -280,8 +280,8 @@ lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
valid_asid_map_def
pspace_in_kernel_window_def cap_refs_in_kernel_window_def
cur_tcb_def sym_refs_def state_refs_of_def state_hyp_refs_of_def vspace_at_asid_def
swp_def valid_irq_states_def)
sorry
swp_def valid_irq_states_def split: option.splits)
done
lemma cte_at_nat_to_cref_zbits [CNodeInv_AI_assms]:
@ -523,9 +523,10 @@ lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: arch_finalise_cap_def)
apply (wp
| clarsimp simp: valid_cap_def split: option.split bool.split
| clarsimp simp: valid_cap_def obj_at_def is_tcb_def is_cap_table_def
split: option.splits bool.split
| intro impI conjI)+
sorry (* add vcpu case *)
done
crunch emptyable[wp, CNodeInv_AI_assms]: finalise_cap "emptyable sl"
@ -689,7 +690,7 @@ next
apply (clarsimp simp add: invs_def valid_state_def
invs_valid_objs invs_psp_aligned)
apply (drule(1) if_unsafe_then_capD, clarsimp+)
sorry
done
next
have replicate_helper:
"\<And>x n. True \<in> set x \<Longrightarrow> replicate n False \<noteq> x"
@ -1010,7 +1011,7 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
| simp del: split_paired_Ex split_paired_All
| simp add: valid_irq_node_def valid_machine_state_def
del: split_paired_All split_paired_Ex)+
(* apply (clarsimp simp: tcb_cap_valid_def cte_wp_at_caps_of_state)
apply (clarsimp simp: tcb_cap_valid_def cte_wp_at_caps_of_state)
apply (frule(1) valid_global_refsD2[where ptr=ptr])
apply (frule(1) cap_refs_in_kernel_windowD[where ptr=ptr])
apply (frule weak_derived_cap_range)
@ -1019,11 +1020,12 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
apply (simp add: is_cap_simps)
apply (subgoal_tac "tcb_cap_valid cap.NullCap ptr s")
apply (simp add: tcb_cap_valid_def)
defer
apply (rule tcb_cap_valid_NullCapD)
apply (erule(1) tcb_cap_valid_caps_of_stateD)
apply (simp add: is_cap_simps)
apply (clarsimp simp: cte_wp_at_caps_of_state)
done *)sorry (* hyp_ref *)
sorry
end

243
proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
View File

@ -48,14 +48,14 @@ lemma vs_lookup_pages_eq:
"\<lbrakk>valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s;
valid_cap cap s; table_cap_ref cap = Some vref; oref \<in> obj_refs cap\<rbrakk>
\<Longrightarrow> (vref \<unrhd> oref) s = (vref \<rhd> oref) s"
apply (clarsimp simp: table_cap_ref_def
apply (clarsimp simp: table_cap_ref_def arch_cap_fun_lift_def
vs_lookup_pages_eq_at[symmetric, THEN fun_cong]
vs_lookup_pages_eq_ap[symmetric, THEN fun_cong]
split: cap.splits arch_cap.splits option.splits)
apply (rule iffI[rotated, OF vs_lookup_pages_vs_lookupI], assumption)
apply (simp add: valid_cap_def)
apply (erule vs_lookup_vs_lookup_pagesI', clarsimp+)
sorry
done
lemma nat_to_cref_unat_of_bl':
"\<lbrakk> length xs < 32; n = length xs \<rbrakk> \<Longrightarrow>
@ -269,7 +269,72 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]:
apply (simp add: empty_slot_def set_cdt_def bind_assoc cong: if_cong)
apply (wp opt_deleted_irq_handler_invs)
apply (simp add: invs_def valid_state_def valid_mdb_def2)
sorry
apply (wp replace_cap_valid_pspace set_cap_caps_of_state2
replace_cap_ifunsafe get_cap_wp
set_cap_idle valid_irq_node_typ set_cap_typ_at
set_cap_irq_handlers set_cap_valid_arch_caps
set_cap_cap_refs_respects_device_region_NullCap
| simp add: trans_state_update[symmetric] del: trans_state_update fun_upd_apply split del: split_if )+
apply (clarsimp simp: is_final_cap'_def2 simp del: fun_upd_apply)
apply (clarsimp simp: conj_comms invs_def valid_state_def valid_mdb_def2)
apply (subgoal_tac "mdb_empty_abs s")
prefer 2
apply (rule mdb_empty_abs.intro)
apply (rule vmdb_abs.intro)
apply (simp add: valid_mdb_def swp_def cte_wp_at_caps_of_state conj_comms)
apply (clarsimp simp: untyped_mdb_def mdb_empty_abs.descendants mdb_empty_abs.no_mloop_n
valid_pspace_def cap_range_def)
apply (clarsimp simp: untyped_inc_def mdb_empty_abs.descendants mdb_empty_abs.no_mloop_n)
apply (simp add: ut_revocable_def cur_tcb_def valid_irq_node_def
no_cap_to_obj_with_diff_ref_Null)
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_cte_at)
apply (rule conjI)
apply (clarsimp simp: irq_revocable_def)
apply (rule conjI)
apply (clarsimp simp: reply_master_revocable_def)
apply (thin_tac "\<forall>irq. irqopt = Some irq \<longrightarrow> P irq" for P)
apply (rule conjI)
apply (clarsimp simp: valid_machine_state_def)
apply (rule conjI)
apply (clarsimp simp:descendants_inc_def mdb_empty_abs.descendants)
apply (rule conjI)
apply (clarsimp simp: reply_mdb_def)
apply (rule conjI)
apply (unfold reply_caps_mdb_def)[1]
apply (rule allEI, assumption)
apply (fold reply_caps_mdb_def)[1]
apply (case_tac "sl = ptr", simp)
apply (simp add: fun_upd_def split del: split_if del: split_paired_Ex)
apply (erule allEI, rule impI, erule(1) impE)
apply (erule exEI)
apply (simp, rule ccontr)
apply (erule(5) emptyable_no_reply_cap)
apply simp
apply (unfold reply_masters_mdb_def)[1]
apply (elim allEI)
apply (clarsimp simp: mdb_empty_abs.descendants)
apply (rule conjI)
apply (simp add: valid_ioc_def)
apply (rule conjI)
apply (clarsimp simp: tcb_cap_valid_def
dest!: emptyable_valid_NullCapD)
apply (rule conjI)
apply (clarsimp simp: mdb_cte_at_def cte_wp_at_caps_of_state)
apply (cases sl)
apply (rule conjI, clarsimp)
apply (subgoal_tac "cdt s \<Turnstile> (ab,bb) \<rightarrow> (ab,bb)")
apply (simp add: no_mloop_def)
apply (rule r_into_trancl)
apply (simp add: cdt_parent_of_def)
apply fastforce
apply (clarsimp simp: cte_wp_at_caps_of_state replaceable_def
vs_cap_ref_simps table_cap_ref_simps
del: allI)
apply (case_tac "is_final_cap' cap s")
apply auto[1]
apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state)
done
lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]:
"dom tcb_cap_cases = {xs. length xs = 3 \<and> unat (of_bl xs :: machine_word) < 5}"
@ -299,6 +364,35 @@ lemma deleting_irq_handler_final [Finalise_AI_asms]:
apply simp
done
lemma arch_thread_set_final_cap[wp]:
"\<lbrace>is_final_cap' cap\<rbrace> arch_thread_set v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
apply (simp add: arch_thread_set_def is_final_cap'_def2 cte_wp_at_caps_of_state)
apply wp
apply (simp add: set_object_def, wp)
apply (case_tac "get_tcb t s"; simp)
apply (clarsimp simp add: split: option.splits)
sorry
lemma arch_thread_get_final_cap[wp]:
"\<lbrace>is_final_cap' cap\<rbrace> arch_thread_get v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
apply (simp add: arch_thread_get_def is_final_cap'_def2 cte_wp_at_caps_of_state, wp)
apply auto
done
lemma dissociate_vcpu_tcb_final_cap[wp]:
"\<lbrace>is_final_cap' cap\<rbrace> dissociate_vcpu_tcb v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
apply (simp add: dissociate_vcpu_tcb_def)
apply wp
sorry
lemma prepare_thread_delete_final[wp]:
"\<lbrace>is_final_cap' cap\<rbrace> prepare_thread_delete t \<lbrace> \<lambda>rv. is_final_cap' cap\<rbrace>"
unfolding prepare_thread_delete_def
apply (wp hoare_drop_imps
| wpc | clarsimp simp add: tcb_cap_cases_def)+
done
lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
"\<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s
\<and> cte_wp_at (op = cap) slot s\<rbrace>
@ -325,10 +419,10 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
appropriate_cte_cap_def
vs_cap_ref_def
| intro impI TrueI ext conjI)+
(* apply (simp add: arch_finalise_cap_def)
apply (simp add: arch_finalise_cap_def)
apply (rule hoare_pre)
apply (wp | wpc | simp only: simp_thms)+ *)
sorry
apply (wp | wpc | simp only: simp_thms)+
done
crunch typ_at_arch [wp]: arch_thread_set "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps set_object_typ_at)
@ -482,12 +576,33 @@ lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]:
dest!: obj_ref_none_no_asid[rule_format])
done
lemma dissociate_vcpu_tcb_no_cap_to_obj_ref[wp]:
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
dissociate_vcpu_tcb v t
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
unfolding dissociate_vcpu_tcb_def
apply wp
sorry
lemma prepare_thread_delete_no_cap_to_obj_ref[wp]:
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
prepare_thread_delete t
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
unfolding prepare_thread_delete_def
apply (wp hoare_drop_imp hoare_vcg_all_lift | wpc)+
apply auto
sorry
lemma prepare_thread_delete_unlive[wp]:
"\<lbrace>\<lambda>_. True\<rbrace> prepare_thread_delete ptr \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ptr\<rbrace>"
sorry
lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
"\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
\<and> cte_wp_at (op = cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
\<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)
\<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and>
valid_arch_objs s \<and>
valid_vspace_objs s \<and>
valid_arch_state s)\<rbrace>
finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>"
@ -499,6 +614,7 @@ lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
apply (rule hoare_pre)
apply ((wp suspend_unlive[unfolded o_def]
suspend_final_cap[where sl=sl]
prepare_thread_delete_unlive[unfolded o_def]
unbind_maybe_notification_not_bound
get_ntfn_ko
unbind_notification_valid_objs
@ -526,13 +642,13 @@ lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
| wpc
| simp add: valid_cap_simps is_nondevice_page_cap_simps)+)
apply (rule hoare_chain)
(* apply (rule arch_finalise_cap_replaceable[where sl=sl])
apply (rule arch_finalise_cap_replaceable[where sl=sl])
apply (clarsimp simp: replaceable_def reachable_pg_cap_def
o_def cap_range_def valid_arch_state_def
ran_tcb_cap_cases is_cap_simps
obj_irq_refs_subset vs_cap_ref_def)+
apply (fastforce split: option.splits vmpage_size.splits) *)
sorry
apply (fastforce split: option.splits vmpage_size.splits)
done
lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]:
assumes x: "\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap"
@ -544,9 +660,11 @@ lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]:
crunch cte_wp_at[wp,Finalise_AI_asms]: dissociate_vcpu_tcb "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
crunch cte_wp_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
crunch cte_wp_at[wp,Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
crunch cte_wp_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
end
interpretation Finalise_AI_1?: Finalise_AI_1
@ -599,9 +717,12 @@ context Arch begin global_naming ARM
crunch irq_node[wp]: vcpu_switch "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps select_wp simp: crunch_simps)
crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps select_wp simp: crunch_simps)
crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
(simp: crunch_simps wp: crunch_wps)
crunch pred_tcb_at[wp]: arch_finalise_cap "pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps)
@ -611,18 +732,18 @@ lemma tcb_cap_valid_pagetable:
= tcb_cap_valid (ArchObjectCap (PageTableCap word None)) slot"
apply (rule ext)
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_nondevice_page_cap_arch_def
is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_arch_def
is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
split: Structures_A.thread_state.split)
sorry
done
lemma tcb_cap_valid_pagedirectory:
"tcb_cap_valid (ArchObjectCap (PageDirectoryCap word (Some v))) slot
= tcb_cap_valid (ArchObjectCap (PageDirectoryCap word None)) slot"
apply (rule ext)
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_nondevice_page_cap_arch_def
is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_arch_def
is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
split: Structures_A.thread_state.split)
sorry
done
lemma store_pde_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table {}) word s\<rbrace>
@ -636,6 +757,9 @@ lemma store_pde_unmap_empty:
crunch empty[wp]: find_free_hw_asid, store_hw_asid, load_hw_asid, set_vm_root_for_flush, page_table_mapped, invalidate_tlb_by_asid
"\<lambda>s. obj_at (empty_table {}) word s"
crunch empty[wp]: vcpu_switch
"\<lambda>s. obj_at (empty_table {}) word s"
lemma store_pte_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table {}) word s\<rbrace>
store_pte xa InvalidPTE
@ -663,12 +787,12 @@ lemma flush_table_empty:
flush_table ac aa b word
\<lbrace>\<lambda>rv s. obj_at (empty_table {}) word s\<rbrace>"
apply (clarsimp simp: flush_table_def set_vm_root_def)
apply (wp do_machine_op_obj_at arm_context_switch_empty hoare_whenE_wp
apply (wp do_machine_op_obj_at arm_context_switch_empty hoare_whenE_wp hoare_drop_imp
| wpc
| simp
| wps)+
apply (rename_tac pd x y)
(* apply (rule_tac Q="\<lambda>pd' s.
apply (rule_tac Q="\<lambda>pd' s.
(if pd \<noteq> pd'
then (\<lambda>s. obj_at
(empty_table {}) word
@ -688,8 +812,8 @@ lemma flush_table_empty:
| wpc
| rule_tac
Q="\<lambda>_ s. obj_at (empty_table {}) word s"
in hoare_strengthen_post)+ *)
sorry
in hoare_strengthen_post)+
done
lemma unmap_page_table_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table {}) word s\<rbrace>
@ -699,15 +823,15 @@ lemma unmap_page_table_empty:
apply (wp store_pde_unmap_empty flush_table_empty page_table_mapped_empty | simp | wpc)+
done
lemma mapM_x_store_pte_valid_arch_objs:
lemma mapM_x_store_pte_valid_vspace_objs:
"\<lbrace>invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and>
(\<forall>x \<in> set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap)) \<rbrace>
mapM_x (\<lambda>p. store_pte p InvalidPTE) pteptrs
\<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
\<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
apply (rule hoare_strengthen_post)
apply (wp mapM_x_wp')
apply (fastforce simp: is_pt_cap_def)+
sorry
done
lemma mapM_x_swp_store_empty_table_set:
"\<lbrace>page_table_at p
@ -719,8 +843,9 @@ lemma mapM_x_swp_store_empty_table_set:
apply (rule hoare_strengthen_post)
apply (rule mapM_x_swp_store_empty_table)
apply (clarsimp simp: obj_at_def empty_table_def)
apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits)
sorry
apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits option.splits)
apply (clarsimp simp add: valid_pde_mappings_def pde_ref_def)
done
definition
replaceable_or_arch_update
@ -872,19 +997,13 @@ lemma delete_asid_empty_table_pd:
\<and> obj_at (empty_table {}) word s\<rbrace>
delete_asid a word
\<lbrace>\<lambda>_ s. obj_at (empty_table {}) word s\<rbrace>"
(* apply (simp add: delete_asid_def)
apply (simp add: delete_asid_def)
apply (wp | wpc)+
apply wps
apply wp
apply (simp add: set_asid_pool_def)
apply wp
apply (case_tac "x2 = word")
defer
apply wps
apply (rule set_object_at_obj)
apply (wp get_object_ret | wps)+
apply (clarsimp simp: obj_at_def empty_table_def)+*)
sorry
apply (clarsimp simp: obj_at_def empty_table_def)+
done
lemma page_directory_at_def2:
"page_directory_at p s = (\<exists>pd. ko_at (ArchObj (PageDirectory pd)) p s)"
@ -933,40 +1052,23 @@ lemma obj_at_empty_tableI:
\<Longrightarrow> obj_at (empty_table {}) p s"
apply safe
apply (simp add: obj_at_def empty_table_def pde_wp_at_def)
(* (* Boring cases *)
(* Boring cases *)
apply (case_tac "\<exists>ko. kheap s p = Some ko")
apply (erule exE) apply (rule_tac x=ko in exI)
apply (rule conjI)
apply assumption
apply (case_tac ko)
apply ((erule_tac x="ucast (kernel_base >> 21) - 1" in allE,
simp add: kernel_base_def kernel_mapping_slots_def)+)[4]
simp add: kernel_base_def)+)[4]
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj) defer 3
apply ((erule_tac x="ucast (kernel_base >> 21) - 1" in allE,
simp add: kernel_base_def kernel_mapping_slots_def)+)[4]
simp add: kernel_base_def)+)[5]
(* Interesting case *)
apply (rename_tac "fun")
apply clarsimp
apply (erule_tac x=x in allE)
apply (case_tac "x \<notin> kernel_mapping_slots")
apply (simp add:valid_pde_mappings_def pde_ref_def)
apply simp
apply (rule conjI)
apply (simp add: invs_def valid_state_def valid_kernel_mappings_def
valid_kernel_mappings_if_pd_def)
apply (erule conjE)+
apply (erule_tac x="ArchObj (PageDirectory fun)" in ballE)
apply simp
apply (simp add: ran_def)
apply (clarsimp simp: invs_def valid_state_def valid_arch_state_def
equal_kernel_mappings_def
obj_at_def a_type_simps)
apply (erule_tac x=p in allE,
erule_tac x="arm_global_pd (arch_state s)" in allE)
apply (erule_tac x="fun" in allE, erule_tac x="pd" in allE)
apply (simp add: empty_table_def) *)
sorry
apply (clarsimp simp add: valid_pde_mappings_def pde_ref_def)
done
lemma pd_shifting_again3:
"is_aligned pd pd_bits \<Longrightarrow> ((ucast (ae :: 11 word) << 3) + (pd :: word32) && ~~ mask pd_bits) = pd"
@ -1027,23 +1129,24 @@ lemma mapM_x_store_pde_InvalidPDE_empty:
defer
apply (rule allI)
apply (erule_tac x="ucast x" in ballE)
(* apply (rule impI)
(* apply (rule impI)*)
apply (frule_tac pd="word" and ae="x" in pd_shifting_again3)
apply (frule_tac pd="word" and ae="x" in pd_shifting_again5)
apply ((simp add: kernel_mapping_slots_def kernel_base_def)+)[3]
apply (subst word_not_le)
apply ((simp add: kernel_base_def)+)[3]
(* apply (subst word_not_le) *)
apply (subst (asm) word_not_le)
apply (cut_tac x="ucast x" and y="kernel_base >> 20" in le_m1_iff_lt)
apply clarsimp
apply (cut_tac x="ucast x" and y="kernel_base >> 21" in le_m1_iff_lt)
apply (simp add: le_m1_iff_lt word_less_nat_alt unat_ucast)
apply (simp add: pde_ref_def)
apply (rule conjI, rule allI, rule impI)
(* apply (simp add: pde_ref_def) *)
(* apply (rule conjI, rule allI, rule impI)
apply (rule pd_shifting_kernel_mapping_slots)
apply simp+
apply (rule allI, rule impI)
apply simp+*)
(* apply (rule allI, rule impI)
apply (rule pd_shifting_global_refs)
apply simp+
apply (wp store_pde_pde_wp_at2)*)
apply (wp store_pde_pde_wp_at2) *)
sorry
lemma word_aligned_pt_slots:
@ -1188,11 +1291,11 @@ lemma replaceable_or_arch_update_pg:
apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps)
done
lemma store_pde_arch_objs_invalid: (* ARMHYP do we need this? *)
(*lemma store_pde_arch_objs_invalid: (* ARMHYP do we need this? *)
"\<lbrace>valid_arch_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
(* apply (wp store_pde_arch_objs_unmap)
apply (simp add: pde_ref_def) *)
sorry
apply (wp store_pde_arch_objs_unmap)
apply (simp add: pde_ref_def)
done *)
lemma store_pde_vspace_objs_invalid:
"\<lbrace>valid_vspace_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"

14
proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
View File

@ -347,6 +347,13 @@ lemmas
wellformed_arch_obj_simps[simp] =
wellformed_arch_obj_def[split_simps arch_kernel_obj.split]
lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>wellformed_arch_obj ao s; kheap s = kheap s'\<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao s'"
apply (case_tac ao, simp_all)
apply (simp add: obj_at_def valid_vcpu_def split: option.splits)
done
section "Virtual Memory"
definition (* ARMHYP *)
@ -1131,6 +1138,13 @@ by (rule kernel_object_exhaust[of ko]; clarsimp simp add: a_type_simps split: if
lemmas aa_type_elims[elim!] =
aa_type_AASIDPoolE aa_type_APageDirectoryE aa_type_APageTableE aa_type_ADeviceDataE aa_type_AUserDataE aa_type_AVCPUE
lemma wellformed_arch_typ:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. wellformed_arch_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. wellformed_arch_obj ao s\<rbrace>"
apply (cases ao; clarsimp simp: valid_vcpu_def split: option.splits; wp?)
apply (rule conjI; clarsimp; wp P)
done
lemma valid_arch_obj_pspaceI:
"\<lbrakk> valid_arch_obj obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_obj obj s'"
apply (cases obj, simp_all)

24
proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy
View File

@ -267,9 +267,9 @@ lemma as_user_getRestart_invs[wp]: "\<lbrace>P\<rbrace> as_user t getRestartPC \
lemma make_arch_fault_msg_invs[wp]: "\<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace>"
apply (cases f)
apply simp
apply simp_all
apply wp
sorry (* add ARMHYP specific cases *)
done
lemma make_fault_message_inv[wp, Ipc_AI_assms]:
"\<lbrace>P\<rbrace> make_fault_msg ft t \<lbrace>\<lambda>rv. P\<rbrace>"
@ -436,6 +436,21 @@ lemma do_ipc_transfer_tcb_caps [Ipc_AI_assms]:
crunch typ_at[Ipc_AI_assms]: handle_arch_fault_reply "P (typ_at T p s)"
lemma transfer_caps_loop_valid_vspace_objs[wp, Ipc_AI_assms]:
"\<lbrace>valid_vspace_objs\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
apply (induct caps arbitrary: slots n mi, simp)
apply (clarsimp simp: Let_def split_def whenE_def
cong: if_cong list.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
derive_cap_is_derived_foo
hoare_drop_imps
| assumption | simp split del: split_if)+
done
end
interpretation Ipc_AI?: Ipc_AI
@ -473,8 +488,11 @@ lemma do_ipc_transfer_respects_device_region[Ipc_AI_cont_assms]:
apply auto
done
crunch state_hyp_refs_of[wp]: set_mrs "\<lambda> s. P (state_hyp_refs_of s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: set_object transfer_caps_loop)
crunch state_hyp_refs_of[wp, Ipc_AI_cont_assms]: do_ipc_transfer "\<lambda> s. P (state_hyp_refs_of s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: transfer_caps_loop)
(wp: crunch_wps simp: zipWithM_x_mapM)
end

116
proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy
View File

@ -283,18 +283,6 @@ lemma vs_lookup_pages_vspace_obj_at_lift:
by (auto simp: vs_refs_pages.vspace_only
intro!: vspace_obj_pred_fI[where f=Ex])
(* ARMHYP not needed?
lemma valid_arch_objs_lift_weak:
assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow>
\<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
shows "\<lbrace>valid_arch_objs\<rbrace> f \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>" (* ARMHYP *)
apply (rule valid_arch_objs_lift)
apply (rule valid_vspace_objs_lift)
apply (rule vs_lookup_arch_obj_at_lift)
apply (rule obj_at arch_state; simp)+
apply (simp add: obj_at_def)
done *)
lemma valid_vspace_objs_lift_weak:
assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
@ -581,34 +569,6 @@ lemma valid_machine_state_lift:
apply simp
done
(*
lemma bool_pred_exhaust:
"(P = (\<lambda>x. x)) \<or> (P = (\<lambda>x. \<not>x)) \<or> (P = (\<lambda>_. True)) \<or> (P = (\<lambda>_. False))"
apply (cases "P True"; cases "P False")
apply (rule disjI2, rule disjI2, rule disjI1, rule ext)
defer
apply (rule disjI1, rule ext)
defer
apply (rule disjI2, rule disjI1, rule ext)
defer
apply (rule disjI2, rule disjI2, rule disjI2, rule ext)
apply (match conclusion in "P x = _" for x \<Rightarrow> \<open>cases x; fastforce\<close>)+
done
*)
(*
lemma valid_ao_at_lift:
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
unfolding valid_ao_at_def
by (wp hoare_vcg_ex_lift y valid_arch_obj_typ z)
lemma valid_ao_at_lift_aobj_at:
assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
unfolding valid_ao_at_def
by (wp hoare_vcg_ex_lift valid_arch_obj_typ aobj_at | clarsimp)+
*)
lemma valid_vso_at_lift:
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
@ -801,5 +761,81 @@ lemma cap_is_device_obj_is_device[simp]:
crunch device_state_inv: storeWord "\<lambda>ms. P (device_state ms)"
(* some hyp_ref invariants *)
lemma state_hyp_refs_of_ep_update: "\<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow>
state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s"
apply (rule all_ext)
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
done
lemma state_hyp_refs_of_ntfn_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
apply (rule all_ext)
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
done
lemma state_hyp_refs_of_tcb_bound_ntfn_update:
"kheap s t = Some (TCB tcb) \<Longrightarrow>
state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
= state_hyp_refs_of s"
apply (rule all_ext)
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
done
lemma state_hyp_refs_of_tcb_state_update:
"kheap s t = Some (TCB tcb) \<Longrightarrow>
state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
= state_hyp_refs_of s"
apply (rule all_ext)
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
done
lemma valid_arch_obj_same_type:
"\<lbrakk>valid_arch_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
\<Longrightarrow> valid_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
apply (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: valid_arch_obj.simps typ_at_same_type)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule valid_pte_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule valid_pde_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (simp add: valid_vcpu_def split: option.splits)
apply (drule typ_at_same_type[rotated]; assumption)
done
lemma valid_vcpu_lift:
assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
assumes t: "\<And>p. \<lbrace>typ_at ATCB p\<rbrace> f \<lbrace>\<lambda>rv. typ_at ATCB p\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_vcpu v s\<rbrace> f \<lbrace>\<lambda>rv s. valid_vcpu v s\<rbrace>"
apply (cases v)
apply (simp add: valid_vcpu_def | wp x hoare_vcg_disj_lift)+
apply (case_tac vcpu_tcb; simp, wp t)
done
lemma valid_vcpu_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
apply (rule all_ext)
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
done
lemma valid_vcpu_same_type:
"\<lbrakk> valid_vcpu v s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> valid_vcpu v (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
by (cases v; case_tac vcpu_tcb; clarsimp simp: valid_vcpu_def typ_at_same_type)
lemma wellformed_arch_obj_same_type:
"\<lbrakk> wellformed_arch_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
by (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: valid_arch_obj.simps typ_at_same_type valid_vcpu_same_type)
end
end

21
proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy
View File

@ -138,6 +138,8 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *)
apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps)
done
crunch caps_of_state[wp]: prepare_thread_delete "\<lambda>s. P (caps_of_state s)"
(wp: mapM_x_wp' crunch_wps)
lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
assumes x: "P cap.NullCap"
@ -145,15 +147,16 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
finalise_cap cap fin
\<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
apply (cases cap, simp_all)
apply (wp suspend_caps_of_state hoare_vcg_all_lift
apply (wp prepare_thread_delete_caps_of_state hoare_vcg_all_lift
suspend_caps_of_state
| simp
| rule impI
| rule hoare_drop_imps)+
apply (clarsimp simp: ball_ran_eq x)
(* apply (clarsimp simp: ball_ran_eq x)
apply (wp delete_one_caps_of_state
| rule impI
| simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+
sorry (* prepare_thread_delete *)
*) sorry
lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]:
@ -181,6 +184,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *)
apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+
done
declare arch_cap_fun_lift_simps [simp del]
lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
"\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace>
cap_delete slot
@ -191,9 +195,14 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp add: atomize_imp)
apply_trace (simp add: table_cap_ref_def[simplified, split_simps cap.split]
del: arch_cap_fun_lift_simps
| rule obj_ref_none_no_asid)+
vspace_bits_defs
del: arch_cap_fun_lift_non_arch
split del: arch_cap.split
cong: cap.case_cong_weak)+
(* apply (rule_tac obj_ref_none_no_asid) *)
sorry
lemma as_user_valid_cap[wp]:
@ -240,7 +249,7 @@ lemma tc_invs[Tcb_AI_asms]:
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
apply_trace ((simp only: simp_thms
| rule wp_split_const_if wp_split_const_if_R
hoare_vcg_all_lift_R
hoare_vcg_E_elim hoare_vcg_const_imp_lift_R

41
proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy
View File

@ -134,31 +134,26 @@ proof -
apply (erule range_cover.sz)
apply (simp add:range_cover_def)
apply (clarsimp simp:get_free_ref_def is_aligned_neg_mask_eq empty_descendants_range_in)
apply (rule conjI[rotated], blast, clarsimp)
apply (drule_tac x = "(obj_ref_of node_cap,nat_to_cref (bits_of node_cap) slota)" in bspec)
apply (clarsimp simp:is_cap_simps nat_to_cref_def word_bits_def
bits_of_def valid_cap_simps cap_aligned_def)+
(* apply (frule(1) range_cover_stuff[where sz = sz])
apply (simp add: free_index_of_def)
apply (frule(1) range_cover_stuff[where sz = sz])
apply (clarsimp dest!:valid_cap_aligned simp:cap_aligned_def word_bits_def)+
apply simp+
apply (clarsimp simp:get_free_ref_def) *)
(* apply (frule cte_wp_at_caps_descendants_range_inI
[where ptr = w and sz = sz and idx = 0 and cref = slot])
subgoal by (clarsimp simp:cte_wp_at_caps_of_state is_aligned_neg_mask_eq)
subgoal by simp
subgoal by (simp add:range_cover_def word_bits_def)
subgoal by (simp add:is_aligned_neg_mask_eq)
apply (clarsimp) *)
(* apply (erule disjE)
apply (clarsimp simp:get_free_ref_def)
apply (erule disjE)
apply (drule_tac x= "cs!0" in bspec)
subgoal by clarsimp
subgoal by simp
apply (clarsimp simp:cte_wp_at_caps_of_state ex_cte_cap_wp_to_def)
apply (clarsimp simp: cte_wp_at_caps_of_state ex_cte_cap_wp_to_def)
apply (rule_tac x=aa in exI,rule exI,rule exI)
apply (rule conjI, assumption)
by (clarsimp simp:diminished_def is_cap_simps mask_cap_def
cap_rights_update_def , simp split:cap.splits )
qed*)
sorry
apply (clarsimp simp: diminished_def is_cap_simps mask_cap_def
cap_rights_update_def,
simp split: cap.splits )
done
qed
lemma asid_bits_ge_0:
@ -262,7 +257,7 @@ lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]:
lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
"\<lbrace>\<lambda>s. descendants_range_in {ptr .. ptr+2^sz - 1} cref s \<and> pspace_no_overlap_range_cover ptr sz s \<and> invs s
\<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2^ sz\<rbrace>
\<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr \<and> cap_is_device c = dev) cref s \<and> idx \<le> 2^ sz\<rbrace>
set_cap (cap.UntypedCap dev ptr sz idx) cref
\<lbrace>\<lambda>rv s. invs s\<rbrace>"
apply (rule hoare_name_pre_state)
@ -276,10 +271,16 @@ lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
set_cap_irq_handlers cap_table_at_lift_valid set_cap_typ_at
set_untyped_cap_refs_respects_device_simple)
apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps)
apply (intro conjI, clarsimp)
apply (rule ext, clarsimp simp:is_cap_simps)
apply (clarsimp split:cap.splits simp:is_cap_simps appropriate_cte_cap_def)
apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD])
apply clarsimp
apply (clarsimp simp:is_cap_simps ex_cte_cap_wp_to_def appropriate_cte_cap_def cte_wp_at_caps_of_state)
apply (clarsimp dest!:valid_global_refsD2 simp:cap_range_def)
apply (simp add:valid_irq_node_def)
apply (clarsimp simp:valid_irq_node_def)
apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state vs_cap_ref_def)
apply (case_tac cap)
apply (simp_all add:vs_cap_ref_def table_cap_ref_def)
apply (rename_tac arch_cap)
@ -289,8 +290,8 @@ lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
valid_refs_def simp del:split_paired_All)
apply (drule_tac x = cref in spec)
apply (clarsimp simp:cte_wp_at_caps_of_state)
(* apply fastforce *)
sorry
apply fastforce
done
lemma pbfs_atleast_pageBits':
@ -409,7 +410,7 @@ lemma store_pde_weaken:
split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
done
(* ARMHYP not needed anymore? *)
(* ARMHYP not needed anymore?
lemma store_pde_nonempty_table:
"\<lbrace>\<lambda>s. \<not> (obj_at (nonempty_table {}) r s)
\<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow>
@ -421,7 +422,7 @@ lemma store_pde_nonempty_table:
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def nonempty_table_def a_type_def)
apply (clarsimp simp add: empty_table_def vspace_bits_defs)
sorry
done *)
(*
lemma valid_arch_state_global_pd: (* ARMHYP restate? *)

28
proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
View File

@ -840,13 +840,9 @@ lemma perform_page_directory_valid_pdpt[wp]:
apply (wp | wpc | simp)+
done
lemma perform_vcpu_valid_pdpt[wp]:
"\<lbrace>valid_pdpt_objs and valid_vcpu_invocation vi\<rbrace>
perform_vcpu_invocation vi \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (simp add: perform_vcpu_invocation_def split_def)
apply (rule hoare_pre)
apply (wp | wpc | simp)+
sorry
crunch valid_pdpt_objs[wp]: perform_vcpu_invocation "valid_pdpt_objs"
(ignore: delete_objects wp: delete_objects_valid_pdpt static_imp_wp)
lemma perform_invocation_valid_pdpt[wp]:
"\<lbrace>invs and ct_active and valid_invocation i and valid_pdpt_objs
@ -1190,22 +1186,22 @@ lemma create_mapping_entries_safe[wp]:
apply (drule_tac x = "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 3)"
in spec)
apply (simp add: vspace_bits_defs)
(* apply (clarsimp simp:not_less[symmetric] split:list.splits)
apply (clarsimp simp:not_less[symmetric] vspace_bits_defs split:list.splits)
apply (clarsimp simp:page_inv_entries_pre_def
Let_def upto_enum_step_def upto_enum_def)
apply (subst (asm) upto_0_to_n2)
apply simp
apply (clarsimp simp:not_less[symmetric])
apply (clarsimp simp:not_less[symmetric] vspace_bits_defs)
apply (subgoal_tac
"(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 3))
= pde.PageTablePDE x xa xb)
\<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 3)) 7")
apply clarsimp
= pde.PageTablePDE x)
\<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3)) 7")
apply (clarsimp simp: vspace_bits_defs)
apply (subgoal_tac "
ptrFromPAddr x + ((vptr >> 12) && 0xFF << 3) \<le>
ptrFromPAddr x + ((vptr >> 12) && 0xFF << 3) + 0x3C")
apply (clarsimp simp:not_less[symmetric])
apply (erule is_aligned_no_wrap')
ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) \<le>
ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) + 0x78")
apply (clarsimp simp:not_less[symmetric] vspace_bits_defs word_1FF_is_mask[symmetric])
(* apply (erule is_aligned_no_wrap')
apply simp
apply clarsimp
apply (rule aligned_add_aligned)

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

@ -87,11 +87,6 @@ lemma valid_ntfn_trans_state[simp]: "valid_ntfn a (trans_state g s) = valid_ntfn
apply (simp add: valid_ntfn_def split: ntfn.splits)
done
lemma [simp]: "\<forall>x5. b = ArchObj x5 \<longrightarrow>
wellformed_arch_obj x5 (trans_state g s) =
wellformed_arch_obj x5 s"
sorry
lemma valid_obj_trans_state[simp]: "valid_obj a b (trans_state g s) = valid_obj a b s"
apply (simp add: valid_obj_def
split: kernel_object.splits option.splits)

10
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -1765,6 +1765,9 @@ lemma cap_swap_fd_reply_masters[wp]:
crunch refs_of[wp]: cap_swap "\<lambda>s. P (state_refs_of s)"
(ignore: set_cap simp: state_refs_of_pspaceI)
crunch hyp_refs_of[wp]: cap_swap "\<lambda>s. P (state_hyp_refs_of s)"
(ignore: set_cap simp: state_refs_of_pspaceI)
crunch cur_tcb[wp]: cap_swap "cur_tcb"
@ -1853,12 +1856,15 @@ lemma cap_swap_irq_handlers[wp]:
done
crunch vspace_objs [wp]: cap_swap "valid_vspace_objs"
(*
crunch arch_objs [wp]: cap_swap "valid_arch_objs"
crunch arch_objs [wp]: cap_move "valid_arch_objs"
crunch arch_objs [wp]: empty_slot "valid_arch_objs"
*)
context CNodeInv_AI begin
@ -1976,7 +1982,7 @@ lemma cap_swap_invs[wp]:
simp del: split_paired_Ex split_paired_All
| rule conjI
| fastforce dest!: valid_reply_caps_of_stateD)+
sorry
done
lemma cap_swap_fd_invs[wp]:
"\<And>a b.

2
proof/invariant-abstract/CSpace_AI.thy
View File

@ -4639,7 +4639,7 @@ crunch empty_table_at[wp]: setup_reply_master "obj_at (empty_table S) p"
lemmas setup_reply_master_valid_vso_at[wp]
= ARM.valid_vso_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
= valid_vso_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
crunch v_ker_map[wp]: setup_reply_master "valid_kernel_mappings"

16
proof/invariant-abstract/Finalise_AI.thy
View File

@ -36,7 +36,6 @@ requalify_facts
no_irq_clearMemory
valid_global_refsD
valid_global_refsD2
prepare_thread_delete_def (* FIXME *)
end
@ -123,7 +122,7 @@ locale Finalise_AI_1 =
\<and> cte_wp_at (op = cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
\<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)
\<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and>
valid_arch_objs s \<and>
valid_vspace_objs s \<and>
valid_arch_state s)\<rbrace>
finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>"
@ -826,19 +825,19 @@ lemma cap_delete_one_cte_wp_at_preserved:
interpretation delete_one_pre
by (unfold_locales, wp cap_delete_one_cte_wp_at_preserved)
lemma (in Finalise_AI_1) finalise_cap_equal_cap[wp]:
"\<lbrace>cte_wp_at (op = cap) sl :: 'a state \<Rightarrow> bool\<rbrace>
finalise_cap cap fin
\<lbrace>\<lambda>rv. cte_wp_at (op = cap) sl\<rbrace>"
apply (cases cap, simp_all split del: if_split)
apply (wp suspend_cte_wp_at_preserved
deleting_irq_handler_cte_preserved
deleting_irq_handler_cte_preserved prepare_thread_delete_cte_wp_at
hoare_drop_imp thread_set_cte_wp_at_trivial
| clarsimp simp: can_fast_finalise_def unbind_maybe_notification_def unbind_notification_def
| clarsimp simp: can_fast_finalise_def unbind_maybe_notification_def
unbind_notification_def
tcb_cap_cases_def
| wpc )+
sorry
done
lemma emptyable_lift:
assumes typ_at: "\<And>P T t. \<lbrace>\<lambda>s. P (typ_at T t s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at T t s)\<rbrace>"
@ -1082,12 +1081,13 @@ lemma (in Finalise_AI_3) finalise_cap_cte_cap_to[wp]:
"\<lbrace>ex_cte_cap_wp_to P sl :: 'a state \<Rightarrow> bool\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>"
apply (cases cap, simp_all add: ex_cte_cap_wp_to_def split del: if_split)
apply (wp hoare_vcg_ex_lift hoare_drop_imps
prepare_thread_delete_cte_preserved_irqn
deleting_irq_handler_cte_preserved_irqn
prepare_thread_delete_cte_preserved_irqn
| simp
| clarsimp simp: can_fast_finalise_def
split: cap.split_asm | wpc)+
sorry
done
lemma (in Finalise_AI_3) finalise_cap_zombie_cap[wp]:
"\<lbrace>cte_wp_at (\<lambda>cp. is_zombie cp \<and> P cp) sl :: 'a state \<Rightarrow> bool\<rbrace>
@ -1096,7 +1096,7 @@ lemma (in Finalise_AI_3) finalise_cap_zombie_cap[wp]:
apply (cases cap, simp_all split del: if_split)
apply (wp deleting_irq_handler_cte_preserved
| clarsimp simp: is_cap_simps can_fast_finalise_def)+
sorry
done
lemma fast_finalise_st_tcb_at:
"\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace>

14
proof/invariant-abstract/Invariants_AI.thy
View File

@ -95,7 +95,8 @@ requalify_facts
hyp_refs_of_live
hyp_refs_of_live_obj
tcb_arch_ref_simps
wellformed_arch_pspace
wellformed_arch_typ
end
lemmas [intro!] = idle_global acap_rights_update_id
@ -1572,11 +1573,6 @@ lemma valid_cap_pspaceI:
simp: obj_range_def valid_untyped_def pred_tcb_at_def
split: option.split sum.split)
(* FIXME move to ArchInvariants and requalify *)
lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>wellformed_arch_obj ao s; kheap s = kheap s'\<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao s'"
sorry
(* FIXME-NTFN: ugly proof *)
lemma valid_obj_pspaceI:
"\<lbrakk> valid_obj ptr obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_obj ptr obj s'"
@ -2204,12 +2200,6 @@ lemma valid_ntfn_typ:
apply (rule hoare_vcg_conj_lift [OF hoare_vcg_prop], simp add: P)
done
(* FIXME move to ArchInvariants and requalify *)
lemma wellformed_arch_typ:
"\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> \<Longrightarrow>
\<lbrace>wellformed_arch_obj ao\<rbrace> f \<lbrace>\<lambda>rv. wellformed_arch_obj ao\<rbrace>"
sorry
lemma valid_obj_typ:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_obj p ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_obj p ob s\<rbrace>"

26
proof/invariant-abstract/IpcCancel_AI.thy
View File

@ -1002,10 +1002,10 @@ lemma unbind_notification_invs:
apply (rule hoare_seq_ext [OF _ get_ntfn_sp])
apply (wp valid_irq_node_typ set_ntfn_valid_objs
| clarsimp)+
defer 4
defer 5
apply (auto elim!: obj_at_weakenE obj_at_valid_objsE if_live_then_nonz_capD2
simp: valid_ntfn_set_bound_None is_ntfn valid_obj_def)[10]
(* apply (clarsimp simp: if_split) *)
simp: valid_ntfn_set_bound_None is_ntfn valid_obj_def)[9]
apply (clarsimp simp: if_split)
apply (rule delta_sym_refs, assumption)
apply (fastforce simp: obj_at_def is_tcb
dest!: pred_tcb_at_tcb_at ko_at_state_refs_ofD
@ -1017,12 +1017,12 @@ lemma unbind_notification_invs:
apply (fastforce simp: obj_at_def is_tcb ntfn_q_refs_no_NTFNBound tcb_at_no_ntfn_bound refs_of_rev
tcb_ntfn_is_bound_def
dest!: pred_tcb_at_tcb_at bound_tcb_at_state_refs_ofD)
(* apply (subst (asm) ko_at_state_refs_ofD, assumption)
apply (subst (asm) ko_at_state_refs_ofD, assumption)
apply (fastforce simp: ntfn_bound_refs_def obj_at_def ntfn_q_refs_no_TCBBound
elim!: pred_tcb_weakenE
dest!: bound_tcb_bound_notification_at refs_in_ntfn_bound_refs symreftype_inverse'
split: option.splits) *)
sorry
dest!: bound_tcb_bound_notification_at refs_in_ntfn_bound_refs symreftype_inverse'
split: option.splits)
done
crunch bound_tcb_at[wp]: cancel_all_signals "bound_tcb_at P t"
@ -1147,7 +1147,7 @@ crunch cte_wp_at[wp]: cancel_all_signals "cte_wp_at P p"
lemma cancel_badged_sends_filterM_helper':
"\<forall>ys.
\<lbrace>\<lambda>s. all_invs_but_sym_refs s \<and> distinct (xs @ ys) \<and> ep_at epptr s
\<lbrace>\<lambda>s. all_invs_but_sym_refs s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s
\<and> ex_nonz_cap_to epptr s
\<and> sym_refs ((state_refs_of s) (epptr := ((set (xs @ ys)) \<times> {EPSend})))
\<and> (\<forall>x \<in> set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace>
@ -1159,7 +1159,7 @@ lemma cancel_badged_sends_filterM_helper':
od
else return True
od) xs
\<lbrace>\<lambda>rv s. all_invs_but_sym_refs s
\<lbrace>\<lambda>rv s. all_invs_but_sym_refs s \<and> sym_refs (state_hyp_refs_of s)
\<and> ep_at epptr s \<and> (\<forall>x \<in> set (xs @ ys). tcb_at x s)
\<and> ex_nonz_cap_to epptr s
\<and> (\<forall>y \<in> set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})
@ -1182,6 +1182,7 @@ lemma cancel_badged_sends_filterM_helper':
apply clarsimp
apply (thin_tac "ep_at epptr s" for s)
apply (thin_tac "tcb_at x s" for x s)
apply (thin_tac "sym_refs (state_hyp_refs_of s)" for s)
apply (frule singleton_eqD, clarify, drule state_refs_of_elemD)
apply (frule(1) if_live_then_nonz_capD, rule refs_of_live, clarsimp)
apply (clarsimp simp: st_tcb_at_refs_of_rev)
@ -1218,8 +1219,9 @@ lemma cancel_badged_sends_invs[wp]:
cong: list.case_cong)
apply (rule hoare_strengthen_post,
rule cancel_badged_sends_filterM_helper[where epptr=epptr])
apply (auto intro:obj_at_weakenE)[1]
(* apply (wp valid_irq_node_typ)
apply (wp valid_irq_node_typ)
apply (clarsimp simp: valid_ep_def conj_comms)
apply (subst obj_at_weakenE[where P'=is_ep], assumption)
apply (clarsimp simp: is_ep_def)
@ -1232,8 +1234,8 @@ lemma cancel_badged_sends_invs[wp]:
apply (drule st_tcb_at_state_refs_ofD)
apply (clarsimp simp only: cancel_badged_sends_invs_helper Un_iff, clarsimp)
apply (simp add: set_eq_subset)
apply wpsimp *)
sorry
apply wpsimp
done
lemma real_cte_emptyable_strg:

26
proof/invariant-abstract/Ipc_AI.thy
View File

@ -214,6 +214,11 @@ locale Ipc_AI =
\<lbrace>cte_wp_at P p :: 'state_ext state \<Rightarrow> bool\<rbrace>
do_fault_transfer x t label msg
\<lbrace> \<lambda>rv. cte_wp_at P p \<rbrace>"
assumes transfer_caps_loop_valid_vspace_objs:
"\<And>ep buffer n caps slots mi.
\<lbrace>valid_vspace_objs::'state_ext state \<Rightarrow> bool\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
assumes arch_get_sanitise_register_info_typ_at[wp]:
"\<And> P T p t.
\<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace>
@ -1045,11 +1050,19 @@ lemma transfer_caps_loop_invs[wp]:
\<and> transfer_caps_srcs caps s\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. invs\<rbrace>"
unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ)
unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs)
end
(* FIXME: move *)
crunch valid_vspace_objs [wp]: set_extra_badge valid_vspace_objs
crunch vspace_objs [wp]: set_untyped_cap_as_full "valid_vspace_objs"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
crunch vspace_objs [wp]: cap_insert "valid_vspace_objs"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
lemma zipWith_append2:
"length ys + 1 < n \<Longrightarrow>
zipWith f [0 ..< n] (ys @ [y]) = zipWith f [0 ..< n] ys @ [f (length ys) y]"
@ -1588,10 +1601,10 @@ crunch irq_handlers[wp]: do_ipc_transfer "valid_irq_handlers :: 'state_ext state
(wp: crunch_wps hoare_vcg_const_Ball_lift simp: zipWithM_x_mapM crunch_simps ball_conj_distrib )
crunch vspace_objs[wp]: transfer_caps_loop "valid_vspace_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: zipWithM_x_mapM crunch_simps)
(wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
crunch vspace_objs[wp]: do_ipc_transfer "valid_vspace_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: zipWithM_x_mapM crunch_simps)
(wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
crunch arch_caps[wp]: do_ipc_transfer "valid_arch_caps :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_valid_arch_caps
@ -2584,9 +2597,10 @@ lemma ri_invs':
conj_comms tcb_at_cte_at_2)
apply (erule delta_sym_refs)
apply (clarsimp split: if_split_asm)
apply ((clarsimp simp: pred_tcb_at_def2 tcb_bound_refs_def2 is_tcb
apply (clarsimp split: if_split_asm if_split) (* FIXME *)
apply ((fastforce simp: pred_tcb_at_def2 tcb_bound_refs_def2 is_tcb
dest!: symreftype_inverse')+)[3]
(* apply (rule conjI)
apply (rule conjI)
apply (clarsimp simp: pred_tcb_at_def2 tcb_bound_refs_def2
split: if_split_asm)
apply (simp add: set_eq_subset)
@ -2623,7 +2637,7 @@ lemma ri_invs':
apply (rule hoare_pre)
apply (wp get_ntfn_wp | wpc | clarsimp)+
apply (clarsimp simp: pred_tcb_at_tcb_at)
done *) sorry
done
lemmas ri_invs[wp]
= ri_invs'[where Q=\<top>,simplified hoare_post_taut, OF TrueI TrueI TrueI,simplified]

130
proof/invariant-abstract/KHeap_AI.thy
View File

@ -23,7 +23,6 @@ requalify_consts
requalify_facts
pspace_in_kernel_window_atyp_lift
(* valid_arch_objs_lift_weak *)
valid_vspace_objs_lift_weak
vs_lookup_vspace_obj_at_lift
vs_lookup_pages_vspace_obj_at_lift
@ -32,7 +31,7 @@ requalify_facts
valid_kernel_mappings_lift
equal_kernel_mappings_lift
valid_machine_state_lift
(* valid_ao_at_lift_aobj_at*)
valid_vso_at_lift
valid_vso_at_lift_aobj_at
valid_arch_state_lift_aobj_at
in_user_frame_lift
@ -50,6 +49,12 @@ requalify_facts
pspace_respects_region_cong
cap_is_device_obj_is_device
storeWord_device_state_inv
state_hyp_refs_of_ep_update
state_hyp_refs_of_ntfn_update
state_hyp_refs_of_tcb_state_update
state_hyp_refs_of_tcb_bound_ntfn_update
wellformed_arch_obj_same_type
end
lemmas cap_is_device_obj_is_device[simp] = cap_is_device_obj_is_device
@ -76,14 +81,6 @@ lemma get_tcb_rev:
"kheap s p = Some (TCB t)\<Longrightarrow> get_tcb p s = Some t"
by (clarsimp simp:get_tcb_def)
(* moved to KHeapPre_AI
lemma get_tcb_SomeD: "get_tcb t s = Some v \<Longrightarrow> kheap s t = Some (TCB v)"
apply (cases "kheap s t"; simp add: get_tcb_def)
apply (rename_tac obj)
apply (case_tac obj; simp)
done
*)
lemma get_tcb_obj_atE[elim!]:
"\<lbrakk> get_tcb t s = Some tcb; get_tcb t s = Some tcb \<Longrightarrow> P (TCB tcb) \<rbrakk> \<Longrightarrow> obj_at P t s"
by (clarsimp dest!: get_tcb_SomeD simp: obj_at_def)
@ -106,13 +103,6 @@ lemma pspace_aligned_obj_update:
done
lemma typ_at_same_type:
assumes "typ_at T p s" "a_type k = a_type ko" "kheap s p' = Some ko"
shows "typ_at T p (s\<lparr>kheap := kheap s(p' \<mapsto> k)\<rparr>)"
using assms
by (clarsimp simp: obj_at_def)
lemma cte_at_same_type:
"\<lbrakk>cte_at t s; a_type k = a_type ko; kheap s p = Some ko\<rbrakk>
\<Longrightarrow> cte_at t (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
@ -133,29 +123,6 @@ lemma untyped_same_type:
unfolding valid_untyped_def
by (clarsimp simp: obj_range_def obj_bits_T)
lemma hoare_to_pure_kheap_upd:
assumes hoare[rule_format]:
"\<And>f. (\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace>
f \<lbrace>\<lambda>r s. P (typ_at (AArch T) p s)\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
assumes typ_eq: "a_type k = a_type ko"
assumes valid: "P (s :: ('z :: state_ext) state)"
assumes at: "ko_at ko p s"
shows "P (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
apply (rule use_valid[where f="
do
s' <- get;
assert (s' = s);
(modify (\<lambda>s. s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>));
return undefined
od", OF _ hoare valid])
apply (fastforce simp add: simpler_modify_def get_def bind_def
assert_def return_def[abs_def] fail_def)[1]
apply wp
apply (insert typ_eq at)
apply clarsimp
apply (erule_tac P=P in rsubst)
by (auto simp add: obj_at_def a_type_def split: kernel_object.splits if_splits)
lemma valid_cap_same_type:
"\<lbrakk> s \<turnstile> cap; a_type k = a_type ko; kheap s p = Some ko \<rbrakk>
\<Longrightarrow> s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr> \<turnstile> cap"
@ -167,6 +134,11 @@ lemma valid_cap_same_type:
assumption, auto)
lemma wellformed_arch_obj_same_type:
"\<lbrakk> wellformed_arch_obj obj s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> wellformed_arch_obj obj (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
oops
lemma valid_obj_same_type:
"\<lbrakk> valid_obj p' obj s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> valid_obj p' obj (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
@ -187,33 +159,9 @@ lemma valid_obj_same_type:
apply (auto elim: typ_at_same_type
simp: tcb_at_typ
split: Structures_A.ntfn.splits option.splits)
apply (simp add: valid_obj_def "ARM.wellformed_arch_obj_def"
ARM_A.arch_kernel_obj.distinct
ARM_A.arch_kernel_obj.inject
split: ARM_A.arch_kernel_obj.splits)
apply (rename_tac v)
apply (case_tac "ARM_A.vcpu_tcb v"; simp add: ARM.valid_vcpu_def)
apply (drule typ_at_same_type[rotated]; assumption)
done
lemma valid_arch_obj_same_type:
"\<lbrakk>valid_arch_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
\<Longrightarrow> valid_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
apply (induction ao rule: ARM_A.arch_kernel_obj.induct;
clarsimp simp: ARM.valid_arch_obj.simps typ_at_same_type)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule ARM.valid_pte_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule ARM.valid_pde_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (rename_tac v)
apply (case_tac "ARM_A.vcpu_tcb v"; simp add: ARM.valid_vcpu_def)
apply (drule typ_at_same_type[rotated]; assumption)
done
apply (clarsimp simp add: valid_obj_def)
apply (auto intro: wellformed_arch_obj_same_type)
done
lemma valid_vspace_obj_same_type:
"\<lbrakk>valid_vspace_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
@ -543,16 +491,15 @@ lemma set_ep_refs_of[wp]:
lemma set_ep_hyp_refs_of[wp]:
"\<lbrace>\<lambda>s. P (ARM.state_hyp_refs_of s)\<rbrace>
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
set_endpoint ep val
\<lbrace>\<lambda>rv s. P (ARM.state_hyp_refs_of s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: set_endpoint_def set_object_def)
apply (rule hoare_seq_ext [OF _ get_object_sp])
apply wp
apply clarsimp
apply (drule_tac ARM.ko_at_state_hyp_refs_ofD)
apply (case_tac obj; clarsimp elim!: rsubst[where P=P])
apply (rule all_ext; clarsimp simp: ARM.state_hyp_refs_of_def ARM.hyp_refs_of_simps ARM.hyp_refs_of_def)
apply (wp, clarsimp)
apply (subst state_hyp_refs_of_ep_update[of ep _ val, simplified fun_upd_def])
apply (case_tac obj; clarsimp simp: typ_at_eq_kheap_obj obj_at_def)
apply assumption
done
@ -815,18 +762,18 @@ lemma set_ntfn_refs_of[wp]:
done
lemma set_ntfn_hyp_refs_of[wp]: (* ARMHYP *)
"\<lbrace>\<lambda>s. P ((ARM.state_hyp_refs_of s))\<rbrace>
"\<lbrace>\<lambda>s. P ((state_hyp_refs_of s))\<rbrace>
set_notification ntfnptr ntfn
\<lbrace>\<lambda>rv s. P (ARM.state_hyp_refs_of s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: set_notification_def set_object_def)
apply (rule hoare_seq_ext [OF _ get_object_sp])
apply wp
apply clarsimp
apply (drule_tac ARM.ko_at_state_hyp_refs_ofD)
apply (case_tac obj; clarsimp elim!: rsubst[where P=P])
apply (rule all_ext; clarsimp simp: ARM.state_hyp_refs_of_def ARM.hyp_refs_of_simps ARM.hyp_refs_of_def)
apply (wp, clarsimp)
apply (subst state_hyp_refs_of_ntfn_update[of ntfnptr _ ntfn, simplified fun_upd_def])
apply (case_tac obj; clarsimp simp: typ_at_eq_kheap_obj obj_at_def)
apply assumption
done
lemma set_ntfn_cur_tcb[wp]:
"\<lbrace>cur_tcb\<rbrace> set_notification ntfn v \<lbrace>\<lambda>rv. cur_tcb\<rbrace>"
apply (simp add: set_notification_def set_object_def)
@ -1302,16 +1249,6 @@ lemma set_object_non_pagetable:
apply (clarsimp simp: obj_at_def)
by (rule vspace_obj_predE)
(*
lemma set_object_arch_objs_non_arch:
"\<lbrace>valid_arch_objs and K (non_arch_obj ko) and obj_at non_arch_obj p\<rbrace>
set_object p ko
\<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (rule assert_pre)
apply (rule hoare_pre)
apply (rule valid_arch_objs_lift_weak)
apply (wp set_object_non_arch | clarsimp)+
done *)
lemma set_object_vspace_objs_non_pagetable:
"\<lbrace>valid_vspace_objs and K (non_vspace_obj ko) and obj_at non_vspace_obj p\<rbrace>
@ -1376,10 +1313,7 @@ by (rule valid_kernel_mappings_lift, wp vsobj_at)
lemma equal_kernel_mappings[wp]: "\<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>_. equal_kernel_mappings\<rbrace>"
by (rule equal_kernel_mappings_lift, wp vsobj_at)
(*
lemma valid_ao_at[wp]:"\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>_. valid_ao_at p\<rbrace>"
by (rule valid_ao_at_lift_aobj_at; wp aobj_at; simp)
*)
lemma valid_vso_at[wp]:"\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>_. valid_vso_at p\<rbrace>"
by (rule valid_vso_at_lift_aobj_at; wp vsobj_at; simp)
@ -1662,7 +1596,7 @@ lemma set_ntfn_minor_invs:
set_notification ptr val
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def)
apply_trace (rule hoare_pre,
apply (rule hoare_pre,
wp_trace set_ntfn_valid_objs valid_irq_node_typ
valid_irq_handlers_lift)
apply (clarsimp elim!: rsubst[where P=sym_refs]
@ -1725,9 +1659,9 @@ lemma dmo_refs_of[wp]:
lemma dmo_hyp_refs_of[wp]:
"\<lbrace>\<lambda>s. P (ARM.state_hyp_refs_of s)\<rbrace>
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
do_machine_op oper
\<lbrace>\<lambda>rv s. P (ARM.state_hyp_refs_of s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: do_machine_op_def split_def)
apply wp
apply (clarsimp elim!: state_hyp_refs_of_pspaceI)

24
proof/invariant-abstract/TcbAcc_AI.thy
View File

@ -1173,16 +1173,21 @@ lemma sts_refs_of[wp]:
apply (simp add: get_tcb_def sts_refs_of_helper)
done
lemma kheap_Some_state_hyp_refs_ofD:
"kheap s p = Some ko \<Longrightarrow> state_hyp_refs_of s p = hyp_refs_of ko"
by (rule ko_at_state_hyp_refs_ofD; simp add: obj_at_def)
(* FIXME should be able to prove this in the generic context *)
lemma sts_hyp_refs_of[wp]:
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
set_thread_state t st
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp, simp, wp)
apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD)
apply (rule state_hyp_refs_update[symmetric])
sorry
apply (wp | simp del: fun_upd_apply)+
apply (clarsimp simp: get_tcb_def split: option.splits kernel_object.splits
simp del: fun_upd_apply)
apply (subst state_hyp_refs_of_tcb_state_update; assumption)
done
lemma sbn_refs_of_helper: "
{r. (r \<in> tcb_st_refs_of ts \<or>
@ -1204,17 +1209,18 @@ lemma sbn_refs_of[wp]:
apply (auto simp: get_tcb_def sbn_refs_of_helper)
done
(* FIXME the same as the above FIXME *)
lemma sbn_hyp_refs_of[wp]:
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
set_bound_notification t ntfn
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply (wp, simp)
apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD
intro!: ext)
apply (auto simp: get_tcb_def)
sorry
apply (wp, simp del: fun_upd_apply)
apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD simp del: fun_upd_apply
intro!: ext)
apply (subst state_hyp_refs_of_tcb_bound_ntfn_update; auto simp: get_tcb_def)
done
lemma set_thread_state_thread_set:
"set_thread_state p st = (do thread_set (tcb_state_update (\<lambda>_. st)) p;

7
proof/invariant-abstract/Untyped_AI.thy
View File

@ -3847,7 +3847,7 @@ lemma invoke_untyp_invs':
distinct_tuple_helper
init_arch_objects_wps
init_arch_objects_nonempty_table
| wp_once retype_region_ret_folded_general)
| wp_once retype_region_ret_folded_general)+
apply ((wp hoare_vcg_const_imp_lift hoare_drop_imp
retype_region_invs_extras[where sz = sz]
retype_region_aligned_for_init[where sz = sz]
@ -3858,7 +3858,7 @@ lemma invoke_untyp_invs':
distinct_map_fst_zip
| simp add: ptr_base
| wp_once retype_region_ret_folded_general)+)[1]
(* apply (clarsimp simp:conj_comms,simp cong:conj_cong)
apply (clarsimp simp:conj_comms,simp cong:conj_cong)
apply (simp add:ball_conj_distrib conj_comms)
apply (strengthen invs_mdb invs_valid_pspace
caps_region_kernel_window_imp[where p="(cref, oref)"]
@ -3943,8 +3943,7 @@ lemma invoke_untyp_invs':
apply (frule untyped_mdb_descendants_range, clarsimp+,
erule invoke_untyped_proofs.descendants_range, simp_all+)[1]
apply (simp add: untyped_range_def atLeastatMost_subset_iff word_and_le2)
*)
sorry
done
qed
lemmas invoke_untyp_invs[wp] =