1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11(*
12Dummy initial kernel state. Real kernel boot up is more complex.
13*)
14
15chapter "An Initial Kernel State"
16
17theory Init_A
18imports "../Retype_A"
19begin
20
21context Arch begin global_naming X64_A
22
23text {*
24  This is not a specification of true kernel
25  initialisation. This theory describes a dummy initial state only, to
26  show that the invariants and refinement relation are consistent.
27*}
28
29(* 8KiB *)
30definition
31  init_irq_node_ptr :: obj_ref where
32  "init_irq_node_ptr = kernel_base + 0x2000"
33
34(* 4KiB *)
35definition
36  init_global_pml4 :: obj_ref where
37  "init_global_pml4 = kernel_base + 0x4000"
38
39(* 4KiB *)
40definition
41  init_global_pdpt :: obj_ref where
42  "init_global_pdpt = kernel_base + 0x5000"
43
44(* 4KiB *)
45definition
46  init_global_pd :: obj_ref where
47  "init_global_pd = kernel_base + 0x6000"
48
49definition
50  "init_arch_state \<equiv> \<lparr>
51    x64_asid_table = Map.empty,
52    x64_global_pml4 = init_global_pml4,
53    x64_kernel_vspace =
54      \<lambda>ref. if ref \<in> {pptr_base .. pptr_base + mask pml4_shift_bits}
55              then X64VSpaceKernelWindow
56              else X64VSpaceInvalidRegion,
57    x64_global_pts = [],
58    x64_global_pdpts = [init_global_pdpt],
59    x64_global_pds = [init_global_pd],
60    x64_current_cr3 = cr3 0 0,
61    x64_allocated_io_ports = \<lambda>_. False,
62    x64_num_ioapics = 1,
63    x64_irq_state = K IRQFree
64   \<rparr>"
65
66definition [simp]:
67  "global_pml4 \<equiv> (\<lambda>_ :: 9 word. InvalidPML4E)
68    (0x1FF := PDPointerTablePML4E (addrFromPPtr init_global_pdpt) {} {})"
69
70(* The kernel uses huge page mappings in the global PDPT to get a view of all physical memory.
71   The exception is the upper-most PDPT entry, which maps to the global page directory. *)
72definition [simp]:
73  "global_pdpt \<equiv> (\<lambda> i :: 9 word. HugePagePDPTE (ucast i << 30) {} {})
74                    (0x1FF := PageDirectoryPDPTE (addrFromPPtr init_global_pd) {} {})"
75
76(* C kernel initialisation refines this down to small pages for devices, but we'll stop here. *)
77definition [simp]:
78  "global_pd \<equiv> (\<lambda> i :: 9 word. LargePagePDE (0x03FE00 + ucast i << 21) {} {})"
79
80definition
81  "init_kheap \<equiv>
82    (\<lambda>x. if \<exists>irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x
83           then Some (CNode 0 (empty_cnode 0))
84           else None)
85    (idle_thread_ptr \<mapsto>
86       TCB \<lparr>
87         tcb_ctable = NullCap,
88         tcb_vtable = NullCap,
89         tcb_reply = NullCap,
90         tcb_caller = NullCap,
91         tcb_ipcframe = NullCap,
92         tcb_state = IdleThreadState,
93         tcb_fault_handler = replicate word_bits False,
94         tcb_ipc_buffer = 0,
95         tcb_fault = None,
96         tcb_bound_notification = None,
97         tcb_mcpriority = minBound,
98         tcb_arch = init_arch_tcb
99         \<rparr>,
100     init_global_pml4 \<mapsto> ArchObj (PageMapL4 global_pml4),
101     init_global_pdpt \<mapsto> ArchObj (PDPointerTable global_pdpt),
102     init_global_pd \<mapsto> ArchObj (PageDirectory global_pd)
103    )"
104
105definition
106  "init_cdt \<equiv> Map.empty"
107
108definition
109  "init_ioc \<equiv>
110   \<lambda>(a,b). (\<exists>obj. init_kheap a = Some obj \<and>
111                  (\<exists>cap. cap_of obj b = Some cap \<and> cap \<noteq> cap.NullCap))"
112
113definition
114  "init_A_st \<equiv> \<lparr>
115    kheap = init_kheap,
116    cdt = init_cdt,
117    is_original_cap = init_ioc,
118    cur_thread = idle_thread_ptr,
119    idle_thread = idle_thread_ptr,
120    machine_state = init_machine_state,
121    interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
122    interrupt_states = \<lambda>_. Structures_A.IRQInactive,
123    arch_state = init_arch_state,
124    exst = ext_init
125  \<rparr>"
126
127end
128end
129