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

autocorres-crefine: update CRefine proofs for AutoCorres

This commit is contained in:
Matthew Brecknell 2017-11-22 10:52:59 +11:00
parent 210465edf3
commit a2dd6d1777
32 changed files with 204 additions and 408 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/ARM/ADT_C.thy
View File

@ -354,7 +354,7 @@ definition
lemma unat_ucast_mask_pageBits_shift:
"unat (ucast (p && mask pageBits >> 2) :: 10 word) = unat ((p::word32) && mask pageBits >> 2)"
apply (simp only: unat_ucast)
apply (rule mod_less)
apply (rule Divides.mod_less)
apply (rule unat_less_power)
apply (simp add: word_bits_def)
apply (rule shiftr_less_t2n)

7
proof/crefine/ARM/Arch_C.thy
View File

@ -471,7 +471,6 @@ shows
del: fun_upd_apply)
apply (erule array_relation_update)
apply (simp add: unat_ucast)
apply (subst mod_less)
apply (drule leq_asid_bits_shift)
apply (simp add: asid_high_bits_def mask_def word_le_nat_alt)
apply simp
@ -3474,7 +3473,7 @@ lemma injection_handler_stateAssert_relocate:
by (simp add: injection_handler_def handleE'_def bind_bindE_assoc bind_assoc)
lemma decodeARMPageDirectoryInvocation_ccorres:
notes if_cong[cong] tl_drop_1[simp]
notes if_cong[cong]
shows
"\<lbrakk> interpret_excaps extraCaps' = excaps_map extraCaps;
isPageDirectoryCap cp \<rbrakk>
@ -3504,8 +3503,8 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
del: Collect_const
cong: StateSpace.state.fold_congs globals.fold_congs
if_cong list.case_cong)
apply (simp add: if_1_0_0 split_def if_to_top_of_bind
del: Collect_const cong: if_cong)
apply (simp add: split_def if_to_top_of_bind
del: Collect_const cong: if_cong)
apply (rule ccorres_rhs_assoc)+
apply csymbr+
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])

11
proof/crefine/ARM/AutoCorresTest.thy
View File

@ -11,10 +11,7 @@
(* Experimental AutoCorres proofs over CRefine: work in progress *)
theory AutoCorresTest
imports (* Frameworks and tactics *)
"../../../lib/clib/AutoCorres_C"
(* import Refine_C last to minimise change to global context *)
Refine_C
imports Refine_C
begin
section \<open>Simple test case: handleYield\<close>
@ -84,7 +81,7 @@ lemma reorder_gets:
(do g;
x \<leftarrow> gets f;
h x od)"
by (fastforce simp: bind_def' valid_def gets_def get_def return_def)
by (fastforce simp: bind_def' NonDetMonad.valid_def gets_def get_def return_def)
thm
(* no arguments, no precondition, dc return *)
@ -107,7 +104,7 @@ lemma (* handleYield_ccorres: *)
(* Show that current thread is unmodified.
* FIXME: proper way to do this? *)
apply (subst reorder_gets[symmetric, unfolded K_bind_def])
using tcbSchedDequeue'_modifies apply (fastforce simp: valid_def)
using tcbSchedDequeue'_modifies apply (fastforce simp: NonDetMonad.valid_def)
apply (subst gets_gets)
apply (rule corres_pre_getCurThread_wrapper)
apply (rule corres_split[OF _ tcbSchedDequeue_ccorres[ac]])
@ -153,7 +150,7 @@ lemma corres_noop2_no_exs:
apply (clarsimp simp: corres_underlying_def)
apply (rule conjI)
apply (drule x, drule y)
apply (clarsimp simp: valid_def empty_fail_def Ball_def Bex_def)
apply (clarsimp simp: NonDetMonad.valid_def empty_fail_def Ball_def Bex_def)
apply fast
apply (insert z)
apply (clarsimp simp: no_fail_def)

64
proof/crefine/ARM/CSpace_C.thy
View File

@ -1080,31 +1080,26 @@ lemma setUntypedCapAsFull_ccorres [corres]:
apply (frule(1) cte_wp_at_valid_objs_valid_cap')
apply clarsimp
apply (intro conjI impI allI)
apply (erule cte_wp_at_weakenE')
apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm)
apply clarsimp
apply (drule valid_cap_untyped_inv,clarsimp simp:max_free_index_def)
apply (rule is_aligned_weaken)
apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
apply assumption
apply (clarsimp simp: max_free_index_def shiftL_nat valid_cap'_def capAligned_def)
apply (simp add:power_minus_is_div unat_power_lower unat_sub word_le_nat_alt t2p_shiftr)
apply clarsimp
apply (erule cte_wp_at_weakenE', simp)
apply clarsimp
apply (drule valid_cap_untyped_inv)
apply (clarsimp simp:max_free_index_def t2p_shiftr unat_sub word_le_nat_alt)
apply (clarsimp simp:field_simps)
apply (rule word_less_imp_diff_less)
apply (subst (asm) eq_commute, fastforce simp: unat_sub word_le_nat_alt)
apply (rule capBlockSize_CL_maxSize)
apply (clarsimp simp: cap_get_tag_UntypedCap)
apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (erule cte_wp_at_weakenE')
apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm)
apply clarsimp
apply (drule valid_cap_untyped_inv,clarsimp simp:max_free_index_def)
apply (rule is_aligned_weaken)
apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
apply assumption
apply (clarsimp simp: max_free_index_def shiftL_nat valid_cap'_def capAligned_def)
apply (simp add:power_minus_is_div unat_power_lower unat_sub word_le_nat_alt t2p_shiftr)
apply clarsimp
apply (erule cte_wp_at_weakenE', simp)
apply clarsimp
apply (drule valid_cap_untyped_inv)
apply (clarsimp simp:max_free_index_def t2p_shiftr unat_sub word_le_nat_alt)
apply (clarsimp simp:field_simps)
apply (rule word_less_imp_diff_less)
apply (subst (asm) eq_commute, fastforce simp: unat_sub word_le_nat_alt)
apply (rule capBlockSize_CL_maxSize)
apply (clarsimp simp: cap_get_tag_UntypedCap)
apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap)
done
lemma ccte_lift:
@ -1178,16 +1173,15 @@ lemma cteInsert_ccorres:
\<inter> {s. destSlot_' s = Ptr dest} \<inter> {s. srcSlot_' s = Ptr src} \<inter> {s. ccap_relation cap (newCap_' s)}) []
(cteInsert cap src dest)
(Call cteInsert_'proc)"
thm cteInsert_body_def
apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_'
simp del: return_bind simp add: Collect_const)
simp del: return_bind
simp add: Collect_const)
apply (rule ccorres_move_c_guard_cte)
apply (ctac pre: ccorres_pre_getCTE)
apply (rule ccorres_move_c_guard_cte)
apply (ctac pre: ccorres_pre_getCTE)
apply csymbr
apply (fold revokable'_fold)
apply (simp (no_asm) only: if_distrib [where f="scast"] scast_1_32 scast_0)
apply (ctac add: revokable_ccorres)
apply (ctac (c_lines 3) add: cteInsert_ccorres_mdb_helper)
apply (simp del: Collect_const)
@ -2237,11 +2231,6 @@ show ?thesis
apply (clarsimp simp: word_sless_msb_less order_le_less_trans
unat_ucast_no_overflow_le word_le_nat_alt ucast_ucast_b
split: if_split )
apply (rule word_0_sle_from_less)
apply (rule order_less_le_trans[where y = 160])
apply (simp add: unat_ucast_no_overflow_le)
apply simp
apply ceqv
apply (ctac add: maskInterrupt_ccorres)
@ -2790,8 +2779,6 @@ lemma gen_framesize_to_H_is_framesize_to_H_if_not_ARMSmallPage:
" c\<noteq>scast Kernel_C.ARMSmallPage \<Longrightarrow>gen_framesize_to_H c = framesize_to_H c"
by (simp add: gen_framesize_to_H_def framesize_to_H_def)
lemma Arch_sameRegionAs_spec:
"\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace> ccap_relation (ArchObjectCap capa) \<acute>cap_a \<and>
ccap_relation (ArchObjectCap capb) \<acute>cap_b \<rbrace>
@ -2860,7 +2847,6 @@ lemma Arch_sameRegionAs_spec:
apply (simp add: gen_framesize_to_H_def)
apply (simp add: Let_def)
apply (clarsimp simp: if_distrib [where f="scast"])
apply (simp add: cap_get_tag_PageCap_small_frame [unfolded cap_tag_defs, simplified])
apply (thin_tac "ccap_relation x cap_b" for x)
apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(16)[simplified], simp)
@ -2890,7 +2876,6 @@ lemma Arch_sameRegionAs_spec:
apply (simp add: c_valid_cap_def cl_valid_cap_def)
apply (simp add: Let_def)
apply (clarsimp simp: if_distrib [where f=scast])
apply (simp add: cap_get_tag_PageCap_frame [unfolded cap_tag_defs, simplified])
apply (thin_tac "ccap_relation x cap_b" for x)
apply (frule cap_get_tag_isCap_unfolded_H_cap(16)[simplified, where cap'=cap_a], simp)
@ -3729,7 +3714,6 @@ lemma sameObjectAs_spec:
-- "capa is an arch cap"
apply (frule cap_get_tag_isArchCap_unfolded_H_cap)
apply (simp add: isArchCap_tag_def2)
apply (simp add: if_1_0_0)
apply (rule conjI, rule impI, clarsimp, rule impI)+
apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
isCap_simps cap_tag_defs)[1]
@ -3739,7 +3723,7 @@ lemma sameObjectAs_spec:
apply (fastforce simp: isArchCap_tag_def2 linorder_not_less [symmetric])+
-- "capa is an irq handler cap"
apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
isCap_simps cap_tag_defs if_1_0_0)
isCap_simps cap_tag_defs)
apply fastforce+
-- "capb is an arch cap"
apply (frule cap_get_tag_isArchCap_unfolded_H_cap)
@ -3866,7 +3850,7 @@ lemma isMDBParentOf_spec:
apply clarsimp
apply (simp add: Let_def case_bool_If)
apply (frule_tac cap="(cap_to_H x2c)" in cap_get_tag_NotificationCap)
apply (simp add: if_1_0_0 if_distrib [where f=scast])
apply clarsimp
-- " main goal"
apply clarsimp

6
proof/crefine/ARM/Delete_C.thy
View File

@ -146,14 +146,13 @@ lemma capRemovable_spec:
apply (clarsimp simp: cap_get_tag_isCap(1-8)[THEN trans[OF eq_commute]])
apply (simp add: capRemovable_def from_bool_def[where b=True] true_def)
apply (clarsimp simp: ccap_zombie_radix_less4)
apply (clarsimp simp: if_distrib [where f=scast])
apply (subst eq_commute, subst from_bool_eq_if)
apply (rule exI, rule conjI, assumption)
apply clarsimp
apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap[THEN iffD2])
apply (case_tac slot)
apply (clarsimp simp: get_capZombiePtr_CL_def Let_def get_capZombieBits_CL_def
isCap_simps unat_eq_0 unat_eq_1
isCap_simps unat_eq_1
less_mask_eq ccap_zombie_radix_less2
split: if_split_asm)
done
@ -163,9 +162,8 @@ lemma capCyclicZombie_spec:
Call capCyclicZombie_'proc
{s'. ret__unsigned_long_' s' = from_bool (capCyclicZombie cap (ptr_val (slot_' s)))}"
apply vcg
apply (clarsimp simp: if_1_0_0 from_bool_0)
apply (clarsimp simp: from_bool_0)
apply (frule(1) cap_get_tag_isCap [THEN iffD2], simp)
apply (clarsimp simp: if_distrib [where f=scast])
apply (subst eq_commute, subst from_bool_eq_if)
apply (simp add: ccap_zombie_radix_less4)
apply (case_tac slot, simp)

2
proof/crefine/ARM/Finalise_C.thy
View File

@ -1160,7 +1160,7 @@ lemma deleteASID_ccorres:
apply (simp add: asid_high_bits_of_def
asidLowBits_def Kernel_C.asidLowBits_def
asid_low_bits_def unat_ucast)
apply (rule sym, rule mod_less)
apply (rule sym, rule Divides.mod_less)
apply (rule unat_less_power[where sz=7, simplified])
apply (simp add: word_bits_conv)
apply (rule shiftr_less_t2n[where m=7, simplified])

6
proof/crefine/ARM/Interrupt_C.thy
View File

@ -36,9 +36,7 @@ lemma getIRQSlot_ccorres:
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cinterrupt_relation_def size_of_def
sint_ucast_eq_uint is_down of_int_uint_ucast
cte_level_bits_def mult.commute mult.left_commute ucast_nat_def
)
apply (simp add:ucast_up_ucast is_up)
cte_level_bits_def mult.commute mult.left_commute ucast_nat_def)
done
lemma ptr_add_assertion_irq_guard:
@ -325,7 +323,7 @@ lemma invokeIRQControl_ccorres:
lemma unat_ucast_16_32:
"unat (ucast (x::(16 word))::32 signed word) = unat x"
apply (subst unat_ucast)
apply (rule mod_less)
apply (rule Divides.mod_less)
apply (rule less_le_trans[OF unat_lt2p])
apply simp
done

6
proof/crefine/ARM/Invoke_C.thy
View File

@ -3343,12 +3343,6 @@ shows
valid_untyped_capBlockSize_misc
valid_untyped_capBlockSize_misc[where z=0, simplified]
of_nat_shiftR)
apply (clarsimp simp:toEnum_object_type_to_H
unat_of_nat_APIType_capBits word_size hd_conv_nth length_ineq_not_Nil
split:if_splits)
apply (clarsimp simp:toEnum_object_type_to_H
unat_of_nat_APIType_capBits word_size hd_conv_nth length_ineq_not_Nil
split:if_splits)
apply (rule syscall_error_throwError_ccorres_n)
apply (case_tac reset; clarsimp simp: syscall_error_rel_def
ccap_relation_untyped_CL_simps shiftL_nat

2
proof/crefine/ARM/IpcCancel_C.thy
View File

@ -48,7 +48,7 @@ proof -
using prems
by (simp add: numDomains_def maxDom_def Suc_le_lessD unat_le_helper)
show ?thesis
using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] mod_less[OF Q]
using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] Q
by (clarsimp simp: cready_queues_index_to_C_def field_simps numDomains_def)
qed

29
proof/crefine/ARM/Ipc_C.thy
View File

@ -1899,10 +1899,10 @@ proof -
apply (rule ccorres_return_Skip[simplified dc_def])
apply (clarsimp)
apply (rule hoare_impI)
apply (wp mapM_x_wp_inv setMR_atcbContext_obj_at[simplified atcbContextGet_def, simplified]
| clarsimp
| wpc)+
apply (cases recvBuffer; simp add: option_to_0_def )
apply (rule mapM_x_wp_inv)
apply (cases recvBuffer; simp add: option_to_0_def split_def)
apply (erule hoare_vcg_conj_lift
[OF setMR_atcbContext_obj_at[simplified atcbContextGet_def, simplified]])
apply wp
apply (clarsimp simp: guard_is_UNIV_def n_msgRegisters_def msgLengthBits_def
mask_def)+
@ -2853,13 +2853,8 @@ proof (rule ccorres_gen_asm, induct caps arbitrary: n slots mi)
apply vcg
apply (rule conseqPre, vcg, clarsimp)
apply (simp add: seL4_MsgExtraCapBits_def)
apply (clarsimp simp: excaps_map_def seL4_MsgExtraCapBits_def word_sle_def
precond_def)
apply (subst (asm) interpret_excaps_test_null)
apply (simp add: unat_of_nat)
apply (simp add: unat_of_nat)
apply (erule le_neq_trans, clarsimp)
apply (simp add: unat_of_nat)
apply (clarsimp simp: excaps_map_def seL4_MsgExtraCapBits_def word_sle_def precond_def)
apply (subst interpret_excaps_test_null; clarsimp simp: unat_of_nat elim!: le_neq_trans)
done
next
note if_split[split]
@ -2953,6 +2948,7 @@ next
note if_split[split del]
note if_cong[cong]
note extra_sle_sless_unfolds [simp del]
note sle_positive[simp del]
from Cons.prems
show ?case
apply (clarsimp simp: Let_def word_sle_def[where b=5] split_def
@ -3217,6 +3213,7 @@ lemma lookupExtraCaps_srcs2:
lemma transferCaps_ccorres [corres]:
notes if_cong[cong]
notes extra_sle_sless_unfolds[simp del]
notes sle_positive[simp del]
shows
"ccorres (\<lambda>r r'. r = message_info_to_H r') ret__struct_seL4_MessageInfo_C_'
(valid_pspace' and tcb_at' receiver
@ -3242,7 +3239,6 @@ lemma transferCaps_ccorres [corres]:
apply (clarsimp simp: option_to_0_def getReceiveSlots_def
simp del: Collect_const)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_const_guards)+
apply (simp (no_asm))
apply (rule_tac R'=UNIV in ccorres_split_throws [OF ccorres_return_C], simp_all)[1]
apply vcg
@ -3252,7 +3248,6 @@ lemma transferCaps_ccorres [corres]:
apply (clarsimp simp: interpret_excaps_test_null excaps_map_def
simp del: Collect_const not_None_eq)
apply (erule notE, rule ccorres_guard_imp2)
apply (rule ccorres_move_const_guards)+
apply (simp (no_asm))
apply (rule ccorres_symb_exec_l)
apply (rule_tac R'=UNIV in ccorres_split_throws [OF ccorres_return_C], simp_all)[1]
@ -3270,8 +3265,6 @@ lemma transferCaps_ccorres [corres]:
simp del: Collect_const
cong: call_ignore_cong)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_const_guards)+
apply (simp (no_asm) only: ccorres_seq_cond_empty ccorres_seq_skip)
apply (ctac add: getReceiveSlots_ccorres)
apply (elim conjE)
apply (rule ccorres_symb_exec_r)
@ -4458,11 +4451,7 @@ proof (rule hoare_gen_asm, induct caps arbitrary: x mi destSlots)
next
case (Cons cp cps)
show ?case using Cons.prems
apply (clarsimp simp: Let_def split del: if_split)
apply (rule hoare_pre)
apply (wp Cons.hyps cteInsert_weak_cte_wp_at2
| wpc | simp add: weak whenE_def split del: if_split)+
done
by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak)
qed
lemma transferCaps_local_slots:

7
proof/crefine/ARM/Retype_C.thy
View File

@ -846,12 +846,7 @@ lemma ptr_add_orth:
apply (drule unat_cong)
apply (simp only: unat_of_nat)
apply (unfold word_bits_len_of)
apply (subst (asm) mod_less)
apply (erule order_less_trans)
apply (simp add: addr_card_wb [symmetric])
apply (subst (asm) mod_less)
apply simp
apply simp
apply (simp add: addr_card_wb [symmetric])
done
lemma dom_lift_t_heap_update:

8
proof/crefine/ARM/Schedule_C.thy
View File

@ -108,7 +108,6 @@ crunch valid_queues'[wp]: "Arch.switchToThread" valid_queues'
(ignore: clearExMonitor)
crunch ksCurDomain[wp]: switchToIdleThread "\<lambda>s. P (ksCurDomain s)"
crunch valid_pspace'[wp]: switchToIdleThread, switchToThread valid_pspace'
(simp: whenE_def)
crunch valid_arch_state'[wp]: switchToThread valid_arch_state'
end
@ -516,9 +515,8 @@ proof -
have b[simp]:
"\<And>w. unat (of_nat (word_log2 (w :: machine_word)) :: machine_word) = word_log2 w"
by (fastforce simp add: unat_of_nat
intro: mod_less order_less_le_trans[OF word_log2_max_word32])
by (fastforce simp: unat_of_nat
intro: Divides.mod_less order_less_le_trans[OF word_log2_max_word32])
have unat_ucast_d[simp]:
"\<And>d. d \<le> maxDomain \<Longrightarrow> unat (ucast d * 0x100 :: machine_word) = unat d * 256"
by (subst unat_mult_simple)
@ -536,7 +534,7 @@ proof -
apply (simp add: word_size)
apply (subst uint_nat)
apply (simp add: unat_of_nat)
apply (subst mod_less)
apply (subst Divides.mod_less)
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (rule iffD2 [OF le_nat_iff[symmetric]])

2
proof/crefine/ARM/StoreWord_C.thy
View File

@ -512,7 +512,6 @@ proof (intro allI impI)
"unat offset = unat (ptr && mask pageBits >> 2)"
apply (simp add: offset_def)
apply (simp add: unat_ucast)
apply (rule mod_less)
apply (simp add: word_less_nat_alt)
done
@ -821,7 +820,6 @@ proof (intro allI impI)
"unat offset = unat (ptr && mask pageBits >> 2)"
apply (simp add: offset_def)
apply (simp add: unat_ucast)
apply (rule mod_less)
apply (simp add: word_less_nat_alt)
done

49
proof/crefine/ARM/Syscall_C.thy
View File

@ -632,8 +632,7 @@ lemma sendFaultIPC_ccorres:
in ccorres_cond_both')
apply clarsimp
apply (frule cap_get_tag_isCap(4)[symmetric],
clarsimp simp: cap_get_tag_EndpointCap to_bool_def
split:if_splits)
fastforce simp: cap_get_tag_EndpointCap to_bool_def)
apply (rule ccorres_rhs_assoc)
apply (rule ccorres_rhs_assoc)
@ -1757,28 +1756,16 @@ lemma scast_maxIRQ_is_less:
apply fastforce
done
lemma validIRQcastingLess: "Kernel_C.maxIRQ <s (ucast((ucast (b :: irq))::word16)) \<Longrightarrow> ARM.maxIRQ < b"
by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size)
lemma validIRQcastingLess: "Kernel_C.maxIRQ <s (ucast((ucast (b :: irq))::word16)) \<Longrightarrow> ARM.maxIRQ < b"
by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size)
lemma scast_maxIRQ_is_not_less: "(\<not> (Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b) \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)"
apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<ge> sint (ucast (ucast b))";
(simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def )?)
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subst (asm) sint_ucast_uint[where b=b and 'c = 32 and 'b = 16 and uc=ucast and uc' = ucast and uuc = "ucast \<circ> ucast" , simplified];
(simp add: is_up_def target_size source_size)?)
apply (subst (asm) uint_is_up_compose[where 'b = 16 and uuc="ucast \<circ> ucast", simplified];
(simp add: is_up_def target_size source_size)?)
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subst (asm) (2) sint_ucast_uint_pred[where 'a = 10 and 'b = 16 and 'c = 32 and uuc = "ucast \<circ> ucast", simplified,symmetric ];
((simp add: is_up_def target_size source_size)?))
apply (subst sint_ucast_uint_pred[where 'a = 10 and 'b = 16 and 'c = 32 and uuc = "ucast \<circ> ucast", simplified,symmetric ];
((simp add: is_up_def target_size source_size)?))
apply (subst (asm) (2) uint_is_up_compose[where 'b = 16 and uuc="ucast \<circ> ucast", simplified];
(simp add: is_up_def target_size source_size)?)
apply (uint_arith)
simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def)
apply (uint_arith)
apply (subst (asm) sint_ucast_uint[where b=b and 'c=32 and 'b=16 and uc=ucast and uc'=ucast and uuc="ucast \<circ> ucast", simplified];
simp add: is_up_def target_size source_size)
apply (cases "sint maxIRQ \<le> sint (UCAST(10 \<rightarrow> 32 signed) b)"; simp add: maxIRQ_def sint_uint)
done
lemma ccorres_handleReserveIRQ:
@ -1827,8 +1814,6 @@ lemma handleInterrupt_ccorres:
apply (rule getIRQSlot_ccorres3)
apply (rule ccorres_getSlotCap_cte_at)
apply (rule_tac P="cte_at' rv" in ccorres_cross_over_guard)
apply (rule ptr_add_assertion_irq_guard[unfolded dc_def])
apply (rule ccorres_move_array_assertion_irq ccorres_move_c_guard_cte)+
apply ctac
apply csymbr
apply csymbr
@ -1890,16 +1875,16 @@ lemma handleInterrupt_ccorres:
apply (ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def])
apply wp
apply vcg
apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up )
apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up)
apply (clarsimp simp: word_sless_alt word_less_alt word_le_def Kernel_C.maxIRQ_def
uint_up_ucast is_up_def
source_size_def target_size_def word_size
sint_ucast_eq_uint is_down is_up word_0_sle_from_less)
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_ctes_of )
apply (clarsimp simp add: if_1_0_0 Collect_const_mem )
apply (clarsimp simp: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def
cte_wp_at_ctes_of ucast_ucast_b is_up)
apply (clarsimp simp: cte_wp_at_ctes_of)
using un_ui_le[of irq maxIRQ]
apply (clarsimp simp: IRQTimer_def IRQSignal_def maxIRQ_def
cte_wp_at_ctes_of ucast_ucast_b is_up)
apply (intro conjI impI)
apply clarsimp
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
@ -1909,14 +1894,10 @@ lemma handleInterrupt_ccorres:
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (frule cap_get_tag_to_H, assumption)
apply (clarsimp simp: to_bool_def)
apply (cut_tac un_ui_le[where b = 159 and a = irq,
simplified word_size])
apply (simp add: ucast_eq_0 is_up_def source_size_def
target_size_def word_size unat_gt_0
| subst array_assertion_abs_irq[rule_format, OF conjI])+
apply (fastforce simp: unat_gt_0 intro!: array_assertion_abs_irq[rule_format])
apply (erule exE conjE)+
apply (erule(1) rf_sr_cte_at_valid[OF ctes_of_cte_at])
apply (clarsimp simp:nat_le_iff)
apply (fastforce simp: unat_gt_0 intro!: array_assertion_abs_irq[rule_format])
apply (clarsimp simp: IRQReserved_def)+
done
end

41
proof/crefine/ARM/Tcb_C.thy
View File

@ -17,12 +17,8 @@ lemma asUser_obj_at' :
including no_pre
apply (simp add: asUser_def)
apply wp
apply (simp add: split_def)
apply (wp threadSet_obj_at'_strongish)+
apply (case_tac "t=t'")
apply clarsimp
apply clarsimp
apply (rule hoare_drop_imps)+
apply (case_tac "t=t'"; clarsimp)
apply (rule hoare_drop_imps)
apply wp
done
@ -679,7 +675,6 @@ lemma invokeTCB_ThreadControl_ccorres:
apply csymbr
apply (simp add: ccorres_cond_iffs Collect_False split_def
del: Collect_const)
apply (simp only: if_1_0_0 simp_thms)
apply (rule ccorres_Cond_rhs_Seq)
(* P *)
apply (rule ccorres_rhs_assoc)+
@ -688,13 +683,13 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (rule checkCapAt_ccorres)
apply ceqv
apply csymbr
apply (simp add: if_1_0_0 true_def Collect_True
apply (simp add: true_def Collect_True
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule checkCapAt_ccorres)
apply ceqv
apply csymbr
apply (simp add: if_1_0_0 true_def Collect_True
apply (simp add: true_def Collect_True
del: Collect_const)
apply (simp add: assertDerived_def bind_assoc del: Collect_const)
apply (rule ccorres_symb_exec_l)
@ -716,7 +711,7 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (strengthen sch_act_wf_weak, wp)
apply (wp empty_fail_stateAssert hoare_case_option_wp | simp del: Collect_const)+
apply csymbr
apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs
apply (simp add: false_def Collect_False ccorres_cond_iffs
del: Collect_const)
apply (rule ccorres_pre_getCurThread)
apply (simp add: when_def to_bool_def)
@ -731,11 +726,10 @@ lemma invokeTCB_ThreadControl_ccorres:
apply wp
apply (clarsimp simp: guard_is_UNIV_def)
apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
tcb_ptr_to_ctcb_ptr_mask tcbBuffer_def
size_of_def cte_level_bits_def
tcbBuffer_def size_of_def cte_level_bits_def
tcbIPCBufferSlot_def)
apply csymbr
apply (simp add: if_1_0_0 Collect_False false_def
apply (simp add: Collect_False false_def
del: Collect_const)
apply (rule ccorres_cond_false_seq, simp)
apply (rule ccorres_pre_getCurThread)
@ -749,8 +743,7 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (rule ccorres_return_CE, simp+)
apply wp
apply (clarsimp simp: guard_is_UNIV_def)
apply (simp add: guard_is_UNIV_def if_1_0_0 false_def
Collect_const_mem)
apply (simp add: guard_is_UNIV_def false_def Collect_const_mem)
apply (clarsimp simp: ccap_relation_def cap_thread_cap_lift cap_to_H_def)
(* \<not>P *)
apply simp
@ -852,13 +845,13 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (rule checkCapAt_ccorres2)
apply ceqv
apply csymbr
apply (simp add: if_1_0_0 true_def Collect_True
apply (simp add: true_def Collect_True
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule checkCapAt_ccorres2)
apply ceqv
apply csymbr
apply (simp add: if_1_0_0 true_def Collect_True
apply (simp add: true_def Collect_True
assertDerived_def bind_assoc
ccorres_cond_iffs dc_def[symmetric]
del: Collect_const)
@ -867,14 +860,14 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (wp empty_fail_stateAssert
hoare_case_option_wp | simp del: Collect_const)+
apply csymbr
apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs
apply (simp add: false_def Collect_False ccorres_cond_iffs
del: Collect_const)
apply (rule ccorres_return_Skip[unfolded dc_def])
apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
tcbVTable_def tcbVTableSlot_def
cte_level_bits_def size_of_def option_to_0_def)
apply csymbr
apply (simp add: if_1_0_0 false_def Collect_False
apply (simp add: false_def Collect_False
del: Collect_const)
apply (rule ccorres_cond_false)
apply (rule ccorres_return_Skip[unfolded dc_def])
@ -916,7 +909,7 @@ lemma invokeTCB_ThreadControl_ccorres:
checkCap_inv [where P="sch_act_simple"]
| simp)+
apply (clarsimp simp: guard_is_UNIV_def from_bool_def true_def
word_sle_def if_1_0_0 Collect_const_mem
word_sle_def Collect_const_mem
option_to_0_def Kernel_C.tcbVTable_def tcbVTableSlot_def
cte_level_bits_def size_of_def cintr_def
tcb_cnode_index_defs)
@ -925,13 +918,13 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (rule checkCapAt_ccorres2)
apply ceqv
apply csymbr
apply (simp add: if_1_0_0 true_def Collect_True
apply (simp add: true_def Collect_True
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule checkCapAt_ccorres2)
apply ceqv
apply csymbr
apply (simp add: if_1_0_0 true_def Collect_True
apply (simp add: true_def Collect_True
assertDerived_def bind_assoc
ccorres_cond_iffs dc_def[symmetric]
del: Collect_const)
@ -941,14 +934,14 @@ lemma invokeTCB_ThreadControl_ccorres:
hoare_case_option_wp
| simp del: Collect_const)+
apply csymbr
apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs
apply (simp add: false_def Collect_False ccorres_cond_iffs
del: Collect_const)
apply (rule ccorres_return_Skip[unfolded dc_def])
apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
Kernel_C.tcbCTable_def tcbCTableSlot_def
cte_level_bits_def size_of_def option_to_0_def)
apply csymbr
apply (simp add: if_1_0_0 false_def Collect_False
apply (simp add: false_def Collect_False
del: Collect_const)
apply (rule ccorres_cond_false)
apply (rule ccorres_return_Skip[unfolded dc_def])

4
proof/crefine/ARM/VSpace_C.thy
View File

@ -2934,8 +2934,8 @@ lemma performPageInvocationUnmap_ccorres:
apply (drule ccap_relation_mapped_asid_0)
apply (frule ctes_of_valid', clarsimp)
apply (drule valid_global_refsD_with_objSize, clarsimp)
apply (clarsimp simp: mask_def valid_cap'_def
vmsz_aligned_aligned_pageBits)
apply (fastforce simp: mask_def valid_cap'_def
vmsz_aligned_aligned_pageBits)
apply assumption
apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split)
apply (drule diminished_PageCap)

2
proof/crefine/ARM_HYP/ADT_C.thy
View File

@ -376,7 +376,7 @@ definition
lemma unat_ucast_mask_pageBits_shift:
"unat (ucast (p && mask pageBits >> 2) :: 10 word) = unat ((p::word32) && mask pageBits >> 2)"
apply (simp only: unat_ucast)
apply (rule mod_less)
apply (rule Divides.mod_less)
apply (rule unat_less_power)
apply (simp add: word_bits_def)
apply (rule shiftr_less_t2n)

2
proof/crefine/ARM_HYP/Arch_C.thy
View File

@ -492,7 +492,7 @@ shows
del: fun_upd_apply)
apply (erule array_relation_update)
apply (simp add: unat_ucast)
apply (subst mod_less)
apply (subst Divides.mod_less)
apply (drule leq_asid_bits_shift)
apply (simp add: asid_high_bits_def mask_def word_le_nat_alt)
apply simp

183
proof/crefine/ARM_HYP/AutoCorresTest.thy
View File

@ -11,10 +11,7 @@
(* Experimental AutoCorres proofs over CRefine: work in progress *)
theory AutoCorresTest
imports (* Frameworks and tactics *)
AutoCorres_C
(* import Refine_C last to minimise change to global context *)
Refine_C
imports Refine_C
begin
section \<open>Simple test case: handleYield\<close>
@ -22,7 +19,7 @@ section \<open>Simple test case: handleYield\<close>
autocorres
[
skip_heap_abs, skip_word_abs, (* for compatibility *)
scope = handleYield,
scope = handleYield doReplyTransfer,
scope_depth = 0,
c_locale = kernel_all_substitute,
no_c_termination
@ -31,15 +28,10 @@ autocorres
context kernel_m begin
text \<open>Export corres_underlying rules for handleYield's callees.\<close>
thm getCurThread_ccorres
lemma getCurThread_wrapper_corres:
"corres_underlying {(x, y). cstate_relation x y} True True (\<lambda>ct ct'. tcb_ptr_to_ctcb_ptr ct = ct') invs' (\<lambda>_. True) getCurThread (gets ksCurThread_')"
by (simp add: getCurThread_def cstate_relation_def Let_def)
thm ccorres_pre_getCurThread
lemma corres_pre_getCurThread_wrapper:
assumes cc: "\<And>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv \<Longrightarrow>
corres_underlying {(x, y). cstate_relation x y} True True R (P rv) (P' rv) (f rv) (f' rv')"
assumes cc: "\<And>rv. corres_underlying {(x, y). cstate_relation x y} True True R (P rv) (P' rv)
(f rv) (f' (tcb_ptr_to_ctcb_ptr rv))"
shows "corres_underlying {(x, y). cstate_relation x y} True True R
(\<lambda>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> P rv s)
(\<lambda>s. \<forall>rv. ksCurThread_' s = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> P' rv s)
@ -51,38 +43,6 @@ lemma corres_pre_getCurThread_wrapper:
apply (clarsimp simp: cstate_relation_def Let_def)
done
thm tcbSchedDequeue_ccorres
lemma tcbSchedDequeue_wrapper_corres:
"tcb_ptr_to_ctcb_ptr ct = ct' \<Longrightarrow>
corres_underlying {(x, y). cstate_relation x y} True True (op=)
(Invariants_H.valid_queues and valid_queues' and tcb_at' ct and valid_objs') \<top>
(tcbSchedDequeue ct) (tcbSchedDequeue' ct')"
apply (rule ccorres_to_corres_no_termination)
apply (simp add: tcbSchedDequeue'_def)
apply (clarsimp simp: ccorres_rrel_nat_unit tcbSchedDequeue_ccorres[simplified])
done
thm tcbSchedAppend_ccorres
lemma tcbSchedAppend_wrapper_corres:
"tcb_ptr_to_ctcb_ptr ct = ct' \<Longrightarrow>
corres_underlying {(x, y). cstate_relation x y} True True (op=)
(Invariants_H.valid_queues and tcb_at' ct and valid_objs') \<top>
(tcbSchedAppend ct) (tcbSchedAppend' ct')"
apply (rule ccorres_to_corres_no_termination)
apply (simp add: tcbSchedAppend'_def)
apply (clarsimp simp: ccorres_rrel_nat_unit tcbSchedAppend_ccorres[simplified])
done
thm rescheduleRequired_ccorres
lemma rescheduleRequired_wrapper_corres:
"corres_underlying {(x, y). cstate_relation x y} True True (op=)
(Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') \<top>
rescheduleRequired rescheduleRequired'"
apply (rule ccorres_to_corres_no_termination)
apply (simp add: rescheduleRequired'_def)
apply (clarsimp simp: ccorres_rrel_nat_unit rescheduleRequired_ccorres[simplified])
done
text \<open>
Proving handleYield_ccorres via handleYield'.
The handleYield spec has one less getCurThread, so we need to use the fact
@ -102,7 +62,7 @@ lemma (* handleYield_ccorres: *)
apply cinit
apply (rule ccorres_pre_getCurThread)
apply (ctac add: tcbSchedDequeue_ccorres)
apply (ctac add: tcbSchedAppend_ccorres)
apply (ctac add: tcbSchedAppend_ccorres)
apply (ctac add: rescheduleRequired_ccorres)
apply (wp weak_sch_act_wf_lift_linear tcbSchedAppend_valid_objs')
apply (vcg exspec= tcbSchedAppend_modifies)
@ -110,7 +70,7 @@ lemma (* handleYield_ccorres: *)
apply (vcg exspec= tcbSchedDequeue_modifies)
apply (clarsimp simp: tcb_at_invs' invs_valid_objs'
valid_objs'_maxPriority valid_objs'_maxDomain)
apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def valid_objs'_maxDomain)
apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def)
done
lemma reorder_gets:
@ -121,7 +81,15 @@ lemma reorder_gets:
(do g;
x \<leftarrow> gets f;
h x od)"
by (fastforce simp: bind_def' valid_def gets_def get_def return_def)
by (fastforce simp: bind_def' NonDetMonad.valid_def gets_def get_def return_def)
thm
(* no arguments, no precondition, dc return *)
rescheduleRequired_ccorres rescheduleRequired_ccorres[ac]
(* one argument, simple precondition, dc return *)
tcbSchedDequeue_ccorres tcbSchedDequeue_ccorres[ac]
(* multiple arguments, complex precondition, non-dc return *)
handleFaultReply_ccorres handleFaultReply_ccorres[ac]
text \<open>Now the proof.\<close>
lemma (* handleYield_ccorres: *)
@ -131,33 +99,23 @@ lemma (* handleYield_ccorres: *)
[]
(handleYield)
(Call handleYield_'proc)"
apply (rule ac_corres_to_ccorres)
apply (rule kernel_all_substitute.handleYield'_ac_corres)
apply simp
apply (simp add: handleYield_def handleYield'_def)
apply (rule corres_guard_imp)
(* Show that current thread is unmodified.
* FIXME: proper way to do this? *)
apply (subst reorder_gets[symmetric, unfolded K_bind_def])
using tcbSchedDequeue'_modifies apply (fastforce simp: valid_def)
apply (subst gets_gets)
apply (rule corres_pre_getCurThread_wrapper)
apply (rule corres_split[OF _ tcbSchedDequeue_wrapper_corres])
apply (rule corres_split[OF _ tcbSchedAppend_wrapper_corres])
apply (rule rescheduleRequired_wrapper_corres)
apply (solves simp)
apply (solves \<open>wp tcbSchedAppend_valid_objs' weak_sch_act_wf_lift_linear | simp\<close>)+
apply (solves \<open>wp tcbSchedDequeue_invs' tcbSchedDequeue_typ_at'
tcbSchedDequeue_valid_queues tcbSchedDequeue_valid_objs'
weak_sch_act_wf_lift_linear\<close>)
apply (solves wp)
apply (clarsimp simp: invs_valid_objs' invs_queues invs_valid_queues' tcb_at_invs'
valid_objs'_maxPriority valid_objs'_maxDomain)
apply (fastforce simp: obj_at'_def st_tcb_at'_def ct_in_state'_def dest: ct_active_runnable')
apply fastforce
done
apply (ac_init)
apply (simp add: handleYield_def handleYield'_def)
(* Show that current thread is unmodified.
* FIXME: proper way to do this? *)
apply (subst reorder_gets[symmetric, unfolded K_bind_def])
using tcbSchedDequeue'_modifies apply (fastforce simp: NonDetMonad.valid_def)
apply (subst gets_gets)
apply (rule corres_pre_getCurThread_wrapper)
apply (rule corres_split[OF _ tcbSchedDequeue_ccorres[ac]])
apply (rule corres_split[OF _ tcbSchedAppend_ccorres[ac]])
apply (rule rescheduleRequired_ccorres[ac])
apply (solves \<open>wp tcbSchedAppend_valid_objs' weak_sch_act_wf_lift
tcbSchedDequeue_valid_queues
| simp\<close>)+
apply (clarsimp simp: invs_valid_objs' tcb_at_invs'
valid_objs'_maxPriority valid_objs'_maxDomain)
by (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def)
end
@ -176,30 +134,7 @@ autocorres
context kernel_m begin
local_setup \<open>AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ARCH/kernel_all.c_pp"\<close>
text \<open>Export corres_underlying rules for handleDoubleFault's callees.\<close>
thm setThreadState_ccorres[no_vars]
lemma setThreadState_wrapper_corres:
"(\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts && mask 4\<rparr>, fl)) \<and>
tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow>
corres_underlying {(x, y). cstate_relation x y} True True (op=)
(\<lambda>s. tcb_at' thread s \<and>
Invariants_H.valid_queues s \<and>
valid_objs' s \<and>
valid_tcb_state' st s \<and>
(ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s) \<top>
(setThreadState st thread) (setThreadState' tptr ts)"
apply (rule ccorres_to_corres_no_termination)
apply (simp add: setThreadState'_def)
apply (clarsimp simp: ccorres_rrel_nat_unit)
using setThreadState_ccorres
apply (fastforce simp: ccorres_underlying_def Ball_def)
done
text \<open>Extra corres_underlying rules.\<close>
lemma corres_gen_asm':
"\<lbrakk> corres_underlying sr nf nf' r Q P' f g; \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; P' s' \<rbrakk> \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow>
corres_underlying sr nf nf' r P P' f g"
by (fastforce simp: corres_underlying_def)
lemma corres_add_noop_rhs2:
"corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> g; return () od)
@ -215,7 +150,7 @@ lemma corres_noop2_no_exs:
apply (clarsimp simp: corres_underlying_def)
apply (rule conjI)
apply (drule x, drule y)
apply (clarsimp simp: valid_def empty_fail_def Ball_def Bex_def)
apply (clarsimp simp: NonDetMonad.valid_def empty_fail_def Ball_def Bex_def)
apply fast
apply (insert z)
apply (clarsimp simp: no_fail_def)
@ -252,7 +187,7 @@ lemma (* handleDoubleFault_ccorres: *)
apply (ctac (no_vcg))
apply (rule ccorres_symb_exec_l)
apply (rule ccorres_return_Skip)
apply (wp asUser_inv getRestartPC_inv)
apply (wp asUser_inv getRestartPC_inv)+
apply (rule empty_fail_asUser)
apply (simp add: getRestartPC_def)
apply wp
@ -261,6 +196,7 @@ lemma (* handleDoubleFault_ccorres: *)
apply (fastforce simp: valid_tcb_state'_def)
done
text \<open>New proof of handleDoubleFault\<close>
lemma (* handleDoubleFault_ccorres: *)
"ccorres dc xfdc (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and
@ -268,31 +204,23 @@ lemma (* handleDoubleFault_ccorres: *)
(UNIV \<inter> {s. ex1_' s = ex1' \<and> tptr_' s = tcb_ptr_to_ctcb_ptr tptr})
[] (handleDoubleFault tptr ex1 ex2)
(Call handleDoubleFault_'proc)"
apply (rule ac_corres_to_ccorres[where R="op="])
apply (rule handleDoubleFault'_ac_corres)
apply (simp add: pred_conj_def)
apply (unfold handleDoubleFault_def handleDoubleFault'_def)
apply (simp only: K_bind_def) -- "normalise"
apply (rule corres_add_noop_rhs2) -- "split out extra haskell code"
apply (rule corres_split')
(* call setThreadState *)
apply (rule corres_gen_asm')
apply (rule setThreadState_wrapper_corres)
apply (simp add: ThreadState_Inactive_def)
apply (fastforce simp: valid_tcb_state'_def ThreadState_Inactive_def)
(* extra haskell code *)
apply simp
apply (rule corres_symb_exec_l_no_exs)
apply simp
apply (rule conjI)
apply (wp asUser_inv getRestartPC_inv)
apply (wp empty_fail_asUser)[1]
apply (rule hoare_TrueI)
apply (simp add: getRestartPC_def)
apply ac_init
prefer 3 apply simp
apply (unfold handleDoubleFault_def handleDoubleFault'_def K_bind_def)
apply (rule corres_add_noop_rhs2) -- "split out extra haskell code"
apply (rule corres_split[OF _ setThreadState_ccorres[ac]])
apply (rule corres_symb_exec_l_no_exs)
apply simp
apply (rule conjI)
apply (wp asUser_inv getRestartPC_inv)
apply (wp empty_fail_asUser)
apply (rule hoare_TrueI)
apply (wpsimp simp: getRestartPC_def)
apply simp
apply (simp add: ThreadState_Inactive_def)
apply wp
apply simp
apply (rule hoare_TrueI)
done
apply (rule hoare_TrueI)
by (fastforce simp: valid_tcb_state'_def)
end
@ -518,7 +446,8 @@ lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
\<lbrace>\<lambda>r _. r = capCNodePtr_CL (cap_cnode_cap_lift cap)\<rbrace>!"
apply (unfold cap_cnode_cap_get_capCNodePtr'_def)
apply wp
apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values shiftr_over_and_dist)
apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values
shiftr_over_and_dist mask_def)
done
lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
@ -526,7 +455,8 @@ lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
\<lbrace>\<lambda>r _. r = capCNodeGuard_CL (cap_cnode_cap_lift cap)\<rbrace>!"
apply (unfold cap_cnode_cap_get_capCNodeGuard'_def)
apply wp
apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values shiftr_over_and_dist)
apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values
shiftr_over_and_dist mask_def)
done
lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
@ -534,7 +464,8 @@ lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
\<lbrace>\<lambda>r _. r = capCNodeRadix_CL (cap_cnode_cap_lift cap)\<rbrace>!"
apply (unfold cap_cnode_cap_get_capCNodeRadix'_def)
apply wp
apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values shiftr_over_and_dist)
apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values
shiftr_over_and_dist mask_def)
done
end

62
proof/crefine/ARM_HYP/CSpace_C.thy
View File

@ -1080,31 +1080,26 @@ lemma setUntypedCapAsFull_ccorres [corres]:
apply (frule(1) cte_wp_at_valid_objs_valid_cap')
apply clarsimp
apply (intro conjI impI allI)
apply (erule cte_wp_at_weakenE')
apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm)
apply clarsimp
apply (drule valid_cap_untyped_inv,clarsimp simp:max_free_index_def)
apply (rule is_aligned_weaken)
apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
apply assumption
apply (clarsimp simp: max_free_index_def shiftL_nat valid_cap'_def capAligned_def)
apply (simp add:power_minus_is_div unat_power_lower unat_sub word_le_nat_alt t2p_shiftr)
apply clarsimp
apply (erule cte_wp_at_weakenE', simp)
apply clarsimp
apply (drule valid_cap_untyped_inv)
apply (clarsimp simp:max_free_index_def t2p_shiftr unat_sub word_le_nat_alt)
apply (clarsimp simp:field_simps)
apply (rule word_less_imp_diff_less)
apply (subst (asm) eq_commute, fastforce simp: unat_sub word_le_nat_alt)
apply (rule capBlockSize_CL_maxSize)
apply (clarsimp simp: cap_get_tag_UntypedCap)
apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (clarsimp split: if_split_asm)
apply (erule cte_wp_at_weakenE')
apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm)
apply clarsimp
apply (drule valid_cap_untyped_inv,clarsimp simp:max_free_index_def)
apply (rule is_aligned_weaken)
apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
apply assumption
apply (clarsimp simp: max_free_index_def shiftL_nat valid_cap'_def capAligned_def)
apply (simp add:power_minus_is_div unat_sub word_le_nat_alt t2p_shiftr)
apply clarsimp
apply (erule cte_wp_at_weakenE', simp)
apply clarsimp
apply (drule valid_cap_untyped_inv)
apply (clarsimp simp:max_free_index_def t2p_shiftr unat_sub word_le_nat_alt)
apply (clarsimp simp:field_simps)
apply (rule word_less_imp_diff_less)
apply (subst (asm) eq_commute, fastforce simp: unat_sub word_le_nat_alt)
apply (rule capBlockSize_CL_maxSize)
apply (clarsimp simp: cap_get_tag_UntypedCap)
apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap)
done
lemma ccte_lift:
@ -1176,16 +1171,15 @@ lemma cteInsert_ccorres:
\<inter> {s. destSlot_' s = Ptr dest} \<inter> {s. srcSlot_' s = Ptr src} \<inter> {s. ccap_relation cap (newCap_' s)}) []
(cteInsert cap src dest)
(Call cteInsert_'proc)"
thm cteInsert_body_def
apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_'
simp del: return_bind simp add: Collect_const)
simp del: return_bind
simp add: Collect_const)
apply (rule ccorres_move_c_guard_cte)
apply (ctac pre: ccorres_pre_getCTE)
apply (rule ccorres_move_c_guard_cte)
apply (ctac pre: ccorres_pre_getCTE)
apply csymbr
apply (fold revokable'_fold)
apply (simp (no_asm) only: if_distrib [where f="scast"] scast_1_32 scast_0)
apply (ctac add: revokable_ccorres)
apply (ctac (c_lines 3) add: cteInsert_ccorres_mdb_helper)
apply (simp del: Collect_const)
@ -2235,11 +2229,6 @@ show ?thesis
apply (clarsimp simp: word_sless_msb_less order_le_less_trans
unat_ucast_no_overflow_le word_le_nat_alt ucast_ucast_b
split: if_split )
apply (rule word_0_sle_from_less)
apply (rule order_less_le_trans[where y = 192])
apply (simp add: unat_ucast_no_overflow_le)
apply simp
apply ceqv
apply (ctac add: maskInterrupt_ccorres)
@ -2861,7 +2850,6 @@ lemma Arch_sameRegionAs_spec:
apply (simp add: gen_framesize_to_H_def)
apply (simp add: Let_def)
apply (clarsimp simp: if_distrib [where f="scast"])
apply (simp add: cap_get_tag_PageCap_small_frame [unfolded cap_tag_defs, simplified])
apply (thin_tac "ccap_relation x cap_b" for x)
apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(16)[simplified], simp)
@ -2891,7 +2879,6 @@ lemma Arch_sameRegionAs_spec:
apply (simp add: c_valid_cap_def cl_valid_cap_def)
apply (simp add: Let_def)
apply (clarsimp simp: if_distrib [where f=scast])
apply (simp add: cap_get_tag_PageCap_frame [unfolded cap_tag_defs, simplified])
apply (thin_tac "ccap_relation x cap_b" for x)
apply (frule cap_get_tag_isCap_unfolded_H_cap(16)[simplified, where cap'=cap_a], simp)
@ -3759,7 +3746,6 @@ lemma sameObjectAs_spec:
-- "capa is an arch cap"
apply (frule cap_get_tag_isArchCap_unfolded_H_cap)
apply (simp add: isArchCap_tag_def2)
apply (simp add: if_1_0_0)
apply (rule conjI, rule impI, clarsimp, rule impI)+
apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
isCap_simps cap_tag_defs)[1]
@ -3769,7 +3755,7 @@ lemma sameObjectAs_spec:
apply (fastforce simp: isArchCap_tag_def2 linorder_not_less [symmetric])+
-- "capa is an irq handler cap"
apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap
isCap_simps cap_tag_defs if_1_0_0)
isCap_simps cap_tag_defs)
apply fastforce+
-- "capb is an arch cap"
apply (frule cap_get_tag_isArchCap_unfolded_H_cap)
@ -3896,7 +3882,7 @@ lemma isMDBParentOf_spec:
apply clarsimp
apply (simp add: Let_def case_bool_If)
apply (frule_tac cap="(cap_to_H x2c)" in cap_get_tag_NotificationCap)
apply (simp add: if_1_0_0 if_distrib [where f=scast])
apply clarsimp
-- " main goal"
apply clarsimp

6
proof/crefine/ARM_HYP/Delete_C.thy
View File

@ -146,14 +146,13 @@ lemma capRemovable_spec:
apply (clarsimp simp: cap_get_tag_isCap(1-8)[THEN trans[OF eq_commute]])
apply (simp add: capRemovable_def from_bool_def[where b=True] true_def)
apply (clarsimp simp: ccap_zombie_radix_less4)
apply (clarsimp simp: if_distrib [where f=scast])
apply (subst eq_commute, subst from_bool_eq_if)
apply (rule exI, rule conjI, assumption)
apply clarsimp
apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap[THEN iffD2])
apply (case_tac slot)
apply (clarsimp simp: get_capZombiePtr_CL_def Let_def get_capZombieBits_CL_def
isCap_simps unat_eq_0 unat_eq_1
isCap_simps unat_eq_1
less_mask_eq ccap_zombie_radix_less2
split: if_split_asm)
done
@ -163,9 +162,8 @@ lemma capCyclicZombie_spec:
Call capCyclicZombie_'proc
{s'. ret__unsigned_long_' s' = from_bool (capCyclicZombie cap (ptr_val (slot_' s)))}"
apply vcg
apply (clarsimp simp: if_1_0_0 from_bool_0)
apply (clarsimp simp: from_bool_0)
apply (frule(1) cap_get_tag_isCap [THEN iffD2], simp)
apply (clarsimp simp: if_distrib [where f=scast])
apply (subst eq_commute, subst from_bool_eq_if)
apply (simp add: ccap_zombie_radix_less4)
apply (case_tac slot, simp)

2
proof/crefine/ARM_HYP/Finalise_C.thy
View File

@ -1160,7 +1160,7 @@ lemma deleteASID_ccorres:
apply (simp add: asid_high_bits_of_def
asidLowBits_def Kernel_C.asidLowBits_def
asid_low_bits_def unat_ucast)
apply (rule sym, rule mod_less)
apply (rule sym, rule Divides.mod_less)
apply (rule unat_less_power[where sz=7, simplified])
apply (simp add: word_bits_conv)
apply (rule shiftr_less_t2n[where m=7, simplified])

6
proof/crefine/ARM_HYP/Interrupt_C.thy
View File

@ -36,9 +36,7 @@ lemma getIRQSlot_ccorres:
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cinterrupt_relation_def size_of_def
sint_ucast_eq_uint is_down of_int_uint_ucast
cte_level_bits_def mult.commute mult.left_commute ucast_nat_def
)
apply (simp add:ucast_up_ucast is_up)
cte_level_bits_def mult.commute mult.left_commute ucast_nat_def)
done
lemma ptr_add_assertion_irq_guard:
@ -325,7 +323,7 @@ lemma invokeIRQControl_ccorres:
lemma unat_ucast_16_32:
"unat (ucast (x::(16 word))::32 signed word) = unat x"
apply (subst unat_ucast)
apply (rule mod_less)
apply (rule Divides.mod_less)
apply (rule less_le_trans[OF unat_lt2p])
apply simp
done

6
proof/crefine/ARM_HYP/Invoke_C.thy
View File

@ -3346,12 +3346,6 @@ shows
valid_untyped_capBlockSize_misc
valid_untyped_capBlockSize_misc[where z=0, simplified]
of_nat_shiftR)
apply (clarsimp simp:toEnum_object_type_to_H
unat_of_nat_APIType_capBits word_size hd_conv_nth length_ineq_not_Nil
split:if_splits)
apply (clarsimp simp:toEnum_object_type_to_H
unat_of_nat_APIType_capBits word_size hd_conv_nth length_ineq_not_Nil
split:if_splits)
apply (rule syscall_error_throwError_ccorres_n)
apply (case_tac reset; clarsimp simp: syscall_error_rel_def
ccap_relation_untyped_CL_simps shiftL_nat

2
proof/crefine/ARM_HYP/IpcCancel_C.thy
View File

@ -48,7 +48,7 @@ proof -
using prems
by (simp add: numDomains_def maxDom_def Suc_le_lessD unat_le_helper)
show ?thesis
using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] mod_less[OF Q]
using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] Q
by (clarsimp simp: cready_queues_index_to_C_def field_simps numDomains_def)
qed

29
proof/crefine/ARM_HYP/Ipc_C.thy
View File

@ -1917,10 +1917,10 @@ proof -
apply (rule ccorres_return_Skip[simplified dc_def])
apply (clarsimp)
apply (rule hoare_impI)
apply (wp mapM_x_wp_inv setMR_atcbContext_obj_at[simplified atcbContextGet_def, simplified]
| clarsimp
| wpc)+
apply (cases recvBuffer; simp add: option_to_0_def )
apply (rule mapM_x_wp_inv)
apply (cases recvBuffer; simp add: option_to_0_def split_def)
apply (erule hoare_vcg_conj_lift
[OF setMR_atcbContext_obj_at[simplified atcbContextGet_def, simplified]])
apply wp
apply (clarsimp simp: guard_is_UNIV_def n_msgRegisters_def msgLengthBits_def
mask_def)+
@ -3014,13 +3014,8 @@ proof (rule ccorres_gen_asm, induct caps arbitrary: n slots mi)
apply vcg
apply (rule conseqPre, vcg, clarsimp)
apply (simp add: seL4_MsgExtraCapBits_def)
apply (clarsimp simp: excaps_map_def seL4_MsgExtraCapBits_def word_sle_def
precond_def)
apply (subst (asm) interpret_excaps_test_null)
apply (simp add: unat_of_nat)
apply (simp add: unat_of_nat)
apply (erule le_neq_trans, clarsimp)
apply (simp add: unat_of_nat)
apply (clarsimp simp: excaps_map_def seL4_MsgExtraCapBits_def word_sle_def precond_def)
apply (subst interpret_excaps_test_null; clarsimp simp: unat_of_nat elim!: le_neq_trans)
done
next
note if_split[split]
@ -3114,6 +3109,7 @@ next
note if_split[split del]
note if_cong[cong]
note extra_sle_sless_unfolds [simp del]
note sle_positive[simp del]
from Cons.prems
show ?case
apply (clarsimp simp: Let_def word_sle_def[where b=5] split_def
@ -3378,6 +3374,7 @@ lemma lookupExtraCaps_srcs2:
lemma transferCaps_ccorres [corres]:
notes if_cong[cong]
notes extra_sle_sless_unfolds[simp del]
notes sle_positive[simp del]
shows
"ccorres (\<lambda>r r'. r = message_info_to_H r') ret__struct_seL4_MessageInfo_C_'
(valid_pspace' and tcb_at' receiver
@ -3403,7 +3400,6 @@ lemma transferCaps_ccorres [corres]:
apply (clarsimp simp: option_to_0_def getReceiveSlots_def
simp del: Collect_const)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_const_guards)+
apply (simp (no_asm))
apply (rule_tac R'=UNIV in ccorres_split_throws [OF ccorres_return_C], simp_all)[1]
apply vcg
@ -3413,7 +3409,6 @@ lemma transferCaps_ccorres [corres]:
apply (clarsimp simp: interpret_excaps_test_null excaps_map_def
simp del: Collect_const not_None_eq)
apply (erule notE, rule ccorres_guard_imp2)
apply (rule ccorres_move_const_guards)+
apply (simp (no_asm))
apply (rule ccorres_symb_exec_l)
apply (rule_tac R'=UNIV in ccorres_split_throws [OF ccorres_return_C], simp_all)[1]
@ -3431,8 +3426,6 @@ lemma transferCaps_ccorres [corres]:
simp del: Collect_const
cong: call_ignore_cong)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_const_guards)+
apply (simp (no_asm) only: ccorres_seq_cond_empty ccorres_seq_skip)
apply (ctac add: getReceiveSlots_ccorres)
apply (elim conjE)
apply (rule ccorres_symb_exec_r)
@ -4650,11 +4643,7 @@ proof (rule hoare_gen_asm, induct caps arbitrary: x mi destSlots)
next
case (Cons cp cps)
show ?case using Cons.prems
apply (clarsimp simp: Let_def split del: if_split)
apply (rule hoare_pre)
apply (wp Cons.hyps cteInsert_weak_cte_wp_at2
| wpc | simp add: weak whenE_def split del: if_split)+
done
by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak)
qed
lemma transferCaps_local_slots:

4
proof/crefine/ARM_HYP/Schedule_C.thy
View File

@ -514,7 +514,7 @@ proof -
have b[simp]:
"\<And>w. unat (of_nat (word_log2 (w :: machine_word)) :: machine_word) = word_log2 w"
by (fastforce simp add: unat_of_nat
intro: mod_less order_less_le_trans[OF word_log2_max_word32])
intro: Divides.mod_less order_less_le_trans[OF word_log2_max_word32])
have unat_ucast_d[simp]:
"\<And>d. d \<le> maxDomain \<Longrightarrow> unat (ucast d * 0x100 :: machine_word) = unat d * 256"
@ -533,7 +533,7 @@ proof -
apply (simp add: word_size)
apply (subst uint_nat)
apply (simp add: unat_of_nat)
apply (subst mod_less)
apply (subst Divides.mod_less)
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (rule iffD2 [OF le_nat_iff[symmetric]])

2
proof/crefine/ARM_HYP/StoreWord_C.thy
View File

@ -490,7 +490,6 @@ proof (intro allI impI)
"unat offset = unat (ptr && mask pageBits >> 2)"
apply (simp add: offset_def)
apply (simp add: unat_ucast)
apply (rule mod_less)
apply (simp add: word_less_nat_alt)
done
@ -799,7 +798,6 @@ proof (intro allI impI)
"unat offset = unat (ptr && mask pageBits >> 2)"
apply (simp add: offset_def)
apply (simp add: unat_ucast)
apply (rule mod_less)
apply (simp add: word_less_nat_alt)
done

44
proof/crefine/ARM_HYP/Syscall_C.thy
View File

@ -632,8 +632,7 @@ lemma sendFaultIPC_ccorres:
in ccorres_cond_both')
apply clarsimp
apply (frule cap_get_tag_isCap(4)[symmetric],
clarsimp simp: cap_get_tag_EndpointCap to_bool_def
split:if_splits)
fastforce simp: cap_get_tag_EndpointCap to_bool_def)
apply (rule ccorres_rhs_assoc)
apply (rule ccorres_rhs_assoc)
@ -1764,21 +1763,12 @@ lemma validIRQcastingLess:
lemma scast_maxIRQ_is_not_less:
"(\<not> (Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b) \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)"
apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<ge> sint (ucast (ucast b))";
(simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def )?)
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subst (asm) sint_ucast_uint[where b=b and 'c = 32 and 'b = 16 and uc=ucast and uc' = ucast and uuc = "ucast \<circ> ucast" , simplified];
(simp add: is_up_def target_size source_size)?)
apply (subst (asm) uint_is_up_compose[where 'b = 16 and uuc="ucast \<circ> ucast", simplified];
(simp add: is_up_def target_size source_size)?)
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subst (asm) (2) sint_ucast_uint_pred[where 'a = 10 and 'b = 16 and 'c = 32 and uuc = "ucast \<circ> ucast", simplified,symmetric ];
((simp add: is_up_def target_size source_size)?))
apply (subst sint_ucast_uint_pred[where 'a = 10 and 'b = 16 and 'c = 32 and uuc = "ucast \<circ> ucast", simplified,symmetric ];
((simp add: is_up_def target_size source_size)?))
apply (subst (asm) (2) uint_is_up_compose[where 'b = 16 and uuc="ucast \<circ> ucast", simplified];
(simp add: is_up_def target_size source_size)?)
apply (uint_arith)
done
simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def)
apply (uint_arith)
apply (subst (asm) sint_ucast_uint[where b=b and 'c=32 and 'b=16 and uc=ucast and uc'=ucast and uuc="ucast \<circ> ucast", simplified];
simp add: is_up_def target_size source_size)
apply (cases "sint maxIRQ \<le> sint (UCAST(10 \<rightarrow> 32 signed) b)"; simp add: maxIRQ_def sint_uint)
done
(* FIXME ARMHYP: move *)
lemma ctzl_spec:
@ -2300,8 +2290,6 @@ lemma handleInterrupt_ccorres:
apply (rule getIRQSlot_ccorres3)
apply (rule ccorres_getSlotCap_cte_at)
apply (rule_tac P="cte_at' rv" in ccorres_cross_over_guard)
apply (rule ptr_add_assertion_irq_guard[unfolded dc_def])
apply (rule ccorres_move_array_assertion_irq ccorres_move_c_guard_cte)+
apply ctac
apply csymbr
apply csymbr
@ -2363,16 +2351,16 @@ lemma handleInterrupt_ccorres:
apply (ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def])
apply wp
apply (vcg exspec=handleReservedIRQ_modifies)
apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up )
apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up)
apply (clarsimp simp: word_sless_alt word_less_alt word_le_def Kernel_C.maxIRQ_def
uint_up_ucast is_up_def
source_size_def target_size_def word_size
sint_ucast_eq_uint is_down is_up word_0_sle_from_less)
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_ctes_of non_kernel_IRQs_def irqVGICMaintenance_def)
apply (clarsimp simp add: if_1_0_0 Collect_const_mem )
apply (clarsimp simp: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def
cte_wp_at_ctes_of ucast_ucast_b is_up)
apply (clarsimp simp: cte_wp_at_ctes_of)
using un_ui_le[of irq maxIRQ]
apply (clarsimp simp: IRQTimer_def IRQSignal_def maxIRQ_def
cte_wp_at_ctes_of ucast_ucast_b is_up)
apply (intro conjI impI)
apply clarsimp
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
@ -2382,14 +2370,10 @@ lemma handleInterrupt_ccorres:
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (frule cap_get_tag_to_H, assumption)
apply (clarsimp simp: to_bool_def)
apply (cut_tac un_ui_le[where b = 191 and a = irq,
simplified word_size])
apply (simp add: ucast_eq_0 is_up_def source_size_def
target_size_def word_size unat_gt_0
| subst array_assertion_abs_irq[rule_format, OF conjI])+
apply (fastforce simp: unat_gt_0 intro!: array_assertion_abs_irq[rule_format])
apply (erule exE conjE)+
apply (erule(1) rf_sr_cte_at_valid[OF ctes_of_cte_at])
apply (clarsimp simp:nat_le_iff)
apply (fastforce simp: unat_gt_0 intro!: array_assertion_abs_irq[rule_format])
apply (clarsimp simp: IRQReserved_def)+
done
end

9
proof/crefine/ARM_HYP/Tcb_C.thy
View File

@ -17,12 +17,8 @@ lemma asUser_obj_at' :
including no_pre
apply (simp add: asUser_def)
apply wp
apply (simp add: split_def)
apply (wp threadSet_obj_at'_strongish)+
apply (case_tac "t=t'")
apply clarsimp
apply clarsimp
apply (rule hoare_drop_imps)+
apply (case_tac "t=t'"; clarsimp)
apply (rule hoare_drop_imps)
apply wp
done
@ -694,7 +690,6 @@ lemma invokeTCB_ThreadControl_ccorres:
apply csymbr
apply (simp add: ccorres_cond_iffs Collect_False split_def
del: Collect_const)
apply (simp only: if_1_0_0 simp_thms)
apply (rule ccorres_Cond_rhs_Seq)
(* P *)
apply (rule ccorres_rhs_assoc)+

4
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -3704,8 +3704,8 @@ lemma performPageInvocationUnmap_ccorres:
apply (drule ccap_relation_mapped_asid_0)
apply (frule ctes_of_valid', clarsimp)
apply (drule valid_global_refsD_with_objSize, clarsimp)
apply (clarsimp simp: mask_def valid_cap'_def
vmsz_aligned_aligned_pageBits)
apply (fastforce simp: mask_def valid_cap'_def
vmsz_aligned_aligned_pageBits)
apply assumption
apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split)
apply (drule diminished_PageCap)

3
proof/infoflow/ADT_IF_Refine_C.thy
View File

@ -141,7 +141,7 @@ lemma handleInterrupt_ccorres:
(handleInterruptEntry_C_body_if)"
proof -
have ucast_not_helper_cheating_unsigned:
"\<And>a. ucast (a::10 word) \<noteq> (0xFFFF :: word16) \<Longrightarrow> ucast (ucast a :: word16) \<noteq> (0xFFFF::32 word)"
"\<And>a. ucast (a::10 word) \<noteq> (0xFFFF :: word16) \<Longrightarrow> ucast a \<noteq> (0xFFFF::32 word)"
by (word_bitwise)
show ?thesis
apply (rule ccorres_guard_imp2)
@ -597,7 +597,6 @@ lemma check_active_irq_corres_C:
apply (rule corres_guard_imp)
apply (rule corres_split[where r'="\<lambda>a c. case a of None \<Rightarrow> c = 0xFFFF | Some x \<Rightarrow> c = ucast x \<and> c \<noteq> 0xFFFF", OF _ ccorres_corres_u_xf])
apply (clarsimp split: if_split option.splits)
apply (rule ucast_ucast_id[symmetric], simp)
apply (rule ccorres_guard_imp)
apply (rule ccorres_rel_imp, rule ccorres_guard_imp)
apply (rule getActiveIRQ_ccorres)