theory CSpace_R

lemma arch_update_setCTE_invs:
  "\<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and invs' and valid_cap' cap\<rbrace>
  setCTE p (cteCap_update (\<lambda>_. cap) oldcte)
  \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def valid_pspace'_def) apply (wp arch_update_setCTE_mdb valid_queues_lift sch_act_wf_lift tcb_in_cur_domain'_lift ct_idle_or_in_cur_domain'_lift
             arch_update_setCTE_iflive arch_update_setCTE_ifunsafe
             valid_irq_node_lift setCTE_typ_at' setCTE_irq_handlers'
             valid_queues_lift' setCTE_pred_tcb_at' irqs_masked_lift
             setCTE_norq hoare_vcg_disj_lift untyped_ranges_zero_lift
           | simp add: pred_tcb_at'_def)+ apply (clarsimp simp: valid_global_refs'_def is_arch_update'_def fun_upd_def[symmetric]
                        cte_wp_at_ctes_of isCap_simps untyped_ranges_zero_fun_upd) apply (frule capMaster_eq_capBits_eq) apply (frule capMaster_isUntyped) apply (drule capMaster_capRange) apply (clarsimp simp: valid_refs'_def valid_cap_sizes'_def) apply (subst untyped_ranges_zero_delta[where xs="[p]"], assumption, simp_all) apply (clarsimp simp: ran_restrict_map_insert cteCaps_of_def
                         untypedZeroRange_def Let_def
                         isCap_simps(1-11)[where v="ArchObjectCap ac" for ac]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and invs' and valid_cap' cap\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and ((\<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 valid_cap' cap\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<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. cte_wp_at' (is_arch_update' cap) p s \<and> cte_wp_at' ((=) oldcte) p s \<and> 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' s \<and> valid_cap' cap s \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s \<and> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] \<and> untyped_ranges_zero_inv (\<lambda>a. if a = p then Some cap else cteCaps_of s a) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; capMasterCap (capability.ArchObjectCap v0) = capMasterCap (cteCap oldcte); cap = capability.ArchObjectCap v0; 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_refs' kernel_data_refs (ctes_of s); global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of 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; valid_cap' (capability.ArchObjectCap v0) s\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (capability.ArchObjectCap v0) = {} \<and> 2 ^ acapBits v0 \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(p \<mapsto> capability.ArchObjectCap v0)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; capMasterCap (capability.ArchObjectCap v0) = capMasterCap (cteCap oldcte); cap = capability.ArchObjectCap v0; 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_refs' kernel_data_refs (ctes_of s); global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of 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; valid_cap' (capability.ArchObjectCap v0) s; capBits (capability.ArchObjectCap v0) = capBits (cteCap oldcte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (capability.ArchObjectCap v0) = {} \<and> 2 ^ acapBits v0 \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(p \<mapsto> capability.ArchObjectCap v0)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; capMasterCap (capability.ArchObjectCap v0) = capMasterCap (cteCap oldcte); cap = capability.ArchObjectCap v0; 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_refs' kernel_data_refs (ctes_of s); global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of 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; valid_cap' (capability.ArchObjectCap v0) s; capBits (capability.ArchObjectCap v0) = capBits (cteCap oldcte); isUntypedCap (capability.ArchObjectCap v0) = isUntypedCap (cteCap oldcte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (capability.ArchObjectCap v0) = {} \<and> 2 ^ acapBits v0 \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(p \<mapsto> capability.ArchObjectCap v0)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; cap = capability.ArchObjectCap v0; 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_refs' kernel_data_refs (ctes_of s); global_refs' s \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of 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; valid_cap' (capability.ArchObjectCap v0) s; capBits (capability.ArchObjectCap v0) = capBits (cteCap oldcte); isUntypedCap (capability.ArchObjectCap v0) = isUntypedCap (cteCap oldcte); capRange (capability.ArchObjectCap v0) = capRange (cteCap oldcte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (capability.ArchObjectCap v0) = {} \<and> 2 ^ acapBits v0 \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(p \<mapsto> capability.ArchObjectCap v0)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; cap = capability.ArchObjectCap v0; 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; \<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize 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; valid_cap' (capability.ArchObjectCap v0) s; acapBits v0 = capBits (cteCap oldcte); \<not> isUntypedCap (cteCap oldcte); capRange (capability.ArchObjectCap v0) = capRange (cteCap oldcte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (cteCap oldcte) = {} \<and> 2 ^ capBits (cteCap oldcte) \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(p \<mapsto> capability.ArchObjectCap v0)) (gsUntypedZeroRanges s) proof (prove)
goal (2 subgoals):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; cap = capability.ArchObjectCap v0; 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; \<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize 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; valid_cap' (capability.ArchObjectCap v0) s; acapBits v0 = capBits (cteCap oldcte); \<not> isUntypedCap (cteCap oldcte); capRange (capability.ArchObjectCap v0) = capRange (cteCap oldcte); ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {p}) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {p}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m (cteCaps_of s)(p \<mapsto> capability.ArchObjectCap v0)) |` {p})
 2. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; cap = capability.ArchObjectCap v0; 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; \<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize 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; valid_cap' (capability.ArchObjectCap v0) s; acapBits v0 = capBits (cteCap oldcte); \<not> isUntypedCap (cteCap oldcte); capRange (capability.ArchObjectCap v0) = capRange (cteCap oldcte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (cteCap oldcte) = {} \<and> 2 ^ capBits (cteCap oldcte) \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s v0. \<lbrakk>ctes_of s p = Some oldcte; valid_objs' s; cap = capability.ArchObjectCap v0; 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; \<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize 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; valid_cap' (capability.ArchObjectCap v0) s; acapBits v0 = capBits (cteCap oldcte); \<not> isUntypedCap (cteCap oldcte); capRange (capability.ArchObjectCap v0) = capRange (cteCap oldcte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (cteCap oldcte) = {} \<and> 2 ^ capBits (cteCap oldcte) \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!