theory CNodeInv_AI

lemma cap_revoke_preservation_desc_of':
  fixes P Q and s :: "'state_ext state"
  assumes x: "\<And>p. \<lbrace>P and Q p\<rbrace> cap_delete p \<lbrace>\<lambda>rv. P\<rbrace>"
  and     y: "\<And>sl s. P s \<Longrightarrow> \<forall>sl' \<in> descendants_of sl (cdt s). Q sl' s"
  assumes p: "\<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>rv. P\<rbrace>"
  shows      "s \<turnstile> \<lbrace>P\<rbrace> cap_revoke ptr \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>" proof (induct rule: cap_revoke_induct) case (1 slot) show ?case apply (subst cap_revoke_simps) apply (wp "1.hyps") apply (wp x p hoare_drop_imps)+ apply (simp_all add: y) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> cap_revoke ptr \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>slot s. \<lbrakk>cap_revoke_dom (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> stg \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (state)
this:
cap_revoke_dom (slot, s_)
\<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> ?stg \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>

goal (1 subgoal):
 1. \<And>slot s. \<lbrakk>cap_revoke_dom (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> stg \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. s_ \<turnstile> \<lbrace>P\<rbrace> 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 \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s''f. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c); (Inr rve, s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d); (Inr rvf, s''f) \<in> fst (cap_delete rvc s''e)\<rbrakk> \<Longrightarrow> s''f \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf\<rbrace> preemption_point \<lbrace>\<lambda>rvg. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c); (Inr rve, s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B10 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> cap_delete rvc \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B9 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B10 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B8 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B9 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P7 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B8 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B1 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P7 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> P b)\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s_) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B1 rv s''\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 8. s_ \<turnstile> \<lbrace>P\<rbrace> without_preemption $ get_cap slot \<lbrace>?B\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (\<forall>x\<in>descendants_of slot (cdt s). (P and Q x) s \<and> (P and Q x) s \<and> (P and Q x) s) \<and> P s proof (prove)
goal:
No subgoals! proof (state)
this:
s_ \<turnstile> \<lbrace>P\<rbrace> cap_revoke slot \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>

goal:
No subgoals!