Miri for Agents

---
name: miri-lang
description: Writing Miri source files — syntax, type system, and iteration workflow
---

# Miri Language Essentials

The short core for writing `.mi` files: how Miri differs from Python and Rust,
the traps that cost earlier agents the most, and the one check → fix → test
loop. Everything else is a lookup, not a read: ask the compiler (see *Looking
things up*) rather than guessing a name.

## Core Syntax

Indentation-sensitive blocks; a `:` puts a one-line body on the header line.

```miri
use system.collections.list
use system.collections.map

struct Point
    x int
    y int

enum Color
    Red
    Blue

trait Drawable
    fn draw()

class Circle implements Drawable
    fn draw(): println("circle")

fn add(a int, b int) int
    a + b

fn main()
    let x int = 5
    var y = 10
    y = add(x, y)
    let p = Point(3, 4)
    var words = Map<String, int>()
    words["a"] = 1
    let items = List([1, 2, 3])
    for item in items
        if item > 1 and not (item == 3): println(f"{item} {p.x}")
    match Color.Red
        Color.Red: println("red")
        Color.Blue: println("blue")
    match Result.Ok(y)
        Result.Ok(v): println(f"ok {v}")
        Result.Err: println("err")
    let maybe int? = words.get("a")
    match maybe
        Some(v) if v > 0: println(f"some {v}")
        Some(_) | None: println("none")
```

## Where Miri Differs

- Bindings are `let` (immutable) and `var` (mutable); there is no `let mut`.
  Parameters are immutable too; mutate a collection argument with `.set(i, v)`.
- Types follow the name with a space: `let x int = 5`, `fn f(a int) int`. No `:`
  before a type, no `->`, no literal suffixes (`42i32`); cast with `as`.
- Logic is `and`, `or`, `not`. Nullable is `T?` with bare `Some`/`None`;
  `Result` patterns need the prefix: `Result.Ok(v)`, `Result.Err`.
- `List([1, 2])` builds from a literal, `List<int>()` is empty, `Map<K, V>()` and
  `Set<T>()` likewise. `[1, 2, 3]` alone is a fixed `Array`; `{}` is a `Map`.
- A `for` over a `Map` walks its keys; there is no `.keys()`.
- An f-string is the only int → String conversion: `f"{n}"`, never `n.to_string()`
  or `"n=" + n`.
- `main() int` returns an exit status; `panic(message)` stops with status 1.
  There is no `exit`.
- Stdlib modules are imported by name (`use system.collections.list`).

```miri,fails=MER_PAR_001,expects-message=Expected an expression, but found :
let x: int = 5
```

```miri,fails=MER_TYP_038,expects-message=Expected enum variant pattern like Result.Ok
fn main()
    match Result.Ok(5)
        Ok(x): x
        Err: 0
```

```miri,fails=MER_TYP_036,expects-message=Cannot instantiate generic class 'List<T>' without explicit type arguments
use system.collections.list

fn main()
    let l = List()
```

## Traps

- **Quotes inside f-string braces** must be the other quote character:
  `f"{m['a']}"`. The same quote ends the string (MER_LEX_012).
- **Positions count characters**, in `length()`, `substring`, `element_at`,
  `code_at` and regex matches alike; only `size()` counts bytes. A `substring`
  range outside the text stops the program (or fails to compile, if constant).
- **Integer overflow stops the program** (`MER_RT_003`) instead of wrapping.
  Where wrapping is meant — a hash, a checksum — write `wrapping_add`,
  `wrapping_sub` or `wrapping_mul` from `system.math`.
- **Walk with `for`, not by position.** `for ch in s` and `for k in m` are one
  pass; indexing a `String`, `Map` or `Set` by a counter repeats lookups.
- **Every statement lives in a function.** A statement beside `main` never runs
  and is refused (MER_TYP_069); put the script's body inside `main`.
- **Integer widths do not convert implicitly.** An `int` value stored into an
  `i32`/`u32` slot, element or field needs `as i32`; the same holds between
  `float` and `f32`. `miri fix --apply` writes the cast.
- **Format specs follow Python**: `f"{x:.2f}"`, `f"{n:>8}"`, `f"{n:08x}"`. A
  precision needs `f` (`{x:.2}` is refused); `x`/`b`/`o` take integers only.
- **Imports are explicit.** A name from another module needs its `use` line;
  `miri fix main.mi --apply --yes` adds one that resolves in exactly one module.

## Looking things up

Ask before guessing a member, a module or a signature. These are cheap and exact:

- `miri view --type String --public` lists what can be called on a type,
  inherited and trait-supplied members included (`List`, `Map`, `int` alike).
- `miri view system.io --outline --public` lists what a module offers; try
  `system.fs`, `system.os`, `system.collections.map` the same way.
- `miri view system.fs --fn read_file` prints one function.
- `miri view --stdlib-root` prints the stdlib roots searched; set
  `MIRI_STDLIB_PATH` when the binary is not beside its `stdlib/`.
- `miri explain MER_TYP_033` describes the rule behind a diagnostic code.

The `miri-testing` pack covers `miri test`; the `miri-gpu` pack covers kernels.

## Verification Loop

This is the one loop the compiler's documentation recommends; everything else defers to it. **Loop:** `miri check --format json` → edit → `miri test` (or `miri run`). Iterate until clean.

1. **miri check** — `miri check myfile.mi --format json`. Each diagnostic has a `code`, a `help` and, where one exists, a `repair` with its edits. A diagnostic without a `repair` is one you edit yourself.
2. **Edit** — `miri fix myfile.mi --apply --yes` writes every recorded repair in one call. Everything else is an ordinary edit; in a file already in canonical layout, `miri patch myfile.mi --replace-in-fn name --old text --new text` makes a scoped edit and re-checks before anything reaches disk.
3. **miri test** / **miri run** — `miri test --dir <DIR>`, `miri run myfile.mi`; both take `--format json`. Only a run finds a fault the frontend cannot see.

The auto-applicable repairs are:
- `add-import`: Import a name that resolves in exactly one module.
- `arrow-return-type`: Drop the `->` before a return type.
- `cast-to-slot-type`: Convert a number with `as` to the width of the place it is stored; a value outside that width's range is truncated or rounded.
- `colon-annotation`: Drop the `:` before a type annotation.
- `concat-to-formatted-string`: Rewrite a `+` chain joining text to values as one f-string.
- `drop-extra-arguments`: Drop positional arguments a call does not declare.
- `drop-iterator-accessor`: Drop a `keys` accessor on a keyed collection and iterate it directly.
- `if-colon`: Write `:` in place of `then`, or after an inline `else`.
- `interpolation-quotes`: Write the string literals inside an f-string's braces with the other quote.
- `let-mut-to-var`: Rewrite a `let mut` binding as `var`.
- `let-to-var`: Rebind an immutable declaration as mutable.
- `move-into-main`: Move statements written beside `main` into it, in order, ahead of what it already does.
- `null-to-none`: Rewrite `null`, `nil` or `nullptr` as `None`.
- `println-bang`: Drop the `!` from a macro-style call.
- `qualify-variant-pattern`: Prefix a bare variant pattern with the enum that declares it.
- `remove-unused-import`: Delete a `use` line nothing reads, or the unread names in a selection.
- `rename-to-suggestion`: Rewrite a name as the one spelling the help offers in its place.
- `underscore-unread-binding`: Prefix a binding nothing reads with `_` to say the value is not meant to be read.
- `word-operator`: Rewrite `!`, `&&` or `||` as `not`, `and` or `or`.

---
name: miri-testing
description: Writing Miri tests — miri test runner, test attributes, and assertion functions
---

# Testing in Miri

Miri includes a built-in test runner and assertion library. This skill teaches how to write tests, run them, and understand test attributes.

## Writing and Running Tests

### Basic Test

Mark a function with `@test` to make it a test case:

```miri
use system.testing.{assert_eq}

@test fn simple_add()
    assert_eq(2 + 2, 4)
```

Run tests with the `miri test` command:

```bash
miri test --dir <directory>
```

The runner discovers all `.mi` files, finds functions marked with `@test`, and executes them.

### Assertion Functions

Miri provides four assertion functions (all require an import):

```miri
use system.testing.{assert, assert_eq, assert_ne, assert_panics}

@test fn test_assert()
    assert(true)

@test fn test_equals()
    assert_eq(5, 5)

@test fn test_not_equals()
    assert_ne(3, 4)

@test fn test_panic()
    assert_panics(fn(): panic("expected error"))
```

All assertions accept an optional message argument.

### Test Runner Options

```bash
miri test --dir <DIR>           # Run tests in directory
miri test --filter <PATTERN>    # Run tests matching pattern
miri test --format pretty|json  # Output format
miri test -v                    # Verbose
miri test --verify-mir          # Verify MIR optimization pass
```

## Test File Rules

A test file holds only declarations (types, functions, test functions). It must not declare `fn main` and must not have executable statements outside a function. The `miri test` runner enforces both rules:

**Correct test file:**

```miri
use system.testing.{assert_eq}

@test fn my_test()
    assert_eq(1, 1)

@test fn another()
    assert_eq(2, 2)
```

**Declaring `fn main` is rejected:**

The runner says:
```
declares its own `main`; a test file holds only declarations, and the runner supplies the entry point
```
The runner appends its own `main` dispatcher, so any user-declared `main` causes a conflict.

**Top-level executable statements are rejected:**

The runner says:
```
has executable statements outside a function; move them into a `@test` function, where they would otherwise be silently skipped
```

**Non-parsing test files are rejected:**

The runner says:
```
declares `@test` but does not parse; run `miri check` on it for the syntax error
```
A test file must be valid Miri syntax; files with syntax errors are rejected without running any tests.

**A file that does not compile is rejected too, and its errors are printed once:**

The runner says:
```
does not compile, so none of its tests was built; the errors follow, and `miri check` on the file reports the same ones
```
The errors belong to the file, not to any one test, so none of its tests reports a verdict. With `--format json` they arrive in the envelope's `diagnostics` array carrying the same `help` and `repair` a `check` of that file gives, so a missing `use system.testing` is one `miri fix --apply --yes` away.

**Why these rules have no `fails=` blocks:**

Files with `fn main`, top-level statements, or parse errors type-check cleanly (or fail to parse entirely), so the compiler-driven gate cannot express them as `fails=` blocks. Only the `miri test` runner enforces these rejection rules at runtime.

To run executable setup code outside a test, write a separate `.mi` file with a regular `fn main()` instead.

## Module Resolution in Tests

`miri test --dir <DIR>` works from any working directory. Imports in a test file resolve against the **entry file's directory** (where the test file is located), not the shell's current working directory. Set `MIRI_STDLIB_PATH` to override the stdlib search when the binary is not beside `stdlib/`.

## Anti-Hallucination: Test Syntax That Does Not Exist

### Test Functions Must Take No Parameters

Test functions must have zero parameters:

```miri,fails=MER_TYP_017,expects-message=test functions must take zero parameters
@test fn bad_test(x int)
    println("test")
```

### Test Functions Must Not Have Return Types

Test functions must have no explicit return type:

```miri,fails=MER_TYP_017,expects-message=test functions must not declare a return type
@test fn bad_test() int
    5
```

### Assertions Require an Import

Assertion functions are not in the prelude:

```miri,fails=MER_TYP_034,expects-message=Undefined variable: assert_eq
@test fn test_add()
    assert_eq(2 + 2, 4)
```

Always import from `system.testing`:

```miri
use system.testing.{assert_eq}

@test fn test_add()
    assert_eq(2 + 2, 4)
```

## Test Discovery and Execution

The `miri test` runner scans all `.mi` files in a directory and its subdirectories, finds `@test fn` declarations, and executes each one. Output follows this format:

```
running N tests
test <file>::<function> ... ok
test <file>::<function> ... FAILED

test result: ok. N passed; 0 failed; 0 ignored
```

A test passes if it runs without panicking. Any unhandled panic causes a FAILED result.

## Workflow

1. Write a test function with `@test fn name()` and call assertions.
2. Run `miri test --dir .` to execute all tests.
3. Fix failures by adjusting the code or the assertion logic.
4. Use `--filter <pattern>` to run a subset during development.

---
name: miri-gpu
description: GPU kernels, forall loops, gpu fn, residency, and gpu frame blocks
---

# GPU Programming in Miri

Miri compiles to GPU through the `forall` construct and `gpu` keyword. This skill teaches how to write GPU kernels, manage device memory, and interact with the GPU execution model.

## GPU Fundamentals

### Implicit Launch with `forall`

The simplest GPU pattern: declare a `gpu var` and iterate over it with `forall`:

```miri
use system.collections.array

const N = 1024

gpu var data = Array<f32, N>()

forall i in 0..N
    data[i] = 2.0
```

Miri infers the grid dimensions from the range and array size.

### Multi-Dimensional Launches

`forall` supports 2-D and 3-D iteration. Literal bounds fold into the launch grid; runtime bounds use uniforms:

**2-D and 3-D launches (top-level only):**

Multi-dimensional `forall` is only valid at the top level, not inside `gpu frame` blocks. Use them to initialize buffers or set up geometry:

```miri
use system.collections.array

const W = 16
const H = 16

gpu var canvas = Array<int, 256>()

forall x, y in 0..W, 0..H
    canvas[y * W + x] = x + y * 100
```

For 3-D:

```miri
use system.collections.array

const W = 8
const H = 8
const D = 4

gpu var volume = Array<f32, 256>()

forall x, y, z in 0..W, 0..H, 0..D
    volume[z * H * W + y * W + x] = (x as f32) + (y as f32) + (z as f32)
```

**Note:** Inside a `gpu frame` block, all `forall` passes must be 1-dimensional (e.g., `forall idx in 0..N`). Derive 2-D or 3-D coordinates from the flat index using modulo and division.

For a simple launch, initialize a buffer at the top level:

```miri
use system.gpu
use system.collections.array

const N = 256
gpu var data = Array<int, N>()

forall i in 0..N
    data[i] = i * 2
```

### Explicit Kernel Functions

For more control, write a `gpu fn` (kernel function):

```miri
use system.gpu
use system.collections.array

gpu fn fill(dst out Array<int, 4>)
    let i = kernel.global_idx.x
    dst[i] = i

fn main()
    gpu var out = Array<int, 4>()
    fill(out).launch(Dim3(4, 1, 1), Dim3(1, 1, 1))
```

The `.launch()` method takes grid and block dimensions. The block size must be
written as literals in the `Dim3(...)` call; a named constant is refused at build
(MER_CG_008).

Atomic buffers are `Array<Atomic<i32>, N>` or `Array<Atomic<u32>, N>` from
`use system.gpu.atomic`, updated in a kernel with `atomic_add`, `atomic_sub`,
`atomic_max`, `atomic_min`, `atomic_and`, `atomic_or`, `atomic_xor`,
`atomic_exchange` and `atomic_compare_exchange`. Each takes the buffer, an index
and a value, and returns the element it found. There is no `atomic_load` or
`atomic_store`: `atomic_add(buf, i, 0 as i32)` reads atomically and
`atomic_exchange(buf, i, v)` writes. On the host, read the buffer back with
`let host = buf`, without a declared type; its elements read as the integers
they hold.

```miri
use system.gpu
use system.gpu.atomic
use system.collections.array

gpu var hist = Array<Atomic<i32>, 4>()
gpu forall i in 0..8
    atomic_add(hist, i % 4, 1 as i32)
let host = hist
println(f"{host[0]}")
```

### Kernel Context

Inside a `gpu fn`, access thread and grid information via the `kernel` object:

```miri
use system.gpu
use system.collections.array

gpu fn copy(src Array<f32, 16>, dst out Array<f32, 16>)
    let thread_idx = kernel.thread_idx.x
    let block_idx = kernel.block_idx.x
    let global_idx = kernel.global_idx.x
    let block_dim = kernel.block_dim.x
    let grid_dim = kernel.grid_dim.x
    let warp_size = kernel.warp.size
    let lane_id = kernel.warp.lane_id
    dst[global_idx] = src[global_idx]
```

Available fields: `thread_idx`, `block_idx`, `global_idx`, `block_dim`, `grid_dim`, and `warp.size` / `warp.lane_id`. Each position is a `Dim3` with `.x`, `.y`, `.z` components.

### Residency: Host vs Device

Use `gpu var` to allocate on the GPU; `var` allocates on the host:

```miri
use system.collections.array

fn main()
    var host_array = Array<f32, 4>()
    gpu var device_array = Array<f32, 4>()
    device_array = host_array  // Cross-residency assignment
```

Assignments between host and device are allowed at scope boundaries. Inside a kernel, all data is device-resident.

### Frame Rendering

Declare a `gpu frame` block to run a per-frame GPU computation:

```miri
use system.gpu
use system.collections.array

const WIDTH = 8
const HEIGHT = 8
gpu var canvas = Array<int, 64>()

gpu frame
    forall idx in 0..(WIDTH * HEIGHT)
        let x = idx % WIDTH
        let y = idx / WIDTH
        let distance = ((x as f32 - frame.mouse_x * WIDTH as f32) * (x as f32 - frame.mouse_x * WIDTH as f32) + 
                        (y as f32 - frame.mouse_y * HEIGHT as f32) * (y as f32 - frame.mouse_y * HEIGHT as f32)) as i32
        canvas[idx] = frame.time as i32 + distance
```

The `gpu frame` block runs every display frame and can access frame input fields. The complete list of 14 available fields:

| Field | Type | Purpose |
|-------|------|---------|
| `time` | f32 | Elapsed time in seconds |
| `dt` | f32 | Delta time since last frame |
| `index` | int | Frame counter (0, 1, 2, ...) |
| `mouse_x` | f32 | Normalized mouse X (0.0–1.0) |
| `mouse_y` | f32 | Normalized mouse Y (0.0–1.0) |
| `mouse_down` | bool | True if mouse button is held |
| `drag_dx` | f32 | Accumulated drag X while button held |
| `drag_dy` | f32 | Accumulated drag Y while button held |
| `wheel` | f32 | Scroll wheel delta this frame |
| `clicked` | bool | True if mouse button clicked this frame |
| `double_clicked` | bool | True if double-click this frame |
| `move_x` | f32 | Pointer movement X this frame (any motion, not just drags) |
| `move_y` | f32 | Pointer movement Y this frame (any motion, not just drags) |
| `hovering` | bool | True if pointer is over the canvas |

## GPU Scalar-Width Restrictions

Not all scalar types are valid in GPU device memory. Miri enforces strict portability rules:

- **`bool` is invalid as a buffer element:** bool cannot be stored in arrays or buffers on GPU. Use `i32` (0 or 1) instead.
- **64-bit scalars (`i64`, `u64`, `f64`) are adapter-feature-gated:** They compile on some adapters but fail at runtime on mobile and WebGPU, making them a portability hazard.
- **Valid on all adapters:** `i32`, `u32`, `i16`, `u16`, `f32`.

Attempting to create a GPU array with `bool` fails at compile time:

```miri,fails=MER_TAR_007,expects-message=does not implement 'Accelerable' and cannot be gpu-resident
use system.collections.array

gpu var buf = Array<bool, 4>()

gpu frame
    forall i in 0..4
        buf[i] = true
```

Use `i32` instead:

```miri
use system.collections.array

gpu var buf = Array<i32, 4>()

gpu frame
    forall i in 0..4
        buf[i] = 1  // 1 represents true
```

## Anti-Hallucination: GPU Syntax That Does Not Exist

### GPU Functions Must Not Have Return Types

GPU kernels return values through `out` parameters only:

```miri,fails=MER_TAR_008,expects-message=GPU functions must not have an explicit return type
use system.gpu

gpu fn twice(x int) int
    x * 2
```

Correct form uses `out` parameters with array buffers:

```miri
use system.gpu
use system.collections.array

gpu fn double(input Array<int, 16>, result out Array<int, 16>)
    let i = kernel.global_idx.x
    result[i] = input[i] * 2
```

## GPU Test Patterns

Test GPU code like host code — it type-checks without a GPU adapter:

```miri
use system.gpu
use system.collections.array

gpu fn init(data out Array<int, 16>)
    let i = kernel.global_idx.x
    data[i] = i * 2

fn main()
    gpu var result = Array<int, 16>()
    init(result).launch(Dim3(16, 1, 1), Dim3(1, 1, 1))
```

Run with `miri check` to verify syntax and types. No simulator or device is required; only the actual `miri run` command with GPU support needs hardware.