theory IRQMasks_IF

lemma cap_revoke_irq_masks':
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
  shows "s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>
             cap_revoke slot
             \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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_pre_spec_validE) apply (wp "1.hyps") apply (wp spec_valid_conj_liftE2 | simp)+ apply (wp drop_spec_validE[OF valid_validE[OF preemption_point_irq_masks]]
                      drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]]
                      cap_delete_domain_sep_inv cap_delete_irq_masks
                      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>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>slot s. (\<And>rv sta rva staa rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, staa) \<in> fst ((without_preemption $ gets cdt) sta); (Inr rvb, stb) \<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) 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>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>

goal (1 subgoal):
 1. \<And>slot s. (\<And>rv sta rva staa rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, staa) \<in> fst ((without_preemption $ gets cdt) sta); (Inr rvb, stb) \<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) 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>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False 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>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 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>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s \<Longrightarrow> ?P' 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>(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>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf\<rbrace> preemption_point \<lbrace>\<lambda>rvg. (\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> cap_delete rvc \<lbrace>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> P (irq_masks_of_state b))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 9. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s \<Longrightarrow> ?P' 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>(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'24 rv s'' rva s''a rvb s''b rvc s''c rvd s''d () s''e ()\<rbrace> preemption_point \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B14 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 st b \<and> ?P'24 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e a b\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<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>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> P (irq_masks_of_state b))\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 9. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<Longrightarrow> next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> domain_sep_inv False (?st166 (cdt s) (descendants_of slot (cdt s)) (next_revoke_cap slot s) ()) s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace> cap_revoke slot \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>

goal:
No subgoals!