Skip to content

Mighty Language Specification v1.0 (Release Candidate 5)

Status: v1.0-RC5 — released alongside v0.24 (2026-05-26). Promotes RC4 to RC5 by absorbing the capability surfaces that landed in v0.20..v0.23 into normative prose. The freeze gate (eight RFC comment windows tracked at docs/spec/rfcs/RFC_DASHBOARD.md) is the only remaining blocker for v1.0 GA. RC5 contains no breaking changes vs RC4 — every addition is descriptive of behaviour that already ships in the v0.20..v0.23 toolchain.

RC5 deltas vs RC4:

  • §11.1.2 — Resumable trait and the hot-reload swap pipeline promoted to normative (the v0.20 + v0.21 Tier 1.5 work). Adds the new MT506x diagnostic band reference.
  • §11.7 — new normative subsection on mty serve [--port] [--watch]
  • mty reload <agent-type> --from new.wasm control surfaces.
  • §22.5 — mty:web/canvas@0.1 and mty:web/input@0.1 WIT interfaces promoted to normative (the v0.23 Track A work).
  • §25.8 — cluster mesh primitives promoted to normative (the v0.18 transport, v0.19 routing, v0.20 mTLS + Tier 4.2 supervisor, v0.21 Tier 4.3 lossless live migration work). Adds the MT503x and MT507x diagnostic bands and AgentAddr = node:type:pid.
  • §27.1 — std.web module row added.
  • §32 — conformance suite table updated to the 24-category / 153-case shipping shape, cross-linking to the new tests/conformance/v1.0-NORMATIVE.md case-classification document.
  • §20.6 — format!() builtin macro promoted to normative. v0.24 Track B shipped the expander + std.fmt runtime contract + MT6009 / MT6010 diagnostic codes. Bare-{expr} string interpolation remains DEFER-V1.1.
  • §A.1 / §A.2 — FROZEN matrix extended to call out cluster mesh, hot reload, std.web, and format! as v1.0 FROZEN; bare string interpolation recorded in §A.2 as a DEFER-V1.1 line item.

Previous status: v1.0-RC4 — released alongside v0.18 (2026-05-26). Promoted RC3 to RC4 by amending §9.2's effect-row grammar to admit the multi-row-variable tail form (RowTail ::= '|' RowVar (',' RowVar)*) that the v0.18 parser ships, and adding the new accepted shapes to the §9.2 dispatch table. No behavioural change for single-row-var signatures; multi-var signatures previously rejected at parse time now parse as Vec<HirRowVar> and lower (single-var-equivalent) at the HIR layer pending the v0.19 multi-var lowerer (see RFC-008).

Previous status: v1.0-RC3 — released alongside v0.12 (2026-05-25, spec polish slice). Promoted the RC2 normative spec to RC3 by closing the three gaps surfaced during v0.11 (operator precedence; six constructor-only typeck codes; missing package/export/requires keywords) and the sixteen ambiguities found by the Python 2nd implementation. RC3 superseded RC2 (v0.9–v0.11) with no normative behaviour change; the diff was restricted to:

  • A new normative §11.1.1 operator-precedence table (replaces the former cross-reference to the non-normative docs/internals/parser.md).
  • §3.3 split into "reserved keywords" + "contextual keywords" + "reserved for future use", with package, export, requires, and 17 other lexer keywords added to the reserved list.
  • §3.2 / §3.4 / §3.5 prose tightening to close the 16 lexer-level ambiguities recorded in dev/history/notes/PYTHON_IMPL_V0_11_NOTES.md.
  • §4 / §10.1 / §13.1 / §16 / §21 minor clarifications for the parser-level findings (fn = <expr> body shorthand; mixed newline/comma field separators; inline arena LABEL : <expr>; optional msg prefix on protocol messages; key value and key = value both accepted in sandbox / budget; requires clauses on unsafe fn).
  • Per-code RC3 disposition for the six FROZEN typeck codes whose emit-sites have not yet landed (see SPEC_RC3_V0_12_NOTES.md).

RC2 baseline: v1.0-RC2 (v0.9 spec-freeze prep). RC2 in turn superseded RC1 (v0.8) by:

  • Resolving the 10 OPEN amendments left by RC1 (3 promoted to FREEZE-MVP, 7 retained as DEFER-V1.1 with explicit RFC cross-references; 1 — A100 — kept FROZEN with its v1.1+ residual tracked via RFC-004).
  • Shipping six first-draft RFCs under docs/spec/rfcs/ covering the architecturally-significant v1.1+ promotion paths.
  • Adding a "v1.0 stability surface" promotion of §A.1 prose.
  • Adding a "v1.1 promotion targets" cross-reference column in §A.2.
  • Appending an "RFCs by amendment" subsection to Appendix C.

Predecessor: docs/spec/v0.1.md (stub) + docs/spec/v0.1-amendments.md (88 amendments with per-amendment **Status:** classifications, RC2 values).

Change log: docs/spec/CHANGELOG.md.

Scope decisions: SPEC_CONSOLIDATION_V0_8_NOTES.md (RC1 baseline) + SPEC_FREEZE_V0_9_NOTES.md (RC2 deltas, OPEN-amendment resolutions, v1.0 freeze plan) + SPEC_RC3_V0_12_NOTES.md (RC3 deltas, Python-impl ambiguity dispositions, per-code FROZEN typeck plan).

Reading instructions. This document is the normative reference for Mighty at the v1.0 release candidate. It is self-contained: a reader does not need to load v0.1.md or the amendments file to use it. Where a section references an amendment (e.g. A55) the citation is for traceability only; the rule itself is stated in this document.

Table of contents

§1 Naming and brand history

The language is named Mighty. The official toolchain binary is mty. Source files use the extension .mty; interface (re-export) files use .mtyi. The manifest filename is mighty.toml and the lockfile is mighty.lock. Diagnostic codes use the prefix MT (for example MT3009).

The language was originally named Stardust with binary sdust, extension .sd, manifest star.toml, and diagnostic prefix SD. The rebrand to Mighty landed in v0.7.0-rebrand (commit chain b83673a..36b3140, dated 2026-05-23) and includes:

  • Source extension .sd → .mty. Source files using .sd continue to compile through any v0.x → v1.0-RC compiler that ships with the bilingual lexer; v1.0 stable will keep the .sd reader for at least one major release before considering removal.
  • CLI binary sdust → mty. The sdust binary alias is no longer shipped; existing scripts must update.
  • WIT package namespaces stardust:caps/* and stardust:web/* → mty:caps/* and mty:web/*. Hosts importing the old names need a shim (see REBRAND_NOTES.md).
  • Diagnostic codes SDxxxx → MTxxxx. The mty explain CLI accepts both MT0001 (canonical) and SD0001 (legacy alias) so historical bug reports and external docs remain navigable.

The GitHub repository has since been renamed to hassard0/Mighty (the on-disk directory may still be stardust for historical continuity). The package edition string "2026" is a calendar year identifying the syntactic revision of the language, not a brand identifier; it stays unchanged across the rebrand.

The mty-ir crate carries the MtyIR mid-level intermediate representation; the historical internal name "SIR" survives as the --ir flag's --sir alias on the mty dump subcommand.

History capsule. Stardust v0.1 (slices 1..8) walked the spec §31 ladder end-to-end. v0.2 lit up every surface the v0.1 deferral list named. v0.3 hardened soundness (NLL, OTLP, slab pool, mid-turn cancel). v0.4 was dogfood + ecosystem (registry, package manager, macros). v0.5 was self-hosting (lexer) + dogfood completion + LSP advanced. v0.6 added the multi-core scheduler, first honest benchmarks, and self-host parser. v0.7 was the brand rename. v0.8 is this consolidation.

§2 Design goals

Mighty is a statically typed, ownership-based, agent-first systems language that compiles to native code and to WebAssembly Components.

The four pillar goals shape every normative decision in this spec:

  1. Determinism by construction. Same source + same inputs + same seed must produce the same observable behaviour, byte-for-byte (see §25.5, A35, A39).
  2. Soundness over convenience. Ownership, borrowing, capabilities, and effects are enforced statically with extensive run-time backup (per-call FsCap, mem charging, mailbox depth). The compiler rejects code that cannot be proven sound rather than degrading guarantees (see §7, §16).
  3. Agent-first concurrency. Concurrency is not bolted on. Agents, protocols, supervisors, mailboxes, deadlines, and budgets are first-class syntactic constructs (see §12, §14).
  4. One compiler, many targets. Native (Cranelift/LLVM), WebAssembly Components, and a fast interpreter share one front-end. The core/edge/web/host profiles select capability surfaces, not languages (see §30).

Two supporting design rules apply throughout:

  • Token-efficient syntax (see §28) — the language is shaped to be cheaply produced and read by LLM agents as well as humans.
  • Capability-first authority — every effectful surface (network, filesystem, clock, DOM, model) is mediated by a typed capability handle. No ambient authority.

§3 Lexical structure

§3.1 Encoding

Source files are encoded in UTF-8. A leading BOM is rejected. Line endings may be LF or CRLF; the lexer normalises CRLF to LF before tokenisation. The recommended file extension is .mty; the historical .sd extension remains accepted by the v1.0 compiler.

§3.2 Comments

Three comment forms:

Syntax Meaning
// rest of line line comment
/* ... */ block comment; nesting allowed
/// rest of line doc comment, captured into the item's API doc-string

Diagnostics:

  • An unterminated /* ... */ (whether nested or not) emits MT0004 unterminated_block_comment at lex time. The lexer recovers by treating everything from the unmatched /* to end-of-file as comment trivia.

Doc-comment disambiguation:

  • A line starting with exactly three / characters is a doc comment (/// docs here).
  • A line starting with four or more / characters is an ordinary line comment (//// banner). It is NOT captured into the API doc.

This rule lets users write banner-style comment dividers without accidentally producing dangling doc-strings.

§3.3 Identifiers and keywords

IDENT = (XID_Start | "_") (XID_Continue | "_")*

Identifier characters follow Unicode UAX-31 XID_Start / XID_Continue. ASCII underscore (_) is permitted in either position. The leading underscore alone (_) is a special discard-pattern token in pattern position; everywhere else it is an identifier.

The keyword set splits three ways: reserved (always lex as keywords), contextual (parsed as keywords only in specific positions), and reserved for future use (the spec reserves the name but the v1.0 lexer accepts them as ordinary identifiers).

§3.3.1 Reserved keywords (v1.0)

The lexer always tokenises these as their keyword kind, never as IDENT:

agent      arena      as         async      await      backoff
break      budget     cap        child      const      continue
derive     detach     dyn        effect     else       enum
export     extern     false      fn         for        if
impl       import     in         join       let        loop
macro      match      mod        move       mut        on
on_fail    package    protocol   pub        ref        requires
restart    return     run        sandbox    scope      self
spawn      state      struct     sup        task       trait
true       type       unsafe     up_to      use        where
while      with       yield

Total: 63 reserved keywords (including the two boolean literals true / false, which lex as TRUE_KW / FALSE_KW rather than as identifiers). Sourced from crates/mty-syntax/src/syntax_kind.rs — the #[token("...")] entries; this list is the v1.0 normative contract.

The reserved name Self (uppercase) is recognised only in type position as the implementing-type sigil inside impl / trait / agent bodies. The lexer emits it as IDENT and the parser routes it; it is not in the reserved table above.

§3.3.2 Contextual keywords

These words are ordinary identifiers in most positions; the parser upgrades them to keywords only in the context listed:

Word Context
proc Item start when immediately followed by macro — begins a proc macro declaration (A94, §20.3).
supervisor Item start — interchangeable with the reserved keyword sup for declaring a supervisor item.
component After extern — selects the Wasm-component extern form (extern component "wasi:...", §17.2).
v0 v1 v2 … After a protocol Name header — optional protocol-version tag (§13.3).

Outside the listed context, each word is a normal identifier and may be used as a variable, function, parameter, field, or type name.

§3.3.3 Reserved for future use

The following names are not v1.0 keywords (the lexer accepts them as identifiers), but the spec reserves them for potential v1.x extensions. An implementation MAY warn when these appear as identifiers; it MUST NOT reject them:

and       deinit    init      or        panic     static    union

and / or are reserved against a future Python-style spelling of the short-circuit logical operators (today these are && / ||). init / deinit are reserved against future explicit constructor/destructor syntax (today these are ordinary method names). panic is reserved against future first-class panic syntax (today it is a function in the prelude). static and union are reserved for v1.x storage-class and untagged-union extensions.

§3.3.4 Keyword-tolerant positions (A3, A4)

A small number of positions accept keyword tokens as if they were identifiers, so that library APIs can use reserved words without forcing callers to use raw-identifier escapes:

  • After . in expression position, any keyword token is accepted as a method or field name. dom.on("click", h) and agent.spawn() parse without escapes.
  • In an effect clause, any keyword token is accepted as an effect name (effect net, model, spawn).

This tolerance does NOT extend to top-level declaration position (you cannot name a function fn return() { ... }).

§3.4 Literals

§3.4.1 Integer literals

Decimal, hexadecimal, octal, and binary forms, optionally with an underscore digit separator and a type suffix:

INT_LITERAL = (DEC | HEX | OCT | BIN) ("_" (DEC | HEX | OCT | BIN))* SUFFIX?
SUFFIX      = ("u" | "i") ("8" | "16" | "32" | "64" | "128" | "size")

Underscore placement rules (codified in RC3):

  • A leading underscore is forbidden by the production (an underscore before the first digit-group makes the token lex as an IDENT, not an INT_LITERAL).
  • A trailing underscore at end-of-literal (1_) is rejected with MT0006 malformed_numeric_literal.
  • Two consecutive underscores (1__2) are rejected with MT0006.
  • Any number of internal single-underscore separators between digit groups is allowed (1_000_000, 0xff_ff_ff).

Unsuffixed integer literals carry the inference shape IntInfer, which unifies permissively with any concrete integer kind via context. After each typed body settles, an explicit defaulting pass rewrites any remaining IntInfer to I32 and FloatInfer to F64 (A19, closes A8). Diagnostics still surface unresolved literals as {integer} when inference fails before the pass.

§3.4.2 Float literals

FLOAT_LITERAL = DEC "." DEC (EXP)? ("f32" | "f64")?

§3.4.3 String and byte literals

UTF-8 string literals ("..."), raw strings (r"...", r#"..."#), byte strings (b"..."), and character literals ('c') per the usual escape grammar.

html"..." is a tagged template form that lowers to a structured DOM fragment value (see §22). At lex time the entire html"..." blob (with inner { and } paired-balanced) emits as a single HTML_LITERAL token; the splitting of inline {name} interpolation placeholders into fragment + identifier sub-tokens is v1.0 OPEN — deferred to v1.1+ (candidate amendment A110, tracked in SPEC_RC3_V0_12_NOTES.md). Until A110 lands, implementations should preserve the original source slice between the quotes for later re-parsing.

§3.4.4 Size literals

SIZE_LITERAL = \d+ (B | KiB | MiB | GiB | k | M)

Binary prefixes KiB/MiB/GiB multiply by 1024 / 1048576 / 1073741824 respectively. Decimal prefixes k and M multiply by 1000 and 1000000 respectively (A1). Lowercase k and uppercase M avoid collision with the duration suffix m (= minutes). Uppercase K is reserved for a future amendment (likely as an alias of KiB); the v1.0 lexer does not consume K as part of a size literal. A literal followed by K therefore lexes as two tokens: an INT_LITERAL and an IDENT (e.g. 5K is INT_LITERAL 5 + IDENT K). Implementations MUST NOT emit a lex-time diagnostic for this case.

Suffix recognition is opt-in: the lexer only consumes a size-suffix letter if it appears in the allowlist above. Any other trailing alphabetic run lexes as a separate IDENT token, with the parser deciding whether the resulting token sequence is meaningful.

§3.4.5 Duration literals

DURATION_LITERAL = \d+ (ns | us | ms | s | m | h)

The token represents a Duration value (see §6.1). The duration suffix m (= 60 seconds) is the reason the size suffix k is lowercase (A1).

§3.5 Punctuation

Standard punctuation per the parser grammar in docs/internals/parser.md. Notable disambiguators:

  • Turbofish (A2): Path::[T1, T2] in expression position carries generic arguments without colliding with Path[index]. Type position retains Path[T1, T2]. Examples: 
    let m = Map::[Str, Json]{}
let s = Some::[I32](42)
  • Postfix ? and ! (A12): the propagate operator (expr?) and the ask/send sugar (expr?Msg(args) / expr!Msg(args)) require their Msg identifier on the same source line. A newline between the postfix and the next identifier disambiguates as plain propagate/boolean-not.

The "same source line" check is computed over all trivia between the postfix token and the next non-trivia token — including whitespace AND comments. A // ...\n line comment between ? and Msg therefore introduces a newline and forces the bare-propagate interpretation, just as a literal \n would. Implementations must not look past the trivia to find a "same-line-by-some-other-rule" identifier. - Macro invocation marker (A90): name!(args) invokes the declarative or procedural macro name. A bare name(args) is a function call. The marker prevents an unresolved foo(...) from silently being interpreted as a macro miss.

§4 Program and module structure

A Mighty source file (.mty) contains a sequence of top-level items. Item kinds:

ITEM := PACKAGE | USE | MOD | FN | STRUCT | ENUM | TRAIT | IMPL
      | AGENT | PROTOCOL | SUPERVISOR | CAP | SANDBOX
      | EXTERN_BLOCK | EXPORT | MACRO | PROC_MACRO
      | CONST | STATIC | DERIVE | TYPE_ALIAS

A package (a directory containing a mighty.toml) groups files into a single module tree. The default entry point is src/main.mty for binary packages and src/lib.mty for library packages.

§4.1 package declaration

A source file MAY begin with a package <path>; declaration giving the file's logical package path. Examples:

package search_api
package counter_web

The trailing semicolon is optional. If present, package MUST be the first non-trivia item in the file. The declaration is informational for tooling; the canonical package name still comes from mighty.toml.

§4.2 use and mod

use otherpkg.path imports symbols. Module paths use . as the separator (std.http, mighty:web/dom).

mod name { ... } declares an inline module. mod name; declares an external module loaded from name.mty or name/mod.mty.

§4.3 Visibility

pub makes an item visible to other modules; pub(crate) restricts to the same package.

§4.4 Function bodies — block form and = <expr> shorthand

Function items have two body forms:

fn add(a: I32, b: I32) -> I32 { a + b }   // block form
fn add(a: I32, b: I32) -> I32 = a + b      // expression shorthand

The expression shorthand fn NAME(...) -> T = <expr> is exactly equivalent to fn NAME(...) -> T { <expr> }. It is the canonical form for single-expression bodies (in particular export c fn / export js fn exports often use it).

A trailing ; after the shorthand body is accepted but optional.

§4.5 Field and entry separators

Inside braced bodies that list a sequence of items (struct fields, enum variants, sandbox entries, budget entries, agent state fields, protocol message declarations), the spec accepts either:

  • a comma (,), or
  • a line break

between adjacent entries. A single body MAY mix the two separators. A trailing separator before the closing brace is permitted but not required. Whitespace runs that contain no separator (and no newline) are an error.

Example (struct with newline-separated fields):

struct User {
    id: UserId
    name: String
    created: Instant
}

Example (same struct with commas):

struct User {
    id: UserId,
    name: String,
    created: Instant,
}

Both are well-formed.

§5 Names, scopes, and visibility

§5.1 Scope kinds

Every lexical scope is one of (A65):

  • PermissiveScope — unknown single-segment value names resolve to fresh inference variables, allowing canonical examples to compile while later passes harden the surface.
  • StrictScope — unknown single-segment names emit MT2021 unresolved_value.

Scope classification:

Construct Scope kind
Top-level fn body Permissive
extern { ... } body Permissive
Macro body Permissive
unsafe { ... } Permissive
arena { ... } Permissive
budget { ... } Permissive
sandbox Name with { ... } { ... } Permissive
agent { ... } body Strict
on Msg(p) { ... } handler Strict
Supervisor body Strict (open)
Capability narrow body Strict (open)

Strict-but-open scopes (supervisor, cap-narrow) currently keep tolerance_open = true for ergonomic compatibility with externally provided caps; the toggle activates MT2021 automatically when the runtime gains first-class supervisor bindings.

§5.2 Per-body tolerance set

Strict scopes accept unknown names that appear in the per-body tolerance set:

  • Agent body: state field names, ctor-param names, sibling-method names.
  • Handler body: parameters from the protocol declaration and the agent's tolerance set.

Multi-segment paths (mod.fn, OpaqueAdt.method) whose first segment resolves to a known module / opaque ADT / local / tolerated identifier also pass without MT2021.

§5.3 Resolution order

For a single-segment name:

  1. Local bindings in the active block (innermost first).
  2. Function parameters.
  3. Agent state and ctor parameters (if in agent context).
  4. Tolerance set (in strict scope) or fresh-var fallback (in permissive scope).
  5. Module-level items visible via use imports.
  6. Prelude items (log, panic, spawn, Some, None, Ok, Err).
  7. Otherwise MT2021 (in strict scope) or fresh inference variable (in permissive scope).

§6 Type system

§6.1 Primitive types

Kind Members
Bool Bool
Integer I8 I16 I32 I64 I128 U8 U16 U32 U64 U128 ISize USize
Float F32 F64
Character Char (Unicode scalar value)
String Str (slice), String (owned heap string)
Byte slice Bytes
Unit Unit
Duration Duration
Size Size (memory-byte count, distinct from USize)

Primitive type names live in both the type and value namespaces (A9): String("hello") calls the String constructor, and let x: String = ... annotates a binding. The opaque-ADT representation in the prelude means value-position references to primitives that lack a real constructor resolve to fresh inference variables rather than hard errors.

§6.2 Composite types

  • Struct — struct Point { x: F64, y: F64 }.
  • Enum — enum Json { Null, Bool(Bool), Num(F64), Str(String), Arr(Vec[Json]), Obj(Map[Str, Json]) }.
  • Tuple — (I32, Str).
  • Array — [T; N] (fixed-size, stack/arena allocable).
  • Vec — Vec[T] (heap-backed growable, allocates on push; push, pop, and clear mutate an addressable receiver when used as statements or as value-producing method calls).
  • Map — Map[K, V] (heap-backed hash map).
  • Reference — &T (shared), &mut T (unique).
  • Raw pointer — *T, *mut T (unsafe, see §21).

§6.3 Result and Option sugar

Result[T, E]   // canonical sum
T!E            // sugar for Result[T, E]
T!{A, B, C}    // anonymous error union (v1.0: lowers to Result[T, Error] sentinel)
Option[T]      // canonical Option

T!E is the primary error-carrying form. T!{A, B, C} is an anonymous error union: v1.0 ships it as a parser-accepted form that lowers to Result[T, Error] where Error is the poison sentinel that unifies with any concrete error (A11). First-class union ADTs are v1.0 OPEN — deferred to v1.1+.

§6.4 Generics

fn map[T, U](xs: Vec[T], f: fn(T) -> U) -> Vec[U]

Bounded generics use a where clause:

fn hash_all[T: Hash](xs: Vec[T]) -> Vec[U64] where T: Eq { ... }

See §18 for the full constraint algebra.

§6.5 Type inference

Two-stage:

  1. HM-style unification over expressions in each fn body (slice 3).
  2. Defaulting pass (A19): any remaining IntInfer becomes I32 and any remaining FloatInfer becomes F64 after the body type-checks.

Diagnostics surface unresolved inference variables as Var{n} or {integer}. The defaulting pass guarantees no IntInfer/FloatInfer escapes the type checker into downstream consumers (borrow checker, codegen, LSP).

§6.6 Type-position vs value-position

Generic argument syntax differs by position (A2):

  • Type position: Map[K, V], Result[T, E], Vec[T].
  • Value position: Map::[Str, Json]{}, Some::[I32](42), Vec::[T]::new().

The double-colon turbofish in value position disambiguates from Path[index].

§6.7 Trait coherence

At most one impl Trait for Type per (trait, self-type) pair (A24). Duplicate triggers MT4022 trait_coherence_violation. Generic-argument overlap detection (impl Hash for Vec[T] vs impl Hash for Vec[U64]) is v1.0 OPEN — deferred to v1.1+.

§6.8 Object safety

A trait used as dyn Trait is object safe iff none of its declared methods (A25):

  • mention Self in any parameter or return type, AND
  • have method-level generic parameters.

Violation: MT4023 dyn_requires_object_safe.

§6.9 Derive

#[derive(...)] is the canonical form (A26). A leading-keyword shorthand derive Trait is also accepted to ease LLM-generated source. v1.0 supports:

Derive Requirement
Copy every field's type must itself be Copy
Hash (none; impl is synthesised as marker)
Eq (none; impl is synthesised as marker)
Sendable (none; impl is marker; A65.b enforces field-shape per use site)

Unknown derive names trigger MT4041 derive_unknown. derive(Copy) field-failure: MT4040 derive_copy_field_not_copy.

§7 Ownership, borrowing, and lifetimes

§7.1 Affine types

Every owned value has an affine type: it is consumed exactly once. Re-using a moved value triggers MT3001 use_after_move. The Copy set (A13, A26) admits cheap-to-duplicate types that opt out of the single-consumption rule:

  • All primitives (Bool, integers, floats, Char, Unit, Duration, Size).
  • Shared references &T, raw pointers *T, function pointers.
  • Str slices (NOT the owning String).
  • Tuples and arrays of Copy elements.
  • User types annotated #[derive(Copy)] whose every field is Copy (A26 enforced via MT4040).
  • Opaque prelude ADTs (Url, Page, Logger, agent types) — these are treated as Copy in v1.0 to keep canonical examples ergonomic; a real per-type registry replaces the blanket rule in v1.1+.

Not Copy: &mut T, raw mut pointers, user-declared structs/enums without the derive, String, Bytes, capability handles (Net, Fs, Clock, Dom, Model), Param/Var parameters.

§7.2 Borrowing

&x produces a shared reference; &mut x produces a unique mutable reference. The standard XOR aliasing rule applies: while &mut x exists, no other reference to x (or any overlapping projection) may exist; while any &x exists, no &mut x may exist.

§7.3 Place algebra (A54)

The borrow checker tracks aliasing per Place, not per whole local:

Place := { root: String, projs: Vec<Proj> }
Proj  := Field(name) | Index | Deref

Two places overlap iff one is a prefix of the other. Disjoint fields (s.a vs s.b) coexist as concurrent borrows.

v1.0 conservatism (A54): Place projections truncate at depth 1 — s.a.b folds to s.a for conflict purposes. Index projections collapse to a single "any index" projection: arr[i] and arr[j] conflict. Lifting the truncation is v1.1+.

§7.4 NLL last-use deactivation (A55)

A borrow's lifetime ends at the last use of its borrower binding in source order, not at the end of the lexical block (A55, supersedes the lexical-region rule A20):

let r = &x          // borrow active
read(r)             // last use of r
let m = &mut x      // OK — r's region ended

Algorithm:

  1. Pre-pass assigns a monotone ProgramPoint to every Path expression and records the highest point each name appears at.
  2. Main walker advances current_point on each Path read. After each use, borrowed regions decay if current_point >= last_use[name].

Approximation level: not Polonius. v1.0 does NOT model:

  • Two-phase borrows
  • Borrows held on one branch of a diamond (ledger join is conservative)
  • Loop back-edge borrows beyond fixed-point detection (A82)

These limits are v1.0 OPEN — flagged for v1.1+.

§7.5 Loop back-edge fixed-point (A82)

Loop bodies (loop, while, for) walk the borrow checker through a bounded fixed-point: up to 16 iterations join the post-body borrow-ledger state into the pre-body baseline via the same conservative joins used at if/match. Convergence is detected as ledger record count stability across two passes.

§7.6 Move of dereferenced ref (A29, A56)

A move via deref of a reference to a non-Copy value emits MT3009 move_out_of_ref:

let r: &Box[I32] = &b
let x = *r          // ERROR MT3009 — non-Copy move via deref

If inner is Copy, let x = *r loads through the ref (no error).

Code Cause Fix
MT3001 Use of a value already moved Clone earlier, or borrow instead
MT3008 Move out of a value currently borrowed Wait for the borrow to end
MT3009 Move via deref of a reference (non-Copy) Clone, take ownership, or borrow

§7.7 Destructors and Drop

Owned values implement Drop to run cleanup at end-of-scope. Drop order is reverse declaration order within a block. Arena-allocated values do NOT run individual Drop; the arena's bulk-free supersedes (see §10).

§7.8 Sendable (A14, A65.b)

A type is Sendable iff every cross-agent message-arg site can guarantee its bytes can be copied or moved into another agent without violating any aliasing or capability invariant.

v1.0 Sendable definition (A65.b, supersedes the slice-4 A14 set):

  • Copy types (other than references and raw pointers) — yes.
  • Owned, Sized values with no internal references (String, Bytes) — yes.
  • Tuples / arrays where every element is Sendable — yes.
  • User ADTs marked #[derive(Sendable)] whose every field is Sendable — yes.
  • References (&T, &mut T), raw pointers, function pointers, capability handles (Net/Fs/Clock/Dom/Model), dyn Trait objects, anything transitively containing one — no.
  • Generic / unbound types — permissive at the check site (rely on monomorphic call sites or downstream propagation).

Cross-agent message-arg sites are target!Msg(args) and target?Msg(args). Non-Sendable args emit MT3011 non_sendable_message_arg with a human-readable note ("contains a &T reference", "capability handle Fs does not cross agent boundaries", etc.).

§7.9 Arena escape (A15)

Spec-level rule: values allocated inside an arena MUST NOT escape the arena's lexical scope unless they are copied, moved through an allowed promotion, or returned as owned values independent of the arena.

v1.0 direct-naming enforcement (A15): if an arena body's tail expression is a path whose root binding is an arena-local non-Copy local, the compiler emits MT3010 arena_escape. Indirect flow (an fn that captures and returns the arena value) is v1.0 OPEN: the runtime backstop trap MT5007 arena_escape_runtime is reserved for v1.1+ allocator-tracked enforcement.

§8 Capabilities

Capabilities represent runtime authority (network, filesystem, clock, DOM, model). No ambient authority: every effectful operation requires a capability handle.

§8.1 Capability types

TyData::Cap { family: CapFamily, constraint: CapConstraint }
CapFamily Effects
Net net
Fs fs
Clock time
Dom dom
Model model
Custom(name) user cap Foo declarations (parsed, typing v1.1+)

§8.2 Constraints (A23)

Variant Meaning
Any top — no restriction
ReadOnly read-only narrowing (Fs only in v1.0)
Path(p) path-prefix glob — accepts only paths under p
Host(xs) network host:port allowlist
And(xs) conjunction — every sub-constraint must hold

§8.3 Narrowing constructors

Built-in narrowing methods (A23):

Method Result constraint
cap.ro(path) And([ReadOnly, Path(path)]) (Fs only semantically)
cap.path(path) And(existing, Path(path))
cap.host(host) And(existing, Host([host]))

§8.4 Subsumption

narrower.is_narrower_or_eq(broader):

  • Any accepts anything.
  • Identical constraints are equal.
  • Path(a) ⊑ Path(b) iff a.starts_with(b).
  • Host(a) ⊑ Host(b) iff every host in a appears in b.
  • ReadOnly ⊑ ReadOnly.
  • And(xs) ⊑ c iff any x in xs is narrower than c.

Call-site enforcement: passing a Cap of the same family but broader constraint than the parameter expects emits MT4010 capability_too_broad.

§8.5 Caps are affine and non-Sendable

Capability handles are non-Copy and non-Sendable. They participate in move/borrow tracking like any other affine value. Passing a raw Fs or Net into a cross-agent message fires MT3011 with a guidance note (see §7.8).

§8.6 Per-call FsCap isolation (A100, A109)

sdust_stdlib::fs::{read, write, exists, list_dir} each accept cap: &FsCap per call. v1.0 guarantees two FsCap values with disjoint allowlists, exercised in the same process, never leak across the divide (A109 pins this contract with a test).

A process-wide default cap acts as a stop-gap (A100): host::dispatch consults current_default_read_cap() / current_default_write_cap() when no per-call cap is materialised. IoErr::Forbidden(path) is returned for denied accesses; IoErr::Denied(path) for caps that exist but do not include the path.

Per-call cap materialisation from the sandbox manifest at the MtyIR lower is v1.0 OPEN — deferred to v1.1+.

§9 Effects

Effects describe observable authority and runtime behaviour. v1.0 effect set:

alloc  net  fs  time  dom  model  spawn  unsafe

Reserved for future use: io, rand, block.

§9.1 Inference (A22)

Bottom-up + fixpoint over the call graph:

  1. Per-fn pass: walk every fn body and record the syntactic effect set:
  2. arena ... → alloc
  3. spawn ..., target!Msg(...), target?Msg(...), detach → spawn
  4. expr @ duration → time
  5. unsafe { ... } → unsafe
  6. html"..." template → alloc
  7. Map literal → alloc
  8. Path-prefix receivers/path-callees fs., net., clock., dom., model. → the corresponding cap effect
  9. Container method names (push, pop, insert, encode, collect, clone, to_string) → alloc
  10. Fixpoint pass: until no set changes (bounded at 32 iterations), for each fn, union the callees' inferred and declared effect sets.
  11. Public-fn discipline: if a pub fn's inferred set is non-empty, verify the declared effect ... clause is a superset. Else MT4001 effect_undeclared.
  12. Profile gate: under profile = "core" (A30, A65.d), any pub fn with alloc in its inferred set triggers MT4002 alloc_in_core.

§9.2 Effect declarations

fn fetch(url: Str, n: &Net) -> Page!NetErr effect net { ... }

fn main(...) -> ... effect net, model, spawn { ... }

Effect names accept keyword tokens (A4). Declaration-vs-inferred subset checking applies at the pub fn boundary.

§9.2.1 Effect rows (RFC-008, v0.15 parser / v0.16 typeck)

v0.15 extends the effect-clause grammar with row variables so that higher-order functions can thread a closure's effects through to the return type (RFC-008). The new productions:

EffectClause ::= 'effect' EffectList RowTail?
               | '!' EffectSet
               | '!' RowVar

EffectSet    ::= '{' EffectList? RowTail? '}'
EffectList   ::= EffectName (',' EffectName)*
RowTail      ::= '|' RowVar (',' RowVar)*          # multi-var since RC4 / v0.18
RowVar       ::= Ident                # convention: single capital, e.g. `E`
EffectName   ::= Ident                # convention: lowercase, e.g. `fs`, `net`

Accepted shapes:

Form Meaning
effect fs, net legacy closed row (existing)
effect fs, net \| E concrete + row tail (v0.15 NEW)
effect fs, net \| E, F concrete + multi-row tail (RC4 / v0.18 NEW)
!{} empty closed row
!{fs, net} concrete closed row
!{fs \| E} concrete + row tail
!{fs, net \| E} multiple concrete + row tail
!{fs \| E, F} concrete + multi-row tail (RC4 / v0.18 NEW)
!{\| E, F} row-only multi-row tail (RC4 / v0.18 NEW)
!E bare row variable

A trailing comma after the last RowVar is rejected — !{| E,} is a parse error. The legacy T!{NetErr, ParseErr} error-union sugar disambiguates from the new multi-row form via the leading | token: any !{...} whose first inner token is | is unambiguously a row-only tail.

Disambiguation with anonymous error unions (A11). The legacy T!{NetErr, ParseErr} error-union sugar shares the !{ ... } lexeme. The parser distinguishes them by the first ident's case (and by the presence of |):

  • !{Ident, ...} where the first ident is uppercase AND no | appears → anonymous error union (legacy A11 behaviour).
  • !{Ident, ...} where the first ident is lowercase, OR a | appears at depth 0 → effect-row clause.
  • Bare !Ident (no braces) on a path-type return type → ALWAYS error sugar, to preserve !FetchErr etc. Users who want a bare row var on a path return type must use the braced form (Foo !{| E}) or the effect ... | E keyword form.

Implementation status (RC4 / v0.18). Parsing of row variables shipped in v0.15; the multi-row-variable tail (| E, F, ...) ships in v0.18 (crates/mty-syntax::parser::types::effect_row_tail). The CST exposes EFFECT_SET, EFFECT_NAME, EFFECT_ROW_TAIL, and one EFFECT_ROW_VAR node per declared row variable; consumers iterate .children().filter(EFFECT_ROW_VAR) uniformly to read the full set. Typeck shipped in v0.16; HirEffectRow::Open(concrete, _) broadened its second field from HirRowVar to Vec<HirRowVar> in v0.17 end-to-end at the HIR + typeck layers. The HIR lowerer is still single-row-var (reads the first EFFECT_ROW_VAR only) pending the v0.19 lowerer broadening; multi-var source signatures parse cleanly today and collapse to a single row var at HIR. Diagnostics MT4055–MT4059 (declaration ambiguity, concrete + inert row, MT4057 single-row signed-effect mismatch, MT4058 call-site arity, MT4059 caller closed-row rejects closure effects) all actively emit as of v0.17/v0.18 with MT4059 enabled once the multi-var parser shipped.

§9.3 Limitations

  • Capability-style call detection is a path-prefix heuristic on the receiver expression — let alias = net; alias.get(...) would not contribute net today. Refinement to typed dispatch is v1.0 OPEN.
  • Recursion via dyn Trait method calls does NOT propagate effects through the dyn (slice 5 keeps dyn effect-free to avoid pessimistic over-tagging).

§10 Arenas and the agent-local heap

§10.1 Arena scopes

Two surface forms are accepted:

arena {
    let big = Vec::[F64]::with_capacity(1_000_000)
    process(big)
}   // arena bulk-frees here

arena turn: lower(parse(tokenize(input))?)   // inline form

The braced form arena [LABEL] { <stmts> } opens an arena scope containing a statement sequence; the inline form arena LABEL : <expr> is exactly equivalent to arena LABEL { <expr> } and is the canonical shorthand for single-expression arena scopes (typically used in turn-handler bodies). The label is optional in both forms.

The arena owns every value allocated inside its scope. Scope exit runs no individual Drop; the arena's bulk-free supersedes (see §7.7).

§10.2 Implementation (A50)

v1.0 ships bumpalo-backed arenas with per-allocation byte-charging (A50, supersedes the slice-7 approximate counter A37):

  • arena {} opens a fresh bumpalo::Bump.
  • Drop of the scope frees every allocation in the frame at once.
  • Allocations are byte-counted against the active BudgetTracker::mem_bytes (see §16).

The Cranelift backend routes ArenaPush / ArenaPop / alloc statements through sdust_runtime::codegen_abi. The slice-6 interpreter keeps its byte-counter for the --legacy-interp path.

§10.3 Agent-local heap

Each agent owns an agent-local heap distinct from all other agents. Cross-agent values cross via Sendable copies (see §7.8) — references are not portable.

§10.4 Memory budget auto-charging (A99)

The MtyIR interpreter charges memory on AdtInit, TupleInit, and ArrayInit rvalue eval via estimate_value_bytes (24 B header + recursive payload estimate). When mem_used > mem_budget the interpreter returns RunResult::MemBudgetExceeded { used, limit } and traps with MT5009.

Entry point: run_fn_with_resource_budget(prog, name, args, host, steps, mem). mem_budget == 0 is the legacy "no cap" sentinel.

§11 Control flow

§11.1 Expressions

if cond { ... } else { ... }
if let Pat = scrutinee { ... } else { ... }
match scrutinee { Pat1 => arm1, Pat2 => arm2, _ => default }
loop { body }
while cond { body }
for pat in iter { body }

if let (A6) and match are unified at the HIR level: the LET_KW presence in IF_EXPR distinguishes the two variants.

§11.1.1 Operator precedence

Expression parsing uses a Pratt-style precedence table. The table below is normative for v1.0 and supersedes any precedence list found in the non-normative docs/internals/parser.md.

Levels go from lowest precedence (binding least tightly) to highest precedence (binding most tightly). Operators on the same row share a level. Associativity is left unless the row is annotated otherwise.

Level Operators Associativity
1 .. ..= (range) left
2 = += -= *= /= %= &= \|= ^= <<= >>= (assignment + compound assignment) right
3 \|\| (short-circuit or) left
4 && (short-circuit and) left
5 == != < <= > >= (comparison) left
6 \| (bitwise or) left
7 ^ (bitwise xor) left
8 & (bitwise and) left
9 << >> (bit shift) left
10 + - (additive) left
11 * / % (multiplicative) left
12 as (type cast) left
13 prefix unary - ! * & &mut move (prefix)
14 postfix .field .method(...) [...] (...) (call) ? (propagate) ?Msg(...) (ask) !Msg(...) (send) @dur (timeout) (postfix)

Notes:

  • Comparison chaining is syntactically left-associative: a < b < c parses as (a < b) < c, then fails the type checker because the inner result is Bool and < is not defined on Bool. Use explicit (a < b) && (b < c) for chained tests. (A future amendment may promote chained comparisons to a parse-time rejection; v1.0 leaves them to the type checker.)
  • Assignment associativity: assignment and compound-assignment are the only binary operators that associate to the right. a = b = c parses as a = (b = c).
  • Postfix ?Msg / !Msg / @dur "same line" rule: the Msg identifier (for ?Msg / !Msg) and the duration literal (for @dur) must appear on the SAME source line as their postfix operator. A newline in the intervening trivia (whitespace or comments) forces the bare-propagate / bare-not / bare-@-error interpretation. See §3.5.
  • Unary - vs subtraction: the lexer always emits a single MINUS token; the parser decides between unary and binary based on left-context.
  • & and &mut: the borrow operator & is a prefix unary at level 13. &mut is a two-token sequence (AMP MUT_KW) treated as a single prefix unary by the parser.

The Rust reference compiler implements this table in crates/mty-syntax/src/parser/exprs.rs::infix_bp (binding-power function). Implementations MAY use any Pratt or precedence-climbing algorithm that yields the same parse trees.

§11.2 Break and continue (A80)

break and continue are first-class HIR nodes:

loop {
    if cond { break }
    if other { continue }
}

let v = loop {
    if done { break value }
}

v1.0 ships unlabelled forms only. Labelled break ('outer: loop { break 'outer }) is v1.0 OPEN — deferred to v1.1+.

Both lower as never for type-check purposes (same as return). The borrow checker walks break value at Position::Move.

§11.3 Iterator protocol (A81)

for x in iter { body } lowers to a wire-protocol method call:

__sdust_iter_next(iter, idx) -> (exhausted: Bool, element: T)

Field 0 drives the loop header's Term::If; field 1 is bound to the loop pattern. The MtyIR interpreter services __sdust_iter_next for ranges (lo..hi, lo..=hi) and arrays. Other receivers return (true, Unit).

Range lowering: lo..hi lowers to TupleInit(lo, hi, inclusive: Bool).

Full trait-based iterators (Iter[T], combinators, user-defined iterables) are v1.0 OPEN — deferred to v1.1+ with the stdlib expansion. The wire protocol is the explicit hand-off so the lowering does not need to change again.

§11.4 Return and never

return e evaluates e and exits the enclosing function. panic(msg) diverges; both return and panic synth as never.

§11.5 Match exhaustiveness (A16)

Non-exhaustive matches emit MT2015 non_exhaustive_match at Error severity (A16 promoted from Warning in slice 4). Add _ => ... to cover the open variants.

§11.6 ? propagation (A7)

expr? propagates Result errors. v1.0 strict rule (A7): the enclosing function MUST return Result[_, _] and the operand MUST be Result[T, E] with E matching the enclosing function's error type. Otherwise:

  • MT2010 question_outside_result — enclosing fn does not return Result.
  • MT2011 question_error_mismatch — error types don't unify.

§12 Agents and mailboxes

Agents are concurrent units with private state, a mailbox for incoming messages, and a handler for each protocol message.

§12.1 Agent declarations

agent Counter {
    state: I32 = 0

    init() -> Counter { Counter { state: 0 } }

    on Inc(by: I32) {
        self.state = self.state + by
    }

    on Get() -> I32 {
        return self.state
    }
}

§12.2 Sending and asking

let c = spawn Counter()
c!Inc(5)              // fire-and-forget send
let n = c?Get()       // ask, wait for reply
let n = c?Get() @100ms // ask with deadline

!Msg(args) posts a message to the agent's mailbox (Sendable-checked per §7.8). ?Msg(args) posts and waits for a reply oneshot. @D attaches a deadline.

§12.3 Mailbox defaults (A40)

Setting Default
Depth 1024 frames
Send policy Block (sender awaits capacity)

Per-agent budgets override via the mb (depth) and mb_policy (Block/Drop/Fail) entries. Under Drop, full-mailbox sends silently discard; under Fail, they return MT5012; under Block, they backpressure.

FIFO ordering of messages is preserved by the mpsc backbone.

§12.4 Slab-pool frames (A72)

Each mailbox is backed by a slab pool of fixed-size payload slots reused via LIFO free-list:

struct Slot {
    inline:   Vec<u8>,             // capacity == inline_bytes (default 64)
    overflow: Option<Box<[u8]>>,    // when payload > inline_bytes
    used:     usize,
}

Pool exhaustion does not block: the frame uses an overflow allocation. Backpressure remains correct because the mpsc still bounds depth; the slab is an allocation amortiser, not a secondary backpressure surface.

§12.5 Agent dispatch model

v1.0 dispatches each agent turn asynchronously through the multi-worker scheduler (see §25):

  1. Worker pops a (agent_id, message) from its local queue or steals from a sibling.
  2. Worker invokes run_handler_isolated for the message in a tokio::task::spawn_blocking context.
  3. The blocking thread races against a cancellation token tied to the per-turn wall budget (A70).
  4. On completion, the agent re-enqueues itself if its mailbox has more messages.

Synchronous dispatch (A32, slice 6) survives only on the --legacy-interp path.

§12.6 Hot reload — Resumable and the swap pipeline (Tier 1.5)

v1.0 ships agent-granular hot reload: an in-flight agent can be paused, snapshotted, swapped against a new code revision, and resumed without dropping its mailbox or any in-flight asks. Three shipping concerns make this normative:

  1. The Resumable trait is the snapshot/restore contract. Any agent that participates in hot reload implements it (or accepts the default ciborium-backed implementation that derives a schema hash from the agent's state record).
trait Resumable {
    const SCHEMA_HASH: U64           // FNV-1a over the structural shape
    fn to_snapshot(&self) -> Bytes
    fn from_snapshot(b: &Bytes) -> Self
}

The default impl (provided by mty-runtime::reload) FNV-1a-hashes the agent's flattened state record and ciborium-encodes its fields. Authors override either method for custom shapes.

  1. The swap pipeline is the runtime-side dance. The control- socket handler for Request::Reload { agent_type, module_b64, deadline_ms } drives it through reload::swap:
pause  → drain mailbox → snapshot via Resumable::to_snapshot
       → schema check (old SCHEMA_HASH → new SCHEMA_HASH,
          optional MigrateFrom<Old> chain via SchemaRegistry
          BFS)
       → restore via Resumable::from_snapshot
       → swap module bytes via Program::with_swapped_agent
       → resume

A ReloadGate (parking_lot condvar) replaces the v0.20 busy-poll in v0.21 so the drain step doesn't burn cycles.

  1. Schema-evolution chains (V1 → V2 → V3) are supported via the MigrateFrom<Old> trait + SchemaRegistry BFS over (old_hash, new_hash) edges. Authors register a migration once; the runtime composes the chain at reload time.

  2. The wasm module side carries two custom sections the runtime reads via wasmparser:

  3. __mty_agent_type — agent type name (UTF-8).

  4. __mty_schema_hash — agent's SCHEMA_HASH (little-endian U64).

§12.7 Reload diagnostic band — MT506x

Code Meaning
MT5060 reload requested for an agent type that is not registered
MT5061 reload module missing __mty_agent_type / __mty_schema_hash section
MT5062 schema hash mismatch and no MigrateFrom path registered
MT5063 MigrateFrom chain failed during restore
MT5064 reload deadline exceeded (drain or restore took too long)
MT5065 swap rejected by Program::with_swapped_agent (e.g. slot count mismatch)
MT5066 Resumable::to_snapshot returned an oversized payload (> 6 MB)
MT5067 Resumable::from_snapshot returned an error
MT5068 reload preempted by a higher-priority operation
MT5069 reserved

The band is documented in dev/history/notes/RELOAD_V0_21_NOTES.md with per-code rationale and CLI-side surfacing notes.

§12.8 mty reload and mty serve --watch (Tier 1.5 control surface)

Two CLI entry points drive reload:

  • mty reload <agent-type> --from new.wasm — one-shot reload. Connects to the runtime's control socket (MTY_RUNTIME_CONTROL_SOCK), reads the new module, sends Request::Reload, prints the response.
  • mty serve [--port <n>] [--watch] — long-running developer loop. mty serve hosts a hand-rolled HTTP/1.1 server plus an RFC 6455 hand-rolled WebSocket for hot-reload broadcasts. With --watch, the notify crate emits file-change events that trigger an automatic rebuild + reload broadcast over the WebSocket. The browser-side mty:web/canvas demo template listens for the broadcast and reloads its canvas.

§13 Protocols

A protocol declares the set of messages an agent can receive.

§13.1 Declaration

protocol CounterApi {
    msg Inc(by: I32)
    msg Get() -> I32
    msg Reset()
}

agent Counter: CounterApi { ... }

The msg keyword prefix is optional — a bare message-shape line inside a protocol body is treated as a msg declaration. The two forms are interchangeable:

protocol SearchApi {
    Query(q: Str) -> Json!SearchErr      // bare form
    msg Ping(msg: Str) -> Str            // explicit form
}

Style: the explicit msg prefix is recommended in the standard library; the bare form is accepted for terser inline protocols. Both shapes appear in the example corpus.

§13.2 Handler-param checks (A28, A65.c)

For local protocols (defined in the current package):

  • MT4030 protocol_arity_mismatch — handler param count ≠ protocol message arity.
  • MT4031 protocol_param_type_mismatch — handler param type does not match the protocol's declared type.
  • MT4032 protocol_missing_handler — protocol declares a message no on Msg(...) covers.
  • MT4033 protocol_extra_handler — on Msg for a name no implemented protocol declares.

For external protocols (referenced through a use import without the protocol's declaration in scope), MT4031 falls back to MT2026 warning (the slice-4 protocol-aware permissive path).

When ANY of an agent's declared protocols is unknown to the type checker, the strict checks are skipped agent-wide.

§13.3 Protocol versioning

Adding a new message to a protocol is a minor-version change. Removing or renaming a message is a major-version change. See Appendix B.

§14 Supervisors

Supervisors restart failed agents per a configured strategy.

§14.1 Declaration

supervisor TopSup strategy OneForOne {
    child counter = Counter()
    child logger = Logger()
}

let s = spawn TopSup()

Strategies (per spec §15 ladder):

  • OneForOne — restart only the failed child.
  • OneForAll — restart every child if any fails.
  • RestForOne — restart the failed child and every child declared after it.
  • Escalate — bubble the failure to the parent supervisor.

§14.2 Restart window (A42)

restart up_to N in DUR clauses keep a sliding window of restart timestamps; the (N+1)-th attempt within DUR denies and escalates per strategy. Top-level supervisors trap with RuntimeError::SupervisorEscalated (MT5013).

Backoff between restarts is uniform-jittered between configured min and max (default 0 ms); the jitter RNG is deterministic given a fixed rng_seed.

§14.3 Migration on restart

Restart spawns route via the load-balanced spawn table (A103); the restarted child may land on a different worker than its predecessor.

§15 Tasks and structured concurrency

§15.1 Task scopes

task scope @5s {
    let r1 = api?Fetch("a")
    let r2 = api?Fetch("b")
    use_both(r1?, r2?)
}

A task scope creates a structured concurrency frame. The scope deadline (@D) applies to every in-flight ask within the scope.

§15.2 Cancellation (A41, A70)

Cancellation reasons:

Reason MTxxxx Fired by
WallBudget MT5009 per-turn wall budget timer
CpuBudget MT5009 (reserved) per-agent CPU sum
AskDeadline MT5011 caller's ?Msg @D deadline
Shutdown MT5020 Runtime::shutdown fires root token

v1.0 cooperative mid-turn cancellation (A70, supersedes A41 between-turn-only model):

  1. Each per-turn run_handler_isolated invocation runs in tokio::task::spawn_blocking.
  2. The async parent races the resulting JoinHandle against a tokio_util::sync::CancellationToken.
  3. When the wall-budget timer fires, the token is fired with CancelReason::WallBudget; the parent drops the join handle (detaches the interpreter thread), emits a BudgetBreach telemetry event with MT5009, and notifies the caller's reply oneshot with RuntimeError::BudgetExceeded.
  4. The blocking thread is detached, not joined: a runaway handler is bounded only by the MtyIR interpreter's step budget (default 1 000 000).
  5. Reply notification is exactly-once: the frame's reply sender is moved into a shared Mutex<Option<...>> slot before scheduling; the cancel arm and blocking shim race to .take() it.

§15.3 Detach

detach { body } spawns body as a fire-and-forget task. It does not participate in any structured scope and cannot be cancelled by a parent task. Use sparingly; supervisors are usually preferable.

§16 Budgets and sandboxes

§16.1 Sandboxes (A43, supersedes A27)

sandbox WorkerSandbox with {
    cpu = 1s
    wall = 30s
    mem = 64MiB
    mb = 1k
    fs = read("/data")
    net = host("api.example.com:443")
} {
    run job(input)?
}

v1.0 runtime semantics (A43):

  • On body entry, a fresh BudgetTracker is constructed from the entries and pushed onto the active budget stack.
  • Capability calls inside the body are checked against the child sandbox's allowlists; breach traps with MT5015.
  • Nested sandboxes compose by stacking budgets; the inner sandbox's allowlist MUST be a subset of the outer (allowlist intersection at construction time).

§16.2 Budgets (A34, A99)

budget {
    wall = 5s
    mem = 16MiB
} run intensive_work(input)?

Entry syntax inside sandbox and budget blocks accepts two equivalent shapes for each key value pair:

sandbox WorkerSandbox with {
    wall = 30s        // explicit `=`
    mem 16MiB         // bare key/value (no `=`)
}

Both forms parse to the same AST and have identical semantics. The explicit = form is recommended for clarity in published code; the bare form is accepted because the example corpus uses it. Field separators inside the block follow the §4.5 rule (newline or comma).

v1.0 enforced budgets:

Budget Effect
wall per-turn wall clock (A70 fires MT5009)
mem running byte allocation tally (A99 fires MT5009)
mb mailbox depth (A40)
mb_policy mailbox full policy Block/Drop/Fail
fs filesystem allowlist (A100)
net network host allowlist

Reserved-for-v1.1+: cpu (per-agent CPU sum) — counter exists in the runtime but is not driven yet.

§16.3 Trap codes

Code Meaning
MT5007 arena escape detected at runtime (reserved, v1.1+)
MT5009 budget exceeded (wall, mem)
MT5010 sandbox violation
MT5011 ask deadline expired
MT5012 mailbox-full Fail policy fired
MT5013 supervisor escalated
MT5015 sandbox capability check failed
MT5020 runtime shutdown

§17 Error handling and panic policy

§17.1 Result and !

Result[T, E] is the canonical sum. T!E is the inline sugar. ? propagates per §11.6.

fn fetch(url: Str, n: &Net) -> Page!NetErr effect net {
    let body = http.get(url, n)?
    return Ok(parse(body))
}

§17.2 Anonymous error unions

fn render(url: Str) -> Page!{NetErr, ParseErr} { ... }

v1.0 sugar: T!{A, B} lowers to Result[T, Error] where Error is the poison sentinel that unifies permissively with concrete errors (A11). First-class union ADTs are v1.0 OPEN — deferred to v1.1+.

§17.3 Panic policy per profile

Profile Panic-on-overflow Panic on bounds-fail Default unwind
host yes yes abort
web yes yes abort
edge yes yes abort
core yes yes abort

v1.0 ships abort-on-panic for every profile. Catch-via-supervisor is the recovery mechanism (see §14). Unwind-table emission is v1.1+.

§18 Generics and constraints

§18.1 Generic parameters

fn map[T, U](xs: Vec[T], f: fn(T) -> U) -> Vec[U]
struct Holder[T] { inner: T }
enum Either[A, B] { Left(A), Right(B) }

§18.2 Bounds

where T: Trait clauses constrain type parameters:

fn hash_all[T: Hash + Eq](xs: Vec[T]) -> Vec[U64] { ... }

§18.3 Monomorphisation (A49)

Each generic fn called with concrete type-args gets its own specialised MtyIR fn before codegen.

v1.0 MVP simplification: the monomorphiser strips generic fns from the codegen unit rather than fully specialising every call site. Programs that exercise generics still type-check; they simply route through the interpreter fallback for execution (A49). Full specialisation is v1.0 OPEN — v1.1+.

§18.4 Trait coherence

Per §6.7: name-only coherence. v1.0 OPEN: generic-arg overlap detection.

§19 Traits and dynamic dispatch

§19.1 Trait declaration

trait Hash {
    fn hash(self: &Self) -> U64
}

trait Render {
    fn render(self: &Self) -> Html
}

§19.2 Impl blocks

impl Hash for String {
    fn hash(self: &Self) -> U64 { ... }
}

§19.3 Method dispatch order (A17)

For a user ADT receiver:

  1. Inherent impl (impl T { fn m(...) }) wins.
  2. Otherwise, search trait impls in scope. Exactly one match dispatches to that fn; two or more matches emits MT4020 method_ambiguous.
  3. No match: MT4021 method_not_found.

Opaque prelude ADTs and primitives use the slice-3 permissive built-in method table (A10) for ergonomics. The table is slated for v1.1+ removal in favour of typed inherent/trait dispatch.

§19.4 dyn Trait

dyn Trait is a fat pointer (data + vtable). v1.0 conservative object safety per §6.8. Coercion: let h: dyn Trait = value where Trait has a registered impl on value's type.

§19.5 Derive

See §6.9. Copy, Hash, Eq, Sendable ship in v1.0.

§20 Compile-time metaprogramming

§20.1 Constants and const fn

const MAX: U32 = 1024
const fn double(x: U32) -> U32 { x * 2 }
const QUOTA: U32 = double(MAX)

const fn bodies are evaluated at compile time. The const evaluator is a v0.4-vintage subset; full const-eval coverage is v1.0 OPEN (no spec amendment, tracked via internals).

§20.2 Declarative macros (A90, A92, A93)

pub macro assert_eq(a, b) {
    let __a = a
    let __b = b
    if __a != __b {
        panic("assert_eq failed: " + str(__a) + " != " + str(__b))
    }
}

Invocation syntax: assert_eq!(x, y) (A90 — the ! marker disambiguates macro calls from function calls).

Hygiene (A92): let bindings in macro bodies are mangled to avoid capturing identifiers from the call site. v1.0 extended-mangling coverage includes IDENT, tuple, struct (shorthand + renamed), ref/ref-mut/ref-kw, and mut-kw patterns. Set-of-scopes hygiene (Racket-style) is v1.0 OPEN — v1.1+.

Cross-file pub macro (A93): a macro marked pub exports from its declaring file via the PackageMacros surface. End-to-end wiring through mty-pkg is v1.0 OPEN — v1.1+ (the surface is shipped; the connector slice is additive).

§20.3 Procedural macros (A94)

proc macro Derive(input: TokenStream) -> TokenStream {
    // body parsing and TokenStream rewriting
}

v1.0 parses, stores, and statically checks proc macros for purity:

  • MT6005 proc_macro_impure — body references effect.…(…) or any call to the well-known impure surface (time, env, io, model, rand).
  • MT6006 proc_macro_unsupported_v0_5 — every call site to a proc macro replaces the call with the sentinel literal 0. The declaration is preserved so the source survives untouched.

Sandboxed execution of proc macros is v1.0 OPEN — v1.1+. The sandbox limits are exposed as constants in sdust_macros::proc::PROC_MACRO_{WALL_MS,MEM_BYTES,STEPS} so the spec and implementation cannot drift.

§20.4 Standard macro library (A95)

crates/mty-macros/lib/ ships five public macros as real Mighty source files:

  • assert.sd — assert!(cond), assert_eq!(a, b), assert_ne!(a, b)
  • debug.sd — debug!(expr) (eprintln of expression text + value)
  • unreachable.sd — unreachable!() (panic with clear message)

Load via sdust_macros::stdlib::load_into(&mut pm). Auto-import via use sdust_macros.assert lights up once mty-pkg pipes its symbol table into HIR lowering (v1.0 OPEN — v1.1+).

§20.5 Macro diagnostic codes (A91, A107)

Code Meaning
MT6001 unknown macro
MT6002 macro arity mismatch
MT6003 macro tokens not paren-balanced
MT6004 hygiene-mangling collision
MT6005 proc macro impure (static purity check)
MT6006 proc macro unsupported (v1.0 — execution deferred)
MT6007 proc macro impure (runtime detection, RFC-003)
MT6008 proc macro resource bound exceeded (RFC-003)
MT6009 format! template malformed (§20.6)
MT6010 format! template uses an unsupported spec (§20.6)

All resolved by mty explain MTxxxx and the LSP code-action hints. v0.6 centralised these codes into sdust_diagnostics::codes (A107); sdust_macros::diag re-exports the bare-u16 values so legacy call-sites compile unchanged.

§20.6 format!() builtin macro

format!("template", args...) is a v1.0 builtin macro that expands at parse time into a string-concatenation expression. The template literal accepts the standard "{} for positional argument" and "{:spec} for typed conversion" placeholders. Conversion specs recognised in v1.0:

Spec Receiver type Expansion
{} any with to_str() (arg).to_str()
{:x} integer (arg).to_hex_str()
{:X} integer (arg).to_hex_upper_str()
{:b} integer (arg).to_bin_str()
{:o} integer (arg).to_oct_str()
{:?} any with to_debug_str() (arg).to_debug_str()

Named placeholders are accepted ({x} reads a local named x). The runtime contract (the to_*_str() methods) lives in std.fmt; the macro lives in crates/mty-macros/src/stdlib/format.rs. Both are checked at parse + lower time so a malformed template fails compile with one of:

  • MT6002 macro_arity_mismatch — placeholder count does not match argument count.
  • MT6009 format_template_malformed — template is not a string literal, or has an unmatched { / }.
  • MT6010 format_unsupported_spec — placeholder uses a spec character not in the v1.0 table above.

String-interpolation literals — the bare "...{expr}..." form — remain DEFER-V1.1. v1.0 users write format!("...{}...", expr) or the equivalent concatenation "..." + str(expr) + "...".

v1.0 FROZEN. The spec list above is the v1.0 conversion vocabulary. Additional specs may be added in v1.x (additive); the existing set is stable.

§21 Unsafe code

unsafe { ... } is a block expression that admits operations the safe subset prohibits:

  • Dereferencing a raw pointer (*T, *mut T).
  • Calling an unsafe fn.
  • Reading or writing through a raw pointer.
  • Constructing certain primitive types from raw bytes.

unsafe blocks count as a permissive scope for unresolved value resolution (see §5.1). The inferred effect set of an unsafe block includes unsafe; the public-fn discipline (see §9.1) requires a declared effect unsafe clause on any pub fn that contains one.

unsafe fn declarations require call sites to be inside an unsafe block.

§21.1 requires clauses on unsafe fn

An unsafe fn MAY carry zero or more requires <expr> clauses between the signature (return type, effect clause) and the body. Each clause is a boolean precondition the caller is responsible for upholding:

pub unsafe fn _from_raw(ptr: *U8, len: USize) -> Bytes
    requires ptr != null
    requires valid(ptr, len)
{
    Bytes { ptr, len }
}

requires clauses parse as ordinary boolean expressions. The body (if any) follows the last requires clause and uses either the braced form { ... } or the = <expr> shorthand from §4.4. A trailing ; (no body) marks the signature as an extern / trait-method declaration.

v1.0 semantics: requires clauses are parse-only. The compiler does not verify them statically and does not emit runtime checks. Their role is documentary — they pin caller obligations into the source so reviewers and future static-verification tooling can consume them. Runtime / static enforcement is v1.0 OPEN — deferred to v1.x (tracked as candidate amendment A111).

§22 Frontend model (DOM, web)

§22.1 DOM capability

Dom is a CapFamily (see §8.1). Common methods:

Method Returns
set_text(id, text) Unit
get_text(id) Str (v1.0: u32 handle, v1.1+ canonical-ABI string)
on_click(id, callback_tag) Unit
query(selector) Option[Str] (v1.0: u32 handle)
get_element_by_id(id) Option[u32] (v0.4 back-compat)
set_text_handle(handle, text) Unit

§22.2 html"..." templates

let v = html"
    <div class='greeting'>
        Hello, {name}!
    </div>
"

html"..." lowers to a structured DOM fragment value. v1.0 effect: alloc (per A22).

§22.3 Wasm Component bindings (A97)

The wasm32-web target imports mighty:web/dom per the WIT declaration in docs/internals/codegen-wasm.md. The MtyIR lowerer routes Dom-cap method calls through BuiltinId::DomOp(name) (A108).

v1.0 OPEN — v1.1+: canonical-ABI return-area bridge so get-text and query return string / option<string> instead of u32 handles.

§22.4 Wasm Component Model packaging (A47)

v1.0 ships core Wasm modules via wasm-encoder with capability imports declared as ordinary function imports under the mighty module namespace. v1.0 OPEN — v1.1+: full Component Model wrappers via wit-component + WIT auto-binding + preview2/wasi-cli host integration.

§22.5 mty:web/canvas@0.1 and mty:web/input@0.1 (Track A, v0.23)

The wasm32-web target imports two additional first-class browser host surfaces alongside mty:web/dom:

  • mty:web/canvas@0.1 — 2D canvas rendering. Functions (selected): begin-frame, clear(color), fill-rect(x, y, w, h, color), stroke-rect, fill-text(x, y, text), set-font, end-frame. Surfaced in Mighty as the Canvas cap family with corresponding methods on std.web.Canvas.
  • mty:web/input@0.1 — keyboard / pointer input polling. Functions: poll-keys() -> list<key-event>, pointer-state() -> pointer-state-record. Surfaced as the Input cap family with corresponding methods on std.web.Input.

Each WIT interface is drift-guarded by WIT_IMPORT_* and WIT_EXPORT_* consts in the Mighty-side binding; a change to the WIT must update the const to compile.

The std.web module surface is described in §27.1. The embedded- core-module regression harness (v0.23) verifies the core module is embedded at byte offset 189 of the produced wasm32-web artefact; the long-standing "header-only component" suspicion from v0.22 was wrong.

v1.0 FROZEN. The interface set is pinned at 0.1.0. v1.1+ may add additional methods (additive only); breaking changes require a 0.2.0 interface bump, which is a major-version change per Appendix B.4.

§23 Backend model (HTTP, agents)

§23.1 http.serve (A36, A96)

fn main(n: Net) effect net, spawn {
    let api = spawn ApiAgent()
    http.serve(":8080", api)
}

v1.0 runtime semantics (A96, supersedes A36):

  • std.http.serve(addr) routes to sdust_stdlib::http_server::start_blocking, which binds a real TCP listener and returns a Str("<handle_id>|<bound_addr>") sentinel.
  • std.http.shutdown(handle) tears the listener down.
  • The accept loop runs in a process-wide tokio runtime and dispatches each request through an AgentDispatch closure installed at startup via http_server::install_agent_dispatch.

v1.0 OPEN — v1.1+: the default closure is still a deterministic 200 OK echo; per-agent routing wiring is the v1.1+ work.

§23.2 Request and Response shape

v1.0 minimal shape: handler returns (status: u16, body: String). Rich Request/Response records, streaming bodies, headers beyond Content-Type, HTTPS, HTTP/2: all v1.0 OPEN — v1.1+.

§23.3 Agent-backed serving

http.serve(addr, agent) from spec §34/example 19 lowers to a runtime call that binds the listener and asks the agent agent?Request(req) @30s per connection.

§24 Compilation pipeline

§24.1 Stages

source bytes (.mty)
       |
       v   mty-syntax::lex   (logos)
   +-------+
   | lexer |
   +-------+
       |  Vec<LexedToken>
       v   mty-syntax::parser   (hand-rolled RD + Pratt)
   +--------+
   | parser |
   +--------+
       |  GreenNode (rowan)
       v
   +-----+
   | CST |
   +-----+
       |
       +---+---+
       |       v   mty-ast (cast wrappers)
       |   typed AST view
       |       |
       v       v
   +-----------+   +---------------+
   | formatter |   | HIR lowering  |   mty-hir
   +-----------+   +---------------+
                            |
                            v
                  +----------+
                  | type/eff |   mty-types
                  +----------+
                            |
                            v
                  +-----------+
                  | borrow ck |   mty-borrow
                  +-----------+
                            |
                            v
                  +--------+
                  | MtyIR  |   mty-ir
                  +--------+
                            |
                            v
            +---------+ +---------+ +----------+
            | interp  | | crane   | | wasm     |
            | (deflt) | | lift    | | -encoder |
            +---------+ +---------+ +----------+

§24.2 Front-end determinism

The compiler is byte-for-byte deterministic at every stage. Same source → same GreenNode → same MtyIR with same arena indices → same emitted bytes. The conformance corpus depends on this.

§24.3 Native backends (A46, A48)

  • Default: Cranelift (via cranelift-codegen 0.132). Used by mty run (JIT) and mty build --target native (AOT object → linked exe).
  • LLVM: scaffolded as mty-codegen-llvm behind a cfg(feature = "llvm") flag, returning LlvmError::FeatureDisabled by default. A future build host with LLVM 17 enables it.

mty run JIT-then-fallback (A48):

  1. Try sdust_codegen_cranelift::jit::build_jit.
  2. On CodegenError::Unsupported(_), fall back to pipeline::run_file_with_runtime (the slice-7 path).
  3. --legacy-interp (A45) routes directly to the slice-6 synchronous interpreter. v1.0 OPEN: deprecation/removal pending in v1.1+ once codegen covers the full MtyIR surface.

§24.4 Native linker discovery (A52)

mty build --target native invokes a host C linker after Cranelift emits the .o. Discovery order:

  1. $MTY_LINKER env var, falling back to the legacy $STARDUST_LINKER spelling with a one-shot deprecation warning.
  2. clang / gcc / cc on PATH (preferred on unix and windows).
  3. link.exe on PATH except when it resolves to MSYS/Git-Bash's /usr/bin/link.exe (which is the GNU coreutils shim).

If none are found, mty build emits the .o and prints an instructive message rather than failing.

§24.5 Wasm backend (A47, A97)

mty build --target wasm32-web emits core Wasm modules per A47. The mighty:web/dom interface is declared per A97. Canonical-ABI bridging for richer return types is v1.1+.

§24.6 Monomorphisation (A49)

See §18.3.

§24.7 Codegen trap codes (A51)

Reserved for runtime traps produced by compiled (Cranelift or Wasm) code:

Code Meaning
MT8001 div by zero
MT8002 out-of-bounds index
MT8003 integer overflow (checked arithmetic only)
MT8004 null deref
MT8005 extern symbol unresolved (libloading miss)
MT8006 unreachable executed
MT8007 codegen rejected MtyIR shape (slice 8 fallback)
MT8008 native linker missing
MT8009 emitted Wasm failed validation
MT8010 monomorphisation failed

All have mty explain MTxxxx entries.

§25 Runtime architecture

§25.1 Scheduler (A101, A105, A106)

v1.0 ships N worker threads + 1 driver runtime (A101):

  • Each worker thread hosts its own tokio current_thread runtime plus a crossbeam_deque::Worker<SpawnTask> (LIFO local) and a Stealer exposed to siblings.
  • A shared Injector<SpawnTask> holds tasks not yet pinned.
  • Worker loop: local LIFO → global injector (batch steal) → sibling stealers (batch steal, random rotation) → tokio::sync::Notify with 50 ms safety timeout.
  • A separate driver current_thread runtime (A105) is exposed as Scheduler::rt. The driver block_on cannot collide with a worker's own block_on(worker_loop_async).

Default worker count (A106): std::thread::available_parallelism() (was 1 in slice 7). MTY_RUNTIME_THREADS=N (or the legacy STARDUST_RUNTIME_THREADS) overrides.

§25.2 Agent affinity (A102)

RuntimeBuilder::spawn_agent_with_affinity(agent, Affinity::Sticky)
Mode Behaviour
Affinity::Sticky pinned to worker 0 at spawn; never migrated
Affinity::Elastic default; round-robin spawn; may be retargeted

Front-end syntax agent X(...): Y with affinity = sticky is reserved but not parsed in v1.0. v1.0 OPEN — v1.1+.

§25.3 Lightweight migration (A103)

v1.0 migration retargets the routing table on next spawn; in-flight loops are not disturbed. Lossless live migration is v1.0 OPEN — v1.1+.

§25.4 Per-worker telemetry (A104)

Each worker exposes WorkerStats { tasks_executed, tasks_stolen, parks, current_queue_depth }. Snapshot accessor: Scheduler::stats() -> Vec<(usize, WorkerStatsSnapshot)>.

The OTLP exporter consumes these as gauges named mty.scheduler.worker.<id>.<metric> (see §35).

§25.5 Deterministic mode (A35, A39)

RuntimeBuilder::deterministic(seed) swaps the multi-worker scheduler for a single-worker current-thread runtime and exposes a seeded XorShift* RNG and LogicalClock. A106 preserves the single-worker pin under deterministic mode.

Replay invariant: given the same MtyIR program and same seed, the emitted telemetry sequence is byte-identical.

§25.6 Host trait (A33)

Effect-marked operations lower to Stmt::EffectInvoke{effect, op, args, out}. The interpreter forwards the call to its Host trait. v1.0 hosts:

  • RealHost — used by mty run, performs real I/O via stdlib.
  • BufferHost — used by tests; returns deterministic stub values (typically Value::Unit or empty string).
  • Compile-side codegen-cranelift uses sdust_runtime::codegen_abi bridging.

Test-time and production hosts share a single interface.

§25.7 Deref-of-ref write path (A44)

The interpreter's assign_place handles Projection::Deref writes: when the destination's projection starts with Deref and the target local holds a Value::Ref, the runtime resolves the ref to its owner local and writes through. This makes (*self).fN = v in agent handler state writebacks actually mutate the state.

run_handler_isolated is the canonical entry point; both the multi-worker scheduler path and the slice-6 sub-interp path (--legacy-interp) call into it.

§25.8 Cluster mesh (Tier 4, v0.18..v0.21)

v1.0 ships a distributed-agent cluster mesh: a Mighty Runtime MAY be configured with a SharedRouter that knows about peer nodes, enabling cross-node send / ask semantics without changing any source-level agent code. The mesh is opt-in via Runtime::with_cluster(SharedRouter); single-node deployments have zero overhead.

§25.8.1 Addressing model. An agent's cluster-wide address is a three-component path:

AgentAddr = node : type : pid
  • node — the cluster node identity (UTF-8; typically a DNS name or stable label assigned at runtime bootstrap).
  • type — the agent type's source-level name (e.g. Counter).
  • pid — the per-node monotonic PID.

Runtime::send_addr(addr, msg) and Runtime::ask_addr(addr, msg, deadline) consult the configured SharedRouter; if the resolved node is the local node, the call short-circuits to the in-process scheduler.

§25.8.2 Transport. Inter-node traffic is framed CBOR-over-TLS (default rustls, ALPN mty/1):

  • Per-frame header: 4-byte little-endian length + 1-byte kind tag.
  • Payload kinds: Send, Ask, Reply, Error, Heartbeat, MigrateSnapshot, MigrateAck, MigrateError.
  • A node-wide CorrelationTable demuxes inbound Reply / Error to the originating ask's reply oneshot.
  • Peer disconnect fans out MT5032 peer_disconnected to every in-flight ask routed through the dropped peer.

§25.8.3 mTLS (v0.20). ClusterMesh::from_config_mtls(cfg) opts into mutual TLS. Peer identity is bound to the certificate's Common Name (CN) via a hand-rolled extract_cn_from_der TLV walker (no extra dependency). The router's verify_peer_identity(node, peer_cn) MUST return Ok(()) before any frame is accepted.

§25.8.4 Cluster supervisor (Tier 4.2, v0.20). ClusterSupervisor runs a cluster-scope restart loop independent of the per-node supervisor tree:

Strategy Behaviour
OneForOne restart only the failed child agent on the chosen node
RestForOne restart the failed child + every cluster-child declared after it
OneForAll restart every cluster-child on every node

Per-child circuit breaker: too many restarts within a window flip the child into :noproc (no-process), broadcast over the cluster event channel. notify_node_disconnect marks every child placed on the disconnected node as :noproc.

§25.8.5 Lossless live migration (Tier 4.3, v0.21). See RFC-006. The orchestrator MigrationOrchestrator::migrate_agent(agent, target, deadline) ships an agent's snapshot + queued mailbox + continuation between nodes:

  • SnapshotSource (origin) — drains the mailbox, snapshots state via Resumable::to_snapshot, ships the wire envelope.
  • SnapshotSink (target) — accepts the envelope, restores via Resumable::from_snapshot, resumes dispatch.
  • 6 MB hard cap on the snapshot payload (MT5066).
  • At-most-once delivery across the migration boundary preserved by tagging in-flight asks with their migration epoch.

§25.8.6 Placement policy. PlacementPolicy trait selects where a fresh / restarted / migrated agent lands. Three bundled implementations:

Policy Behaviour
StickyPolicy always picks the agent's origin node when reachable
LeastLoadedPolicy picks the node with the fewest live agents
StaticPolicy reads a node-of-type map from the manifest

Manifest binding (in mighty.toml):

[cluster.placement]
default = "least-loaded"

[cluster.placement.types]
Counter = "sticky"
Logger  = { policy = "static", node = "log-1" }

§25.8.7 Telemetry. Cluster operations emit OTel spans under the mighty.cluster.* namespace (mighty.cluster.send, mighty.cluster.migrate, mighty.cluster.disconnect) plus counters mty.cluster.frames{kind, direction} and mty.cluster.migrations{outcome}.

§25.8.8 Cluster diagnostic bands.

Band Domain
MT503x cluster transport / routing
MT507x cluster migration / placement

Selected codes:

Code Meaning
MT5030 peer not found in router table
MT5031 peer handshake failed (TLS or mTLS identity mismatch)
MT5032 peer disconnected (fans out to in-flight asks)
MT5033 router rejected frame (oversized, malformed, kind unknown)
MT5070 migration target not reachable
MT5071 migration snapshot too large (> 6 MB)
MT5072 migration deadline exceeded
MT5073 migration sink rejected restore (incompatible Resumable)
MT5074 placement policy returned no candidate
MT5075 placement manifest references unknown node

mty explain MTxxxx resolves every code.

v1.0 FROZEN. Address shape, transport framing kinds, mTLS binding, supervisor strategy set, PlacementPolicy trait surface, manifest schema, and the MT503x / MT507x bands are stable across v1.x. Additive expansion (new policies, new frame kinds via reserved slots) is permitted; breaking changes require a major-version bump.

§26 Foreign function interface

§26.1 extern { fn ... }

extern {
    fn sqlite3_open(path: *const Char, db: *mut *mut Sqlite3) -> I32
}

Resolution (A53):

  • Per-name override from mighty.toml's [extern] table: 
    [extern]
"sqlite3_open" = "libsqlite3"
  • Otherwise the host libc:
  • Linux: libc.so.6 → libc.so
  • macOS: libSystem.dylib
  • Windows: msvcrt.dll → ucrtbase.dll

Unresolved names trap with MT8005 extern_unresolved at the call site.

extern { ... } blocks are a permissive scope (see §5.1). Calls require unsafe if the extern fn is declared unsafe fn.

§26.2 export fn and export <abi> fn

export is the dual of extern: it marks a Mighty function as externally callable from a host environment.

export fn mount(root_id: Str, initial: I32) -> Unit { ... }

export c fn _add(a: I32, b: I32) -> I32 = a + b

export js fn handle_click(id: U32) -> Unit { ... }

Three surface forms:

Form ABI
export fn Default — exposes the Mighty calling convention to hosts that can speak it (today: Mighty-to-Mighty across components, the wasm32-web target's component exports).
export c fn C ABI — function is callable via the platform C calling convention with the extern "C" mangling. Used for FFI surface and for wasm32 __add-style core-module exports.
export js fn JavaScript ABI — function is wrapped for direct invocation from a JS host via the wasm32-web target's JS shim.

The export <abi> token is part of the item, parsed as a single declaration. The inner fn carries the normal fn syntax (including the = <expr> shorthand from §4.4). Either form may also be unsafe (export c unsafe fn ...).

Exported functions are subject to the same effect-clause discipline as pub fn (§9.1).

§26.4 C, C++, JavaScript, Python interop

C interop: via extern (call into C) and export c fn (call out from Mighty). Standard C ABI; name-mangling per platform.

C++: name-mangling-aware externs are v1.1+.

JavaScript: lowered through the Wasm Component target's mighty:web/* imports plus export js fn exports. v1.0 DOM surface per §22; broader JS interop (callbacks, structured data round-trip) is v1.1+.

Python: not shipped in v1.0.

§26.5 Data interop

JSON via Json enum and std.json::{encode, decode}. Binary serialisation via std.cbor (v1.1+) and std.proto (v1.1+); v1.0 ships hand-rolled byte-level access through Bytes + slice methods.

§27 Standard library v1.0 surface

§27.1 Modules

Module Surface
std.fs read, write, exists, list_dir (cap-gated, A100)
std.net get, post, tcp.connect, tcp.listen
std.http serve, shutdown, parse_request_line
std.json encode, decode, Json enum
std.time now, sleep, Duration operators
std.log log, info, warn, error
std.panic panic, assert!, unreachable!
std.collections Vec, Map, Set
std.string full Str method surface (A98)
std.bytes Bytes + slice ops
std.rand XorShift, LogicalClock (deterministic in det-mode)
std.web Canvas + Input (v0.23 Track A, wasm32-web target). See §22.5 for the WIT interfaces and cap-family definitions. Methods include Canvas::{begin_frame, clear, fill_rect, stroke_rect, fill_text, set_font, end_frame} and Input::{poll_keys, pointer_state}.

§27.2 Str method surface (A98)

Category Methods
Search contains, starts_with, ends_with, find → Option[USize]
Indexing char_at(i) → Option[Char], slice(start, end) → Option[Str]
Case to_lower / to_lowercase, to_upper / to_uppercase
Whitespace trim, trim_start, trim_end
Splitting split(sep) → Vec[Str], chars, bytes
Mutation replace(from, to), repeat(n), push, push_str, clear, pop

Vec helpers: get(idx), first, last, iter.

The v0.4 permissive stubs that returned Bool(false) for contains and Unit for find/slice are replaced with real semantics in v1.0.

§27.3 HTTP client

let body = http.get("https://api.example.com/users", &net)?

Returns Bytes; pair with std.json::decode for structured response.

§27.4 HTTP server (§23)

http.serve(":8080", agent)

See §23. v1.0 default dispatcher echoes; per-agent wiring is v1.0 OPEN — v1.1+.

§28 Token-efficiency rules

Mighty is designed for both LLM and human authoring. Several syntactic choices optimise for terseness and parseability under token budgets:

  1. Single-character postfix operators for the most common shapes: ? (propagate), !Msg(args) (send), ?Msg(args) (ask), @D (deadline).
  2. Keyword-leading expression forms (run, if let, match, loop) keep statements scannable.
  3. Turbofish only in expression position (A2) — the type-position bracket form remains terse.
  4. Anonymous error unions T!{A, B} avoid a named-error-type declaration for short-lived combinations.
  5. derive Trait keyword shorthand (A26) alongside the canonical #[derive(Trait)].
  6. Keyword-tolerant .method (A3) — library APIs can use reserved-word method names without raw-identifier ceremony.

The shorthand forms have equivalent semantics to the canonical forms.

§29 Toolchain, build modes, and flags

§29.1 mty CLI subcommands

Subcommand Purpose
mty new scaffold a new package
mty check parse + type-check + borrow-check
mty fmt format source files
mty run JIT execute (--legacy-interp for slice-6 interp)
mty build AOT build (--target native / --target wasm32-web)
mty test run package tests
mty bench run package benches (criterion)
mty dump dump intermediate forms (--ir / --sir / --hir)
mty explain render a diagnostic code's explanation
mty doc render docstrings to HTML
mty lsp language-server mode (stdio)
mty registry package-registry interactions

§29.2 Build profiles

Compiler-side profiles:

Profile Optimisation Debug info Notes
dev (default) none full fastest compile
release level 3 minimal production builds
bench level 3 minimal benchmark builds

Target-side language profiles (see §30): host, web, edge, core.

§29.3 Environment variables

Variable Effect
MTY_RUNTIME_THREADS override scheduler worker count (A101, A106)
MTY_OTLP_ENDPOINT activate real OTLP exporter (A71)
MTY_TRACE JSON-line trace sink path (file:PATH)
MTY_LINKER override native linker discovery (A52)

Note: MTY_* is the primary spelling as of v0.36 T4. The legacy STARDUST_* prefix is intentionally retained for back-compat with v0.6 deployments; the first lookup that falls through to a STARDUST_* name emits a one-shot deprecation warning on stderr.

§30 Profiles

The package-level profile = "..." setting in mighty.toml selects the capability surface and a few enforcement modes:

Profile Description
host full stdlib, alloc free, all caps available; the default
web Wasm-Component-targeted; DOM cap; restricted I/O surface
edge server-edge runtime profile; net + fs; no DOM
core embedded / no-heap; alloc is hard-banned (A30, A65.d)

Under core, any pub fn whose inferred effect set contains alloc triggers MT4002 alloc_in_core.

§31 Construction history

The v1.0 surface is the product of nine ladder steps:

Step Tag Highlight
v0.1 (slices 1-8) v0.1.0 spec walk: lexer → parser → HIR → typeck → borrow → runtime → codegen
v0.2 v0.2.0 deferral closure: full effects, std types, doc gen
v0.3 v0.3.0 soundness pass: place algebra, NLL, OTLP, slab, mid-turn cancel
v0.4 v0.4.0 dogfood + ecosystem: registry, package manager, declarative macros
v0.5 v0.5.0 self-host lexer + dogfood completion + LSP advanced + proc macros parse
v0.6 v0.6.0 multi-core scheduler + first benchmarks + self-host parser
v0.7 v0.7.0-rebrand Stardust → Mighty brand rename
v0.8 v0.8.0 spec consolidation v1.0-RC (this document)
v1.0 (RC, then stable) release candidate frozen; bug-fix train opens

See docs/spec/CHANGELOG.md for the per-amendment log grouped by ladder step.

§32 Conformance suite

The conformance suite lives at tests/conformance/ and is the authoritative oracle for normative behaviour. As of v0.23 the suite ships 24 categories / 153 cases, packaged by scripts/build-conformance-kit.sh into a versioned tarball auto-attached to every tagged release.

Category Cases Notes
lexical/ 3 per-token-class coverage
parser/ 3 grammar production cases
type_checking/ 30 per-MTxxxx fire cases incl. v0.12/v0.14/v0.22 emit landings
type_inference/ 5 bidirectional / HM closure inference
borrow_checking/ 14 place / NLL / loop / Polonius cases
ownership_rejection/ 4 affine move violations
effect_checking/ 5 A30 / A65.d + effect-row poly cases (RFC-008)
capability_checking/ 4 A23 / A65 cap narrowing
budget_violation/ 6 A43 sandbox + A70 wall + A99 mem
traits_derive/ 4 derive Copy/Hash/Eq/Sendable
macros/ 6 A90 / A91 / A92 + set-of-scopes (RFC-009)
agent_protocol/ 5 A28 / A65.c
mailbox_ordering/ 7 A40 / A72 + multi-core ordering
supervisor_restart/ 4 A42 restart window + cluster supervisor strategies
control_flow/ 5 A80 / A81 / A82
runtime/ 6 A33 / A35 deterministic
runtime-7/ 8 slice-7 interpreter + deadline / sandbox / counter
runtime_traps/ 2 MT5009 / MT5011
codegen/ 9 cranelift native + wasm-encoder core
spec_coverage/ 5 meta-cases pinning prose claims to actual fixtures
deterministic_replay/ 5 byte-identical replay traces (v0.20+)
formatter_idempotence/ 5 fmt(input) == canonical (v0.20+)
native_abi/ 4 per-backend link-and-run (v0.20 fixtures, v0.21 harness)
wasm_component/ 4 per-backend component-shape diff (v0.20 fixtures, v0.21 harness)
Total 153 24 / 24 categories populated

The harness runs cargo test --workspace. As of v0.23: 1604 Rust tests plus 474 Python tests in the impl-py/ 2nd-impl pass.

Coverage. 63% direct (one fixture per diagnostic code's positive fire), 99% any-harness (counting cases that exercise the code via spec_coverage / runtime / codegen paths). Only MT3012 (DROP_IN_CONST_CONTEXT) is uncovered — deferred pending HIR CONST_DECL lowering.

Normative vs informative split. v1.0 declares which of the 153 cases are NORMATIVE (every conforming implementation MUST pass) vs INFORMATIVE (illustrative; pass not required for the v1.0 GA conformance claim). See tests/conformance/v1.0-NORMATIVE.md.

Kit packaging. scripts/build-conformance-kit.sh packages the suite + this spec + docs/spec/conformance.md into mty-conformance-kit-vX.Y.Z.tar.gz. See tests/conformance/CONFORMANCE_KIT.md for the manifest and use protocol.

§33 Diagnostic catalog

All diagnostics carry an MTxxxx code. Numeric bands:

Band Domain
MT0xxx lexer / generic IO
MT1xxx parser / CST
MT2xxx type checker
MT3xxx ownership / borrow / move
MT4xxx effects / capabilities / traits / coherence
MT5xxx runtime traps
MT6xxx macros (A91, A107)
MT7xxx (reserved)
MT8xxx codegen / linker (A51)

mty explain MTxxxx is single-sourced on sdust_diagnostics::codes (A107) and resolves every code uniformly, including the macro-band MT6001..MT6006. The legacy SDxxxx prefix remains accepted by mty explain for back-compat.

The full catalog ships at docs/reference/diagnostics.md.

§33.1 FROZEN typeck codes with deferred emit-site (RC3)

Six typeck-band codes have their explain text and code-point registered in sdust_diagnostics::codes and are listed in docs/spec/conformance-coverage.md, but the v1.0 compiler does not yet emit them (the conditions they describe are funneled into more general codes today). The spec treats them as FROZEN — the code-point and explain text are stable — with the emit-site landing scheduled for v1.x:

Code Title Current behaviour today v1.x emit landing
MT2003 CANNOT_INFER_TYPE Falls through to a generic {integer}/{float} placeholder v1.x trait-iterator + collect chain
MT2009 UNKNOWN_VARIANT Funneled into MT2007 or MT2021 v1.x enum-aware resolver
MT2022 NOT_A_STRUCT Funneled into MT2002 (unresolved type) v1.x struct-init kind check
MT2023 GENERIC_ARG_MISMATCH Not reachable until explicit lifetimes ship v1.x with lifetime kind
MT2024 LAMBDA_ARITY_MISMATCH Funneled into MT2005 (wrong arg count) v1.x lambda-arity refinement
MT2025 CANNOT_TAKE_REF Borrow checker accepts via implicit promotion v1.x stricter borrow-pass

Implementations targeting v1.0 MAY emit any of these codes today; the explain-text contract is stable. Implementations MUST NOT recycle these code-points for other conditions. See SPEC_RC3_V0_12_NOTES.md for the per-code rationale.

§34 Worked examples

The canonical examples are under examples/. v1.0 ships 20+ end-to-end programs covering every spec section:

Example Topic
01_hello.mty log("hello, Mighty")
02_types.mty primitives, struct, enum
03_generics.mty bounded generics
04_errors.mty T!{NetErr, ParseErr} (A11)
05_control_flow.mty if let, match, for, loop, break
06_agents.mty spawn, !Msg, ?Msg @D
07_agent_echo.mty bidirectional ask
08_counter.mty agent state mutation (A44)
09_arenas.mty arena allocation
10_capabilities.mty cap narrowing
11_budgets.mty sandbox + budget
12_extern.mty libc extern (A53)
13_supervisor.mty restart semantics (A42)
14_macros.mty declarative macro
15_proc_macro.mty proc macro decl (A94)
16_traits.mty inherent + trait dispatch
17_derive.mty derive(Copy, Hash, Eq, Sendable)
18_iterators.mty for / __sdust_iter_next (A81)
19_backend_service.mty http.serve + agent
20_frontend_component.mty html"...", DOM cap

Each compiles to native and to wasm32-web (v0.6: 20/20 each).

§35 Telemetry and observability

§35.1 JSON-line sink (A38)

By default the runtime emits structured logs as one JSON object per event line on stderr (or the path in MTY_TRACE=file:PATH; legacy STARDUST_TRACE still accepted). Event kinds: turn_start, turn_end, send, ask, reply, spawn, restart, budget_breach, shutdown. Every event carries ts (ms since epoch) and a kind field; per-kind additional fields vary.

The JSON-line sink is OpenTelemetry-flavoured but not strict OTLP (A38). Setting MTY_OTLP_ENDPOINT (or legacy STARDUST_OTLP_ENDPOINT) swaps in the strict OTLP exporter (A71).

§35.2 OTLP wire-format exporter (A71, supersedes A38)

MTY_OTLP_ENDPOINT=<url> (or legacy STARDUST_OTLP_ENDPOINT) activates a real opentelemetry_sdk::TracerProvider configured with opentelemetry_otlp::SpanExporter over gRPC (tonic). Spans use the mighty.* semantic-convention namespace:

  • mighty.turn.start, mighty.turn.end
  • mighty.send, mighty.ask, mighty.reply
  • mighty.spawn, mighty.restart
  • mighty.budget.breach

Resource attributes carry service.name = "mighty-runtime" plus the crate version.

OTLP failure (collector unreachable, malformed URL) never breaks runtime construction: the runtime falls through to the JSON sink and prints one diagnostic line on stderr.

The exporter is gated behind a default-on otlp cargo feature so minimum-binary builds can drop the transitive deps via --no-default-features.

§35.3 Per-worker scheduler metrics (A104)

Per §25.4. Exported as OTLP gauges named mty.scheduler.worker.<id>.<metric>:

  • tasks_executed
  • tasks_stolen
  • parks
  • current_queue_depth

§36 Package manager and registry

§36.1 Manifest schema

[package]
name = "my-app"
version = "0.1.0"
edition = "2026"
profile = "host"

[deps]
log = "1.0"
http = { version = "2.1", features = ["server"] }

[extern]
"sqlite3_open" = "libsqlite3"

The manifest filename is mighty.toml (rebranded from star.toml in v0.7). The lockfile is mighty.lock.

§36.2 Resolution

Dependency resolution is SemVer-flavoured (see Appendix B). The package manager (mty-pkg) resolves dependencies against a registry.

Default registry slug: mighty-pkg/registry (renamed from stardust-pkg/registry in v0.36 T4; both spellings still resolve to the same default via mty_pkg::registry::is_official_registry so manifests that pinned the legacy slug keep working). The pre-v0.7 DNS-shaped default (pkg.stardust.dev) is no longer referenced in code; the GitHub-Releases-backed slug above is canonical.

§36.3 Registry protocol

JSON-over-HTTPS index. v1.0 surface:

  • GET /<name>/index.json — package version list
  • GET /<name>/<version>/manifest.json — manifest snapshot
  • GET /<name>/<version>/contents.tar.gz — package contents
  • POST /publish — authenticated publish

§37 LSP and editor integration

§37.1 Capabilities (A74)

v1.0 LSP capabilities (shipped in v0.5 per A74):

  • textDocument/didOpen, didChange, didClose
  • textDocument/publishDiagnostics
  • textDocument/hover
  • textDocument/definition
  • textDocument/formatting
  • textDocument/completion (keyword + semantic; locals-in-scope; receiver-aware method/field completion after .)
  • textDocument/semanticTokens/full + /range — 14-type + 3-modifier legend
  • textDocument/rename + prepareRename — single-file scope
  • textDocument/inlayHint — inferred-type hints for let bindings and fn parameters
  • textDocument/codeAction — MT2021, MT2002, MT3001, MT4001 quick fixes via Levenshtein edit distance ≤ 2
  • textDocument/signatureHelp — call and method-call sites
  • workspace.workspaceFolders capability + workspace/didChangeWorkspaceFolders and workspace/didChangeWatchedFiles notification handlers

§37.2 Single-file scope decision

Cross-file rename and cross-file go-to-def require a workspace-wide resolve map that is not yet plumbed through mty-driver. v1.0 ships the LSP protocol surface and restricts scope to the active file.

v1.0 OPEN — v1.1+: cross-file rename / cross-file go-to-def / workspace resolve map.

§37.3 Borrow check in the editor

The editor pipeline skips the borrow check for latency. mty check from the CLI is the authoritative borrow-check oracle.

§37.4 Tests

cargo test -p mty-lsp covers 45 tests across 9 files (10 unit, 11 baseline integration, 5 semantic_tokens, 5+2 rename, 3 inlay_hints, 2 code_action, 3 signature_help, 1 workspace_folders, 3 completion_semantic).

§38 Benchmarks and performance budgets

The mty-bench workspace member (added in v0.6) ships six benchmark categories with code-level comparators in Rust, Go, and C++:

Category Mighty impl
parse_throughput crates/mty-bench/benches/parse_throughput/mighty.rs
agent_send_latency crates/mty-bench/benches/agent_send_latency/mighty.rs
mailbox_throughput crates/mty-bench/benches/mailbox_throughput/mighty.rs
http_server_throughput crates/mty-bench/benches/http_server_throughput/mighty.rs
compile_to_native crates/mty-bench/benches/compile_to_native/mighty.rs
wasm_size crates/mty-bench/benches/wasm_size/mighty.rs

Each category has a per-category doc under docs/benchmarks/*.md with methodology, recorded numbers, and the v1.1+ optimisation backlog.

The v0.6 build host did not have Go / g++ / TinyGo / Emscripten, so cross-language comparator numbers are marked (pending — Reference env) in each category doc. The Mighty numbers themselves are real (recorded by criterion).

§39 Self-hosting

v1.0 self-host status:

Stage Status
Lexer v0.5: shipped, byte-for-byte diff matches host
Parser v0.6: ~1930 LOC, 13/13 bootstrap tests, examples 01-05
HIR / lowering v1.0 OPEN — v1.1+
Type checker v1.0 OPEN — v1.1+
Borrow checker v1.0 OPEN — v1.1+
Codegen v1.0 OPEN — v1.1+

The self-host parser is a syntactic subset. Deferred productions (send sugar !Msg(args), deadline @duration, HTML literals, agent/protocol/supervisor blocks, unsafe blocks) wait on v1.1+.

The parser runs through a host bridge that lexes via the Rust lexer and parses via the Mighty parser source under a Rust harness.

Appendix A — v1.0 scope (FROZEN / OPEN matrix)

RC2 stability surface. The §A.1 FROZEN list IS the v1.0 stability surface. Every feature listed in §A.1 carries the following v1.x commitment:

  • No breaking changes within v1.x. The feature's fire conditions, observable behaviour, and source-level shape are stable. New features may be added (additive only); messages may be refined but conditions may not.
  • Diagnostic codes are permanent. Once a code is assigned in §A.1, its numeric value never changes; see Appendix B.3.
  • Stability is enforced by the conformance corpus. Every FROZEN feature has at least one positive-fire conformance case (gaps tracked in SPEC_FREEZE_V0_9_NOTES.md blocker #3).

§A.2 below is the v1.1 promotion-target backlog. Items in §A.2 ship in v1.0 with their current behaviour but MAY evolve with backwards-incompatible behaviour changes within their documented scope. Each §A.2 item links to its tracking RFC (if any) or to the ordinary backlog tracker.

A.1 FROZEN features

Features in this list ship in v1.0 with a stability commitment: no breaking changes within v1.x without a major-version bump.

Lexical and syntactic:

  • UTF-8 source, line/block/doc comments, identifiers, all literal forms including size suffixes k/M (A1), turbofish (A2), keyword-tolerant .method (A3), keyword-tolerant effect names (A4), run <expr> form (A5), if let (A6), postfix ?/! same-line rule (A12), macro marker name!(args) (A90).
  • Reserved keyword set, derive Trait shorthand alongside #[derive(...)] (A26).
  • Strict ? (A7), MT2010/MT2011 emission.
  • Strict match exhaustiveness (A16, MT2015 Error).

Type system:

  • Primitive set, composite types, generics, where bounds, defaulting pass (A19, closes A8), per-position turbofish (A2).
  • Trait coherence — name-only (A24).
  • dyn Trait object safety (A25, MT4023).
  • Method dispatch order (A17, MT4020/MT4021).
  • Derives: Copy, Hash, Eq, Sendable (A26, A65.b).

Ownership:

  • Affine types, Copy set (A26 supersedes A13).
  • Place-algebra borrow tracking (A54).
  • NLL last-use deactivation (A55).
  • Loop back-edge fixed-point (A82).
  • Precise MT3009 emission (A56).
  • Sendable trait + check at message sites (A65.b).

Effects and capabilities:

  • Effect inference algorithm (A22, MT4001).
  • core profile alloc ban (A30, A65.d, MT4002).
  • Capability constraints (A23, MT4010).
  • Per-call FsCap isolation contract (A100, A109).
  • Effect/Host trait dispatch (A33).

Control flow:

  • if/match/loop/while/for, break/continue first-class (A80).
  • Iterator wire protocol (A81).

Agents and runtime:

  • Mailbox depth/policy defaults (A40, A72 slab pool).
  • Async dispatch via multi-worker scheduler (A101..A106).
  • Per-worker telemetry (A104).
  • Driver runtime separation (A105).
  • Deterministic mode preserves single-worker pin (A39, A106).
  • Cooperative mid-turn cancellation (A70 supersedes A41).
  • Supervisor restart window (A42).
  • Deref-of-ref write path (A44).
  • Top-level sandbox runtime enforcement (A43 supersedes A27).
  • Memory auto-charging (A99 supersedes A37).
  • bumpalo-backed arenas (A50).

HTTP and DOM:

  • std.http.serve real socket bind (A96 supersedes A36).
  • DOM cap via mighty:web/dom (A97, A108).
  • Canvas + input via mty:web/canvas@0.1 + mty:web/input@0.1 (§22.5, v0.23). std.web.{Canvas, Input} Mighty-side bindings drift-guarded by WIT_IMPORT_* / WIT_EXPORT_* consts.

Cluster mesh:

  • AgentAddr = node:type:pid addressing (§25.8.1).
  • Framed CBOR-over-TLS transport (§25.8.2) + mTLS opt-in (§25.8.3).
  • ClusterSupervisor strategies OneForOne / RestForOne / OneForAll + per-child circuit breaker (§25.8.4).
  • Lossless live migration via MigrationOrchestrator (§25.8.5, RFC-006).
  • PlacementPolicy trait + 3 bundled policies + [cluster.placement] manifest block (§25.8.6).
  • Cluster telemetry under mighty.cluster.* OTel namespace (§25.8.7).
  • MT503x / MT507x diagnostic bands (§25.8.8).

Hot reload (Tier 1.5):

  • Resumable trait + default ciborium-backed impl (§12.6).
  • reload::swap pause → drain → snapshot → schema-check → restore → resume pipeline + ReloadGate condvar drain (§12.6).
  • MigrateFrom<Old> + SchemaRegistry BFS for schema-evolution chains (§12.6).
  • __mty_agent_type + __mty_schema_hash wasm custom sections (§12.6).
  • MT506x diagnostic band (§12.7).
  • mty reload + mty serve [--port] [--watch] control surface (§12.8).

Macros:

  • Marker name!(args) (A90), MT6001 (A91), extended hygiene mangling (A92), cross-file pub macro surface (A93), standard macro lib (A95), central macro diag catalog (A107).
  • Set-of-scopes hygiene (RFC-009, shipped v0.13..v0.15) wired into HIR via the scope-aware resolver.
  • Effect-row polymorphism (RFC-008, shipped v0.13..v0.19) — HirEffectRow::Open(Vec<HirRowVar>), MT4055..MT4059 active.
  • format! builtin macro + std.fmt runtime contract (v0.24); v1.0 spec table at §20.6. MT6009 / MT6010 active.

Codegen:

  • Cranelift default + LLVM scaffold (A46).
  • JIT-first execution (A48).
  • bumpalo arenas (A50).
  • Codegen trap codes MT8001..MT8010 (A51).
  • Native linker discovery (A52).
  • libloading-resolved externs (A53).

Observability:

  • JSON-line telemetry sink, OTLP exporter (A71 supersedes A38), per-worker scheduler metrics (A104).

Toolchain:

  • LSP surface per A74 (single-file scope).
  • mty-bench six-category bench corpus (v0.6).
  • Self-host lexer + parser (subset) per v0.5/v0.6.

A.2 v1.1 promotion targets (was: OPEN features)

Features in this list ship in v1.0 as experimental: they MAY evolve in v1.x with backwards-incompatible behaviour changes within their documented scope. Stability is not committed.

RC2 split this list into two columns:

  • DEFER-V1.1 items have a design path documented (RFC or ordinary-backlog tracker). v1.1+ adopts the path.
  • Additive-v1.1+ items have FREEZE-MVP semantics in v1.0: the MVP behaviour is the v1.0 normative contract, and v1.1+ expansions land as new additive amendments that never change MVP semantics. Programs that compile in v1.0 continue to compile in v1.x.

Architecturally significant — RFC track:

  • Anonymous error unions (A11, DEFER-V1.1) — currently resolve to Result[T, Error] sentinel. v1.1+: first-class union ADTs. Tracked by RFC-001.
  • Wasm Component Model wrapper (A47, DEFER-V1.1) — core modules only in v1.0. v1.1+: wit-component + WIT auto-binding + preview2/wasi-cli. Tracked by RFC-002.
  • Canonical-ABI DOM return bridge (A97, DEFER-V1.1) — get-text and query return u32 handles in v1.0. v1.1+: real string / option<string> returns. Tracked by RFC-002.
  • Proc-macro execution (A94, DEFER-V1.1) — parse + store only in v1.0, MT6006-gated at every call site. v1.1+: sandboxed execution. Tracked by RFC-003.
  • Per-call FsCap manifest materialisation (A100 carryover, A109 follow-up, DEFER-V1.1) — process-wide default cap is the v1.0 contract; A100 itself stays FROZEN. v1.1+: MtyIR lower threads per-call cap from sandbox manifest. Tracked by RFC-004.
  • Agent affinity front-end syntax (A102, DEFER-V1.1) — runtime API only in v1.0. v1.1+: agent X with affinity = sticky parser support. Tracked by RFC-005.
  • Lossless live agent migration (A103, DEFER-V1.1) — routing- table-only in v1.0. v1.1+: in-flight loop migration. Tracked by RFC-006. Update (v0.21): the full Tier 4.3 orchestrator shipped; this row remains in §A.2 only until the RFC-006 comment window closes (the design has been promoted to v1.0 FROZEN per §25.8.5 / §A.1).
  • Bare string interpolation (§20.6, DEFER-V1.1) — the bare "...{expr}..." interpolation literal is not parsed in v1.0; users write format!("...{}...", expr) instead. v1.1+: typed compile-time interpolation literals. No RFC; this is straightforward parser/lower work. (The format! builtin macro itself shipped in v0.24 — see §20.6 for the v1.0 surface.)

FREEZE-MVP — additive expansion in v1.1+:

  • Arena escape direct-naming detection (A15, FREEZE-MVP) — direct-naming MT3010 is the v1.0 contract. v1.1+ adds an additive indirect-flow detector (programs accepted by v1.0 continue to compile).
  • Arena runtime enforcement (A31, FREEZE-MVP) — static MT3010 + bumpalo (A50) + auto-charging (A99) are the v1.0 contract. MT5007 stays reserved; v1.1+ activates it when the indirect-flow detector lands.
  • Per-(fn, type-args) monomorphisation (A49, FREEZE-MVP) — strips generics; calls route via the slice-7 interpreter fallback (A48) for execution. v1.1+ adds full specialisation as a purely additive optimisation.

Ordinary backlog (no RFC needed):

  • Permissive method table (A10) — kept for opaque prelude ADTs. v1.1+: typed inherent/trait dispatch removes residual permissive table.
  • --legacy-interp flag (A45, DEFER-V1.1) — retained pending v1.1+ deprecation once codegen covers the full MtyIR surface.
  • Per-agent HTTP dispatch wiring (A96) — default-echo dispatcher in v1.0. v1.1+: real per-agent routing through install_agent_dispatch.
  • LSP cross-file features (A74) — single-file scope in v1.0. v1.1+: cross-file rename / go-to-def / workspace resolve map.
  • Trait coherence generic-arg overlap (A24) — name-only in v1.0. v1.1+: full overlap detection.
  • Set-of-scopes macro hygiene (A92) — extended mangling pass in v1.0. v1.1+: Racket-style set-of-scopes.
  • Self-host HIR + typeck + borrow + codegen (§39) — parser only in v1.0. v1.1+: full ladder.
  • Labelled break/continue (A80) — unlabelled only in v1.0. v1.1+: 'outer: loop { break 'outer }.
  • Full trait-based iterators (A81) — wire protocol only in v1.0. v1.1+: Iter[T], combinators, user-defined iterables.
  • Cross-file pub macro use (A93) — surface ready, wiring pending. v1.1+: end-to-end import via mty-pkg.
  • Standard macro auto-import (A95) — manual load_into in v1.0. v1.1+: use sdust_macros.assert works automatically.

Appendix B — Backwards-compatibility policy

B.1 SemVer commitments

Mighty follows semantic versioning at the language and runtime level:

  • MAJOR version bumps may break source compatibility (deprecate syntax, remove keywords, change runtime semantics in observable ways).
  • MINOR version bumps may add new syntax, new stdlib surface, and new diagnostic codes, but MUST NOT break existing FROZEN features.
  • PATCH version bumps fix bugs only; no syntax or runtime semantic changes.

The v1.0 FROZEN matrix in Appendix A is the v1.x stability surface. OPEN features may evolve within v1.x.

B.2 Deprecation cycle

Within v1.x:

  1. A feature is marked deprecated in a minor release; a MT9xxx-band warning fires at use sites.
  2. The deprecation warning remains for at least one minor cycle (typically two).
  3. Removal occurs in the next MAJOR release.

Special cases shipped in v1.0:

  • .sd file extension reader — present in v1.0; deprecation warning planned for v1.2; removal in v2.0 (no earlier).
  • SDxxxx diagnostic prefix in mty explain — alias retained indefinitely (back-compat with v0.6 bug reports).
  • STARDUST_* env vars — retained for back-compat. As of v0.36 T4 each variable has a primary MTY_* spelling; the legacy STARDUST_* name still works but the first fall-through emits a one-shot deprecation warning on stderr.
  • --legacy-interp — flagged for v1.1+ deprecation review.
  • v0.4 plain-call macro form (without !, A90) — flagged for v1.1+ deprecation review.

B.3 Diagnostic code stability

Once a diagnostic code is assigned, its numeric value is permanent. A code's message may evolve in minor releases; its fire conditions are covered by the FROZEN / OPEN matrix for the underlying spec rule.

B.4 Wire format stability

  • OTLP (A71) follows OpenTelemetry semantic conventions; spans named mighty.* are stable within v1.x.
  • WIT interfaces under mty:caps/* and mty:web/* follow the WIT version-pinning convention; v1.0 interfaces are pinned at 0.1.0.

Appendix C — Cross-reference map (amendment → spec section)

Amendment v1.0-RC section(s)
A1 §3.4.4 size literals
A2 §3.5 punctuation; §6.6 type-position vs value-position
A3 §3.3 identifiers and keywords
A4 §3.3; §9.2 effect declarations
A5 §16.1 sandboxes
A6 §11.1 expressions
A7 §11.6 ? propagation
A8 → A19 §6.5 type inference
A9 §6.1 primitive types
A10 §19.3 method dispatch order (residual perm)
A11 §6.3 Result/Option; §17.2 anon error unions
A12 §3.5 punctuation
A13 → A26 §7.1 affine types (Copy set)
A14 → A65.b §7.8 Sendable
A15 §7.9 arena escape
A16 §11.5 match exhaustiveness
A17 §19.3 method dispatch order
A18 → A28, A65.c §13.2 handler-param checks
A19 §3.4.1 / §6.5 defaulting pass
A20 → A55 §7.4 NLL last-use deactivation
A21 → A65 §5.1 scope kinds
A22 §9.1 effect inference
A23 §8.2 / §8.3 capability constraints
A24 §6.7 / §19 trait coherence
A25 §6.8 object safety
A26 §6.9 / §7.1 derive
A27 → A43 §16.1 sandboxes
A28 §13.2 handler-param checks
A29 → A56 §7.6 move via deref
A30, A65.d §30 profiles; §9.1 effect inference
A31 §7.9; §10 arenas
A32 §12.5 agent dispatch model (superseded by async)
A33 §25.6 Host trait
A34 §16 budgets/sandboxes (superseded by A43+A70+A99)
A35 §25.5 deterministic mode
A36 → A96 §23.1 http.serve
A37 → A50, A99 §10.4 mem auto-charging
A38 → A71 §35 telemetry
A39 §25.5 deterministic mode
A40 §12.3 mailbox defaults
A41 → A70 §15.2 cancellation
A42 §14.2 restart window
A43 §16.1 sandboxes
A44 §25.7 deref-of-ref write path
A45 §24.3 native backends
A46 §24.3 native backends
A47 §22.4 Wasm Component packaging
A48 §24.3 native backends
A49 §18.3 monomorphisation
A50 §10.2 arena implementation
A51 §24.7 codegen trap codes
A52 §24.4 native linker discovery
A53 §26.1 extern resolution
A54 §7.3 place algebra
A55 §7.4 NLL last-use
A56 §7.6 move via deref
A65 §5.1 scope kinds
A65.b §7.8 Sendable
A65.c §13.2 handler-param checks
A65.d §30 profiles
A70 §15.2 cancellation
A71 §35.2 OTLP exporter
A72 §12.4 slab-pool frames
A73 §25 (internal infrastructure)
A74 §37 LSP
A80 §11.2 break/continue
A81 §11.3 iterator protocol
A82 §7.5 loop back-edge fixed-point
A90 §3.5 punctuation; §20.2 declarative macros
A91 §20.5 macro diagnostic codes
A92 §20.2 declarative macros (hygiene)
A93 §20.2 declarative macros (cross-file)
A94 §20.3 procedural macros
A95 §20.4 standard macro library
A96 §23.1 http.serve
A97 §22 frontend model
A98 §27.2 Str method surface
A99 §10.4 mem auto-charging
A100 §8.6 / §27.1 FsCap allowlist
A101 §25.1 scheduler
A102 §25.2 affinity
A103 §25.3 migration
A104 §25.4 per-worker telemetry
A105 §25.1 driver runtime separation
A106 §25.1 default worker count
A107 §20.5 / §33 central diag catalog
A108 §22.3 / §22.1 BuiltinId::DomOp
A109 §8.6 per-call FsCap isolation

C.1 RFCs by amendment (RC2)

RC5 extension (v0.24). Two further RFCs (RFC-008 effect rows, RFC-009 set-of-scopes hygiene) joined the table in v0.13 + v0.15 and shipped within v0.13..v0.19. The table below covers all 8. The originally-authored 6 (RFC-001..006) are unchanged.

The v0.9 spec-freeze prep slice authored 6 first-draft RFCs covering the architecturally-significant v1.1+ promotion paths. v0.13 added two more (RFC-008 effect rows, RFC-009 set-of-scopes hygiene), both of which shipped within v0.13..v0.19. Each RFC has Summary + Motivation + Detailed Design + Drawbacks + Alternatives Considered + Unresolved Questions + Adoption Plan sections.

RFC Covers Target Comment window Implementation status
RFC-001 A11 v1.1 30 days not yet shipped
RFC-002 A47, A97 v1.1 60 days not yet shipped
RFC-003 A94 v1.1 30 days not yet shipped (budget constants in tree)
RFC-004 A100, A109 v1.1 30 days not yet shipped (cap-name resolver landed v0.21)
RFC-005 A102 v1.1 14 days not yet shipped
RFC-006 A103 v0.21 (shipped) 60 days SHIPPED v0.21 (Tier 4.3)
RFC-008 (new) v0.13 (shipped) 30 days SHIPPED v0.13..v0.19
RFC-009 (new) v0.13 (shipped) 30 days SHIPPED v0.13..v0.15 (Accepted)

Live status (open / closed / disposition / days remaining) lives in rfcs/RFC_DASHBOARD.md. Per-RFC window policy lives in rfcs/COMMENT_WINDOWS.md.

The v0.9 freeze plan (in SPEC_FREEZE_V0_9_NOTES.md) documents the path from v0.9 → v1.0 stable. As of v0.24 the four original blockers are reduced to one: the eight RFC comment windows (all opened 2026-05-26). Earliest possible v1.0.0 tag: 2026-07-26 (the day after RFC-002 and RFC-006 close, assuming no re-opens). The conformance kit at v1.0 (Track B, §32) and Python 2nd-impl feature-freeze (Track A, blocker #1) are both already shipped.

End of Mighty Language Specification v1.0 (Release Candidate 5).