kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Refinement

lemma ADT_C_if_Init_Fin_serial_weak:
  "Init_Fin_serial_weak (ADT_C_if fp utf) s {s'.
                \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}" apply (rule Init_Fin_serial.serial_to_weak) apply (rule ADT_C_if_Init_Fin_serial) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial_weak (ADT_C_if fp utf) s {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial (ADT_C_if fp utf) s {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal:
No subgoals!
theory Noninterference_Refinement

lemma Fin_ADT_C_if:
  "Fin (ADT_C_if fp utf) ((uc, s), m) = ((uc, cstate_to_A s), m)" by (simp add: ADT_C_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Fin (ADT_C_if fp utf) ((uc, s), m) = ((uc, cstate_to_A s), m)
theory Noninterference_Refinement

lemma Fin_Init_s0_ADT_C_if:
  "s0' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> Fin (ADT_C_if fp utf) s0' = s0" by (clarsimp simp: ADT_C_if_def s0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s0' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> Fin (ADT_C_if fp utf) s0' = s0
theory Noninterference_Refinement

lemma xnonleakage_C:
  "abstract_to_C.conc.xNonleakage_gen" apply(rule abstract_to_C.xNonleakage_gen_refinement_closed) apply(rule xnonleakage) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abstract_to_C.xNonleakage_gen proof (prove)
goal (1 subgoal):
 1. xNonleakage_gen proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma s0_ptrs_aligned:
  "is_aligned init_global_pd 14"
  "is_aligned High_pd_ptr 14"
  "is_aligned Low_pd_ptr 14"
  "is_aligned High_pt_ptr 10"
  "is_aligned Low_pt_ptr 10"
  "is_aligned Silc_cnode_ptr 14"
  "is_aligned High_cnode_ptr 14"
  "is_aligned Low_cnode_ptr 14"
  "is_aligned High_tcb_ptr 9"
  "is_aligned Low_tcb_ptr 9"
  "is_aligned idle_tcb_ptr 9"
  "is_aligned ntfn_ptr 4"
  "is_aligned irq_cnode_ptr 10" by (simp_all add: is_aligned_def s0_ptr_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_aligned init_global_pd 14 &&& is_aligned High_pd_ptr 14 &&& is_aligned Low_pd_ptr 14) &&& is_aligned High_pt_ptr 10 &&& is_aligned Low_pt_ptr 10 &&& is_aligned Silc_cnode_ptr 14) &&& (is_aligned High_cnode_ptr 14 &&& is_aligned Low_cnode_ptr 14 &&& is_aligned High_tcb_ptr 9) &&& (is_aligned Low_tcb_ptr 9 &&& is_aligned idle_tcb_ptr 9) &&& is_aligned ntfn_ptr 4 &&& is_aligned irq_cnode_ptr 10
theory Example_Valid_StateH

lemma pd_offs_min':
  "is_aligned ptr 14 \<Longrightarrow> (ptr::32 word) \<le> ptr + (ucast (x:: 12 word) << 2)" apply (erule is_aligned_no_wrap'[OF _ ucast_less_shiftl_helper]) apply (simp add: word_bits_def) apply simp done

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

lemma pd_offs_min:
  "Low_pd_ptr \<le> Low_pd_ptr + (ucast (x:: 12 word) << 2)"
  "High_pd_ptr \<le> High_pd_ptr + (ucast (x:: 12 word) << 2)"
  "init_global_pd \<le> init_global_pd + (ucast (x:: 12 word) << 2)" by (simp_all add: pd_offs_min' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_pd_ptr \<le> Low_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2) &&& High_pd_ptr \<le> High_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2) &&& init_global_pd \<le> init_global_pd + (UCAST(12 \<rightarrow> 32) x << 2)
theory Example_Valid_StateH

lemma pd_offs_max':
  "is_aligned ptr 14 \<Longrightarrow> (ptr::word32) + (ucast (x:: 12 word) << 2) \<le> ptr + 0x3fff" apply (rule word_plus_mono_right) apply (simp add: shiftl_t2n mult.commute) apply (rule div_to_mult_word_lt) apply simp apply (rule plus_one_helper) apply simp apply (cut_tac ucast_less[where x=x]) 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 14 \<Longrightarrow> ptr + (UCAST(12 \<rightarrow> 32) x << 2) \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 2 \<le> 0x3FFF
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> UCAST(12 \<rightarrow> 32) x * 4 \<le> 0x3FFF
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> UCAST(12 \<rightarrow> 32) x \<le> 0x3FFF div 4
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> UCAST(12 \<rightarrow> 32) x \<le> 0xFFF
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 0xFFF + 1
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 0x1000
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; UCAST(12 \<rightarrow> ?'a31) x < 2 ^ LENGTH(12)\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 0x1000
 2. is_aligned ptr 14 \<Longrightarrow> LENGTH(12) < LENGTH(?'a31)
 3. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> LENGTH(12) < LENGTH(32)
 2. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 14 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. ptr \<le> ptr + 2 ^ 14 - 1 \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma pd_offs_max:
  "Low_pd_ptr + (ucast (x:: 12 word) << 2) \<le> Low_pd_ptr + 0x3fff"
  "High_pd_ptr + (ucast (x:: 12 word) << 2) \<le> High_pd_ptr + 0x3fff"
  "init_global_pd + (ucast (x:: 12 word) << 2) \<le> init_global_pd + 0x3fff" by (simp_all add: pd_offs_max' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2) \<le> Low_pd_ptr + 0x3FFF &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2) \<le> High_pd_ptr + 0x3FFF &&& init_global_pd + (UCAST(12 \<rightarrow> 32) x << 2) \<le> init_global_pd + 0x3FFF
theory Example_Valid_StateH

lemma pd_offs_in_range':
  "is_aligned ptr 14 \<Longrightarrow>
     ptr + (ucast (x:: 12 word) << 2) \<in> pd_offs_range ptr" apply (clarsimp simp: pd_offs_min' pd_offs_max' pd_offs_range_def add.commute) apply (rule is_aligned_add[OF _ is_aligned_shift]) apply (erule is_aligned_weaken) apply simp done

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

lemma pd_offs_in_range:
  "Low_pd_ptr + (ucast (x:: 12 word) << 2) \<in> pd_offs_range Low_pd_ptr"
  "High_pd_ptr + (ucast (x:: 12 word) << 2) \<in> pd_offs_range High_pd_ptr"
  "init_global_pd + (ucast (x:: 12 word) << 2) \<in> pd_offs_range init_global_pd" by (simp_all add: pd_offs_in_range' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2) \<in> pd_offs_range Low_pd_ptr &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2) \<in> pd_offs_range High_pd_ptr &&& init_global_pd + (UCAST(12 \<rightarrow> 32) x << 2) \<in> pd_offs_range init_global_pd
theory Example_Valid_StateH

lemma pd_offs_range_correct:
  "x \<in> pd_offs_range Low_pd_ptr \<Longrightarrow> \<exists>y. x = Low_pd_ptr + (ucast (y:: 12 word) << 2)"
  "x \<in> pd_offs_range High_pd_ptr \<Longrightarrow> \<exists>y. x = High_pd_ptr + (ucast (y:: 12 word) << 2)"
  "x \<in> pd_offs_range init_global_pd \<Longrightarrow> \<exists>y. x = init_global_pd + (ucast (y:: 12 word) << 2)" by (simp_all add: pd_offs_range_correct' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> pd_offs_range Low_pd_ptr \<Longrightarrow> \<exists>y. x = Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) &&& (x \<in> pd_offs_range High_pd_ptr \<Longrightarrow> \<exists>y. x = High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) &&& (x \<in> pd_offs_range init_global_pd \<Longrightarrow> \<exists>y. x = init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2))
theory Example_Valid_StateH

lemma pt_offs_min':
  "is_aligned ptr 10 \<Longrightarrow> (ptr::word32) \<le> ptr + (ucast (x:: 8 word) << 2)" apply (erule is_aligned_no_wrap') apply (rule ucast_less_shiftl_helper) apply (simp add: word_bits_def) apply simp done

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

lemma pt_offs_min:
  "Low_pt_ptr \<le> Low_pt_ptr + (ucast (x:: 8 word) << 2)"
  "High_pt_ptr \<le> High_pt_ptr + (ucast (x:: 8 word) << 2)" by (simp_all add: pt_offs_min' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_pt_ptr \<le> Low_pt_ptr + (UCAST(8 \<rightarrow> 32) x << 2) &&& High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) x << 2)
theory Example_Valid_StateH

lemma pt_offs_max':
  "is_aligned ptr 10 \<Longrightarrow> (ptr::word32) + (ucast (x:: 8 word) << 2) \<le> ptr + 0x3ff" apply (rule word_plus_mono_right) apply (simp add: shiftl_t2n mult.commute) apply (rule div_to_mult_word_lt) apply simp apply (rule plus_one_helper) apply simp apply (cut_tac ucast_less[where x=x]) 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 10 \<Longrightarrow> ptr + (UCAST(8 \<rightarrow> 32) x << 2) \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> UCAST(8 \<rightarrow> 32) x << 2 \<le> 0x3FF
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> UCAST(8 \<rightarrow> 32) x * 4 \<le> 0x3FF
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<le> 0x3FF div 4
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<le> 0xFF
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < 0xFF + 1
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < 0x100
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 10; UCAST(8 \<rightarrow> ?'a23) x < 2 ^ LENGTH(8)\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < 0x100
 2. is_aligned ptr 10 \<Longrightarrow> LENGTH(8) < LENGTH(?'a23)
 3. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (2 subgoals):
 1. is_aligned ptr 10 \<Longrightarrow> LENGTH(8) < LENGTH(32)
 2. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (1 subgoal):
 1. is_aligned ptr 10 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal (1 subgoal):
 1. ptr \<le> ptr + 2 ^ 10 - 1 \<Longrightarrow> ptr \<le> ptr + 0x3FF proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma pt_offs_max:
  "Low_pt_ptr + (ucast (x:: 8 word) << 2) \<le> Low_pt_ptr + 0x3ff"
  "High_pt_ptr + (ucast (x:: 8 word) << 2) \<le> High_pt_ptr + 0x3ff" by (simp_all add: pt_offs_max' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) x << 2) \<le> Low_pt_ptr + 0x3FF &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) x << 2) \<le> High_pt_ptr + 0x3FF
theory Example_Valid_StateH

lemma pt_offs_in_range':
  "is_aligned ptr 10 \<Longrightarrow>
     ptr + (ucast (x:: 8 word) << 2) \<in> pt_offs_range ptr" apply (clarsimp simp: pt_offs_min' pt_offs_max' pt_offs_range_def add.commute) apply (rule is_aligned_add[OF _ is_aligned_shift]) apply (erule is_aligned_weaken) apply simp done

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

lemma pt_offs_in_range:
  "Low_pt_ptr + (ucast (x:: 8 word) << 2) \<in> pt_offs_range Low_pt_ptr"
  "High_pt_ptr + (ucast (x:: 8 word) << 2) \<in> pt_offs_range High_pt_ptr" by (simp_all add: pt_offs_in_range' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) x << 2) \<in> pt_offs_range Low_pt_ptr &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) x << 2) \<in> pt_offs_range High_pt_ptr
theory Example_Valid_StateH

lemma pt_offs_range_correct:
  "x \<in> pt_offs_range Low_pt_ptr \<Longrightarrow> \<exists>y. x = Low_pt_ptr + (ucast (y:: 8 word) << 2)"
  "x \<in> pt_offs_range High_pt_ptr \<Longrightarrow> \<exists>y. x = High_pt_ptr + (ucast (y:: 8 word) << 2)" by (simp_all add: pt_offs_range_correct' s0_ptrs_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> pt_offs_range Low_pt_ptr \<Longrightarrow> \<exists>y. x = Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) &&& (x \<in> pt_offs_range High_pt_ptr \<Longrightarrow> \<exists>y. x = High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2))
theory Example_Valid_StateH

lemma bl_to_bin_le2p_aux:
  "bl_to_bin_aux bs w \<le> (w + 1) * (2 ^ length bs) - 1" apply (induct bs arbitrary: w) apply clarsimp apply clarsimp apply (rule conjI; clarsimp) apply (drule meta_spec, erule xtr8 [rotated], simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs w \<le> (w + 1) * 2 ^ length bs - 1 proof (prove)
goal (2 subgoals):
 1. \<And>w. bl_to_bin_aux [] w \<le> (w + 1) * 2 ^ length [] - 1
 2. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w \<le> (w + 1) * 2 ^ length bs - 1) \<Longrightarrow> bl_to_bin_aux (a # bs) w \<le> (w + 1) * 2 ^ length (a # bs) - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w \<le> (w + 1) * 2 ^ length bs - 1) \<Longrightarrow> bl_to_bin_aux (a # bs) w \<le> (w + 1) * 2 ^ length (a # bs) - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs) \<Longrightarrow> (a \<longrightarrow> bl_to_bin_aux bs (1 + 2 * w) < (w + 1) * (2 * 2 ^ length bs)) \<and> (\<not> a \<longrightarrow> bl_to_bin_aux bs (2 * w) < (w + 1) * (2 * 2 ^ length bs)) proof (prove)
goal (2 subgoals):
 1. \<And>a bs w. \<lbrakk>\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs; a\<rbrakk> \<Longrightarrow> bl_to_bin_aux bs (1 + 2 * w) < (w + 1) * (2 * 2 ^ length bs)
 2. \<And>a bs w. \<lbrakk>\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs; \<not> a\<rbrakk> \<Longrightarrow> bl_to_bin_aux bs (2 * w) < (w + 1) * (2 * 2 ^ length bs) proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma bl_to_bin_le2p: "bl_to_bin bs \<le> (2 ^ length bs) - 1" apply (unfold bl_to_bin_def) apply (rule xtr3) prefer 2 apply (rule bl_to_bin_le2p_aux) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs \<le> 2 ^ length bs - 1 proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs 0 \<le> 2 ^ length bs - 1 proof (prove)
goal (2 subgoals):
 1. 2 ^ length bs - 1 = ?b
 2. bl_to_bin_aux bs 0 \<le> ?b proof (prove)
goal (2 subgoals):
 1. bl_to_bin_aux bs 0 \<le> ?b
 2. 2 ^ length bs - 1 = ?b proof (prove)
goal (1 subgoal):
 1. 2 ^ length bs - 1 = (0 + 1) * 2 ^ length bs - 1 proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma of_bl_length_le:
  "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) \<le> 2 ^ k - 1" by (simp add: of_bl_length_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length x = k; k < LENGTH('a)\<rbrakk> \<Longrightarrow> of_bl x \<le> 2 ^ k - 1
theory Example_Valid_StateH

lemma cnode_offs_min:
  "length x = 10 \<Longrightarrow> Low_cnode_ptr \<le> Low_cnode_ptr + of_bl x * 0x10"
  "length x = 10 \<Longrightarrow> High_cnode_ptr \<le> High_cnode_ptr + of_bl x * 0x10"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr \<le> Silc_cnode_ptr + of_bl x * 0x10" by (simp_all add: cnode_offs_min' s0_ptrs_aligned)

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

lemma cnode_offs_max':
  "\<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> (ptr::word32) + of_bl x * 0x10 \<le> ptr + 0x3fff" apply (rule word_plus_mono_right) apply (rule div_to_mult_word_lt) apply simp apply (rule plus_one_helper) apply simp apply (drule of_bl_length_less[where '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. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr + of_bl x * 0x10 \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> of_bl x * 0x10 \<le> 0x3FFF
 2. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> of_bl x \<le> 0x3FFF div 0x10
 2. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> of_bl x \<le> 0x3FF
 2. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> of_bl x < 0x3FF + 1
 2. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> of_bl x < 0x400
 2. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (3 subgoals):
 1. is_aligned ptr 14 \<Longrightarrow> 10 < LENGTH(32)
 2. \<lbrakk>is_aligned ptr 14; of_bl x < 2 ^ 10\<rbrakk> \<Longrightarrow> of_bl x < 0x400
 3. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; of_bl x < 2 ^ 10\<rbrakk> \<Longrightarrow> of_bl x < 0x400
 2. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length x = 10; ptr \<le> ptr + 2 ^ 14 - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma cnode_offs_max:
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<le> Low_cnode_ptr + 0x3fff"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<le> High_cnode_ptr + 0x3fff"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<le> Silc_cnode_ptr + 0x3fff" by (simp_all add: cnode_offs_max' s0_ptrs_aligned)

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

lemma cnode_offs_in_range':
  "\<lbrakk>is_aligned ptr 14; length x = 10\<rbrakk> \<Longrightarrow>
     ptr + of_bl x * 0x10 \<in> cnode_offs_range ptr" apply (clarsimp simp: cnode_offs_min' cnode_offs_max' 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_triv2[where x="of_bl x" and n=4, simplified]) done

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

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

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

lemma le_mask_eq: "x \<le> 2 ^ n - 1 \<Longrightarrow> x AND mask n = (x :: 'a :: len word)" by (metis and_mask_eq_iff_le_mask mask_2pm1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> 2 ^ n - 1 \<Longrightarrow> x && mask n = x