theory CNodeInv_AI

lemma cap_revoke_termination:
  "All (cap_revoke_dom :: (machine_word \<times> bool list) \<times> 'state_ext state \<Rightarrow> bool)" apply (rule cap_revoke.termination) apply (rule wf_cap_revoke_recset) apply (clarsimp simp add: cap_revoke_recset_def in_monad select_def
                  dest!:    iffD1[OF in_get_cap_cte_wp_at] in_select_ext_weak) apply (frule use_validE_R [OF _ cap_delete_rvk_prog]) apply (rule rpo_sym) apply (frule use_validE_R [OF _ cap_delete_deletes]) apply simp apply (simp add: revoke_progress_ord_def) apply (erule disjE) apply (drule_tac f="\<lambda>f. f (aa, ba)" in arg_cong) apply (clarsimp simp: cte_wp_at_caps_of_state cap_to_rpo_def) apply (simp split: cap.split_asm) apply (erule (1) use_valid [OF _ preemption_point_caps_of_state]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. All cap_revoke_dom proof (prove)
goal (2 subgoals):
 1. wf ?R
 2. \<And>slot s 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> ((slot, stg), slot, s) \<in> ?R proof (prove)
goal (1 subgoal):
 1. \<And>slot s 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> ((slot, stg), slot, s) \<in> cap_revoke_recset proof (prove)
goal (1 subgoal):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st\<rbrakk> \<Longrightarrow> revoke_progress_ord (?m16 a b rv st aa ba rvd stf stg) (map_option cap_to_rpo \<circ> caps_of_state st)
 2. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; revoke_progress_ord (?m16 a b rv st aa ba rvd stf stg) (map_option cap_to_rpo \<circ> caps_of_state stf)\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; revoke_progress_ord (map_option cap_to_rpo \<circ> caps_of_state st) (map_option cap_to_rpo \<circ> caps_of_state stf)\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; revoke_progress_ord (map_option cap_to_rpo \<circ> caps_of_state st) (map_option cap_to_rpo \<circ> caps_of_state stf)\<rbrakk> \<Longrightarrow> True
 2. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; revoke_progress_ord (map_option cap_to_rpo \<circ> caps_of_state st) (map_option cap_to_rpo \<circ> caps_of_state stf); cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; revoke_progress_ord (map_option cap_to_rpo \<circ> caps_of_state st) (map_option cap_to_rpo \<circ> caps_of_state stf); cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; map_option cap_to_rpo \<circ> caps_of_state st = map_option cap_to_rpo \<circ> caps_of_state stf \<or> (\<Sum>x\<in>dom (caps_of_state stf). rpo_measure x (map_option cap_to_rpo (caps_of_state stf x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))); cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf; map_option cap_to_rpo \<circ> caps_of_state st = map_option cap_to_rpo \<circ> caps_of_state stf\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))
 2. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf; (\<Sum>x\<in>dom (caps_of_state stf). rpo_measure x (map_option cap_to_rpo (caps_of_state stf x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf; (map_option cap_to_rpo \<circ> caps_of_state st) (aa, ba) = (map_option cap_to_rpo \<circ> caps_of_state stf) (aa, ba)\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))
 2. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf; (\<Sum>x\<in>dom (caps_of_state stf). rpo_measure x (map_option cap_to_rpo (caps_of_state stf x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; caps_of_state st (a, b) = Some rv; caps_of_state st (aa, ba) = Some rvd; caps_of_state stf (aa, ba) = Some NullCap; (case rvd of NullCap \<Rightarrow> (None, 0) | Zombie p zb n \<Rightarrow> (Some (p, replicate (zombie_cte_bits zb) False), 2) | _ \<Rightarrow> (None, 3)) = (None, 0)\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))
 2. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf; (\<Sum>x\<in>dom (caps_of_state stf). rpo_measure x (map_option cap_to_rpo (caps_of_state stf x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv st aa ba rvd stf stg. \<lbrakk>rvd \<noteq> NullCap; (Inr (), stf) \<in> fst (cap_delete (aa, ba) st); (Inr (), stg) \<in> fst (preemption_point stf); (aa, ba) \<in> descendants_of (a, b) (cdt st); rv \<noteq> NullCap; descendants_of (a, b) (cdt st) \<noteq> {}; cte_wp_at ((=) rv) (a, b) st; cte_wp_at ((=) rvd) (aa, ba) st; cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) stf; (\<Sum>x\<in>dom (caps_of_state stf). rpo_measure x (map_option cap_to_rpo (caps_of_state stf x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x)))\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>dom (caps_of_state stg). rpo_measure x (map_option cap_to_rpo (caps_of_state stg x))) < (\<Sum>x\<in>dom (caps_of_state st). rpo_measure x (map_option cap_to_rpo (caps_of_state st x))) proof (prove)
goal:
No subgoals!