theory Ctac_lemmas_C

lemma c_guard_abs_tcb_ctes':
  fixes p :: "cte_C ptr"
  shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s
    \<and> (n < ucast tcbCNodeEntries) \<longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr (((ptr_val (tcb s') && ~~mask tcbBlockSizeBits)
        + n * 2^cteSizeBits))" apply (clarsimp) apply (rule c_guard_abs_cte[rule_format], intro conjI, simp_all) apply (simp add: cte_at'_obj_at', rule disjI2) apply (frule ptr_val_tcb_ptr_mask) apply (rule_tac x="n * 2^cteSizeBits" in bexI) apply (simp add: mask_def) apply (simp add: word_less_nat_alt tcbCNodeEntries_def tcb_cte_cases_def objBits_defs) apply (case_tac "unat n", simp_all add: unat_eq_of_nat, rename_tac n_rem) apply (case_tac "n_rem", simp_all add: unat_eq_of_nat, (rename_tac n_rem)?)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s \<and> n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries \<longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (tcb s') && ~~ mask tcbBlockSizeBits) + n * 2 ^ cteSizeBits) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (tcb s') && ~~ mask tcbBlockSizeBits) + n * 2 ^ cteSizeBits) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ((ptr_val (tcb s') && ~~ mask tcbBlockSizeBits) + n * 2 ^ cteSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries\<rbrakk> \<Longrightarrow> \<exists>na\<in>dom tcb_cte_cases. tcb_at' ((ptr_val (tcb s') && ~~ mask tcbBlockSizeBits) + n * 2 ^ cteSizeBits - na) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr (tcb s'))) && ~~ mask tcbBlockSizeBits = ctcb_ptr_to_tcb_ptr (tcb s')\<rbrakk> \<Longrightarrow> \<exists>na\<in>dom tcb_cte_cases. tcb_at' ((ptr_val (tcb s') && ~~ mask tcbBlockSizeBits) + n * 2 ^ cteSizeBits - na) s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr (tcb s'))) && ~~ mask tcbBlockSizeBits = ctcb_ptr_to_tcb_ptr (tcb s')\<rbrakk> \<Longrightarrow> tcb_at' ((ptr_val (tcb s') && ~~ mask tcbBlockSizeBits) + n * 2 ^ cteSizeBits - n * 2 ^ cteSizeBits) s
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr (tcb s'))) && ~~ mask tcbBlockSizeBits = ctcb_ptr_to_tcb_ptr (tcb s')\<rbrakk> \<Longrightarrow> n * 2 ^ cteSizeBits \<in> dom tcb_cte_cases proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n < UCAST(32 signed \<rightarrow> 32) tcbCNodeEntries; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr (tcb s'))) && ~~ mask tcbBlockSizeBits = ctcb_ptr_to_tcb_ptr (tcb s')\<rbrakk> \<Longrightarrow> n * 2 ^ cteSizeBits \<in> dom tcb_cte_cases proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; unat n < 5; ptr_val (tcb s') && ~~ mask 9 = ctcb_ptr_to_tcb_ptr (tcb s')\<rbrakk> \<Longrightarrow> n * 0x10 = 0x40 \<or> n * 0x10 = 0x30 \<or> n * 0x10 = 0x20 \<or> n * 0x10 = 0x10 \<or> n * 0x10 = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s' n_rem. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s; n_rem < 4; ptr_val (tcb s') && ~~ mask 9 = ctcb_ptr_to_tcb_ptr (tcb s'); n = 1 + word_of_nat n_rem\<rbrakk> \<Longrightarrow> word_of_nat n_rem * 0x10 = 0x30 \<or> word_of_nat n_rem * 0x10 = 0x20 \<or> word_of_nat n_rem * 0x10 = 0x10 \<or> word_of_nat n_rem * 0x10 = 0 \<or> 0x10 + word_of_nat n_rem * 0x10 = 0 proof (prove)
goal:
No subgoals!