theory ArchArch_IF

lemma get_asid_pool_revrv':
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
     (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') \<top> (get_asid_pool ptr)" unfolding get_asid_pool_def apply (rule_tac W="\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv'" in equiv_valid_rv_bind) apply (rule get_object_revrv') apply (case_tac "aag_can_read aag ptr") apply (simp) apply (case_tac rv) apply (simp | rule fail_ev2_l)+ apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj) apply (simp | rule return_ev2 | rule fail_ev2_l)+ apply (clarsimp simp: equiv_valid_2_def) apply (case_tac rv) apply (clarsimp simp: fail_def)+ apply (case_tac rv') apply (clarsimp simp: fail_def)+ apply (rename_tac arch_kernel_obj arch_kernel_obj') apply (case_tac arch_kernel_obj) apply (case_tac arch_kernel_obj') apply (clarsimp simp: fail_def return_def)+ apply (rule get_object_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (\<lambda>_. True) (get_asid_pool ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (\<lambda>_. True) (do kobj <- get_object ptr;
case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (\<lambda>_. True) (get_object ptr)
 2. \<And>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; aag_can_read aag ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. aag_can_read aag ptr \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q rv) (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv x11 x12. \<lbrakk>aag_can_read aag ptr; rv = CNode x11 x12\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q rv) (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<And>rv x2. \<lbrakk>aag_can_read aag ptr; rv = TCB x2\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q rv) (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<And>rv x3. \<lbrakk>aag_can_read aag ptr; rv = Endpoint x3\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q rv) (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 4. \<And>rv x4. \<lbrakk>aag_can_read aag ptr; rv = Notification x4\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q rv) (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 5. \<And>rv x5. \<lbrakk>aag_can_read aag ptr; rv = ArchObj x5\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q rv) (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 6. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 7. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv x5. \<lbrakk>aag_can_read aag ptr; rv = ArchObj x5\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q (ArchObj x5)) (case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv arch_kernel_obj. \<lbrakk>aag_can_read aag ptr; rv = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q (ArchObj arch_kernel_obj)) (case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv arch_kernel_obj x1. \<lbrakk>aag_can_read aag ptr; rv = ArchObj arch_kernel_obj; arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q (ArchObj arch_kernel_obj)) (case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv arch_kernel_obj x2. \<lbrakk>aag_can_read aag ptr; rv = ArchObj arch_kernel_obj; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q (ArchObj arch_kernel_obj)) (case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail)
 3. \<And>rv arch_kernel_obj x3. \<lbrakk>aag_can_read aag ptr; rv = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q (ArchObj arch_kernel_obj)) (case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail)
 4. \<And>rv arch_kernel_obj x41 x42. \<lbrakk>aag_can_read aag ptr; rv = ArchObj arch_kernel_obj; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q (ArchObj arch_kernel_obj)) (case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail)
 5. \<And>rv rv'. \<lbrakk>aag_can_read aag ptr \<longrightarrow> rv = rv'; pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. aag_can_read aag ptr \<longrightarrow> rv = rv') (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. True) (?Q rv) (?Q rv') (case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s t a b aa ba. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q rv s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' s t a b aa ba x11 x12. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q rv s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv = CNode x11 x12\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<And>rv rv' s t a b aa ba x2. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q rv s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv = TCB x2\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 3. \<And>rv rv' s t a b aa ba x3. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q rv s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv = Endpoint x3\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 4. \<And>rv rv' s t a b aa ba x4. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q rv s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv = Notification x4\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 5. \<And>rv rv' s t a b aa ba x5. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case rv of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q rv s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv = ArchObj x5\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv' s t a b aa ba x5. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv' s t a b aa ba x5 x11 x12. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv' = CNode x11 x12\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<And>rv' s t a b aa ba x5 x2. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv' = TCB x2\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 3. \<And>rv' s t a b aa ba x5 x3. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv' = Endpoint x3\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 4. \<And>rv' s t a b aa ba x5 x4. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv' = Notification x4\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 5. \<And>rv' s t a b aa ba x5 x5a. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case rv' of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q rv' t; reads_equiv aag s t; affects_equiv aag l s t; rv' = ArchObj x5a\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba x5 x5a. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case x5 of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case x5a of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj x5) s; ?Q (ArchObj x5a) t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj'. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x1. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x2. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 3. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x3. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 4. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 5. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x1 x1a. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = ASIDPool x1; arch_kernel_obj' = ASIDPool x1a\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 2. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x1 x2. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = ASIDPool x1; arch_kernel_obj' = PageTable x2\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 3. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x1 x3. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = ASIDPool x1; arch_kernel_obj' = PageDirectory x3\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 4. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x1 x41 x42. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = ASIDPool x1; arch_kernel_obj' = DataPage x41 x42\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 5. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x2. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 6. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x3. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 7. \<And>s t a b aa ba arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>pasObjectAbs aag ptr \<notin> subjectReads (pasPolicy aag) (pasSubject aag); (a, b) \<in> fst ((case arch_kernel_obj of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) s); (aa, ba) \<in> fst ((case arch_kernel_obj' of ASIDPool x \<Rightarrow> return x | _ \<Rightarrow> fail) t); ?Q (ArchObj arch_kernel_obj) s; ?Q (ArchObj arch_kernel_obj') t; reads_equiv aag s t; affects_equiv aag l s t; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba
 8. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal:
No subgoals!