kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpaceInv_AI

lemma cap_master_cap_eqDs1:
  "cap_master_cap cap = cap.EndpointCap ref bdg rghts
     \<Longrightarrow> bdg = 0 \<and> rghts = UNIV
          \<and> (\<exists>bdg rghts. cap = cap.EndpointCap ref bdg rghts)"
  "cap_master_cap cap = cap.NotificationCap ref bdg rghts
     \<Longrightarrow> bdg = 0 \<and> rghts = UNIV
          \<and> (\<exists>bdg rghts. cap = cap.NotificationCap ref bdg rghts)"
  "cap_master_cap cap = cap.CNodeCap ref bits gd
     \<Longrightarrow> gd = [] \<and> (\<exists>gd. cap = cap.CNodeCap ref bits gd)"
  "cap_master_cap cap = cap.ThreadCap ref
     \<Longrightarrow> cap = cap.ThreadCap ref"
  "cap_master_cap cap = cap.DomainCap
     \<Longrightarrow> cap = cap.DomainCap"
  "cap_master_cap cap = cap.NullCap
     \<Longrightarrow> cap = cap.NullCap"
  "cap_master_cap cap = cap.IRQControlCap
     \<Longrightarrow> cap = cap.IRQControlCap"
  "cap_master_cap cap = cap.IRQHandlerCap irq
     \<Longrightarrow> cap = cap.IRQHandlerCap irq"
  "cap_master_cap cap = cap.Zombie ref tp n
     \<Longrightarrow> cap = cap.Zombie ref tp n"
  "cap_master_cap cap = cap.UntypedCap dev ref bits 0
     \<Longrightarrow> \<exists>f. cap = cap.UntypedCap dev ref bits f"
  "cap_master_cap cap = cap.ReplyCap ref master rghts
     \<Longrightarrow> master = True \<and> rghts = UNIV
          \<and> (\<exists>master rghts. cap = cap.ReplyCap ref master rghts)" by (clarsimp simp: cap_master_cap_def
              split: cap.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((cap_master_cap cap = EndpointCap ref bdg rghts \<Longrightarrow> bdg = 0 \<and> rghts = UNIV \<and> (\<exists>bdg rghts. cap = EndpointCap ref bdg rghts)) &&& (cap_master_cap cap = NotificationCap ref bdg rghts \<Longrightarrow> bdg = 0 \<and> rghts = UNIV \<and> (\<exists>bdg rghts. cap = NotificationCap ref bdg rghts))) &&& (cap_master_cap cap = CNodeCap ref bits gd \<Longrightarrow> gd = [] \<and> (\<exists>gd. cap = CNodeCap ref bits gd)) &&& (cap_master_cap cap = ThreadCap ref \<Longrightarrow> cap = ThreadCap ref) &&& (cap_master_cap cap = DomainCap \<Longrightarrow> cap = DomainCap)) &&& ((cap_master_cap cap = NullCap \<Longrightarrow> cap = NullCap) &&& (cap_master_cap cap = IRQControlCap \<Longrightarrow> cap = IRQControlCap) &&& (cap_master_cap cap = IRQHandlerCap irq \<Longrightarrow> cap = IRQHandlerCap irq)) &&& (cap_master_cap cap = Zombie ref tp n \<Longrightarrow> cap = Zombie ref tp n) &&& (cap_master_cap cap = UntypedCap dev ref bits 0 \<Longrightarrow> \<exists>f. cap = UntypedCap dev ref bits f) &&& (cap_master_cap cap = ReplyCap ref master rghts \<Longrightarrow> master = True \<and> rghts = UNIV \<and> (\<exists>master rghts. cap = ReplyCap ref master rghts))
theory CSpaceInv_AI

lemma cap_master_cap_arch_eqD:
    "cap_master_cap cap = ArchObjectCap acap
     \<Longrightarrow> \<exists>ac. cap = ArchObjectCap ac \<and> acap = cap_master_arch_cap ac" by (clarsimp simp: cap_master_cap_def
              split: cap.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap cap = ArchObjectCap acap \<Longrightarrow> \<exists>ac. cap = ArchObjectCap ac \<and> acap = cap_master_arch_cap ac
theory CSpaceInv_AI

lemma cap_badge_simps [simp]:
 "cap_badge (cap.EndpointCap r badge rights)       = Some badge"
 "cap_badge (cap.NotificationCap r badge rights)   = Some badge"
 "cap_badge (cap.UntypedCap dev p n f)             = None"
 "cap_badge (cap.NullCap)                          = None"
 "cap_badge (cap.DomainCap)                        = None"
 "cap_badge (cap.CNodeCap r bits guard)            = None"
 "cap_badge (cap.ThreadCap r)                      = None"
 "cap_badge (cap.DomainCap)                        = None"
 "cap_badge (cap.ReplyCap r master rights)         = None"
 "cap_badge (cap.IRQControlCap)                    = None"
 "cap_badge (cap.IRQHandlerCap irq)                = None"
 "cap_badge (cap.Zombie r b n)                     = None"
 "cap_badge (cap.ArchObjectCap cap)                = None" by (auto simp: cap_badge_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cap_badge (EndpointCap r badge rights) = Some badge &&& cap_badge (NotificationCap r badge rights) = Some badge &&& cap_badge (UntypedCap dev p n f) = None) &&& cap_badge NullCap = None &&& cap_badge DomainCap = None &&& cap_badge (CNodeCap r bits guard) = None) &&& (cap_badge (ThreadCap r) = None &&& cap_badge DomainCap = None &&& cap_badge (ReplyCap r master rights) = None) &&& (cap_badge IRQControlCap = None &&& cap_badge (IRQHandlerCap irq) = None) &&& cap_badge (Zombie r b n) = None &&& cap_badge (ArchObjectCap cap) = None
theory CSpaceInv_AI

lemma cdt_parent_of_def:
  "m \<turnstile> p cdt_parent_of c \<equiv> m c = Some p" by (simp add: cdt_parent_rel_def is_cdt_parent_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<leadsto> c \<equiv> m c = Some p
theory CSpaceInv_AI

lemma x_sym: "(s = t) = r \<Longrightarrow> (t = s) = r" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s = t) = r \<Longrightarrow> (t = s) = r
theory CSpaceInv_AI

lemma set_inter_not_emptyD1: "\<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> A" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> A
theory CSpaceInv_AI

lemma set_inter_not_emptyD3: "\<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> A \<noteq> B" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> A \<noteq> B
theory CSpaceInv_AI

lemma untyped_range_in_cap_range: "untyped_range x \<subseteq> cap_range x" by(simp add: cap_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_range x \<subseteq> cap_range x
theory CSpaceInv_AI

lemma set_object_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_wp_at P p (kheap_update (\<lambda>ps. (kheap s)(ptr \<mapsto> ko)) s)\<rbrace>
  set_object ptr ko
  \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>" by (wpsimp wp: set_object_wp_strong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at P p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ko)\<rparr>)\<rbrace> set_object ptr ko \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace>
theory CSpaceInv_AI

lemma set_cap_cte_wp_at:
  "\<lbrace>(\<lambda>s. if p = ptr then P cap else cte_wp_at P p s) and cte_at ptr\<rbrace>
  set_cap cap ptr
  \<lbrace>\<lambda>uu s. cte_wp_at P p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply (wp set_cap_caps_of_state) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. if p = ptr then P cap else cte_wp_at P p s) and cte_wp_at (\<lambda>_. True) ptr\<rbrace> set_cap cap ptr \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. (p = ptr \<longrightarrow> P cap) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap))) and cte_wp_at (\<lambda>_. True) ptr\<rbrace> set_cap cap ptr \<lbrace>\<lambda>uu s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. (p = ptr \<longrightarrow> P cap) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap))) and cte_wp_at (\<lambda>_. True) ptr) s \<Longrightarrow> \<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<and> P capa proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_cte_wp_at':
  "\<lbrace>\<lambda>s. if p = ptr then (P cap \<and> cte_at ptr s) else cte_wp_at P p s\<rbrace>
  set_cap cap ptr
  \<lbrace>\<lambda>uu s. cte_wp_at P p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply (wp set_cap_caps_of_state) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = ptr then P cap \<and> cte_wp_at (\<lambda>_. True) ptr s else cte_wp_at P p s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>uu. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = ptr \<longrightarrow> P cap \<and> (\<exists>cap. caps_of_state s ptr = Some cap)) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>uu s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (p = ptr \<longrightarrow> P cap \<and> (\<exists>cap. caps_of_state s ptr = Some cap)) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)) \<Longrightarrow> \<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<and> P capa proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_a_type_inv:
  "((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> typ_at T p t = typ_at T p s" apply (subgoal_tac "EX x. typ_at T p s = x") apply (elim exE) apply (cut_tac P="(=) x" in set_cap_typ_at[of _ T p cap slot]) apply (fastforce simp: valid_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> typ_at T p t = typ_at T p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((), t) \<in> fst (set_cap cap slot s); \<exists>x. typ_at T p s = x\<rbrakk> \<Longrightarrow> typ_at T p t = typ_at T p s
 2. ((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> \<exists>x. typ_at T p s = x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>((), t) \<in> fst (set_cap cap slot s); typ_at T p s = x\<rbrakk> \<Longrightarrow> typ_at T p t = typ_at T p s
 2. ((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> \<exists>x. typ_at T p s = x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>((), t) \<in> fst (set_cap cap slot s); typ_at T p s = x; \<lbrace>\<lambda>s. x = typ_at T p s\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv s. x = typ_at T p s\<rbrace>\<rbrakk> \<Longrightarrow> typ_at T p t = typ_at T p s
 2. ((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> \<exists>x. typ_at T p s = x proof (prove)
goal (1 subgoal):
 1. ((), t) \<in> fst (set_cap cap slot s) \<Longrightarrow> \<exists>x. typ_at T p s = x proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_tcb:
  "\<lbrace>tcb_at p'\<rbrace> set_cap cap  p \<lbrace>\<lambda>rv. tcb_at p'\<rbrace>" by (clarsimp simp: tcb_at_typ intro!: set_cap_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at p'\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. tcb_at p'\<rbrace>
theory CSpaceInv_AI

lemma set_cap_sets:
  "\<lbrace>\<top>\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c = cap) p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply (wp set_cap_caps_of_state) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. caps_of_state s p = Some cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((caps_of_state s)(p \<mapsto> cap)) p = Some cap proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> set_cap x p \<lbrace>\<lambda>_. valid_cap c\<rbrace>" by (simp add: valid_cap_typ set_cap_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> set_cap x p \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory CSpaceInv_AI

lemma set_cap_aligned [wp]:
 "\<lbrace>pspace_aligned\<rbrace>
  set_cap c p
  \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" apply (simp add: set_cap_def split_def) apply (wp set_object_aligned get_object_wp | wpc)+ apply (auto simp: a_type_def obj_at_def wf_cs_upd fun_upd_def[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_cap c p \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do obj <- get_object (fst p);
(case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> c) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p)
od \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<Longrightarrow> \<forall>ko. ko_at ko (fst p) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> pspace_aligned s) \<and> (\<not> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> pspace_aligned s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index 1 \<longrightarrow> pspace_aligned s) \<and> (snd p \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> pspace_aligned s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> pspace_aligned s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p = tcb_cnode_index 4 \<longrightarrow> pspace_aligned s) \<and> (snd p \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_distinct [wp]:
 "\<lbrace>pspace_distinct\<rbrace> set_cap c p \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>" apply (simp add: set_cap_def split_def) apply (wp set_object_distinct get_object_wp | wpc)+ apply (auto simp: a_type_def obj_at_def wf_cs_upd fun_upd_def[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> set_cap c p \<lbrace>\<lambda>rv. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> do obj <- get_object (fst p);
(case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> c) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p)
od \<lbrace>\<lambda>rv. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_distinct s \<Longrightarrow> \<forall>ko. ko_at ko (fst p) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> pspace_distinct s) \<and> (\<not> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> pspace_distinct s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index 1 \<longrightarrow> pspace_distinct s) \<and> (snd p \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> pspace_distinct s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> pspace_distinct s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p = tcb_cnode_index 4 \<longrightarrow> pspace_distinct s) \<and> (snd p \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_cte_cap_wp_to:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> P cap'
                           \<longrightarrow> p' \<in> cte_refs cap (interrupt_irq_node s) \<and> P cap) p s
        \<and> ex_cte_cap_wp_to P p' s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace>" apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state del: split_paired_Ex) apply (wp hoare_vcg_ex_lift) apply clarify by (metis fun_upd_other fun_upd_same option.sel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> P cap' \<longrightarrow> p' \<in> cte_refs cap (interrupt_irq_node s) \<and> P cap) p s \<and> ex_cte_cap_wp_to P p' s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>capa. caps_of_state s p = Some capa \<and> (p' \<in> cte_refs capa (interrupt_irq_node s) \<and> P capa \<longrightarrow> p' \<in> cte_refs cap (interrupt_irq_node s) \<and> P cap)) \<and> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p' \<in> cte_refs cap (interrupt_irq_node s))\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p' \<in> cte_refs cap (interrupt_irq_node s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>capa. caps_of_state s p = Some capa \<and> (p' \<in> cte_refs capa (interrupt_irq_node s) \<and> P capa \<longrightarrow> p' \<in> cte_refs cap (interrupt_irq_node s) \<and> P cap)) \<and> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p' \<in> cte_refs cap (interrupt_irq_node s)) \<Longrightarrow> \<exists>x xa. ((caps_of_state s)(p \<mapsto> cap)) x = Some xa \<and> P xa \<and> p' \<in> cte_refs xa (interrupt_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s p = Some capa; p' \<in> cte_refs capa (interrupt_irq_node s) \<and> P capa \<longrightarrow> p' \<in> cte_refs cap (interrupt_irq_node s) \<and> P cap; caps_of_state s (a, b) = Some capaa; P capaa; p' \<in> cte_refs capaa (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>x xa. ((caps_of_state s)(p \<mapsto> cap)) x = Some xa \<and> P xa \<and> p' \<in> cte_refs xa (interrupt_irq_node s)
theory CSpaceInv_AI

lemma update_cap_iflive:
  "\<lbrace>cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p
      and if_live_then_nonz_cap\<rbrace>
     set_cap cap p \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>" apply (wp set_cap_iflive) apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p and if_live_then_nonz_cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs cap) p and if_live_then_nonz_cap) s \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) p s \<and> if_live_then_nonz_cap s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma update_cap_ifunsafe:
  "\<lbrace>cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap
                      \<and> (\<forall>cp. appropriate_cte_cap cp cap'
                                 = appropriate_cte_cap cp cap)) p
      and if_unsafe_then_cap
      and (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace>
     set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>" apply (wp set_cap_ifunsafe) apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap)) p and if_unsafe_then_cap and (\<lambda>s. cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (\<lambda>cap'. cte_refs cap' = cte_refs cap \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap)) p and if_unsafe_then_cap and (\<lambda>s. cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)) s \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>p'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> (p' \<notin> cte_refs cap (interrupt_irq_node s) \<or> (\<exists>cp. appropriate_cte_cap cp cap' \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> (p' \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) p' s) \<and> (p' = p \<longrightarrow> cap = NullCap)) p s \<and> if_unsafe_then_cap s \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_refs [wp]:
  "\<lbrace>\<lambda>x. P (global_refs x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (global_refs x)\<rbrace>" by (rule global_refs_lift) wp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. P (global_refs x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (global_refs x)\<rbrace>
theory CSpaceInv_AI

lemma set_cap_globals [wp]:
  "\<lbrace>valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range cap = {})\<rbrace>
  set_cap cap p
  \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" apply (simp add: valid_global_refs_def valid_refs_def2 Ball_def) apply (wp set_cap_caps_of_state hoare_vcg_all_lift hoare_vcg_imp_lift) apply (clarsimp simp: ran_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and (\<lambda>s. global_refs s \<inter> cap_range cap = {})\<rbrace> set_cap cap p \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> global_refs s \<inter> cap_range x = {}) and (\<lambda>s. global_refs s \<inter> cap_range cap = {})\<rbrace> set_cap cap p \<lbrace>\<lambda>_ s. \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> global_refs s \<inter> cap_range x = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> global_refs s \<inter> cap_range x = {}) and (\<lambda>s. global_refs s \<inter> cap_range cap = {})) s \<Longrightarrow> \<forall>x. x \<notin> ran ((caps_of_state s)(p \<mapsto> cap)) \<or> global_refs s \<inter> cap_range x = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x a b. \<lbrakk>\<forall>x. (\<exists>a b. caps_of_state s (a, b) = Some x) \<longrightarrow> global_refs s \<inter> cap_range x = {}; global_refs s \<inter> cap_range cap = {}; global_refs s \<inter> cap_range x \<noteq> {}\<rbrakk> \<Longrightarrow> ((a, b) = p \<longrightarrow> cap \<noteq> x) \<and> ((a, b) \<noteq> p \<longrightarrow> caps_of_state s (a, b) \<noteq> Some x) proof (prove)
goal:
No subgoals!