KernRift | Documentation

1. Types & Variables

KernRift targets bare-metal x86-64 and ARM64. The type precedes the name (C-style).

Type	Width	Description
`uint8` / `u8`	1 B	Unsigned byte.
`uint32` / `u32`	4 B	Unsigned 32-bit integer.
`uint64` / `addr`	8 B	Unsigned 64-bit, pointer-sized.
`bool`	1 B	Boolean (`true` / `false`).
`[T]`	16 B	Slice. A fat pointer (ptr, len). No hidden allocations.

uint32 status = UART0.Status
uint8  byte   = 0xFF
bool   ready  = false

// Constants are inlined at every use site
const uint32 UART_ENABLE = 0x0001

2. Control Flow

KernRift supports standard control flow structures with no implicit returns.

If / Else

Conditions are full expressions. Parentheses are optional.

if status == 0 {
    uint32 x = 1
} else {
    uint32 x = 2
}

Loops

Supports while loops and range-based for loops.

while i < n {
    i += 1
}

// Exclusive range
for i in 0..10 {
    total += i
}

3. Structs and Enums

Data layout is C-style packed. Field offsets are compile-time constants.

struct UartRegs {
    Control: uint32,   // offset 0
    Status:  uint32,   // offset 4
    Data:    uint8,    // offset 8
}

enum UartBase: uint64 {
    Uart0 = 0x40000000,
    Uart1 = 0x40001000,
}

4. Hardware Access (MMIO)

To safely interface with hardware, use the device block. This maps physical registers to typed, volatile-safe memory accesses. Requires the @module_caps(Mmio) capability.

@module_caps(Mmio)

device UART0 at 0x3F000000 {
    Data   at 0x00 : uint8  rw
    Status at 0x04 : uint32 ro
}

fn read_status() -> uint32 {
    // The compiler emits a volatile load instruction
    return UART0.Status 
}

5. Kernel Safety Annotations

Annotations appear immediately before functions and dictate physical hardware constraints. Invalid call edges (e.g., calling an allocator from an interrupt) are rejected at compile time.

Execution Contexts: `@ctx(...)`

thread: Normal thread / task context.
boot: Early boot, before scheduling is active.
irq: Hardware interrupt handler.
nmi: Non-maskable interrupt (strictest).

Side Effects: `@eff(...)`

Mmio: Performs memory-mapped I/O.
alloc: Allocates memory (strictly forbidden in irq).
block: May put the thread to sleep.

// This function is verified to never yield or block
@noyield
@ctx(irq)
fn irq_handler() { 
    // Handle hardware interrupt safely
}

6. Advanced Kernel Primitives

Tail Calls

A tail_call(callee, args) intrinsic discards the current stack frame before jumping. This guarantees zero stack growth, making it the only mathematically safe way to implement infinite polling loops inside fixed-stack @ctx(irq) handlers.

Per-CPU Variables

Native support for SMP architecture. Declaring a percpu variable automatically compiles down to a %gs or %fs relative address access.

percpu cpu_active_tasks: uint32

fn log_task() {
    percpu_write<uint32>(cpu_active_tasks, 0x01)
}

Physical Code Shaping

Add @hotpath to a function, and the compiler mathematically computes its entry offset and injects 0x90 NOPs into the binary to achieve perfect 16-byte alignment, completely eradicating Instruction-Cache misses.

7. Cryptographic Verification & Artifacts

To prevent supply chain attacks and guarantee semantic integrity, KernRift emits strict JSON contracts that can be cryptographically hashed and signed using Ed25519.

Emitting Contracts

Generate the semantic contract alongside the binary, and sign it with a private key:

$ kernriftc check --contracts-out contracts.json \
    --hash-out contracts.sha256 \
    --sign-ed25519 secret.hex \
    --sig-out contracts.sig driver.kr

Verifying Contracts

In the CI pipeline or loader, verify that the artifact exactly matches the signed JSON schema:

$ kernriftc verify --contracts contracts.json \
    --hash contracts.sha256 \
    --sig contracts.sig \
    --pubkey pubkey.hex