kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_R

lemma szw: "sz < word_bits" using cte_wp_at_valid_objs_valid_cap'[OF cte_wp_at'] misc by (clarsimp simp: valid_cap_simps' capAligned_def invs_valid_objs')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz < word_bits proof (prove)
using this:
valid_objs' s \<Longrightarrow> \<exists>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx \<and> valid_cap' (cteCap cte) s
ct_active' s
invs' s

goal (1 subgoal):
 1. sz < word_bits
theory Untyped_R

lemma idx_le_new_offs:
  "\<not> reset
   \<longrightarrow> idx \<le> unat ((ptr && mask sz) + (of_nat (length slots) * 2 ^ (APIType_capBits tp us)))" using misc idx_cases range_cover.range_cover_base_le[OF cover] apply (clarsimp simp only: simp_thms) apply (erule order_trans) apply (simp add: word_le_nat_alt[symmetric]
                   shiftl_t2n mult.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> reset \<longrightarrow> idx \<le> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) proof (prove)
using this:
ct_active' s
invs' s
\<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz
ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat (length slots) << APIType_capBits tp us)

goal (1 subgoal):
 1. \<not> reset \<longrightarrow> idx \<le> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; idx \<le> unat (ptr - (ptr && ~~ mask sz)); ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat (length slots) << APIType_capBits tp us); \<not> reset\<rbrakk> \<Longrightarrow> idx \<le> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat (length slots) << APIType_capBits tp us); \<not> reset\<rbrakk> \<Longrightarrow> unat (ptr - (ptr && ~~ mask sz)) \<le> unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh" by (simp add: valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh
theory Untyped_R

lemma deleteObjects_ksCurThread[wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" apply (simp add: deleteObjects_def3) apply (wp | simp add: doMachineOp_def split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do y <- assert (is_aligned ptr sz);
y <- stateAssert (deletionIsSafe ptr sz) [];
y <- doMachineOp (freeMemory ptr sz);
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ sz - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma ex_tupI:
  "P (fst x) (snd x) \<Longrightarrow> \<exists>a b. P a b" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (fst x) (snd x) \<Longrightarrow> \<exists>a b. P a b
theory Untyped_R

lemma ex_cte_cap_wp_to_irq_state_independent_H[simp]:
  "irq_state_independent_H (ex_cte_cap_wp_to' P slot)" by (simp add: ex_cte_cap_wp_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_H (ex_cte_cap_wp_to' P slot)
theory Untyped_R

lemma updateFreeIndex_ctes_of:
  "\<lbrace>\<lambda>s.  P (modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx))))\<rbrace>
    updateFreeIndex ptr idx
  \<lbrace>\<lambda>r s.  P (ctes_of s)\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def getSlotCap_def) apply (wp updateCap_ctes_of_wp getCTE_wp' | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule rsubst[where P=P]) apply (case_tac cte) apply (clarsimp simp: modify_map_def fun_eq_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx))))\<rbrace> updateFreeIndex ptr idx \<lbrace>\<lambda>r s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx))))\<rbrace> do y <- do cte <- getCTE ptr;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cte <- getCTE ptr;
updateCap ptr (capFreeIndex_update (\<lambda>_. idx) (cteCap cte))
od \<lbrace>\<lambda>r s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx)))) \<Longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) ptr s) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) ptr s \<longrightarrow> P (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P (modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx)))); ctes_of s ptr = Some cte\<rbrakk> \<Longrightarrow> P (modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. ctes_of s ptr = Some cte \<Longrightarrow> modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx))) = modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x1 x2. \<lbrakk>ctes_of s ptr = Some cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> modify_map (ctes_of s) ptr (cteCap_update (capFreeIndex_update (\<lambda>_. idx))) = modify_map (ctes_of s) ptr (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte))) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma setCTE_ct_in_state:
  "\<lbrace>ct_in_state' P\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" apply (rule hoare_name_pre_state) apply (rule hoare_pre, wp ct_in_state'_decomp setCTE_pred_tcb_at') apply (auto simp: ct_in_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_state' P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>ct_in_state' P s; s = sa\<rbrakk> \<Longrightarrow> st_tcb_at' P (?t6 s) sa \<and> ?t6 s = ksCurThread sa proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma (in range_cover) funky_aligned:
  "is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit" apply (rule aligned_add_aligned) apply (rule is_aligned_andI1) apply (rule aligned) apply (rule is_aligned_mult_triv2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit proof (prove)
goal (3 subgoals):
 1. is_aligned (ptr && foo) ?n
 2. is_aligned (v * 2 ^ sbit) sbit
 3. sbit \<le> ?n proof (prove)
goal (3 subgoals):
 1. is_aligned ptr ?n
 2. is_aligned (v * 2 ^ sbit) sbit
 3. sbit \<le> ?n proof (prove)
goal (2 subgoals):
 1. is_aligned (v * 2 ^ sbit) sbit
 2. sbit \<le> sbit proof (prove)
goal (1 subgoal):
 1. sbit \<le> sbit proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_valid_pspace':
  "\<lbrace>\<lambda>s. valid_pspace' s \<and> s \<turnstile>' cap
          \<and> slot \<noteq> parent \<and> caps_overlap_reserved' (untypedRange cap) s
          \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                              sameRegionAs (cteCap cte) cap) parent s
          \<and> \<not> isZombie cap \<and> descendants_range' cap parent (ctes_of s)\<rbrace>
     insertNewCap parent slot cap
   \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (simp add: valid_pspace'_def) apply (wp insertNewCap_valid_mdb) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> valid_cap' cap s \<and> slot \<noteq> parent \<and> caps_overlap_reserved' (untypedRange cap) s \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent s \<and> \<not> isZombie cap \<and> descendants_range' cap parent (ctes_of s)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> valid_cap' cap s \<and> slot \<noteq> parent \<and> caps_overlap_reserved' (untypedRange cap) s \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent s \<and> \<not> isZombie cap \<and> descendants_range' cap parent (ctes_of s)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> valid_cap' cap s \<and> slot \<noteq> parent \<and> caps_overlap_reserved' (untypedRange cap) s \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent s \<and> \<not> isZombie cap \<and> descendants_range' cap parent (ctes_of s) \<Longrightarrow> (valid_objs' and valid_cap' cap and pspace_aligned' and pspace_distinct') s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> (valid_mdb' and valid_objs' and K (slot \<noteq> parent) and caps_overlap_reserved' (untypedRange cap) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent and K (\<not> isZombie cap) and valid_cap' cap and (\<lambda>s. descendants_range' cap parent (ctes_of s))) s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: insertNewCap_def) apply (wp setCTE_iflive' getCTE_wp') apply (clarsimp elim!: cte_wp_at_weakenE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) parent s \<longrightarrow> ((\<lambda>next s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> cteCap cte = capability.NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap (CTE cap (MDB next parent True True))). ko_wp_at' (Not \<circ> live') p' s) slot s \<and> if_live_then_nonz_cap' s) \<circ> (mdbNext \<circ> cteMDBNode)) cte s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_cte_wp_at'':
  "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and K (\<not> P NullCap)\<rbrace>
     insertNewCap parent slot cap
   \<lbrace>\<lambda>rv s. cte_wp_at' (P \<circ> cteCap) p s\<rbrace>" apply (simp add: insertNewCap_def tree_cte_cteCap_eq) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and K (\<not> P capability.NullCap)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. cte_wp_at' (P \<circ> cteCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and (\<lambda>y. \<not> P capability.NullCap)\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and (\<lambda>y. \<not> P capability.NullCap)) s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) parent s \<longrightarrow> ((\<lambda>next s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> cteCap cte = capability.NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> (case ((cteCaps_of s)(slot \<mapsto> cteCap (CTE cap (MDB next parent True True)))) p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2)) \<circ> (mdbNext \<circ> cteMDBNode)) cte s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_cap_to'[wp]:
  "\<lbrace>ex_cte_cap_to' p\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. ex_cte_cap_to' p\<rbrace>" apply (simp add: ex_cte_cap_to'_def) apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node'[OF insertNewCap_ksInterrupt]) apply (wp hoare_vcg_ex_lift insertNewCap_cte_wp_at') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace>
 2. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) f) cref s\<rbrace>
 2. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> \<exists>x. (cte_wp_at' (\<lambda>cte. p \<in> cte_refs' (cteCap cte) (irq_node' s)) x and K (p \<notin> cte_refs' capability.NullCap (irq_node' s))) s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_nullcap:
  "\<lbrace>P and cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) slot\<rbrace> insertNewCap parent slot cap \<lbrace>Q\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace> insertNewCap parent slot cap \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def) apply (subgoal_tac "cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) slot s") apply fastforce apply (clarsimp simp: insertNewCap_def in_monad cte_wp_at_ctes_of liftM_def
                 dest!: use_valid [OF _ getCTE_sp[where P="(=) s" for s], OF _ refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot\<rbrace> insertNewCap parent slot cap \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> insertNewCap parent slot cap \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<forall>s. P s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s \<longrightarrow> (\<forall>x\<in>fst (insertNewCap parent slot cap s). case x of (x, xa) \<Rightarrow> Q x xa); P s; ((), b) \<in> fst (insertNewCap parent slot cap s)\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>\<forall>s. P s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s \<longrightarrow> (\<forall>x\<in>fst (insertNewCap parent slot cap s). case x of (x, xa) \<Rightarrow> Q x xa); P s; ((), b) \<in> fst (insertNewCap parent slot cap s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s\<rbrakk> \<Longrightarrow> Q () b
 2. \<And>s b. \<lbrakk>\<forall>s. P s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s \<longrightarrow> (\<forall>x\<in>fst (insertNewCap parent slot cap s). case x of (x, xa) \<Rightarrow> Q x xa); P s; ((), b) \<in> fst (insertNewCap parent slot cap s)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<forall>s. P s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s \<longrightarrow> (\<forall>x\<in>fst (insertNewCap parent slot cap s). case x of (x, xa) \<Rightarrow> Q x xa); P s; ((), b) \<in> fst (insertNewCap parent slot cap s)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain' and ct_active'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" apply (wp ct_idle_or_in_cur_domain'_lift_futz[where Q=\<top>]) apply (rule_tac Q="\<lambda>_. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive) t and obj_at' (\<lambda>tcb. d = tcbDomain tcb) t"
             in hoare_strengthen_post) apply (wp | clarsimp elim: obj_at'_weakenE)+ apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and ct_active'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>d t. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s \<and> True\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t\<rbrace>
 2. \<And>s. (ct_idle_or_in_cur_domain' and ct_active') s \<Longrightarrow> (ct_idle_or_in_cur_domain' and ct_active' and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>d t. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s \<and> True\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive) t and obj_at' (\<lambda>tcb. d = tcbDomain tcb) t\<rbrace>
 2. \<And>d t rv s. (obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive) t and obj_at' (\<lambda>tcb. d = tcbDomain tcb) t) s \<Longrightarrow> obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s
 3. \<And>s. (ct_idle_or_in_cur_domain' and ct_active') s \<Longrightarrow> (ct_idle_or_in_cur_domain' and ct_active' and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>d t s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s \<Longrightarrow> obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive) t s \<and> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s
 2. \<And>d t rv s. (obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive) t and obj_at' (\<lambda>tcb. d = tcbDomain tcb) t) s \<Longrightarrow> obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s
 3. \<And>s. (ct_idle_or_in_cur_domain' and ct_active') s \<Longrightarrow> (ct_idle_or_in_cur_domain' and ct_active' and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_irq_issued'[wp]:
  "\<lbrace>\<lambda>s. P (irq_issued' irq s)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. P (irq_issued' irq s)\<rbrace>" by (simp add: irq_issued'_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_issued' irq s)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. P (irq_issued' irq s)\<rbrace>
theory Untyped_R

lemma insertNewCap_ct_in_state'[wp]:
  "\<lbrace>ct_in_state' p\<rbrace>insertNewCap parent slot cap \<lbrace>\<lambda>rv. ct_in_state' p\<rbrace>" unfolding ct_in_state'_def apply (rule hoare_pre) apply wps apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' p\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. ct_in_state' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' p (ksCurThread s) s\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. st_tcb_at' p (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. st_tcb_at' p (ksCurThread s) s\<rbrace>
 2. \<And>s. st_tcb_at' p (ksCurThread s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. st_tcb_at' p (ksCurThread prev_s)\<rbrace>
 2. \<And>s. st_tcb_at' p (ksCurThread s) s \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' p (ksCurThread s) s \<Longrightarrow> st_tcb_at' p (ksCurThread s) s proof (prove)
goal:
No subgoals!