theory EmptyFail_AI

lemma cap_revoke_spec_empty_fail:
  fixes slot and s :: "'state_ext state"
  shows "spec_empty_fail (cap_revoke slot) s" proof (induct rule: cap_revoke.induct) case (1 slot) show ?case apply (subst cap_revoke.simps) apply (rule spec_empty_fail_bindE', ((wp drop_spec_empty_fail | simp)+)[1])+ apply (simp add: whenE_def | intro conjI impI)+ apply (rule spec_empty_fail_bindE',
               ((wp drop_spec_empty_fail select_ext_empty_fail | simp)+)[1])+ apply (rule "1.hyps", simp+) apply (wp drop_spec_empty_fail)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (cap_revoke slot) s proof (state)
goal (1 subgoal):
 1. \<And>slot s. (\<And>rv st rva sta rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, sta) \<in> fst ((without_preemption $ gets cdt) st); (Inr rvb, stb) \<in> fst ((returnOk $ descendants_of slot rva) sta); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) stb); (Inr rvd, std) \<in> fst ((without_preemption $ get_cap rvc) stc); (Inr rve, ste) \<in> fst (assertE (rvd \<noteq> NullCap) std); (Inr rvf, stf) \<in> fst (cap_delete rvc ste); (Inr rvg, stg) \<in> fst (preemption_point stf)\<rbrakk> \<Longrightarrow> spec_empty_fail (cap_revoke slot) stg) \<Longrightarrow> spec_empty_fail (cap_revoke slot) s proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s_); (Inr ?rva, ?sta) \<in> fst ((without_preemption $ gets cdt) ?st); (Inr ?rvb, ?stb) \<in> fst ((returnOk $ descendants_of slot ?rva) ?sta); ?rv \<noteq> NullCap \<and> ?rvb \<noteq> {}; (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) ?rvb) ?stb); (Inr ?rvd, ?std) \<in> fst ((without_preemption $ get_cap ?rvc) ?stc); (Inr ?rve, ?ste) \<in> fst (assertE (?rvd \<noteq> NullCap) ?std); (Inr ?rvf, ?stf) \<in> fst (cap_delete ?rvc ?ste); (Inr ?rvg, ?stg) \<in> fst (preemption_point ?stf)\<rbrakk> \<Longrightarrow> spec_empty_fail (cap_revoke slot) ?stg

goal (1 subgoal):
 1. \<And>slot s. (\<And>rv st rva sta rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, st) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, sta) \<in> fst ((without_preemption $ gets cdt) st); (Inr rvb, stb) \<in> fst ((returnOk $ descendants_of slot rva) sta); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) stb); (Inr rvd, std) \<in> fst ((without_preemption $ get_cap rvc) stc); (Inr rve, ste) \<in> fst (assertE (rvd \<noteq> NullCap) std); (Inr rvf, stf) \<in> fst (cap_delete rvc ste); (Inr rvg, stg) \<in> fst (preemption_point stf)\<rbrakk> \<Longrightarrow> spec_empty_fail (cap_revoke slot) stg) \<Longrightarrow> spec_empty_fail (cap_revoke slot) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (cap_revoke slot) s_ proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (doE cap <- without_preemption $ get_cap slot;
cdt <- without_preemption $ gets cdt;
descendants <- returnOk $ descendants_of slot cdt;
whenE (cap \<noteq> NullCap \<and> descendants \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) descendants;
cap <- without_preemption $ get_cap child;
assertE (cap \<noteq> NullCap);
cap_delete child;
preemption_point;
cap_revoke slot
odE)
odE) s_ proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(Inr x, s') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr xa, s'a) \<in> fst ((without_preemption $ gets cdt) s'); (Inr xb, s'b) \<in> fst ((returnOk $ descendants_of slot xa) s'a)\<rbrakk> \<Longrightarrow> spec_empty_fail (whenE (x \<noteq> NullCap \<and> xb \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) xb;
cap <- without_preemption $ get_cap child;
assertE (cap \<noteq> NullCap);
cap_delete child;
preemption_point;
cap_revoke slot
odE)) s'b proof (prove)
goal (3 subgoals):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); x \<noteq> NullCap \<and> xb \<noteq> {}\<rbrakk> \<Longrightarrow> spec_empty_fail (doE child <- liftE (select_ext (next_revoke_cap slot) xb);
cap <- liftE (get_cap child);
y <- assertE (cap \<noteq> NullCap);
y <- cap_delete child;
y <- preemption_point;
cap_revoke slot
odE) s'b
 2. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); x = NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk ()) s'b
 3. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); xb = {}\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk ()) s'b proof (prove)
goal (3 subgoals):
 1. \<And>x s' xa s'a xb s'b xc s'c xd s'd xe s'e xf s'f xg s'g. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); x \<noteq> NullCap \<and> xb \<noteq> {}; (Inr xc, s'c) \<in> fst (liftE (select_ext (next_revoke_cap slot) xb) s'b); (Inr xd, s'd) \<in> fst (liftE (get_cap xc) s'c); (Inr xe, s'e) \<in> fst (assertE (xd \<noteq> NullCap) s'd); (Inr xf, s'f) \<in> fst (cap_delete xc s'e); (Inr xg, s'g) \<in> fst (preemption_point s'f)\<rbrakk> \<Longrightarrow> spec_empty_fail (cap_revoke slot) s'g
 2. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); x = NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk ()) s'b
 3. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); xb = {}\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk ()) s'b proof (prove)
goal (2 subgoals):
 1. \<And>x s' xa s'a xb s'b. \<lbrakk>(NullCap, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); x = NullCap\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk ()) s'b
 2. \<And>x s' xa s'a xb s'b. \<lbrakk>(x, s') \<in> fst (get_cap slot s_); (xa, s'a) \<in> fst (gets cdt s'); (Inr xb, s'b) \<in> fst (returnOk (descendants_of slot xa) s'a); xb = {}\<rbrakk> \<Longrightarrow> spec_empty_fail (returnOk ()) s'b proof (prove)
goal:
No subgoals! proof (state)
this:
spec_empty_fail (cap_revoke slot) s_

goal:
No subgoals!