machine+aspec: add Arch_Kernel_Config_Lemmas
While having a single Kernel_Config_Lemmas was fine for constraining the number of domains, it does not work for constraining architecture-specific configuration options/values. Add an (empty for now) Arch_Kernel_Config_Lemmas theory to every architecture that imports the generic Kernel_Config_Lemmas. Change all imports of Kernel_Config_Lemmas to import Arch_Kernel_Config_Lemmas instead. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
parent
27d838af86
commit
9288b78694
|
@ -12,7 +12,7 @@ imports
|
||||||
"ExecSpec.Arch_Structs_B"
|
"ExecSpec.Arch_Structs_B"
|
||||||
ExceptionTypes_A
|
ExceptionTypes_A
|
||||||
VMRights_A
|
VMRights_A
|
||||||
ExecSpec.Kernel_Config_Lemmas
|
ExecSpec.Arch_Kernel_Config_Lemmas
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch .
|
context begin interpretation Arch .
|
||||||
|
|
|
@ -15,7 +15,7 @@ imports
|
||||||
"ExecSpec.Arch_Structs_B"
|
"ExecSpec.Arch_Structs_B"
|
||||||
ExceptionTypes_A
|
ExceptionTypes_A
|
||||||
VMRights_A
|
VMRights_A
|
||||||
ExecSpec.Kernel_Config_Lemmas
|
ExecSpec.Arch_Kernel_Config_Lemmas
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming ARM_A
|
context Arch begin global_naming ARM_A
|
||||||
|
|
|
@ -15,7 +15,7 @@ imports
|
||||||
"ExecSpec.Arch_Structs_B"
|
"ExecSpec.Arch_Structs_B"
|
||||||
ExceptionTypes_A
|
ExceptionTypes_A
|
||||||
VMRights_A
|
VMRights_A
|
||||||
ExecSpec.Kernel_Config_Lemmas
|
ExecSpec.Arch_Kernel_Config_Lemmas
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming ARM_A
|
context Arch begin global_naming ARM_A
|
||||||
|
|
|
@ -11,7 +11,7 @@ imports
|
||||||
"ExecSpec.Arch_Structs_B"
|
"ExecSpec.Arch_Structs_B"
|
||||||
ExceptionTypes_A
|
ExceptionTypes_A
|
||||||
VMRights_A
|
VMRights_A
|
||||||
ExecSpec.Kernel_Config_Lemmas
|
ExecSpec.Arch_Kernel_Config_Lemmas
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming RISCV64_A
|
context Arch begin global_naming RISCV64_A
|
||||||
|
|
|
@ -11,7 +11,7 @@ imports
|
||||||
"ExecSpec.Arch_Structs_B"
|
"ExecSpec.Arch_Structs_B"
|
||||||
ExceptionTypes_A
|
ExceptionTypes_A
|
||||||
VMRights_A
|
VMRights_A
|
||||||
ExecSpec.Kernel_Config_Lemmas
|
ExecSpec.Arch_Kernel_Config_Lemmas
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming X64_A
|
context Arch begin global_naming X64_A
|
||||||
|
|
|
@ -0,0 +1,18 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2023, Proofcraft Pty Ltd
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* Architecture-specific lemmas constraining Kernel_Config definitions *)
|
||||||
|
|
||||||
|
theory Arch_Kernel_Config_Lemmas
|
||||||
|
imports
|
||||||
|
Kernel_Config_Lemmas
|
||||||
|
Platform
|
||||||
|
begin
|
||||||
|
|
||||||
|
context Arch begin global_naming AARCH64
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -12,7 +12,7 @@ imports
|
||||||
"Word_Lib.WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
"Lib.Defs"
|
"Lib.Defs"
|
||||||
Setup_Locale
|
Setup_Locale
|
||||||
Kernel_Config_Lemmas
|
Kernel_Config
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming AARCH64
|
context Arch begin global_naming AARCH64
|
||||||
|
|
|
@ -0,0 +1,18 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2023, Proofcraft Pty Ltd
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* Architecture-specific lemmas constraining Kernel_Config definitions *)
|
||||||
|
|
||||||
|
theory Arch_Kernel_Config_Lemmas
|
||||||
|
imports
|
||||||
|
Kernel_Config_Lemmas
|
||||||
|
Platform
|
||||||
|
begin
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -12,7 +12,7 @@ imports
|
||||||
"Lib.Lib"
|
"Lib.Lib"
|
||||||
"Word_Lib.WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
Setup_Locale
|
Setup_Locale
|
||||||
Kernel_Config_Lemmas
|
Kernel_Config
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming ARM
|
context Arch begin global_naming ARM
|
||||||
|
|
|
@ -0,0 +1,18 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2023, Proofcraft Pty Ltd
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* Architecture-specific lemmas constraining Kernel_Config definitions *)
|
||||||
|
|
||||||
|
theory Arch_Kernel_Config_Lemmas
|
||||||
|
imports
|
||||||
|
Kernel_Config_Lemmas
|
||||||
|
Platform
|
||||||
|
begin
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM_HYP
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -12,7 +12,7 @@ imports
|
||||||
"Lib.Lib"
|
"Lib.Lib"
|
||||||
"Word_Lib.WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
Setup_Locale
|
Setup_Locale
|
||||||
Kernel_Config_Lemmas
|
Kernel_Config
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming ARM_HYP
|
context Arch begin global_naming ARM_HYP
|
||||||
|
|
|
@ -4,6 +4,8 @@
|
||||||
* SPDX-License-Identifier: GPL-2.0-only
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
(* Architecture-independent lemmas constraining Kernel_Config definitions *)
|
||||||
|
|
||||||
theory Kernel_Config_Lemmas
|
theory Kernel_Config_Lemmas
|
||||||
imports "$L4V_ARCH/Kernel_Config"
|
imports "$L4V_ARCH/Kernel_Config"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -0,0 +1,18 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2023, Proofcraft Pty Ltd
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* Architecture-specific lemmas constraining Kernel_Config definitions *)
|
||||||
|
|
||||||
|
theory Arch_Kernel_Config_Lemmas
|
||||||
|
imports
|
||||||
|
Kernel_Config_Lemmas
|
||||||
|
Platform
|
||||||
|
begin
|
||||||
|
|
||||||
|
context Arch begin global_naming RISCV64
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -12,7 +12,7 @@ imports
|
||||||
"Word_Lib.WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
"Lib.Defs"
|
"Lib.Defs"
|
||||||
Setup_Locale
|
Setup_Locale
|
||||||
Kernel_Config_Lemmas
|
Kernel_Config
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming RISCV64
|
context Arch begin global_naming RISCV64
|
||||||
|
|
|
@ -0,0 +1,18 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2023, Proofcraft Pty Ltd
|
||||||
|
*
|
||||||
|
* SPDX-License-Identifier: GPL-2.0-only
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* Architecture-specific lemmas constraining Kernel_Config definitions *)
|
||||||
|
|
||||||
|
theory Arch_Kernel_Config_Lemmas
|
||||||
|
imports
|
||||||
|
Kernel_Config_Lemmas
|
||||||
|
Platform
|
||||||
|
begin
|
||||||
|
|
||||||
|
context Arch begin global_naming X64
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -12,7 +12,7 @@ imports
|
||||||
"Word_Lib.WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
"Lib.Defs"
|
"Lib.Defs"
|
||||||
Setup_Locale
|
Setup_Locale
|
||||||
Kernel_Config_Lemmas
|
Kernel_Config
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context Arch begin global_naming X64
|
context Arch begin global_naming X64
|
||||||
|
|
Loading…
Reference in New Issue