theory Finalise_R

lemma invs_asid_update_strg':
  "invs' s \<and> tab = armKSASIDTable (ksArchState s) \<longrightarrow>
   invs' (s\<lparr>ksArchState := armKSASIDTable_update
            (\<lambda>_. tab (asid := None)) (ksArchState s)\<rparr>)" apply (simp add: invs'_def) apply (simp add: valid_state'_def) apply (simp add: valid_global_refs'_def global_refs'_def valid_arch_state'_def valid_asid_table'_def valid_machine_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) apply (auto simp add: ran_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<and> tab = armKSASIDTable (ksArchState s) \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. tab(asid := None)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. valid_state' s \<and> cur_tcb' s \<and> tab = armKSASIDTable (ksArchState s) \<longrightarrow> valid_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid := None)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. valid_pspace' 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> tab = armKSASIDTable (ksArchState s) \<longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid := None)) (ksArchState s)\<rparr>) \<and> valid_arch_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid := None)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid := None)) (ksArchState s)\<rparr>) \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. valid_pspace' 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_refs' kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> (\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0) \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) 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> tab = armKSASIDTable (ksArchState s) \<longrightarrow> dom (\<lambda>a. if a = asid then None else armKSASIDTable (ksArchState s) a) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (\<lambda>a. if a = asid then None else armKSASIDTable (ksArchState s) a) \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] proof (prove)
goal:
No subgoals!