theory Retype_DP

lemma update_available_range_wp:
  "\<lbrace> (\<lambda>s. cdl_current_domain s = minBound)
     and <uref \<mapsto>c - \<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped) \<and>* P> \<rbrace>
  update_available_range pick_range (map pick new_obj_refs) uref (UntypedCap dev obj_range free_range)
  \<lbrace>\<lambda>r s. cdl_current_domain s = minBound \<and>
  (\<exists>nfr\<subseteq>pick_range - set (map pick new_obj_refs).
  <(\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P>
  s)\<rbrace>" apply wp apply (simp add:update_available_range_def) apply (wp) apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post[OF set_cap_wp]) apply (rule_tac x = new_range in exI) apply (intro conjI,assumption+) apply (sep_select 2,assumption) apply wp apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)\<rbrace> update_available_range pick_range (map pick new_obj_refs) uref (UntypedCap dev obj_range free_range) \<lbrace>\<lambda>r s. cdl_current_domain s = minBound \<and> (\<exists>nfr\<subseteq>pick_range - set (map pick new_obj_refs). cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> update_available_range pick_range (map pick new_obj_refs) uref (UntypedCap dev obj_range free_range) \<lbrace>\<lambda>rv s. \<exists>nfr\<subseteq>pick_range - set (map pick new_obj_refs). cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) s\<rbrace>
 2. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> do new_range <- select {x. x \<subseteq> pick_range - pick ` set new_obj_refs};
set_cap uref (UntypedCap dev obj_range new_range)
od \<lbrace>\<lambda>rv s. \<exists>nfr\<subseteq>pick_range - pick ` set new_obj_refs. cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) s\<rbrace>
 2. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<And>new_range. \<lbrace>?B4 new_range\<rbrace> set_cap uref (UntypedCap dev obj_range new_range) \<lbrace>\<lambda>rv s. \<exists>nfr\<subseteq>pick_range - pick ` set new_obj_refs. cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) s\<rbrace>
 2. \<lbrace>?P'1\<rbrace> select {x. x \<subseteq> pick_range - pick ` set new_obj_refs} \<lbrace>?B4\<rbrace>
 3. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<And>new_range. ?P6 new_range \<Longrightarrow> \<lbrace>?P'6 new_range\<rbrace> set_cap uref (UntypedCap dev obj_range new_range) \<lbrace>\<lambda>rv s. \<exists>nfr\<subseteq>pick_range - pick ` set new_obj_refs. cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) s\<rbrace>
 2. \<lbrace>?P'1\<rbrace> select {x. x \<subseteq> pick_range - pick ` set new_obj_refs} \<lbrace>\<lambda>new_range. ?P'6 new_range and K (?P6 new_range)\<rbrace>
 3. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<And>new_range rv s. \<lbrakk>?P6 new_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range new_range \<and>* ?R9 new_range) s\<rbrakk> \<Longrightarrow> \<exists>nfr\<subseteq>pick_range - pick ` set new_obj_refs. cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) s
 2. \<lbrace>?P'1\<rbrace> select {x. x \<subseteq> pick_range - pick ` set new_obj_refs} \<lbrace>\<lambda>new_range. cdl.lift (uref \<mapsto>c - \<and>* ?R9 new_range) and K (?P6 new_range)\<rbrace>
 3. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<And>new_range rv s. \<lbrakk>?P6 new_range; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range new_range \<and>* ?R9 new_range) s\<rbrakk> \<Longrightarrow> new_range \<subseteq> pick_range - pick ` set new_obj_refs \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range new_range \<and>* P) s
 2. \<lbrace>?P'1\<rbrace> select {x. x \<subseteq> pick_range - pick ` set new_obj_refs} \<lbrace>\<lambda>new_range. cdl.lift (uref \<mapsto>c - \<and>* ?R9 new_range) and K (?P6 new_range)\<rbrace>
 3. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<And>new_range rv s. \<lbrakk>new_range \<subseteq> pick_range - pick ` set new_obj_refs; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range new_range \<and>* ?R9 new_range) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range new_range \<and>* P) s
 2. \<lbrace>?P'1\<rbrace> select {x. x \<subseteq> pick_range - pick ` set new_obj_refs} \<lbrace>\<lambda>new_range. cdl.lift (uref \<mapsto>c - \<and>* ?R9 new_range) and K (new_range \<subseteq> pick_range - pick ` set new_obj_refs)\<rbrace>
 3. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> select {x. x \<subseteq> pick_range - pick ` set new_obj_refs} \<lbrace>\<lambda>new_range. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) and K (new_range \<subseteq> pick_range - pick ` set new_obj_refs)\<rbrace>
 2. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> ?P'1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> cdl_current_domain s = minBound \<and> (\<forall>x\<in>{x. x \<subseteq> pick_range - pick ` set new_obj_refs}. (cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) and K (x \<subseteq> pick_range - pick ` set new_obj_refs)) s) proof (prove)
goal:
No subgoals!