kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_R

lemma caps_contained_n: "caps_contained' n" proof - from valid have "caps_contained' m" .. thus ?thesis apply (clarsimp simp: caps_contained'_def) apply (simp add: n_Some_eq split: if_split_asm) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_contained' n proof (state)
goal (1 subgoal):
 1. caps_contained' n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. caps_contained' m proof (state)
this:
caps_contained' m

goal (1 subgoal):
 1. caps_contained' n proof (prove)
using this:
caps_contained' m

goal (1 subgoal):
 1. caps_contained' n proof (prove)
goal (1 subgoal):
 1. \<And>p p' c na c' n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); n p = Some (CTE c na); n p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x. \<lbrakk>\<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); \<not> P p; m p = Some (CTE c n); \<not> P p'; m p' = Some (CTE c' n')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals! proof (state)
this:
caps_contained' n

goal:
No subgoals!
theory Retype_R

lemma descendants [simp]:
  "descendants_of' p n = descendants_of' p m" apply (unfold n_def) apply (subst descendants_of_retype') apply (erule P) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n = descendants_of' p m proof (prove)
goal (1 subgoal):
 1. descendants_of' p (\<lambda>p. if P p then Some makeObject else m p) = descendants_of' p m proof (prove)
goal (2 subgoals):
 1. \<And>p. P p \<Longrightarrow> m p = None
 2. descendants_of' p m = descendants_of' p m proof (prove)
goal (1 subgoal):
 1. descendants_of' p m = descendants_of' p m proof (prove)
goal:
No subgoals!
theory Retype_R

lemma valid_nullcaps_n: "valid_nullcaps n" proof - from valid have "valid_nullcaps m" .. thus ?thesis apply (clarsimp simp: valid_nullcaps_def) apply (simp add: n_Some_eq split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_nullcaps n proof (state)
goal (1 subgoal):
 1. valid_nullcaps n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_nullcaps m proof (state)
this:
valid_nullcaps m

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
using this:
valid_nullcaps m

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; n p = Some (CTE capability.NullCap na)\<rbrakk> \<Longrightarrow> na = nullMDBNode proof (prove)
goal:
No subgoals! proof (state)
this:
valid_nullcaps n

goal:
No subgoals!
theory Retype_R

lemma ut_rev_n: "ut_revocable' n" proof - from valid have "ut_revocable' m" .. thus ?thesis apply (clarsimp simp: ut_revocable'_def) apply (simp add: n_Some_eq split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ut_revocable' n proof (state)
goal (1 subgoal):
 1. ut_revocable' n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. ut_revocable' m proof (state)
this:
ut_revocable' m

goal (1 subgoal):
 1. ut_revocable' n proof (prove)
using this:
ut_revocable' m

goal (1 subgoal):
 1. ut_revocable' n proof (prove)
goal (1 subgoal):
 1. \<And>p cap na. \<lbrakk>\<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; n p = Some (CTE cap na); isUntypedCap cap\<rbrakk> \<Longrightarrow> mdbRevocable na proof (prove)
goal:
No subgoals! proof (state)
this:
ut_revocable' n

goal:
No subgoals!
theory Retype_R

lemma class_links_m:
  "class_links m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. class_links m
theory Retype_R

lemma next_not_P2:
  "\<lbrakk> m \<turnstile> p \<leadsto> p'; p' \<noteq> nullPointer \<rbrakk> \<Longrightarrow> \<not> P p'" using dlist apply (clarsimp simp: mdb_next_unfold) apply (erule(1) valid_dlistE) apply clarsimp apply (clarsimp dest!: P) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> p'; p' \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<not> P p' proof (prove)
using this:
valid_dlist m

goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> p'; p' \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<not> P p' proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> nullPointer; valid_dlist m; m p = Some z; p' = mdbNext (cteMDBNode z); P (mdbNext (cteMDBNode z))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> nullPointer; m p = Some z; p' = mdbNext (cteMDBNode z); P (mdbNext (cteMDBNode z))\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 2. \<And>z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> nullPointer; m p = Some z; p' = mdbNext (cteMDBNode z); P (mdbNext (cteMDBNode z)); m (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z cte'. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> nullPointer; m p = Some z; p' = mdbNext (cteMDBNode z); P (mdbNext (cteMDBNode z)); m (mdbNext (cteMDBNode z)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_R

lemma irq_control_n:
  "irq_control n" apply (clarsimp simp add: irq_control_def) apply (simp add: n_Some_eq split: if_split_asm) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (erule (1) irq_controlD, rule irq_control) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control n proof (prove)
goal (1 subgoal):
 1. \<And>p na. n p = Some (CTE capability.IRQControlCap na) \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<not> P p; m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. \<not> P p' \<and> (\<not> P p' \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<not> P p; m p = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. \<not> P p' \<and> (\<not> P p' \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n p' n'. \<lbrakk>\<not> P p; m p = Some (CTE capability.IRQControlCap n); mdbRevocable n; \<not> P p'; m p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!
theory Retype_R

lemma dist_z_m: "distinct_zombies m" using valid by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_zombies m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. distinct_zombies m
theory Retype_R

lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m" using valid by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. reply_masters_rvk_fb m
theory Retype_R

lemma reply_masters_rvk_fb_n: "reply_masters_rvk_fb n" using reply_masters_rvk_fb_m by (simp add: n_def reply_masters_rvk_fb_def
                ball_ran_eq makeObject_cte isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb n proof (prove)
using this:
reply_masters_rvk_fb m

goal (1 subgoal):
 1. reply_masters_rvk_fb n
theory Retype_R

lemma valid_n:
  "valid_mdb_ctes n" by (simp add: valid_mdb_ctes_def dlist_n no_0_n mdb_chain_0_n
                valid_badges_n caps_contained_n untyped_mdb_n
                untyped_inc_n mdb_chunked_n valid_nullcaps_n ut_rev_n
                class_links_n irq_control_n dist_z_n
                reply_masters_rvk_fb_n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes n
theory Retype_R

lemma obj_range'_subset:
  "\<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val)\<rbrakk>
   \<Longrightarrow> obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}" unfolding obj_range'_def by (rule new_range_subset, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val)\<rbrakk> \<Longrightarrow> obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val)\<rbrakk> \<Longrightarrow> {ptr'..ptr' + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
theory Retype_R

lemma caps_no_overlapD'':
  "\<lbrakk>cte_wp_at' (\<lambda>cap. cteCap cap = c) q s;caps_no_overlap'' ptr sz s\<rbrakk>
   \<Longrightarrow> untypedRange c \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow>
       {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange c" apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps caps_no_overlap''_def
        simp del:atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff) apply (drule_tac x = cte in bspec) apply fastforce apply (erule(1) impE) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cap. cteCap cap = c) q s; caps_no_overlap'' ptr sz s\<rbrakk> \<Longrightarrow> untypedRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>\<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s q = Some cte; c = cteCap cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>ctes_of s q = Some cte; c = cteCap cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> cte \<in> ran (ctes_of s)
 2. \<And>cte x. \<lbrakk>ctes_of s q = Some cte; c = cteCap cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>ctes_of s q = Some cte; c = cteCap cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>ctes_of s q = Some cte; c = cteCap cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_valid_pspace_untyped':
  assumes  mko: "makeObjectKO dev ty = Some val"
  and    not_0: "n \<noteq> 0"
  and    cover: "range_cover ptr sz (objBitsKO val + gbits) n"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0
            \<and> caps_overlap_reserved' {ptr .. ptr + of_nat (n * 2^gbits * 2 ^ objBitsKO val ) - 1} s \<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" apply (wp createObjects_valid_pspace' [OF mko not_0 cover]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<Longrightarrow> pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> ptr \<noteq> 0 proof (prove)
goal:
No subgoals!
theory Retype_R

lemma getObject_valid_pde'[wp]:
  "\<lbrace>valid_objs'\<rbrace> getObject x \<lbrace>valid_pde'\<rbrace>" apply (rule hoare_chain) apply (rule hoare_vcg_conj_lift) apply (rule getObject_ko_at, simp) apply (simp add: objBits_simps archObjSize_def pdeBits_def) apply (rule getObject_inv[where P=valid_objs']) apply (simp add: loadObject_default_inv) apply simp apply (clarsimp simp: projectKOs valid_obj'_def dest!: obj_at_valid_objs') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> getObject x \<lbrace>valid_pde'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> getObject x \<lbrace>?Q\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> valid_pde' rv s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P4\<rbrace> getObject x \<lbrace>?Q4\<rbrace>
 2. \<lbrace>?P'4\<rbrace> getObject x \<lbrace>?Q'4\<rbrace>
 3. \<And>s. valid_objs' s \<Longrightarrow> ?P4 s \<and> ?P'4 s
 4. \<And>rv s. ?Q4 rv s \<and> ?Q'4 rv s \<Longrightarrow> valid_pde' rv s proof (prove)
goal (4 subgoals):
 1. \<And>v. 1 < 2 ^ objBits v
 2. \<lbrace>?P'4\<rbrace> getObject x \<lbrace>?Q'4\<rbrace>
 3. \<And>s. valid_objs' s \<Longrightarrow> True \<and> ?P'4 s
 4. \<And>rv s. ko_at' rv x s \<and> ?Q'4 rv s \<Longrightarrow> valid_pde' rv s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'4\<rbrace> getObject x \<lbrace>?Q'4\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> ?P'4 s
 3. \<And>rv s. ko_at' rv x s \<and> ?Q'4 rv s \<Longrightarrow> valid_pde' rv s proof (prove)
goal (3 subgoals):
 1. \<And>p q n ko. \<lbrace>valid_objs'\<rbrace> loadObject p q n ko \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> valid_objs' s
 3. \<And>rv s. ko_at' rv x s \<and> valid_objs' s \<Longrightarrow> valid_pde' rv s proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_objs' s \<Longrightarrow> True \<and> valid_objs' s
 2. \<And>rv s. ko_at' rv x s \<and> valid_objs' s \<Longrightarrow> valid_pde' rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. ko_at' rv x s \<and> valid_objs' s \<Longrightarrow> valid_pde' rv s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma copyGlobalMappings_valid_pspace[wp]:
  "\<lbrace>valid_pspace'\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" by (simp add: valid_pspace'_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace'\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>
theory Retype_R

lemma createObjects_orig_obj_at2':
  "\<lbrace>\<lambda>s. n \<noteq> 0
      \<and> range_cover ptr sz (objBitsKO val + gbits) n
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> P (obj_at' P' p s)
      \<and> \<not> (case_option False P' (projectKO_opt val))
      \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (obj_at' P' p s)\<rbrace>" unfolding obj_at'_real_def by (wp createObjects_orig_ko_wp_at2') auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (obj_at' P' p s) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> P' x) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (obj_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> P (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P' obj) p s) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> P' x) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P' obj) p s)\<rbrace>
theory Retype_R

lemma createObjects_obj_at_other:
  assumes cover: "range_cover ptr sz (objBitsKO val + gbits) n"
  and     not_0: "n\<noteq> 0"
  shows  "\<lbrace>\<lambda>s. obj_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects ptr n val gbits \<lbrace>\<lambda>_. obj_at' P p\<rbrace>" apply (simp add: createObjects_def) apply (wp createObjects_orig_obj_at'[where sz = sz]) using cover not_0 apply (clarsimp simp: cover not_0 valid_pspace'_def pspace_no_overlap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>_. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' P p s \<and> pspace_no_overlap' ptr sz s proof (prove)
using this:
range_cover ptr sz (objBitsKO val + gbits) n
n \<noteq> 0

goal (1 subgoal):
 1. \<And>s. obj_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' P p s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createNewCaps_cte_wp_at:
  assumes cover: "range_cover ptr sz (APIType_capBits ty us) n"
  and not_0 : "n \<noteq> 0"
  shows "\<lbrace>\<lambda>s. cte_wp_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createNewCaps ty ptr n us dev
  \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>" apply (wp createNewCaps_cte_wp_at') apply (auto simp: cover not_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> cte_wp_at' P p s \<and> range_cover ptr ?sz1 (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz1 s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma state_refs_ko_wp_at_eq:
  "state_refs_of' s = (\<lambda>x. {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s})" apply (rule ext) apply (simp add: state_refs_of'_def ko_wp_at'_def
            split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of' s = (\<lambda>x. {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s}) proof (prove)
goal (1 subgoal):
 1. \<And>x. state_refs_of' s x = {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s} proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_pspace_only:
  "\<lbrakk> \<And>f s. P (ksPSpace_update f s) = P s \<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: createObjects_def createObjects'_def unless_def alignError_def
                   split_def lookupAround2_pspace_no) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>f s. P (ksPSpace_update f s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>f s. P (ksPSpace_update f s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> do y <- when (ptr && mask (objBitsKO val + gbits) \<noteq> 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL n (objBitsKO val + gbits) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat n << gbits) - 1]) ps))
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_R

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

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

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

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

lemma threadSet_qsL2[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>" by (simp add: threadSet_def | wp updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>