theory VSpace_C

lemma findPDForASIDAssert_pd_at_wp2:
  "\<lbrace>\<lambda>s. \<forall>pd. pd_at_asid' pd asid s
        \<and> pd \<notin> ran (option_map snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid}))
        \<and> option_map snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}
         \<longrightarrow> P pd s\<rbrace> findPDForASIDAssert asid \<lbrace>P\<rbrace>" apply (rule hoare_pre) apply (simp add: findPDForASIDAssert_def const_def
                    checkPDAt_def checkPDUniqueToASID_def
                    checkPDASIDMapMembership_def) apply (wp findPDForASID_pd_at_wp) apply clarsimp apply (drule spec, erule mp) apply clarsimp apply (clarsimp split: option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} \<longrightarrow> P pd s\<rbrace> findPDForASIDAssert asid \<lbrace>P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> findPDForASIDAssert asid \<lbrace>P\<rbrace>
 2. \<And>s. \<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} \<longrightarrow> P pd s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do pd <- findPDForASID asid <catch> (\<lambda>y. fail);
y <- assert (pd && mask pdBits = 0);
y <- stateAssert (page_directory_at' pd) [];
y <- stateAssert (\<lambda>s. pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>)) [];
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb);
return pd
od \<lbrace>P\<rbrace>
 2. \<And>s. \<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} \<longrightarrow> P pd s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> map_option snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} \<longrightarrow> P pd s \<Longrightarrow> True \<and> (\<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s) \<longrightarrow> pd && mask pdBits = 0 \<longrightarrow> page_directory_at' pd s \<longrightarrow> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb) \<longrightarrow> P pd s) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>\<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> (armKSASIDMap (ksArchState s) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState s) asid = Some (a, pd))) \<longrightarrow> P pd s; pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s\<rbrakk> \<Longrightarrow> P pd s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s\<rbrakk> \<Longrightarrow> pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>) \<and> (armKSASIDMap (ksArchState s) asid = None \<or> (\<exists>a. armKSASIDMap (ksArchState s) asid = Some (a, pd))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>pd && mask pdBits = 0; page_directory_at' pd s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s)|\<^bsub>(- {asid})\<^esub>); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb; pd_at_asid' pd asid s; \<forall>a. armKSASIDMap (ksArchState s) asid \<noteq> Some (a, pd)\<rbrakk> \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None proof (prove)
goal:
No subgoals!