theory TcbAcc_R

lemma setObject_update_TCB_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 exst: "exst_same tcb' tcbu'"
  shows "corres r (ko_at (TCB tcb) add)
                  (ko_at' tcb' add)
                  (set_object add (TCB tcbu)) (setObject add tcbu')" apply (rule_tac F="tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'" in corres_req) apply (clarsimp simp: state_relation_def obj_at_def obj_at'_def) apply (frule(1) pspace_relation_absD) apply (clarsimp simp: projectKOs other_obj_relation_def exst) apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (rule setObject_other_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 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) (ko_at' tcb' add) (set_object add (TCB tcbu)) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; ko_at (TCB tcb) add s; ko_at' tcb' add s'\<rbrakk> \<Longrightarrow> tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'
 2. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add) (ko_at' tcb' add) (set_object add (TCB tcbu)) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. \<lbrakk>kheap s add = Some (TCB tcb); pspace_relation (kheap s) (ksPSpace s'); 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> exst_same tcb' tcbu'
 2. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add) (ko_at' tcb' add) (set_object add (TCB tcbu)) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. \<lbrakk>kheap s add = Some (TCB tcb); pspace_relation (kheap s) (ksPSpace s'); 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> exst_same tcb' tcbu'
 2. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add) (ko_at' tcb' add) (set_object add (TCB tcbu)) (setObject add tcbu') proof (prove)
goal (1 subgoal):
 1. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> corres r (ko_at (TCB tcb) add) (ko_at' tcb' add) (set_object add (TCB tcbu)) (setObject add tcbu') proof (prove)
goal (3 subgoals):
 1. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> corres r ?Q27 ?Q'27 (set_object add (TCB tcbu)) (setObject add tcbu')
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> ?Q27 s
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> ?Q'27 s proof (prove)
goal (4 subgoals):
 1. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> corres ?r'31 ?Q27 ?Q'27 (set_object add (TCB tcbu)) (setObject add tcbu')
 2. \<And>x y. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ?r'31 x y\<rbrakk> \<Longrightarrow> r x y
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> ?Q27 s
 4. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> ?Q'27 s proof (prove)
goal (10 subgoals):
 1. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> updateObject tcbu' = updateObject_default tcbu'
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s
 3. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> is_other_obj_relation_type (a_type (TCB tcbu))
 4. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 5. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> exst_same' (injectKO ko) (injectKO tcbu')
 6. \<And>v. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> 1 < 2 ^ objBits v
 7. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKO tcbu')
 8. \<And>x y. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> (typ_at (a_type (TCB tcbu)) add and obj_at (same_caps (TCB tcbu)) add) s
 10. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' 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. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> updateObject tcbu' x xa xb xc xd = updateObject_default tcbu' x xa xb xc xd
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s
 3. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> is_other_obj_relation_type (a_type (TCB tcbu))
 4. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 5. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> exst_same' (injectKO ko) (injectKO tcbu')
 6. \<And>v. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> 1 < 2 ^ objBits v
 7. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKO tcbu')
 8. \<And>x y. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> (typ_at (a_type (TCB tcbu)) add and obj_at (same_caps (TCB tcbu)) add) s
 10. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' 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' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s
 2. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> is_other_obj_relation_type (a_type (TCB tcbu))
 3. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 4. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> exst_same' (injectKO ko) (injectKO tcbu')
 5. \<And>v. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> 1 < 2 ^ objBits v
 6. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKO tcbu')
 7. \<And>x y. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 8. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> (typ_at (a_type (TCB tcbu)) add and obj_at (same_caps (TCB tcbu)) add) s
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s proof (prove)
goal (9 subgoals):
 1. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> is_other_obj_relation_type (a_type (TCB tcbu))
 2. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> objBits ko = objBits tcbu'
 3. \<And>ko. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; tcb' = ko\<rbrakk> \<Longrightarrow> exst_same' (injectKO ko) (injectKO tcbu')
 4. \<And>v. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> 1 < 2 ^ objBits v
 5. tcb_relation tcb tcb' \<and> exst_same tcb' tcbu' \<Longrightarrow> other_obj_relation (TCB tcbu) (injectKO tcbu')
 6. \<And>x y. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 7. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> (typ_at (a_type (TCB tcbu)) add and obj_at (same_caps (TCB tcbu)) add) s
 8. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s
 9. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at (TCB tcb) add s\<rbrakk> \<Longrightarrow> typ_at ATCB add s \<and> 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
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> obj_at' ((=) tcb') add s
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<and> exst_same tcb' tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> injectKO tcbu')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb'; exst_same tcb' 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'; exst_same tcb' 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'; exst_same tcb' 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'; exst_same tcb' 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'; exst_same tcb' 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'; exst_same tcb' 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'; exst_same tcb' 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!