theory SyscallArgs_C

lemma getMRs_rel:
  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and>
        case_option \<top> valid_ipc_buffer_ptr' buffer s \<and>
        cur_tcb' s\<rbrace>
  getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace>" apply (simp add: getMRs_rel_def) apply (rule hoare_pre) apply (rule_tac x=mi in hoare_exI) apply wp apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv,s)}" in hoare_strengthen_post) apply (wp det_result det_wp_getMRs) apply clarsimp apply (clarsimp simp: cur_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}\<rbrace>
 2. \<And>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>rv s. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(rv, s)}\<rbrace>
 2. \<And>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'5\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>rv s. fst (getMRs (ksCurThread s) buffer mi s) = {(rv, s)}\<rbrace>
 2. \<And>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s \<Longrightarrow> msgLength mi \<le> msgMaxLength \<and> ?P'5 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'5\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv, s)}\<rbrace>
 2. \<And>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv, s)} \<Longrightarrow> fst (getMRs (ksCurThread s) buffer mi s) = {(rv, s)}
 3. \<And>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s \<Longrightarrow> msgLength mi \<le> msgMaxLength \<and> ?P'5 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv, s)} \<Longrightarrow> fst (getMRs (ksCurThread s) buffer mi s) = {(rv, s)}
 2. \<And>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s \<Longrightarrow> msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<and> cur_tcb' s \<Longrightarrow> msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s proof (prove)
goal:
No subgoals!