theory Syscall_DR

lemma empty_when_fail_get_mrs:
  notes option.case_cong_weak [cong]
  shows "empty_when_fail (get_mrs a b c)" apply (clarsimp simp:get_mrs_def) apply (rule empty_when_fail_compose)+ apply (simp add:empty_when_fail_return split:option.splits)+ apply (rule conjI) apply clarsimp apply (rule empty_when_fail_mapM) apply (simp add:empty_when_fail_load_word_offs weak_det_spec_load_word_offs) apply clarsimp apply (rule empty_when_fail_mapM) apply (simp add:empty_when_fail_load_word_offs weak_det_spec_load_word_offs) apply (clarsimp simp:empty_when_fail_return 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:empty_when_fail_thread_get) apply (simp add:weak_det_spec_thread_get) done

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