theory Retype_R

lemma ctes_of_retype:
  assumes ko: "makeObjectKO dev tp = Some obj"
      and pv: "pspace_aligned' s" "pspace_distinct' s"
     and pv': "pspace_aligned' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
              "pspace_distinct' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
      and al: "\<forall>x \<in> set addrs. is_aligned x (objBitsKO obj)"
      and pn: "\<forall>x \<in> set addrs. ksPSpace s x = None"
   shows
  "map_to_ctes (\<lambda> xa. if xa \<in> set addrs then Some obj else ksPSpace s xa)
      = (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.CapTableObject) \<and> x \<in> set addrs
              \<or> tp = Inr (APIObjectType ArchTypes_H.TCBObject)
                         \<and> (x && ~~ mask tcbBlockSizeBits \<in> set addrs) \<and> (x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)
             then Some (CTE NullCap nullMDBNode)
             else map_to_ctes (ksPSpace s) x)"
  (is "map_to_ctes ?ps' = ?map'") using cte_wp_at_retype' [where P="(=) cte" for cte, OF ko pv pv' al pn]
        arg_cong [where f=Not, OF cte_wp_at_retype' [OF ko pv pv' al pn, where P="\<top>"]] apply (simp(no_asm_use) add: cte_wp_at_ctes_of cong: if_cong) apply (rule ext) apply (case_tac "map_to_ctes ?ps' x") apply (simp(no_asm_simp)) apply (simp split: if_split_asm) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) = (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
using this:
cte_wp_at' ((=) ?cte3) ?p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> ?p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> ?p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> ?p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then ?cte3 = CTE capability.NullCap nullMDBNode else cte_wp_at' ((=) ?cte3) ?p s)
(\<not> cte_wp_at' (\<lambda>_. True) ?p1 (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> ?p1 \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> ?p1 && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> ?p1 && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else cte_wp_at' (\<lambda>_. True) ?p1 s))

goal (1 subgoal):
 1. map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) = (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte))\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) = (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte))\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte)); map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = None\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x)
 2. \<And>x a. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte)); map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = Some a\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte)); map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = None\<rbrakk> \<Longrightarrow> (tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<longrightarrow> x \<notin> set addrs) \<and> (x && ~~ mask tcbBlockSizeBits \<in> set addrs \<longrightarrow> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<longrightarrow> x && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<and> ((tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<longrightarrow> x \<notin> set addrs) \<and> (x && ~~ mask tcbBlockSizeBits \<in> set addrs \<longrightarrow> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<longrightarrow> x && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> None = ctes_of s x)
 2. \<And>x a. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte)); map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = Some a\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = Some cte) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then cte = CTE capability.NullCap nullMDBNode else ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) p = None) = (\<not> (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then True else \<exists>cte. ctes_of s p = Some cte)); map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = Some a\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) x = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
goal:
No subgoals!