theory CSpace_R

lemma cteInsert_invs:
 "\<lbrace>invs' and cte_wp_at' (\<lambda>c. cteCap c=NullCap) dest and valid_cap' cap and
  (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)
  and cte_wp_at' (untyped_derived_eq cap o cteCap) src
  and ex_cte_cap_to' dest and (\<lambda>s. \<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def valid_pspace'_def) apply (wpsimp wp: cur_tcb_lift tcb_in_cur_domain'_lift sch_act_wf_lift CSpace_R.valid_queues_lift
                    valid_irq_node_lift valid_queues_lift' irqs_masked_lift cteInsert_norq
              simp: st_tcb_at'_def) apply (auto simp: invs'_def valid_state'_def valid_pspace'_def elim: valid_capAligned) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s) and cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src and ex_cte_cap_wp_to' (\<lambda>_. True) dest and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s) and cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src and ex_cte_cap_wp_to' (\<lambda>_. True) dest and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. (\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s; valid_cap' cap s; src \<noteq> dest; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s\<rbrakk> \<Longrightarrow> capAligned cap proof (prove)
goal:
No subgoals!