kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchADT_IF

lemma do_user_op_pas_refined[ADT_IF_assms, wp]:
  "do_user_op_if f tc \<lbrace>pas_refined aag\<rbrace>" apply (simp add: do_user_op_if_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma do_use_op_guarded_pas_domain[ADT_IF_assms, wp]:
  "do_user_op_if f tc \<lbrace>guarded_pas_domain aag\<rbrace>" by (rule guarded_pas_domain_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>
theory ArchADT_IF

lemma tcb_arch_ref_tcb_context_set[ADT_IF_assms, simp]:
  "tcb_arch_ref (tcb_arch_update (arch_tcb_context_set tc) tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_arch_ref (tcb_arch_update (arch_tcb_context_set tc) tcb) = tcb_arch_ref tcb
theory ArchADT_IF

lemma arch_activate_idle_thread_scheduler_action[ADT_IF_assms, wp]:
  "arch_activate_idle_thread t \<lbrace>\<lambda>s :: det_state. P (scheduler_action s)\<rbrace>" by (wpsimp simp: arch_activate_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> arch_activate_idle_thread t \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
theory ArchADT_IF

lemma arch_perform_invocation_noErr[ADT_IF_assms, wp]:
  "\<lbrace>\<top>\<rbrace> arch_perform_invocation a -, \<lbrace>Q\<rbrace>" by (wpsimp simp: arch_perform_invocation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_perform_invocation a -, \<lbrace>Q\<rbrace>
theory ArchADT_IF

lemma arch_invoke_irq_control_noErr[ADT_IF_assms, wp]:
  "\<lbrace>\<top>\<rbrace> arch_invoke_irq_control a -, \<lbrace>Q\<rbrace>" by (cases a; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_invoke_irq_control a -, \<lbrace>Q\<rbrace>
theory ArchADT_IF

lemma getActiveIRQ_None[ADT_IF_assms]:
  "(None,s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s)  \<Longrightarrow>
   irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = None" apply (erule use_valid) apply (wp dmo_getActiveIRQ_wp) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (None, s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s) \<Longrightarrow> irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = None proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = a\<rbrace>
 2. ?P s proof (prove)
goal (1 subgoal):
 1. irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))
theory ArchADT_IF

lemma getActiveIRQ_Some[ADT_IF_assms]:
  "(Some i, s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s)
   \<Longrightarrow> irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = Some i" apply (erule use_valid) apply (wp dmo_getActiveIRQ_wp) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Some i, s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s) \<Longrightarrow> irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = Some i proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>a b. irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = a\<rbrace>
 2. ?P s proof (prove)
goal (1 subgoal):
 1. irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))
theory ArchADT_IF

lemma idle_equiv_as_globals_equiv:
  "arm_global_pd (arch_state s) \<noteq> idle_thread s
   \<Longrightarrow> idle_equiv st s =
       globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s,
                         kheap:= (kheap st)(arm_global_pd (arch_state s) :=
                                              kheap s (arm_global_pd (arch_state s))),
                                            cur_thread := cur_thread s\<rparr>) s" by (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pd (arch_state s) \<noteq> idle_thread s \<Longrightarrow> idle_equiv st s = globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s))), cur_thread := cur_thread s\<rparr>) s
theory ArchADT_IF

lemma idle_equiv_as_globals_equiv_scheduler:
  "arm_global_pd (arch_state s) \<noteq> idle_thread s
   \<Longrightarrow> idle_equiv st s =
       globals_equiv_scheduler (st\<lparr>arch_state := arch_state s, machine_state := machine_state s,
                                   kheap:= (kheap st)(arm_global_pd (arch_state s) :=
                                                        kheap s (arm_global_pd (arch_state s)))\<rparr>) s" by (clarsimp simp: idle_equiv_def tcb_at_def2 globals_equiv_scheduler_def
                     arch_globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pd (arch_state s) \<noteq> idle_thread s \<Longrightarrow> idle_equiv st s = globals_equiv_scheduler (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s)))\<rparr>) s
theory ArchADT_IF

lemma invs_pd_not_idle_thread[intro]:
  "invs s \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s" by (fastforce simp: invs_def valid_state_def valid_global_objs_def
                      obj_at_def valid_idle_def pred_tcb_at_def empty_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s
theory ArchADT_IF

lemma kernel_entry_if_idle_equiv[ADT_IF_assms]:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st
         and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" apply (rule hoare_pre) apply (rule idle_globals_lift) apply (wp kernel_entry_if_globals_equiv) apply force apply (fastforce intro!: invs_pd_not_idle_thread)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. idle_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. idle_equiv st\<rbrace>
 2. \<And>s. (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?P3\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. ?P3 s \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s
 3. \<And>s. (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> (idle_equiv st and ?P3) s proof (prove)
goal (3 subgoals):
 1. \<And>st s. (globals_equiv st and ?P3) s \<Longrightarrow> (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s
 2. \<And>s. ?P3 s \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s
 3. \<And>s. (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> (idle_equiv st and ?P3) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> (ct_idle s \<longrightarrow> tc = idle_context s) \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s
 2. \<And>s. (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)) s \<Longrightarrow> (idle_equiv st and (\<lambda>s. invs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> (ct_idle s \<longrightarrow> tc = idle_context s))) s proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma do_user_op_if_idle_equiv[ADT_IF_assms, wp]:
  "\<lbrace>idle_equiv st and invs\<rbrace>
   do_user_op_if uop tc
   \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" unfolding do_user_op_if_def by (wpsimp wp: dmo_user_memory_update_idle_equiv dmo_device_memory_update_idle_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>idle_equiv st and invs\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>_. idle_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>idle_equiv st and invs\<rbrace> do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
allow_read <- return {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x};
allow_write <- return {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x};
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
u <- return (uop t pl pr pxn (tc, um |` allow_read, (ds \<circ> ptrFromPAddr) |` allow_read, es));
assert (u \<noteq> {});
(e, tc', um', ds', es') <- select u;
do_machine_op (user_memory_update ((um' |` allow_write \<circ> addrFromPPtr) |` (- dom ds)));
do_machine_op (device_memory_update ((ds' |` allow_write \<circ> addrFromPPtr) |` dom ds));
do_machine_op (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>_. idle_equiv st\<rbrace>
theory ArchADT_IF

lemma kernel_entry_if_valid_pdpt_objs[wp]:
 "\<lbrace>valid_pdpt_objs and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
  kernel_entry_if e tc
  \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" apply (case_tac "e = Interrupt") apply (simp add: kernel_entry_if_def) apply (wp | wpc | simp add: kernel_entry_if_def)+ apply (wpsimp simp: ran_tcb_cap_cases arch_tcb_update_aux2
                    wp: hoare_weak_lift_imp thread_set_invs_trivial)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and invs\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
return (r, tc)
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?P'48 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>rv s. invs s \<and> ct_active s\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?Q41\<rbrace> gets cur_thread \<lbrace>\<lambda>t s. (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> ?P'48 t s\<rbrace>
 3. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and ct_active) s\<rbrakk> \<Longrightarrow> ?Q41 s proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma kernel_entry_if_valid_vspace_objs_if[ADT_IF_assms, wp]:
  "\<lbrace>valid_vspace_objs_if and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. valid_vspace_objs_if\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs_if and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. valid_vspace_objs_if\<rbrace>
theory ArchADT_IF

lemma handle_preemption_if_valid_pdpt_objs[ADT_IF_assms, wp]:
  "\<lbrace>valid_vspace_objs_if\<rbrace> handle_preemption_if a \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>" by (simp add: handle_preemption_if_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs_if\<rbrace> handle_preemption_if a \<lbrace>\<lambda>rv. valid_vspace_objs_if\<rbrace>
theory ArchADT_IF

lemma schedule_if_valid_pdpt_objs[ADT_IF_assms, wp]:
  "\<lbrace>valid_vspace_objs_if\<rbrace> schedule_if a \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>" by (simp add: schedule_if_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs_if\<rbrace> schedule_if a \<lbrace>\<lambda>rv. valid_vspace_objs_if\<rbrace>
theory ArchADT_IF

lemma do_user_op_if_valid_pdpt_objs[ADT_IF_assms, wp]:
  "\<lbrace>valid_vspace_objs_if\<rbrace> do_user_op_if a b \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>" by (simp add: do_user_op_if_def | wp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs_if\<rbrace> do_user_op_if a b \<lbrace>\<lambda>rv. valid_vspace_objs_if\<rbrace>
theory ArchADT_IF

lemma valid_vspace_objs_if_ms_update[ADT_IF_assms, simp]:
  "valid_vspace_objs_if (machine_state_update f s) = valid_vspace_objs_if s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs_if (machine_state_update f s) = valid_vspace_objs_if s
theory ArchADT_IF

lemma do_user_op_if_irq_state_of_state[ADT_IF_assms]:
  "do_user_op_if utf uc \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" apply (rule hoare_pre) apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_user_op_if utf uc \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_user_op_if utf uc \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 2. \<And>s. P (irq_state_of_state s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma do_user_op_if_irq_masks_of_state[ADT_IF_assms]:
  "do_user_op_if utf uc \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>" apply (rule hoare_pre) apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> do_user_op_if utf uc \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_user_op_if utf uc \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>s. P (irq_masks_of_state s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma do_user_op_if_irq_measure_if[ADT_IF_assms]:
  "do_user_op_if utf uc \<lbrace>\<lambda>s. P (irq_measure_if s)\<rbrace>" apply (rule hoare_pre) apply (simp add: do_user_op_if_def user_memory_update_def irq_measure_if_def
         | wps |wp dmo_wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_measure_if s)\<rbrace> do_user_op_if utf uc \<lbrace>\<lambda>_ s. P (irq_measure_if s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_user_op_if utf uc \<lbrace>\<lambda>_ s. P (irq_measure_if s)\<rbrace>
 2. \<And>s. P (irq_measure_if s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Noninterference

lemma sameFor_refl: "refl (sameFor g ab irqab asidab domainab d)" by (auto intro!: refl_onI equiv_for_refl
             simp: sameFor_def sameFor_subject_def sameFor_scheduler_def domain_fields_equiv_def
            split: partition.splits
            intro: states_equiv_for_refl globals_equiv_refl globals_equiv_scheduler_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refl (sameFor g ab irqab asidab domainab d)
theory Noninterference

lemma domain_fields_equiv_sym:
  "domain_fields_equiv s t \<Longrightarrow> domain_fields_equiv t s" by (clarsimp simp: domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_fields_equiv s t \<Longrightarrow> domain_fields_equiv t s
theory Noninterference

lemma sameFor_sym:
  "sym (sameFor g ab irqab asidab domainab d)" by (fastforce intro: symI
                 simp: sameFor_def sameFor_subject_def sameFor_scheduler_def
                split: partition.splits
                intro: states_equiv_for_sym globals_equiv_sym equiv_for_sym domain_fields_equiv_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym (sameFor g ab irqab asidab domainab d)
theory Noninterference

lemma domain_fields_equiv_trans:
  "\<lbrakk> domain_fields_equiv s t; domain_fields_equiv t u \<rbrakk>
     \<Longrightarrow> domain_fields_equiv s u" by (clarsimp simp: domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domain_fields_equiv s t; domain_fields_equiv t u\<rbrakk> \<Longrightarrow> domain_fields_equiv s u
theory Noninterference

lemma sameFor_trans:
  "trans (sameFor g ab irqab asidab domainab d)" apply (rule transI) apply (auto simp: sameFor_def sameFor_subject_def sameFor_scheduler_def
             split: partition.splits
             intro: states_equiv_for_trans globals_equiv_trans
                    equiv_for_trans domain_fields_equiv_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trans (sameFor g ab irqab asidab domainab d) proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> sameFor g ab irqab asidab domainab d; (y, z) \<in> sameFor g ab irqab asidab domainab d\<rbrakk> \<Longrightarrow> (x, z) \<in> sameFor g ab irqab asidab domainab d proof (prove)
goal:
No subgoals!
theory Noninterference

lemma is_label[simp]:
  "x \<noteq> SilcLabel \<Longrightarrow> OrdinaryLabel (label_of x) = x" by (case_tac x, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> SilcLabel \<Longrightarrow> OrdinaryLabel (label_of x) = x
theory Noninterference

lemma pasSubject_not_SilcLabel:
  "silc_inv aag s s' \<Longrightarrow> pasSubject aag \<noteq> SilcLabel" by (auto simp: silc_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv aag s s' \<Longrightarrow> pasSubject aag \<noteq> SilcLabel
theory Noninterference

lemma sameFor_reads_equiv_f_g':
  "\<lbrakk> pas_cur_domain aag s \<or> pas_cur_domain aag s'; silc_inv aag st s;
     (((uc,s),mode),((uc',s'),mode')) \<in> same_for aag (Partition (label_of (pasSubject aag))) \<rbrakk>
     \<Longrightarrow> reads_equiv_f_g aag s s'" apply (frule pasSubject_not_SilcLabel) apply (auto simp: reads_equiv_f_g_def reads_equiv_def2 sameFor_def
                    sameFor_subject_def silc_dom_equiv_def globals_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag s \<or> pas_cur_domain aag s'; silc_inv aag st s; (((uc, s), mode), (uc', s'), mode') \<in> same_for aag (Partition (label_of (pasSubject aag)))\<rbrakk> \<Longrightarrow> reads_equiv_f_g aag s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag s \<or> pas_cur_domain aag s'; silc_inv aag st s; (((uc, s), mode), (uc', s'), mode') \<in> same_for aag (Partition (label_of (pasSubject aag))); pasSubject aag \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> reads_equiv_f_g aag s s' proof (prove)
goal:
No subgoals!
theory Noninterference

lemma sameFor_scheduler_equiv:
  "(s,s') \<in> same_for aag PSched
   \<Longrightarrow> scheduler_equiv aag (internal_state_if s) (internal_state_if s')" by (clarsimp simp: scheduler_equiv_def sameFor_def sameFor_scheduler_def silc_dom_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> same_for aag PSched \<Longrightarrow> scheduler_equiv aag (internal_state_if s) (internal_state_if s')
theory Noninterference

lemma schedule_reads_affects_equiv_sameFor_PSched:
  "\<lbrakk> scheduler_equiv aag s s'; scheduler_modes mode = scheduler_modes mode';
     interrupted_modes mode = interrupted_modes mode' \<rbrakk>
     \<Longrightarrow> (((uc,s),mode),((uc',s'),mode')) \<in> same_for aag PSched" by (simp add: sameFor_def sameFor_scheduler_def scheduler_equiv_def silc_dom_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_modes mode = scheduler_modes mode'; interrupted_modes mode = interrupted_modes mode'\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc', s'), mode') \<in> same_for aag PSched