theory Ipc_AC

lemma copy_mrs_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    K ((\<not> is_subject aag receiver \<longrightarrow> case_option True (\<lambda>buf'. auth_ipc_buffers st receiver =
                                                                ptr_range buf' msg_align_bits) rbuf) \<and>
       (case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits) rbuf) \<and>
       unat n < 2 ^ (msg_align_bits - word_size_bits))\<rbrace>
   copy_mrs sender sbuf receiver rbuf n
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" unfolding copy_mrs_def apply (rule hoare_gen_asm) apply (wp as_user_respects_in_ipc store_word_offs_respects_in_ipc
            mapM_wp' hoare_vcg_const_imp_lift hoare_vcg_all_lift
         | wpc | fastforce split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K ((pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case rbuf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case rbuf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits) \<and> unat n < 2 ^ (msg_align_bits - word_size_bits))\<rbrace> copy_mrs sender sbuf receiver rbuf n \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K ((pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case rbuf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case rbuf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits) \<and> unat n < 2 ^ (msg_align_bits - word_size_bits))\<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>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case rbuf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case rbuf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits) \<and> unat n < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st\<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>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal:
No subgoals!