theory ADT_IF

lemma cap_revoke_irq_state_inv'':
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
  shows
    "s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace>
         cap_revoke slot
         \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" proof(induct rule: cap_revoke.induct[where ?a1.0=s]) case (1 slot s) show ?case apply (subst cap_revoke.simps) apply (rule hoare_spec_gen_asm) apply (rule hoare_pre_spec_validE) apply (wp "1.hyps") apply (wp spec_valid_conj_liftE2 | simp)+ apply (wp drop_spec_validE[OF preemption_point_irq_state_inv[simplified validE_R_def]]
                      drop_spec_validE[OF preemption_point_irq_state_inv'[where irq=irq]]
                      drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]]
                      cap_delete_domain_sep_inv cap_delete_irq_state_inv
                      drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp]
                      drop_spec_validE[OF liftE_wp] drop_spec_validE[OF hoare_vcg_conj_liftE1]
                   | simp | wp (once) hoare_drop_imps)+ apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>slot s. (\<And>rv stb rva staa rvb stba rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, staa) \<in> fst ((without_preemption $ gets cdt) stb); (Inr rvb, stba) \<in> fst ((returnOk $ descendants_of slot rva) staa); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> 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> ?stg \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal (1 subgoal):
 1. \<And>slot s. (\<And>rv stb rva staa rvb stba rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, stb) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, staa) \<in> fst ((without_preemption $ gets cdt) stb); (Inr rvb, stba) \<in> fst ((returnOk $ descendants_of slot rva) staa); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) stba); (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>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<lbrakk>irq_is_recurring irq st; (irq_state_inv st and domain_sep_inv False sta) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s''f. \<lbrakk>irq_is_recurring irq st; (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>?B18 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf\<rbrace> preemption_point \<lbrace>\<lambda>rvg. irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>irq_is_recurring irq st; (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>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> cap_delete rvc \<lbrace>?B18 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>irq_is_recurring irq st; (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>?B15 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (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>?B14 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B15 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (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>?P13 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B14 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (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>?B7 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P13 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> irq_state_inv st b)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B6 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B7 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 8. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> without_preemption $ get_cap slot \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 9. \<lbrakk>irq_is_recurring irq st; (irq_state_inv st and domain_sep_inv False sta) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e s''f. \<lbrakk>irq_is_recurring irq st; (rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d); (Inr (), s''f) \<in> fst (cap_delete rvc s''e)\<rbrakk> \<Longrightarrow> s''f \<turnstile> \<lbrace>?P'26 rv s'' rva s''a rvb s''b rvc s''c rvd s''d () s''e ()\<rbrace> preemption_point \<lbrace>\<lambda>rv. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>irq_is_recurring irq st; (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>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> cap_delete rvc \<lbrace>\<lambda>a b. domain_sep_inv False sta b \<and> ?P'26 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e a b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>irq_is_recurring irq st; (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>?B15 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>irq_is_recurring irq st; (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>?B14 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B15 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>irq_is_recurring irq st; (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>?P13 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B14 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>irq_is_recurring irq st; (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>?B7 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P13 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> irq_state_inv st b)\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. \<And>rv s''. \<lbrakk>irq_is_recurring irq st; (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s)\<rbrakk> \<Longrightarrow> s'' \<turnstile> \<lbrace>?B6 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B7 rv s''\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 8. irq_is_recurring irq st \<Longrightarrow> s \<turnstile> \<lbrace>?P'2\<rbrace> without_preemption $ get_cap slot \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 9. \<lbrakk>irq_is_recurring irq st; (irq_state_inv st and domain_sep_inv False sta) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_is_recurring irq st; irq_state_inv st s \<and> domain_sep_inv False sta s\<rbrakk> \<Longrightarrow> next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> domain_sep_inv False (?sta248 (cdt s) (descendants_of slot (cdt s)) (next_revoke_cap slot s) ()) s \<and> irq_is_recurring (?irq247 (cdt s) (descendants_of slot (cdt s)) (next_revoke_cap slot s) ()) st \<and> domain_sep_inv False (?sta246 (cdt s) (descendants_of slot (cdt s)) (next_revoke_cap slot s) ()) s \<and> irq_is_recurring (?irq245 (cdt s) (descendants_of slot (cdt s)) (next_revoke_cap slot s) ()) st proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>

goal:
No subgoals!