theory Recycle_C

lemma heap_to_user_data_in_user_mem'[simp]:
  "\<lbrakk>pspace_aligned' as;pspace_distinct' as\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace as) (option_to_0 \<circ> user_mem' as) =
  heap_to_user_data (ksPSpace as)(underlying_memory (ksMachineState as))" apply (rule ext)+ apply (clarsimp simp: heap_to_user_data_def option_map_def
                 split: option.splits) apply (subst option_to_0_user_mem') apply (subst map_option_byte_to_word_heap) apply (clarsimp simp: projectKO_opt_user_data map_comp_def
                  split: option.split_asm kernel_object.split_asm) apply (frule(1) pspace_alignedD') apply (frule(1) pspace_distinctD') apply (subgoal_tac "x + ucast off * 4 + xa  && ~~ mask pageBits = x" ) apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def) apply (simp add: ARM.pageBits_def) apply (subst mask_lower_twice2[where n = 2 and m = 12,simplified,symmetric]) apply (subst is_aligned_add_helper[THEN conjunct2,where n1 = 2]) apply (erule aligned_add_aligned) apply (simp add: is_aligned_mult_triv2[where n = 2,simplified]) apply  (clarsimp simp: objBits_simps ARM.pageBits_def) apply simp apply (rule is_aligned_add_helper[THEN conjunct2]) apply (simp add: ARM.pageBits_def objBits_simps) apply (rule word_less_power_trans2[where k = 2,simplified]) apply (rule less_le_trans[OF ucast_less]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' as; pspace_distinct' as\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace as) (option_to_0 \<circ> user_mem' as) = heap_to_user_data (ksPSpace as) (underlying_memory (ksMachineState as)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_aligned' as; pspace_distinct' as\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace as) (option_to_0 \<circ> user_mem' as) x = heap_to_user_data (ksPSpace as) (underlying_memory (ksMachineState as)) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (option_to_0 \<circ> user_mem' as) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (\<lambda>x. if x \<in> {y. \<not> pointerInUserData y as} then 0 else underlying_memory (ksMachineState as) x) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x x2 off xa. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2; xa < 4\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 + xa \<notin> {y. \<not> pointerInUserData y as}
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData\<rbrakk> \<Longrightarrow> pointerInUserData (x + UCAST(10 \<rightarrow> 32) off * 4 + xa) as
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> pointerInUserData (x + UCAST(10 \<rightarrow> 32) off * 4 + xa) as
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> pointerInUserData (x + UCAST(10 \<rightarrow> 32) off * 4 + xa) as
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (3 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as; x + UCAST(10 \<rightarrow> 32) off * 4 + xa && ~~ mask pageBits = x\<rbrakk> \<Longrightarrow> pointerInUserData (x + UCAST(10 \<rightarrow> 32) off * 4 + xa) as
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 + xa && ~~ mask pageBits = x
 3. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 + xa && ~~ mask pageBits = x
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 + xa && ~~ mask 12 = x
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> (x + UCAST(10 \<rightarrow> 32) off * 4 + xa && ~~ mask 2) && ~~ mask 12 = x
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (4 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> is_aligned (x + UCAST(10 \<rightarrow> 32) off * 4) 2
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> xa < 2\<^sup>2
 3. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 && ~~ mask 12 = x
 4. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (5 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> is_aligned (UCAST(10 \<rightarrow> 32) off * 4) 2
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 2 \<le> objBitsKO KOUserData
 3. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> xa < 2\<^sup>2
 4. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 && ~~ mask 12 = x
 5. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (4 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 2 \<le> objBitsKO KOUserData
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> xa < 2\<^sup>2
 3. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 && ~~ mask 12 = x
 4. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (3 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> xa < 2\<^sup>2
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 && ~~ mask 12 = x
 3. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> x + UCAST(10 \<rightarrow> 32) off * 4 && ~~ mask 12 = x
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (3 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> is_aligned x 12
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) off * 4 < 2 ^ 12
 3. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (2 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) off * 4 < 2 ^ 12
 2. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (4 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) off < 2 ^ (12 - 2)
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 2 \<le> 12
 3. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 4. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal (5 subgoals):
 1. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> LENGTH(10) < LENGTH(32)
 2. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(10) \<le> 2 ^ (12 - 2)
 3. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 2 \<le> 12
 4. \<And>x off xa. \<lbrakk>xa < 4; pspace_aligned' as; pspace_distinct' as; ksPSpace as x = Some KOUserData; is_aligned x (objBitsKO KOUserData); ps_clear x (objBitsKO KOUserData) as\<rbrakk> \<Longrightarrow> 12 < LENGTH(32)
 5. \<And>x x2. \<lbrakk>pspace_aligned' as; pspace_distinct' as; map_to_user_data (ksPSpace as) x = Some x2\<rbrakk> \<Longrightarrow> byte_to_word_heap (underlying_memory (ksMachineState as)) x = byte_to_word_heap (underlying_memory (ksMachineState as)) x proof (prove)
goal:
No subgoals!