# 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.