From b4bd34100c8e9e24c99e017fdf0e1d38a2190712 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Wed, 11 Dec 2024 16:39:49 +1100 Subject: [PATCH] arm access: proof update for det_ext refactor Signed-off-by: Corey Lewis --- proof/access-control/ARM/ArchAccess.thy | 11 ++ proof/access-control/ARM/ArchArch_AC.thy | 13 +- proof/access-control/ARM/ArchCNode_AC.thy | 25 +-- proof/access-control/ARM/ArchIpc_AC.thy | 8 +- proof/access-control/ARM/ArchRetype_AC.thy | 29 ++- proof/access-control/ARM/ArchTcb_AC.thy | 5 +- proof/access-control/ARM/ExampleSystem.thy | 102 +++++++---- proof/access-control/Access.thy | 18 +- proof/access-control/Access_AC.thy | 25 +-- proof/access-control/CNode_AC.thy | 128 ++++++------- proof/access-control/DomainSepInv.thy | 202 ++++++--------------- proof/access-control/Finalise_AC.thy | 89 ++------- proof/access-control/Ipc_AC.thy | 53 +++--- proof/access-control/Retype_AC.thy | 121 ++++-------- proof/access-control/Syscall_AC.thy | 109 ++++++----- proof/access-control/Tcb_AC.thy | 21 +-- 16 files changed, 390 insertions(+), 569 deletions(-) diff --git a/proof/access-control/ARM/ArchAccess.thy b/proof/access-control/ARM/ArchAccess.thy index 60797287eb..8d79094627 100644 --- a/proof/access-control/ARM/ArchAccess.thy +++ b/proof/access-control/ARM/ArchAccess.thy @@ -88,6 +88,11 @@ lemmas state_vrefs_upd = revokable_update.state_vrefs machine_state_update.state_vrefs more_update.state_vrefs + scheduler_action_update.state_vrefs + domain_index_update.state_vrefs + cur_domain_update.state_vrefs + domain_time_update.state_vrefs + ready_queues_update.state_vrefs end @@ -138,6 +143,7 @@ abbreviation integrity_asids_aux :: pp_opt = pp_opt' \ (\asid'. asid' \ 0 \ asid_high_bits_of asid' = asid_high_bits_of asid \ pasASIDAbs aag asid' \ subjects)" +\ \FIXME: could we define integrity_asids to operate on arch_state only?\ definition integrity_asids :: "'a PAS \ 'a set \ obj_ref \ asid \ 'y::state_ext state \ 'z:: state_ext state \ bool" where "integrity_asids aag subjects x a s s' \ @@ -159,6 +165,11 @@ lemmas integrity_asids_updates = interrupt_update.integrity_asids_update cur_thread_update.integrity_asids_update machine_state_update.integrity_asids_update + scheduler_action_update.integrity_asids_update + domain_index_update.integrity_asids_update + cur_domain_update.integrity_asids_update + domain_time_update.integrity_asids_update + ready_queues_update.integrity_asids_update (* The kheap isn't used in ARM's integrity_asids definition, but we need the following lemmas in some generic contexts *) diff --git a/proof/access-control/ARM/ArchArch_AC.thy b/proof/access-control/ARM/ArchArch_AC.thy index 93c3edfaa9..0302e3eade 100644 --- a/proof/access-control/ARM/ArchArch_AC.thy +++ b/proof/access-control/ARM/ArchArch_AC.thy @@ -1011,21 +1011,20 @@ lemma delete_asid_respects: by (wpsimp wp: set_asid_pool_respects_clear hoare_vcg_all_lift simp: obj_at_def pas_refined_refl delete_asid_def asid_pool_integrity_def) -lemma authorised_arch_inv_sa_update: +lemma authorised_arch_inv_sa_update[simp]: "authorised_arch_inv aag i (scheduler_action_update (\_. act) s) = authorised_arch_inv aag i s" by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def split: arch_invocation.splits page_invocation.splits) +crunch set_thread_state_act + for authorised_arch_inv[wp]: "authorised_arch_inv aag i" + lemma set_thread_state_authorised_arch_inv[wp]: "set_thread_state ref ts \authorised_arch_inv aag i\" unfolding set_thread_state_def - apply (wpsimp wp: dxo_wp_weak) - apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def - split: arch_invocation.splits page_invocation.splits) - apply (wpsimp wp: set_object_wp)+ - by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def - split: arch_invocation.splits page_invocation.splits) + apply (wpsimp wp: set_object_wp) + by (clarsimp simp: authorised_arch_inv_def) end diff --git a/proof/access-control/ARM/ArchCNode_AC.thy b/proof/access-control/ARM/ArchCNode_AC.thy index d7af0cb9ec..fcdedb800e 100644 --- a/proof/access-control/ARM/ArchCNode_AC.thy +++ b/proof/access-control/ARM/ArchCNode_AC.thy @@ -114,15 +114,12 @@ lemma list_integ_lift[CNode_AC_assms]: "\list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ f \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\" - assumes ekh: "\P. f \\s. P (ekheap s)\" - assumes rq: "\P. f \\s. P (ready_queues s)\" shows "\integrity aag X st and Q\ f \\_. integrity aag X st\" apply (rule hoare_pre) apply (unfold integrity_def[abs_def] integrity_asids_def) apply (simp only: integrity_cdt_list_as_list_integ) - apply (rule hoare_lift_Pf2[where f="ekheap"]) - apply (simp add: tcb_states_of_state_def get_tcb_def) - apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+ + apply (simp add: tcb_states_of_state_def get_tcb_def) + apply (wp li[simplified tcb_states_of_state_def get_tcb_def])+ apply (simp only: integrity_cdt_list_as_list_integ) apply (simp add: tcb_states_of_state_def get_tcb_def) done @@ -374,16 +371,9 @@ lemma auth_graph_map_def2: "auth_graph_map f S = (\(x, auth, y). (f x, auth, f y)) ` S" by (auto simp add: auth_graph_map_def image_def intro: rev_bexI) -(* FIXME move to AInvs *) -lemma store_pte_ekheap[wp]: - "store_pte p pte \\s. P (ekheap s)\" - apply (simp add: store_pte_def set_pt_def) - apply (wp get_object_wp) - apply simp - done - crunch store_pte - for asid_table_inv[wp]: "\s. P (asid_table s)" + for etcbs_of[wp]: "\s. P (etcbs_of s)" + and asid_table_inv[wp]: "\s. P (asid_table s)" lemma store_pte_pas_refined[wp]: "\pas_refined aag and @@ -501,13 +491,6 @@ lemma set_asid_pool_thread_bound_ntfns[wp]: split: kernel_object.split_asm option.split) done -(* FIXME move to AInvs *) -lemma set_asid_pool_ekheap[wp]: - "set_asid_pool p pool \\s. P (ekheap s)\" - apply (simp add: set_asid_pool_def) - apply (wp get_object_wp | simp)+ - done - lemma set_asid_pool_pas_refined[wp]: "\pas_refined aag and (\s. \(x, y) \ graph_of pool. diff --git a/proof/access-control/ARM/ArchIpc_AC.thy b/proof/access-control/ARM/ArchIpc_AC.thy index b7d2687f13..cebd554a14 100644 --- a/proof/access-control/ARM/ArchIpc_AC.thy +++ b/proof/access-control/ARM/ArchIpc_AC.thy @@ -17,6 +17,7 @@ declare handle_arch_fault_reply_typ_at[Ipc_AC_assms] crunch cap_insert_ext for integrity_asids[Ipc_AC_assms, wp]: "integrity_asids aag subjects x a st" + (ignore_del: cap_insert_ext) \ \FIXME: should these ext consts still be ignored in DetSched_AI files and beyond?\ lemma arch_derive_cap_auth_derived[Ipc_AC_assms]: "\\\ arch_derive_cap acap \\rv _. rv \ NullCap \ auth_derived rv (ArchObjectCap acap)\, -" @@ -203,8 +204,6 @@ lemma list_integ_lift_in_ipc[Ipc_AC_assms]: "\list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ f \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\" - assumes ekh: "\P. \\s. P (ekheap s)\ f \\rv s. P (ekheap s)\" - assumes rq: "\P. \ \s. P (ready_queues s) \ f \ \rv s. P (ready_queues s) \" shows "\integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\ f \\_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\" @@ -212,9 +211,8 @@ lemma list_integ_lift_in_ipc[Ipc_AC_assms]: apply (simp del:split_paired_All) apply (rule hoare_pre) apply (simp only: integrity_cdt_list_as_list_integ) - apply (rule hoare_lift_Pf2[where f="ekheap"]) - apply (simp add: tcb_states_of_state_def get_tcb_def) - apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+ + apply (simp add: tcb_states_of_state_def get_tcb_def) + apply (wp li[simplified tcb_states_of_state_def get_tcb_def])+ apply (simp only: integrity_cdt_list_as_list_integ) apply (simp add: tcb_states_of_state_def get_tcb_def) done diff --git a/proof/access-control/ARM/ArchRetype_AC.thy b/proof/access-control/ARM/ArchRetype_AC.thy index 5b2f637b27..032fe2eea9 100644 --- a/proof/access-control/ARM/ArchRetype_AC.thy +++ b/proof/access-control/ARM/ArchRetype_AC.thy @@ -17,7 +17,7 @@ lemma invs_mdb_cte': context retype_region_proofs begin interpretation Arch . lemma vs_refs_no_global_pts_default[simp]: - "vs_refs_no_global_pts (default_object ty dev us) = {}" + "vs_refs_no_global_pts (default_object ty dev us d) = {}" by (simp add: default_object_def default_arch_object_def tyunt vs_refs_no_global_pts_def pde_ref2_def pte_ref_def o_def @@ -33,12 +33,25 @@ end context retype_region_proofs' begin interpretation Arch . +\ \FIXME: move to pas_refined_state_objs_to_policy_subset?\ +lemma pas_refined_subsets_tcb_domain_map_wellformed: + "\ pas_refined aag s; + state_objs_to_policy s' \ state_objs_to_policy s; + state_asids_to_policy aag s' \ state_asids_to_policy aag s; + state_irqs_to_policy aag s' \ state_irqs_to_policy aag s; + tcb_domain_map_wellformed aag s \ tcb_domain_map_wellformed aag s'; + interrupt_irq_node s' = interrupt_irq_node s \ + \ pas_refined aag s'" + by (simp add: pas_refined_def) + (blast dest: auth_graph_map_mono[where G="pasObjectAbs aag"]) + lemma pas_refined: - "\ invs s; pas_refined aag s \ \ pas_refined aag s'" - apply (erule pas_refined_state_objs_to_policy_subset) - apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable) - apply (rule subsetI, rename_tac x, case_tac x, simp) - apply (erule state_bits_to_policy.cases) + "\ invs s; pas_refined aag s; pas_cur_domain aag s; \x\ set (retype_addrs ptr ty n us). is_subject aag x \ + \ pas_refined aag s'" + apply (erule pas_refined_subsets_tcb_domain_map_wellformed) + apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable) + apply (rule subsetI, rename_tac x, case_tac x, simp) + apply (erule state_bits_to_policy.cases) apply (solves \auto intro!: sbta_caps intro: caps_retype split: cap.split\) apply (solves \auto intro!: sbta_untyped intro: caps_retype split: cap.split\) apply (blast intro: state_bits_to_policy.intros) @@ -57,7 +70,7 @@ lemma pas_refined: apply clarsimp apply (erule state_irqs_to_policy_aux.cases) apply (solves\auto intro!: sita_controlled intro: caps_retype split: cap.split\) - apply (rule domains_of_state) + apply (erule (2) tcb_domain_map_wellformed) apply simp done @@ -427,7 +440,7 @@ lemma retype_region_integrity_asids[Retype_AC_assms]: \x\up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} x a s st \ \ integrity_asids aag {pasSubject aag} x a s (st\kheap := \a. if a \ (\x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0 ..< n} - then Some (default_object typ dev o_bits) + then Some (default_object typ dev o_bits d) else kheap s a\)" by clarsimp diff --git a/proof/access-control/ARM/ArchTcb_AC.thy b/proof/access-control/ARM/ArchTcb_AC.thy index ac6be4cc0a..f2c2e957bd 100644 --- a/proof/access-control/ARM/ArchTcb_AC.thy +++ b/proof/access-control/ARM/ArchTcb_AC.thy @@ -32,14 +32,12 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]: apply (rule hoare_gen_asm)+ apply (subst invoke_tcb.simps) apply (subst option_update_thread_def) - apply (subst set_priority_extended.dxo_eq) apply (rule hoare_weaken_pre) apply (rule_tac P="case ep of Some v \ length v = word_bits | _ \ True" in hoare_gen_asm) apply (simp only: split_def) apply (((simp add: conj_comms, strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong) - | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_liftE_R hoare_vcg_conj_elimE hoare_vcg_const_imp_liftE_R hoare_vcg_conj_liftE_R | wp restart_integrity_autarch set_mcpriority_integrity_autarch @@ -79,7 +77,8 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]: | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified] emptyable_def a_type_def partial_inv_def | wpc - | strengthen invs_mdb use_no_cap_to_obj_asid_strg + | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state + invs_mdb use_no_cap_to_obj_asid_strg tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"] tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"]))+ apply (clarsimp simp: authorised_tcb_inv_def) diff --git a/proof/access-control/ARM/ExampleSystem.thy b/proof/access-control/ARM/ExampleSystem.thy index 6282d5ef13..2417840a72 100644 --- a/proof/access-control/ARM/ExampleSystem.thy +++ b/proof/access-control/ARM/ExampleSystem.thy @@ -312,6 +312,9 @@ where tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, + tcb_priority = undefined, + tcb_time_slice = undefined, + tcb_domain = 0, tcb_arch = \tcb_context = undefined\ \" @@ -333,6 +336,9 @@ where tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, + tcb_priority = undefined, + tcb_time_slice = undefined, + tcb_domain = 0, tcb_arch = \tcb_context = undefined\\" definition @@ -362,13 +368,6 @@ lemmas kh1_obj_def = definition exst1 :: "det_ext" where "exst1 \ \work_units_completed_internal = undefined, - scheduler_action_internal = undefined, - ekheap_internal = \x. None, - domain_list_internal = undefined, - domain_index_internal = undefined, - cur_domain_internal = undefined, - domain_time_internal = undefined, - ready_queues_internal = undefined, cdt_list_internal = undefined\" definition @@ -380,6 +379,12 @@ where is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, + scheduler_action = undefined, + domain_list = undefined, + domain_index = undefined, + cur_domain = undefined, + domain_time = undefined, + ready_queues = undefined, machine_state = undefined, interrupt_irq_node = (\_. 10), interrupt_states = undefined, @@ -455,9 +460,13 @@ where else if (asid_high_bits_of x = asid_high_bits_of asid1_3065) then T1 else undefined)" +definition Sys1DomainMap :: "Sys1Labels agent_domain_map" where + "Sys1DomainMap \ (\_. {}) (0 := {UT1, T1})" + definition Sys1PAS :: "Sys1Labels PAS" where "Sys1PAS \ \ pasObjectAbs = Sys1AgentMap, pasASIDAbs = Sys1ASIDMap, pasIRQAbs = (\_. IRQ1), - pasPolicy = Sys1AuthGraph, pasSubject = UT1, pasMayActivate = True, pasMayEditReadyQueues = True, pasMaySendIrqs = True, pasDomainAbs = undefined \" + pasPolicy = Sys1AuthGraph, pasSubject = UT1, pasMayActivate = True, pasMayEditReadyQueues = True, + pasMaySendIrqs = True, pasDomainAbs = Sys1DomainMap \" subsubsection \Proof of pas_refined for Sys1\ @@ -548,22 +557,28 @@ lemma thread_bound_ntfns_1: declare AllowSend_def[simp] AllowRecv_def[simp] -lemma domains_of_state_s1[simp]: - "domains_of_state s1 = {}" - apply (rule equalityI) - apply (rule subsetI) - apply clarsimp - apply (erule domains_of_state_aux.induct) - apply (simp add: s1_def exst1_def) - apply simp - done +lemma etcbs_of_s1: + "etcbs_of s1 = [3079 \ etcb_of (un_TCB obj1_3079), 3080 \ etcb_of (un_TCB obj1_3080)]" + by (fastforce simp: etcbs_of'_def s1_def kh1_def kh1_obj_def) + +lemma domains_of_state_s1: + "domains_of_state s1 = {(3079, 0), (3080, 0)}" + by (fastforce simp: etcbs_of_s1 kh1_obj_def + elim: domains_of_state_aux.cases + split: if_split_asm + intro!: domtcbs) + +lemma tcb_domain_map_wellformed_s1: + "tcb_domain_map_wellformed Sys1PAS s1" + by (clarsimp simp: tcb_domain_map_wellformed_aux_def Sys1PAS_def domains_of_state_s1 + Sys1AgentMap_simps Sys1DomainMap_def) lemma "pas_refined Sys1PAS s1" apply (clarsimp simp: pas_refined_def) apply (intro conjI) subgoal by (simp add: Sys1_wellformed) subgoal by (simp add: irq_map_wellformed_aux_def s1_def Sys1AgentMap_simps Sys1PAS_def) - subgoal by (simp add: tcb_domain_map_wellformed_aux_def) + subgoal by (simp add: tcb_domain_map_wellformed_s1) apply (clarsimp simp: auth_graph_map_def Sys1PAS_def state_objs_to_policy_def @@ -851,6 +866,9 @@ where tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, + tcb_priority = undefined, + tcb_time_slice = undefined, + tcb_domain = 0, tcb_arch = \tcb_context = undefined\\" @@ -872,6 +890,9 @@ where tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, + tcb_priority = undefined, + tcb_time_slice = undefined, + tcb_domain = 0, tcb_arch = \tcb_context = undefined\\" (* the boolean in BlockedOnReceive is True if the object can receive but not send. @@ -904,6 +925,12 @@ where is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, + scheduler_action = undefined, + domain_list = undefined, + domain_index = undefined, + cur_domain = undefined, + domain_time = undefined, + ready_queues = undefined, machine_state = undefined, interrupt_irq_node = (\_. 9001), interrupt_states = undefined, @@ -964,10 +991,14 @@ where (asid2_3063 := UT2, asid2_3065 := T2 )" +definition Sys2DomainMap :: "Sys2Labels agent_domain_map" where + "Sys2DomainMap \ (\_. {}) (0 := {UT2, T2})" + definition Sys2PAS :: "Sys2Labels PAS" where "Sys2PAS \ \ pasObjectAbs = Sys2AgentMap, pasASIDAbs = Sys2ASIDMap, pasIRQAbs = (\_. IRQ2), - pasPolicy = Sys2AuthGraph, pasSubject = UT2, pasMayActivate = True, pasMayEditReadyQueues = True, pasMaySendIrqs = True, pasDomainAbs = undefined \" + pasPolicy = Sys2AuthGraph, pasSubject = UT2, pasMayActivate = True, pasMayEditReadyQueues = True, + pasMaySendIrqs = True, pasDomainAbs = Sys2DomainMap \" @@ -1052,15 +1083,21 @@ lemma Sys2AgentMap_simps: "Sys2AgentMap 9001 = IRQ2" by (simp_all add: Sys2AgentMap_def) -lemma domains_of_state_s2[simp]: - "domains_of_state s2 = {}" - apply (rule equalityI) - apply (rule subsetI) - apply clarsimp - apply (erule domains_of_state_aux.induct) - apply (simp add: s2_def exst1_def) - apply simp - done +lemma etcbs_of_s2: + "etcbs_of s2 = [3079 \ etcb_of (un_TCB obj2_3079), 3080 \ etcb_of (un_TCB obj2_3080)]" + by (fastforce simp: etcbs_of'_def s2_def kh2_def kh2_obj_def) + +lemma domains_of_state_s2: + "domains_of_state s2 = {(3079, 0), (3080, 0)}" + by (fastforce simp: etcbs_of_s2 kh2_obj_def + elim: domains_of_state_aux.cases + split: if_split_asm + intro!: domtcbs) + +lemma tcb_domain_map_wellformed_s2: + "tcb_domain_map_wellformed Sys2PAS s2" + by (clarsimp simp: tcb_domain_map_wellformed_aux_def Sys2PAS_def domains_of_state_s2 + Sys2AgentMap_simps Sys2DomainMap_def) lemma thread_bound_ntfns_2[simp]: "thread_bound_ntfns s2 = Map.empty" @@ -1073,13 +1110,14 @@ lemma thread_bound_ntfns_2[simp]: lemma "pas_refined Sys2PAS s2" apply (clarsimp simp: pas_refined_def) apply (intro conjI) - apply (simp add: Sys2_wellformed) - apply (simp add: Sys2PAS_def s2_def Sys2AgentMap_def - irq_map_wellformed_aux_def) + apply (simp add: Sys2_wellformed) + apply (simp add: Sys2PAS_def s2_def Sys2AgentMap_def + irq_map_wellformed_aux_def) + apply (clarsimp simp: tcb_domain_map_wellformed_s2) apply (clarsimp simp: auth_graph_map_def Sys2PAS_def state_objs_to_policy_def - state_bits_to_policy_def tcb_domain_map_wellformed_aux_def)+ + state_bits_to_policy_def) apply (erule state_bits_to_policyp.cases, simp_all) apply (drule s2_caps_of_state, clarsimp) apply (elim disjE, simp_all add: cap_auth_conferred_def diff --git a/proof/access-control/Access.thy b/proof/access-control/Access.thy index 681c28b59a..0979c9d16d 100644 --- a/proof/access-control/Access.thy +++ b/proof/access-control/Access.thy @@ -246,15 +246,16 @@ unauthorised subjects (see integrity_ready_queues). \ -inductive_set domains_of_state_aux for ekheap where +\ \FIXME: should this be etcbs_of instead of kheap?\ +inductive_set domains_of_state_aux for etcbs_of where domtcbs: - "\ ekheap ptr = Some etcb; d = tcb_domain etcb \ \ (ptr, d) \ domains_of_state_aux ekheap" + "\ etcbs_of ptr = Some tcb; d = etcb_domain tcb \ \ (ptr, d) \ domains_of_state_aux etcbs_of" -abbreviation "domains_of_state s \ domains_of_state_aux (ekheap s)" +abbreviation "domains_of_state s \ domains_of_state_aux (etcbs_of s)" definition tcb_domain_map_wellformed_aux where - "tcb_domain_map_wellformed_aux aag etcbs_doms \ - \(ptr, d) \ etcbs_doms. pasObjectAbs aag ptr \ pasDomainAbs aag d" + "tcb_domain_map_wellformed_aux aag tcbs_doms \ + \(ptr, d) \ tcbs_doms. pasObjectAbs aag ptr \ pasDomainAbs aag d" abbreviation tcb_domain_map_wellformed where "tcb_domain_map_wellformed aag s \ tcb_domain_map_wellformed_aux aag (domains_of_state s)" @@ -660,7 +661,7 @@ inductive integrity_obj_alt for aag activate subjects l' ko ko' where \ integrity_obj_alt aag activate subjects l' ko ko'" -subsubsection \ekheap and ready queues\ +subsubsection \ready queues\ text\ @@ -679,10 +680,6 @@ definition integrity_ready_queues where "integrity_ready_queues aag subjects queue_labels rq rq' \ pasMayEditReadyQueues aag \ (queue_labels \ subjects = {} \ (\threads. threads @ rq = rq'))" -inductive integrity_eobj for aag subjects l' eko eko' where - tre_lrefl: "l' \ subjects \ integrity_eobj aag subjects l' eko eko'" -| tre_orefl: "eko = eko' \ integrity_eobj aag subjects l' eko eko'" - abbreviation object_integrity where "object_integrity aag \ integrity_obj (aag :: 'a PAS) (pasMayActivate aag) {pasSubject aag}" @@ -846,7 +843,6 @@ definition integrity_subjects :: "'a set \ 'a PAS \ bool \ obj_ref set \ det_ext state \ det_ext state \ bool" where "integrity_subjects subjects aag activate X s s' \ (\x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x)) - \ (\x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \ integrity_cdt_state aag subjects s s' \ integrity_cdt_list_state aag subjects s s' \ (\x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) diff --git a/proof/access-control/Access_AC.thy b/proof/access-control/Access_AC.thy index 1205f16c3e..a39f92fedb 100644 --- a/proof/access-control/Access_AC.thy +++ b/proof/access-control/Access_AC.thy @@ -228,7 +228,7 @@ lemma is_transferable_null_filter[simp]: lemma tcb_domain_map_wellformed_mono: "\ domains_of_state s' \ domains_of_state s; tcb_domain_map_wellformed pas s \ \ tcb_domain_map_wellformed pas s'" - by (auto simp: tcb_domain_map_wellformed_aux_def get_etcb_def) + by (auto simp: tcb_domain_map_wellformed_aux_def) lemma pas_refined_mem: "\ (x, auth, y) \ state_objs_to_policy s; pas_refined aag s \ @@ -460,8 +460,6 @@ lemmas integrity_obj_simps [simp] = tro_lrefl[OF singletonI] trm_orefl[OF refl] trd_orefl[OF refl] - tre_lrefl[OF singletonI] - tre_orefl[OF refl] lemma cdt_change_allowedI: "\ m \ pptr \* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr \ @@ -681,12 +679,6 @@ lemma tro_trans: apply (drule_tac x = x in spec)+ by force -lemma tre_trans: - "\ (\x. integrity_eobj aag es (pasObjectAbs aag x) (ekh x) (ekh' x)); - (\x. integrity_eobj aag es (pasObjectAbs aag x) (ekh' x) (ekh'' x)) \ - \ (\x. integrity_eobj aag es (pasObjectAbs aag x) (ekh x) (ekh'' x))" - by (fastforce elim!: integrity_eobj.cases intro: integrity_eobj.intros) - subsection \Integrity transitivity\ @@ -968,7 +960,6 @@ proof - apply (frule(3) trcdtlist_trans) apply (frule(1) trinterrupts_trans[simplified]) apply (frule(1) trasids_trans[simplified]) - apply (frule(1) tre_trans[simplified]) apply (frule(1) trrqs_trans[simplified]) by blast qed @@ -1024,15 +1015,13 @@ context Access_AC_2 begin lemma eintegrity_sa_update[simp]: "integrity aag X st (scheduler_action_update f s) = integrity aag X st s" - by (simp add: integrity_subjects_def) + by (auto simp add: integrity_subjects_def ) lemma trans_state_back[simp]: "trans_state (\_. exst s) s = s" by simp -declare wrap_ext_op_det_ext_ext_def[simp] - -crunch set_thread_state_ext +crunch set_thread_state_act for integrity[wp]: "integrity aag X st" crunch set_thread_state @@ -1271,7 +1260,7 @@ lemma as_user_thread_bound_ntfn[wp]: done lemma tcb_domain_map_wellformed_lift: - assumes 1: "\P. f \\s. P (ekheap s)\" + assumes 1: "\P. f \\s. P (etcbs_of s)\" shows "f \tcb_domain_map_wellformed aag\" by (rule 1) @@ -1533,10 +1522,6 @@ lemma integrity_mono: auto simp: indirect_send_def direct_send_def direct_call_def direct_reply_def elim: reply_cap_deletion_integrity_mono cnode_integrity_mono arch_integrity_obj_atomic_mono)[1] - apply (rule conjI) - apply clarsimp - apply (drule_tac x=x in spec)+ - apply (erule integrity_eobj.cases; auto intro: integrity_eobj.intros) apply (rule conjI) apply (intro allI) apply (drule_tac x=x in spec)+ @@ -1576,7 +1561,7 @@ lemma tcb_domain_map_wellformed_independent[intro!, simp]: "tcb_domain_map_wellformed aag (s\machine_state := machine_state s\irq_state := f (irq_state (machine_state s))\\) = tcb_domain_map_wellformed aag s" - by (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def) + by (simp add: tcb_domain_map_wellformed_aux_def) subsection\Transitivity of integrity lemmas and tactics\ diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy index b79309883c..f7ff2f1441 100644 --- a/proof/access-control/CNode_AC.thy +++ b/proof/access-control/CNode_AC.thy @@ -25,9 +25,9 @@ section\CNode-specific AC.\ (* FIXME: Move. *) -lemma tcb_domain_map_wellformed_ekheap[intro!, simp]: - "ekheap (P s) = ekheap s \ tcb_domain_map_wellformed aag (P s) = tcb_domain_map_wellformed aag s" - by (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def) +lemma tcb_domain_map_wellformed_etcbs_of[intro!, simp]: + "etcbs_of (P s) = etcbs_of s \ tcb_domain_map_wellformed aag (P s) = tcb_domain_map_wellformed aag s" + by (simp add: tcb_domain_map_wellformed_aux_def) (* FIXME: for some reason crunch does not discover the right precondition *) lemma set_cap_integrity_autarch: @@ -39,10 +39,6 @@ lemma integrity_cdt_list_as_list_integ: list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st s" by (fastforce elim: integrity_cdt_listE list_integE intro: list_integI integrity_cdt_list_intros) -crunch cap_swap_ext,cap_move_ext,empty_slot_ext - for ekheap[wp]: "\s. P (ekheap s)" - and ready_queues[wp]: "\s. P (ready_queues s)" - crunch set_untyped_cap_as_full for integrity_autarch: "integrity aag X st" @@ -78,19 +74,19 @@ locale CNode_AC_1 = and set_cap_state_vrefs: "\P. \pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ set_cap cap slot - \\_ s :: det_ext state. P (state_vrefs s)\" + \\_ s :: det_state. P (state_vrefs s)\" and set_cdt_state_vrefs[wp]: - "\P. set_cdt t \\s :: det_ext state. P (state_vrefs s)\" + "\P. set_cdt t \\s :: det_state. P (state_vrefs s)\" and set_cdt_state_asids_to_policy[wp]: - "\P. set_cdt t \\s. P (state_asids_to_policy aag s)\" + "\P. set_cdt t \\s::det_state. P (state_asids_to_policy aag s)\" and arch_post_cap_deletion_integrity[wp]: "arch_post_cap_deletion acap \integrity aag X st\" and arch_post_cap_deletion_cur_domain[wp]: - "\P. arch_post_cap_deletion acap \\s. P (cur_domain s)\" + "\P. arch_post_cap_deletion acap \\s::det_state. P (cur_domain s)\" and arch_finalise_cap_cur_domain: - "\P. arch_finalise_cap acap final \\s. P (cur_domain s)\" + "\P. arch_finalise_cap acap final \\s::det_state. P (cur_domain s)\" and prepare_thread_delete_cur_domain: - "\P. prepare_thread_delete p \\s. P (cur_domain s)\" + "\P. prepare_thread_delete p \\s::det_state. P (cur_domain s)\" and maskInterrupt_underlying_memory[wp]: "\P. maskInterrupt m irq \\s. P (underlying_memory s)\" and maskInterrupt_device_state[wp]: @@ -99,29 +95,25 @@ locale CNode_AC_1 = "\Q a b c d e. \ \list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ cap_insert_ext a b c d e - \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\; - \P. cap_insert_ext a b c d e \\s. P (ekheap s)\; \P. cap_insert_ext a b c d e \\s. P (ready_queues s)\ \ + \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\ \ \ \integrity aag X st and Q\ cap_insert_ext a b c d e \\_. integrity aag X st\" and cap_move_ext_list_integ_lift: "\Q a b c d. \ \list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ cap_move_ext a b c d - \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\; - \P. cap_move_ext a b c d \\s. P (ekheap s)\; \P. cap_move_ext a b c d \\s. P (ready_queues s)\ \ + \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\ \ \ \integrity aag X st and Q\ cap_move_ext a b c d \\_. integrity aag X st\" and cap_swap_ext_extended_list_integ_lift: "\Q a b c d. \ \list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ cap_swap_ext a b c d - \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\; - \P. cap_swap_ext a b c d \\s. P (ekheap s)\; \P. cap_swap_ext a b c d \\s. P (ready_queues s)\ \ + \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\ \ \ \integrity aag X st and Q\ cap_swap_ext a b c d \\_. integrity aag X st\" and empty_slot_extended_list_integ_lift: "\Q a b. \ \list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ empty_slot_ext a b - \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\; - \P. empty_slot_ext a b \\s. P (ekheap s)\; \P. empty_slot_ext a b \\s. P (ready_queues s)\ \ + \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\ \ \ \integrity aag X st and Q\ empty_slot_ext a b \\_. integrity aag X st\" begin @@ -915,17 +907,12 @@ lemma set_cdt_pas_refined: split: if_split_asm | blast)+ done -lemma pas_refined_original_cap_update[simp]: - "pas_refined aag (is_original_cap_update f s) = pas_refined aag s" - by (simp add: pas_refined_def state_objs_to_policy_def) - -lemma pas_refined_machine_state_update[simp]: - "pas_refined aag (machine_state_update f s) = pas_refined aag s" - by (simp add: pas_refined_def state_objs_to_policy_def state_refs_of_def) - -lemma pas_refined_interrupt_states_update[simp]: - "pas_refined aag (interrupt_states_update f s) = pas_refined aag s" - by (simp add: pas_refined_def state_objs_to_policy_def state_refs_of_def) +lemma pas_refined_updates[simp]: + "\f. pas_refined aag (is_original_cap_update f s) = pas_refined aag s" + "\f. pas_refined aag (machine_state_update f s) = pas_refined aag s" + "\f. pas_refined aag (interrupt_states_update f s) = pas_refined aag s" + "\f. pas_refined aag (ready_queues_update f s) = pas_refined aag s" + by (simp add: pas_refined_def state_objs_to_policy_def)+ crunch deleted_irq_handler for pas_refined[wp]: "pas_refined aag" @@ -947,10 +934,14 @@ lemma update_cdt_pas_refined: apply simp done +\ \FIXME: move\ lemma state_objs_to_policy_more_update[simp]: - "state_objs_to_policy (trans_state f s) = - state_objs_to_policy s" - by (simp add: state_objs_to_policy_def) + "\f. state_objs_to_policy (trans_state f s) = state_objs_to_policy s" + "\f. state_objs_to_policy (scheduler_action_update f s) = state_objs_to_policy s" + "\f. state_objs_to_policy (domain_index_update f s) = state_objs_to_policy s" + "\f. state_objs_to_policy (cur_domain_update f s) = state_objs_to_policy s" + "\f. state_objs_to_policy (domain_time_update f s) = state_objs_to_policy s" + by (simp add: state_objs_to_policy_def)+ end @@ -1224,11 +1215,16 @@ lemma mapM_mapM_x_valid: "\P\ mapM_x f xs \\rv. Q\ = \P\ mapM f xs \\rv. Q\" by (simp add: mapM_x_mapM liftM_def[symmetric] hoare_liftM_subst) +\ \FIXME: move to ainvs\ +lemma set_thread_state_act_scheduler_action_lift: + "\\f s. P (scheduler_action_update f s) = P s\ \ set_thread_state_act t \P\" + apply (simp add: set_thread_state_act_def set_scheduler_action_def) + by (wpsimp wp: gts_wp) lemma sts_thread_bound_ntfns[wp]: "set_thread_state t st \\s. P (thread_bound_ntfns s)\" apply (simp add: set_thread_state_def) - apply (wpsimp wp: set_object_wp dxo_wp_weak) + apply (wpsimp wp: set_object_wp set_thread_state_act_scheduler_action_lift) apply (clarsimp simp: thread_bound_ntfns_def get_tcb_def split: if_split option.splits kernel_object.splits elim!: rsubst[where P=P, OF _ ext]) @@ -1239,7 +1235,7 @@ lemma sts_thread_st_auth[wp]: set_thread_state t st \\_ s. P (thread_st_auth s)\" apply (simp add: set_thread_state_def) - apply (wpsimp wp: set_object_wp dxo_wp_weak) + apply (wpsimp wp: set_object_wp set_thread_state_act_scheduler_action_lift) apply (clarsimp simp: get_tcb_def thread_st_auth_def tcb_states_of_state_def elim!: rsubst[where P=P, OF _ ext]) done @@ -1249,18 +1245,11 @@ lemma sbn_thread_bound_ntfns[wp]: set_bound_notification t ntfn \\_ s. P (thread_bound_ntfns s)\" apply (simp add: set_bound_notification_def) - apply (wpsimp wp: set_object_wp dxo_wp_weak) + apply (wpsimp wp: set_object_wp) apply (clarsimp simp: get_tcb_def thread_bound_ntfns_def elim!: rsubst[where P=P, OF _ ext]) done -(* FIXME move to AInvs *) -lemma set_thread_state_ekheap[wp]: - "set_thread_state t st \\s. P (ekheap s)\" - apply (simp add: set_thread_state_def) - apply (wpsimp wp: set_scheduler_action_wp simp: set_thread_state_ext_def) - done - lemma set_simple_ko_tcb_states_of_state[wp]: "set_simple_ko f ptr val \\s. P (tcb_states_of_state s)\" apply (simp add: set_simple_ko_def set_object_def) @@ -1294,13 +1283,6 @@ lemma set_simple_ko_thread_bound_ntfns[wp]: split: kernel_object.split_asm if_splits) done -(* FIXME move to AInvs *) -lemma set_simple_ko_ekheap[wp]: - "set_simple_ko f ptr ep \\s. P (ekheap s)\" - apply (simp add: set_simple_ko_def) - apply (wpsimp wp: get_object_wp) - done - context CNode_AC_3 begin @@ -1308,8 +1290,8 @@ lemma sts_st_vrefs[wp]: "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ set_thread_state t st \\_ s :: det_ext state. P (state_vrefs s)\" - apply (simp add: set_thread_state_def del: set_thread_state_ext_extended.dxo_eq) - apply (wpsimp wp: set_object_wp dxo_wp_weak) + apply (simp add: set_thread_state_def ) + apply (wpsimp wp: set_object_wp set_thread_state_act_scheduler_action_lift) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs elim!: rsubst[where P=P, OF _ ext] dest!: get_tcb_SomeD) @@ -1383,19 +1365,39 @@ lemma thread_set_thread_bound_ntfns_trivT: context CNode_AC_3 begin +\ \FIXME: move\ +\ \FIXME: horrible proof, domains_of_state_aux could maybe be (etcbs_of s ||> etcb_domain) directly\ +lemma tcb_domain_map_wellformed_lift_strong: + assumes 1: "\P. f \\s. P (etcbs_of s ||> etcb_domain)\" + shows "f \tcb_domain_map_wellformed aag\" + apply (clarsimp simp: valid_def elim!: tcb_domain_map_wellformed_mono[rotated] domains_of_state_aux.cases) + apply (subgoal_tac "(etcbs_of s ||> etcb_domain) ptr = Some (etcb_domain tcb)") + apply (auto simp: in_opt_map_Some_eq intro!: domtcbs)[1] + apply (rule ccontr) + apply (frule (1) use_valid[OF _ 1], fastforce simp: in_opt_map_Some_eq) + done + +lemma thread_set_edomains: + "\\x. tcb_domain (f x) = tcb_domain x\ \ + thread_set f tptr \\s. P (etcbs_of s ||> etcb_domain)\" + unfolding thread_set_def + apply (wpsimp wp: set_object_wp get_object_wp) + by (auto elim!: rsubst[where P=P] dest!: get_tcb_SomeD simp: etcbs_of'_def opt_map_def) + lemma thread_set_pas_refined_triv: assumes cps: "\tcb. \(getF, v)\ran tcb_cap_cases. getF (f tcb) = getF tcb" and st: "\tcb. tcb_state (f tcb) = tcb_state tcb" and ntfn: "\tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb" + and dom: "\tcb. tcb_domain (f tcb) = tcb_domain tcb" shows "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ thread_set f t \\_. pas_refined aag\" - by (wpsimp wp: tcb_domain_map_wellformed_lift thread_set_state_vrefs + by (wpsimp wp: tcb_domain_map_wellformed_lift_strong thread_set_state_vrefs thread_set_edomains[OF dom] simp: pas_refined_def state_objs_to_policy_def | wps thread_set_caps_of_state_trivial[OF cps] thread_set_thread_st_auth_trivT[OF st] thread_set_thread_bound_ntfns_trivT[OF ntfn])+ -lemmas thread_set_pas_refined = thread_set_pas_refined_triv[OF ball_tcb_cap_casesI] +lemmas thread_set_pas_refined = thread_set_pas_refined_triv[OF ball_tcb_cap_casesI, simplified] end @@ -1521,7 +1523,7 @@ crunch deleted_irq_handler for cur_domain[wp]: "\s. P (cur_domain s)" lemma preemption_point_cur_domain[wp]: - "preemption_point \\s. P (cur_domain s)\" + "preemption_point \\s::det_state. P (cur_domain s)\" by (wp preemption_point_inv', simp+) lemma cnode_inv_auth_derivations_If_Insert_Move: @@ -1533,26 +1535,26 @@ lemma cnode_inv_auth_derivations_If_Insert_Move: context CNode_AC_3 begin lemma post_cap_deletion_cur_domain[wp]: - "post_cap_deletion c \\s. P (cur_domain s)\" + "post_cap_deletion c \\s::det_state. P (cur_domain s)\" by (wpsimp simp: post_cap_deletion_def) crunch cap_swap_for_delete, empty_slot - for cur_domain[wp]: "\s. P (cur_domain s)" + for cur_domain[wp]: "\s::det_state. P (cur_domain s)" (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) crunch finalise_cap - for cur_domain[wp]: "\s. P (cur_domain s)" + for cur_domain[wp]: "\s::det_state. P (cur_domain s)" (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) lemma rec_del_cur_domain[wp]: - "rec_del call \\s. P (cur_domain s)\" + "rec_del call \\s::det_state. P (cur_domain s)\" by (rule rec_del_preservation; wp) crunch cap_delete - for cur_domain[wp]: "\s. P (cur_domain s)" + for cur_domain[wp]: "\s::det_state. P (cur_domain s)" lemma cap_revoke_cur_domain[wp]: - "cap_revoke slot \\s. P (cur_domain s)\" + "cap_revoke slot \\s::det_state. P (cur_domain s)\" by (rule cap_revoke_preservation2; wp) end diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy index 7d2c2c6421..76b802ff8e 100644 --- a/proof/access-control/DomainSepInv.thy +++ b/proof/access-control/DomainSepInv.thy @@ -106,13 +106,18 @@ lemma domain_sep_inv_triv: apply (rule cte_pres, rule irq_pres) done -lemma domain_sep_inv_arch_state_update[simp]: - "domain_sep_inv irqs st (s\arch_state := blah\) = domain_sep_inv irqs st s" - by (simp add: domain_sep_inv_def) - -lemma domain_sep_inv_machine_state_update[simp]: - "domain_sep_inv irqs st (s\machine_state := X\) = domain_sep_inv irqs st s" - by (simp add: domain_sep_inv_def) +lemma domain_sep_inv_updates[simp]: + "\f. domain_sep_inv irqs st (trans_state f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (arch_state_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (machine_state_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (is_original_cap_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (cdt_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (scheduler_action_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (domain_index_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (cur_domain_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (domain_time_update f s) = domain_sep_inv irqs st s" + "\f. domain_sep_inv irqs st (ready_queues_update f s) = domain_sep_inv irqs st s" + by (simp add: domain_sep_inv_def)+ lemma detype_interrupts_states[simp]: "interrupt_states (detype S s) = interrupt_states s" @@ -254,18 +259,6 @@ lemma cte_wp_at_is_derived_domain_sep_inv_cap: dest: cte_wp_at_norm DomainCap_is_derived is_derived_IRQHandlerCap) done -lemma domain_sep_inv_exst_update[simp]: - "domain_sep_inv irqs st (trans_state f s) = domain_sep_inv irqs st s" - by (simp add: domain_sep_inv_def) - -lemma domain_sep_inv_is_original_cap_update[simp]: - "domain_sep_inv irqs st (s\is_original_cap := X\) = domain_sep_inv irqs st s" - by (simp add: domain_sep_inv_def) - -lemma domain_sep_inv_cdt_update[simp]: - "domain_sep_inv irqs st (s\cdt := X\) = domain_sep_inv irqs st s" - by (simp add: domain_sep_inv_def) - crunch update_cdt for domain_sep_inv[wp]: "domain_sep_inv irqs st" @@ -358,10 +351,13 @@ crunch set_simple_ko for domain_sep_inv[wp]: "domain_sep_inv irqs st" (wp: domain_sep_inv_triv) +crunch set_thread_state_act + for neg_cte_wp_at[wp]: "\s. \ cte_wp_at P c s" + lemma set_thread_state_neg_cte_wp_at[wp]: "set_thread_state a b \\s. \ cte_wp_at P slot s\" apply (simp add: set_thread_state_def) - apply (wp set_object_wp get_object_wp dxo_wp_weak| simp)+ + apply (wp set_object_wp get_object_wp | simp)+ apply (case_tac "a = fst slot") apply (clarsimp split: kernel_object.splits) apply (erule notE) @@ -396,26 +392,27 @@ crunch set_thread_state, set_bound_notification, get_bound_notification for domain_sep_inv[wp]: "domain_sep_inv irqs st" (wp: domain_sep_inv_triv) -lemma thread_set_tcb_fault_update_neg_cte_wp_at[wp]: - "thread_set (tcb_fault_update blah) t \\s. \ cte_wp_at P slot s\" - apply (simp add: thread_set_def) - apply (wp set_object_wp get_object_wp | simp)+ - apply (case_tac "t = fst slot") - apply (clarsimp split: kernel_object.splits) - apply (erule notE) - apply (erule cte_wp_atE) - apply (fastforce simp: obj_at_def) - apply (drule get_tcb_SomeD) - apply (rule cte_wp_at_tcbI) - apply simp - apply assumption - apply (fastforce simp: tcb_cap_cases_def split: if_splits) - apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) - done - -lemma thread_set_tcb_fault_update_domain_sep_inv[wp]: - "thread_set (tcb_fault_update blah) t \domain_sep_inv irqs st\" - by (wp domain_sep_inv_triv) +lemma thread_set_domain_sep_inv_triv: + "\\tcb. \(getF, v) \ ran tcb_cap_cases. getF (f tcb) = getF tcb\ + \ thread_set f t \domain_sep_inv irqs st\" + by (wpsimp wp: domain_sep_inv_triv thread_set_cte_wp_at_trivial simp: ran_tcb_cap_cases) + +lemmas thread_set_tcb_fault_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_fault_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_ipc_buffer_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_ipc_buffer_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_fault_handler_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_fault_handler_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_mcpriority_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_mcpriority_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_priority_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_priority_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_time_slice_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_time_slice_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_domain_update_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_domain_update f" for f, simplified ran_tcb_cap_cases, simplified] +lemmas thread_set_tcb_registers_caps_merge_default_tcb_domain_sep_inv[wp] + = thread_set_domain_sep_inv_triv[where f="tcb_registers_caps_merge tcb" for tcb, simplified ran_tcb_cap_cases tcb_registers_caps_merge_def, simplified] crunch as_user for domain_sep_inv[wp]: "domain_sep_inv irqs st" @@ -446,8 +443,8 @@ lemma reply_cancel_ipc_domain_sep_inv[wp]: \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" apply (simp add: reply_cancel_ipc_def) apply wp - apply (rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv]) - apply auto + apply (rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv]) + apply auto done crunch finalise_cap @@ -589,31 +586,13 @@ lemma cte_wp_at_weak_derived_ReplyCap: apply auto done -lemma thread_set_tcb_registers_caps_merge_default_tcb_neg_cte_wp_at[wp]: - "thread_set (tcb_registers_caps_merge default_tcb) word \\s. \ cte_wp_at P slot s\" - unfolding thread_set_def - apply (wp set_object_wp | simp)+ - apply (case_tac "word = fst slot") - apply (clarsimp split: kernel_object.splits) - apply (erule notE) - apply (erule cte_wp_atE) - apply (fastforce simp: obj_at_def) - apply (drule get_tcb_SomeD) - apply (rule cte_wp_at_tcbI) - apply simp - apply assumption - apply (clarsimp simp: tcb_cap_cases_def tcb_registers_caps_merge_def split: if_splits) - apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) - done - -lemma thread_set_tcb_registers_caps_merge_default_tcb_domain_sep_inv[wp]: - "thread_set (tcb_registers_caps_merge default_tcb) word \domain_sep_inv irqs st\" - by (wp domain_sep_inv_triv) +crunch possible_switch_to + for domain_sep_inv[wp]: "domain_sep_inv irqs st" lemma cancel_badged_sends_domain_sep_inv[wp]: "cancel_badged_sends epptr badge \domain_sep_inv irqs st\" apply (simp add: cancel_badged_sends_def) - apply (wpsimp wp: dxo_wp_weak mapM_wp | simp add: filterM_mapM | wp (once) hoare_drop_imps)+ + apply (wpsimp wp: mapM_wp | simp add: filterM_mapM | wp (once) hoare_drop_imps)+ done lemma create_cap_domain_sep_inv[wp]: @@ -934,7 +913,7 @@ lemma send_fault_ipc_domain_sep_inv: crunch do_reply_transfer, handle_fault, reply_from_kernel, restart for domain_sep_inv[wp]: "\s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)" - (wp: handle_arch_fault_reply_domain_sep_inv dxo_wp_weak crunch_wps ignore: thread_set) + (wp: crunch_wps handle_arch_fault_reply_domain_sep_inv ignore: thread_set) end @@ -942,69 +921,6 @@ crunch setup_reply_master for domain_sep_inv[wp]: "domain_sep_inv irqs st" (wp: crunch_wps simp: crunch_simps) -lemma thread_set_tcb_ipc_buffer_update_neg_cte_wp_at[wp]: - "thread_set (tcb_ipc_buffer_update f) t \\s. \ cte_wp_at P slot s\" - unfolding thread_set_def - apply (wp set_object_wp | simp)+ - apply (case_tac "t = fst slot") - apply (clarsimp split: kernel_object.splits) - apply (erule notE) - apply (erule cte_wp_atE) - apply (fastforce simp: obj_at_def) - apply (drule get_tcb_SomeD) - apply (rule cte_wp_at_tcbI) - apply simp - apply assumption - apply (fastforce simp: tcb_cap_cases_def split: if_splits) - apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) - done - -lemma thread_set_tcb_ipc_buffer_update_domain_sep_inv[wp]: - "thread_set (tcb_ipc_buffer_update f) t \domain_sep_inv irqs st\" - by (rule domain_sep_inv_triv; wp) - -lemma thread_set_tcb_fault_handler_update_neg_cte_wp_at[wp]: - "thread_set (tcb_fault_handler_update f) t \\s. \ cte_wp_at P slot s\" - unfolding thread_set_def - apply (wp set_object_wp | simp)+ - apply (case_tac "t = fst slot") - apply (clarsimp split: kernel_object.splits) - apply (erule notE) - apply (erule cte_wp_atE) - apply (fastforce simp: obj_at_def) - apply (drule get_tcb_SomeD) - apply (rule cte_wp_at_tcbI) - apply simp - apply assumption - apply (fastforce simp: tcb_cap_cases_def split: if_splits) - apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) - done - -lemma thread_set_tcb_fault_handler_update_domain_sep_inv[wp]: - "thread_set (tcb_fault_handler_update f) t \domain_sep_inv irqs st\" - by (rule domain_sep_inv_triv; wp) - -lemma thread_set_tcb_tcb_mcpriority_update_neg_cte_wp_at[wp]: - "thread_set (tcb_mcpriority_update f) t \\s. \ cte_wp_at P slot s\" - unfolding thread_set_def - apply (wp set_object_wp | simp)+ - apply (case_tac "t = fst slot") - apply (clarsimp split: kernel_object.splits) - apply (erule notE) - apply (erule cte_wp_atE) - apply (fastforce simp: obj_at_def) - apply (drule get_tcb_SomeD) - apply (rule cte_wp_at_tcbI) - apply simp - apply assumption - apply (fastforce simp: tcb_cap_cases_def split: if_splits) - apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) - done - -lemma thread_set_tcb_tcp_mcpriority_update_domain_sep_inv[wp]: - "thread_set (tcb_mcpriority_update f) t \domain_sep_inv irqs st\" - by (rule domain_sep_inv_triv; wp) - lemma same_object_as_domain_sep_inv_cap: "\ same_object_as a cap; domain_sep_inv_cap irqs cap \ \ domain_sep_inv_cap irqs a" @@ -1021,18 +937,9 @@ lemma checked_cap_insert_domain_sep_inv: apply (erule (1) same_object_as_domain_sep_inv_cap) done -crunch bind_notification,reschedule_required +crunch bind_notification, set_mcpriority, set_priority, invoke_domain for domain_sep_inv[wp]: "domain_sep_inv irqs st" - -lemma set_mcpriority_domain_sep_inv[wp]: - "set_mcpriority tcb_ref mcp \domain_sep_inv irqs st\" - unfolding set_mcpriority_def by wp - -lemma invoke_domain_domain_set_inv: - "invoke_domain word1 word2 \domain_sep_inv irqs st\" - apply (simp add: invoke_domain_def) - apply (wp dxo_wp_weak | simp)+ - done + (ignore: thread_set) context DomainSepInv_2 begin @@ -1053,11 +960,10 @@ lemma invoke_tcb_domain_sep_inv: apply (simp add: split_def cong: option.case_cong) apply (wp checked_cap_insert_domain_sep_inv hoare_vcg_all_liftE_R hoare_vcg_all_lift hoare_vcg_const_imp_liftE_R cap_delete_domain_sep_inv cap_delete_deletes - dxo_wp_weak cap_delete_valid_cap cap_delete_cte_at hoare_weak_lift_imp + cap_delete_valid_cap cap_delete_cte_at hoare_weak_lift_imp | wpc | strengthen | simp add: option_update_thread_def emptyable_def tcb_cap_cases_def - tcb_cap_valid_def tcb_at_st_tcb_at - del: set_priority_extended.dxo_eq)+ + tcb_cap_valid_def tcb_at_st_tcb_at)+ done lemma perform_invocation_domain_sep_inv': @@ -1069,7 +975,6 @@ lemma perform_invocation_domain_sep_inv': apply (wp send_ipc_domain_sep_inv invoke_tcb_domain_sep_inv invoke_cnode_domain_sep_inv invoke_control_domain_sep_inv invoke_irq_handler_domain_sep_inv arch_perform_invocation_domain_sep_inv - invoke_domain_domain_set_inv | simp add: split_def | blast)+ done @@ -1173,9 +1078,9 @@ lemma handle_recv_domain_sep_inv: apply (wp | simp add: invs_valid_objs invs_mdb invs_sym_refs tcb_at_invs)+ done -crunch handle_interrupt, activate_thread, choose_thread +crunch handle_interrupt, activate_thread, choose_thread, handle_yield for domain_sep_inv[wp]: "\s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)" - (wp: dxo_wp_weak crunch_wps) + (wp: crunch_wps ignore: thread_set) lemma handle_event_domain_sep_inv: "\domain_sep_inv irqs st and invs and (\s. ev \ Interrupt \ ct_active s)\ @@ -1184,7 +1089,7 @@ lemma handle_event_domain_sep_inv: apply (case_tac ev, simp_all) apply (rule hoare_pre) apply (wpsimp wp: handle_send_domain_sep_inv handle_call_domain_sep_inv - handle_recv_domain_sep_inv handle_reply_domain_sep_inv hy_inv + handle_recv_domain_sep_inv handle_reply_domain_sep_inv | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def)+ apply (rule_tac E'="\rv s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state) \ invs s \ valid_fault rv" @@ -1193,11 +1098,14 @@ lemma handle_event_domain_sep_inv: apply (wp | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def | auto)+ done +crunch next_domain + for domain_sep_inv[wp]: "domain_sep_inv irqs st" + (simp: crunch_simps) + lemma schedule_domain_sep_inv: "(schedule :: (unit,det_ext) s_monad) \domain_sep_inv irqs (st :: 'state_ext state)\" - apply (simp add: schedule_def allActiveTCBs_def) + apply (simp add: schedule_def) apply (wp add: guarded_switch_to_lift hoare_drop_imps - del: ethread_get_wp | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric] schedule_choose_new_thread_def)+ done diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy index 36f064cfa3..87a56d12de 100644 --- a/proof/access-control/Finalise_AC.thy +++ b/proof/access-control/Finalise_AC.thy @@ -72,12 +72,12 @@ begin lemma tcb_sched_action_dequeue_integrity': "\integrity aag X st and pas_refined aag and - (\s. pasSubject aag \ pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\ + (\s. pasSubject aag \ pasDomainAbs aag (etcb_domain (the (etcbs_of s thread))))\ tcb_sched_action tcb_sched_dequeue thread \\_. integrity aag X st\" apply (wpsimp simp: tcb_sched_action_def) apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def - tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def + tcb_domain_map_wellformed_aux_def etcbs_of'_def obj_at_def split: option.splits) done @@ -88,10 +88,10 @@ lemma tcb_sched_action_dequeue_integrity[wp]: apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def - tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def + tcb_domain_map_wellformed_aux_def split: option.splits) - apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE) - apply (auto intro: domtcbs) + apply (erule_tac x="(thread, etcb_domain (the (etcbs_of s thread)))" in ballE) + apply (auto simp: etcbs_of'_def obj_at_def intro: domtcbs) done lemma tcb_sched_action_enqueue_integrity[wp]: @@ -99,8 +99,8 @@ lemma tcb_sched_action_enqueue_integrity[wp]: apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def - tcb_domain_map_wellformed_aux_def tcb_at_def get_etcb_def - tcb_sched_enqueue_def etcb_at_def + tcb_domain_map_wellformed_aux_def tcb_at_def + tcb_sched_enqueue_def split: option.splits) apply (metis append.simps(2)) done @@ -108,12 +108,12 @@ lemma tcb_sched_action_enqueue_integrity[wp]: text \See comment for @{thm tcb_sched_action_dequeue_integrity'}\ lemma tcb_sched_action_append_integrity': "\integrity aag X st and - (\s. pasSubject aag \ pasDomainAbs aag (tcb_domain (the (ekheap s thread))))\ + (\s. pasSubject aag \ pasDomainAbs aag (etcb_domain (the (etcbs_of s thread))))\ tcb_sched_action tcb_sched_append thread \\_. integrity aag X st\" apply (simp add: tcb_sched_action_def) apply wp - apply (clarsimp simp: integrity_def integrity_ready_queues_def etcb_at_def + apply (clarsimp simp: integrity_def integrity_ready_queues_def etcbs_of'_def obj_at_def split: option.splits) done @@ -124,10 +124,10 @@ lemma tcb_sched_action_append_integrity[wp]: apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def - tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def + tcb_domain_map_wellformed_aux_def split: option.splits) - apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE) - apply (auto intro: domtcbs) + apply (erule_tac x="(thread, etcb_domain (the (etcbs_of s thread)))" in ballE) + apply (auto simp: etcbs_of'_def obj_at_def intro: domtcbs) done lemma tcb_sched_action_append_integrity_pasMayEditReadyQueues: @@ -212,11 +212,10 @@ crunch reschedule_required for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag" (* FIXME move to AInvs *) -lemma tcb_sched_action_ekheap[wp]: - "tcb_sched_action p1 p2 \\s. P (ekheap s)\" +lemma tcb_sched_action_etcbs_of[wp]: + "tcb_sched_action p1 p2 \\s. P (etcbs_of s)\" apply (simp add: tcb_sched_action_def) - apply wp - apply (simp add: etcb_at_def) + apply wpsimp done (* FIXME move to CNode *) @@ -224,12 +223,6 @@ lemma scheduler_action_update_pas_refined[simp]: "pas_refined aag (scheduler_action_update (\_. param_a) s) = pas_refined aag s" by (simp add: pas_refined_def) -lemma set_bound_notification_ekheap[wp]: - "set_bound_notification t st \\s. P (ekheap s)\" - apply (simp add: set_bound_notification_def) - apply (wp set_scheduler_action_wp | simp)+ - done - lemma sbn_thread_st_auth[wp]: "set_bound_notification t ntfn \\s. P (thread_st_auth s)\" apply (simp add: set_bound_notification_def) @@ -278,6 +271,9 @@ lemma unbind_maybe_notification_pas_refined[wp]: apply (wp set_simple_ko_pas_refined hoare_drop_imps | wpc | simp)+ done +crunch possible_switch_to + for pas_refined[wp]: "pas_refined aag" + lemma cancel_all_ipc_pas_refined[wp]: "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ cancel_all_ipc epptr @@ -987,15 +983,6 @@ lemmas dmo_valid_cap[wp] = valid_cap_typ[OF do_machine_op_obj_at] context Finalise_AC_1 begin -lemma set_eobject_integrity_autarch: - "\integrity aag X st and K (is_subject aag ptr)\ - set_eobject ptr obj - \\_. integrity aag X st\" - apply (simp add: set_eobject_def) - apply wp - apply (simp add: integrity_subjects_def) - done - lemma cancel_badged_sends_pas_refined[wp]: "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ cancel_badged_sends epptr badge @@ -1003,46 +990,6 @@ lemma cancel_badged_sends_pas_refined[wp]: unfolding cancel_badged_sends_def by (wpsimp simp: filterM_mapM wp: mapM_wp_inv set_thread_state_pas_refined get_simple_ko_wp) -end - - -lemma rsubst': - "\ P s s'; s=t; s'=t' \ \ P t t'" - by auto - -lemma thread_set_pas_refined_triv_idleT: - assumes cps: "\tcb. \(getF, v)\ran tcb_cap_cases. getF (f tcb) = getF tcb" - and st: "\tcb. P (tcb_state tcb) \ tcb_state (f tcb) = tcb_state tcb" - and ba: "\tcb. Q (tcb_bound_notification tcb) - \ tcb_bound_notification (f tcb) = tcb_bound_notification tcb" - shows "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and idle_tcb_at (\(st, ntfn, arch). P st \ Q ntfn \ R arch) t\ - thread_set f t - \\_. pas_refined aag\" - apply (simp add: pas_refined_def state_objs_to_policy_def) - apply (rule hoare_pre) - apply (wps thread_set_caps_of_state_trivial[OF cps]) - apply (simp add: thread_set_def) - apply (wpsimp wp: set_object_wp) - apply (clarsimp simp: pred_tcb_def2 fun_upd_def[symmetric] - del: subsetI) - apply (subst state_vrefs_tcb_upd, fastforce+) - apply (clarsimp simp: tcb_at_def) - apply (subst state_vrefs_tcb_upd, fastforce+) - apply (clarsimp simp: tcb_at_def) - apply (rule conjI) - apply (erule_tac P="\ ts ba. auth_graph_map a (state_bits_to_policy cps ts ba cd vr) \ ag" - for a cps cd vr ag in rsubst') - apply (drule get_tcb_SomeD) - apply (rule ext, clarsimp simp add: thread_st_auth_def get_tcb_def st tcb_states_of_state_def) - apply (drule get_tcb_SomeD) - apply (rule ext, clarsimp simp: thread_bound_ntfns_def get_tcb_def ba) - apply (clarsimp) - done - - -context Finalise_AC_1 begin - lemma cap_delete_respects: "\integrity aag X st and cdt_change_allowed' aag slot and pas_refined aag and einvs and simple_sched_action and emptyable slot\ diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy index eb7a8cc056..cdf5e8bd38 100644 --- a/proof/access-control/Ipc_AC.thy +++ b/proof/access-control/Ipc_AC.thy @@ -294,13 +294,13 @@ lemma set_scheduler_action_integrity_once_ts_upd: apply (simp add: get_tcb_def) done -crunch set_thread_state_ext +crunch set_thread_state_act for integrity_once_ts_upd: "integrity_once_ts_upd t ts aag X st" lemma set_thread_state_integrity_once_ts_upd: "set_thread_state t ts' \integrity_once_ts_upd t ts aag X st\" apply (simp add: set_thread_state_def) - apply (wpsimp wp: set_object_wp set_thread_state_ext_integrity_once_ts_upd) + apply (wpsimp wp: set_object_wp set_thread_state_act_integrity_once_ts_upd) apply (clarsimp simp: fun_upd_def dest!: get_tcb_SomeD) apply (simp add: get_tcb_def cong: if_cong) done @@ -1760,8 +1760,7 @@ locale Ipc_AC_2 = Ipc_AC_1 + and empty_slot_extended_list_integ_lift_in_ipc: "\ \list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\ empty_slot_ext a b - \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\; - \P. empty_slot_ext a b \\s. P (ekheap s)\; \P. empty_slot_ext a b \\s. P (ready_queues s)\ \ + \\_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\ \ \ \integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\ empty_slot_ext a b \\_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\" @@ -1789,7 +1788,7 @@ lemma cap_insert_ext_integrity_in_ipc_autarch: apply (simp add: integrity_tcb_in_ipc_def split del: if_split) apply (unfold integrity_def) apply (simp only: integrity_cdt_list_as_list_integ) - apply (rule hoare_lift_Pf[where f="ekheap"]) + apply (rule hoare_lift_Pf[where f="etcbs_of"]) apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def tcb_states_of_state_def get_tcb_def split del: if_split cong: if_cong) @@ -1966,7 +1965,7 @@ lemma set_original_respects_in_ipc_autarch: apply (subst (asm) integrity_asids_updates(6)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done lemma update_cdt_fun_upd_respects_in_ipc_autarch: @@ -1982,7 +1981,7 @@ lemma update_cdt_fun_upd_respects_in_ipc_autarch: apply (subst (asm) integrity_asids_updates(2)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done lemma set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch: @@ -2120,9 +2119,9 @@ lemma do_ipc_transfer_respects_in_ipc: end -lemma sts_ext_running_noop: - "\P and st_tcb_at (runnable) receiver\ set_thread_state_ext receiver \\_. P\" - apply (simp add: set_thread_state_ext_def get_thread_state_def thread_get_def +lemma sts_act_running_noop: + "\P and st_tcb_at (runnable) receiver\ set_thread_state_act receiver \\_. P\" + apply (simp add: set_thread_state_act_def get_thread_state_def thread_get_def | wp set_scheduler_action_wp)+ apply (clarsimp simp add: st_tcb_at_def obj_at_def get_tcb_def) done @@ -2133,7 +2132,7 @@ lemma set_thread_state_running_respects_in_ipc: set_thread_state receiver Running \\_. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\" apply (simp add: set_thread_state_def) - apply (wpsimp wp: set_object_wp sts_ext_running_noop) + apply (wpsimp wp: set_object_wp sts_act_running_noop) apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def get_tcb_rev update_tcb_state_in_ipc cong: if_cong elim: update_tcb_state_in_ipc[unfolded fun_upd_def]) @@ -2200,7 +2199,7 @@ lemma set_original_respects_in_ipc_reply: apply (subst (asm) integrity_asids_updates(6)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done end @@ -2230,7 +2229,7 @@ lemma update_cdt_reply_in_ipc: apply (subst (asm) integrity_asids_updates(2)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done end @@ -2280,10 +2279,10 @@ lemma set_scheduler_action_respects_in_ipc_autarch: \\_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\" unfolding set_scheduler_action_def apply (wpsimp simp: integrity_tcb_in_ipc_def integrity_def tcb_states_of_state_def get_tcb_def) - apply (subst (asm) integrity_asids_updates(4)[symmetric]) + apply (subst (asm) integrity_asids_updates(14)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done end @@ -2302,19 +2301,19 @@ lemma tcb_sched_action_respects_in_ipc_autarch: apply wp apply (clarsimp simp: integrity_def integrity_tcb_in_ipc_def tcb_states_of_state_def get_tcb_def integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def - tcb_at_def get_etcb_def tcb_sched_enqueue_def etcb_at_def + tcb_at_def tcb_sched_enqueue_def etcb_at_def split: option.splits) apply (intro conjI impI) apply (fastforce intro: exists_cons_append) - apply (subst (asm) integrity_asids_updates(4)[symmetric]) + apply (subst (asm) integrity_asids_updates(22)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) apply (fastforce intro: exists_cons_append) - apply (subst (asm) integrity_asids_updates(4)[symmetric]) + apply (subst (asm) integrity_asids_updates(22)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done crunch possible_switch_to, set_thread_state @@ -2597,7 +2596,7 @@ lemma set_thread_state_running_respects_in_ipc_reply: set_thread_state receiver Running \\_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\" apply (simp add: set_thread_state_def set_object_def get_object_def) - apply (wp sts_ext_running_noop) + apply (wp sts_act_running_noop) apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def cong: if_cong elim!: fault_tcb_atE elim: update_tcb_state_in_ipc_reply[unfolded fun_upd_def]) @@ -2638,7 +2637,7 @@ lemma set_cdt_empty_slot_respects_in_ipc_autarch: apply (subst (asm) integrity_asids_updates(2)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done end @@ -2726,17 +2725,17 @@ lemma set_scheduler_action_respects_in_fault_reply: "set_scheduler_action action \integrity_tcb_in_fault_reply aag X receiver ctxt st\" unfolding set_scheduler_action_def apply (wpsimp simp: integrity_tcb_in_fault_reply_def integrity_def tcb_states_of_state_def get_tcb_def) - apply (subst (asm) integrity_asids_updates(4)[symmetric]) + apply (subst (asm) integrity_asids_updates(14)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) - apply (fastforce simp: trans_state_def) + apply (fastforce simp: trans_state_def abstract_state.defs) done lemma handle_fault_reply_respects_in_fault_reply: "handle_fault_reply f thread label mrs \integrity_tcb_in_fault_reply aag X thread TRFContext st\" by (cases f; wpsimp wp: as_user_respects_in_fault_reply handle_arch_fault_reply_typ_at) -crunch set_thread_state_ext +crunch set_thread_state_act for respects_in_fault_reply: "integrity_tcb_in_fault_reply aag X receiver ctxt st" lemma thread_set_no_fault_respects_in_fault_reply: @@ -2744,7 +2743,7 @@ lemma thread_set_no_fault_respects_in_fault_reply: thread_set (\tcb. tcb \ tcb_fault := None \) thread \\_. integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\" apply (simp add: thread_set_def) - apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp) + apply (wp set_thread_state_act_respects_in_fault_reply set_object_wp) apply (clarsimp simp: integrity_tcb_in_fault_reply_def) apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD) apply (rule tifr_remove_fault[OF refl refl]) @@ -2756,7 +2755,7 @@ lemma set_thread_state_respects_in_fault_reply: set_thread_state thread tst \\_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\" apply (simp add: set_thread_state_def) - apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp) + apply (wp set_thread_state_act_respects_in_fault_reply set_object_wp) apply (clarsimp simp: integrity_tcb_in_fault_reply_def) apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD) apply (rule tifr_reply[OF refl refl]) diff --git a/proof/access-control/Retype_AC.thy b/proof/access-control/Retype_AC.thy index b81ad611ab..06230ee5d3 100644 --- a/proof/access-control/Retype_AC.thy +++ b/proof/access-control/Retype_AC.thy @@ -156,7 +156,7 @@ lemma sita_detype: lemmas pas_refined_by_subsets = pas_refined_state_objs_to_policy_subset lemma dtsa_detype: "domains_of_state (detype R s) \ domains_of_state s" - by (auto simp: detype_def detype_ext_def + by (auto simp: detype_def etcbs_of'_def intro: domtcbs elim!: domains_of_state_aux.cases split: if_splits) @@ -204,9 +204,10 @@ locale Retype_AC_1 = and nonzero_data_to_nat_simp: "\x. 0 < data_to_nat x \ 0 < x" and retype_region_proofs'_pas_refined: - "\ retype_region_proofs' s ty us ptr sz n dev; invs s; pas_refined aag s \ + "\ retype_region_proofs' s ty us ptr sz n dev; invs s; pas_refined aag s; + pas_cur_domain aag s; \x\ set (retype_addrs ptr ty n us). is_subject aag x \ \ pas_refined aag (s\kheap := \x. if x \ set (retype_addrs ptr ty n us) - then Some (default_object ty dev us) + then Some (default_object ty dev us (cur_domain s)) else kheap s x\)" and dmo_freeMemory_respects: "\integrity aag X st and K (is_aligned ptr bits \ bits < word_bits \ word_size_bits \ bits @@ -234,7 +235,7 @@ locale Retype_AC_1 = \x\up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} p a s st \ \ integrity_asids aag {pasSubject aag} p a s (st\kheap := \a. if a \ (\x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0 ..< n} - then Some (default_object typ dev o_bits) + then Some (default_object typ dev o_bits d) else kheap s a\)" begin @@ -243,7 +244,7 @@ lemma detype_integrity: \ integrity aag X st (detype refs s)" apply (erule integrity_trans) apply (clarsimp simp: integrity_def integrity_asids_detype) - apply (clarsimp simp: detype_def detype_ext_def integrity_def) + apply (clarsimp simp: detype_def integrity_def) done lemma sta_detype: @@ -326,14 +327,14 @@ lemma retype_region_integrity: retype_region ptr num_objects o_bits type dev \\_. integrity aag X st\" apply (rule hoare_gen_asm)+ - apply (simp only: retype_region_def retype_region_ext_extended.dxo_eq) - apply (simp only: retype_addrs_def retype_region_ext_def + apply (simp only: retype_region_def) + apply (simp only: retype_addrs_def foldr_upd_app_if' fun_app_def K_bind_def) apply wp apply (clarsimp simp: not_less) apply (erule integrity_trans) apply (clarsimp simp: integrity_def retype_region_integrity_asids) - apply (fastforce intro: tro_lrefl tre_lrefl + apply (fastforce intro: tro_lrefl dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def] simp: image_def p_assoc_help power_sub) done @@ -418,8 +419,17 @@ end context retype_region_proofs' begin -lemma domains_of_state: "domains_of_state s' \ domains_of_state s" - unfolding s'_def by simp +lemma tcb_domain_map_wellformed: + "\tcb_domain_map_wellformed aag s; pas_cur_domain aag s; \x\ set (retype_addrs ptr ty n us). is_subject aag x\ + \ tcb_domain_map_wellformed aag s'" + unfolding s'_def ps_def + apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) + apply (erule domains_of_state_aux.cases) + apply (clarsimp simp: etcbs_of'_def split: if_split_asm kernel_object.splits) + apply (clarsimp simp: default_object_def default_tcb_def tyunt split: apiobject_type.splits) + defer + apply (force intro: domtcbs) + done (* FIXME MOVE next to cte_at_pres *) lemma cte_wp_at_pres: @@ -436,79 +446,33 @@ lemma caps_of_state_pres: end - -lemma retype_region_ext_kheap_update: - "\Q xs and R xs\ retype_region_ext xs ty \\_. Q xs\ - \ \\s. Q xs (kheap_update f s) \ R xs (kheap_update f s)\ - retype_region_ext xs ty - \\_ s. Q xs (kheap_update f s)\" - apply (clarsimp simp: valid_def retype_region_ext_def) - apply (erule_tac x="kheap_update f s" in allE) - apply (clarsimp simp: split_def bind_def gets_def get_def return_def modify_def put_def) - done - -lemma use_retype_region_proofs_ext': - assumes x: "\(s::det_ext state). \ retype_region_proofs s ty us ptr sz n dev; P s \ +lemma use_retype_region_proofs': + assumes x: "\(s::det_ext state). \ retype_region_proofs s ty us ptr sz n dev; P s; pas_cur_domain aag s; + \x\ set (retype_addrs ptr ty n us). is_subject aag x \ \ Q (retype_addrs ptr ty n us) (s\kheap := \x. if x \ set (retype_addrs ptr ty n us) - then Some (default_object ty dev us ) + then Some (default_object ty dev us (cur_domain s)) else kheap s x\)" - assumes y: "\xs. \Q xs and R xs\ retype_region_ext xs ty \\_. Q xs\" - assumes z: "\f xs s. R xs (kheap_update f s) = R xs s" shows "\ ty = CapTableObject \ 0 < us; \s. P s \ Q (retype_addrs ptr ty n us) s \ \ \\s. valid_pspace s \ valid_mdb s \ range_cover ptr sz (obj_bits_api ty us) n \ caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} s \ caps_no_overlap ptr sz s \ pspace_no_overlap_range_cover ptr sz s \ (\slot. cte_wp_at (\c. up_aligned_area ptr sz \ cap_range c \ cap_is_device c = dev) slot s) \ - P s \ R (retype_addrs ptr ty n us) s\ + P s \ pas_cur_domain aag s \ (\x\ set (retype_addrs ptr ty n us). is_subject aag x)\ retype_region ptr n us ty dev \Q\" apply (simp add: retype_region_def split del: if_split) - apply (rule hoare_pre, (wp | simp)+) - apply (rule retype_region_ext_kheap_update[OF y]) - apply (wp | simp)+ + apply wpsimp apply (clarsimp simp: retype_addrs_fold foldr_upd_app_if fun_upd_def[symmetric]) apply safe - apply (rule x) - apply (rule retype_region_proofs.intro, simp_all)[1] - apply (fastforce simp: range_cover_def obj_bits_api_def z slot_bits_def2 word_bits_def)+ - done - -lemmas use_retype_region_proofs_ext = - use_retype_region_proofs_ext'[where Q="\_. Q" and P=Q, simplified] for Q - - -context is_extended begin - -lemma pas_refined_tcb_domain_map_wellformed': - assumes tdmw: "\tcb_domain_map_wellformed aag and P\ f \\_. tcb_domain_map_wellformed aag\" - shows "\pas_refined aag and P\ f \\_. pas_refined aag\" - apply (simp add: pas_refined_def) - apply (wp tdmw) - apply (wp lift_inv) - apply simp+ - done - -end - - -lemma retype_region_ext_pas_refined: - "\pas_refined aag and pas_cur_domain aag and K (\x\ set xs. is_subject aag x)\ - retype_region_ext xs ty - \\_. pas_refined aag\" - including classic_wp_pre - apply (subst and_assoc[symmetric]) - apply (wp retype_region_ext_extended.pas_refined_tcb_domain_map_wellformed') - apply (simp add: retype_region_ext_def, wp) - apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) - apply (erule domains_of_state_aux.cases) - apply (clarsimp simp: foldr_upd_app_if' fun_upd_def[symmetric] split: if_split_asm) - apply (clarsimp simp: default_ext_def default_etcb_def split: apiobject_type.splits) - defer - apply (force intro: domtcbs) + apply (rule x) + apply (rule retype_region_proofs.intro, simp_all)[1] + apply (fastforce simp: range_cover_def obj_bits_api_def slot_bits_def2 word_bits_def)+ done +lemmas use_retype_region_proofs = + use_retype_region_proofs'[where Q="\_. Q" and P=Q, simplified] for Q context Retype_AC_1 begin @@ -524,12 +488,10 @@ lemma retype_region_pas_refined: \\_. pas_refined aag\" apply (rule hoare_gen_asm) apply (rule hoare_pre) - apply (rule use_retype_region_proofs_ext'[where P = "invs and pas_refined aag"]) - apply clarsimp - apply (erule (2) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro]) - apply (wp retype_region_ext_pas_refined) - apply simp - apply auto + apply (rule use_retype_region_proofs'[where P = "invs and pas_refined aag"]) + apply clarsimp + apply (erule (4) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro]) + apply auto done end @@ -898,14 +860,11 @@ lemma retype_region_pas_refined': \\_. pas_refined aag\" apply (rule hoare_gen_asm)+ apply (rule hoare_weaken_pre) - apply (rule use_retype_region_proofs_ext'[where P="invs and pas_refined aag"]) - apply clarsimp - apply (erule (2) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro]) - apply (wp retype_region_ext_pas_refined) - apply simp - apply fastforce - apply fastforce - apply clarsimp + apply (rule use_retype_region_proofs'[where P="invs and pas_refined aag"]) + apply clarsimp + apply (erule (4) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro]) + apply simp + apply fastforce apply clarsimp apply (frule valid_cap_range_untyped[OF invs_valid_objs]) apply (fastforce simp: cte_wp_at_caps_of_state) diff --git a/proof/access-control/Syscall_AC.thy b/proof/access-control/Syscall_AC.thy index ad13ff9fb8..4acb173ce5 100644 --- a/proof/access-control/Syscall_AC.thy +++ b/proof/access-control/Syscall_AC.thy @@ -189,13 +189,16 @@ lemma set_thread_state_authorised[wp]: apply (wpsimp wp: sts_valid_arch_inv ct_in_state_set) done +crunch set_thread_state_act + for kheap[wp]: "\s. P (kheap s)" + lemma sts_first_restart: "\(=) st and (\s. thread = cur_thread s)\ set_thread_state thread Structures_A.thread_state.Restart \\rv s. \p ko. kheap s p = Some ko \ (is_tcb ko \ p \ cur_thread st) \ kheap st p = Some ko\" unfolding set_thread_state_def - by (wpsimp wp: set_object_wp dxo_wp_weak simp: is_tcb) + by (wpsimp wp: set_object_wp simp: is_tcb) lemma lcs_reply_owns: "\pas_refined aag and K (is_subject aag thread)\ @@ -397,20 +400,13 @@ lemma handle_reply_respects: dest: invs_cur) done -lemma ethread_set_time_slice_pas_refined[wp]: - "ethread_set (tcb_time_slice_update f) thread \pas_refined aag\" - apply (simp add: ethread_set_def set_eobject_def | wp)+ - apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) - apply (erule_tac x="(a, b)" in ballE) - apply force - apply (erule notE) - apply (erule domains_of_state_aux.cases, simp add: get_etcb_def split: if_split_asm) - apply (force intro: domtcbs)+ - done + lemma thread_set_time_slice_pas_refined[wp]: - "thread_set_time_slice tptr time \pas_refined aag\" - by (simp add: thread_set_time_slice_def | wp)+ + "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ + thread_set_time_slice tptr time + \\_. pas_refined aag\" + by (simp add: thread_set_time_slice_def | wp thread_set_pas_refined)+ lemma dec_domain_time_pas_refined[wp]: "dec_domain_time \pas_refined aag\" @@ -420,7 +416,6 @@ lemma dec_domain_time_pas_refined[wp]: crunch timer_tick for pas_refined[wp]: "pas_refined aag" - (wp_del: timer_tick_extended.pas_refined_tcb_domain_map_wellformed) locale Syscall_AC_wps = @@ -580,11 +575,12 @@ lemma dec_domain_time_integrity[wp]: done lemma timer_tick_integrity[wp]: - "\integrity aag X st and pas_refined aag and (\s. ct_active s \ is_subject aag (cur_thread s))\ + "\integrity aag X st and pas_refined aag and (\s. ct_active s \ is_subject aag (cur_thread s)) + and pspace_aligned and valid_vspace_objs and valid_arch_state\ timer_tick \\_. integrity aag X st\" apply (simp add: timer_tick_def) - apply (wp ethread_set_integrity_autarch gts_wp + apply (wp thread_set_integrity_autarch thread_set_pas_refined gts_wp thread_get_wp | wpc | simp add: thread_set_time_slice_def split del: if_split)+ apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) done @@ -630,6 +626,7 @@ lemma handle_interrupt_integrity: ackInterrupt_device_state_inv resetTimer_device_state_inv | wpc | simp add: get_irq_slot_def get_irq_state_def)+ + apply (rule conjI[rotated], fastforce) \ \IRQTimer preconditions\ apply clarsimp apply (rule conjI, fastforce)+ \ \valid_objs etc.\ apply (clarsimp simp: cte_wp_at_caps_of_state) @@ -676,8 +673,6 @@ lemma valid_fault_User[simp]: "valid_fault (UserException word1 word2)" by (simp add: valid_fault_def) -declare hy_inv[wp del] - lemma handle_yield_integrity[wp]: "\integrity aag X st and pas_refined aag and is_subject aag \ cur_thread\ handle_yield @@ -748,7 +743,7 @@ lemma tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues: apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def - tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def + tcb_domain_map_wellformed_aux_def etcb_at_def split: option.splits) done @@ -776,7 +771,7 @@ See comment for @{thm tcb_sched_action_dequeue_integrity'} \ lemma switch_to_thread_respects': "\integrity aag X st and pas_refined aag - and (\s. pasSubject aag \ pasDomainAbs aag (tcb_domain (the (ekheap s t))))\ + and (\s. pasSubject aag \ pasDomainAbs aag (etcb_domain (the (etcbs_of s t))))\ switch_to_thread t \\_. integrity aag X st\" unfolding switch_to_thread_def @@ -813,9 +808,6 @@ lemma choose_thread_respects: apply (clarsimp simp: etcb_at_def) (* thread we're switching to is in cur_domain *) apply (rule_tac s = "cur_domain s" in subst) - apply (clarsimp simp: max_non_empty_queue_def) - apply (frule tcb_at_ekheap_dom[OF st_tcb_at_tcb_at]) - apply (simp add: valid_sched_def) apply (clarsimp simp: max_non_empty_queue_def) apply (metis (mono_tags, lifting) setcomp_Max_has_prop hd_in_set) (* pas_cur_domain *) @@ -831,7 +823,7 @@ lemma guarded_switch_to_respects: lemma next_domain_tcb_domain_map_wellformed[wp]: "next_domain \tcb_domain_map_wellformed aag\" - by (wpsimp simp: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def) + by (wpsimp simp: next_domain_def thread_set_domain_def Let_def wp: dxo_wp_weak ) lemma valid_blocked_2_valid_blocked_except[simp]: "valid_blocked_2 queues kh sa ct \ valid_blocked_except_2 t queues kh sa ct" @@ -841,8 +833,8 @@ lemma valid_blocked_2_valid_blocked_except[simp]: lemma next_domain_valid_sched: "\valid_sched and (\s. scheduler_action s = choose_new_thread)\ next_domain \\_. valid_sched\" apply (simp add: next_domain_def Let_def) - apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def) - apply (simp add:valid_blocked_2_def) + apply (wpsimp wp: dxo_wp_weak) + apply (simp add: valid_sched_def) done text \ @@ -852,22 +844,20 @@ because t's domain may contain multiple labels. See the comment for \ lemma valid_sched_action_switch_subject_thread: "\ scheduler_action s = switch_thread t; valid_sched_action s; - valid_etcbs s; pas_refined aag s; pas_cur_domain aag s \ - \ pasObjectAbs aag t \ pasDomainAbs aag (tcb_domain (the (ekheap s t))) \ - pasSubject aag \ pasDomainAbs aag (tcb_domain (the (ekheap s t)))" + pas_refined aag s; pas_cur_domain aag s \ + \ pasObjectAbs aag t \ pasDomainAbs aag (etcb_domain (the (etcbs_of s t))) \ + pasSubject aag \ pasDomainAbs aag (etcb_domain (the (etcbs_of s t)))" apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_2_def - switch_in_cur_domain_2_def in_cur_domain_2_def valid_etcbs_def - etcb_at_def st_tcb_at_def obj_at_def is_etcb_at_def) - apply (rule conjI) - apply (force simp: pas_refined_def tcb_domain_map_wellformed_aux_def - intro: domtcbs) - apply force + switch_in_cur_domain_2_def in_cur_domain_2_def etcbs_of'_def + etcb_at_def st_tcb_at_def obj_at_def) + apply (fastforce simp: pas_refined_def tcb_domain_map_wellformed_aux_def etcbs_of'_def + intro: domtcbs) done lemma next_domain_integrity[wp]: "next_domain \integrity aag X st\" - apply (wpsimp simp: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def) - apply (clarsimp simp: get_etcb_def integrity_subjects_def lfp_def) + apply (wpsimp simp: next_domain_def Let_def reset_work_units_ext_extended.dxo_eq[simplified reset_work_units_def]) + apply (clarsimp simp: integrity_subjects_def) done lemma pas_refined_cur_thread[iff]: @@ -885,6 +875,12 @@ lemma switch_to_idle_thread_pas_refined: unfolding switch_to_idle_thread_def by (wpsimp wp: do_machine_op_pas_refined) +lemma next_domain_pas_refined[wp]: + "next_domain \pas_refined aag\" + apply (wpsimp simp: next_domain_def Let_def reset_work_units_ext_extended.dxo_eq[simplified reset_work_units_def]) + apply (clarsimp simp: pas_refined_def) + done + lemma schedule_choose_new_thread_integrity: "\invs and valid_sched and valid_list and integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag) @@ -906,7 +902,7 @@ lemma schedule_integrity: switch_to_idle_thread_respects choose_thread_respects gts_wp hoare_drop_imps set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued tcb_sched_action_enqueue_valid_blocked_except tcb_sched_action_append_integrity' - | simp add: allActiveTCBs_def schedule_choose_new_thread_def + | simp add: schedule_choose_new_thread_def | rule hoare_pre_cont[where f=next_domain])+ apply (auto simp: obj_at_def st_tcb_at_def not_cur_thread_2_def valid_sched_def valid_sched_action_def weak_valid_sched_action_def @@ -922,10 +918,9 @@ lemma schedule_integrity_pasMayEditReadyQueues: and guarded_pas_domain aag and K (pasMayEditReadyQueues aag)\ schedule \\_. integrity aag X st\" - supply ethread_get_wp[wp del] supply schedule_choose_new_thread_integrity[wp] supply if_split[split del] - apply (simp add: schedule_def wrap_is_highest_prio_def[symmetric]) + apply (simp add: schedule_def wrap_is_highest_prio_def[symmetric] ) apply (wp, wpc) (* resume current thread *) apply wp @@ -939,7 +934,8 @@ lemma schedule_integrity_pasMayEditReadyQueues: (* is_highest_prio *) apply (simp add: wrap_is_highest_prio_def) apply ((wp (once) hoare_drop_imp)+)[1] - apply (wpsimp wp: tcb_sched_action_enqueue_valid_blocked_except hoare_vcg_imp_lift' gts_wp)+ + apply (wpsimp wp: tcb_sched_action_enqueue_valid_blocked_except hoare_vcg_imp_lift' gts_wp + hoare_vcg_disj_lift hoare_vcg_all_lift)+ apply (clarsimp simp: if_apply_def2 cong: imp_cong conj_cong) apply (safe; ((solves \clarsimp simp: valid_sched_def not_cur_thread_def valid_sched_action_def weak_valid_sched_action_def\)?)) @@ -952,7 +948,7 @@ crunch choose_thread lemma schedule_pas_refined: "schedule \pas_refined aag\" - apply (simp add: schedule_def allActiveTCBs_def) + apply (simp add: schedule_def) apply (wp add: guarded_switch_to_lift switch_to_thread_pas_refined switch_to_idle_thread_pas_refined gts_wp guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues @@ -960,7 +956,6 @@ lemma schedule_pas_refined: next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps set_scheduler_action_cnt_valid_sched enqueue_thread_queued tcb_sched_action_enqueue_valid_blocked_except - del: ethread_get_wp | wpc | simp add: schedule_choose_new_thread_def)+ done @@ -970,10 +965,6 @@ crunch invoke_untyped for arch_state[wp]: "\s :: det_ext state. P (arch_state s)" (wp: crunch_wps preemption_point_inv mapME_x_inv_wp simp: crunch_simps sequence_x_mapM_x) -crunch_ignore (add: cap_swap_ext cap_move_ext cap_insert_ext create_cap_ext set_thread_state_ext - empty_slot_ext retype_region_ext set_priority ethread_set tcb_sched_action - reschedule_required possible_switch_to next_domain set_domain timer_tick) - lemma zet_zip_contrapos: "fst t \ set xs \ t \ set (zip xs ys)" by (auto simp: set_zip_helper) @@ -1021,6 +1012,9 @@ lemma sts_Restart_ct_active[wp]: apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) done +crunch reschedule_required + for ct_active [wp]: "ct_active" + lemma cancel_all_ipc_ct_active[wp]: "cancel_all_ipc ptr \ct_active\" apply (wp mapM_x_wp set_simple_ko_ct_active | wps | simp add: cancel_all_ipc_def | wpc)+ @@ -1075,9 +1069,9 @@ crunch handle_event (wp: syscall_valid crunch_wps check_cap_inv dxo_wp_weak simp: crunch_simps ignore: syscall) -crunch ethread_set, timer_tick, possible_switch_to, handle_interrupt - for pas_cur_domain[wp]: "pas_cur_domain aag" - (wp: crunch_wps simp: crunch_simps ignore_del: ethread_set timer_tick possible_switch_to) +crunch timer_tick, possible_switch_to, handle_interrupt + for pas_cur_domain[wp]: "pas_cur_domain aag :: det_state \ _" + (wp: crunch_wps simp: crunch_simps) lemma dxo_idle_thread[wp]: "\\s. P (idle_thread s) \ do_extended_op f \\_ s. P (idle_thread s)\" @@ -1106,32 +1100,31 @@ crunch handle_event (wp: syscall_valid crunch_wps simp: check_cap_at_def ignore: check_cap_at syscall) crunch - transfer_caps_loop, ethread_set, possible_switch_to, thread_set_priority, + transfer_caps_loop, possible_switch_to, thread_set_priority, set_priority, set_domain, invoke_domain, cap_move_ext, timer_tick, cap_move, cancel_badged_sends, possible_switch_to - for cur_domain[wp]: "\s. P (cur_domain s)" - (wp: crunch_wps simp: filterM_mapM rule: transfer_caps_loop_pres - ignore_del: ethread_set set_priority set_domain cap_move_ext timer_tick possible_switch_to) + for cur_domain[wp]: "\s::det_state. P (cur_domain s)" + (wp: crunch_wps simp: filterM_mapM rule: transfer_caps_loop_pres) lemma invoke_cnode_cur_domain[wp]: - "invoke_cnode a \\s. P (cur_domain s)\" + "invoke_cnode a \\s::det_state. P (cur_domain s)\" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ done crunch handle_event - for cur_domain[wp]: "\s. P (cur_domain s)" + for cur_domain[wp]: "\s::det_state. P (cur_domain s)" (wp: syscall_valid crunch_wps check_cap_inv simp: crunch_simps ignore: check_cap_at syscall) lemma handle_event_guarded_pas_domain[wp]: - "handle_event e \guarded_pas_domain aag\" + "handle_event e \guarded_pas_domain aag :: det_state \ _\" by (wpsimp wp: guarded_pas_domain_lift) lemma handle_interrupt_guarded_pas_domain[wp]: - "handle_interrupt blah \guarded_pas_domain aag\" + "handle_interrupt blah \guarded_pas_domain aag :: det_state \ _\" by (wpsimp wp: guarded_pas_domain_lift) lemma integrity_irq_state_independent[simp]: diff --git a/proof/access-control/Tcb_AC.thy b/proof/access-control/Tcb_AC.thy index 9555729fdf..32e574909f 100644 --- a/proof/access-control/Tcb_AC.thy +++ b/proof/access-control/Tcb_AC.thy @@ -115,9 +115,9 @@ lemma restart_pas_refined: restart t \\_. pas_refined aag\" apply (simp add: restart_def get_thread_state_def) - apply (wp set_thread_state_pas_refined setup_reply_master_pas_refined thread_get_wp' - | strengthen invs_mdb - | fastforce)+ + apply (wpsimp wp: set_thread_state_pas_refined setup_reply_master_pas_refined thread_get_wp' + | strengthen invs_mdb)+ + apply fastforce done lemma option_update_thread_set_safe_lift: @@ -136,20 +136,11 @@ lemma set_priority_integrity_autarch[wp]: by (simp add: set_priority_def | wp)+ lemma set_priority_pas_refined[wp]: - "\pas_refined aag\ + "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ set_priority tptr prio \\_. pas_refined aag\" - apply (simp add: set_priority_def thread_set_priority_def - ethread_set_def set_eobject_def get_etcb_def - | wp hoare_vcg_imp_lift')+ - apply (simp add: tcb_sched_action_def | wp)+ - apply (clarsimp simp: etcb_at_def pas_refined_def tcb_domain_map_wellformed_aux_def - split: option.splits) - apply (erule_tac x="(a, b)" in ballE) - apply simp - apply (erule domains_of_state_aux.cases) - apply (force intro: domtcbs split: if_split_asm) - done + unfolding set_priority_def thread_set_priority_def + by (wpsimp wp: thread_set_pas_refined) lemma gts_test[wp]: "\\\ get_thread_state t \\rv s. test rv = st_tcb_at test t s\"