theory Retype_C

lemma updateNewFreeIndex_noop_ccorres:
  "ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)
      {s. (case untypedZeroRange cap of None \<Rightarrow> True
          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)} hs
      (updateNewFreeIndex slot) Skip"
  (is "ccorres _ _ ?P ?P' hs _ _") apply (simp add: updateNewFreeIndex_def getSlotCap_def) apply (rule ccorres_guard_imp) apply (rule ccorres_pre_getCTE[where P="\<lambda>rv. cte_wp_at' ((=) rv) slot and ?P"
        and P'="K ?P'"]) apply (case_tac "cteCap cte", simp_all add: ccorres_guard_imp[OF ccorres_return_Skip])[1] defer apply (clarsimp simp: cte_wp_at_ctes_of) apply simp apply (simp add: updateTrackedFreeIndex_def getSlotCap_def) apply (rule ccorres_guard_imp) apply (rule_tac P="\<lambda>rv. cte_wp_at' ((=) rv) slot and K (rv = cte) and ?P"
        in ccorres_pre_getCTE[where P'="K ?P'"]) defer apply (clarsimp simp: cte_wp_at_ctes_of) apply simp apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: bind_def simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (clarsimp simp: zero_ranges_are_zero_def
                        cte_wp_at_ctes_of
                 split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (updateNewFreeIndex slot) SKIP proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex (cteCap cte)) | _ \<Rightarrow> return ()
od) SKIP proof (prove)
goal (3 subgoals):
 1. ccorres dc xfdc ?Q6 ?Q'6 hs (do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex (cteCap cte)) | _ \<Rightarrow> return ()
od) SKIP
 2. \<And>s. (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> ?Q6 s
 3. \<And>s. s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<Longrightarrow> s \<in> ?Q'6 proof (prove)
goal (3 subgoals):
 1. \<And>cte. ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) (K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} cte) hs (case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex (cteCap cte)) | _ \<Rightarrow> return ()) SKIP
 2. \<And>s. (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s
 3. \<And>s. s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (updateTrackedFreeIndex slot x104) SKIP
 2. \<And>s. (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s
 3. \<And>s. s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>s. (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s
 2. \<And>s. s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')}
 3. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (updateTrackedFreeIndex slot x104) SKIP proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')}
 2. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (updateTrackedFreeIndex slot x104) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (updateTrackedFreeIndex slot x104) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} hs (do cte <- getCTE slot;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (?Q25 cte x101 x102 x103 x104) (?Q'25 cte x101 x102 x103 x104) hs (do cte <- getCTE slot;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP
 2. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s\<rbrakk> \<Longrightarrow> ?Q25 cte x101 x102 x103 x104 s
 3. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> s \<in> ?Q'25 cte x101 x102 x103 x104 proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 rv. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) rv) slot and K (rv = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) (K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} rv) hs (do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap rv) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap rv)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP
 2. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s\<rbrakk> \<Longrightarrow> \<forall>ctea. ctes_of s slot = Some ctea \<longrightarrow> (cte_wp_at' ((=) ctea) slot and K (ctea = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s
 3. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; (cte_wp_at' ((=) cte) slot and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s\<rbrakk> \<Longrightarrow> \<forall>ctea. ctes_of s slot = Some ctea \<longrightarrow> (cte_wp_at' ((=) ctea) slot and K (ctea = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) s
 2. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')}
 3. \<And>cte x101 x102 x103 x104 rv. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) rv) slot and K (rv = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) (K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} rv) hs (do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap rv) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap rv)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} (cte_to_H cte')}
 2. \<And>cte x101 x102 x103 x104 rv. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) rv) slot and K (rv = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) (K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} rv) hs (do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap rv) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap rv)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 rv. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) rv) slot and K (rv = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) (K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} rv) hs (do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap rv) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap rv)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 rv. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (cte_wp_at' ((=) rv) slot and K (rv = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) \<sigma> \<and> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} rv \<and> (\<sigma>, s) \<in> rf_sr} SKIP {s. \<exists>(rv, \<sigma>')\<in>fst ((do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap rv) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap rv)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 rv \<sigma>. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> {s. (cte_wp_at' ((=) rv) slot and K (rv = cte) and (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)) \<sigma> \<and> s \<in> K {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} rv \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap rv) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - \<lbrace>\<acute>((=) r)\<rbrace>\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. x104) (cteCap rv)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 \<sigma> x. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; cte_wp_at' ((=) cte) slot \<sigma>; valid_objs' \<sigma>; cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot \<sigma>; case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capability.UntypedCap x101 x102 x103 x104) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))\<rparr>, x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 \<sigma> x. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; cte_wp_at' ((=) cte) slot \<sigma>; valid_objs' \<sigma>; cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot \<sigma>; case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (case untypedZeroRange (capability.UntypedCap x101 x102 x103 x104) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))) (t_hrs_' (globals x)) proof (prove)
goal:
No subgoals!