diff --git a/proof/refine/ARM/CNodeInv_R.thy b/proof/refine/ARM/CNodeInv_R.thy index 3459ade0a2..c89336a3e1 100644 --- a/proof/refine/ARM/CNodeInv_R.thy +++ b/proof/refine/ARM/CNodeInv_R.thy @@ -627,7 +627,7 @@ lemma prepareThreadDelete_ctes_of_thread: "\\s. \node. ctes_of s x = Some (CTE (ThreadCap t) node)\ prepareThreadDelete t \\rv s. \node. ctes_of s x = Some (CTE (ThreadCap t) node)\" - by (wpsimp simp: prepareThreadDelete_def) + by (wpsimp simp: prepareThreadDelete_def fpuThreadDelete_def) lemma suspend_not_recursive_ctes: "\\s. P (not_recursive_ctes s)\ @@ -655,9 +655,7 @@ lemma prepareThreadDelete_not_recursive_ctes: "\\s. P (not_recursive_ctes s)\ prepareThreadDelete t \\rv s. P (not_recursive_ctes s)\" - apply (simp only: prepareThreadDelete_def cteCaps_of_def) - apply wp - done + by (wpsimp simp: prepareThreadDelete_def fpuThreadDelete_def not_recursive_ctes_def cteCaps_of_def) definition finaliseSlot_recset :: "((word32 \ bool \ kernel_state) \ (word32 \ bool \ kernel_state)) set" @@ -5237,6 +5235,11 @@ lemma invalid_Thread_CNode: apply (clarsimp simp: obj_at'_def projectKOs) done +(* FIXME MOVE *) +lemma all_Not_False[simp]: + "All Not = False" + by blast + lemma Final_notUntyped_capRange_disjoint: "\ isFinal cap sl (cteCaps_of s); cteCaps_of s sl' = Some cap'; sl \ sl'; capUntypedPtr cap = capUntypedPtr cap'; capBits cap = capBits cap'; @@ -5251,22 +5254,12 @@ lemma Final_notUntyped_capRange_disjoint: apply (elim disjE isCapDs[elim_format]) apply (clarsimp simp: valid_cap'_def obj_at'_def projectKOs objBits_simps' - typ_at'_def ko_wp_at'_def + typ_at'_def ko_wp_at'_def + page_table_at'_def page_directory_at'_def + sameObjectAs_def3 isCap_simps split: capability.split_asm zombie_type.split_asm - arch_capability.split_asm - dest!: spec[where x=0]) - apply (clarsimp simp: sameObjectAs_def3 isCap_simps) - apply (simp add: isCap_simps) - apply (simp add: isCap_simps) - apply (clarsimp simp: valid_cap'_def - obj_at'_def projectKOs objBits_simps - typ_at'_def ko_wp_at'_def - page_table_at'_def page_directory_at'_def - split: capability.split_asm zombie_type.split_asm - arch_capability.split_asm - dest!: spec[where x=0]) - apply fastforce+ - apply (clarsimp simp: isCap_simps sameObjectAs_def3) + arch_capability.split_asm option.split_asm + dest!: spec[where x=0])+ done lemma capBits_capUntyped_capRange: @@ -8779,6 +8772,7 @@ crunch irq_states' [wp]: finaliseCap valid_irq_states' no_irq_invalidateLocalTLB_ASID no_irq_setHardwareASID no_irq_set_current_pd no_irq_invalidateLocalTLB_VAASID no_irq_cleanByVA_PoU + no_irq_switchFpuOwner no_irq_nativeThreadUsingFPU simp: crunch_simps armv_contextSwitch_HWASID_def o_def setCurrentPD_to_abs) lemma finaliseSlot_IRQInactive': diff --git a/proof/refine/ARM/Finalise_R.thy b/proof/refine/ARM/Finalise_R.thy index 58eb7048a8..0098e02e1f 100644 --- a/proof/refine/ARM/Finalise_R.thy +++ b/proof/refine/ARM/Finalise_R.thy @@ -2721,9 +2721,29 @@ lemma unbindMaybeNotification_tcb_at'[wp]: apply (wp gbn_wp' | wpc | simp)+ done +lemma dmo_nativeThreadUsingFPU_invs'[wp]: + "\invs'\ doMachineOp (nativeThreadUsingFPU thread) \\_. invs'\" + apply (wp dmo_invs' no_irq_nativeThreadUsingFPU no_irq) + apply clarsimp + apply (drule_tac P4="\m'. underlying_memory m' p = underlying_memory m p" + in use_valid[where P=P and Q="\_. P" for P]) + apply (simp add: nativeThreadUsingFPU_def machine_op_lift_def + machine_rest_lift_def split_def | wp)+ + done + +lemma dmo_switchFpuOwner_invs'[wp]: + "\invs'\ doMachineOp (switchFpuOwner thread cpu) \\_. invs'\" + apply (wp dmo_invs' no_irq_switchFpuOwner no_irq) + apply clarsimp + apply (drule_tac P4="\m'. underlying_memory m' p = underlying_memory m p" + in use_valid[where P=P and Q="\_. P" for P]) + apply (simp add: switchFpuOwner_def machine_op_lift_def + machine_rest_lift_def split_def | wp)+ + done + crunch cte_wp_at'[wp]: prepareThreadDelete "cte_wp_at' P p" crunch valid_cap'[wp]: prepareThreadDelete "valid_cap' cap" -crunch invs[wp]: prepareThreadDelete "invs'" +crunch invs[wp]: prepareThreadDelete "invs'" (ignore: doMachineOp) end diff --git a/proof/refine/ARM/Invariants_H.thy b/proof/refine/ARM/Invariants_H.thy index 70718807a6..6c90e9d601 100644 --- a/proof/refine/ARM/Invariants_H.thy +++ b/proof/refine/ARM/Invariants_H.thy @@ -2162,7 +2162,7 @@ lemma cte_wp_at_cases': apply (erule is_aligned_no_wrap') apply (simp add: word_bits_conv) apply (simp add: tcb_cte_cases_def split: if_split_asm) - apply (subgoal_tac "(p - n) + n \ (p - n) + 511") + apply (subgoal_tac "(p - n) + n \ (p - n) + 0x3FF") apply (simp add: field_simps) apply (rule word_plus_mono_right) apply (simp add: tcb_cte_cases_def split: if_split_asm) diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index b031a5bb31..368bcaf622 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/proof/refine/ARM/IpcCancel_R.thy @@ -1439,10 +1439,37 @@ lemma (in delete_one) suspend_corres: apply (clarsimp simp add: invs'_def valid_state'_def valid_queues_inQ_queues) done +lemma no_fail_switchFpuOwner[wp]: + "no_fail \ (ARM.switchFpuOwner thread cpu)" + by (simp add: ARM.switchFpuOwner_def Arch.no_fail_machine_op_lift) + +lemma no_fail_nativeThreadUsingFPU[wp]: + "no_fail \ (ARM.nativeThreadUsingFPU thread)" + unfolding ARM.nativeThreadUsingFPU_def + by (wpsimp wp: no_fail_bind Arch.no_fail_machine_op_lift) + lemma (in delete_one) prepareThreadDelete_corres: "corres dc (tcb_at t) (tcb_at' t) (prepare_thread_delete t) (ArchRetypeDecls_H.ARM_H.prepareThreadDelete t)" - by (simp add: ArchVSpace_A.ARM_A.prepare_thread_delete_def ArchRetype_H.ARM_H.prepareThreadDelete_def) + apply (simp add: ArchVSpace_A.ARM_A.prepare_thread_delete_def ArchRetype_H.ARM_H.prepareThreadDelete_def + ArchVSpace_A.ARM_A.fpu_thread_delete_def ArchRetype_H.ARM_H.fpuThreadDelete_def + ARM_H.fromPPtr_def) + apply (rule corres_guard_imp) + apply (rule corres_split[where r'="(=)"]) + apply (rule corres_machine_op) + apply (rule corres_Id, rule refl, simp) + apply wpsimp + apply (rule corres_when) + apply clarsimp + apply wpsimp + apply (rule corres_machine_op) + apply (rule corres_Id, rule refl, simp) + apply wpsimp + apply clarsimp + apply wpsimp + apply wpsimp + apply auto + done lemma no_refs_simple_strg': "st_tcb_at' simple' t s' \ P {} \ st_tcb_at' (\st. P (tcb_st_refs_of' st)) t s'" @@ -2668,6 +2695,8 @@ lemma suspend_unqueued: apply wp+ done +crunch unqueued: fpuThreadDelete "obj_at' (Not \ tcbQueued) t" + (simp: comp_def) crunch unqueued: prepareThreadDelete "obj_at' (Not \ tcbQueued) t" crunch inactive: prepareThreadDelete "st_tcb_at' ((=) Inactive) t'" crunch nonq: prepareThreadDelete " \s. \d p. t' \ set (ksReadyQueues s (d, p))" diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy index 2708b28ab0..f632ebef86 100644 --- a/proof/refine/ARM/KHeap_R.thy +++ b/proof/refine/ARM/KHeap_R.thy @@ -608,8 +608,8 @@ lemma cte_wp_at_ctes_of: apply (simp add: field_simps) apply (clarsimp split: if_split_asm del: disjCI) apply (simp add: ps_clear_def3 field_simps) - apply (rule disjI2, rule exI[where x="p - (p && ~~ mask 9)"]) - apply (clarsimp simp: ps_clear_def3[where na=9] is_aligned_mask + apply (rule disjI2, rule exI[where x="p - (p && ~~ mask tcb_bits)"]) + apply (clarsimp simp: ps_clear_def3[where na=tcb_bits] is_aligned_mask word_bw_assocs field_simps) done diff --git a/proof/refine/ARM/Retype_R.thy b/proof/refine/ARM/Retype_R.thy index 8888942ed0..71ec5946b4 100644 --- a/proof/refine/ARM/Retype_R.thy +++ b/proof/refine/ARM/Retype_R.thy @@ -2422,7 +2422,7 @@ lemma other_objs_default_relation: default_ep_def makeObject_endpoint default_notification_def makeObject_notification default_ntfn_def fault_rel_optionation_def - initContext_def + initContext_def newFPUState_def arch_tcb_context_get_def atcbContextGet_def default_arch_tcb_def newArchTCB_def arch_tcb_relation_def diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index f040d40a8e..3a75826a64 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -3213,6 +3213,18 @@ lemmas msgRegisters_unfold unfolded fromEnum_def enum_register, simplified, unfolded toEnum_def enum_register, simplified] +lemma thread_get_registers: + "thread_get (arch_tcb_get_registers \ tcb_arch) t = as_user t (gets user_regs)" + apply (simp add: thread_get_def as_user_def arch_tcb_get_registers_def + arch_tcb_context_get_def arch_tcb_context_set_def) + apply (rule bind_cong [OF refl]) + apply (clarsimp simp: gets_the_member) + apply (simp add: get_def the_run_state_def set_object_def get_object_def + put_def bind_def return_def gets_def) + apply (drule get_tcb_SomeD) + apply (clarsimp simp: map_upd_triv select_f_def image_def return_def) + done + lemma getMRs_corres: "corres (=) (tcb_at t) (tcb_at' t and case_option \ valid_ipc_buffer_ptr' buf) @@ -3222,8 +3234,7 @@ lemma getMRs_corres: by (simp add: gets_def) have T: "corres (\con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t) (thread_get (arch_tcb_get_registers o tcb_arch) t) (asUser t (mapM getRegister ARM_H.msgRegisters))" - unfolding arch_tcb_get_registers_def - apply (subst thread_get_as_user) + apply (subst thread_get_registers) apply (rule asUser_corres') apply (subst mapM_gets) apply (simp add: getRegister_def) @@ -3302,6 +3313,28 @@ lemma storeWordUser_valid_ipc_buffer_ptr' [wp]: unfolding valid_ipc_buffer_ptr'_def2 by (wp hoare_vcg_all_lift storeWordUser_typ_at') +lemma thread_set_as_user_registers: + "thread_set (\tcb. tcb \ tcb_arch := arch_tcb_set_registers (f (arch_tcb_get_registers (tcb_arch tcb))) + (tcb_arch tcb) \) t + = as_user t (modify (modify_registers f))" +proof - + have P: "\f. det (modify f)" + by (simp add: modify_def) + thus ?thesis + apply (simp add: as_user_def P thread_set_def) + apply (clarsimp simp: select_f_def simpler_modify_def bind_def image_def modify_registers_def + arch_tcb_set_registers_def arch_tcb_get_registers_def + arch_tcb_context_set_def arch_tcb_context_get_def) + done +qed + +lemma UserContext_fold: + "UserContext (fpu_state s) (foldl (\s (x, y). s(x := y)) (user_regs s) xs) = + foldl (\s (r, v). UserContext (fpu_state s) ((user_regs s)(r := v))) s xs" + apply (induct xs arbitrary: s; simp) + apply (clarsimp split: prod.splits) + by (metis user_context.sel(1) user_context.sel(2)) + lemma setMRs_corres: assumes m: "mrs' = mrs" shows @@ -3309,7 +3342,8 @@ lemma setMRs_corres: (tcb_at' t and case_option \ valid_ipc_buffer_ptr' buf) (set_mrs t buf mrs) (setMRs t buf mrs')" proof - - have setRegister_def2: "setRegister = (\r v. modify (\s. s ( r := v )))" + have setRegister_def2: + "setRegister = (\r v. modify (\s. UserContext (fpu_state s) ((user_regs s)(r := v))))" by ((rule ext)+, simp add: setRegister_def) have S: "\xs ys n m. m - n \ length xs \ (zip xs (drop n (take m ys))) = zip xs (drop n ys)" @@ -3323,24 +3357,23 @@ proof - show ?thesis using m unfolding setMRs_def set_mrs_def - apply (clarsimp simp: arch_tcb_set_registers_def arch_tcb_get_registers_def cong: option.case_cong split del: if_split) + apply (clarsimp cong: option.case_cong split del: if_split) apply (subst bind_assoc[symmetric]) apply (fold thread_set_def[simplified]) - apply (subst thread_set_as_user[where f="\context. \reg. - if reg \ set (take (length mrs) msg_registers) - then mrs ! (the_index msg_registers reg) else context reg",simplified]) + apply (subst thread_set_as_user_registers) apply (cases buf) - apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify + apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_modify take_min_len zip_take_triv2 min.commute) apply (rule corres_guard_imp) - apply (rule corres_split_nor[OF asUser_corres']) + apply (rule corres_split_nor [OF asUser_corres']) apply (rule corres_modify') - apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold + apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold UserContext_fold + modify_registers_def cong: if_cong simp del: the_index.simps) apply ((wp |simp)+)[6] \ \buf = Some a\ using if_split[split del] - apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify + apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_modify take_min_len zip_take_triv2 min.commute msgMaxLength_def msgLengthBits_def) apply (simp add: msg_max_length_def) @@ -3348,9 +3381,9 @@ proof - apply (rule corres_split_nor[OF asUser_corres']) apply (rule corres_modify') apply (simp only: msgRegisters_unfold cong: if_cong) - apply (fastforce simp: fold_fun_upd[symmetric]) + apply (fastforce simp: fold_fun_upd[symmetric] modify_registers_def UserContext_fold) apply clarsimp - apply (rule corres_split_nor) + apply (rule corres_split_nor) apply (rule_tac S="{((x, y), (x', y')). y = y' \ x' = (a + (of_nat x * 4)) \ x < unat max_ipc_words}" in zipWithM_x_corres) apply (fastforce intro: storeWordUser_corres)