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

isabelle2021-1: Refine 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-01-14 17:35:41 +11:00 committed by Gerwin Klein
parent 0ee20aec7f
commit 84713327a5
13 changed files with 93 additions and 150 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -746,7 +746,6 @@ lemma setObject_PD_corres [@lift_corres_args, corres]:
apply (simp add: pd_bits_def pageBits_def)
apply (simp add: pd_bits_def pageBits_def)
apply clarsimp
apply (clarsimp simp: nth_ucast nth_shiftl)
apply (drule test_bit_size)
apply (clarsimp simp: word_size pd_bits_def pageBits_def)
apply arith
@ -823,7 +822,6 @@ lemma setObject_PT_corres [@lift_corres_args, corres]:
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: pt_bits_def pageBits_def)
apply clarsimp
apply (clarsimp simp: nth_ucast nth_shiftl)
apply (drule test_bit_size)
apply (clarsimp simp: word_size pt_bits_def pageBits_def)
apply arith
@ -1177,8 +1175,7 @@ lemma ensureSafeMapping_corres [corres]:
lemma asidHighBitsOf [simp]:
"asidHighBitsOf asid = ucast (asid_high_bits_of asid)"
apply (simp add: asidHighBitsOf_def asid_high_bits_of_def asidHighBits_def)
apply (rule word_eqI)
apply (simp add: word_size nth_ucast)
apply word_eqI_solve
done

47
proof/refine/ARM/Arch_R.thy
View File

@ -82,7 +82,7 @@ lemma createObject_typ_at':
apply (erule allE)+
apply (erule(1) impE)
apply (subgoal_tac "x \<in> {x..x + 2 ^ objBitsKO y - 1}")
apply (fastforce simp:is_aligned_neg_mask_eq p_assoc_help)
apply (fastforce simp: p_assoc_help)
apply (rule first_in_uptoD)
apply (drule(1) pspace_alignedD')
apply (clarsimp simp: is_aligned_no_wrap' p_assoc_help)
@ -386,7 +386,8 @@ lemma mask_vmrights_corres:
mask_vm_rights_def nth_ucast
validate_vm_rights_def vm_read_write_def
vm_kernel_only_def vm_read_only_def
split: bool.splits)
split: bool.splits
simp del: bit_0)
lemma vm_attributes_corres:
"vmattributes_map (attribs_from_word w) = attribsFromWord w"
@ -435,8 +436,7 @@ lemma ARMMMU_improve_cases:
crunch inv [wp]: "ARM_H.decodeInvocation" "P"
(wp: crunch_wps mapME_x_inv_wp getASID_wp
simp: forME_x_def crunch_simps
ARMMMU_improve_cases)
simp: crunch_simps ARMMMU_improve_cases)
lemma case_option_corresE:
assumes nonec: "corres r Pn Qn (nc >>=E f) (nc' >>=E g)"
@ -969,12 +969,12 @@ shows
apply (rule_tac P="map_data = None \<and> kernel_base \<le> vaddr + 2 ^ pageBitsForSize vmpage_size - 1
\<or> (\<exists>asid' vaddr'. map_data = Some (asid', vaddr') \<and> (asid',vaddr') \<noteq> (asid,vaddr))"
in corres_symmetric_bool_cases[where Q=\<top> and Q'=\<top>, OF refl])
apply (erule disjE; clarsimp simp: whenE_def kernel_base_def pptrBase_def ARM.pptrBase_def
apply (erule disjE; clarsimp simp: whenE_def kernel_base_def pptrBase_def
split: option.splits)
apply clarsimp
apply (rule corres_splitEE'[where r'=dc and P=\<top> and P'=\<top>])
apply (case_tac map_data
; clarsimp simp: whenE_def kernel_base_def pptrBase_def ARM.pptrBase_def
; clarsimp simp: whenE_def kernel_base_def pptrBase_def
corres_returnOkTT)
\<comment> \<open>pd=undefined as vspace_at_asid not used in find_pd_for_asid_corres and avoid unresolved schematics\<close>
apply (rule corres_splitEE'[
@ -1030,7 +1030,7 @@ shows
apply (simp split: cap.split arch_cap.split option.split,
intro conjI allI impI, simp_all)[1]
apply (rule whenE_throwError_corres_initial, simp)
apply (simp add: kernel_base_def ARM.pptrBase_def pptrBase_def)
apply (simp add: kernel_base_def pptrBase_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -1099,7 +1099,7 @@ shows
apply (rule whenE_throwError_corres, simp)
apply clarsimp
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: kernel_base_def ARM.pptrBase_def pptrBase_def)
apply (clarsimp simp: kernel_base_def pptrBase_def)
apply (rule case_option_corresE)
apply (rule corres_trivial)
apply clarsimp
@ -1334,7 +1334,7 @@ lemma sts_valid_arch_inv':
lemma less_pptrBase_valid_pde_offset':
"\<lbrakk> vptr < pptrBase; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF \<rbrakk>
\<Longrightarrow> valid_pde_mapping_offset' (((x * 4) + (vptr >> 20 << 2)) && mask pdBits)"
apply (clarsimp simp: ARM.pptrBase_def pptrBase_def pdBits_def pageBits_def
apply (clarsimp simp: pptrBase_def pdBits_def pageBits_def
valid_pde_mapping_offset'_def pd_asid_slot_def)
apply (drule word_le_minus_one_leq, simp add: pdeBits_def)
apply (drule le_shiftr[where u=vptr and n=20])
@ -1376,7 +1376,7 @@ lemma createMappingEntries_valid_pde_slots':
apply (simp add: pdBits_def pageBits_def)
apply (clarsimp simp: upto_enum_step_def linorder_not_less pd_bits_def
lookup_pd_slot_def Let_def field_simps
mask_add_aligned pdeBits_def)
mask_add_aligned pdeBits_def take_bit_Suc)
apply (erule less_pptrBase_valid_pde_offset'
[unfolded pdBits_def pageBits_def pdeBits_def, simplified], simp+)
done
@ -1512,8 +1512,7 @@ lemma ensureSafeMapping_valid_slots_duplicated':
lemma is_aligned_ptrFromPAddr_aligned:
"m \<le> 28 \<Longrightarrow> is_aligned (ptrFromPAddr p) m = is_aligned p m"
apply (simp add:ptrFromPAddr_def is_aligned_mask
pptrBaseOffset_def pptrBase_def ARM.physBase_def physBase_def)
apply (simp add:ptrFromPAddr_def is_aligned_mask pptrBaseOffset_def pptrBase_def physBase_def)
apply (subst add.commute)
apply (subst mask_add_aligned)
apply (erule is_aligned_weaken[rotated])
@ -1560,7 +1559,7 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
apply (frule is_aligned_no_wrap'[where off = "0x3c"])
apply simp
apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
apply (clarsimp simp: mask_def add.commute upto_enum_step_def)
apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc)
apply simp
apply wp+
apply (intro conjI impI)
@ -1576,7 +1575,7 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
apply (frule is_aligned_no_wrap'[where off = "0x3c" and sz = 6])
apply simp
apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
apply (clarsimp simp: mask_def add.commute upto_enum_step_def
apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc
superSectionPDEOffsets_def pdeBits_def)
done
@ -1797,29 +1796,13 @@ crunch st_tcb_at': performPageDirectoryInvocation, performPageTableInvocation, p
performASIDPoolInvocation "st_tcb_at' P t"
(wp: crunch_wps getASID_wp getObject_cte_inv simp: crunch_simps)
crunch aligned': "Arch.finaliseCap" pspace_aligned'
(wp: crunch_wps getASID_wp simp: crunch_simps)
lemmas arch_finalise_cap_aligned' = finaliseCap_aligned'
crunch distinct': "Arch.finaliseCap" pspace_distinct'
(wp: crunch_wps getASID_wp simp: crunch_simps)
lemmas arch_finalise_cap_distinct' = finaliseCap_distinct'
crunch nosch [wp]: "Arch.finaliseCap" "\<lambda>s. P (ksSchedulerAction s)"
(wp: crunch_wps getASID_wp simp: crunch_simps updateObject_default_def)
crunch st_tcb_at' [wp]: "Arch.finaliseCap" "st_tcb_at' P t"
(wp: crunch_wps getASID_wp simp: crunch_simps)
crunch typ_at' [wp]: "Arch.finaliseCap" "\<lambda>s. P (typ_at' T p s)"
(wp: crunch_wps getASID_wp simp: crunch_simps)
crunch cte_wp_at': "Arch.finaliseCap" "cte_wp_at' P p"
(wp: crunch_wps getASID_wp simp: crunch_simps)
lemma invs_asid_table_strengthen':
"invs' s \<and> asid_pool_at' ap s \<and> asid \<le> 2 ^ asid_high_bits - 1 \<longrightarrow>
invs' (s\<lparr>ksArchState :=
@ -1918,7 +1901,7 @@ lemma performASIDControlInvocation_invs' [wp]:
apply (strengthen refl ctes_of_valid_cap'[mk_strg I E])
apply (clarsimp simp: conj_comms invs_valid_objs')
apply (frule_tac ptr="w1" in descendants_range_caps_no_overlapI'[where sz = pageBits])
apply (fastforce simp:is_aligned_neg_mask_eq cte_wp_at_ctes_of)
apply (fastforce simp: cte_wp_at_ctes_of)
apply (simp add:empty_descendants_range_in')
apply (frule(1) if_unsafe_then_capD'[OF _ invs_unsafe_then_cap',rotated])
apply (fastforce simp:cte_wp_at_ctes_of)
@ -1932,7 +1915,7 @@ lemma performASIDControlInvocation_invs' [wp]:
apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
apply (simp add: pageBits_def minUntypedSizeBits_def)
apply (frule_tac cte="CTE (capability.UntypedCap False a b c) m" for a b c m in valid_global_refsD', clarsimp)
apply (simp add: is_aligned_neg_mask_eq Int_commute)
apply (simp add: Int_commute)
by (auto simp:empty_descendants_range_in' objBits_simps max_free_index_def
archObjSize_def asid_low_bits_def word_bits_def pageBits_def
range_cover_full descendants_range'_def2 is_aligned_mask

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

@ -48,9 +48,7 @@ where
lemma rightsFromWord_correspondence:
"rightsFromWord w = rights_mask_map (data_to_rights w)"
by (simp add: rightsFromWord_def rights_mask_map_def
data_to_rights_def Let_def nth_ucast)
by (simp add: rightsFromWord_def rights_mask_map_def data_to_rights_def Let_def del: bit_0)
primrec
cnodeinv_relation :: "Invocations_A.cnode_invocation \<Rightarrow> Invocations_H.cnode_invocation \<Rightarrow> bool"
@ -5905,7 +5903,6 @@ 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)
@ -5945,7 +5942,6 @@ 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)
@ -7160,7 +7156,6 @@ 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

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

@ -595,7 +595,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
hence [simp]: "((cbits + length guard = 0) = False) \<and>
((cbits = 0 \<and> guard = []) = False) \<and>
(0 < cbits \<or> guard \<noteq> []) " by simp
note if_split [split del] drop_append[simp del]
note drop_append[simp del]
from "1.prems"
have ?thesis
apply -
@ -1455,7 +1455,7 @@ lemma ps_clear_16:
"\<lbrakk> ps_clear p tcbBlockSizeBits s; is_aligned p tcbBlockSizeBits \<rbrakk> \<Longrightarrow> ksPSpace s (p + 2^cteSizeBits) = None"
apply (simp add: ps_clear_def)
apply (drule equals0D[where a="p + 2^cteSizeBits"])
apply (simp add: dom_def field_simps objBits_defs)
apply (simp add: dom_def add.commute objBits_defs take_bit_Suc)
apply (drule mp)
apply (rule word_plus_mono_right)
apply simp

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

@ -666,6 +666,7 @@ lemma capUntypedSize_capBits:
ARM_H.capUntypedSize_def
pteBits_def pdeBits_def
ptBits_def pdBits_def
shiftl_eq_mult
split: capability.splits arch_capability.splits
zombie_type.splits)
apply fastforce

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

@ -2601,9 +2601,9 @@ lemma getPDE_det:
apply (rule conjI)
apply (subst add.commute)
apply (rule word_diff_ls')
apply (clarsimp simp:field_simps not_le plus_one_helper)
apply (simp add:field_simps is_aligned_no_wrap' is_aligned_mask)
apply simp
apply (clarsimp simp: not_le plus_one_helper)
apply (subst add.commute)
apply (simp add: is_aligned_no_wrap' is_aligned_mask)
apply auto
done
@ -3201,7 +3201,8 @@ lemma getTCB_det:
apply (subst add.commute)
apply (rule word_diff_ls')
apply (clarsimp simp:field_simps not_le plus_one_helper)
apply (simp add:field_simps is_aligned_no_wrap' is_aligned_mask)
apply (subst add.commute)
apply (simp add: is_aligned_no_wrap' is_aligned_mask)
apply simp
apply auto
done
@ -3455,7 +3456,8 @@ lemma ctes_of_ko_at:
(\<exists>ptr ko. (ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko))"
apply (clarsimp simp: map_to_ctes_def Let_def split: if_split_asm)
apply (intro exI conjI, assumption)
apply (simp add: obj_range'_def objBits_simps' is_aligned_no_wrap' field_simps)
apply (simp add: obj_range'_def objBits_simps' add.commute)
apply (simp add: is_aligned_no_wrap')
apply (intro exI conjI, assumption)
apply (clarsimp simp: objBits_simps' obj_range'_def word_and_le2)
apply (thin_tac "P" for P)+
@ -4062,7 +4064,6 @@ 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')

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

@ -140,8 +140,7 @@ lemma decodeCNodeInvocation_empty_fail[intro!, wp, simp]:
apply (simp_all add: decodeCNodeInvocation_def
split_def cnode_invok_case_cleanup unlessE_whenE
cong: if_cong bool.case_cong list.case_cong)
apply (simp | wp | wpc | safe)+
done
by (simp | wp | wpc | safe)+
lemma empty_fail_getObject_ap [intro!, wp, simp]:
"empty_fail (getObject p :: asidpool kernel)"

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

@ -166,7 +166,7 @@ lemma whenE_rangeCheck_eq:
"(rangeCheck (x :: 'a :: {linorder, integral}) y z) =
(whenE (x < fromIntegral y \<or> fromIntegral z < x)
(throwError (RangeError (fromIntegral y) (fromIntegral z))))"
by (simp add: rangeCheck_def unlessE_whenE ucast_id linorder_not_le[symmetric])
by (simp add: rangeCheck_def unlessE_whenE linorder_not_le[symmetric])
(* 125 = maxIRQ *)
lemma unat_ucast_ucast_shenanigans[simp]:
@ -468,7 +468,6 @@ lemma IRQHandler_valid':
by (simp add: valid_cap'_def capAligned_def word_bits_conv)
crunch valid_mdb'[wp]: setIRQState "valid_mdb'"
crunch cte_wp_at[wp]: setIRQState "cte_wp_at' P p"
lemma no_fail_setIRQTrigger: "no_fail \<top> (setIRQTrigger irq trig)"
by (simp add: setIRQTrigger_def)
@ -809,19 +808,13 @@ lemma updateTimeSlice_valid_queues[wp]:
(* catch up tcbSchedAppend to tcbSchedEnqueue, which has these from crunches on possibleSwitchTo *)
crunch ifunsafe[wp]: tcbSchedAppend if_unsafe_then_cap'
crunch irq_handlers'[wp]: tcbSchedAppend valid_irq_handlers'
(simp: unless_def tcb_cte_cases_def wp: crunch_wps)
crunch irq_states'[wp]: tcbSchedAppend valid_irq_states'
crunch pde_mappigns'[wp]: tcbSchedAppend valid_pde_mappings'
crunch irqs_masked'[wp]: tcbSchedAppend irqs_masked'
(simp: unless_def wp: crunch_wps)
crunch ct[wp]: tcbSchedAppend cur_tcb'
(wp: cur_tcb_lift crunch_wps)
crunch cur_tcb'[wp]: tcbSchedAppend cur_tcb'
(simp: unless_def wp: crunch_wps)
lemma timerTick_invs'[wp]:
"\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: timerTick_def)

10
proof/refine/ARM/KHeap_R.thy
View File

@ -18,7 +18,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma obj_at_getObject:
assumes R:
"\<And>a b p q n ko s obj::'a::pspace_storable.
"\<And>a b n ko s obj::'a::pspace_storable.
\<lbrakk> (a, b) \<in> fst (loadObject t t n ko s); projectKO_opt ko = Some obj \<rbrakk> \<Longrightarrow> a = obj"
shows "\<lbrace>obj_at' P t\<rbrace> getObject t \<lbrace>\<lambda>(rv::'a::pspace_storable) s. P rv\<rbrace>"
by (auto simp: getObject_def obj_at'_def in_monad valid_def
@ -158,8 +158,8 @@ lemma updateObject_cte_is_tcb_or_cte:
(\<exists>cte'. ko = KOCTE cte' \<and> ko' = KOCTE cte \<and> s' = s
\<and> p = q \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s)"
apply (clarsimp simp: updateObject_cte typeError_def alignError_def
tcbVTableSlot_def tcbCTableSlot_def to_bl_0 to_bl_1 rev_take objBits_simps'
in_monad map_bits_to_bl cte_level_bits_def in_magnitude_check field_simps
tcbVTableSlot_def tcbCTableSlot_def to_bl_1 rev_take objBits_simps'
in_monad map_bits_to_bl cte_level_bits_def in_magnitude_check
lookupAround2_char1
split: kernel_object.splits)
apply (subst(asm) in_magnitude_check3, simp+)
@ -412,8 +412,6 @@ lemma getObject_valid_obj:
declare fail_inv[simp]
declare return_inv[simp]
lemma typeError_inv [wp]:
"\<lbrace>P\<rbrace> typeError x y \<lbrace>\<lambda>rv. P\<rbrace>"
by (simp add: typeError_def|wp)+
@ -700,7 +698,7 @@ lemma map_to_ctes_upd_tcb:
apply (simp only: field_simps)
apply (erule is_aligned_no_overflow)
apply (simp add: objBits_simps field_simps)
apply (clarsimp simp: tcb_cte_cases_def objBits_simps' field_simps
apply (clarsimp simp: tcb_cte_cases_def objBits_simps'
split: if_split_asm)
apply (subst mask_in_range, assumption)
apply (simp only: atLeastAtMost_iff order_refl simp_thms)

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

@ -517,7 +517,7 @@ lemma global_pd_offset:
apply simp
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)
apply (simp add: pptrBase_def)
apply simp
done
@ -525,7 +525,7 @@ lemma globalPDEWindow_neg_mask:
"\<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a);is_aligned ptr pdBits\<rbrakk>
\<Longrightarrow> y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}
\<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}"
apply (clarsimp simp:pptrBase_def ARM.pptrBase_def)
apply (clarsimp simp: pptrBase_def)
apply (intro conjI)
apply (rule_tac y = "y &&~~ mask (vs_ptr_align a)" in order_trans)
apply (rule is_aligned_le_mask)
@ -612,7 +612,7 @@ lemma copyGlobalMappings_ksPSpace_stable:
apply (clarsimp simp:blah)
apply (intro conjI)
apply (rule word_plus_mono_right)
apply (simp add:ARM.pptrBase_def pptrBase_def pdBits_def pageBits_def pdeBits_def)
apply (simp add: pptrBase_def pdBits_def pageBits_def pdeBits_def)
apply (word_bitwise,simp)
apply (rule is_aligned_no_wrap'[OF ptr_al])
apply (simp add:pdBits_def pageBits_def pdeBits_def)
@ -627,7 +627,7 @@ lemma copyGlobalMappings_ksPSpace_stable:
have offset_bound:
"\<And>x. \<lbrakk>is_aligned ptr 14;ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 0x3FFF\<rbrakk>
\<Longrightarrow> x - ptr < 0x4000"
apply (clarsimp simp: ARM.pptrBase_def pptrBase_def field_simps)
apply (clarsimp simp: pptrBase_def field_simps take_bit_Suc)
apply unat_arith
done
@ -671,10 +671,10 @@ lemma copyGlobalMappings_ksPSpace_stable:
apply (rule conjI)
apply (rule le_shiftr[where u="pptrBase >> 18" and n=2, simplified shiftr_shiftr, simplified])
apply (rule word_le_minus_mono_left[where x=ptr and y="(pptrBase >> 18) + ptr", simplified])
apply (simp add: ARM.pptrBase_def pptrBase_def field_simps)
apply (simp add: pptrBase_def add.commute take_bit_Suc)
apply (simp add:field_simps)
apply (erule is_aligned_no_wrap')
apply (simp add: ARM.pptrBase_def pptrBase_def pdBits_def pageBits_def)
apply (simp add: pptrBase_def pdBits_def pageBits_def)
apply (drule le_m1_iff_lt[THEN iffD1,THEN iffD2,rotated])
apply simp
apply (drule le_shiftr[where u = "x - ptr" and n = 2])
@ -803,7 +803,7 @@ lemma copyGlobalMappings_ksPSpace_concrete:
apply simp
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)
apply (simp add: pptrBase_def)
apply simp
done
@ -1602,7 +1602,8 @@ lemma unmapPage_valid_duplicates'[wp]:
apply (rule hoare_post_imp_R[OF lookupPTSlot_aligned[where sz= vmpage_size]])
apply (simp add:pageBitsForSize_def)
apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
apply (clarsimp simp:mask_def add.commute upto_enum_step_def largePagePTEOffsets_def pteBits_def)
apply (clarsimp simp: mask_def add.commute upto_enum_step_def largePagePTEOffsets_def
pteBits_def take_bit_Suc)
apply wp+
apply ((wp storePTE_no_duplicates' mapM_x_mapM_valid
storePDE_no_duplicates' checkMappingPPtr_Section
@ -1624,7 +1625,8 @@ lemma unmapPage_valid_duplicates'[wp]:
apply (erule is_aligned_weaken,simp)
apply simp
apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
apply (clarsimp simp:mask_def add.commute upto_enum_step_def superSectionPDEOffsets_def pdeBits_def)
apply (clarsimp simp: mask_def add.commute upto_enum_step_def superSectionPDEOffsets_def
pdeBits_def take_bit_Suc)
apply (clarsimp simp:ptBits_def pageBits_def vs_entry_align_def)
done

12
proof/refine/ARM/Schedule_R.thy
View File

@ -61,7 +61,7 @@ proof -
done
qed
lemmas findM_awesome = findM_awesome' [OF _ _ _ suffix_order.order.refl]
lemmas findM_awesome = findM_awesome' [OF _ _ _ suffix_order.refl]
(* Levity: added (20090721 10:56:29) *)
declare objBitsT_koTypeOf [simp]
@ -144,23 +144,17 @@ crunches tcbSchedEnqueue, tcbSchedAppend, tcbSchedDequeue
and pred_tcb_at'[wp]: "pred_tcb_at' proj P t"
(wp: threadSet_pred_tcb_no_state simp: unless_def tcb_to_itcb'_def)
crunches setQueue
for state_refs_of'[wp]: "\<lambda>s. P (state_refs_of' s)"
lemma removeFromBitmap_valid_queues_no_bitmap_except[wp]:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
removeFromBitmap d p
\<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>"
unfolding bitmapQ_defs valid_queues_no_bitmap_except_def
by (wp| clarsimp simp: bitmap_fun_defs)+
by (wp | clarsimp simp: bitmap_fun_defs)+
lemma removeFromBitmap_bitmapQ:
"\<lbrace> \<lambda>s. True \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<not> bitmapQ d p s \<rbrace>"
unfolding bitmapQ_defs bitmap_fun_defs
apply (wp | clarsimp simp: bitmap_fun_defs wordRadix_def)+
apply (subst (asm) complement_nth_w2p, simp_all)
apply (fastforce intro!: order_less_le_trans[OF word_unat_mask_lt] simp: word_size)
done
by (wpsimp simp: bitmap_fun_defs wordRadix_def)
lemma removeFromBitmap_valid_bitmapQ[wp]:
" \<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and

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

@ -16,9 +16,6 @@ declare hoare_in_monad_post[wp]
declare trans_state_update'[symmetric,simp]
declare empty_fail_sequence_x[simp]
declare storeWordUser_typ_at' [wp]
declare of_nat_power [simp del]
declare word_neq_0_conv [simp del]
declare complement_def[simp]
(* Auxiliaries and basic properties of priority bitmap functions *)
@ -1403,9 +1400,6 @@ lemma asUser_getRegister_corres:
apply (clarsimp simp: getRegister_def)
done
crunch inv[wp]: getRegister "P"
(ignore_del: getRegister)
lemma user_getreg_inv'[wp]:
"\<lbrace>P\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>x. P\<rbrace>"
by (wp asUser_inv)
@ -1515,9 +1509,6 @@ lemma asUser_tcb_in_cur_domain'[wp]:
apply (clarsimp simp: obj_at'_def)
done
crunch tcb_in_cur_domain'[wp]: asUser "\<lambda>s. P (tcb_in_cur_domain' t)"
(simp: crunch_simps wp: hoare_drop_imps getObject_inv_tcb setObject_ct_inv)
lemma asUser_tcbDomain_inv[wp]:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> asUser t m \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>"
apply (simp add: asUser_def tcb_in_cur_domain'_def threadGet_def)
@ -2483,12 +2474,14 @@ lemma prioL2Index_bit_set:
apply (insert and_mask_less'[where w=p and n=wordRadix], simp add: wordRadix_def)
done
lemma addToBitmap_bitmapQ:
"\<lbrace> \<lambda>s. True \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ d p \<rbrace>"
unfolding addToBitmap_def
modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
by (wp, clarsimp simp: bitmap_fun_defs bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set)
by (wpsimp simp: bitmap_fun_defs bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set
simp_del: bit_exp_iff)
lemma addToBitmap_valid_queues_no_bitmap_except:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
@ -2516,7 +2509,7 @@ lemma prioToL1Index_bits_low_high_eq:
lemma prioToL1Index_bit_not_set:
"\<not> (~~ ((2 :: machine_word) ^ prioToL1Index p)) !! prioToL1Index p"
apply (subst word_ops_nth_size, simp_all add: prioToL1Index_bit_set)
apply (subst word_ops_nth_size, simp_all add: prioToL1Index_bit_set del: bit_exp_iff)
apply (fastforce simp: prioToL1Index_def wordRadix_def word_size
intro: order_less_le_trans[OF word_shiftr_lt])
done
@ -2575,6 +2568,7 @@ proof -
show ?thesis
unfolding removeFromBitmap_def
supply bit_not_iff[simp del] bit_not_exp_iff[simp del]
apply (simp add: let_into_return[symmetric])
unfolding bitmap_fun_defs when_def
apply wp
@ -2627,8 +2621,8 @@ lemma addToBitmap_bitmapQ_no_L1_orphans[wp]:
lemma addToBitmap_bitmapQ_no_L2_orphans[wp]:
"\<lbrace> bitmapQ_no_L2_orphans \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>"
unfolding bitmap_fun_defs bitmapQ_defs
apply wp
apply clarsimp
supply bit_exp_iff[simp del]
apply wpsimp
apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_set)
done
@ -2662,8 +2656,6 @@ proof -
by - (erule hoare_strengthen_post; fastforce elim: valid_bitmap_valid_bitmapQ_exceptE)
qed
crunch valid_queues[wp]: threadGet "Invariants_H.valid_queues"
lemma threadGet_const_tcb_at:
"\<lbrace>\<lambda>s. tcb_at' t s \<and> obj_at' (P s \<circ> f) t s\<rbrace> threadGet f t \<lbrace>\<lambda>rv s. P s rv \<rbrace>"
apply (simp add: threadGet_def liftM_def)
@ -3059,8 +3051,6 @@ lemma rescheduleRequired_ksQ':
apply (wpsimp wp: tcbSchedEnqueue_ksQ)
done
crunch ksQ[wp]: getCurThread "\<lambda>s. P (ksReadyQueues s p)"
lemma threadSet_tcbState_st_tcb_at':
"\<lbrace>\<lambda>s. P st \<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>"
apply (simp add: threadSet_def pred_tcb_at'_def)
@ -3500,7 +3490,7 @@ lemma pspace_dom_dom:
apply (drule wf_cs_0)
apply clarsimp
apply (rule_tac x = n in exI)
apply (clarsimp simp: of_bl_def word_of_int_hom_syms)
apply (clarsimp simp: of_bl_def)
apply (rule range_eqI [where x = 0], simp)+
apply (rename_tac vmpage_size)
apply (rule exI [where x = 0])
@ -3855,8 +3845,6 @@ crunches setThreadState, setBoundNotification
crunch it' [wp]: removeFromBitmap "\<lambda>s. P (ksIdleThread s)"
crunch ctes_of [wp]: setQueue "\<lambda>s. P (ctes_of s)"
lemma sts_ctes_of [wp]:
"\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>"
apply (simp add: setThreadState_def)
@ -4012,7 +4000,6 @@ crunch nosch[wp]: tcbSchedEnqueue "\<lambda>s. P (ksSchedulerAction s)"
(simp: unless_def)
crunch nosch[wp]: tcbSchedAppend "\<lambda>s. P (ksSchedulerAction s)"
(simp: unless_def)
crunch nosch[wp]: tcbSchedDequeue "\<lambda>s. P (ksSchedulerAction s)"
lemma rescheduleRequired_sa_cnt[wp]:
"\<lbrace>\<lambda>s. True \<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"

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

@ -55,7 +55,7 @@ lemma whenE_rangeCheck_eq:
"(rangeCheck (x :: 'a :: {linorder, integral}) y z) =
(whenE (x < fromIntegral y \<or> fromIntegral z < x)
(throwError (RangeError (fromIntegral y) (fromIntegral z))))"
by (simp add: rangeCheck_def unlessE_whenE ucast_id linorder_not_le[symmetric])
by (simp add: rangeCheck_def unlessE_whenE linorder_not_le[symmetric])
lemma APIType_map2_CapTable[simp]:
"(APIType_map2 ty = Structures_A.CapTableObject)
@ -293,9 +293,9 @@ next
toInteger_nat fromInteger_nat wordBits_def)
apply (simp add: not_le)
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: fromAPIType_def ARM_H.fromAPIType_def)
apply (clarsimp simp: fromAPIType_def)
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: fromAPIType_def ARM_H.fromAPIType_def)
apply (clarsimp simp: fromAPIType_def)
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'" in corres_splitEE[OF _ corres_if])
apply (rule_tac corres_split_norE)
prefer 2
@ -310,14 +310,14 @@ next
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def word_bits_def
is_aligned_weaken)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def ucast_id)+
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (simp add: unat_arith_simps(2) unat_2p_sub_1 word_bits_def)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def ucast_id)+
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (simp add: unat_eq_0 word_less_nat_alt)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def ucast_id)+
apply (clarsimp simp:toInteger_word ucast_id unat_arith_simps(2) cap_aligned_def)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (clarsimp simp:toInteger_word unat_arith_simps(2) cap_aligned_def)
apply (subst unat_sub)
apply (simp add: linorder_not_less word_le_nat_alt)
apply (fold neq0_conv)
@ -789,7 +789,7 @@ lemma decodeUntyped_wf[wp]:
apply clarsimp
apply (drule(1) ctes_of_valid_cap'[OF _ invs_valid_objs'])+
apply simp
apply (clarsimp simp: toEnum_of_nat [OF less_Suc_unat_less_bound] ucast_id)
apply (clarsimp simp: toEnum_of_nat [OF less_Suc_unat_less_bound])
apply (subgoal_tac "args ! 4 \<le> 2 ^ capCNodeBits nodeCap")
prefer 2
apply (clarsimp simp: isCap_simps)
@ -808,7 +808,7 @@ lemma decodeUntyped_wf[wp]:
apply (simp add: unats_def)
apply (simp add: unats_def)
apply (rule inj_onI)
apply (clarsimp simp: toEnum_of_nat[OF less_Suc_unat_less_bound] ucast_id isCap_simps)
apply (clarsimp simp: toEnum_of_nat[OF less_Suc_unat_less_bound] isCap_simps)
apply (erule(2) inj_bits, simp add: word_bits_def cte_level_bits_def)
apply (subst Suc_unat_diff_1)
apply (rule word_le_plus_either,simp)
@ -932,7 +932,7 @@ lemma corres_list_all2_mapM_':
apply simp+
done
lemmas suffix_refl = suffix_order.order.refl
lemmas suffix_refl = suffix_order.refl
lemmas corres_list_all2_mapM_
= corres_list_all2_mapM_' [OF suffix_refl suffix_refl]
@ -1339,7 +1339,6 @@ lemma do_ext_op_update_cdt_list_symb_exec_l':
update_cdt_list_def set_cdt_list_def bind_def put_def get_def gets_def return_def)
done
crunch irq_node[wp]: update_cdt "\<lambda>s. P (interrupt_irq_node s)"
crunches updateMDB, updateNewFreeIndex
for it'[wp]: "\<lambda>s. P (ksIdleThread s)"
and ups'[wp]: "\<lambda>s. P (gsUserPages s)"
@ -1538,8 +1537,7 @@ shows
apply clarsimp
apply (erule (2) valid_dlistEn)
apply simp
apply(simp only: cdt_list_relation_def valid_mdb_def2
del: split_paired_All split_paired_Ex split del: if_split)
apply(simp only: cdt_list_relation_def valid_mdb_def2)
apply(subgoal_tac "finite_depth (cdt s)")
prefer 2
apply(simp add: finite_depth valid_mdb_def2[simplified,symmetric])
@ -1834,7 +1832,7 @@ lemma n'_rtrancl_eq:
(if p = site then p' \<noteq> site \<and> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
else if m \<turnstile> p \<leadsto>\<^sup>* parent then m \<turnstile> p \<leadsto>\<^sup>* p' \<or> p' = site
else m \<turnstile> p \<leadsto>\<^sup>* p')"
by (auto simp: rtrancl_eq_or_trancl n'_trancl_eq split)
by (auto simp: rtrancl_eq_or_trancl n'_trancl_eq)
lemma mdbNext_parent_site [simp]:
"mdbNext parent_node \<noteq> site"
@ -2256,7 +2254,7 @@ lemma mdb_chunked_n' [simp]:
apply (simp(no_asm) add: sameRegionAs_def3 isCap_simps)
apply (drule valid_capI')+
apply (drule valid_capAligned)+
apply (clarsimp simp: capAligned_def is_aligned_no_overflow interval_empty)
apply (clarsimp simp: capAligned_def is_aligned_no_overflow)
apply clarsimp
apply (erule disjE)
apply simp
@ -2716,7 +2714,6 @@ lemma no_default_zombie:
"cap_relation (default_cap tp p sz d) cap \<Longrightarrow> \<not>isZombie cap"
by (cases tp, auto simp: isCap_simps)
crunch typ_at'[wp]: updateNewFreeIndex "\<lambda>s. P (typ_at' T p s)"
lemmas updateNewFreeIndex_typ_ats[wp] = typ_at_lifts[OF updateNewFreeIndex_typ_at']
lemma updateNewFreeIndex_valid_objs[wp]:
@ -2806,8 +2803,6 @@ lemma insertNewCap_overlap_reserved'[wp]:
apply (erule(2) caps_overlap_reserved'_D)
done
crunch typ_at'[wp]: insertNewCap "\<lambda>s. P (typ_at' T p s)"
(wp: crunch_wps)
crunch ksArch[wp]: insertNewCap "\<lambda>s. P (ksArchState s)"
(wp: crunch_wps)
@ -2964,7 +2959,6 @@ 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)+
@ -3235,8 +3229,6 @@ lemmas corres_split_retype_createNewCaps
simplified bind_assoc, simplified ]
declare split_paired_Ex[simp add]
crunch cte_wp_at[wp]: do_machine_op "\<lambda>s. P (cte_wp_at P' p s)"
lemma retype_region_caps_overlap_reserved:
"\<lbrace>valid_pspace and valid_mdb and
pspace_no_overlap_range_cover ptr sz and caps_no_overlap ptr sz and
@ -3544,8 +3536,7 @@ lemma pspace_no_overlap_valid_untyped':
\<Longrightarrow> valid_untyped' d ptr bits idx s"
apply (clarsimp simp: valid_untyped'_def ko_wp_at'_def split del: if_split)
apply (frule(1) pspace_no_overlapD')
apply (simp add: obj_range'_def[symmetric] is_aligned_neg_mask_eq Int_commute
)
apply (simp add: obj_range'_def[symmetric] Int_commute)
apply (erule disjE)
apply (drule base_member_set[simplified field_simps])
apply (simp add: word_bits_def)
@ -4160,10 +4151,6 @@ lemma updateFreeIndex_descendants_of2:
crunch typ_at'[wp]: updateFreeIndex "\<lambda>s. P (typ_at' T p s)"
crunch pspace_aligned'[wp]: updateFreeIndex "pspace_aligned'"
crunch pspace_distinct'[wp]: updateFreeIndex "pspace_distinct'"
lemma updateFreeIndex_cte_wp_at:
"\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. P (cteCap_update (if p = slot
then capFreeIndex_update (\<lambda>_. idx) else id) c)) p s\<rbrace>
@ -4239,18 +4226,21 @@ lemma resetUntypedCap_corres:
apply (rule corres_split_nor[OF _ updateFreeIndex_corres])
apply (rule preemptionPoint_corres)
apply simp
apply (simp add: getFreeRef_def getFreeIndex_def
free_index_of_def)
apply (simp add: getFreeRef_def getFreeIndex_def free_index_of_def)
apply clarify
apply (subst unat_mult_simple)
apply (clarsimp )
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply (subst unat_p2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing, simp+)
apply (rule nat_less_power_trans2, simp_all)[1]
apply (simp add: unat_of_nat)
apply clarsimp
apply (subst unat_of_nat32)
apply (erule order_less_le_trans)
apply simp
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply simp
apply wp+
apply (rule corres_machine_op)
@ -4293,14 +4283,18 @@ lemma resetUntypedCap_corres:
apply (subst is_aligned_weaken[OF is_aligned_mult_triv2])
apply (simp add: Kernel_Config.resetChunkBits_def minUntypedSizeBits_def)
apply (subst unat_mult_simple)
apply (clarsimp)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply (subst unat_p2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing, simp+)
apply (rule nat_less_power_trans2, simp_all)[1]
apply (simp add: unat_of_nat)
apply simp
apply (rule order_less_imp_le, rule nat_less_power_trans2)
apply (simp add: unat_of_nat)
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply simp
apply simp
apply (clarsimp simp add: valid_cap_def cap_aligned_def)
@ -4432,7 +4426,6 @@ 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])