theory Lookups_D

lemma gets_the_resolve_cap:
  "gets_the (resolve_cap cnode_cap cap_ptr remaining_size) =
   resolve_address_bits cnode_cap cap_ptr remaining_size" apply (induct cnode_cap cap_ptr remaining_size rule: resolve_cap.induct [simplified]) apply (subst resolve_cap.simps) apply (subst resolve_address_bits.simps) apply (clarsimp simp: unlessE_def liftE_bindE assertE_liftE gets_the_get_cnode) apply (rule bind_cong, rule refl) apply (rule bind_apply_cong, rule refl) apply (clarsimp simp: liftE_bindE) apply (rule bind_apply_cong, rule refl) apply (clarsimp simp: in_monad gets_the_get_cnode [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (resolve_cap cnode_cap cap_ptr remaining_size) = resolve_address_bits cnode_cap cap_ptr remaining_size proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size. (\<And>v s va. \<lbrakk>is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) \<Longrightarrow> gets_the (resolve_cap cnode_cap cap_ptr remaining_size) = resolve_address_bits cnode_cap cap_ptr remaining_size proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size. (\<And>v s va. \<lbrakk>is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) \<Longrightarrow> gets_the (if is_cnode_cap cnode_cap then do {
  cnode \<leftarrow> opt_cnode $ cap_object cnode_cap;
radix_size \<leftarrow> oreturn $ cdl_cnode_size_bits cnode;
guard_size \<leftarrow> oreturn $ cap_guard_size cnode_cap;
cap_guard \<leftarrow> oreturn $ cap_guard cnode_cap;
level_size \<leftarrow> oreturn (radix_size + guard_size);
oassert (level_size \<noteq> 0) >>= K_bind (do {
  guard \<leftarrow> oreturn $ (cap_ptr >> remaining_size - guard_size) && mask guard_size;
if \<not> (guard_size \<le> remaining_size \<and> guard = cap_guard) \<or> remaining_size < level_size then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> remaining_size - level_size) && mask radix_size;
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (remaining_size - level_size);
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}
})
} else othrow FaultError) = resolve_address_bits cnode_cap cap_ptr remaining_size proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size. (\<And>v s va. \<lbrakk>is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) \<Longrightarrow> gets_the (if is_cnode_cap cnode_cap then do {
  cnode \<leftarrow> opt_cnode $ cap_object cnode_cap;
radix_size \<leftarrow> oreturn $ cdl_cnode_size_bits cnode;
guard_size \<leftarrow> oreturn $ cap_guard_size cnode_cap;
cap_guard \<leftarrow> oreturn $ cap_guard cnode_cap;
level_size \<leftarrow> oreturn (radix_size + guard_size);
oassert (level_size \<noteq> 0) >>= K_bind (do {
  guard \<leftarrow> oreturn $ (cap_ptr >> remaining_size - guard_size) && mask guard_size;
if \<not> (guard_size \<le> remaining_size \<and> guard = cap_guard) \<or> remaining_size < level_size then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> remaining_size - level_size) && mask radix_size;
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (remaining_size - level_size);
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}
})
} else othrow FaultError) = doE unlessE (is_cnode_cap cnode_cap) $ throw;
cnode <- liftE $ get_cnode $ cap_object cnode_cap;
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cnode_cap;
cap_guard <- returnOk $ cap_guard cnode_cap;
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (cap_ptr >> remaining_size - guard_size) && mask guard_size;
unlessE (guard_size \<le> remaining_size \<and> guard = cap_guard) $ throw;
whenE (remaining_size < level_size) $ throw;
offset <- returnOk $ (cap_ptr >> remaining_size - level_size) && mask radix_size;
slot <- returnOk (cap_object cnode_cap, unat offset);
size_left <- returnOk (remaining_size - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ get_cap slot;
if is_cnode_cap next_cap then resolve_address_bits next_cap cap_ptr size_left else returnOk (slot, size_left)
odE
odE proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size. \<lbrakk>\<And>v s va. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)); cap_guard_size cnode_cap \<le> remaining_size; (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap\<rbrakk> \<Longrightarrow> do x <- get_cnode (cap_object cnode_cap);
xa <- assert (0 < cdl_cnode_size_bits x \<or> 0 < cap_guard_size cnode_cap);
gets_the (if remaining_size < cdl_cnode_size_bits x + cap_guard_size cnode_cap then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> remaining_size - (cdl_cnode_size_bits x + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (remaining_size - (cdl_cnode_size_bits x + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
})
od = do cnode <- get_cnode (cap_object cnode_cap);
y <- assert (0 < cdl_cnode_size_bits cnode \<or> 0 < cap_guard_size cnode_cap);
doE y <- whenE (remaining_size < cdl_cnode_size_bits cnode + cap_guard_size cnode_cap) throw;
if remaining_size \<le> cdl_cnode_size_bits cnode + cap_guard_size cnode_cap then returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ get_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits cnode)));
if is_cnode_cap next_cap then resolve_address_bits next_cap cap_ptr (remaining_size - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap)) else returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits cnode))), remaining_size - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap))
odE
odE
od proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size v s s'. \<lbrakk>\<And>v s va. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)); cap_guard_size cnode_cap \<le> remaining_size; (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; (v, s') \<in> fst (get_cnode (cap_object cnode_cap) s)\<rbrakk> \<Longrightarrow> (do x <- assert (0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap);
gets_the (if remaining_size < cdl_cnode_size_bits v + cap_guard_size cnode_cap then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
})
od) s' = (do y <- assert (0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap);
doE y <- whenE (remaining_size < cdl_cnode_size_bits v + cap_guard_size cnode_cap) throw;
if remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap then returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), 0) else doE next_cap <- liftE $ get_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v)));
if is_cnode_cap next_cap then resolve_address_bits next_cap cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) else returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))
odE
odE
od) s' proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size v s s' rv st. \<lbrakk>\<And>v s va. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)); cap_guard_size cnode_cap \<le> remaining_size; (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; (v, s') \<in> fst (get_cnode (cap_object cnode_cap) s); (rv, st) \<in> fst (assert (0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap) s')\<rbrakk> \<Longrightarrow> gets_the (if remaining_size < cdl_cnode_size_bits v + cap_guard_size cnode_cap then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) st = (doE y <- whenE (remaining_size < cdl_cnode_size_bits v + cap_guard_size cnode_cap) throw;
if remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap then returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), 0) else doE next_cap <- liftE $ get_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v)));
if is_cnode_cap next_cap then resolve_address_bits next_cap cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) else returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))
odE
odE) st proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size v s s' st. \<lbrakk>\<And>v s va. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)); (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; (v, s') \<in> fst (get_cnode (cap_object cnode_cap) s); ((), st) \<in> fst (assert (0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap) s'); remaining_size \<noteq> cdl_cnode_size_bits v + cap_guard_size cnode_cap; \<not> remaining_size < cdl_cnode_size_bits v + cap_guard_size cnode_cap\<rbrakk> \<Longrightarrow> (do x <- get_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v)));
gets_the (if is_cnode_cap x then resolve_cap x cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) else oreturnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)))
od) st = (do next_cap <- get_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v)));
if is_cnode_cap next_cap then resolve_address_bits next_cap cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) else returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))
od) st proof (prove)
goal (1 subgoal):
 1. \<And>cnode_cap cap_ptr remaining_size v s s' st rv sta. \<lbrakk>\<And>v s va. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some v; 0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap; \<not> remaining_size \<le> cdl_cnode_size_bits v + cap_guard_size cnode_cap; opt_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) s = Some va; is_cnode_cap va\<rbrakk> \<Longrightarrow> gets_the (resolve_cap va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) = resolve_address_bits va cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)); (cap_ptr >> remaining_size - cap_guard_size cnode_cap) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; (v, s') \<in> fst (get_cnode (cap_object cnode_cap) s); ((), st) \<in> fst (assert (0 < cdl_cnode_size_bits v \<or> 0 < cap_guard_size cnode_cap) s'); remaining_size \<noteq> cdl_cnode_size_bits v + cap_guard_size cnode_cap; \<not> remaining_size < cdl_cnode_size_bits v + cap_guard_size cnode_cap; (rv, sta) \<in> fst (get_cap (cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))) st)\<rbrakk> \<Longrightarrow> gets_the (if is_cnode_cap rv then resolve_cap rv cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) else oreturnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) sta = (if is_cnode_cap rv then resolve_address_bits rv cap_ptr (remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) else returnOk ((cap_object cnode_cap, unat ((cap_ptr >> remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits v))), remaining_size - (cdl_cnode_size_bits v + cap_guard_size cnode_cap))) sta proof (prove)
goal:
No subgoals!