theory Ipc_C

lemma syscallMessage_ccorres:
  "n < unat n_syscallMessage
      \<Longrightarrow> register_from_H (ARM_H.syscallMessage ! n)
           = index syscallMessageC n" apply (simp add: ARM_H.syscallMessage_def syscallMessageC_def
                   ARM.syscallMessage_def
                   MessageID_Exception_def MessageID_Syscall_def
                   n_syscallMessage_def msgRegisters_unfold) apply (simp add: upto_enum_def fromEnum_def enum_register) apply (simp add: toEnum_def enum_register) apply (clarsimp simp: fupdate_def Kernel_C.CPSR_def
              | drule nat_less_cases' | erule disjE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < unat n_syscallMessage \<Longrightarrow> register_from_H (FaultHandler_H.syscallMessage ! n) = kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall].[n] proof (prove)
goal (1 subgoal):
 1. n < 12 \<Longrightarrow> register_from_H (([register.R0 .e. register.R7] @ [register.FaultIP, register.SP, register.LR, register.CPSR]) ! n) = fupdate (Suc 0) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate (Suc 0) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate (Suc 0) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 11 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate 0 (fupdate 10 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.LR)) (fupdate 0 (fupdate 9 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate 0 (fupdate 8 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 7 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R7)) (fupdate 0 (fupdate 6 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R6)) (fupdate 0 (fupdate 5 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5)) (fupdate 0 (fupdate 4 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4)) (fupdate 0 (fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3)) (fupdate 0 (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2)) (fupdate 0 (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R1)) (fupdate 0 (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R0)) (ARRAY _ _. 0))))))))))))))).[0].[n] proof (prove)
goal (1 subgoal):
 1. n < 12 \<Longrightarrow> register_from_H ([toEnum 0, toEnum (Suc 0), toEnum (Suc (Suc 0)), toEnum (Suc (Suc (Suc 0))), toEnum (Suc (Suc (Suc (Suc 0)))), toEnum (Suc (Suc (Suc (Suc (Suc 0))))), toEnum (Suc (Suc (Suc (Suc (Suc (Suc 0)))))), toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))), register.FaultIP, register.SP, register.LR, register.CPSR] ! n) = fupdate (Suc 0) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate (Suc 0) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate (Suc 0) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 11 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate 0 (fupdate 10 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.LR)) (fupdate 0 (fupdate 9 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate 0 (fupdate 8 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 7 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R7)) (fupdate 0 (fupdate 6 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R6)) (fupdate 0 (fupdate 5 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5)) (fupdate 0 (fupdate 4 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4)) (fupdate 0 (fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3)) (fupdate 0 (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2)) (fupdate 0 (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R1)) (fupdate 0 (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R0)) (ARRAY _ _. 0))))))))))))))).[0].[n] proof (prove)
goal (1 subgoal):
 1. n < 12 \<Longrightarrow> register_from_H ([register.R0, register.R1, register.R2, register.R3, register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] ! n) = fupdate (Suc 0) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate (Suc 0) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate (Suc 0) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 11 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate 0 (fupdate 10 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.LR)) (fupdate 0 (fupdate 9 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate 0 (fupdate 8 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 7 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R7)) (fupdate 0 (fupdate 6 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R6)) (fupdate 0 (fupdate 5 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5)) (fupdate 0 (fupdate 4 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4)) (fupdate 0 (fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3)) (fupdate 0 (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2)) (fupdate 0 (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R1)) (fupdate 0 (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R0)) (ARRAY _ _. 0))))))))))))))).[0].[n] proof (prove)
goal:
No subgoals!