theory Tcb_C

lemma frame_gp_registers_convs:
  "length ARM_H.frameRegisters = unat n_frameRegisters"
  "length ARM_H.gpRegisters = unat n_gpRegisters"
  "n < length ARM_H.frameRegisters \<Longrightarrow>
     index frameRegistersC n = register_from_H (ARM_H.frameRegisters ! n)"
  "n < length ARM_H.gpRegisters \<Longrightarrow>
     index gpRegistersC n = register_from_H (ARM_H.gpRegisters ! n)" apply (simp_all add: ARM_H.gpRegisters_def ARM_H.frameRegisters_def
                       ARM.gpRegisters_def n_gpRegisters_def
                       ARM.frameRegisters_def n_frameRegisters_def
                       frameRegistersC_def gpRegistersC_def msgRegisters_unfold
                       fupdate_def Arrays.update_def toEnum_def
                       upto_enum_def fromEnum_def enum_register) apply (auto simp: less_Suc_eq fcp_beta Kernel_C.LR_def R14_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (length TCB_H.frameRegisters = unat n_frameRegisters &&& length TCB_H.gpRegisters = unat n_gpRegisters) &&& (n < length TCB_H.frameRegisters \<Longrightarrow> kernel_all_global_addresses.frameRegisters.[n] = register_from_H (TCB_H.frameRegisters ! n)) &&& (n < length TCB_H.gpRegisters \<Longrightarrow> kernel_all_global_addresses.gpRegisters.[n] = register_from_H (TCB_H.gpRegisters ! n)) proof (prove)
goal (2 subgoals):
 1. n < Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<Longrightarrow> (if n = 9 then SCAST(32 signed \<rightarrow> 32) R12 else (ARRAY i. if i = 8 then SCAST(32 signed \<rightarrow> 32) R11 else (ARRAY i. if i = 7 then SCAST(32 signed \<rightarrow> 32) R10 else (ARRAY i. if i = 6 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R9 else (ARRAY i. if i = 5 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R8 else (ARRAY i. if i = 4 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R1 else (ARRAY i. if i = 3 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R0 else (ARRAY i. if i = 2 then SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR else (ARRAY i. if i = Suc 0 then SCAST(32 signed \<rightarrow> 32) Kernel_C.SP else (ARRAY i. if i = 0 then SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP else (ARRAY _. 0).[i]).[i]).[i]).[i]).[i]).[i]).[i]).[i]).[i]).[n]) = register_from_H ([register.FaultIP, register.SP, register.CPSR, register.R0, register.R1, register.R8, register.R9, SL, FP, IP] ! n)
 2. n < Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<Longrightarrow> (if n = 8 then SCAST(32 signed \<rightarrow> 32) Kernel_C.TPIDRURO else (ARRAY i. if i = 7 then SCAST(32 signed \<rightarrow> 32) Kernel_C.TPIDRURW else (ARRAY i. if i = 6 then SCAST(32 signed \<rightarrow> 32) R14 else (ARRAY i. if i = 5 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R7 else (ARRAY i. if i = 4 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R6 else (ARRAY i. if i = 3 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R5 else (ARRAY i. if i = 2 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R4 else (ARRAY i. if i = Suc 0 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R3 else (ARRAY i. if i = 0 then SCAST(32 signed \<rightarrow> 32) Kernel_C.R2 else (ARRAY _. 0).[i]).[i]).[i]).[i]).[i]).[i]).[i]).[i]).[n]) = register_from_H ([register.R2, register.R3, register.R4, register.R5, register.R6, register.R7, register.LR, register.TPIDRURW, register.TPIDRURO] ! n) proof (prove)
goal:
No subgoals!