Login
Phase 2: Organization and boot
Login

xv6 §2, "Operating system organization". "Thus an operating system must fulfill three requirements: multiplexing, isolation, and interaction."

Phase 2 takes the images Phase 1 built and boots them on firmware. Glint learns where it is and what machine it is on, shows that it can take the machine over from firmware, settles what it assumes about the code it will run, and ends by taking the machine over on every boot. Multiplexing, isolation and interaction all depend on how Glint is organized: a small privileged core, with Linux and Zephyr code behind seams (the Loose coupling point under The development text in PLAN.md). xv6 §2.3 gives the reason for keeping the core small: in a large monolithic kernel "no one developer understands all of the interactions between different parts of the code; this is a recipe for bugs."

The phase follows the course Run modes in the plan sets. It first leaves boot services only on request, with the shell's native command (2.6), as a demonstration. It then adds what every boot needs in order to leave them by default: the files it will use, loaded before the exit (2.9), and the switch itself (2.10). So Phase 3 starts from native mode, with hosted mode as the fallback.

The phase uses Track T's bin/glint-run, which boots an image under QEMU 11.1.2 and U-Boot 2026.07 and passes when an expected line appears on the serial console (rung 3 of the demonstration ladder in PLAN.md). Logic that can be tested without firmware is also checked at rung 1, in crystal spec, where spec/support/fake_efi.cr learns each new firmware call the phase makes. Each such call (SetWatchdogTimer, GetMemoryMap, ExitBootServices, AllocatePages) also gets its wrapper in Z.1's single boundary, c/efi_boundary.c and boot/efi_boundary.cr. Most slices land for aarch64 and x86_64 together. Two do not: the architectures describe their hardware differently (a devicetree on Arm, ACPI tables on x86) and take exceptions differently (a vector base register on Arm, a GDT and IDT on x86), so 2.4 and 2.7 split under rule 6. Track Z's Z.3 must land before 2.4a, and Z.9 before 2.5.

The boot's lines come in a fixed order, and every slice that prints says where its lines fall, so that the phase demo can check the order. Before the exit, through the firmware's console: Phase 1's greetings, then 2.2's privilege line, 2.3's memory map, 2.4's console line, 2.9's preload line, and 2.6's Mode: line when the boot stays hosted. After the exit, through Zephyr's UART: Left boot services, the final memory map's summary and Mode: native. The shell prompt comes last either way.

The slices below were refined when the phase started (rule 9). Every quoted passage was checked against xv6-riscv-book commit fa3b46bc43 and Hailperin's LaTeX source. Sizes are non-spec lines, as in rule 2.

Slices

2.1 Booting under firmware. This slice is met by Track T's T.11 (check-in ee3aec1c) and has no check-in of its own. bin/glint-run writes an ESP image with Cleave::Fat16 holding the Phase 1 image as EFI/BOOT/BOOTAA64.EFI or EFI/BOOT/BOOTX64.EFI and the files of spec/fixtures/esp/. It boots that disk headless under the project-built QEMU (virt for aarch64, q35 for x86_64) with the project-built U-Boot, whose standard boot finds and starts the image. The demonstration is spec/run/glint_run_spec.cr, which runs bin/glint-run aarch64 --expect "Hello from C via Glint" (and x86_64) and checks that "Hello from Glint" appeared first. Since Z.1, the same command proves the ELF-built images. xv6 §2.6 ("Code: Starting xv6, the first process and system call") walks through boot from the firmware's side first: "When the RISC-V computer powers on, it initializes itself and runs a boot loader which is stored in read-only memory." U-Boot is Glint's boot loader. It opens the phase because every later slice is shown on a booted machine, and it is the project's first rung-3 demonstration, which is Demonstrability moving from specs to firmware. Size: none.

2.2 Where am I. boot/privilege.cr reports the privilege level Glint was entered at. On aarch64 it reads CurrentEL and prints Entered at EL2 or Entered at EL1. On x86_64, where UEFI always enters in 64-bit mode at ring 0, the question that matters is whether the CPU offers AMD's SVM, so it reads CPUID leaf 0x80000001 (ECX bit 2) and prints Entered at ring 0, SVM available or Entered at ring 0, SVM not available. This is the boot's first line after Phase 1's greetings. The plan takes EL2 entry on the Beagle boards as documented but not yet confirmed (Run modes), so Glint reports the level rather than assuming it, and 2.6 reads the report. The slice also fixes the machines glint-run boots, so the report has something definite to show. QEMU's virt has virtualization off by default (hw/arm/virt.c sets vms->virt = false), so U-Boot, and Glint after it, would run at EL1; glint-run now boots aarch64 as -M virt,virtualization=on, which matches the boards. On x86_64 it passes -cpu EPYC, the model T.9 checked with query-cpu-model-expansion (svm=true). QEMU's default qemu64 also lists SVM under TCG (target/i386/cpu.c), but naming the model keeps the demonstration's CPU stated. A --no-virtualization option drops virtualization=on on aarch64 and passes -cpu EPYC,svm=off on x86_64, so the other answer is shown too. Right after the report, and on every boot, Glint turns off the five-minute watchdog that UEFI has firmware arm before it starts a boot option (U-Boot calls efi_set_watchdog(300) in lib/efi_loader/efi_helper.c), with SetWatchdogTimer(0, 0, 0, NULL). Otherwise a shell left idle would reset the machine five minutes into the first hosted boot. It is unconditional because every boot spends some time hosted, and a boot that leaves boot services loses nothing: U-Boot's ExitBootServices turns the watchdog off too. It prints nothing. A spec checks the wording from given register values, and that the fake table records exactly one SetWatchdogTimer call, with those arguments, before the shell first reads a key. On firmware, bin/glint-run aarch64 --expect "Entered at EL2" and bin/glint-run x86_64 --expect "SVM available" show the normal case, and --no-virtualization with --expect "Entered at EL1" (or "SVM not available") shows the other; 2.6 uses the same option to show that native mode does not need virtualization. It comes right after 2.1 because it needs only a booted image, and the watchdog must be off before any later slice leaves a booted Glint waiting. Reporting a fact instead of assuming it keeps the claim testable, which is Demonstrability. Its passage is xv6 §2.2 ("User mode, supervisor mode, and system calls"): "CPUs provide hardware support for strong isolation." Hailperin §7.3.1 states the principle the report checks: "the operating system needs to be privileged relative to the processes". About 110 lines.

2.3 The memory map. boot/memory_map.cr calls GetMemoryMap, keeps a copy and prints a summary, Memory map: N entries, M MiB usable (F MiB free now), followed by one line per descriptor (type, physical start, page count, attributes). These lines follow 2.2's privilege line. Usable means memory Glint may allocate once it owns the machine: EfiConventionalMemory, plus EfiBootServicesCode and EfiBootServicesData, which become free after ExitBootServices. Free now is EfiConventionalMemory alone, the only part a hosted Glint may touch. Usable is a promise for later, not for the moment of the exit: U-Boot marks its own code, stack and page tables EfiBootServicesCode (add_u_boot_and_runtime in lib/efi_loader/efi_memory.c), and Glint is still running on that stack until 2.6 switches to its own, and on those page tables until 3.2 loads Glint's own. Phase 3's allocator therefore hands out boot-services memory only after 3.2 (3.1 says how). There is no allocator yet, so the copy lives in a fixed 16 KiB buffer in the image, room for 409 of U-Boot's 40-byte descriptors; a map too large for it is reported and marked incomplete, not truncated. The parser steps through the map by the descriptor size the firmware returns, not by the size of Glint's own descriptor structure, since UEFI allows the two to differ. It is ordinary Crystal. The fake table learns GetMemoryMap, including its "buffer too small" answer. The fixtures in spec/fixtures/memory_map/ are recorded from the boot itself: each is the descriptor lines of a bin/glint-run log for one machine, saved with the QEMU and U-Boot versions in a header comment and re-recorded by hand when either pin changes. spec/memory_map_spec.cr rebuilds raw maps from them, at U-Boot's 40-byte stride and at a wider one, and checks the parser and the two totals. On firmware, bin/glint-run aarch64 --expect "Memory map:" (and x86_64) shows it, which is Demonstrability. Its passage is xv6 §2.1 ("Abstracting physical resources"): Unix processes do not handle physical memory directly, and "This allows the operating system to decide where to place a process in memory". Glint can make that decision only once it knows what memory exists. It must run while boot services exist, so it comes before 2.6, which reads the map once more, into the same buffer, as it leaves boot services; that final map is the one Phase 3 uses. About 150 lines.

2.4a Finding the hardware: the devicetree. xv6 needs no such step: "Xv6 is written for the support hardware simulated by qemu's '-machine virt' option" (xv6 §2), so its device addresses are built in. Glint is written for no one machine, so it reads the description firmware passes. This slice adds boot/config_table.cr, which searches the EFI configuration table by GUID, and boot/fdt.cr, which finds the console UART in a devicetree. On aarch64 virt, U-Boot passes on QEMU's own devicetree under the devicetree GUID. In it, /chosen has stdout-path = "/pl011@9000000", and that node has compatible = "arm,pl011", "arm,primecell", reg at 0x09000000 with size 0x1000, and SPI 1 as its interrupt (create_uart in hw/arm/virt.c). The reader follows stdout-path to the node and checks its compatible; it does not take the first UART in the tree, which QEMU's source warns only old software does. It keeps what it found (the compatible and the reg address) as 2.6's input, and prints Console: PL011 at 0x9000000 (devicetree) after the memory map. This reader is a second devicetree reader beside Cleave::Fdt, and that is deliberate. Inside the image there is no garbage collector and no full String or Hash, so Cleave::Fdt cannot run there; Build constraints in the plan allows exactly this, "a small allocation-free reader that is checked against Cleave::Fdt in specs". The reader only reads, allocates nothing, and is held to cleave by a spec that compares both on compat/zephyr/dts/qemu-virt.dtb, the devicetree Z.3 recorded from the project-built QEMU, which is why Z.3 lands first. If the kernel's prelude later grows enough for Cleave::Fdt, the second reader goes. The fake table learns a configuration table holding a devicetree. On firmware, bin/glint-run aarch64 --expect "Console: PL011" shows it. It comes before 2.6 because 2.6 compares this finding with the class the image was built for before firmware goes away, and before 2.4b because aarch64 leads (rule 6). One description-driven mechanism in place of board code (principle 6, No BSPs) is Parsimony in Tambassi's sense [39]. About 170 lines.

2.4b Finding the hardware: ACPI. On x86_64 q35, U-Boot builds with ACPI (GENERATE_ACPI_TABLE) and installs no devicetree. It copies the tables QEMU built (hw/i386/acpi-build.c) and installs them under the ACPI 2.0 GUID: FACS, DSDT, FADT, MADT, HPET, MCFG and WAET, reached from an RSDP that points to an RSDT, with no XSDT. None is a serial console table: QEMU builds an SPCR for Arm virt but not for x86. The UART appears only in the DSDT, as AML: a device COM1 with _HID PNP0501 and a _CRS naming I/O port 0x3F8 (8 ports) and IRQ 4 (serial_isa_build_aml in hw/char/serial-isa.c). This slice adds boot/acpi.cr, found through 2.4a's config_table.cr. Glint does not interpret AML. The reader checks the RSDP, RSDT, FADT and DSDT checksums, then looks in the DSDT for the PNP0501 EISA identifier and the I/O-port descriptor in the _CRS that follows it. If that search fails it uses the PC's standard COM1 port, 0x3F8, and says so. Like 2.4a it keeps its finding (PNP0501 and the port) for 2.6, and it prints Console: 16550 at port 0x3f8 (ACPI DSDT) after the memory map. Cleave has no ACPI reader, so there is nothing to compare against; spec/acpi_spec.cr builds small tables laid out as QEMU's sources produce them, including one with no COM1 device and one with a bad checksum. On firmware, bin/glint-run x86_64 --expect "Console: 16550" shows it. It follows 2.4a because it reuses the configuration-table search and shares nothing else with it. The passage is the other half of xv6's starting point: its kernel sits at 0x80000000 because "the address range 0x0:0x80000000 contains I/O devices" (§2.6), a fact xv6 knows in advance and Glint must look up. Keeping the reader to the two facts the console needs, with no AML interpreter, is Parsimony. About 190 lines.

2.5 Native mode's system table. Before Glint may leave boot services, it needs something to run on afterwards. This slice builds it, and nothing at boot reaches it yet. boot/native_table.cr builds a system table of Glint's own for use after the exit. It keeps the firmware's RuntimeServices pointer and its configuration tables (the devicetree or ACPI tables, which live in reserved memory). Its ConOut, StdErr and ConIn are Z.9's provider over Zephyr's UART, so input is a polled UART read, with bytes mapped to keys as Z.9 describes. In place of the firmware's boot services it has a table of Glint's own, and every entry in it is filled. LocateProtocol answers the console protocols and returns EFI_NOT_FOUND for everything else. Every other entry, ExitBootServices included, points to one stub that returns EFI_UNSUPPORTED. One stub serves every signature, since a function that ignores its arguments is safe to call with any of them under all three calling conventions, where the caller removes what it passed; on x86_64 the stub is declared ms_abi, like the firmware's functions. A stub is better than a null pointer: a call through a null entry faults with no message, while EFI_UNSUPPORTED is a status every Phase 1 caller already checks. Later slices fill entries as they gain providers, first 3.1's page allocation. boot/native_console.cr brings the console up after the exit: it runs Z.8's init runner on the console device and checks device_is_ready, returning the device's status, through Z.9's table, if not. It is the only code that initialises a Zephyr device, and it runs only after a successful ExitBootServices (2.6). It prints nothing of its own; 2.6's lines after the exit come through it. Every Phase 1 call site, the shell included, keeps working through the platform interface, and ls gets a clean "not found". It is demonstrated at rung 1: a spec builds the native table over Z.9's fake UART, runs Phase 1's scripted shell session through it, calls every boot-service entry and checks each answer, and runs the console bring-up against a fake UART whose init fails. At rung 2 both images link it, and its rung-3 evidence is 2.6's. It comes after Z.9, whose provider it installs, and before 2.6, so that 2.6 lands with a defined path after a successful exit. Swapping the firmware's console for a Zephyr driver behind the same protocols, with no call site changed, is Loose Coupling. Its passage is xv6 §2.1: "To achieve strong isolation it's helpful to forbid applications from directly accessing sensitive hardware resources, and instead to abstract the resources into services." After the exit Glint's own code still reaches the console only as a service. About 230 lines. That passes ~200 because a table with any entry left unfilled would not be safe to hand to Phase 1's callers.

2.6 Choosing the mode and leaving boot services. This is the phase's exit demonstration, and the one place where Glint decides whether to leave. boot/mode.cr makes the choice between hosted and native mode, always before ExitBootServices is attempted, because after a failed attempt hosted mode no longer exists. It is a plain function of what earlier slices found. Native requires a complete memory map (2.3) and a console that matches the class the image was built for (principle 6 in the plan): the console 2.4 found must have the address, or port, recorded beside the console device in Z.8's table, and a compatible of the same family (arm,pl011 or arm,sbsa-uart for the PL011 driver; ns16550, or the ACPI identifier PNP0501, for the NS16550 driver). The privilege level from 2.2 is reported beside the result, since native mode does not need virtualization. Before the exit, this comparison is all Glint does with the UART: the firmware still owns it, and Run modes in the plan forbids taking it over. The request in this phase is hosted unless the shell's new native command asks for native. glint-run gains a repeatable --type LINE option that types each line into the serial console after a glint> prompt. The Mode: line is printed once per boot, as the decision's outcome. A hosted outcome prints it through the firmware's console: at boot as the last line before the first prompt, Mode: hosted (default), and when native is refused, with the reason, for example Mode: hosted (console differs from build class: arm,pl011 at 0x9040000). A native outcome prints it through Zephyr's UART after the exit. boot/exit.cr leaves boot services: it reads the map into 2.3's buffer, calls nothing else (any boot-service call may change the map), and calls ExitBootServices with the new map key, retrying once with a fresh map if the key has gone stale, as UEFI allows. That map is the final one, the map Glint now owns. On success, Glint first moves off the firmware's stack, which lies in memory 2.3 counts as usable, onto a 64 KiB stack in its own image, aligned to a page and with an unused page below it, which 3.3 turns into a guard page. xv6 starts the same way: "The instructions at _entry set up a stack so that xv6 can run C code" (§2.6). It then switches to 2.5's table and brings up Zephyr's console, which prints Left boot services, the final map's summary in 2.3's format, and Mode: native, before the prompt returns. If the exit fails twice, or the console does not come up after it, the firmware's console can no longer be trusted, and UEFI leaves only GetMemoryMap and ExitBootServices safe to call. Glint then writes ExitBootServices failed: <status> (or Zephyr console failed: <status>) through the Zephyr driver's poll_out on the UART as firmware left it, without running the driver's init, and halts with interrupts masked (wfi or hlt in a loop). That is safe for both drivers on these machines. With CONFIG_MMU unset, poll_out reads only the device's constant configuration, whose address or port needs no init, and for the NS16550 a spinlock in zeroed data. It writes the data register without reprogramming the UART, so the bytes go out at the rate firmware set. Under U-Boot a stale key is refused before any device is touched (efi_exit_boot_services in lib/efi_loader/efi_boottime.c checks the key first), so the UART is as it was. Firmware that switched the UART off before failing would leave poll_out waiting on a full FIFO: a hang, not corruption, which 13.2–13.3 check on the boards. spec/mode_spec.cr checks every combination of findings and request, including a console at another address and a PL011 against an NS16550 build; that the hosted path leaves the watchdog as 2.2 set it, meaning the fake table shows one SetWatchdogTimer(0, 0, 0, NULL) before the first prompt and the mode choice adds none; that a successful exit calls GetMemoryMap and then ExitBootServices with that map's key and nothing between; and, with a fake table that rejects the exit twice, that only GetMemoryMap and ExitBootServices are called after the first failure, that the report reaches Z.9's fake UART although init never ran, and that the halt is reached. On firmware, bin/glint-run aarch64 --expect "Mode: hosted (default)", bin/glint-run aarch64 --type native --expect "Mode: native" and the latter with --no-virtualization (and each for x86_64) show the three ordinary outcomes, and the second checks that Left boot services and the map summary come before Mode: native. Later slices add inputs to this decision, never a second decision point: 2.9's preload result, 2.10's request file and 4.3a's hypervisor mode. It comes after 2.2–2.5, which supply its inputs and the table it switches to. One decision point, rather than mode checks scattered through the code, means the choice to leave, and what happens when leaving fails, is made in one file, which is Parsimony. Its passages are xv6 §2.1, on the alternative to a kernel that isolates: "The downside of this library approach is that, if there is more than one application running, the applications must be well-behaved." Hosted mode is Glint running as a library on the firmware, acceptable only while Glint is the only program running. And xv6 §2.3 ("Kernel organization"): "A key design question is what part of the operating system should run in supervisor mode." From the exit on, the answer excludes firmware: only code linked into Glint, Glint's own or Zephyr's, drives a device. About 280 lines. That passes ~200 because a decision with no exit to act on, or an exit with no decision guarding it, would land a path that leaves Glint unseen.

2.7a Panic, and the Arm vectors. boot/panic.cr adds a panic path for Glint's own failed checks: it prints the message through whatever console the system table holds (the firmware's in hosted mode, Zephyr's in native mode) and halts, and it takes over 2.6's halt. Once Glint is in native mode, boot/vectors_aarch64.cr and a 2 KiB vector table install in VBAR_EL2 or VBAR_EL1, whichever level 2.2 reported; 2.6's exit installs them right after the stack switch. They report any unexpected exception through the same path. The report gives the exception class from ESR, the ESR value, ELR (the address of the instruction that faulted), the general registers and SP. FAR is printed only for the classes that set it, chiefly instruction and data aborts. For an undefined instruction the faulting address is ELR. The shell gains a fault command, which in native mode prints the address of its udf #0, as fault: udf at 0x<address>, and then executes it, so the report's ELR can be checked against a number printed beforehand. In hosted mode the firmware owns the vectors, and an undefined instruction would reach U-Boot's own handler, which reports in its own words and then resets the CPU (arch/arm/lib/interrupts_64.c; on x86 it hangs). So the command refuses: fault: native mode only (firmware owns the exception vectors). A spec checks the report's format from given register values, and that fault refuses in hosted mode. On firmware, bin/glint-run aarch64 --type native --type fault --expect "Panic: undefined instruction" shows it, and the spec behind it checks that ELR equals the address fault printed. It comes before Phase 3 because 3.3's guard-page demonstration needs a fault to be reported; Phase 4 (4.1) later replaces these vectors with full trap handling. xv6 §2.7 assumes kernel code is written "to be bug-free"; a panic is the evidence when that assumption fails, which is Demonstrability. The same section says why halting is right: "Panicking is not desirable, but is preferable to continuing execution." About 230 lines, over ~200 because the vector table shows nothing without the report it calls.

2.7b The x86 vectors. On x86_64 the same report needs a GDT and an IDT of Glint's own. The firmware's GDT lives in boot-services memory, which 2.3 counts as usable, and IDT entries must name a code segment Glint controls. boot/vectors_x86_64.cr and its stubs load both, from 2.6's exit right after the stack switch, so the firmware's GDT is out of use before Phase 3 hands that memory out. They fill the 32 exception vectors; each stub pushes the vector and, for vectors the CPU gives none, a zero error code, so one handler serves all 32. The report gives the vector, the error code, RIP (the faulting instruction, which is the faulting address for an invalid opcode, vector 6) and the general registers. CR2 is printed only for a page fault (vector 14). fault prints fault: ud2 at 0x<address> and then executes ud2, and refuses in hosted mode as on Arm. A spec checks the format, and bin/glint-run x86_64 --type native --type fault --expect "Panic: invalid opcode" shows it on firmware, with RIP checked against the printed address. It follows 2.7a because aarch64 leads, and it is separate because a vector base register and a descriptor-table pair share no code; only 2.7a's panic path is shared. Its passage is xv6 §2.7, on what a panic is for: "A kernel developer would react to a panic by working to identify and fix the underlying code bug." That needs the right address. Reporting it for each kind of fault, rather than a register that may hold a stale value, is Clarity. About 210 lines.

2.7c Overflow is a panic. A small addendum, found while Phase 3 was refined. Crystal checks integer arithmetic, and on overflow it calls __crystal_raise_overflow. In the image that function, in prelude/efi.cr, is an endless loop, so an overflow in Glint's own code hangs the machine without a word, which is exactly the silent failure 2.7 exists to prevent. This slice makes it call 2.7's panic with Panic: arithmetic overflow and the address it was called from, in both modes, through whatever console the system table holds. The shell's fault command takes an optional argument, and fault "overflow" performs a checked addition that overflows, so the path can be shown. At rung 3, bin/glint-run aarch64 --type 'fault "overflow"' --expect "Panic: arithmetic overflow" (and x86_64) shows it, in native mode and with --mode hosted. Its passage is the one 2.7a cites, xv6 §2.7: "Panicking is not desirable, but is preferable to continuing execution." A hang is neither. It comes after 2.7b because it uses both architectures' panic path, and before Phase 3, whose address arithmetic is the first large body of code where an overflow is plausible. Turning a silent hang into a report is Demonstrability. About 30 lines.

2.8 The threat model. docs/threat-model.md states what Glint assumes about guests and about itself, adapting xv6 §2.7 ("Security Model") with guest in place of process: "The operating system must assume that a process's user-level code will do its best to wreck the kernel or other processes." xv6 lists what such code may try: bad pointers, instructions not meant for it, control registers, device hardware and clever system-call arguments. The document names, for each, the guest's equivalent and the slice where Glint stops it. It also states what Glint assumes about itself, about firmware, about Zephyr code linked into it, about the files it loads from the ESP, and about devices that can write memory by DMA without an IOMMU (Devices and the Linux guest in the plan). Its structure is fixed so that a spec can read it: one ## heading per subject (## Guests, ## Glint, ## Firmware, ## Zephyr code, ## ESP files, ## DMA), and under each, one top-level bullet per assumption. Every bullet ends with the slices that enforce or test it, in parentheses, comma-separated, as in (4.5) or (Z.9, 3.3): a phase number or track letter, a dot, and a slice number with an optional letter, such as 2.7a. Nothing follows the closing parenthesis but the end of the bullet. The demonstration is spec/threat_model_spec.cr at rung 1: it checks that every bullet ends in that pattern, and that each named slice appears as a bold slice heading (**4.5) in a phase or track document under docs/phases/. It comes after 2.7 because two of its assumptions about Glint itself are answered there: that its own code is bug-free is checked by 2.7's panic, and what it trusts of firmware and of Zephyr code is settled by 2.5–2.7, which decide what still runs after the exit. It comes before 2.9, the first slice that carries outside data, the ESP's files and later guest images, across the exit, so what Glint assumes about that data is written first. It must also precede every argument check in Phase 4 (4.5) and every pass-through decision in Phase 10, which are judged against it. Stating the boundary explicitly, so later code can be checked against it, is Clarity. About 120 lines of document and 40 of spec.

2.9a Loading before the exit. After the exit, firmware can no longer read the disk, and Glint has no storage driver of its own until Phase 6. So whatever a native Glint will read must be in memory first. When native mode is requested, boot/preload.cr reads every regular file in the ESP's root directory, through Phase 1's file protocol, into pages it allocates with AllocatePages as EfiLoaderData. The memory map lists those pages as the loader's, so neither the exit nor Phase 3's allocator frees them, and they are Glint's own memory from then on. It records each file's name, address and size in a fixed table in the image, as 2.3 does for the map, and prints Preloaded N files, K KiB after the console line. Because 2.6 reads the final map only after this, the map records the preload's pages. A failed preload (a file too large for memory, or the table full) is one more input to 2.6's decision, and the boot stays hosted with the reason, for example Mode: hosted (preload failed: Image: EFI_OUT_OF_RESOURCES). The fake table learns AllocatePages, and spec/preload_spec.cr preloads spec/fixtures/esp/ through it and checks the table against the fixture's files. On firmware, bin/glint-run aarch64 --type native --expect "Preloaded" (and x86_64) shows the count, and the final map has the preload's EfiLoaderData entry. Its passage is xv6 §2.6: "The boot loader copies the xv6 kernel into memory at physical address 0x80000000." Before the exit Glint acts as its own boot loader, for everything that must outlive firmware. It belongs late in Phase 2, not at the start of Phase 3: it is part of how a boot hands the machine over, it needs only Phase 1's file protocol and 2.6's exit, and Phase 3 opens with an allocator whose input, the final map, must already include the preload. It comes after 2.8, which states what Glint assumes about these files, and before 2.10, since a boot that left by default without it would cut Glint off from its files. Copying only what is needed, once, before firmware goes, is Parsimony. About 190 lines; 2.9 was split in two by rule 3 when one check-in came to about 490.

2.9b Serving the loaded files. After the exit, boot/preload_fs.cr serves 2.9a's files, read-only, as SIMPLE_FILE_SYSTEM from 2.5's table, whose LocateProtocol now answers that protocol too. OpenVolume gives the root; Open finds a file by name, Read returns its bytes, or, on the root, the EFI_FILE_INFO records ls reads; Write and the rest refuse. On x86_64 every entry has an ms_abi wrapper, as 2.5's console has. So ls and cat work unchanged after the exit, and Phase 3 (3.6) finds a guest image the same way. spec/preload_spec.cr checks that EfiFile reads the same bytes from the preload provider as from the fake firmware, and that ls lists the same names through the native table after a fake exit. On firmware, bin/glint-run aarch64 --type native --type ls --type .cat "hello.txt". --expect "Hello from the ESP!" (and x86_64) reads a file after the exit. Its passage is xv6 §2.1: Unix applications "interact with storage only through the file system's open, read, write, and close system calls". After the exit Glint's own shell still reaches its files only through that protocol. It follows 2.9a, whose table it serves. Serving loaded files behind the same protocol the firmware served, so no caller changes, is Loose Coupling. About 200 lines.

2.10 Native by default. From this slice on, every boot first loads what it needs (2.9), then leaves boot services and runs native, and hosted mode is the fallback, as Run modes in the plan states. This is the one slice that changes the default. In boot/mode.cr the default request becomes native. A boot can still ask for another mode: before deciding, 2.6's decision reads the ESP file glint-mode.txt, whose one word is hosted or native (4.3a adds hypervisor), and glint-run gains --mode MODE, which writes it. A word the decision does not know keeps the boot hosted, with the reason. A hosted boot prints Mode: hosted (requested), and the native command still leaves from it, as the demonstration 2.6 built. No new lines are printed: a default boot simply runs on, after the console line and the preload line, through the exit to Left boot services, the final map and Mode: native. A spec extends spec/mode_spec.cr with the request file: absent, each word, and an unknown word. On firmware, bin/glint-run aarch64 --expect "Mode: native" (and x86_64) boots native with nothing typed, and --mode hosted --expect "Mode: hosted (requested)" shows the fallback. Its passage is the end of xv6's boot walk-through in §2.6: "Then it starts a shell on the console. The system is up." It closes the phase because it needs everything before it: the decision and exit (2.6), the vectors (2.7), the written assumptions (2.8) and the preload (2.9). From here, native boots do everything hosted ones did in Phases 1 and 2. Phase 3 needs it, since it takes over the MMU, which firmware owns until the exit. Stating the default in one place, so every later demonstration runs native with no typed step, is Clarity. About 60 lines.

Phase demo: on both architectures under QEMU and U-Boot, Glint boots, reports its privilege level, memory map and console, preloads its files, leaves boot services by default, keeps its console through Zephyr's UART driver, and panics cleanly on a deliberate fault at the address it printed. Asked to stay hosted, it does, and its native command still leaves.

The demo is spec/run/phase2_spec.cr, which needs QEMU_SRC, UBOOT_SRC and ZEPHYR_SRC. For each architecture it makes three runs and checks each log's order against the order stated at the top of this document; it does not try to tell which driver wrote a line. The first run, bin/glint-run aarch64 --type fault --expect "Panic: undefined instruction" (on x86_64, "Panic: invalid opcode"), checks for Entered at EL2 (or Entered at ring 0, SVM available), the Memory map: summary, the Console: line and the Preloaded line, then Left boot services, a second Memory map: summary and Mode: native, then fault: udf at (or ud2 at) an address, and the panic, whose ELR (or RIP) equals that address. The fault typed after the exit is read through Zephyr's driver, so the run shows console input as well as output. The second, --mode hosted --type native --type 'cat "hello.txt"', checks Mode: hosted (requested) before the first prompt, then, after the typed native, the preload line, Left boot services and Mode: native, and finally the file's contents read after the exit. The third, --no-virtualization --expect "Mode: native", checks that it follows Entered at EL1 (or SVM not available): native mode does not need virtualization.

References