kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_IF

lemma cap_insert_globals_equiv:
  "\<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace>
   cap_insert new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding cap_insert_def fun_app_def by (wpsimp wp: update_cdt_globals_equiv set_original_globals_equiv
                 set_cap_globals_equiv hoare_drop_imps dxo_wp_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> do src_cap <- get_cap src_slot;
dest_original <- return (is_cap_revocable new_cap src_cap);
old_cap <- get_cap dest_slot;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap new_cap src_slot;
set_cap new_cap dest_slot;
is_original <- gets is_original_cap;
src_parent <- return (should_be_parent_of src_cap (is_original src_slot) new_cap dest_original);
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
update_cdt (\<lambda>cdt. cdt(dest_slot := if src_parent then Some src_slot else cdt src_slot));
do_extended_op (cap_insert_ext src_parent src_slot dest_slot src_p dest_p);
set_original dest_slot dest_original
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory CNode_IF

lemma cap_move_globals_equiv:
  "\<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace>
   cap_move new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding cap_move_def fun_app_def by (wpsimp wp: set_original_globals_equiv set_cdt_globals_equiv set_cap_globals_equiv dxo_wp_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> cap_move new_cap src_slot dest_slot \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> do set_cap new_cap dest_slot;
set_cap NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return (cdt src_slot);
cdt' <- return (cdt(dest_slot := parent, src_slot := None));
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p);
is_original <- gets is_original_cap;
set_original dest_slot (is_original src_slot);
set_original src_slot False
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory CNode_IF

lemma cap_swap_globals_equiv:
  "\<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace>
   cap_swap cap1 slot1 cap2 slot2
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding cap_swap_def by (wpsimp wp: set_original_globals_equiv set_cdt_globals_equiv set_cap_globals_equiv dxo_wp_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> cap_swap cap1 slot1 cap2 slot2 \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> do set_cap cap2 slot1;
set_cap cap1 slot2;
slot1_p <- gets (\<lambda>s. cdt s slot1);
slot2_p <- gets (\<lambda>s. cdt s slot2);
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n);
set_cdt (cdt'(slot1 := cdt' slot2, slot2 := cdt' slot1));
do_extended_op (cap_swap_ext slot1 slot2 slot1_p slot2_p);
is_original <- gets is_original_cap;
set_original slot1 (is_original slot2);
set_original slot2 (is_original slot1)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory CNode_IF

lemma irq_is_recurring_triv:
  assumes a: "\<And>P. \<lbrace>(\<lambda>s. P (irq_masks (machine_state s))) and Q\<rbrace>
                   (f :: ('s state, 'a) nondet_monad)
                   \<lbrace>\<lambda>rv s. P (irq_masks (machine_state s))\<rbrace>"
  shows "\<lbrace>irq_is_recurring irq and Q\<rbrace> f \<lbrace>\<lambda>_. irq_is_recurring irq\<rbrace>" apply (clarsimp simp: irq_is_recurring_def valid_def) apply (rule use_valid[OF _ is_irq_at_triv[OF a]]) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_is_recurring irq and Q\<rbrace> f \<lbrace>\<lambda>_. irq_is_recurring irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b n. \<lbrakk>(a, b) \<in> fst (f s); \<forall>n. \<exists>m. is_irq_at s irq (n + m); Q s\<rbrakk> \<Longrightarrow> \<exists>m. is_irq_at b irq (n + m) proof (prove)
goal (2 subgoals):
 1. \<And>s a b n. \<lbrakk>(a, b) \<in> fst (f s); \<forall>n. \<exists>m. is_irq_at s irq (n + m); Q s\<rbrakk> \<Longrightarrow> (?r13 s a b n, b) \<in> fst (f (?s13 s a b n))
 2. \<And>s a b n. \<lbrakk>(a, b) \<in> fst (f s); \<forall>n. \<exists>m. is_irq_at s irq (n + m); Q s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>m. is_irq_at s irq (n + m)) and Q) (?s13 s a b n) proof (prove)
goal (1 subgoal):
 1. \<And>s a b n. \<lbrakk>(a, b) \<in> fst (f s); \<forall>n. \<exists>m. is_irq_at s irq (n + m); Q s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>m. is_irq_at s irq (n + m)) and Q) s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma domain_sep_inv_to_interrupt_states_pres:
  assumes a: "\<And>st. \<lbrace>domain_sep_inv False (st :: 's state) and P\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv False st\<rbrace>"
  shows "\<lbrace>(\<lambda>s. Q (interrupt_states s)) and P and domain_sep_inv False st\<rbrace>
         f
         \<lbrace>\<lambda>_ s. Q (interrupt_states s)\<rbrace>" apply (clarsimp simp: valid_def) apply (erule use_valid) apply (rule hoare_strengthen_post) apply (rule_tac st3=s in a) apply (fastforce simp: domain_sep_inv_def) apply (simp add: domain_sep_inv_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. Q (interrupt_states s)) and P and domain_sep_inv False st\<rbrace> f \<lbrace>\<lambda>_ s. Q (interrupt_states s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> Q (interrupt_states b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s a b\<rbrace> f \<lbrace>\<lambda>a b. Q (interrupt_states b)\<rbrace>
 2. \<And>s a b. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> ?P11 s a b s proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> \<lbrace>?P11 s a b\<rbrace> f \<lbrace>?Q14 s a b\<rbrace>
 2. \<And>s a b rv sa. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s; ?Q14 s a b rv sa\<rbrakk> \<Longrightarrow> Q (interrupt_states sa)
 3. \<And>s a b. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> ?P11 s a b s proof (prove)
goal (2 subgoals):
 1. \<And>s a b rv sa. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s; domain_sep_inv False s sa\<rbrakk> \<Longrightarrow> Q (interrupt_states sa)
 2. \<And>s a b. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> (domain_sep_inv False s and P) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>Q (interrupt_states s); P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> (domain_sep_inv False s and P) s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma only_timer_irq_inv_pres:
  assumes a:
    "\<And>P. \<lbrace>(\<lambda>s. P (irq_masks (machine_state s))) and Q\<rbrace>
          f
          \<lbrace>\<lambda>rv s. P (irq_masks (machine_state s))\<rbrace>"
  assumes b: "\<And>st :: 's state. \<lbrace>domain_sep_inv False st and P\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv False st\<rbrace>"
  shows "\<lbrace>only_timer_irq_inv irq (st :: 's state) and Q and P\<rbrace> f \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (clarsimp simp: only_timer_irq_inv_def valid_def) apply (rule conjI) apply (erule use_valid[OF _ b], simp) apply (erule use_valid[OF _ only_timer_irq_pres[OF a b]]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st and Q and P\<rbrace> f \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); domain_sep_inv False st s; only_timer_irq irq s; Q s; P s\<rbrakk> \<Longrightarrow> domain_sep_inv False st b \<and> only_timer_irq irq b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); domain_sep_inv False st s; only_timer_irq irq s; Q s; P s\<rbrakk> \<Longrightarrow> domain_sep_inv False st b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); domain_sep_inv False st s; only_timer_irq irq s; Q s; P s\<rbrakk> \<Longrightarrow> only_timer_irq irq b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); domain_sep_inv False st s; only_timer_irq irq s; Q s; P s\<rbrakk> \<Longrightarrow> only_timer_irq irq b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>domain_sep_inv False st s; only_timer_irq irq s; Q s; P s\<rbrakk> \<Longrightarrow> (only_timer_irq irq and Q and P and domain_sep_inv False (?st26 s a b)) s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma only_timer_irq_inv_domain_sep_inv[intro]:
  "only_timer_irq_inv irq st s \<Longrightarrow> domain_sep_inv False st s" by (simp add: only_timer_irq_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_timer_irq_inv irq st s \<Longrightarrow> domain_sep_inv False st s
theory CNode_IF

lemma irq_is_recurring_not_masked:
  "irq_is_recurring irq (s :: det_state) \<Longrightarrow> \<not> irq_masks (machine_state s) irq" apply (clarsimp simp: irq_is_recurring_def) apply (blast dest: is_irq_at_not_masked) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_is_recurring irq s \<Longrightarrow> \<not> irq_masks (machine_state s) irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. \<exists>m. is_irq_at s irq (n + m); irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma dmo_getActiveIRQ_globals_equiv:
  "\<lbrace>globals_equiv st\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (wp dmo_getActiveIRQ_wp) apply (auto simp: globals_equiv_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. irq_state_independent_A (globals_equiv st)
 2. \<And>s. globals_equiv st s \<Longrightarrow> globals_equiv st s proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma gets_irq_masks_equiv_valid:
  "equiv_valid_inv I A (\<lambda>s. \<not> (irq_masks s) irq \<and> (\<forall>x. x \<noteq> irq \<longrightarrow> (irq_masks s) x)) (gets irq_masks)" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. \<not> irq_masks s irq \<and> (\<forall>x. x \<noteq> irq \<longrightarrow> irq_masks s x)) (gets irq_masks)
theory CNode_IF

lemma irq_state_increment_reads_respects_memory:
  "equiv_valid_inv (equiv_machine_state P and equiv_irq_state)
                   (equiv_for (\<lambda>x. aag_can_affect_label aag l \<and>
                                   pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l)
                              underlying_memory)
                   \<top> (modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) apply (fastforce intro: equiv_forI elim: equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P and equiv_irq_state) (equiv_for (aag_can_affect aag l) underlying_memory) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (equiv_machine_state P and equiv_irq_state) (equiv_for (aag_can_affect aag l) underlying_memory) (=) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>(equiv_machine_state P and equiv_irq_state) s t; equiv_for (aag_can_affect aag l) underlying_memory s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> (equiv_machine_state P and equiv_irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) (t\<lparr>irq_state := Suc (irq_state t)\<rparr>) \<and> equiv_for (aag_can_affect aag l) underlying_memory (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) (t\<lparr>irq_state := Suc (irq_state t)\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma irq_state_increment_reads_respects_device:
  "equiv_valid_inv (equiv_machine_state P and equiv_irq_state)
                   (equiv_for (\<lambda>x. aag_can_affect_label aag l \<and>
                                   pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) l)
                              device_state)
                   \<top> (modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) apply (fastforce intro: equiv_forI elim: equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state P and equiv_irq_state) (equiv_for (aag_can_affect aag l) device_state) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (equiv_machine_state P and equiv_irq_state) (equiv_for (aag_can_affect aag l) device_state) (=) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>(equiv_machine_state P and equiv_irq_state) s t; equiv_for (aag_can_affect aag l) device_state s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> (equiv_machine_state P and equiv_irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) (t\<lparr>irq_state := Suc (irq_state t)\<rparr>) \<and> equiv_for (aag_can_affect aag l) device_state (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) (t\<lparr>irq_state := Suc (irq_state t)\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma use_equiv_valid_inv:
  "\<lbrakk> x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st; equiv_valid_inv I P g f \<rbrakk>
     \<Longrightarrow> fst x = fst y \<and> P (snd y) (snd x) \<and> I (snd y) (snd x)" apply (clarsimp simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def) apply (drule spec)+ apply (erule impE) apply fastforce apply (drule(1) bspec | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st; equiv_valid_inv I P g f\<rbrakk> \<Longrightarrow> fst x = fst y \<and> P (snd y) (snd x) \<and> I (snd y) (snd x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st; \<forall>st t. g st \<and> g t \<and> I st t \<and> P st t \<longrightarrow> (\<forall>x\<in>fst (f st). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> P s' t')\<rbrakk> \<Longrightarrow> fst x = fst y \<and> P (snd y) (snd x) \<and> I (snd y) (snd x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st; g ?st15 \<and> g ?t17 \<and> I ?st15 ?t17 \<and> P ?st15 ?t17 \<longrightarrow> (\<forall>x\<in>fst (f ?st15). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f ?t17). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> P s' t')\<rbrakk> \<Longrightarrow> fst x = fst y \<and> P (snd y) (snd x) \<and> I (snd y) (snd x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st\<rbrakk> \<Longrightarrow> g ?st15 \<and> g ?t17 \<and> I ?st15 ?t17 \<and> P ?st15 ?t17
 2. \<lbrakk>x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st; \<forall>x\<in>fst (f ?st15). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f ?t17). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> P s' t'\<rbrakk> \<Longrightarrow> fst x = fst y \<and> P (snd y) (snd x) \<and> I (snd y) (snd x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> fst (f st); y \<in> fst (f s); g s; g st; I s st; P s st; \<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f st). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> P s' t'\<rbrakk> \<Longrightarrow> fst x = fst y \<and> P (snd y) (snd x) \<and> I (snd y) (snd x) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma reset_work_units_reads_respects[wp]:
  "reads_respects aag l \<top> reset_work_units" apply (simp add: reset_work_units_def equiv_valid_def2) apply (rule modify_ev2) apply (force intro: reads_equiv_work_units_completed_update affects_equiv_work_units_completed_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) reset_work_units proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (modify (work_units_completed_update (\<lambda>_. 0))) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (work_units_completed_update (\<lambda>_. 0) s) (work_units_completed_update (\<lambda>_. 0) t) \<and> affects_equiv aag l (work_units_completed_update (\<lambda>_. 0) s) (work_units_completed_update (\<lambda>_. 0) t) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma update_work_units_reads_respects[wp]:
  "reads_respects aag l \<top> update_work_units" apply (simp add: update_work_units_def equiv_valid_def2) apply (rule modify_ev2) apply (force intro: reads_equiv_work_units_completed_update' affects_equiv_work_units_completed_update') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) update_work_units proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (modify (\<lambda>s. work_units_completed_update (\<lambda>_. work_units_completed s + 1) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (work_units_completed_update (\<lambda>_. work_units_completed s + 1) s) (work_units_completed_update (\<lambda>_. work_units_completed t + 1) t) \<and> affects_equiv aag l (work_units_completed_update (\<lambda>_. work_units_completed s + 1) s) (work_units_completed_update (\<lambda>_. work_units_completed t + 1) t) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma work_units_limit_reached_reads_respects[wp]:
  "reads_respects aag l \<top> work_units_limit_reached" apply (simp add: work_units_limit_reached_def, wp) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) work_units_limit_reached proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> work_units_completed s = work_units_completed t proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma preemption_point_def2:
  "(preemption_point :: (unit,det_ext) p_monad) =
   doE liftE update_work_units;
       rv \<leftarrow> liftE work_units_limit_reached;
       if rv then doE liftE reset_work_units;
                      liftE (do_machine_op (getActiveIRQ True)) >>=E
                      case_option (returnOk ()) (K (throwError $ ()))
                  odE
       else returnOk()
   odE" apply (rule ext) apply (simp add: preemption_point_def OR_choiceE_def wrap_ext_bool_det_ext_ext_def
                   ef_mk_ef work_units_limit_reached_def select_f_def empty_fail_cond) apply (clarsimp simp: work_units_limit_reached_def gets_def liftE_def select_f_def get_def
                        lift_def return_def bind_def bindE_def split_def image_def
                 split: option.splits sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. preemption_point = doE liftE update_work_units;
rv <- liftE work_units_limit_reached;
if rv then doE liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (K (throwError $ ()))
odE else returnOk ()
odE proof (prove)
goal (1 subgoal):
 1. \<And>x. preemption_point x = (doE liftE update_work_units;
rv <- liftE work_units_limit_reached;
if rv then doE liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (K (throwError $ ()))
odE else returnOk ()
odE) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (doE y <- liftE update_work_units;
ex <- liftE get;
(rv, uu_) <- liftE (\<lambda>s. (fst ((do work_units <- gets work_units_completed;
return (work_units_limit \<le> work_units)
od) ex) \<times> {s}, snd (gets work_units_completed ex)));
if rv then doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>x2. throwError ())
odE else returnOk ()
odE) x = (doE y <- liftE update_work_units;
rv <- liftE (do work_units <- gets work_units_completed;
return (work_units_limit \<le> work_units)
od);
if rv then doE liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (K (throwError $ ()))
odE else returnOk ()
odE) x proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma cca_can_read:
  "\<lbrakk> valid_mdb s; valid_objs s; cdt_change_allowed' aag slot s; pas_refined aag s \<rbrakk>
     \<Longrightarrow> aag_can_read aag (fst slot)" apply (frule(3) cdt_change_allowed_delete_derived) by (rule read_delder_thread_read_thread_rev[OF reads_lrefl])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; cdt_change_allowed' aag slot s; pas_refined aag s\<rbrakk> \<Longrightarrow> aag_can_read aag (fst slot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; cdt_change_allowed' aag slot s; pas_refined aag s; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag (fst slot)
theory CNode_IF

lemma all_children_subjectReads:
  "pas_refined aag s \<Longrightarrow> all_children (aag_can_read aag \<circ> fst) (cdt s)" apply (rule all_childrenI) apply simp apply (erule read_delder_thread_read_thread_rev) by (rule aag_cdt_link_DeleteDerived)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> all_children (aag_can_read aag \<circ> fst) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>pas_refined aag s; cdt s c = Some p; (aag_can_read aag \<circ> fst) p\<rbrakk> \<Longrightarrow> (aag_can_read aag \<circ> fst) c proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>pas_refined aag s; cdt s c = Some p; aag_can_read aag (fst p)\<rbrakk> \<Longrightarrow> aag_can_read aag (fst c) proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>pas_refined aag s; cdt s c = Some p\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), DeleteDerived, pasObjectAbs aag (fst c)) \<in> pasPolicy aag