diff --git a/proof/refine/ARM_HYP/ArchAcc_R.thy b/proof/refine/ARM_HYP/ArchAcc_R.thy index 7699a3b4d..0bbf27b4f 100644 --- a/proof/refine/ARM_HYP/ArchAcc_R.thy +++ b/proof/refine/ARM_HYP/ArchAcc_R.thy @@ -103,7 +103,7 @@ lemma asid_low_bits [simp]: "asidLowBits = asid_low_bits" by (simp add: asid_low_bits_def asidLowBits_def) -lemma get_asid_pool_corres [corres]: +lemma get_asid_pool_corres [@lift_corres_args, corres]: "corres (\p p'. p = inv ASIDPool p' o ucast) (asid_pool_at p) (asid_pool_at' p) (get_asid_pool p) (getObject p)" @@ -264,7 +264,7 @@ lemma pde_relation_aligned_simp: by (clarsimp simp: pde_relation_aligned_def pde_bits_def split: ARM_HYP_H.pde.splits if_splits) -lemma get_pde_corres [corres]: +lemma get_pde_corres [@lift_corres_args, corres]: "corres (pde_relation_aligned (p >> pde_bits)) (pde_at p) (pde_at' p) (get_pde p) (getObject p)" apply (simp add: getObject_def get_pde_def get_pd_def get_object_def split_def bind_assoc) @@ -558,7 +558,7 @@ lemma valid_pde_duplicates_at'_pde_obj: done -lemma get_master_pde_corres [corres]: +lemma get_master_pde_corres [@lift_corres_args, corres]: "corres master_pde_relation (pde_at p) (pde_at' p and (\s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') @@ -568,7 +568,7 @@ lemma get_master_pde_corres [corres]: apply (rule no_fail_pre, wp) apply clarsimp apply (clarsimp simp: in_monad) - using get_pde_corres [of p] + using get_pde_corres [OF refl, of p] apply (clarsimp simp: corres_underlying_def) apply (drule bspec, assumption, clarsimp) apply (drule (1) bspec, clarsimp) @@ -642,7 +642,7 @@ lemma pte_relation_aligned_simp: by (clarsimp simp: pte_relation_aligned_def pte_bits_def split: ARM_HYP_H.pte.splits if_splits) -lemma get_pte_corres [corres]: +lemma get_pte_corres [@lift_corres_args, corres]: "corres (pte_relation_aligned (p >> pte_bits)) (pte_at p) (pte_at' p) (get_pte p) (getObject p)" apply (simp add: getObject_def get_pte_def get_pt_def get_object_def split_def bind_assoc) @@ -851,7 +851,7 @@ lemma get_master_pte_corres [corres]: apply (rule no_fail_pre, wp) apply clarsimp apply (clarsimp simp: in_monad) - using get_pte_corres [of p] + using get_pte_corres [OF refl, of p] apply (clarsimp simp: corres_underlying_def) apply (drule bspec, assumption, clarsimp) apply (drule (1) bspec, clarsimp) @@ -1273,12 +1273,11 @@ lemma getPTE_wp: lemmas get_pde_wp_valid = hoare_add_post'[OF get_pde_valid get_pde_wp] lemma page_table_at_lift: - "\s s'. (s, s') \ state_relation \ - (pspace_aligned s \ valid_pde (ARM_A.PageTablePDE ptr) s \ (ptrFromPAddr ptr) = ptr') \ + "\s s'. (s, s') \ state_relation \ (ptrFromPAddr ptr) = ptr' \ + (pspace_aligned s \ valid_pde (ARM_A.PageTablePDE ptr) s) \ pspace_distinct' s' \ page_table_at' ptr' s'" by (fastforce intro!: page_table_at_state_relation) - lemmas checkPTAt_corres [corresK] = corres_stateAssert_implied_frame[OF page_table_at_lift, folded checkPTAt_def] @@ -1457,8 +1456,7 @@ lemma createMappingEntries_valid_slots' [wp]: apply (auto elim: is_aligned_weaken) done -lemmas mapME_x_corresK_inv = - mapME_x_corres_inv[OF corresK_unlift[where F=F], THEN corresK_lift[where F=F], corresK] for F +lemmas [corresc_simp] = master_pte_relation_def master_pde_relation_def lemma ensure_safe_mapping_corres [corres]: "mapping_map m m' \ @@ -1470,11 +1468,9 @@ lemma ensure_safe_mapping_corres [corres]: apply (cases m; cases m'; simp; match premises in "(_ \ op =) p p'" for p p' \ \cases "fst p"; cases "fst p'"\; clarsimp) by (corressimp corresK: mapME_x_corresK_inv - simp: master_pte_relation_def master_pde_relation_def wp: get_master_pte_wp get_master_pde_wp getPTE_wp getPDE_wp; auto simp add: valid_mapping_entries_def)+ - lemma asidHighBitsOf [simp]: "asidHighBitsOf asid = ucast (asid_high_bits_of asid)" apply (simp add: asidHighBitsOf_def asid_high_bits_of_def asidHighBits_def) @@ -1483,10 +1479,10 @@ lemma asidHighBitsOf [simp]: done lemma page_directory_at_lift: - "\s s'. (s, s') \ state_relation \ + "corres_inst_eq ptr ptr' \ \s s'. (s, s') \ state_relation \ True \ (pspace_aligned s \ page_directory_at ptr s) \ - pspace_distinct' s' \ page_directory_at' ptr s'" - by (fastforce intro!: page_directory_at_state_relation) + pspace_distinct' s' \ page_directory_at' ptr' s'" + by (fastforce simp: corres_inst_eq_def intro!: page_directory_at_state_relation ) lemmas checkPDAt_corres = corres_stateAssert_implied_frame[OF page_directory_at_lift, folded checkPDAt_def] @@ -1501,9 +1497,7 @@ lemma ko_at_typ_at_asidpool: "ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) x s \ typ_at (AArch AASIDPool) x s" by (clarsimp simp: obj_at_def a_type_simps) -lemma find_pd_for_asid_corres [corres]: - notes [corres del] = get_asid_pool_corres and [corres] = get_asid_pool_corres' - shows +lemma find_pd_for_asid_corres [@lift_corres_args, corres]: "corres (lfr \ op =) ((\s. valid_arch_state s \ vspace_at_asid asid pd s) and valid_vspace_objs and pspace_aligned and K (0 < asid \ asid \ mask asidBits)) @@ -1544,6 +1538,7 @@ lemma find_pd_for_asid_corres [corres]: by (simp add: ranI)+ apply (insert prems) apply (fastforce simp add: asidRange_def mask_2pm1[symmetric]) + subgoal for x by (insert asid_pool_at[of x], auto simp: arm_asid_table_related) subgoal for x ko xa apply (cases ko; simp) apply (frule arm_asid_table_related[where s'=s', simplified o_def]) @@ -1562,7 +1557,7 @@ lemma find_pd_for_asid_corres': and pspace_aligned and K (0 < asid \ asid \ mask asidBits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (find_pd_for_asid asid) (findPDForASID asid)" - apply (rule corres_guard_imp, rule find_pd_for_asid_corres) + apply (rule corres_guard_imp, rule find_pd_for_asid_corres[OF refl]) apply fastforce apply simp done diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy index 161b58650..e5641748e 100644 --- a/proof/refine/ARM_HYP/Arch_R.thy +++ b/proof/refine/ARM_HYP/Arch_R.thy @@ -567,7 +567,7 @@ lemma resolve_vaddr_corres: apply (clarsimp simp: page_table_pte_at_lookupI' page_table_at_state_relation) apply clarsimp apply (erule(3) page_table_at_state_relation) - apply wp+ + apply wpsimp+ apply (clarsimp simp: page_directory_pde_at_lookupI) apply (clarsimp simp: page_directory_pde_at_lookupI' page_directory_at_state_relation) done @@ -622,7 +622,7 @@ lemma dec_arch_inv_page_flush_corres: apply (rule corres_splitEE) prefer 2 apply (rule corres_lookup_error) - apply (rule find_pd_for_asid_corres) + apply (rule find_pd_for_asid_corres[OF refl]) apply (rule whenE_throwError_corres, simp) apply simp apply (rule whenE_throwError_corres, simp) @@ -908,8 +908,7 @@ lemma dec_vcpu_inv_corres: apply (cases args; clarsimp) apply (case_tac list; clarsimp simp add: rangeCheck_def range_check_def unlessE_whenE) apply (clarsimp simp: shiftL_nat whenE_bindE_throwError_to_if) - supply corresK(7)[corresK del] - apply (corressimp corresK: corresK_if wp: get_vcpu_wp corres_rv_defer_left) + apply (corressimp wp: get_vcpu_wp) apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def ucast_id valid_cap'_def valid_cap_def make_virq_def makeVIRQ_def split:if_split) @@ -1119,7 +1118,7 @@ shows valid_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap wd (Some optv)))" in corres_guard_imp) - apply (rule find_pd_for_asid_corres) + apply (rule find_pd_for_asid_corres[OF refl]) apply (clarsimp simp: valid_cap_def) apply (simp add: mask_def) apply assumption @@ -1198,7 +1197,7 @@ shows apply (rule corres_splitEE) prefer 2 apply (rule corres_lookup_error) - apply (rule find_pd_for_asid_corres) + apply (rule find_pd_for_asid_corres[OF refl]) apply (rule whenE_throwError_corres) apply simp apply simp @@ -1270,7 +1269,7 @@ shows apply (rule corres_splitEE) prefer 2 apply (rule corres_lookup_error) - apply (rule find_pd_for_asid_corres) + apply (rule find_pd_for_asid_corres [OF refl]) apply (rule whenE_throwError_corres, simp, simp) apply (rule corres_splitEE) prefer 2 @@ -1347,7 +1346,7 @@ shows apply (rule corres_splitEE) prefer 2 apply (rule corres_lookup_error) - apply (rule find_pd_for_asid_corres) + apply (rule find_pd_for_asid_corres [OF refl]) apply (rule whenE_throwError_corres, simp) apply clarsimp apply (simp add: liftE_bindE) @@ -1389,6 +1388,7 @@ shows apply (simp, rule corres_guard_imp[OF dec_vcpu_inv_corres]; simp) done + lemma invokeVCPUInjectIRQ_corres: "corres (op =) (vcpu_at v) (vcpu_at' v) (do y \ invoke_vcpu_inject_irq v index virq; @@ -1397,12 +1397,7 @@ lemma invokeVCPUInjectIRQ_corres: (invokeVCPUInjectIRQ v index virq)" unfolding invokeVCPUInjectIRQ_def invoke_vcpu_inject_irq_def apply (clarsimp simp: bind_assoc) - apply (corressimp corres: corres_get_vcpu set_vcpu_corres wp: corres_rv_wp_left get_vcpu_wp) - apply (rule corresK_split) - apply (rule corresK_if[where F=True]) - apply (corressimp corres: corres_get_vcpu set_vcpu_corres - corresK: corresK_machine_op - wp: corres_rv_wp_left wp_post_taut get_vcpu_wp)+ + apply (corressimp corres: corres_get_vcpu set_vcpu_corres wp: get_vcpu_wp) apply clarsimp apply (safe ; case_tac "vcpuVGIC rv'" @@ -1416,7 +1411,7 @@ lemmas corres_discard_r = lemma dmo_gets_corres: "corres (op =) P P' (do_machine_op (gets f)) (doMachineOp (gets f))" - apply (corres corresK: corresK_machine_op) + apply (corres) apply (auto simp : corres_underlyingK_def) done @@ -1431,14 +1426,7 @@ lemma invoke_vcpu_read_register_corres: (invokeVCPUReadReg v r)" unfolding invoke_vcpu_read_register_def invokeVCPUReadReg_def read_vcpu_register_def readVCPUReg_def apply (rule corres_discard_r) - apply corres - apply (corres_once corresK: corresK_if) - apply (corresc) - apply (corressimp corres: corres_get_vcpu - corresK: corresK_machine_op corresK_if - wp: corres_rv_defer_left)+ - apply (rule conjI) - apply (intro allI impI conjI; rule TrueI) (* FIXME where is this coming from? *) + apply (corressimp corres: corres_get_vcpu wp: get_vcpu_wp) apply (clarsimp simp: vcpu_relation_def split: option.splits) apply (wpsimp simp: getCurThread_def)+ done @@ -1465,15 +1453,8 @@ lemma invoke_vcpu_write_register_corres: unfolding invokeVCPUWriteReg_def invoke_vcpu_write_register_def write_vcpu_register_def writeVCPUReg_def apply (rule corres_discard_r) - apply corres - apply (corres_once corresK: corresK_if) - apply (corresc) - apply (corressimp corres: set_vcpu_corres corres_get_vcpu - corresK: corresK_if corresK_machine_op - wp: corres_rv_defer_left)+ - apply (rule conjI) - apply (intro allI impI conjI; rule TrueI) (* FIXME where is this coming from? *) - apply (auto simp: vcpu_relation_def split: option.splits)[1] + apply (corressimp corres: set_vcpu_corres corres_get_vcpu wp: get_vcpu_wp) + subgoal by (auto simp: vcpu_relation_def split: option.splits) apply (wpsimp simp: getCurThread_def)+ done @@ -1504,8 +1485,9 @@ lemma associate_vcpu_tcb_corres: (associateVCPUTCB v t)" unfolding associate_vcpu_tcb_def associateVCPUTCB_def apply (clarsimp simp: bind_assoc) - apply (corressimp search: corres_get_vcpu set_vcpu_corres simp: vcpu_relation_def) - apply (wpsimp wp: get_vcpu_wp getVCPU_wp)+ + apply (corressimp search: corres_get_vcpu set_vcpu_corres + wp: get_vcpu_wp getVCPU_wp + simp: vcpu_relation_def) apply (rule_tac Q="\_. invs and tcb_at t" in hoare_strengthen_post) apply wp apply clarsimp @@ -1524,15 +1506,15 @@ lemma associate_vcpu_tcb_corres: apply (simp add: valid_vcpu'_def typ_at_tcb') apply (clarsimp simp: typ_at_to_obj_at_arches obj_at'_def) apply (clarsimp simp: typ_at_to_obj_at_arches obj_at'_def) - apply (rule corres_rv_proveT, clarsimp) - apply (wpsimp wp: arch_thread_get_wp getObject_tcb_wp simp: archThreadGet_def)+ + apply (corressimp wp: arch_thread_get_wp getObject_tcb_wp + simp: archThreadGet_def)+ apply (rule conjI) apply clarsimp apply (rule conjI) apply clarsimp apply (frule (1) sym_refs_tcb_vcpu, fastforce) apply (clarsimp simp: obj_at_def) - apply clarsimp + apply (clarsimp simp: vcpu_relation_def) apply (frule (1) sym_refs_vcpu_tcb, fastforce) apply (clarsimp simp: obj_at_def) apply normalise_obj_at' diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy index 3198f1b33..d5db8d443 100644 --- a/proof/refine/ARM_HYP/CSpace1_R.thy +++ b/proof/refine/ARM_HYP/CSpace1_R.thy @@ -558,7 +558,6 @@ lemma getSlotCap_valid: apply (clarsimp) apply (clarsimp simp add: valid_def) done - lemma rab_corres': "\ cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a; bits = length (snd a) \ \ @@ -599,7 +598,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply (clarsimp simp: in_monad) apply (rule get_cap_success) by (auto simp: in_monad intro!: get_cap_success) (* takes time *) - note if_split [split del] isCNodeCap_cap_map[simp del] drop_append[simp del] + note if_split [split del] { assume "cbits + length guard = 0 \ cbits = 0 \ guard = []" hence ?thesis apply (simp add: caps isCap_defs @@ -613,7 +612,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) hence [simp]: "((cbits + length guard = 0) = False) \ ((cbits = 0 \ guard = []) = False) \ (0 < cbits \ guard \ []) " by simp - note if_split [split del] + note if_split [split del] drop_append[simp del] from "1.prems" have ?thesis apply - @@ -624,56 +623,48 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply (subst cnode_cap_case_if) apply (corressimp search: getSlotCap_corres IH wp: get_cap_wp getSlotCap_valid no_fail_stateAssert - corres_rv_defer_right simp: locateSlot_conv) - supply isCNodeCap_cap_map[simp] apply (simp add: drop_postfix_eq) apply clarsimp apply (prove "is_aligned ptr (4 + cbits) \ cbits \ word_bits - cte_level_bits") apply (erule valid_CNodeCapE; fastforce) subgoal premises prems for s s' x apply (insert prems) - apply (rule conjI) - apply (clarsimp split: if_splits) - apply safe[1] - apply (clarsimp simp: valid_cap_def) - apply (erule cap_table_at_cte_at) - subgoal by simp - apply (frule (1) cte_wp_valid_cap) - subgoal for cap by (cases cap; simp) - apply (simp add: caps lookup_failure_map_def) - apply (frule guard_mask_shift[where guard=guard]) - apply (intro conjI) - apply fastforce - apply clarsimp - apply (rule conjI) - apply (clarsimp simp add: objBits_simps cte_level_bits_def) - apply (erule (2) valid_CNodeCapE) - apply (erule (3) cte_map_shift') - subgoal by simp - apply (clarsimp simp add: objBits_simps cte_level_bits_def) - apply (erule (1) cte_map_shift; assumption?) - subgoal by simp - apply (clarsimp simp: cte_level_bits_def) - apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps) - apply (rule and_mask_less_size, simp add: word_bits_def word_size cte_level_bits_def) - apply (clarsimp simp: isCap_simps caps split: if_splits) - apply (intro conjI impI allI;clarsimp?) + apply (rule context_conjI) + apply (simp add: guard_mask_shift[OF \to_bl _ = _\, where guard=guard,symmetric]) + apply (simp add: caps lookup_failure_map_def) + apply (rule conjI) + apply (clarsimp split: if_splits) + apply (intro conjI impI allI;clarsimp?) apply (subst \to_bl _ = _\[symmetric]) apply (drule postfix_dropD) - apply clarsimp + apply clarsimp apply (prove "32 + (cbits + length guard) - length cref = (cbits + length guard) + (32 - length cref)") apply (drule len_drop_lemma, simp, arith) apply simp apply (subst drop_drop [symmetric]) subgoal by simp - apply (simp add: objBits_simps cte_level_bits_def) - apply (erule (1) cte_map_shift; assumption?) - apply clarsimp - subgoal by (simp add: cte_level_bits_def) - done - done + apply (erule (2) valid_CNodeCapE) + apply (rule cap_table_at_cte_at[OF _ refl]) + apply (simp add: obj_at_def is_cap_table_def well_formed_cnode_n_def) + apply (frule (2) cte_wp_valid_cap) + apply (rule context_conjI) + apply (intro conjI impI allI;clarsimp?) + apply (clarsimp simp add: objBits_simps cte_level_bits_def) + apply (erule (2) valid_CNodeCapE) + apply (erule (3) cte_map_shift') + apply simp + apply (clarsimp simp add: objBits_simps cte_level_bits_def) + apply (erule (1) cte_map_shift; assumption?) + subgoal by simp + apply (clarsimp simp: cte_level_bits_def) + apply (rule conjI) + apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps) + apply (rule and_mask_less_size, simp add: word_bits_def word_size cte_level_bits_def) + apply (clarsimp split: if_splits) + done + done } ultimately show ?thesis by fast diff --git a/proof/refine/ARM_HYP/Corres.thy b/proof/refine/ARM_HYP/Corres.thy index 3006042b7..aba52e6ef 100644 --- a/proof/refine/ARM_HYP/Corres.thy +++ b/proof/refine/ARM_HYP/Corres.thy @@ -9,7 +9,7 @@ *) theory Corres -imports StateRelation "../../../lib/Corres_Method" +imports StateRelation "../../../lib/CorresK_Lemmas" begin text {* Instantiating the corres framework to this particular state relation. *} diff --git a/proof/refine/ARM_HYP/Finalise_R.thy b/proof/refine/ARM_HYP/Finalise_R.thy index f1e6aa0ae..3110db8be 100644 --- a/proof/refine/ARM_HYP/Finalise_R.thy +++ b/proof/refine/ARM_HYP/Finalise_R.thy @@ -4753,27 +4753,6 @@ lemma cteDeleteOne_ct_not_ksQ: apply (clarsimp) done -(* FIXME move to Corres_Method? *) - -lemma corres_underlying_equiv_raw: "(nf \ no_fail P f) \ (nf' \ no_fail P' f) \ - corres_underlyingK Id nf nf' True (op =) P P' f f" - apply (simp add: corres_underlyingK_def corres_underlying_def Id_def) - by (auto simp: no_fail_def) - -lemma corres_underlying_equiv_dc_raw: "(nf \ no_fail P f) \ (nf' \ no_fail P' f) \ - corres_underlyingK Id nf nf' True dc P P' f f" - apply (simp add: corres_underlyingK_def corres_underlying_def Id_def) - by (auto simp: no_fail_def) -(* FIXME cleanup *) - -lemmas corres_underlying_equiv [corresK] = - corres_underlying_equiv_raw[where nf=False and nf'=True and P=\, simplified] - -lemmas corres_underlying_equiv_dc [corresK] = - corres_underlying_equiv_dc_raw[where nf=False and nf'=True and P=\, simplified] - -(* end of move to Corres_Method *) - (* FIXME Move to Machine_AI? *) lemma no_fail_set_gic_vcpu_ctrl_lr[wp]: "no_fail \ (set_gic_vcpu_ctrl_lr w p)" by (wpsimp simp: set_gic_vcpu_ctrl_lr_def) diff --git a/proof/refine/ARM_HYP/Interrupt_R.thy b/proof/refine/ARM_HYP/Interrupt_R.thy index 739ddf976..d6188d8f4 100644 --- a/proof/refine/ARM_HYP/Interrupt_R.thy +++ b/proof/refine/ARM_HYP/Interrupt_R.thy @@ -627,6 +627,46 @@ crunch ex_nonz_cap_to' [wp]: doMachineOp "\s. P (ex_nonz_cap_to' (ksCurT lemma runnable_not_halted: "runnable st \ \ halted st" by (auto simp: runnable_eq) +lemma dmo_wp_no_rest: + "\K((\s f. P s = (P (machine_state_update (machine_state_rest_update f) s)))) and P\ do_machine_op (machine_op_lift f) \\_. P\" + apply (simp add: do_machine_op_def machine_op_lift_def bind_assoc) + apply wpsimp + apply (clarsimp simp add: machine_rest_lift_def in_monad select_f_def ignore_failure_def) + apply (clarsimp split: if_splits) + apply (drule_tac x=s in spec) + apply (drule_tac x="\_. b" in spec) + apply simp + apply (erule rsubst[OF _ arg_cong[where f=P]]) + apply clarsimp + done + +lemma dmo_gets_wp: + "\\s. P (f (machine_state s)) s\ do_machine_op (gets f) \P\" + apply (simp add: submonad_do_machine_op.gets) + apply wpsimp + done + +lemma thread_state_relation_frame: + "thread_state_relation st'' st' \ + thread_state_relation st st' = (st = st'')" + by (cases st''; cases st'; cases st; fastforce) + +lemma thread_state_relation_send_rev_simp: + "thread_state_relation st (BlockedOnSend a b c d) = + (\y. (st = (Structures_A.BlockedOnSend a y)) \ b = sender_badge y \ c = sender_can_grant y \ d = sender_is_call y)" + by (cases st; fastforce) + +lemmas thread_state_rev_simps'[#\solves \simp\\] = + thread_state_relation_frame[of Structures_A.thread_state.Running Structures_H.thread_state.Running] + thread_state_relation_frame[of Structures_A.thread_state.Inactive Structures_H.thread_state.Inactive] + thread_state_relation_frame[of "Structures_A.thread_state.BlockedOnReceive x" "Structures_H.thread_state.BlockedOnReceive x" for x] + thread_state_relation_frame[of Structures_A.thread_state.Restart Structures_H.thread_state.Restart] + thread_state_relation_frame[of "Structures_A.thread_state.BlockedOnNotification x" "Structures_H.thread_state.BlockedOnNotification x" for x] + thread_state_relation_frame[of Structures_A.thread_state.IdleThreadState Structures_H.thread_state.IdleThreadState] + thread_state_relation_frame[of "Structures_A.thread_state.BlockedOnReply" "Structures_H.thread_state.BlockedOnReply"] + +lemmas thread_state_rev_simps = thread_state_rev_simps' thread_state_relation_send_rev_simp + lemma vgic_maintenance_corres [corres]: "corres dc einvs (\s. invs' s \ sch_act_not (ksCurThread s) s \ (\p. ksCurThread s \ set (ksReadyQueues s p))) @@ -638,26 +678,19 @@ lemma vgic_maintenance_corres [corres]: get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_lr_def set_gic_vcpu_ctrl_lr_def cong: if_cong) - apply (corres corres: gct_corres[unfolded getCurThread_def] gts_corres - corresK: corresK_if) - (* 33 subgoals; the following solves all but one. *) - apply (corres corres: hf_corres - | (rule corres_rv_weaken[OF _ corres_rv_trivial]; fastforce) - | (rule corres_rv_weaken[OF _ corres_rv_trivial]; case_tac rv; case_tac rv'; - fastforce simp: runnable_eq) - | unfold valid_fault_def - | solves \wp dmo'_gets_wp gts_wp gts_wp'\ - | solves \simp; intro conjI impI; wp\ - | solves \simp only: submonad_do_machine_op.gets; wp\ - )+ - apply (auto simp: valid_fault_def + apply (corressimp corres: gct_corres[unfolded getCurThread_def] + gts_corres[@lift_corres_args] + wp: no_fail_machine_op_lift dmo_wp_no_rest) + apply (corressimp corres: hf_corres[@lift_corres_args] + wp: dmo_gets_wp dmo'_gets_wp gts_wp gts_wp')+ + apply safe + by (auto simp: valid_fault_def thread_state_rev_simps elim: ct_active_st_tcb_at_weaken [OF _ iffD1[OF runnable_eq], simplified ct_in_state_def] st_tcb_ex_cap'[OF _ _ runnable_not_halted] st_tcb_ex_cap'' pred_tcb'_weakenE split: Structures_H.thread_state.splits) - done lemma handle_reserved_irq_corres[corres]: "corres dc einvs @@ -725,8 +758,7 @@ lemma handle_interrupt_corres: apply wp+ apply clarsimp apply clarsimp - apply (corres corresK: corresK_machine_op) - apply (wpsimp simp: no_fail_ackInterrupt)+ + apply corressimp done lemma invs_ChooseNewThread: diff --git a/proof/refine/ARM_HYP/IpcCancel_R.thy b/proof/refine/ARM_HYP/IpcCancel_R.thy index 50c35326c..b4aeb3f81 100644 --- a/proof/refine/ARM_HYP/IpcCancel_R.thy +++ b/proof/refine/ARM_HYP/IpcCancel_R.thy @@ -1433,15 +1433,8 @@ lemma archThreadGet_corres: "(\a a'. arch_tcb_relation a a' \ f a = f' a') \ corres (op =) (tcb_at t) (tcb_at' t) (arch_thread_get f t) (archThreadGet f' t)" unfolding arch_thread_get_def archThreadGet_def - apply corres - apply (rule corresK_drop) - apply (rule corres_bind_return2) - apply (rule corres_split) - prefer 2 - apply (rule get_tcb_corres) - apply (rule corres_return[where P=\ and P'=\,THEN iffD2]) - apply (clarsimp simp: tcb_relation_def) - apply wpsimp+ + apply (corressimp corres: get_tcb_corres) + apply (clarsimp simp: tcb_relation_def) done lemma tcb_vcpu_relation: @@ -1469,11 +1462,10 @@ lemma corres_gets_current_vcpu[corres]: lemma vcpuInvalidateActive_corres[corres]: "corres dc \ \ vcpu_invalidate_active vcpuInvalidateActive" unfolding vcpuInvalidateActive_def vcpu_invalidate_active_def - apply (corressimp corres: vcpuDisable_corres simp: modifyArchState_def) - apply (rule corresK_assume_guard) - apply (rule corres_modify[where P=\ and P'=\]) - apply (clarsimp simp: state_relation_def arch_state_relation_def) - apply wpsimp+ + apply (corressimp corres: vcpuDisable_corres + corresK: corresK_modifyT + simp: modifyArchState_def) + apply (clarsimp simp: state_relation_def arch_state_relation_def) done lemma tcb_ko_at': @@ -1484,17 +1476,15 @@ lemma archThreadSet_corres: "(\a a'. arch_tcb_relation a a' \ arch_tcb_relation (f a) (f' a')) \ corres dc (tcb_at t) (tcb_at' t) (arch_thread_set f t) (archThreadSet f' t)" apply (simp add: arch_thread_set_def archThreadSet_def) - apply (corres corres: get_tcb_corres) - apply (rule corresK_drop) - apply (rename_tac tcb tcb') - apply (rule_tac tcb=tcb and tcb'=tcb' in tcb_update_corres') - apply (simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+ - apply wpsimp+ + apply (corres corres: get_tcb_corres tcb_update_corres') + apply wpsimp+ + apply (auto simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+ done lemma archThreadSet_corres_vcpu_None[corres]: - "corres dc (tcb_at t) (tcb_at' t) - (arch_thread_set (tcb_vcpu_update Map.empty) t) (archThreadSet (atcbVCPUPtr_update Map.empty) t)" + "t = t' \ corres dc (tcb_at t) (tcb_at' t') + (arch_thread_set (tcb_vcpu_update Map.empty) t) (archThreadSet (atcbVCPUPtr_update Map.empty) t')" + apply simp apply (rule archThreadSet_corres) apply (simp add: arch_tcb_relation_def) done @@ -1505,19 +1495,19 @@ lemma no_fail_getRegister[wp]: "no_fail \ (getRegister r)" lemma no_fail_setRegister[wp]: "no_fail \ (setRegister r v)" by (simp add: setRegister_def) +lemmas corresK_as_user' = + corres_as_user'[atomized, THEN corresK_lift_rule, THEN mp] + lemma asUser_sanitise_corres[corres]: - "b=b' \ corres dc (tcb_at t) (tcb_at' t) + "b=b' \ t = t' \ corres dc (tcb_at t) (tcb_at' t') (as_user t (do cpsr \ getRegister CPSR; setRegister CPSR (sanitise_register b CPSR cpsr) od)) - (asUser t (do cpsr \ getRegister CPSR; + (asUser t' (do cpsr \ getRegister CPSR; setRegister CPSR (sanitiseRegister b' CPSR cpsr) od))" unfolding sanitiseRegister_def sanitise_register_def - apply (corres corres: corres_as_user') - apply (clarsimp simp: tcb_relation_def arch_tcb_relation_def) - apply (rule corres_Id, simp, simp) - apply wpsimp + apply (corressimp corresK: corresK_as_user') done crunch typ_at'[wp]: vcpuInvalidateActive "\s. P (typ_at' T p s)" @@ -1553,7 +1543,7 @@ lemma helper: "vcpu_relation v1 v2 \ vcpu_relation v1 v3 \ko. \tcb. ko = TCB tcb \ tcb_vcpu (tcb_arch tcb) = Some v) t and obj_at (\ko. \vcpu. ko = ArchObj (VCPU vcpu) \ vcpu_tcb vcpu = Some t) v) (tcb_at' t and vcpu_at' v) @@ -1565,7 +1555,7 @@ lemma dissociateVCPUTCB_corres [corres]: simp: archThreadSet_def tcb_ko_at' tcb_at_typ_at' | strengthen imp_drop_strg[where Q="tcb_at t s" for s] imp_drop_strg[where Q="vcpu_at' v s \ typ_at' TCBT t s" for s] - | (rule corres_rv_proveT, fastforce simp: vcpu_relation_def ))+ + | corres_rv)+ apply (corressimp wp: get_vcpu_wp getVCPU_wp getObject_tcb_wp arch_thread_get_wp corres_rv_wp_left simp: archThreadGet_def tcb_ko_at')+ apply (clarsimp simp: typ_at_tcb' typ_at_to_obj_at_arches) @@ -1593,8 +1583,6 @@ lemma prepareThreadDelete_corres: apply (wp arch_thread_get_wp) apply (wpsimp wp: getObject_tcb_wp simp: archThreadGet_def) apply clarsimp - apply (rule corres_rv_proveT, simp) - apply clarsimp apply (rule conjI) apply clarsimp apply (frule (1) sym_refs_tcb_vcpu, fastforce) diff --git a/proof/refine/ARM_HYP/KHeap_R.thy b/proof/refine/ARM_HYP/KHeap_R.thy index ccbc4d28c..f0f9f0840 100644 --- a/proof/refine/ARM_HYP/KHeap_R.thy +++ b/proof/refine/ARM_HYP/KHeap_R.thy @@ -1142,7 +1142,7 @@ lemma set_ep_corres [corres]: (set_endpoint ptr e) (setEndpoint ptr e')" apply (simp add: set_endpoint_def setEndpoint_def is_ep_def[symmetric]) apply (corres_search search: set_other_obj_corres[where P="\_. True"]) - apply (wp get_object_ret get_object_wp)+ + apply (corressimp wp: get_object_ret get_object_wp)+ by (clarsimp simp: is_ep obj_at_simps) lemma set_ntfn_corres [corres]: @@ -1151,7 +1151,7 @@ lemma set_ntfn_corres [corres]: (set_notification ptr ae) (setNotification ptr ae')" apply (simp add: set_notification_def setNotification_def is_ntfn_def[symmetric]) apply (corres_search search: set_other_obj_corres[where P="\_. True"]) - apply (wp get_object_ret get_object_wp)+ + apply (corressimp wp: get_object_ret get_object_wp)+ by (clarsimp simp: is_ntfn obj_at_simps) lemma no_fail_getNotification [wp]: diff --git a/proof/refine/ARM_HYP/Refine.thy b/proof/refine/ARM_HYP/Refine.thy index b4542175c..7ff4ea534 100644 --- a/proof/refine/ARM_HYP/Refine.thy +++ b/proof/refine/ARM_HYP/Refine.thy @@ -535,8 +535,12 @@ proof - pointerInDeviceData_relation[OF rel valid' valid]) qed -definition +abbreviation + "ex_abs G \ ex_abs_underlying state_relation G" + +lemma ex_abs_def: "ex_abs G \ \s'. \s. ((s :: (det_ext) state),s') \ state_relation \ G s" + by (auto simp add: ex_abs_underlying_def[abs_def]) lemma device_update_invs': "\invs'\doMachineOp (device_memory_update ds) diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 87440aa6f..e750ce387 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -1068,7 +1068,7 @@ lemma arch_switch_idle_thread_corres: arch_switch_to_idle_thread Arch.switchToIdleThread" unfolding arch_switch_to_idle_thread_def ARM_HYP_H.switchToIdleThread_def - apply (corressimp corres: git_corres set_vm_root_corres vcpuSwitch_corres[where vcpu=None, simplified] + apply (corressimp corres: git_corres set_vm_root_corres[@lift_corres_args] vcpuSwitch_corres[where vcpu=None, simplified] wp: tcb_at_idle_thread_lift tcb_at'_ksIdleThread_lift vcpuSwitch_it') apply (clarsimp simp: invs_valid_objs invs_arch_state invs_valid_asid_map invs_valid_vs_lookup invs_psp_aligned invs_distinct invs_unique_refs invs_vspace_objs) diff --git a/proof/refine/ARM_HYP/SubMonad_R.thy b/proof/refine/ARM_HYP/SubMonad_R.thy index 136759456..b35206666 100644 --- a/proof/refine/ARM_HYP/SubMonad_R.thy +++ b/proof/refine/ARM_HYP/SubMonad_R.thy @@ -32,7 +32,7 @@ lemma corres_machine_op: done lemmas corresK_machine_op = - corres_machine_op[atomized, THEN corresK_lift_rule, rule_format] + corres_machine_op[atomized, THEN corresK_lift_rule, rule_format, corresK] lemma doMachineOp_mapM: assumes "\x. empty_fail (m x)" diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index 7e437161b..6eba504d1 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -2110,7 +2110,7 @@ lemma unmap_page_corres: apply (rule corres_guard_imp) apply (rule corres_split_catch [where E="\_. \" and E'="\_. \"], simp) apply (rule corres_split_strengthen_ftE[where ftr'=dc], - rule find_pd_for_asid_corres) + rule find_pd_for_asid_corres[OF refl]) apply (rule corres_splitEE) apply clarsimp apply (rule flush_page_corres)