theory KHeap_DR

lemma cdl_resolve_address_bits_eq:
  "a+t\<le> length cref \<and> length cref \<le> 32\<longrightarrow>
  CSpace_D.resolve_address_bits cap (of_bl cref) t =
  CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) t" proof (induct t  arbitrary: a cap cref rule: less_induct) case (less t) show ?case apply clarify apply (subst KHeap_DR.resolve_address_bits.simps,rule sym) apply (subst KHeap_DR.resolve_address_bits.simps) apply (subst bindE_def,rule sym,subst bindE_def) apply (rule bind_eqI,rule arg_cong[where f="\<lambda>x. lift (K_bind x)"]) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI,rule arg_cong[where f=lift],rule ext) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI,rule arg_cong[where f=lift],rule ext) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI,rule arg_cong[where f=lift],rule ext) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI,rule arg_cong[where f=lift],rule ext) apply (subst bindE_def,rule sym,subst bindE_def) apply (rule ext,simp add:returnOk_def lift_def) apply (case_tac "\<not> (0<radix_size \<or> 0<guard_size)") apply (clarsimp simp:assertE_def) apply (clarsimp simp:assertE_def) apply (rule_tac x=x in fun_cong) apply (subst bindE_def,rule sym,subst bindE_def) apply (case_tac "\<not> guard_size \<le> t") apply (clarsimp simp:unlessE_def bind_def return_def returnOk_def lift_def) apply (rule bind_eqI') apply (clarsimp simp:returnOk_def return_def) apply (rule ext) apply (clarsimp simp:of_bl_drop shiftr_over_and_dist) apply (subst shiftr_mask2) apply clarsimp apply arith apply (simp add: mask_twice) apply (rule arg_cong[where f=lift],rule ext) apply (clarsimp simp:unlessE_def whenE_def return_def) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI') apply (rule ext) apply (clarsimp simp:of_bl_drop shiftr_over_and_dist) apply (subst shiftr_mask2) apply clarsimp apply arith apply (simp add:return_def mask_twice) apply (rule arg_cong[where f=lift],rule ext) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI') apply clarsimp apply (rule arg_cong[where f=lift],rule ext) apply (subst bindE_def,rule sym,subst bindE_def) apply (rule ext,clarsimp simp:bind_def lift_def) apply (rule_tac x = x in fun_cong) apply (subst bindE_def,rule sym,subst bindE_def,rule bind_eqI,rule arg_cong[where f=lift],rule ext)+ apply (clarsimp split:if_splits) apply (rule "less.hyps"[rule_format]) apply fastforce+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + t \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) t = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) t proof (state)
goal (1 subgoal):
 1. \<And>x a cap cref. (\<And>y a cap cref. y < x \<Longrightarrow> a + y \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) y = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) y) \<Longrightarrow> a + x \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) x = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) x proof (state)
this:
?y < t \<Longrightarrow> ?a + ?y \<le> length ?cref \<and> length ?cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits ?cap (of_bl ?cref) ?y = CSpace_D.resolve_address_bits ?cap (of_bl (drop ?a ?cref)) ?y

goal (1 subgoal):
 1. \<And>x a cap cref. (\<And>y a cap cref. y < x \<Longrightarrow> a + y \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) y = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) y) \<Longrightarrow> a + x \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) x = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) x proof (prove)
goal (1 subgoal):
 1. a + t \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) t = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) t = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) t = doE unlessE (Types_D.is_cnode_cap cap) $ throw;
cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> doE unlessE (Types_D.is_cnode_cap cap) $ throw;
cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE = doE unlessE (Types_D.is_cnode_cap cap) $ throw;
cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> (unlessE (Types_D.is_cnode_cap cap) $ throw) >>= lift (K_bind (doE cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE)) = (unlessE (Types_D.is_cnode_cap cap) $ throw) >>= lift (K_bind (doE cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> doE cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE = doE cnode <- liftE $ get_cnode $ cap_object cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>cnode. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> doE radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE = doE radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>cnode radix_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> doE guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE = doE guard_size <- returnOk $ cap_guard_size cap;
cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>cnode radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> doE cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE = doE cap_guard <- returnOk $ cap_guard cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>cnode radix_size guard_size cap_guard. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> doE level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE = doE level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>cnode radix_size guard_size cap_guard. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> returnOk (radix_size + guard_size) >>= lift (\<lambda>level_size. doE assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl (drop a cref) >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl (drop a cref) >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = returnOk (radix_size + guard_size) >>= lift (\<lambda>level_size. doE assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> t - guard_size) && mask guard_size;
unlessE (guard_size \<le> t \<and> guard = cap_guard) $ throw;
whenE (t < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> t - level_size) && mask radix_size;
slot <- returnOk (cap_object cap, unat offset);
size_left <- returnOk (t - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32\<rbrakk> \<Longrightarrow> (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) x = (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl cref >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) x proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; \<not> (0 < radix_size \<or> 0 < guard_size)\<rbrakk> \<Longrightarrow> (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) x = (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl cref >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) x
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; \<not> \<not> (0 < radix_size \<or> 0 < guard_size)\<rbrakk> \<Longrightarrow> (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) x = (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl cref >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) x proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; \<not> \<not> (0 < radix_size \<or> 0 < guard_size)\<rbrakk> \<Longrightarrow> (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) x = (doE y <- assertE (0 < radix_size \<or> 0 < guard_size);
guard <- return (Inr ((of_bl cref >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) x proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size\<rbrakk> \<Longrightarrow> (doE guard <- return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) x = (doE guard <- return (Inr ((of_bl cref >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) x proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size\<rbrakk> \<Longrightarrow> doE guard <- return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE = doE guard <- return (Inr ((of_bl cref >> t - guard_size) && mask guard_size));
y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size\<rbrakk> \<Longrightarrow> return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> guard_size \<le> t\<rbrakk> \<Longrightarrow> return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE)
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t\<rbrakk> \<Longrightarrow> return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t\<rbrakk> \<Longrightarrow> return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size)) >>= lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t\<rbrakk> \<Longrightarrow> return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False))
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size s. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False) = ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> (of_bl cref >> t - guard_size) && mask guard_size = ((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (3 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> length cref - a \<le> LENGTH(32)
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> (of_bl cref >> t - guard_size) && mask guard_size = ((of_bl cref >> t - guard_size) && mask (length cref - a - (t - guard_size))) && mask guard_size
 3. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (3 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> length cref - a \<le> 32
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> (of_bl cref >> t - guard_size) && mask guard_size = ((of_bl cref >> t - guard_size) && mask (length cref - a - (t - guard_size))) && mask guard_size
 3. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; guard_size \<le> t\<rbrakk> \<Longrightarrow> (of_bl cref >> t - guard_size) && mask guard_size = ((of_bl cref >> t - guard_size) && mask (length cref - a - (t - guard_size))) && mask guard_size
 2. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>guard. doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size cap_guard x guard. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; \<not> \<not> guard_size \<le> t; return (Inr ((of_bl cref >> t - guard_size) && mask guard_size)) = return (Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size))\<rbrakk> \<Longrightarrow> doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE = doE y <- unlessE (guard_size \<le> t \<and> guard = cap_guard) throw;
y <- whenE (t < radix_size + guard_size) throw;
offset <- return (Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size));
slot <- return (Inr (cap_object cap, unat offset));
size_left <- return (Inr (t - (radix_size + guard_size)));
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> doE offset <- \<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False);
slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE = doE offset <- \<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False);
slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size s. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False) = ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr (((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> ((of_bl cref >> t - (radix_size + guard_size)) && (mask (length cref - a) >> t - (radix_size + guard_size))) && mask radix_size = (of_bl cref >> t - (radix_size + guard_size)) && mask radix_size
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (3 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr (((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> length cref - a \<le> LENGTH(32)
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr (((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> ((of_bl cref >> t - (radix_size + guard_size)) && mask (length cref - a - (t - (radix_size + guard_size)))) && mask radix_size = (of_bl cref >> t - (radix_size + guard_size)) && mask radix_size
 3. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (3 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr (((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> length cref - a \<le> 32
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr (((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> ((of_bl cref >> t - (radix_size + guard_size)) && mask (length cref - a - (t - (radix_size + guard_size)))) && mask radix_size = (of_bl cref >> t - (radix_size + guard_size)) && mask radix_size
 3. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr (((of_bl cref >> t - guard_size) && (mask (length cref - a) >> t - guard_size)) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size\<rbrakk> \<Longrightarrow> ((of_bl cref >> t - (radix_size + guard_size)) && mask (length cref - a - (t - (radix_size + guard_size)))) && mask radix_size = (of_bl cref >> t - (radix_size + guard_size)) && mask radix_size
 2. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>offset. doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size offset. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE = doE slot <- \<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False);
size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size offset. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False))\<rbrakk> \<Longrightarrow> (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False)) = (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False))
 2. \<And>radix_size guard_size offset. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False)) = (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>slot. doE size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>slot. doE size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size offset. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False)) = (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False))\<rbrakk> \<Longrightarrow> lift (\<lambda>slot. doE size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE) = lift (\<lambda>slot. doE size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size offset slot. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False)) = (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False))\<rbrakk> \<Longrightarrow> doE size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE
odE = doE size_left <- \<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size offset slot. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False)) = (\<lambda>s. ({(Inr (cap_object cap, unat offset), s)}, False))\<rbrakk> \<Longrightarrow> (\<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False)) >>= lift (\<lambda>size_left. if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) size_left else returnOk (slot, size_left)
odE) = (\<lambda>s. ({(Inr (t - (radix_size + guard_size)), s)}, False)) >>= lift (\<lambda>size_left. if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) size_left else returnOk (slot, size_left)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size a b x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); t \<noteq> radix_size + guard_size\<rbrakk> \<Longrightarrow> (doE next_cap <- liftE (KHeap_D.get_cap (a, b));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) (t - (radix_size + guard_size)) else returnOk ((a, b), t - (radix_size + guard_size))
odE) x = (doE next_cap <- liftE (KHeap_D.get_cap (a, b));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (t - (radix_size + guard_size)) else returnOk ((a, b), t - (radix_size + guard_size))
odE) x proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size a b x. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); t \<noteq> radix_size + guard_size\<rbrakk> \<Longrightarrow> doE next_cap <- liftE (KHeap_D.get_cap (a, b));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) (t - (radix_size + guard_size)) else returnOk ((a, b), t - (radix_size + guard_size))
odE = doE next_cap <- liftE (KHeap_D.get_cap (a, b));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (t - (radix_size + guard_size)) else returnOk ((a, b), t - (radix_size + guard_size))
odE proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size a b x next_cap. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); t \<noteq> radix_size + guard_size\<rbrakk> \<Longrightarrow> (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (t - (radix_size + guard_size)) else returnOk ((a, b), t - (radix_size + guard_size))) = (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) (t - (radix_size + guard_size)) else returnOk ((a, b), t - (radix_size + guard_size))) proof (prove)
goal (1 subgoal):
 1. \<And>radix_size guard_size next_cap. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); t \<noteq> radix_size + guard_size; Types_D.is_cnode_cap next_cap\<rbrakk> \<Longrightarrow> CSpace_D.resolve_address_bits next_cap (of_bl cref) (t - (radix_size + guard_size)) = CSpace_D.resolve_address_bits next_cap (of_bl (drop a cref)) (t - (radix_size + guard_size)) proof (prove)
goal (2 subgoals):
 1. \<And>radix_size guard_size next_cap. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); t \<noteq> radix_size + guard_size; Types_D.is_cnode_cap next_cap\<rbrakk> \<Longrightarrow> t - (radix_size + guard_size) < t
 2. \<And>radix_size guard_size next_cap. \<lbrakk>a + t \<le> length cref; length cref \<le> 32; 0 < radix_size \<or> 0 < guard_size; (\<lambda>s. ({(Inr ((of_bl cref >> t - guard_size) && mask guard_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - guard_size) && mask guard_size), s)}, False)); \<not> t < radix_size + guard_size; (\<lambda>s. ({(Inr ((of_bl (drop a cref) >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)) = (\<lambda>s. ({(Inr ((of_bl cref >> t - (radix_size + guard_size)) && mask radix_size), s)}, False)); t \<noteq> radix_size + guard_size; Types_D.is_cnode_cap next_cap\<rbrakk> \<Longrightarrow> a + (t - (radix_size + guard_size)) \<le> length cref \<and> length cref \<le> 32 proof (prove)
goal:
No subgoals! proof (state)
this:
a + t \<le> length cref \<and> length cref \<le> 32 \<longrightarrow> CSpace_D.resolve_address_bits cap (of_bl cref) t = CSpace_D.resolve_address_bits cap (of_bl (drop a cref)) t

goal:
No subgoals!