theory Untyped_DR

lemma update_available_range_dcorres:
  "dcorres dc \<top> ( K(\<exists>idx. untyped_cap = transform_cap (cap.UntypedCap dev ptr sz idx)
    \<and> free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids)
   and valid_idle and (\<lambda>s. fst cref \<noteq> idle_thread s) and valid_etcbs)
  (update_available_range new_range oids
    (transform_cslot_ptr cref) untyped_cap)
  (CSpaceAcc_A.set_cap
    (cap.UntypedCap dev ptr sz idx')
    cref)" apply (rule dcorres_expand_pfx) apply (clarsimp simp:update_available_range_def) apply (rule corres_guard_imp) apply (rule select_pick_corres) apply (rule set_cap_corres) apply clarsimp apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (K (\<exists>idx. untyped_cap = transform_cap (cap.UntypedCap dev ptr sz idx) \<and> free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids) and valid_idle and (\<lambda>s. fst cref \<noteq> idle_thread s) and valid_etcbs) (update_available_range new_range oids (transform_cslot_ptr cref) untyped_cap) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz idx') cref) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (K (\<exists>idx. untyped_cap = transform_cap (cap.UntypedCap dev ptr sz idx) \<and> free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids) and valid_idle and (\<lambda>s. fst cref \<noteq> idle_thread s) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (update_available_range new_range oids (transform_cslot_ptr cref) untyped_cap) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz idx') cref) proof (prove)
goal (1 subgoal):
 1. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do new_range <- select {x. x \<subseteq> new_range - set oids};
KHeap_D.set_cap (transform_cslot_ptr cref) (cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} new_range)
od) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz idx') cref) proof (prove)
goal (3 subgoals):
 1. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q10 s' idx) (?Q'10 s' idx) (do new_range <- select {x. x \<subseteq> new_range - set oids};
KHeap_D.set_cap (transform_cslot_ptr cref) (cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} new_range)
od) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz idx') cref)
 2. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q10 s' idx s
 3. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'10 s' idx s proof (prove)
goal (3 subgoals):
 1. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?P14 s' idx) (?Q'10 s' idx) (KHeap_D.set_cap (transform_cslot_ptr cref) (cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (?x14 s' idx))) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz idx') cref)
 2. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; transform s' = s\<rbrakk> \<Longrightarrow> (?P14 s' idx and (\<lambda>s. ?x14 s' idx \<in> {x. x \<subseteq> new_range - set oids})) s
 3. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'10 s' idx s proof (prove)
goal (4 subgoals):
 1. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (?x14 s' idx) = transform_cap (cap.UntypedCap dev ptr sz idx')
 2. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr cref = transform_cslot_ptr cref
 3. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x14 s' idx \<in> {x. x \<subseteq> new_range - set oids})) s
 4. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> fst cref \<noteq> idle_thread s \<and> valid_etcbs s proof (prove)
goal (4 subgoals):
 1. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> ?x14 s' idx = free_range_of_untyped idx' sz ptr
 2. \<And>s' idx. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr cref = transform_cslot_ptr cref
 3. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x14 s' idx \<in> {x. x \<subseteq> new_range - set oids})) s
 4. \<And>s' idx s. \<lbrakk>untyped_cap = cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} (free_range_of_untyped idx sz ptr); free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids; valid_idle s'; fst cref \<noteq> idle_thread s'; valid_etcbs s'; s' = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> fst cref \<noteq> idle_thread s \<and> valid_etcbs s proof (prove)
goal:
No subgoals!