From 239037906e7e24d3a97f5a72d8b12626b95614cf Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 23 Feb 2021 17:43:27 +1100 Subject: [PATCH] isabelle-2021: update InfoFlow Signed-off-by: Gerwin Klein --- proof/infoflow/ADT_IF.thy | 9 +-- proof/infoflow/Arch_IF.thy | 10 ++-- proof/infoflow/Example_Valid_State.thy | 82 +++++++++++++------------- proof/infoflow/FinalCaps.thy | 3 +- proof/infoflow/Noninterference.thy | 6 +- proof/infoflow/Scheduler_IF.thy | 1 + proof/infoflow/Tcb_IF.thy | 1 - proof/infoflow/UserOp_IF.thy | 3 +- 8 files changed, 55 insertions(+), 60 deletions(-) diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 1783f9758..cfcb931ac 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -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': "\P\ f \Q\,\E\ \ \P\ f -,\E\" diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy index 59c563298..ac6bafe4e 100644 --- a/proof/infoflow/Arch_IF.thy +++ b/proof/infoflow/Arch_IF.thy @@ -136,12 +136,10 @@ lemma get_asid_pool_revrv': apply(rule_tac W="\rv rv'. aag_can_read aag ptr \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)+ diff --git a/proof/infoflow/Example_Valid_State.thy b/proof/infoflow/Example_Valid_State.thy index 40b9175f1..9a3d71874 100644 --- a/proof/infoflow/Example_Valid_State.thy +++ b/proof/infoflow/Example_Valid_State.thy @@ -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 \ nat \ 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) \ 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) \ 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 \ ucast x << 20") - apply (subgoal_tac "0xFFFFF + (ucast x << 20) \ 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 \ ucast x << 20") + apply (subgoal_tac "0xFFFFF + (ucast x << 20) \ 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" diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index ac819de69..311e3bae3 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -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) diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index ab3075c0a..7ad7f79e7 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -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)" diff --git a/proof/infoflow/Scheduler_IF.thy b/proof/infoflow/Scheduler_IF.thy index c9d1f9c9f..c4381ae3a 100644 --- a/proof/infoflow/Scheduler_IF.thy +++ b/proof/infoflow/Scheduler_IF.thy @@ -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) diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy index 963d83b64..60afc111b 100644 --- a/proof/infoflow/Tcb_IF.thy +++ b/proof/infoflow/Tcb_IF.thy @@ -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="\_. pas_refined aag"] check_cap_inv2[where Q="\_ s. t \ idle_thread s"] out_invs_trivial case_option_wpE cap_delete_deletes cap_delete_valid_cap cap_insert_valid_cap out_cte_at diff --git a/proof/infoflow/UserOp_IF.thy b/proof/infoflow/UserOp_IF.thy index aac4c3e4b..990641c7c 100644 --- a/proof/infoflow/UserOp_IF.thy +++ b/proof/infoflow/UserOp_IF.thy @@ -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]