theory Ipc_R

lemma handle_fault_reply_registers_corres:
  "corres (=) (tcb_at t) (tcb_at' t)
           (do t' \<leftarrow> arch_get_sanitise_register_info t;
               y \<leftarrow> as_user t
                (zipWithM_x
                  (\<lambda>r v. setRegister r
                          (sanitise_register t' r v))
                  msg_template msg);
               return (label = 0)
            od)
           (do t' \<leftarrow> getSanitiseRegisterInfo t;
               y \<leftarrow> asUser t
                (zipWithM_x
                  (\<lambda>r v. setRegister r (sanitiseRegister t' r v))
                  msg_template msg);
               return (label = 0)
            od)" apply (rule corres_guard_imp) apply (clarsimp simp: arch_get_sanitise_register_info_def getSanitiseRegisterInfo_def) apply (rule corres_split) apply (rule asUser_corres') apply(simp add: setRegister_def sanitise_register_def
                       sanitiseRegister_def syscallMessage_def) apply(subst zipWithM_x_modify)+ apply(rule corres_modify') apply (simp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (do t' <- arch_get_sanitise_register_info t;
y <- as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t' r v)) msg_template msg);
return (label = (0::'a))
od) (do t' <- local.getSanitiseRegisterInfo t;
y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister t' r v)) msg_template msg);
return (label = (0::'a))
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do t' <- arch_get_sanitise_register_info t;
y <- as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register t' r v)) msg_template msg);
return (label = (0::'a))
od) (do t' <- local.getSanitiseRegisterInfo t;
y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister t' r v)) msg_template msg);
return (label = (0::'a))
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do y <- as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg);
return (label = (0::'a))
od) (do y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg);
return (label = (0::'a))
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ?r'6 ?P6 ?P'6 (as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg)) (asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg))
 2. \<And>rv rv'. ?r'6 rv rv' \<Longrightarrow> corres (=) (?R6 rv) (?R'6 rv') (return (label = (0::'a))) (return (label = (0::'a)))
 3. \<lbrace>?Q6\<rbrace> as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg) \<lbrace>?R'6\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. corres_underlying Id False True ?r'6 (\<lambda>_. True) (\<lambda>_. True) (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg) (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg)
 2. \<And>rv rv'. ?r'6 rv rv' \<Longrightarrow> corres (=) (?R6 rv) (?R'6 rv') (return (label = (0::'a))) (return (label = (0::'a)))
 3. \<lbrace>?Q6\<rbrace> as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg) \<lbrace>?R'6\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q6) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. corres_underlying Id False True ?r'6 (\<lambda>_. True) (\<lambda>_. True) (zipWithM_x (\<lambda>r v. modify (\<lambda>uc. uc(r := case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))) msg_template msg) (zipWithM_x (\<lambda>r v. modify (\<lambda>uc. uc(r := case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))) msg_template msg)
 2. \<And>rv rv'. ?r'6 rv rv' \<Longrightarrow> corres (=) (?R6 rv) (?R'6 rv') (return (label = (0::'a))) (return (label = (0::'a)))
 3. \<lbrace>?Q6\<rbrace> as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg) \<lbrace>?R'6\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q6) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. corres_underlying Id False True ?r'6 (\<lambda>_. True) (\<lambda>_. True) (modify (\<lambda>s. foldl (\<lambda>s (a, b). s(a := case a of CPSR \<Rightarrow> b && 0xF8000000 || 0x150 | _ \<Rightarrow> b)) s (zip msg_template msg))) (modify (\<lambda>s. foldl (\<lambda>s (a, b). s(a := case a of CPSR \<Rightarrow> b && 0xF8000000 || 0x150 | _ \<Rightarrow> b)) s (zip msg_template msg)))
 2. \<And>rv rv'. ?r'6 rv rv' \<Longrightarrow> corres (=) (?R6 rv) (?R'6 rv') (return (label = (0::'a))) (return (label = (0::'a)))
 3. \<lbrace>?Q6\<rbrace> as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg) \<lbrace>?R'6\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q6) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<forall>s s'. (s, s') \<in> Id \<longrightarrow> (foldl (\<lambda>s (a, b). s(a := case a of CPSR \<Rightarrow> b && 0xF8000000 || 0x150 | _ \<Rightarrow> b)) s (zip msg_template msg), foldl (\<lambda>s (a, b). s(a := case a of CPSR \<Rightarrow> b && 0xF8000000 || 0x150 | _ \<Rightarrow> b)) s' (zip msg_template msg)) \<in> Id
 2. ?r'6 () ()
 3. \<And>rv rv'. ?r'6 rv rv' \<Longrightarrow> corres (=) (?R6 rv) (?R'6 rv') (return (label = (0::'a))) (return (label = (0::'a)))
 4. \<lbrace>?Q6\<rbrace> as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register False r v)) msg_template msg) \<lbrace>?R6\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister False r v)) msg_template msg) \<lbrace>?R'6\<rbrace>
 6. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q6) s
 7. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'6) s proof (prove)
goal:
No subgoals!