kings-crown/FVELER_Isabelle huggingface dataset:
theory InfoFlow_IF

lemma set_object_rev:
  "reads_equiv_valid_inv A aag (\<lambda> s. kheap s ptr = Some obj \<and> is_subject aag ptr) (set_object ptr obj)" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def set_object_def bind_def
                      get_def gets_def put_def return_def assert_def get_object_def
                dest: update_object_noop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. kheap s ptr = Some obj \<and> is_subject aag ptr) (set_object ptr obj)
theory InfoFlow_IF

lemma lookup_error_on_failure_rev:
  "reads_equiv_valid_inv A aag P m \<Longrightarrow>
   reads_equiv_valid_inv A aag P (lookup_error_on_failure s m)" unfolding lookup_error_on_failure_def handleE'_def by (wp | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag P m \<Longrightarrow> reads_equiv_valid_inv A aag P (lookup_error_on_failure s m) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag P m \<Longrightarrow> reads_equiv_valid_inv A aag P (do v <- m;
case v of Inl e \<Rightarrow> (throwError \<circ> FailedLookup s) e | Inr v' \<Rightarrow> return (Inr v')
od)
theory InfoFlow_IF

lemma internal_exst[simp]:
  "cdt_list_internal o exst = cdt_list"
  "ekheap_internal o exst = ekheap" by (simp_all add: o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_list_internal \<circ> exst = cdt_list &&& ekheap_internal \<circ> exst = ekheap
theory InfoFlow_IF

lemma gets_kheap_revrv':
  "reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag) id) \<top> (gets kheap)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist elim: reads_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag) id) (\<lambda>_. True) (gets kheap) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag) id) ?P (gets kheap)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> equiv_for (aag_can_read aag) id (kheap s) (kheap t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_cdt_revrv':
  "reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) \<top> (gets cdt)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist elim: reads_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) (\<lambda>_. True) (gets cdt) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) ?P (gets cdt)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> equiv_for (aag_can_read aag \<circ> fst) id (cdt s) (cdt t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_cdt_list_revrv':
  "reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) \<top> (gets cdt_list)" apply(rule equiv_valid_rv_guard_imp) apply(rule gets_evrv) apply(fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist elim: reads_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) (\<lambda>_. True) (gets cdt_list) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) ?P (gets cdt_list)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> equiv_for (aag_can_read aag \<circ> fst) id (cdt_list s) (cdt_list t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_is_original_cap_revrv':
  "reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) \<top> (gets is_original_cap)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist elim: reads_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) (\<lambda>_. True) (gets is_original_cap) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read aag \<circ> fst) id) ?P (gets is_original_cap)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> equiv_for (aag_can_read aag \<circ> fst) id (is_original_cap s) (is_original_cap t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_ready_queues_revrv':
  "reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read_domain aag) id) \<top> (gets ready_queues)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) 
  (* NB: only force works here *)
   apply (force simp: equiv_for_comp equiv_for_def disjoint_iff_not_equal elim: reads_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read_domain aag) id) (\<lambda>_. True) (gets ready_queues) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv A aag (equiv_for (aag_can_read_domain aag) id) ?P (gets ready_queues)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> equiv_for (aag_can_read_domain aag) id (ready_queues s) (ready_queues t)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> equiv_for (aag_can_read_domain aag) id (ready_queues s) (ready_queues t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_cur_thread_ev:
  "reads_equiv_valid_inv A aag \<top> (gets cur_thread)" apply (rule equiv_valid_guard_imp) apply wp apply (simp add: reads_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (gets cur_thread) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_inv A aag ?Q (gets cur_thread)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> cur_thread s = cur_thread t proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_kheap_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
                            (equiv_for (aag_can_read aag or aag_can_affect aag l) id) \<top> (gets kheap)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist
                   elim: reads_equivE affects_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for (aag_can_read aag or aag_can_affect aag l) id) (\<lambda>_. True) (gets kheap) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for (aag_can_read aag or aag_can_affect aag l) id) ?P (gets kheap)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (aag_can_read aag or aag_can_affect aag l) id (kheap s) (kheap t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_machine_state_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
     (equiv_machine_state (aag_can_read aag or aag_can_affect aag l) and equiv_irq_state)
     \<top> (gets machine_state)" by (fastforce simp: equiv_valid_2_def gets_def get_def return_def bind_def
                elim: reads_equivE affects_equivE equiv_forE
               intro: equiv_forI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_machine_state (aag_can_read aag or aag_can_affect aag l) and equiv_irq_state) (\<lambda>_. True) (gets machine_state)
theory InfoFlow_IF

lemma gets_machine_state_revrv':
  "reads_equiv_valid_rv_inv A aag (equiv_machine_state (aag_can_read aag) and equiv_irq_state)
                            \<top> (gets machine_state)" by (fastforce simp: equiv_valid_2_def gets_def get_def return_def bind_def
                elim: reads_equivE affects_equivE equiv_forE
               intro: equiv_forI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (equiv_machine_state (aag_can_read aag) and equiv_irq_state) (\<lambda>_. True) (gets machine_state)
theory InfoFlow_IF

lemma gets_cdt_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
                            (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id)
                            \<top> (gets cdt)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist
                   elim: reads_equivE affects_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (\<lambda>_. True) (gets cdt) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) ?P (gets cdt)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id (cdt s) (cdt t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_cdt_list_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
                            (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id)
                            \<top> (gets cdt_list)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist
                   elim: reads_equivE affects_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (\<lambda>_. True) (gets cdt_list) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) ?P (gets cdt_list)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id (cdt_list s) (cdt_list t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_ekheap_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
                            (equiv_for (aag_can_read aag or aag_can_affect aag l) id) \<top> (gets ekheap)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist
                   elim: reads_equivE affects_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for (aag_can_read aag or aag_can_affect aag l) id) (\<lambda>_. True) (gets ekheap) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for (aag_can_read aag or aag_can_affect aag l) id) ?P (gets ekheap)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (aag_can_read aag or aag_can_affect aag l) id (ekheap s) (ekheap t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_is_original_cap_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
                            (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id)
                            \<top> (gets is_original_cap)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) apply (fastforce simp: equiv_for_comp[symmetric] equiv_for_or or_comp_dist
                  elim: reads_equivE affects_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (\<lambda>_. True) (gets is_original_cap) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) ?P (gets is_original_cap)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id (is_original_cap s) (is_original_cap t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma gets_ready_queues_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag
                            (equiv_for (aag_can_read_domain aag or aag_can_affect_domain aag l) id)
                            \<top> (gets ready_queues)" apply (rule equiv_valid_rv_guard_imp) apply (rule gets_evrv) 
  (* NB: only clarsimp works here *)
   apply (clarsimp simp: equiv_for_def disjoint_iff_not_equal elim!: reads_equivE affects_equivE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for (aag_can_read_domain aag or aag_can_affect_domain aag l) id) (\<lambda>_. True) (gets ready_queues) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (equiv_for (aag_can_read_domain aag or aag_can_affect_domain aag l) id) ?P (gets ready_queues)
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (aag_can_read_domain aag or aag_can_affect_domain aag l) id (ready_queues s) (ready_queues t)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (aag_can_read_domain aag or aag_can_affect_domain aag l) id (ready_queues s) (ready_queues t)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma as_user_reads_respects:
  "reads_respects aag l (K (det f \<and> is_subject aag thread)) (as_user thread f)" apply (simp add: as_user_def split_def) apply (rule gen_asm_ev) apply (wp set_object_reads_respects select_f_ev gets_the_ev) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (det f \<and> is_subject aag thread)) (as_user thread f) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. det f \<and> is_subject aag thread) (do tcb <- gets_the (get_tcb thread);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. det f \<and> is_subject aag thread \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb thread);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det f \<and> is_subject aag thread; True\<rbrakk> \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb thread s = get_tcb thread t) s \<and> K (det f) s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). True \<and> True)) proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma get_message_info_rev:
  "reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_message_info ptr)" by (wpsimp wp: as_user_rev getRegister_inv simp: get_message_info_def det_getRegister)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_message_info ptr)
theory InfoFlow_IF

lemma syscall_rev:
  assumes reads_res_m_fault:
    "reads_equiv_valid_inv A aag P m_fault"
  assumes reads_res_m_error:
    "\<And>v. reads_equiv_valid_inv A aag (Q (Inr v)) (m_error v)"
  assumes reads_res_h_fault:
    "\<And>v. reads_equiv_valid_inv A aag (Q (Inl v)) (h_fault v)"
  assumes reads_res_m_finalise:
    "\<And>v. reads_equiv_valid_inv A aag (R (Inr v)) (m_finalise v)"
  assumes reads_res_h_error:
    "\<And>v. reads_equiv_valid_inv A aag (R (Inl v)) (h_error v)"
  assumes m_fault_hoare:
    "\<lbrace>P\<rbrace> m_fault \<lbrace>Q\<rbrace>"
  assumes m_error_hoare:
    "\<And>v. \<lbrace>Q (Inr v)\<rbrace> m_error v \<lbrace>R\<rbrace>"
  shows "reads_equiv_valid_inv A aag P (Syscall_A.syscall m_fault h_fault m_error h_error m_finalise)" unfolding Syscall_A.syscall_def without_preemption_def fun_app_def by (wp assms equiv_valid_guard_imp[OF liftE_bindE_ev]
      | rule hoare_strengthen_post[OF m_error_hoare]
      | rule hoare_strengthen_post[OF m_fault_hoare]
      | wpc
      | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag P (syscall m_fault h_fault m_error h_error m_finalise) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag P (doE r_fault <- liftE m_fault;
case r_fault of Inl f \<Rightarrow> liftE (h_fault f) | Inr a \<Rightarrow> doE r_error <- liftE (m_error a);
case r_error of Inl e \<Rightarrow> liftE (h_error e) | Inr b \<Rightarrow> m_finalise b
odE
odE)
theory InfoFlow_IF

lemma syscall_reads_respects_g:
  assumes reads_res_m_fault:
    "reads_respects_g aag l P m_fault"
  assumes reads_res_m_error:
    "\<And>v. reads_respects_g aag l (Q'' v) (m_error v)"
  assumes reads_res_h_fault:
    "\<And>v. reads_respects_g aag l (Q' v) (h_fault v)"
  assumes reads_res_m_finalise:
    "\<And>v. reads_respects_g aag l (R'' v) (m_finalise v)"
  assumes reads_res_h_error:
    "\<And>v. reads_respects_g aag l (R' v) (h_error v)"
  assumes m_fault_hoare:
    "\<lbrace>P\<rbrace> m_fault \<lbrace>case_sum Q' Q''\<rbrace>"
  assumes m_error_hoare:
    "\<And>v. \<lbrace>Q'' v\<rbrace> m_error v \<lbrace>case_sum R' R''\<rbrace>"
  shows "reads_respects_g aag l P (Syscall_A.syscall m_fault h_fault m_error h_error m_finalise)" unfolding Syscall_A.syscall_def without_preemption_def fun_app_def by (wp assms equiv_valid_guard_imp[OF liftE_bindE_ev]
      | rule hoare_strengthen_post[OF m_error_hoare]
      | rule hoare_strengthen_post[OF m_fault_hoare]
      | wpc
      | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l P (syscall m_fault h_fault m_error h_error m_finalise) proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l P (doE r_fault <- liftE m_fault;
case r_fault of Inl f \<Rightarrow> liftE (h_fault f) | Inr a \<Rightarrow> doE r_error <- liftE (m_error a);
case r_error of Inl e \<Rightarrow> liftE (h_error e) | Inr b \<Rightarrow> m_finalise b
odE
odE)
theory InfoFlow_IF

lemma spec_equiv_valid_hoist_guard:
  "((P st) \<Longrightarrow> spec_equiv_valid_inv st I A \<top> f) \<Longrightarrow> spec_equiv_valid_inv st I A P f" by (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P st \<Longrightarrow> spec_equiv_valid_inv st I A (\<lambda>_. True) f) \<Longrightarrow> spec_equiv_valid_inv st I A P f
theory InfoFlow_IF

lemma for_each_byte_of_word_imp:
  "\<lbrakk> \<And>x. P x \<Longrightarrow> Q x; for_each_byte_of_word P p \<rbrakk>
     \<Longrightarrow> for_each_byte_of_word Q p" by (fastforce simp: for_each_byte_of_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. P x \<Longrightarrow> Q x; for_each_byte_of_word P p\<rbrakk> \<Longrightarrow> for_each_byte_of_word Q p
theory InfoFlow_IF

lemma modifies_at_mostD:
  "\<lbrakk> modifies_at_most aag L P f; P s; (rv,s') \<in> fst(f s) \<rbrakk>
     \<Longrightarrow> equiv_but_for_labels aag L s s'" by (auto simp: modifies_at_most_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modifies_at_most aag L P f; P s; (rv, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L s s'
theory InfoFlow_IF

lemma invs_kernel_mappings:
  "invs s \<Longrightarrow> valid_kernel_mappings s" by (auto simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_kernel_mappings s
theory InfoFlow_IF

lemma load_word_offs_rev:
  "for_each_byte_of_word (aag_can_read aag) (a + of_nat x * of_nat word_size)
   \<Longrightarrow> reads_equiv_valid_inv A aag \<top> (load_word_offs a x)" unfolding load_word_offs_def fun_app_def by (fastforce intro: equiv_valid_guard_imp[OF dmo_loadWord_rev])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. for_each_byte_of_word (aag_can_read aag) (a + word_of_nat x * word_of_nat word_size) \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (load_word_offs a x) proof (prove)
goal (1 subgoal):
 1. for_each_byte_of_word (aag_can_read aag) (a + word_of_nat x * word_of_nat word_size) \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (do_machine_op (loadWord (a + word_of_nat (x * word_size))))
theory InfoFlow_IF

lemma modifies_at_mostI:
  assumes hoare: "\<And>st. \<lbrace>P and equiv_but_for_labels aag L st\<rbrace> f \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
  shows "modifies_at_most aag L P f" apply (clarsimp simp: modifies_at_most_def) apply (erule use_valid) apply (rule hoare) apply (fastforce simp: equiv_but_for_labels_def states_equiv_for_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modifies_at_most aag L P f proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L s b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. P s \<Longrightarrow> \<lbrace>?P9 s a b\<rbrace> f \<lbrace>\<lambda>a. equiv_but_for_labels aag L s\<rbrace>
 2. \<And>s a b. P s \<Longrightarrow> ?P9 s a b s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. P s \<Longrightarrow> (P and equiv_but_for_labels aag L s) s proof (prove)
goal:
No subgoals!
theory ArchInfoFlow_IF

lemma asid_pool_at_kheap:
  "asid_pool_at ptr s = (\<exists>asid_pool. kheap s ptr = Some (ArchObj (ASIDPool asid_pool)))" by (simp add: atyp_at_eq_kheap_obj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch AASIDPool) ptr s = (\<exists>asid_pool. kheap s ptr = Some (ArchObj (ASIDPool asid_pool)))
theory ArchInfoFlow_IF

lemma equiv_asid:
  "equiv_asid asid s s' = equiv_asid' asid (arm_asid_table (arch_state s) (asid_high_bits_of asid))
                                           (arm_asid_table (arch_state s') (asid_high_bits_of asid))
                                           (kheap s) (kheap s')" by (auto simp: equiv_asid_def equiv_asid'_def asid_pool_at_kheap split: option.splits )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asid asid s s' = equiv_asid' asid (asid_table s (asid_high_bits_of asid)) (asid_table s' (asid_high_bits_of asid)) (kheap s) (kheap s')