theory Tcb_R

lemma decodeReadRegisters_corres:
  "corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t)
     (decode_read_registers args (cap.ThreadCap t))
     (decodeReadRegisters args (ThreadCap t))" apply (simp add: decode_read_registers_def decodeReadRegisters_def) apply (cases args, simp_all) apply (case_tac list, simp_all) apply (simp add: decodeTransfer_def) apply (simp add: range_check_def rangeCheck_def frameRegisters_def gpRegisters_def) apply (simp add: unlessE_def split del: if_split, simp add: returnOk_def split del: if_split) apply (rule corres_guard_imp) apply (rule corres_split_norE) apply (rule corres_trivial) apply (fastforce simp: returnOk_def) apply (simp add: liftE_bindE) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_trivial) apply (clarsimp simp: whenE_def) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (decode_read_registers args (cap.ThreadCap t)) (decodeReadRegisters args (capability.ThreadCap t)) proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (case args of [] \<Rightarrow> throwError ExceptionTypes_A.syscall_error.TruncatedMessage | [flags] \<Rightarrow> throwError ExceptionTypes_A.syscall_error.TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 $ word_of_nat (length MachineExports.frameRegisters + length MachineExports.gpRegisters);
p <- case cap.ThreadCap t of cap.ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError ExceptionTypes_A.syscall_error.IllegalOperation;
returnOk $ tcb_invocation.ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters
odE) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [flags] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | flags # n # x \<Rightarrow> doE rangeCheck n 1 $ length TCB_H.frameRegisters + length TCB_H.gpRegisters;
transferArch <- decodeTransfer $ fromIntegral $ flags `~shiftR~` 8;
self <- withoutFailure $ getCurThread;
whenE (capTCBPtr (capability.ThreadCap t) = self) $ throw Fault_H.syscall_error.IllegalOperation;
returnOk (tcbinvocation.ReadRegisters (capTCBPtr (capability.ThreadCap t)) (flags !! 0) n transferArch)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list. args = a # list \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (case list of [] \<Rightarrow> throwError ExceptionTypes_A.syscall_error.TruncatedMessage | n # x \<Rightarrow> doE y <- range_check n 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
returnOk (tcb_invocation.ReadRegisters t (a !! 0) n ArchDefaultExtraRegisters)
odE) (case list of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | n # x \<Rightarrow> doE y <- rangeCheck n (Suc 0) (length TCB_H.frameRegisters + length TCB_H.gpRegisters);
transferArch <- decodeTransfer (UCAST(32 \<rightarrow> 8) (a >> 8));
self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
returnOk (tcbinvocation.ReadRegisters t (a !! 0) n transferArch)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (doE y <- range_check aa 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
returnOk (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters)
odE) (doE y <- rangeCheck aa (Suc 0) (length TCB_H.frameRegisters + length TCB_H.gpRegisters);
transferArch <- decodeTransfer (UCAST(32 \<rightarrow> 8) (a >> 8));
self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
returnOk (tcbinvocation.ReadRegisters t (a !! 0) aa transferArch)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (doE y <- range_check aa 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
returnOk (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters)
odE) (doE y <- rangeCheck aa (Suc 0) (length TCB_H.frameRegisters + length TCB_H.gpRegisters);
self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
returnOk (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (doE y <- unlessE (1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)) (throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
returnOk (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters)
odE) (doE y <- unlessE (1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)) (throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))));
self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
returnOk (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t) (invs' and tcb_at' t) (doE y <- if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE y <- if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)));
self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?Q6 a list aa lista) (?Q'6 a list aa lista) (doE y <- if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE y <- if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)));
self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE)
 2. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ?Q6 a list aa lista s
 3. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q'6 a list aa lista s proof (prove)
goal (6 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?P10 a list aa lista) (?P'10 a list aa lista) (if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)))) (if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))))
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R10 a list aa lista) (?R'10 a list aa lista) (doE self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE)
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R'10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> (?P10 a list aa lista and ?Q10 a list aa lista) s
 6. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> (?P'10 a list aa lista and ?Q'10 a list aa lista) s proof (prove)
goal (6 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters)))) (if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))))
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R10 a list aa lista) (?R'10 a list aa lista) (doE self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE)
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R'10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a list aa lista) s
 6. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'10 a list aa lista) s proof (prove)
goal (5 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R10 a list aa lista) (?R'10 a list aa lista) (doE self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE self <- liftE getCurThread;
y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE)
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R'10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a list aa lista) s
 5. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'10 a list aa lista) s proof (prove)
goal (5 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R10 a (aa # lista) aa lista) (?R'10 a (aa # lista) aa lista) (do self <- gets cur_thread;
doE y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE
od) (do self <- getCurThread;
doE y <- whenE (t = self) (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE
od)
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. ?R'10 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a list aa lista) s
 5. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'10 a list aa lista) s proof (prove)
goal (7 subgoals):
 1. \<And>a list aa lista self rv'. \<lbrakk>args = a # aa # lista; list = aa # lista; self = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R28 a list aa lista self) (?R'28 a list aa lista rv') (doE y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE y <- whenE (t = rv') (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE)
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a (aa # lista) aa lista\<rbrace> gets cur_thread \<lbrace>?R28 a list aa lista\<rbrace>
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 a (aa # lista) aa lista\<rbrace> getCurThread \<lbrace>?R'28 a list aa lista\<rbrace>
 4. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q33 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'31 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a list aa lista) s
 7. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'10 a list aa lista) s proof (prove)
goal (7 subgoals):
 1. \<And>a list aa lista self rv'. \<lbrakk>args = a # aa # lista; list = aa # lista; self = rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>_. True) (\<lambda>_. True) (doE y <- whenE (t = self) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
return (Inr (tcb_invocation.ReadRegisters t (a !! 0) aa ArchDefaultExtraRegisters))
odE) (doE y <- whenE (t = rv') (throwError Fault_H.syscall_error.IllegalOperation);
return (Inr (tcbinvocation.ReadRegisters t (a !! 0) aa copy_register_sets.ARMNoExtraRegisters))
odE)
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a (aa # lista) aa lista\<rbrace> gets cur_thread \<lbrace>\<lambda>self _. True\<rbrace>
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 a (aa # lista) aa lista\<rbrace> getCurThread \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q33 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'31 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a list aa lista) s
 7. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'10 a list aa lista) s proof (prove)
goal (6 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 a (aa # lista) aa lista\<rbrace> gets cur_thread \<lbrace>\<lambda>self _. True\<rbrace>
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 a (aa # lista) aa lista\<rbrace> getCurThread \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (ExceptionTypes_A.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q33 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list aa lista\<rbrace> if 1 \<le> aa \<and> aa \<le> word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters) then return (Inr ()) else throwError (Fault_H.syscall_error.RangeError 1 (word_of_nat (length MachineExports.frameRegisters) + word_of_nat (length MachineExports.gpRegisters))) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'31 a list aa lista\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a list aa lista) s
 6. \<And>a list aa lista s. \<lbrakk>args = a # aa # lista; list = aa # lista; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'10 a list aa lista) s proof (prove)
goal:
No subgoals!