theory Arch_C

lemma array_assertion_abs_pde_16_no_lookup:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_directory_at' (ptr_val ptr && ~~ mask pdBits) s)
        \<and> (n s' \<le> 16 \<and> (x s' \<noteq> k \<longrightarrow> n s' \<noteq> 0 \<and> is_aligned (ptr_val ptr) 6))
    \<longrightarrow> (x s' = k \<or> array_assertion (ptr :: pde_C ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2, clarsimp) apply (frule(1) page_directory_at_rf_sr, clarsimp) apply (erule clift_array_assertion_imp, simp_all) apply (rule_tac x="unat ((ptr_val ptr && mask pdBits) >> 2)" in exI) apply (simp add: shiftl_t2n[where n=2, symmetric, THEN trans[rotated],
                   OF mult.commute, simplified]) apply (cases ptr, simp add: shiftr_shiftl1) apply (rule conjI, rule trans,
         rule word_plus_and_or_coroll2[symmetric, where w="mask pdBits"]) apply (simp, rule is_aligned_neg_mask_eq[THEN sym], rule is_aligned_andI1,
          erule is_aligned_weaken, simp) apply (rule order_trans, erule add_mono[OF order_refl], simp) apply (rule unat_le_helper) apply (simp add: is_aligned_mask mask_def pdBits_def pageBits_def) apply (word_bitwise, simp add: pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> page_directory_at' (ptr_val ptr && ~~ mask pdBits) s \<and> n s' \<le> 16 \<and> (x s' \<noteq> k \<longrightarrow> n s' \<noteq> 0 \<and> is_aligned (ptr_val ptr) 6) \<longrightarrow> x s' = k \<or> array_assertion ptr (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (ptr_val ptr && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned (ptr_val ptr) 6\<rbrakk> \<Longrightarrow> array_assertion ptr (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' y. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (ptr_val ptr && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned (ptr_val ptr) 6; cslift s' (pd_Ptr (ptr_val ptr && ~~ mask pdBits)) = Some y\<rbrakk> \<Longrightarrow> array_assertion ptr (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (ptr_val ptr && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned (ptr_val ptr) 6\<rbrakk> \<Longrightarrow> \<exists>i. ptr = pde_Ptr ((ptr_val ptr && ~~ mask pdBits) + word_of_nat i * 4) \<and> i + n s' \<le> 4096 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (ptr_val ptr && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned (ptr_val ptr) 6\<rbrakk> \<Longrightarrow> ptr = pde_Ptr ((ptr_val ptr && ~~ mask pdBits) + word_of_nat (unat (ptr_val ptr && mask pdBits >> 2)) * 4) \<and> unat (ptr_val ptr && mask pdBits >> 2) + n s' \<le> 4096 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (ptr_val ptr && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned (ptr_val ptr) 6\<rbrakk> \<Longrightarrow> ptr = pde_Ptr ((ptr_val ptr && ~~ mask pdBits) + (ptr_val ptr && mask pdBits >> 2 << 2)) \<and> unat (ptr_val ptr && mask pdBits >> 2) + n s' \<le> 4096 proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned xa 6; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> xa = (xa && ~~ mask pdBits) + ((xa && mask pdBits) && ~~ mask 2) \<and> unat (xa && mask pdBits >> 2) + n s' \<le> 4096 proof (prove)
goal (2 subgoals):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned xa 6; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> (xa && mask pdBits) + (xa && ~~ mask pdBits) = (xa && ~~ mask pdBits) + ((xa && mask pdBits) && ~~ mask 2)
 2. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned xa 6; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> unat (xa && mask pdBits >> 2) + n s' \<le> 4096 proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned xa 6; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> unat (xa && mask pdBits >> 2) + n s' \<le> 4096 proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned xa 6; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> unat (xa && mask pdBits >> 2) \<le> 4080 proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ mask pdBits) s; n s' \<le> 16; 0 < n s'; is_aligned xa 6; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> xa && mask pdBits >> 2 \<le> word_of_nat 4080 proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> k; (s, s') \<in> rf_sr; page_directory_at' (xa && ~~ (2 ^ (12 + pdeBits) - 1)) s; n s' \<le> 16; 0 < n s'; xa && 0x3F = 0; ptr = pde_Ptr xa\<rbrakk> \<Longrightarrow> xa && 2 ^ (12 + pdeBits) - 1 >> 2 \<le> 0xFF0 proof (prove)
goal:
No subgoals!