theory Finalise_DR

lemma flush_space_dwp[wp]:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_space x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>" apply (clarsimp simp:flush_space_def) apply (wp|wpc)+ apply (clarsimp split:option.splits) apply (rule do_machine_op_wp) apply clarsimp apply (wp hoare_weak_lift_imp)+ apply (rule do_machine_op_wp) apply clarsimp apply wp apply (rule hoare_allI) apply (rule hoare_drop_imp) apply (rule do_machine_op_wp) apply clarsimp apply wp apply (rule hoare_conjI) apply (rule hoare_drop_imp) apply (clarsimp simp:load_hw_asid_def) apply wp apply (clarsimp simp:load_hw_asid_def) apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_space 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 <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>maybe_hw_asid y x2. maybe_hw_asid = Some x2 \<Longrightarrow> \<lbrace>?R12 maybe_hw_asid y x2\<rbrace> do_machine_op (invalidateLocalTLB_ASID x2) \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?R12 maybe_hw_asid y x s)\<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>x2. \<lbrace>?R12 (Some x2) () x2\<rbrace> do_machine_op (invalidateLocalTLB_ASID x2) \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?R12 maybe_hw_asid y x s)\<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>x2. \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID x2 \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs)\<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>x2 m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID x2 \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs)\<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>?P'34 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?P'33 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. \<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs\<rbrace>
 3. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?P'34 maybe_hw_asid s) \<and> ?P'33 maybe_hw_asid s\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>maybe_hw_asid. \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?P'33 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. \<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs\<rbrace>
 3. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> ?P'33 maybe_hw_asid s\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>maybe_hw_asid. \<lbrace>?P'33 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. \<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs\<rbrace>
 3. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> ?P'33 maybe_hw_asid s\<rbrace>
 4. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid. \<lbrace>?P'33 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. \<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> ?P'33 maybe_hw_asid s\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid x. \<lbrace>?P'33 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. maybe_hw_asid = Some x \<longrightarrow> transform s = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> ?P'33 maybe_hw_asid s\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid x. \<lbrace>?P'33 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> ?P'33 maybe_hw_asid s\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid x. \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> transform s = cs\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> transform s = 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 s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> transform s = cs\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>r s. r = None \<longrightarrow> transform s = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 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>rv s. transform s = cs\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid x \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> load_hw_asid x \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> transform s = cs proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
return (map_option fst (asid_map x))
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> transform s = cs proof (prove)
goal (1 subgoal):
 1. \<And>s. transform s = cs \<Longrightarrow> transform s = cs proof (prove)
goal:
No subgoals!