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

isabelle-2021 arm : update Refine 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-09-16 09:54:08 +10:00 committed by Gerwin Klein
parent 239037906e
commit 43e558cd9b
14 changed files with 175 additions and 186 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
proof/refine/ARM/ArchAcc_R.thy
View File

@ -120,7 +120,6 @@ lemma getObject_ASIDPool_corres [corres]:
apply (simp add: return_def)
apply (simp add: in_magnitude_check objBits_simps
archObjSize_def pageBits_def)
apply clarsimp
apply (clarsimp simp: state_relation_def pspace_relation_def)
apply (drule bspec, blast)
apply (clarsimp simp: other_obj_relation_def asid_pool_relation_def)
@ -245,7 +244,6 @@ lemma getObject_PDE_corres [corres]:
split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp: typ_at'_def ko_wp_at'_def)
apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def)
apply (clarsimp simp: bind_def)
apply (clarsimp simp: state_relation_def pspace_relation_def)
apply (drule bspec, blast)
apply (clarsimp simp: other_obj_relation_def pde_relation_def)
@ -497,7 +495,6 @@ lemma getObject_PTE_corres [corres]:
split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp: typ_at'_def ko_wp_at'_def)
apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pteBits_def)
apply (clarsimp simp: bind_def)
apply (clarsimp simp: state_relation_def pspace_relation_def)
apply (drule bspec, blast)
apply (clarsimp simp: other_obj_relation_def pte_relation_def)

5
proof/refine/ARM/CNodeInv_R.thy
View File

@ -5905,6 +5905,7 @@ lemma valid_cap'_handy_bits:
"s \<turnstile>' Zombie r zb n \<Longrightarrow> n < 2 ^ word_bits"
"\<lbrakk> s \<turnstile>' Zombie r zb n; n \<noteq> 0 \<rbrakk> \<Longrightarrow> of_nat n - 1 < (2 ^ (zBits zb) :: word32)"
"s \<turnstile>' Zombie r zb n \<Longrightarrow> zBits zb < word_bits"
including no_0_dvd no_take_bit
apply (insert zombieCTEs_le[where zb=zb],
simp_all add: valid_cap'_def)
apply (clarsimp elim!: order_le_less_trans)
@ -5944,6 +5945,7 @@ lemma ex_Zombie_to2:
"\<lbrakk> ctes_of s p = Some cte; cteCap cte = Zombie p' b n;
n \<noteq> 0; valid_objs' s \<rbrakk>
\<Longrightarrow> ex_cte_cap_to' (p' + (2^cteSizeBits * of_nat n - 2^cteSizeBits)) s"
including no_take_bit no_0_dvd
apply (simp add: ex_cte_cap_to'_def cte_wp_at_ctes_of)
apply (intro exI, rule conjI, assumption)
apply (simp add: image_def)
@ -7158,6 +7160,7 @@ next
have pred_conj_assoc: "\<And>P Q R. (P and (Q and R)) = (P and Q and R)"
by (rule ext, simp)
show ?case
including no_take_bit no_0_dvd
apply (simp only: rec_del_concrete_unfold cap_relation.simps)
apply (simp add: reduceZombie_def Let_def
liftE_bindE
@ -7930,7 +7933,7 @@ lemma m_cap:
lemma sameRegion_cap'_src [simp]:
"sameRegionAs cap' c = sameRegionAs src_cap c"
using parency unfolding weak_derived'_def
apply (case_tac "isReplyCap src_cap")
apply (case_tac "isReplyCap src_cap"; clarsimp)
apply (clarsimp simp: capMasterCap_def split: capability.splits arch_capability.splits
; fastforce simp: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps split: if_split_asm)+
done

1
proof/refine/ARM/CSpace_I.thy
View File

@ -1127,6 +1127,7 @@ qed
lemma cte_refs_capRange:
"\<lbrakk> s \<turnstile>' c; \<forall>irq. c \<noteq> IRQHandlerCap irq \<rbrakk> \<Longrightarrow> cte_refs' c x \<subseteq> capRange c"
including no_take_bit
apply (cases c; simp add: capRange_def isCap_simps)
apply (clarsimp dest!: valid_capAligned
simp: capAligned_def objBits_simps field_simps)

1
proof/refine/ARM/CSpace_R.thy
View File

@ -3840,6 +3840,7 @@ lemma create_reply_master_corres:
lemma cte_map_nat_to_cref:
"\<lbrakk> n < 2 ^ b; b < word_bits \<rbrakk> \<Longrightarrow>
cte_map (p, nat_to_cref b n) = p + (of_nat n * 2^cte_level_bits)"
including no_take_bit
apply (clarsimp simp: cte_map_def nat_to_cref_def
dest!: less_is_drop_replicate)
apply (rule arg_cong [where f="\<lambda>x. x * 2^cte_level_bits"])

38
proof/refine/ARM/Detype_R.thy
View File

@ -7,6 +7,7 @@
theory Detype_R
imports Retype_R
begin
context begin interpretation Arch . (*FIXME: arch_split*)
text \<open>Establishing that the invariants are maintained
@ -402,35 +403,30 @@ lemma map_to_ctes_delete:
lemma word_range_card:
"base \<le>base + h \<Longrightarrow> card {base..base + (h::word32)} = (unat h) + 1"
proof (induct h)
case 1 show ?case by simp
proof (induct h rule: word_induct2)
case zero show ?case by simp
next
case (2 h)
case (suc h)
have interval_plus_one_word32:
"\<And>base ceil. \<lbrakk>base \<le> ceil + 1;ceil \<le> ceil + 1\<rbrakk> \<Longrightarrow>
{base..ceil + 1} = {base .. ceil } \<union> {ceil + (1::word32)}"
by (auto intro:order_antisym simp:not_le inc_le)
show ?case
using suc plus_one_helper2[where n = h and x = h,simplified]
apply (subst add.commute[where a = 1])
apply (subst add.assoc[symmetric])
apply (subst interval_plus_one_word32)
using 2
apply (simp add: field_simps)
apply (subst add.assoc)
apply (rule word_plus_mono_right)
using 2 plus_one_helper2[where n = h and x = h,simplified]
apply (simp add: field_simps)
using 2
apply (simp add: field_simps)
apply (subst card_Un_disjoint,simp+)
using 2
apply (subst card_Un_disjoint; simp)
apply (clarsimp simp: field_simps)
using 2
apply (subst 2)
apply (erule word_plus_mono_right2)
using 2 plus_one_helper2[where n = h and x = h,simplified]
apply (subst suc)
apply (erule word_plus_mono_right2)
apply (simp add: field_simps)
apply simp
apply simp
apply (simp add: unatSuc)
done
qed
@ -2037,7 +2033,8 @@ proof -
fix obj src a m
show "\<And>s'. \<lbrakk>cte_check obj src a m; ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1}"
by (case_tac obj)
(auto simp add: cte_check_def objBits_simps' field_simps
(auto simp add: cte_check_def objBits_simps' diff_eq_eq
add.commute[where b=a]
word_plus_mono_right is_aligned_no_wrap'
tcbVTableSlot_def tcbCTableSlot_def tcbReplySlot_def
tcbCallerSlot_def tcbIPCBufferSlot_def )
@ -4056,6 +4053,7 @@ lemma createNewCaps_ret_len:
| intro conjI impI)+)+
done
lemma no_overlap_check:
"\<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s;
pspace_aligned' s;n\<noteq> 0\<rbrakk>
@ -4064,6 +4062,7 @@ lemma no_overlap_check:
(fst (lookupAround2 (ptr + of_nat (shiftL n bits - Suc 0))
(ksPSpace s))) s =
return () s"
including no_0_dvd
apply (clarsimp split:option.splits simp:assert_def lookupAround2_char1 not_less)
apply (rule ccontr)
apply (frule(1) pspace_no_overlapD')
@ -4407,7 +4406,7 @@ lemma createObjects'_page_directory_at':
apply (rule createObjects'_wp_subst)
apply simp
apply (clarsimp simp:valid_def)
apply (frule use_valid[OF _ createObjects_ko_at_strg[where 'b = pde]])
apply (frule use_valid[OF _ createObjects_ko_at_strg[where 'a = pde]])
apply (simp add:objBits_simps archObjSize_def pdeBits_def)
apply simp
apply (simp add:projectKO_def projectKO_opt_pde return_def)
@ -4628,8 +4627,8 @@ lemma new_cap_addrs_def2:
"n < 2 ^ 32
\<Longrightarrow> new_cap_addrs (Suc n) ptr obj
= map (\<lambda>n. ptr + (n << objBitsKO obj)) [0.e.of_nat n]"
by (simp add:new_cap_addrs_def upto_enum_word unat_of_nat
Fun.comp_def)
including no_take_bit
by (simp add:new_cap_addrs_def upto_enum_word unat_of_nat Fun.comp_def)
lemma createTCBs_tcb_at':
"\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
@ -4734,7 +4733,7 @@ proof -
done
show ?thesis
using assms
including no_take_bit using assms
apply (clarsimp simp:valid_pspace'_def)
apply (frule range_cover.aligned)
apply (frule(3) pspace_no_overlap'_tail)
@ -5201,6 +5200,7 @@ lemma createNewObjects_def2:
apply (simp add:range_cover_def objSize_eq_capBits)+
done
show ?case
including no_take_bit
apply simp
using snoc.prems
apply (subst upto_enum_inc_1)
@ -5486,7 +5486,7 @@ lemma createNewObjects_Cons:
case Nil thus ?case by simp
next
case (Cons x xs)
thus ?case by (simp add:unat_of_nat32)
thus ?case including no_take_bit by (simp add:unat_of_nat32)
qed
show ?thesis

4
proof/refine/ARM/Interrupt_R.thy
View File

@ -266,7 +266,7 @@ lemma decodeIRQControlInvocation_corres:
dest!: not_le_imp_less
simp: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq ucast_nat_def
split: list.splits)[1]
apply (simp add: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq ucast_nat_def[symmetric])
apply (simp add: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq)
apply (rule corres_guard_imp)
apply (rule whenE_throwError_corres, clarsimp, clarsimp)
apply (rule_tac F="unat y \<le> unat maxIRQ" in corres_gen_asm)
@ -325,6 +325,7 @@ lemma arch_decode_irq_control_valid'[wp]:
| wp (once) hoare_drop_imps)+
apply (clarsimp simp add: invs_valid_objs' irq_const_defs unat_word_ariths word_le_nat_alt
not_less unat_le_helper unat_of_nat)
apply (rule order.trans, rule unat_ucast_le, assumption)
done
lemma decode_irq_control_valid'[wp]:
@ -342,6 +343,7 @@ lemma decode_irq_control_valid'[wp]:
| wp (once) hoare_drop_imps)+
apply (clarsimp simp: invs_valid_objs' irq_const_defs unat_word_ariths word_le_nat_alt
not_less unat_le_helper unat_of_nat)
apply (rule order.trans, rule unat_ucast_le, assumption)
done
lemma valid_globals_ex_cte_cap_irq:

26
proof/refine/ARM/Invariants_H.thy
View File

@ -3326,30 +3326,8 @@ lemma superSectionPDE_offsets_eq: "superSectionPDE_offsets = superSectionPDEOff
lemma mask_wordRadix_less_wordBits:
assumes sz: "wordRadix \<le> size w"
shows "unat ((w::'a::len word) && mask wordRadix) < wordBits"
proof -
note pow_num = semiring_numeral_class.power_numeral
{ assume "wordRadix = size w"
hence ?thesis
by (fastforce intro!: unat_lt2p[THEN order_less_le_trans]
simp: wordRadix_def wordBits_def' word_size)
} moreover {
assume "wordRadix < size w"
hence ?thesis unfolding wordRadix_def wordBits_def' mask_def
apply simp
apply (subst unat_less_helper, simp_all)
apply (rule word_and_le1[THEN order_le_less_trans])
apply (simp add: word_size bintrunc_mod2p)
apply (subst int_mod_eq', simp_all)
apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp)
apply (simp del: pow_num)
apply (subst int_mod_eq', simp_all)
apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp)
apply (simp del: pow_num)
done
}
ultimately show ?thesis using sz by fastforce
qed
using word_unat_mask_lt[where m=wordRadix and w=w] assms
by (simp add: wordRadix_def wordBits_def')
lemma priority_mask_wordRadix_size:
"unat ((w::priority) && mask wordRadix) < wordBits"

8
proof/refine/ARM/PageTableDuplicates.thy
View File

@ -830,13 +830,13 @@ lemma copyGlobalMappings_ksPSpace_concrete:
apply (rule le_less_trans[OF word_and_le1])
apply simp
apply (frule_tac d1 = "pptrBase >> 20 << 2" in is_aligned_add_helper[THEN conjunct2])
apply (simp add:ARM.pptrBase_def pptrBase_def)
apply (simp add:field_simps pdeBits_def)
apply (simp add: pptrBase_def)
apply (simp add: pdeBits_def)
apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2])
apply (simp add: pdeBits_def)
apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
in is_aligned_add_helper[THEN conjunct2])
apply (simp add:ARM.pptrBase_def pptrBase_def pdeBits_def)
in is_aligned_add_helper[THEN conjunct2])
apply (simp add: pptrBase_def pdeBits_def)
apply (simp add: pdeBits_def)
apply (cut_tac copyGlobalMappings_ksPSpace_sameD)
apply simp

2
proof/refine/ARM/Refine.thy
View File

@ -547,7 +547,7 @@ lemma kernel_corres':
apply (rule corres_underlying_trivial)
apply (rule no_fail_getActiveIRQ)
apply clarsimp
apply (rule_tac x=irqa in option_corres)
apply (rule_tac x=irq in option_corres)
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply (simp add: when_def)
apply (rule corres_when[simplified dc_def], simp)

238
proof/refine/ARM/Retype_R.thy
View File

@ -1737,20 +1737,21 @@ proof -
"image (\<lambda>n. ptr + 2 ^ obj_bits_api (APIType_map2 ty) us * n)
{x. x \<le> of_nat n - 1} =
set (retype_addrs ptr (APIType_map2 ty) n us)"
apply (clarsimp simp: retype_addrs_def image_def Bex_def ptr_add_def
Collect_eq)
apply (rule iffI)
apply (clarsimp simp: field_simps word_le_nat_alt)
apply (rule_tac x="unat x" in exI)
apply (simp add: unat_sub_if_size range_cover.unat_of_nat_n[OF cover]
not_le not_zero
split: if_split_asm)
apply (clarsimp simp: field_simps word_le_nat_alt)
apply (rule_tac x="of_nat x" in exI)
apply (simp add: unat_sub_if_size range_cover.unat_of_nat_n[OF cover])
apply (rule nat_le_Suc_less_imp)
apply (metis le_unat_uoi nat_less_le not_le_imp_less)
done
including no_take_bit
apply (clarsimp simp: retype_addrs_def image_def Bex_def ptr_add_def
Collect_eq)
apply (rule iffI)
apply (clarsimp simp: field_simps word_le_nat_alt)
apply (rule_tac x="unat x" in exI)
apply (simp add: unat_sub_if_size range_cover.unat_of_nat_n[OF cover]
not_le not_zero
split: if_split_asm)
apply (clarsimp simp: field_simps word_le_nat_alt)
apply (rule_tac x="of_nat x" in exI)
apply (simp add: unat_sub_if_size range_cover.unat_of_nat_n[OF cover])
apply (rule nat_le_Suc_less_imp)
apply (metis le_unat_uoi nat_less_le not_le_imp_less)
done
have new_caps_adds_fold:
"map (\<lambda>n. ptr + 2 ^ objBitsKO ko * n) [0.e.2 ^ gbits * of_nat n - 1] =
@ -1770,6 +1771,7 @@ proof -
have al': "is_aligned ptr (obj_bits_api (APIType_map2 ty) us)"
by (simp add: obj_bits_api ko)
show ?thesis
including no_take_bit
apply (simp add: when_def retype_region2_def createObjects'_def
createObjects_def aligned obj_bits_api[symmetric]
ko[symmetric] al' shiftl_t2n data_map_insert_def[symmetric]
@ -1790,11 +1792,11 @@ proof -
obj_bits_api[symmetric] shiftl_t2n upto_enum_red'
range_cover.unat_of_nat_n[OF cover])
apply (rule corres_split_nor[OF corres_trivial])
apply (clarsimp simp: retype_addrs_fold[symmetric]
ptr_add_def upto_enum_red' not_zero'
range_cover.unat_of_nat_n[OF cover] word_le_sub1)
apply (rule_tac f=g in arg_cong)
apply clarsimp
apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero'
range_cover.unat_of_nat_n[OF cover] word_le_sub1
simp del: word_of_nat_eq_0_iff)
apply (rule_tac f=g in arg_cong)
apply clarsimp
apply (rename_tac x eps ps)
apply (rule_tac P="\<lambda>s. x = kheap s \<and> eps = ekheap (s) \<and> ?P s" and
P'="\<lambda>s. ps = ksPSpace s \<and> ?P' s" in corres_modify)
@ -1927,7 +1929,7 @@ lemma createObjects_ko_at_strg:
fixes ptr :: word32
assumes cover: "range_cover ptr sz ((objBitsKO ko) + gbits) n"
assumes not_0: "n\<noteq> 0"
assumes pi: "\<And>s. projectKO_opt ko = Some val"
assumes pi: "projectKO_opt ko = Some val"
shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
createObjects ptr n ko gbits
\<lbrace>\<lambda>r s. \<forall>x \<in> set r. \<forall>offs < 2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace>"
@ -1938,9 +1940,11 @@ proof -
apply (simp add:word_le_sub1)
done
note unat_of_nat_shiftl = range_cover.unat_of_nat_n_shift[OF cover,where gbits = gbits,simplified]
note word_of_nat_eq_0_iff[simp del]
have in_new:"\<And>idx offs. \<lbrakk>idx \<le> of_nat n - 1;offs<2 ^ gbits\<rbrakk>
\<Longrightarrow> ptr + (idx << objBitsKO ko + gbits) + (offs << objBitsKO ko)
\<in> set (new_cap_addrs (n * 2 ^ gbits) ptr ko)"
including no_take_bit
apply (insert range_cover_not_zero[OF not_0 cover] not_0)
apply (clarsimp simp:new_cap_addrs_def image_def)
apply (rule_tac x ="unat (2 ^ gbits * idx + offs)" in bexI)
@ -2891,67 +2895,66 @@ lemma obj_range'_subset:
by (rule new_range_subset, auto)
lemma obj_range'_subset_strong:
"\<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val)\<rbrakk>
\<Longrightarrow> obj_range' ptr' val \<subseteq> {ptr..ptr + (of_nat n * 2 ^ objBitsKO val) - 1}"
unfolding obj_range'_def
apply (frule(1) obj_range'_subset)
apply (simp add:obj_range'_def)
apply (intro conjI impI)
apply (erule(1) impE)
apply clarsimp
apply (case_tac "n = 0")
apply (clarsimp simp:new_cap_addrs_def)
proof -
assume cover:"range_cover ptr sz (objBitsKO val) n"
and mem_p:"ptr' \<in> set (new_cap_addrs n ptr val)"
and not_0:"n\<noteq> 0"
assumes "range_cover ptr sz (objBitsKO val) n"
and "ptr' \<in> set (new_cap_addrs n ptr val)"
shows "obj_range' ptr' val \<subseteq> {ptr..ptr + (of_nat n * 2 ^ objBitsKO val) - 1}"
proof -
{
assume cover: "range_cover ptr sz (objBitsKO val) n"
and mem_p: "ptr' \<in> set (new_cap_addrs n ptr val)"
and not_0: "n\<noteq> 0"
note n_less = range_cover.range_cover_n_less[OF cover]
have unat_of_nat_m1: "unat (of_nat n - (1::word32)) < n"
using not_0 n_less
by (simp add:unat_of_nat_minus_1)
have decomp:"of_nat n * 2 ^ objBitsKO val = of_nat (n - 1) * 2 ^ objBitsKO val + (2 :: word32) ^ objBitsKO val"
apply (simp add:distrib_right[where b = "1 :: 32 word",simplified,symmetric])
have unat_of_nat_m1: "unat (of_nat n - (1::machine_word)) < n"
using not_0 n_less by (simp add:unat_of_nat_minus_1)
have decomp:
"of_nat n * 2 ^ objBitsKO val =
of_nat (n - 1) * 2 ^ objBitsKO val + (2 :: machine_word) ^ objBitsKO val"
apply (simp add:distrib_right[where b = "1 :: machine_word",simplified,symmetric])
using not_0 n_less
apply simp
done
show "ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + of_nat n * 2 ^ objBitsKO val - 1"
have "ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + of_nat n * 2 ^ objBitsKO val - 1"
using cover including no_take_bit
apply (subst decomp)
apply (simp add:add.assoc[symmetric])
apply (simp add:p_assoc_help)
apply (rule order_trans[OF word_plus_mono_left word_plus_mono_right])
using mem_p not_0
using mem_p not_0
apply (clarsimp simp:new_cap_addrs_def shiftl_t2n)
apply (rule word_plus_mono_right)
apply (subst mult.commute)
apply (rule word_mult_le_mono1[OF word_of_nat_le])
using n_less not_0
using n_less not_0
apply (simp add:unat_of_nat_minus_1)
apply (rule p2_gt_0[THEN iffD2])
using cover
apply (simp add:word_bits_def range_cover_def)
apply (simp only: word_bits_def[symmetric])
apply (clarsimp simp: unat_of_nat_minus_1[OF n_less(1) not_0])
apply (rule nat_less_power_trans2
[OF range_cover.range_cover_le_n_less(2),OF cover, folded word_bits_def])
apply (simp add:unat_of_nat_m1 less_imp_le)
using cover
apply (simp add:unat_of_nat_m1 less_imp_le)
apply (simp add:range_cover_def word_bits_def)
apply (rule machine_word_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::machine_word))"]
apply (clarsimp simp:unat_of_nat_m1)
apply (simp add:range_cover_def word_bits_def)
apply (rule machine_word_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"]
apply (clarsimp simp:unat_of_nat_m1)
using cover
apply (simp add:range_cover_def word_bits_def)
apply (rule olen_add_eqv[THEN iffD2])
apply (subst add.commute[where a = "2^objBitsKO val - 1"])
apply (subst p_assoc_help[symmetric])
apply (rule is_aligned_no_overflow)
using cover
apply (clarsimp simp:range_cover_def word_bits_def)
apply (erule aligned_add_aligned[OF _ is_aligned_mult_triv2])
apply simp+
done
qed
apply (rule olen_add_eqv[THEN iffD2])
apply (subst add.commute[where a = "2^objBitsKO val - 1"])
apply (subst p_assoc_help[symmetric])
apply (rule is_aligned_no_overflow)
apply (clarsimp simp:range_cover_def word_bits_def)
apply (erule aligned_add_aligned[OF _ is_aligned_mult_triv2]; simp)
apply simp
by (meson assms(1) is_aligned_add is_aligned_mult_triv2 is_aligned_no_overflow' range_cover_def)
}
with assms show ?thesis
unfolding obj_range'_def
apply -
apply (frule(1) obj_range'_subset)
apply (simp add: obj_range'_def)
apply (cases "n = 0"; clarsimp simp:new_cap_addrs_def)
done
qed
lemma caps_no_overlapD'':
"\<lbrakk>cte_wp_at' (\<lambda>cap. cteCap cap = c) q s;caps_no_overlap'' ptr sz s\<rbrakk>
@ -3301,73 +3304,73 @@ proof -
have upbound:" unat ((((of_nat n)::word32) * 2 ^ gbits)) * unat ((2::word32) ^ objBitsKO val) < 2 ^ word_bits"
using range_cover.range_cover_le_n_less[OF cover' le_refl] cover'
apply -
apply (drule nat_less_power_trans)
apply (simp add:range_cover_def)
apply (drule nat_less_power_trans)
apply (simp add:range_cover_def)
apply (fold word_bits_def)
using unat_of_nat_shift not_0
apply (simp add:field_simps shiftl_t2n)
done
have not_0': "(2::word32) ^ (objBitsKO val + gbits) * of_nat n \<noteq> 0"
apply (rule range_cover_not_zero_shift[OF not_0,unfolded shiftl_t2n,OF _ le_refl])
apply (rule range_cover_rel[OF cover])
apply simp+
apply (rule range_cover_rel[OF cover]; simp)
done
have "gbits < word_bits"
using cover
by (simp add:range_cover_def word_bits_def)
thus ?thesis
apply -
apply (insert not_0 cover ptr_in)
apply (frule range_cover.range_cover_le_n_less[OF _ le_refl])
apply (fold word_bits_def)
apply (simp add:shiftL_nat )
apply (simp add:range_cover.unat_of_nat_n_shift)
apply (clarsimp simp:new_cap_addrs_def shiftl_t2n)
apply (rename_tac pa)
apply (rule word_plus_mono_right)
apply (rule order_trans)
apply (subst mult.commute)
apply (rule word_mult_le_iff[THEN iffD2])
apply (clarsimp simp:p2_gt_0 range_cover_def word_bits_def)
apply (drule range_cover_rel[where sbit' = "0"])
apply (simp+)[2]
apply (erule less_le_trans[OF range_cover.range_cover_le_n_less(2)])
apply (clarsimp simp:field_simps power_add)
apply (rule unat_le_helper)
apply (rule of_nat_mono_maybe_le[THEN iffD1])
using range_cover.range_cover_le_n_less[OF cover' le_refl]
apply (simp_all only:word_bits_def[symmetric])
including no_take_bit
apply -
apply (insert not_0 cover ptr_in)
apply (frule range_cover.range_cover_le_n_less[OF _ le_refl])
apply (fold word_bits_def)
apply (simp add:shiftL_nat )
apply (simp add:range_cover.unat_of_nat_n_shift)
apply (clarsimp simp:new_cap_addrs_def shiftl_t2n)
apply (rename_tac pa)
apply (rule word_plus_mono_right)
apply (rule order_trans)
apply (subst mult.commute)
apply (rule word_mult_le_iff[THEN iffD2])
apply (clarsimp simp:p2_gt_0 range_cover_def word_bits_def)
apply (drule range_cover_rel[where sbit' = "0"])
apply (simp+)[2]
apply (erule less_le_trans[OF range_cover.range_cover_le_n_less(2)])
apply (clarsimp simp:field_simps power_add)
apply (rule unat_le_helper)
apply (rule of_nat_mono_maybe_le[THEN iffD1])
using range_cover.range_cover_le_n_less[OF cover' le_refl]
apply (simp_all only:word_bits_def[symmetric])
apply simp
apply (drule nat_less_power_trans)
apply (simp add:range_cover_def word_bits_def)
apply (rule less_le_trans[OF mult_less_mono1])
apply (rule unat_mono)
apply (rule_tac y1= "pa" in of_nat_mono_maybe'[THEN iffD1,rotated -1])
apply (assumption)
apply (simp add:word_bits_def)
apply (simp add:word_bits_def)
apply simp
using unat_of_nat_shift
apply (simp add:field_simps shiftl_t2n)
apply simp
apply (drule nat_less_power_trans)
apply (simp add:range_cover_def word_bits_def)
apply (rule less_le_trans[OF mult_less_mono1])
apply (rule unat_mono)
apply (rule_tac y1= "pa" in of_nat_mono_maybe'[THEN iffD1,rotated -1])
apply (assumption)
apply (simp add:word_bits_def)
apply (simp add:word_bits_def)
apply simp
using unat_of_nat_shift
apply (simp add:field_simps shiftl_t2n)
apply simp
apply (rule word_less_sub_1)
apply (simp add:power_add field_simps)
apply (subst mult.assoc[symmetric])
apply (rule word_mult_less_mono1)
apply (rule word_of_nat_less)
using unat_of_nat_shift
apply (simp add:shiftl_t2n field_simps)
apply unat_arith
using upbound
apply (simp add:word_bits_def)
apply (rule machine_word_plus_mono_right_split[where sz = sz])
apply (rule less_le_trans[rotated -1])
apply (rule range_cover.range_cover_compare_bound[OF cover'])
apply (simp add: unat_minus_one[OF not_0'])
using range_cover.unat_of_nat_n_shift[OF cover le_refl]
apply (simp add:shiftl_t2n power_add field_simps)
apply (simp add:range_cover_def word_bits_def)
done
apply (rule word_less_sub_1)
apply (simp add:power_add field_simps)
apply (subst mult.assoc[symmetric])
apply (rule word_mult_less_mono1)
apply (rule word_of_nat_less)
using unat_of_nat_shift
apply (simp add:shiftl_t2n field_simps)
apply (meson less_exp objBitsKO_bounded2 of_nat_less_pow_32 word_gt_a_gt_0)
using upbound
apply (simp add:word_bits_def)
apply (rule machine_word_plus_mono_right_split[where sz = sz])
apply (rule less_le_trans[rotated -1])
apply (rule range_cover.range_cover_compare_bound[OF cover'])
apply (simp add: unat_minus_one[OF not_0'])
using range_cover.unat_of_nat_n_shift[OF cover le_refl]
apply (simp add:shiftl_t2n power_add field_simps)
apply (simp add:range_cover_def word_bits_def)
done
qed
lemma createObjects_orig_ko_wp_at2':
@ -3930,7 +3933,7 @@ lemma createObjects_makeObject_not_tcbQueued:
shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
createObjects ptr n tcb 0
\<lbrace>\<lambda>rv s. \<forall>addr\<in>set rv. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive) addr s\<rbrace>"
apply (rule hoare_strengthen_post[OF createObjects_ko_at_strg[where 'b=tcb]])
apply (rule hoare_strengthen_post[OF createObjects_ko_at_strg[where 'a=tcb]])
using assms
apply (auto simp: obj_at'_def projectKO_opt_tcb objBitsKO_def
objBits_def makeObject_tcb)
@ -5248,6 +5251,7 @@ lemma corres_retype_region_createNewCaps:
init_arch_objects (APIType_map2 (Inr ty)) y n us x;
return x od)
(createNewCaps ty y n us dev)"
including no_take_bit
apply (rule_tac F="range_cover y sz
(obj_bits_api (APIType_map2 (Inr ty)) us) n \<and>
n \<noteq> 0 \<and>

2
proof/refine/ARM/Syscall_R.thy
View File

@ -604,7 +604,7 @@ lemma dec_dom_inv_wf[wp]:
apply (simp add:null_def)
apply (simp add:valid_cap'_def)
apply (simp add:not_le)
apply (simp add:ucast_nat_def[symmetric])
apply (simp del: Word.of_nat_unat flip: ucast_nat_def)
apply (rule word_of_nat_le)
apply (simp add:numDomains_def maxDomain_def)
done

4
proof/refine/ARM/TcbAcc_R.thy
View File

@ -765,9 +765,9 @@ lemma threadSet_cte_wp_at'T:
apply (simp add: threadSet_def)
apply (rule hoare_seq_ext [where B="\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s"])
apply (rule setObject_cte_wp_at2')
apply (clarsimp simp: updateObject_default_def projectKOs in_monad objBits_simps
apply (clarsimp simp: updateObject_default_def projectKOs in_monad
obj_at'_def objBits_simps' in_magnitude_check prod_eq_iff)
apply (case_tac tcba, clarsimp simp: bspec_split [OF spec [OF x]])
apply (case_tac tcb, clarsimp simp: bspec_split [OF spec [OF x]])
apply (clarsimp simp: updateObject_default_def in_monad bind_def
projectKOs)
apply (wp getObject_tcb_wp)

6
proof/refine/ARM/Tcb_R.thy
View File

@ -1989,6 +1989,7 @@ lemma decodeWriteRegisters_corres:
corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t)
(decode_write_registers args (cap.ThreadCap t))
(decodeWriteRegisters args (ThreadCap t))"
including no_take_bit
apply (simp add: decode_write_registers_def decodeWriteRegisters_def)
apply (cases args, simp_all)
apply (case_tac list, simp_all)
@ -2648,9 +2649,8 @@ lemma decodeSetTLSBase_corres:
"corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
(decode_set_tls_base w (cap.ThreadCap t))
(decodeSetTLSBase w (capability.ThreadCap t))"
apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
split: list.split)
by (rule sym, rule ucast_id)
by (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
split: list.split)
lemma decodeTCBInvocation_corres:
"\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';

23
proof/refine/ARM/Untyped_R.thy
View File

@ -66,9 +66,9 @@ lemma APIType_map2_CapTable[simp]:
kernel_object.split arch_kernel_object.splits)
lemma alignUp_H[simp]:
"Untyped_H.alignUp = Word_Lib.alignUp"
"Untyped_H.alignUp = More_Word_Operations.alignUp"
apply (rule ext)+
apply (clarsimp simp:Untyped_H.alignUp_def Word_Lib.alignUp_def mask_def)
apply (clarsimp simp:Untyped_H.alignUp_def More_Word_Operations.alignUp_def mask_def)
done
(* MOVE *)
@ -258,6 +258,7 @@ next
note word_unat_power [symmetric, simp del]
show ?thesis
including no_take_bit
apply (rule corres_name_pre)
apply clarsimp
apply (subgoal_tac "cte_wp_at' (\<lambda>cte. cteCap cte = (capability.UntypedCap d w n idx)) (cte_map slot) s'")
@ -747,6 +748,7 @@ lemma decodeUntyped_wf[wp]:
(UntypedCap d w sz idx) cs
\<lbrace>valid_untyped_inv'\<rbrace>,-"
unfolding decodeUntypedInvocation_def
including no_take_bit
apply (simp add: unlessE_def[symmetric] unlessE_whenE rangeCheck_def whenE_def[symmetric]
returnOk_liftE[symmetric] Let_def cap_case_CNodeCap_True_throw
split del: if_split cong: if_cong list.case_cong)
@ -2962,6 +2964,7 @@ lemma createNewCaps_range_helper:
\<and> (\<forall>p. capClass (capfn p) = PhysicalClass
\<and> capUntypedPtr (capfn p) = p
\<and> capBits (capfn p) = (APIType_capBits tp us))\<rbrace>"
including no_0_dvd
apply (simp add: createNewCaps_def toAPIType_def Arch_createNewCaps_def
split del: if_split cong: option.case_cong)
apply (rule hoare_grab_asm)+
@ -2972,8 +2975,7 @@ lemma createNewCaps_range_helper:
apply (case_tac apiobject_type, simp_all split del: if_split)
apply (rule hoare_pre, wp)
apply (frule range_cover_not_zero[rotated -1],simp)
apply (clarsimp simp: APIType_capBits_def
objBits_simps archObjSize_def ptr_add_def o_def)
apply (clarsimp simp: APIType_capBits_def objBits_simps archObjSize_def ptr_add_def o_def)
apply (subst upto_enum_red')
apply unat_arith
apply (clarsimp simp: o_def fromIntegral_def toInteger_nat fromInteger_nat)
@ -3010,8 +3012,7 @@ lemma createNewCaps_range_helper2:
apply (rule hoare_assume_pre)
apply (rule hoare_strengthen_post)
apply (rule createNewCaps_range_helper)
apply (clarsimp simp: capRange_def interval_empty ptr_add_def
word_unat_power[symmetric]
apply (clarsimp simp: capRange_def ptr_add_def word_unat_power[symmetric]
simp del: atLeastatMost_subset_iff
dest!: less_two_pow_divD)
apply (rule conjI)
@ -4197,6 +4198,7 @@ lemma resetUntypedCap_corres:
(invs' and valid_untyped_inv_wcap' ui' (Some (UntypedCap dev ptr sz idx)) and ct_active')
(reset_untyped_cap slot)
(resetUntypedCap (cte_map slot))"
including no_take_bit
apply (rule corres_gen_asm, clarsimp)
apply (simp add: reset_untyped_cap_def resetUntypedCap_def
liftE_bindE)
@ -4435,6 +4437,7 @@ lemma resetUntypedCap_invs_etc:
and pspace_no_overlap' ptr sz\<rbrace>, \<lbrace>\<lambda>_. invs'\<rbrace>"
(is "\<lbrace>invs' and valid_untyped_inv_wcap' ?ui (Some ?cap) and ct_active' and ?asm\<rbrace>
?f \<lbrace>\<lambda>_. invs' and ?vu2 and ct_active' and ?psp\<rbrace>, \<lbrace>\<lambda>_. invs'\<rbrace>")
including no_0_dvd no_take_bit
apply (simp add: resetUntypedCap_def getSlotCap_def
liftE_bind_return_bindE_returnOk bindE_assoc)
apply (rule hoare_vcg_seqE[rotated])
@ -5429,14 +5432,14 @@ lemma invokeUntyped_invs'':
Q' s"
obtain cref reset ptr tp us slots dev
where pf:
"invokeUntyped_proofs s cref reset (ptr && ~~ mask sz) ptr tp us slots
sz idx dev"
where pf: "invokeUntyped_proofs s cref reset (ptr && ~~ mask sz) ptr tp us slots sz idx dev"
and ui: "ui = Invocations_H.Retype cref reset (ptr && ~~ mask sz) ptr tp us slots dev"
using vui1 misc
apply (cases ui, simp only: Invocations_H.untyped_invocation.simps)
apply (frule(2) invokeUntyped_proofs.intro)
apply (clarsimp simp: cte_wp_at_ctes_of word_bw_assocs)
apply clarsimp
apply (unfold cte_wp_at_ctes_of)
apply (drule meta_mp; clarsimp)
done
note vui = vui1[simplified ui Invocations_H.untyped_invocation.simps]