theory SR_lemmas_C

lemma ctes_of_aligned_bits [simp]:
  assumes pa: "pspace_aligned' s"
  and    cof: "ctes_of s p = Some cte"
  and   bits: "bits \<le> cte_level_bits"
  shows  "is_aligned p bits" proof - from cof have "cte_wp_at' ((=) cte) p s" by (simp add: cte_wp_at_ctes_of) thus ?thesis apply - apply (rule is_aligned_weaken[OF _ bits]) apply (erule cte_wp_atE') apply assumption apply (simp add: tcb_cte_cases_def field_simps split: if_split_asm) apply (fastforce elim: aligned_add_aligned[OF _ _ cte_bits_le_tcb_bits]
                         simp: is_aligned_def cte_level_bits_def)+ apply (erule is_aligned_weaken[OF _  cte_bits_le_tcb_bits]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p bits proof (state)
goal (1 subgoal):
 1. is_aligned p bits proof (chain)
picking this:
ctes_of s p = Some cte proof (prove)
using this:
ctes_of s p = Some cte

goal (1 subgoal):
 1. cte_wp_at' ((=) cte) p s proof (state)
this:
cte_wp_at' ((=) cte) p s

goal (1 subgoal):
 1. is_aligned p bits proof (prove)
using this:
cte_wp_at' ((=) cte) p s

goal (1 subgoal):
 1. is_aligned p bits proof (prove)
goal (1 subgoal):
 1. cte_wp_at' ((=) cte) p s \<Longrightarrow> is_aligned p bits proof (prove)
goal (1 subgoal):
 1. cte_wp_at' ((=) cte) p s \<Longrightarrow> is_aligned p cte_level_bits proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s p = Some (KOCTE ctea); ps_clear p cte_level_bits s; is_aligned p cte_level_bits; cte = ctea\<rbrakk> \<Longrightarrow> is_aligned p cte_level_bits
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (p - ptr') = Some (getF, setF); cte = getF tcb\<rbrakk> \<Longrightarrow> is_aligned p cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (p - ptr') = Some (getF, setF); cte = getF tcb\<rbrakk> \<Longrightarrow> is_aligned p cte_level_bits proof (prove)
goal (5 subgoals):
 1. \<And>tcb ptr' getF. \<lbrakk>cte = tcbIPCBufferFrame tcb; ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; p = ptr' + 0x40; tcbIPCBufferFrame = getF\<rbrakk> \<Longrightarrow> is_aligned (ptr' + 0x40) cte_level_bits
 2. \<And>tcb ptr' getF. \<lbrakk>cte = tcb.tcbCaller tcb; ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; p = ptr' + 0x30; tcb.tcbCaller = getF\<rbrakk> \<Longrightarrow> is_aligned (ptr' + 0x30) cte_level_bits
 3. \<And>tcb ptr' getF. \<lbrakk>cte = tcb.tcbReply tcb; ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; p = ptr' + 0x20; tcb.tcbReply = getF\<rbrakk> \<Longrightarrow> is_aligned (ptr' + 0x20) cte_level_bits
 4. \<And>tcb ptr' getF. \<lbrakk>cte = tcb.tcbVTable tcb; ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; p = ptr' + 0x10; tcb.tcbVTable = getF\<rbrakk> \<Longrightarrow> is_aligned (ptr' + 0x10) cte_level_bits
 5. \<And>tcb ptr' getF. \<lbrakk>cte = tcb.tcbCTable tcb; ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; p = ptr'; tcb.tcbCTable = getF\<rbrakk> \<Longrightarrow> is_aligned ptr' cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF. \<lbrakk>cte = tcb.tcbCTable tcb; ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; p = ptr'; tcb.tcbCTable = getF\<rbrakk> \<Longrightarrow> is_aligned ptr' cte_level_bits proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned p bits

goal:
No subgoals!