# RIL Safety Verification

## Done

### Ptr type (Phase 1-2)

`il::Type::Ptr` distinct from `W64`. All memory ops use `Ptr` for base

registers. Loads/stores of pointer values use `Ptr` as the type.

Backend treats `Ptr` identically to `W64` for codegen.

### Explicit casts (Phase 3)

`MakePtr` (`ptr`) makes integer-to-pointer crossings explicit.

Pointer-to-integer is a safe demotion (no instruction needed).

### Provenance rules (Phase 4)

Closed set of pointer-producing instructions documented in `il.rad`:

Reserve, Copy(DataSym/FnAddr), Load with Ptr type, Elem, BinOp::Add

on Ptr, Call returning Ptr, block params, MakePtr. Pointer-to-integer

flows are safe and need no dedicated instruction.

### unsafe keyword (Phase 5)

`unsafe fn` and `unsafe { }` blocks. Integer-to-pointer casts

(`addr as *T`) only allowed in unsafe context. Resolver enforces.

### Elem instruction (Phase 6 partial)

Bounds-checked element pointer: `elem %dst %base %idx %len stride`.

Backend lowers to `bltu + ebreak + mul + add`. Verifier checks

locally without CFG analysis. Used for all user-facing array/slice

indexing, for-loop iteration, append, delete, fill, byte copy.

### Verifier (Phase 7)

SSA type checker in `il/verify.rad`. Tracks `Ptr(bound)` per register.

Checks:

- Memory op bases are Ptr

- Static offset access within allocation bounds

- Elem base is Ptr, result is Ptr(stride)

- MakePtr counted as provenance escape

## Remaining gaps

### Slice re-slicing uses unchecked `add ptr`

`&slice[start..end]` offsets the data pointer via `add ptr` with no

bounds check. This is safe in practice because the resulting pointer

is only used as a slice data pointer — all access goes through `Elem`.

But untrusted IL could forge a slice pointing anywhere by constructing

an `add ptr` with an arbitrary offset, then wrapping it in a slice

struct.

### Constant-index array access uses unchecked `add ptr`

When the resolver validates a constant array index at compile time,

the lowerer emits plain `add ptr`. The verifier checks this statically

against the allocation bound from `Reserve`. This is sound for known

allocations but `Ptr(0)` (unknown bound) skips the check.

### Pointers from memory/params/calls have unknown bounds

`load ptr`, function parameters, and call return values produce

`Ptr(0)`. The verifier can't check accesses through them. All

indexing goes through `Elem` which bounds-checks at runtime.

---

## Future: First-class slices in IL

The current model relies on runtime bounds checking (`Elem`) as the

last line of defense. Every element access is checked, so forging a

slice can't access arbitrary memory — the worst case is a bounds-check

trap. This is the WebAssembly model.

For static verification (proving at load time that no trap can occur),

slices need to be a first-class IL concept:

```

SliceNew  %slice %base %len %cap %stride   ;; construct from known alloc

SlicePtr  %ptr %slice                       ;; extract data pointer

SliceLen  %len %slice                       ;; extract length

SliceElem %ptr %slice %idx                  ;; bounds-checked element

```

### Why this helps

`SliceNew` is the only way to construct a slice. The verifier checks

that `%base` is `Ptr(B)` and `len * stride <= B` -- the allocation is

large enough for the claimed length. After construction, `SliceElem`

is provably safe because the length was validated against the

allocation.

An attacker can't forge a `(ptr, len)` pair by storing to memory --

the only path to a slice value is `SliceNew`, which the verifier

validates.

### What it costs

- Slices stop being plain `{ptr, len, cap}` memory layouts. They

  become opaque IL values.

- Every slice operation becomes a dedicated instruction.

- The lowerer must emit `SliceNew` instead of manual stores.

- Re-slicing becomes `SliceSlice %new %old %start %end` with the

  verifier checking `start <= end <= old.len`.

- More complex IL, simpler verifier.

### Trade-off

With `Elem` on every access, the current model is already safe against

memory corruption -- the worst outcome of a forged slice is a trap.

First-class slices would additionally prove no trap can occur, enabling

trap-free execution in verified domains.

Whether this is needed depends on the exokernel's requirements:

- If domains are allowed to trap (and the kernel handles it), the

  current model is sufficient.

- If domains must be proven trap-free, first-class slices are needed.

---

## Future: Global data bounds

`Copy(DataSym)` currently produces `Ptr(0)`. The verifier could look

up the `Data` entry in `Program.data` to get the size and produce

`Ptr(size)`. Straightforward extension, not yet implemented.

## Future: Exokernel region types

`PagePtr(handle, offset)`, `DevicePtr(handle, offset)`, etc. as

provenance classes checked against the domain's capability set.

Needs the exokernel's capability model to be defined first.