diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 37dc81ace..8a05a9d91 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -3061,7 +3061,7 @@ lemma reset_untyped_cap_irq_state_inv: preemption_point_irq_state_inv'[where irq=irq] get_cap_wp | rule irq_state_inv_triv - | simp + | simp add: unless_def | wp_once dmo_wp)+ done diff --git a/proof/infoflow/Example_Valid_StateH.thy b/proof/infoflow/Example_Valid_StateH.thy index 0e3a16f13..191a166e4 100644 --- a/proof/infoflow/Example_Valid_StateH.thy +++ b/proof/infoflow/Example_Valid_StateH.thy @@ -1107,6 +1107,7 @@ where High_cnode_ptr \ 10, Silc_cnode_ptr \ 10, irq_cnode_ptr \ 0), + gsUntypedZeroRanges = ran (map_comp untypedZeroRange (option_map cteCap o map_to_ctes kh0H)), gsMaxObjectSize = card (UNIV :: word32 set), ksDomScheduleIdx = 0, ksDomSchedule = [(0 ,10), (1, 10)], @@ -1547,6 +1548,11 @@ lemma map_to_ctes_kh0H: ((clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None irq_node_offs_in_range | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1])+ +lemma option_update_range_map_comp: + "option_update_range m m' = map_add m' m" + by (simp add: fun_eq_iff option_update_range_def map_comp_def map_add_def + split: option.split) + lemma tcb_offs_in_rangeI: "\ptr \ ptr + x; ptr + x \ ptr + 2 ^ 9 - 1\ \ ptr + x \ tcb_offs_range ptr" by (simp add: tcb_offs_range_def) @@ -3034,16 +3040,11 @@ lemma s0H_invs: apply (clarsimp split: split_if_asm) apply (rule conjI) apply (clarsimp simp: kdr_pspace_domain_valid) (* use axiomatization for now *) - apply (rule conjI) - apply (clarsimp simp: s0H_internal_def) - apply (rule conjI) - apply (clarsimp simp: s0H_internal_def) - apply (rule conjI) - apply (clarsimp simp: s0H_internal_def maxDomain_def numDomains_def dschDomain_def dschLength_def) - apply (rule conjI) - apply (clarsimp simp: s0H_internal_def newKernelState_def newKSDomSched) - apply (rule conjI) - apply (clarsimp simp: s0H_internal_def newKernelState_def newKSDomSched) + (* unfold s0H_internal for remaining goals *) + apply (clarsimp simp: s0H_internal_def cteCaps_of_def + untyped_ranges_zero_inv_def + maxDomain_def numDomains_def dschDomain_def dschLength_def) + apply (clarsimp simp: newKernelState_def newKSDomSched) apply (clarsimp simp: cur_tcb'_def obj_at'_def projectKO_eq project_inject s0H_internal_def objBitsKO_def s0_ptrs_aligned) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified s0H_internal_def]) apply (simp add: objBitsKO_def kh0H_simps[simplified cte_level_bits_def]) diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index b98390644..a7a6298d2 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -2116,7 +2116,7 @@ lemma reset_untyped_cap_silc_inv: apply (rule hoare_gen_asm) apply (simp add: reset_untyped_cap_def cong: if_cong) apply (rule validE_valid, rule hoare_pre) - apply (wp set_cap_silc_inv_simple | simp)+ + apply (wp set_cap_silc_inv_simple | simp add: unless_def)+ apply (rule valid_validE, rule_tac Q="\_. cte_wp_at is_untyped_cap slot and silc_inv aag st" in hoare_strengthen_post) apply (rule validE_valid, rule mapME_x_inv_wp, rule hoare_pre) diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index beb1a5933..c4bf1f83c 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -2548,12 +2548,19 @@ lemma partitionIntegrity_irq_state_update[simp]: apply(cut_tac s=y and aag=aag in partitionIntegrity_refl) apply(clarsimp simp: partitionIntegrity_def integrity_subjects_def domain_fields_equiv_def globals_equiv_scheduler_def silc_dom_equiv_def equiv_for_def) done - + +lemma invs_if_Invs: + "invs_if s + \ Invs (internal_state_if s) + \ det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s)" + by (simp add: invs_if_def) + lemma do_user_op_A_if_confidentiality: notes read_respects_irq = use_ev[OF check_active_irq_if_reads_respects_f_g[ - where st=s0_internal and st'=s0_internal and irq=timer_irq]] and + where st=s0_internal and st'=s0_internal and irq=timer_irq + and aag="current_aag (internal_state_if s)"]] and read_respects_user_op = use_ev[OF do_user_op_if_reads_respects_f_g[ where aag="current_aag (internal_state_if s)" and st="s0_internal"]] @@ -2577,10 +2584,9 @@ lemma do_user_op_A_if_confidentiality: H: "(_,_) \ fst (check_active_irq_if _ p)" for p q \ \rule revcut_rl[OF read_respects_irq[where t=q, OF H]]\) apply assumption - apply (clarsimp simp: invs_if_def Invs_def) - apply assumption - apply(clarsimp simp: invs_if_def Invs_def) - apply(drule uwr_PSched_cur_domain) + apply (clarsimp dest!: invs_if_Invs simp: Invs_def) + apply (drule uwr_PSched_cur_domain) + apply (clarsimp dest!: invs_if_Invs simp: Invs_def) apply(clarsimp simp: current_aag_def) apply simp apply fastforce @@ -2591,7 +2597,8 @@ lemma do_user_op_A_if_confidentiality: apply assumption apply (match premises in "s = ((_,p),_)" and H: "(_,_) \ fst (check_active_irq_if _ p)" for p \ \rule revcut_rl[OF use_valid[OF H check_active_irq_if_User_det_inv]]\) - apply (clarsimp simp: invs_if_def Invs_def cur_thread_context_of_def) + apply (simp(no_asm_use) add: invs_if_def Invs_def cur_thread_context_of_def) + apply (clarsimp simp only: simp_thms) apply simp apply (erule use_valid) apply(wp check_active_irq_if_wp) @@ -2601,7 +2608,8 @@ lemma do_user_op_A_if_confidentiality: apply (simp add: active_from_running)+ apply (match premises in "t_aux = (_,q)" and H: "(_,q) \ fst (check_active_irq_if _ _)" for q \ \rule revcut_rl[OF use_valid[OF H check_active_irq_if_User_det_inv]]\) - apply (clarsimp simp: invs_if_def Invs_def cur_thread_context_of_def) + apply (simp(no_asm_use) add: invs_if_def Invs_def cur_thread_context_of_def) + apply (clarsimp simp only: simp_thms) apply simp apply(erule_tac s'=yc in use_valid) apply(wp check_active_irq_if_wp) @@ -2615,19 +2623,21 @@ lemma do_user_op_A_if_confidentiality: apply (match premises in "t = ((_,q),_)" for q \ \rule revcut_rl[OF current_aag_def[where t=q]]\) apply (rule guarded_pas_is_subject_current_aag[rule_format]) - apply (simp add: active_from_running)+ + apply (simp only: active_from_running)+ apply(drule uwr_PSched_cur_domain, simp add: current_aag_def) apply simp apply simp apply simp apply(rule reads_equiv_f_g_affects_equiv_uwr) - apply (simp add: invs_if_def Invs_def)+ + apply ((clarsimp simp: Invs_def dest!: invs_if_Invs; rule TrueI)+) + apply (simp add: invs_if_def Invs_def)+ apply(erule use_valid[OF _ do_user_op_if_partitionIntegrity]) apply(erule use_valid[OF _ check_active_irq_if_wp]) apply(clarsimp) apply(frule (1) ct_running_cur_thread_not_idle_thread[OF invs_valid_idle]) apply (rule guarded_pas_is_subject_current_aag[rule_format]) - apply (simp add: active_from_running)+ + apply (simp only: active_from_running)+ + apply simp apply(erule_tac s'=s'aa in use_valid[OF _ do_user_op_if_partitionIntegrity]) apply(erule_tac s'=yc in use_valid[OF _ check_active_irq_if_wp]) apply(clarsimp) @@ -2636,11 +2646,10 @@ lemma do_user_op_A_if_confidentiality: \rule revcut_rl[OF ct_running_cur_thread_not_idle_thread[OF invs_valid_idle[OF H]]]\) apply assumption apply (rule guarded_pas_is_subject_current_aag[rule_format]) - apply (simp add: active_from_running)+ + apply (simp only: active_from_running)+ apply(simp add: sys_mode_of_def) apply(simp add: user_context_of_def) done - lemma do_user_op_A_if_confidentiality': "\(XX, YY) \ uwr PSched; XX = s; YY = t; (s, t) \ uwr (part s); (s, t) \ uwr u; diff --git a/proof/infoflow/Retype_IF.thy b/proof/infoflow/Retype_IF.thy index 83a541f08..e43709a65 100644 --- a/proof/infoflow/Retype_IF.thy +++ b/proof/infoflow/Retype_IF.thy @@ -1045,6 +1045,10 @@ lemma delete_objects_pspace_no_overlap_again: apply(simp add: valid_cap_simps cap_aligned_def is_aligned_neg_mask_eq field_simps) done +lemma ex_tupleI: + "P (fst t) (snd t) \ \a b. P a b" + by blast + lemma reset_untyped_cap_reads_respects_g: "reads_equiv_valid_g_inv (affects_equiv aag l) aag (\s. cte_wp_at is_untyped_cap slot s \ invs s \ ct_active s @@ -1052,7 +1056,7 @@ lemma reset_untyped_cap_reads_respects_g: \ is_subject aag (fst slot) \ (descendants_of slot (cdt s) = {})) (reset_untyped_cap slot)" - apply (simp add: reset_untyped_cap_def) + apply (simp add: reset_untyped_cap_def cong: if_cong) apply (rule equiv_valid_guard_imp) apply (wp set_cap_reads_respects_g dmo_clearMemory_reads_respects_g | simp add: unless_def when_def split del: split_if)+ @@ -1128,12 +1132,14 @@ lemma reset_untyped_cap_reads_respects_g: apply (clarsimp simp: ptr_range_def[symmetric] global_refs_def descendants_range_def2) apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) - apply (strengthen empty_descendants_range_in) + apply (strengthen refl[where t=True] refl ex_tupleI[where t=slot] + empty_descendants_range_in + | clarsimp)+ apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD) apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in) apply clarsimp+ - apply (cases slot, fastforce) + apply fastforce done lemma equiv_valid_obtain: