arm-hyp crefine: bitfield generator proof updates
This commit is contained in:
parent
564359b13e
commit
00bff34f07
|
@ -5064,7 +5064,7 @@ lemma decodeARMMMUInvocation_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)
|
||||
|
|
|
@ -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:
|
||||
|
@ -1274,7 +1275,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"
|
||||
|
@ -1310,7 +1311,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"
|
||||
|
@ -2767,11 +2768,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"
|
||||
|
@ -3288,7 +3285,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)
|
||||
|
@ -3641,7 +3638,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,
|
||||
|
@ -3698,7 +3695,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:
|
||||
|
@ -3992,7 +3989,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)
|
||||
|
@ -4357,7 +4354,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"
|
||||
|
@ -4366,7 +4363,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:
|
||||
|
@ -4379,7 +4376,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"
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)
|
||||
|
@ -1139,7 +1139,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:
|
||||
|
@ -1199,7 +1199,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
|
||||
|
||||
|
||||
|
@ -1225,7 +1225,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:
|
||||
|
@ -1458,7 +1458,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)
|
||||
|
@ -1987,7 +1987,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:
|
||||
|
@ -2023,8 +2023,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:
|
||||
|
@ -2063,7 +2062,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:
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -2776,7 +2776,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
|
||||
|
|
|
@ -328,7 +328,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)
|
||||
|
@ -659,7 +659,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)
|
||||
|
|
|
@ -3269,7 +3269,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
|
||||
|
|
|
@ -1359,7 +1359,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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -1852,7 +1852,7 @@ lemma virq_to_H_arrayp[simp]:
|
|||
lemma virq_virq_active_set_virqEOIIRQEN_spec':
|
||||
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. virq_get_tag \<acute>virq = scast virq_virq_active\<rbrace>
|
||||
Call virq_virq_active_set_virqEOIIRQEN_'proc
|
||||
\<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v) \<rbrace>"
|
||||
\<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>"
|
||||
apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
|
||||
apply vcg
|
||||
apply (clarsimp simp: virq_to_H_def virqSetEOIIRQEN_def o_def)
|
||||
|
@ -1865,7 +1865,7 @@ lemma virq_virq_active_set_virqEOIIRQEN_spec':
|
|||
lemma virq_virq_invalid_set_virqEOIIRQEN_spec':
|
||||
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. virq_get_tag \<acute>virq = scast virq_virq_invalid\<rbrace>
|
||||
Call virq_virq_invalid_set_virqEOIIRQEN_'proc
|
||||
\<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v) \<rbrace>"
|
||||
\<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>"
|
||||
apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
|
||||
apply vcg
|
||||
apply (clarsimp simp: virq_to_H_def virqSetEOIIRQEN_def o_def)
|
||||
|
@ -1878,7 +1878,7 @@ lemma virq_virq_invalid_set_virqEOIIRQEN_spec':
|
|||
lemma virq_virq_pending_set_virqEOIIRQEN_spec':
|
||||
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. virq_get_tag \<acute>virq = scast virq_virq_pending\<rbrace>
|
||||
Call virq_virq_pending_set_virqEOIIRQEN_'proc
|
||||
\<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v) \<rbrace>"
|
||||
\<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>"
|
||||
apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
|
||||
apply vcg
|
||||
apply (clarsimp simp: virq_to_H_def virqSetEOIIRQEN_def o_def)
|
||||
|
|
|
@ -280,7 +280,7 @@ lemma valid_tcb'_vcpuE [elim_format]:
|
|||
by auto
|
||||
|
||||
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> \<inter> \<lbrace>\<acute>archInfo = from_bool t\<rbrace>)
|
||||
"\<forall>s t v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace> \<inter> \<lbrace>\<acute>archInfo = from_bool t\<rbrace>)
|
||||
Call sanitiseRegister_'proc
|
||||
\<lbrace>\<acute>ret__unsigned_long = sanitiseRegister t r v\<rbrace>"
|
||||
apply vcg
|
||||
|
|
|
@ -1109,7 +1109,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')
|
||||
|
|
|
@ -3555,7 +3555,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)
|
||||
|
@ -3571,7 +3571,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
|
||||
|
@ -3619,7 +3619,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)
|
||||
|
@ -3634,7 +3634,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
|
||||
|
@ -3845,7 +3845,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);
|
||||
|
|
Loading…
Reference in New Issue