diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy index 176c55851..6dcbcb132 100644 --- a/proof/refine/ARM_HYP/Arch_R.thy +++ b/proof/refine/ARM_HYP/Arch_R.thy @@ -2589,7 +2589,7 @@ lemma assoc_invs': apply (clarsimp simp: typ_at_tcb' obj_at'_def) supply fun_upd_apply[simp] - apply clarsimp + apply (clarsimp simp: hyp_live'_def arch_live'_def) apply (rule_tac rfs'="state_hyp_refs_of' s" in delta_sym_refs, assumption) apply (clarsimp split: if_split_asm) apply (clarsimp simp: state_hyp_refs_of'_def obj_at'_def projectKOs tcb_vcpu_refs'_def diff --git a/proof/refine/ARM_HYP/Finalise_R.thy b/proof/refine/ARM_HYP/Finalise_R.thy index 69f1b682c..3880283c5 100644 --- a/proof/refine/ARM_HYP/Finalise_R.thy +++ b/proof/refine/ARM_HYP/Finalise_R.thy @@ -2643,12 +2643,12 @@ lemma dissoc_invs': apply (drule (1) valid_objs_valid_vcpu') apply (clarsimp simp: valid_vcpu'_def) supply fun_upd_apply[simp] - apply (rule_tac rfs'="state_hyp_refs_of' s" in delta_sym_refs, assumption) - apply (clarsimp split: if_split_asm) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp: state_hyp_refs_of'_def obj_at'_def projectKOs tcb_vcpu_refs'_def + apply (clarsimp simp: state_hyp_refs_of'_def obj_at'_def projectKOs tcb_vcpu_refs'_def split: option.splits if_split_asm) - apply (clarsimp simp: state_hyp_refs_of'_def obj_at'_def projectKOs) + apply safe + apply (rule_tac rfs'="state_hyp_refs_of' s" in delta_sym_refs) + apply (clarsimp simp: state_hyp_refs_of'_def obj_at'_def projectKOs tcb_vcpu_refs'_def + split: option.splits if_split_asm)+ done lemma setVCPU_archThreadSet_None_eq: diff --git a/proof/refine/ARM_HYP/PageTableDuplicates.thy b/proof/refine/ARM_HYP/PageTableDuplicates.thy index ad17bd6a3..037a424ac 100644 --- a/proof/refine/ARM_HYP/PageTableDuplicates.thy +++ b/proof/refine/ARM_HYP/PageTableDuplicates.thy @@ -1347,10 +1347,23 @@ lemma lookupPTSlot_aligned: apply (case_tac sz,simp_all add:ptBits_def pageBits_def) done +lemma doMachineOp_live_vcpu_at_tcb[wp]: "\\s xb. (p s) = (p (s\ksMachineState := xb\))\ \ doMachineOp f \\s. live_vcpu_at_tcb (p s) s\" + apply (simp add: doMachineOp_def) + apply wpsimp + apply (rule_tac x=x in exI) + apply (case_tac "atcbVCPUPtr (tcbArch x)") + apply clarsimp+ + done + +lemma flushPage_valid_arch_state'[wp]: "flushPage a pd asid vptr \ valid_arch_state' \" + apply (simp add: flushPage_def setVMRootForFlush_def) + apply(wpsimp wp: crunch_wps getHWASID_valid_arch' simp: crunch_simps unless_def)+ + sorry + crunch valid_arch_state'[wp]: flushPage valid_arch_state' (wp: crunch_wps getHWASID_valid_arch' simp: crunch_simps unless_def - ignore:getObject updateObject setObject) + ignore:getObject updateObject setObject doMachineOp) crunch valid_arch_state'[wp]: flushTable "\s. vs_valid_duplicates' (ksPSpace s)" diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy index 3b62cd3e1..9d792feb6 100644 --- a/proof/refine/ARM_HYP/Retype_R.thy +++ b/proof/refine/ARM_HYP/Retype_R.thy @@ -4349,6 +4349,8 @@ apply (wp createObjects_orig_ko_wp_at2') apply auto done +crunch ko_wp_at_'_P[wp]: doMachineOp "\s. P (ko_wp_at' P' t s)" + lemma createNewCaps_ko_wp_atQ': "\(\s. P (ko_wp_at' P' p s) \ range_cover ptr sz (APIType_capBits ty us) n \ n \ 0 diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index 037d3429f..08d63d3f6 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -3668,17 +3668,24 @@ lemma setObject_vcpu_obj_at'_no_vcpu[wp]: done lemma setVCPU_valid_arch': - "\valid_arch_state' and (\s. vcpuTCBPtr vcpu = None \ - (\p a. armHSCurVCPU (ksArchState s) = Some (p,a) \ p \ v)) \ - setObject v (vcpu::vcpu) \\_. valid_arch_state'\" - apply (simp add: valid_arch_state'_def valid_asid_table'_def option_case_all_conv) - apply wp_pre - apply (rule hoare_lift_Pf[where f=ksArchState]; (wp hoare_vcg_imp_lift hoare_vcg_all_lift)?) -apply (wpsimp wp: setObject_ko_wp_at simp: objBits_simps archObjSize_def vcpu_bits_def pageBits_def, simp+) -apply wpsimp+ - sorry - -(*****) + "\valid_arch_state' and (\s. \a. armHSCurVCPU (ksArchState s) = Some (v,a) \ hyp_live' (KOArch (KOVCPU vcpu))) \ + setObject v (vcpu::vcpu) + \\_. valid_arch_state'\" + apply (simp add: valid_arch_state'_def valid_asid_table'_def option_case_all_conv pred_conj_def) + apply (rule hoare_vcg_conj_lift[rotated]) + apply (rule hoare_vcg_conj_lift[rotated]) + apply (subst conj_commute[where P="\a. _ a \ _ a"]) + apply (subst conj_commute[where P="\a. _ a \ _ a"]) + apply (subst conj_assoc)+ + apply (rule hoare_vcg_conj_lift[rotated]) + apply (rule hoare_vcg_conj_lift[rotated]) + apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) + apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift setObject_ko_wp_at) + apply (simp add: objBits_simps archObjSize_def vcpu_bits_def pageBits_def)+ + apply safe + apply (clarsimp simp: is_vcpu'_def ko_wp_at'_def)+ + apply (wp hoare_vcg_all_lift hoare_drop_imp)+ +done lemma setVCPU_nosch [wp]: "\\s. P (ksSchedulerAction s)\ setObject p (v::vcpu) \\rv s. P (ksSchedulerAction s)\" @@ -4286,11 +4293,42 @@ lemma vcpuSwitch_invs_no_cicd'[wp]: apply (auto simp: invs_no_cicd'_def valid_state'_def valid_arch_state'_def pred_conj_def) done +crunch valid_arch_state'[wp]: checkPDNotInASIDMap valid_arch_state' +crunch valid_arch_state'[wp]: findPDForASID valid_arch_state' +crunch valid_arch_state'[wp]: armv_contextSwitch valid_arch_state' +crunch ko_wp_at'[wp]: armv_contextSwitch "ko_wp_at' P' t" + +lemma valid_case_option_post_wp': + "(\x. \P x\ f \\rv. Q x\) \ + \case ep of Some x \ P x | _ \ \_. True\ + f \\rv. case ep of Some x \ Q x | _ \ \_. True\" + by (cases ep, simp_all add: hoare_vcg_prop) + +abbreviation + "live_vcpu_at_tcb p s \ \x. ko_at' x p s \ + (case atcbVCPUPtr (tcbArch x) of None \ \_. True + | Some x \ ko_wp_at' (is_vcpu' and hyp_live') x) s" + lemma setVMRoot_valid_arch_state'[wp]: - "\valid_arch_state'\ setVMRoot p \\rv. valid_arch_state'\" + "\valid_arch_state' and live_vcpu_at_tcb p\ + setVMRoot p + \\rv. valid_arch_state'\" apply (simp add: setVMRoot_def getThreadVSpaceRoot_def) - apply (wpsimp simp: checkPDNotInASIDMap_def throwError_def wp: getObject_tcb_wp) - sorry + apply ((wpsimp wp: hoare_vcg_imp_lift hoare_vcg_ex_lift + getObject_tcb_wp valid_case_option_post_wp' + whenE_inv locateSlotTCB_inv)+ + , rule_tac x=x in exI + , subst simp_thms + , clarsimp)+ + apply wpsimp+ + apply (rule_tac Q="\_. valid_arch_state' and live_vcpu_at_tcb p" + in hoare_post_imp) + apply clarsimp + apply fastforce + apply (wpsimp wp: hoare_vcg_imp_lift hoare_vcg_ex_lift + getObject_tcb_wp valid_case_option_post_wp' + whenE_inv locateSlotTCB_inv)+ + done lemma setVMRoot_invs'[wp]: "\invs'\ setVMRoot p \\rv. invs'\"