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

x64 crefine: 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 18:58:42 +08:00
parent d567d52b17
commit 232b23e314
2 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
proof/crefine/X64/Interrupt_C.thy
View File

@ -13,8 +13,8 @@ context kernel_m begin
lemma invokeIRQHandler_AckIRQ_ccorres:
"ccorres dc xfdc
invs' (UNIV \<inter> {s. irq_' s = ucast irq}) []
(invokeIRQHandler (AckIRQ irq)) (Call invokeIRQHandler_AckIRQ_'proc)"
apply (cinit lift: irq_')
(InterruptDecls_H.invokeIRQHandler (AckIRQ irq)) (Call invokeIRQHandler_AckIRQ_'proc)"
apply (cinit lift: irq_' simp: Interrupt_H.invokeIRQHandler_def invokeIRQHandler_def)
apply (ctac add: maskInterrupt_ccorres)
apply (simp add: from_bool_def false_def)
done
@ -60,13 +60,13 @@ lemma invokeIRQHandler_SetIRQHandler_ccorres:
and irq_handler_inv_valid' (SetIRQHandler irq cp slot))
(UNIV \<inter> {s. irq_' s = ucast irq} \<inter> {s. slot_' s = Ptr slot}
\<inter> {s. ccap_relation cp (cap_' s)}) []
(invokeIRQHandler (SetIRQHandler irq cp slot))
(InterruptDecls_H.invokeIRQHandler (SetIRQHandler irq cp slot))
(Call invokeIRQHandler_SetIRQHandler_'proc)"
proof -
have valid_objs_invs'_strg: "\<And>s. invs' s \<longrightarrow> valid_objs' s"
by (clarsimp)
show ?thesis
apply (cinit lift: irq_' slot_' cap_')
apply (cinit lift: irq_' slot_' cap_' simp: Interrupt_H.invokeIRQHandler_def)
apply (rule ccorres_Guard_intStateIRQNode_array_Ptr)
apply (rule ccorres_move_array_assertion_irq)
apply (simp add: ucast_up_ucast is_up of_int_uint_ucast[symmetric])
@ -103,9 +103,9 @@ lemma invokeIRQHandler_ClearIRQHandler_ccorres:
"ccorres dc xfdc
(invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and K(irq \<le> 0xFF))
(UNIV \<inter> {s. irq_' s = ucast irq}) []
(invokeIRQHandler (ClearIRQHandler irq))
(InterruptDecls_H.invokeIRQHandler (ClearIRQHandler irq))
(Call invokeIRQHandler_ClearIRQHandler_'proc)"
apply (cinit lift: irq_')
apply (cinit lift: irq_' simp: Interrupt_H.invokeIRQHandler_def)
apply (rule ccorres_Guard_intStateIRQNode_array_Ptr)
apply (rule ccorres_move_array_assertion_irq)
apply (simp add: ucast_up_ucast is_up of_int_uint_ucast[symmetric])

6
proof/crefine/X64/Syscall_C.thy
View File

@ -1686,6 +1686,7 @@ lemma handleInterrupt_ccorres:
apply csymbr
apply csymbr
apply (ctac (no_vcg) add: sendSignal_ccorres)
apply (simp add: maskIrqSignal_def)
apply (ctac (no_vcg) add: maskInterrupt_ccorres)
apply (ctac add: ackInterrupt_ccorres [unfolded dc_def])
apply wp+
@ -1694,7 +1695,7 @@ lemma handleInterrupt_ccorres:
apply (rule ccorres_rhs_assoc)+
apply csymbr+
apply (rule ccorres_cond_false_seq)
apply simp
apply (simp add: maskIrqSignal_def)
apply (ctac (no_vcg) add: maskInterrupt_ccorres)
apply (ctac add: ackInterrupt_ccorres [unfolded dc_def])
apply wp
@ -1703,7 +1704,8 @@ lemma handleInterrupt_ccorres:
apply (case_tac rva, simp_all del: Collect_const)[1]
prefer 3
apply metis
apply ((rule ccorres_guard_imp2,
apply ((simp add: maskIrqSignal_def,
rule ccorres_guard_imp2,
rule ccorres_cond_false_seq, simp,
rule ccorres_cond_false_seq, simp,
ctac (no_vcg) add: maskInterrupt_ccorres,