theory CSpace1_R

lemma set_cap_not_quite_corres:
  assumes cr:
  "pspace_relations (ekheap s) (kheap s) (ksPSpace 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'"
  "(x,t') \<in> fst (updateCap p' c' s')"
  "valid_objs s" "pspace_aligned s" "pspace_distinct s" "cte_at p s"
  "pspace_aligned' s'" "pspace_distinct' s'"
  "interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s')"
  "(arch_state s, ksArchState s') \<in> arch_state_relation"
  assumes c: "cap_relation c c'"
  assumes p: "p' = cte_map p"
  shows "\<exists>t. ((),t) \<in> fst (set_cap c p s) \<and>
             pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and>
             cdt t = cdt s \<and>
             cdt_list t = cdt_list s \<and>
             ekheap t = ekheap s \<and>
             scheduler_action t = scheduler_action s \<and>
             ready_queues t = ready_queues s \<and>
             is_original_cap t = is_original_cap s \<and>
             interrupt_state_relation (interrupt_irq_node t) (interrupt_states t)
                              (ksInterruptState t') \<and>
             (arch_state t, ksArchState t') \<in> arch_state_relation \<and>
             cur_thread t = ksCurThread t' \<and>
             idle_thread t = ksIdleThread t' \<and>
             machine_state t = ksMachineState t' \<and>
             work_units_completed t = ksWorkUnitsCompleted t' \<and>
             domain_index t = ksDomScheduleIdx t' \<and>
             domain_list t = ksDomSchedule t' \<and>
             cur_domain t = ksCurDomain t' \<and>
             domain_time t = ksDomainTime t'" using cr apply (clarsimp simp: updateCap_def in_monad) apply (drule use_valid [OF _ getCTE_sp[where P="\<lambda>s. s2 = s" for s2], OF _ refl]) apply clarsimp apply (drule(7) set_cap_not_quite_corres_prequel) apply simp apply (rule c) apply (rule p) apply (erule exEI) apply clarsimp apply (frule setCTE_pspace_only) apply (clarsimp simp: set_cap_def split_def in_monad set_object_def
                        get_object_def
                 split: Structures_A.kernel_object.split_asm if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
using this:
pspace_relations (ekheap s) (kheap s) (ksPSpace 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'
(x, t') \<in> fst (updateCap p' c' s')
valid_objs s
pspace_aligned s
pspace_distinct s
cte_wp_at (\<lambda>_. True) p s
pspace_aligned' s'
pspace_distinct' s'
interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s')
(arch_state s, ksArchState s') \<in> arch_state_relation

goal (1 subgoal):
 1. \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>s'' cte. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace 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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; (cte, s'') \<in> fst (getCTE p' s'); ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'')\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>s'' cte. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace 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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s''); (cte_wp_at' (\<lambda>c. c = cte) p' and (=) s') s''\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace 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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'\<rbrakk> \<Longrightarrow> cap_relation (?c23 cte) (cteCap (cteCap_update (\<lambda>_. c') cte))
 2. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'\<rbrakk> \<Longrightarrow> p' = cte_map p
 3. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; \<exists>t. ((), t) \<in> fst (set_cap (?c23 cte) p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t')\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'\<rbrakk> \<Longrightarrow> cap_relation (?c23 cte) c'
 2. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'\<rbrakk> \<Longrightarrow> p' = cte_map p
 3. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; \<exists>t. ((), t) \<in> fst (set_cap (?c23 cte) p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t')\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'\<rbrakk> \<Longrightarrow> p' = cte_map p
 2. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t')\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t')\<rbrakk> \<Longrightarrow> \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; ((), x) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap x) (kheap x) (ksPSpace t')\<rbrakk> \<Longrightarrow> ((), x) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap x) (kheap x) (ksPSpace t') \<and> cdt x = cdt s \<and> cdt_list x = cdt_list s \<and> ekheap x = ekheap s \<and> scheduler_action x = scheduler_action s \<and> ready_queues x = ready_queues s \<and> is_original_cap x = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node x) (interrupt_states x) (ksInterruptState t') \<and> (arch_state x, ksArchState t') \<in> arch_state_relation \<and> cur_thread x = ksCurThread t' \<and> idle_thread x = ksIdleThread t' \<and> machine_state x = ksMachineState t' \<and> work_units_completed x = ksWorkUnitsCompleted t' \<and> domain_index x = ksDomScheduleIdx t' \<and> domain_list x = ksDomSchedule t' \<and> cur_domain x = ksCurDomain t' \<and> domain_time x = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; ((), x) \<in> fst (set_cap c p s); pspace_relations (ekheap x) (kheap x) (ksPSpace t')\<rbrakk> \<Longrightarrow> cdt x = cdt s \<and> cdt_list x = cdt_list s \<and> ekheap x = ekheap s \<and> scheduler_action x = scheduler_action s \<and> ready_queues x = ready_queues s \<and> is_original_cap x = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node x) (interrupt_states x) (ksInterruptState t') \<and> (arch_state x, ksArchState t') \<in> arch_state_relation \<and> cur_thread x = ksCurThread t' \<and> idle_thread x = ksIdleThread t' \<and> machine_state x = ksMachineState t' \<and> work_units_completed x = ksWorkUnitsCompleted t' \<and> domain_index x = ksDomScheduleIdx t' \<and> domain_list x = ksDomSchedule t' \<and> cur_domain x = ksCurDomain t' \<and> domain_time x = ksDomainTime t' proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>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'; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) p s; pspace_aligned' s'; pspace_distinct' s'; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); (arch_state s, ksArchState s') \<in> arch_state_relation; ((), t') \<in> fst (setCTE p' (cteCap_update (\<lambda>_. c') cte) s'); cte_wp_at' (\<lambda>c. c = cte) p' s'; ((), x) \<in> fst (set_cap c p s); pspace_relations (ekheap x) (kheap x) (ksPSpace t'); \<exists>ps'. t' = s'\<lparr>ksPSpace := ps'\<rparr>\<rbrakk> \<Longrightarrow> cdt x = cdt s \<and> cdt_list x = cdt_list s \<and> ekheap x = ekheap s \<and> scheduler_action x = scheduler_action s \<and> ready_queues x = ready_queues s \<and> is_original_cap x = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node x) (interrupt_states x) (ksInterruptState t') \<and> (arch_state x, ksArchState t') \<in> arch_state_relation \<and> cur_thread x = ksCurThread t' \<and> idle_thread x = ksIdleThread t' \<and> machine_state x = ksMachineState t' \<and> work_units_completed x = ksWorkUnitsCompleted t' \<and> domain_index x = ksDomScheduleIdx t' \<and> domain_list x = ksDomSchedule t' \<and> cur_domain x = ksCurDomain t' \<and> domain_time x = ksDomainTime t' proof (prove)
goal:
No subgoals!