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

x64: fix AInvs after merge

This commit is contained in:
Joel Beeren 2017-03-14 12:16:13 +11:00
parent 67daaea42a
commit eb8ee72610
2 changed files with 18 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy
View File

@ -290,15 +290,6 @@ crunch valid_list [wp, DetSchedSchedule_AI_assms]:
crunch cur_tcb [wp, DetSchedSchedule_AI_assms]: handle_arch_fault_reply, handle_vm_fault cur_tcb
crunch valid_sched [wp, DetSchedSchedule_AI_assms]: handle_hypervisor_fault valid_sched
(ignore:)
crunch not_queued [wp, DetSchedSchedule_AI_assms]: handle_hypervisor_fault "not_queued t"
(ignore:)
crunch sched_act_not [wp, DetSchedSchedule_AI_assms]: handle_hypervisor_fault "scheduler_act_not t"
(ignore:)
end
global_interpretation DetSchedSchedule_AI?: DetSchedSchedule_AI
@ -307,4 +298,19 @@ global_interpretation DetSchedSchedule_AI?: DetSchedSchedule_AI
case 1 show ?case by (unfold_locales; (fact DetSchedSchedule_AI_assms)?)
qed
context Arch begin global_naming X64
lemma handle_hyp_fault_valid_sched[wp]:
"\<lbrace>valid_sched and invs and st_tcb_at active t and not_queued t and scheduler_act_not t\<rbrace>
handle_hypervisor_fault t fault \<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (cases fault; wpsimp wp: handle_fault_valid_sched simp: valid_fault_def)
end
global_interpretation DetSchedSchedule_AI_handle_hypervisor_fault?: DetSchedSchedule_AI_handle_hypervisor_fault
proof goal_cases
interpret Arch .
case 1 show ?case by (unfold_locales; (fact handle_hyp_fault_valid_sched)?)
qed
end

4
proof/invariant-abstract/X64/ArchSyscall_AI.thy
View File

@ -95,7 +95,9 @@ crunch cte_wp_at[wp,Syscall_AI_assms]: handle_arch_fault_reply "\<lambda>s. P (c
lemma hh_invs[wp, Syscall_AI_assms]:
"\<lbrace>invs and ct_active\<rbrace> handle_hypervisor_fault thread fault \<lbrace>\<lambda>rv. invs\<rbrace>"
"\<lbrace>invs and ct_active and st_tcb_at active thread and ex_nonz_cap_to_thread\<rbrace>
handle_hypervisor_fault thread fault
\<lbrace>\<lambda>rv. invs\<rbrace>"
by (cases fault) wpsimp
end