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

isabelle-2021: update InfoFlow 

Signed-off-by: Gerwin Klein <kleing@unsw.edu.au>
This commit is contained in:
Gerwin Klein 2021-02-23 17:43:27 +11:00 committed by Gerwin Klein
parent 9e5a7583fc
commit 239037906e
8 changed files with 55 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
proof/infoflow/ADT_IF.thy
View File

@ -2845,19 +2845,12 @@ lemma preemption_point_irq_state_inv'[wp]:
dmo_getActiveIRQ_wp
| wpc
| simp add: reset_work_units_def)+
apply (elim conjE)
apply simp
apply (wp OR_choiceE_wp[where P'="irq_state_inv st" and P''="irq_state_inv st"]
dmo_getActiveIRQ_wp
| wpc
| simp add: reset_work_units_def)+
apply(clarsimp simp: irq_state_inv_def)
apply(simp add: next_irq_state_Suc[OF _ recurring_next_irq_state_dom])
apply (clarsimp simp: irq_state_next_def)
apply(simp add: next_irq_state_Suc'[OF _ recurring_next_irq_state_dom])
apply(wp | simp add: update_work_units_def irq_state_inv_def | fastforce)+
done
done
lemma validE_validE_E':
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>"

10
proof/infoflow/Arch_IF.thy
View File

@ -136,12 +136,10 @@ lemma get_asid_pool_revrv':
apply(rule_tac W="\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow>rv = rv'" in equiv_valid_rv_bind)
apply(rule get_object_revrv')
apply(case_tac "aag_can_read aag ptr")
apply(simp)
apply(case_tac rv')
apply(simp | rule fail_ev2_l)+
apply(rename_tac arch_kernel_obj)
apply(case_tac arch_kernel_obj)
apply(simp | rule return_ev2 | rule fail_ev2_l)+
apply(simp split: kernel_object.splits)
apply(rule conjI | clarsimp | rule fail_ev2_l)+
apply(simp split: arch_kernel_obj.splits)
apply(rule conjI | clarsimp | rule return_ev2 | rule fail_ev2_l)+
apply(clarsimp simp: equiv_valid_2_def)
apply(case_tac rv)
apply(clarsimp simp: fail_def)+

82
proof/infoflow/Example_Valid_State.thy
View File

@ -280,9 +280,7 @@ where
Some $ bin_to_bl bits (of_nat n)"
lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)"
apply (clarsimp simp: nat_to_bl_def to_bl_def)
apply (auto simp: uint_nat le_def word_size)
done
by (clarsimp simp: nat_to_bl_def to_bl_def le_def word_size)
definition
the_nat_to_bl :: "nat \<Rightarrow> nat \<Rightarrow> bool list"
@ -333,13 +331,13 @@ lemma nat_to_bl_eq:
apply (erule_tac x="b div 2" in allE)
apply (erule impE)
apply (metis power_commutes td_gal_lt zero_less_numeral)
apply (clarsimp simp: bin_rest_def bin_last_def zdiv_int)
apply (clarsimp simp: bin_last_def zdiv_int)
apply (rule iffI [rotated], clarsimp)
apply (subst (asm) (1 2 3 4) bin_to_bl_aux_alt)
apply (clarsimp simp: mod_eq_dvd_iff)
apply (subst split_div_mod [where k=2])
apply clarsimp
apply (metis of_nat_numeral not_mod_2_eq_0_eq_1 of_nat_1 of_nat_eq_iff zmod_int)
apply presburger
done
lemma nat_to_bl_mod_n_eq [simp]:
@ -1266,7 +1264,7 @@ lemma valid_obj_s0[simp]:
shared_page_ptr_def
valid_vm_rights_def vm_kernel_only_def
kernel_base_def pageBits_def pt_bits_def vmsz_aligned_def
is_aligned_def[THEN meta_eq_to_obj_eq, THEN iffD2]
is_aligned_def[THEN iffD2]
is_aligned_addrFromPPtr_n)+
apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
valid_ipc_buffer_cap_def valid_tcb_state_def valid_arch_tcb_def
@ -1274,7 +1272,7 @@ lemma valid_obj_s0[simp]:
is_valid_vtable_root_def)+
apply (simp add: valid_vm_rights_def vm_kernel_only_def
kernel_base_def pageBits_def vmsz_aligned_def
is_aligned_def[THEN meta_eq_to_obj_eq, THEN iffD2]
is_aligned_def[THEN iffD2]
is_aligned_addrFromPPtr_n)
done
@ -1313,12 +1311,14 @@ lemma pspace_distinct_s0:
apply (clarsimp simp: s0_ptr_defs cte_level_bits_def)
apply (case_tac "(ucast irq << 4) < (ucast irqa << 4)")
apply (frule udvd_decr'[where K="0x10::32 word" and ua=0, simplified])
apply (simp add: shiftl_t2n uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^4" and b="2^28", simplified])
apply simp
apply (simp add: shiftl_t2n uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^4" and b="2^28", simplified])
apply simp
apply (simp add: shiftl_t2n uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^4" and b="2^28", simplified])
apply simp
apply (simp add: uint_shiftl word_size bintrunc_shiftl)
apply (simp add: shiftl_int_def take_bit_eq_mod)
apply (frule_tac y="ucast irq << 4" in word_plus_mono_right[where x="0xE000800F"])
apply (simp add: shiftl_t2n)
apply (case_tac "(1::32 word) \<le> ucast irqa")
@ -1359,12 +1359,14 @@ lemma pspace_distinct_s0:
apply simp
apply (case_tac "(ucast irq << 4) > (ucast irqa << 4)")
apply (frule udvd_decr'[where K="0x10::32 word" and ua=0, simplified])
apply (simp add: shiftl_t2n uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^4" and b="2^28", simplified])
apply simp
apply (simp add: shiftl_t2n uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^4" and b="2^28", simplified])
apply simp
apply (simp add: shiftl_t2n uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^4" and b="2^28", simplified])
apply simp
apply (simp add: uint_shiftl word_size bintrunc_shiftl)
apply (simp add: shiftl_int_def take_bit_eq_mod)
apply (frule_tac y="ucast irqa << 4" in word_plus_mono_right[where x="0xE000800F"])
apply (simp add: shiftl_t2n)
apply (case_tac "(1::32 word) \<le> ucast irq")
@ -1689,41 +1691,41 @@ lemma valid_global_pd_mappings_s0[simp]:
apply simp
apply simp
apply (case_tac "ucast x << 20 < (0xE0000000::32 word)")
apply (subgoal_tac "(0xE0000000::32 word) - 0x100000 \<ge> ucast x << 20")
apply (subgoal_tac "0xFFFFF + (ucast x << 20) \<le> 0xDFFFFFFF")
apply (drule_tac y="0xFFFFF + (ucast x << 20)" and z="0xDFFFFFFF::32 word" in order_trans_rules(23))
apply simp
apply ((drule(1) order_trans_rules(23))+, force)
apply (simp add: add.commute
word_plus_mono_left[where x="0xFFFFF" and z="0xDFF00000", simplified])
apply (simp add: shiftl_t2n)
apply (rule udvd_decr'[where K="0x100000" and q="0xE0000000" and ua=0, simplified])
apply (subgoal_tac "(0xE0000000::32 word) - 0x100000 \<ge> ucast x << 20")
apply (subgoal_tac "0xFFFFF + (ucast x << 20) \<le> 0xDFFFFFFF")
apply (drule_tac y="0xFFFFF + (ucast x << 20)" and z="0xDFFFFFFF::32 word" in order_trans_rules(23))
apply simp
apply ((drule(1) order_trans_rules(23))+, force)
apply (simp add: add.commute)
apply (simp add: word_plus_mono_left[where x="0xFFFFF" and z="0xDFF00000", simplified])
apply (simp add: shiftl_t2n)
apply (rule udvd_decr'[where K="0x100000" and q="0xE0000000" and ua=0, simplified])
apply simp
apply (simp add: uint_word_ariths)
apply (subst mod_mult_mult1[where c="2^20" and b="2^12", simplified])
apply simp
apply simp
apply simp
apply (erule notE)
apply (cut_tac x="ucast x::32 word" and n=20 in shiftl_shiftr_id)
apply simp
apply (simp add: ucast_less[where 'b=12, simplified])
apply simp
apply (rule ucast_up_inj[where 'b=32])
apply (erule notE)
apply (cut_tac x="ucast x::32 word" and n=20 in shiftl_shiftr_id)
apply simp
apply simp
apply (drule_tac c="0xFFFFF + (ucast x << 20)" and d="0xFFFFF" and b="0xFFFFF" in word_sub_mono)
apply simp
apply (rule word_sub_le)
apply (rule order_trans_rules(23)[rotated], assumption)
apply simp
apply (simp add: add.commute)
apply (rule no_plus_overflow_neg)
apply simp
apply (drule_tac x="ucast x << 20" in order_trans_rules(23), assumption)
apply (simp add: le_less_trans)
apply (simp add: ucast_less[where 'b=12, simplified])
apply simp
done
apply (rule ucast_up_inj[where 'b=32])
apply simp
apply simp
apply (drule_tac c="0xFFFFF + (ucast x << 20)" and d="0xFFFFF" and b="0xFFFFF" in word_sub_mono)
apply simp
apply (rule word_sub_le)
apply (rule order_trans_rules(23)[rotated], assumption)
apply simp
apply (simp add: add.commute)
apply (rule no_plus_overflow_neg)
apply simp
apply (drule_tac x="ucast x << 20" in order_trans_rules(23), assumption)
apply (simp add: le_less_trans)
apply simp
done
lemma pspace_in_kernel_window_s0[simp]:
"pspace_in_kernel_window s0_internal"

3
proof/infoflow/FinalCaps.thy
View File

@ -1305,9 +1305,10 @@ lemma reply_cancel_ipc_silc_inv:
apply wps
apply (wp static_imp_wp hoare_vcg_all_lift hoare_vcg_ball_lift)
apply clarsimp
apply (rename_tac b a)
apply (frule(1) descendants_of_owned_or_transferable, force, force, elim disjE)
apply (clarsimp simp add:silc_inv_def)
apply (case_tac "cdt s (aa,ba)")
apply (case_tac "cdt s (a,b)")
apply (fastforce dest: descendants_of_NoneD)
apply (elim is_transferable.cases)
apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at simp: cte_wp_at_caps_of_state)

6
proof/infoflow/Noninterference.thy
View File

@ -638,7 +638,6 @@ lemma dmo_device_memory_update_globals_equiv_scheduler:
apply clarsimp
apply(simp add: device_memory_update_def simpler_modify_def)
apply(clarsimp simp: globals_equiv_scheduler_def split: option.splits)
apply blast
done
@ -3109,9 +3108,11 @@ lemma kernel_schedule_if_confidentiality:
apply(case_tac u, simp_all)
apply(frule (6) uwr_reads_equiv_f_g_affects_equiv)
apply(simp split: prod.splits)
apply(rename_tac x1 x1' x2 x1'' x2')
supply [[simproc del: defined_all]]
apply(case_tac s', case_tac t')
apply(simp add: split_paired_all)
apply(frule_tac s=x2 and t=x2a and s2=x2
apply(frule_tac s=x2 and t=x2' and s2=x2
in use_ev[OF schedule_if_reads_respects_f_g
[where st=s0_internal, OF current_domains_distinct]])
apply assumption
@ -3490,7 +3491,6 @@ lemma small_Step_confidentiality_part_not_PSched:
| simp_all add: not_schedule_modes_KernelEntry)+)[1]
apply(drule do_user_op_A_if_confidentiality'[
where s=s and t=t and s'=s' and t'=t' and u=u],simp+)
apply blast
apply(drule do_user_op_A_if_confidentiality'[
where s=s and t=t and s'=s' and t'=t' and u=u], simp+)
apply(drule_tac s=s and t=t and u=u and s'="(aa,ba)"

1
proof/infoflow/Scheduler_IF.thy
View File

@ -1653,6 +1653,7 @@ lemma reads_respects_scheduler_invisible_domain_switch:
apply (rule equiv_valid_2_bind_pre[where R'=dc])
apply (rule equiv_valid_2_bind_pre[where R'="(=)"])
apply simp
apply (rename_tac rv'b)
apply (rule_tac P="rv'b = choose_new_thread" in EquivValid.gen_asm_ev2_l)
apply simp
apply (rule equiv_valid_2_bind_pre)

1
proof/infoflow/Tcb_IF.thy
View File

@ -354,7 +354,6 @@ shows "
hoare_vcg_E_elim hoare_vcg_const_imp_lift_R
hoare_vcg_R_conj
| (wp
check_cap_inv2[where Q="\<lambda>_. pas_refined aag"]
check_cap_inv2[where Q="\<lambda>_ s. t \<noteq> idle_thread s"]
out_invs_trivial case_option_wpE cap_delete_deletes
cap_delete_valid_cap cap_insert_valid_cap out_cte_at

3
proof/infoflow/UserOp_IF.thy
View File

@ -236,7 +236,8 @@ lemma requiv_ptable_rights_eq:
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
vspace_cap_rights_to_auth_def)+)[4]
apply clarsimp
apply (frule_tac r=ba in some_get_page_info_kmapsD)
apply (rename_tac b)
apply (frule_tac r=b in some_get_page_info_kmapsD)
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
vspace_cap_rights_to_auth_def)+)[4]