theory ArchEmptyFail_AI

lemma arch_decode_ARMASIDPoolAssign_empty_fail:
  "invocation_type label = ArchInvocationLabel ARMASIDPoolAssign
    \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)" apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def
            split: arch_cap.splits cap.splits option.splits | intro impI allI)+ apply (rule empty_fail_bindE) apply simp apply (rule empty_fail_bindE) apply ((simp | wp)+)[1] apply (rule empty_fail_bindE) apply ((simp | wp)+)[1] apply (rule empty_fail_bindE) apply ((simp | wp)+)[1] apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def
                           bind_def return_def returnOk_def lift_def liftE_def select_ext_def
                           gets_def get_def assert_def fail_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invocation_type label = ArchInvocationLabel ARMASIDPoolAssign \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
y <- whenE (asid_table (asid_high_bits_of x12) = None) (throwError (FailedLookup False InvalidRoot));
y <- whenE (x11 \<noteq> the (asid_table (asid_high_bits_of x12))) (throwError (InvalidCapability 0));
pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (liftE (gets (arm_asid_table \<circ> arch_state)))
 2. \<And>x11 x12 rv. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (rv (asid_high_bits_of x12) = None) (throwError (FailedLookup False InvalidRoot));
y <- whenE (x11 \<noteq> the (rv (asid_high_bits_of x12))) (throwError (InvalidCapability 0));
pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 rv. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (rv (asid_high_bits_of x12) = None) (throwError (FailedLookup False InvalidRoot));
y <- whenE (x11 \<noteq> the (rv (asid_high_bits_of x12))) (throwError (InvalidCapability 0));
pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 rv. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (whenE (rv (asid_high_bits_of x12) = None) (throwError (FailedLookup False InvalidRoot)))
 2. \<And>x11 x12 rv rva. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (x11 \<noteq> the (rv (asid_high_bits_of x12))) (throwError (InvalidCapability 0));
pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 rv rva. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (x11 \<noteq> the (rv (asid_high_bits_of x12))) (throwError (InvalidCapability 0));
pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 rv rva. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (whenE (x11 \<noteq> the (rv (asid_high_bits_of x12))) (throwError (InvalidCapability 0)))
 2. \<And>x11 x12 rv rva rvb. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 rv rva rvb. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE pool <- liftE (get_asid_pool x11);
y <- whenE (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select pool x12) (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 rv rva rvb. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (liftE (get_asid_pool x11))
 2. \<And>x11 x12 rv rva rvb rvc. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select rvc x12) (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 rv rva rvb rvc. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
offset <- liftE (select_ext (\<lambda>_. free_asid_pool_select rvc x12) (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}));
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 rv rva rvb rvc. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE offset <- doE y <- whenE (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
liftE (select_ext (\<lambda>_. free_asid_pool_select rvc x12) (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}))
odE;
returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) offset + x12) x11 (snd (f ! 0))))
odE) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 rv rva rvb rvc. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0} = {}) (throwError DeleteFirst);
liftE (select_ext (\<lambda>_. free_asid_pool_select rvc x12) (- dom rvc \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12 \<noteq> 0}))
odE)
 2. \<And>x11 x12 rv rva rvb rvc rvd. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) rvd + x12) x11 (snd (f ! 0))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11_ x12_\<rbrakk> \<Longrightarrow> empty_fail (doE y <- whenE (- dom rvc_ \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12_ \<noteq> 0} = {}) (throwError DeleteFirst);
liftE (select_ext (\<lambda>_. free_asid_pool_select rvc_ x12_) (- dom rvc_ \<inter> {x. UCAST(10 \<rightarrow> 32) x + x12_ \<noteq> 0}))
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 rv rva rvb rvc rvd. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; f \<noteq> []; \<exists>x51. fst (f ! 0) = ArchObjectCap (PageDirectoryCap x51 None); e = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> empty_fail (returnOk (InvokeASIDPool (Assign (UCAST(10 \<rightarrow> 32) rvd + x12) x11 (snd (f ! 0))))) proof (prove)
goal:
No subgoals!