theory Retype_C

lemma retype_ctes_helper:
  assumes pal: "pspace_aligned' s"
  and    pdst: "pspace_distinct' s"
  and     pno: "pspace_no_overlap' ptr sz s"
  and      al: "is_aligned ptr (objBitsKO ko)"
  and      sz: "objBitsKO ko \<le> sz"
  and     szb: "sz < word_bits"
  and     mko: "makeObjectKO dev tp = Some ko"
  and      rc: "range_cover ptr sz (objBitsKO ko) n"
  shows  "map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa) =
   (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs n ptr ko) \<or>
           tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and>
           x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs n ptr ko) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases
        then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x)" using mko pal pdst proof (rule ctes_of_retype) show "pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)" using pal pdst pno szb al sz rc apply - apply (rule retype_aligned_distinct'', simp_all) done show "pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)" using pal pdst pno szb al sz rc apply - apply (rule retype_aligned_distinct'', simp_all) done show "\<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)" using al szb apply - apply (rule new_cap_addrs_aligned, simp_all) done show "\<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None" using al szb pno pal rc sz apply - apply (drule(1) pspace_no_overlap_disjoint') apply (frule new_cap_addrs_subset) apply (clarsimp simp: More_Word_Operations.ptr_add_def field_simps) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa) = (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs n ptr ko) \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs n ptr ko) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (prove)
using this:
makeObjectKO dev tp = Some ko
pspace_aligned' s
pspace_distinct' s

goal (1 subgoal):
 1. map_to_ctes (\<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa) = (\<lambda>x. if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> x \<in> set (new_cap_addrs n ptr ko) \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> x && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs n ptr ko) \<and> x && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then Some (CTE capability.NullCap nullMDBNode) else ctes_of s x) proof (state)
goal (4 subgoals):
 1. pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)
 2. pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)
 3. \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)
 4. \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>) proof (prove)
using this:
pspace_aligned' s
pspace_distinct' s
pspace_no_overlap' ptr sz s
sz < word_bits
is_aligned ptr (objBitsKO ko)
objBitsKO ko \<le> sz
range_cover ptr sz (objBitsKO ko) n

goal (1 subgoal):
 1. pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; sz < word_bits; is_aligned ptr (objBitsKO ko); objBitsKO ko \<le> sz; range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_aligned' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)

goal (3 subgoals):
 1. pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)
 2. \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)
 3. \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>) proof (prove)
using this:
pspace_aligned' s
pspace_distinct' s
pspace_no_overlap' ptr sz s
sz < word_bits
is_aligned ptr (objBitsKO ko)
objBitsKO ko \<le> sz
range_cover ptr sz (objBitsKO ko) n

goal (1 subgoal):
 1. pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; sz < word_bits; is_aligned ptr (objBitsKO ko); objBitsKO ko \<le> sz; range_cover ptr sz (objBitsKO ko) n\<rbrakk> \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_distinct' (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s xa\<rparr>)

goal (2 subgoals):
 1. \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)
 2. \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko) proof (prove)
using this:
is_aligned ptr (objBitsKO ko)
sz < word_bits

goal (1 subgoal):
 1. \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko); sz < word_bits\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)

goal (1 subgoal):
 1. \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
using this:
is_aligned ptr (objBitsKO ko)
sz < word_bits
pspace_no_overlap' ptr sz s
pspace_aligned' s
range_cover ptr sz (objBitsKO ko) n
objBitsKO ko \<le> sz

goal (1 subgoal):
 1. \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko); sz < word_bits; pspace_no_overlap' ptr sz s; pspace_aligned' s; range_cover ptr sz (objBitsKO ko) n; objBitsKO ko \<le> sz\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko); sz < word_bits; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko) n; objBitsKO ko \<le> sz; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko); sz < word_bits; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko) n; objBitsKO ko \<le> sz; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; set (new_cap_addrs n ptr ko) \<subseteq> {ptr..More_Word_Operations.ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko); sz < word_bits; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO ko) n; objBitsKO ko \<le> sz; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; set (new_cap_addrs n ptr ko) \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ksPSpace s x = None proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>set (new_cap_addrs n ptr ko). ksPSpace s x = None

goal:
No subgoals!