aarch64 cspec: add Kernel_C.thy to base CKernel image on

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

spec/cspec/AARCH64/Kernel_C.thy

@@ -0,0 +1,110 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+theory Kernel_C
+imports
+  "ExecSpec.MachineTypes"
+  "CLib.CTranslationNICTA"
+  "AsmRefine.CommonOps"
+begin
+
+external_file
+  "../c/build/$L4V_ARCH/kernel_all.c_pp"
+
+context begin interpretation Arch .
+
+requalify_types
+  machine_state
+
+end
+
+declare [[populate_globals=true]]
+
+context begin interpretation Arch . (*FIXME: arch_split*)
+
+type_synonym cghost_state = "(machine_word \<rightharpoonup> vmpage_size) * (machine_word \<rightharpoonup> nat)
+    * ghost_assertions"
+
+definition
+  gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
+  "gs_clear_region ptr bits gs \<equiv>
+   (%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
+    %x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))"
+
+definition
+  gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
+  where
+  "gs_new_frames sz ptr bits \<equiv> \<lambda>gs.
+   if bits < pageBitsForSize sz then gs
+   else (\<lambda>x. if \<exists>n\<le>mask (bits - pageBitsForSize sz).
+                  x = ptr + n * 2 ^ pageBitsForSize sz then Some sz
+             else fst gs x, snd gs)"
+
+definition
+  gs_new_cnodes:: "nat \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
+  where
+  "gs_new_cnodes sz ptr bits \<equiv> \<lambda>gs.
+   if bits < sz + 4 then gs
+   else (fst gs, \<lambda>x. if \<exists>n\<le>mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4)
+                     then Some sz
+                     else fst (snd gs) x, snd (snd gs))"
+
+abbreviation
+  gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> machine_word"
+  where
+  "gs_get_assn k \<equiv> ghost_assertion_data_get k (snd o snd)"
+
+abbreviation
+  gs_set_assn :: "int \<Rightarrow> machine_word \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
+  where
+  "gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd o apsnd)"
+
+declare [[record_codegen = false]]
+declare [[allow_underscore_idents = true]]
+
+end
+
+(* workaround for the fact that the C parser wants to know the vmpage sizes*)
+(* create appropriately qualified aliases *)
+context begin interpretation Arch . global_naming vmpage_size
+requalify_consts ARMSmallPage ARMLargePage ARMHugePage
+end
+
+definition
+  ctcb_size_bits :: nat
+where
+  "ctcb_size_bits \<equiv> 10"
+
+definition
+  ctcb_offset :: "64 word"
+where
+  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
+
+lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
+
+cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS
+
+install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
+  [machinety=machine_state, ghostty=cghost_state]
+
+text \<open>Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix
+  for these:\<close>
+hide_const (open)
+  numDomains
+
+(* hide vmpage sizes again *)
+hide_const
+  vmpage_size.ARMSmallPage
+  vmpage_size.ARMLargePage
+  vmpage_size.ARMHugePage
+
+(* re-allow fully qualified accesses (for consistency). Slightly clunky *)
+context Arch begin
+global_naming "AARCH64.vmpage_size" requalify_consts ARMSmallPage ARMLargePage ARMHugePage
+global_naming "AARCH64" requalify_consts ARMSmallPage ARMLargePage ARMHugePage
+end
+
+end