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

isabelle2021-1 ainvs arm: AInvs update 

Mostly word proof changes, and small number of places where tactics
solve more.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-11-17 09:44:18 +11:00 committed by Gerwin Klein
parent 71e78ac126
commit 9e8fea8dad
19 changed files with 75 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -352,6 +352,7 @@ lemma pde_at_aligned_vptr:
is_aligned_shiftl_self)+
apply (prove "pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits)")
subgoal
supply bit_simps[simp del]
apply (subst mask_lower_twice[symmetric, where n=6])
apply (simp add: pd_bits_def pageBits_def)
apply (subst add.commute, subst add_mask_lower_bits)
@ -392,11 +393,9 @@ lemma pde_shifting:
have H: "(0xF::word32) < 2 ^ 4" by simp
from prems show ?thesis
apply (subst (asm) word_plus_and_or_coroll)
apply (rule word_eqI)
apply word_eqI
subgoal for n
apply (clarsimp simp: word_size nth_shiftr is_aligned_nth)
apply (spec "n + 20")
apply (frule test_bit_size[where n="n + 20"])
apply (spec "20 + n")
apply (simp add: word_size)
apply (insert H)
apply (drule (1) order_le_less_trans)
@ -404,7 +403,6 @@ lemma pde_shifting:
apply (drule_tac z="2 ^ 4" in order_le_less_trans, assumption)
apply (drule word_power_increasing)
by simp+
apply (clarsimp simp: word_size nth_shiftl nth_shiftr is_aligned_nth)
apply (erule disjE)
apply (insert H)[1]
@ -412,8 +410,8 @@ lemma pde_shifting:
apply (drule bang_is_le)
apply (drule order_le_less_trans[where z="2 ^ 4"], assumption)
apply (drule word_power_increasing; simp)
apply (spec "n' + 20")
apply (frule test_bit_size[where n = "n' + 20"])
apply (spec "20 + n'")
apply (frule test_bit_size)
by (simp add: word_size)
qed
done

2
proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy
View File

@ -79,7 +79,7 @@ lemma replace_cap_invs:
apply (erule allEI, erule allEI)
apply (drule_tac x="fst p" in spec, drule_tac x="snd p" in spec)
apply (clarsimp simp: gen_obj_refs_subset)
apply (drule(1) disjoint_subset, simp)
apply (drule(1) disjoint_subset, erule (1) notE)
apply (rule conjI)
apply (erule descendants_inc_minor)
apply simp

3
proof/invariant-abstract/ARM/ArchCSpace_AI.thy
View File

@ -420,9 +420,6 @@ lemma tcb_cnode_index_def2 [CSpace_AI_assms]:
apply (rule nth_equalityI)
apply (simp add: word_bits_def)
apply (clarsimp simp: to_bl_nth word_size word_bits_def)
apply (subst of_nat_ucast[where 'a=32 and 'b=3])
apply (simp add: is_down_def target_size_def source_size_def word_size)
apply (simp add: nth_ucast del: unsigned_of_nat)
apply fastforce
done

2
proof/invariant-abstract/ARM/ArchDetype_AI.thy
View File

@ -71,7 +71,7 @@ next
x = ptr + of_nat n' * 4 + 2 \<or> x = ptr + of_nat n' * 4 + 3)"
by (simp add: xin' conj_disj_distribL ex_disj_distrib field_simps)
show "?thesis m x" by (simp add: xin word_rsplit_0 cong: if_cong)
show "?thesis m x" by (simp add: xin word_rsplit_0 word_bits_conv cong: if_cong)
qed
from al have "is_aligned (ptr + of_nat n' * 4) 2"

6
proof/invariant-abstract/ARM/ArchInvariants_AI.thy
View File

@ -1410,6 +1410,7 @@ lemmas abs_atyp_at_lifts =
lemma page_directory_pde_atI:
"\<lbrakk> page_directory_at p s; x < 2 ^ pageBits;
pspace_aligned s \<rbrakk> \<Longrightarrow> pde_at (p + (x << 2)) s"
supply bit_simps[simp del]
apply (clarsimp simp: obj_at_def pde_at_def)
apply (drule (1) pspace_alignedD[rotated])
apply (clarsimp simp: a_type_def
@ -1429,6 +1430,7 @@ lemma page_directory_pde_atI:
lemma page_table_pte_atI:
"\<lbrakk> page_table_at p s; x < 2^(pt_bits - 2); pspace_aligned s \<rbrakk> \<Longrightarrow> pte_at (p + (x << 2)) s"
supply bit_simps[simp del]
apply (clarsimp simp: obj_at_def pte_at_def)
apply (drule (1) pspace_alignedD[rotated])
apply (clarsimp simp: a_type_def
@ -1889,7 +1891,7 @@ proof -
apply (erule (6) 2)
apply (clarsimp simp: vs_refs_pages_def graph_of_def obj_at_def
pde_ref_pages_def data_at_def
dest!: vs_lookup_pages1D elim!: disjE
dest!: vs_lookup_pages1D
split: if_split_asm pde.splits)
apply (frule_tac d=ac in vpt, assumption+)
apply (erule converse_rtranclE)
@ -2431,7 +2433,7 @@ lemma valid_arch_mdb_eqI:
assumes "caps_of_state s = caps_of_state s'"
assumes "is_original_cap s = is_original_cap s'"
shows "valid_arch_mdb (is original_cap s') (caps_of_state s')"
by (clarsimp simp: valid_arch_mdb_def)
by clarsimp
lemma arch_tcb_context_absorbs[simp]:
"arch_tcb_context_set uc2 (arch_tcb_context_set uc1 a_tcb) \<equiv> arch_tcb_context_set uc2 a_tcb"

13
proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy
View File

@ -30,21 +30,20 @@ lemma asid_high_bits_of_add_ucast:
"is_aligned w asid_low_bits \<Longrightarrow>
asid_high_bits_of (ucast (x::10 word) + w) = asid_high_bits_of w"
apply (rule word_eqI)
apply (simp add: word_size asid_high_bits_of_def nth_ucast nth_shiftr is_aligned_nth)
apply (simp add: word_size asid_high_bits_of_def is_aligned_nth)
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: nth_ucast)
apply clarsimp
apply (drule test_bit_size)
apply (simp add: word_size asid_low_bits_def)
apply (auto dest: test_bit_size simp: word_size asid_low_bits_def nth_ucast)
apply (simp add: asid_low_bits_def)
apply (auto dest: test_bit_size simp: word_size asid_low_bits_def)
done
lemma asid_high_bits_of_add:
"\<lbrakk>is_aligned w asid_low_bits; x \<le> 2 ^ asid_low_bits - 1\<rbrakk>
\<Longrightarrow> asid_high_bits_of (w + x) = asid_high_bits_of w"
apply (rule word_eqI)
apply (simp add: word_size asid_high_bits_of_def nth_ucast nth_shiftr
is_aligned_nth)
apply (simp add: word_size asid_high_bits_of_def is_aligned_nth)
apply (drule le2p_bits_unset_32, simp add: asid_low_bits_def)
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
@ -52,7 +51,7 @@ lemma asid_high_bits_of_add:
apply (case_tac "na < asid_low_bits")
apply (simp add: asid_low_bits_def linorder_not_less word_bits_def)
apply (auto dest: test_bit_size
simp: asid_low_bits_def word_bits_def nth_ucast)
simp: asid_low_bits_def word_bits_def)
done
lemma pageBits_less_word_bits [simp]:

2
proof/invariant-abstract/ARM/ArchRetype_AI.thy
View File

@ -1264,7 +1264,7 @@ lemma storeWord_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
storeWord x 0
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
by (simp add: storeWord_def word_rsplit_0 | wp)+
by (simp add: storeWord_def word_rsplit_0 word_bits_conv | wp)+
lemma clearMemory_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>

2
proof/invariant-abstract/ARM/ArchSchedule_AI.thy
View File

@ -25,7 +25,7 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]:
apply (erule use_valid)
apply (simp add: storeWord_def word_rsplit_0)
apply wp
apply simp
apply (clarsimp simp: word_bits_conv)
done
crunch device_state_inv[wp]: clearExMonitor "\<lambda>ms. P (device_state ms)"

2
proof/invariant-abstract/ARM/ArchUntyped_AI.thy
View File

@ -18,7 +18,7 @@ lemma of_bl_nat_to_cref[Untyped_AI_assms]:
apply (clarsimp intro!: less_mask_eq
simp: nat_to_cref_def of_drop_to_bl
word_size word_less_nat_alt word_bits_def)
by (simp add: take_bit_nat_def)
by (metis add_lessD1 le_unat_uoi nat_le_iff_add nat_le_linear)
lemma cnode_cap_ex_cte[Untyped_AI_assms]:

8
proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy
View File

@ -115,8 +115,6 @@ lemma shift_0x3C_set:
nth_shiftl neg_mask_test_bit
word_bits_conv)
apply (safe, simp_all add: is_aligned_nth)[1]
apply (drule_tac x="Suc (Suc n)" in spec)
apply simp
apply (rule_tac x="ucast x && mask 4" in image_eqI)
apply (rule word_eqI[rule_format])
apply (drule_tac x=n in word_eqD)
@ -1089,7 +1087,7 @@ lemma neg_mask_pt_6_4:
(ptr::word32) && ~~ mask 6 && mask pt_bits >> 2"
apply (simp add:pt_bits_def pageBits_def)
apply word_bitwise
apply (simp add:word_size)
apply (simp add:word_size mask_def)
done
lemma neg_mask_pd_6_4:
@ -1097,7 +1095,7 @@ lemma neg_mask_pd_6_4:
(ptr::word32) && ~~ mask 6 && mask pd_bits >> 2"
apply (simp add:pd_bits_def pageBits_def)
apply word_bitwise
apply (simp add:word_size)
apply (simp add:word_size mask_def)
done
lemma mask_out_same_pt:
@ -1192,7 +1190,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (clarsimp simp :upto_enum_def upto_enum_step_def
Fun.comp_def upto_0_to_n2)
apply (cut_tac x = "of_nat x" and n = 2 in word_power_nonzero_32)
apply (simp add:word_of_nat_less word_bits_def of_nat_neq_0 del: word_of_nat_eq_0_iff)+
apply (simp add:word_of_nat_less word_bits_def of_nat_neq_0)+
done
have neq_pt_offset: "\<And>z zs xa (p::word32). \<lbrakk>[0 , 4 .e. 0x3C] = z # zs;
xa \<in> set zs;is_aligned p 6 \<rbrakk> \<Longrightarrow>

35
proof/invariant-abstract/ARM/ArchVSpace_AI.thy
View File

@ -83,15 +83,7 @@ lemma asid_low_high_bits':
asid_high_bits_of x = asid_high_bits_of y;
x \<le> 2 ^ asid_bits - 1; y \<le> 2 ^ asid_bits - 1 \<rbrakk>
\<Longrightarrow> x = y"
apply (rule asid_low_high_bits)
apply (rule word_eqI)
apply (subst (asm) bang_eq)
apply (simp add: nth_ucast asid_low_bits_def word_size)
apply (rule word_eqI)
apply (subst (asm) bang_eq)+
apply (simp add: nth_ucast asid_low_bits_def)
apply assumption+
done
by (rule asid_low_high_bits; (assumption|word_eqI_solve simp: asid_low_bits_def)?)
lemma table_cap_ref_at_eq:
"table_cap_ref c = Some [x] \<longleftrightarrow> vs_cap_ref c = Some [x]"
@ -680,34 +672,29 @@ lemma ex_asid_high_bits_plus:
apply (rule word_and_le1)
apply (subst (asm) mask_def)
apply (simp add: upper_bits_unset_is_l2p_32 [symmetric])
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size nth_ucast nth_shiftl)
apply (rule word_eqI)
apply (clarsimp simp: word_size nth_ucast nth_shiftl nth_shiftr asid_high_bits_of_def
asid_low_bits_def word_bits_def asid_bits_def)
apply (subst word_plus_and_or_coroll; word_eqI)
apply (clarsimp simp: asid_high_bits_of_def asid_low_bits_def word_bits_def asid_bits_def)
apply (rule iffI)
prefer 2
apply fastforce
apply (clarsimp simp: linorder_not_less)
apply (subgoal_tac "n < 17", simp)
apply (clarsimp simp add: linorder_not_le [symmetric])
done
by (metis add_One_commute add_diff_inverse_nat le_add1 less_diff_conv2 less_imp_diff_less
numeral_plus_numeral semiring_norm(10) semiring_norm(2) semiring_norm(3)
semiring_norm(4) semiring_norm(9))
lemma asid_high_bits_shl:
"\<lbrakk> is_aligned base asid_low_bits; base \<le> mask asid_bits \<rbrakk> \<Longrightarrow> ucast (asid_high_bits_of base) << asid_low_bits = base"
apply (simp add: mask_def upper_bits_unset_is_l2p_32 [symmetric])
apply (rule word_eqI[rule_format])
apply (simp add: is_aligned_nth nth_ucast nth_shiftl nth_shiftr asid_low_bits_def
asid_high_bits_of_def word_size asid_bits_def word_bits_def)
apply word_eqI
apply (simp add: asid_low_bits_def asid_high_bits_of_def word_bits_conv asid_bits_def)
apply (rule iffI, clarsimp)
apply (rule context_conjI)
apply (clarsimp simp add: linorder_not_less [symmetric])
apply simp
apply (subgoal_tac "n < 17", simp)
apply (clarsimp simp add: linorder_not_le [symmetric])
done
by (metis less_imp_le_nat linorder_neqE_nat nat_diff_less numeral_plus_numeral pl_pl_rels
semiring_norm(10) semiring_norm(2) semiring_norm(3) semiring_norm(8) semiring_norm(9)
trans_less_add1)
lemma valid_asid_map_unmap:

50
proof/invariant-abstract/CSpaceInv_AI.thy
View File

@ -496,7 +496,7 @@ lemma set_cap_cte_wp_at:
set_cap cap ptr
\<lbrace>\<lambda>uu s. cte_wp_at P p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (wpx set_cap_caps_of_state)
apply (wp set_cap_caps_of_state)
apply clarsimp
done
@ -506,7 +506,7 @@ lemma set_cap_cte_wp_at':
set_cap cap ptr
\<lbrace>\<lambda>uu s. cte_wp_at P p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (wpx set_cap_caps_of_state)
apply (wp set_cap_caps_of_state)
apply clarsimp
done
@ -536,7 +536,7 @@ lemma set_cap_tcb:
lemma set_cap_sets:
"\<lbrace>\<top>\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c = cap) p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (wpx set_cap_caps_of_state)
apply (wp set_cap_caps_of_state)
apply clarsimp
done
@ -655,13 +655,10 @@ lemma set_cap_cte_cap_wp_to:
\<and> ex_cte_cap_wp_to P p' s\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace>"
apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state)
apply wpx
apply (intro impI, elim conjE exE)
apply (case_tac "(a, b) = p")
apply fastforce
apply fastforce
done
apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state del: split_paired_Ex)
apply (wp hoare_vcg_ex_lift)
apply clarify
by (metis fun_upd_other fun_upd_same option.sel)
lemma set_cap_iflive:
@ -684,7 +681,7 @@ lemma update_cap_iflive:
"\<lbrace>cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p
and if_live_then_nonz_cap\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>"
apply (wpx set_cap_iflive)
apply (wp set_cap_iflive)
apply (clarsimp elim!: cte_wp_at_weakenE)
done
@ -701,7 +698,7 @@ lemma set_cap_ifunsafe:
\<and> (cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>"
apply (simp add: if_unsafe_then_cap_def)
apply (wpx set_cap_cte_cap_wp_to)
apply (wp set_cap_cte_cap_wp_to hoare_vcg_all_lift hoare_vcg_imp_lift)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_caps_of_state)
@ -720,7 +717,7 @@ lemma update_cap_ifunsafe:
and if_unsafe_then_cap
and (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace>
set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>"
apply (wpx set_cap_ifunsafe)
apply (wp set_cap_ifunsafe)
apply (clarsimp elim!: cte_wp_at_weakenE)
done
@ -737,8 +734,8 @@ lemma set_cap_globals [wp]:
"\<lbrace>valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range cap = {})\<rbrace>
set_cap cap p
\<lbrace>\<lambda>_. valid_global_refs\<rbrace>"
apply (simp add: valid_global_refs_def valid_refs_def2)
apply (wpx set_cap_caps_of_state)
apply (simp add: valid_global_refs_def valid_refs_def2 Ball_def)
apply (wp set_cap_caps_of_state hoare_vcg_all_lift hoare_vcg_imp_lift)
apply (clarsimp simp: ran_def)
apply blast
done
@ -1009,7 +1006,7 @@ lemma new_cap_valid_pspace:
set_cap cap p
\<lbrace>\<lambda>rv. valid_pspace\<rbrace>"
apply (simp add: valid_pspace_def)
apply (wpx set_cap_valid_objs new_cap_iflive new_cap_ifunsafe new_cap_zombies)
apply (wp set_cap_valid_objs new_cap_iflive new_cap_ifunsafe new_cap_zombies)
apply (auto simp: cte_wp_at_caps_of_state)
done
@ -1244,7 +1241,7 @@ lemma delete_duplicate_valid_pspace:
set_cap cap.NullCap p
\<lbrace>\<lambda>rv. valid_pspace\<rbrace>"
apply (simp add: valid_pspace_def)
apply (wpx set_cap_valid_objs delete_duplicate_iflive delete_duplicate_ifunsafe
apply (wp set_cap_valid_objs delete_duplicate_iflive delete_duplicate_ifunsafe
set_cap_zombies, auto elim!: cte_wp_at_weakenE)
done
@ -1258,7 +1255,7 @@ lemma set_cap_valid_pspace:
set_cap cap p
\<lbrace>\<lambda>rv. valid_pspace\<rbrace>"
apply (simp add: valid_pspace_def)
apply (wpx set_cap_valid_objs set_cap_iflive set_cap_zombies)
apply (wp set_cap_valid_objs set_cap_iflive set_cap_zombies)
apply (clarsimp elim!: cte_wp_at_weakenE | rule conjI)+
done
@ -1289,7 +1286,7 @@ lemma set_cap_idle[wp]:
lemma set_cap_cte_at_neg[wp]:
"\<lbrace>\<lambda>s. \<not> cte_at sl s\<rbrace> set_cap cap sl' \<lbrace>\<lambda>rv s. \<not> cte_at sl s\<rbrace>"
apply (simp add: cte_at_typ)
apply (wpx set_cap_typ_at)
apply (wp set_cap_typ_at)
done
lemma set_cap_cte_wp_at_neg:
@ -1338,10 +1335,10 @@ lemma set_cap_irq_handlers:
\<and> cte_wp_at (\<lambda>cap'. \<forall>irq \<in> cap_irqs cap - cap_irqs cap'. irq_issued irq s) ptr s\<rbrace>
set_cap cap ptr
\<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>"
apply (simp add: valid_irq_handlers_def irq_issued_def)
apply wpx
apply (simp add: valid_irq_handlers_def irq_issued_def Ball_def)
apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift)
apply (clarsimp simp: cte_wp_at_caps_of_state elim!: ranE split: if_split_asm)
apply (auto intro: ranI)
apply auto
done
lemma arch_obj_caps_of:
@ -1819,7 +1816,7 @@ lemma cap_insert_ex_cap:
apply (simp add: cap_insert_def)
apply (wp|simp split del: if_split)+
apply (wp set_cap_cap_to get_cap_wp set_cap_cte_wp_at set_untyped_cap_as_full_cte_wp_at)+
apply (clarsimp simp: set_untyped_cap_as_full_def split del: if_splits)
apply (clarsimp simp: set_untyped_cap_as_full_def split del: if_split)
apply (wp set_cap_cap_to get_cap_wp)+
apply (clarsimp elim!: cte_wp_at_weakenE simp: is_cap_simps cte_wp_at_caps_of_state)
apply (simp add: masked_as_full_def)
@ -1865,7 +1862,7 @@ lemma cap_insert_ifunsafe:
apply (simp add: cap_insert_def)
apply (wp get_cap_wp | simp split del: if_split)+
apply (rule new_cap_ifunsafe)
apply (simp add: set_untyped_cap_as_full_def split del: if_splits)
apply (simp add: set_untyped_cap_as_full_def split del: if_split)
apply (wp set_cap_cte_wp_at set_cap_ifunsafe set_cap_cte_cap_wp_to get_cap_wp)+
apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state)
apply (rule untyped_cap_update_ex_cte_cap_wp_to)
@ -1907,7 +1904,7 @@ lemma cap_insert_cap_wp_to[wp]:
cte_wp_at_caps_of_state update_cdt_def)
apply (wp get_cap_wp | simp split del: if_split)+
apply (rule allI)
apply (clarsimp simp del: split_def,rule conjI)
apply (clarsimp, rule conjI)
apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state)
apply (rule_tac x = a in exI)
apply (rule_tac x = b in exI)
@ -2002,8 +1999,7 @@ lemma set_untyped_cap_full_valid_objs:
\<lbrace>\<lambda>r. valid_objs\<rbrace>"
apply (simp add: set_untyped_cap_as_full_def split del: if_split)
apply (wp set_cap_valid_objs)
apply (clarsimp simp: valid_cap_free_index_update tcb_cap_valid_caps_of_stateD
cte_wp_at_caps_of_state caps_of_state_valid_cap)
apply (clarsimp simp: tcb_cap_valid_caps_of_stateD cte_wp_at_caps_of_state caps_of_state_valid_cap)
done

4
proof/invariant-abstract/CSpace_AI.thy
View File

@ -388,9 +388,7 @@ lemma of_bl_take:
"length xs < len_of TYPE('a) \<Longrightarrow> of_bl (take n xs) = ((of_bl xs) >> (length xs - n) :: ('a :: len) word)"
apply (clarsimp simp: bang_eq and_bang test_bit_of_bl
rev_take conj_comms nth_shiftr)
apply safe
apply simp_all
apply (clarsimp elim!: rsubst[where P="\<lambda>x. rev xs ! x"])+
apply auto
done

23
proof/invariant-abstract/LevityCatch_AI.thy
View File

@ -105,18 +105,15 @@ lemma mask_split_aligned_neg:
shows "(p && ~~ mask m) + (ucast x << a) = p \<Longrightarrow> False"
apply (subst (asm) word_plus_and_or_coroll)
apply (clarsimp simp: word_simps bang_eq)
subgoal for n
apply (drule test_bit_size)
apply (clarsimp simp: word_simps)
using len by arith
apply (metis bit_imp_le_length diff_add_inverse le_add1 len(2) less_diff_iff)
apply (insert x)
apply (erule notE)
apply (rule word_eqI)
apply word_eqI
subgoal for n
using len
apply (clarsimp simp: word_simps bang_eq)
apply (clarsimp)
apply (spec "n + a")
by (clarsimp simp: word_ops_nth_size word_size)
by (clarsimp simp: add.commute)
done
lemma mask_alignment_ugliness:
@ -126,14 +123,8 @@ lemma mask_alignment_ugliness:
\<forall>n \<ge> m. \<not>z !! n\<rbrakk>
\<Longrightarrow> False"
apply (erule notE)
apply (rule word_eqI)
apply (clarsimp simp: is_aligned_nth word_ops_nth_size word_size)
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size)
subgoal for \<dots> na
apply (spec na)+
by simp
by auto
apply (subst word_plus_and_or_coroll; word_eqI)
apply (meson linorder_not_le)
by (auto simp: le_def)
end

2
proof/invariant-abstract/Retype_AI.thy
View File

@ -278,7 +278,7 @@ lemma range_cover_le_n_less:
lemma unat_of_nat_n :"unat ((of_nat n):: 'a :: len word) = n"
using range_cover_n_less
by (simp add:unat_of_nat del: unsigned_of_nat)
by (simp add:unat_of_nat)
lemma unat_of_nat_n_shift:

6
proof/invariant-abstract/Schedule_AI.thy
View File

@ -54,10 +54,10 @@ lemma findM_inv'':
apply simp
done
lemmas findM_inv' = findM_inv''[OF suffix_order.order.refl]
lemmas findM_inv' = findM_inv''[OF suffix_order.refl]
lemma findM_inv:
assumes x: "\<And>x xs. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. P\<rbrace>"
assumes x: "\<And>x. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. P\<rbrace>"
shows "\<lbrace>P\<rbrace> findM m xs \<lbrace>\<lambda>rv. P\<rbrace>"
by (rule findM_inv', simp_all add: x)
@ -78,7 +78,7 @@ lemma postfix_tails:
apply clarsimp
apply clarsimp
apply (erule meta_allE, erule meta_allE, drule meta_mp,
rule suffix_appendI[OF suffix_order.order.refl])
rule suffix_appendI[OF suffix_order.refl])
apply clarsimp
apply (erule suffix_ConsI)
done

5
proof/invariant-abstract/TcbAcc_AI.thy
View File

@ -892,10 +892,9 @@ lemma get_cap_aligned:
lemma shiftr_eq_mask_eq:
"a && ~~ mask b = c && ~~ mask b \<Longrightarrow> a >> b = c >> b"
apply (rule word_eqI)
apply (drule_tac x="n + b" in word_eqD)
apply (case_tac "n + b < size a")
apply (drule_tac x="b + n" in word_eqD)
apply (case_tac "b + n < size a")
apply (simp add: nth_shiftr word_size word_ops_nth_size)
apply (simp add: nth_shiftr)
apply (auto dest!: test_bit_size simp: word_size)
done

10
proof/invariant-abstract/Untyped_AI.thy
View File

@ -419,10 +419,8 @@ lemma range_cover_stuff:
apply simp
apply (subst shiftl_shiftr1)
apply (simp_all add: word_size)
apply (rule bit_eqI)
apply (simp add: word_bits_conv shiftl_word_eq bit_and_iff bit_push_bit_iff bit_1_iff bit_mask_iff bit_exp_iff not_le)
apply auto
done
apply (word_eqI_solve simp: word_bits_conv)
done
have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz"
using bound cmp not_0
@ -478,7 +476,7 @@ lemma range_cover_stuff:
apply (subst unat_shiftl_absorb[where p = "sz - bits"])
apply (rule order_trans[OF le_shiftr])
apply (rule space)
apply (simp add: shiftr_div_2n_w word_bits_def)+
apply (simp add: word_bits_def power_minus_is_div)+
apply (simp add: shiftl_t2n[symmetric] field_simps shiftr_shiftl1)
apply (subst is_aligned_diff_neg_mask[OF is_aligned_weaken])
apply (rule is_aligned_triv)
@ -512,7 +510,7 @@ lemma range_cover_stuff:
apply (subst word_of_nat_le)
apply (subst unat_power_lower_machine)
apply ((simp add: word_bits_def)+)[3]
apply (simp del: word_of_nat_eq_0_iff)
apply simp
apply (erule of_nat_neq_0)
apply (erule le_less_trans)
apply (rule power_strict_increasing)

10
proof/invariant-abstract/VSpaceEntries_AI.thy
View File

@ -87,16 +87,6 @@ lemma ucast_neg_mask:
apply (auto simp:nth_ucast neg_mask_test_bit word_size)
done
lemma shiftr_eq_neg_mask_eq:
"a >> b = c >> b \<Longrightarrow> a && ~~ mask b = c && ~~ mask b"
apply (rule word_eqI[rule_format])
apply (simp add:neg_mask_test_bit)
apply (drule_tac f = "\<lambda>x. x !! (n - b)" in arg_cong)
apply (simp add:nth_shiftr)
apply (rule iffI)
apply simp+
done
lemma delete_objects_reduct:
"valid (\<lambda>s. P (kheap (s :: ('z::state_ext) state))) (modify (detype {ptr..ptr + 2 ^ bits - 1}))
(\<lambda>_ s. P(kheap (s :: ('z::state_ext) state))) \<Longrightarrow>