theory TcbAcc_R

lemma set_eobject_corres:
  assumes tcbs: "non_exst_same tcb' tcbu'"
  assumes e: "etcb_relation etcb tcb' \<Longrightarrow> etcb_relation etcbu tcbu'"
  assumes tables': "\<forall>(getF, v) \<in> ran tcb_cte_cases. getF tcbu' = getF tcb'"
  assumes r: "r () ()"
  shows "corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb))
                  (ko_at' tcb' add)
                  (set_eobject add etcbu) (setObject add tcbu')" apply (rule_tac F="non_exst_same tcb' tcbu' \<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 (clarsimp simp: projectKOs other_obj_relation_def ekheap_relation_def e tcbs) apply (drule bspec, erule domI) apply (clarsimp simp: e) apply (erule conjE) apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (rule set_eobject_corres'[where P="(=) tcb'"]) apply simp defer apply (simp add: r) apply (fastforce simp: is_etcb_at_def elim!: obj_at_weakenE) apply (subst(asm) eq_commute) apply (clarsimp simp: obj_at'_def) 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 (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s; ko_at' tcb' add s'\<rbrakk> \<Longrightarrow> non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu'
 2. non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko koa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap s add = Some etcb; ksPSpace s' add = Some ko; ekheap_relation (ekheap s) (ksPSpace s'); kheap s add = Some koa; is_tcb koa; 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> non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu'
 2. non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko koa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap s add = Some etcb; ksPSpace s' add = Some ko; ekheap_relation (ekheap s) (ksPSpace s'); kheap s add = Some koa; is_tcb koa; 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 koa add. \<exists>z. ksPSpace s' x' = Some z \<and> P koa z\<rbrakk> \<Longrightarrow> non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu'
 2. non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' koa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap s add = Some etcb; ksPSpace s' add = Some (KOTCB tcb'); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; kheap s add = Some koa; is_tcb koa; is_aligned add (objBitsKO (KOTCB tcb')); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ps_clear add (objBitsKO (KOTCB tcb')) 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\<in>obj_relation_cuts koa add. case x of (x', P) \<Rightarrow> \<exists>z. ksPSpace s' x' = Some z \<and> P koa z\<rbrakk> \<Longrightarrow> etcb_relation etcbu tcbu'
 2. non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (2 subgoals):
 1. \<And>s s' koa. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap s add = Some etcb; ksPSpace s' add = Some (KOTCB tcb'); kheap s add = Some koa; is_tcb koa; is_aligned add (objBitsKO (KOTCB tcb')); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ps_clear add (objBitsKO (KOTCB tcb')) 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\<in>obj_relation_cuts koa add. case x of (x', P) \<Rightarrow> \<exists>z. ksPSpace s' x' = Some z \<and> P koa z; \<exists>tcb'. ksPSpace s' add = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s add)) tcb'\<rbrakk> \<Longrightarrow> etcb_relation etcbu tcbu'
 2. non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (1 subgoal):
 1. non_exst_same tcb' tcbu' \<and> etcb_relation etcbu tcbu' \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> corres r (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) (ko_at' tcb' add) (set_eobject add etcbu) (setObject add tcbu') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> corres r ?Q39 ?Q'39 (set_eobject add etcbu) (setObject add tcbu')
 2. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> ?Q39 s
 3. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> ?Q'39 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> corres ?r'43 ?Q39 ?Q'39 (set_eobject add etcbu) (setObject add tcbu')
 2. \<And>x y. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ?r'43 x y\<rbrakk> \<Longrightarrow> r x y
 3. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> ?Q39 s
 4. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> ?Q'39 s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'\<rbrakk> \<Longrightarrow> etcb_relation etcbu tcbu'
 2. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s
 3. \<And>x y. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 4. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (tcb_at add and is_etcb_at add) s
 5. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>ko. non_exst_same ko tcbu') add and obj_at' ((=) tcb') add) s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s
 2. \<And>x y. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 3. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (tcb_at add and is_etcb_at add) s
 4. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>ko. non_exst_same ko tcbu') add and obj_at' ((=) tcb') add) s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; dc x y\<rbrakk> \<Longrightarrow> r x y
 2. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (tcb_at add and is_etcb_at add) s
 3. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>ko. non_exst_same ko tcbu') add and obj_at' ((=) tcb') add) s
 4. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; (tcb_at add and (\<lambda>s. ekheap s add = Some etcb)) s\<rbrakk> \<Longrightarrow> (tcb_at add and is_etcb_at add) s
 2. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>ko. non_exst_same ko tcbu') add and obj_at' ((=) tcb') add) s
 3. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; ko_at' tcb' add s\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>ko. non_exst_same ko tcbu') add and obj_at' ((=) tcb') add) s
 2. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>ko. non_exst_same ko tcbu') add and obj_at' ((=) tcb') add) s
 2. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; etcb_relation etcbu tcbu'; obj_at' ((=) tcb') add s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(add \<mapsto> KOTCB tcbu')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>non_exst_same tcb' tcbu'; 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>non_exst_same tcb' tcbu'; 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>non_exst_same tcb' tcbu'; 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>non_exst_same tcb' tcbu'; 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>non_exst_same tcb' tcbu'; 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>non_exst_same tcb' tcbu'; 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>non_exst_same tcb' tcbu'; 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!