kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchRetype_IF

lemma clearMemory_ev[Retype_IF_assms]:
  "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (clearMemory ptr bits)" unfolding clearMemory_def apply simp apply (rule equiv_valid_guard_imp) apply (rule bind_ev) apply (rule cleanCacheRange_RAM_ev) apply (rule mapM_x_ev[OF storeWord_ev]) apply (rule wp_post_taut | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (clearMemory ptr bits) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (do mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1];
cleanCacheRange_RAM ptr (ptr + word_of_nat bits - 1) (addrFromPPtr ptr)
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1];
cleanCacheRange_RAM ptr (ptr + word_of_nat bits - 1) (addrFromPPtr ptr)
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) ?Q (do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1];
cleanCacheRange_RAM ptr (ptr + word_of_nat bits - 1) (addrFromPPtr ptr)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (?Q3 rv) (cleanCacheRange_RAM ptr (ptr + word_of_nat bits - 1) (addrFromPPtr ptr))
 2. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) ?P'3 (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1])
 3. \<lbrace>?P''3\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1] \<lbrace>?Q3\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) ?P'3 (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1])
 2. \<lbrace>?P''3\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1] \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1] \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> storeWord x 0 \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?P''3\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1] \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma freeMemory_ev[Retype_IF_assms]:
  "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (freeMemory ptr bits)" unfolding freeMemory_def apply (rule equiv_valid_guard_imp) apply (rule mapM_x_ev[OF storeWord_ev]) apply (rule wp_post_taut | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (freeMemory ptr bits) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) (\<lambda>_. True) (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) ?Q (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1])
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> storeWord x 0 \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. True \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma dmo_cacheRangeOp_reads_respects:
  "(\<And>a b. reads_respects aag l \<top> (do_machine_op (oper a b)))
   \<Longrightarrow> reads_respects aag l \<top> (do_machine_op (cacheRangeOp oper x y z))" apply (simp add: cacheRangeOp_def) apply (rule dmo_mapM_x_ev) apply (simp add: split_def) apply (rule hoare_TrueI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. reads_respects aag l (\<lambda>_. True) (do_machine_op (oper a b))) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (cacheRangeOp oper x y z)) proof (prove)
goal (1 subgoal):
 1. (\<And>a b. reads_respects aag l (\<lambda>_. True) (do_machine_op (oper a b))) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (mapM_x (\<lambda>(x, y). oper x y) (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))]))) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<And>a b. reads_respects aag l (\<lambda>_. True) (do_machine_op (oper a b)); xa \<in> set (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (case xa of (x, xa) \<Rightarrow> oper x xa))
 2. \<And>xa. \<lbrakk>\<And>a b. reads_respects aag l (\<lambda>_. True) (do_machine_op (oper a b)); xa \<in> set (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (case xa of (x, xa) \<Rightarrow> oper x xa) \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>a b. reads_respects aag l (\<lambda>_. True) (do_machine_op (oper a b)); xa \<in> set (zip [lineStart x , lineStart x + word_of_nat cacheLine .e. lineStart y] [lineStart z , lineStart z + word_of_nat cacheLine .e. lineStart (z + (y - x))])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (case xa of (x, xa) \<Rightarrow> oper x xa) \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma dmo_cleanCacheRange_PoU_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (cleanCacheRange_PoU vsrat vend pstart))" unfolding cleanCacheRange_PoU_def by (wp dmo_cacheRangeOp_reads_respects dmo_mol_reads_respects | simp add: cleanByVA_PoU_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (cleanCacheRange_PoU vsrat vend pstart)) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (cacheRangeOp cleanByVA_PoU vsrat vend pstart))
theory ArchRetype_IF

lemma set_pd_globals_equiv:
  "\<lbrace>globals_equiv st and (\<lambda>s. a \<noteq> arm_global_pd (arch_state s))\<rbrace> set_pd a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding set_pd_def by (wpsimp wp: set_object_globals_equiv[THEN hoare_set_object_weaken_pre] simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. a \<noteq> arm_global_pd (arch_state s))\<rbrace> set_pd a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. a \<noteq> arm_global_pd (arch_state s))\<rbrace> set_object a (ArchObj (PageDirectory b)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchRetype_IF

lemma set_pd_reads_respects:
  "reads_respects aag l (K (is_subject aag a)) (set_pd a b)" unfolding set_pd_def by (blast intro: equiv_valid_guard_imp set_object_reads_respects)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag a)) (set_pd a b) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag a)) (set_object a (ArchObj (PageDirectory b)))
theory ArchRetype_IF

lemma set_pd_reads_respects_g:
  "reads_respects_g aag l (\<lambda> s. is_subject aag ptr \<and> ptr \<noteq> arm_global_pd (arch_state s)) (set_pd ptr pd)" by (fastforce intro: equiv_valid_guard_imp[OF reads_respects_g] doesnt_touch_globalsI
                       set_pd_reads_respects set_pd_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag ptr \<and> ptr \<noteq> arm_global_pd (arch_state s)) (set_pd ptr pd)
theory ArchRetype_IF

lemma get_object_arm_global_pd_revg:
  "reads_equiv_valid_g_inv A aag (\<lambda> s. p = arm_global_pd (arch_state s)) (get_object p)" apply (unfold get_object_def fun_app_def) apply (subst gets_apply) apply (wp gets_apply_ev') defer apply (wp hoare_drop_imps) apply (rule conjI) apply assumption apply simp apply (auto simp: reads_equiv_g_def globals_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. p = arm_global_pd (arch_state s)) (get_object p) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. p = arm_global_pd (arch_state s)) (do kh <- gets kheap;
assert (kh p \<noteq> None);
return (the (kh p))
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. p = arm_global_pd (arch_state s)) (do a <- gets_apply kheap p;
assert (a \<noteq> None);
return (the a)
od) proof (prove)
goal (3 subgoals):
 1. \<forall>s t. reads_equiv_g aag s t \<and> A s t \<and> ?P' s \<and> ?P' t \<longrightarrow> kheap s p = kheap t p
 2. \<lbrace>?P''\<rbrace> gets_apply kheap p \<lbrace>\<lambda>rv s. True \<and> (rv \<noteq> None \<longrightarrow> True)\<rbrace>
 3. \<And>s. p = arm_global_pd (arch_state s) \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P''\<rbrace> gets_apply kheap p \<lbrace>\<lambda>rv s. True \<and> (rv \<noteq> None \<longrightarrow> True)\<rbrace>
 2. \<And>s. p = arm_global_pd (arch_state s) \<Longrightarrow> ?P' s \<and> ?P'' s
 3. \<forall>s t. reads_equiv_g aag s t \<and> A s t \<and> ?P' s \<and> ?P' t \<longrightarrow> kheap s p = kheap t p proof (prove)
goal (2 subgoals):
 1. \<And>s. p = arm_global_pd (arch_state s) \<Longrightarrow> ?P' s \<and> True \<and> (kheap s p \<noteq> None \<longrightarrow> True)
 2. \<forall>s t. reads_equiv_g aag s t \<and> A s t \<and> ?P' s \<and> ?P' t \<longrightarrow> kheap s p = kheap t p proof (prove)
goal (3 subgoals):
 1. \<And>s. p = arm_global_pd (arch_state s) \<Longrightarrow> ?P' s
 2. \<And>s. p = arm_global_pd (arch_state s) \<Longrightarrow> True \<and> (kheap s p \<noteq> None \<longrightarrow> True)
 3. \<forall>s t. reads_equiv_g aag s t \<and> A s t \<and> ?P' s \<and> ?P' t \<longrightarrow> kheap s p = kheap t p proof (prove)
goal (2 subgoals):
 1. \<And>s. p = arm_global_pd (arch_state s) \<Longrightarrow> True \<and> (kheap s p \<noteq> None \<longrightarrow> True)
 2. \<forall>s t. reads_equiv_g aag s t \<and> A s t \<and> p = arm_global_pd (arch_state s) \<and> p = arm_global_pd (arch_state t) \<longrightarrow> kheap s p = kheap t p proof (prove)
goal (1 subgoal):
 1. \<forall>s t. reads_equiv_g aag s t \<and> A s t \<and> p = arm_global_pd (arch_state s) \<and> p = arm_global_pd (arch_state t) \<longrightarrow> kheap s p = kheap t p proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma get_pd_revg:
  "reads_equiv_valid_g_inv A aag (\<lambda> s. ptr = arm_global_pd (arch_state s)) (get_pd ptr)" unfolding get_pd_def by (wp get_object_arm_global_pd_revg | wpc | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. ptr = arm_global_pd (arch_state s)) (get_pd ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. ptr = arm_global_pd (arch_state s)) (do kobj <- get_object ptr;
case kobj of ArchObj (PageDirectory pd) \<Rightarrow> return pd | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od)
theory ArchRetype_IF

lemma store_pde_reads_respects:
  "reads_respects aag l (K (is_subject aag (ptr && ~~ mask pd_bits)))
                         (store_pde ptr pde)" unfolding store_pde_def fun_app_def apply (wp set_pd_reads_respects get_pd_rev) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (ptr && ~~ mask pd_bits))) (store_pde ptr pde) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (ptr && ~~ mask pd_bits))) (do base <- return (ptr && ~~ mask pd_bits);
offset <- return (ptr && mask pd_bits >> 2);
pd <- get_pd base;
return (pd(UCAST(32 \<rightarrow> 12) offset := pde)) >>= set_pd base
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (is_subject aag (ptr && ~~ mask pd_bits)) s \<Longrightarrow> K (is_subject aag (ptr && ~~ mask pd_bits)) s \<and> (\<forall>pd. ako_at (PageDirectory pd) (ptr && ~~ mask pd_bits) s \<longrightarrow> True \<and> K (is_subject aag (ptr && ~~ mask pd_bits)) s) proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma store_pde_globals_equiv:
  "\<lbrace>globals_equiv s and (\<lambda> s. ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
   store_pde ptr pde
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding store_pde_def apply (wp set_pd_globals_equiv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace> do base <- return (ptr && ~~ mask pd_bits);
offset <- return (ptr && mask pd_bits >> 2);
pd <- get_pd base;
(return $ pd(UCAST(32 \<rightarrow> 12) offset := pde)) >>= set_pd base
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. (globals_equiv s and (\<lambda>s. ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) sa \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (ptr && ~~ mask pd_bits) sa \<longrightarrow> (globals_equiv s and (\<lambda>s. ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) sa proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma store_pde_reads_respects_g:
  "reads_respects_g aag l (\<lambda>s. is_subject aag (ptr && ~~ mask pd_bits) \<and>
                               ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))
                    (store_pde ptr pde)" by (fastforce intro: equiv_valid_guard_imp[OF reads_respects_g] doesnt_touch_globalsI
                       store_pde_reads_respects store_pde_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag (ptr && ~~ mask pd_bits) \<and> ptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) (store_pde ptr pde)
theory ArchRetype_IF

lemma get_pde_rev:
  "reads_equiv_valid_inv A aag (K (is_subject aag (ptr && ~~ mask pd_bits))) (get_pde ptr)" unfolding get_pde_def fun_app_def by (wpsimp wp: get_pd_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag (ptr && ~~ mask pd_bits))) (get_pde ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag (ptr && ~~ mask pd_bits))) (do base <- return (ptr && ~~ mask pd_bits);
offset <- return (ptr && mask pd_bits >> 2);
pd <- get_pd base;
return (pd (UCAST(32 \<rightarrow> 12) offset))
od)
theory ArchRetype_IF

lemma get_pde_revg:
  "reads_equiv_valid_g_inv A aag (\<lambda>s. (ptr && ~~ mask pd_bits) = arm_global_pd (arch_state s))
                                 (get_pde ptr)" unfolding get_pde_def fun_app_def by (wpsimp wp: get_pd_revg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. ptr && ~~ mask pd_bits = arm_global_pd (arch_state s)) (get_pde ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv A aag (\<lambda>s. ptr && ~~ mask pd_bits = arm_global_pd (arch_state s)) (do base <- return (ptr && ~~ mask pd_bits);
offset <- return (ptr && mask pd_bits >> 2);
pd <- get_pd base;
return (pd (UCAST(32 \<rightarrow> 12) offset))
od)
theory ArchRetype_IF

lemma mol_exclusive_state:
  "machine_op_lift mop \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace>" apply (simp add: machine_op_lift_def machine_rest_lift_def) apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> do mr <- gets machine_state_rest;
(r, mr') <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. mr'))
od \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma dmo_mol_globals_equiv:
  "do_machine_op (machine_op_lift f) \<lbrace>globals_equiv s\<rbrace>" apply (rule dmo_no_mem_globals_equiv) apply (simp add: machine_op_lift_def machine_rest_lift_def) apply (wp mol_exclusive_state | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (machine_op_lift f) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> do mr <- gets machine_state_rest;
(r, mr') <- select_f (ignore_failure f mr);
modify (machine_state_rest_update (\<lambda>_. mr'))
od \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma dmo_cleanCacheRange_PoU_globals_equiv:
  "do_machine_op (cleanCacheRange_PoU x y z) \<lbrace>globals_equiv s\<rbrace>" unfolding cleanCacheRange_PoU_def by (wp dmo_mol_globals_equiv dmo_cacheRangeOp_lift | simp add: cleanByVA_PoU_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (cleanCacheRange_PoU x y z) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (cacheRangeOp cleanByVA_PoU x y z) \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchRetype_IF

lemma dmo_cleanCacheRange_reads_respects_g:
  "reads_respects_g aag l \<top> (do_machine_op (cleanCacheRange_PoU x y z))" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule dmo_cleanCacheRange_PoU_reads_respects) apply (rule doesnt_touch_globalsI[where P="\<top>", simplified, OF dmo_cleanCacheRange_PoU_globals_equiv]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (do_machine_op (cleanCacheRange_PoU x y z)) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (do_machine_op (cleanCacheRange_PoU x y z))
 2. doesnt_touch_globals ?Q1 (do_machine_op (cleanCacheRange_PoU x y z))
 3. \<And>s. True \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (do_machine_op (cleanCacheRange_PoU x y z))
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
theory ArchRetype_IF

lemma mol_globals_equiv:
  "machine_op_lift mop \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding machine_op_lift_def apply (simp add: machine_rest_lift_def split_def) apply wp apply (clarsimp simp: globals_equiv_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> (machine_rest_lift \<circ> ignore_failure) mop \<lbrace>\<lambda>_ ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv st (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> \<forall>x\<in>fst (ignore_failure mop (machine_state_rest sa)). globals_equiv st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := snd x\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma storeWord_globals_equiv:
  "storeWord p v \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding storeWord_def apply (simp add: is_aligned_mask[symmetric]) apply wp apply (clarsimp simp: globals_equiv_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> storeWord p v \<lbrace>\<lambda>_ ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> do assert (p && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! 1, p + 3 := word_rsplit v ! 0)))
od \<lbrace>\<lambda>_ ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> do y <- assert (is_aligned p 2);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! Suc 0, p + 3 := word_rsplit v ! 0)))
od \<lbrace>\<lambda>_ ms. globals_equiv st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv st (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> is_aligned p 2 \<longrightarrow> globals_equiv st (s\<lparr>machine_state := underlying_memory_update (\<lambda>m. m(p := word_rsplit v ! 3, p + 1 := word_rsplit v ! 2, p + 2 := word_rsplit v ! Suc 0, p + 3 := word_rsplit v ! 0)) sa\<rparr>) proof (prove)
goal:
No subgoals!