kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma valid_nullcaps_next:
  "\<lbrakk> m (mdbNext n) = Some (CTE NullCap n'); m p = Some (CTE c n);
    no_0 m; valid_dlist m; valid_nullcaps m \<rbrakk> \<Longrightarrow> False" apply (erule (1) valid_nullcapsE) apply (erule_tac p=p in valid_dlistEn, assumption) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbNext n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; valid_dlist m; valid_nullcaps m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbNext n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; valid_dlist m; mdbPrev n' = 0; mdbNext n' = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbNext n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; mdbPrev n' = 0; mdbNext n' = 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE c n)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>m (mdbNext n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; mdbPrev n' = 0; mdbNext n' = 0; m (mdbNext (cteMDBNode (CTE c n))) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbNext n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; mdbPrev n' = 0; mdbNext n' = 0; m (mdbNext (cteMDBNode (CTE c n))) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setupReplyMaster_valid_pspace':
  "\<lbrace>valid_pspace' and tcb_at' t\<rbrace>
     setupReplyMaster t
   \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (simp add: valid_pspace'_def) apply (wp setupReplyMaster_valid_mdb) apply (simp_all add: valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and tcb_at' t\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. ?slot13 = t + 2 ^ objBits undefined * tcbReplySlot
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t) s \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> (valid_mdb' and valid_pspace' and tcb_at' t) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setupReplyMaster_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: setupReplyMaster_def locateSlot_conv) 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> setupReplyMaster t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
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) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (if cteCap cte = capability.NullCap then \<lambda>s. noReplyCapsFor t s \<longrightarrow> cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))). ko_wp_at' (Not \<circ> live') p' s) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<and> if_live_then_nonz_cap' s else if_live_then_nonz_cap') s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma ex_nonz_tcb_cte_caps':
  "\<lbrakk>ex_nonz_cap_to' t s; tcb_at' t s; valid_objs' s; sl \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow>
   ex_cte_cap_to' (t + sl) s" apply (clarsimp simp: ex_nonz_cap_to'_def ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (subgoal_tac "s \<turnstile>' cteCap cte") apply (rule_tac x=cref in exI, rule_tac x=cte in exI) apply (clarsimp simp: valid_cap'_def obj_at'_def projectKOs dom_def
                  split: cte.split_asm capability.split_asm) apply (case_tac cte) apply (clarsimp simp: ctes_of_valid_cap') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to' t s; tcb_at' t s; valid_objs' s; sl \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) (t + sl) s proof (prove)
goal (1 subgoal):
 1. \<And>cref a b cte. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> \<exists>cref cte. ctes_of s cref = Some cte \<and> t + sl \<in> cte_refs' (cteCap cte) (irq_node' s) proof (prove)
goal (2 subgoals):
 1. \<And>cref a b cte. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> \<exists>cref cte. ctes_of s cref = Some cte \<and> t + sl \<in> cte_refs' (cteCap cte) (irq_node' s)
 2. \<And>cref a b cte. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (2 subgoals):
 1. \<And>cref a b cte. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> ctes_of s cref = Some cte \<and> t + sl \<in> cte_refs' (cteCap cte) (irq_node' s)
 2. \<And>cref a b cte. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>cref a b cte. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>cref a b cte x1 x2. \<lbrakk>tcb_at' t s; valid_objs' s; tcb_cte_cases sl = Some (a, b); ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_irq_handlers':
  "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (\<forall>irq. cteCap cte = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace>
     setCTE ptr cte
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: valid_irq_handlers'_def cteCaps_of_def irq_issued'_def) apply (wp hoare_use_eq [where f=ksInterruptState, OF setCTE_ksInterruptState setCTE_ctes_of_wp]) apply (auto simp: ran_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (\<forall>irq. cteCap cte = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> (\<forall>irq. cteCap cte = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> (\<forall>irq. cteCap cte = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<Longrightarrow> \<forall>cap\<in>ran (map_option cteCap \<circ> (ctes_of s)(ptr \<mapsto> cte)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setupReplyMaster_irq_handlers'[wp]:
  "\<lbrace>valid_irq_handlers'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (wp setCTE_irq_handlers' getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_handlers' s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<and> (if cteCap cte = capability.NullCap then \<lambda>s. noReplyCapsFor t s \<longrightarrow> valid_irq_handlers' s \<and> (\<forall>irq. cteCap (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode))) = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) else valid_irq_handlers') s) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setupReplyMaster_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def ) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> setupReplyMaster t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> setupReplyMaster t \<lbrace>\<lambda>_ s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace>
 2. \<And>p. \<lbrace>typ_at' UserDataDeviceT (p && ~~ mask pageBits)\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. typ_at' UserDataDeviceT (p && ~~ mask pageBits)\<rbrace>
 3. \<And>p. \<lbrace>\<lambda>s. underlying_memory (ksMachineState s) p = 0\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv s. underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setupReplyMaster_cte_wp_at'':
  "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and K (\<not> P NullCap)\<rbrace>
     setupReplyMaster t
   \<lbrace>\<lambda>rv s. cte_wp_at' (P \<circ> cteCap) p s\<rbrace>" apply (simp add: setupReplyMaster_def locateSlot_conv tree_cte_cteCap_eq) apply (wp getCTE_wp') apply (fastforce 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> setupReplyMaster t \<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 oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
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) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (if cteCap cte = capability.NullCap then \<lambda>s. noReplyCapsFor t s \<longrightarrow> (case ((cteCaps_of s)(t + 2 ^ cte_level_bits * tcbReplySlot \<mapsto> cteCap (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode))))) p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2) else (\<lambda>s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2)) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setupReplyMaster_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp add: ex_nonz_cap_to'_def) apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift setupReplyMaster_cte_wp_at') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace>
 2. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s \<Longrightarrow> \<exists>x. (cte_wp_at' (\<lambda>cte. p \<in> zobj_refs' (cteCap cte)) x and K (p \<notin> zobj_refs' capability.NullCap)) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma mdb_next_pres:
  "\<lbrakk> m p = Some v;
 mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \<rbrakk> \<Longrightarrow>
  m(p \<mapsto> x) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b" by (simp add: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v)\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b
theory CSpace_R

lemma mdb_next_rtrans_next_pres:
  "\<lbrakk> m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \<rbrakk> \<Longrightarrow>
   m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>* b = m \<turnstile> a \<leadsto>\<^sup>* b" by (simp add: rtrancl_eq_or_trancl mdb_next_trans_next_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v)\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>* b = m \<turnstile> a \<leadsto>\<^sup>* b
theory CSpace_R

lemma arch_update_descendants':
  "\<lbrakk> is_arch_update' cap oldcte; m p = Some oldcte\<rbrakk> \<Longrightarrow>
  descendants_of' x (m(p \<mapsto> cteCap_update (\<lambda>_. cap) oldcte)) = descendants_of' x m" apply (erule same_master_descendants) apply (auto simp: is_arch_update'_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_arch_update' cap oldcte; m p = Some oldcte\<rbrakk> \<Longrightarrow> descendants_of' x (m(p \<mapsto> cteCap_update (\<lambda>_. cap) oldcte)) = descendants_of' x m proof (prove)
goal (4 subgoals):
 1. is_arch_update' cap oldcte \<Longrightarrow> capMasterCap (cteCap oldcte) = capMasterCap cap
 2. is_arch_update' cap oldcte \<Longrightarrow> \<not> isReplyCap cap
 3. is_arch_update' cap oldcte \<Longrightarrow> \<not> isEndpointCap cap
 4. is_arch_update' cap oldcte \<Longrightarrow> \<not> isNotificationCap cap proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma capMaster_zobj_refs:
  "capMasterCap c = capMasterCap c' \<Longrightarrow> zobj_refs' c = zobj_refs' c'" by (simp add: capMasterCap_def split: capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capMasterCap c = capMasterCap c' \<Longrightarrow> zobj_refs' c = zobj_refs' c'
theory CSpace_R

lemma cte_refs_Master:
  "cte_refs' (capMasterCap cap) = cte_refs' cap" by (rule ext, simp add: capMasterCap_def split: capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_refs' (capMasterCap cap) = cte_refs' cap
theory CSpace_R

lemma zobj_refs_Master:
  "zobj_refs' (capMasterCap cap) = zobj_refs' cap" by (simp add: capMasterCap_def split: capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zobj_refs' (capMasterCap cap) = zobj_refs' cap
theory CSpace_R

lemma capMaster_same_refs:
  "capMasterCap a = capMasterCap b \<Longrightarrow> cte_refs' a = cte_refs' b \<and> zobj_refs' a = zobj_refs' b" apply (rule conjI) apply (rule master_eqI, rule cte_refs_Master, simp) apply (rule master_eqI, rule zobj_refs_Master, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capMasterCap a = capMasterCap b \<Longrightarrow> cte_refs' a = cte_refs' b \<and> zobj_refs' a = zobj_refs' b proof (prove)
goal (2 subgoals):
 1. capMasterCap a = capMasterCap b \<Longrightarrow> cte_refs' a = cte_refs' b
 2. capMasterCap a = capMasterCap b \<Longrightarrow> zobj_refs' a = zobj_refs' b proof (prove)
goal (1 subgoal):
 1. capMasterCap a = capMasterCap b \<Longrightarrow> zobj_refs' a = zobj_refs' b proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma arch_update_setCTE_iflive:
  "\<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and if_live_then_nonz_cap'\<rbrace>
  setCTE p (cteCap_update (\<lambda>_. cap) oldcte)
  \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (wp setCTE_iflive') apply (clarsimp simp: cte_wp_at_ctes_of is_arch_update'_def dest!: capMaster_zobj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and if_live_then_nonz_cap'\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and if_live_then_nonz_cap') s \<Longrightarrow> cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap (cteCap_update (\<lambda>_. cap) oldcte)). ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_cur_tcb[wp]:
  "\<lbrace>cur_tcb'\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" by (wp cur_tcb_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>
theory CSpace_R

lemma setCTE_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def ) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace>
 2. \<And>p. \<lbrace>typ_at' UserDataDeviceT (p && ~~ mask pageBits)\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. typ_at' UserDataDeviceT (p && ~~ mask pageBits)\<rbrace>
 3. \<And>p. \<lbrace>\<lambda>s. underlying_memory (ksMachineState s) p = 0\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv s. underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!