theory CLevityCatch

lemma asUser_get_registers:
  "\<lbrace>tcb_at' target\<rbrace>
     asUser target (mapM getRegister xs)
   \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. map ((atcbContextGet o tcbArch) tcb) xs = rv) target s\<rbrace>" apply (induct xs) apply (simp add: mapM_empty asUser_return) apply wp apply simp apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond) apply wp apply simp apply (rule hoare_strengthen_post) apply (erule hoare_vcg_conj_lift) apply (rule asUser_inv) apply (simp add: getRegister_def) apply (wp mapM_wp') apply clarsimp apply (erule(1) obj_at_conj') apply (wp) apply (simp add: asUser_def split_def threadGet_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: getRegister_def simpler_gets_def
                        obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) xs = rv) target\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister []) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) [] = rv) target\<rbrace>
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister (x1 # xs)) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) (x1 # xs) = rv) target\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>tcb_at' target\<rbrace> do u <- stateAssert (tcb_at' target) [];
return []
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. [] = rv) target\<rbrace>
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister (x1 # xs)) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) (x1 # xs) = rv) target\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at' target s \<Longrightarrow> tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. [] = []) target s
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister (x1 # xs)) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) (x1 # xs) = rv) target\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister (x1 # xs)) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map ((atcbContextGet \<circ> tcbArch) tcb) (x1 # xs) = rv) target\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' target\<rbrace> do rv <- asUser target (getRegister x1);
rva <- asUser target (mapM getRegister xs);
u <- stateAssert (tcb_at' target) [];
return (rv # rva)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 # map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1 xs x. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?B9 x1 xs x\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv s. tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 # map (atcbContextGet (tcbArch tcb)) xs = x # rv) target s\<rbrace>
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>?B9 x1 xs\<rbrace>
 3. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (3 subgoals):
 1. \<And>x1 xs x. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?B9 x1 xs x\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv s. tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s\<rbrace>
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>?B9 x1 xs\<rbrace>
 3. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (4 subgoals):
 1. \<And>x1 xs x. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?B9 x1 xs x\<rbrace> asUser target (mapM getRegister xs) \<lbrace>?Q14 x1 xs x\<rbrace>
 2. \<And>x1 xs x rv s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; ?Q14 x1 xs x rv s\<rbrakk> \<Longrightarrow> tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s
 3. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>?B9 x1 xs\<rbrace>
 4. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (4 subgoals):
 1. \<And>x1 xs x. \<lbrace>?P'17 x1 xs x\<rbrace> asUser target (mapM getRegister xs) \<lbrace>?Q'17 x1 xs x\<rbrace>
 2. \<And>x1 xs x rv s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target s \<and> ?Q'17 x1 xs x rv s\<rbrakk> \<Longrightarrow> tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s
 3. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>x s. tcb_at' target s \<and> ?P'17 x1 xs x s\<rbrace>
 4. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (4 subgoals):
 1. \<And>x1 xs x P. \<lbrace>P\<rbrace> mapM getRegister xs \<lbrace>\<lambda>x. P\<rbrace>
 2. \<And>x1 xs x rv s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target s \<and> ?P'17 x1 xs x s\<rbrakk> \<Longrightarrow> tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s
 3. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>x s. tcb_at' target s \<and> ?P'17 x1 xs x s\<rbrace>
 4. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (4 subgoals):
 1. \<And>xs P. \<lbrace>P\<rbrace> mapM (\<lambda>a. gets (\<lambda>uc. uc a)) xs \<lbrace>\<lambda>x. P\<rbrace>
 2. \<And>x1 xs x rv s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target s \<and> ?P'17 x1 xs x s\<rbrakk> \<Longrightarrow> tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s
 3. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>x s. tcb_at' target s \<and> ?P'17 x1 xs x s\<rbrace>
 4. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (3 subgoals):
 1. \<And>x1 xs x rv s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target s \<and> ?P'17 x1 xs x s\<rbrakk> \<Longrightarrow> tcb_at' target s \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>x s. tcb_at' target s \<and> ?P'17 x1 xs x s\<rbrace>
 3. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (3 subgoals):
 1. \<And>x1 xs x rv s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target s; ?P'17 x1 xs x s; tcb_at' target s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) x1 = x \<and> map (atcbContextGet (tcbArch tcb)) xs = rv) target s
 2. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>x s. tcb_at' target s \<and> ?P'17 x1 xs x s\<rbrace>
 3. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?Q8 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>x s. tcb_at' target s \<and> obj_at' (\<lambda>k. atcbContextGet (tcbArch k) x1 = x) target s\<rbrace>
 2. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> ?Q8 x1 xs s proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?P'37 x1 xs\<rbrace> asUser target (getRegister x1) \<lbrace>\<lambda>rv. obj_at' (\<lambda>k. atcbContextGet (tcbArch k) x1 = rv) target\<rbrace>
 2. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> tcb_at' target s \<and> ?P'37 x1 xs s proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs. \<lbrace>tcb_at' target\<rbrace> do uc <- liftM (atcbContextGet \<circ> tcbArch) (getObject target);
p <- select_f (mapM getRegister xs uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) target;
return (fst p)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace> \<Longrightarrow> \<lbrace>?P'37 x1 xs\<rbrace> do uc <- liftM (atcbContextGet \<circ> tcbArch) (getObject target);
p <- select_f (getRegister x1 uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) target;
return (fst p)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>k. atcbContextGet (tcbArch k) x1 = rv) target\<rbrace>
 2. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> tcb_at' target s \<and> ?P'37 x1 xs s proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs s. \<lbrakk>\<lbrace>tcb_at' target\<rbrace> asUser target (mapM getRegister xs) \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. map (atcbContextGet (tcbArch tcb)) xs = rv) target\<rbrace>; tcb_at' target s\<rbrakk> \<Longrightarrow> tcb_at' target s \<and> (tcb_at' target s \<longrightarrow> (\<exists>t. ko_at' t target s \<and> ((\<lambda>uc s. \<forall>x\<in>fst (getRegister x1 uc). obj_at' (\<lambda>obj. if target = target then atcbContextGet (tcbArch (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj)) x1 = fst x else atcbContextGet (tcbArch obj) x1 = fst x) target s) \<circ> (atcbContextGet \<circ> tcbArch)) t s)) proof (prove)
goal:
No subgoals!