theory Finalise_DR

lemma invalidate_asid_entry_dwp[wp]:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid_entry x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>" apply (clarsimp simp:invalidate_asid_entry_def) apply wp apply (clarsimp simp:invalidate_asid_def) apply wp+ apply (clarsimp simp:invalidate_hw_asid_entry_def) apply wp+ apply (clarsimp simp:load_hw_asid_def) apply wp apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid_entry x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do maybe_hw_asid <- load_hw_asid x;
y <- when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid));
invalidate_asid x
od \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>maybe_hw_asid y. \<lbrace>?B2 maybe_hw_asid y\<rbrace> invalidate_asid x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>?B2 maybe_hw_asid\<rbrace>
 3. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>?B1\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>maybe_hw_asid. \<lbrace>?B2 maybe_hw_asid ()\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(x := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>?B2 maybe_hw_asid\<rbrace>
 3. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>?B1\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q13 maybe_hw_asid\<rbrace> invalidate_hw_asid_entry (the maybe_hw_asid) \<lbrace>\<lambda>a b. transform (b\<lparr>arch_state := arch_state b\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) b)(x := None)\<rparr>\<rparr>) = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q13 maybe_hw_asid else (\<lambda>a. transform (a\<lparr>arch_state := arch_state a\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) a)(x := None)\<rparr>\<rparr>) = cs)\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?Q13 (Some y)\<rbrace> do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(y := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>a b. transform (b\<lparr>arch_state := arch_state b\<lparr>arm_asid_map := \<lambda>a. if a = x then None else arm_asid_map (arch_state b) a\<rparr>\<rparr>) = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q13 maybe_hw_asid else (\<lambda>a. transform (a\<lparr>arch_state := arch_state a\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) a)(x := None)\<rparr>\<rparr>) = cs)\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then \<lambda>x2. transform (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the maybe_hw_asid := None)\<rparr>, arch_state := arch_state (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the maybe_hw_asid := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := \<lambda>a. if a = x then None else arm_asid_map (arch_state (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the maybe_hw_asid := None)\<rparr>\<rparr>)) a\<rparr>\<rparr>) = cs else (\<lambda>a. transform (a\<lparr>arch_state := arch_state a\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) a)(x := None)\<rparr>\<rparr>) = cs)\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
return (map_option fst (asid_map x))
od \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then \<lambda>x2. transform (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the maybe_hw_asid := None)\<rparr>, arch_state := arch_state (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the maybe_hw_asid := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := \<lambda>a. if a = x then None else arm_asid_map (arch_state (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the maybe_hw_asid := None)\<rparr>\<rparr>)) a\<rparr>\<rparr>) = cs else (\<lambda>a. transform (a\<lparr>arch_state := arch_state a\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) a)(x := None)\<rparr>\<rparr>) = cs)\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. transform s = cs \<Longrightarrow> (if \<exists>y. map_option fst ((arm_asid_map \<circ> arch_state) s x) = Some y then \<lambda>x2. transform (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the (map_option fst ((arm_asid_map \<circ> arch_state) s x)) := None)\<rparr>, arch_state := arch_state (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the (map_option fst ((arm_asid_map \<circ> arch_state) s x)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := \<lambda>a. if a = x then None else arm_asid_map (arch_state (x2\<lparr>arch_state := arch_state x2\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) x2)(the (map_option fst ((arm_asid_map \<circ> arch_state) s x)) := None)\<rparr>\<rparr>)) a\<rparr>\<rparr>) = cs else (\<lambda>a. transform (a\<lparr>arch_state := arch_state a\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) a)(x := None)\<rparr>\<rparr>) = cs)) s proof (prove)
goal:
No subgoals!