theory ADT_H

lemma cteMap_correct:
  assumes rel:              "(s,s') \<in> state_relation"
  assumes valid_objs:       "valid_objs s"
  assumes pspace_aligned:   "pspace_aligned s"
  assumes pspace_distinct:  "pspace_distinct s"
  assumes pspace_aligned':  "pspace_aligned' s'"
  assumes pspace_distinct': "pspace_distinct' s'"
  shows "p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map p) = p" proof - from rel have gsCNodes:
    "\<forall>a n. (\<exists>cs. kheap s a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) \<longleftrightarrow>
           gsCNodes s' a = Some n" by (simp add: state_relation_def ghost_relation_def) show ?thesis apply (simp add: dom_def cteMap_def  split: if_split_asm) apply (clarsimp simp: caps_of_state_cte_wp_at split: if_split_asm) apply (drule cte_wp_cte_at) apply (intro conjI impI) apply (rule some_equality) apply (clarsimp simp add: split_def) apply (frule gsCNodes[rule_format,THEN iffD2]) apply clarsimp apply (frule (1) cte_at_CNodeI) apply (frule (2) cte_map_inj_eq[OF _ _ _ valid_objs pspace_aligned pspace_distinct]) apply clarsimp apply (clarsimp simp add: split_def) apply (frule gsCNodes[rule_format,THEN iffD2]) apply clarsimp apply (frule (1) cte_at_CNodeI) apply (frule (2) cte_map_inj_eq[OF _ _ _ valid_objs pspace_aligned pspace_distinct]) apply clarsimp apply (case_tac p) apply (clarsimp simp add: cte_wp_at_cases) apply (erule disjE) apply clarsimp apply (drule_tac x=a in spec, drule_tac x=b in spec, simp) apply (cut_tac a=a and n=sz in gsCNodes[rule_format]) apply clarsimp apply (simp add: well_formed_cnode_n_def dom_def Collect_eq) apply (erule_tac x=b in allE) apply simp apply (thin_tac "ALL x. P x" for P) apply clarsimp apply (frule TCB_implies_KOTCB[OF state_relation_pspace_relation[OF rel]]) apply clarsimp using pspace_aligned'[simplified pspace_aligned'_def] apply (drule_tac x=a in bspec, simp add: dom_def) apply (simp add: objBitsKO_def cte_map_def) apply (rule conjI[rotated]) apply (drule tcb_cap_cases_length) apply (frule_tac b=b and c=cte_level_bits in bin_to_bl_of_bl_eq) apply (fastforce simp: cte_level_bits_def objBits_defs)+ apply (case_tac "b = [False, False, False]") apply simp apply (frule_tac b=b and c=cte_level_bits in bin_to_bl_of_bl_eq) apply (fastforce simp: tcb_cap_cases_length cte_level_bits_def objBits_defs)+ apply (subgoal_tac "ksPSpace s' (cte_map (a, b)) = None") prefer 2 apply (rule ccontr) apply clarsimp using pspace_distinct'[simplified pspace_distinct'_def] apply (drule_tac x=a in bspec, simp add: dom_def) apply (simp add: ps_clear_def dom_def mask_2pm1[symmetric] x_power_minus_1) apply (simp add: objBitsKO_def) apply (drule_tac a="cte_map (a, b)" in equals0D) apply (clarsimp simp add: cte_map_def) apply (drule tcb_cap_cases_length) apply (erule impE) apply (rule word_plus_mono_right) apply (cut_tac 'a=machine_word_len and xs=b in of_bl_length, fastforce simp: word_bits_conv) apply (drule_tac k="2^cte_level_bits" in word_mult_less_mono1) apply (fastforce simp: cte_level_bits_def objBits_defs)+ apply (simp add: mask_def) apply (rule ccontr) apply (simp add: not_le) apply (drule (1) less_trans, fastforce simp: cte_level_bits_def objBits_defs) apply (drule is_aligned_no_overflow'[simplified mask_2pm1[symmetric]]) apply (simp add: word_bits_conv) apply simp apply (erule impE) apply (drule is_aligned_no_overflow'[simplified mask_2pm1[symmetric]]) apply (cut_tac 'a=machine_word_len and xs=b in of_bl_length, simp add: word_bits_conv) apply (drule_tac k="2^cte_level_bits" in word_mult_less_mono1) apply (fastforce simp: cte_level_bits_def objBits_defs)+ apply (erule word_random) apply (rule order.strict_implies_order) apply (erule less_trans) apply (fastforce simp: cte_level_bits_def objBits_defs mask_def) apply (simp add: mult.commute[of _ "2^cte_level_bits"]
                    shiftl_t2n[of _ cte_level_bits, simplified, symmetric]) apply word_bitwise apply simp apply (case_tac b, simp) apply (rename_tac b, case_tac b, simp) apply (rename_tac b, case_tac b, simp) apply (clarsimp simp add: test_bit_of_bl eval_nat_numeral cte_level_bits_def) apply (simp add: cte_map_def split: option.splits) apply (drule tcb_cap_cases_length) apply (rule of_bl_mult_and_not_mask_eq[where m=cte_level_bits, simplified]) apply (fastforce simp: cte_level_bits_def objBits_defs)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map p) = p proof (state)
goal (1 subgoal):
 1. p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map p) = p proof (chain)
picking this:
(s, s') \<in> state_relation proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. \<forall>a n. (\<exists>cs. kheap s a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (gsCNodes s' a = Some n) proof (state)
this:
\<forall>a n. (\<exists>cs. kheap s a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (gsCNodes s' a = Some n)

goal (1 subgoal):
 1. p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map p) = p proof (prove)
goal (1 subgoal):
 1. p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map p) = p proof (prove)
goal (1 subgoal):
 1. ((\<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b)) \<longrightarrow> (\<exists>y. caps_of_state s p = Some y) \<longrightarrow> (SOME (a, bl). cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)) = p) \<and> ((\<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)) \<longrightarrow> (\<exists>y. caps_of_state s p = Some y) \<longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p) proof (prove)
goal (1 subgoal):
 1. \<And>cap. cte_wp_at ((=) cap) p s \<Longrightarrow> ((\<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b)) \<longrightarrow> (SOME (a, bl). cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)) = p) \<and> ((\<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)) \<longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p) proof (prove)
goal (1 subgoal):
 1. \<And>cap. cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> ((\<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b)) \<longrightarrow> (SOME (a, bl). cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)) = p) \<and> ((\<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)) \<longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b)\<rbrakk> \<Longrightarrow> (SOME (a, bl). cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)) = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b)\<rbrakk> \<Longrightarrow> case p of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)
 2. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 3. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b)\<rbrakk> \<Longrightarrow> gsCNodes s' (fst p) = Some (length (snd p))
 2. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 3. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); \<exists>cs. kheap s a = Some (CNode (length b) cs) \<and> well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> gsCNodes s' (fst p) = Some (length (snd p))
 2. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 3. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (3 subgoals):
 1. \<And>a b cs. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> gsCNodes s' (fst p) = Some (length (snd p))
 2. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 3. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (3 subgoals):
 1. \<And>a b cs. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs; cte_wp_at (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> gsCNodes s' (fst p) = Some (length (snd p))
 2. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 3. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (3 subgoals):
 1. \<And>a b cs. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs; cte_wp_at (\<lambda>_. True) (a, b) s; (a, b) = p\<rbrakk> \<Longrightarrow> gsCNodes s' (fst p) = Some (length (snd p))
 2. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 3. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<exists>a b. cte_map (a, b) = cte_map p \<and> gsCNodes s' a = Some (length b); case x of (a, bl) \<Rightarrow> cte_map (a, bl) = cte_map p \<and> gsCNodes s' a = Some (length bl)\<rbrakk> \<Longrightarrow> x = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); cte_map (aa, ba) = cte_map p; gsCNodes s' aa = Some (length ba)\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); cte_map (aa, ba) = cte_map p; gsCNodes s' aa = Some (length ba); \<exists>cs. kheap s a = Some (CNode (length b) cs) \<and> well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cs. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); cte_map (aa, ba) = cte_map p; gsCNodes s' aa = Some (length ba); kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cs. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); cte_map (aa, ba) = cte_map p; gsCNodes s' aa = Some (length ba); kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs; cte_wp_at (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cs. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_map (a, b) = cte_map p; gsCNodes s' a = Some (length b); cte_map (aa, ba) = cte_map p; gsCNodes s' aa = Some (length ba); kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs; cte_wp_at (\<lambda>_. True) (a, b) s; (a, b) = p\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<forall>a b. cte_map (a, b) = cte_map p \<longrightarrow> gsCNodes s' a \<noteq> Some (length b); p = (a, b)\<rbrakk> \<Longrightarrow> (cte_map p && ~~ mask tcbBlockSizeBits, bin_to_bl_aux 3 (uint (cte_map p >> cte_level_bits)) []) = p proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(\<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap)) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr)); \<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b)\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); \<exists>sz fun. kheap s a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap)\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; gsCNodes s' a \<noteq> Some (length b)\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; gsCNodes s' a \<noteq> Some (length b); (\<exists>cs. kheap s a = Some (CNode sz cs) \<and> well_formed_cnode_n sz cs) = (gsCNodes s' a = Some sz)\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; sz \<noteq> length b; gsCNodes s' a = Some sz\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); \<forall>a. (\<exists>y. fun a = Some y) = (length a = sz); fun b = Some cap; sz \<noteq> length b; gsCNodes s' a = Some sz\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); fun b = Some cap; sz \<noteq> length b; gsCNodes s' a = Some sz; (\<exists>y. fun b = Some y) = (length b = sz)\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b
 2. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>aa ba. cte_map (aa, ba) = cte_map (a, b) \<longrightarrow> gsCNodes s' aa \<noteq> Some (length ba); p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p = (a, b); (\<exists>tcb. kheap s a = Some (TCB tcb)) \<and> (\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
using this:
\<forall>x\<in>dom (ksPSpace s'). is_aligned x (objBitsKO (the (ksPSpace s' x)))

goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a (objBitsKO (the (ksPSpace s' a)))\<rbrakk> \<Longrightarrow> cte_map (a, b) && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (cte_map (a, b) >> cte_level_bits)) [] = b proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a \<and> bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits\<rbrakk> \<Longrightarrow> bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; length b = 3\<rbrakk> \<Longrightarrow> bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; length b = 3\<rbrakk> \<Longrightarrow> length b + cte_level_bits \<le> tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; length b = 3\<rbrakk> \<Longrightarrow> length b + cte_level_bits < LENGTH(32)
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; length b = 3; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b\<rbrakk> \<Longrightarrow> bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b = [False, False, False]\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]\<rbrakk> \<Longrightarrow> length b + cte_level_bits \<le> tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]\<rbrakk> \<Longrightarrow> length b + cte_level_bits < LENGTH(32)
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b\<rbrakk> \<Longrightarrow> ksPSpace s' (cte_map (a, b)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b\<rbrakk> \<Longrightarrow> ksPSpace s' (cte_map (a, b)) = None
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) \<noteq> None\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (cte_map (a, b)) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
using this:
\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'

goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (cte_map (a, b)) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (cte_map (a, b)) = Some y; ps_clear a (objBitsKO (the (ksPSpace s' a))) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (cte_map (a, b)) = Some y; (mask_range a (objBitsKO (KOTCB tcb')) - {a}) \<inter> {a. \<exists>y. ksPSpace s' a = Some y} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (cte_map (a, b)) = Some y; (mask_range a tcbBlockSizeBits - {a}) \<inter> {a. \<exists>y. ksPSpace s' a = Some y} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (cte_map (a, b)) = Some y; cte_map (a, b) \<notin> (mask_range a tcbBlockSizeBits - {a}) \<inter> {a. \<exists>y. ksPSpace s' a = Some y}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; a + of_bl b * 2 ^ cte_level_bits \<le> a + mask tcbBlockSizeBits \<longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; a + of_bl b * 2 ^ cte_level_bits \<le> a + mask tcbBlockSizeBits \<longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0; length b = 3\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits \<le> a + mask tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits \<le> mask tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b < 2 ^ length b\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits \<le> mask tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (6 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> 0 < 2 ^ cte_level_bits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> unat (2 ^ length b) * unat (2 ^ cte_level_bits) < 2 ^ LENGTH(32)
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 2 ^ length b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits \<le> mask tcbBlockSizeBits
 4. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 5. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 6. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 2 ^ length b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits \<le> mask tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 8 * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits \<le> 2 ^ tcbBlockSizeBits - 1
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 8 * 2 ^ cte_level_bits; \<not> of_bl b * 2 ^ cte_level_bits \<le> 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (4 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 8 * 2 ^ cte_level_bits; 2 ^ tcbBlockSizeBits - 1 < of_bl b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 3. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a \<le> a + mask tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + of_bl b * 2 ^ cte_level_bits \<longrightarrow> of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits\<rbrakk> \<Longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits; of_bl b < 2 ^ length b\<rbrakk> \<Longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (5 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 0 < 2 ^ cte_level_bits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits\<rbrakk> \<Longrightarrow> unat (2 ^ length b) * unat (2 ^ cte_level_bits) < 2 ^ LENGTH(32)
 3. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits; of_bl b * 2 ^ cte_level_bits < 2 ^ length b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits
 4. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 5. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; a \<le> a + mask tcbBlockSizeBits; of_bl b * 2 ^ cte_level_bits < 2 ^ length b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> a \<le> a + of_bl b * 2 ^ cte_level_bits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 2 ^ length b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits \<le> mask tcbBlockSizeBits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits < 2 ^ length b * 2 ^ cte_level_bits\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ cte_level_bits < mask tcbBlockSizeBits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3\<rbrakk> \<Longrightarrow> 2 ^ length b * 2 ^ cte_level_bits < mask tcbBlockSizeBits
 2. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = Some y; length b = 3; of_bl b * 2 ^ cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some y; tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a >> cte_level_bits)) [] = b; KOTCB tcb' = y; length b = 3; of_bl b << cte_level_bits = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some y; tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a >> cte_level_bits)) [] = b; KOTCB tcb' = y; length b = 3; takefill False (Suc (Suc (Suc (Suc 28)))) (replicate cte_level_bits False @ [of_bl b !! 0, of_bl b !! 1, of_bl b !! 2, of_bl b !! 3, of_bl b !! 4, of_bl b !! 5, of_bl b !! 6, of_bl b !! 7, of_bl b !! 8, of_bl b !! 9, of_bl b !! 10, of_bl b !! 11, of_bl b !! 12, of_bl b !! 13, of_bl b !! 14, of_bl b !! 15, of_bl b !! 16, of_bl b !! 17, of_bl b !! 18, of_bl b !! 19, of_bl b !! 20, of_bl b !! 21, of_bl b !! 22, of_bl b !! 23, of_bl b !! 24, of_bl b !! 25, of_bl b !! 26, of_bl b !! 27, of_bl b !! 28, of_bl b !! 29, of_bl b !! 30, of_bl b !! 31]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb tcb' y. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some y; tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a >> cte_level_bits)) [] = b; KOTCB tcb' = y; length b = 3; takefill False 32 (replicate cte_level_bits False @ [rev b ! 0, rev b ! Suc 0, rev b ! 2, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb tcb' y aa list. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some y; tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a >> cte_level_bits)) [] = b; KOTCB tcb' = y; length b = 3; takefill False 32 (replicate cte_level_bits False @ [rev b ! 0, rev b ! Suc 0, rev b ! 2, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]; b = aa # list\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a ba tcb tcb' y aa b ab list. \<lbrakk>p = (a, ba); kheap s a = Some (TCB tcb); ksPSpace s' a = Some y; tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; ba \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a >> cte_level_bits)) [] = ba; KOTCB tcb' = y; length ba = 3; takefill False 32 (replicate cte_level_bits False @ [rev ba ! 0, rev ba ! Suc 0, rev ba ! 2, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]; ba = aa # b; b = ab # list\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a ba tcb tcb' y aa bb ab b ac list. \<lbrakk>p = (a, ba); kheap s a = Some (TCB tcb); ksPSpace s' a = Some y; tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; ba \<noteq> [False, False, False]; bin_to_bl_aux 3 (uint (a >> cte_level_bits)) [] = ba; KOTCB tcb' = y; length ba = 3; takefill False 32 (replicate cte_level_bits False @ [rev ba ! 0, rev ba ! Suc 0, rev ba ! 2, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]; ba = aa # bb; bb = ab # b; b = ac # list\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) = b; ksPSpace s' (cte_map (a, b)) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = None\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = None; length b = 3\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ cte_level_bits && ~~ mask tcbBlockSizeBits = a proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = None; length b = 3\<rbrakk> \<Longrightarrow> is_aligned a tcbBlockSizeBits
 2. \<And>a b tcb get set restr tcb'. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); ksPSpace s' a = Some (KOTCB tcb'); tcb_relation tcb tcb'; is_aligned a tcbBlockSizeBits; b \<noteq> [False, False, False]; bin_to_bl_aux (length b) (uint (a + of_bl b * 2 ^ cte_level_bits >> cte_level_bits)) [] = b; ksPSpace s' (a + of_bl b * 2 ^ cte_level_bits) = None; length b = 3\<rbrakk> \<Longrightarrow> length b + cte_level_bits \<le> tcbBlockSizeBits proof (prove)
goal:
No subgoals! proof (state)
this:
p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map p) = p

goal:
No subgoals!