theory UserOp_IF

lemma dmo_device_state_update_reads_respects_g:
  "reads_respects_g aag l (\<lambda>s. dom um \<subseteq> device_region s) (do_machine_op (device_memory_update um))" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) apply (clarsimp simp: do_machine_op_def device_memory_update_def
                        gets_def get_def select_f_def bind_def in_monad) apply (clarsimp simp: reads_equiv_g_def globals_equiv_def split: option.splits) apply (subgoal_tac "reads_respects aag l \<top> (do_machine_op (device_memory_update um))") apply (fastforce simp: equiv_valid_def2 equiv_valid_2_def in_monad do_machine_op_def
                          device_memory_update_def select_f_def idle_equiv_def) apply (rule use_spec_ev) apply (simp add: device_memory_update_def) apply (rule do_machine_op_spec_reads_respects) apply (simp add: equiv_valid_def2) apply (rule modify_ev2) apply (fastforce intro: map_add_eq equiv_forI elim: equiv_forE split: option.splits) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. dom um \<subseteq> dom (device_state (machine_state s))) (do_machine_op (device_memory_update um)) proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst (do_machine_op (device_memory_update um) s); ((), ba) \<in> fst (do_machine_op (device_memory_update um) t); dom um \<subseteq> dom (device_state (machine_state s)); dom um \<subseteq> dom (device_state (machine_state t)); reads_equiv_g aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv_g aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state s)); dom um \<subseteq> dom (device_state (machine_state t)); reads_equiv_g aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv_g aag (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) \<and> idle_equiv (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t)); reads_respects aag l (\<lambda>_. True) (do_machine_op (device_memory_update um))\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) \<and> idle_equiv (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um\<rparr>\<rparr>) (t\<lparr>machine_state := machine_state t\<lparr>device_state := device_state (machine_state t) ++ um\<rparr>\<rparr>)
 2. \<And>s t. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (device_memory_update um)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do_machine_op (device_memory_update um)) proof (prove)
goal (1 subgoal):
 1. \<And>s t st. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (device_memory_update um)) proof (prove)
goal (1 subgoal):
 1. \<And>s t st. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s t st. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) (modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>))
 2. \<And>s t st P. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>))
 2. \<And>s t st P. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t sa ta. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t)); equiv_machine_state (aag_can_read aag) sa ta; equiv_machine_state (aag_can_affect aag l) sa ta; True; True\<rbrakk> \<Longrightarrow> () = () \<and> equiv_machine_state (aag_can_read aag) (sa\<lparr>device_state := device_state sa ++ um\<rparr>) (ta\<lparr>device_state := device_state ta ++ um\<rparr>) \<and> equiv_machine_state (aag_can_affect aag l) (sa\<lparr>device_state := device_state sa ++ um\<rparr>) (ta\<lparr>device_state := device_state ta ++ um\<rparr>)
 2. \<And>s t st P. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s t st P. \<lbrakk>dom um \<subseteq> dom (device_state (machine_state t)); affects_equiv aag l s t; reads_equiv aag s t; arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t); idle_equiv s t; cur_thread s = cur_thread t; dom (device_state (machine_state s)) = dom (device_state (machine_state t))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal:
No subgoals!