theory CNodeInv_R

lemma updateCap_ifunsafe':
  "\<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> valid_objs' s
       \<and> cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s).
                        cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) r s
                             \<and> (r = sl \<longrightarrow> cap = NullCap)) sl s
       \<and> (cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_to' sl s)\<rbrace>
      updateCap sl cap
   \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (simp add: ifunsafe'_def3 o_def) apply wp apply clarsimp apply (subgoal_tac "ex_cte_cap_to' cref s") apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (rule_tac x=crefa in exI) apply (clarsimp simp: cteCaps_of_def modify_map_def) apply (rule ccontr, drule bspec, clarsimp, erule(1) conjI) apply (clarsimp split: if_split_asm) apply (drule_tac x=cref in spec) apply (clarsimp dest!: modify_map_K_D
                   simp: ex_cte_cap_to'_cteCap
                  split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s)\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s)\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s) \<Longrightarrow> \<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) sl (K cap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) sl (K cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s) proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) cref s\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa cte crefa ctea. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref cte. ctes_of s cref = Some cte \<and> sl \<in> cte_refs' (cteCap cte) (irq_node' s)); modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap; ctes_of s sl = Some cte; \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). (\<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap) \<and> (r = sl \<longrightarrow> cap = capability.NullCap); ctes_of s crefa = Some ctea; cref \<in> cte_refs' (cteCap ctea) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa cte crefa ctea. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref cte. ctes_of s cref = Some cte \<and> sl \<in> cte_refs' (cteCap cte) (irq_node' s)); modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap; ctes_of s sl = Some cte; \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). (\<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap) \<and> (r = sl \<longrightarrow> cap = capability.NullCap); ctes_of s crefa = Some ctea; cref \<in> cte_refs' (cteCap ctea) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cap'. modify_map (cteCaps_of s) sl (\<lambda>y. cap) crefa = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa cte. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref cte. ctes_of s cref = Some cte \<and> sl \<in> cte_refs' (cteCap cte) (irq_node' s)); (if cref = sl then Some cap else map_option cteCap (ctes_of s cref)) = Some capa; capa \<noteq> capability.NullCap; \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). (\<exists>cte. ctes_of s r = Some cte \<and> cteCap cte = capability.NullCap) \<and> (r = sl \<longrightarrow> cap = capability.NullCap); ctes_of s sl = Some cte; cref \<in> cte_refs' (cteCap cte) (irq_node' s)\<rbrakk> \<Longrightarrow> cref \<in> cte_refs' cap (irq_node' s)
 2. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa cte. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref cte. ctes_of s cref = Some cte \<and> sl \<in> cte_refs' (cteCap cte) (irq_node' s)); (if cref = sl then Some cap else map_option cteCap (ctes_of s cref)) = Some capa; capa \<noteq> capability.NullCap; ctes_of s sl = Some cte; cref \<in> cte_refs' (cteCap cte) (irq_node' s); cref \<notin> cte_refs' cap (irq_node' s); (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte = capability.NullCap) \<and> (cref = sl \<longrightarrow> cap = capability.NullCap)\<rbrakk> \<Longrightarrow> False
 2. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cref capa. \<lbrakk>\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cref capa. \<lbrakk>valid_objs' s; cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = sl \<longrightarrow> cap = capability.NullCap)) sl s; cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) sl s; modify_map (cteCaps_of s) sl (\<lambda>y. cap) cref = Some capa; capa \<noteq> capability.NullCap; (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal:
No subgoals!