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

isabelle-2021: update DSpecProofs 

Signed-off-by: Gerwin Klein <kleing@unsw.edu.au>
This commit is contained in:
Gerwin Klein 2021-02-18 10:18:02 +11:00 committed by Gerwin Klein
parent 6f72b06db3
commit b5f320ece4
6 changed files with 19 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
proof/capDL-api/Arch_DP.thy
View File

@ -63,16 +63,13 @@ lemma decode_page_map_intent_rv_20_24:
[(PageDirectoryCap ptr real' asid',pdref)]
(PageIntent (PageMapIntent vaddr perms vmattr))
\<lbrace>\<lambda>r s. R r\<rbrace>, -"
apply (simp add:decode_invocation_def get_index_def
get_page_intent_def throw_opt_def cap_rights_def
decode_page_invocation_def throw_on_none_def get_mapped_asid_def)
apply (simp add: decode_invocation_def get_index_def get_page_intent_def throw_opt_def
cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def)
apply (wp alternativeE_wp select_wp | wpc)+
apply (rule validE_validE_R)
apply (wp alternativeE_wp)
apply (simp add:cdl_page_mapping_entries_def
split del:if_splits | wp | wpc)+
apply auto
apply (rule validE_validE_R)
apply (wp alternativeE_wp)
apply (simp add:cdl_page_mapping_entries_def split del:if_split | wp | wpc)+
apply auto
done
lemma decode_page_map_intent_rv_16_12:
@ -92,7 +89,7 @@ lemma decode_page_map_intent_rv_16_12:
apply (wp alternativeE_wp select_wp)
apply (rule validE_validE_R)
apply (wp alternativeE_wp)
apply (simp add:cdl_page_mapping_entries_def split del:if_splits)
apply (simp add:cdl_page_mapping_entries_def)
apply (wp cdl_lookup_pt_slot_rv | wpc | simp)+
apply auto
done

5
proof/capDL-api/IRQ_DP.thy
View File

@ -394,11 +394,6 @@ shows "\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>* (root_t
apply (clarsimp dest!: reset_cap_asid_simps2)
done
lemma obj_tcb_simps [simp]:
"is_tcb tcb \<Longrightarrow> Tcb (obj_tcb tcb) = tcb"
by (clarsimp simp: is_tcb_def obj_tcb_def split: cdl_object.splits)
lemma seL4_IRQHandler_SetEndpoint_wp:
"\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*

18
proof/capDL-api/Invocation_DP.thy
View File

@ -202,7 +202,7 @@ lemma syscall_valid_helper:
arg_decode_fn arg_error_handler_fn
perform_syscall_fn
\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r. Inv\<rbrace>"
apply (simp add:syscall_def del:split_paired_all)
apply (simp add:syscall_def)
apply (rule hoare_vcg_handle_elseE)
apply simp
apply simp
@ -455,9 +455,6 @@ lemma corrupt_ipc_buffer_active_tcbs[wp]:
apply wp
done
crunch cdl_current_thread [wp]: update_thread "\<lambda>s. P (cdl_current_thread s)"
(wp: crunch_wps)
lemma update_thread_wp:
"\<lbrace>tcb_at' (\<lambda>tcb. P (f tcb)) thread\<rbrace> update_thread thread f
\<lbrace>\<lambda>rv. tcb_at' P thread \<rbrace>"
@ -508,8 +505,7 @@ lemma handle_pending_interrupts_no_ntf_cap:
apply (rule hoare_pre)
apply (wp send_signal_no_pending
| wpc
| simp add: option_select_def handle_interrupt_def
split del: if_splits)+
| simp add: option_select_def handle_interrupt_def split del: if_split)+
apply (wp alternative_wp select_wp hoare_drop_imps hoare_vcg_all_lift)
apply simp
done
@ -696,14 +692,6 @@ crunch cdl_current_thread[wp]: invoke_untyped "\<lambda>s. P (cdl_current_thread
helper
simp:cdl_cur_thread_detype crunch_simps)
crunch cdl_current_thread[wp]: insert_cap_sibling "\<lambda>s. P (cdl_current_thread s)"
(wp:select_wp mapM_x_wp' crunch_wps hoare_unless_wp
simp: crunch_simps)
crunch cdl_current_thread[wp]: insert_cap_child "\<lambda>s. P (cdl_current_thread s)"
(wp:select_wp mapM_x_wp' crunch_wps hoare_unless_wp
simp:crunch_simps)
crunch cdl_current_thread[wp]: move_cap "\<lambda>s. P (cdl_current_thread s)"
(wp:select_wp mapM_x_wp' crunch_wps hoare_unless_wp
simp:crunch_simps)
@ -855,7 +843,7 @@ lemma syscall_valid_helper_allow_error:
perform_syscall_fn
\<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s)
\<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>,\<lbrace>\<lambda>r. Inv\<rbrace>"
apply (simp add:syscall_def del:split_paired_all)
apply (simp add:syscall_def)
apply (rule hoare_vcg_handle_elseE)
apply (erule hoare_pre)
apply simp

20
proof/capDL-api/KHeap_DP.thy
View File

@ -679,15 +679,13 @@ lemma reset_cap_asid_ep_cap:
lemma reset_cap_asid_ntfn_cap:
"reset_cap_asid cap = reset_cap_asid cap'
\<Longrightarrow> is_ntfn_cap cap = is_ntfn_cap cap'"
apply (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def)
done
by (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def)
lemma cap_rights_reset_cap_asid:
"reset_cap_asid cap = reset_cap_asid cap'
\<Longrightarrow> cap_rights cap = cap_rights cap'"
apply (clarsimp simp: cap_rights_def reset_cap_asid_def)
apply (case_tac cap; (case_tac cap'; simp))
done
by (case_tac cap; (case_tac cap'; simp))
(* Lemmas about valid_src_cap *)
lemma reset_cap_asid_cnode_cap:
@ -789,9 +787,6 @@ lemma fast_finalise_cap_non_ep_wp:
"\<lbrace><P> and K (\<not> ep_related_cap cap') \<rbrace> fast_finalise cap' final \<lbrace>\<lambda>y. <P>\<rbrace>"
by (case_tac cap',simp_all add:ep_related_cap_def)
crunch inv [wp]: is_final_cap "\<lambda>s. P"
(wp:crunch_wps select_wp simp:split_def unless_def)
lemma delete_cap_simple_wp:
"\<lbrace>\<lambda>s. <ptr \<mapsto>c cap \<and>* R> s \<and> \<not> ep_related_cap cap\<rbrace>
delete_cap_simple ptr
@ -1042,10 +1037,10 @@ lemma decode_cnode_mint_rvu:
apply (metis reset_cap_asid_cap_type)
apply (frule (1) reset_cap_asid_ep_cap[THEN iffD1])
apply simp
apply (metis reset_cap_asid_cap_badge ep_related_capI)
apply (metis reset_cap_asid_cap_badge ep_related_capI(1))
apply (frule (1) reset_cap_asid_ntfn_cap[THEN iffD1])
apply simp
apply (metis reset_cap_asid_cap_badge ep_related_capI)
apply (metis reset_cap_asid_cap_badge ep_related_capI(2))
apply (metis option.inject reset_cap_asid_cnode_cap)
apply (metis cap_rights_reset_cap_asid)
apply sep_solve
@ -1103,15 +1098,10 @@ lemma decode_cnode_mutate_rvu:
apply (clarsimp dest!: mapu_dest_opt_cap
simp: conj_comms update_cap_data_non cong:non_cap_cong)
apply (subst (asm) reset_cap_asid_ep_related_cap[OF sym], assumption)
apply (metis reset_cap_asid_cap_type reset_cap_asid_ep_related_cap valid_src_cap_asid_cong
ep_related_capI)
apply (metis reset_cap_asid_cap_type valid_src_cap_asid_cong ep_related_capI(1-2))
apply sep_solve
done
crunch preserve [wp]: decode_cnode_invocation "P"
(wp: derive_cap_wpE unlessE_wp hoare_whenE_wp select_wp hoare_drop_imps
simp: hoare_if_simpE if_apply_def2 throw_on_none_def)
lemma do_kernel_op_pull_back:
"\<lbrace>\<lambda>s. P s\<rbrace> oper \<lbrace>\<lambda>r. Q r\<rbrace> \<Longrightarrow>
\<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do_kernel_op oper \<lbrace>\<lambda>r s. Q r (kernel_state s)\<rbrace>"

25
proof/capDL-api/Retype_DP.thy
View File

@ -491,7 +491,7 @@ lemma invoke_untyped_exception:
apply (simp add: whenE_def)
apply wp+
apply clarsimp
apply (cut_tac p = "(a,b)" in opt_cap_sep_imp)
apply (cut_tac p = "uref" in opt_cap_sep_imp)
apply sep_solve
apply (clarsimp dest!: reset_cap_asid_simps2)
done
@ -561,12 +561,6 @@ lemma update_thread_intent_has_children[wp]:
\<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>"
by (simp add:has_children_def is_cdt_parent_def | wp )+
crunch cdt[wp]: set_cap "\<lambda>s. P (cdl_cdt s)"
(wp:select_wp simp:crunch_simps corrupt_intents_def)
crunch has_children[wp]: set_cap "has_children slot"
(wp:select_wp simp:crunch_simps corrupt_intents_def simp:has_children_def is_cdt_parent_def)
lemma seL4_Untyped_Retype_sep:
"\<lbrakk>cap_object root_cnode_cap = root_cnode;
@ -711,13 +705,6 @@ lemma seL4_Untyped_Retype_sep:
* become parents, and never lose their children *
**********************************************************************)
crunch cdt_inc[wp]: set_cap "\<lambda>s. cdl_cdt s child = parent"
(wp:select_wp simp:crunch_simps)
crunch cdt_inc[wp]: has_restart_cap "\<lambda>s. cdl_cdt s child = parent"
(wp:select_wp simp:crunch_simps)
crunch cdt_inc[wp]: schedule "\<lambda>s. cdl_cdt s child = parent"
(wp:select_wp alternative_wp crunch_wps simp:crunch_simps)
@ -857,12 +844,6 @@ lemma lookup_cap_rvu':
crunch cdl_current_thread [wp]: handle_pending_interrupts "\<lambda>s. P (cdl_current_thread s)"
(wp: alternative_wp select_wp)
crunch cdl_current_thread [wp]: lookup_slot_for_cnode_op "\<lambda>s. P (cdl_current_thread s)"
(wp: alternative_wp select_wp)
crunch cdl_current_thread [wp]: lookup_slot "\<lambda>s. P (cdl_current_thread s)"
(wp: alternative_wp select_wp)
crunch cdl_current_thread [wp]: lookup_cap "\<lambda>s. P (cdl_current_thread s)"
(wp: alternative_wp select_wp hoare_drop_imps)
@ -1049,10 +1030,6 @@ lemma transfer_caps_loop_cdl_parent:
lemmas reset_untyped_cap_cdl2[wp] = reset_untyped_cap_cdl_parent[THEN valid_validE_E]
crunch cdl_parent[wp]: invoke_untyped "\<lambda>s. cdl_cdt s slot = Some parent"
(wp: assert_inv crunch_wps select_wp mapME_x_inv_wp alternative_wp
simp: crunch_simps detype_def)
crunch cdt_parent: inject_reply_cap "\<lambda>s. cdl_cdt s slot = Some parent"
(simp: crunch_simps unless_def wp: crunch_wps)

12
proof/capDL-api/TCB_DP.thy
View File

@ -705,8 +705,7 @@ lemma call_kernel_with_intent_no_fault_helper':
done
lemma is_tcb_cap_is_object: "is_tcb_cap tcb_cap \<Longrightarrow> TcbCap (cap_object tcb_cap) = tcb_cap"
apply (clarsimp simp: cap_type_def cap_object_simps split: cdl_cap.splits)
done
by (clarsimp simp: cap_type_def split: cdl_cap.splits)
lemma reset_cap_asid_mem_mapping:
@ -1033,6 +1032,7 @@ shows
reset_cap_asid buffer_frame_cap = reset_cap_asid (buffer_frame_cap') " in hoare_gen_asmEx)
apply (simp)
apply (elim exE)
supply [[simproc del: defined_all]]
apply simp
apply (rule false_e_explode)
apply (rule no_exception_conj')
@ -1056,7 +1056,7 @@ shows
apply (rule conjI)
prefer 2
apply (simp add: sep_conj_assoc update_tcb_fault_endpoint_def)
apply (clarsimp simp:unify cap_object_simps dest!:cap_typeD)
apply (clarsimp simp:unify dest!:cap_typeD)
apply (rule sep_map_c_any[where cap = RestartCap])
apply (sep_schem)
apply sep_solve
@ -1158,12 +1158,6 @@ shows
apply (sep_solve)
done
crunch idle_thread[wp]: set_cap "\<lambda>s. P (cdl_current_thread s)"
(wp: crunch_wps)
crunch current_domain[wp]: set_cap "\<lambda>s. P (cdl_current_domain s)"
(wp: crunch_wps)
lemma reset_cap_asid_pending:
"reset_cap_asid cap' = reset_cap_asid cap
\<Longrightarrow> is_pending_cap cap' = is_pending_cap cap"