theory Detype_R

lemma cap_table_at_gsCNodes_eq:
  "(s, s') \<in> state_relation
    \<Longrightarrow> (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" apply (clarsimp simp: state_relation_def ghost_relation_def
                        obj_at_def is_cap_table) apply (drule_tac x = ptr in spec)+ apply (drule_tac x = bits in spec)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); \<forall>a sz. (\<exists>dev. kheap s a = Some (ArchObj (DataPage dev sz))) = (gsUserPages s' a = Some sz); \<forall>a n. (\<exists>cs. kheap s a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (gsCNodes s' a = Some n); 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> (gsCNodes s' ptr = Some bits) = (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>cs. ko = CNode bits cs \<and> well_formed_cnode_n bits cs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues 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>sz. (\<exists>dev. kheap s ptr = Some (ArchObj (DataPage dev sz))) = (gsUserPages s' ptr = Some sz); \<forall>n. (\<exists>cs. kheap s ptr = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (gsCNodes s' ptr = Some n)\<rbrakk> \<Longrightarrow> (gsCNodes s' ptr = Some bits) = (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>cs. ko = CNode bits cs \<and> well_formed_cnode_n bits cs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues 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>sz. (\<exists>dev. kheap s ptr = Some (ArchObj (DataPage dev sz))) = (gsUserPages s' ptr = Some sz); (\<exists>cs. kheap s ptr = Some (CNode bits cs) \<and> well_formed_cnode_n bits cs) = (gsCNodes s' ptr = Some bits)\<rbrakk> \<Longrightarrow> (gsCNodes s' ptr = Some bits) = (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>cs. ko = CNode bits cs \<and> well_formed_cnode_n bits cs)) proof (prove)
goal:
No subgoals!