theory Arch_AC

lemma set_mrs_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf)\<rbrace>
   set_mrs thread buf msgs
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: set_mrs_def split del: if_split) apply (wpsimp wp: gets_the_wp get_wp put_wp mapM_x_wp'
                    store_word_offs_integrity_autarch[where thread=thread]
              simp: split_def zipWithM_x_mapM_x split_del: if_split)+ apply (clarsimp elim!: in_set_zipE split: if_split_asm) apply (rule order_le_less_trans[where y=msg_max_length]) apply (fastforce simp add: le_eq_less_or_eq) apply (simp add: msg_max_length_def msg_align_bits' word_size_bits_def) apply simp apply (wp set_object_integrity_autarch hoare_drop_imps hoare_vcg_all_lift)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>));
case buf of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length msgs))) | Some pptr \<Rightarrow> do y <- zipWithM_x (store_word_offs pptr) (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) msgs);
return (nat_to_len (min (length msgs) msg_max_length))
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2 a b s. \<lbrakk>buf = Some x2; is_subject aag thread; ipc_buffer_has_auth aag thread (Some x2); (a, b) \<in> set (zip (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) msgs)); integrity aag X st s\<rbrakk> \<Longrightarrow> a < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>tcb. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?B6 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> integrity aag X st s)\<rbrace>
 3. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?Q5\<rbrace> gets_the (get_tcb thread) \<lbrace>?B6\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (4 subgoals):
 1. \<And>x2 a b s. \<lbrakk>integrity aag X st s; buf = Some x2; is_subject aag thread; ipc_buffer_has_auth aag thread (Some x2); Suc (length msg_registers) \<le> msg_max_length; a = msg_max_length \<or> Suc (length msg_registers) \<le> a \<and> a < msg_max_length; b \<in> set (drop (length msg_registers) msgs)\<rbrakk> \<Longrightarrow> a < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>tcb. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?B6 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> integrity aag X st s)\<rbrace>
 3. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?Q5\<rbrace> gets_the (get_tcb thread) \<lbrace>?B6\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (5 subgoals):
 1. \<And>x2 a b s. \<lbrakk>integrity aag X st s; buf = Some x2; is_subject aag thread; ipc_buffer_has_auth aag thread (Some x2); Suc (length msg_registers) \<le> msg_max_length; a = msg_max_length \<or> Suc (length msg_registers) \<le> a \<and> a < msg_max_length; b \<in> set (drop (length msg_registers) msgs)\<rbrakk> \<Longrightarrow> a \<le> msg_max_length
 2. \<And>x2 a b s. \<lbrakk>integrity aag X st s; buf = Some x2; is_subject aag thread; ipc_buffer_has_auth aag thread (Some x2); Suc (length msg_registers) \<le> msg_max_length; a = msg_max_length \<or> Suc (length msg_registers) \<le> a \<and> a < msg_max_length; b \<in> set (drop (length msg_registers) msgs)\<rbrakk> \<Longrightarrow> msg_max_length < 2 ^ (msg_align_bits - word_size_bits)
 3. \<And>tcb. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?B6 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> integrity aag X st s)\<rbrace>
 4. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?Q5\<rbrace> gets_the (get_tcb thread) \<lbrace>?B6\<rbrace>
 5. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (4 subgoals):
 1. \<And>x2 a b s. \<lbrakk>integrity aag X st s; buf = Some x2; is_subject aag thread; ipc_buffer_has_auth aag thread (Some x2); Suc (length msg_registers) \<le> msg_max_length; a = msg_max_length \<or> Suc (length msg_registers) \<le> a \<and> a < msg_max_length; b \<in> set (drop (length msg_registers) msgs)\<rbrakk> \<Longrightarrow> msg_max_length < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>tcb. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?B6 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> integrity aag X st s)\<rbrace>
 3. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?Q5\<rbrace> gets_the (get_tcb thread) \<lbrace>?B6\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?B6 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> integrity aag X st s)\<rbrace>
 2. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?Q5\<rbrace> gets_the (get_tcb thread) \<lbrace>?B6\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?B6 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x. integrity aag X st\<rbrace>
 2. is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf \<Longrightarrow> \<lbrace>?Q5\<rbrace> gets_the (get_tcb thread) \<lbrace>?B6\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf; integrity aag X st s\<rbrakk> \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> (integrity aag X st and K (is_subject aag thread)) s proof (prove)
goal:
No subgoals!