theory Intent_DR

lemma set_registers_corres:
  "dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs)
  (corrupt_tcb_intent y)
  (mapM (%r. do v \<leftarrow> as_user thread (getRegister r);
                as_user y (setRegister r v)
             od) (x)
  )" apply (induct_tac "x") apply (clarsimp simp:bind_assoc mapM_def sequence_def) apply (rule corres_guard_imp) apply (rule dummy_corrupt_tcb_intent_corres[unfolded dc_def]) apply simp+ apply (clarsimp simp:mapM_def) apply (subst duplicate_corrupt_tcb_intent[symmetric]) apply (clarsimp simp:sequence_def) apply (rule_tac Q'="%r. tcb_at y and valid_idle and not_idle_thread y and valid_etcbs"
                  in corres_split_forwards' [where Q="%r. \<top>"]) apply (rule corres_symb_exec_r) apply (rule set_register_corres) apply (wp|simp)+ apply (simp add:bind_assoc dc_def[symmetric]) apply (rule corres_dummy_return_l) apply (rule corres_split_forwards' [where r'="dc" and Q="%x. \<top>" and Q'="%x. \<top>"]) apply (rule corres_guard_imp) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) x) proof (prove)
goal (2 subgoals):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) [])
 2. \<And>a list. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (a # list)) proof (prove)
goal (2 subgoals):
 1. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (return [])
 2. \<And>a list. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (a # list)) proof (prove)
goal (4 subgoals):
 1. dcorres (\<lambda>a b. True) ?Q5 ?Q'5 (corrupt_tcb_intent y) (return [])
 2. \<And>s. True \<Longrightarrow> ?Q5 s
 3. \<And>s. tcb_at y s \<and> valid_idle s \<and> not_idle_thread y s \<and> valid_etcbs s \<Longrightarrow> ?Q'5 s
 4. \<And>a list. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (a # list)) proof (prove)
goal (3 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. tcb_at y s \<and> valid_idle s \<and> not_idle_thread y s \<and> valid_etcbs s \<Longrightarrow> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s
 3. \<And>a list. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (mapM (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (sequence (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list)) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (sequence (do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od # map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (sequence (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list)) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (do corrupt_tcb_intent y;
corrupt_tcb_intent y
od) (sequence (do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od # map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (do ya <- corrupt_tcb_intent y;
corrupt_tcb_intent y
od) (do x <- do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od;
y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (4 subgoals):
 1. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres (?r'11 a list) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od)
 2. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a\<rbrace> do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od \<lbrace>\<lambda>r. tcb_at y and valid_idle and not_idle_thread y and valid_etcbs\<rbrace>
 4. \<And>a list rv rv'. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); ?r'11 a list rv rv'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (7 subgoals):
 1. \<And>a list v. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres (?r'11 a list) (\<lambda>_. True) (?Q'13 a list v) (corrupt_tcb_intent y) (as_user y (setRegister a v))
 2. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a\<rbrace> as_user thread (getRegister a) \<lbrace>?Q'13 a list\<rbrace>
 3. \<And>a list s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); tcb_at y s \<and> valid_idle s \<and> not_idle_thread y s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> as_user thread (getRegister a) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (as_user thread (getRegister a))
 5. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>r _. True\<rbrace>
 6. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a\<rbrace> do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od \<lbrace>\<lambda>r. tcb_at y and valid_idle and not_idle_thread y and valid_etcbs\<rbrace>
 7. \<And>a list rv rv'. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); ?r'11 a list rv rv'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (6 subgoals):
 1. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a\<rbrace> as_user thread (getRegister a) \<lbrace>\<lambda>v. valid_idle and not_idle_thread y and valid_etcbs\<rbrace>
 2. \<And>a list s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); tcb_at y s \<and> valid_idle s \<and> not_idle_thread y s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> as_user thread (getRegister a) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (as_user thread (getRegister a))
 4. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>r _. True\<rbrace>
 5. \<And>a list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a\<rbrace> do v <- as_user thread (getRegister a);
as_user y (setRegister a v)
od \<lbrace>\<lambda>r. tcb_at y and valid_idle and not_idle_thread y and valid_etcbs\<rbrace>
 6. \<And>a list rv rv'. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); dc rv rv'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (1 subgoal):
 1. \<And>list. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (1 subgoal):
 1. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (1 subgoal):
 1. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y >>= return) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []);
return (() # y)
od) proof (prove)
goal (4 subgoals):
 1. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []))
 2. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>tcb_at y and valid_idle and not_idle_thread y and valid_etcbs\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>list x ya. \<lbrakk>dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); dc x ya\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (() # ya)) proof (prove)
goal (6 subgoals):
 1. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> dcorres dc (?Q53 list) (?Q'53 list) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []))
 2. \<And>list s. \<lbrakk>dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); True\<rbrakk> \<Longrightarrow> ?Q53 list s
 3. \<And>list s. \<lbrakk>dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'53 list s
 4. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>list. dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])) \<Longrightarrow> \<lbrace>tcb_at y and valid_idle and not_idle_thread y and valid_etcbs\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return []) \<lbrace>\<lambda>x _. True\<rbrace>
 6. \<And>list x ya. \<lbrakk>dcorres dc (\<lambda>_. True) (\<lambda>a. tcb_at y a \<and> valid_idle a \<and> not_idle_thread y a \<and> valid_etcbs a) (corrupt_tcb_intent y) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (() # y)
od) (map (\<lambda>r. do v <- as_user thread (getRegister r);
as_user y (setRegister r v)
od) list) (return [])); dc x ya\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (() # ya)) proof (prove)
goal:
No subgoals!