kings-crown/FVELER_Isabelle huggingface dataset:
theory InfoFlow_IF

lemma states_equiv_for_identical_kheap_updates:
  "\<lbrakk> states_equiv_for P Q R S s s'; identical_kheap_updates s s' kh kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" by (auto simp: states_equiv_for_def identical_kheap_updates_def
          elim!: equiv_forE equiv_asids_identical_kheap_updates
         intro!: equiv_forI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; identical_kheap_updates s s' kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)
theory InfoFlow_IF

lemma states_equiv_forE:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "equiv_machine_state P (machine_state s) (machine_state s')"
          "equiv_for P kheap s s'"
          "equiv_for (P \<circ> fst) cdt s s'"
          "equiv_for (P \<circ> fst) cdt_list s s'"
          "equiv_for P ekheap s s'"
          "equiv_for (P \<circ> fst) is_original_cap s s'"
          "equiv_for Q interrupt_states s s'"
          "equiv_for Q interrupt_irq_node s s'"
          "equiv_asids R s s'"
          "equiv_for S ready_queues s s'" using sef[simplified states_equiv_for_def] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>equiv_machine_state P (machine_state s) (machine_state s'); equiv_for P kheap s s'; equiv_for (P \<circ> fst) cdt s s'; equiv_for (P \<circ> fst) cdt_list s s'; equiv_for P ekheap s s'; equiv_for (P \<circ> fst) is_original_cap s s'; equiv_for Q interrupt_states s s'; equiv_for Q interrupt_irq_node s s'; equiv_asids R s s'; equiv_for S ready_queues s s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
equiv_for P kheap s s' \<and> equiv_machine_state P (machine_state s) (machine_state s') \<and> equiv_for (P \<circ> fst) cdt s s' \<and> equiv_for P ekheap s s' \<and> equiv_for (P \<circ> fst) cdt_list s s' \<and> equiv_for (P \<circ> fst) is_original_cap s s' \<and> equiv_for Q interrupt_states s s' \<and> equiv_for Q interrupt_irq_node s s' \<and> equiv_for S ready_queues s s' \<and> equiv_asids R s s'

goal (1 subgoal):
 1. (\<lbrakk>equiv_machine_state P (machine_state s) (machine_state s'); equiv_for P kheap s s'; equiv_for (P \<circ> fst) cdt s s'; equiv_for (P \<circ> fst) cdt_list s s'; equiv_for P ekheap s s'; equiv_for (P \<circ> fst) is_original_cap s s'; equiv_for Q interrupt_states s s'; equiv_for Q interrupt_irq_node s s'; equiv_asids R s s'; equiv_for S ready_queues s s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma equiv_for_apply: "equiv_for P g (f s) (f s') = equiv_for P (g o f) s s'" by (simp add: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for P g (f s) (f s') = equiv_for P (g \<circ> f) s s'
theory InfoFlow_IF

lemma states_equiv_forE_kheap:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. P x \<Longrightarrow> kheap s x = kheap s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> kheap s x = kheap s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> kheap s x = kheap s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_forE_mem:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. P x \<Longrightarrow>
    (underlying_memory (machine_state s)) x = (underlying_memory (machine_state s')) x \<and>
    (device_state (machine_state s)) x = (device_state (machine_state s')) x" using sef apply (clarsimp simp: states_equiv_for_def elim: equiv_forE) apply (elim equiv_forE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<and> device_state (machine_state s) x = device_state (machine_state s') x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<and> device_state (machine_state s) x = device_state (machine_state s') x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<And>x. P x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<and> device_state (machine_state s) x = device_state (machine_state s') x) \<Longrightarrow> thesis; equiv_for P kheap s s'; equiv_for P underlying_memory (machine_state s) (machine_state s'); equiv_for P device_state (machine_state s) (machine_state s'); equiv_for (P \<circ> fst) cdt s s'; equiv_for P ekheap s s'; equiv_for (P \<circ> fst) cdt_list s s'; equiv_for (P \<circ> fst) is_original_cap s s'; equiv_for Q interrupt_states s s'; equiv_for Q interrupt_irq_node s s'; equiv_for S ready_queues s s'; equiv_asids R s s'\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<And>x. P x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<and> device_state (machine_state s) x = device_state (machine_state s') x) \<Longrightarrow> thesis; equiv_asids R s s'; \<And>x. P x \<Longrightarrow> kheap s x = kheap s' x; \<And>x. P x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x; \<And>x. P x \<Longrightarrow> device_state (machine_state s) x = device_state (machine_state s') x; \<And>x. (P \<circ> fst) x \<Longrightarrow> cdt s x = cdt s' x; \<And>x. P x \<Longrightarrow> ekheap s x = ekheap s' x; \<And>x. (P \<circ> fst) x \<Longrightarrow> cdt_list s x = cdt_list s' x; \<And>x. (P \<circ> fst) x \<Longrightarrow> is_original_cap s x = is_original_cap s' x; \<And>x. Q x \<Longrightarrow> interrupt_states s x = interrupt_states s' x; \<And>x. Q x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x; \<And>x. S x \<Longrightarrow> ready_queues s x = ready_queues s' x\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma states_equiv_forE_cdt:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. P (fst x) \<Longrightarrow> cdt s x = cdt s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. P (fst x) \<Longrightarrow> cdt s x = cdt s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. P (fst x) \<Longrightarrow> cdt s x = cdt s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_forE_cdt_list:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. P (fst x) \<Longrightarrow> cdt_list s x = cdt_list s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. P (fst x) \<Longrightarrow> cdt_list s x = cdt_list s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. P (fst x) \<Longrightarrow> cdt_list s x = cdt_list s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_forE_ekheap:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. P x \<Longrightarrow> ekheap s x = ekheap s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> ekheap s x = ekheap s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> ekheap s x = ekheap s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_forE_interrupt_states:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. Q x \<Longrightarrow> interrupt_states s x = interrupt_states s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. Q x \<Longrightarrow> interrupt_states s x = interrupt_states s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. Q x \<Longrightarrow> interrupt_states s x = interrupt_states s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_forE_interrupt_irq_node:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. Q x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. Q x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. Q x \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_forE_ready_queues:
  assumes sef: "states_equiv_for P Q R S s s'"
  obtains "\<And>x. S x \<Longrightarrow> ready_queues s x = ready_queues s' x" using sef by (auto simp: states_equiv_for_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. S x \<Longrightarrow> ready_queues s x = ready_queues s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
states_equiv_for P Q R S s s'

goal (1 subgoal):
 1. ((\<And>x. S x \<Longrightarrow> ready_queues s x = ready_queues s' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma equiv_for_refl:
  "equiv_for P f s s" by (auto simp: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for P f s s
theory InfoFlow_IF

lemma equiv_for_trans:
  "\<lbrakk> equiv_for P f s t; equiv_for P f t u \<rbrakk> \<Longrightarrow> equiv_for P f s u" by (auto simp: equiv_for_def)

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

lemma states_equiv_for_trans:
  "\<lbrakk> states_equiv_for P Q R S s t; states_equiv_for P Q R S t u \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S s u" by (auto simp: states_equiv_for_def
          intro: equiv_for_trans equiv_asids_trans equiv_forI
           elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s t; states_equiv_for P Q R S t u\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S s u
theory InfoFlow_IF

lemma or_comp_dist:
  "(A or B) \<circ> f = (A \<circ> f or B \<circ> f)" by (simp add: pred_disj_def comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A or B) \<circ> f = (A \<circ> f or B \<circ> f)
theory InfoFlow_IF

lemma idle_equiv_refl:
  "idle_equiv s s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv s s
theory InfoFlow_IF

lemma idle_equiv_sym:
  "idle_equiv s s' \<Longrightarrow> idle_equiv s' s" by (clarsimp simp add: idle_equiv_def)

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

lemma idle_equiv_trans:
  "\<lbrakk> idle_equiv s s'; idle_equiv s' s'' \<rbrakk> \<Longrightarrow> idle_equiv s s''" by (clarsimp simp add: idle_equiv_def tcb_at_def get_tcb_def split: option.splits
                  kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_equiv s s'; idle_equiv s' s''\<rbrakk> \<Longrightarrow> idle_equiv s s''
theory InfoFlow_IF

lemma equiv_asids_aag_can_read_asid:
  "equiv_asids (aag_can_read_asid aag) s s' =
   (\<forall>d \<in> subjectReads (pasPolicy aag) (pasSubject aag). equiv_asids (\<lambda>x. d = pasASIDAbs aag x) s s')" by (auto simp: equiv_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asids (aag_can_read_asid aag) s s' = (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_asids (\<lambda>x. d = pasASIDAbs aag x) s s')
theory InfoFlow_IF

lemma reads_equiv_def2:
  "reads_equiv aag s s' = (states_equiv_for (aag_can_read aag) (aag_can_read_irq aag)
                                            (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and>
                           cur_thread s = cur_thread s' \<and>
                           cur_domain s = cur_domain s' \<and>
                           scheduler_action s = scheduler_action s' \<and>
                           work_units_completed s = work_units_completed s' \<and>
                           irq_state (machine_state s) = irq_state (machine_state s'))" by (auto simp: reads_equiv_def equiv_for_def states_equiv_for_def equiv_asids_aag_can_read_asid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s s' = (states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s'))
theory InfoFlow_IF

lemma reads_equivE:
  assumes sef: "reads_equiv aag s s'"
  obtains "equiv_for (aag_can_read aag) kheap s s'"
          "equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s')"
          "equiv_for ((aag_can_read aag) \<circ> fst) cdt s s'"
          "equiv_for ((aag_can_read aag) \<circ> fst) cdt_list s s'"
          "equiv_for (aag_can_read aag) ekheap s s'"
          "equiv_for ((aag_can_read aag) \<circ> fst) is_original_cap s s'"
          "equiv_for (aag_can_read_irq aag) interrupt_states s s'"
          "equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'"
          "equiv_asids (aag_can_read_asid aag) s s'"
          "equiv_for (aag_can_read_domain aag) ready_queues s s'"
          "cur_thread s = cur_thread s'"
          "cur_domain s = cur_domain s'"
          "scheduler_action s = scheduler_action s'"
          "work_units_completed s = work_units_completed s'"
          "irq_state (machine_state s) = irq_state (machine_state s')" using sef by (auto simp: reads_equiv_def2 elim: states_equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>equiv_for (aag_can_read aag) kheap s s'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
reads_equiv aag s s'

goal (1 subgoal):
 1. (\<lbrakk>equiv_for (aag_can_read aag) kheap s s'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma states_equiv_for_non_asid_pool_kheap_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for P id kh kh';
     non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_non_asid_pool_kheap_update
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for P id kh kh'; non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_non_asid_pool_kheap_update:
  "\<lbrakk> reads_equiv aag s s'; equiv_for (aag_can_read aag) id kh kh';
     non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh' \<rbrakk>
     \<Longrightarrow> reads_equiv aag (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_non_asid_pool_kheap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read aag) id kh kh'; non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_identical_kheap_updates:
  "\<lbrakk> reads_equiv aag s s'; identical_kheap_updates s s' kh kh' \<rbrakk>
     \<Longrightarrow> reads_equiv aag (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_identical_kheap_updates)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; identical_kheap_updates s s' kh kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_cdt_update:
  "\<lbrakk> reads_equiv aag s s'; equiv_for ((aag_can_read aag) \<circ> fst) id kh kh' \<rbrakk>
     \<Longrightarrow> reads_equiv aag (s\<lparr>cdt := kh\<rparr>) (s'\<lparr>cdt := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_cdt_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read aag \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>cdt := kh\<rparr>) (s'\<lparr>cdt := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_cdt_list_update:
  "\<lbrakk> reads_equiv aag s s'; equiv_for ((aag_can_read aag) \<circ> fst) id (kh (cdt_list s)) (kh' (cdt_list s')) \<rbrakk>
     \<Longrightarrow> reads_equiv aag (cdt_list_update kh s) (cdt_list_update kh' s')" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_cdt_list_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read aag \<circ> fst) id (kh (cdt_list s)) (kh' (cdt_list s'))\<rbrakk> \<Longrightarrow> reads_equiv aag (cdt_list_update kh s) (cdt_list_update kh' s')
theory InfoFlow_IF

lemma reads_equiv_identical_ekheap_updates:
  "\<lbrakk> reads_equiv aag s s'; identical_ekheap_updates s s' (kh (ekheap s)) (kh' (ekheap s')) \<rbrakk>
     \<Longrightarrow> reads_equiv aag (ekheap_update kh s) (ekheap_update kh' s')" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_identical_ekheap_updates)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; identical_ekheap_updates s s' (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow> reads_equiv aag (ekheap_update kh s) (ekheap_update kh' s')
theory InfoFlow_IF

lemma reads_equiv_ekheap_updates:
  "\<lbrakk> reads_equiv aag s s'; equiv_for (aag_can_read aag) id (kh (ekheap s)) (kh' (ekheap s')) \<rbrakk>
     \<Longrightarrow> reads_equiv aag (ekheap_update kh s) (ekheap_update kh' s')" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_ekheap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read aag) id (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow> reads_equiv aag (ekheap_update kh s) (ekheap_update kh' s')
theory InfoFlow_IF

lemma reads_equiv_is_original_cap_update:
  "\<lbrakk>reads_equiv aag s s'; equiv_for ((aag_can_read aag) \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow>
   reads_equiv aag (s\<lparr>is_original_cap := kh\<rparr>) (s'\<lparr>is_original_cap := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_is_original_cap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read aag \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>is_original_cap := kh\<rparr>) (s'\<lparr>is_original_cap := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_interrupt_states_update:
  "\<lbrakk> reads_equiv aag s s'; equiv_for (aag_can_read_irq aag) id kh kh' \<rbrakk>
     \<Longrightarrow> reads_equiv aag (s\<lparr>interrupt_states := kh\<rparr>) (s'\<lparr>interrupt_states := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_interrupt_states_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read_irq aag) id kh kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>interrupt_states := kh\<rparr>) (s'\<lparr>interrupt_states := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_interrupt_irq_node_update:
  "\<lbrakk> reads_equiv aag s s'; equiv_for (aag_can_read_irq aag) id kh kh' \<rbrakk>
     \<Longrightarrow> reads_equiv aag (s\<lparr>interrupt_irq_node := kh\<rparr>) (s'\<lparr>interrupt_irq_node := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_interrupt_irq_node_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read_irq aag) id kh kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>interrupt_irq_node := kh\<rparr>) (s'\<lparr>interrupt_irq_node := kh'\<rparr>)
theory InfoFlow_IF

lemma reads_equiv_ready_queues_update:
  "\<lbrakk> reads_equiv aag s s'; equiv_for (aag_can_read_domain aag) id kh kh' \<rbrakk>
     \<Longrightarrow> reads_equiv aag (s\<lparr>ready_queues := kh\<rparr>) (s'\<lparr>ready_queues := kh'\<rparr>)" by (fastforce simp: reads_equiv_def2 intro: states_equiv_for_ready_queues_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; equiv_for (aag_can_read_domain aag) id kh kh'\<rbrakk> \<Longrightarrow> reads_equiv aag (ready_queues_update (\<lambda>_. kh) s) (ready_queues_update (\<lambda>_. kh') s')
theory InfoFlow_IF

lemma reads_equiv_scheduler_action_update:
  "reads_equiv aag s s' \<Longrightarrow>
   reads_equiv aag (s\<lparr>scheduler_action := kh\<rparr>) (s'\<lparr>scheduler_action := kh\<rparr>)" by (fastforce simp: reads_equiv_def2 states_equiv_for_def equiv_for_def elim!: equiv_asids_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s s' \<Longrightarrow> reads_equiv aag (scheduler_action_update (\<lambda>_. kh) s) (scheduler_action_update (\<lambda>_. kh) s')