theory Syscall_DR

lemma weak_det_spec_get_mrs:
  notes option.case_cong_weak [cong]
  shows "weak_det_spec P (get_mrs a b c)" apply (clarsimp simp:get_mrs_def) apply (rule weak_det_spec_compose)+ apply (simp add:weak_det_spec_simps split:option.splits)+ apply (rule conjI) apply clarsimp apply (rule weak_det_spec_mapM) apply (simp add:weak_det_spec_load_word_offs) apply clarsimp apply (rule weak_det_spec_mapM) apply (simp add:weak_det_spec_load_word_offs) apply (simp add:weak_det_spec_thread_get) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (get_mrs a b c) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) a;
buf_mrs <- case b of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length];
return (take (unat (mi_length c)) (map context msg_registers) @ take (unat (mi_length c) - length msg_registers) buf_mrs)
od) proof (prove)
goal (3 subgoals):
 1. \<And>Q r Qa ra. weak_det_spec (Qa ra) (return (take (unat (mi_length c)) (map r msg_registers) @ take (unat (mi_length c) - length msg_registers) ra))
 2. \<And>Q r P. weak_det_spec P (case b of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length])
 3. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (2 subgoals):
 1. \<And>P. (Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length])))) \<and> (\<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) [])))
 2. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (3 subgoals):
 1. \<And>P. Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length])))
 2. \<And>P. \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) []))
 3. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (3 subgoals):
 1. \<And>P x2. \<lbrakk>Suc (length msg_registers) \<le> msg_max_length; b = Some x2\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs x2) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))
 2. \<And>P. \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) []))
 3. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (3 subgoals):
 1. \<And>P x2 r Pa. \<lbrakk>Suc (length msg_registers) \<le> msg_max_length; b = Some x2\<rbrakk> \<Longrightarrow> weak_det_spec Pa (load_word_offs x2 r)
 2. \<And>P. \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) []))
 3. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (2 subgoals):
 1. \<And>P. \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<forall>x2. b = Some x2 \<longrightarrow> weak_det_spec P (mapM (load_word_offs x2) []))
 2. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (2 subgoals):
 1. \<And>P x2. \<lbrakk>\<not> Suc (length msg_registers) \<le> msg_max_length; b = Some x2\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs x2) [])
 2. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (2 subgoals):
 1. \<And>P x2 r Pa. \<lbrakk>\<not> Suc (length msg_registers) \<le> msg_max_length; b = Some x2\<rbrakk> \<Longrightarrow> weak_det_spec Pa (load_word_offs x2 r)
 2. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal (1 subgoal):
 1. \<And>P. weak_det_spec P (thread_get (arch_tcb_get_registers \<circ> tcb_arch) a) proof (prove)
goal:
No subgoals!