theory ArchFinalise_AI

lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]:
  "\<lbrace>\<lambda>s. P (tcb_cap_valid cap ptr s)\<rbrace> do_machine_op mop \<lbrace>\<lambda>_ s. P (tcb_cap_valid cap ptr s)\<rbrace>" apply (simp add: tcb_cap_valid_def no_cap_to_obj_with_diff_ref_def) apply (rule hoare_pre) apply wps apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_cap_valid cap ptr s)\<rbrace> do_machine_op mop \<lbrace>\<lambda>_ s. P (tcb_cap_valid cap ptr s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))))\<rbrace> do_machine_op mop \<lbrace>\<lambda>_ s. P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op mop \<lbrace>\<lambda>_ s. P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))))\<rbrace>
 2. \<And>s. P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> do_machine_op mop \<lbrace>\<lambda>rv s'. P (tcb_at (fst ptr) prev_s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) prev_s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) prev_s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))))\<rbrace>
 2. \<And>s. P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<Longrightarrow> P (tcb_at (fst ptr) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd ptr) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst ptr) st cap) (fst ptr) s \<and> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst ptr) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) proof (prove)
goal:
No subgoals!