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

ARM bisim: proof update for user_context refactor

This commit is contained in:
Gerwin Klein 2018-02-27 15:40:08 +11:00
parent b0cac3ec77
commit 51190d18d1
2 changed files with 40 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
proof/bisim/Syscall_S.thy
View File

@ -640,59 +640,59 @@ lemma handle_event_bisim:
handle_reply_def
cong: syscall.case_cong)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all)[1]
apply (rename_tac syscall)
apply (case_tac syscall, simp_all)[1]
apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp)
apply (rule bisim_guard_imp_both)
apply (rule bisim_symb_exec_r_bs)
apply (rule handle_reply_bisim)
apply (rule handle_recv_bisim)
apply simp
apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp)
apply (rule bisim_guard_imp_both)
apply (rule bisim_symb_exec_r_bs)
apply (rule handle_reply_bisim)
apply (rule handle_recv_bisim)
apply simp
apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_reply_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_reply_bisim, simp)
apply (simp add: handle_yield_def Syscall_A.handle_yield_def)
apply (rule bisim_guard_imp_both, rule bisim_refl', simp)
apply (simp add: handle_yield_def Syscall_A.handle_yield_def)
apply (rule bisim_guard_imp_both, rule bisim_refl', simp)
apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp)
apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp)
apply (rule bisim_split_refl)
apply (rule handle_fault_bisim)
apply wp+
apply (simp add: cur_tcb_def)
apply (rule bisim_split_refl)
apply (rule handle_fault_bisim)
apply wp+
apply (simp add: cur_tcb_def)
apply (rule bisim_refl)
apply simp
apply (rename_tac vmfault_type)
apply (rule bisim_guard_imp_both)
apply (rule bisim_split_refl)
apply (rule handle_fault_bisim)
apply wp+
apply (simp add: cur_tcb_def)
apply (rule bisim_split_catch_req)
apply (rule bisim_reflE)
apply (rule handle_fault_bisim)
apply wp
apply (case_tac vmfault_type, simp_all)[1]
apply (wp separate_state_pres)
apply (rule hoare_pre, wps, wp, simp)
apply wp
apply (rule hoare_pre, wps, wp, simp)
apply simp
apply (rule bisim_refl)
apply simp
apply (rename_tac vmfault_type)
apply (rule bisim_guard_imp_both)
apply (rule bisim_split_refl)
apply (rule bisim_split_catch_req)
apply (rule bisim_reflE)
apply (rule handle_fault_bisim)
apply wp
apply (case_tac vmfault_type, simp_all)[1]
apply (wp separate_state_pres)
apply (rule hoare_pre, wps, wp, simp)
apply wp
apply (rule hoare_pre, wps, wp, simp)
apply simp
apply (wp separate_state_pres)+
apply (rule hoare_pre, wps, wp+, simp)
apply wpsimp+
apply (wp separate_state_pres)+
apply (rule hoare_pre, wps, wp+, simp)
apply wpsimp+
apply (simp add: cur_tcb_def)
apply (rule bisim_refl, simp)
apply (rule bisim_refl, simp)
done
lemma call_kernel_bisim:

4
spec/sep-abstract/Syscall_SA.thy
View File

@ -84,7 +84,7 @@ where
thread \<leftarrow> liftE $ gets cur_thread;
info \<leftarrow> without_preemption $ get_message_info thread;
ptr \<leftarrow> without_preemption $ liftM data_to_cptr $
as_user thread $ get_register cap_register;
as_user thread $ getRegister cap_register;
syscall
(doE
(cap, slot) \<leftarrow> cap_fault_on_failure (of_bl ptr) False $ lookup_cap_and_slot thread ptr;
@ -147,7 +147,7 @@ definition
thread \<leftarrow> gets cur_thread;
ep_cptr \<leftarrow> liftM data_to_cptr $ as_user thread $
get_register cap_register;
getRegister cap_register;
(cap_fault_on_failure (of_bl ep_cptr) True $ doE
ep_cap \<leftarrow> lookup_cap thread ep_cptr;