theory ArchIpc_IF

lemma copy_mrs_reads_respects[Ipc_IF_assms]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label)
     (K (aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf
                                             \<and> unat n < 2 ^ (msg_align_bits - word_size_bits)))
     (copy_mrs sender sbuf receiver rbuf n)" unfolding copy_mrs_def fun_app_def apply (rule gen_asm_ev) apply (wp mapM_ev'' store_word_offs_reads_respects load_word_offs_reads_respects
            as_user_set_register_reads_respects' as_user_reads_respects
         | wpc
         | simp add: det_setRegister det_getRegister split del: if_split)+ apply clarsimp apply (rename_tac n') apply (subgoal_tac "ptr_range (x + of_nat n' * of_nat word_size) word_size_bits
                      \<subseteq> ptr_range x msg_align_bits") apply (simp add: for_each_byte_of_word_def2) apply (simp add: aag_can_read_or_affect_ipc_buffer_def) apply (erule conjE) apply (rule ballI) apply (erule bspec) apply (erule (1) subsetD[rotated]) apply (rule ptr_range_subset) apply (simp add: aag_can_read_or_affect_ipc_buffer_def) apply (simp add: msg_align_bits') apply (simp add: msg_align_bits word_bits_def) apply (simp add: word_size_def word_size_bits_def) apply (subst upto_enum_step_shift_red[where us=2, simplified]) apply (simp add: msg_align_bits word_bits_def aag_can_read_or_affect_ipc_buffer_def )+ apply (fastforce simp: image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> unat n < 2 ^ (msg_align_bits - word_size_bits))) (copy_mrs sender sbuf receiver rbuf n) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> unat n < 2 ^ (msg_align_bits - word_size_bits))) (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) proof (prove)
goal (1 subgoal):
 1. aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> unat n < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (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) proof (prove)
goal (1 subgoal):
 1. aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> unat n < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> \<forall>x. sbuf = Some x \<longrightarrow> (\<exists>x. rbuf = Some x) \<longrightarrow> (\<forall>xa. Suc (length msg_registers) \<le> unat n \<and> (xa = unat n \<or> Suc (length msg_registers) \<le> xa \<and> xa < unat n) \<longrightarrow> for_each_byte_of_word (aag_can_read_or_affect aag l) (x + word_of_nat xa * word_of_nat word_size)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; xb = unat n \<or> Suc (length msg_registers) \<le> xb \<and> xb < unat n\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read_or_affect aag l) (x + word_of_nat xb * word_of_nat word_size) proof (prove)
goal (1 subgoal):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read_or_affect aag l) (x + word_of_nat n' * word_of_nat word_size) proof (prove)
goal (2 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n; ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits\<rbrakk> \<Longrightarrow> for_each_byte_of_word (aag_can_read_or_affect aag l) (x + word_of_nat n' * word_of_nat word_size)
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n; ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits. aag_can_read_or_affect aag l x
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; is_aligned x msg_align_bits \<and> (\<forall>x\<in>ptr_range x msg_align_bits. aag_can_read_or_affect aag l x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n; ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits. aag_can_read_or_affect aag l x
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n; ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits; is_aligned x msg_align_bits; \<forall>x\<in>ptr_range x msg_align_bits. aag_can_read_or_affect aag l x\<rbrakk> \<Longrightarrow> \<forall>x\<in>ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits. aag_can_read_or_affect aag l x
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>x xa n' xb. \<lbrakk>aag_can_read_or_affect aag l sender; unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n; ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits; is_aligned x msg_align_bits; \<forall>x\<in>ptr_range x msg_align_bits. aag_can_read_or_affect aag l x; xb \<in> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l xb
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (2 subgoals):
 1. \<And>x xa n' xb. \<lbrakk>aag_can_read_or_affect aag l sender; unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n; ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits; is_aligned x msg_align_bits; xb \<in> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits\<rbrakk> \<Longrightarrow> xb \<in> ptr_range x msg_align_bits
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (1 subgoal):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> ptr_range (x + word_of_nat n' * word_of_nat word_size) word_size_bits \<subseteq> ptr_range x msg_align_bits proof (prove)
goal (4 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> is_aligned x msg_align_bits
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 3. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 4. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * word_of_nat word_size \<in> set [x , x + word_size .e. x + 2 ^ msg_align_bits - 1] proof (prove)
goal (3 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> word_size_bits \<le> msg_align_bits
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 3. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * word_of_nat word_size \<in> set [x , x + word_size .e. x + 2 ^ msg_align_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> msg_align_bits < word_bits
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * word_of_nat word_size \<in> set [x , x + word_size .e. x + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - word_size_bits); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * word_of_nat word_size \<in> set [x , x + word_size .e. x + 2 ^ msg_align_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - 2); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * 4 \<in> set [x , x + 4 .e. x + 2 ^ msg_align_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - 2); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> is_aligned x msg_align_bits
 2. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - 2); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> msg_align_bits < LENGTH(32)
 3. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - 2); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits
 4. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; aag_can_read_or_affect_ipc_buffer aag l (Some x); unat n < 2 ^ (msg_align_bits - 2); sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * 4 \<in> set (map (\<lambda>xa. x + word_of_nat xa * 4) [0..<2 ^ (msg_align_bits - 2)]) proof (prove)
goal (1 subgoal):
 1. \<And>x xa n'. \<lbrakk>aag_can_read_or_affect aag l sender; is_aligned x 9 \<and> (\<forall>x\<in>ptr_range x 9. aag_can_read_or_affect aag l x); unat n < 128; sbuf = Some x; rbuf = Some xa; Suc (length msg_registers) \<le> unat n; n' = unat n \<or> Suc (length msg_registers) \<le> n' \<and> n' < unat n\<rbrakk> \<Longrightarrow> x + word_of_nat n' * 4 \<in> (\<lambda>xa. x + word_of_nat xa * 4) ` {0..<128} proof (prove)
goal:
No subgoals!