kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_R

lemma valid_queues_lift_asm':
  assumes tat: "\<And>d p t. \<lbrace>\<lambda>s. \<not> obj_at' (inQ d p) t s \<and> Q d p s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> obj_at' (inQ d p) t s\<rbrace>"
  and     prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
  shows   "\<lbrace>\<lambda>s. valid_queues' s \<and> (\<forall>d p. Q d p s)\<rbrace> f \<lbrace>\<lambda>_. valid_queues'\<rbrace>" apply (simp only: valid_queues'_def imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
            tat prq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> (\<forall>d p. Q d p s)\<rbrace> f \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))) \<and> (\<forall>d p. Q d p s)\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))) \<and> (\<forall>d p. Q d p s) \<Longrightarrow> \<forall>x xa xb. \<not> obj_at' (inQ x xa) xb s \<and> Q x xa s \<or> xb \<in> set (ksReadyQueues s (x, xa)) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects'_ct[wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> createObjects' p n v us \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" by (rule createObjects_pspace_only, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> createObjects' p n v us \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>
theory Retype_R

lemma threadSet_ko_wp_at2':
  "\<lbrace>\<lambda>s. P (ko_wp_at' P' p s) \<and> (\<forall>tcb_x :: tcb. P' (injectKO (F tcb_x)) = P' (injectKO tcb_x))\<rbrace>
     threadSet F ptr
   \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace>" apply (simp add: threadSet_def split del: if_split) apply (wp setObject_ko_wp_at getObject_tcb_wp | simp add: objBits_simps')+ apply (auto simp: ko_wp_at'_def obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' P' p s) \<and> (\<forall>tcb_x. P' (injectKOS (F tcb_x)) = P' (injectKOS tcb_x))\<rbrace> threadSet F ptr \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' P' p s) \<and> (\<forall>tcb_x. P' (KOTCB (F tcb_x)) = P' (KOTCB tcb_x))\<rbrace> do tcb <- getObject ptr;
setObject ptr (F tcb)
od \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ko_wp_at' P' p s) \<and> (\<forall>tcb_x. P' (KOTCB (F tcb_x)) = P' (KOTCB tcb_x)) \<Longrightarrow> tcb_at' ptr s \<longrightarrow> (\<exists>t. (ptr = p \<longrightarrow> ko_at' t p s \<and> P (ko_wp_at' (\<lambda>y. P' (KOTCB t)) p s)) \<and> (ptr \<noteq> p \<longrightarrow> ko_at' t ptr s)) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma threadSet_ko_wp_at2'_futz:
  "\<lbrace>\<lambda>s. P (ko_wp_at' P' p s) \<and> obj_at' Q ptr s
         \<and> (\<forall>tcb_x :: tcb. Q tcb_x \<longrightarrow> P' (injectKO (F tcb_x)) = P' (injectKO tcb_x))\<rbrace>
     threadSet F ptr
   \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace>" apply (simp add: threadSet_def split del: if_split) apply (wp setObject_ko_wp_at getObject_tcb_wp | simp add: objBits_simps')+ apply (auto simp: ko_wp_at'_def obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' P' p s) \<and> obj_at' Q ptr s \<and> (\<forall>tcb_x. Q tcb_x \<longrightarrow> P' (injectKOS (F tcb_x)) = P' (injectKOS tcb_x))\<rbrace> threadSet F ptr \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' P' p s) \<and> obj_at' Q ptr s \<and> (\<forall>tcb_x. Q tcb_x \<longrightarrow> P' (KOTCB (F tcb_x)) = P' (KOTCB tcb_x))\<rbrace> do tcb <- getObject ptr;
setObject ptr (F tcb)
od \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ko_wp_at' P' p s) \<and> obj_at' Q ptr s \<and> (\<forall>tcb_x. Q tcb_x \<longrightarrow> P' (KOTCB (F tcb_x)) = P' (KOTCB tcb_x)) \<Longrightarrow> tcb_at' ptr s \<longrightarrow> (\<exists>t. (ptr = p \<longrightarrow> ko_at' t p s \<and> P (ko_wp_at' (\<lambda>y. P' (KOTCB (F t))) p s)) \<and> (ptr \<noteq> p \<longrightarrow> ko_at' t ptr s)) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_ko_wp_at2:
  "\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO ko + gbits) n \<and> n \<noteq> 0
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> P (ko_wp_at' P' p s)
      \<and> (P' ko \<longrightarrow> P True)
      \<and> pspace_no_overlap' ptr sz s\<rbrace>
    createObjects ptr n ko gbits
   \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace>" apply (simp add: createObjects_def) apply (wp createObjects_orig_ko_wp_at2') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO ko + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' ko \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO ko + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' ko \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n ko gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO ko + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (objBitsKO ko + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' ko \<longrightarrow> P True) \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> range_cover ptr ?sz3 (objBitsKO ko + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' P' p s) \<and> (P' ko \<longrightarrow> P True) \<and> pspace_no_overlap' ptr ?sz3 s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createNewCaps_obj_at':
  "\<lbrace>\<lambda>s. obj_at' (P :: ('a :: pspace_storable) \<Rightarrow> bool) p s
       \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0
       \<and> pspace_aligned' s \<and> pspace_distinct' s
       \<and> pspace_no_overlap' ptr sz s
       \<and> koType(TYPE('a)) \<noteq> koType(TYPE(pde))
       \<and> (\<forall>tcb d. \<not>tcbQueued tcb \<and> tcbState tcb = Inactive \<longrightarrow> ((\<exists>obj :: 'a. injectKOS obj = KOTCB (tcb\<lparr>tcbDomain := d\<rparr>) \<and> P obj) \<longleftrightarrow> (\<exists>obj :: 'a. injectKOS obj = KOTCB tcb \<and> P obj)))\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. obj_at' P p s\<rbrace>" by (wp createNewCaps_obj_at'', auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' P p s \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> koType TYPE('a) \<noteq> koType TYPE(ARM_H.pde) \<and> (\<forall>tcb d. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> P obj) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> P obj))\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>
theory Retype_R

lemma createObjects_nosch'[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
     createObjects' ptr n val gbits
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" by (rule createObjects_pspace_only, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
theory Retype_R

lemma koTypeOf_eq_UserDataT:
  "(koTypeOf ko = UserDataT)
        = (ko = KOUserData)" by (cases ko, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (koTypeOf ko = UserDataT) = (ko = KOUserData)
theory Retype_R

lemma valid_irq_node_lift_asm:
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>"
  assumes y: "\<And>p. \<lbrace>real_cte_at' p and Q\<rbrace> f \<lbrace>\<lambda>rv. real_cte_at' p\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s \<and> Q s\<rbrace> f \<lbrace>\<lambda>rv s. valid_irq_node' (irq_node' s) s\<rbrace>" apply (simp add: valid_irq_node'_def) apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node' [OF x]) apply (wp hoare_vcg_all_lift y) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s \<and> Q s\<rbrace> f \<lbrace>\<lambda>rv s. valid_irq_node' (irq_node' s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s) \<and> Q s\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s)\<rbrace>
 2. \<And>s. is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s) \<and> Q s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>fa. \<lbrace>?P3 fa\<rbrace> f \<lbrace>\<lambda>rv s. is_aligned fa (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (fa + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s)\<rbrace>
 2. \<And>s. is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s) \<and> Q s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s) \<and> Q s \<Longrightarrow> is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>x. (real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) x << cteSizeBits)) and Q) s) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma valid_irq_handlers_cte_wp_at_form':
  "valid_irq_handlers' = (\<lambda>s. \<forall>irq. irq_issued' irq s \<or>
                               (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = IRQHandlerCap irq) p s))" by (auto simp: valid_irq_handlers'_def cteCaps_of_def cte_wp_at_ctes_of
                 fun_eq_iff ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers' = (\<lambda>s. \<forall>irq. irq_issued' irq s \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s))
theory Retype_R

lemma createNewCaps_irq_handlers':
  "\<lbrace>valid_irq_handlers' and pspace_no_overlap' ptr sz
       and pspace_aligned' and pspace_distinct'
       and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: valid_irq_handlers_cte_wp_at_form' irq_issued'_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             createNewCaps_cte_wp_at2) apply (clarsimp simp: makeObject_cte) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers' and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s)) and pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> \<forall>x. intStateIRQTable (ksInterruptState s) x = irqstate.IRQSignal \<or> (\<forall>xa. \<not> cte_wp_at' (\<lambda>a. cteCap a = capability.IRQHandlerCap x) xa s \<and> cteCap makeObject \<noteq> capability.IRQHandlerCap x \<and> n \<noteq> 0 \<and> range_cover ptr (?sz6 x xa) (APIType_capBits ty us) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz6 x xa) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal \<or> (\<forall>p. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap irq) p s); pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; intStateIRQTable (ksInterruptState s) x \<noteq> irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<not> cte_wp_at' (\<lambda>a. cteCap a = capability.IRQHandlerCap x) xa s \<and> range_cover ptr (?sz6 x xa) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz6 x xa) s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma valid_pde_mappings'_def3:
  "valid_pde_mappings' =
     (\<lambda>s. \<forall>x. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s)" apply (simp add: valid_pde_mappings'_def) apply (rule ext, rule iff_allI) apply (auto simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde_mappings' = (\<lambda>s. \<forall>x. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) = (\<lambda>s. \<forall>x. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. (\<forall>pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) = (\<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_pde_mappings'[wp]:
  "\<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (objBitsKO ko + gbits) n  \<and> n \<noteq> 0
            \<and> pspace_aligned' s \<and> pspace_distinct' s
            \<and> pspace_no_overlap' ptr sz s
            \<and> (\<forall>pde. projectKO_opt ko = Some pde \<longrightarrow> pde = InvalidPDE)\<rbrace>
       createObjects ptr n ko gbits
   \<lbrace>\<lambda>_. valid_pde_mappings'\<rbrace>" by (simp add: createObjects_def objBits_def | intro conjI | wp | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (objBitsKO ko + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>pde. projectKO_opt ko = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>_. valid_pde_mappings'\<rbrace>
theory Retype_R

lemma getObject_valid_pde_mapping':
  "\<lbrace>valid_pde_mappings' and K (p && mask pdBits = p')\<rbrace> getObject p \<lbrace>\<lambda>pde s. valid_pde_mapping' p' pde\<rbrace>" apply (wp getPDE_wp) apply (clarsimp simp: valid_pde_mappings'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings' and K (p && mask pdBits = p')\<rbrace> getObject p \<lbrace>\<lambda>pde s. valid_pde_mapping' p' pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_pde_mappings' and K (p && mask pdBits = p')) s \<Longrightarrow> \<forall>ko. ko_at' ko p s \<longrightarrow> valid_pde_mapping' p' ko proof (prove)
goal:
No subgoals!
theory Retype_R

lemma mapM_x_copyGlobalMappings_pde_mappings':
  "\<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
        and K (\<forall>x \<in> set xs. is_aligned x pdBits)\<rbrace>
      mapM_x copyGlobalMappings xs \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post) apply (rule mapM_x_wp [OF _ subset_refl]) apply (wp copyGlobalMappings_pde_mappings' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (\<forall>x\<in>set xs. is_aligned x pdBits)\<rbrace> mapM_x copyGlobalMappings xs \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. is_aligned x pdBits \<Longrightarrow> \<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)\<rbrace> mapM_x copyGlobalMappings xs \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set xs. is_aligned x pdBits \<Longrightarrow> \<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)\<rbrace> mapM_x copyGlobalMappings xs \<lbrace>?Q2\<rbrace>
 2. \<And>rv s. \<lbrakk>\<forall>x\<in>set xs. is_aligned x pdBits; ?Q2 rv s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>set xs. is_aligned x pdBits; x \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)\<rbrace> copyGlobalMappings x \<lbrace>\<lambda>rv. valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)\<rbrace>
 2. \<And>rv s. \<lbrakk>\<forall>x\<in>set xs. is_aligned x pdBits; (valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)) s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects'_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> createObjects' a b c d \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" apply (simp add: createObjects'_def split_def) apply (wp unless_wp|wpc|simp add: alignError_def)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> createObjects' a b c d \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> do y <- unless (a && mask (objBitsKO c + d) = 0) (alignError (objBitsKO c + d));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (a + word_of_nat (shiftL b (objBitsKO c + d) - Suc 0)) ps) of None \<Rightarrow> return () | Some aa \<Rightarrow> assert (fst aa < a);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> c)) (map (\<lambda>n. a + (n << objBitsKO c)) [0 .e. (word_of_nat b << d) - 1]) ps))
od \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> a && mask (objBitsKO c + d) \<noteq> 0 \<longrightarrow> ?Q32 s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma copyGlobalMappings_inv[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace>
    copyGlobalMappings newPD
   \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>" by (simp add: copyGlobalMappings_def storePDE_def split_def
      | wp mapM_x_wp_inv setObject_ksMachine updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> copyGlobalMappings newPD \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>
theory Retype_R

lemma doMachineOp_return_foo:
  "doMachineOp (do x\<leftarrow>a;return () od) = (do (doMachineOp a); return () od)" apply (clarsimp simp: doMachineOp_def bind_def gets_def
                        get_def return_def select_f_def split_def simpler_modify_def) apply (rule ext)+ apply simp apply (rule set_eqI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (do x <- a;
return ()
od) = do doMachineOp a;
return ()
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union>x\<in>(\<Union>x\<in>fst (a (ksMachineState s)). {((), snd x)}) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}, snd (a (ksMachineState s)))) = (\<lambda>s. (\<Union>x\<in>fst (a (ksMachineState s)) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}, snd (a (ksMachineState s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>(\<Union>x\<in>fst (a (ksMachineState s)). {((), snd x)}) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}, snd (a (ksMachineState s))) = (\<Union>x\<in>fst (a (ksMachineState s)) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}, snd (a (ksMachineState s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>(\<Union>x\<in>fst (a (ksMachineState s)). {((), snd x)}) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}) = (\<Union>x\<in>fst (a (ksMachineState s)) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}) proof (prove)
goal (1 subgoal):
 1. \<And>s x. (x \<in> (\<Union>x\<in>(\<Union>x\<in>fst (a (ksMachineState s)). {((), snd x)}) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)})) = (x \<in> (\<Union>x\<in>fst (a (ksMachineState s)) \<times> {s}. {((), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)})) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma doMachineOp_mapM_x_wp:
  assumes empty_fail:"\<And>x. empty_fail (f x)"
  assumes valid: "\<And>z. \<lbrace>P\<rbrace> doMachineOp (f z) \<lbrace>\<lambda>y. P\<rbrace>"
  shows "\<lbrace>P\<rbrace> doMachineOp (mapM_x f xs) \<lbrace>\<lambda>y. P\<rbrace>" apply (clarsimp simp: mapM_x_mapM doMachineOp_return_foo) apply (subst doMachineOp_mapM) apply (wp valid empty_fail mapM_wp' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doMachineOp (mapM_x f xs) \<lbrace>\<lambda>y. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do y <- doMachineOp (mapM f xs);
return ()
od \<lbrace>\<lambda>y. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. empty_fail (f x)
 2. \<lbrace>P\<rbrace> do y <- mapM (doMachineOp \<circ> f) xs;
return ()
od \<lbrace>\<lambda>y. P\<rbrace> proof (prove)
goal:
No subgoals!