Skip to content

Mighty v0.1 Spec Amendments

Decisions made during implementation that extend or clarify the v0.1 language specification (stardust_language_spec_v0_1.md). Each amendment carries the slice in which it was adopted; consumers should treat these as part of the v0.1 reference.

Status legend (added during v1.0-RC consolidation)

Each amendment below carries a **Status:** line classifying it for the v1.0 release candidate:

  • FROZEN - normative decision shipped + tested + stable for at least two slices; folded into v1.0-RC verbatim.
  • SUPERSEDED - made obsolete by a later amendment (cross-referenced).
  • OPEN - partial / experimental / has documented gaps; v1.0 ships it as-is with v1.1+ evolution path.
  • REVERTED - tried and rolled back (none in the v0.1..v0.6 corpus).

Counts at v1.0-RC: 63 FROZEN, 15 SUPERSEDED, 10 OPEN, 0 REVERTED (88 total).

Counts at v1.0-RC2 (v0.9 spec freeze): 66 FROZEN-or-FROZEN-MVP (63 FROZEN + 3 FREEZE-MVP), 15 SUPERSEDED, 7 DEFER-V1.1, 0 REVERTED (88 total). The 7 DEFER-V1.1 amendments retain their OPEN-style semantics for the v1.0 stability surface (they ship in v1.0 as-is, MAY evolve in v1.x); the v0.9 freeze-prep slice records the RFC track and the v1.1 promotion path in SPEC_FREEZE_V0_9_NOTES.md. The 3 amendments reclassified to FREEZE-MVP (A15, A31, A49) lock the MVP behaviour as the v1.0 normative contract; any v1.1+ extension lands as a new additive amendment that does not change MVP semantics.

Counts at v1.0-RC3 (v0.12 spec polish, 2026-05-25): unchanged amendment ledger (88 total). RC3 is a docs-only polish that:

  • Promotes operator precedence to normative spec §11.1.1 (closes the v0.11 surfacing of KNOWN_ISSUES #10).
  • Splits §3.3 into reserved / contextual / reserved-for-future-use keyword subsections and adds the 20 lexer keywords missing from RC2's list (closes KNOWN_ISSUES #12; covers Python-impl Findings #8, #9, #12, #16).
  • Codifies the 16 Python-impl ambiguities from dev/history/notes/PYTHON_IMPL_V0_11_NOTES.md into normative prose.
  • Adds candidate amendments A110 (HTML interpolation lexing layer) and A111 (runtime / static enforcement of requires clauses) as v1.0-OPEN — deferred-to-v1.1+. Neither is allocated a number in this file until they ship in a v0.12+ slice; they are tracked in SPEC_RC3_V0_12_NOTES.md.

See docs/spec/CHANGELOG.md for the chronological log, docs/spec/v1.0-rc.md for the consolidated normative spec, and dev/history/notes/SPEC_RC3_V0_12_NOTES.md for the per-finding dispositions.

A1 — Decimal size-literal suffixes k and M (slice 2)

Status: FROZEN - Decimal size-literal suffixes k/M shipped slice 2; lexer stable through v0.6.

Spec §3.4 defines SIZE_LITERAL as \d+(B|KiB|MiB|GiB). Slice 2 adds two decimal (base-10) suffixes for count-style contexts (e.g. mailbox depth, queue length):

Suffix Meaning Example
k × 1 000 1k = 1 000
M × 1 000 000 2M = 2 000 000

The lowercase k and uppercase M (rather than m) avoid collision with DURATION_LITERAL's m suffix (= minutes). KiB/MiB/GiB remain binary (×1024, ×1 048 576, ×1 073 741 824). Lowercase m remains a duration unit; uppercase K is reserved for a future amendment (likely as an alias of KiB).

Tokenization: both k and M lex as SIZE_LITERAL. Semantic interpretation is the consumer's responsibility (e.g. the sandbox/budget block loader).

Why this choice: lowercase k matches the conventional SI-prefix shorthand seen in 1k-style limits across most ecosystems. Uppercase M distinguishes million from minute without forcing a non-standard collision. The dispatch suggested all-lowercase, but that collided with the slice-1 duration suffix already in use across every example.

A2 — Expression-position turbofish Path::[T1, T2] (slice 2)

Status: FROZEN - Turbofish Path::[T,U] shipped slice 2; parser stable through v0.6.

Spec §6.2 uses Path[T1, T2] in type position (e.g. Map[Str, Json]). Expression position is ambiguous because Map[k] already denotes index access.

Slice 2 adopts the Rust-flavored turbofish: in expression position, Path::[T1, T2] carries the generic arguments. Examples:

let m = Map::[Str, Json]{}
let s = Some::[I32](42)

The :: disambiguates from Path[index]. Type position is unchanged — Result[T, E], Map[K, V] etc. retain the bracket-only form per spec §6.2.

A3 — Keyword-tolerant .method and .field (slice 2)

Status: FROZEN - Keyword-tolerant .method/.field shipped slice 2; widely used.

After a . in expression position, the parser accepts any keyword token as a method or field name. This lets library APIs use reserved words:

dom.on("click", h)      // `on` is a keyword
x.match                 // `match` is a keyword
agent.spawn()           // `spawn` is a keyword

Outside .-postfix position, identifiers must remain non-keyword. This is the same trick rustc uses for raw identifiers, without the r# syntax — a method-position keyword is unambiguous because the preceding . separates it from any statement context.

A4 — Keyword-tolerant effect names (slice 2)

Status: FROZEN - Keyword-tolerant effect names shipped slice 2.

effect clauses accept keyword tokens as effect names:

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

Spec §10 does not enumerate effect names; allowing keywords matches the spec §34 example which lists spawn as an effect.

A5 — run <expr> as an expression form (slice 2)

Status: FROZEN - run form shipped slice 2 (slice 3+ restricts to sandbox/budget).

A new RUN_EXPR CST node introduces run <expr> as a leading-keyword expression, parseable anywhere an expression is allowed. This is the form used in sandbox bodies per spec §16.1:

sandbox X with { ... } { run job(input)? }

Slice 2 does not constrain where run can appear; slice 3 (the type checker) is expected to restrict it to sandbox and budget contexts.

A6 — if let Pattern = expr { ... } (slice 2)

Status: FROZEN - if let shipped slice 2; widely used.

if let parses as the existing IF_EXPR CST shape with an optional leading LET_KW, pattern, and = before the scrutinee. Spec §13 describes the construct in prose; slice 2 makes it grammatical.

The CST shape (single IF_EXPR kind) keeps the AST view and formatter simple; HIR lowering branches on LET_KW presence into distinct HirExpr::If vs HirExpr::IfLet variants.

A7 — ? strictly requires Result-returning enclosing fn (slice 3)

Status: FROZEN - Strict ? rule shipped slice 3 (MT2010/MT2011 stable).

Spec §17 implies ? propagates errors only inside a Result-returning function but doesn't state this as a hard rule. Slice 3's type checker makes it explicit: expr? requires the enclosing function's return type to be Result[_, _] and the operand to 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.

Examples 06 and 11 escape the strict rule only because of the slice-3 permissive tolerance policy (see §A10): work, step, job, etc. are unknown identifiers whose call sites synthesise to fresh inference variables, and Var? is short-circuited to a fresh variable rather than triggering MT2010. Slice 4 will tighten this: once those scopes (agent state, supervisor scope, capability narrow) become first-class, those examples will need explicit Unit!WorkErr / Unit!RunErr return types.

A8 — Integer-literal defaulting to I32 (slice 3)

Status: SUPERSEDED - Superseded by A19 (explicit defaulting pass in slice 4).

Unsuffixed integer literals (42, 0) have the type IntInfer, which unifies permissively with any concrete integer kind via context. If a literal participates in inference but is never forced to a concrete type by context, slice 3 surfaces it in diagnostics as {integer}. Slice 4 will add an explicit defaulting pass that promotes leftover IntInfer to I32 and FloatInfer to F64 (Rust-style).

Suffixed literals (42_u64, 3.14_f32) take the suffixed type directly and never enter IntInfer / FloatInfer.

A9 — String, Bytes, primitive type names live in both type and value namespaces (slice 3)

Status: FROZEN - Primitive names in both namespaces shipped slice 3; stable.

String("hello") calls the String constructor; let x: String = ... annotates with the String type. Slice 3 treats primitive type names as both type-namespace aliases (for annotation positions) and (via the prelude's opaque-ADT representation) value-namespace identifiers (though value-position references resolve to fresh inference variables rather than concrete callables — slice 3 does not yet model primitive constructors).

A10 — Built-in method table (slice 3)

Status: SUPERSEDED - Permissive method table superseded by A17 (slice 4) + A65/A65.c (v0.3) strict scopes; opaque prelude still uses table residually.

Slice 3 cannot do full trait-dispatch method resolution. It maintains a permissive built-in method table mapping method names (len, get, ok_or, read, write, embed, post, encode, serve, ...) to permissive (variadic, fresh-var return) signatures. Unknown methods on opaque receivers silently produce fresh inference variables (rather than MT2007 unknown_method) to keep the canonical examples compiling without a full standard library.

The table lives in crates/mty-types/src/prelude.rs::build_prelude. Slice 5 will replace this with real impl-block resolution once trait coherence lands.

A11 — Anonymous error unions T!{A, B} resolve to Result[T, Error] (slice 3)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Anonymous error unions still resolve to Result[T, Error] sentinel in v1.0; first-class union ADTs tracked in RFC-001. See SPEC_FREEZE_V0_9_NOTES.md.

Spec §17.2 introduces T!{A, B} as sugar for an anonymous error union type. Slice 3 does not yet model anonymous union types as first-class ADTs; it resolves them to Result[T, Error] (where Error is the poison sentinel that unifies permissively with any concrete error). This keeps example 04 (which uses Page!{NetErr, ParseErr}) compiling without forcing a v0.2-style union machinery in slice 3.

A12 — Postfix ? and ! require their Msg identifier on the same line (slice 3)

Status: FROZEN - Same-line postfix ?/! rule shipped slice 3; stable.

Slice 2 disambiguated expr? (propagate) from expr?Msg(args) (ask) by trivia-skipping lookahead. This glued multi-line code such as

let body = fetch(url)?
parse(body)?

into a single fetch(url)?parse(body)?Ok(...) ask chain. Slice 3 adds a same-line-aware lookahead: if the trivia between ? (or !) and the next identifier contains a newline, the postfix is treated as plain propagate (QUESTION_EXPR) or boolean-not, never as ask/send sugar.

A13 — Copy derivation set for slice 4

Status: SUPERSEDED - Hardcoded Copy set superseded by A26 #[derive(Copy)] in slice 5.

Spec §7 doesn't enumerate which types are Copy. Slice 4 hardcodes the set rather than driving it from a derive(Copy) annotation (slice 5 adds that). Slice-4 Copy types:

  • All primitives: Bool, all Int, all Float, Char, Unit, Duration, Size
  • Shared references &T; raw pointers *T; function pointers
  • Str (the slice; the heap-owning String is NOT Copy)
  • Tuples and arrays of Copy elements
  • Opaque prelude ADTs (Url, Page, Logger, agent types, ...) — BOLD slice-4 decision to keep canonical examples compiling

Not Copy: mutable references, user-declared structs/enums, String, Bytes, Param/Var. Slice 5 will replace the opaque-Copy rule with real per-type derive(Copy).

A14 — Sendable set for cross-agent messages (slice 4)

Status: SUPERSEDED - Conservative Sendable set superseded by A65.b full Sendable trait in v0.3.

Spec §7.6 requires cross-agent values to be "owned, copied, shared immutable, or serialized" but doesn't formalise the membership test. Slice 4 implements Sendable:

  • Copy types (other than references and raw pointers) — yes
  • Owned String and Bytes — yes
  • Tuples / arrays where every element is Sendable — yes
  • Opaque ADTs — yes (BOLD permissive; slice 6 audits with a real serializable-shape registry)
  • User struct/enum ADTs — yes iff every variant payload is Sendable
  • References (&T, &mut T), raw pointers, function pointers — no
  • Param/Var — yes (conservative permissive; slice 5 trait bounds tighten via a Send bound)

Args to !Msg(args) and ?Msg(args) are checked at the call site and emit MT3011 non_sendable_message_arg on failure.

A15 — Arena escape: direct-naming MVP (slice 4)

Status: FREEZE-MVP (was OPEN at v1.0-RC) - Direct-naming MT3010 is the v1.0 normative contract. Sound (never lets a value escape with a dead-arena borrow); incomplete (some programs that should be safe are statically rejected). Indirect-flow detection ships as a separate additive amendment in v1.1+. See SPEC_FREEZE_V0_9_NOTES.md.

Spec §7.5 says "values allocated inside an arena cannot escape unless copied, moved through an allowed promotion, or returned as owned values independent of the arena". Slice 4's MVP enforces the direct-naming case: if an arena body's tail expression is a path whose root binding is an arena-local non-Copy local, emit MT3010 arena_escape. Indirect flow (e.g. a fn that captures and returns the value) is post-v0.1.

A16 — Match exhaustiveness is an error (slice 4)

Status: FROZEN - MT2015 promoted to Error in slice 4; stable.

Slice 3 emitted MT2015 non_exhaustive_match at Warning severity. Slice 4 promotes it to Error. The diagnostic code and the underlying coverage logic are unchanged.

A17 — Method dispatch policy (slice 4)

Status: FROZEN - Method dispatch policy shipped slice 4; trait coherence (A24) layers on top.

User-declared struct/enum receivers require an impl block method; unknown methods on a user ADT emit MT2007 unknown_method. Opaque prelude ADTs and primitives keep the slice-3 permissive built-in table (variadic, fresh-var return) so canonical examples that call arbitrary methods on opaque receivers (url.parse(...), etc.) continue to compile. Slice 5 replaces the built-in table once trait coherence lands.

A18 — Protocol-aware agent handler params (slice 4)

Status: SUPERSEDED - Warning-only check superseded by A28 (strict MT4030..MT4033) + A65.c (strict types).

on Msg(p1, p2) handler parameters take their types from the first matching message in any implemented protocol. If no protocol declares the message, handler params fall back to fresh inference variables and the compiler emits MT2026 protocol_msg_unknown (warning).

A19 — Integer/float defaulting pass (slice 4)

Status: FROZEN - Defaulting pass shipped slice 4; closes A8 deferral.

Closes the A8 deferral. After each fn body / agent handler / state initializer / supervisor child is type-checked, the side-table walker rewrites any remaining Int(IntInfer) to I32 and Float(FloatInfer) to F64. Diagnostics and downstream consumers (the borrow checker, future codegen) see concrete primitives.

A20 — Lexical borrow regions (Rust 2015 style) (slice 4)

Status: SUPERSEDED - Lexical regions superseded by A55 NLL last-use deactivation in v0.3.

A borrow's region is the innermost enclosing block of the borrow expression. On block exit, the borrow is considered to decay and the source local's Borrowed{n} / BorrowedMut state releases. This is the conservative MVP; NLL / Polonius is post-v0.1 and will let some currently-rejected programs through.

A21 — Scope-aware tolerance for unresolved values (slice 4)

Status: SUPERSEDED - Unconditional tolerance superseded by A65 scope-aware policy in v0.3.

Closes the slice-3 "opaque tolerance" deferral. Single-segment unresolved value names now emit MT2021 unresolved_value unless:

  • the body is in tolerance_open mode (inside unsafe, sandbox, budget, arena bodies, supervisor child expressions, and extern block contents), OR
  • the name appears in the per-body tolerance set (agent state names, agent ctor-param names, agent method names — for bodies inside the agent), OR
  • the name resolves through the prelude (log, panic, spawn, ...).

Multi-segment paths whose first segment is a known module / opaque ADT / local / tolerated identifier remain permissive. Top-level fn bodies have an empty tolerance set — they must declare everything they call (e.g. via extern { fn ... }).

A22 — Effect inference algorithm (slice 5)

Status: FROZEN - Effect inference algorithm shipped slice 5; stable through v0.6.

Spec §9 introduces effects but doesn't pin the inference algorithm. Slice 5 chooses bottom-up + fixpoint over the call graph:

  1. Initial pass: walk every fn body, accumulating an effect set from syntactic constructs (arena → alloc, spawn → spawn, deadlines → time, capability method/path → corresponding cap effect, container methods → alloc, agent send/ask → spawn, etc.).
  2. Fixpoint pass: for each fn, union the inferred effects of every fn it calls (resolved by name) plus that fn's declared effects. Iterate until no set changes; bound at 32 iterations.
  3. Public-fn discipline: every pub fn with a non-empty inferred effect set must have a declared effect ... clause that is a superset. Else MT4001 effect_undeclared.

Capability-style call detection is heuristic (path-prefix on receiver: net.get(...), fs.read(...), etc.). Refinement to per-receiver typed dispatch is post-v0.1.

A23 — Capability narrowing constraints (slice 5)

Status: FROZEN - Capability narrowing constraints shipped slice 5; stable.

Spec §8.1 mentions fs.ro("/data") without specifying the constraint algebra. Slice 5 models five constraint kinds:

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

Subsumption (narrower-or-equal): Any accepts anything; identical constraints accept each other; Path subsumes prefix-of-prefix; Host subsumes set-subset; And is narrower iff any element is.

Slice 5 rejects broaden-via-cast at call sites with MT4010 capability_too_broad. Built-in narrowing constructors in slice 5: cap.ro(path), cap.path(path), cap.host(host).

A24 — Trait coherence + dispatch (slice 5)

Status: FROZEN - Name-only trait coherence shipped slice 5; generic-arg overlap detection deferred to v1.1+.

Slice 5 ships name-only trait coherence: at most one impl Trait for Type per (trait, self-type) pair; duplicate triggers MT4022 trait_coherence_violation. Generic-argument overlap detection (e.g. impl Hash for Vec[T] vs impl Hash for Vec[U64]) is post-v0.1.

Method dispatch order on a user ADT: 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.

A25 — dyn Trait object safety (slice 5)

Status: FROZEN - dyn Trait object safety shipped slice 5; conservative rules stable.

dyn Trait is parsed as a type. Slice-5 conservative object-safety rules ban any trait whose declared methods: - mention Self in any parameter or return type, OR - have method-level generic parameters.

Violation: MT4023 dyn_requires_object_safe. Slice 5 does not implement a full coercion sugar — let h: dyn Trait = value is the only entry point and the receiver type must have a registered impl.

A26 — Derive set (slice 5)

Status: FROZEN - Derive set shipped slice 5; supersedes A13.

Slice 5 supports #[derive(Copy)], #[derive(Hash)], and #[derive(Eq)]. The bracketed form #[derive(...)] is the canonical spelling; the parser also accepts a leading-keyword shorthand derive Copy for ease of LLM-generated source. Other derive names emit MT4041 derive_unknown.

Copy validation: every field's type must itself be Copy (or in defs.user_copy); otherwise MT4040 derive_copy_field_not_copy.

Hash / Eq register a synthetic TraitImpl entry so dyn Hash/dyn Eq coercions resolve. No method body is generated — slice 5 lacks codegen.

A27 — Top-level sandbox items (slice 5)

Status: SUPERSEDED - Metadata-only sandbox parsing superseded by A43 (slice 7 runtime enforcement).

Spec §16.1 places sandbox at the top level. Slice 5 parses and lowers sandbox Name with { entries } { body } as a new HirItem::Sandbox variant. Type-checking treats the body as unit-typed under sandbox tolerance. Runtime semantics arrive in later slices.

A28 — Strict protocol-handler checks (slice 5)

Status: FROZEN - Strict protocol-handler checks shipped slice 5; supersedes A18.

Slice 4 emitted a warning (MT2026) for on Msg referring to an unknown protocol message. Slice 5 promotes this to a hard error when the agent's declared protocols are known to the type checker (declared in the same package or visible via import):

  • MT4030 protocol_arity_mismatch — handler param count ≠ protocol message arity.
  • 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.

When ANY of an agent's declared protocols is unknown (typical for external-package protocols like http.Handler), the strict checks are skipped and the slice-4 MT2026 warning still applies.

A29 — move *ref is MT3009 (slice 5)

Status: SUPERSEDED - Reserved-only MT3009 superseded by A56 precise emission in v0.3.

Slice 4 deferred precise modelling of move *r where r: &T. Slice 5 flags such expressions as MT3009 move_out_of_ref. (Implementation: the borrow walker's Move visitor detects a deref-of-ref operand and emits MT3009 instead of silently proceeding.)

A30 — Strict-profile alloc ban (slice 5)

Status: FROZEN - Strict-profile alloc ban shipped slice 5; A65.d ratifies in v0.3 conformance.

When mighty.toml declares profile = "core", any public fn whose inferred effect set contains alloc triggers MT4002 alloc_in_core. The default profile is host (permissive). This matches spec §9's "strict profile mode" clause.

A31 — Arena runtime enforcement deferred to slice 7 (slice 6)

Status: FREEZE-MVP (was OPEN at v1.0-RC) - Static MT3010 (A15, borrow-check) + bumpalo allocator (A50) + interpreter auto-charging (A99) are the v1.0 normative arena runtime contract. The runtime MT5007 arena_escape_runtime trap stays reserved for v1.1+ — it would activate only for the indirect-flow case that A15's static check does not yet cover, and that flow is unreachable in v1.0 dogfood. No source-level v1.0 program triggers the gap. See SPEC_FREEZE_V0_9_NOTES.md.

Spec §10 places arena lifetimes at the heart of the deterministic memory model. Slice 6 lowers arena <name> { body } to ArenaPush(id) / ArenaPop(id) MtyIR sentinels and tracks an arena stack per interpreter frame, but it does not enforce that values escape with a borrow tied to the active arena scope — borrow-check MT3010 covers that statically, and the slice-7 runtime will enforce again at allocation/free time. MT5007 arena_escape_runtime is reserved for that future trap.

A32 — Slice-6 agent dispatch is synchronous (slice 6)

Status: SUPERSEDED - Synchronous slice-6 dispatch superseded by async tokio-backed dispatch (slice 7) and A70 cancellation.

Spec §13–§14 describe asynchronous, mailbox-backed agent dispatch. Slice 6's interpreter dispatches agent!Msg(args) and agent?Msg(args) synchronously by calling the handler fn directly (single-threaded, deterministic, no queue). Real mailbox slabs, work-stealing, and supervisor restart arrive in slice 7. The @<duration> deadline syntax parses and lowers to metadata on the Ask rvalue but does not affect slice-6 execution.

A33 — Effect calls dispatched via Host trait (slice 6)

Status: FROZEN - Effect/Host trait dispatch shipped slice 6; stable.

Effect-marked operations (fs.read(path), net.get(url), model.embed(q), etc.) lower to Stmt::EffectInvoke{effect, op, args, out}. The interpreter forwards the call to its Host trait. The default host (RealHost for mty run, BufferHost for tests) returns deterministic stub values (typically Value::Unit or an empty string); it does not perform real I/O. Slice 7 wires the runtime's syscall surface into the same trait, so test-time hosts and production hosts share a single interface.

A34 — Budgets + sandboxes are metadata in slice 6 (slice 6)

Status: SUPERSEDED - Metadata-only budgets/sandboxes (slice 6) superseded by A43+A70+A99 runtime enforcement.

Spec §16 defines budget { ... } run body and sandbox Name with { ... } { body }. Slice 6 lowers these by emitting the body unchanged; the entries are not enforced at run time. The borrow checker already validates the syntactic shape; the slice-7 runtime will enforce CPU / wall / memory / mailbox-depth / path / host budgets. MT5009 budget_exceeded and MT5010 sandbox_violation are reserved for that future enforcement.

A35 — Slice-6 interpreter is single-thread deterministic (slice 6)

Status: FROZEN - Slice-6 deterministic interpreter shipped; A39 deterministic mode lifts to runtime.

The slice-6 interpreter is fully deterministic given the same MtyIR Program and Host: single-threaded, no work stealing, no system clock reads, no RNG (unless the host injects one), HashMap iteration ordered by index. This determinism backs the runtime conformance corpus (tests/conformance/runtime/). Slice 7's work-stealing scheduler will introduce a separate deterministic mode matching spec §25.5.

A36 — std.http.serve MVP shape (slice 7)

Status: SUPERSEDED - Slice-7 in-memory http.serve shape superseded by A96 (real socket bind, agent dispatch).

Slice 7 ships a minimal std.http server. The runtime exposes:

  • parse_request_line(bytes) -> Option<Request> — parses an HTTP/1.1 GET request line (GET /path?q=x HTTP/1.1).
  • serve_in_memory(handler) — binds 127.0.0.1:0 (returns the allocated port), accepts connections, parses the first request line, and invokes the handler. Handler returns (status: u16, body: String) which is serialised as a plain text HTTP/1.1 response.

http.serve(":8080", 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. Slice 7 ships the primitives; full agent-bound serving with rich Request/Response records is a slice-8 stdlib deliverable.

Slice 7 deliberately punts on streaming bodies, headers beyond Content-Type, HTTPS, and HTTP/2.

A37 — Slice-7 memory budget approximation (slice 7)

Status: SUPERSEDED - Approximate slice-7 memory budget superseded by A50 (bumpalo) + A99 (auto-charging) in v0.5.

Without a real arena allocator (slice 8 work), the slice-7 mem_bytes budget counter is approximate: the runtime records bytes only via explicit BudgetTracker::record_mem(n) calls. The MtyIR interpreter does not auto-count allocations, so a program can breach in production that slice 7's tests miss. Slice 8 wires the real allocator + per-allocation byte charging.

A38 — Telemetry JSON schema (slice 7)

Status: SUPERSEDED - OTLP-flavoured JSON superseded by A71 (real OTLP wire-format) in v0.3.

Slice 7 emits structured logs as one JSON object per event line on stderr (or STARDUST_TRACE=file:PATH). The schema is OpenTelemetry-flavoured but not strict OTLP. 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; additional fields vary per kind. Strict OTLP wire format ships in slice 8 (with the codegen).

A39 — Deterministic mode (slice 7)

Status: FROZEN - Deterministic mode shipped slice 7; A106 keeps single-worker pin under deterministic(seed).

RuntimeBuilder::deterministic(seed) swaps the tokio executor for the current-thread runtime and exposes a seeded XorShift* RNG and LogicalClock. Slice 7 ships the executor swap and the primitives; the full test deterministic block lowering and replay-diff harness arrive with slice 8 codegen. Replay invariant (still slice-7 valid): given the same MtyIR program and same seed, the emitted telemetry sequence is byte-identical.

A40 — Mailbox defaults (slice 7)

Status: FROZEN - Mailbox depth/policy defaults shipped slice 7; A72 adds slab-pool optimisation underneath unchanged API.

Default mailbox depth is 1024 frames; default send policy is Block (sender awaits capacity). Per-agent budgets can override both via the mb (depth) and mb_policy (Block/Drop/Fail) entries. A full mailbox under Drop silently discards; under Fail it returns MT5012 to the sender; under Block (default) the sender backpressures.

A41 — Slice-7 cancellation semantics (slice 7)

Status: SUPERSEDED - Between-turn cancellation superseded by A70 cooperative mid-turn cancellation in v0.3.

task scope @D and ?Msg(args) @D deadlines fire at the next await point. The slice-6 per-turn evaluator is synchronous from the executor's view, so a deadline cannot pre-empt a running turn; it cancels the next queued turn. This is acceptable in slice 7 because every turn is bounded by an interpreter step budget (default 1 000 000 steps); a single turn cannot run forever. Slice 8 will integrate cooperative cancellation into native code.

A42 — restart up_to N in DUR semantics (slice 7)

Status: FROZEN - Restart window semantics shipped slice 7; stable.

Slice 7's RestartTracker keeps a sliding window of restart timestamps and denies the (N+1)-th restart attempt within DUR. On denial the supervisor escalates per its strategy (escalate → parent supervisor; top-level → RuntimeError::SupervisorEscalated trap with MT5013). Backoff between restarts is uniform-jittered between the configured min and max (default 0 ms); the jitter RNG is deterministic given a fixed rng_seed.

A43 — Top-level sandbox executes as a child runtime (slice 7)

Status: FROZEN - Top-level sandbox runtime execution shipped slice 7; supersedes A27.

A27's metadata-only sandbox Name with {...} { body } (slice 5) gains runtime execution: at body entry the runtime constructs a child BudgetTracker from the entries and pushes it onto the active budget stack. Capability calls inside the body are checked against the child's allowlists; breach traps with MT5015. Nested sandboxes compose by stacking budgets; the inner sandbox's allowlist must be a subset of the outer (slice 7 enforces intersection at allowlist construction time).

A44 — Slice-7 deref-of-ref write path (slice 7)

Status: FROZEN - Deref-of-ref write path shipped slice 7; stable.

Slice 6's Interp::assign_place treated Projection::Deref writes as a no-op (refs were opaque). Slice 7 added a deref-of-ref write path: 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. Both the new run_handler_isolated entry point and the slice-6 sub-interp path benefit; slice-6 invoke_handler now delegates to run_handler_isolated rather than its earlier "field 0 = reply int" counter heuristic. The 290 baseline tests pass unchanged; the counter example (08) now returns the correct 1, 2, 3 sequence under both mty run and the programmatic Runtime API.

A45 — mty run --legacy-interp opt-out (slice 7)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Flag retained for diagnostic value; deprecation review at v1.1 once codegen covers the full MtyIR surface (currently blocked by A49's strip-generics MVP). See SPEC_FREEZE_V0_9_NOTES.md.

mty run <file> defaults to the slice-7 runtime path (pipeline::run_file_with_runtime). --legacy-interp invokes the slice-6 synchronous interpreter via pipeline::run_file. The flag exists for diagnostic comparison during slice 7 stabilisation; it will likely be removed (or repurposed) in v0.2 once the runtime is the only execution path.

A46 — Cranelift-only native backend, LLVM scaffolded (slice 8)

Status: FROZEN - Cranelift default backend + LLVM scaffold shipped slice 8; LLVM activation still gated on build host.

Spec §24.5 calls for LLVM as the native backend, with Cranelift (§24.6) as a fast secondary path. Slice 8 inverts the priority for v0.1 because the build host had no LLVM/llvm-config available, and the inkwell-based scaffold would have failed to compile. The decision:

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

This trades LLVM's optimization quality for a v0.1 that actually ships. Cranelift produces correct, working binaries at acceptable speed; LLVM-quality optimization is a v0.2 win.

A47 — Wasm Component Model deferred to v0.2 (slice 8)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Core modules are the v1.0 normative contract; full wit-component wrapper + WIT auto-binding + preview2/wasi-cli integration tracked in RFC-002. See SPEC_FREEZE_V0_9_NOTES.md.

Spec §24.7 calls for emitting Component Model wrappers via wit-component. Slice 8 ships core Wasm modules (via wasm-encoder 0.250) with capability imports declared as ordinary function imports under the mighty module namespace. The component-model wrapper, WIT auto-binding, and full preview2/wasi-cli host integration land in v0.2.

A hand-written WIT sketch lives at docs/internals/codegen-wasm.md documenting the eventual shape.

A48 — mty run defaults to JIT (slice 8)

Status: FROZEN - mty run JIT-then-fallback shipped slice 8; stable.

mty run previously executed via the slice-7 runtime, which itself called the slice-6 interpreter per turn. Slice 8 changes the default:

  1. Try sdust_codegen_cranelift::jit::build_jit first.
  2. On CodegenError::Unsupported(_) (the slice-8 backend rejects the MtyIR shape), fall back to pipeline::run_file_with_runtime (the slice-7 path).
  3. --legacy-interp (A45) still routes to the slice-6 synchronous interpreter directly.

The Unsupported fallback is opaque to the user — programs simply run.

A49 — Per-(fn, type-args) monomorphization (slice 8)

Status: FREEZE-MVP (was OPEN at v1.0-RC) - The strip-generics MVP is the v1.0 normative contract. Sound (generics type-check; calls route through the slice-7 interpreter fallback per A48); v1.1+ full specialisation ships as a purely additive optimisation (programs that ran under the fallback in v1.0 keep running). See SPEC_FREEZE_V0_9_NOTES.md.

Spec §24.5 leaves the monomorphization strategy open. Slice 8 picks the simple route: each generic fn called with concrete type-args gets its own specialized MtyIR fn before codegen. Code-bloat is accepted as the v0.1 cost. Size-optimized shared-generic dispatch (v0.2) will unify identical instantiations.

Slice-8 MVP simplification: the monomorphizer 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.

A50 — bumpalo-backed arenas with byte-charging (slice 8)

Status: FROZEN - bumpalo-backed arenas with byte-charging shipped slice 8; supersedes A37.

Slice 7's arena was an "approximate byte counter" (A37) — no real allocation, no real free. Slice 8 ships a real arena via bumpalo:

  • arena {} scope 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.

The codegen-cranelift runtime ABI bridge (sdust_runtime::codegen_abi) routes ArenaPush / ArenaPop / alloc statements through this type. The slice-6 interpreter still uses its byte-counter for the legacy path.

A51 — Codegen trap codes MT8001..MT8010 (slice 8)

Status: FROZEN - MT8001..MT8010 codegen trap codes reserved + emitted slice 8; stable.

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

  • 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 monomorphization failed

All have mty explain SD8xxx entries.

A52 — Native linker discovery order (slice 8)

Status: FROZEN - Native linker discovery order shipped slice 8; stable.

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

  1. $STARDUST_LINKER env var.
  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, not MSVC).

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

A53 — extern { fn ... } resolved via libloading (slice 8)

Status: FROZEN - libloading-resolved externs shipped slice 8; stable.

Each extern { fn foo(...) } declaration in user source resolves at runtime against:

  • A per-name override from mighty.toml's [extern] table (e.g. "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 at the call site.

A54 — Field-level borrow tracking via Place algebra (v0.3)

Status: FROZEN - Place-algebra borrow tracking shipped v0.3; depth-1 truncation noted as future work but contract stable.

The slice-4 borrow checker tracked aliasing at whole-local granularity: &mut s blocked &s.field even when no aliasing actually existed. v0.3 promotes the per-local map to a BorrowLedger keyed by Place:

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

Two places overlap iff one is a prefix of the other. New borrows conflict iff their Place overlaps any existing record's Place; disjoint fields (s.a vs s.b) coexist.

v0.3 truncates Place projections at depth 1 — deeper paths (s.a.b) fold to s.a for conflict purposes. This is conservative (rejects programs Rust would accept) but sound. Lifting the truncation is post-v0.3.

Index edges collapse to a single "any index" projection: arr[i] and arr[j] conflict in v0.3.

Module: crates/mty-borrow/src/place.rs. Ledger in state.rs::BorrowLedger. Conflict resolution in flow.rs::try_place_borrow.

A55 — NLL last-use deactivation (v0.3)

Status: FROZEN - NLL last-use deactivation shipped v0.3; supersedes A20.

The slice-4 lexical region was: a borrow ends at the lexical scope of the borrower binding. v0.3 ships a hand-rolled NLL approximation: a borrow ends at the last use of its borrower binding (in source order).

Algorithm per fn body:

  1. Pre-pass (nll::compute_last_use): walk the typed HIR in source order, assign a monotone ProgramPoint to every Path expression, record the highest point each name appears at.
  2. Main walker: advance current_point on every Path read in lockstep with the pre-pass. After each Path use of name, if current_point - 1 >= last_use[name], decay every ledger record whose borrower == name.

The borrower binding is captured in let r = &x via a pending_borrower hand-off in walk_stmt; the Borrow { .. } handler stamps the new ledger record with the pending borrower's name.

Approximation level. NOT polonius. We do NOT model: - Two-phase borrows - Borrow held on one branch of a diamond (ledger join is conservative) - Loop back-edge borrows

These are flagged in BORROW_V0_3_NOTES.md for v0.4.

Module: crates/mty-borrow/src/nll.rs. Decay hook in flow.rs::maybe_decay_after_use.

A56 — Precise MT3009 for move *ref (v0.3)

Status: FROZEN - Precise MT3009 emission shipped v0.3; supersedes A29.

Slice 4 reserved MT3009 (move_out_of_ref) but never emitted it. v0.3 implements:

  • let x = *r where expr_ty[r] = Ref { inner } and inner is non-Copy → MT3009.
  • let x = move *r (explicit move) — same check.
  • let x = *r where inner IS Copy → accepted (load through the ref).

Message names the reference for clarity: cannot move out of *r: dereferencing a reference does not transfer ownership

Trichotomy with neighbouring codes: | 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 |

Detector: flow.rs::check_deref_move. Message constructor: diag.rs::move_out_of_ref_named.

A70 — Cooperative mid-turn cancellation (v0.3)

Status: FROZEN - Cooperative mid-turn cancellation shipped v0.3; supersedes A41.

Closes A41 ("deadline arrives at next await"). The slice-7 runtime ran each agent turn synchronously and could only fire deadlines between turns. v0.3 wraps every per-turn run_handler_isolated call in tokio::task::spawn_blocking and races the resulting JoinHandle against a tokio_util::sync::CancellationToken. When the per-turn wall-budget timer expires the token is fired with CancelReason::WallBudget; the parent task drops the join handle (detaches the interpreter thread), emits a BudgetBreach event with MT5009, and notifies the caller's ask-side reply oneshot with RuntimeError::BudgetExceeded.

Cancellation reasons:

Reason SD5xxx 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

The blocking thread is detached, not joined: a runaway handler is bounded only by the MtyIR interpreter's step budget (default 1 000 000). That guarantees the worst-case wall time of the detached thread is finite without making the async runtime wait for it.

Reply notification is exactly-once: the frame's reply sender is moved into a shared Mutex<Option<...>> slot before scheduling, and the cancel arm and blocking shim race to .take() it. Whoever wins sends; the other no-ops. No double-send, no hang.

Implementation: crates/mty-runtime/src/cancel.rs, crates/mty-runtime/src/agent.rs::run_one_turn_async.

A71 — OTLP wire-format telemetry (v0.3)

Status: FROZEN - Real OTLP wire-format shipped v0.3; supersedes A38.

Closes A38 ("OTLP-flavoured JSON, not strict OTLP"). v0.3 adds a real opentelemetry_sdk::TracerProvider configured with opentelemetry_otlp::SpanExporter over gRPC (tonic). Activation is env-driven and best-effort:

  • STARDUST_OTLP_ENDPOINT=<url> set → real OTLP export
  • otherwise → slice-7 JSON-line emitter unchanged

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

Spans use the mighty.* semantic-convention namespace — mighty.turn.start, mighty.send, etc. — with the slice-7 event fields promoted to OTel attributes. Resource attributes carry service.name = "mighty-runtime" plus the crate version. See docs/internals/telemetry-otlp.md for the full attribute table.

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

A72 — Slab-pool mailbox frames (v0.3)

Status: FROZEN - Slab-pool mailbox frames shipped v0.3; performance optimisation under A40 API.

Closes A40 ("Mailbox = bounded MPSC"). v0.3 introduces sdust_runtime::slab_pool::SlabPool, a per-mailbox pool of fixed- size payload slots reused via a LIFO free-list. Each slot is:

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

The Mailbox::send / try_send API surface is unchanged; each admitted MessageFrame carries an invisible PooledFrame handle that returns the slot to the pool on drop. Pool defaults are tunable via SlabPool::with_layout(capacity, inline_bytes); the default matches the A40 mailbox depth of 1024 frames.

When the pool is exhausted, sends still succeed: the frame uses an overflow PooledFrame whose bytes live on a standalone heap allocation. Backpressure remains correct because the mpsc channel still bounds depth; the slab is an allocation amortiser, not a secondary backpressure surface.

FIFO of messages is preserved by the mpsc backbone; slab-slot indices are LIFO for cache locality but are not observable from user programs.

Implementation: crates/mty-runtime/src/slab_pool.rs, crates/mty-runtime/src/mailbox.rs::Mailbox::admit.

A73 — Batched per-turn deadline scheduler (v0.3)

Status: FROZEN - Batched deadline scheduler shipped v0.3; stable internal infrastructure.

crates/mty-runtime/src/delay_timers.rs ships a DelayScheduler built on tokio_util::time::DelayQueue so many concurrent per-turn deadlines share a single timer wheel instead of allocating one tokio::time::Sleep per call. The default per-turn cancellation path (A70) still uses a single tokio::spawn(sleep + cancel) — fine for the common case where each agent has at most one in-flight turn — but DelayScheduler is the building block supervisors will adopt when they track many children's per-turn budgets in v0.4.

A65 — Scope-aware permissive/strict type-check policy (v0.3)

Status: FROZEN - Scope-aware permissive/strict policy shipped v0.3; supersedes A21.

Slice-3's amendment A21 ("unknown values resolve to fresh inference vars rather than MT2021") was applied unconditionally so the canonical examples kept compiling while later slices hardened other surfaces. v0.3 tightens this: each lexical scope now carries a ScopeKind and the unresolved-name fresh-var fallback only fires in permissive scopes (top-level fn, extern, macro, unsafe, arena, budget, sandbox). Strict scopes (agent body, handler body, plus the framework-marked supervisor and cap-narrow bodies) promote an unresolved name to MT2021 with a scope-aware note. The per-body tolerance set (agent state, ctor-params, sibling methods) still escapes the strict check.

SupervisorBody and CapNarrowBody are marked strict for framework consistency but currently keep tolerance_open=true so v0.2 surface (supervisor child expressions referencing not-yet-bound caps, and sandbox-with bodies using fns brought in by the runtime sandbox) continues to compile. Flipping the toggle in slice 7 activates MT2021 automatically.

Documentation: docs/internals/typeck.md "Scope-aware permissive/ strict policy (v0.3 / A65)". Tests: crates/mty-types/tests/scope_strict_agent.rs, scope_strict_supervisor.rs, scope_permissive_extern.rs.

A65.b — Sendable trait at cross-agent message sites (v0.3)

Status: FROZEN - Sendable trait shipped v0.3; supersedes A14.

v0.3 gives the cross-agent message-arg type-shape contract a formal name and definition. Sendable = a Copy type, an owned Sized value with no internal references, or a user ADT marked #[derive(Sendable)]. References (&T/&mut T), capability handles (Net/Fs/Clock/Dom/Model), dyn Trait objects, and any compound that transitively contains one are explicitly NOT Sendable.

The check fires at every HirExpr::Send / HirExpr::Ask site; violation emits MT3011 with a human-readable reason note ("contains a &T reference", "capability handle Fs does not cross agent boundaries", "field payload of Body is not Sendable: ..."). Generic / unbound types are treated permissively to avoid regressing slice-3 fresh-var inference at send-arg positions.

#[derive(Sendable)] is a pure marker: it registers a synthetic empty TraitImpl and adds the ADT to DefMap::user_sendable. The per-send check enforces the actual field-shape contract — the derive is an opt-in audit signal.

Documentation: docs/internals/sendable.md. Tests: crates/mty-types/tests/sendable_copy_passes.rs, sendable_non_copy_fails.rs, plus three unit tests in crates/mty-types/src/sendable.rs.

A65.c — MT4031 strict handler param-type check, local-protocol only (v0.3)

Status: FROZEN - MT4031 strict handler param-type check (local protocols) shipped v0.3; supersedes A18 fully.

Slice-5 only enforced arity for protocol-handler parameters (MT4030). Slice-3's permissive flow kept the types unchecked: a handler that bound its param to a fresh inference var would let any in-body usage pin the param to an arbitrary type, even when the protocol declared something incompatible.

v0.3 tightens this for local protocols (defined in the current package; identified by membership in DefMap::protocol_msg_names). The handler's params are bound to fresh inference vars, the body type-checks normally, and a final unification step compares each param's inferred type with the protocol-declared type. Mismatch fires MT4031 protocol_param_type_mismatch with both spans.

For external protocols (e.g. http.Handler referenced through a use import without its declaration in scope), the slice-5 fallback MT2026 path is preserved. This keeps canonical examples 13 and 19 compiling unchanged; once the external protocol's declaration becomes visible to defs, MT4031 will activate automatically.

Documentation: docs/internals/typeck.md, docs/internals/traits.md. Tests: crates/mty-types/tests/protocol_param_strict.rs, conformance case tests/conformance/agent_protocol/05_handler_param_type/.

A65.d — core profile rejects alloc (v0.3 conformance)

Status: FROZEN - core profile rejects alloc ratified v0.3; reinforces A30.

The slice-5 crate::effects::infer_and_validate already fires MT4002 alloc_in_core when the inferred effect set of a public fn contains alloc under the strict profile = "core". v0.3 ratifies the rule as part of the soundness contract and adds a direct unit test (core_profile_rejects_alloc) plus a conformance case shape under tests/conformance/effect_checking/05_strict_core_profile/. The conformance harness reads the workspace's mighty.toml (currently profile = "host"), so the conformance case asserts the neutral-fire outcome and defers the positive-fire to the unit test until per-case mighty.toml overrides land.

Documentation: docs/internals/effects.md.

A74 — LSP v0.5 capability expansion (v0.5)

Status: FROZEN - LSP v0.5 capability expansion shipped v0.5; single-file scope frozen for v1.0, cross-file rename deferred to v1.1+.

The v0.2 LSP MVP shipped 7 features (didOpen/didChange/didClose, publishDiagnostics, hover, definition, formatting, keyword-only completion). v0.5 closes the documented gaps by adding:

  • textDocument/semanticTokens/full + /range — 14-type + 3-modifier legend; CST-walk classifier (keywords, types, fns, params, strings, numbers, comments, operators, namespaces, enum members, type params, macros, properties); delta-encoded per the LSP wire format.
  • textDocument/rename + textDocument/prepareRename — single-file scope; validates new name is a legal Mighty IDENT and not a reserved keyword; classifies top-level vs local and restricts the walk to the smallest enclosing block for locals.
  • textDocument/inlayHint — inferred-type hints for let bindings (no : annotation) and fn parameters; viewport-filtered; uninteresting types (Var / Param / Error) suppressed.
  • textDocument/codeAction — quick fixes triggered by MT2021 (unresolved value), MT2002 (unresolved type), MT3001 (use-after-move → .clone() suggestion), MT4001 (effect undeclared → add effect { name } to fn signature). Suggestions use Levenshtein edit distance ≤ 2.
  • textDocument/signatureHelp — call + method-call sites; active parameter computed by counting depth-1 commas between ( and cursor; CALL_EXPR resolves to fn/variant; METHOD_CALL_EXPR resolves to built-in methods or impl methods.
  • workspace.workspaceFolders capability + the workspace/didChangeWorkspaceFolders and workspace/didChangeWatchedFiles notification handlers (logging only; analysis remains per-file).
  • Semantic completion: locals-in-scope (CST walk of LET_STMT + FN_PARAM of the enclosing fn), receiver-aware method/field completion after . (resolves the receiver name via expr_ty + fn_params, then enumerates impl_methods + traits.by_method + ADT fields).

Single-file decision. Cross-file rename / cross-file go-to-def require a workspace-wide resolve map that isn't yet plumbed through mty-driver. v0.5 ships the LSP protocol surface and restricts scope to the active file; the editor preview lets users catch any unintended cross-file rewrites. The follow-up slice will build the multi-file resolve.

Borrow check still deferred. The editor pipeline still skips the borrow check for latency reasons; mty check from the CLI is the authoritative borrow-check oracle.

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

Documentation: docs/internals/lsp.md, docs/reference/cli/mty-lsp.md, LSP_V0_5_NOTES.md (interpretation calls).

A80 — break / continue as real HIR nodes (v0.5)

Status: FROZEN - break/continue as real HIR nodes shipped v0.5; labelled break deferred to v1.1+.

Slice 4 parsed break and continue as identifiers; loop scanning patterns like loop { if cond { break } … } therefore never actually exited and the MtyIR interpreter only escaped via its step budget. Slice 5 adds:

  • BREAK_KW and CONTINUE_KW lexer tokens (spec §3.3).
  • Parser productions for break, break <value>, and continue as expressions (mirrors Rust); v0.5 ships unlabelled only — labelled break ('outer: loop { break 'outer }) is deferred to v0.6.
  • HirExpr::Break(Option<ExprId>) + HirExpr::Continue.
  • MtyIR LoopFrame stack on FnBuilder: lower_loop / lower_while / lower_for push (continue_target, exit_target, result_local) before lowering their body so lower_expr of Break / Continue can route the terminator correctly.
  • Type checker synths both as never (same as Return).
  • Borrow checker walks break value at Position::Move.

Documentation: docs/internals/loops.md. Tests: crates/mty-syntax/tests/parse_break_continue.rs, crates/mty-hir/tests/lower_break_continue.rs, crates/mty-sir/tests/loop_break.rs, crates/mty-sir/tests/loop_continue.rs.

A81 — Iterator protocol via __sdust_iter_next (v0.5)

Status: FROZEN - __sdust_iter_next wire protocol shipped v0.5; full trait-based iterators deferred to v1.1+.

for x in iter { body } had no exhaustion check before this slice — slice 4 wired the back-edge but the loop only escaped via budget. v0.5 introduces a minimal wire protocol so for i in 1..N and for v in arr actually terminate:

  • Ranges (lo..hi / lo..=hi) lower to TupleInit(lo, hi, inclusive_marker: Bool); the marker lets the iterator distinguish exclusive (<) from inclusive (<=).
  • The MtyIR for-loop header calls MethodCall { receiver: iter, method: "__sdust_iter_next", args: [idx] }. The result is a (exhausted: Bool, element: T) tuple. Field 0 drives the header's Term::If; field 1 is bound to the loop pattern via a new pats::lower_pat_bind helper.
  • The interpreter's permissive method table services __sdust_iter_next for ranges and arrays (crates/mty-sir/src/ interp/run.rs::eval_method).
  • All other receivers return (true, Unit) so a misused for-loop exits immediately rather than spinning.

Full trait-based iterators (Iter[T], combinators, user-defined iterables) are deferred to v0.6 with the stdlib expansion. The wire protocol is the explicit hand-off so the lowering doesn't have to change again.

Documentation: docs/internals/iterators.md. Tests: crates/mty-sir/tests/for_range.rs, crates/mty-hir/tests/lower_for_range.rs.

A82 — Loop back-edge fixed-point in the borrow checker (v0.5)

Status: FROZEN - Loop back-edge fixed-point shipped v0.5; stable.

Slice 4's walk_block ran each loop body once, leaving the borrow ledger state at the bottom of the body — wrong as soon as the body takes a borrow whose state has to merge with the back-edge on the next iteration. Slice 5 adds BorrowCx::loop_fixed_point, called by Loop/While/For walkers:

  1. Snapshot pre-body locals + BorrowLedger.
  2. Up to 16 iterations: walk body; join post-body state into the pre-body baseline via the existing join_states + join_ledgers functions (the same conservative joins used at if/match).
  3. Convergence test: ledger record count stable across two passes. Because join_ledgers is monotonic in the records, this is a sound convergence condition.
  4. After the cap, run one final walk + join and exit. The cap exists so a divergent body (which is itself a checker bug) still terminates analysis.

Documentation: docs/internals/borrowck.md (extended with §"Loop back-edges"). Tests: crates/mty-borrow/tests/loop_back_edge.rs.

A90 — name!(args) macro invocation marker (v0.5)

Status: FROZEN - name!(args) marker shipped v0.5; v0.4 plain-call form retained for back-compat (v1.1+ may deprecate).

v0.4 had no syntactic distinction between a function call and a macro call: an unresolved foo(...) could be a typo'd function name OR an undeclared macro, and the compiler couldn't tell which. v0.5 adds a Rust-style trailing ! marker:

MACRO_CALL = PATH "!" TOKEN_TREE
TOKEN_TREE = "(" ...paren-balanced opaque tokens... ")"

The parser recognizes IDENT BANG L_PAREN as a MACRO_CALL whose arguments are a single opaque TOKEN_TREE. The macro expander splits the tree on commas at depth 0 to recover individual argument source slices, preserving v0.4's substitution semantics.

The v0.4 plain-call form (foo(args) for a registered macro foo) is kept for backwards-compat; v0.6 may deprecate it.

Documentation: docs/spec/macros-v0.5.md, docs/internals/macros.md. Tests: crates/mty-macros/tests/mac_marker.rs.

A91 — MT6001 unknown_macro activated (v0.5)

Status: FROZEN - MT6001 unknown_macro activated v0.5; stable.

A consequence of A90: a name!(args) call site whose name has no matching declarative or procedural macro decl now triggers MT6001 unknown_macro at the HIR-lowering layer. The plain-call form (without !) intentionally does NOT trigger MT6001 — the lowering layer can't distinguish a typo'd foo() from a regular function call there. MT6001 fires only for the explicit name!(...) shape.

Documentation: docs/spec/macros-v0.5.md. Tests: crates/mty-macros/tests/unknown_macro_sd6001.rs, crates/mty-hir/src/lower/macros.rs::tests::unknown_bang_macro_emits_sd6001.

A92 — Extended hygiene mangling (v0.5)

Status: FROZEN - Extended hygiene mangling shipped v0.5; set-of-scopes hygiene deferred to v1.1+.

v0.4's mangler only renamed let IDENT = … bindings. v0.5 extends coverage to tuple, struct (shorthand + renamed), ref/ref-mut/ref-kw, and mut-kw patterns. The macro body's let statements get parsed lexically (no proper AST for the body); after let the walker scans forward to the first = at depth 0, treating the prefix as the pattern extent.

Three rules avoid false positives in the lexical walker:

  1. IDENT followed by :: or . is a path segment, not a binding.
  2. IDENT followed by { is a struct-pattern type name, not a binding (the bindings are inside the braces).
  3. IDENT followed by ( is an enum-pattern constructor, not a binding (the bindings are inside the parens).

Set-of-scopes hygiene (Racket-style) is still deferred — extended mangling covers ~95% of real cases.

Documentation: docs/spec/macros-v0.5.md, docs/internals/macros.md. Tests: crates/mty-macros/tests/tuple_pattern_hygiene.rs.

A93 — Cross-file pub macro (v0.5)

Status: FROZEN - Cross-file pub macro surface shipped v0.5; end-to-end use wiring through mty-pkg deferred to v1.1+.

MacroDef gains is_pub: bool. A new PackageMacros type splits a file's macros into local (every decl) and exported (the public ones only). When the importer's use otherpkg.foo resolves, the HIR lowering layer calls PackageMacros::register_use(other, alias_map) to copy every exported macro into the importer's local set.

The end-to-end pkg → HIR import wiring lights up once mty-pkg pipes its symbol table into HIR lowering. v0.5 ships the PackageMacros surface and an in-memory two-file fixture test; the connector slice is strictly additive.

Documentation: docs/spec/macros-v0.5.md, docs/internals/macros.md. Tests: crates/mty-macros/tests/cross_file_macro.rs.

A94 — Procedural macros (parse-and-store) + MT6005/MT6006 (v0.5)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Parse + store + purity check + MT6006 call-site gating is the v1.0 normative contract (preserves source survival). Sandboxed execution surface + TokenStream marshalling protocol tracked in RFC-003. See SPEC_FREEZE_V0_9_NOTES.md.

v0.5 adds a proc macro Name(input: TokenStream) -> TokenStream { body } declaration form. The parser recognizes the two-token proc macro prefix (proc is an IDENT — the keyword set is frozen) and stores the body as opaque brace-balanced tokens.

Execution is gated. v0.5 ships parsing + storage + a static purity check; the sandboxed sub-interpreter that will run procedural macros is a v0.6 deliverable. Two diagnostics enforce the v0.5 contract:

  • MT6005 proc_macro_impure fires at decl time if the body references effect.…(…) or a bare call to the well-known impure surface (time, env, io, model, rand).
  • MT6006 proc_macro_unsupported_v0_5 fires at every call site to a procedural macro and replaces the call with the sentinel literal 0. The macro declaration is preserved so the call-site source survives untouched into v0.6.

The v0.6 sandbox limits are exposed today as constants in sdust_macros::proc::PROC_MACRO_{WALL_MS,MEM_BYTES,STEPS} so spec and implementation cannot drift before v0.6 ships.

Documentation: docs/spec/macros-v0.5.md, docs/internals/macros.md. Tests: crates/mty-macros/tests/proc_macro_parses.rs.

A95 — Standard macro library shipped with mty-macros (v0.5)

Status: FROZEN - Standard macro library shipped v0.5; auto-import wiring through mty-pkg deferred to v1.1+.

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)

The sources are include_str!d into the sdust_macros::stdlib module so projects can load them into their PackageMacros via sdust_macros::stdlib::load_into(&mut pm). Auto-import via use sdust_macros.assert lights up once mty-pkg pipes its package symbol table into HIR lowering.

Documentation: docs/spec/macros-v0.5.md, docs/internals/macros.md. Tests: crates/mty-macros/tests/stdlib_macros.rs.

A96 — std.http.serve binds a real socket (v0.5 dogfood)

Status: FROZEN - std.http.serve real socket bind shipped v0.5; per-agent dispatch wiring still default echo (v1.1+ closes).

The dispatcher sdust_stdlib::host::dispatch now routes std.http.serve(addr) to sdust_stdlib::http_server::start_blocking, which binds a 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. The default closure is a deterministic 200 OK echo so the bound-socket smoke test in crates/mty-stdlib/tests/http_serve_real.rs roundtrips without a runtime-side agent binding.

Closes Gap 1 in DEMOS_V0_4_NOTES.md.

A97 — mighty:web/dom interface added to the wasm32-web world (v0.5 dogfood)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Four-method DOM surface declared; set-text / on-click fully canonical; get-text / query return u32 handles in v1.0 with a read-string-handle shim. Real option<string> returns + canonical-ABI return-area bridge tracked in RFC-002. See SPEC_FREEZE_V0_9_NOTES.md.

The Wasm Component generated for the web target now declares an import on mighty:web/dom with the four-method surface:

interface dom {
  set-text: func(id: string, text: string);
  get-text: func(id: string) -> string;
  on-click: func(id: string, callback-tag: string);
  query: func(selector: string) -> option<string>;
  // v0.4 back-compat:
  get-element-by-id: func(id: string) -> option<u32>;
  set-text-handle: func(handle: u32, text: string);
}

The core module declares four matching (ptr, len)-shaped imports under mighty:web/dom. MtyIR-side lowering of dom.<op>(...) method calls is reserved (emit_dom_call is wired with #[allow(dead_code)]) until the MtyIR adds a BuiltinId::Dom(...) variant in v0.6.

Closes Gap 2 in DEMOS_V0_4_NOTES.md.

A98 — Str method table real impls (v0.5 dogfood)

Status: FROZEN - Str method table real impls shipped v0.5; stable.

sdust_sir::interp::run::eval_method now binds real implementations for the v0.5 Str method surface:

  • 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

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

Closes Gap 3 in DEMOS_V0_4_NOTES.md.

A99 — RunResult::MemBudgetExceeded + Memory auto-charging (v0.5 dogfood)

Status: FROZEN - MemBudgetExceeded + auto-charging shipped v0.5; supersedes A37.

The MtyIR interpreter gains a paired memory budget:

  • RunResult::MemBudgetExceeded { used: u64, limit: u64 } — new outcome variant, exit code 4, MT5009 trap code.
  • Interp.mem_used / Interp.mem_budget — mem_budget == 0 is the legacy "no cap" sentinel.
  • AdtInit, TupleInit, ArrayInit rvalue eval charges bytes via estimate_value_bytes (24 B header + recursive payload estimate); charging beyond mem_budget returns EvalOutcome::Trap("MT5009", _) which the interpreter promotes to RunResult::MemBudgetExceeded.
  • New entry point run_fn_with_resource_budget(prog, name, args, host, steps, mem) exposes the cap; existing run_fn_with_budget is unchanged.

Closes Gap 4 in DEMOS_V0_4_NOTES.md.

A100 — FsCap allowlist enforcement via process-wide default cap (v0.5 dogfood)

Status: FROZEN (v1.0 contract: process-wide-default cap enforcement) - The v0.5 FROZEN classification is retained: process-wide-default cap enforcement is the v1.0 normative contract. The v1.0-RC residual "per-call materialisation from manifest still v1.1+" is tracked at RFC-004. A109 already pinned the per-call isolation invariant (FROZEN); RFC-004 lifts the MtyIR-lower threading without disturbing the A100 contract. See SPEC_FREEZE_V0_9_NOTES.md.

sdust_stdlib::fs adds:

  • IoErr::Forbidden(path) variant complementing Denied(path).
  • FsCap::allows(&Path) -> bool public allowlist query.
  • Process-wide DEFAULT_READ_CAP / DEFAULT_WRITE_CAP slots with install_default_read_cap(cap) -> previous_cap / install_default_write_cap setters and current_default_read_cap() / current_default_write_cap() snapshot helpers.

host::dispatch consults the current default cap on every std.fs.read / write / exists / list_dir call. A Forbidden path now returns Result::Err(forbidden:<path>) (variant 1 of the synthetic Result ADT) instead of silently succeeding.

This is the v0.5 stopgap until the MtyIR lowerer materialises per-call caps from the sandbox manifest into the call shape (post-v0.5 task).

Closes Gap 5 in DEMOS_V0_4_NOTES.md.

A101 — v0.6 multi-worker scheduler (v0.6)

Status: FROZEN - v0.6 multi-worker scheduler shipped; stable.

Slice 7 (A39) shipped a tokio multi-thread runtime as the scheduler with worker_threads configurable via STARDUST_RUNTIME_THREADS. The spec §25.4 contract is "work-stealing per core", which tokio's internal scheduler provides — but the runtime exposed no per-core telemetry, no affinity, and no programmatic load balancing.

v0.6 replaces the single-runtime model with N worker threads + 1 driver runtime:

  • Each worker thread hosts its own tokio current_thread runtime plus a crossbeam_deque::Worker<SpawnTask> (LIFO local) + 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 is exposed as Scheduler::rt so slice-7 callers can keep using runtime.scheduler.rt.block_on(...) unchanged.

STARDUST_RUNTIME_THREADS semantics preserved; default is now std::thread::available_parallelism() (was 1).

A102 — Agent affinity hints (v0.6)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Runtime API (Affinity::Sticky / Elastic, spawn_agent_with_affinity) is the v1.0 normative contract; front-end syntax agent X(...): Y with affinity = sticky tracked in RFC-005. See SPEC_FREEZE_V0_9_NOTES.md.

Two coarse affinity modes added:

  • Affinity::Sticky — pinned to worker 0 at spawn, never selected by the load monitor for migration.
  • Affinity::Elastic — default; round-robin assignment at spawn, may be retargeted by the monitor.

Front-end syntax (agent X(...): Y with affinity = sticky) is reserved but not parsed in v0.6. Only the RuntimeBuilder::spawn_agent_with_affinity runtime API is exposed.

A103 — Lightweight migration (v0.6)

Status: DEFER-V1.1 (was OPEN at v1.0-RC) - Lightweight migration (routing-table-only) is the v1.0 normative contract; lossless live migration with snapshot/restore + proxy-sender protocol tracked in RFC-006. RFC-006 may slip to v1.2 if the tokio runtime primitives prove harder than the v1.1-alpha cycle can absorb. See SPEC_FREEZE_V0_9_NOTES.md.

Live lossless migration of an in-flight tokio task between runtimes is non-trivial (tokio doesn't expose per-task waker-set re-binding). v0.6 ships lightweight migration: the monitor updates the routing table so the next spawn of that agent lands on the lighter worker. Existing loops continue on their original worker.

This is enough to:

  • Distribute new agent spawns evenly across workers.
  • Re-balance after supervisor-driven restarts (the restart spawn picks up the new route).
  • Keep cross-worker mailbox semantics correct (mpsc is runtime-safe).

Lossless live migration is v0.7+ scope.

A104 — Per-worker scheduler telemetry (v0.6)

Status: FROZEN - Per-worker telemetry shipped v0.6; stable.

Each worker exposes WorkerStats { tasks_executed, tasks_stolen, parks, current_queue_depth }. Snapshot accessor: Scheduler::stats() -> Vec<(usize, WorkerStatsSnapshot)>. The OTLP exporter (slice-7 infrastructure) consumes these as gauges named mty.scheduler.worker.<id>.<metric>.

A105 — Scheduler driver runtime separation (v0.6)

Status: FROZEN - Driver runtime separation shipped v0.6; stable internal.

Slice 7's Scheduler::rt: Arc<TokioRt> was the only runtime; both the embedder's block_on and the spawned agent loops shared it. With N workers each holding their own current_thread runtime, the block_on from the embedder must not collide with a worker's own block_on(worker_loop_async). v0.6 therefore keeps Scheduler::rt as a dedicated standalone runtime — separate from any worker — which the driver uses for runtime.scheduler.rt.block_on(user_main).

This preserves the slice-7 API surface byte-identically while unlocking the multi-worker architecture.

A106 — Default worker count = available_parallelism (v0.6)

Status: FROZEN - Default worker count = available_parallelism shipped v0.6; supersedes A39 default but preserves deterministic(seed) override.

RuntimeBuilder default switches from threads = 1 (A39) to workers = std::thread::available_parallelism().unwrap_or(1). Deterministic mode (.deterministic(seed)) still forces a single worker for reproducibility.

STARDUST_RUNTIME_THREADS=N continues to override.

.threads(n) retained as a slice-7 alias of .workers(n).

A107 — Central diagnostic catalog for MT6001-MT6006 (v0.6)

Status: FROZEN - Central diag catalog for MT6001-MT6006 shipped v0.6; stable.

The macro-band diagnostic codes (MT6001 unknown_macro through MT6006 proc_macro_unsupported_v0_5) live in sdust_diagnostics::codes as DiagCode constants alongside every other Mighty diagnostic. sdust_macros::diag keeps the historical bare-u16 constants but re-exports their values from the catalog; adding a new SD6xxx now means adding it to one file (mty-diagnostics/src/codes.rs) and re-exporting the u16 from mty-macros/src/diag.rs. mty explain SDxxxx is single-sourced on the catalog and now resolves MT6001-MT6006 the same way it resolves every other code.

A108 — BuiltinId::DomOp(name) MtyIR variant (v0.6)

Status: FROZEN - BuiltinId::DomOp shipped v0.6; closes v0.5 deferral #6.

sdust_sir::sir::BuiltinId gains a DomOp(String) variant carrying the bare MtyIR method name (set_text, get_text, on_click, query, …). The lowerer emits Call { func: BuiltinId::DomOp(m) } whenever a method-call receiver resolves to TyData::Cap { family: CapFamily::Dom, .. } — both the HirExpr::MethodCall chained-receiver path and the local.method(args) Call-as-Path shortcut. The wasm32-web backend routes DomOp through emit_dom_call to the four mighty:web/dom imports; the MtyIR interpreter routes it through host.extern_call("dom.<name>", args) for headless test runs; the cranelift native backend stubs it to a zero placeholder (DOM cap has no native target). Closes v0.5 deferral #6.

A109 — Per-call FsCap isolation contract (v0.6)

Status: FROZEN - Per-call FsCap isolation contract pinned v0.6; manifest-driven materialisation still v1.1+.

sdust_stdlib::fs::{read, write, exists, list_dir} already accept cap: &FsCap per call — v0.6 pins the isolation contract with a test proving that two FsCap values with disjoint allowlists, exercised in the same process, never leak across the divide (read/write/exists/ list_dir each verified to deny the cross-cap path, with the denied write verified to not touch disk). Per-call cap materialisation from the sandbox manifest at the MtyIR lower remains v0.7 work; the process-wide default cap (A100) continues to bridge that gap.