theory Finalise_R

lemma tcb_update_all_corres':
  assumes tcbs: "tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'"
  assumes tables: "\<forall>(getF, v) \<in> ran tcb_cap_cases. getF tcbu = getF tcb"
  assumes tables': "\<forall>(getF, v) \<in> ran tcb_cte_cases. getF tcbu' = getF tcb'"
  assumes r: "r () ()"
  assumes e: "etcb_relation etcb tcb' \<Longrightarrow> etcb_relation etcbu tcbu'"
  shows "corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb))
                  (ko_at' tcb' add)
                  (set_thread_all add tcbu etcbu) (setObject add tcbu')" apply (rule_tac F="tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu'" in corres_req) apply (clarsimp simp: state_relation_def obj_at_def obj_at'_def) apply (frule(1) pspace_relation_absD) apply (force simp: projectKOs other_obj_relation_def ekheap_relation_def e) apply (erule conjE) apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (rule set_thread_all_corres[where P="(=) tcb'"]) apply (rule ext)+ apply simp defer apply (simp add: is_other_obj_relation_type_def
                           projectKOs objBits_simps'
                           other_obj_relation_def tcbs r)+ apply (fastforce simp: is_etcb_at_def elim!: obj_at_weakenE dest: bspec[OF tables]) apply (subst(asm) eq_commute, assumption) apply (clarsimp simp: projectKOs obj_at'_def objBits_simps) apply (subst map_to_ctes_upd_tcb, assumption+) apply (simp add: ps_clear_def3 field_simps objBits_defs mask_def) apply (subst if_not_P) apply (fastforce dest: bspec [OF tables', OF ranI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_thread_all add tcbu etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s; ko_at' tcb' add s'\<rbrakk> \<Longrightarrow> tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu'
 2. tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_thread_all add tcbu etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); kheap s add = Some (TCB tcb); ekheap s add = Some etcb; ksPSpace s' add = Some ko; ekheap_relation (ekheap s) (ksPSpace s'); is_aligned add (objBitsKO ko); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); fst (projectKO ko s') = {(tcb', s')}; ps_clear add (objBitsKO ko) s'; ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu'
 2. tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_thread_all add tcbu etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); kheap s add = Some (TCB tcb); ekheap s add = Some etcb; ksPSpace s' add = Some ko; ekheap_relation (ekheap s) (ksPSpace s'); is_aligned add (objBitsKO ko); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); fst (projectKO ko s') = {(tcb', s')}; ps_clear add (objBitsKO ko) s'; ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; \<forall>(x', P)\<in>obj_relation_cuts (TCB tcb) add. \<exists>z. ksPSpace s' x' = Some z \<and> P (TCB tcb) z\<rbrakk> \<Longrightarrow> tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu'
 2. tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_thread_all add tcbu etcbu) (setObject add tcbu') proof (prove)
goal (1 subgoal):
 1. tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_thread_all add tcbu etcbu) (setObject add tcbu') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_thread_all add tcbu etcbu) (setObject add tcbu') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> corres r ?Q40 ?Q'40 (set_thread_all add tcbu etcbu) (setObject add tcbu')
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> ?Q40 s
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> ?Q'40 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> corres ?r'44 ?Q40 ?Q'40 (set_thread_all add tcbu etcbu) (setObject add tcbu')
 2. \<And>x y. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ?r'44 x y\<rbrakk> \<Longrightarrow> r x y
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> ?Q40 s
 4. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> ?Q'40 s proof (prove)
goal (10 subgoals):
 1. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> updateObject tcbu' = updateObject_default tcbu'
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s
 3. \<And>ko. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 4. \<And>v. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 5. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> etcb_relation etcbu ?tcb'47
 6. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> injectKOS tcbu' = KOTCB ?tcb'47
 7. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKOS tcbu')
 8. \<And>x y. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (obj_at (same_caps (TCB tcbu)) add and is_etcb_at add) s
 10. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s proof (prove)
goal (10 subgoals):
 1. \<And>x xa xb xc xd. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> updateObject tcbu' x xa xb xc xd = updateObject_default tcbu' x xa xb xc xd
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s
 3. \<And>ko. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 4. \<And>v. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 5. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> etcb_relation etcbu ?tcb'47
 6. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> injectKOS tcbu' = KOTCB ?tcb'47
 7. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKOS tcbu')
 8. \<And>x y. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (obj_at (same_caps (TCB tcbu)) add and is_etcb_at add) s
 10. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s
 2. \<And>ko. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 3. \<And>v. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 4. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> etcb_relation etcbu ?tcb'47
 5. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> injectKOS tcbu' = KOTCB ?tcb'47
 6. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKOS tcbu')
 7. \<And>x y. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 8. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (obj_at (same_caps (TCB tcbu)) add and is_etcb_at add) s
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s proof (prove)
goal (9 subgoals):
 1. \<And>ko. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 2. \<And>v. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> etcb_relation etcbu ?tcb'47
 4. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> injectKOS tcbu' = KOTCB ?tcb'47
 5. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKOS tcbu')
 6. \<And>x y. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 7. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (obj_at (same_caps (TCB tcbu)) add and is_etcb_at add) s
 8. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at (TCB tcb) add s \<and> ekheap s add = Some etcb\<rbrakk> \<Longrightarrow> obj_at (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, t) \<Rightarrow> getF tcb' = getF tcbu)) add s \<and> is_etcb_at add s
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKOS tcbu')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> {add + 1..add + mask tcbBlockSizeBits} \<inter> dom (ksPSpace s) = {}
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<lambda>x. if \<exists>getF setF. tcb_cte_cases (x - add) = Some (getF, setF) \<and> getF tcbu' \<noteq> getF tcb' then case tcb_cte_cases (x - add) of Some (getF, setF) \<Rightarrow> Some (getF tcbu') else ctes_of s x) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<lambda>x. if \<exists>getF setF. tcb_cte_cases (x - add) = Some (getF, setF) \<and> getF tcbu' \<noteq> getF tcb' then case tcb_cte_cases (x - add) of Some (getF, setF) \<Rightarrow> Some (getF tcbu') else ctes_of s x) = ctes_of s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<nexists>getF setF. tcb_cte_cases (x - add) = Some (getF, setF) \<and> getF tcbu' \<noteq> getF tcb'
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ctes_of s = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; etcb_relation etcbu tcbu'; ksPSpace s add = Some (KOTCB tcb'); is_aligned add tcbBlockSizeBits; ps_clear add tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ctes_of s = ctes_of s proof (prove)
goal:
No subgoals!