kings-crown/FVELER_Isabelle huggingface dataset:
theory Example_Valid_StateH

lemma word_div_mult':
  fixes c :: "'a::len word"
  shows "\<lbrakk>0 < c; a \<le> b * c \<rbrakk> \<Longrightarrow> a div c \<le> b" using div_lt_mult word_le_not_less by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < c; a \<le> b * c\<rbrakk> \<Longrightarrow> a div c \<le> b proof (prove)
using this:
\<lbrakk>?i < ?k div ?x; 0 < ?x\<rbrakk> \<Longrightarrow> ?i * ?x < ?k
(?b \<le> ?a) = (\<not> ?a < ?b)

goal (1 subgoal):
 1. \<lbrakk>0 < c; a \<le> b * c\<rbrakk> \<Longrightarrow> a div c \<le> b
theory Example_Valid_StateH

lemma cnode_offs_range_correct:
  "x \<in> cnode_offs_range Low_cnode_ptr \<Longrightarrow> \<exists>y. length y = 10 \<and> (x = Low_cnode_ptr + of_bl y * 0x10)"
  "x \<in> cnode_offs_range High_cnode_ptr \<Longrightarrow> \<exists>y. length y = 10 \<and> (x = High_cnode_ptr + of_bl y * 0x10)"
  "x \<in> cnode_offs_range Silc_cnode_ptr \<Longrightarrow> \<exists>y. length y = 10 \<and> (x = Silc_cnode_ptr + of_bl y * 0x10)" by (simp_all add: cnode_offs_range_correct' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> cnode_offs_range Low_cnode_ptr \<Longrightarrow> \<exists>y. length y = 10 \<and> x = Low_cnode_ptr + of_bl y * 0x10) &&& (x \<in> cnode_offs_range High_cnode_ptr \<Longrightarrow> \<exists>y. length y = 10 \<and> x = High_cnode_ptr + of_bl y * 0x10) &&& (x \<in> cnode_offs_range Silc_cnode_ptr \<Longrightarrow> \<exists>y. length y = 10 \<and> x = Silc_cnode_ptr + of_bl y * 0x10)
theory Example_Valid_StateH

lemma tcb_offs_min':
  "is_aligned ptr 9 \<Longrightarrow> (ptr::word32) \<le> ptr + ucast (x:: 9 word)" apply (erule is_aligned_no_wrap') apply (cut_tac x=x and 'a=32 in ucast_less) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 9 \<Longrightarrow> ptr \<le> ptr + UCAST(9 \<rightarrow> 32) x proof (prove)
goal (1 subgoal):
 1. UCAST(9 \<rightarrow> 32) x < 2 ^ 9 proof (prove)
goal (2 subgoals):
 1. LENGTH(9) < LENGTH(32)
 2. UCAST(9 \<rightarrow> 32) x < 2 ^ LENGTH(9) \<Longrightarrow> UCAST(9 \<rightarrow> 32) x < 2 ^ 9 proof (prove)
goal (1 subgoal):
 1. UCAST(9 \<rightarrow> 32) x < 2 ^ LENGTH(9) \<Longrightarrow> UCAST(9 \<rightarrow> 32) x < 2 ^ 9 proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma tcb_offs_min:
  "Low_tcb_ptr \<le> Low_tcb_ptr + ucast (x:: 9 word)"
  "High_tcb_ptr \<le> High_tcb_ptr + ucast (x:: 9 word)"
  "idle_tcb_ptr \<le> idle_tcb_ptr + ucast (x:: 9 word)" by (simp_all add: tcb_offs_min' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_tcb_ptr \<le> Low_tcb_ptr + UCAST(9 \<rightarrow> 32) x &&& High_tcb_ptr \<le> High_tcb_ptr + UCAST(9 \<rightarrow> 32) x &&& idle_tcb_ptr \<le> idle_tcb_ptr + UCAST(9 \<rightarrow> 32) x
theory Example_Valid_StateH

lemma tcb_offs_max':
  "is_aligned ptr 9 \<Longrightarrow> (ptr::word32) + ucast (x:: 9 word) \<le> ptr + 0x1ff" apply (rule word_plus_mono_right) apply (rule plus_one_helper) apply (cut_tac ucast_less[where x=x and 'a=32]) apply simp apply simp apply (drule is_aligned_no_overflow) apply (simp add: add.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 9 \<Longrightarrow> ptr + UCAST(9 \<rightarrow> 32) x \<le> ptr + 0x1FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 9 \<Longrightarrow> UCAST(9 \<rightarrow> 32) x \<le> 0x1FF
 2. is_aligned ptr 9 \<Longrightarrow> ptr \<le> ptr + 0x1FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 9 \<Longrightarrow> UCAST(9 \<rightarrow> 32) x < 0x1FF + 1
 2. is_aligned ptr 9 \<Longrightarrow> ptr \<le> ptr + 0x1FF proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 9; UCAST(9 \<rightarrow> 32) x < 2 ^ LENGTH(9)\<rbrakk> \<Longrightarrow> UCAST(9 \<rightarrow> 32) x < 0x1FF + 1
 2. is_aligned ptr 9 \<Longrightarrow> LENGTH(9) < LENGTH(32)
 3. is_aligned ptr 9 \<Longrightarrow> ptr \<le> ptr + 0x1FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 9 \<Longrightarrow> LENGTH(9) < LENGTH(32)
 2. is_aligned ptr 9 \<Longrightarrow> ptr \<le> ptr + 0x1FF proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 9 \<Longrightarrow> ptr \<le> ptr + 0x1FF proof (prove)
goal (1 subgoal):
 1. ptr \<le> ptr + 2 ^ 9 - 1 \<Longrightarrow> ptr \<le> ptr + 0x1FF proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma tcb_offs_max:
  "Low_tcb_ptr + ucast (x:: 9 word) \<le> Low_tcb_ptr + 0x1ff"
  "High_tcb_ptr + ucast (x:: 9 word) \<le> High_tcb_ptr + 0x1ff"
  "idle_tcb_ptr + ucast (x:: 9 word) \<le> idle_tcb_ptr + 0x1ff" by (simp_all add: tcb_offs_max' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_tcb_ptr + UCAST(9 \<rightarrow> 32) x \<le> Low_tcb_ptr + 0x1FF &&& High_tcb_ptr + UCAST(9 \<rightarrow> 32) x \<le> High_tcb_ptr + 0x1FF &&& idle_tcb_ptr + UCAST(9 \<rightarrow> 32) x \<le> idle_tcb_ptr + 0x1FF
theory Example_Valid_StateH

lemma tcb_offs_in_range':
  "is_aligned ptr 9 \<Longrightarrow>
     ptr + ucast (x:: 9 word) \<in> tcb_offs_range ptr" by (clarsimp simp: tcb_offs_min' tcb_offs_max' tcb_offs_range_def add.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 9 \<Longrightarrow> ptr + UCAST(9 \<rightarrow> 32) x \<in> tcb_offs_range ptr
theory Example_Valid_StateH

lemma tcb_offs_in_range:
  "Low_tcb_ptr + ucast (x:: 9 word) \<in> tcb_offs_range Low_tcb_ptr"
  "High_tcb_ptr + ucast (x:: 9 word) \<in> tcb_offs_range High_tcb_ptr"
  "idle_tcb_ptr + ucast (x:: 9 word) \<in> tcb_offs_range idle_tcb_ptr" by (simp_all add: tcb_offs_in_range' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_tcb_ptr + UCAST(9 \<rightarrow> 32) x \<in> tcb_offs_range Low_tcb_ptr &&& High_tcb_ptr + UCAST(9 \<rightarrow> 32) x \<in> tcb_offs_range High_tcb_ptr &&& idle_tcb_ptr + UCAST(9 \<rightarrow> 32) x \<in> tcb_offs_range idle_tcb_ptr
theory Example_Valid_StateH

lemma tcb_offs_range_correct:
  "x \<in> tcb_offs_range Low_tcb_ptr \<Longrightarrow> \<exists>y. x = Low_tcb_ptr + ucast (y:: 9 word)"
  "x \<in> tcb_offs_range High_tcb_ptr \<Longrightarrow> \<exists>y. x = High_tcb_ptr + ucast (y:: 9 word)"
  "x \<in> tcb_offs_range idle_tcb_ptr \<Longrightarrow> \<exists>y. x = idle_tcb_ptr + ucast (y:: 9 word)" by (simp_all add: tcb_offs_range_correct' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> tcb_offs_range Low_tcb_ptr \<Longrightarrow> \<exists>y. x = Low_tcb_ptr + UCAST(9 \<rightarrow> 32) y) &&& (x \<in> tcb_offs_range High_tcb_ptr \<Longrightarrow> \<exists>y. x = High_tcb_ptr + UCAST(9 \<rightarrow> 32) y) &&& (x \<in> tcb_offs_range idle_tcb_ptr \<Longrightarrow> \<exists>y. x = idle_tcb_ptr + UCAST(9 \<rightarrow> 32) y)
theory Example_Valid_StateH

lemma caps_dom_length_10:
  "Silc_caps x = Some y \<Longrightarrow> length x = 10"
  "High_caps x = Some y \<Longrightarrow> length x = 10"
  "Low_caps x = Some y \<Longrightarrow> length x = 10" by (simp_all add: Silc_caps_def High_caps_def Low_caps_def the_nat_to_bl_def nat_to_bl_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Silc_caps x = Some y \<Longrightarrow> length x = 10) &&& (High_caps x = Some y \<Longrightarrow> length x = 10) &&& (Low_caps x = Some y \<Longrightarrow> length x = 10)
theory Example_Valid_StateH

lemma dom_caps:
  "dom Silc_caps = {x. length x = 10}"
  "dom High_caps = {x. length x = 10}"
  "dom Low_caps = {x. length x = 10}" apply (simp_all add: Silc_caps_def High_caps_def Low_caps_def the_nat_to_bl_def nat_to_bl_def dom_def split: if_split_asm) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom Silc_caps = {x. length x = 10} &&& dom High_caps = {x. length x = 10} &&& dom Low_caps = {x. length x = 10} proof (prove)
goal (3 subgoals):
 1. {a. a \<noteq> [False, False, False, False, False, False, False, False, True, False] \<longrightarrow> a \<noteq> [False, True, False, False, True, True, True, True, True, False] \<longrightarrow> length a = 10} = {x. length x = 10}
 2. {a. a \<noteq> [False, False, False, False, False, False, False, False, False, True] \<longrightarrow> a \<noteq> [False, False, False, False, False, False, False, False, True, False] \<longrightarrow> a \<noteq> [False, False, False, False, False, False, False, False, True, True] \<longrightarrow> a \<noteq> [False, True, False, False, True, True, True, True, True, False] \<longrightarrow> length a = 10} = {x. length x = 10}
 3. {a. a \<noteq> [False, False, False, False, False, False, False, False, False, True] \<longrightarrow> a \<noteq> [False, False, False, False, False, False, False, False, True, False] \<longrightarrow> a \<noteq> [False, False, False, False, False, False, False, False, True, True] \<longrightarrow> a \<noteq> [False, True, False, False, True, True, True, True, True, False] \<longrightarrow> length a = 10} = {x. length x = 10} proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma not_in_range_None:
  "\<lbrakk>x \<notin> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> Low_cte Low_cnode_ptr x = None"
  "\<lbrakk>x \<notin> cnode_offs_range High_cnode_ptr\<rbrakk> \<Longrightarrow> High_cte High_cnode_ptr x = None"
  "\<lbrakk>x \<notin> cnode_offs_range Silc_cnode_ptr\<rbrakk> \<Longrightarrow> Silc_cte Silc_cnode_ptr x = None"
  "\<lbrakk>x \<notin> pd_offs_range Low_pd_ptr\<rbrakk> \<Longrightarrow> Low_pdH Low_pd_ptr x = None"
  "\<lbrakk>x \<notin> pd_offs_range High_pd_ptr\<rbrakk> \<Longrightarrow> High_pdH High_pd_ptr x = None"
  "\<lbrakk>x \<notin> pd_offs_range init_global_pd\<rbrakk> \<Longrightarrow> global_pdH' init_global_pd x = None"
  "\<lbrakk>x \<notin> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> Low_ptH Low_pt_ptr x = None"
  "\<lbrakk>x \<notin> pt_offs_range High_pt_ptr\<rbrakk> \<Longrightarrow> High_ptH High_pt_ptr x = None" by (clarsimp simp: cnode_offs_range_def pd_offs_range_def pt_offs_range_def s0_ptr_defs kh0H_obj_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((x \<notin> cnode_offs_range Low_cnode_ptr \<Longrightarrow> Low_cte Low_cnode_ptr x = None) &&& (x \<notin> cnode_offs_range High_cnode_ptr \<Longrightarrow> High_cte High_cnode_ptr x = None)) &&& (x \<notin> cnode_offs_range Silc_cnode_ptr \<Longrightarrow> Silc_cte Silc_cnode_ptr x = None) &&& (x \<notin> pd_offs_range Low_pd_ptr \<Longrightarrow> Low_pdH Low_pd_ptr x = None)) &&& ((x \<notin> pd_offs_range High_pd_ptr \<Longrightarrow> High_pdH High_pd_ptr x = None) &&& (x \<notin> pd_offs_range init_global_pd \<Longrightarrow> global_pdH' init_global_pd x = None)) &&& (x \<notin> pt_offs_range Low_pt_ptr \<Longrightarrow> Low_ptH Low_pt_ptr x = None) &&& (x \<notin> pt_offs_range High_pt_ptr \<Longrightarrow> High_ptH High_pt_ptr x = None)
theory Example_Valid_StateH

lemma not_disjointI:
  "\<lbrakk>x = y; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> A \<inter> B \<noteq> {}" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> A \<inter> B \<noteq> {}
theory Example_Valid_StateH

lemma kh0H_dom_tcb:
  "kh0H x = Some (KOTCB tcb) \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr" apply (frule domI[where m="kh0H"]) apply (simp add: kh0H_dom) apply (elim disjE) apply (drule irq_node_offs_range_correct cnode_offs_range_correct pd_offs_range_correct pt_offs_range_correct | clarsimp simp: kh0H_all_obj_def s0_ptrs_aligned split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kh0H x = Some (KOTCB tcb) \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh0H x = Some (KOTCB tcb); x \<in> dom kh0H\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh0H x = Some (KOTCB tcb); x = init_globals_frame \<or> x = idle_tcb_ptr \<or> x = High_tcb_ptr \<or> x = Low_tcb_ptr \<or> x = irq_cnode_ptr \<or> x = ntfn_ptr \<or> x \<in> irq_node_offs_range \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<or> x \<in> cnode_offs_range High_cnode_ptr \<or> x \<in> cnode_offs_range Low_cnode_ptr \<or> x \<in> pd_offs_range init_global_pd \<or> x \<in> pd_offs_range High_pd_ptr \<or> x \<in> pd_offs_range Low_pd_ptr \<or> x \<in> pt_offs_range High_pt_ptr \<or> x \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr proof (prove)
goal (15 subgoals):
 1. \<lbrakk>kh0H x = Some (KOTCB tcb); x = init_globals_frame\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 2. \<lbrakk>kh0H x = Some (KOTCB tcb); x = idle_tcb_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 3. \<lbrakk>kh0H x = Some (KOTCB tcb); x = High_tcb_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 4. \<lbrakk>kh0H x = Some (KOTCB tcb); x = Low_tcb_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 5. \<lbrakk>kh0H x = Some (KOTCB tcb); x = irq_cnode_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 6. \<lbrakk>kh0H x = Some (KOTCB tcb); x = ntfn_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 7. \<lbrakk>kh0H x = Some (KOTCB tcb); x \<in> irq_node_offs_range\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 8. \<lbrakk>kh0H x = Some (KOTCB tcb); x \<in> cnode_offs_range Silc_cnode_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 9. \<lbrakk>kh0H x = Some (KOTCB tcb); x \<in> cnode_offs_range High_cnode_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
 10. \<lbrakk>kh0H x = Some (KOTCB tcb); x \<in> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> x = Low_tcb_ptr \<or> x = High_tcb_ptr \<or> x = idle_tcb_ptr
A total of 15 subgoals... proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma mask_in_tcb_offs_range:
  "x && ~~ mask 9 = ptr \<Longrightarrow> x \<in> tcb_offs_range ptr" apply (clarsimp simp: tcb_offs_range_def mask_neg_le objBitsKO_def) apply (cut_tac and_neg_mask_plus_mask_mono[where p=x and n=9]) apply (simp add: add.commute mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && ~~ mask 9 = ptr \<Longrightarrow> x \<in> tcb_offs_range ptr proof (prove)
goal (1 subgoal):
 1. ptr = x && ~~ mask 9 \<Longrightarrow> x \<le> 0x1FF + (x && ~~ mask 9) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = x && ~~ mask 9; x \<le> (x && ~~ mask 9) + mask 9\<rbrakk> \<Longrightarrow> x \<le> 0x1FF + (x && ~~ mask 9) proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma set_mem_neq:
  "\<lbrakk>y \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> x \<noteq> y" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> x \<noteq> y
theory Example_Valid_StateH

lemma neg_mask_decompose:
  "x && ~~ mask n = ptr \<Longrightarrow> x = ptr + (x && mask n)" by (clarsimp simp: AND_NOT_mask_plus_AND_mask_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && ~~ mask n = ptr \<Longrightarrow> x = ptr + (x && mask n)
theory Example_Valid_StateH

lemma opt_None_not_dom:
  "m a = None \<Longrightarrow> a \<notin> dom m" by (simp add: dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m a = None \<Longrightarrow> a \<notin> dom m
theory Example_Valid_StateH

lemma not_in_tcb_offs:
  "\<forall>tcb. kh0H (x && ~~ mask 9) \<noteq> Some (KOTCB tcb)
    \<Longrightarrow> x \<notin> tcb_offs_range Low_tcb_ptr"
  "\<forall>tcb. kh0H (x && ~~ mask 9) \<noteq> Some (KOTCB tcb)
    \<Longrightarrow> x \<notin> tcb_offs_range High_tcb_ptr"
  "\<forall>tcb. kh0H (x && ~~ mask 9) \<noteq> Some (KOTCB tcb)
    \<Longrightarrow> x \<notin> tcb_offs_range idle_tcb_ptr" by (fastforce simp: s0_ptrs_aligned dest: tcb_offs_range_mask_eq)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>tcb. kh0H (x && ~~ mask 9) \<noteq> Some (KOTCB tcb) \<Longrightarrow> x \<notin> tcb_offs_range Low_tcb_ptr) &&& (\<forall>tcb. kh0H (x && ~~ mask 9) \<noteq> Some (KOTCB tcb) \<Longrightarrow> x \<notin> tcb_offs_range High_tcb_ptr) &&& (\<forall>tcb. kh0H (x && ~~ mask 9) \<noteq> Some (KOTCB tcb) \<Longrightarrow> x \<notin> tcb_offs_range idle_tcb_ptr)
theory Example_Valid_StateH

lemma gt_imp_neq:
  "x > y \<Longrightarrow> x \<noteq> (y::'a::order)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y < x \<Longrightarrow> x \<noteq> y
theory Example_Valid_StateH

lemma option_update_range_map_comp:
  "option_update_range m m' = map_add m' m" by (simp add: fun_eq_iff option_update_range_def map_comp_def map_add_def
         split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. option_update_range m m' = m' ++ m
theory Example_Valid_StateH

lemma tcb_offs_in_rangeI:
  "\<lbrakk>ptr \<le> ptr + x; ptr + x \<le> ptr + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> ptr + x \<in> tcb_offs_range ptr" by (simp add: tcb_offs_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<le> ptr + x; ptr + x \<le> ptr + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> ptr + x \<in> tcb_offs_range ptr
theory Example_Valid_StateH

lemma mask_neg_add_aligned:
  "is_aligned q n \<Longrightarrow> p + q && ~~ mask n = (p && ~~ mask n) + q" apply (subst add.commute) apply (simp add: mask_out_add_aligned[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned q n \<Longrightarrow> p + q && ~~ mask n = (p && ~~ mask n) + q proof (prove)
goal (1 subgoal):
 1. is_aligned q n \<Longrightarrow> q + p && ~~ mask n = (p && ~~ mask n) + q proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma kh_s0H[simp]:
  "ksPSpace s0H_internal = kh0H" by (simp add: s0H_internal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace s0H_internal = kh0H
theory Example_Valid_StateH

lemma pspace_distinctD'':
  "\<lbrakk>\<exists>v. ksPSpace s x = Some v \<and> objBitsKO v = n; pspace_distinct' s\<rbrakk>
    \<Longrightarrow> ps_clear x n s" apply clarsimp apply (drule(1) pspace_distinctD') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>v. ksPSpace s x = Some v \<and> objBitsKO v = n; pspace_distinct' s\<rbrakk> \<Longrightarrow> ps_clear x n s proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>pspace_distinct' s; ksPSpace s x = Some v; n = objBitsKO v\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>pspace_distinct' s; n = objBitsKO v; ps_clear x (objBitsKO v) s\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma cnode_offs_min2':
  "is_aligned ptr 14 \<Longrightarrow> (ptr::word32) \<le> ptr + 0x10 * (x && mask 10)" apply (erule is_aligned_no_wrap') apply (subst mult.commute) apply (rule div_lt_mult) apply (cut_tac and_mask_less'[where n=10]) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x10 * (x && mask 10) proof (prove)
goal (1 subgoal):
 1. 0x10 * (x && mask 10) < 2 ^ 14 proof (prove)
goal (1 subgoal):
 1. (x && mask 10) * 0x10 < 2 ^ 14 proof (prove)
goal (2 subgoals):
 1. x && mask 10 < 2 ^ 14 div 0x10
 2. 0 < 0x10 proof (prove)
goal (3 subgoals):
 1. ?w6 && mask 10 < 2 ^ 10 \<Longrightarrow> x && mask 10 < 2 ^ 14 div 0x10
 2. 10 < LENGTH(?'a6)
 3. 0 < 0x10 proof (prove)
goal (2 subgoals):
 1. 10 < LENGTH(32)
 2. 0 < 0x10 proof (prove)
goal (1 subgoal):
 1. 0 < 0x10 proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma cnode_offs_min2:
  "Low_cnode_ptr \<le> Low_cnode_ptr + 0x10 * (x && mask 10)"
  "High_cnode_ptr \<le> High_cnode_ptr + 0x10 * (x && mask 10)"
  "Silc_cnode_ptr \<le> Silc_cnode_ptr + 0x10 * (x && mask 10)" by (simp_all add: cnode_offs_min2' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_cnode_ptr \<le> Low_cnode_ptr + 0x10 * (x && mask 10) &&& High_cnode_ptr \<le> High_cnode_ptr + 0x10 * (x && mask 10) &&& Silc_cnode_ptr \<le> Silc_cnode_ptr + 0x10 * (x && mask 10)
theory Example_Valid_StateH

lemma cnode_offs_max2:
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<le> Low_cnode_ptr + 0x3fff"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<le> High_cnode_ptr + 0x3fff"
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<le> Silc_cnode_ptr + 0x3fff" by (simp_all add: cnode_offs_max2' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_cnode_ptr + 0x10 * (x && mask 10) \<le> Low_cnode_ptr + 0x3FFF &&& High_cnode_ptr + 0x10 * (x && mask 10) \<le> High_cnode_ptr + 0x3FFF &&& Silc_cnode_ptr + 0x10 * (x && mask 10) \<le> Silc_cnode_ptr + 0x3FFF
theory Example_Valid_StateH

lemma cnode_offs_in_range2':
  "\<lbrakk>is_aligned ptr 14\<rbrakk> \<Longrightarrow>
     ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range ptr" apply (clarsimp simp: cnode_offs_min2' cnode_offs_max2' cnode_offs_range_def add.commute cte_level_bits_def) apply (rule is_aligned_add) apply (erule is_aligned_weaken) apply simp apply (rule_tac is_aligned_mult_triv1[where n=4, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 14 \<Longrightarrow> ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range ptr proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 14 \<Longrightarrow> is_aligned (ptr + 0x10 * (x && mask 10)) 4 proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> is_aligned ptr 4
 2. is_aligned ptr 14 \<Longrightarrow> is_aligned (0x10 * (x && mask 10)) 4 proof (prove)
goal (2 subgoals):
 1. 4 \<le> 14
 2. is_aligned ptr 14 \<Longrightarrow> is_aligned (0x10 * (x && mask 10)) 4 proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 14 \<Longrightarrow> is_aligned (0x10 * (x && mask 10)) 4 proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma cnode_offs_in_range2:
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range Silc_cnode_ptr"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range Low_cnode_ptr"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range High_cnode_ptr" by (simp_all add: cnode_offs_in_range2' s0_ptrs_aligned)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Silc_cnode_ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range Silc_cnode_ptr &&& Low_cnode_ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range Low_cnode_ptr &&& High_cnode_ptr + 0x10 * (x && mask 10) \<in> cnode_offs_range High_cnode_ptr