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

x64 refine: proof updates for new arch split functions 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-04-29 16:59:01 +08:00
parent 26a49fcbde
commit 9bf346481e
3 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/refine/X64/DomainTime_R.thy
View File

@ -243,7 +243,7 @@ lemma handleInterrupt_valid_domain_time:
apply (rule_tac B="\<lambda>_ s. 0 < ksDomainTime s" in hoare_seq_ext[rotated])
apply (rule hoare_pre, wp, simp)
apply (rename_tac st)
apply (case_tac st, simp_all)
apply (case_tac st, simp_all add: maskIrqSignal_def)
(* IRQSignal : no timer tick, trivial preservation of ksDomainTime *)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply (rule hoare_pre, (wp | wpc)+)

13
proof/refine/X64/Interrupt_R.thy
View File

@ -364,8 +364,8 @@ lemma invoke_irq_handler_corres:
corres dc (einvs and irq_handler_inv_valid i)
(invs' and irq_handler_inv_valid' i')
(invoke_irq_handler i)
(invokeIRQHandler i')"
apply (cases i, simp_all add: invokeIRQHandler_def)
(InterruptDecls_H.invokeIRQHandler i')"
apply (cases i, simp_all add: Interrupt_H.invokeIRQHandler_def invokeIRQHandler_def)
apply (rule corres_guard_imp, rule corres_machine_op)
apply (rule corres_Id, simp_all)
apply (rule no_fail_maskInterrupt)
@ -438,8 +438,8 @@ lemma ct_in_current_domain_ksMachineState:
lemma invoke_irq_handler_invs'[wp]:
"\<lbrace>invs' and irq_handler_inv_valid' i\<rbrace>
invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (cases i, simp_all add: invokeIRQHandler_def)
InterruptDecls_H.invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (cases i, simp_all add: Interrupt_H.invokeIRQHandler_def invokeIRQHandler_def)
apply (wp dmo_maskInterrupt)
apply (clarsimp simp add: invs'_def valid_state'_def valid_irq_masks'_def
valid_machine_state'_def ct_not_inQ_def
@ -834,7 +834,8 @@ apply (rule corres_split)
apply (case_tac xb, simp_all add: doMachineOp_return)[1]
apply (clarsimp simp add: when_def doMachineOp_return)
apply (rule corres_guard_imp, rule send_signal_corres)
apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind)+
apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind
arch_mask_irq_signal_def maskIrqSignal_def)+
apply ( rule corres_split)
apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
apply ((wp |simp)+)
@ -967,7 +968,7 @@ lemma hint_invs[wp]:
apply (rule conjI; rule impI)
apply (wp dmo_maskInterrupt_True getCTE_wp'
| wpc | simp add: doMachineOp_bind )+
| wpc | simp add: doMachineOp_bind maskIrqSignal_def)+
apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp)
apply (clarsimp simp: cte_wp_at_ctes_of ex_nonz_cap_to'_def)
apply fastforce

4
proof/refine/X64/Syscall_R.thy
View File

@ -525,10 +525,10 @@ crunch typ_at'[wp]: "performIRQControl" "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQControl_typ_ats[wp] =
typ_at_lifts [OF performIRQControl_typ_at']
crunch typ_at'[wp]: invokeIRQHandler "\<lambda>s. P (typ_at' T p s)"
crunch typ_at'[wp]: InterruptDecls_H.invokeIRQHandler "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQHandler_typ_ats[wp] =
typ_at_lifts [OF invokeIRQHandler_typ_at']
typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
crunch tcb_at'[wp]: setDomain "tcb_at' tptr"
(simp: crunch_simps)