theory Untyped_AI

lemma invoke_untyped_pred_tcb_at:
  "\<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at ((Not \<circ> inactive) and (Not \<circ> idle)) t s
        \<and> ct_active s \<and> valid_untyped_inv ui s\<rbrace>
   invoke_untyped ui
   \<lbrace>\<lambda>_ s :: 'state_ext state. pred_tcb_at proj Q t s\<rbrace>" apply (rule hoare_pre, rule invoke_untyped_Q,
         (wp init_arch_objects_wps | simp)+) apply (rule hoare_name_pre_state, clarsimp) apply (wp retype_region_st_tcb_at) apply fastforce apply (wp reset_untyped_cap_pred_tcb_at | simp)+ apply (cases ui, clarsimp) apply (frule(1) st_tcb_ex_cap[OF _ invs_iflive]) apply (clarsimp split: Structures_A.thread_state.splits) apply (drule ex_nonz_cap_to_overlap,
         ((simp add: cte_wp_at_caps_of_state is_cap_simps descendants_range_def2
                     empty_descendants_range_in)+)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> valid_untyped_inv ui s\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ptr us tp slot reset sz slots dev. ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> pred_tcb_at proj Q t x \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 2. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. pred_tcb_at proj Q t x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 3. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 4. \<And>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> valid_untyped_inv ui s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and pred_tcb_at proj Q t and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pred_tcb_at proj Q t s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 2. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. pred_tcb_at proj Q t x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 3. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 4. \<And>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> valid_untyped_inv ui s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and pred_tcb_at proj Q t and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr us tp a b reset sz slots dev s sa. \<lbrakk>ui = Retype (a, b) reset (ptr && ~~ mask sz) ptr tp us slots dev; invs s; pred_tcb_at proj Q t s; cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) (a, b) s; pspace_no_overlap (up_aligned_area ptr sz) s; range_cover ptr sz (obj_bits_api tp us) (length slots); tp = CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s; caps_no_overlap ptr sz s; s = sa\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr (?sz30 ptr us tp a b reset sz slots dev s)) sa \<and> pred_tcb_at proj Q t sa \<and> range_cover ptr (?sz30 ptr us tp a b reset sz slots dev s) (obj_bits_api tp us) (length slots) \<and> valid_objs sa \<and> pspace_aligned sa
 2. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. pred_tcb_at proj Q t x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 3. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 4. \<And>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> valid_untyped_inv ui s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and pred_tcb_at proj Q t and valid_untyped_inv ui and ct_active) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. pred_tcb_at proj Q t x \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 2. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>_. pred_tcb_at proj Q t\<rbrace>
 3. \<And>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> valid_untyped_inv ui s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and pred_tcb_at proj Q t and valid_untyped_inv ui and ct_active) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pred_tcb_at proj Q t s \<and> invs s \<and> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s \<and> ct_active s \<and> valid_untyped_inv ui s \<Longrightarrow> (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Retype (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8; pred_tcb_at proj Q t s; invs s; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x4 = x4 && ~~ mask sz; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; x2; descendants_of (a, b) (cdt s) = {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2 x4 x5 x6 x7 x8 sz idx st. \<lbrakk>ui = Retype (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8; pred_tcb_at proj Q t s; invs s; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x4 = x4 && ~~ mask sz; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; x2; descendants_of (a, b) (cdt s) = {}; (Not \<circ> inactive and Not \<circ> idle) st\<rbrakk> \<Longrightarrow> \<not> halted st
 2. \<And>s a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Retype (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8; pred_tcb_at proj Q t s; invs s; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x4 = x4 && ~~ mask sz; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; x2; descendants_of (a, b) (cdt s) = {}; ex_nonz_cap_to t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Retype (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8; pred_tcb_at proj Q t s; invs s; st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s; ct_active s; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x4 = x4 && ~~ mask sz; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; x2; descendants_of (a, b) (cdt s) = {}; ex_nonz_cap_to t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) (a, b) s proof (prove)
goal:
No subgoals!