theory Finalise_DR

lemma store_hardware_asid_dwp[wp]:
  "\<lbrace>\<lambda>s. transform s = cs\<rbrace> store_hw_asid a xa \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>" apply (clarsimp simp:store_hw_asid_def) apply wp apply (simp add:find_pd_for_asid_assert_def) apply wp apply (simp add:find_pd_for_asid_def) apply (wp|wpc)+ 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>s. transform s = cs\<rbrace> store_hw_asid a xa \<lbrace>\<lambda>xb a. transform a = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> do pd <- find_pd_for_asid_assert a;
asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (xa, pd))\<rparr>\<rparr>);
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(xa \<mapsto> a)\<rparr>\<rparr>)
od \<lbrace>\<lambda>xb a. transform a = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd s. transform (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(a \<mapsto> (xa, pd))\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(a \<mapsto> (xa, pd))\<rparr>\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(a \<mapsto> (xa, pd))\<rparr>\<rparr>))(xa \<mapsto> a)\<rparr>\<rparr>) = cs\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do pd <- find_pd_for_asid a <catch> (\<lambda>y. fail);
y <- get_pde pd;
return pd
od \<lbrace>\<lambda>pd s. transform (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>b. if b = a then Some (xa, pd) else arm_asid_map (arch_state s) b, arm_hwasid_table := \<lambda>b. if b = xa then Some a else arm_hwasid_table (arch_state s) b\<rparr>\<rparr>) = cs\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'18\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pd b. transform (b\<lparr>arch_state := arch_state b\<lparr>arm_asid_map := \<lambda>c. if c = a then Some (xa, pd) else arm_asid_map (arch_state b) c, arm_hwasid_table := \<lambda>c. if c = xa then Some a else arm_hwasid_table (arch_state b) c\<rparr>\<rparr>) = cs\<rbrace>, -
 2. \<And>s. transform s = cs \<Longrightarrow> True \<and> ?P'18 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'18\<rbrace> doE y <- assertE (0 < a);
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE \<lbrace>\<lambda>pd b. transform (b\<lparr>arch_state := arch_state b\<lparr>arm_asid_map := \<lambda>ba. if ba = a then Some (xa, pd) else arm_asid_map (arch_state b) ba, arm_hwasid_table := \<lambda>ba. if ba = xa then Some a else arm_hwasid_table (arch_state b) ba\<rparr>\<rparr>) = cs\<rbrace>, -
 2. \<And>s. transform s = cs \<Longrightarrow> True \<and> ?P'18 s proof (prove)
goal (1 subgoal):
 1. \<And>s. transform s = cs \<Longrightarrow> True \<and> (0 < a \<longrightarrow> True \<and> True \<and> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of a) = None \<longrightarrow> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of a) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (pool (UCAST(32 \<rightarrow> 10) a) = None \<longrightarrow> True) \<and> (\<forall>x. pool (UCAST(32 \<rightarrow> 10) a) = Some x \<longrightarrow> transform (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>b. if b = a then Some (xa, x) else arm_asid_map (arch_state s) b, arm_hwasid_table := \<lambda>b. if b = xa then Some a else arm_hwasid_table (arch_state s) b\<rparr>\<rparr>) = cs)))) proof (prove)
goal:
No subgoals!