# Freestanding kernel and hosted mechanism checks.

EMU ?= $(or $(RAD_EMULATOR),emulator)

HOST_EMU ?= $(EMU)

COMPILER := ../bin/radiance.rv64.dev

COMPILE := $(HOST_EMU) -memory-size=385024 -data-size=348160 -stack-size=512 -run $(COMPILER)

MODULES :=

.PHONY: all check clean compiler-check

all: kernel.rv64

compiler-check:

$(COMPILER): compiler-check

	$(MAKE) -C .. RAD_EMULATOR=$(abspath $(shell command -v $(HOST_EMU)))

kernel.rv64: main.rad arch/entry.ras $(MODULES) $(COMPILER)

	$(COMPILE) -pkg kernel -start arch/entry.ras -mod main.rad $(addprefix -mod ,$(MODULES)) -o $@

check.rv64: check.rad $(MODULES) $(COMPILER)

	$(COMPILE) -pkg kernel -mod check.rad $(addprefix -mod ,$(MODULES)) -o $@

check: all check.rv64

	$(HOST_EMU) -run check.rv64

	$(EMU) -machine -no-guard-stack -max-steps=1000000 -count-instructions -run kernel.rv64

clean:

	rm -f kernel.rv64 check.rv64

# Kernel implementation decisions

The specification at https://radiant.computer/system/kernel takes precedence

for fixed call numbers, handle layout, rights, and object behavior. These notes

record the contracts established through step 1 of the 22-step plan.

## Source and trust boundary

- Kernel mechanisms use freestanding Radiance; RAS owns machine entry, register

  state, atomics, and MMIO. Hosted checks exercise the same mechanism modules.

  Make and shell provide build and verification plumbing.

- Use `Once` for explicit-consumption obligations and safe references for

  ordinary mutation. Raw addresses belong at platform and user-memory boundaries.

- Image loading is restricted to trusted binary RIL. Pointer-provenance and

  type-safety verification, including verifiable compiler output, are deferred.

  The compiler IL contains machine-word types and raw address operations; source

  compilation and structural decoding do not prove isolation from hostile code.

- All components that can change admitted executable bytes remain in the TCB,

  whether loading occurs inside or outside M-mode. Executable image code is

  immutable; writable image state is an instance resource.

- The reference machine uses RAD0 and the sibling emulator, not an assumed

  QEMU `virt` memory map. Emulator execution is not evidence of real-hardware

  cache behavior or timing bounds. Report instruction counts, not host timings.

## Validation

Use the current machine-capable sibling emulator. Set `RAD_EMULATOR`, pass

`EMU` to the kernel Make invocation, or put `emulator` on PATH. The kernel build

checks compiler dependencies. From the repository root, run:

```sh

make -C kernel check

```

The linked freestanding entry point and hosted runner must execute; an assertion failure must fail the check.

The entry probe uses explicit M-mode success/fault finish writes; secondary

harts idle. This checks machine entry, not user-domain execution. Finish writes

are a check protocol, not a domain-exit operation.

# Kernel implementation plan

Specification: https://radiant.computer/system/kernel.

This is a 22-commit progression from a freestanding entry point to budgeted

multicore domain execution. Each step is a signed, buildable commit with the

mechanism and emulator checks available at that boundary. NOTES.md records

only established contracts; this plan describes the full dependency order.

## Implementation boundary

- Use Radiance for kernel mechanisms and RAS for architectural entry, register

  state, atomics, and MMIO. Make and shell provide build plumbing. User-space

  scheduling and application policy are not kernel mechanisms.

- Load only trusted binary RIL through the Radiance compiler and shared RV64

  backend. Pointer-provenance and type-safety verification, including verifiable

  compiler output, are deferred from the outset. Encoding and structural checks

  do not provide isolation from hostile programs. Components able to change

  executable bytes remain in the TCB.

- Keep modules single-purpose, below 1,000 lines with a 500-line target. Keep

  kernel source below 10,000 non-comment lines. Do not duplicate native lowering.

- Compiler prerequisites occupy explicit dependency steps. No successful no-op

  stands in for an operation, and no test claims a later stage's behavior.

## Commit sequence

1. **Freestanding machine image.** Build the Radiance/RAS entry point, failure path, linked RAD0 image, and hosted mechanism-check runner. Execute the machine entry point.

2. **Bounded platform discovery.** Decode version-17 FDT data into RAM, reservations, hart topology, CLINT, PLIC, and device regions. Reject malformed and truncated descriptions.

3. **Physical frame ownership.** Allocate and clear contiguous frames, exclude reserved memory, and enforce exact range and exhaustion checks.

4. **Typed capability identities.** Define packed handles, object kinds, rights, slot generations, and retirement. Reject fabricated, stale, wrong-kind, and reserved-bit handles.

5. **Domains and startup authority.** Create bounded Pending domains with private handle tables and Events state. Establish non-ambient self authority and terminal-event reservations.

6. **Transactional capability operations.** Grant with attenuation, transfer atomically, and drop handles without inventing authority. Enforce Events locality and Interrupt exclusivity.

7. **Aligned aggregate code generation.** Preserve proven alignment in aggregate copies and exact-width register returns. Exercise machine boot and the compiler regression without changing layout.

8. **Persistent Page lifetimes.** Connect Page allocation and splitting to authority, object claims, and recipient-domain lifetime pins. Reclaim only after every claim and pin is gone.

9. **Ordered event publication.** Publish complete shared-ring entries with acquire/release ordering, validate consumer progress, reserve terminal delivery, and coalesce IRQ notifications.

10. **Architectural context boundary.** Save complete user register state on private machine frames, enter U-mode, return direct-call results, classify faults, and wake M-mode idle.

11. **Defining-module layout resolution.** Prepare a nominal type’s defining imports before resolving its layout. Reject by-value cycles and retain pointer recursion.

12. **Finite hart-bound budgets.** Implement conserved tick quantities, budget splitting and binding, incarnation-qualified context identities, exact-use accounting, and CLINT preemption.

13. **Waits and one-shot timeouts.** Retain accepted timeouts under event backpressure, validate waits, authorize wakeups, and choose timer deadlines without granting execution budget.

14. **Devices and external interrupts.** Validate bounded MMIO access and route exclusive interrupt ownership through masked PLIC claims, consumption, draining, and transfer.

15. **Bounded assembler storage and fences.** Size linking tables from name tokens and encode memory/I/O and instruction-fetch fences. Exercise assembler and compiler regressions.

16. **Binary RIL codec and standalone compilation.** Encode complete IL graphs in RIL0, validate binary structure, and compile decoded inputs through the existing RV64 backend. Keep provenance and type-safety verification deferred.

17. **Shared image catalogs and native execution.** Link ordered, namespaced image catalogs through the shared RV64 backend. Add typed user primitives, seven source-compiled binary images, private native state, and machine trap execution. Make and shell provide build plumbing.

18. **Complete image instances and contexts.** Create owned private image instances and activate complete argument/stack ranges. Add independent contexts, the instance workload, and checks for shared state within a domain and isolation between trusted instances.

19. **Lifecycle and reclamation.** Implement exit, faults, administrative destruction, creation-ancestry cascades, reparenting, and deferred reclamation after context quiescence. Preserve terminal reports and surviving Page recipients.

20. **Complete direct-call dispatch.** Validate every direct call and metadata query, including the budget/context additions and Delegate. Exercise authority, error returns, effects, and query error validation in hosted checks.

21. **Hart startup and bounded mailboxes.** Publish shared boot state, start private per-hart machine stacks, serialize kernel mutation with linear lock ownership, and exchange bounded requests through CLINT software interrupts. Exercise 1, 2, and 8 harts.

22. **Multicore runtime and complete boot.** Connect budgeted architectural owners, call effects, local continuations, remote admission, reserved Stop requests, and acknowledged teardown. Bootstrap real root authority and run control workloads on 1, 2, and 8 harts, including continued machine operation after root exit.

## Validation

From the repository root, set `RAD_EMULATOR` to the sibling emulator executable

and run `make -C kernel check` at every step. Compiler/backend steps also run

`make std-test bin-test` and their focused compiler or machine regressions.

NOTES.md identifies each step's observable checks and emulator prerequisites.

- Exercise the actual changed machine path when a step adds architectural

  behavior. Assertion failure must fail the check. Independent emulator changes

  are signed in the sibling repository; record required revisions in NOTES.md.

- Test authority, resource bounds, state transitions, ABI results, and concurrency

  invariants, not source spelling or wiring. Decode malformed binary encodings

  and exercise resource exhaustion, event backpressure, and finite budgets.

- Final checks cover all direct calls, native image state, 1/2/8-hart control

  workloads, acknowledged remote destruction, and root exit without shutdown.

  Check final module sizes and the signed, buildable 22-step sequence.

- The emulator supplies shared RAM and independent hart architectural state;

  machine U-mode/M-mode images cannot escape through hosted syscalls. Deterministic

  interleaving tests are not measurements of hardware cache behavior or timing.

  Instruction counts may describe a specific build, never establish isolation.

- The trusted binary-input requirement and deferred provenance/type-safety

  verification remain explicit in every validation claim.

// Machine entry with a boot-time trap sink.

.text;

	la     %t0    @bootFault;

	csrw   mtvec  %t0;

	csrr   %a0    mhartid;

	bnez   %a0    @bootIdle;

	call   @"::default";

	li     %t1    0x5555;

	j      @bootFinish;

@bootFault

	csrr   %t1    mcause;

	slli   %t1    %t1    16;

	li     %t0    0x3333;

	or     %t1    %t1    %t0;

@bootFinish

	li     %t0    0x10001000;

	sw     %t1    0(%t0);

@bootIdle

	wfi;

	j      @bootIdle;

//! Hosted entry for kernel mechanism checks.

/// Run the available kernel mechanism checks.

@default fn main() -> u32 {

    return 0;

}

//! Freestanding machine initialization.

/// Maximum online harts in this kernel build.

constant MAX_HARTS: u64 = 8;

/// Validate the entry hart before machine initialization.

@default fn main(hart: u64) -> u32 {

    assert hart < MAX_HARTS;

    return 0;

}