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

arm crefine: proof updates for bitfield generator changes 

The name mangling of "v" changes in a few places, and mask_def is
occasionally needed where it wasn't before.
This commit is contained in:
Gerwin Klein 2017-09-14 17:27:19 +10:00
parent 15076ecda6
commit 564359b13e
13 changed files with 53 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -913,7 +913,7 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (subst is_aligned_neg_mask [OF _ order_refl],
rule is_aligned_addrFromPPtr_n,
rule is_aligned_andI2,
simp add: is_aligned_def,
simp add: is_aligned_def mask_def,
simp)+
apply (clarsimp simp: attribsFromWord_def split: if_split)
apply word_bitwise
@ -4473,7 +4473,7 @@ lemma Arch_decodeInvocation_ccorres:
apply (clarsimp simp: cap_lift_asid_pool_cap cap_lift_page_directory_cap
cap_to_H_def to_bool_def valid_cap'_def
cap_page_directory_cap_lift_def
cap_asid_pool_cap_lift_def mask_def[where n=4]
cap_asid_pool_cap_lift_def mask_def
asid_shiftr_low_bits_less[unfolded mask_def asid_bits_def] word_and_le1
elim!: ccap_relationE split: if_split_asm)
apply (clarsimp split: list.split)

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

@ -609,7 +609,7 @@ lemma ccorres_updateMDB_set_mdbNext [corres]:
"src=src' \<Longrightarrow>
ccorres dc xfdc ((\<lambda>_. src \<noteq> 0 \<and> (dest\<noteq>0 \<longrightarrow> is_aligned dest 3)))
({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter>
{s. v_' s = dest}) []
{s. v32_' s = dest}) []
(updateMDB src (mdbNext_update (\<lambda>_. dest)))
(Call mdb_node_ptr_set_mdbNext_'proc)"
unfolding updateMDB_def
@ -619,7 +619,7 @@ lemma ccorres_updateMDB_set_mdbNext [corres]:
apply simp
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE [where P = "\<lambda>cte s. ctes_of s src' = Some cte" and
P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v = dest\<rbrace>)"])
P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>)"])
apply (rule ccorres_from_spec_modifies_heap)
apply (rule mdb_node_ptr_set_mdbNext_spec)
apply (rule mdb_node_ptr_set_mdbNext_modifies)
@ -642,7 +642,7 @@ lemma ccorres_updateMDB_set_mdbNext [corres]:
apply (erule (2) cspace_cte_relation_upd_mdbI)
apply (simp add: cmdbnode_relation_def)
subgoal for _ s' by (cases "v_' s' = 0"; simp)
subgoal for _ s' by (cases "v32_' s' = 0"; simp)
apply (erule_tac t = s'a in ssubst)
apply simp
@ -657,7 +657,7 @@ lemma ccorres_updateMDB_set_mdbPrev [corres]:
"src=src' \<Longrightarrow>
ccorres dc xfdc ((\<lambda>_. src \<noteq> 0 \<and> (dest\<noteq>0 \<longrightarrow>is_aligned dest 3)) )
({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter>
{s. v_' s = dest}) []
{s. v32_' s = dest}) []
(updateMDB src (mdbPrev_update (\<lambda>_. dest)))
(Call mdb_node_ptr_set_mdbPrev_'proc)"
unfolding updateMDB_def
@ -667,7 +667,7 @@ lemma ccorres_updateMDB_set_mdbPrev [corres]:
apply simp
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE [where P = "\<lambda>cte s. ctes_of s src' = Some cte" and
P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v = dest\<rbrace>)"])
P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = dest\<rbrace>)"])
apply (rule ccorres_from_spec_modifies_heap)
apply (rule mdb_node_ptr_set_mdbPrev_spec)
apply (rule mdb_node_ptr_set_mdbPrev_modifies)
@ -690,7 +690,7 @@ lemma ccorres_updateMDB_set_mdbPrev [corres]:
apply (erule (2) cspace_cte_relation_upd_mdbI)
apply (simp add: cmdbnode_relation_def)
subgoal for _ s' by (cases "v_' s' = 0"; simp)
subgoal for _ s' by (cases "v32_' s' = 0"; simp)
apply (erule_tac t = s'a in ssubst)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff typ_heap_simps')
@ -839,7 +839,7 @@ lemma update_freeIndex:
"ccorres dc xfdc
(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = UntypedCap d p sz i) srcSlot
and (\<lambda>_. is_aligned (of_nat i' :: word32) 4 \<and> i' \<le> 2 ^ sz))
(UNIV \<inter> {s. cap_ptr_' s = Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])} \<inter> {s. v_' s = (of_nat (i') :: word32)>> 4})
(UNIV \<inter> {s. cap_ptr_' s = Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])} \<inter> {s. v32_' s = (of_nat (i') :: word32)>> 4})
[] (updateCap srcSlot (UntypedCap d p sz i'))
(Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)"
apply (rule ccorres_gen_asm)
@ -882,10 +882,10 @@ proof -
(of_nat i' >> 4 << 6) && ~~ mask 6 >>
5) &&
1) \<and>
cap_C.words_C x1.[Suc 0] && 0x1F =
cap_C.words_C x1.[Suc 0] && mask 5 =
(cap_C.words_C x1.[Suc 0] && 0x3F ||
(of_nat i' >> 4 << 6) && ~~ mask 6) &&
0x1F \<and>
(of_nat i' >> 4 << 6) && ~~ mask 6) && mask 5
\<and>
i' =
unat
((cap_C.words_C x1.[Suc 0] && 0x3F ||
@ -913,11 +913,12 @@ proof -
done
note option.case_cong_weak [cong]
note mask_def [of "Suc 0", simp]
show "ccorresG rf_sr \<Gamma> dc xfdc (cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot)
(UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v = (of_nat i' :: word32) >> 4\<rbrace>) []
(UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = (of_nat i' :: word32) >> 4\<rbrace>) []
(updateCap srcSlot (capability.UntypedCap d p sz i')) (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)"
apply (cinit lift: cap_ptr_' v_')
apply (cinit lift: cap_ptr_' v32_')
apply (rule ccorres_pre_getCTE)
apply (rule_tac P = "\<lambda>s. ctes_of s srcSlot = Some rv \<and> (\<exists>i. cteCap rv = UntypedCap d p sz i)" in
ccorres_from_vcg[where P' = UNIV])
@ -986,7 +987,7 @@ lemma capBlockSize_CL_maxSize:
apply (clarsimp simp: cap_lift_def)
apply (clarsimp simp: cap_untyped_cap_def cap_null_cap_def)
apply (rule word_and_less')
apply simp
apply (simp add: mask_def)
done
lemma t2p_shiftr:
@ -1276,7 +1277,7 @@ lemma updateMDB_mdbNext_set_mdbPrev:
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr (mdbNext_CL (mdb_node_lift mdbc)) :: cte_C ptr)\<rbrace>
(call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbNext_CL (mdb_node_lift mdbc)):: cte_C ptr
\<rightarrow>[''cteMDBNode_C'']),
v_' := ptr_val slotc |))
v32_' := ptr_val slotc |))
mdb_node_ptr_set_mdbPrev_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a)))
FI)"
apply (rule ccorres_guard_imp2) -- "replace preconditions by schematics"
@ -1312,7 +1313,7 @@ lemma updateMDB_mdbPrev_set_mdbNext:
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr)\<rbrace>
(call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr
\<rightarrow>[''cteMDBNode_C'']),
v_' := ptr_val slotc |))
v32_' := ptr_val slotc |))
mdb_node_ptr_set_mdbNext_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a)))
FI)"
apply (rule ccorres_guard_imp2) -- "replace preconditions by schematics"
@ -2769,11 +2770,7 @@ lemma is_aligned_small_frame_cap_lift:
"cap_get_tag cap = scast cap_small_frame_cap \<Longrightarrow>
is_aligned (cap_small_frame_cap_CL.capFBasePtr_CL
(cap_small_frame_cap_lift cap)) 12"
apply (simp add: cap_small_frame_cap_lift_def
cap_lift_small_frame_cap)
apply (rule is_aligned_andI2)
apply (simp add: is_aligned_def)
done
by (simp add: cap_small_frame_cap_lift_def cap_lift_small_frame_cap)
lemma fff_is_pageBits:
"(0xFFF :: word32) = 2 ^ pageBits - 1"
@ -3260,7 +3257,7 @@ lemma get_capSizeBits_valid_shift:
apply (clarsimp split: vmpage_size.split)+
(* untyped *)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_lift_def cap_tag_defs)
apply (clarsimp simp: cap_lift_def cap_tag_defs mask_def)
apply (subgoal_tac "index (cap_C.words_C ccap) 1 && 0x1F \<le> 0x1F")
apply (simp add: unat_arith_simps)
apply (simp add: word_and_le1)
@ -3611,7 +3608,7 @@ lemma sameRegionAs_spec:
apply (subgoal_tac "capBlockSize_CL (cap_untyped_cap_lift cap_a) \<le> 0x1F")
apply (simp add: word_le_make_less)
apply (simp add: cap_untyped_cap_lift_def cap_lift_def
cap_tag_defs word_and_le1)
cap_tag_defs word_and_le1 mask_def)
apply (clarsimp simp: get_capSizeBits_valid_shift_word)
apply (clarsimp simp: from_bool_def Let_def split: if_split bool.splits)
apply (subst unat_of_nat32,
@ -3668,7 +3665,7 @@ lemma capFSize_range:
"\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow>
capFSize_CL (cap_frame_cap_lift cap) \<le> 3"
apply (simp add: cap_frame_cap_lift_def)
apply (simp add: cap_lift_def cap_tag_defs word_and_le1)
apply (simp add: cap_lift_def cap_tag_defs word_and_le1 mask_def)
done
lemma Arch_sameObjectAs_spec:
@ -3962,7 +3959,7 @@ lemma updateCapData_spec:
apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap)
apply (rule word_le_nat_alt[THEN iffD1])
apply (rule word_and_le1)
apply simp
apply (simp add: mask_def)
apply (simp add: word_sle_def)
apply (rule conjI, clarsimp simp: ccap_relation_NullCap_iff cap_tag_defs)
@ -4330,7 +4327,7 @@ lemma (in kernel_m) updateMDB_set_mdbPrev:
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr ptr:: cte_C ptr)\<rbrace>
(call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr ptr:: cte_C ptr
\<rightarrow>[''cteMDBNode_C'']),
v_' := slotc |))
v32_' := slotc |))
mdb_node_ptr_set_mdbPrev_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a)))
FI)"
apply (rule ccorres_guard_imp2) -- "replace preconditions by schematics"
@ -4339,7 +4336,7 @@ lemma (in kernel_m) updateMDB_set_mdbPrev:
apply (rule ccorres_updateMDB_cte_at)
apply (ctac add: ccorres_updateMDB_set_mdbPrev)
apply (ctac ccorres: ccorres_updateMDB_skip)
apply (simp add: Collect_const_mem)
apply (simp)
done
lemma (in kernel_m) updateMDB_set_mdbNext:
@ -4352,7 +4349,7 @@ lemma (in kernel_m) updateMDB_set_mdbNext:
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr ptr:: cte_C ptr)\<rbrace>
(call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr ptr:: cte_C ptr
\<rightarrow>[''cteMDBNode_C'']),
v_' := slotc |))
v32_' := slotc |))
mdb_node_ptr_set_mdbNext_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a)))
FI)"
apply (rule ccorres_guard_imp2) -- "replace preconditions by schematics"

10
proof/crefine/ARM/CSpace_RAB_C.thy
View File

@ -316,7 +316,7 @@ next
apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap)
apply (rule order_le_less_trans, rule word_le_nat_alt[THEN iffD1],
rule word_and_le1)
apply simp
apply (simp add: mask_def)
done
have cgD: "\<And>capGuard cap cap'. \<lbrakk> capGuard = capCNodeGuard_CL (cap_cnode_cap_lift cap');
@ -335,7 +335,7 @@ next
apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap)
apply (rule order_le_less_trans, rule word_le_nat_alt[THEN iffD1],
rule word_and_le1)
apply simp
apply (simp add: mask_def)
done
have rxgd:
@ -350,7 +350,7 @@ next
apply (subst unat_plus_simple[symmetric], subst no_olen_add_nat)
apply (rule order_le_less_trans, rule add_le_mono)
apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+
apply simp
apply (simp add: mask_def)
done
(* Move outside this context? *)
@ -434,7 +434,7 @@ next
cap_lift_cnode_cap)
apply (rule less_mask_eq
| rule order_le_less_trans, (rule word_and_le1)+
| simp)+
| simp add: mask_def)+
apply (simp add: word_less_nat_alt)
apply (rule order_le_less_trans, rule add_le_mono)
apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+
@ -452,7 +452,7 @@ next
apply (subst unat_plus_simple[THEN iffD1])
apply (subst no_olen_add_nat)
apply (simp add: cap_lift_cnode_cap cap_cnode_cap_lift_def
cap_get_tag_isCap[symmetric])
cap_get_tag_isCap[symmetric] mask_def)
apply (rule order_le_less_trans, rule add_le_mono)
apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+
apply simp

17
proof/crefine/ARM/Fastpath_C.thy
View File

@ -456,7 +456,7 @@ lemma lookup_fp_ccorres':
apply (subst unat_plus_simple[symmetric], subst no_olen_add_nat)
apply (rule order_le_less_trans, rule add_le_mono)
apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+
apply simp
apply (simp add: mask_def)
apply (rule ccorres_guard_imp2)
apply csymbr+
apply (rule ccorres_Guard_Seq, csymbr)
@ -1126,7 +1126,7 @@ lemma thread_state_ptr_set_tsType_np_spec:
apply (clarsimp simp: typ_heap_simps')
apply (rule exI, rule conjI[OF _ conjI [OF _ refl]])
apply (simp_all add: thread_state_lift_def)
apply (auto simp: "StrictC'_thread_state_defs")
apply (auto simp: "StrictC'_thread_state_defs" mask_def)
done
lemma thread_state_ptr_mset_blockingObject_tsType_spec:
@ -1186,7 +1186,7 @@ lemma mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_spec:
apply (rule exI, rule conjI[OF _ refl])
apply (simp add: mdb_node_lift_def word_ao_dist shiftr_over_or_dist ucast_id)
apply (fold limited_and_def)
apply (simp add: limited_and_simps)
apply (simp add: limited_and_simps mask_def)
done
@ -1212,7 +1212,7 @@ lemma mdb_node_ptr_set_mdbPrev_np_spec:
apply (subst parent_update_child, erule typ_heap_simps', simp+)
apply (clarsimp simp: typ_heap_simps' word_sle_def word_sless_def)
apply (rule exI, rule conjI [OF _ refl])
apply (simp add: mdb_node_lift_def limited_and_simps)
apply (simp add: mdb_node_lift_def limited_and_simps mask_def)
done
lemma cap_reply_cap_ptr_new_np_spec2:
@ -1445,7 +1445,7 @@ lemma mi_check_messageInfo_raw:
= mi_from_H (messageInfoFromWord mi)"
apply (simp add: messageInfoFromWord_def Let_def mi_from_H_def
seL4_MessageInfo_lift_def fcp_beta msgLengthBits_def msgExtraCapBits_def
msgMaxExtraCaps_def shiftL_nat)
msgMaxExtraCaps_def shiftL_nat mask_def)
apply (subst if_not_P)
apply (simp add: linorder_not_less msgMaxLength_def n_msgRegisters_def)
apply (erule order_trans, simp)
@ -1974,7 +1974,7 @@ lemma cap_reply_cap_ptr_new_np_updateCap_ccorres:
apply (simp add: cap_to_H_simps word_ao_dist cl_valid_cap_def
limited_and_simps cap_reply_cap_def
limited_and_simps1[OF lshift_limited_and, OF limited_and_from_bool]
shiftr_over_or_dist word_bw_assocs)
shiftr_over_or_dist word_bw_assocs mask_def)
done
lemma fastpath_copy_mrs_ccorres:
@ -2010,8 +2010,7 @@ shows
apply (simp add: min.absorb2)
apply (rule allI, rule conseqPre, vcg)
apply (simp)
apply (simp add: length_msgRegisters n_msgRegisters_def
word_bits_def hoare_TrueI)+
apply (simp add: length_msgRegisters n_msgRegisters_def word_bits_def hoare_TrueI)+
done
lemma switchToThread_ksCurThread:
@ -2050,7 +2049,7 @@ lemma cap_page_directory_cap_get_capPDBasePtr_spec2:
apply vcg
apply (clarsimp simp: word_sle_def word_sless_def
cap_page_directory_cap_lift_def
cap_lift_page_directory_cap)
cap_lift_page_directory_cap mask_def)
done
lemma ccorres_flip_Guard2:

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

@ -988,7 +988,7 @@ lemma invalidateASIDEntry_ccorres:
apply (rule unat_less_power[where sz=8, simplified])
apply (simp add: word_bits_conv)
apply (rule order_le_less_trans, rule word_and_le1)
apply simp
apply (simp add: mask_def)
apply (rule ccorres_return_Skip)
apply (fold dc_def)
apply (ctac add: invalidateASID_ccorres)
@ -996,7 +996,7 @@ lemma invalidateASIDEntry_ccorres:
apply (simp add: guard_is_UNIV_def)
apply wp
apply (clarsimp simp: Collect_const_mem pde_pde_invalid_lift_def pde_lift_def
order_le_less_trans[OF word_and_le1])
order_le_less_trans[OF word_and_le1] mask_def)
done
end

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

@ -2774,7 +2774,7 @@ lemma capCNodeRadix_CL_less_32:
"cap_get_tag ccap = scast cap_cnode_cap \<Longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift ccap) < 32"
apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap)
apply (rule order_le_less_trans, rule word_and_le1)
apply simp
apply (simp add: mask_def)
done
lemmas unat_capCNodeRadix_CL_less_32

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

@ -325,7 +325,7 @@ lemmas rf_sr_tcb_update_no_queue_gen
lemma threadSet_tcbState_simple_corres:
"ccorres dc xfdc (tcb_at' thread)
{s. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := v_' s && mask 4\<rparr>, fl)) \<and>
{s. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := v32_' s && mask 4\<rparr>, fl)) \<and>
thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
(threadSet (tcbState_update (\<lambda>_. st)) thread) (Call thread_state_ptr_set_tsType_'proc)"
apply (rule threadSet_corres_lemma)
@ -656,7 +656,7 @@ lemma ctcb_relation_unat_dom_eq:
lemma threadSet_queued_ccorres [corres]:
shows "ccorres dc xfdc (tcb_at' thread)
{s. v_' s = from_bool v \<and> thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
{s. v32_' s = from_bool v \<and> thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
(threadSet (tcbQueued_update (\<lambda>_. v)) thread)
(Call thread_state_ptr_set_tcbQueued_'proc)"
apply (rule threadSet_corres_lemma)

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

@ -3108,7 +3108,6 @@ next
subst shiftl_shiftr2, simp, simp)
apply (simp add: seL4_MessageInfo_lift_def word_bw_assocs
word_sle_def t2n_mask_eq_if)
apply (simp add: mask_def)
apply (rule conjI)
apply (clarsimp simp: ccap_rights_relation_def cap_rights_to_H_def
false_def true_def to_bool_def allRights_def

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

@ -1347,7 +1347,7 @@ lemma updateFreeIndex_ccorres:
apply (rule unat_of_nat_eq unat_of_nat_eq[symmetric],
erule order_le_less_trans,
rule power_strict_increasing, simp_all)
apply (rule unat_less_helper, rule order_le_less_trans[OF word_and_le1], simp)
apply (rule unat_less_helper, rule order_le_less_trans[OF word_and_le1], simp add: mask_def)
done
end

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

@ -781,7 +781,7 @@ lemma capFVMRights_range:
"\<And>cap. cap_get_tag cap = scast cap_small_frame_cap \<Longrightarrow>
cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) \<le> 3"
by (simp add: cap_frame_cap_lift_def cap_small_frame_cap_lift_def
cap_lift_def cap_tag_defs word_and_le1)+
cap_lift_def cap_tag_defs word_and_le1 mask_def)+
lemma dumb_bool_for_all: "(\<forall>x. x) = False"
by auto

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

@ -208,7 +208,7 @@ lemma is_aligned_tcb_ptr_to_ctcb_ptr:
done
lemma sanitiseRegister_spec:
"\<forall>s t v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v___unsigned_long = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace>)
"\<forall>s t v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace>)
Call sanitiseRegister_'proc
\<lbrace>\<acute>ret__unsigned_long = sanitiseRegister t r v\<rbrace>"
apply vcg

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

@ -1094,7 +1094,7 @@ lemma restart_ccorres:
lemma setNextPC_ccorres:
"ccorres dc xfdc \<top>
(UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>
\<inter> {s. v___unsigned_long_' s = val}) []
\<inter> {s. v_' s = val}) []
(asUser thread (setNextPC val))
(Call setNextPC_'proc)"
apply (cinit')

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

@ -2786,7 +2786,7 @@ lemma ccap_relation_mapped_asid_0:
apply (drule word_shift_zero [where m=8])
apply (rule order_trans)
apply (rule word_and_le1)
apply simp
apply (simp add: mask_def)
apply (simp add: asid_low_bits_def word_bits_def)
apply simp
apply (rule ccontr)
@ -2802,7 +2802,7 @@ lemma ccap_relation_mapped_asid_0:
apply (drule word_shift_zero [where m=8])
apply (rule order_trans)
apply (rule word_and_le1)
apply simp
apply (simp add: mask_def)
apply (simp add: asid_low_bits_def word_bits_def)
apply simp
done
@ -2850,7 +2850,7 @@ lemma ccap_relation_PageCap_generics:
generic_frame_cap_get_capFIsDevice_CL_def
elim!: ccap_relationE)
apply (simp add: gen_framesize_to_H_def)
apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1]
apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1] mask_def
split: if_split)
apply (clarsimp split: if_split_asm)
apply (frule(1) cap_get_tag_isCap_unfolded_H_cap)
@ -2865,7 +2865,7 @@ lemma ccap_relation_PageCap_generics:
option_to_0_def
elim!: ccap_relationE)
apply (simp add: gen_framesize_to_H_is_framesize_to_H_if_not_ARMSmallPage)
apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1]
apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1] mask_def
split: if_split)
apply (clarsimp split: if_split_asm)
done
@ -3105,7 +3105,7 @@ lemma vmAttributesFromWord_spec:
\<lparr> armExecuteNever_CL = (\<^bsup>s\<^esup>w >> 2) && 1,
armParityEnabled_CL = (\<^bsup>s\<^esup>w >> 1) && 1,
armPageCacheable_CL = \<^bsup>s\<^esup>w && 1 \<rparr> \<rbrace>"
by (vcg, simp add: vm_attributes_lift_def word_sless_def word_sle_def)
by (vcg, simp add: vm_attributes_lift_def word_sless_def word_sle_def mask_def)
lemma cap_to_H_PDCap_tag:
"\<lbrakk> cap_to_H cap = ArchObjectCap (PageDirectoryCap p A);