theory Finalise_DR

lemma get_ipc_buffer_words_irq_state_independent[intro!, simp]:
  "get_ipc_buffer_words (s\<lparr>irq_state := f (irq_state s)\<rparr>)
   = get_ipc_buffer_words s" apply (rule ext, rule ext) apply (simp add: get_ipc_buffer_words_def) apply (case_tac "tcb_ipcframe x", simp_all) apply (clarsimp split: ARM_A.arch_cap.splits) apply (rule arg_cong[where f=the]) apply (rule evalMonad_mapM_cong) apply (simp add: evalMonad_def) apply safe apply ((clarsimp simp: loadWord_def bind_def gets_def get_def return_def in_monad)+)[3] apply (rule loadWord_inv) apply (rule df_loadWord) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words (s\<lparr>irq_state := f (irq_state s)\<rparr>) = get_ipc_buffer_words s proof (prove)
goal (1 subgoal):
 1. \<And>x xa. get_ipc_buffer_words (s\<lparr>irq_state := f (irq_state s)\<rparr>) x xa = get_ipc_buffer_words s x xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. the (evalMonad (case tcb_ipcframe x of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer x && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) xa) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) (s\<lparr>irq_state := f (irq_state s)\<rparr>)) = the (evalMonad (case tcb_ipcframe x of ArchObjectCap (PageCap dev buf rights sz mapdata) \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer x && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) xa) else return [] | ArchObjectCap _ \<Rightarrow> return [] | _ \<Rightarrow> return []) s) proof (prove)
goal (1 subgoal):
 1. \<And>x xa x12. tcb_ipcframe x = ArchObjectCap x12 \<Longrightarrow> the (evalMonad (case x12 of PageCap dev buf rights sz mapdata \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer x && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) xa) else return [] | _ \<Rightarrow> return []) (s\<lparr>irq_state := f (irq_state s)\<rparr>)) = the (evalMonad (case x12 of PageCap dev buf rights sz mapdata \<Rightarrow> if AllowRead \<in> rights then mapM loadWord (map (\<lambda>n. buf + (tcb_ipc_buffer x && mask (pageBitsForSize sz)) + word_of_nat (n * word_size)) xa) else return [] | _ \<Rightarrow> return []) s) proof (prove)
goal (1 subgoal):
 1. \<And>x xa x31 x32 x33 x34 x35. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer x && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xa)) (s\<lparr>irq_state := f (irq_state s)\<rparr>)) = the (evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer x && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xa)) s) proof (prove)
goal (1 subgoal):
 1. \<And>x xa x31 x32 x33 x34 x35. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer x && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xa)) (s\<lparr>irq_state := f (irq_state s)\<rparr>) = evalMonad (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer x && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) xa)) s proof (prove)
goal (3 subgoals):
 1. \<And>x xa x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> evalMonad (loadWord xb) (s\<lparr>irq_state := f (irq_state s)\<rparr>) = evalMonad (loadWord xb) s
 2. \<And>x xa x31 x32 x33 x34 x35 P xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord xb \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>x xa x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> det_or_fail (loadWord xb) proof (prove)
goal (3 subgoals):
 1. \<And>x x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> (fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>)) = {} \<longrightarrow> fst (loadWord xb s) = {}) \<and> (fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>)) \<noteq> {} \<longrightarrow> fst (loadWord xb s) \<noteq> {} \<and> (fst (loadWord xb s) \<noteq> {} \<longrightarrow> pick (fst ` fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>))) = pick (fst ` fst (loadWord xb s))))
 2. \<And>x xa x31 x32 x33 x34 x35 P xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord xb \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>x xa x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> det_or_fail (loadWord xb) proof (prove)
goal (5 subgoals):
 1. \<And>x x31 x32 x33 x34 x35 xb a b. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33; fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>)) = {}; (a, b) \<in> fst (loadWord xb s)\<rbrakk> \<Longrightarrow> (a, b) \<in> {}
 2. \<And>x x31 x32 x33 x34 x35 xb a b. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33; (a, b) \<in> fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>)); (a, b) \<notin> {}; fst (loadWord xb s) = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x x31 x32 x33 x34 x35 xb a b aa ba. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33; (a, b) \<in> fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>)); (a, b) \<notin> {}; pick (fst ` fst (loadWord xb (s\<lparr>irq_state := f (irq_state s)\<rparr>))) \<noteq> pick (fst ` fst (loadWord xb s)); (aa, ba) \<in> fst (loadWord xb s)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> {}
 4. \<And>x xa x31 x32 x33 x34 x35 P xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord xb \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>x xa x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> det_or_fail (loadWord xb) proof (prove)
goal (2 subgoals):
 1. \<And>x xa x31 x32 x33 x34 x35 P xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> loadWord xb \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>x xa x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> det_or_fail (loadWord xb) proof (prove)
goal (1 subgoal):
 1. \<And>x xa x31 x32 x33 x34 x35 xb. \<lbrakk>tcb_ipcframe x = ArchObjectCap (PageCap x31 x32 x33 x34 x35); AllowRead \<in> x33\<rbrakk> \<Longrightarrow> det_or_fail (loadWord xb) proof (prove)
goal:
No subgoals!