theory Invoke_C

lemma reset_untyped_inner_offs_helper:
  "\<lbrakk> cteCap cte = UntypedCap dev ptr sz idx;
      i \<le> unat ((of_nat idx - 1 :: addr) div 2 ^ sz2);
      sz2 \<le> sz; idx \<noteq> 0;
      valid_cap' (cteCap cte) s
    \<rbrakk>
    \<Longrightarrow> of_nat i * 2 ^ sz2 < (2 ^ sz :: addr)" apply (clarsimp simp: valid_cap_simps' untypedBits_defs) apply (rule word_less_power_trans2, simp_all) apply (rule word_of_nat_less) apply (erule order_le_less_trans) apply (simp only: word_less_nat_alt[symmetric]) apply (simp add: shiftr_div_2n_w[symmetric] word_size) apply (rule shiftr_less_t2n) apply (simp add: word_of_nat_le) apply (rule of_nat_neq_0, simp) apply (erule order_le_less_trans) apply (rule power_strict_increasing, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; i \<le> unat ((word_of_nat idx - 1) div 2 ^ sz2); sz2 \<le> sz; idx \<noteq> 0; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> word_of_nat i * 2 ^ sz2 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; i \<le> unat ((word_of_nat idx - 1) div 2 ^ sz2); sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> word_of_nat i * 2 ^ sz2 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; i \<le> unat ((word_of_nat idx - 1) div 2 ^ sz2); sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> word_of_nat i < 2 ^ (sz - sz2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; i \<le> unat ((word_of_nat idx - 1) div 2 ^ sz2); sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> i < unat (2 ^ (sz - sz2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> unat ((word_of_nat idx - 1) div 2 ^ sz2) < unat (2 ^ (sz - sz2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> (word_of_nat idx - 1) div 2 ^ sz2 < 2 ^ (sz - sz2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> word_of_nat idx - 1 >> sz2 < 2 ^ (sz - sz2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> word_of_nat idx - 1 < 2 ^ (sz2 + (sz - sz2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> word_of_nat idx \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> idx < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCap cte = capability.UntypedCap dev ptr sz idx; sz2 \<le> sz; 0 < idx; capAligned (capability.UntypedCap dev ptr sz idx); valid_untyped' dev ptr sz idx s; ptr \<noteq> 0; 4 \<le> sz; sz \<le> 29; is_aligned (word_of_nat idx) 4\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals!