# RIL Verifiability: Proposed Lowerer and IL Changes

Based on `notes/ril-security-requirements.md`. The goal is to make RIL

statically verifiable for memory safety, supporting the exokernel's

trusted-domain guarantees.

## Current State

Today, RIL has four scalar types: `W8`, `W16`, `W32`, `W64`. Pointers are

`W64` -- indistinguishable from integers. Memory instructions (`Load`,

`Store`, `Blit`) take plain `Reg` operands as addresses. There is no

provenance tracking, no bounds information, and nothing preventing an

integer from being used as a memory base. The `lowerCast` / `ilType`

functions in the lowerer collapse `resolver::Type::Pointer` to `il::Type::W64`,

erasing pointer identity entirely.

---

## Phase 1: Pointer/Integer Type Distinction in IL

### 1.1 Add `Ptr` to `il::Type`

```

pub union Type {

    W8, W16, W32, W64,

    Ptr,        // New: pointer-width value with provenance

}

```

`Ptr` is the same physical width as `W64` but carries different semantic

meaning. The verifier treats them as incompatible types.

**Files:** `lib/std/lang/il.rad`

- Add `Ptr` variant to `Type`.

- Update `typeSize` to return 8 for `Ptr`.

### 1.2 Update `ilType` in the lowerer

Change the lowerer's `ilType` function so `resolver::Type::Pointer`,

`resolver::Type::Slice` (which contains a pointer), and

`resolver::Type::Fn` map to `il::Type::Ptr` instead of `il::Type::W64`.

**Files:** `lib/std/lang/lower.rad` (function `ilType`, ~line 6974)

### 1.3 Update the IL printer

Teach the IL printer to emit `ptr` for the new type variant.

**Files:** `lib/std/lang/il/printer.rad`

### 1.4 Update the backend

The RV64 backend (`isel.rad`, `emit.rad`) must treat `Ptr` identically to

`W64` for code generation -- same register class, same instructions. The

distinction is purely for the verifier, not for codegen.

**Files:** `lib/std/arch/rv64/isel.rad`, `lib/std/arch/rv64/emit.rad`

---

## Phase 2: Typed Memory Instruction Operands

### 2.1 Enforce pointer-typed bases on memory ops

Currently:

```

Load  { typ, dst: Reg, src: Reg, offset }

Store { typ, src: Val, dst: Reg, offset }

Blit  { dst: Reg, src: Reg, size: Val }

```

The `src`/`dst` address registers are untyped. A verifier pass should

reject any `Load`/`Store`/`Blit` whose base register was not defined by

a pointer-producing instruction.

This does NOT require changing the `Instr` union itself (registers are

untyped in the encoding). Instead, a **type map** is maintained:

each SSA register is assigned either a word type or `Ptr`. The verifier

checks that `Load.src`, `Store.dst`, and `Blit.{dst,src}` registers

have type `Ptr`.

### 2.2 Lowerer must produce consistently typed registers

Update the lowerer so that every register holding a pointer is produced by

a `Ptr`-typed instruction. Key sites:

- `emitReserve` -- `Reserve` produces a stack pointer: its result type

  should be recorded as `Ptr`.

- `emitDataAddr` / `emitFnAddr` -- `Copy` of a `DataSym` or `FnAddr`

  produces a `Ptr`.

- `emitLoad` for pointer-typed fields -- `Load` of a pointer field

  returns a `Ptr`-typed register.

- Address arithmetic (field offsets, array indexing via `BinOp::Add` on

  a pointer base) -- result is `Ptr`.

- `buildSliceValue` -- the pointer component is `Ptr`, the length/cap

  components are `W32`.

**Files:** `lib/std/lang/lower.rad` (many functions; grep for

`emitReserve`, `emitDataAddr`, `emitFnAddr`, `emitLoad`, `emitRead`,

`buildSliceValue`, `lowerIndex`, `lowerFieldAccess`)

---

## Phase 3: Restrict Integer-to-Pointer Conversion

### 3.1 Forbid `int as *T` in the lowerer

The lowerer's `lowerCast` currently delegates to `lowerNumericCast` for

all same-size casts, which is a no-op. For `int -> ptr`, it must instead

emit a dedicated **`IntToPtr`** IL instruction (or reject it outright).

Add to `il::Instr`:

```

IntToPtr { dst: Reg, val: Val },   // Explicit, auditable

PtrToInt { dst: Reg, val: Val },   // Pointer -> integer (one-way)

```

- `PtrToInt` produces a `W64`. The resulting integer CANNOT be fed back

  into memory ops.

- `IntToPtr` produces a `Ptr`. The verifier rejects this in user code;

  it is only permitted in `@trusted` functions (see Phase 5).

### 3.2 Update `lowerCast`

When source is an integer type and destination is `Pointer`, emit

`IntToPtr` instead of silently treating the value as compatible.

When source is `Pointer` and destination is an integer, emit `PtrToInt`.

**Files:** `lib/std/lang/lower.rad` (`lowerCast`, `lowerNumericCast`)

---

## Phase 4: Provenance-Producing Instructions

### 4.1 Define the closed set of pointer-producing operations

A verifier must be able to enumerate every instruction that can produce

a `Ptr`-typed result. The exhaustive list:

| Instruction       | Provenance source                        |

|--------------------|------------------------------------------|

| `Reserve`          | Stack allocation (local provenance)      |

| `Copy(DataSym)`    | Global/static data address               |

| `Copy(FnAddr)`     | Function address (code section)          |

| `Load` of ptr field| Derived from an existing pointer         |

| `BinOp::Add(ptr,i)`| Pointer arithmetic (derived)             |

| `Call` returning ptr| Callee-produced pointer                 |

| Block parameter    | Merges pointer values from predecessors  |

| `IntToPtr`         | Trusted-only escape hatch                |

Any other instruction producing a register used as a memory base is a

verifier error.

### 4.2 Pointer arithmetic constraints

When emitting `BinOp::Add` for pointer offset computation (field access,

array indexing), the lowerer should tag the result as `Ptr`. The verifier

checks:

- Exactly one operand is `Ptr`, the other is an integer.

- The result is `Ptr` with the same provenance as the pointer operand.

`BinOp::Sub` between two pointers produces an integer (`W64`), not a

pointer. This is the `ptr - ptr -> usize` pattern.

**Files:** `lib/std/lang/lower.rad` (field/index lowering),

`lib/std/lang/il.rad` (documentation)

---

## Phase 5: Trusted Boundary Annotation

### 5.1 Add `@trusted` function attribute

Functions that must perform raw address manipulation (syscall wrappers,

allocator internals, kernel glue) are annotated `@trusted`. The verifier

relaxes pointer-provenance checks inside `@trusted` functions but tracks

them as trust boundaries.

This requires:

- Scanner/parser support for the `@trusted` attribute.

- A `trusted: bool` field on `il::Fn`.

- The verifier skipping `IntToPtr` rejection inside trusted functions.

**Files:** `lib/std/lang/scanner.rad`, `lib/std/lang/parser.rad`,

`lib/std/lang/resolver.rad`, `lib/std/lang/lower.rad`, `lib/std/lang/il.rad`

### 5.2 Confine `ecall` to trusted functions

`Ecall` passes raw register values to the environment. A verifier should

require that `Ecall` only appears in `@trusted` functions, since the

syscall interface is an inherent trust boundary.

---

## Phase 6: Bounds Verification (Future)

The lowerer emits bounds checks as explicit IL (compare + branch to

trap). The verifier must prove that every memory access is covered by

a bounds check, without moving or inserting checks itself.

### Design Principle

Bounds checks stay in the lowerer. The lowerer has the most context

for optimization: it knows when a check is redundant (constant index

into a known-size array), when to hoist (loop over `0..len`), when

two accesses share one check. The verifier is purely an analysis

pass that confirms the lowerer's output is safe.

### 6.1 Static offsets (no CFG analysis needed)

Field access produces `add ptr %field %base <const>`. The verifier

tracks each `Ptr` register's allocation size (from `Reserve`).

For constant offsets: check `offset + access_size <= alloc_size`.

This covers record fields, tagged union payloads, slice header

fields -- the bulk of pointer derivations.

### 6.2 Dynamic offsets (requires dominance analysis)

Array/slice indexing produces:

```

load w32 %len %slice 8            ;; load length

br.ult %idx %len @ok @trap        ;; bounds check

@ok

mul w64 %off %idx %stride

add ptr %elem %base %off           ;; derive element pointer

```

The verifier must prove that the `add ptr` is dominated by a

`br.ult` that establishes `%idx < %len`, and that `%base` is

valid for `%len * %stride` bytes.

This requires:

1. **Dominator tree** -- computed from the block predecessor

   lists already in the IL. Standard algorithm, linear time.

2. **Bounds facts** -- at each `br.ult %a %b @pass @fail`, the

   verifier records that `%a < %b` holds on the @pass edge.

3. **Provenance table** -- each `Ptr` register carries

   `(origin, bound)` where origin is a `Reserve`/`DataSym`/

   parameter ID and bound is the allocation size or a register

   holding the dynamic length.

4. **Access check** -- for each `Load`/`Store`/`Blit`, verify

   that the base pointer's derived offset is covered by a

   dominating bounds fact against the same bound.

For a `Reserve { size: N }`, the bound is the constant `N`.

For a slice data pointer, the bound is `len * stride` where

`len` was loaded from the same slice header.

### 6.3 Provenance tracking

The verifier maintains a side-table mapping each `Ptr` register

to its provenance:

- **Origin**: which allocation or parameter it derives from.

- **Bound**: static size (for `Reserve`/globals) or the register

  holding the dynamic bound (for slice data pointers).

- **Offset**: accumulated constant offset from the origin base.

Derived pointers inherit their parent's provenance:

- `add ptr %dst %base <imm>` -- same origin, offset += imm.

- `add ptr %dst %base %dynoff` -- same origin, offset is dynamic

  (must be covered by a dominating bounds check).

### 6.4 Explicit region types (exokernel)

For the exokernel use case, extend the provenance model:

- `PagePtr(handle, offset)` -- pointer into a granted page.

- `DevicePtr(handle, offset)` -- pointer to a device mapping.

- `PortalPtr(handle, field)` -- pointer to a cross-domain portal.

These would be additional provenance classes that the kernel

verifier checks against the domain's capability set.

### Implementation cost

Dominance computation and dataflow tracking are standard SSA

algorithms. The main engineering work is connecting bounds facts

to pointer derivations across blocks. This is a substantial but

bounded effort -- probably 500-1000 lines of verifier code.

---

## Phase 7: Verifier Implementation

### 7.1 SSA type checker

Walk each function's blocks in order. Maintain a type map

`Reg -> Type` (where `Type` includes `Ptr`). For each instruction:

1. Record the destination register's type.

2. For `Load`/`Store`/`Blit`, check that the base register has type `Ptr`.

3. For `IntToPtr`, check that the function is `@trusted`.

4. For `BinOp` with a `Ptr` operand, check the arithmetic constraints.

### 7.2 Provenance checker (future)

Extend the type checker with provenance sets. Each `Ptr` register carries

a provenance tag. Derived pointers inherit their parent's tag. The

verifier rejects memory access through a pointer whose provenance is not

in the current domain's authorized set.

---

## Implementation Order

Recommended sequence, each step independently useful:

1. **Phase 1** (type distinction) -- smallest change, enables all later work.

2. **Phase 2** (typed memory ops) -- makes the lowerer provenance-aware.

3. **Phase 3** (cast restrictions) -- closes the int-to-ptr hole.

4. **Phase 7.1** (basic verifier) -- can now check real programs.

5. **Phase 5** (trusted boundaries) -- needed before restricting stdlib.

6. **Phase 4** (formalize pointer producers) -- refine verifier rules.

7. **Phase 6** (bounds/provenance) -- full exokernel support.

---

## Key Invariant

After all phases, the following must hold:

> Every `Load`, `Store`, or `Blit` instruction operates through a register

> of type `Ptr`, whose provenance traces back to an authorized allocation

> or grant, and whose derived offset is within the bounds of that

> allocation.

This is the RIL-level encoding of the exokernel's security guarantee.