theory EmptyFail

lemma empty_fail_getCTE [intro!, wp, simp]:
  "empty_fail (getCTE slot)" apply (simp add: getCTE_def getObject_def split_def) apply (intro empty_fail_bind, simp_all) apply (simp add: loadObject_cte typeError_def alignCheck_def alignError_def
                   magnitudeCheck_def
            split: Structures_H.kernel_object.split) apply (auto split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getCTE slot) proof (prove)
goal (1 subgoal):
 1. empty_fail (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 (fromPPtr slot) map));
loadObject (fromPPtr slot) (fst p) (snd (lookupAround2 (fromPPtr slot) map)) (snd p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. empty_fail (loadObject (fromPPtr slot) (fst xa) (snd (lookupAround2 (fromPPtr slot) x)) (snd xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<forall>x6. (fromPPtr slot - fst xa = tcbIPCBufferSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCallerSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbReply x6)
od)))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCaller x6)
od))))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbReply x6)
od)))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbIPCBufferSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbIPCBufferFrame x6)
od)))))) \<and> (fromPPtr slot - fst xa \<noteq> tcbIPCBufferSlot << objBits undefined \<longrightarrow> (fromPPtr slot - fst xa = tcbCallerSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbReply x6)
od)))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCallerSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCaller x6)
od))))) \<and> (fromPPtr slot - fst xa \<noteq> tcbCallerSlot << objBits undefined \<longrightarrow> (fromPPtr slot - fst xa = tcbReplySlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (tcbReplySlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbReply x6)
od)))) \<and> (fromPPtr slot - fst xa \<noteq> tcbReplySlot << objBits undefined \<longrightarrow> (fromPPtr slot - fst xa = tcbCTableSlot << objBits undefined \<longrightarrow> (tcbCTableSlot << objBits undefined = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbCTable x6)
od))) \<and> (fromPPtr slot - fst xa \<noteq> tcbCTableSlot << objBits undefined \<longrightarrow> (fromPPtr slot - fst xa = tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
return (tcbVTable x6)
od)) \<and> (fromPPtr slot - fst xa \<noteq> tcbVTableSlot << objBits undefined \<longrightarrow> snd xa = KOTCB x6 \<longrightarrow> empty_fail (do y <- unless (fst xa && mask (objBits x6) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fst xa < 1 << objBits x6) fail;
fail
od))))))) \<and> (\<forall>x7. snd xa = KOCTE x7 \<longrightarrow> empty_fail (do y <- unless (fromPPtr slot = fst xa) fail;
y <- unless (fromPPtr slot && mask (objBits x7) = 0) fail;
y <- case snd (lookupAround2 (fromPPtr slot) x) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - fromPPtr slot < 1 << objBits x7) fail;
return x7
od)) proof (prove)
goal:
No subgoals!