theory Arch_R

lemma sts_valid_arch_inv':
  "\<lbrace>valid_arch_inv' ai\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_arch_inv' ai\<rbrace>" apply (cases ai, simp_all add: valid_arch_inv'_def) apply (clarsimp simp: valid_pti'_def split: page_table_invocation.splits) apply (intro allI conjI impI) apply (wp | simp)+ apply (rename_tac page_invocation) apply (case_tac page_invocation, simp_all add: valid_page_inv'_def)[1] apply (wp valid_slots_lift' valid_slots_duplicated_lift'|simp)+ apply (clarsimp simp: valid_aci'_def split: asidcontrol_invocation.splits) apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule hoare_pre, wp) apply clarsimp apply (clarsimp simp: valid_apinv'_def split: asidpool_invocation.splits) apply (rule hoare_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_inv' ai\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_arch_inv' ai\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = invocation.InvokePageTable x1 \<Longrightarrow> \<lbrace>valid_pti' x1\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_pti' x1\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv' x3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_page_inv' x3\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = invocation.InvokePageTable x1 \<Longrightarrow> (\<forall>x11 x12. x1 = ARM_H.PageTableUnmap x11 x12 \<longrightarrow> \<lbrace>cte_wp_at' (is_arch_update' (capability.ArchObjectCap x11)) x12 and valid_cap' (capability.ArchObjectCap x11) and (\<lambda>y. isPageTableCap x11)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (is_arch_update' (capability.ArchObjectCap x11)) x12 and valid_cap' (capability.ArchObjectCap x11) and (\<lambda>y. isPageTableCap x11)\<rbrace>) \<and> (\<forall>x21 x22 x23 x24. x1 = ARM_H.PageTableMap x21 x22 x23 x24 \<longrightarrow> \<lbrace>cte_wp_at' (is_arch_update' x21) x22 and ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x24 and valid_cap' x21 and valid_pde' x23 and (\<lambda>y. valid_pde_mapping' (x24 && mask pdBits) x23 \<and> vs_entry_align (KOArch (KOPDE x23)) = 0)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (is_arch_update' x21) x22 and ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x24 and valid_cap' x21 and valid_pde' x23 and (\<lambda>y. valid_pde_mapping' (x24 && mask pdBits) x23 \<and> vs_entry_align (KOArch (KOPDE x23)) = 0)\<rbrace>)
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv' x3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_page_inv' x3\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1 x11 x12. \<lbrakk>ai = invocation.InvokePageTable x1; x1 = ARM_H.PageTableUnmap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (is_arch_update' (capability.ArchObjectCap x11)) x12 and valid_cap' (capability.ArchObjectCap x11) and (\<lambda>y. isPageTableCap x11)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (is_arch_update' (capability.ArchObjectCap x11)) x12 and valid_cap' (capability.ArchObjectCap x11) and (\<lambda>y. isPageTableCap x11)\<rbrace>
 2. \<And>x1 x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable x1; x1 = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (is_arch_update' x21) x22 and ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x24 and valid_cap' x21 and valid_pde' x23 and (\<lambda>y. valid_pde_mapping' (x24 && mask pdBits) x23 \<and> vs_entry_align (KOArch (KOPDE x23)) = 0)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (is_arch_update' x21) x22 and ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x24 and valid_cap' x21 and valid_pde' x23 and (\<lambda>y. valid_pde_mapping' (x24 && mask pdBits) x23 \<and> vs_entry_align (KOArch (KOPDE x23)) = 0)\<rbrace>
 3. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv' x3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_page_inv' x3\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv' x3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_page_inv' x3\<rbrace>
 2. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 3. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>page_invocation. ai = invocation.InvokePage page_invocation \<Longrightarrow> \<lbrace>valid_page_inv' page_invocation\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_page_inv' page_invocation\<rbrace>
 2. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 3. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>page_invocation x1. \<lbrakk>ai = invocation.InvokePage (ARM_H.PageGetAddr x1); page_invocation = ARM_H.PageGetAddr x1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>page_invocation x21 x22 x23 x24 x25 x26. \<lbrakk>ai = invocation.InvokePage (ARM_H.PageFlush x21 x22 x23 x24 x25 x26); page_invocation = ARM_H.PageFlush x21 x22 x23 x24 x25 x26\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>page_invocation x31 x32 x33 x34. \<lbrakk>ai = invocation.InvokePage (ARM_H.PageMap x31 x32 x33 x34); page_invocation = ARM_H.PageMap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (is_arch_update' x32) x33 and valid_slots' x34 and valid_cap' x32 and (\<lambda>y. valid_pde_slots' x34) and valid_slots_duplicated' x34\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (is_arch_update' x32) x33 and valid_slots' x34 and valid_cap' x32 and (\<lambda>y. valid_pde_slots' x34) and valid_slots_duplicated' x34\<rbrace>
 4. \<And>page_invocation x41 x42. \<lbrakk>ai = invocation.InvokePage (ARM_H.PageUnmap x41 x42); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci' x4\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_aci' x4\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4a. ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4a) \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x2 s \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx) x3 s \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4a local.asid_low_bits \<and> x4a < 2 ^ local.asid_bits\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x2 s \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx) x3 s \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4a local.asid_low_bits \<and> x4a < 2 ^ local.asid_bits\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4a. ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4a) \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>cte. ctes_of s x2 = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<exists>cte. ctes_of s x3 = Some cte \<and> (\<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx)) \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4a local.asid_low_bits \<and> x4a < 2 ^ local.asid_bits\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. (\<exists>cte. ctes_of s x2 = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<exists>cte. ctes_of s x3 = Some cte \<and> (\<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx)) \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4a local.asid_low_bits \<and> x4a < 2 ^ local.asid_bits\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4a s. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4a); (\<exists>cte. ctes_of s x2 = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<exists>cte. ctes_of s x3 = Some cte \<and> (\<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx)) \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4a local.asid_low_bits \<and> x4a < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s x2 = Some cte \<and> cteCap cte = capability.NullCap) \<and> (\<exists>cte. ctes_of s x3 = Some cte \<and> (\<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx)) \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4a local.asid_low_bits \<and> x4a < 2 ^ local.asid_bits
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv' x5\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_apinv' x5\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3. ai = invocation.InvokeASIDPool (asidpool_invocation.Assign x1 x2 x3) \<Longrightarrow> \<lbrace>asid_pool_at' x2 and cte_wp_at' (isPDCap \<circ> cteCap) x3 and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. asid_pool_at' x2 and cte_wp_at' (isPDCap \<circ> cteCap) x3 and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s. \<lbrakk>ai = invocation.InvokeASIDPool (asidpool_invocation.Assign x1 x2 x3); (asid_pool_at' x2 and cte_wp_at' (isPDCap \<circ> cteCap) x3 and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits)) s\<rbrakk> \<Longrightarrow> asid_pool_at' x2 s \<and> cte_wp_at' (isPDCap \<circ> cteCap) x3 s \<and> 0 < x1 \<and> x1 < 2 ^ local.asid_bits proof (prove)
goal:
No subgoals!