theory Finalise_DR

lemma update_restart_pc_dcorres: "dcorres dc P P' (return ()) (update_restart_pc t)" apply (monad_eq simp: update_restart_pc_def as_user_def gets_the_def
                        getRegister_def setRegister_def set_object_def get_object_def
                        corres_underlying_def return_def select_f_def) apply (clarsimp simp: get_tcb_def split: option.splits kernel_object.splits) apply (clarsimp simp: transform_def transform_objects_def) apply (intro impI conjI) apply (rule ext) apply (clarsimp simp: map_add_def restrict_map_def transform_tcb_def
                          transform_full_intent_def cap_register_def capRegister_def
                          get_tcb_message_info_def msg_info_register_def msgInfoRegister_def
                          get_tcb_mrs_def msgRegisters_A_unfold
                          get_ipc_buffer_words_def transform_current_thread_def
                          ARM.faultRegister_def ARM.nextInstructionRegister_def
                   split: option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (update_restart_pc t) proof (prove)
goal (1 subgoal):
 1. \<And>b a tcb. \<lbrakk>P (transform b); P' b; get_tcb t b = Some a; kheap b t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap b)(t \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b a. \<lbrakk>P (transform b); P' b; kheap b t = Some (TCB a)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap b)(t \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b a. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a)\<rbrakk> \<Longrightarrow> (t \<noteq> idle_thread b \<longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) (if ptr = t then Some (TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>)) else (kheap b |` (- {idle_thread b} - {t})) ptr)) = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)) \<and> transform_current_thread (update_kheap ((kheap b)(t \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform_current_thread b) \<and> (t = idle_thread b \<longrightarrow> transform_current_thread (update_kheap ((kheap b)(idle_thread b \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform_current_thread b) proof (prove)
goal (3 subgoals):
 1. \<And>b a. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a); t \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) (if ptr = t then Some (TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>)) else (kheap b |` (- {idle_thread b} - {t})) ptr)) = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr))
 2. \<And>b a. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a); t \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> transform_current_thread (update_kheap ((kheap b)(t \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform_current_thread b
 3. \<And>b a. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a); t = idle_thread b\<rbrakk> \<Longrightarrow> transform_current_thread (update_kheap ((kheap b)(idle_thread b \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform_current_thread b proof (prove)
goal (3 subgoals):
 1. \<And>b a x. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a); t \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) (if ptr = t then Some (TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>)) else (kheap b |` (- {idle_thread b} - {t})) ptr))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr))) x
 2. \<And>b a. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a); t \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> transform_current_thread (update_kheap ((kheap b)(t \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform_current_thread b
 3. \<And>b a. \<lbrakk>P \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>; P' b; kheap b t = Some (TCB a); t = idle_thread b\<rbrakk> \<Longrightarrow> transform_current_thread (update_kheap ((kheap b)(idle_thread b \<mapsto> TCB (a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch a))(faultRegister := arch_tcb_context_get (tcb_arch a) nextInstructionRegister)) (tcb_arch a)\<rparr>))) b) = transform_current_thread b proof (prove)
goal:
No subgoals!