theory Fastpath_C

lemma armv_contextSwitch_HWASID_fp_rewrite:
  "monadic_rewrite True False
    (pd_has_hwasid pd and pd_at_asid' pd asid and
        (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd
                                     = set_option (pde_stored_asid v)))
    (armv_contextSwitch pd asid)
    (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))" apply (simp add: getHWASID_def armv_contextSwitch_def
                        bind_assoc loadHWASID_def
                        findPDForASIDAssert_def
                        checkPDAt_def checkPDUniqueToASID_def
                        checkPDASIDMapMembership_def
                        stateAssert_def2[folded assert_def]) apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_gets_l) apply (rule monadic_rewrite_symb_exec_l) apply (rule monadic_rewrite_assert monadic_rewrite_gets_l)+ apply (rule_tac P="asidMap asid \<noteq> None \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)"
               in monadic_rewrite_gen_asm) apply (simp add: case_option_If2 split_def) apply (rule monadic_rewrite_refl) apply (wpsimp wp: findPDForASID_pd_at_wp simp: empty_fail_catch)+ apply (clarsimp simp: pd_has_hwasid_def cte_level_bits_def
                        field_simps cte_wp_at_ctes_of
                        word_0_sle_from_less
                        isCap_simps invs_valid_pspace'
              simp del: Collect_const rf_sr_upd_safe) apply (drule(1) pd_at_asid_inj') apply (clarsimp simp: singleton_eq_o2s singleton_eq_o2s[THEN trans[OF eq_commute]]) apply (cases "pde_stored_asid v", simp_all) apply (clarsimp simp: asid_map_pd_to_hwasids_def set_eq_subset
                 elim!: ranE) apply (case_tac "x = asid") apply clarsimp apply (erule notE, rule_tac a=x in ranI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) (armv_contextSwitch pd asid) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v)))) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
pda <- findPDForASID asid <catch> const fail;
y <- assert (pda && mask pdBits = 0);
x <- gets (page_directory_at' pda);
y <- assert x;
x <- gets (\<lambda>s. pda \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>));
y <- assert x;
asidMapa <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMapa asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pda = xb);
hwasid <- case case asidMap asid of None \<Rightarrow> Nothing | Some (hw_asid, xa) \<Rightarrow> Just hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some x \<Rightarrow> return x;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v)))) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?Q2 (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
pda <- findPDForASID asid <catch> const fail;
y <- assert (pda && mask pdBits = 0);
x <- gets (page_directory_at' pda);
y <- assert x;
x <- gets (\<lambda>s. pda \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>));
y <- assert x;
asidMapa <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMapa asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pda = xb);
hwasid <- case case asidMap asid of None \<Rightarrow> Nothing | Some (hw_asid, xa) \<Rightarrow> Just hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some x \<Rightarrow> return x;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))
 2. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<And>asidMap. monadic_rewrite True False (?P5 asidMap) (do pda <- findPDForASID asid <catch> const fail;
y <- assert (pda && mask pdBits = 0);
x <- gets (page_directory_at' pda);
y <- assert x;
x <- gets (\<lambda>s. pda \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>));
y <- assert x;
asidMapa <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMapa asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> pda = b);
hwasid <- case case asidMap asid of None \<Rightarrow> Nothing | Some (hw_asid, x) \<Rightarrow> Just hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some a \<Rightarrow> return a;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))
 2. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?P5 ((armKSASIDMap \<circ> ksArchState) s) s proof (prove)
goal (5 subgoals):
 1. \<And>asidMap rv. monadic_rewrite True False (?Q9 asidMap rv) (do y <- assert (rv && mask pdBits = 0);
x <- gets (page_directory_at' rv);
y <- assert x;
x <- gets (\<lambda>s. rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>));
y <- assert x;
asidMapa <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMapa asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b);
hwasid <- case case asidMap asid of None \<Rightarrow> Nothing | Some (hw_asid, x) \<Rightarrow> Just hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some a \<Rightarrow> return a;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))
 2. \<And>asidMap P. \<lbrace>P\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>asidMap. empty_fail (findPDForASID asid <catch> const fail)
 4. \<And>asidMap. \<lbrace>?P5 asidMap\<rbrace> findPDForASID asid <catch> const fail \<lbrace>?Q9 asidMap\<rbrace>
 5. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?P5 ((armKSASIDMap \<circ> ksArchState) s) s proof (prove)
goal (5 subgoals):
 1. \<And>asidMap rv x xa xb. \<lbrakk>rv && mask pdBits = 0; x; xa; case xb asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P32 asidMap rv x xa xb) (do hwasid <- case case asidMap asid of None \<Rightarrow> Nothing | Some (hw_asid, x) \<Rightarrow> Just hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some a \<Rightarrow> return a;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))
 2. \<And>asidMap P. \<lbrace>P\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>asidMap. empty_fail (findPDForASID asid <catch> const fail)
 4. \<And>asidMap. \<lbrace>?P5 asidMap\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>rv s. rv && mask pdBits = 0 \<longrightarrow> page_directory_at' rv s \<longrightarrow> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b) \<longrightarrow> ?P32 asidMap rv (page_directory_at' rv s) (rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>)) ((armKSASIDMap \<circ> ksArchState) s) s\<rbrace>
 5. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?P5 ((armKSASIDMap \<circ> ksArchState) s) s proof (prove)
goal (5 subgoals):
 1. \<And>asidMap rv x xa xb. \<lbrakk>rv && mask pdBits = 0; x; xa; case xb asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b; asidMap asid \<noteq> None \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q34 asidMap rv x xa xb) (do hwasid <- case case asidMap asid of None \<Rightarrow> Nothing | Some (hw_asid, x) \<Rightarrow> Just hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some a \<Rightarrow> return a;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))
 2. \<And>asidMap P. \<lbrace>P\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>asidMap. empty_fail (findPDForASID asid <catch> const fail)
 4. \<And>asidMap. \<lbrace>?P5 asidMap\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>rv s. rv && mask pdBits = 0 \<longrightarrow> page_directory_at' rv s \<longrightarrow> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b) \<longrightarrow> ((\<lambda>_. asidMap asid \<noteq> None \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)) and ?Q34 asidMap rv (page_directory_at' rv s) (rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>)) ((armKSASIDMap \<circ> ksArchState) s)) s\<rbrace>
 5. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?P5 ((armKSASIDMap \<circ> ksArchState) s) s proof (prove)
goal (5 subgoals):
 1. \<And>asidMap rv x xa xb. \<lbrakk>rv && mask pdBits = 0; x; xa; if \<exists>a b. xb asid = Some (a, b) then case the (xb asid) of (x, xa) \<Rightarrow> rv = xa else True; (\<exists>a b. asidMap asid = Some (a, b)) \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q34 asidMap rv True True xb) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v)))) (doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))
 2. \<And>asidMap P. \<lbrace>P\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>asidMap. empty_fail (findPDForASID asid <catch> const fail)
 4. \<And>asidMap. \<lbrace>?P5 asidMap\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>rv s. rv && mask pdBits = 0 \<longrightarrow> page_directory_at' rv s \<longrightarrow> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b) \<longrightarrow> ((\<lambda>_. asidMap asid \<noteq> None \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)) and ?Q34 asidMap rv (page_directory_at' rv s) (rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>)) ((armKSASIDMap \<circ> ksArchState) s)) s\<rbrace>
 5. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?P5 ((armKSASIDMap \<circ> ksArchState) s) s proof (prove)
goal (4 subgoals):
 1. \<And>asidMap P. \<lbrace>P\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>asidMap. empty_fail (findPDForASID asid <catch> const fail)
 3. \<And>asidMap. \<lbrace>?P5 asidMap\<rbrace> findPDForASID asid <catch> const fail \<lbrace>\<lambda>rv s. rv && mask pdBits = 0 \<longrightarrow> page_directory_at' rv s \<longrightarrow> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> rv = b) \<longrightarrow> ((\<lambda>_. asidMap asid \<noteq> None \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)) and (\<lambda>a. rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>))) s\<rbrace>
 4. \<And>s. (pd_has_hwasid pd and pd_at_asid' pd asid and (\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v))) s \<Longrightarrow> ?P5 ((armKSASIDMap \<circ> ksArchState) s) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>pd_has_hwasid pd s; pd_at_asid' pd asid s; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = set_option (pde_stored_asid v); pda && mask pdBits = 0; page_directory_at' pda s; pda \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pda = xb; pd_at_asid' pda asid s\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = the (pde_stored_asid v) proof (prove)
goal (1 subgoal):
 1. \<And>s pda va. \<lbrakk>pd_at_asid' pd asid s; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = {va}; pda && mask pdBits = 0; page_directory_at' pda s; pda \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pda = xb; pd_at_asid' pda asid s; set_option (pde_stored_asid v) = {va}\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = the (pde_stored_asid v) proof (prove)
goal (1 subgoal):
 1. \<And>s pda va. \<lbrakk>asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = {va}; pda && mask pdBits = 0; page_directory_at' pda s; pda \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pda = xb; pd_at_asid' pda asid s; set_option (pde_stored_asid v) = {va}; pda = pd\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = the (pde_stored_asid v) proof (prove)
goal (1 subgoal):
 1. \<And>s va. \<lbrakk>asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = {va}; pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; pde_stored_asid v = Some va\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = va proof (prove)
goal (1 subgoal):
 1. \<And>s va a. \<lbrakk>asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = {va}; pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; a = va; pde_stored_asid v = Some va\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = va proof (prove)
goal (1 subgoal):
 1. \<And>s va x. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; pde_stored_asid v = Some va; {hwasid. (hwasid, pd) \<in> ran (armKSASIDMap (ksArchState s))} \<subseteq> {va}; armKSASIDMap (ksArchState s) x = Some (va, pd)\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = va proof (prove)
goal (2 subgoals):
 1. \<And>s va x. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; pde_stored_asid v = Some va; {hwasid. (hwasid, pd) \<in> ran (armKSASIDMap (ksArchState s))} \<subseteq> {va}; armKSASIDMap (ksArchState s) x = Some (va, pd); x = asid\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = va
 2. \<And>s va x. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; pde_stored_asid v = Some va; {hwasid. (hwasid, pd) \<in> ran (armKSASIDMap (ksArchState s))} \<subseteq> {va}; armKSASIDMap (ksArchState s) x = Some (va, pd); x \<noteq> asid\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = va proof (prove)
goal (1 subgoal):
 1. \<And>s va x. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (\<lambda>a. map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) a)); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; pde_stored_asid v = Some va; {hwasid. (hwasid, pd) \<in> ran (armKSASIDMap (ksArchState s))} \<subseteq> {va}; armKSASIDMap (ksArchState s) x = Some (va, pd); x \<noteq> asid\<rbrakk> \<Longrightarrow> (\<exists>a b. armKSASIDMap (ksArchState s) asid = Some (a, b)) \<and> fst (the (armKSASIDMap (ksArchState s) asid)) = va proof (prove)
goal (1 subgoal):
 1. \<And>s va x. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; pde_stored_asid v = Some va; {hwasid. (hwasid, pd) \<in> ran (armKSASIDMap (ksArchState s))} \<subseteq> {va}; armKSASIDMap (ksArchState s) x = Some (va, pd); x \<noteq> asid\<rbrakk> \<Longrightarrow> map_option snd ((armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) x) = Some pd proof (prove)
goal:
No subgoals!