theory Ipc_IF

lemma copy_mrs_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
   copy_mrs sender sbuf receiver rbuf n
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding copy_mrs_def including no_pre apply (wp | wpc)+ apply (rule_tac Q="\<lambda>_. globals_equiv s" in hoare_strengthen_post) apply (wp mapM_wp' | wpc)+ apply (wp store_word_offs_globals_equiv)+ apply fastforce apply simp apply (rule_tac Q="\<lambda>_. globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)"
                in hoare_strengthen_post) apply (wp mapM_wp' as_user_globals_equiv) apply (simp) apply (fastforce) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> copy_mrs sender sbuf receiver rbuf n \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> do hardware_mrs <- return $ take (unat n) msg_registers;
mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs;
buf_mrs <- case (sbuf, rbuf) of (None, b) \<Rightarrow> return [] | (Some sb_ptr, None) \<Rightarrow> return [] | (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)];
return $ min n $ nat_to_len $ length hardware_mrs + length buf_mrs
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> do hardware_mrs <- return $ take (unat n) msg_registers;
mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs;
buf_mrs <- case (sbuf, rbuf) of (None, b) \<Rightarrow> return [] | (Some sb_ptr, None) \<Rightarrow> return [] | (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)];
return $ min n $ nat_to_len $ length hardware_mrs + length buf_mrs
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>hardware_mrs x x2 x2a. \<lbrakk>sbuf = Some x2; rbuf = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R30 hardware_mrs x x2 x2a\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs x2a x) [length msg_registers + 1..<Suc (unat n)] \<lbrace>\<lambda>buf_mrs. globals_equiv s\<rbrace>
 2. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x sa. (sbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. sbuf = Some xa \<longrightarrow> (rbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xb. rbuf = Some xb \<longrightarrow> ?R30 hardware_mrs x xa xb sa))\<rbrace>
 3. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>hardware_mrs x x2 x2a. \<lbrakk>sbuf = Some x2; rbuf = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R30 hardware_mrs x x2 x2a\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs x2a x) [length msg_registers + 1..<Suc (unat n)] \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>hardware_mrs x x2 x2a rv sa. \<lbrakk>sbuf = Some x2; rbuf = Some x2a; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 3. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x sa. (sbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. sbuf = Some xa \<longrightarrow> (rbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xb. rbuf = Some xb \<longrightarrow> ?R30 hardware_mrs x xa xb sa))\<rbrace>
 4. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>hardware_mrs x x2 x2a xa v. \<lbrakk>sbuf = Some x2; rbuf = Some x2a; xa \<in> set [length msg_registers + 1..<Suc (unat n)]\<rbrakk> \<Longrightarrow> \<lbrace>?B39 hardware_mrs x x2 x2a xa v\<rbrace> store_word_offs x2a xa v \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>hardware_mrs x x2 x2a xa. \<lbrakk>sbuf = Some x2; rbuf = Some x2a; xa \<in> set [length msg_registers + 1..<Suc (unat n)]\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> load_word_offs x2 xa \<lbrace>?B39 hardware_mrs x x2 x2a xa\<rbrace>
 3. \<And>hardware_mrs x x2 x2a rv sa. \<lbrakk>sbuf = Some x2; rbuf = Some x2a; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 4. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x sa. (sbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. sbuf = Some x \<longrightarrow> (rbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. rbuf = Some x \<longrightarrow> globals_equiv s sa))\<rbrace>
 5. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>hardware_mrs x x2 x2a rv sa. \<lbrakk>sbuf = Some x2; rbuf = Some x2a; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 2. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x sa. (sbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. sbuf = Some x \<longrightarrow> (rbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. rbuf = Some x \<longrightarrow> globals_equiv s sa))\<rbrace>
 3. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x sa. (sbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. sbuf = Some x \<longrightarrow> (rbuf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. rbuf = Some x \<longrightarrow> globals_equiv s sa))\<rbrace>
 2. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender (getRegister r);
as_user receiver (setRegister r v)
od) hardware_mrs \<lbrace>\<lambda>x. globals_equiv s\<rbrace>
 2. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>hardware_mrs. \<lbrace>?B hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user sender (getRegister r);
as_user receiver (setRegister r v)
od) hardware_mrs \<lbrace>\<lambda>_. globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
 2. \<And>hardware_mrs rv sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> globals_equiv s sa
 3. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>hardware_mrs x sa. \<lbrakk>x \<in> set hardware_mrs; (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa\<rbrakk> \<Longrightarrow> (globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)) sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa
 2. \<And>hardware_mrs rv sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> globals_equiv s sa
 3. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>\<lambda>hardware_mrs. globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>hardware_mrs rv sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> globals_equiv s sa
 2. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>\<lambda>hardware_mrs. globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> return $ take (unat n) msg_registers \<lbrace>\<lambda>hardware_mrs. globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> proof (prove)
goal:
No subgoals!