theory Untyped_AI

lemma cte_wp_at_range_cover:
  "\<lbrakk>bits < word_bits; rv\<le> 2^ sz; invs s;
    cte_wp_at ((=) (UntypedCap dev w sz idx)) p s;
    0 < n; n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits)\<rbrakk>
   \<Longrightarrow> range_cover (alignUp (w + of_nat rv) bits) sz bits n" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_def valid_untyped_def cap_aligned_def) apply (drule range_cover_stuff) apply simp_all apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; cte_wp_at ((=) (UntypedCap dev w sz idx)) p s; 0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); 0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits)\<rbrakk> \<Longrightarrow> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); 0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); s \<turnstile> UntypedCap dev w sz idx\<rbrakk> \<Longrightarrow> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); 0 < n; n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal (5 subgoals):
 1. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0\<rbrakk> \<Longrightarrow> n \<le> unat (2 ^ ?sz10 - word_of_nat ?rv10 >> ?bits10)
 2. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0\<rbrakk> \<Longrightarrow> ?rv10 \<le> 2 ^ ?sz10
 3. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0\<rbrakk> \<Longrightarrow> ?sz10 < word_bits
 4. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned ?w10 ?sz10
 5. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0; ?rv10 \<le> unat (alignUp (?w10 + word_of_nat ?rv10) ?bits10 - ?w10) \<and> alignUp (?w10 + word_of_nat ?rv10) ?bits10 && ~~ mask ?sz10 = ?w10 \<and> range_cover (alignUp (?w10 + word_of_nat ?rv10) ?bits10) ?sz10 ?bits10 n\<rbrakk> \<Longrightarrow> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bits < word_bits; rv \<le> 2 ^ sz; invs s; caps_of_state s p = Some (UntypedCap dev w sz idx); n \<le> unat (2 ^ sz - word_of_nat rv >> bits); is_aligned w sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {w..w + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {w..w + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {w + word_of_nat idx..w + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; w \<noteq> 0; rv \<le> unat (alignUp (w + word_of_nat rv) bits - w) \<and> alignUp (w + word_of_nat rv) bits && ~~ mask sz = w \<and> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n\<rbrakk> \<Longrightarrow> range_cover (alignUp (w + word_of_nat rv) bits) sz bits n proof (prove)
goal:
No subgoals!