kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma finaliseSlot_invs:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_to' slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (rule validE_valid, rule hoare_post_impErr) apply (rule finaliseSlot_invs'') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>?Q2\<rbrace>, \<lbrace>?E2\<rbrace>
 2. \<And>rv s. ?Q2 rv s \<Longrightarrow> invs' s
 3. \<And>e s. ?E2 e s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<Longrightarrow> invs' s
 2. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma finaliseSlot_sch_act_simple:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_to' slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (rule validE_valid, rule hoare_post_impErr) apply (rule finaliseSlot_invs'') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>?Q2\<rbrace>, \<lbrace>?E2\<rbrace>
 2. \<And>rv s. ?Q2 rv s \<Longrightarrow> sch_act_simple s
 3. \<And>e s. ?E2 e s \<Longrightarrow> sch_act_simple s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<Longrightarrow> sch_act_simple s
 2. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> sch_act_simple s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma finaliseSlot_removeable:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_to' slot s)\<rbrace>
     finaliseSlot slot e
   \<lbrace>\<lambda>rv s. fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s\<rbrace>,-" apply (rule validE_validE_R, rule hoare_post_impErr) apply (rule finaliseSlot_invs'') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv s. fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>?Q2\<rbrace>, \<lbrace>?E2\<rbrace>
 2. \<And>rv s. ?Q2 rv s \<Longrightarrow> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s
 3. \<And>e s. ?E2 e s \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<Longrightarrow> fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s
 2. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma finaliseSlot_irqs:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_to' slot s)\<rbrace>
     finaliseSlot slot e
   \<lbrace>\<lambda>rv s. \<forall>sl'. snd rv \<noteq> NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)\<rbrace>,-" apply (rule validE_validE_R, rule hoare_post_impErr) apply (rule finaliseSlot_invs'') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>rv s. \<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> e \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)\<rbrace> finaliseSlot slot e \<lbrace>?Q2\<rbrace>, \<lbrace>?E2\<rbrace>
 2. \<And>rv s. ?Q2 rv s \<Longrightarrow> \<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)
 3. \<And>e s. ?E2 e s \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' slot s (cteCap cte)) slot s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<Longrightarrow> \<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> slot \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)
 2. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma reduceZombie_invs:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_to' slot s)
           \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace>
     reduceZombie cap slot exposed
   \<lbrace>\<lambda>rv s. invs' s\<rbrace>" apply (rule validE_valid) apply (rule hoare_post_impErr, rule hoare_pre, rule reduceZombie_invs'[where p=slot]) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace> reduceZombie cap slot exposed \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace> reduceZombie cap slot exposed \<lbrace>\<lambda>rv. invs'\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s s'' rv sa. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) s); invs' sa \<and> sch_act_simple sa \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) rv sa\<rbrakk> \<Longrightarrow> invs' sa \<and> sch_act_simple sa \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) rv sa)
 2. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<Longrightarrow> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P9 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P9 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s)
 3. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P9 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P9 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) \<Longrightarrow> invs' s
 4. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma reduceZombie_sch_act_simple:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_to' slot s)
           \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace>
     reduceZombie cap slot exposed
   \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" apply (rule validE_valid, rule hoare_pre,
         rule hoare_post_impErr) apply (rule reduceZombie_invs'[where p=slot]) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace> reduceZombie cap slot exposed \<lbrace>\<lambda>rv. sch_act_simple\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q2\<rbrace> reduceZombie cap slot exposed \<lbrace>?Q5\<rbrace>, \<lbrace>?E5\<rbrace>
 2. \<And>rv s. ?Q5 rv s \<Longrightarrow> sch_act_simple s
 3. \<And>e s. ?E5 e s \<Longrightarrow> sch_act_simple s
 4. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s s'' rv sa. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) s); invs' sa \<and> sch_act_simple sa \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) rv sa\<rbrakk> \<Longrightarrow> invs' sa \<and> sch_act_simple sa \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) rv sa)
 2. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P9 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P9 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) \<Longrightarrow> sch_act_simple s
 3. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> sch_act_simple s
 4. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<Longrightarrow> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P9 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P9 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma cteDelete_typ_at' [wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> cteDelete slot exposed \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>" by (wp cteDelete_preservation | simp | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> cteDelete slot exposed \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>
theory CNodeInv_R

lemma use_spec_corres':
  assumes x: "\<And>s. Q s \<Longrightarrow> spec_corres s r P P' f f'"
  shows      "corres r (P and Q) P' f f'" apply (clarsimp simp: corres_underlying_def) apply (frule x) apply (clarsimp simp: spec_corres_def corres_underlying_def) apply (erule(1) my_BallE, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (P and Q) P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q a; P' b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd (f' b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q a; P' b; spec_corres a r P P' f f'\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd (f' b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q a; P' b; \<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> a = s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd (f' s')\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd (f' b) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma drop_spec_corres:
  "corres r P P' f f' \<Longrightarrow> spec_corres s r P P' f f'" unfolding spec_corres_def apply (erule corres_guard_imp) apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P P' f f' \<Longrightarrow> spec_corres s r P P' f f' proof (prove)
goal (1 subgoal):
 1. corres r P P' f f' \<Longrightarrow> corres r (P and (=) s) P' f f' proof (prove)
goal (2 subgoals):
 1. \<And>sa. (P and (=) s) sa \<Longrightarrow> P sa
 2. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma spec_corres_guard_imp:
  assumes x: "spec_corres s r Q Q' f f'"
  assumes y: "P s \<Longrightarrow> Q s" "\<And>s'. P' s' \<Longrightarrow> Q' s'"
  shows      "spec_corres s r P P' f f'" unfolding spec_corres_def apply (rule corres_guard_imp) apply (rule x[unfolded spec_corres_def]) apply (clarsimp elim!: y) apply (erule y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r P P' f f' proof (prove)
goal (1 subgoal):
 1. corres r (P and (=) s) P' f f' proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' f f'
 2. \<And>sa. (P and (=) s) sa \<Longrightarrow> ?Q sa
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>sa. (P and (=) s) sa \<Longrightarrow> (Q and (=) s) sa
 2. \<And>s. P' s \<Longrightarrow> Q' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P' s \<Longrightarrow> Q' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma spec_corres_returns[simp]:
  "spec_corres s r  P P' (return x) (return y) = (\<forall>s'. (P s \<and> P' s' \<and> (s, s') \<in> state_relation) \<longrightarrow> r x y)"
  "spec_corres s r' P P' (returnOk x) (returnOk y) = (\<forall>s'. (P s \<and> P' s' \<and> (s, s') \<in> state_relation) \<longrightarrow> r' (Inr x) (Inr y))" by (simp add: spec_corres_def returnOk_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r P P' (return x) (return y) = (\<forall>s'. P s \<and> P' s' \<and> (s, s') \<in> state_relation \<longrightarrow> r x y) &&& spec_corres s r' P P' (returnOk x) (returnOk y) = (\<forall>s'. P s \<and> P' s' \<and> (s, s') \<in> state_relation \<longrightarrow> r' (Inr x) (Inr y))
theory CNodeInv_R

lemma cte_map_replicate:
  "cte_map (ptr, replicate bits False) = ptr" by (simp add: cte_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map (ptr, replicate bits False) = ptr
theory CNodeInv_R

lemma spec_corres_req:
  "\<lbrakk> \<And>s'. \<lbrakk> P s; P' s'; (s, s') \<in> state_relation \<rbrakk> \<Longrightarrow> F;
     F \<Longrightarrow> spec_corres s r P P' f f' \<rbrakk>
     \<Longrightarrow> spec_corres s r P P' f f'" unfolding spec_corres_def apply (rule corres_assume_pre, erule meta_mp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. \<lbrakk>P s; P' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> F; F \<Longrightarrow> spec_corres s r P P' f f'\<rbrakk> \<Longrightarrow> spec_corres s r P P' f f' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. \<lbrakk>P s; P' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> F; F \<Longrightarrow> corres r (P and (=) s) P' f f'\<rbrakk> \<Longrightarrow> corres r (P and (=) s) P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>sa s'. \<lbrakk>\<And>s'. \<lbrakk>P s; P' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> F; (P and (=) s) sa; P' s'; (sa, s') \<in> state_relation\<rbrakk> \<Longrightarrow> F proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma rec_del_concrete_empty:
  "red_zombie_will_fail cap \<Longrightarrow> rec_del_concrete (ReduceZombieCall cap slot ex) = {}" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. red_zombie_will_fail cap \<Longrightarrow> rec_del_concrete (ReduceZombieCall cap slot ex) = {}
theory CNodeInv_R

lemma spec_corres_add_asm:
  "spec_corres s r P Q f g \<Longrightarrow> spec_corres s r (P and F) Q f g" unfolding spec_corres_def apply (erule corres_guard_imp) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r P Q f g \<Longrightarrow> spec_corres s r (P and F) Q f g proof (prove)
goal (1 subgoal):
 1. corres r (P and (=) s) Q f g \<Longrightarrow> corres r (P and F and (=) s) Q f g proof (prove)
goal (2 subgoals):
 1. \<And>sa. (P and F and (=) s) sa \<Longrightarrow> (P and (=) s) sa
 2. \<And>s. Q s \<Longrightarrow> Q s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma spec_corres_gen_asm2:
  "(F \<Longrightarrow> spec_corres s r Q P' f g) \<Longrightarrow> spec_corres s r Q (P' and (\<lambda>s. F)) f g" unfolding spec_corres_def by (auto intro: corres_gen_asm2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> spec_corres s r Q P' f g) \<Longrightarrow> spec_corres s r Q (P' and (\<lambda>s. F)) f g proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> corres r (Q and (=) s) P' f g) \<Longrightarrow> corres r (Q and (=) s) (P' and (\<lambda>s. F)) f g
theory CNodeInv_R

lemma spec_corres_if:
  "\<lbrakk> G = G'; G \<Longrightarrow> spec_corres s r P P' a c; \<not> G \<Longrightarrow> spec_corres s r Q Q' b d\<rbrakk>
    \<Longrightarrow> spec_corres s r (\<lambda>x. (G \<longrightarrow> P x) \<and> (\<not> G \<longrightarrow> Q x)) (\<lambda>x. (G' \<longrightarrow> P' x) \<and> (\<not> G' \<longrightarrow> Q' x))
        (if G then a else b) (if G' then c else d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G = G'; G \<Longrightarrow> spec_corres s r P P' a c; \<not> G \<Longrightarrow> spec_corres s r Q Q' b d\<rbrakk> \<Longrightarrow> spec_corres s r (\<lambda>x. (G \<longrightarrow> P x) \<and> (\<not> G \<longrightarrow> Q x)) (\<lambda>x. (G' \<longrightarrow> P' x) \<and> (\<not> G' \<longrightarrow> Q' x)) (if G then a else b) (if G' then c else d)
theory CNodeInv_R

lemma spec_corres_liftME2:
  "spec_corres s (f \<oplus> r) P P' m (liftME fn m')
      = spec_corres s (f \<oplus> (\<lambda>x. r x \<circ> fn)) P P' m m'" by (simp add: spec_corres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s (f \<oplus> r) P P' m (liftME fn m') = spec_corres s (f \<oplus> (\<lambda>x. r x \<circ> fn)) P P' m m'
theory CNodeInv_R

lemma rec_del_ReduceZombie_emptyable:
  "\<lbrace>invs
      and (cte_wp_at ((=) cap) slot and is_final_cap' cap
      and (\<lambda>y. is_zombie cap)) and
         (\<lambda>s. \<not> ex \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and
         emptyable slot and
         (\<lambda>s. \<not> cap_removeable cap slot \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s))\<rbrace>
   rec_del (ReduceZombieCall cap slot ex) \<lbrace>\<lambda>rv. emptyable slot\<rbrace>, -" by (rule rec_del_emptyable [where args="ReduceZombieCall cap slot ex", simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (cte_wp_at ((=) cap) slot and is_final_cap' cap and (\<lambda>y. is_zombie cap)) and (\<lambda>s. \<not> ex \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and emptyable slot and (\<lambda>s. \<not> cap_removeable cap slot \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s))\<rbrace> rec_del (ReduceZombieCall cap slot ex) \<lbrace>\<lambda>rv. emptyable slot\<rbrace>, -
theory CNodeInv_R

lemma finaliseSlot_typ_at'[wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> finaliseSlot ptr exposed \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>" by (rule finaliseSlot_preservation, (wp | simp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> finaliseSlot ptr exposed \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>
theory CNodeInv_R

lemma wf_cteRevoke_recset:
  "wf cteRevoke_recset" by (simp add: cteRevoke_recset_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf cteRevoke_recset
theory CNodeInv_R

lemma cteRevoke_typ_at':
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" by (wp cteRevoke_preservation | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
theory CNodeInv_R

lemma cteRevoke_invs':
  "\<lbrace>invs' and sch_act_simple\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (rule_tac Q="\<lambda>rv. invs' and sch_act_simple" in hoare_strengthen_post) apply (wpsimp wp: cteRevoke_preservation cteDelete_invs' cteDelete_sch_act_simple)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs' and sch_act_simple\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv. invs' and sch_act_simple\<rbrace>
 2. \<And>rv s. (invs' and sch_act_simple) s \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!