From e9e562c33d5f91b68661860bc2863f4d138fd4bd Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 17 Apr 2020 03:01:31 +1000 Subject: [PATCH] riscv crefine: introduce registers_count type abbrev Signed-off-by: Rafal Kolanski --- proof/crefine/RISCV64/StateRelation_C.thy | 2 +- proof/crefine/RISCV64/Wellformed_C.thy | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/proof/crefine/RISCV64/StateRelation_C.thy b/proof/crefine/RISCV64/StateRelation_C.thy index 5c2ad4add..ab2bfc4f1 100644 --- a/proof/crefine/RISCV64/StateRelation_C.thy +++ b/proof/crefine/RISCV64/StateRelation_C.thy @@ -233,7 +233,7 @@ fun | "register_from_H RISCV64.NextIP = scast Kernel_C.NextIP" definition - cregs_relation :: "(MachineTypes.register \ machine_word) \ machine_word[35] \ bool" + cregs_relation :: "(MachineTypes.register \ machine_word) \ machine_word[registers_count] \ bool" where "cregs_relation Hregs Cregs \ \r. Hregs r = Cregs.[unat (register_from_H r)]" diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index bcb1c85cb..694c2e534 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -39,7 +39,8 @@ abbreviation pt_Ptr :: "machine_word \ (pte_C[512]) ptr" where "pt_Ptr == Ptr" type_synonym tcb_cnode_array = "cte_C[5]" -type_synonym registers_array = "machine_word[35]" +type_synonym registers_count = 35 +type_synonym registers_array = "machine_word[registers_count]" abbreviation "user_context_Ptr \ Ptr :: addr \ user_context_C ptr" abbreviation "machine_word_Ptr \ Ptr :: addr \ machine_word ptr"