theory ArchArch_IF

lemma find_pd_for_asid_reads_respects:
  "reads_respects aag l (K (is_subject_asid aag asid)) (find_pd_for_asid asid)" apply (simp add: find_pd_for_asid_def) apply (subst gets_applyE) 
  (* everything up to and including get_asid_pool, both executions are the same.
     it is only get_asid_pool that can return different values and for which we need
     to go equiv_valid_2. We rewrite using associativity to make the decomposition
     easier *)
   apply (subst bindE_assoc[symmetric])+ apply (simp add: equiv_valid_def2) apply (subst rel_sum_comb_equals[symmetric]) apply (rule equiv_valid_rv_guard_imp) apply (rule_tac R'="\<lambda> rv rv'. rv (ucast asid) = rv' (ucast asid)" and Q="\<top>\<top>" and Q'="\<top>\<top>"
                in equiv_valid_2_bindE) apply (clarsimp split: option.splits simp: throwError_def returnOk_def) apply (intro conjI impI allI) apply (rule return_ev2, simp) apply (rule return_ev2, simp) apply wp+ apply (rule_tac R'="(=)"
               and Q="\<lambda> rv s. rv = (arm_asid_table (arch_state s)) (asid_high_bits_of asid)
                            \<and> is_subject_asid aag asid \<and> asid \<noteq> 0"
               and Q'="\<lambda> rv s. rv = (arm_asid_table (arch_state s)) (asid_high_bits_of asid)
                             \<and> is_subject_asid aag asid \<and> asid \<noteq> 0"
                in equiv_valid_2_bindE) apply (simp add: equiv_valid_def2[symmetric]) apply (split option.splits) apply (intro conjI impI allI) apply (simp add: throwError_def) apply (rule return_ev2, simp) apply (rule equiv_valid_2_liftE) apply (clarsimp) apply (rule get_asid_pool_revrv) apply (wp gets_apply_wp)+ apply (subst rel_sum_comb_equals) apply (subst equiv_valid_def2[symmetric]) apply (wp gets_apply_ev | simp)+ apply (fastforce intro: requiv_arm_asid_table_asid_high_bits_of_asid_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject_asid aag asid)) (find_pd_for_asid asid) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject_asid aag asid) (doE y <- assertE (0 < asid);
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr);
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x2 \<Rightarrow> returnOk x2
odE) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject_asid aag asid) (doE y <- assertE (0 < asid);
a <- liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid));
pool <- case a of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr);
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject_asid aag asid) (doE y <- assertE (0 < asid);
a <- liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid));
pool <- case a of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr);
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject_asid aag asid) (doE pool <- doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr));
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>y. is_subject_asid aag asid) (doE pool <- doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr));
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) (\<lambda>y. is_subject_asid aag asid) (doE pool <- doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr));
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P10 (doE pool <- doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr));
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE)
 2. \<And>s. is_subject_asid aag asid \<Longrightarrow> ?P10 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) ((=) \<oplus> (=)) (\<lambda>_. True) (\<lambda>_. True) (case rv (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x) (case rv' (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x)
 2. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 3. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) ?P13 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)))
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P13 and ?S13) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid) \<Longrightarrow> (rv' (UCAST(32 \<rightarrow> 10) asid) = None \<longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) (\<lambda>_. True) (return (Inl InvalidRoot))) \<and> (\<forall>x2. rv' (UCAST(32 \<rightarrow> 10) asid) = Some x2 \<longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) (\<lambda>_. True) (return (Inr x2)))
 2. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 3. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) ?P13 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)))
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P13 and ?S13) s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid); rv' (UCAST(32 \<rightarrow> 10) asid) = None\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) (\<lambda>_. True) (return (Inl InvalidRoot))
 2. \<And>rv rv' x2. \<lbrakk>rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid); rv' (UCAST(32 \<rightarrow> 10) asid) = Some x2\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) (\<lambda>_. True) (return (Inr x2))
 3. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 4. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 5. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) ?P13 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)))
 6. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P13 and ?S13) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' x2. \<lbrakk>rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid); rv' (UCAST(32 \<rightarrow> 10) asid) = Some x2\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) (\<lambda>_. True) (return (Inr x2))
 2. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 3. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) ?P13 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)))
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P13 and ?S13) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 2. \<lbrace>?S13\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 3. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) ?P13 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)))
 4. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P13 and ?S13) s proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) ?P13 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE >>=E case_option (throwError InvalidRoot) (\<lambda>ptr. liftE (get_asid_pool ptr)))
 2. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P13 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr)) (case rv' of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr))
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr))
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. (rv = None \<longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (throwError InvalidRoot)) \<and> (\<forall>x2. rv = Some x2 \<longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (liftE (get_asid_pool x2)))
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. rv = None \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (throwError InvalidRoot)
 2. \<And>rv x2. rv = Some x2 \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (liftE (get_asid_pool x2))
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 5. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 6. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (6 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. None = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (return (Inl InvalidRoot))
 2. \<And>rv x2. rv = Some x2 \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (liftE (get_asid_pool x2))
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 5. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 6. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv x2. rv = Some x2 \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid))) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (liftE (get_asid_pool x2))
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv x2. rv = Some x2 \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (\<lambda>s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (get_asid_pool x2)
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>x2. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (\<lambda>s. Some x2 = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (get_asid_pool x2)
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 4. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 5. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 2. \<lbrace>?S38\<rbrace> doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE \<lbrace>\<lambda>rv s. rv = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace>, -
 3. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 4. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and ?S38 and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ((=) \<oplus> (=)) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 2. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and (\<lambda>s. 0 < asid \<longrightarrow> (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 2. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and (\<lambda>s. 0 < asid \<longrightarrow> (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?P38 (doE y <- assertE (0 < asid);
liftE (gets_apply (arm_asid_table \<circ> arch_state) (asid_high_bits_of asid))
odE)
 2. \<And>s. is_subject_asid aag asid \<Longrightarrow> (?P38 and (\<lambda>s. 0 < asid \<longrightarrow> (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. is_subject_asid aag asid \<Longrightarrow> (0 < asid \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid))) \<and> (0 < asid \<longrightarrow> asid \<noteq> 0) proof (prove)
goal:
No subgoals!