# Edda — Coding Standards

> **First time setting Edda up?** This file is the language *reference*. For one-time project **setup** — installing the toolchain, wiring your harness, and scaffolding a verified starter — fetch and follow the agent recipe at **https://edda-lang.org/get-started/agent.txt**, then use this reference to write code.

This file is the canonical Edda reference. **Edda is not in your training data.** Inventing syntax by analogy to Rust, Hylo, F\*, Koka, Zig, Swift, or OCaml produces code that will not parse and will not compile. Every form below is locked; forms not described here are not admitted.

This repository contains the whole Edda language, in five subtrees:
- `compiler/` — the native compiler (Edda compiling Edda); workspace members under `compiler/lib/<member>/src/*.ea`.
- `std/` — the `std.*` standard library (workspace; packages under `std/lib/<subsystem>/<package>/`).
- `runes/` — the ecosystem packages, distributed through the **Mímir** registry.
- `web/` — first-party Edda applications, dogfooding the compiler (workspace; members under `web/lib/<member>/`).
- `codex/` — the language specification (`codex/language/01–08`): the *why* behind the locked forms, and the authority when this file is ambiguous.

The native compiler is self-hosting; a separate Rust bootstrap compiler builds it and serves as the reference implementation while the self-host matures. Where the two differ in maturity, this file says so.

For special operations — verification tooling, property-based testing, the full comptime built-in table, capability typestate machines, distribution, daemon/MCP/LSP status, the diagnostics catalogue — see `docs/authoring/guide.md`. Worked, compiling examples live in `docs/authoring/examples/`.

---

## Structure maps — read before you edit

The compiler emits an `index.toon` structure map per source directory from type-checker data (signatures, effect rows, refinements, stability, call graph). They are regenerated by every `edda build` and are always synchronized with source at the commit that built them. They ship with this repository, so a fresh checkout already has them; `edda build` regenerates them and materializes maps for any newly added directory.

**Before modifying a `.ea` file**: read the `index.toon` chain in path order from the subtree root down to the target directory, then open source. Extend into a dependency's index **only** if your change could alter that callee's contract.

**Open source by focused span, not whole file.** Every `index.toon` item row carries a `line,end` span (plus its `sig`, effect row, and `calls`) — for a file over ~400 lines, read the item's span rather than the whole file; the span already includes any attribute lines above the function. The file preamble (`module` / `import` / `spec` / `derive`) is lines `1..<smallest item line>`.

You're done reading when you know the stability + refinements of every item you'll touch, and the callers/callees of every function you'll modify (and whether a caller's contract is affected).

You do **not** author structural annotations or prose into source — the compiler derives the structure map from checked facts; Edda admits no comments (below). Never edit an `index.toon` by hand.

---

## Listening to the compiler

Diagnostic output is part of the contract — errors, warnings, and lint notes alike. Filtering to just `error[...]` discards signals about correct-but-degrading code.

- **`error[...]`** — must be resolved. The `note:` lines often name the fix.
- **`warn[...]`** — builds but encodes a maintenance hazard. Same priority as errors in code you just wrote; pre-existing in unrelated files is tech debt — don't add to the pile.
- **`note: ...`** — explains *why* the rule exists.

Key lints: `unused_import` (remove or use the leaf); `structure_map_too_dense` (a directory's `index.toon` would exceed ~250 lines, or the directory co-locates call-disjoint over-budget files — split into subdirectories per the diagnostic's prescription; **no opt-out exists**: the per-package `allow` severity was removed, so every diagnostic class is at its default or escalated); `filename_encodes_hierarchy` (`list_widget.ea` → `list/widget.ea`; the directory tree IS the namespace); `file_low_cohesion` (≥400 LOC AND the intra-file call graph splits into disjoint clusters / hub-and-spoke — mutually-recursive walkers correctly stay one file); `binding_should_be_let` (`var` never reassigned → `let`).

Standing build command: `edda build 2>&1 | grep -E "^(build:|error|warn\[)"` — include warnings, not just errors.

---

## Comments — none admitted

Edda source admits **no comments** — no `//`, `///`, `//!`, `/!!`, `!!!`, no block comments (`/* ... */`); the lexer rejects every comment token (`error[comment_not_admitted]`). No doc-comment tier system exists.

A comment can only restate what the code says (redundant) or claim what a local check cannot validate (drift-prone) — and stale comments poison LLM reasoning, entering context as high-confidence fact indistinct from checked fact. So every comment-function relocates: **claims about code** (pure / sorted / blocked-on) → effect rows / refinements / attributes / the issue tracker; **descriptions** → *derived* into the structure map (never authored by hand); **rationale / "why"** → the conversation and tracker, never recorded in-repo (an in-repo decision record drifts exactly like a comment).

The only residual free text in source is the mandatory `reason:` on `@trust` / `@unverified` / `@deprecated` — capped and attached to the item it excuses.

---

## Identifiers and naming

| Item | Casing | Example |
|---|---|---|
| Primitive types | lowercase | `i32`, `u64`, `f32`, `bool`, `usize`, `()`, `String`, `Codepoint`, `never` |
| User-defined types | CamelCase | `Point`, `Filesystem`, `IoError` |
| Field names | snake_case | `peer_seq`, `traffic_keys` |
| Sum-variant constructors | snake_case (dot-prefixed) | `.syn_sent`, `.ack_received`, `.ok`, `.err` |
| Function names | snake_case | `read_file`, `alloc_array` |
| Modules / namespaces | snake_case | `std.os.fs`, `local.parser.tokens` |
| Attributes | snake_case (`@`-prefixed) | `@deprecated`, `@layout`, `@unverified`, `@trust` |

Identifiers start with ASCII letter or underscore; ASCII letters/digits/underscores only. **No Unicode identifiers.**

---

## Reserved keywords (closed set)

```
function   type        spec        comptime    let
var        uninit      public      mutable     take
init       with        where       requires    ensures
decreases  result      forall      exists      return
match      case        if          else        loop
for        in          break       continue    raise
panic      handle      scope       captures    provides
as         import      true        false       stable
unstable   linear      affine      derive      extern
```

- `result` — reserved binding for the return value inside `ensures` clauses only.
- `stable` / `unstable` — function and type stability modifiers. These two are **contextual soft-keywords**: the lexer emits them as ordinary identifiers and the parser recognizes them only in stability-declaration position, so `let stable = 3` or a field named `stable` are admitted.
- `linear` / `affine` / `derive` / `extern` — **hard-reserved** (rejected as identifiers). `linear` / `affine` are type-declaration modifiers for consumption discipline; `derive` is a top-level form parallel to `spec`; `extern` is the external-implementation body form.
- `decreases` — refinement clause for termination measures.

---

## Primitive types

| Type | Range / Notes |
|---|---|
| `i8`, `i16`, `i32`, `i64`, `i128` | Signed integers |
| `u8`, `u16`, `u32`, `u64`, `u128` | Unsigned integers |
| `isize`, `usize` | Pointer-width — `usize` for indices, lengths, capacities |
| `f32`, `f64` | IEEE-754 single and double precision |
| `bool` | `true` / `false`; no implicit int coercion |
| `()` | Unit type; sole value `()` |
| `never` | Bottom type for diverging expressions |
| `String` | Owned UTF-8 heap-allocated string (CamelCase — heap-backed) |
| `Codepoint` | Unicode scalar value (decoding utilities: `std.text.utf8`) |
| `Type` | Comptime meta-type — values are types (`i32`, `String`, etc.) |
| `HeapPtr` | **Stdlib-internal only** — backs `Box(T)`; user code never spells it. |

Defaults:
- Integer literal type: `i64`. Literals do **not** coerce to context — annotate the binding (`let n: usize = ...`) when the target type differs, including when a `match`/`if` arm mixes a literal with a `usize` expression.
- Float literal type: `f64`.
- String literals `"..."` are static-backed `String` (no allocator needed).

---

## Numeric operators

**Trapping by default.** Use explicit-mode operators for non-default behaviour.

| Default (trapping) | Wrapping | Saturating | Checked (raises `err: Overflow`) |
|---|---|---|---|
| `+` `-` `*` `/` `%` | `+%` `-%` `*%` | `+\|` `-\|` `*\|` | `+?` `-?` `*?` `%?` |

- `%` — **Euclidean modulo**, integer types only (result always non-negative; postcondition `b != 0 ⇒ 0 <= result < abs(b)`). Matches SMT-LIB `(mod x y)` so discharge is one solver call. Traps on `b == 0` and `INT_MIN % -1`; `%?` is the checked variant. No wrapping/saturating modulo, and **no float modulo operator**.
- Comparison `==` `!=` `<` `<=` `>` `>=` (non-associative within a tier — `a < b < c` is a syntax error); boolean `&&` `||` `!` (short-circuiting); bitwise `&` `|` `^` `~` `<<` `>>`.
- Type cast: `value as T` (trapping); also `as T wrapping` / `saturating` / `checked`.

Float division by zero traps — add `requires b != 0.0` (or `where b != 0.0` on the param).

---

## Composite types

| Form | Example |
|---|---|
| Tuple | `(i32, String)`; values `(1, "ok")`; positional, n ≥ 2; `(x)` is grouping, not a tuple |
| Slice | `[T]`; access `xs[i]`; length `xs.len()` |
| Slice subrange | `data[lo..<hi]`, `data[lo..]`, `data[..hi]`, `data[..]` — mode inherits from parent |
| Range | `Range_<T>` from `spec std.core.range.Range(T)`; literals `0..<n`, `0..=n` |
| Fixed-size array | `Array_<T>_<N>` from `spec std.collections.array.Array(T, N)` |

---

## Declarations

### Functions

Full clause set, **in order**:

```
function name(<params>) -> ReturnType
    with {<effect-row>}
    where <refinement-bindings>
    requires <precondition>
    ensures  <postcondition>
    decreases <termination-measure>
{ <body> }
```

```edda
function add(x: i32, y: i32) -> i32 {
    return x + y
}

function load(rfs: ReadOnlyFilesystem, path: String, allocator: Allocator) -> String
    with {rfs, allocator, err: fs.FsError}
    requires path.len() > 0
{ ... }
```

- **Mode position**: `name: <mode> Type`. The binding name leads; the mode (if any) sits between colon and type. `mutable buf: [u8]` is **wrong**; `buf: mutable [u8]` is right.
- **Return type is mandatory.** No return-type inference. Unit return: `-> ()`.
- Empty effect row may be written as `with {}` or omitted entirely (pure function).

### Variables

```edda
let x: i32 = 42
var y: i32 = 0
let z = "hello"
uninit buf: Buffer
```

- **No `let mut`.** Use `var`.
- No module-level `let` / `var`. Module-level constants are `function name() -> T { value }` (possibly `comptime`-cached).
- `uninit` declarations may only appear in function bodies.

### Records

```edda
public type Point {
    x: f64
    y: f64
}

let p = Point { x: 1.0, y: 2.0 }
```

Fields in the **declaration body are newline-separated** — commas between fields are admitted but unidiomatic, and a trailing separator is admitted too. Inside a **struct literal** (`Point { x: 1.0, y: 2.0 }`), fields are comma-separated as you'd expect for an expression. Struct literals require all fields visible. There is no `..default` shorthand.

### Sum types

```edda
public type Direction {
    case north
    case south
    case east
}

public type FetchOutcome {
    case ok(i32)
    case err(stream.IoError)
}

public type ParseError {
    case wrong_token_count(got: usize)
    case invalid_operator
}

let r: FetchOutcome = FetchOutcome.ok(42)
let e: ParseError = ParseError.wrong_token_count(got: 3)
```

`case <name>` lines, newline-separated, no commas. **Declaration** uses `case` (no dot); **construction** qualifies — `Direction.north`, `FetchOutcome.ok(42)`; **inside `match`** the dot-prefixed form is the pattern — `case .north`, `case .ok(let v)`, `case .wrong_token_count(let got)`.

**The payload's declaration form dictates the construction form.** An unnamed payload (`case ok(i32)`) constructs positionally (`.ok(42)`); a named payload (`case wrong_token_count(got: usize)`) constructs with named arguments (`.wrong_token_count(got: 3)`). The stdlib's `Option` declares `case some(value: T)`, so construction is `Option_T.Option.some(value: x)`. Named payloads are one of the few sites where named arguments appear at a call site.

### Stability modifiers

`stable function` / `stable type` puts the signature on the stable (versioned) surface. A `stable` item is verifier-constrained: effect-row whitelist (`err` / `panic` / `alloc` / `yield` / `DeterministicRandom` only — no `io` / `random` / ambient `time`); stable callees only; no hash-map iteration (diagnostic `stability_hash_iter` — iterate a sorted snapshot of the keys instead); no pointer-identity-dependent returns; `scope(coherence)` but **not** `scope(exec)` — full rules in `docs/authoring/guide.md`. `@unverified` on a `stable function` is rejected. Defaults: `public` → `unstable`; non-`public` → no stability obligation.

### Linear / affine types

```edda
linear type FileHandle { ... }
affine type Counter { ... }
```

- `linear T` cannot be dropped silently (losing one unconsumed is rejected); `affine T` may be dropped but otherwise behaves linearly.
- Passing a `linear T` by `let` does **not** discharge the obligation — only `take` does; a `handle` block must consume any linear value on both success and failure paths.

### Modules and imports

```edda
import std.core.option
import std.os.fs.{read_to_string, write_string}
import std.os.fs as fs
import std.io.stream
import std.io.stream as io
import local.parser.tokens
```

Forms in order: bare import; selected-names `.{...}`; `as` alias; bare leaf (reference `leaf.Item`); aliased leaf; same-package `local.<path>` (resolves from `<pkg-root>/src/`).

Path resolution:
- `std.*` — standard library. Paths follow the physical directory layout: `lib/io/stream/` → `std.io.stream`, `lib/mem/alloc/` → `std.mem.alloc`, `lib/core/option/` → `std.core.option`, etc.
- `local.<path>` — same-package, resolves from `<pkg-root>/src/`. (`local.` is an **import** form only — it is not admitted in `spec` invocation paths; see Specs.)
- Any other prefix — a **rune** dependency declared in `package.toml`, or another workspace member's `root_namespace`.

**The leaf is canonical.** `import std.A.B.C` brings `C` into scope; reference items as `C.Item`. Inside the defining file (declares `module std.A.B.C`), the leaf is auto-bound as a self-alias — `stream.IoError` works inside `module std.io.stream` and in any consumer that wrote `import std.io.stream`. Consumers MAY alias (`import std.io.stream as io`, then `io.IoError`); defining files cannot alias themselves. Cross-package effect rows: `err: alloc.AllocError` / `err: stream.IoError` / `err: fs.FsError` / `err: str.ParseFloatError`.

### File-level `module` declaration

Every `.ea` file inside a workspace member begins with a `module <root>.<file>` declaration naming this file's position in the package's module tree:

```edda
module source.file

import std.core.option
import local.read as read_mod
```

Without this declaration, cross-file type references in the same package fail with `error[import_resolution_error]: unresolved path <Type>`.

When an imported leaf collides with a local binding (a field or local named like the module), alias with the `_mod` suffix: `import local.read as read_mod`, then `read_mod.Read` — the project convention.

### Layout — single package vs workspace

Single package: `<pkg-root>/package.toml` + `<pkg-root>/src/*.ea`. Workspace: the root `package.toml` carries `[workspace]` with either an explicit `members = ["foo", "bar"]` list or `discover = true` (auto-enumerate `lib/<...>/package.toml`); each member lives at `lib/<member>/{package.toml, src/*.ea}`. Members are implicitly each other's dependencies by `root_namespace` — `import bar.shared` inside `foo` resolves with no `[[dependencies]]` entry.

In this repository the four buildable trees are siblings: `compiler/`, `std/`, `runes/`, and `web/`, each its own workspace. A `web/` member consumes runes by `[[dependencies]]` path into `runes/lib/<name>` (e.g. `source = "path+../../../runes/lib/hermod"`). Pre-built distributable packages are **runes** (archive `.rune`); source root is always `src/`; registry brand **Mímir**. Manifest shape, hashes, and the distribution surface: `docs/authoring/guide.md` (+ `codex/language/08-packages.md`).

### Attributes

Attributes prefix the item directly below them and take an optional named-arg list in parentheses.

```edda
@deprecated(reason: "Use `read_bytes` instead.", since: "v0.2")
public function read_blob(rfs: ReadOnlyFilesystem, path: String, allocator: Allocator) -> [u8] { ... }

@unverified(reason: "RFC 5246 specifies this byte layout")
function pack_header(version: i32, kind: i32) -> i32 { ... }

@layout(packed)
type WireHeader { ... }
```

Attribute family — a **closed whitelist** of nine: `@layout`, `@align`, `@repr`, `@abi`, `@unverified`, `@trust`, `@deprecated`, `@property`, `@target_requires`. Any other `@name` is a **hard error** (`error[unknown_attribute]`) — the `@`-namespace is as dead to prose as `//` (no attribute-shaped escape hatch; see anti-patterns). The only residual free text is the mandatory `reason:` on `@trust` / `@unverified` / `@deprecated`.

---

## Modes (call-site keywords on non-default args)

```edda
let n = read(s)
write(mutable s)
let bytes = consume(take s)
uninit t: String
produce(init t)
```

- `let` — borrowed read-only view (default; no keyword at call site).
- `mutable` — borrowed mutable view.
- `take` — ownership transferred to callee.
- `init` — callee initialises a previously-`uninit` binding.

**Struct-literal field initialisers admit mode keywords** — when a field consumes a `linear`/`affine` binding the transfer must be explicit with `take` (`Line { start: take a, end: take b }`), exactly as at a call site; ownership transfer is never implicit. A field initialised from a copy (non-linear) type, a literal, or a temporary needs no keyword.

---

## Control flow

### If

```edda
let max = if a > b { a } else { b }
```

`if` is both an expression (both branches yield the same type) and a statement.

### Match

```edda
return match opt {
    case .some(let value) => transform(value)
    case .none            => fallback
}
```

Patterns admitted in the V1.0 surface:
- Variant: `case .variant(let v)`, `case .variant(_)`, `case .variant`.
- Tuple: `case (let a, let b)`, `case (let a, _)`.
- Struct: `case Point { x: let xv, y: _ }`, `case Point { x: 0.0, y: let yv }`, `case Point { x: let xv, .. }` (explicit rest).
- Literal: `case 0`, `case "hello"`, `case true`.
- Wildcard: `case _`.
- Guarded: `case .some(let v) where v > 0 => ...`.
- Range: `case 0..<10`, `case 0..=255` — endpoints must be literal constants of an ordered primitive type.
- Or: `case .a | .b`, `case 0 | 1 | 2` — every alternative binds the same names with the same types and modes.
- `@`-binding: `case whole @ .some(let v)` — binds the matched value as `whole` and matches its shape against the subpattern.
- Slice: `case [first, second]`, `case [head, ..tail]`, `case [..init, last]`, `case []` — at most one rest binding per pattern.

Reserved post-V1.0: mixed modes on destructured tuple positions (`(let a, mutable b)`).

### Loops

```edda
loop { if done { break }; advance() }
loop decreases (n - i) { ... }
for x in xs { consume(x) }
```

`for` is a **statement**, not an expression — to collect, push into a `Vec`:

```edda
spec std.collections.vec.Vec(i64)

uninit out: Vec_i64.Vec
Vec_i64.new(init out, allocator)?
for x in xs {
    if keep(x) { Vec_i64.push(mutable out, x, allocator)? }
}
```

`break <expr>` exits a `loop`-as-expression with that value; `continue` advances the innermost loop. Unbounded `loop` without `decreases` implicitly contributes `effect divergence` to the row.

### Return / raise / panic

```edda
return value
raise ParseError.wrong_token_count(got: 3)
panic("invariant violated")
```

All have type `never` and exit non-locally.

---

## Effect rows

Row syntax: `with { <entry>, <entry>, ... }` (e.g. `with {rfs, allocator, err: fs.FsError}`). Empty row may be omitted entirely; `with {}` also admitted.

Entry kinds:
- **Capability**: bare identifier matching a parameter name. `with {rfs}` means "this function uses the capability passed as `rfs`." Calls through a *narrowed local* (e.g. a scoped filesystem derived from a parameter) attribute to the source parameter's row entry.
- **Pure typed effect**: `err: <Type>`, `panic`, `yield: <Type>`, `cancellation`, `divergence`, `nondet`.
- **Graded effect**: `alloc(bytes <= N)`, `io(calls <= N)`, `time(ops <= N)` — constant non-negative bounds. The graded forms are locked V1.0 surface; bound *verification* is still maturing in the native compiler.

Rows are **closed** (exactly listed, no row variable), **unordered** (init semantics), **unique**.

### `?` propagation

```edda
let text = fs.read_to_string(rfs, path, allocator)?
```

`?` propagates the callee's `err: T` entries into the caller's row. The caller's row must already contain (or be compatible with) each `err: T`.

**`?` does NOT unwrap `Option` or `Outcome`** and does **not** propagate other effect kinds (`cancellation`, `divergence`, `nondet`). For sum-type chaining, use `match` or combinators. **No `?.` chaining, no `??` coalesce.**

### Effect handlers

```edda
let content = handle err: fs.FsError as e -> match e {
    case .not_found => default_config()
    case _          => raise e
} { read_config(rfs, path, allocator)? }
```

Form: `handle <effect>: <Type> as <binder> -> <recovery-expr> { <body> }`. Removes `<effect>: T` from the body's row and binds the caught value to `<binder>` (typed `T`); recovery may pattern-match, `raise`, default, or `panic`, and its row joins the surrounding context. `err:` is the literal keyword — `handle err: T as e -> ...`, not `handle e: T -> ...`; the binder name is yours (an unused binder is admitted).

### Structured concurrency

```edda
scope(exec) group {
    let fa = group.spawn { work(a) }
    return match fa.await { case .ok(let v) => v  case .err(let e) => raise e }
}
```

`scope(exec) <name>` (requires `Executor`) opens a task scope; `<name>.spawn { <body> }` opens a child (spawn args are `take`-mode) yielding a `linear Task(T)` joined via `.await`. The scope **cannot exit while children run** (no fire-and-forget); **no `mutable` crosses a spawn boundary** — pass `take` of a fresh value. `cancellation` / `divergence` / `nondet` each have a handler form like `err: T`.

**`std.task`.** `group.spawn { body }` produces `linear Task(T)`. `.await` is **compiler-lowered** (not a stdlib function); the stdlib surface is `detach` / `cancel` / `cancel_and_await` (losing the handle is `linear_unconsumed`). Cross-task errors travel as `Outcome(T, E)` in the body's return value — **not** `err: T` in the row (a spawn body's row carries capabilities + `cancellation` only). `await`'s row is `{cancellation}`; cancellation surfaces via `handle cancellation -> ...` or the enclosing `scope(exec)`. Full surface + the `alloc.fork()` per-task allocator: `docs/authoring/guide.md`.

### Coherence regions

`scope(coherence) <name> { <body> }` is **observational atomicity** — outsiders see only pre- or post-region state, never intermediate; partial mutations remain on failure (non-rollback). `init` not admitted inside; `take` consumed at entry. Composes with `scope(exec)`.

---

## Refinements

Four positions: (1) on a parameter type — `i: usize where i < v.len()`; (2) on a record field — `len: usize where len <= items.len()`; (3) top-level `requires <pred>`; (4) top-level `ensures <pred>` (`result` = the return value). Plus `where` on `spec` declarations (comptime-arg constraints).

```edda
function clamp(value: take T, lo: take T, hi: take T) -> T
    requires lo <= hi
    ensures  result >= lo
    ensures  result <= hi
{ ... }
```

**Built-in obligations** (compiler-discharged): integer overflow on `+ - *`, slice index `xs[i]` carries `i < xs.len()`, float `a / b` carries `b != 0.0`, narrowing cast carries "value in T's range".

### `decreases` — termination

```edda
function factorial(n: usize) -> usize
    decreases n
{ return if n == 0 { 1 } else { n * factorial(n - 1) } }
```

Required on every recursive function whose termination isn't structurally obvious, and on every unbounded `loop`. The measure is a non-negative integer that strictly decreases each call/iteration; absence forces `effect divergence` in the row. When no structural measure exists (e.g. walking a `Box`-linked structure), thread an explicit fuel parameter and `decreases fuel` — see `docs/authoring/examples/tree.ea`.

### Trust hatches

`@unverified(reason: "...")` skips SMT discharge for the whole function. `@trust(reason: "...")` skips discharge at a single annotated site. Both require the `reason` field. **No `assume` keyword exists.**

### V1.0 decidable fragment

V1.0 fragment: `AUFLIA + extensionality + bounded quantifiers`. The native compiler discharges it with its own in-tree CDCL(T) solver (`compiler/lib/refine/src/solver/` — no external process); the Rust bootstrap discharges the same fragment via an embedded Z3. NLA / bitvector / floating-point predicates are post-V1.0 — keep them behind `@trust` / `@unverified`.

**Bounded quantifiers** — `forall <ident> in <iter>: <body>` and `exists <ident> in <iter>: <body>`. `<iter>` is a range (`0..<n`) or slice (`xs`); `<body>` is a `bool` predicate over the bound variable. Bound variable is in scope only inside `<body>`. Admissible only in refinement positions (`where` / `requires` / `ensures`).

Note: `edda check` type-checks only — refinement obligations are discharged by `edda build`. A clean `check` does not mean your `requires`/`decreases` obligations hold.

---

## Specs — Edda's only generic mechanism

**No language-level generics.** No `<T>` parameters in declarations, no traits, no `impl T { ... }` blocks. Reuse happens through `spec` — concrete codegen templates with comptime arguments.

```edda
public spec Stack(comptime T: Type) where size_of(T) > 0 {
    public type Stack { items: [T], len: usize where len <= items.len() }
    public function push(s: mutable Stack, item: take T) -> () with {panic} { ... }
}
```

Instantiation is a file-scope `spec` invocation naming the **full module path** (never `local.`), followed by use of the generated instance module:

```edda
spec std.collections.vec.Vec(i64)
spec mypkg.stack.Stack(i64)

uninit v: Vec_i64.Vec
Vec_i64.new(init v, allocator)?
Vec_i64.push(mutable v, 42, allocator)?
```

- The instance module is named `<SpecLeaf>_<args>` with dots mangled to underscores: `Vec(i64)` → `Vec_i64`; `Option(Box_TreeNode.Box)` → `Option_Box_TreeNode_Box`.
- Reference the instance's type as `Vec_i64.Vec` — or, when the spec's main type shares the spec's name, the bare instance name is admitted shorthand (`next: Box_Link`).
- Spec invocations live at **file scope** only — never inside a function body. Each instantiation is **content-addressed** via BLAKE3 over its canonical encoding; same arguments produce the same artifact hash.

**`provides` clauses** declare operator/function-shape requirements (`spec Sum(comptime T: Type where T provides +, 0)`); the check happens at invocation. **Outbound type parameters** (`function map<comptime U: Type>(...)`) introduce additional comptime args inside spec bodies; codegen monomorphises per `(T, U, ...)` tuple.

---

## Derive forms (closed whitelist)

```edda
type Point {
    x: i32
    y: i32
}

derive eq, hash, debug for Point
derive properties for Point
```

`derive` is a top-level declaration form parallel to `spec`. It desugars to a sequence of spec invocations. The vocabulary is **closed**:

| Derive item | Use |
|---|---|
| `eq` | structural equality |
| `ord` | total ordering (requires `eq`) |
| `hash` | content hashing |
| `debug` | debug formatting |
| `clone` | structural copying (non-linear/affine only) |
| `properties` | PBT generators + property runner |
| `serialize` / `deserialize` | canonical serialisation |

**User-defined derives are not admitted.** Custom codegen goes through writing a `spec`. Generated modules follow spec-mangling (spec leaf first, like `Vec_i32`): `derive eq for Point` produces module `eq_Point` (entry point `eq_Point.eq`); `ord` → `ord_Point.compare`, `hash` → `hash_Point.hash`, `debug` → `debug_Point.format`.

---

## Comptime

Five keyword positions — forced-evaluation expression, comptime block, comptime parameter, `comptime if`, and `comptime for` (in that order below):

```edda
let TABLE_SIZE = comptime compute_size()

let table: [u32] = comptime { var t: [u32] = ...; for i in 0..<256 { t[i] = entry(i) }; t }

function array_of<comptime T: Type, comptime N: usize>(...) -> ...

comptime if target.supports(Subprocess) { link(p, plan, alloc)? } else { ... }

comptime for i in 0..<field_count(T) { total = total +% 1 }
```

`comptime if` is the target-conditional branch — the dead branch is elided **before** typecheck (see Capabilities → per-target availability).

`comptime for <ident> in <comptime-range> { <body> }` is a monomorphization-time unrolled loop, used inside a `spec` body to walk a comptime `Type` parameter's fields/variants (the range bound is canonically `field_count(T)` or a similar introspection builtin — this is the mechanism `derive eq`/`hash`/`debug`/etc. use). **Only this field-walk idiom is currently implemented** — `comptime for` over an arbitrary comptime-decidable range (a literal bound, outside a spec body's field-walk) is not yet lowered.

Comptime-pure built-ins on `Type` (admissible in `where` / refinement predicates): `size_of`, `align_of`, `offset_of`, `field_count`, `field_name_at`, `field_type_at`, `is_*` (signed/unsigned/integer/floating/numeric/primitive), `target.supports`. Full signatures: `docs/authoring/guide.md`.

---

## Function types and closures

`function(T1, T2) -> R with {row}` is first-class anywhere a type appears. The fully wired form is **passing a named function as a value**:

```edda
function dispatch(out: Stdout, target: function(Stdout, String) -> () with {out}, arg: String) -> () with {out} { target(out, arg) }
```

Indirect calls thread capabilities and propagate `err: T` via `?` like direct calls. **Closure-literal support is still maturing**: zero-capture closures and scalar captures (word-sized primitives, `let` or `take` mode) lower and execute; record/aggregate captures and heap-backed escaping captures (`String`, records) are not yet reliable end-to-end. For anything beyond simple scalar captures, factor the body into a named top-level function and pass it by name — the pattern above. (Locked `captures {...}` syntax: `docs/authoring/guide.md`.)

---

## Recursive types

Via `std.mem.alloc.Box(T)` indirection. Spec invocations materialise before type bodies resolve, so `Box_*` is available when the type is parsed:

```edda
spec std.mem.alloc.Box(TreeNode)
spec std.core.option.Option(Box_TreeNode.Box)

type TreeNode {
    value: i64
    left: Option_Box_TreeNode_Box.Option
    right: Option_Box_TreeNode_Box.Option
}
```

Construct with `Box_TreeNode.new(take node, allocator)?` (row `{allocator, err: alloc.AllocError}`); read through with `Box_TreeNode.get(b)`; consume with `Box_TreeNode.unbox(take b, mutable allocator)` or `Box_TreeNode.drop(take b)`. Mutual recursion (A → B → A) takes a `Box` on each cyclic edge — declare each `spec …Box(T)` first. Worked example: `docs/authoring/examples/tree.ea`.

---

## Capabilities

**Locked nominal types** (18): `Filesystem`, `ReadOnlyFilesystem`, `SandboxedFilesystem`, `Network`, `LocalhostNetwork`, `RestrictedNetwork`, `Clock`, `MonotonicClock`, `Random`, `DeterministicRandom`, `Allocator`, `BoundedAllocator`, `Executor`, `Stdin`, `Stdout`, `Stderr`, `Subprocess`, `Debugger`. **No `World` aggregate** — capabilities are passed individually.

**Narrowing** (one-way, produces a strictly weaker capability). Implemented in the stdlib today:
- `fs.read_only(wfs: Filesystem) -> ReadOnlyFilesystem`
- `fs.scoped_to(rfs: ReadOnlyFilesystem, prefix) -> ReadOnlyFilesystem` / `fs.scoped_to_w(wfs: Filesystem, prefix) -> Filesystem`
- `clock.monotonic()`
- `alloc.fork(a: Allocator) -> Allocator` (and `alloc.close(take a)`)
- `subprocess.allowing(allowlist)` / `subprocess.scoped_to(dir)`

Locked in the catalogue but **not yet in the stdlib**: `Network.bind_localhost` / `.restrict_to`, `Random.deterministic`, `Allocator.bounded`, `Executor.child`. (`SandboxedFilesystem` is in the locked catalogue; today's scoping helpers return scoped `ReadOnlyFilesystem` / `Filesystem` views.)

**Capabilities cannot be synthesised** — `Filesystem.new()` is rejected. They come only from parameters or narrowing of a held capability. The entry point declares which it needs:

```edda
import std.io.stream

public function main(stdin: Stdin, out: Stdout) -> () with {stdin, out, divergence} {
    out.print_line("hello")
}
```

### `Subprocess`, per-target availability, typestate

`Subprocess` spawns external processes via `std.os.process`: `spawn(p: Subprocess, take bundle: ChildSpec, allocator) -> ChildHandle` (typestate `running → exited`); consume the handle with `wait(take h) -> ExitOutcome` / `kill(take h) -> ExitOutcome` / `detach(take h)`, else `linear_unconsumed`. `ChildSpec.of(exe, args).with_stdout(take h).with_fs(take ro_fs)…build()` grants the child a **subset** of capabilities the parent holds — it cannot exercise authority the parent lacks.

**Per-target availability** is locked per `(cap, target)` (monotonic — `✗→✓` admissible, `✓→✗` not). Gate code two ways: `@target_requires(T)` (the function does not exist on unsupported targets) and `comptime if target.supports(T) { ... } else { ... }` (dead branch elided **before** typecheck, so the unsupported arm may reference absent caps). `Subprocess` is `✗` on `wasm32-wasi-preview1` and `bare_metal`.

`Debugger` is the OS process-control capability behind the planned verification-aware source debugger; it rides `ptrace` / `DebugActiveProcess`, so it is available only on hosted OSes (`✓` on `linux` / `windows` / `macos` / `freebsd`; `✗` on `wasi` / `browser` / `bare_metal`). The nominal type is compiler-known; the debugger tooling itself is a roadmap item.

**Typestate** is tracked statically — `Allocator` (`open → closed` via `alloc.close`), `Network` connection (`dialing → connected → closing → closed`, design-locked); ops invalid in a state are compile errors (`typestate_violation`), no runtime checks. Full `ChildSpec` method set, per-target table, and state machines: `docs/authoring/guide.md`.

---

## Strings

```edda
let s: String = "hello"
let greeting = f"hello, {name}"
let bs = s.bytes()
let n = s.len()
let dup = string.concat(s, " world", allocator)?
```

`"..."` is static-backed. `s.bytes()` → `[u8]`; `s.len()` is **byte** length (not codepoints). `std.text.string` carries the allocating helpers — `concat`, `clone`, `trim`, `split`, `replace`, `to_lowercase` / `to_uppercase` (each takes an `Allocator`, raising `err: alloc.AllocError`) — plus pure `equals`, `find`, `contains`, `starts_with` / `ends_with`, and `from_owned_utf8(take bytes) -> String`. There is **no codepoint iterator yet**; codepoint-level decoding lives in `std.text.utf8`.

**f-strings** (`f"..."`) interpolate any expression whose type has a canonical formatter — primitives, `bool`, `String`, derived-`debug` types. No `to_string` calls needed.

**Multi-line strings** use `"""..."""` (common indent bounded by the closing `"""` is stripped). **Plain `"..."` is single-line** — no embedded newlines.

---

## Stdin / Stdout API

Defined in `std.io.stream` (import it). Locked surface:

| Operation | Effects | Notes |
|---|---|---|
| `out.print_line(s)` / `out.print(s)` | `{out}` | `print_line` appends `\n`. |
| `errout.eprint_line(s)` / `errout.eprint(s)` | `{errout}` | Stderr equivalents. Unbuffered. |
| `stdin.read_line() -> String` | `{stdin, err: stream.IoError}` | Returned `String` includes the trailing newline byte(s); strip explicitly. EOF → `err: stream.IoError` (variant `unexpected_eof`). |

Method form (`out.print_line(s)`) and module form (`stream.print_line(out, s)`) are both admitted — `obj.method(args)` desugars to `method(obj, args)`.

No `println` / `writeln` / `puts`. `stdin.read_line()` does not take an `Allocator` — the runtime handles the buffer.

Stdlib error types are **path-qualified** in rows (`err: stream.IoError` / `alloc.AllocError` / `fs.FsError` / `str.ParseFloatError`); bare names don't resolve.

---

## Filesystem and parsing

Filesystem access lives in `std.os.fs`. Reads take a `ReadOnlyFilesystem` and an `Allocator`; writes take a `Filesystem`:

```edda
let text  = fs.read_to_string(rfs, path, allocator)?
let bytes = fs.read_bytes(rfs, path, allocator)?
let names = fs.read_dir(rfs, dir, allocator)?
fs.write_string(wfs, path, contents)
fs.write_bytes(wfs, path, bytes)
```

Each read raises `err: fs.FsError` (variants include `not_found`, `permission_denied`, `invalid_utf8`, `os_error`). There are no bare `fs.read` / `fs.write` functions.

Numeric parsing lives in `std.text.str`: `str.parse_f64(bytes) -> f64`, `str.parse_i64(bytes) -> i64`, `str.parse_u64(bytes) -> u64`. Each raises `str.ParseFloatError` or `str.ParseIntError` via the effect row.

---

## Stdlib renames

| Old | New |
|---|---|
| `std.result` | `std.core.outcome` |
| `Result(T, E)` | `Outcome(T, E)` |

`Outcome(T, E)` is the value-shaped success/failure carrier (collections, channels, task-join — anywhere failure is part of the storage API). Ordinary fallible functions use `err: T`; **`Outcome` is forbidden as a fallible function's return type.**

---

## Module-level shape

Order within a file:
1. `module <root>.<file>` declaration.
2. `import` declarations.
3. `spec` invocations.
4. `derive` declarations.
5. Top-level items (`type`, `function`, attribute-prefixed forms) — any order within this section; no forward declarations needed.

**Visibility**: `public` makes the item part of the module's public surface. Default is module-internal. No `private`, no `crate`, no `protected`.

---

## Anti-patterns — things that look right but aren't

High-frequency mistakes for anyone arriving from Rust, Hylo, Swift, OCaml, etc.

### Syntax

- **Sum types use `case`, not `|`.** `type X = | .a | .b` does not parse.
- **Record fields are newline-separated in declarations.** Commas (incl. trailing) are admitted but unidiomatic — prefer newline separation. Struct **literals** always use commas — that's an expression.
- **No comments of any kind.** `//`, `///`, `//!`, `/!!`, `!!!`, and `/* ... */` all fail to lex (`error[comment_not_admitted]`). Claims about code go in effect rows / refinements / attributes / the issue tracker; descriptions are derived into the structure map; rationale lives in the conversation and tracker, not in source. See "Comments — none admitted".
- **`@invariant`, `@pattern`, `@note`, `@internal`, `@section`, or ANY non-whitelist `@name` are hard-rejected** (`error[unknown_attribute]`) — not "tolerated and ignored". The `@`-namespace is a closed whitelist (see Attributes). Invariants → `where`/`requires`/`ensures`; patterns → `spec`; stability → the `stable`/`unstable` keywords. **Smuggling prose into a fake attribute is comment-poison under new syntax** — the source surface is sterile by design; do not reach for an attribute when comments are gone.
- **No `let mut x`.** Use `var x`.
- **No `&str` / `&T` borrowed-view types.** A borrowed string is `let String`; a borrowed slice is `let [T]`. Modes carry ownership.
- **Mode position is `name: <mode> Type`**, not `<mode> name: Type`. `buf: mutable [u8]`, not `mutable buf: [u8]`.
- **`for` is a statement, not an expression.** To collect, push into a `Vec` (see Loops).
- **Named arguments appear only in three places**: attribute args, named variant payloads, and `with`/`captures` rows. Ordinary call sites are positional.
- **No `discard <expr>`.** Use `let _ = <expr>`.
- **No multi-line `"..."`.** Use `"""..."""` with indent-stripping.
- **`result` is a reserved keyword** (the binding inside `ensures`). Pick `value`/`output`/etc. for locals.
- **Integer literals don't coerce.** A bare `0` is `i64`; annotate the binding (`let n: usize = ...`) when arms or operands need another integer type.

### Generics and traits

- **No `<T>` generic parameters in declarations.** Use `spec`.
- **No traits, no `impl Trait`, no typeclasses, no `dyn Trait`.** Specs are concrete codegen templates; use function-valued parameters for dispatch.
- **No `impl T { ... }` blocks.** Methods are free functions whose first parameter is the receiver; `obj.method()` desugars to `method(obj)`.
- **No custom derives.** The whitelist is closed; custom codegen goes through a `spec`.
- **`local.` is not admitted in `spec` invocation paths.** Instantiate your own package's spec by its full root-namespace path: `spec mypkg.stack.Stack(i64)`.

### Errors and chaining

- **`?` does not unwrap `Option` or `Outcome`.** It propagates `err: T` only. Use `match` or combinators for sum types.
- **No `?.` chaining operator. No `??` coalesce.**
- **Never return `Outcome(T, E)` from a fallible function.** Errors travel through the effect row. `Outcome` is a storage carrier only.
- **`std.result` was renamed to `std.core.outcome`.** Old name does not resolve. See "Stdlib renames" section.
- **No `assume` keyword.** Use `@unverified(reason: "...")` on the item or `@trust(reason: "...")` at a site.

### Numeric

- **Integer overflow traps by default.** Use `+%` (wrap), `+|` (saturate), `+?` (checked, raises `err: Overflow`).
- **Narrowing casts trap on out-of-range by default.** Use `as T wrapping` / `as T saturating` / `as T checked`.
- **Float division by zero traps.** Add `requires b != 0.0`.

### Termination

- **Recursive functions and unbounded `loop` without a `decreases` clause** must admit `effect divergence` in the row.

### Concurrency

- **No fire-and-forget spawn.** Every task lives inside a `scope(exec) <name>` block.
- **No ambient `Executor`** — it's a parameter, never magic-bound.
- **Cannot share `mutable` across a spawn boundary.** Pass `take` of a fresh value.

### Capabilities

- **No `Filesystem.new()` / `Allocator.new()` / etc.** Capabilities come only from parameters or narrowing.
- **No global allocator.** `Allocator` is a parameter; allocating functions propagate `err: alloc.AllocError`.
- **Path-qualify stdlib error types in leaf form.** Use `alloc.AllocError` / `stream.IoError` / `fs.FsError` / `str.ParseFloatError`. Bare names don't resolve and break provenance verification. Consumer files may alias (`as io`, etc.) but the canonical reference is the leaf.
- **No `World` aggregate.** Capabilities are passed individually to `main`.
- **`stdin.read_line()` includes the trailing newline.** Strip CRLF/LF before comparing or parsing.
- **Filesystem reads take `ReadOnlyFilesystem` + `Allocator`.** Narrow a `Filesystem` with `fs.read_only(wfs)` before reading; there are no allocator-free read helpers.

### Types

- **No self-referential types without `Box`.** Use `spec std.mem.alloc.Box(T)` and reference `Box_T`.
- **No `Maybe<T>` / `T?` / `T | None`.** Use `Option(T)` from `std.core.option` — and construct with the named payload: `.some(value: x)`.
- **No spelling `HeapPtr` in user code** — it's a stdlib-internal carrier. Use `Box(T)` or `[T]`.
- **No dropping linear values.** Passing by `let` does not discharge the obligation — only `take` does.

### File structure

- **`spec` invocations cannot appear inside a function body** — top-level only.
- **A type referencing `Vec_i64` requires `spec std.collections.vec.Vec(i64)` earlier in the file.** Order: imports → spec invocations → derive → types → functions.

---

## Code Quality

- **Control flow** — early returns; nesting ≤ 4; bound recursion with `decreases` or admit `divergence`.
- **Size** — function ≤ 80 lines; file size governed by `file_low_cohesion` (fires only on disjoint-cluster / hub-and-spoke shape — mutually-recursive walkers correctly stay one file).
- **Validate at boundaries** — `where` / `requires` at system edges; trust internal callers within the discharged contract; don't re-check compiler-discharged obligations.
- **Smallest scope** — bindings at point of use; chained access ≤ 3 levels (extract intermediates).
- **Errors are explicit** — `handle` or `?`; `let _ = ...` only when the error carries no actionable info.

---

## Build, run, toolchain

Everyday verbs: `edda build` (type-check + refinement-discharge + codegen, emitting `.mir` + `.o` under `target/edda/<triple>/` and regenerating every `index.toon`), `edda check` (type-check only — no refinement discharge), `edda run` (build + link + execute), `edda test`. Distribution and registry verbs: `edda add` / `update` / `audit` / `publish` / `why`, plus `edda contract-diff` (today a package-level contract delta; the per-function diff surface is locked design — see `docs/authoring/guide.md`).

Further verbs exist at varying maturity (`hot`, `bench`, `gc`, `promote`, `demote`, `regenerate`, `clean`, `fmt`, `lint`, `daemon`, `structmap`, `key`); the native driver currently implements `build` / `check` / `run` / `test` / `version` and parses-but-stubs the rest, while the Rust bootstrap carries the wider surface (including `lint --trust-points` and `test --properties`). Expect "not yet implemented" on some paths and consult `docs/authoring/guide.md` for per-feature status.

Output trees under `target/` are build artifacts — never commit them.