theory Arch_R

lemma ensureSafeMapping_valid_slots_duplicated':
  "\<lbrace>\<lambda>s. slots_duplicated_ensured entries s\<rbrace>
  ensureSafeMapping entries
  \<lbrace>\<lambda>rv s. valid_slots_duplicated' entries s\<rbrace>,-" apply (simp add:ensureSafeMapping_def) apply (case_tac entries) apply (case_tac a) apply (case_tac aa) apply (rule hoare_pre) apply (simp add:slots_duplicated_ensured_def | wp)+ apply (rule hoare_pre) apply (wp mapME_x_inv_wp getPTE_wp| wpc)+ apply clarsimp apply (clarsimp simp:valid_slots_duplicated'_def) apply (simp add:slots_duplicated_ensured_def) apply (rule hoare_pre) apply (rule_tac P = "\<exists>p. b = [p]" and
      P' = "\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s" in hoare_gen_asmE) apply (clarsimp simp:mapME_singleton) apply (wp getPTE_wp|wpc)+ apply (clarsimp simp:valid_slots_duplicated'_def obj_at'_real_def split:option.splits) apply (intro impI conjI) apply (erule ko_wp_at'_weakenE) apply (simp add:projectKO_opt_pte vs_entry_align_def
       split:Structures_H.kernel_object.splits
       arch_kernel_object.splits) apply (erule ko_wp_at'_weakenE) apply (simp add:projectKO_opt_pte vs_entry_align_def
      split:Structures_H.kernel_object.splits
      arch_kernel_object.splits) apply clarsimp apply (case_tac b) apply (case_tac a) apply (rule hoare_pre) apply (simp add:slots_duplicated_ensured_def | wp)+ apply (rule hoare_pre) apply (rule_tac P = "\<exists>p. ba = [p]" and
      P' = "\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s" in hoare_gen_asmE) apply (clarsimp simp:mapME_singleton) apply (wp getPDE_wp|wpc)+ apply (clarsimp simp:valid_slots_duplicated'_def obj_at'_real_def split:option.splits) apply (intro impI conjI) apply (erule ko_wp_at'_weakenE) apply (simp add:projectKO_opt_pde vs_entry_align_def
       split:Structures_H.kernel_object.splits
       arch_kernel_object.splits) apply (erule ko_wp_at'_weakenE) apply (simp add:projectKO_opt_pde vs_entry_align_def
      split:Structures_H.kernel_object.splits
      arch_kernel_object.splits) apply clarsimp apply (simp add:slots_duplicated_ensured_def) apply (rule hoare_pre) apply (wp mapME_x_inv_wp getPDE_wp| wpc)+ apply clarsimp apply (fastforce simp:valid_slots_duplicated'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>slots_duplicated_ensured entries\<rbrace> ensureSafeMapping entries \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a. entries = Inl a \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>entries = Inl a; a = (aa, b)\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>a aa b. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 3. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 4. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>?P'3 a aa b\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>a aa b s. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.InvalidPTE; slots_duplicated_ensured entries s\<rbrakk> \<Longrightarrow> ?P'3 a aa b s
 3. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 4. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 5. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>entries = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>x xa xb xc xd. returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) b \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b))\<rbrace>, -
 2. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>entries = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 a aa b x21 x22 x23 x24 x25\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>x xa xb xc xd. returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) b \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b))\<rbrace>, -
 2. \<And>a aa b x21 x22 x23 x24 x25 s. \<lbrakk>entries = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25; \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ?P'9 a aa b x21 x22 x23 x24 x25 s
 3. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 4. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>a aa b x21 x22 x23 x24 x25 x s. \<lbrakk>entries = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25; valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)) s\<rbrakk> \<Longrightarrow> \<forall>ko. ko_at' ko x s \<longrightarrow> True \<and> (ko = ARM_H.InvalidPTE \<longrightarrow> valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)) s) \<and> (\<forall>x xa xb xc xd. ko = ARM_H.LargePagePTE x xa xb xc xd \<longrightarrow> valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)) s) \<and> (\<forall>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd \<longrightarrow> True)
 2. \<And>a aa b x21 x22 x23 x24 x25 s. \<lbrakk>entries = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25; \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)) s
 3. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 4. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x21 x22 x23 x24 x25 s. \<lbrakk>entries = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25; \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> valid_slots_duplicated' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)) s
 2. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd. returnOk ())) b \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b))\<rbrace>, -
 2. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>?P'62 a aa b x31 x32 x33 x34 x35\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd. returnOk ())) b \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b))\<rbrace>, -
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ?P'62 a aa b x31 x32 x33 x34 x35 s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd. returnOk ())) b \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b))\<rbrace>, -
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p. entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]) \<Longrightarrow> \<lbrace>page_table_at' (p && ~~ mask ptBits)\<rbrace> liftE (getObject p) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd. returnOk ()) \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]))\<rbrace>, -
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> True \<and> (\<forall>ko. ko_at' ko p s \<longrightarrow> (ko = ARM_H.InvalidPTE \<longrightarrow> valid_slots_duplicated' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p])) s) \<and> (\<forall>x xa xb xc xd. ko = ARM_H.LargePagePTE x xa xb xc xd \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd \<longrightarrow> valid_slots_duplicated' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p])) s))
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p s ko. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s\<rbrakk> \<Longrightarrow> (ko = ARM_H.InvalidPTE \<longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s) \<and> ((\<exists>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd) \<longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s)
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p s ko. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; ko = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 2. \<And>x31 x32 x33 x34 x35 p s ko. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; \<exists>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 3. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 4. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p s ko koa. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; ko = ARM_H.InvalidPTE; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0
 2. \<And>x31 x32 x33 x34 x35 p s ko. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; \<exists>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 3. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 4. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p s ko. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; \<exists>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 p s ko koa. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p]); page_table_at' (p && ~~ mask ptBits) s; \<exists>x xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0
 2. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 3. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a aa b x31 x32 x33 x34 x35 s. \<lbrakk>entries = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35; \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. b = [p] \<and> page_table_at' (p && ~~ mask ptBits) s) and K (\<exists>p. b = [p])) s
 2. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>b. entries = Inr b \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>entries = Inr b; b = (a, ba)\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>b a ba x21 x22 x23. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 3. \<And>b a ba x31 x32 x33 x34 x35 x36 x37. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 4. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>b a ba. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<lbrace>?P'301 b a ba\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 2. \<And>b a ba s. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.InvalidPDE; slots_duplicated_ensured entries s\<rbrakk> \<Longrightarrow> ?P'301 b a ba s
 3. \<And>b a ba x21 x22 x23. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 4. \<And>b a ba x31 x32 x33 x34 x35 x36 x37. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, -
 5. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x31 x32 x33 x34 x35 x36 x37. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe xf. returnOk ()) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) ba \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba))\<rbrace>, -
 2. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>b a ba x31 x32 x33 x34 x35 x36 x37. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>?P'312 b a ba x31 x32 x33 x34 x35 x36 x37\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe xf. returnOk ()) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) ba \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba))\<rbrace>, -
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ?P'312 b a ba x31 x32 x33 x34 x35 x36 x37 s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>b a ba x31 x32 x33 x34 x35 x36 x37. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe xf. returnOk ()) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) ba \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba))\<rbrace>, -
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p. entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]) \<Longrightarrow> \<lbrace>page_directory_at' (p && ~~ mask pdBits)\<rbrace> liftE (getObject p) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe xf. returnOk ()) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst) \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]))\<rbrace>, -
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> True \<and> (\<forall>ko. ko_at' ko p s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> valid_slots_duplicated' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p])) s) \<and> (\<forall>x xa xb. ko = ARM_H.PageTablePDE x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> valid_slots_duplicated' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p])) s) \<and> (\<forall>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> True))
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s\<rbrakk> \<Longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s) \<and> ((\<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf) \<longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s)
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; ko = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 2. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; \<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 3. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 4. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko koa. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; ko = ARM_H.InvalidPDE; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0
 2. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; \<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 3. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 4. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) p s; \<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 p s ko koa. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p]); page_directory_at' (p && ~~ mask pdBits) s; \<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0
 2. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 3. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>entries = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37; \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>p. ba = [p] \<and> page_directory_at' (p && ~~ mask pdBits) s) and K (\<exists>p. ba = [p])) s
 2. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>slots_duplicated_ensured entries\<rbrace> case entries of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. valid_slots_duplicated' entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> is_aligned p 6\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe. returnOk ())) ba \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>entries = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>?P'579 b a ba x41 x42 x43 x44 x45 x46\<rbrace> mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe. returnOk ())) ba \<lbrace>\<lambda>rv. valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba))\<rbrace>, -
 2. \<And>b a ba x41 x42 x43 x44 x45 x46 s. \<lbrakk>entries = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; \<exists>p. ba = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> is_aligned p 6\<rbrakk> \<Longrightarrow> ?P'579 b a ba x41 x42 x43 x44 x45 x46 s proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x41 x42 x43 x44 x45 x46 x s. \<lbrakk>entries = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba)) s\<rbrakk> \<Longrightarrow> \<forall>ko. ko_at' ko x s \<longrightarrow> True \<and> (ko = ARM_H.InvalidPDE \<longrightarrow> valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba)) s) \<and> (\<forall>x xa xb. ko = ARM_H.PageTablePDE x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba)) s)
 2. \<And>b a ba x41 x42 x43 x44 x45 x46 s. \<lbrakk>entries = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; \<exists>p. ba = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> is_aligned p 6\<rbrakk> \<Longrightarrow> valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba)) s proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x41 x42 x43 x44 x45 x46 s. \<lbrakk>entries = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; \<exists>p. ba = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> is_aligned p 6\<rbrakk> \<Longrightarrow> valid_slots_duplicated' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba)) s proof (prove)
goal:
No subgoals!