diff --git a/proof/refine/ARM_HYP/CNodeInv_R.thy b/proof/refine/ARM_HYP/CNodeInv_R.thy index 637c697bf..eb5f25db8 100644 --- a/proof/refine/ARM_HYP/CNodeInv_R.thy +++ b/proof/refine/ARM_HYP/CNodeInv_R.thy @@ -9565,9 +9565,23 @@ crunch irq_states' [wp]: vcpuDisable, vcpuEnable, vcpuRestore valid_irq_states' set_gic_vcpu_ctrl_lr_def setACTLR_def ignore: getObject setObject) +crunch irq_states' [wp]: vcpuUpdate, vgicUpdate valid_irq_states' + (ignore: doMachineOp getObject setObject) + +lemma vcpuSaveRegister_irq_states'[wp]: + "\P. \\s. P (irq_masks s)\ mop \\_ s. P (irq_masks s)\ \ + vcpuSaveRegister vr r mop \valid_irq_states'\" + by (wpsimp simp: vcpuSaveRegister_def wp: doMachineOp_irq_states' + | subst doMachineOp_bind | rule empty_fail_bind)+ + lemma vcpuSave_irq_states' [wp]: "vcpuSave v \valid_irq_states'\" - sorry + apply (wpsimp simp: vcpuSave_def vcpuregs_gets wp: doMachineOp_irq_states' isb_irq_masks) + apply (rule_tac S="set gicIndices" in mapM_x_wp) + by (wpsimp wp: doMachineOp_irq_states' get_gic_vcpu_ctrl_lr_irq_masks get_gic_vcpu_ctrl_apr_irq_masks + get_gic_vcpu_ctrl_vmcr_irq_masks getACTLR_irq_masks get_gic_vcpu_ctrl_hcr_irq_masks + getSCTLR_irq_masks dsb_irq_masks + | subst doMachineOp_bind | rule empty_fail_bind)+ crunch irq_states' [wp]: finaliseCap valid_irq_states' (wp: crunch_wps hoare_unless_wp getASID_wp no_irq diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 23daef0c9..833e577bf 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -1503,10 +1503,15 @@ lemma setVCPU_cap_to'[wp]: crunch cap_to'[wp]: vcpuDisable, vcpuRestore, vcpuEnable "ex_nonz_cap_to' p" (ignore: doMachineOp getObject setObject) +crunch cap_to'[wp]: vcpuUpdate, vcpuSaveRegister, vgicUpdate "ex_nonz_cap_to' p" + (ignore: doMachineOp getObject setObject) + lemma vcpuSave_cap_to'[wp]: "\ex_nonz_cap_to' p\ vcpuSave param_a \\_. ex_nonz_cap_to' p\" apply (wpsimp simp: vcpuSave_def modifyArchState_def | simp)+ - sorry + apply (rule_tac S="set gicIndices" in mapM_x_wp) + apply wpsimp+ + done lemma vcpuSwitch_cap_to'[wp]: "\ex_nonz_cap_to' p\ vcpuSwitch param_a \\_. ex_nonz_cap_to' p\" diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index c08af256f..7a40b5782 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -4058,19 +4058,6 @@ lemma setVCPU_tcb_in_cur_domain'[wp]: "\tcb_in_cur_domain' t\ setObject p (v::vcpu) \\_. tcb_in_cur_domain' t\" by (wp tcb_in_cur_domain'_lift) -lemma setVCPU_invs: - "\invs' and valid_vcpu' v\ setObject p (v::vcpu) \\_. invs'\" - apply (simp add: invs'_def valid_state'_def valid_pspace'_def) - apply (wp sch_act_wf_lift valid_global_refs_lift' irqs_masked_lift - valid_irq_node_lift - cur_tcb_lift valid_irq_handlers_lift'' - untyped_ranges_zero_lift - updateObject_default_inv - | simp add: cteCaps_of_def - | rule setObject_ksPSpace_only)+ - apply (clarsimp simp: o_def) - oops - lemma vcpuregs_sets_invs_no_cicd'[wp]: "\invs_no_cicd'\ doMachineOp (set_r12_fiq w) \\rv. invs_no_cicd'\" "\invs_no_cicd'\ doMachineOp (set_r11_fiq w) \\rv. invs_no_cicd'\" @@ -4303,24 +4290,33 @@ lemma vcpuRestore_hyp[wp]: "\ko_wp_at' (is_vcpu' and hyp_live') v\ vcpuRestore x \\_. ko_wp_at' (is_vcpu' and hyp_live') v\" by (wpsimp simp: vcpuRestore_def wp: dmo_vcpu_hyp | subst doMachineOp_bind | rule empty_fail_bind)+ + +lemma getObject_vcpu_ko_at': + "(vcpu::vcpu, s') \ fst (getObject p s) \ s' = s \ ko_at' vcpu p s" + apply (rule context_conjI) + apply (drule use_valid, rule getObject_inv[where P="op = s"]; simp add: loadObject_default_inv) + apply (drule use_valid, rule getObject_ko_at; clarsimp simp: obj_at_simps vcpu_bits_def) + done + lemma vcpuUpdate_hyp[wp]: "\vcpu. vcpuTCBPtr (f vcpu) = vcpuTCBPtr vcpu \ \ko_wp_at' (is_vcpu' and hyp_live') v\ vcpuUpdate vr f \\_. ko_wp_at' (is_vcpu' and hyp_live') v\" - apply (wpsimp simp: vcpuUpdate_def wp: dmo_vcpu_hyp setObject_ko_wp_at - | subst doMachineOp_bind | rule empty_fail_bind)+ - apply (simp add: objBits_def objBitsKO_def archObjSize_def vcpu_bits_def pageBits_def)+ - apply (case_tac "vr=v"; wpsimp) - apply (wpsimp wp: hoare_drop_imp getObject_inv_vcpu getObject_typ_at')+ -sorry + apply (wpsimp simp: vcpuUpdate_def) + apply (wpsimp wp: setObject_ko_wp_at simp: objBits_def objBitsKO_def vcpu_bits_def pageBits_def archObjSize_def) + apply (simp, simp) + apply (wpsimp wp: hoare_drop_imp) + apply (case_tac "vr=v"; wpsimp simp: is_vcpu'_def) + by (clarsimp simp: valid_def in_monad hyp_live'_def arch_live'_def obj_at'_real_def ko_wp_at'_def projectKOs is_vcpu'_def + dest!: getObject_vcpu_ko_at')+ lemma vcpuSaveRegister_hyp[wp]: "\ko_wp_at' (is_vcpu' and hyp_live') v\ vcpuSaveRegister vr r mop \\_. ko_wp_at' (is_vcpu' and hyp_live') v\" - by (wpsimp simp: vcpuSaveRegister_def wp: dmo_vcpu_hyp setObject_ko_wp_at + by (wpsimp simp: vcpuSaveRegister_def wp: dmo_vcpu_hyp | subst doMachineOp_bind | rule empty_fail_bind)+ lemma vgicUpdate_hyp[wp]: "\ko_wp_at' (is_vcpu' and hyp_live') v\ vgicUpdate vr f \\_. ko_wp_at' (is_vcpu' and hyp_live') v\" - by (wpsimp simp: vgicUpdate_def wp: dmo_vcpu_hyp setObject_ko_wp_at + by (wpsimp simp: vgicUpdate_def wp: dmo_vcpu_hyp | subst doMachineOp_bind | rule empty_fail_bind)+ lemma vcpuSave_hyp[wp]: @@ -4332,9 +4328,12 @@ lemma vcpuSave_hyp[wp]: lemma vcpuUpdate_arch_state'[wp]: "\vcpu. vcpuTCBPtr (f vcpu) = vcpuTCBPtr vcpu \ \valid_arch_state'\ vcpuUpdate vr f \\_. valid_arch_state'\" - apply (wpsimp simp: vcpuUpdate_def hyp_live'_def arch_live'_def + including no_pre + apply (wpsimp simp: vcpuUpdate_def wp: setVCPU_valid_arch') - sorry + by (clarsimp simp: valid_def in_monad hyp_live'_def arch_live'_def valid_arch_state'_def + obj_at'_real_def ko_wp_at'_def projectKOs is_vcpu'_def + dest!: getObject_vcpu_ko_at')+ crunch arch_state'[wp]: vcpuSaveRegister, vgicUpdate "valid_arch_state'" (ignore: doMachineOp getObject setObject) @@ -4412,6 +4411,48 @@ lemma setVCPU_regs_vgic_invs': apply (fastforce simp: ko_wp_at'_def projectKOs) done +lemma setVCPU_vgic_invs': + "\invs' and ko_at' vcpu v\ + setObject v (vcpuVGIC_update f vcpu) \\_. invs'\" + unfolding invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def + valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def + supply fun_upd_apply[simp del] + apply (wpsimp wp: setObject_vcpu_no_tcb_update + [where f="\vcpu. vcpuVGIC_update f vcpu"] + sch_act_wf_lift tcb_in_cur_domain'_lift valid_queues_lift + setObject_state_refs_of' setObject_state_hyp_refs_of' valid_global_refs_lift' + valid_irq_node_lift_asm [where Q=\] valid_irq_handlers_lift' + cteCaps_of_ctes_of_lift irqs_masked_lift ct_idle_or_in_cur_domain'_lift + valid_irq_states_lift' hoare_vcg_all_lift hoare_vcg_disj_lift + valid_pde_mappings_lift' setObject_typ_at' cur_tcb_lift + setVCPU_vgic_valid_arch' + simp: objBits_simps archObjSize_def vcpu_bits_def pageBits_def + state_refs_of'_vcpu_empty state_hyp_refs_of'_vcpu_absorb) + apply (clarsimp simp: if_live_then_nonz_cap'_def obj_at'_real_def) + apply (fastforce simp: ko_wp_at'_def projectKOs) + done + +lemma setVCPU_actlr_invs': + "\invs' and ko_at' vcpu v\ + setObject v (vcpuACTLR_update f vcpu) \\_. invs'\" + unfolding invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def + valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def + supply fun_upd_apply[simp del] + apply (wpsimp wp: setObject_vcpu_no_tcb_update + [where f="\vcpu. vcpuACTLR_update f vcpu"] + sch_act_wf_lift tcb_in_cur_domain'_lift valid_queues_lift + setObject_state_refs_of' setObject_state_hyp_refs_of' valid_global_refs_lift' + valid_irq_node_lift_asm [where Q=\] valid_irq_handlers_lift' + cteCaps_of_ctes_of_lift irqs_masked_lift ct_idle_or_in_cur_domain'_lift + valid_irq_states_lift' hoare_vcg_all_lift hoare_vcg_disj_lift + valid_pde_mappings_lift' setObject_typ_at' cur_tcb_lift + setVCPU_actlr_valid_arch' + simp: objBits_simps archObjSize_def vcpu_bits_def pageBits_def + state_refs_of'_vcpu_empty state_hyp_refs_of'_vcpu_absorb) + apply (clarsimp simp: if_live_then_nonz_cap'_def obj_at'_real_def) + apply (fastforce simp: ko_wp_at'_def projectKOs) + done + lemma setVCPU_regs_vgic_actlr_invs': "\invs' and ko_at' vcpu v\ setObject v (vcpuRegs_update f (vcpuVGIC_update f' (vcpuACTLR_update f'' vcpu))) \\_. invs'\" @@ -4433,6 +4474,26 @@ lemma setVCPU_regs_vgic_actlr_invs': apply (fastforce simp: ko_wp_at'_def projectKOs) done +lemma setVCPU_regs_invs': + "\invs' and ko_at' vcpu v\ setObject v (vcpuRegs_update f vcpu) \\_. invs'\" + unfolding invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def + valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def + supply fun_upd_apply[simp del] + apply (wpsimp wp: setObject_vcpu_no_tcb_update + [where f="\vcpu. vcpuRegs_update f vcpu"] + sch_act_wf_lift tcb_in_cur_domain'_lift valid_queues_lift + setObject_state_refs_of' setObject_state_hyp_refs_of' valid_global_refs_lift' + valid_irq_node_lift_asm [where Q=\] valid_irq_handlers_lift' + cteCaps_of_ctes_of_lift irqs_masked_lift ct_idle_or_in_cur_domain'_lift + valid_irq_states_lift' hoare_vcg_all_lift hoare_vcg_disj_lift + valid_pde_mappings_lift' setObject_typ_at' cur_tcb_lift + setVCPU_regs_valid_arch' + simp: objBits_simps archObjSize_def vcpu_bits_def pageBits_def + state_refs_of'_vcpu_empty state_hyp_refs_of'_vcpu_absorb) + apply (clarsimp simp: if_live_then_nonz_cap'_def obj_at'_real_def) + apply (fastforce simp: ko_wp_at'_def projectKOs) + done + lemma vcpuDisable_invs'[wp]: "vcpuDisable v \invs'\" unfolding vcpuDisable_def isb_def setHCR_def setSCTLR_def set_gic_vcpu_ctrl_hcr_def @@ -4533,6 +4594,21 @@ lemma dmo_dsb_invs'[wp]: apply wpsimp+ done +lemma setVCPU_invs: + "\invs' and valid_vcpu' v\ setObject p (v::vcpu) \\_. invs'\" + apply (simp add: invs'_def valid_state'_def valid_pspace'_def) + apply (wp sch_act_wf_lift valid_global_refs_lift' irqs_masked_lift + valid_irq_node_lift + cur_tcb_lift valid_irq_handlers_lift'' + untyped_ranges_zero_lift + updateObject_default_inv + | simp add: cteCaps_of_def + | rule setObject_ksPSpace_only)+ + apply (clarsimp simp: o_def) + oops + + + lemma vcpuregs_sets_invs'[wp]: "\invs'\ doMachineOp (set_r12_fiq w) \\rv. invs'\" "\invs'\ doMachineOp (set_r11_fiq w) \\rv. invs'\" @@ -4589,34 +4665,30 @@ including no_pre apply wpsimp+ done -lemma vcpuUpdate_invs': - "\invs'\ vcpuUpdate v f \\_. invs'\" -(* apply (wpsimp simp: vcpuUpdate_def doMachineOp_mapM wp: mapM_wp setVCPU_regs_vgic_actlr_invs') - apply (rule_tac S="set gicIndices" in mapM_x_wp) - by (wpsimp wp: dmo'_gets_wp - simp: get_gic_vcpu_ctrl_apr_def get_gic_vcpu_ctrl_vmcr_def getACTLR_def - get_gic_vcpu_ctrl_hcr_def getSCTLR_def)+ *) sorry - lemma vcpuSaveRegister_invs': "\invs'\ doMachineOp mop \\_. invs'\ \ \invs'\ vcpuSaveRegister vr r mop \\_. invs'\" - by (wpsimp simp: vcpuSaveRegister_def doMachineOp_mapM - wp: vcpuUpdate_invs' mapM_wp setVCPU_regs_vgic_actlr_invs') + apply (wpsimp simp: vcpuSaveRegister_def doMachineOp_mapM vcpuUpdate_def + wp: mapM_wp setVCPU_regs_vgic_actlr_invs' setVCPU_regs_invs') + apply simp+ + done lemma vgicUpdate_invs': "\invs'\ vgicUpdate v f \\_. invs'\" - by (wpsimp simp: vgicUpdate_def doMachineOp_mapM - wp: vcpuUpdate_invs' mapM_wp setVCPU_regs_vgic_actlr_invs') + apply (wpsimp simp: vgicUpdate_def doMachineOp_mapM vcpuUpdate_def + wp: mapM_wp setVCPU_regs_vgic_actlr_invs' setVCPU_vgic_invs') + done lemma vcpuSave_invs': "\invs'\ vcpuSave v \\_. invs'\" apply (wpsimp simp: vcpuSave_def doMachineOp_mapM - wp: vcpuUpdate_invs' vcpuSaveRegister_invs' vgicUpdate_invs' + wp: vcpuSaveRegister_invs' vgicUpdate_invs' mapM_wp setVCPU_regs_vgic_actlr_invs') apply (rule_tac S="set gicIndices" in mapM_x_wp) - by (wpsimp wp: dmo'_gets_wp vgicUpdate_invs' vcpuSaveRegister_invs' vcpuUpdate_invs' + apply (wpsimp wp: dmo'_gets_wp vgicUpdate_invs' vcpuSaveRegister_invs' setVCPU_actlr_invs' simp: get_gic_vcpu_ctrl_apr_def get_gic_vcpu_ctrl_vmcr_def getACTLR_def - get_gic_vcpu_ctrl_hcr_def getSCTLR_def)+ + get_gic_vcpu_ctrl_hcr_def getSCTLR_def vcpuUpdate_def)+ + done lemma vcpuSwitch_invs'[wp]: "\invs' and (case v of None \ \ | Some x \ ko_wp_at' (is_vcpu' and hyp_live') x)\ @@ -5404,7 +5476,7 @@ lemma setObject_ap_ksDomScheduleIdx [wp]: lemma setASIDPool_invs [wp]: "\invs' and valid_asid_pool' ap\ setObject p (ap::asidpool) \\_. invs'\" apply (simp add: invs'_def valid_state'_def valid_pspace'_def) - apply (wp sch_act_wf_lift valid_global_refs_lift' irqs_masked_lift + apply_trace (wp sch_act_wf_lift valid_global_refs_lift' irqs_masked_lift valid_irq_node_lift cur_tcb_lift valid_irq_handlers_lift'' untyped_ranges_zero_lift