Change log 1 — effects, the loop, targets · rendered from docs/CHANGE-LOG.md

CHANGES.md — Onus specification changes

Changes to onus-spec-v0.md and onus-impl-spec-v0.md made since the implementation started. Apply in order. Each entry states what changed, why, and what to do in the codebase. Entries marked (applied to docs) are already in the spec files; entries marked (to apply) need the spec text added as well as the code.

2026-09-03 — Effect marker ! replaced by may (applied to docs)

Change. The effect list after a return type is introduced by the keyword may instead of !. may is a reserved word.

fn main(args: List[Text], files: io.Files) -> Result[Unit, io.Error] may io.file, alloc
fn map[T, U, e](xs: List[T], f: fn(T) -> U may e) -> List[U] may e, alloc

Grammar (§2.3): every [ "!" effects ] is now [ "may" effects ] — in fn_decl, type (function types), iface_item, and the closure form of primary. Stream[T] may e likewise.

Why. ! reads as “not” in every language a model knows; may reads correctly for every effect (may allocate, may panic, may write) and states the declaration as the claim it is.

Codebase. Lexer: add may to keywords; ! is no longer a token outside !=. Parser: four productions. Printer: emit may. All fixtures and the three examples updated. No semantic change.

2026-09-03 — Regeneration loop specified as a separate document (applied to docs)

Change. docs/onus-loop-v0.md added. It is a candidate spec for the component that drives the model against the compiler. It does not change the language.

Codebase. Nothing now. It depends on the compiler’s JSON outputs (§9.1, §11.1, §13) being stable and on onus next (M9), which are already in the plan. Do not start on it until M10 is done.

2026-09-03 — Targets: dual backends as a design goal (applied; M11 and M12 done 2026-09-05, docs/CHANGES.md items 93–104)

Change. Onus programs compile to JavaScript and to native code from the same source, and later to WebAssembly. This is a stated goal, not an accident of architecture, and it adds a section to the language spec and two milestones to the implementation spec.

Language spec: new §19 “Targets” (insert after §18 Worked examples)

19. Targets

An Onus program compiles unchanged to every supported target. Observable behaviour is defined by this specification, never by the host. Where this specification is silent on something a program can observe, that is a defect in the specification.

19.1 Runtime primitive surface

Each target provides a runtime implementing exactly the following primitives. Everything else in std.* is written in Onus and compiled by the same backend as user code.

• Memory: allocate, free-at-scope-exit (native) or no-op (collected hosts).
• Int: 64-bit signed arithmetic with overflow detection; see 19.3.
• Float: IEEE 754 binary64 arithmetic; classify; formatting to text per the algorithm in std.float (shortest round-trip representation).
• Text: UTF-8 storage; grapheme-cluster segmentation per Unicode 16.0 (pinned; the runtime carries the tables); byte and grapheme views; equality by code point sequence.
• Bytes: contiguous byte sequence with bounds-checked access.
• Panic: raise with an obligation id and optional model; recover boundary.
• Capabilities: opaque handles for io.Files, io.Env, io.Net, io.Clock, io.Rand, sql.Db, plus the __fake constructor available only to test modules.
• io.* and sql.* raw calls, each mapped one-to-one from an assume leaf in std.io / std.sql.

The primitive surface is versioned with the specification. A backend that lacks a primitive reports E0800 primitive unavailable on target at build time for any program reaching it.

19.2 Host claims

Code that can only run on one host declares it with a claim: host.js, host.native, host.wasm. These are asserted claims (§7.1) introduced only at assume leaves that call host-specific facilities, and they propagate like any claim. A path may forbid { host.js, host.native, host.wasm } to require portability, and the compiler then rejects anything reachable that depends on a host.

19.3 Integer representation

Int is 64-bit signed on every target. On targets without native 64-bit integers (JavaScript), the backend chooses a representation per value: a double-precision number where the verifier has proved |x| <= 2^53 - 1 for every value the binding can hold, and an arbitrary-precision integer otherwise. The choice appears in the ledger as an obligation of kind representation, so a reviewer can see which values are running on the slow path and tighten refinements to move them.

19.4 Fully specified behaviour

The following are specified so that all targets agree: Map iteration is in key order under Ord[K]; integer division truncates toward zero and % takes the sign of the dividend; Float to Text is the shortest round-trip form; example blocks run in source order; Stream elements are produced on demand and never buffered beyond one element by the runtime.

19.5 Differential testing

Every example and property runs on every built target. Any disagreement between targets on a program the compiler accepted is a backend defect, reported as E0801 target disagreement with the example, the two results and the targets.

Language spec: §17 Open questions

Add: Concurrency, when designed, must fit both a single-threaded event-loop host and a native multi-threaded one; structured concurrency over immutable inputs with channels by value is the working assumption.

Implementation spec: decisions table

Add a row:

| Native target | LLVM IR text emitted by the compiler; clang assembles and links against a small C runtime | Own lowering (semantics stay ours), borrowed instruction selection and optimisation; nothing to install beyond Xcode CLT / clang on Linux |

Add to §6 Codegen: the codegen pass has two emitters behind one interface, emit(ctx, target). The lowering from checked AST plus obligation statuses to a target-neutral form is shared; only the final emission differs. Do not duplicate lowering logic per target.

Implementation spec: milestones

M11 — Native backend. LLVM IR emitter; C runtime for the 19.1 primitive surface (no sql yet); onus build --target native produces an executable via clang. proved obligations emit no code; checked obligations emit compare-and-branch to onus_panic with the obligation id; recover via setjmp/longjmp. Int is i64 with llvm.*.with.overflow intrinsics. Accept: Mandelbrot builds natively and writes an identical PGM to the JS build; every example passes on both targets; E0801 fires on a deliberately broken runtime primitive.

M12 — Targets complete. sql primitives in the C runtime over libpq; host claims; Int representation obligations in the JS backend; differential test harness running all fixtures on both targets; WebAssembly emission via the same LLVM path (--target wasm), with io.* mapped to WASI. Accept: all three examples build and agree on both native and JS; the reporting example runs natively against Postgres; a path with forbid { host.js } rejects a JS-only assume leaf.

Codebase now. Nothing changes before M10. When starting M11: the shared lowering in codegen/ is the design constraint — if the JS emitter has lowering logic tangled into emission, separate it first, and add a fixture set for the target-neutral form.

2026-09-03 — Documents added, no spec impact

• docs/onus-pitch.md — a short pitch. Its example uses E0201 on a may sql.read, alloc signature; if the compiler’s E0201 text ends up different from the illustrative one, the pitch follows the compiler, not the reverse.

Not changed, but decided

• The syntax borrows F#’s data model only (unions with of, match ... with, when, { x with ... }) and is deliberately not F# elsewhere. Already in §2 “Borrowing policy”. Do not import F# conventions the spec does not name.
• Product output is JavaScript in one step; --emit ts is a fixture-suite oracle only. Already in the implementation spec and CLAUDE.md.
• The compiler is the only checker. No warnings, no lint, ever.

Change log 2 — testing · rendered from docs/CHANGE-LOG-02.md

CHANGE-LOG-02.md — Onus specification changes: testing

Follows CHANGES.md. Apply after it. Adds the testing model to onus-spec-v0.md and onus-impl-spec-v0.md. Nothing here changes the type system or the verifier; it adds two syntax forms, two ledger fields, two onus test modes, and one reported metric.

2026-09-03 — Testing model (applied; M13 done 2026-09-05, docs/CHANGES.md items 105–109)

Principle. Behaviour is established by contracts (proved) or by examples and properties (checked); dependencies are supplied as capabilities and faked in test modules; only assume leaves need testing against reality. There is no assertion library, no mocking library, and no separate test runner: the assertion language is the contract language, the mock mechanism is fake, and the runner is the compiler.

Language spec: new §20 “Testing” (insert after §19 Targets)

20. Testing

20.1 What is tested and where

Concern	Mechanism	Lives in
Behaviour, all inputs	requires / ensures / invariant, proved	the function’s interface
Behaviour, specific inputs	example (§5.2)	the function’s interface
Behaviour, generated inputs	property (§5.2)	the function’s interface
Dependencies	capabilities passed as parameters; fake (§8.4)	test module
Scenarios across modules	example blocks in a test module, with fakes at the edges	test module
Contact with reality	verify blocks on assume leaves (20.2)	next to the assumption
Regressions	example blocks pinned from counterexamples (loop spec §7)	the function’s interface
Strength of the contracts	regeneration audits (loop spec §8) and contract mutation (20.4)	onus test

There is no test tree parallel to the source. An example is attached to what it exemplifies.

Functions with the nondet effect take their source of nondeterminism (io.Clock, io.Rand) as a capability, so a test supplies a fixed one. A test that could be flaky is not expressible.

20.2 Assumption verification

An assume may carry a verify block: an Onus function body that exercises the assumption against the real resource and yields Bool.

assume Idempotent "Vendor API deduplicates on req.key for 24h; see contract §4.2"
  verify(client: payments.Client) may io.net, alloc {
    let a: Receipt = try payments.charge(client: client, key: "verify-1", amount: 100) else _: false
    let b: Receipt = try payments.charge(client: client, key: "verify-1", amount: 100) else _: false
    a.id == b.id
  }

• The block’s parameters are capabilities, supplied by the environment running onus test --assumptions, never constructed by the block.
• The block declares its effects like any function and may not exceed the effects of the function containing the assume.
• verify blocks are never run by onus check; they run only under onus test --assumptions, which is expected to be pointed at a staging or test environment.
• An assume without a verify block is permitted and is reported as unverifiable in the ledger.

20.3 Ledger fields

Each assume entry in the ledger (§9.1, §11.1) gains:

• verifiable: bool — whether a verify block exists.
• last_verified: { at: timestamp, target: string, result: "passed" | "failed" } | null — recorded by onus test --assumptions, persisted in .onus/ledger/.

The review tool shows assumptions as assumed, verified against or assumed, unverified. A path may require policy verified_assumptions_only, which fails the build if any reachable assume lacks a passing verification within a repository-configured age.

20.4 Contract mutation

onus test --mutate weakens contracts one at a time and reports which weakenings no example or property detects. Mutations applied, per obligation: drop an ensures clause; replace a refinement bound with its base type; negate a guard in a property; drop a law. A mutation that survives — every example and property still passes — is reported as M0001 undetected contract weakening with the mutation and the function. It is not an error; it is the signal that the examples are not carrying the contract’s meaning.

Mutation never touches bodies. Bodies are the model’s; weakening them is what the loop already does implicitly by regenerating.

20.5 Obligation coverage

The reported test metric is obligation coverage, per module and per path:

• obligations proved;
• obligations checked, and of those, how many are exercised by at least one example or property;
• assumptions, and of those, how many are verifiable and how many have a current passing verification;
• contract mutations detected versus surviving.

Line coverage is not reported and cannot be enabled.

20.6 The runner

onus test evaluates example and property blocks (already done by onus check), runs test modules, and on multi-target builds runs everything on each target, reporting disagreement as E0801 (§19.5). onus test --assumptions runs verify blocks against supplied capabilities. onus test --mutate runs contract mutation. There is no plugin mechanism and no configuration file beyond the repository’s target and environment settings.

Grammar (§2.3)

stmt        = ...
            | "assume" TNAME STRING [ NL verify_block ]
verify_block = "verify" "(" [ params ] ")" [ "may" effects ] block ;

verify is a reserved word.

Implementation spec

§4 Passes. Pass 9 (claims) records verify blocks on assume sites; they are type- and effect-checked like functions in pass 4/6 but excluded from codegen except under --assumptions.

§5 Runtime. .onus/ledger/ gains assumptions.json, keyed by module and assume location hash, holding last_verified.

§7 Reports. interface.json and path.json gain the two ledger fields per assumption and an obligation_coverage block per module/path.

Milestones. Add to M8 (claims, capabilities, paths): verify blocks parsed, checked, and stored; onus test --assumptions runs them against capabilities constructed from a repository config; ledger fields populated; policy verified_assumptions_only. Accept: the checkout example’s Idempotent assumption has a verify block that passes against a fake payments service and the path report shows it as verified.

Add to M10 (review tool): assumption freshness shown in the path and ledger views.

Add M13 — Contract mutation and coverage. onus test --mutate with the four mutation kinds; M0001 reporting; obligation coverage in interface.json, path.json and the review tool. Accept: dropping the ensures on recent_orders is detected by its property; dropping a deliberately unexercised refinement in a fixture survives and is reported.

Codebase now

Nothing until M8. The fake mechanism and test module already planned for M8 are the foundation; verify blocks reuse the same capability-construction path.

Not changed, but decided

• There is no assertion library. Contracts are the assertion language.
• There is no mocking library. Capabilities and fake are the whole mechanism.
• There is no separate test runner or plugin system. onus test is the compiler.
• Line coverage is not a concept in Onus.

Change log 3 — trust zones · rendered from docs/CHANGE-LOG-03.md

CHANGE-LOG-03.md — Onus specification changes: trust zones

Follows CHANGE-LOG-02.md. Apply after it. Adds zones — per-module levels of strictness — to onus-spec-v0.md, onus-impl-spec-v0.md and onus-loop-v0.md. The type system and verifier are unchanged; zones add a manifest, a dependency rule, per-zone policy bundles, a promotion command, and zone-aware loop behaviour.

2026-09-05 — Trust zones (applied; 2026-09-07, docs/CHANGES.md items 201–203: the hardened modifier, then the manifest, the zones pass and the reports, then the zone commands, the promotions ledger, the loop and the review page; onus zone promote runs the audit’s static half, and its regeneration half through the loop when given a model, item 204)

Principle. Trust in Onus is per artefact: interfaces are the human’s, bodies are the model’s, and the ledger records what each obligation rests on. A project is not uniformly trusted at any moment in its life — a hardened core coexists with a subsystem being prototyped against it — so strictness is declared per module, and the only rule that matters is that nothing at a higher level of trust ever rests on a claim from a lower one.

Language spec: new §21 “Zones” (insert after §20 Testing)

21. Zones

Every module belongs to exactly one zone. A zone is a level of strictness. There are three:

Zone	Meaning
draft	Being designed. The ledger is recorded but not authoritative. Interfaces may change freely, by human or model. Bodies may be human-edited.
hardened	In service. Interfaces are the human’s, bodies are the model’s (loop spec §1). The ledger is authoritative.
critical	In service and load-bearing. hardened, plus every public entry is on a path; no unverified assumptions; no recover; no checked obligation without an exercising example or property.

Zones are declared in the project manifest (21.4), not in modules, because a zone change is a decision about the project and its diff is what a reviewer approves.

21.1 The dependency rule

A module may depend on another module’s interface only if that interface is at the same zone or higher. draft may depend on anything. hardened may depend on hardened and critical. critical may depend only on critical.

One exception makes integration possible: a draft module may mark individual public items hardened. A hardened or critical module may depend on those items — and only those — from the draft module. A hardened item in a draft module is checked to the hardened standard: its contracts may not be changed by the loop, its obligations appear in the authoritative ledger, and its assume leaves are subject to the depending zone’s policies. Its body remains draft.

-- in a draft module
pub hardened fn charge(client: Client, req: ChargeRequest) -> Result[Receipt, Error] may io.net, alloc
  ensures ...

This is the mechanism for building a new subsystem against a stable core: harden the boundary first, and the core is permitted to see only the boundary.

Violations are E0900 dependency crosses zone boundary, naming both modules, the zones, and the item.

21.2 Zone policies

Each zone applies a fixed bundle of the policies that already exist:

• draft: none. assume unrestricted; recover unrestricted; checked unrestricted.
• hardened: no_loop_authored_claims (the loop may not edit interfaces; loop spec §1 and §5); assumptions must have a justification string.
• critical: hardened plus verified_assumptions_only (§20.3), forbid { recover } on every path, checked_requires_example, and no_third_party_assumes unless individually excepted in the manifest.

A module may add policies beyond its zone’s bundle. It may not remove any.

21.3 Promotion and demotion

onus zone promote <module> <zone> runs the regeneration audit (loop spec §8) on the module at the target zone’s standard: bodies are regenerated from interfaces alone, and every finding becomes a proposal. Promotion succeeds only when the audit reports no findings and the zone’s policies pass; the manifest change is opened for review like any other change. The audit result is stored in the ledger as the promotion record.

onus zone demote <module> <zone> is always permitted and always recorded. Demoting a module that others depend on does not break the build; it marks every dependent’s guarantees that rest on the demoted module as conditional in the ledger and the path reports, until the module is promoted again.

Zones only ever change through these commands. Editing the manifest directly is E0901 manifest edited outside zone command.

21.4 Manifest

onus.toml at the repository root:

[zones]
"app.core.*"      = "critical"
"app.reporting"   = "hardened"
"app.payments.*"  = "draft"
default           = "draft"

[zones.exceptions]
"app.core.checkout" = { third_party_assumes = ["vendor.payments.charge"] }

Patterns match module names; the most specific match wins. default applies to modules not matched. A new module is draft unless the manifest says otherwise.

21.5 Reporting

The interface document, path report and ledger carry the zone of every item. A path report additionally lists the zones it crosses and every hardened-item-in-draft-module it depends on. The review tool renders zones as regions, with draft regions visibly distinct, and the promotion history of each module.

Grammar (§2.3)

visibility  = [ "pub" ] [ "hardened" ] [ "sealed" ] ;

hardened as a visibility modifier is permitted only on pub items in draft modules; elsewhere it is E0902 hardened modifier outside draft zone. hardened is a reserved word.

Implementation spec

§2 Layout. Add zones/ under compiler/src/: manifest parsing, zone resolution, dependency rule, policy bundles.

§4 Passes. Add pass 12a, after paths: zones — resolve every module’s zone from the manifest, check the dependency rule (E0900), apply zone policy bundles (feeding the same checks paths and policies already run), record zone per item for reports.

§7 Reports. interface.json items gain zone; path.json gains zones_crossed and draft_dependencies; ledger gains promotions (module, from, to, audit result, timestamp) and conditional flags on obligations resting on demoted modules.

CLI. onus zone promote, onus zone demote, onus zone show. Promote depends on the loop for the regeneration audit; before the loop exists it runs the audit’s static half only (policies) and records that the body-regeneration half was skipped.

Milestones. Add M16 — Zones (M14 is the loop and M15 the compiler in Onus in the implementation spec; edited 2026-09-07). Manifest, dependency rule, policy bundles, hardened modifier, zone fields in reports, onus zone commands (static half). Accept: the checkout example split into app.core.* critical, app.reporting hardened and a new app.payments draft module with one hardened item that app.core.checkout depends on; a dependency on a non-hardened draft item fails E0900; demoting app.reporting marks the reporting path conditional.

Add to M10 (review tool): zones as regions; promotion history.

Loop spec

§3 What the model sees. Context policy defaults by zone: draft → scope, and the model may also see the conversation history for the module (design mode); hardened → module; critical → none.

§1 and §5. The rule “the loop never edits claims” applies in hardened and critical. In draft the loop may edit interfaces directly and proposals are unnecessary; the ledger records the edits as loop-authored so the promotion audit can find them.

§4.1 Escalation. In critical, escalation goes to the frontier model on the first stall, and widen_effects proposals are never emitted — an effect widening on a critical module is a human decision from the start.

§8 Regeneration audits. The audit is the promotion mechanism; its standard is the target zone’s policy bundle.

Codebase now

The manifest format and the dependency rule can be implemented as soon as M8 is done, since they reuse policy checks. The hardened modifier is a one-token grammar change; do it with the next grammar touch rather than separately.

Not changed, but decided

• Zones are per module, declared in the manifest, changed only by command. There is no per-function zone; the hardened modifier is the sole finer grain, and it exists only to expose a boundary from a draft module.
• Nothing at a higher zone rests on a claim from a lower one. This is the invariant everything else serves.
• Promotion is earned by the regeneration audit; there is no manual override.

Change log 4 — views and the DOM · rendered from docs/CHANGE-LOG-04.md

CHANGE-LOG-04.md — Onus specification changes: views and the DOM capability

Follows CHANGE-LOG-03.md. Apply after it. Adds what the workbench needs to be written in Onus: a dom capability, a View tree type, and a diff-and-patch runtime primitive. No framework. The type system and verifier are unchanged; this is one capability, one stdlib module, one runtime primitive, and a host claim.

2026-09-05 — Views and the DOM (applied; 2026-09-08, docs/CHANGES.md items 208 (the capability, the primitive, std.view and the counter), 209 (the vocabulary for documents and std.html) and 210 (the workbench in Onus))

Principle. UI frameworks exist for human authors: syntax that reads like markup, components to reason about one piece at a time, lifecycle hooks, an ecosystem. A model needs none of that. What remains is the one non-ergonomic problem — keeping the DOM in sync with state without rebuilding it — and that is a small runtime primitive, not a dependency. A view in Onus is a pure function from state to a tree value; the tree is verifiable like any other value; only the patch step touches the DOM.

Language spec: new §22 “Views” (insert after §21 Zones)

22. Views

22.1 The dom capability

dom.Root is a capability granting access to one DOM subtree. It is constructed by the runtime for main on the js host only (host claim host.js, §19.2) and attenuated like any capability: dom.subtree(root: Root, id: Text) -> Root narrows to a child.

Effects: dom.read (query layout, focus, scroll position), dom.write (patch the tree), dom.event (receive events). All three require a dom.Root in scope.

22.2 The View type

std.view defines an immutable tree:

union View[Msg] =
  | Element of tag: Tag, attrs: List[Attr], children: List[View[Msg]], key: Option[Text]
  | Text of value: Text
  | Keyed of key: Text, child: View[Msg]

union Attr[Msg] =
  | Attribute of name: AttrName, value: Text
  | On of event: EventKind, msg: Msg
  | Property of name: PropName, value: Text

Tag, AttrName, PropName and EventKind are closed unions of the HTML vocabulary; there is no string-tagged element. A view function is any pure function returning View[Msg]. Handlers are messages, not closures: an On carries a value of the application’s Msg type, so a view cannot capture capabilities or perform effects, and the set of things a UI can do is the closed Msg union.

22.3 The program shape

pub fn view(state: State) -> View[Msg] may alloc
pub fn update(state: State, msg: Msg, api: ModelApi, clock: io.Clock) -> Result[State, AppError] may io.net, io.clock, alloc

std.view.run(root: dom.Root, init: State, view: fn(State) -> View[Msg] may alloc, update: fn(State, Msg) -> Result[State, E] may e) may dom.read, dom.write, dom.event, e, alloc, diverge drives the loop: render, diff against the previous tree, patch, wait for an event, dispatch its Msg to update, repeat. run is the only function in std.view with dom.write; a path over a workbench entry may forbid { dom.write } on everything except std.view.run via except.

Capabilities the UI needs (ModelApi, io.Net, the ledger store) are parameters of update, never of view. A view cannot reach anything; it can only describe.

22.4 Verifiable views

Because a View is a value, properties over it are ordinary contracts:

property every_button_has_handler(s: State) {
  forall v: View[Msg] in View.descendants(of: view(state: s)) where v is Element(tag: Button, ..):
    exists a: Attr[Msg] in v.attrs: a is On(event: Click, ..)
}

property labelled_inputs(s: State) {
  forall v: View[Msg] in View.descendants(of: view(state: s)) where v is Element(tag: Input, ..):
    View.has_label(tree: view(state: s), for: v)
}

std.view ships a small set of such properties (buttons have handlers, inputs have labels, images have alt text, no nested interactive elements) that an application opts into per view function with claims view.accessible. Accessibility becomes a claim, propagated and reported like any other.

22.5 Runtime primitive

One addition to the primitive surface (§19.1): dom.patch(root, previous: View, next: View) — diff two trees and apply the minimal set of DOM mutations. Keyed children reorder by key; unkeyed children reconcile positionally. Events are delivered as (EventKind, path-to-node) pairs and mapped back to Msg by the runtime from the current tree. The primitive is perhaps two hundred lines in the JS runtime; on native and WASM targets it is unavailable (E0800) unless a host provides a DOM.

22.6 What is absent

No component abstraction beyond functions; no local component state (all state is in State); no lifecycle hooks; no context or dependency injection (capabilities are parameters); no string-tagged elements; no inline styles as strings (a Style union in std.view, closed, with a Custom variant that carries host.js); no templating syntax.

Grammar (§2.3)

No change. Views are ordinary values and functions. is in the property examples is the existing pattern test on unions; if the parser does not yet support expr is pattern in expression position, add:

cmp_expr    = add_expr [ CMP_OP add_expr | "is" pattern ] ;

Implementation spec

§5 Runtime. Add dom.ts to the JS runtime: Root capability, patch, event delivery, subtree. Native and WASM runtimes return E0800 for any dom.* primitive.

Stdlib. Add std/view.onus: View, Attr, Tag, AttrName, PropName, EventKind, Style, run, descendants, has_label, and the accessibility properties. Written in Onus, verified like everything else. This is the first stdlib module written against the self-hosted compiler and should be treated as a fixture for it.

Milestones. Add M17 — Views (M15 is the compiler in Onus and M16 zones in the implementation spec; edited 2026-09-08). dom capability, dom.patch, std.view, the accessibility claim set. Accept: a counter application (state, view, update) runs in a browser from the JS target; every_button_has_handler is proved for it; forbid { dom.write } on a path rejects a direct dom.write outside std.view.run; the same source built for native fails with E0800 naming the primitive.

M10 (review tool) is redefined: the workbench’s logic — path layout, interface diff rendering, ledger queries, the task queue — is written in Onus against std.view, in a draft zone, and promoted when its audit is clean. The hand-written TypeScript shell is reduced to bootstrapping main and nothing else. Reorder: M15 before M10’s rewrite.

Loop spec

No change. The workbench’s update is where the loop’s task-creating moves live; they were already structured. Design mode (draft zone) is the state in which the workbench itself is being built.

Codebase now

Nothing until the self-hosted compiler is stable enough to compile std.view. When it is, dom.patch in the JS runtime is the only piece of TypeScript to write; everything else is Onus.

Not changed, but decided

• No UI framework, ever. std.view is a tree type and a patch primitive.
• Views are pure and handlers are messages. A view cannot perform effects or hold capabilities.
• Accessibility is a claim, not a lint. It propagates and it appears in the ledger.
• The workbench is written in Onus. The only TypeScript in it is dom.patch and the bootstrap.

Changes forced by implementation · rendered from docs/CHANGES.md

Spec changes

Changes to onus-spec-v0.md forced by implementation, by milestone. Each is marked in the spec with <!-- changed: reason --> and pinned by a fixture. Changes the spec author makes are logged in CHANGE-LOG.md and its sequels, dated, with what the codebase must do about each; this file records only what implementation forced.

M1 — front end

Grammar (§2.3)

The provisional EBNF was made LL(1) and brought into line with the spec’s own examples. The grammar as implemented is grammar-v0.md. Differences:

1. Continuation newlines. A newline is not significant before ->, else, {, claims, requires, ensures, invariant or decreases. The EBNF placed NL tokens inside fn_decl, iface_item and loop in ways that did not tokenise consistently (e.g. a signature followed by contracts needed two consecutive newlines). Fixtures: roundtrip/messy/continuations.
2. Single-line blocks. block accepts { stmt } on one line (the §18.3 example writes if ... { return Err(Empty) }); the canonical form is always multi-line. Fixture: roundtrip/messy/single_line_block.
3. inout position. param = NAME ":" ["inout"] type, matching §4.1’s grid: inout Grid[T, w, h] and the call-site form grid: inout grid, which is now also in the grammar (call_args). The EBNF had inout before the name. Fixtures: roundtrip/14_fn_signatures, roundtrip/23_expr_postfix.
4. Labelled and explicit type arguments. targ = [NAME ":"] (type | expr) for Db[ReadOnly, schema: "orders"] (§8.2), and a call may carry explicit [...] arguments for sql.select[text: "..."](...) (§18.2). Fixtures: roundtrip/23_expr_postfix, roundtrip/34_types.
5. Ranges. a ..< b is a domain form of for and of quantifier in clauses (§5.1, §5.3), not an expression. Fixtures: roundtrip/19_for, 27_quantifiers.
6. implies and is. implies is the lowest-precedence, non-associative operator (§3.6 laws); x is Pattern sits at comparison level (§3.8.1). Chaining implies is E0011. Fixtures: roundtrip/22_expr_logic, syntax/e0011.
7. Claim predicates. A derived claim’s body is the small effect-predicate language of §6.3 (effects == { ... }, effects, claims, and/or/not), not a general expression. Fixture: roundtrip/09_claims.
8. Policy scopes. outside { self, std.* } is scope = "self" | QNAME [".*"]. Fixture: roundtrip/12_policy.
9. Test modules and fake. ["test"] "module" and the fake QTNAME { ... } primary of §8.4 are in the grammar; fake outside a test module is E0012. Fixtures: roundtrip/31_test_module_fake, syntax/e0012.
10. recover as an effect name in effect sets, for forbid { recover } (§10.2). Fixture: roundtrip/11_path.
11. Effect lists inside parameter lists. fn(T) -> U ! e, xs: List[T] is ambiguous; a comma followed by NAME ":" ends the effect list, and effect names are lowercase (QNAME), never claims. Fixture: roundtrip/34_types.
12. Quantifier binder types have no where clause of their own; where after the binder belongs to the quantifier (§5.3).
13. Mixed and/or (E0007) and chained comparisons (E0006) are parse errors as §2.1 requires. Fixtures: syntax/e0006, syntax/e0007.
14. E0002 (bare expression statement is not a call) is checked by the parser; example, property and law blocks are exempt because their bare expressions are assertions (§5.2). Fixture: syntax/e0002.
15. Soft keywords. The spec’s examples use of, require and path as names (Float.of, auth.require, path: "..."). Item and clause keywords that cannot occur inside an expression are therefore reserved only where an item or clause can begin. Listed in grammar-v0.md.
16. Parentheses are not AST nodes; the printer emits the minimal set. and/or are n-ary nodes. Fixture: roundtrip/messy/parens.

Lexical (§2, §3.1)

17. Text literals are single-line. A raw newline in a text literal is E0004; use \n. The §18.2 SQL literal is rewritten on one line. This keeps one canonical spelling per string value. Fixture: syntax/e0004.
18. Comments are preserved by the canonical printer (attached to the line-level construct they precede or follow) and excluded from hashes. Fixture: roundtrip/29_comments.
19. Literal normalisation in canonical form: _ separators dropped, durations in the largest exact unit, floats in shortest form. Fixture: roundtrip/messy/literals.

Canonical form (§2.2)

20. The layout rules are stated precisely in grammar-v0.md (“Canonical form”). Notably: bracketed lists break one element per line at 100 columns, else if canonicalises to a nested block (as §2.3 already said), and blank lines inside blocks are removed.

Named arguments (§5, §10.1, §18)

21. Ok(x) / Err(e) in the prose and examples contradicted “arguments are passed by name at every call” and the call_args grammar. The examples now write Ok(value: x) and Err(error: e); Result’s fields are value and error. Fixtures: the three worked examples.

Claims are type names (§6.3, §9, §18.3)

22. §2 and the grammar make claims TNAMEs; the §6.3 examples used lowercase (pure, total). The examples now read Pure, Total, RealtimeSafe, and require { Total, Idempotent }.

Capabilities (§8)

23. capability Db[mode: DbMode] is written capability Db[const mode: DbMode] per the tparams grammar, and mode in { ReadOnly, ReadWrite } is written mode == ReadOnly or mode == ReadWrite (there is no set-membership expression in v0). Fixture: roundtrip/10_capability.

Diagnostics (§13)

24. location.def is null for a diagnostic outside any definition (e.g. a malformed module header).

M2 — resolve and types

25. Intrinsics (§3.12, new). intrinsic fn (no body) and intrinsic type declare runtime-provided primitives, legal only under module std.… (E0102 elsewhere). Their contracts and effects are assumed obligations in the ledger (§12.2 extended). Chosen over a hardcoded primitive table (contracts would live outside Onus) and over a general extern (the FFI §17 defers). Fixtures: roundtrip/35_intrinsic, syntax/e0102, syntax/e0003_intrinsic_with_body.
26. Function types carry parameter names (§3.7). fn(x: T) -> U rather than fn(T) -> U: calls are named, so a call through a function value needs labels. A closure assigned to a function type may use its own parameter names. Fixtures: roundtrip/03_type_alias, 28_closures, 34_types.

Modules and resolution (§11, §3.4, §3.6, §3.10)

27. Module files. a.b.c lives at <root>/a/b/c.onus; std.* lives under the standard library root and no other file may declare a std.* name (E0112). A file declaring a name other than its path is E0104; an import that finds no file is E0103. The root is --root or is inferred from the entry file and its module name. Fixtures: checker/e0103, e0104, e0112.
28. Prelude. Every module implicitly sees the public types and variants (not the functions) of std.results, std.option, std.list, std.grid, std.map, std.int, std.float, std.text, std.bool, std.bytes and std.duration. These implicit imports are type-only and are not edges for cycle detection. The Result module is std.results because result is a keyword.
29. Companion functions. T.f denotes function f of the module that declares T; for a primitive, that module is std.<lowercase name> (Int.to_text → std.int.to_text). Functions are never in scope unqualified across modules.
30. Variant scope. A bare variant resolves in this module’s unions, then the prelude’s, then the imports’ public unions; more than one candidate is E0108 and must be qualified with the module alias. Two unions in one module may not share a variant name (E0107), since there is no Union.Variant syntax.
31. Module aliases win in dotted names. auth.require(...) denotes the module even when a parameter auth is in scope (§18.3 relies on this); a bare auth is the parameter. Aliases live in their own namespace.
32. No shadowing. A local may not reuse the name of another local or parameter (E0113). Module-level functions and constants may be shadowed, because parameters are the labels callers read and the spec’s own API pairs select(..., statement:) with sql.statement. Fixture: checker/e0113.
33. Examples and properties share a namespace separate from functions, so example escape_count may accompany fn escape_count (§18.1); paths and policies likewise.
34. Unit is a built-in value; TypeInfo and Spec are nameable types.
35. Interface dispatch is written Ord.compare(a: x, b: y): the interface’s type parameter is instantiated from the arguments (or an explicit argument) and an impl must exist (E0333) unless the type is a parameter bounded by that interface. Inside an interface or impl its functions are in scope bare. Fixture: checker/e0333.

Typing (§3, §4, §5, §10)

36. Generic instantiation takes type arguments from an explicit [...], then from the expected type in checking position, then from the arguments; an unbound parameter is E0324. This is instantiation, not inference onto declarations. Fixture: checker/ok_types, e0324.
37. Type indices (Grid[T, width, height]) must be literals, consts or parameters; at a call whose result type uses a parameter as an index, the argument must be such an expression (E0337). Fixture: checker/e0337.
38. Capability restrictions. Labelled arguments beyond a capability’s declared parameters (schema: "orders") are restrictions; a capability with more restrictions is accepted where one with fewer is required (§8.2). This is the one subtyping rule beyond refinement subsumption in impl spec §3.3.
39. Expression statements must have type Unit (E0339): a discarded Result is never silent. example, property and law bodies are assertions and must be Bool.
40. Unreachable code is an error, not a warning: a statement after a return on every path (E0332) and a match arm no value can reach (E0327). Fixtures: checker/e0332, e0326_e0327_match.
41. recover blocks yield the value of their final expression statement and may not return; Panicked is a record in std.results.
42. Closures may not capture capabilities (E0330), in addition to vars and inout parameters (§3.7). Fixture: checker/e0330_capture_capability.

M3 — effects

43. Function-level decreases (§5.1). Recursion needs a measure but the grammar only had decreases as a loop clause; it is now also a contract clause of a function (decreases n after requires/ensures). A recursive cycle whose functions lack one and do not declare diverge is E0320. Fixtures: roundtrip/14_fn_signatures, checker/e0320.

44. Resource effects are declared by grants (§6.1, §8). sql.read is the effect read of module sql, declared by a capability in that module granting sql.read; it is spelled the same everywhere and is reachable only where that module is imported. Any other effect name is E0202. The primitive set stays closed.

45. mutate is about the caller’s own parameters (§6.1). A function needs mutate iff it assigns to or passes on one of its inout parameters; a callee’s mutate does not propagate through a local var (Mandelbrot’s render calls Grid.set with may alloc only).

46. What allocates (§6.1). List literals, ++ and closure creation are alloc; records and variants are values and are not. A loop while without decreases is diverge. recover absorbs panic.

47. Effect polymorphism (§6.2). Passing a function value to a parameter of type fn(...) -> U ! e binds e to the value’s effects beyond those the parameter lists; the call contributes the callee’s effects with e substituted. A function value may not flow into a function-typed position (binding, argument, return) declaring fewer effects (E0201). Fixtures: checker/ok_effects, e0201_fn_value_flow.

48. Purity of contracts. A const fn declares no effects; requires, ensures, decreases and where clauses may allocate and nothing else.

49. Impl effects (§3.6). An impl function declaring effects beyond the interface’s is E0334. Fixture: checker/e0334_impl_effects.

50. Examples completed (§18.2, §18.3). The reporting and checkout examples referenced modules and functions the spec did not show; app.config, app.auth, vendor.payments, Request, Order, Basket, load_basket, record_order and the no_third_party_assumes policy are now in examples/, and Receipt is payments.Receipt.

51. Contract conveniences (§3.9, §5.3). A bare variant in a pattern (result is Ok, | Ok ->) matches any payload, like Ok(..); and a quantifier whose domain has type Result[List[T], E] or Option[List[T]] ranges over the contained list and is vacuously true for Err/None. Both appear in the spec’s own examples (§3.8.1, §18.2, §18.3).

M4 — const evaluator

52. const fn may allocate (§3.8.1). The spec’s own parse_select returns an AST, which allocates; a const fn therefore declares at most alloc (M3 item 48 narrowed). Its signature in §3.8.1 gains may alloc.
53. ConstError and TypeInfo in the library (§3.8.1). ConstError is the record std.check.ConstError { offset, message } (prelude); offset indexes the graphemes of the constant text. A const fn reads a type through std.typeinfo (TypeInfo.name, TypeInfo.fields), whose intrinsics exist only at check time. Spec values wait for the verifier.
54. When check-time checks run. At a call whose arguments are all constant, the callee’s requires proved clauses are evaluated; false is E0700, located at the offending grapheme of the literal passed for the callee’s first const Text parameter when a ConstError was produced. Clauses with runtime arguments are left to the verifier. select no longer needs .ok: columns_match takes the text and the row type.
55. Check-time failures. A contract failing or an intrinsic panicking during evaluation is E0701; a const that is not evaluable is E0701; exceeding the step budget is E0501, naming the function.
56. Examples at check time (§5.2). An example whose statements are all evaluable (pure functions, constant values) runs at check time and a false assertion is E0702; one that needs the runtime is deferred to the generated tests of milestone 5.

M5 — codegen, everything checked

57. Obligations are objects (impl spec §3.5). The contracts pass creates one per site of §12.1 with status checked, except requires proved clauses the const evaluator discharged (proved). Codegen inserts a runtime check iff checked.

58. Where checks live. A callee checks its own non-pinned requires and parameter refinements on entry, on behalf of every call site; call-site refinement obligations stay in the ledger but emit no second check. ensures, the return type’s refinement, let/var/assignment flows, record and variant field refinements, loop invariants and decreases are checked at their sites. Int and Duration + - * / % go through checked runtime arithmetic (overflow).

59. inout convention (impl spec §6). A function with inout parameters returns [result, ...parameters] and the caller reassigns its variables; intrinsics follow the same convention (Grid.set). Intrinsic shims pass const type parameters first, then parameters, positionally.

60. try unwinds with an exception (EarlyReturn) caught by the enclosing function, instead of the impl spec’s if (r.tag === 'Err') return r;, so that a try nested inside a larger expression keeps evaluation order. match is a labelled block of pattern tests in arm order, which is how guards fall through.

61. Generics and interfaces. Type parameters are erased; a bounded parameter T: I becomes a hidden dictionary argument and I.f(...) dispatches through it; impl functions are emitted as I$Type$f and each impl exports its dictionary I$Type.

62. Tests and main. Every example, property and law becomes a vitest case in <module>.examples.test.js (properties and laws under fast-check generators derived from parameter types and filtered by their refinements). onus run emits a launcher that constructs the root capabilities main names (§8.3) and maps Ok/Err/Panic to exit codes 0/1/2. std.sql at runtime has no driver in v0: connect returns Err(Connection).

63. Function values are positional at runtime. A closure takes its parameters positionally, a call through a function value passes the arguments in the type’s parameter order, and a declared function used as a value is wrapped in an adapter to its named-argument form. This is what lets a closure use its own parameter names against a function type (§3.7, item 26) without a runtime mismatch; the tsc --strict oracle caught the original defect.

M6 — verification

64. Lowering (impl spec §7.1). Records and unions are not SMT datatypes: field access is an uninterpreted projection per type instantiation, a variant test compares an uninterpreted integer tag, lists have uninterpreted len/get, Text is an opaque sort whose literals are pairwise distinct, and every call is an uninterpreted function per instantiation (a fresh constant when effectful) with the callee’s ensures and return refinement asserted about the result. A value’s declared refinements are facts, recursively through record fields, union payloads and list elements. Floats are opaque values; a float operation makes only the operand it appears in unknown.

65. Path knowledge (§3.2.1). A body is walked once with fresh SMT constants per var assignment; if conditions, match arms (with the failure of earlier arms), loop conditions and invariants inside loops, their negation and the invariants after exit, for ranges and list membership, and try success are facts. Loops and branch joins forget the variables they assign. An early-returning branch leaves its negated condition in force afterwards.

66. Constant discharge. An obligation without a solver condition whose predicate and inputs are constants (the Viewport literal of §18.1) is decided by evaluation; this is how float refinements over constants are proved.

67. Statuses and codes. unsat → proved; sat → checked, or for a pinned clause failed with the model as counterexample (E0302 ensures, E0342 requires); unknown/timeout → checked for unpinned nonlinear obligations, otherwise E0501. The panic rule of §6.1 is E0343 (a checked obligation in a function without panic); a const fn with a checked obligation is E0703. Overflow obligations are exempt from both in v0: the ±2^53 range is the runtime’s assumption (impl spec §12.1) and they stay runtime checks.

68. Codegen consumes statuses. A callee’s entry check for a requires clause or a parameter refinement is omitted when every call site proved it (whole-program), so Mandelbrot’s generated code carries no checks.

69. CLI. onus check --ledger prints the obligations of the entry file with their statuses and provenance; --budget <ms> sets the per-obligation solver budget (default 500); --no-cache bypasses .onus/cache/; ONUS_DUMP_SMT=<dir> writes every problem for inspection.

70. Checkout example (§18.3). recent_orders’s ensures forall o: Order in result: o.customer == who.id needs the Spec mechanism and is commented out until it exists; its proof from the statement’s where clause is the open item of item 53.

71. Sequential solving. The impl spec (§7.2) runs obligations in parallel up to the CPU count; v0 runs one z3 -in -smt2 process at a time with spawnSync, relying on the proof cache for repeat runs. Mandelbrot, reporting and checkout verify in a few seconds each; parallelism is a performance item for later.

M7 — reports

72. Elided bodies (§2.3, §11.1). onus interface must render “canonical source syntax with bodies elided to { ... }” and the rendering must be valid Onus, so ... is a token and { ... } is a function body the parser accepts (Block.elided). Outside an interface document it is E0115 elided body outside an interface document, reported by the resolver; the checker never sees an elided body.
73. Interface document shape (§11.1). Beyond the example in the spec the document carries: every item of the module with its visibility (private items included, since the ledger and the assumptions must be complete); a module-level ledger of every obligation with status and provenance and module obligations totals, both of which the prose of §11 asks for; a failed count; on each contract pinned, sites (how many obligations the clause generated) and checked_at as a file:line:col of the first runtime check; loop invariant/decreases clauses listed as contracts of their function; examples and propertys reported under the function of the same name (§18.1) and as items of their own otherwise. hash is b3: + BLAKE3 of the module’s canonical text.
74. Diagnostics (§13). canonical_hash is filled for every diagnostic whose file has a canonical form. onus check --json prints one object per line. repairs are still only produced for E0001.
75. Schemas. JSON Schema (draft-07) for both documents lives in packages/compiler/src/report/schema/; the test suite validates every fixture’s diagnostics and the three examples’ interfaces against them.

M8 — claims, capabilities, paths

76. Claim participation (§7.1). “Participates in the relevant effect” is given a definition: a callee participates in an asserted claim when it has an observable effect — io.file, io.net or a resource effect. The quiet effects (alloc, mutate, panic, diverge, nondet, io.env, io.clock, io.rand) change nothing an observer could see twice, so a callee with only those never has to carry the claim. An assume covers the function and everything beneath it. Intrinsics carry only what they declare, like their contracts (§3.12). Codes: E0203 derived claim not satisfied, E0204 asserted claim not propagated, E0205 assume of a derived claim, E0206 assume of an undeclared claim.
77. Capability rules (§8, §8.3). A record field of capability type is E0601; a pub fn main parameter of a non-root capability type is E0602; a non-test module importing a test module is E0600. fake outside a test module was already the parser’s E0012.
78. Paths (§9). Reachability is breadth-first over calls in bodies, closures included, with interface calls resolved on concrete receivers through the impl table. Function values and dispatch on type parameters are E0410. New codes E0412–E0415 for the bound, forbid, require and policy clauses; E0411 for a bound that allows a forbidden effect. Policy scopes: self is the path’s module; std.* matches std and every module beneath it.
79. Path report (§9.1). Adds effects.forbid, obligations.failed, ok, and permitted_by ∈ { "scope", "except", null }. checked_at and constructed_at are module.fn:line:col. Capability construction sites are every reachable call returning a capability, including attenuation; their assumes are empty until the stdlib records connect-time assumptions. onus path <file> [<name>] --json.
80. Checkout example (§18.3). Under item 76, handle_checkout’s claim requires auth.require (network) and load_basket (sql.read) to carry Idempotent. Idempotent moves to a shared app.contracts module (vendor.payments already imports app.auth, so app.auth cannot import vendor.payments); auth.require claims it, justified by having no participating callees; load_basket claims it with an assume that a select reads only. The path therefore lists three assumptions — load_basket and record_order in the module’s own scope, charge permitted by except — and “exactly one assumption” (impl spec §9, M8) is read as exactly one external assumption, which is what the reviewer is trusting on another party’s word. The spec’s “1 assumed” presumed std.sql derives record_order’s idempotency from the statement (item 53), which v0 does not do.

M9 — onus next

81. Constrained decoding (§14, impl spec §8). onus next <file> --offset <n> takes a UTF-16 index (the implementation plan’s --offset, not §14’s --at file:offset) and returns tokens, expectedType and inScope. Tokens are the kinds the parser tests at the cursor after parsing the prefix; because the lexer drops a newline before a continuation token, a position after a newline reports the union of both tokenisations. Names in the vocabulary: keywords and punctuation as themselves, ident (names and soft keywords), type-ident, literal:int|float|text|duration, newline, eof. The expected type comes from a Hole expression at the cursor with every open bracket and block closed after it; it is null when the cursor is not in expression position or nothing expects a type there (a bare statement start). Refinements are spelled out in the type text and not enforced. Locals in scope are listed outermost first; module items are not. v0 keeps no resident state between calls (impl spec §12, item 5).
82. may replaces ! (§2.3, §6). Requested by the spec author (docs/CHANGE-LOG.md, 2026-09-03): ! reads as negation. may is a reserved word and ! is no longer a token (!= remains). Applied to the grammar, every example in the spec, the standard library, the examples and the fixtures.

M10 — the review tool

83. Path report additions (§9.1, §15.1). The path view must draw the reachable graph, and the tool computes nothing, so the report carries graph.nodes (qualified name, module, entry/fn/intrinsic, effects, carried claims, obligation counts, assume and recover counts) and graph.edges (caller, callee, effects at the site, location); gates (a sealed record type some reachable function returns and others demand as a parameter — the typestate of §18.3, drawn as the gate region); recovers; and ledger rows for every obligation of a reachable function.
84. Interface item locations (§11.1). Each item carries at, so the review page can show an item’s canonical source when the reviewer opens a body; the interface itself still contains no bodies.
85. Interface diff (§11.1, §15.1). onus interface <file> --diff <old.json> and onus review --against <old.json> compare two documents of one module. v0 decides compatibility textually: a requires added or an ensures removed is breaking, the reverse compatible; a widened effect set or a changed signature line is breaking; new assumptions, recover sites and obligations that left proved are listed. Implication between clauses (a weaker requires written differently) is not checked; the module is breaking when a public item is. Schema in interface-diff.schema.json.
86. The review tool (§15). packages/review is dependency-free and renders one self-contained HTML page from the reports (impl spec §12, item 4 resolved: no framework). Views: paths (graph laid out top-down from the entry, assume leaves in amber and recover sites in purple as the only colours, unresolvable calls as a break, gate regions shaded), interfaces (bodies collapsed to { ... }, opening counted per module in the page), ledger (filterable by state, with assumptions, recover sites and capability construction sites), diff, and diagnostics with the solver’s counterexample. onus review <entry> [--out <dir>] [--against <old.json>] writes index.html and review.json. Not in v0: the path condition in the counterexample view, promotion drafts, and decisions or contract edits flowing back as tasks (§15.1); an invalid program’s page shows its diagnostics only.

Testing model (docs/CHANGE-LOG-02.md, applied 2026-09-04)

87. _ in try ... else (§2.3). The verify example in §20.2 writes else _: false; the binder may now be _, which binds nothing. The printer keeps it.

88. verify blocks (§20.2). verify is a reserved word and a continuation token, so verify(...) on the line after an assume attaches to it. A block is a definition of its own (kind verify, parent the function): it sees the module and its parameters, not the function’s locals; its calls are not the function’s (no false recursion); its obligations are its own and the panic rule applies to it; it yields Bool, each bare expression being an assertion and try ... else _: v yielding v. Its declared effects must contain its body’s and may not exceed its function’s (E0207); its parameters must be capabilities (E0208).

89. The environment (§20.2, §20.6). onus test --assumptions supplies each parameter from a test module whose public zero-parameter functions return capabilities — fakes in practice — named by onus.json (test.env) or --env; io.Files, io.Env, io.Net and io.Clock come from the runtime when the environment gives none. A parameter with no source is E0603. Generated code exports each block as verify$<n> only in that mode, and a generated launcher runs them and prints the outcomes.

90. The ledger (§20.3). .onus/ledger/assumptions.json, keyed by module name and the BLAKE3 of the assumption’s canonical text; each record has at, target, result, claim, def. The interface and path reports carry verifiable and last_verified per assumption; the review page shows assumed, verified against or unverified. policy verified_assumptions_only is the compiler’s own policy name: E0416 when a reachable assumption has no passing record younger than onus.json test.max_assumption_age_days (default 7).

91. onus test (§20.6) and the checkout example. Without flags it builds and runs the generated vitest suite; --mutate waits for M13. charge’s assumption gained a verify block that calls charge twice with one key; auth.require no longer declares io.clock it never used, so the block’s effects fit charge’s; examples/checkout/test_env.onus and onus.json supply the fakes. The block passes, and the path report lists it as verified.

92. Verify blocks in the reports (§20.2). Bodies are elided from the interface, so the block a reviewer must read to judge a verification travels with the assumption: interface and path assumption entries carry verify, the block’s canonical text or null, and the review page shows it under the assumption in the path, interface and ledger views.

M11 — native backend

93. One lowering, two emitters (impl spec §6). Code generation is now lower.ts (checked AST plus obligation statuses → the target-neutral form in ir.ts) and two renderers, js.ts and native.ts. Every decision about what generated code does is made once in the lowering; the form is printed by onus build --emit ir and pinned for the fixture suite in test/codegen/lowered/. The JavaScript output is unchanged in behaviour.

94. Native representation (§19.1). Int/Duration are i64, Float is double, Bool is i1, and everything else is a pointer to an array of 64-bit slots (a variant’s tag first), so generic code and runtime primitives move slots and callers convert at the boundary. inout parameters are pointers. proved obligations emit nothing; checked ones branch to onus_panic, whose message matches the JavaScript runtime’s; Int arithmetic uses the overflow intrinsics; try is a branch that returns the error. The runtime is packages/runtime/native/ (onus.c, onus.h), compiled and linked by clang from the emitted .ll. Float to Text follows JavaScript’s shortest round-trip layout (§19.4).

95. The v0 native subset. Programs reaching closures or function values, interfaces, runtime quantifiers, recover, fake, TypeInfo, old(...) in a checked postcondition, structural equality on aggregates, Map, Bytes, sql, or Text operations needing grapheme tables are refused with E0800 primitive unavailable on target, as §19.1 allows. Allocation is never freed (free-at-scope-exit is deferred). recover via setjmp/longjmp and the Int representation obligations are M12.

96. Differential testing (§19.5). onus test --target all runs the examples on both targets and reports each disagreement as E0801; properties and laws run on JavaScript only. onus build --target native writes <out>/native/<module> and onus run --target native runs it. The C runtime’s -DONUS_BROKEN_INT_TO_TEXT exists for the acceptance test that E0801 fires on a broken primitive.

97. M12 names the JavaScript sql implementation. M12’s text listed only the C runtime’s libpq primitives, but its acceptance (all three examples agree on both targets; reporting runs against Postgres) needs sql real on the JavaScript side too, which impl spec §5 has always described over pg and which v0 shipped as a stub (item 62). The milestone now says so, and takes recover from M11.

M12 — targets complete

98. Host claims (§19.2). std.host declares the asserted claims js, native and wasm; a claim’s name may be lowercase (grammar §2.3) so they read as host.js. The JavaScript-only intrinsics (Text.len, graphemes, bytes, lower, trim, Map.*, Bytes.len, TypeInfo.*) carry claims host.js; the native emitter refuses any reached function carrying it (E0800). A forbid clause may name claims as well as effects: a reachable function carrying one is E0413. Derived-claim predicates may name a claim by a lowercase qualified name.
99. Representation obligations (§19.3). Every Int or Duration parameter and let/var gets an obligation of kind representation, proved when the binding’s declared type keeps every value within ±2^53 - 1 and otherwise checked. They are reported in the ledger and exempt from the panic rule like overflow. The slow path is not implemented: a checked binding keeps the number representation, and the existing overflow checks panic rather than switch to arbitrary precision. The ledger says which values that concerns.
100. std.sql on both targets (§8.1, §18.2; impl spec §5). JavaScript: sql.ts over pg, driven synchronously by a worker thread with Atomics.wait (Onus calls are synchronous; pg is not). Native: onus_sql.c over libpq, found through pg_config, Homebrew’s keg or ONUS_LIBPQ; without it std.sql is E0800. connect(mode: ReadOnly) sets default_transaction_read_only = on, verifies it, and refuses a superuser role, which could not be held to it; the remaining assumption is named at the construction site in the path report. restrict sets the search path, deadline the statement timeout (Err(Timeout)).
101. Row decoders (§18.2). For each sql.select whose row type is a record the compiler generates a decoder in the target-neutral form (decoder on the call, reject statements): one column per primitive field, then the record’s refinements; a failure is Err(Refinement) with the row and column, a missing or ill-typed column Err(Malformed). JavaScript passes it as $decode; natively it is a generated function the C runtime calls per row.
102. recover natively (§10.2). The body becomes a function over the enclosing locals’ addresses, run under setjmp; a panic inside longjmps back and becomes Err(Panicked { obligation, location }) with the same texts as the JavaScript runtime.
103. WebAssembly (§19). --target wasm compiles the same LLVM IR with a WASI SDK (WASI_SDK_PATH or /opt/wasi-sdk) to program.wasm and writes run_wasm.mjs for Node’s built-in WASI; std.sql is E0800 there. No SDK was available where this was written, so the path is untested end to end; onus build --target wasm reports the missing SDK.
104. Differential harness (§19.5). Every fixture and example with example blocks is built for both targets: those in the native subset must agree on every example, the rest must be refused with E0800. The SQL tests run against a Postgres at ONUS_TEST_DSN (default: the postgres:17 Docker container with password onus) and skip with a notice otherwise.

M13 — contract mutation and coverage

105. Assertion obligations (§5.2, §20.4). Every bare Bool statement of an example, property or law body is an obligation of kind assertion: proved when the contracts of what it calls entail it, and otherwise checked “run as a test”. A proved assertion is a fact for the assertions after it. Tests are not functions, so these are exempt from the panic rule. Lowering test bodies exposed a contract that calls its own function (ensures compare(a: a, b: a) == 0); the verifier now states such a contract once instead of unfolding it forever.
106. What “detected” means (§20.4). Weakening a contract never changes a body, so re-running the tests cannot notice it. A mutation of an ensures clause, a result refinement or a record field refinement is detected when an assertion the verifier proved from the contracts stops being provable without the clause: the test restates what the clause promised. Negating a property’s guards is the one dynamic mutation: the property is re-run over the complement of its domain and detects the mutation by failing. onus test --mutate prints one row per mutation, M0001 undetected contract weakening for the survivors, exits 0, and writes .onus/ledger/mutations.json, which the reports read. Static mutations need z3 and are skipped with a notice without it.
107. Two of §20.4’s mutations are not applied. Laws are not dropped: a law is itself the only test of the interface clause it states, so its absence could never be detected and every law would be reported. And parameter refinements are not widened: accepting more inputs is a stronger promise by the callee, not a weaker one, and nothing a caller’s test asserts can depend on it. Result and field refinements are widened.
108. Obligation coverage (§20.5). The runtime records a hit per check reached when ONUS_COVERAGE_DIR is set; the generated test file writes them after its tests, since test runners end their workers without running exit handlers. onus test merges the hits into .onus/ledger/coverage.json, keeping the larger count per check across runs, and prints the coverage line. interface.json, path.json and the review page carry obligation_coverage: proved; checked and how many of those a test reached; assumptions, verifiable and verified; and mutations detected and surviving. Representation obligations have no runtime check and are not counted as checks. Coverage is measured on the JavaScript target only.
109. The acceptance test is pinned on Mandelbrot. The ensures on recent_orders stays deferred (item 36), so the milestone’s acceptance is dropping ensures result <= limit on escape_count, which property escape_bounded detects, and widening the result refinement of a fixture function no test restates, which survives and is reported. The build directory for onus test is resolved to an absolute path, which vitest needs, and the mutated programs are written beside it in out-mutate so the program’s own test run does not see them.

M14 — regeneration loop

110. The loop package (loop spec §1, §10). packages/loop with onus-loop run <task.json>; onus loop run forwards to it, since the compiler cannot depend on a package that depends on the compiler. watch needs task intake and is not in v0. Model access is one interface with three implementations: scripted, for the tests; Claude Code as a subprocess (claude -p, the nested-session markers stripped from its environment); the Anthropic Messages API over fetch, which could not be exercised here for want of a key. The constrained-decoding hook of §3.7 is declared and supplied by nothing.
111. The context (§3). Assembled through the compiler library, never from an import’s source: the targets with bodies elided and the examples and properties that name them; the interfaces of every module in scope and every import; sibling bodies per the context policy; every diagnostic of the last check as §13 JSON, except E0115 on a target, which is the task itself; failing examples with their text; counterexamples from the task and from the diagnostics; the standard library interfaces the targets’ types select. The one fixed text describes the rules and Onus syntax, which is language knowledge, not a convention. Simplification: diagnostics are not narrowed to callees; everything in scope is shown.
112. Never a claim (§1, §4). Model output is parsed as Onus. A target whose signature, contracts, effects or claims differ from the baseline is refused with a note; a second refusal is out of scope, with a proposal built from the difference. An added function is refused once the same way, since helper introduction (§4.1 step 3) is off. Only bodies are spliced, under the target’s own signature, and the file is put in canonical form so E0001 never reaches the model. Mechanical repairs apply only to spans inside a target body.
113. Classification and the ladder (§4, §4.1). A stall is an outcome identical to an earlier one, or one that grew twice running. A contract conflict is a counterexample against a target’s clause with the same body proposed twice; it ends in a weaken_postcondition or add_precondition proposal carrying the counterexample. The ladder walks full history, then a wider context policy, skips steps 3 and 4 as configured off, and stops. Examples are evaluated at check time (E0702), so a wrong body usually fails there before the verifier runs; the loop treats those like any other diagnostic.
114. Changes (§6). .onus/changes/<task>/change.json: the interface diff per module in scope (empty by construction when the baseline had diagnostics, as an implement baseline always has, since only target bodies are spliced and signatures are compared textually), the ledger delta, the body diff, the trace, metrics, proposals and audit findings. A blocked report adds the cause, the last diagnostics and the best attempt, and the working tree is left as found. onus review gains a Changes view, proposals marked proposed by loop.
115. Regeneration audits (§8). Findings are obligation_regressed and example_failed, each becoming a proposal (add_example, add_claim). Bodies that differ in callees are not reported: the interface documents carry no call graph.
116. A live run. With Claude Code as the model, escape_count was regenerated from its interface alone and was green on the first iteration in 41 seconds, with the loop invariant and measure intact. The test runs only with ONUS_LOOP_LIVE=1.
117. Deferred. Production feedback (§7), onus loop watch, and the per-repository aggregates of §11; metrics are per change.
118. OpenRouter and key files. A fourth model, openrouter[:<model>], over the chat-completions protocol; the default model is OPENROUTER_MODEL or deepseek/deepseek-v4-flash, chosen on the results in item 119; moonshotai/kimi-k2.7-code is the alternative. The CLI reads .env and .env.local from the project root and the current directory, never overriding the real environment, so keys stay off the command line; both files are ignored by git. The live test takes its model from ONUS_LOOP_MODEL.
119. What running four open-weight models taught the loop. (a) A provider that never answers hangs the task; API requests now time out after three minutes and the task ends as a model error. (b) Each iteration’s prompt and answer are kept in the change’s work directory (change.json still carries only the prompt hash, §6), so a blocked task can be read. (c) A blocked report’s last_diagnostics are the last iteration’s, including syntax diagnostics of an answer that never parsed. (d) When an answer does not parse, the notes quote each offending line and the tokens the grammar admits there, from onus next’s machinery (§14): a model that does not know Onus writes while, is told “expected an expression”, and writes while again; told that a line may start with loop, it has what it needs. Results on the Mandelbrot task: DeepSeek V4 Flash and Kimi K2.7 Code green on the first iteration (5 s and 20 s), GLM 5.3 Flash green on the second (98 s), Qwen3 Coder Next blocked on the budget without a parseable answer before or after (d), and Claude Sonnet 5 through OpenRouter green on the second (15 s) after a syntax slip on the first. The OpenRouter default is DeepSeek V4 Flash on these results. The runs are logged in docs/BENCHMARK.md, and packages/loop/bench/run.mjs appends a row per model so the log can be revisited.

M15.0 — prerequisites for the compiler in Onus

120. Recursion measures are obligations (§5.1). The effects pass records every recursive cycle; the contracts pass puts a decreases obligation at every call within a cycle (the callee’s measure over the arguments strictly below the caller’s measure taken at entry) and one at entry (the measure non-negative); the verifier discharges both; a checked one becomes a runtime check on both targets, the arguments bound to temporaries so they are evaluated once. Before this, a recursive function only had to declare a measure. Fixtures: direct, mutual, structural over a list through slice’s length contract, and a measure over record fields, all proved; a measure that grows, checked and panicking on both targets.
121. A cycle shares one measure (§5.1). E0320 now also fires when the functions of a cycle declare measures that differ once parameters are numbered by position, which is the spec’s “same expression up to renaming” made mechanical.
122. The standard library grew (§16, provisional). std.text: count, code_points, of_code_points, of_code_point, slice, index_of, contains, ends_with, split, join, repeat, replace, compare, upper, positions counted in code points (len stays grapheme-based and JavaScript-only); an empty separator splits into code points and an empty from leaves replace alone, since a refinement count(t: it) > 0 on those arguments cannot be proved for a literal. std.int.parse and std.float.parse return Option. std.list: Builder[T] with builder, push, built, finish, and map, filter, fold, index_of, contains, reverse written in Onus. std.io: read, and a Console capability with print and eprint, a fifth root the runtime supplies to main. Every new function has contracts and examples; the examples run at check time, as generated tests on JavaScript, and natively through the harness. A builder is a value the runtime shares: bind it once and push through that binding (a rule the type system does not yet enforce).
123. Structural equality natively (§19.1). The native emitter generates a comparer per concrete type: primitives by value, Text by the runtime, records field by field, unions by tag then fields, lists element by element through onus_rt_list_eq with the element comparer. Equality on a value of a type parameter stays E0800, so List.index_of and List.contains are JavaScript-only, like the closure-taking combinators.
124. Two runtime fixes the library work exposed. A native file write is flushed at once, so a read after a write sees it as on JavaScript; and the JavaScript emitter gives each inout call its own temporaries, since two such calls on one variable in a block redeclared them. A program’s build no longer emits the standard library’s own test files, which the library’s examples had just introduced.
125. Deferred from M15.0. Map on the native target and the Process capability for z3, which the checker and verifier stages need, not the front end; the stack-depth story, which the parser stage will settle.

M15.1 — the front end in Onus, first part: the lexer

126. The lexer in Onus (self/). self/tokens.onus, self/lexer.onus and self/lexdump.onus: the token stream of lexer.ts reproduced, positions in code points rather than UTF-16 units, every loop and helper contracted so that the verifier proves termination and every index obligation; the file checks with no diagnostic and no may panic. The differential test runs the dump program over every .onus file in the repository and compares it with the TypeScript lexer’s stream, tokens, comments and diagnostics alike, and the same natively on Mandelbrot. One agreed-on limit: past 2^53 the JavaScript runtime’s Int cannot hold a literal exactly (item 99), so the dump compares digits as written and the value stays a known gap.
127. What writing it taught the compiler. (a) The verifier now gives the right operand of and, or and implies the left operand (or its negation) as a fact, so i < n and List.get(xs: xs, i: i) proves its index. (b) A float literal lowers to an opaque constant instead of sinking every obligation around it; an obligation the solver cannot settle is still tried by constant evaluation afterwards. (c) The native emitter labels every function’s entry block, without which a short-circuit as a function’s first statement referred to a block that did not exist; it emits aggregate and computed const items as slots filled on first use, and builds compile-time lists, records and variants. (d) Grammar facts a model would also need: constants are names, not upper-case; a multi-statement match arm needs braces; there is no conditional expression; patterns bind a variant’s field by its own name and may not rename it; a name from an imported module is always qualified by the alias.
128. Still to come in M15.1. The canonical printer in Onus, then onus fmt reimplemented and the byte-identical acceptance.

M15.1 — the front end in Onus, second part: the parser

129. The parser in Onus (self/ast.onus, self/parser.onus, self/astdump.onus). The syntax tree of ast.ts as records and recursive unions (field names that are reserved words carry a suffix or prefix: ty, where_, is_pub), and the recursive-descent parser of parser.ts reproduced: the thrown ParseError became Result and try, with recovery at statement and item boundaries; the parser state is one record passed inout, its position bound by the record’s own refinements; and every function of the recursive cycle takes a rank and shares the measure (tokens left) * 64 + rank, so a call at a lower rank, or after a token was consumed, is strictly smaller. The verifier proves the whole parser: 160 measure obligations, 287 postconditions, every index. Not carried over: the cursor and hole of onus next (§14). A dump program prints the tree one node per line, spans in code points, and the differential test compares it with the TypeScript parser’s tree on every source in the repository, syntax diagnostics included; they agree on all of them.
130. What the parser taught the compiler. (a) The verifier’s join after an if forgot everything a branch assigned; it now keeps each branch’s new facts under that branch’s condition and relates a joined variable to each branch’s value, which is what if p.pos < n { p = { p with pos: p.pos + 1 } } needs to keep p.toks known. (b) The code generator snapshotted every old(x) at entry whether or not any obligation would read it; a recursive-descent parser copying its token list on every call ran in quadratic time (76 s on the lexer’s own source, now 70 ms). Snapshots are taken only for contracts some obligation of which is checked at runtime. (c) A try that returned early from a function with inout parameters returned the bare value on JavaScript, not the value with the parameters; pinned by test/codegen/inout_try.onus. (d) More language facts a model needs: it is reserved even as a variable name; a call’s non-Unit result may not be discarded, so token-consuming helpers come in Unit flavours; old(...) is not allowed in a loop invariant, so a loop binds what it needs before it; a pattern cannot shadow an enclosing binding, so nested matches on two Options move into a helper.
131. Contract shapes that proved. advance promises a step only below the last token, since the stream’s final eof is a lexer invariant the record does not state; the helpers that consume exactly one token say result implies p.pos == old(p).pos + 1; every production that always consumes says result is Ok implies p.pos > old(p).pos, which is what the loops’ measures and the up-rank calls rest on.
132. Still to come in M15.1. The canonical printer in Onus, then onus fmt reimplemented and the byte-identical acceptance.

M15.1 — the front end in Onus, third part: structural recursion and the printer

133. Structural measures (§5.1, spec change). decreases may name a value of a record, union or list type, meaning the structural order: at each recursive call the argument must be a proper part of the measure at entry, reached by pattern matching, field access or List.get. The verifier decides this from the terms themselves (a pattern field is a projection of the scrutinee, an element read is a projection of the list) and marks the obligation proved by the structural order; otherwise it reports E0344 and never falls back to a runtime check, since no general size exists to compare. No entry obligation is generated for a structural measure. Every walk over a syntax tree in the compiler in Onus needs this; the dump program declared diverge until now.
134. The document renderer and comment attachment in Onus. self/doc.onus is doc.ts: the same Doc forms, the same fits and render, driven by a Builder used as a stack (List.at and List.pop, added to std.list for it). self/comments.onus is comments.ts: the site walk over the tree, keyed by node kind and span, the leading, trailing and dangling sets, and the same choice of owner for every comment. One known divergence: the renderer measures width in code points where the TypeScript renderer counts UTF-16 units, so a line holding a character outside the basic plane could break differently; no source in the repository has one.
135. The printer and fmt in Onus. self/printer.onus is printer.ts with one structural change: where the TypeScript printer has an operand helper, the Onus printer has wrap(d, paren) with the precedence test at each call, so that every recursive call passes a proper part of the node and decreases <node> is proved for every walk. self/fmt.onus is onus fmt --stdout: read, lex, parse, attach comments, print; syntax diagnostics go to the error stream and the exit code is nonzero. packages/compiler/test/self/printer.test.ts builds it once and runs it over every source in the repository: a source without syntax errors must print byte-for-byte as the TypeScript printer prints it, and a source with syntax errors must be refused by both. All agree, which is the M15.1 acceptance.
136. Integer literals carry their digits. tokens.IntLit and ast.IntLit in Onus have a text field beside value: the digits with underscores and leading zeros removed, which is what the canonical printer writes. value alone was not enough: Int on the JavaScript target is a double (item 99), so a literal above 2^53 such as the 9223372036854775807 in test/roundtrip/21_expr_arith.onus loses precision in the lexer’s own arithmetic and printed wrongly. The same limitation means the lexer in Onus does not hold such a literal’s value exactly; it is the representation concern of §19.3 and is left for the arbitrary-precision path.
137. What the printer taught the compiler. (a) A pattern binder shadows a top-level function of the same name, and a call to the function inside the arm is then E0323 not callable: Expr is not a function; binders cannot be renamed (item 130), so the walkers are expr_doc, block_doc, stmt_doc, params_doc, effects_doc and pattern_doc. The diagnostic is correct but does not say why the name changed meaning; a better message is deferred. (b) A closure’s parameters put the parameter walk into the expression cycle, so collect_params needs a structural measure too; the effects pass reports the cycle member without one (E0320). (c) An example that calls a generic function evaluates that function’s body at check time with its type parameter unsubstituted, so an intrinsic returning T (List.get in head[T]) handed the evaluator a value it could not convert, and the pass threw (cannot convert a T, reported as E0999). Such a call is now not a constant: the example is left to test time, as any non-constant example is. (d) ensures result is None in a function returning Option[T] for a type parameter T lowered the variant test in the wrong sort and z3 rejected the query (E0999); the test is now lowered in the context of the scrutinee’s type. Both are pinned by test/verify/ok_generic_is_in_ensures.onus, whose example reached the first and whose contracts reached the second.
138. No diverge left in self/. self/astdump.onus now gives every walk the node as its measure (item 133) and drops diverge; the parser’s differential test is unchanged.

M15.2 — the checker in Onus, first part: loading, resolution and the type layer

139. A structural measure may be passed on unchanged (§5.1, spec change). The type checker in Onus, like the one in TypeScript, routes expr(e) through helpers that take the same node and recurse on its parts, so expr calls call(e), which calls expr(a.value). The structural rule of item 133 rejected the first call: the argument is the measure itself, not a proper part. The verifier now classifies every call on a structural measure as strict (a proper part), equal (the measure itself, through aliases) or neither; strict calls are proved as before, neither is E0344 as before, and equal calls are settled once every function is lowered: they are proved when the calls passing the measure unchanged form no cycle of their own, since every cycle then takes a proper part somewhere, and are E0344 when they do. Pinned by test/verify/ok_structural_helper.onus and test/verify/e0344_equal_cycle.onus.
140. Dict in std.map. Map.put copies the whole map on every write, which a checker’s definition and scope tables cannot afford. Dict[K, V] is an in-place table with value keys for Int and Text, on the Builder model (bind once, write through that binding): dict, count, set, find, contains, remove, keys and values in insertion order. JavaScript runtime and --emit ts type; pinned by test/stdlib/map_ops.onus.
141. Nodes are keyed, not numbered. The syntax tree in Onus has no node ids. Side tables are keyed by defs.node_key(file, tag, span): the file, a syntactic class (expression, type, pattern, statement, item, signature part, other) and the span, packed into one Int (a file is limited to 2^20 code points and a compilation to 1024 files). Two nodes of one class never share a span, so the key is unique; comment attachment already keyed sites the same way. A definition carries its declaring node (defs.DeclNode) so that later passes reach the declaration without a node table.
142. Loading and resolution in Onus. self/report.onus (diagnostics and source files), self/defs.onus, self/context.onus (the compilation context, one record of tables that dicts and builders make writable through a copy), self/loader.onus (resolve/loader.ts: the module graph, the prelude, E0101, E0103, E0104, E0112, and pass 2 for every loaded file) and self/resolve.onus (resolve/resolve.ts: definition collection and every rule of §3.10 and §11). self/check.onus is onus check in Onus: it runs the passes implemented so far and prints every diagnostic as one line. packages/compiler/test/self/checker.test.ts builds it once and runs it over every source in the repository against the TypeScript pipeline up to the same pass; codes, files, spans and order must agree, and they do up to resolve.
143. What the resolver taught. (a) fn, claims and module are keywords, so they cannot be field names; the records use fn_def, claim_table and mod. (b) A Some(value) arm inside another Some(value) arm is shadowing (item 130), so nested optionals go through small total accessors (or_neg, find_or) or one match per level in a helper. (c) The measure of a mutual recursion is a parameter position (item 121), so a fuel measure must sit at the same position in every function of its cycle; the basic evaluator in Onus puts it first. (d) A dict inside a record is written through a local copy (var d = r.table; Map.set(d: inout d, …)), which the runtime shares; the verifier does not see the record change, so no contract speaks about a dict’s contents.

M15.2 — the checker in Onus, second part: types, constants and effects

144. The type checker in Onus. self/effectset.onus (effects/set.ts), self/types.onus (types/type.ts: the type representation, equality after stripping refinements, assignability, substitution, the type variable tests), self/basic.onus (consteval/basic.ts) and self/typecheck.onus (types/check.ts, with exhaustiveness from types/exhaustive.ts). The port keeps the TypeScript structure, which item 139 made possible: check_expr(e) hands e to ctor, call, binary and the rest, and each recurses on the parts. One structural change: a refinement’s predicate is not checked where the type is elaborated but from a queue once the enclosing item is done, so that elaborating a type never re-enters the expression checker and the elaboration functions form a cycle of their own with a depth measure. The diagnostics are the same, in another order, so the differential test compares them sorted.
145. The constant evaluator and pass in Onus. self/values.onus (consteval/values.ts), self/evaluator.onus (consteval/eval.ts with consteval/intrinsics.ts) and self/consteval.onus (consteval/pass.ts with consteval/offsets.ts). What TypeScript does with exceptions the evaluator does with a Result whose error is NotConstF, PanicF, BudgetF or ReturnF, propagated by try; integer overflow is caught with recover, so a constant that leaves ±2^53 is E0701 as before instead of a panic in the compiler. An intrinsic is evaluated by calling the standard library function it names, after its refinements are checked by hand so that the evaluator itself has no panic effect. Union results (Int.parse, Float.classify) are rebuilt from the union’s variants by name.
146. The effects pass in Onus. self/effects.onus (effects/check.ts): sites, containment, closures, verify blocks, the flow of function values into function-typed positions, the call graph, Tarjan’s strongly connected components with a depth measure, and the measure keys of §5.1 computed over the printed measure. printer.print_expr is the printer’s new entry point for it.
147. M15.2 acceptance. self/check.onus runs load, resolve, types, constants and effects in the order of driver.ts, stopping at the first pass that reports as the driver does. packages/compiler/test/self/checker.test.ts runs it over every source in the repository against the TypeScript pipeline up to effects; codes, files and spans agree on all of them.
148. A function named eval (codegen bug). The JavaScript emitter renamed reserved words where a local was declared and where a function was referenced, but not where a function was declared, so a module with fn eval produced a file Node refuses in strict mode. Every declaration site now goes through the same renaming. Pinned by test/codegen/reserved_names.onus, whose functions are named eval, delete and new.
149. What the checker taught. (a) A loop or a recursion whose measure is a field of an inout record cannot be proved to decrease once the body passes that record to a callee, since the callee may change the field; a local counter written back afterwards is the shape that proves. (b) A counter declared var i: Int = 0 loses i >= 0 at a loop head; declaring it var i: Int where it >= 0 = 0 keeps it. (c) The evaluator’s Ev record refines steps and budget to be non-negative for the same reason. (d) A function that takes the same node as a helper and re-matches it is the idiom that lets a large match be split, now that item 139 admits the call.

2026-09-05 — M15.3, first part: the verifier in Onus, and what porting it found

150. A callee’s ensures about an inout parameter was a contradiction (verifier soundness bug). The lowering bound both a parameter and old(param) to the argument’s term, so List.push’s ensures built(b: b) == built(b: old(b)) + 1 became built(b) == built(b) + 1; and since a definition’s callee axioms are shared by every condition of its body, every obligation in a function that pushed to a builder was proved vacuously. Found when the verification-condition builder in Onus proved fuel < fuel. Now an inout argument gets a fresh post-call term: the callee’s ensures sees it for the parameter and the passed term for old(param), and the body walker re-binds the variable to it after the expression (§3.2.1: a call through inout is an assignment). verify/lower.ts (rebound, calleeFacts with pre and post bindings), verify/vc.ts (lower), and the same in self/lower.onus and self/vc.onus. Pinned by test/verify/ok_inout_post.onus (the exit value is known through the ensures) and test/verify/e0343_inout_stale.onus (the value known before the call is stale, and nothing after the call is vacuous).
151. The match join keeps what each arm learned (verifier precision). After a match whose arms assigned a variable the walker forgot everything about it, unlike the if join; the parser’s loops over match parse_x(p: inout p) with had only ever “verified” through item 150’s contradiction. The join now mirrors if: a fresh constant per assigned variable, equal to each fall-through arm’s value under that arm’s condition (the earlier arms’ failure, its test and its guard), the arm’s facts under the same condition, and the disjunction of the fall-through conditions, which is sound because arms are exhaustive (§4.4). verify/vc.ts (match) and self/vc.onus (match_stmt). Pinned by test/verify/ok_match_join.onus.
152. What the two fixes uncovered in self/. Fifty obligations across the compiler in Onus had been proved vacuously; the match join settled fifteen, and the rest were real gaps, fixed at the source: loop invariants that lost a bound (j <= n, i < List.len(xs: parts), List.built(b: segs) >= 1, steps <= 100000000), counters declared Int where Int where it >= 0 (or it < List.len(...)) was meant, a var end: Int that lost >= 0, digits_end gaining ensures is_digit(at(src, start)) implies result > start, a slice in the constant evaluator’s grapheme_span whose lower bound could exceed the text (a bug), and in the parser: take (consume or fail at the end of input) in place of skip where the next token is known, so p.pos > old(p).pos follows; type_args and call_args promising result is Ok implies p.pos > old(p).pos; and the measure (List.len(xs: p.toks) - p.pos) * 2 + flag(b: more) for loops that end by clearing more, since a decreases clause must fall on every iteration, the last included.
153. The verifier in Onus. self/formula.onus (formulas and SMT-LIB text), self/z3.onus (finding and running z3 through io.Process, the proof cache), self/lower.onus (lowering expressions, callee contracts, type facts, structural measures), self/vc.onus (the body walker of verify/vc.ts: bindings, havoc, joins, loops, for, obligations at calls, fields and arithmetic), self/constant.onus (constant discharge), self/verifier.onus (the pass: z3 outcomes, counterexamples, the equal-measure cycle rule, the panic and const-fn rules). Obligation ids and node keys replace object identity; the contracts pass records the expression at each refinement and requires site and the constructor of each field initialiser (expr_nodes, ctor_of) for constant discharge. report.Diagnostic carries an optional ObligationInfo (kind, text, status, counterexample) as the TypeScript one does. Left out for now: the ONUS_DUMP_SMT debugging dump and contract mutation (§20.4, an option of buildVCs the Onus builder does not take).
154. Claims, capabilities and paths in Onus. self/claimcheck.onus (tiers, carried claims, assume sites keyed by module and BLAKE3 of the canonical statement, propagation, E0203–E0206; claims is a keyword, hence the module name), self/capabilities.onus (E0600–E0602), self/paths.onus (reachability, bounds, forbids, required claims, policies, gates and capability sites into PathAnalysis records for the path report; E0410–E0416). The driver in Onus reads no assumption ledger yet, so policy verified_assumptions_only reports E0416 for every assumption, as the TypeScript compiler does without a ledger. self/check.onus runs the passes in the driver’s order (contracts, claims, capabilities, verify, paths) with --z3, --budget and --cache; main takes io.Process.
155. Text.split for a prefix. A decreases text is trimmed of its at the call to … suffix by taking the first piece of Text.split, which needs no index proof; Text.index_of plus Text.slice would have required one the verifier cannot give.
156. The reports in Onus. self/json.onus (JSON values, compact and two-space-indented text as JSON.stringify writes them), self/loc.onus (line tables per file, locations as the reports print them), self/codes.onus (the code titles, generated from report/codes.ts), self/interface.onus (the §11.1 document and the elided canonical text; the coverage line, with the test coverage table and mutation records the driver in Onus does not read yet at zero), self/pathreport.onus (the §9.1 document), self/diagjson.onus (the §13 object, with the E0001 repair and the canonical hash). The printer gained print_item, print_signature, print_verify, print_type and print_module_elided; the loader keeps each file’s comment table for them; report.Diagnostic carries repairs. self/check.onus prints the documents with --interface-json, --path-json and --diag-json, and packages/compiler/test/self/reports.test.ts compares them byte for byte with onus interface --json, onus path --json and onus check --json on every source in the repository. The one known difference, not exercised by any source: positions count code points here and UTF-16 units there, so a line with a character outside the basic plane would place a later column differently.
157. What the report differential found in the checker in Onus. The earlier differentials compared codes and spans; the JSON compares everything. Brought into line with the TypeScript compiler: a parser diagnostic names the definition being parsed (tokens.Diagnostic carries it; an impl is Iface[Target] with the target’s source text rebuilt from its tokens); a file that already carries a diagnostic gets no canonical text, hence no canonical_hash; E0113 says at which line the earlier binding is; E0700 carries its obligation (requires, failed); the evaluator’s precondition messages for List.get, List.replicate, List.slice and Bytes.get are the runtime’s, word for word. The verifier’s body walker looked parameters of examples, properties and laws up under the wrong key tag, so their names were “not in the verifier’s scope” and their obligations stayed checked; the fixture suite had not caught it because every property and law fixture is exercised through the TypeScript walker.
158. A nested generic call evaluates at check time (TypeScript evaluator). first_or(xs: [3, 4], fallback: 7) calling head[T] calling List.get converted the intrinsic’s result with the type T of head, not the Int it was called at, and threw “cannot convert a T”, so the example was deferred; the evaluator in Onus, whose values need no conversion, ran it. The TypeScript evaluator now keeps the instantiation of each frame and resolves a nested call’s type arguments through it, so the two agree and the example passes at check time.
159. One differential for the verifier and the reports. packages/compiler/test/self/verifier.test.ts now compares, for every source, the §13 diagnostics, the obligation ledger and the interface and path documents from one run of self/check.onus (--diag-json --ledger --interface-json --path-json), running the compiler in Onus on several sources at a time; the earlier separate reports test is folded in. It is slow (each self/ module verifies most of the compiler again, twice) and carries a four-hour timeout; the follow-ups are a per-module verification cache, cached timeouts and a faster body walker in Onus.

2026-09-06 — the module verification cache

160. A module verified once is replayed. verify/modcache.ts and self/modcache.onus (impl spec §7.3): a module’s key is the BLAKE3 of its canonical text, its imports’ keys, the compiler (ts or self), the z3 version, the budget and a format number; the entry is the final status and provenance of each of its obligations in creation order, written only when verifying the module reported no diagnostic. On a hit the verifier assigns the stored statuses, builds no conditions for the module and discharges nothing of it; the rules run as before and report nothing, being deterministic on statuses. The two compilers keep separate entries, so the differential still verifies everything on both sides once. Pinned by test/verify/modcache.test.ts: a replay yields the same ledger and no new entry, a changed module a new entry, a module with a diagnostic no entry. The differential over every source, which took 37 minutes with only the proof cache warm, takes 9 with the module cache filling as it goes and under a minute once it is warm.

2026-09-06 — verifying the compiler’s own code generator

161. Sorts and projections are named by the qualified type. Verifying self/lowerir.onus, which imports both ast and ir, found that the lowering named the SMT sort of a type by its bare name: ast.Stmt and ir.Stmt both became Stmt, their Let.name projections collided (Ident against Text), and z3 rejected every problem that used the second as ill-sorted — 627 E0999s on one module, and a soundness hole had the sorts agreed. verify/lower.ts slug and self/lower.onus slug now use the qualified name (ast.Stmt, std.list.List_ast.Arg), for constant variant arguments too. Pinned by test/verify/ok_same_name_sorts.onus with lib/stmt_a.onus and lib/stmt_b.onus. The module cache format is 2.
162. Type facts are asserted only where a refinement is reachable. Verifying self/jsemit.onus exhausted a 4 GB heap before the first z3 call: typeFacts walked every variant and field of the recursive ir and ast types to depth four for each bound name, declaring millions of projections whose only fact was a list length bound. The bound is now an axiom of the list sort, stated once when the sort’s functions are declared (forall xs. len(xs) >= 0, printed with the declarations), and typeFacts/type_facts first ask hasFacts/has_facts — memoised by type and remaining depth — whether a refinement is reachable through fields and elements within the depth left, and skip the walk otherwise. The conditions built are identical (the emitter module: 345 conditions, the same 5,218 formula nodes) in 72 ms and 92 MB instead of 217 s and 1.6 GB retained; the fixture suite’s ledgers are unchanged.

2026-09-06 — M15.4: the JavaScript emitter in Onus and the fixed point

163. Codegen in Onus. self/ir.onus is the target-neutral form of codegen/ir.ts, self/irtext.onus its text (onus build --emit ir), self/lowerir.onus the lowering of codegen/lower.ts (obligation statuses to runtime checks, entry checks, dictionary passing, inout results, match compilation, measures, old snapshots, early returns, generators for properties, verify blocks), self/jsemit.onus the JavaScript emitter of codegen/js.ts, and self/build.onus the emitAll of codegen/build.ts (package.json, the vitest config, every module, every .examples.test.js, the launcher of main). self/check.onus gained --ir (print the form of every non-library module) and --emit <dir> --runtime <specifier>. Every function of the port is verified: decreases fuel at each call of a recursive cycle, with a zero-fuel guard returning the empty form, and the measures the first verification found not strictly falling (68 sites passed fuel on unchanged) now fall.

164. The codegen differential. test/self/codegen.test.ts runs both compilers to paths on every source in the repository that checks clean, with the same budget and proof cache, and requires the printed form of every non-library module and every file onus build writes to agree byte for byte, name for name. It does, on every source.

165. The fixed point. scripts/bootstrap.sh builds self/ with stage0 (the TypeScript compiler until bootstrap/ exists) into stage1, with stage1 into stage2, with stage2 into stage3, and requires stage2 and stage3 to be identical file for file; it is, and stage1 — the compiler as the TypeScript compiler emits it — is identical to stage2 as well: the Onus compiler compiled by itself is byte-identical to itself compiled by the TypeScript compiler (M15.4’s acceptance, for the JavaScript target). The chain runs in about seven minutes with the module cache warm. The native emitter and the remaining CLI commands are not yet in Onus.

166. No integer above ±2^53 in the compiler’s own source. The one disagreement the codegen differential found was the Onus lexer’s duration overflow check, value > 9223372036854775: the TypeScript compiler prints the literal’s digits, the compiler in Onus prints the JavaScript number it holds (…776). This is the Int representation gap of item 99, not a codegen bug, and the compiler’s own source now avoids it: push_duration compares the literal’s digits against the limit as text and reads the nanoseconds with the unit’s zeros appended, so the check is exact on every target and needs no multiplication. Pinned by the lexer differential and the codegen differential on self/.

167. The native emitter in Onus. self/native.onus is codegen/native.ts: the LLVM IR text for clang, reachability from main and the non-library examples, lazily filled aggregate constants, row decoders, recover bodies as functions over the captured locals, structural comparers per type, and E0800 for what the native subset does not compile (the same words, from unsupported_detail). Two things the port could not copy: a double literal’s IEEE bits are found with exact operations (scaling by powers of two, halving, and thirteen nibbles extracted by doubling), since the runtime has no bit cast and an Int on the JavaScript target cannot hold them; and a text’s UTF-8 bytes are computed from its code points, since Text.bytes claims host.js. self/check.onus gained --native <dir> (writes <dir>/native/program.ll and reports E0800) and --no-libpq. The codegen differential (test/self/codegen.test.ts) now also requires the native program and the E0800 diagnostics to agree byte for byte with emitNative, and they do on every source. Running clang and comparing the targets (§19.5) stay with the CLI, which is the next port.

168. A recursive union’s comparer no longer unfolds the type. The codegen differential over every source made the TypeScript native emitter overflow its stack: eqSlots compared a record’s or variant’s fields inline, so a union with a field of its own type recursed without end — the memoised per-type comparer existed but was used only at the top and for list elements. Both emitters now compare a nested record, union or list field through the type’s comparer (eqField, eq_field), which refers to itself for a recursive type; primitives stay inline. Pinned natively by test/native/eq_recursive.onus, whose examples compare recursive trees on both targets.

169. The command line in Onus. self/cli.onus is onus check, fmt, build, run, interface and path (cli/main.ts), with the pieces those commands needed and the reports in Onus lacked: diagtext.onus (the text rendering of a diagnostic), a JSON reader and accessors in json.onus, idiff.onus (the §15.1 interface diff over two documents as JSON values, so a document read from a file and one just produced compare alike), pathtext.onus (the path report’s text, read from its own JSON), and nativebuild.onus (clang, libpq and the WASI SDK found by running them, the same flags as native-build.ts, E0800 and E0999 as there). test, review, loop and next stay with the TypeScript onus until M15.5. Two things wait on language changes and are written into the module’s header: the runtime turns a returned Err into exit status 1, so usage and I/O failures cannot be 2 as the TypeScript command line reports them, and run relays a program’s output after it finishes because io.run captures it — a main that chooses its exit status, and a primitive that inherits the standard streams, are the first candidates for the language-change process. The standard library is --stdlib or ONUS_STDLIB, the runtime for build and run is --runtime or ONUS_RUNTIME. test/self/cli.test.ts runs both command lines on a fixed set of invocations and requires identical standard output, agreement on failure, and identical files written — the JavaScript build, the LLVM IR, and the image mandelbrot renders on both targets. scripts/bootstrap.sh now builds the compiler with onus build at every stage.

170. The reports in Onus read the ledgers. ledger.onus reads <root>/.onus/ledger/{assumptions,coverage,mutations}.json as report/ledger.ts does (absent or malformed reads as empty); the command line puts them in the context, and the interface and path documents now carry last_verified, checked_exercised, assumptions_verified and the mutation counts from them, in the same scope as the TypeScript reports (a module’s name prefix, a path’s reachable functions). The CLI differential found this: the mandelbrot example keeps a mutation ledger from an earlier onus test --mutate. Under policy verified_assumptions_only an assumption with a passing record is now current; its age is not checked, because io.Clock has no reading primitive — the third candidate for the process.

2026-09-06 — polymorphic recursion (M15.5, the first change through the process)

171. Polymorphic recursion is E0345 (spec §3.6). A generic function calling itself, directly or through other generic functions, at an instantiation that places one of its own type parameters inside a type constructor (depth[T] calling depth[Pair[T]]) needs an unbounded set of instantiations, which the native target’s monomorphisation (impl spec §6.1) cannot compile; Rust and Go reject it likewise. The types pass builds the instantiation graph after every module — a node per (generic function, type parameter); for a call in f to a generic g passing τ for g’s parameter Q, an edge from (f, P) to (g, Q) for each type parameter P of f occurring in τ, expansive when τ is not P itself — and reports an expansive edge whose target reaches its source, once per call, on every target. What is lost is nested data types whose type encodes a shape invariant; Onus states those as contracts. Fixtures: test/checker/e0345_polymorphic_recursion.onus (the nested Nest[T]) and test/checker/ok_generic_recursion.onus (recursion at the same type, mutual recursion between generics, generic code calling generics at concrete types, and Tree[T]). Made in both compilers: the process’s freeze of the TypeScript compiler starts when M15.7’s fixture runner exists, since until then the fixture suite and the differentials run over the TypeScript library (the skill’s text is corrected). Review artefacts: the interface diff of self/typecheck.onus is + fn polymorphic_recursion, compatible; the ledger delta of the module is 23 obligations added, none removed, no status changed — 12 proved (10 measures, the rest refinements and a loop invariant) and 11 checked, all of them representation and overflow obligations, which v0 checks at runtime by rule (§6.1). self/codes.onus changed in the body of title only.
172. A structural measure is never a runtime check. Found by the accepting fixture above under --emit ts: when a function’s decreases measure is a record, union or list and its obligations are not yet final (a pipeline stopped before verification, as the TypeScript-oracle test stops), both lowerings emitted $measure as an Int local and a < check against it at each recursive call, which tsc --strict refuses and which at runtime would compare aggregates. The verifier settles a structural measure as proved or as E0344; only a numeric measure (Int or Duration, §5.1) is ever checked at runtime, so codegen/lower.ts and self/lowerir.onus now emit the measure local and the checks only for numeric measures. Product output is unchanged: after verification a structural measure has no unproved obligation.

2026-09-06 — Map on the native target (M15.5)

173. Map and Dict natively; calls carry their type arguments. The C runtime gains an insertion-ordered hash table keyed by value (Int, Duration, Bool, Unit as slots, Text by its bytes), with tombstones for removal and Map.put copying (spec §19.1). The twelve std.map intrinsics no longer claim host.js. The emitters pass a key kind on every keyed operation, taken from the call’s type arguments, which the target-neutral form now records: call gains targs, the instantiation of the callee’s type parameters at the call (empty for a non-generic callee), printed as f[Int, Text](…) in the form’s text. A Dict keyed by any other type — Float included, whose JavaScript equality is not slot equality — is E0800 on the native target. Fixtures: test/native/dict.onus runs on both targets (text and integer keys, insertion order under replacement and removal, the persistent Map); test/native/e0800_dict_key.onus pins the refusal. No generic function over a Dict[K, V] compiles natively yet: the key kind of a type parameter waits on the specialisation step (impl spec §6.1). Review artefacts: the interface diff of self/ir.onus is the Call variant of Expr gaining targs (reported breaking, as a public union’s shape is); of self/native.onus, two private functions added and call_val’s signature widened by the type arguments; self/lowerir.onus, self/irtext.onus and self/jsemit.onus changed in bodies and pattern arity only. Ledger deltas: ir: 0 -> 0 obligations; added 0 ({}; checked kinds {}), removed 0, status changes 0; native: 240 -> 242 obligations; added 2 ({‘checked’: 1, ‘proved’: 1}; checked kinds {‘representation’: 1}), removed 0, status changes 0 — the checked additions are representation and overflow obligations, checked at runtime by rule. The chain from bootstrap/ reached the fixed point and stage2 was promoted.

174. Generic code compiles natively by specialisation (impl spec §6.1). codegen/specialise.ts and self/specialise.onus run first inside emitNative: every call to a generic function is retargeted to a copy of it specialised to the call’s type arguments (from the targs item 173 added to calls), copies are named f[Int, Text], appended to their module in discovery order, and specialised in turn until the set is closed — finite by §3.6, the rule item 171 made for this. Inside a copy the type parameters are concrete, so equality on a type parameter, a Dict keyed by one and the rest resolve to the concrete type; generic functions themselves are dropped, and the emitters’ reachability is keyed by emitted name rather than definition, since a definition now has many copies. The JavaScript target is untouched. Fixture: test/native/generics.onus — swap[T], first_or[T], equality on a T, count_of[T], List.index_of at Text and Bool, and a Dict[K, Int] keyed by a type parameter — runs on both targets. The native census of the compiler itself fell from 481 refused functions to 14 (five Text.trim, five hash.blake3_hex, one each of Text.lower, len, graphemes, and a Bytes value). Review artefacts: the interface diff of self/native.onus is the five reachability visitors taking a context and a queue of names (private, reported breaking) and emit_native unchanged; self/specialise.onus is new, 266 obligations, 177 proved and 89 checked, every checked one a representation or overflow obligation; the native ledger lost one obligation with no status change. Fixed point reached from bootstrap/; promoted.

175. The rest of the primitive surface natively; no stdlib module claims host.js (§19.1). The C runtime gains onus_lib.c: Text.len, graphemes, lower, upper and trim over Unicode 16.0 tables generated from the UCD by scripts/unicode-tables.mjs into unicode_tables.h (grapheme clusters per UAX #29 with the GB9c, GB11 and GB12–13 state; default case conversion with SpecialCasing’s one-to-many mappings and Final_Sigma; trim over JavaScript’s WhiteSpace and LineTerminator set, which is what the host does); Bytes as the text layout, so Text.bytes is a view and Bytes.len/get read it; hash.blake3_hex over the vendored BLAKE3 1.8.2 reference implementation in blake3/, built portable (-DBLAKE3_NO_*, -DBLAKE3_USE_NEON=0); io.run over posix_spawnp with three pipes, poll and a monotonic deadline, returning the Output record, NotFound for a program that cannot start and Other with “prog did not finish within N ms” on timeout, exactly the host’s messages, and Other for every call under WASI, which has no processes; io.mkdir creating parents; and typeinfo.name/fields reading a two-slot object. Both native emitters build that object where a type is used as a value (the expression form and the compile-time value, through typeSlug/lowerir.type_slug) in place of the null they emitted, emit Bytes constants as text-layout globals, and map Bytes to a pointer; both build drivers add the new C sources and flags. The ten remaining claims host.js in std.text, std.bytes, std.hash and std.typeinfo are removed with their std.host imports. Spec §19.1 lists the primitives. Fixtures: test/native/text_native.onus (lengths, cases, bytes, BLAKE3 vectors, TypeInfo; runs on both targets), test/native/process_native.onus (a main exercising run five ways and mkdir, compared to the JavaScript build’s output and files), and test/native/unicode.test.ts driving unicode_probe.onus: case conversion and trim for every code point of the cased blocks (over 14,000) and Final_Sigma, SpecialCasing and grapheme clustering over 31 texts, each line compared with what the Node host (ICU, Unicode 16.0) computes. Review artefacts: the interface diff of self/native.onus is three private functions added (bytes_global, typeinfo_obj, typeinfo_owner) and the module comment (reported breaking, as any doc change is); self/nativebuild.onus unchanged; ledger delta of native +6 obligations, 4 proved, 2 checked (both overflow on a counter and a length in bytes_global, like every checked obligation in the module), no status change; nativebuild unchanged. The native census of self/cli.onus is zero: onus build self/cli.onus --target native writes cli, and that binary, with node absent, checks mandelbrot with every obligation proved through z3 by io.run in 0.7 s and builds it for the native target to an image byte-identical to the node-hosted build’s. It still needs --stdlib and --runtime; embedding them is the release work of M15.5. Fixed point reached from bootstrap/; promoted.

176. A column counts code points (§13). The first fixture with characters outside the Basic Multilingual Plane (item 175’s text_native.onus) made the two compilers disagree on one column: the TypeScript compiler computed columns as UTF-16 units from the offset, the compiler in Onus as code points, and the specification said neither. Code points it is, since a column must not depend on the host’s string representation; source.ts now counts them and the spec says so. Fixture: test/checker/e0105_columns_code_points.onus, an unknown name after four flag emoji at column 20 rather than 24. The compiler in Onus is unchanged.

177. Interface calls inside obligations lower per receiver sort. The first fixture that did arithmetic on an interface method’s result (total + Shape.area(s: x) with x: T bounded by Shape) was E0999 in both compilers: the verifier names the uninterpreted function for a call by the sorts of its instantiated parameters, but for a call through an interface the checker appends the interface’s own type parameter to the call’s instantiation (callSignature) and the verifier’s substitution stopped at the method’s own type parameters, so the function was declared over the interface’s parameter sort and applied at the caller’s. Both verifiers now bind the interface’s parameter to that last type argument (verify/lower.ts, self/lower.onus: res_iface, iface_param_of), so Shape.area at Rect and at a caller’s T are two functions and an ensures stated through the interface is proved. Fixture: test/verify/ok_interface_calls.onus, 13 proved and 7 checked, no diagnostic. The Onus verifier’s interface gains two private functions; its ledger +4 obligations, 1 proved and 3 checked representation obligations on the new loop indices, no status change.

178. Function values, closures, interfaces, runtime quantifiers, fake and old(...) compile natively (§19.1). Both native emitters: a value of a function type is a pointer to a closure object, slot 0 the code address and the rest the captured values, and its code takes the object and one slot per parameter (ptr for inout) and returns a slot. A declared function used as a value gets an adapter @"m.f$fn" from that convention to its signature and a constant object @"m.f$val", emitted once; a closure is lifted to @"closure$N" over its free locals (a walk of its body in first-use order, less what it binds), captured by value at construction as §3.7 requires, and returns slots, so try and return inside it convert through the function’s own return type. An impl’s dictionary is a constant table of its methods’ objects in interface order, reached with the dictionary; a bounded type parameter’s dictionary is a hidden leading ptr parameter, and a call through a dictionary loads the method’s slot and calls it as a closure. A quantifier evaluated at runtime is a loop over its domain (range, list, the list inside an Ok/Some or nothing, the two Booleans) stopping at the first counterexample or witness. fake is an object of its behaviours, which no primitive reads. old(x) in a checked postcondition copies x where its type can be mutated in place — builders, grids and maps through new runtime primitives (onus_list_builder_copy, onus_grid_copy, onus_map_clone), lists, records and unions holding them through a generated copier per type, everything else shared, which is indistinguishable from the JavaScript host’s deep copy. What E0800 still refuses: Spec values, a generic function used as a value, and sql without libpq. Fixtures: test/native/function_values.onus (declared functions and intrinsics as values, closures capturing lets and parameters, closures returned, composed, stored in records and lists, passed with inout, two impls of an interface with bounded generic callers, quantifiers over lists, ranges, results and Bool) and test/native/old_native.onus (a builder and a record holding one, with postconditions the verifier cannot prove so the copies run); both run on both targets, as do codegen/features.onus, stdlib/list_generic.onus and the interface fixture of item 177, which the native suite now lists. test/native/unsupported.onus is gone with its test, since its program compiles; the E0800 path is pinned by the Dict key fixture. Review artefacts: the interface diff of self/native.onus is two private records and 27 private functions added, call_val taking the call’s dictionaries, and the state record and module comment changed; self/lower.onus as item 177. Ledger delta of native: +401 obligations, 254 proved and 147 checked, every checked one an overflow or representation obligation on counters, indices and sizes, like the rest of the module; no status change. The codegen differential found one disagreement while porting — the Onus emitter generated a copier before allocating the call’s temporary, one counter apart from the oracle — fixed in the port. Fixed point reached from bootstrap/; promoted.

179. The native stage of the bootstrap chain, and the differentials run natively (impl spec M15.5). scripts/bootstrap.sh, after the fixed point, has stage2 build self/cli.onus for the native target and then runs that executable with a path holding only clang, z3 and the system directories — no node, no TypeScript — to build the compiler for JavaScript, which must equal stage2 file for file, and for the native target, whose LLVM IR must equal what stage2 emitted for it; the stage is skipped with a notice without clang. The seven differential tests under test/self/ take their driver from test/self/driver.ts: under node as before, or, with ONUS_SELF_NATIVE=1 (pnpm --filter compiler test:self-native), the program of self/ built with onus build --target native — lexdump, astdump, fmt, check and cli — so that lexing, parsing, printing, checking, verification, the reports, code generation for both targets and the command line are compared with the TypeScript compiler on every source with the compiler in Onus running natively; the assertions that run a driver’s own examples as generated JavaScript tests are skipped in that mode. Measured on this machine: the JavaScript-hosted stage2 builds the compiler natively in 5 s, and the native compiler builds itself for JavaScript in 1.2 s and for the native target in 3.6 s. The native run found one disagreement in the repository: e0701_const_evaluation.onus declared the constant 9007199254740993, which the JavaScript host holds as the double 9007199254740992 (item 99’s deferred arbitrary-precision path) and the native host holds exactly, so the E0701 text differed by one. The fixture now uses 2^53 itself, outside the safe range and the same number on every host, so it pins the rule rather than the host’s rounding; the inexactness of Int beyond 2^53 on the JavaScript target stays item 99. No language or compiler change; the skill’s steps 5 and 6 name the stage and the native differentials.

180. The compiler carries the standard library and both runtimes (impl spec M15.5, release). self/bundle.onus, generated by scripts/bundle.mjs and committed, holds every file of packages/stdlib/std, the JavaScript runtime’s dist/*.js and the C runtime (onus.c, onus.h, onus_lib.c, onus_sql.c, unicode_tables.h, blake3/, its licence) as text constants, with the root package’s version; a test regenerates it and compares. The loader reads std.* from the bundle when no --stdlib (or ONUS_STDLIB) is given, under the paths onus:std/…, and the prelude is always imported. onus build with no --runtime (or ONUS_RUNTIME) writes the JavaScript runtime to <out>/onus-runtime/ and generated modules import ./onus-runtime/index.js, climbing out of their own directories (../onus-runtime/index.js from std/); --target native with no runtime location writes the C sources to <out>/native/runtime/ and compiles against them. onus --version prints the version. So that a generated JavaScript program depends on nothing installed, the runtime hashes with its own BLAKE3 (packages/runtime/src/blake3.ts, checked against the reference implementation at every structural boundary in test/stdlib/blake3.test.ts) and @noble/hashes is no longer a dependency of the runtime; pg remains one for programs that use sql, loaded only when they do. Found on the way and fixed: the command line in Onus rejected a bare entry name (onus check main.onus) with E0104, since the root it derived was the working directory and the path had no directory; a bare name now lives at .. The TypeScript compiler is unchanged: it resolves its runtime from the workspace, and the differentials always pass --stdlib and --runtime. Fixture: test/self/cli.test.ts builds the command line natively, removes node from the path, and checks, builds for JavaScript, runs under node, builds natively and runs mandelbrot from a directory holding only its source, the two images equal; test/self/bundle.test.ts pins the bundle. Review artefacts: self/bundle.onus is new (a record, two constants, two functions, no obligations); the interface diffs of self/loader.onus, self/nativebuild.onus and self/cli.onus are empty but for the usage text, and self/build.onus gains write_bundled_runtime (public) and runtime_for; ledger deltas: build +2 obligations, both checked (a representation and an overflow obligation on the directory depth), the other three unchanged. Fixed point reached from bootstrap/, the native stage agrees; promoted.

181. A self-contained bootstrap/, and the build on GitHub (impl spec M15.5, release). The chain no longer passes --runtime: every stage after the first is built by the compiler in Onus, which carries its runtime (item 180), so a stage holds onus-runtime/ and imports it relatively, and the chain runs from the repository root with relative paths, so nothing it emits names a machine. bootstrap/ therefore builds the compiler wherever node runs, which the workflows rely on. .github/workflows/ci.yml runs the gates on every push and pull request on Linux: the packages build, the whole suite, the chain with its native stage, and the self differentials against the native compiler, with clang and z3 installed and the proof caches kept between runs under a key of the sources they were computed from. .github/workflows/release.yml runs on a tag v* (and by hand): Linux x86_64, Linux arm64 and macOS arm64 each build onus from bootstrap/ with node and clang as build-time dependencies only, refuse a tag that does not name the root package’s version, smoke-test the binary from a bare directory with no node on its path, and package onus, the licences and the README as onus-<version>-<target>.tar.gz; a final job creates the GitHub Release with one archive per platform. macOS on Intel is not built (decided 2026-09-06); Windows waits on the C runtime’s port and is the next item. The first run published v0.0.0 for the three platforms; the Linux builds verified the compiler cold in 10.5 minutes and, with the proof cache restored, in under a minute. The first CI run found two host differences and no compiler fault: vitest colours its output on GitHub, so the generated-tests check now runs it without colour; and the runner’s node carries Unicode 17.0 while §19.1 pins 16.0 (six Latin letters given case mappings in 17.0 differed), so the comparison of the native text tables with the host runs only on a host at 16.0 (process.versions.unicode) and ci.yml pins node 22.13.0, which has it. When the specification moves to a newer Unicode, the tables, the guard and the pin move together.

182. A Homebrew tap. brew install JamesRandall/onus/compiler installs onus on macOS (Apple Silicon) and Linux (x86_64, arm64) from the release archives, with z3 as a dependency, so a Mac user is never asked by Gatekeeper about an unsigned download; the formula is named compiler in the tap JamesRandall/onus (repository homebrew-onus), as decided 2026-09-06. scripts/brew-formula.sh <version> <archives> renders Formula/compiler.rb from the archives’ checksums, and the release workflow’s last job pushes it to the tap when the secret HOMEBREW_TAP_TOKEN (a fine-grained token with write access to the tap) is present, otherwise attaches it to the run for a manual update. The formula’s test checks the version and checks a small program. Signing and notarising the macOS binary would need an Apple developer account and is not done; Windows, once ported, gets no Homebrew route.

183. A clock reading: io.now (§19.1; the first M15.6 language change). io.now(clock: io.Clock) -> Duration may io.clock, nondet is a monotonic reading since the program started, at the host’s resolution, which two readings compare and subtract; it is not a calendar time. Chosen over nanoseconds since the epoch because a monotonic reading is an exact Int on every target, while epoch nanoseconds exceed the JavaScript host’s exact range (item 99), and because timing — budgets, timeouts, elapsed time — is what the compiler needs. The JavaScript runtime reads performance.now(); the C runtime reads CLOCK_MONOTONIC against the origin onus_start records. Neither compiler changes: the intrinsic is declared in std.io and both emitters map it as they map every primitive. Fixture: test/native/clock_native.onus, a main whose two readings are ordered and small, run on both targets. The fixture found that the C runtime had never carried the two std.duration primitives, nanos and of_millis, since no native program had used a Duration; they are an identity and a multiplication over the nanosecond i64, and §19.1’s surface is complete again. Process: made through the skill with the chain’s native stage and the native differentials; self/bundle.onus regenerated so the compiler carries the new runtime; self/ does not use io.now in this change.

184. A process on the standard streams: io.exec (§19.1; the second M15.6 language change). io.exec(process: io.Process, program: Text, args: List[Text]) -> Result[Int, Error] may io.file, nondet, alloc runs the program with this process’s own standard streams inherited — what it reads and writes is the user’s terminal, not captured — and returns its exit status, -1 when a signal ended it; a program that cannot start is NotFound, any other failure Other, and under WebAssembly every call is Other. The JavaScript runtime spawns with the streams inherited; the C runtime flushes its own buffers and spawns without file actions. This is what onus run needs to hand a program the terminal instead of relaying its captured output after it finishes (item 169); the command line takes it up in a later change, since self/ may not use a primitive in the change that introduces it. Neither compiler changes. Fixture: test/native/exec_native.onus, a main whose child writes to the shared output and exits 3 and whose second program does not exist, the same output on both targets. Process: through the skill with the native stage and the native differentials; self/bundle.onus regenerated.

185. main chooses its exit status (§8.3; the third M15.6 language change). main returns Result[Unit, E] or Result[Int, E]: Ok(Unit) ends the process with status 0, Ok(n) with status n as the platform takes it, Err(e) writes the error to standard error and ends with 1, a panic with 2; any other return type is E0604, new in both checkers’ capabilities pass (mainStatus, main_status), which before accepted any return type while both runtimes reported every Ok as 0. The lowering’s description of main gains status, printed as status in the target-neutral form and written into the launcher’s JSON; the JavaScript runtime returns the Ok value as the exit code when the description says so; the native emitters pass the flag to onus_finish(ptr, i1), which reads the Ok slot. Fixtures: test/checker/e0604_main_return.onus (a main returning Int) and test/native/status_native.onus (a main returning Ok(3), exit status 3 on both targets with nothing on standard error). This is what the command line in Onus needs to report usage and I/O failures as 2, as the TypeScript one does (item 169); it takes the feature up in a later change, with io.exec for run. Review artefacts, under .onus/changes/185/ (item 186): the interface diffs of self/ are MainSpec gaining status (ir), and one private function each in lowerir, irtext and native, plus the public main_status in capabilities, which the lowering shares; ledger deltas are +2 in capabilities (one proved, one checked representation obligation on the looked-up definition), the other six unchanged. Fixed point reached, native stage agrees, promoted; self/bundle.onus regenerated.

186. Review artefacts under .onus/changes/<item>/. Until now the interface diff and the ledger delta the process makes the human review were computed in passing and paraphrased in the CHANGES.md item, with the before-snapshots in an ignored directory and the after-documents nowhere. scripts/change-review.mjs begin <item> <module>... snapshots the interface documents before a change, and finish <item> writes, under .onus/changes/<item>/ (ignored by git, as the loop’s proposals are; decided 2026-09-06), each module’s §15.1 interface diff, its interface after the change as JSON and as canonical text with bodies elided, and ledger.md: every obligation added, removed or changed in status, per module, keyed by definition, kind and text. The documents come from the compiler under bootstrap/. The skill’s steps 3, 6 and 7 name the script and the directory. Change 185’s artefacts were produced from its snapshots after the fact; items 183 and 184 touched no module of self/ but the generated bundle.

187. The command line reports exit statuses and hands run the terminal. With items 184 and 185 promoted, self/cli.onus uses them: its main returns Result[Int, io.Error] and reports what the TypeScript command line does — 0 success, 1 diagnostics (or a breaking interface, or a native build that failed), 2 usage or I/O failure — by mapping each command’s outcome through one table of the markers the commands already returned, printing onus: <error> for a failure no command reported itself; check and fmt now return the diagnostics marker after printing their counts rather than the count as the error the runtime used to print. run starts the program through io.exec on the user’s own streams and ends with the program’s status, 1 when a signal ended it or it could not start, as the TypeScript one does; the captured relay is gone. That closes both notes of item 169. Fixture: test/self/cli.test.ts now requires identical exit statuses on every invocation, not agreement on failure alone; it caught the two commands whose markers had not been mapped. Review artefacts under .onus/changes/187/: the interface diff of self/cli.onus is main returning Result[Int, io.Error], build_command and run_program returning the status, the module header (the doc comment of usage), and four private functions added (failure_status, exit_status, exit_status_of, usage_failure); the ledger delta is one obligation fewer, the proved refinement on io.run’s timeout argument that exec does not take, no status change. Not a language change; made through the process for the chain and the differentials.

188. io.remove_all and io.list_dir (§19.1). io.remove_all(files: io.Files, path: Text) -> Result[Unit, Error] may io.file removes a file, or a directory and everything under it, and is Ok when nothing is there; io.list_dir(files, path) -> Result[List[Text], Error] may io.file, alloc is a directory’s names in code point order (UTF-8 byte order natively, the same order), without . and .., NotFound when the directory is not there; a permission failure is Denied. onus test needs both, as the TypeScript command line has them: to clear the coverage files of the previous run before merging the new ones, so the ledger reflects the last run alone, and to find the files the test workers wrote (item 189). The JavaScript runtime removes recursively and forcibly and reads the directory; the C runtime walks the tree and sorts. Neither compiler changes. Fixtures: test/native/remove_native.onus (a tree, a file and something absent removed) and test/native/list_native.onus (names listed in order, a missing directory NotFound), the same output on both targets. Process: through the skill; self/bundle.onus regenerated; self/ does not use them in this change.

189. onus test in Onus: examples, properties and laws, and obligation coverage (M15.6; §19.5, §20.5, §20.6). self/testcmd.onus (new) and self/cli.onus provide onus test <entry> [--out <dir>] [--target js|native|all] as the TypeScript command line does. On js: build, run the generated example, property and law tests under vitest on the user’s own streams (io.exec), fold the hit files the test workers wrote under <out>/coverage/ (cleared first, so the ledger reflects the last run alone) into <root>/.onus/ledger/coverage.json, keeping the larger count per check, and print obligation coverage: … over the program’s own obligations and assumptions; the status is vitest’s. On native: build the executable and run its examples, printing what it prints; 1 when any fails. On all: also run the examples under vitest’s JSON reporter (<out>/examples.report.json), print each outcome with (js), and report every disagreement as E0801 (§19.5); 1 on a disagreement or a failure. A program with no example, property or law says so and succeeds. --assumptions and --mutate are refused with status 2 and run with the TypeScript onus until items 190 and 191; build’s runtime selection moved into runtime_choice, shared with test. One change to both compilers, forced by the port: onus test used to hand the coverage directory to the generated tests through the environment, which io.exec does not pass on (item 184); the generated vitest.config.mjs now sets ONUS_COVERAGE_DIR itself, to coverage/ beside the config (from import.meta.url) when the environment does not, so a run of the generated tests by any means records beside the program. The first attempt wrote the output directory’s absolute path into the config and the chain caught it: stage2 and stage3 differed in that one line. Two deliberate differences from the TypeScript helpers: the module of a vitest test file is found by matching its path against the emitted modules rather than by the output directory’s length, and the JSON-reporter run does not set CI=1, which only affected the terminal reporter. Fixtures: test/self/cli.test.ts gains test on test/native/primitives.onus staged in a fresh directory (equal exit status, equal obligation coverage line, equal coverage.json byte for byte; a program without tests; the refused switches and an unknown target) and test --target native and --target all on primitives and mandelbrot (standard output and status identical). Review artefacts under .onus/changes/189/: the interface diff of cli is RuntimeChoice, runtime_choice, test_command and js_flag added and the module comment and usage text changed; build has no interface change; the ledger delta is cli 45 → 48 obligations (28 proved, 20 checked: one index refinement proved, two representation obligations on counters checked) and testcmd new with 22 (10 proved, 12 checked: the representation and overflow obligations on counters and indices, as throughout self/). Fixed point reached from bootstrap/, native stage agrees; promoted.

190. A calendar time: io.time (§19.1; an M15.6 language change). io.time(clock: io.Clock) -> Int may io.clock, nondet is the calendar time as whole milliseconds since 1970-01-01T00:00:00 UTC, an Int that is exact on every target (item 99 is why it is milliseconds in an Int and not nanoseconds in a Duration); io.now (item 183) stays the monotonic reading for timing. onus test --assumptions needs it to date the ledger’s last_verified records (§20.3), which the TypeScript command line takes from the host’s clock, and the checker’s age rule on those records (test.max_assumption_age_days, item 90), which the compiler in Onus has not enforced for want of a clock (self/ledger.onus), can follow. The JavaScript runtime returns the host’s epoch milliseconds; the C runtime reads CLOCK_REALTIME. Neither compiler changes: the intrinsic is declared in std.io and both emitters map it as they map every primitive. Fixture: test/native/time_native.onus, a main whose reading lies between 2020 and 2100 and whose two readings are ordered, run on both targets. Process: through the skill with the chain’s native stage and the native differentials; self/bundle.onus regenerated; no self/ module changes, so there are no review artefacts beyond the bundle; self/ does not use io.time in this change.

191. onus test --assumptions in Onus (M15.6; §20.2, §20.3, §20.6). self/assumptions.onus (new; codegen/assumptions.ts), self/config.onus (new; config.ts: onus.json’s test.env, test.target and test.max_assumption_age_days, with the defaults) and self/cli.onus provide onus test <entry> --assumptions [--env <test module>]: the entry and the environment module (--env, else onus.json’s test.env under the root) are loaded and checked through paths; the environment’s producers are its public zero-parameter functions returning a capability; every module is emitted with its verify blocks as functions; a verify parameter with neither a producer nor a root capability of std.io is E0603; the launcher run_assumptions.js is written as the TypeScript one is, byte for byte, and run under node through io.run (an hour’s timeout, where the TypeScript command line has none); its outcomes are printed one per line and recorded in .onus/ledger/assumptions.json under the calendar time of the run, io.time (item 190) formatted as Date.toISOString prints it (assumptions.iso_of_millis, pinned by an example on four dates); the ledger keeps the records of earlier runs, in file order. The command line’s main takes io.Clock for it. Two loader fixes the port exposed, in both compilers so the differential stays meaningful: a second bare file name (onus check checkout.onus test_env.onus) is at the working directory’s root like the first (item 180 covered the first alone, loader.root_for), and the inferred root is the entry’s directory as the entry names it, so imported files are reported the way the entry was given (vendor/payments.onus, not ./vendor/payments.onus and not the absolute path the TypeScript loader used to print for a relative entry). Fixtures: test/self/cli.test.ts gains test --assumptions on the checkout example staged in a fresh directory: standard output and status identical, the launcher byte for byte, the ledger equal but for the time, the time in the ISO form; the environment named with --env and a second run over the ledger the first left; without onus.json, E0603 on both, identical; and the two-bare-files check. Review artefacts under .onus/changes/191/: the interface diff of cli is test_assumptions, config_env_path, module_at_path, file_id_of, module_of_file and copy_record added, main and test_command taking clock: io.Clock and claiming io.clock, and the module comment and usage text changed; loader has no interface change; the ledger delta is cli 48 → 54 obligations (29 proved, 25 checked: a refinement proved, four counter representations and overflows checked), loader unchanged, config new with 1 (checked, a representation) and assumptions new with 81 (45 proved, 36 checked: the representation and overflow obligations of the date arithmetic and of counters, and the four example assertions, which run rather than prove). Fixed point reached from bootstrap/, native stage agrees; promoted. --mutate is next (item 192).

192. onus test --mutate in Onus (M15.6; §20.4). self/mutate.onus (new; mutate/mutate.ts) and self/cli.onus provide onus test <entry> --mutate: every contract weakening §20.4 names over the program’s own modules — each ensures clause dropped, each refined result or record field widened to its base type, each guarded property’s guards negated — assessed one at a time. A static weakening is detected when a test assertion the verifier proved becomes unprovable: the conditions are rebuilt with the weakening in force and the proved assertions put to z3 again, the first that is no longer unsat naming the detector; without z3 the static weakenings are skipped and a line on stderr says so. A guard negation is detected when the property, re-emitted with its guards negated into <out>-mutate/mutate/<i> and run under vitest’s JSON reporter, fails over the complement of its domain. Survivors are M0001 undetected contract weakening rows of the run, not diagnostics; the records go to .onus/ledger/mutations.json under the calendar time of the run, and the status is 0. For the static weakenings the verifier in Onus gains what the TypeScript one has had since M13: lower.Mutation (kind, definition, clause span, field) is carried by the lowerer’s state, and three places withhold a fact under it — the callee’s result refinement (widened_ret), the callee’s ensures clause at the span (dropped) and a record field’s refinement (field_type); vc.build_vcs takes the mutation, None from the verifier. The port found nothing to change in either compiler. Fixtures: test/self/cli.test.ts gains test --mutate on test/mutate/unexercised.onus (the guard of half_is_smaller detected, plus_zero’s surviving, the widened result of half surviving under z3; standard output and status identical, the records equal, the time in the ISO form, the programs under out-mutate/) and on mandelbrot (dropping the ensures of escape_count detected by escape_bounded, M13’s acceptance, identical on both). Review artefacts under .onus/changes/192/: the interface diff is lower with Mutation added, Lw carrying it and new_lw taking it, vc.build_vcs taking it, and cli with test_mutate added and the usage text changed; verifier unchanged; the ledger delta is cli 54 → 59 (30 proved, 29 checked: a refinement proved, counters checked), lower 349 → 352 (three representation obligations on definition ids checked), vc and verifier unchanged, mutate new with 12 (3 proved, 9 checked: representation and overflow on ids, budgets and the counter). Fixed point reached from bootstrap/, native stage agrees; promoted. test is now whole in Onus; review, next and loop remain.

193. onus review in Onus (M15.6; §15). self/review.onus (new; report/review.ts and the @onus/review package’s render.ts and layout.ts) and self/cli.onus provide onus review <entry> [--out <dir>] [--against <interface.json>]: after the pipeline ran to paths the bundle review.json is collected — every user module’s interface document (item 92’s interface_of) and canonical source, every path report, the diagnostics as JSON, the interface diff of the entry module against the given document, and the changes the regeneration loop wrote under .onus/changes/*/change.json, narrowed as the page shows them and newest first — and index.html renders every view of it: the path view with its layered graph (breadth first from the entry, as authority flows; unresolvable calls as breaks; gate regions around the guarded nodes), the interface view with bodies collapsed and their opening counted, the ledger view with its filters, the diff view, the changes view with proposals marked as the loop’s, and the diagnostics view with the solver’s model. The renderer reads the JSON documents directly (json.Json), since every document is produced by a module self/ already has, and its page is byte for byte the TypeScript page: the same style sheet and script, the same markup. Diagnostics are reported on the terminal and the page then holds them alone; the status is 1 when any was reported, 2 when --against does not name an interface document. The run’s time (io.time, item 190) dates the bundle. Neither compiler changed. Fixtures: test/self/cli.test.ts gains review on the checkout example staged with a loop change written under .onus/changes/task_test/ (the bundle and the page identical but for the time; the assumed leaf, the gate, the blocked change and its proposal, the collapsed body present), --against a renamed copy of its own interface (identical; the diff view present), --against a file that is not a document (status 2), and an invalid program (identical; status 1; the page holds E0416). Review artefacts under .onus/changes/193/: the interface diff of cli is review_command added and the usage text changed; the ledger delta is cli 59 → 60 (an index refinement proved) and review new with 123 obligations (26 proved, 97 checked: the representation and overflow obligations of the layout arithmetic and the counters, as throughout self/). Fixed point reached from bootstrap/, native stage agrees; promoted. next and loop remain.

194. Conditions with inout calls run when they are tested (impl spec §6, codegen; found by item 195). Two lowering bugs, in both compilers, the same way. A call with inout arguments lowers to a statement that assigns its results back, placed before the statement its expression belongs to. In a loop while condition that put the call before the loop, so the condition was evaluated once and every later test read a stale value: a loop guarded by below(c: inout c) and c.n < 10 ran to 10 and asked below once. As a later operand of and, or or implies it put the call before the whole expression, so it ran even when the earlier operands had decided the result. Now the condition’s own statements are collected: a loop whose condition has any runs them before the loop into a flag and again at the end of every iteration, the loop testing the flag; a chain whose later operand has any keeps the result in a flag and runs that operand under if flag (and), if not flag (or) or, for implies, the negated left side. A condition without such statements lowers as before, so every pinned form (test/codegen/lowered/) and every differential is unchanged. The compiler’s own parser never had an inout call in a condition until item 195 made its token tests record, which is how the bugs surfaced: the import loop stopped after one iteration and lookahead tests ran past a false left operand. Fixture: test/native/inout_conditions.onus, an example on every case (seen counts the calls, n the outcome), run on both targets. Neither the verifier nor the emitters change: the flag is a local of the IR the emitters already have. Review artefacts under .onus/changes/194/: lowerir has no interface change (Later, short_circuit and implies_expr are private); the ledger delta is 572 → 593 obligations (361 proved, 232 checked: the new functions’ fuel and index refinements proved, their representation and overflow obligations checked, no status changed). Process: promoted on its own before item 195, since a compiler whose conditions hoist would miscompile the parser that item instruments — the chain’s stage1 could not parse its own import line — which is the self-application rule of the skill in practice.

195. onus next in Onus (M15.6; §14). self/nextcmd.onus (new; next/next.ts), self/parser.onus, self/tokens.onus, self/loader.onus and self/cli.onus provide onus next <file> --offset <n> [--json]: the legal next tokens at the offset, the expected type there and the local names in scope, as the TypeScript command line prints them. The parser gains the two features its port left out (item 158’s note): the legal set and the hole. With a Cursor token at the offset (and eof after it, so the parser’s loops still run at the cursor), every grammar test of a token kind — the at_* functions, which now take the parser inout and record the kind when the tested token is the cursor, the set tests at_cmp_op, at_add_op, at_mul_op and at_literal_pattern, and expecting before the dispatches over items, statements, patterns and primaries — records into Parser.legal until the first syntax error or until the cursor is consumed (advance stops recording; take goes through it); loop guards and negative lookahead keep using kind_at, which never records, and the chained-comparison re-test peeks as the TypeScript one does. When the prefix ends with a newline the run without it adds the continuation kinds, as legalTokensAt does. parse_with_hole parses the prefix with a Hole token, closers for every open bracket and block, a newline and eof; primary makes it an ast.Hole, which the resolver and the checker already record under its span. next lexes the prefix (offsets are code points, item 181), adds the file with the holed parse (loader.add_parsed, split from add_file), runs load, resolve and types on it whatever the diagnostics, and reads the hole’s tables by the key of its zero-width span; the type text spells the refinements out innermost first (typecheck.show on the base). tokens.decoder_name_of maps the grammar names to the decoder vocabulary. Fixtures: test/self/cli.test.ts gains next at every token of test/next/positions.onus and at its end, --json output identical on both, plus the text form, an expected type with its refinement and the names in scope, and the refused offsets. The instrumentation is what surfaced item 194. The resolver’s list of names visible at a hole now walks every scope below the module’s, as the TypeScript one does: a record field’s refinement sees the earlier fields (the two positions the sweep found). Review artefacts under .onus/changes/195/: the interface diff of parser is Parser carrying cursor, recording and legal, the at_* functions taking the parser inout and claiming alloc (with accept_*, skip_newline, visibility and the recoveries), qtname_ahead and effect_follows likewise, and prefix_tokens, legal_tokens_at and parse_with_hole added; tokens.Kind gains Cursor and Hole and decoder_name and decoder_name_of are added; loader.add_parsed is added; cli gains next_command; resolve has no interface change. The ledger delta is parser 1153 → 1218 obligations (1053 proved, 165 checked: 48 proved and 12 checked added, the checked ones the representation and overflow obligations of offsets and counters; six proved obligations of take, parse_stmt, add_expr and mul_expr gone with the tests that moved into the helpers; no status changed), cli 60 → 62, loader 63 → 64, resolve and tokens unchanged, and nextcmd new with 14 (9 proved, 5 checked representations). Fixed point reached from bootstrap/, native stage agrees; promoted. loop remains.

196. std.http (§19.1; an M15.6 language change). http.request(net: io.Net, method: Text, url: Text, headers: List[Text], body: Text, timeout_ms: Int) -> Result[http.Response, io.Error] may io.net, nondet, alloc sends one request and waits for the whole response, Response {status, body}; http.post and http.get are the two shapes over it. Any HTTP status is a response; a host that cannot be reached is NotFound naming the URL, a request that does not complete within timeout_ms (0 for no limit) is Other, as is anything else that keeps the request from completing. The regeneration loop in Onus (item 197) needs it for the Anthropic and OpenRouter providers; the loop in TypeScript used fetch. The JavaScript runtime is synchronous, so the request runs in a child node doing fetch, the request on its standard input and the answer one JSON line back; the native runtime runs curl with its options in a configuration file (the headers, which carry keys, never touch a command line) and reads the status code --write-out appends to the captured body; curl must be on the path, as clang and z3 must. Neither compiler changes: the intrinsic is declared in std.http and both emitters map it as they map every primitive ($rt.http.request, @onus_http_request). Fixture: test/native/http_native.onus, a main that posts to a server the test starts on a local port, gets a missing path and a port nothing listens on, with the same output on both targets. Process: through the skill with the chain’s native stage and the native differentials; self/bundle.onus regenerated; self/ does not use std.http in this change.

197. onus loop in Onus (M15.6; docs/onus-loop-v0.md). self/regen.onus (new; packages/loop/src: task, env, model, edit, project, context, change, cycle) and self/cli.onus provide onus loop run <task.json> [--root <dir>] [--model <spec>] [--budget <ms>] [--json] [--no-write], the regeneration loop of the loop spec run in the compiler’s own process: the task validated as task.schema.json admits it (by hand: the same required keys, enumerations, minimums and forbidden extras), the scope read and put in canonical form, the baseline checked through paths with the working texts as entries (an import of a scope module finds the entry already registered, so the texts overlay the tree as the TypeScript readFile hook did), the targets selected, then the cycle of §4 — the model context of §3 assembled from the compiler’s own interface documents and reports, the answer’s fenced Onus parsed as a fragment, the target bodies spliced under their baseline signatures and the file put back in canonical form, the check with up to three rounds of high-confidence repairs inside the target bodies, the classification, the ladder of §4.1, the budgets of §4.2 — and the conclusion: the bodies written and change.json under .onus/changes/<task>/, or a blocked report with the last diagnostics and the best attempt. Proposals (§5), the regeneration audit (§8), tickets and the syntax notes with the legal tokens at the offending line (onus next, item 195) are as the TypeScript loop has them; change.json is the same document, byte for byte but for the time and the milliseconds, the prompt hash carrying the b3: prefix of the compiler’s hashes. The model sits behind generate: a scripted list of answers (the tests), Claude Code as a subprocess (sh unsets the CLAUDE* markers so a nested run may start), and the Anthropic and OpenRouter APIs over std.http (item 196), the keys from the environment or .env/.env.local in the root and the working directory, never a command line. Two deliberate differences: --root is taken as given rather than resolved, so the files a change names are as the root names them (the differential passes each side its own absolute root), and the model’s request timeout is the loop’s constant on every provider. The command line’s main takes io.Net for it. Fixtures: test/self/cli.test.ts gains loop run on the loop package’s calc fixture with a scripted model: a wrong body then a right one opening a change in two iterations (standard output, the written body and change.json identical), a stall walking the ladder to a blocked report (--json identical), a ticket answered with a proposal and no edit, an invalid task, an unknown model and watch. Review artefacts under .onus/changes/197/: the interface diff of cli is loop_command and six helpers added, main taking net: io.Net and claiming io.net, and the usage text; the ledger delta is cli 62 → 68 (35 proved, 33 checked: three index refinements proved, three representations checked) and regen new with 218 obligations (58 proved, 160 checked: the representation and overflow obligations of offsets, counters and budgets throughout, as everywhere in self/). Fixed point reached from bootstrap/, native stage agrees; promoted. With it every command of the TypeScript onus has its counterpart in Onus: M15.6 is complete, and M15.7 — retiring the TypeScript compiler behind a fixture runner in Onus — is next.

198. The fixture runner in Onus (M15.7, first step; impl spec §10). self/fixtures.onus is a program, run_fixtures <dir>... [--stdlib] [--out] [--runtime] [--update], that runs the compiler’s own test suite from a fixtures.json manifest in each fixture directory, in place of vitest over the TypeScript library. A manifest is one section or a list of sections, each of a kind: diagnostics (every .onus file, or sources, checked to the pass to under root, its diagnostics as {code, span, file?} and with ledger its obligations compared with .expect.json; ok_ fixtures, or the clean prefixes, and everything under expect_none must produce none; every code of the catalogue under the covers prefixes less except must be produced; budget/budgets, also, dir), canonical (own canonical form, messy/ pairs), lowered (the entry module’s target-neutral form against <golden>/<name>.ir.txt, <repo>/ standing for the working directory), examples (each source’s examples pass on the targets and the targets agree; dirs sweeps directories for sources with examples, skip_prefixes, allow_refusal admits E0800, properties includes properties and laws), and programs (cases whose main runs with args on the targets, writing the stdout file’s text and exiting with status; via a wrapper script). A section that requires z3 or clang that is absent is skipped with a notice; --update rewrites the expectation files exactly as the TypeScript harness did (verified byte for byte over every expectation in the tree). self/codes.onus gains all_codes(), the catalogue in order, for the coverage check. The manifests cover the fixture-shaped suites of test/syntax, roundtrip, checker (with std/reserved.onus, whose expectation is now a file), paths, verify, examples, codegen (goldens and the generated tests), stdlib (every std module checks; the examples of the five fixture modules) and native (the twelve programs that must agree on both targets, and the sweep of every fixture with examples under checker, paths, codegen, stdlib and native, refusal allowed); every existing expectation passes unchanged. Not reproduced: the AST equality of the round-trip property (the printed text’s equality with the fixture and its idempotence are), and the bespoke vitest cases (counterexample text, the worked-example paths, the native primitive programs, next, loop, review, mutate, the assumptions ledger), which become programs cases and CLI expectation fixtures in the next changes of M15.7. scripts/bootstrap.sh builds self/fixtures.onus at every stage beside self/cli.onus, so run_fixtures.js is in the fixed point, in the native compiler’s JavaScript build, and in bootstrap/; scripts/fixtures.sh runs the suite with it (ONUS_FIXTURES names another runner, such as a chain’s stage2 for the acceptance step of the skill); test/self/fixtures.test.ts builds the runner with stage0 and requires the suite to pass under it, the bridge while vitest exists. Review artefacts under .onus/changes/198/: the interface diff of codes is all_codes added; fixtures is new with 36 obligations (18 proved, the index refinements; 18 checked, the overflow obligations of counters and lengths and the representation obligations of pass indices, budgets and statuses, as everywhere in self/). Fixed point reached from bootstrap/, native stage agrees; promoted.

199. The bespoke tests as fixtures (M15.7, second step; impl spec §10). Every vitest case that asserted something in code rather than through a fixture is now a manifest case the runner in Onus (item 198) runs, and the runner grew the kinds they need. cli cases run the compiler under test (--cli, the run_cli.js beside the runner) in a staged working directory — a copy of stage_dir or the stage files, an earlier case’s directory (in), then write, remove and edit (from/to, dates_to, append) — with $dir, $stage, $root, $now and a marker-computed $offset substituted into the arguments, and check the exit status, the standard streams (stdout pinned to a file, stdout_text, stdout_contains, stdout_lacks, stdout_canonical, stderr_*) and the files left behind (files pinned, files_text, files_contain, files_exist, files_absent, file_hashes, count_files) after normalise rules (dates, ms, tokens, hash, stage, out, root, last_line). programs cases run each target in its own directory with env, via (a wrapper script: the std.http fixture’s local server), cflags, and compare the targets (same_stdout, same_files); a section may name the runtime its programs import and a probe program that must exit 0 for it to run (the std.sql cases lay out their schema in the probe and are skipped with its reason when no Postgres answers). builds cases must build, or be refused natively with the expected codes (E0800 for a Dict keyed by a record); examples sections take cflags and expect_disagreement (E0801 from the deliberately broken runtime); next_sweep checks that the token present is legal at every position of every source and pins the complete answer of onus next at every token of positions.onus; script cases pin a shell script’s output (the bundle’s freshness; the released native compiler with clang alone on the path, when --native-cli names one). requires may also name libpq, cli, native_cli and unicode16, on a section or a case. nativebuild.build_native takes cflags. The manifests: test/cli (the command line: check, fmt, --emit ir, interface and its diffs, path, build and run on both targets with the image’s hash, test with its coverage ledger, the assumptions of checkout and its path report, the policy verified_assumptions_only with a fresh, a stale and a failed record, mutation and the interface’s coverage counts, review with a loop change, against a previous document and of an invalid program, next at twenty-five positions, and the loop with a scripted model — 93 cases, 9 more needing z3), test/native (the primitive programs, the Unicode probe compared with the host’s tables on both targets, the broken runtime), test/codegen (the worked examples build, a violated requires panics with its obligation), test/stdlib (the process and file programs, BLAKE3 over the lengths that exercise every branch of the algorithm on both targets, blake3_lengths.onus), test/sql and test/next. The expectation files were generated with --update and read. Found by the conversion and fixed: the compiler in Onus never checked a verification record’s age — ledger.is_verified took any passing record — where the TypeScript compiler required one no older than max_assumption_age_days (§20.3); Context gains now_ms and assumption_max_age_ms, set by the command line from the clock and onus.json, ledger.is_current and ledger.millis_of_iso (the inverse of assumptions.iso_of_millis, with an example) decide, and the policy cases pin it. Also found: a program whose bundled runtime could not load pg hung forever in std.sql.connect, the main thread waiting on a worker that had died importing it; the worker now signals when it starts (the bridge gives up after 30 s) and imports pg on the first connect, so the failure is the connect’s Connection error. Not reproduced, and dropped with the TypeScript compiler: the fast-check round-trip over generated syntax trees, the JSON-schema validation of the interface, diagnostic and path documents (their shapes are pinned by the cli cases), the E0999 injection (the compiler in Onus has no exception to catch), and --emit ts. Review artefacts under .onus/changes/199/: the interface diffs are nativebuild.build_native and build_with taking cflags (breaking, two callers in cli), Context gaining now_ms and assumption_max_age_ms, ledger.is_verified gaining alloc with is_current, millis_of_iso and two helpers added, cli.setup and the five commands that call it taking the clock, and fixtures reworked (46 definitions added, run_program and outcome_ok removed, Options, Args and main changed). The ledger deltas: cli 68 → 69 (one overflow of the configured age in milliseconds, checked); paths 88 → 90 (the days of the message, one proved, one overflow checked); ledger 5 → 76 (27 proved: the index refinements and the day-of-year arithmetic; 49 checked: the representation and overflow obligations of the parsed fields and the millisecond products, and the seven assertions of the example); fixtures 36 → 125 (42 proved: the index and slice refinements, copy_tree’s decreases and the lexer’s precondition; 83 checked: the representation and overflow obligations of scanner indices and counters, as everywhere in self/); context, assumptions, config and nativebuild unchanged. The suite under stage2: 445 passed, 3 skipped (the fixture that does not check, the two Postgres sections). Fixed point reached from bootstrap/, native stage agrees; promoted.

200. The TypeScript compiler is removed (M15.7, done). packages/compiler, packages/loop and packages/review are gone with their vitest suites: the compiler is self/, and bootstrap/ — the JavaScript it emitted for itself at the last fixed point — is what runs it (pnpm onus is node bootstrap/run_cli.js). The fixture suite moved from packages/compiler/test to test/, manifests and expectations unchanged but for the paths they name ($dir kept the pinned outputs as they were; the lowered goldens name <repo>/test/…); the JSON schemas of the interface, diagnostic and path documents moved to docs/schema/, the loop’s to docs/schema/loop/; the loop benchmark is scripts/bench.mjs, running onus loop run --json from bootstrap/ per model. pnpm test is scripts/fixtures.sh; scripts/bootstrap.sh requires bootstrap/ as stage0 and has no TypeScript fallback; scripts/bundle.mjs formats the bundle with bootstrap/; CI builds the runtime, runs the chain, and runs the suite under the chain’s stage2 with its native compiler for the release case (the self differentials, which compared the two compilers, are gone with one of them). vitest and fast-check stay as the workspace’s dev dependencies because generated tests import them by name (onus test); typescript stays for the runtime. The documents follow: CLAUDE.md and AGENTS.md (the repository map, the commands, the hard rules that named TypeScript files or --emit ts, which no longer exists), impl spec §2 (the layout), §10, §11 and M15.7 (done), the skill (stage0, where codes and fixtures live, the acceptance step, and a history note in place of “While the TypeScript compiler exists”), the README, the grammar’s and the loop spec’s pointers, the website’s status and loop pages, and the comments in self/ that named their TypeScript originals. M15.7’s second acceptance — a deliberate change to an emitter in self/ is caught by the stage comparison before promotion — was exercised by item 194, whose loop-lowering fix first surfaced as a stage difference. Fixed point reached from bootstrap/, native stage agrees, the suite under stage2 green; promoted.

201. The hardened modifier (M16, first change; spec §2.3, §21; docs/CHANGE-LOG-03.md). Spec §21 “Zones” is inserted after §20 as the change log wrote it, and the grammar’s visibility becomes [ "pub" ] [ "hardened" ] [ "sealed" ] with hardened a reserved word (the grammar document likewise). The compiler in Onus parses, prints and carries it: ast.Visibility.is_hardened, defs.Def is_hardened (from the declaration’s visibility; false on every synthetic definition), the keyword in tokens, the parser’s visibility and its legal-token lists, the printer (pub hardened sealed record), so onus fmt and onus interface render it and onus next offers it. Nothing checks it yet: E0902 (the modifier outside a pub item of a draft module) needs the manifest and is item 202’s, with the dependency rule, E0900 and E0901. Under the self-application rule self/ does not use the modifier. Fixtures: test/roundtrip/36_hardened.onus (a fn, a record and a sealed record marked hardened, its own canonical form), test/syntax/e0003_hardened_reserved.onus (let hardened is a syntax error), and the cli cases interface_hardened_text (canonical text with the modifier) and interface_hardened_json. The milestone is M16 — Zones in the implementation spec (the change log said M14, which is the loop). The acceptance of the change log names app.core.*, app.reporting and app.payments; the worked examples of §18 keep their module names and are zoned as they are (impl spec M16). Review artefacts under .onus/changes/201/: the interface diffs are ast.Visibility and defs.Def gaining is_hardened (breaking, as any record field is), resolve.add taking it, and tokens.keywords gaining the word; the ledger delta is empty in all twelve modules snapshotted (the parser’s 1218 obligations, the printer’s 92, the lexer’s 311, unchanged). The suite under stage2: 451 passed, 3 skipped; the next sweep’s pinned answers gain hardened at the eleven item positions. Fixed point reached from bootstrap/, native stage agrees; promoted.

202. The manifest and the zones pass (M16; spec §21, impl spec §4 pass 12a; docs/CHANGE-LOG-03.md). self/toml.onus reads the subset of TOML the manifest uses (tables, quoted or bare keys, strings, one-line arrays, inline tables; anything else is an error naming the line). self/zones.onus is the pass: onus.toml at the project root gives every module its zone (an exact rule, else the longest prefix.* rule, else default, else draft; the standard library is critical), and the pass checks the dependency rule over every reference the resolver recorded — a node key decodes to its file and span (defs.key_file, key_span), so the report lands on the use — once per (module, definition), with the hardened items of draft modules as the one exception (E0900); the modifier’s placement, on a public item of a draft module only (E0902); the hardened bundle, a justification on every assumption (E0905); and the critical bundle: every public function on a path (E0903), every checked contract obligation exercised by the coverage ledger (E0904; the overflow and representation obligations of arithmetic are exempt, a narrowing recorded in §21.2), and on every path whose entry a critical module holds, recover forbidden (E0413), third-party assumptions forbidden unless the manifest’s [zones.exceptions] names them (E0415), and verification required (E0416, unless the path declares the policy itself and pass 12 reported it). A manifest that cannot be read is E0906. The pass runs after paths as pass 12 (--to zones, now the default of every command) and needs the files capability for the manifest. The reports: the interface document carries the module’s zone and each item’s zone and hardened (a hardened item of a draft module is held to hardened); the path report carries zone, zones_crossed, draft_dependencies and conditional (always false until item 203). Context gains zones and zone_exceptions. The fixture runner reads a manifest-level covers across sections, since each zone fixture is a project of its own. Fixtures under test/zones/: a zoned project that checks (ok_zoned: critical core.*, hardened svc depending on core and on the hardened payments.charge of a draft module), one per diagnostic, and ok_exception (the third-party assumption the manifest excepts). Every existing expectation is unchanged but the interface and path documents, which gain the fields. Review artefacts under .onus/changes/202/: the interface diffs are Context gaining project_root, zones and zone_exceptions (breaking, as a record field is), defs gaining key_file, key_tag and key_span (its ledger 8 → 26: 13 proved, 13 checked, the decoders’ arithmetic), interface gaining is_hardened and item_zone, cli gaining the pass name in usage and passes, and the runner’s diagnostics_dir and run_section taking the shared seen with coverage_of added; the ledger delta is empty in every snapshotted module; toml is new with 98 obligations (53 proved, 45 checked: the scanner’s index arithmetic) and zones with 24 (5 proved, 19 checked: the representation and overflow obligations of key decoding, ranks and the age in days). onus test, test --assumptions, test --mutate and the loop’s inner check stop at the paths pass, since the coverage and verification ledgers the critical bundle reads are what they write; check, build, run, interface, path, review and next run to zones. The suite under stage2: 470 passed, 3 skipped; the interface and path documents pinned by the cli cases gain the fields, and three cases pin that onus test clears E0904 and that the path report of a critical entry says so. Fixed point reached from bootstrap/, native stage agrees; promoted.

203. The zone commands, the promotions ledger and the zone-aware loop and review page (M16, done; spec §21.3–§21.5; loop spec §1, §3, §4.1, §5, §8; docs/CHANGE-LOG-03.md). onus zone show prints the manifest as the commands write it and the promotion history; onus zone promote <module> <zone> writes the candidate manifest under .onus/zone-candidate/, runs the pipeline over the module’s source with the candidate as the project’s manifest, refuses on any diagnostic (the target zone’s policy bundle, §21.2, is what the zones pass reports), and otherwise writes the manifest at the root, signed, and appends the promotion record to .onus/ledger/promotions.json (module, from, to, at, kind, audit); onus zone demote <module> <zone> writes and records without checking. The audit is the static half — “policies passed; regeneration skipped” — because the regeneration half of loop spec §8 needs a model, and a second model is not configurable in v0; it is deferred, not dropped. The signature is the BLAKE3 of the [zones] and [zones.exceptions] tables as zones.canonical_text serialises them (rules sorted by pattern, default last, exceptions sorted); a manifest whose signature does not match is E0901, and a manifest with no signature — written by hand before the first command, as the worked examples’ are — is accepted (§21.3, a note). Demotion: the zones pass reads the promotions ledger, and a dependency on a module whose latest record is a demotion is not E0900 but a conditional guarantee, recorded per dependent module (Context.conditional_on) and reported: the interface document’s conditional_on and each ledger row’s conditional, the path report’s conditional and conditional_on over every reachable module (§21.3, §21.5). The review page draws the zones of a path as regions around its nodes (draft regions dashed) and lists the promotion history beside the ledger, from the review data’s promotions. The loop (self/regen.onus) reads the zone of the target’s module from the baseline: the context policy’s default is scope in draft, module in hardened and none in critical when the task gives none (its context_policy is empty until resolved, then the change records the resolved one); in draft a model answer that changes the target’s signature is spliced, signature and body, and the change lists the item under loop_authored; in critical a stall does not walk the ladder — it would go to the frontier model, which is not configured, so the task is blocked with that message — and a widen_effects proposal is never emitted (loop spec §4.1); the change document carries zone. The worked examples are zoned: examples/checkout/onus.toml makes checkout and app.* hardened and vendor.* draft with the exception for vendor.payments.charge, and vendor/payments.onus marks Client, Error, Receipt and charge hardened; examples/reporting/onus.toml makes reporting and app.config hardened. The M16 acceptance is the cli-zones section of test/cli: the checkout project is tested (coverage), verified (--assumptions) and promoted module by module — app.contracts and app.auth reach critical (the promotion check loads every source under the root, since the paths that cover a module’s functions are declared wherever the project declares them), and checkout itself is refused with E0416, because its two structural assumptions (load_basket’s and record_order’s Idempotent) have no verify block and critical admits no unverified assumption, and with E0903, because recent_orders is public and on no path; the refusal is pinned, checkout stays hardened, its path report names vendor.payments.charge under draft_dependencies and crosses all three zones, and the review page draws the regions. Reaching the change log’s “checkout critical” needs verify blocks on those two assumptions, against a fake sql.Db in the example’s environment module, which is an edit to the worked example of §18.3 and is left for its author to decide; a promotion of a module with a public function on no path is refused with E0903; a signed manifest edited by hand is E0901; demoting app.config under reporting marks the reporting path conditional, and demoting core.math under svc in the zoned fixture project marks svc’s interface conditional with no E0900. Found by the zoned example and fixed: item 201 propagated the hardened modifier to the definitions of functions and records but not to claims, capabilities, unions, interfaces, constants and type aliases (resolve passed false for them), so checkout’s use of the hardened vendor.payments.Client was E0900; every item definition now carries its declaration’s modifier. A module that carries hardened items cannot itself be promoted — the modifier is E0902 outside draft — which is the rule working as written: the boundary is hardened first, the module later, once its modifiers are dropped. Fixtures: test/zones/e0901_edited_manifest, and svc in test/zones/ok_zoned gains a path so it can be promoted to critical. Review artefacts under .onus/changes/203/: the interface diffs are cli gaining zone_command, project_sources and manifest_or_empty with the usage text; ledger gaining the promotions reader and writer, promotion_json and demoted_modules, with Ledger carrying promotions; zones gaining the signature, the canonical text, write_manifest, set_zone and the conditional helpers, with Manifest carrying signature; review gaining the regions, the promotions view and its data; regen gaining target_zone and default_policy, with Run carrying zone and loop_authored; tables gaining PromotionRecord; Context gaining promotions, demoted and conditional_on. The ledger delta: cli 69 → 83 (10 proved, 4 checked added: the command’s indices and its budget), review 123 → 137 (14 checked: the regions’ coordinates), zones 24 → 28 (2 proved, 2 checked), the rest unchanged, nothing regressed. The suite under stage2: 492 passed, 3 skipped. Fixed point reached from bootstrap/, native stage agrees; promoted.

204. The regeneration half of onus zone promote, as an instrument (M16; spec §21.3, loop spec §8). With --model <spec> (the loop’s specs: claude-code, anthropic, openrouter[:<model>], scripted:<file>), promote runs, after the static check passes, a regenerate task over the module through regen.run_task: the module’s bodies are discarded and rebuilt from the interfaces alone (context_policy: none) and the change is written under .onus/changes/promote_<module>/. Decided 2026-09-07 with the spec author, and recorded in §21.3: the audit does not gate the promotion. What promotion rests on is what the compiler can check — the zone’s policy bundle, verified assumptions, exercised obligations — and the promotion record carries, for the reviewer, the module’s contract mutations from the ledger (“mutations: d detected, s surviving”) and the regeneration’s outcome: “passed in N iteration(s)”, “N finding(s)” (each printed), why it did not conclude (blocked, with the cause), or “skipped” without a model. The reasoning: regeneration measures how much of a module’s meaning is in its interface; our own compiler, whose specification is its fixture suite, would read low on it correctly, as would any module specified by its output, so a reading is a result and not a bar, and mutation testing is the cheaper twin of the same question. Fixtures: zone_promote_audit (the scripted model answers svc.bill correctly: “regeneration passed in 1 iteration(s)”) and zone_promote_audit_findings (a wrong answer: the run is blocked as a stall, the promotion still succeeds and the record says so). Found by the first of them: the loop took the target’s zone from the baseline’s context, whose check stops at the paths pass, so every module read as draft; it now reads the manifest itself (zones.read_manifest on the project root). The change document carries zone and the resolved context_policy (none for a regeneration), which the case pins. Found by the first real readings (docs/BENCHMARK.md, “The regeneration audit”): the audit filed an E0115 left by a body the model never produced as obligation_regressed, “the interfaces were sufficient to check the old body but not to reconstruct it”, which is not what happened; such a diagnostic is now the finding not_reconstructed, naming the function no usable body came back for, so a reviewer can tell the model’s silence from the interfaces’ insufficiency. Review artefacts under .onus/changes/204/: the interface diffs are cli gaining audited_regeneration, audit_of_change and mutation_summary with zone_command changed, and regen gaining manifest_or_empty with target_zone taking the files capability; the ledger delta is cli 83 → 90 (1 proved, 6 checked added: the iteration and mutation counts), regen unchanged, nothing regressed. The suite under stage2: 494 passed, 3 skipped. Fixed point reached from bootstrap/, native stage agrees; promoted.

205. The working tree is the loop’s state during a run (loop spec §9). The first honest-looking reading of the regeneration audit was not one: Claude Code, run as a subprocess in a directory where the original mandelbrot.onus still lay on disk, returned the three bodies byte-identical to the originals, variable names included (docs/BENCHMARK.md). The loop had elided the bodies only in memory. Now ask writes the working texts to their files before every model call — a model with a file system reads exactly what the prompt shows, elided bodies included — and conclude writes the texts the run started from back whenever it does not open a change (blocked, error, or --no-write), which is what “restoring the working tree when blocked” meant all along. The scripted-model cases pin that a blocked run leaves the file as found and an opened change writes it. It was not enough: with the elided tree on disk the subprocess read the repository’s own copy of the example instead (its main came back with the viewport, the image size and the PGM header, which no interface states), which item 206 answers by restricting the subprocess’s tools. Review artefacts under .onus/changes/205/: the interface diff is regen gaining write_working and restore_tree; the ledger delta is empty. The suite under stage2: 494 passed, 3 skipped. Fixed point reached from bootstrap/, native stage agrees; promoted.

206. The subprocess model reads nothing but the prompt (loop spec §9). Item 205 was necessary and not sufficient: Claude Code as a subprocess ran in the repository, where its read tools found the example’s original in examples/. Tried directly: in print mode Claude Code refuses to read outside its working directory, and --disallowedTools removes the tools altogether (--tools "" makes it write tool calls as text instead). So ClaudeCode carries a sandbox, <root>/.onus/model-sandbox, an empty directory model_from_spec creates, and generate changes into it before exec claude with Read, Glob, Grep, Bash, Task, WebFetch, WebSearch, Edit, Write and NotebookEdit disallowed; the prompt on stdin is all it has. The API models never had a file system. With it the first honest reading was taken (docs/BENCHMARK.md): Claude Code reconstructed mandelbrot green in two answers, render the same computation refactored and main a different program — an ASCII rendering to a text file where the original writes an 800×600 PGM — with no finding, since nothing in main’s interface states what it writes; loop spec §8’s third finding, “green but different”, is the one to build next. Review artefacts under .onus/changes/206/: the interface diff is regen.Model’s ClaudeCode variant gaining sandbox (breaking); the ledger delta is one index refinement proved more. The suite under stage2: 494 passed, 3 skipped. Fixed point reached from bootstrap/, native stage agrees; promoted.

207. The finding “green but different” (loop spec §8; spec §11.1). Loop spec §8’s third finding was not reported in v0 (item 115), and the first honest regeneration showed why it is the one that matters: mandelbrot’s main came back as a different program with a green ledger. Now, when a regeneration checks clean, the audit compares each target’s body with the one it replaced — the functions it calls (every resolved reference inside the body that names a function), the effects it uses (the effects pass’s inference) and the literal constants it writes (as the printer prints them) — and a difference is the finding green_but_different, naming the function and what was added or removed, proposed as add_example. The comparison lives in interface as callees_of, effects_used and constants_of, and the interface document’s function items carry callees so the interface diff reports callees added and removed (compatible, never breaking) and the review page’s diff view shows them for any loop change. Fixture: zone_promote_audit_different in test/cli, the scripted model regenerating svc.bill as payments.charge(pence: x) + payments.charge(pence: x) — green, and no longer calling core.math.double — which the promotion record reports as one finding. With it the reading of docs/BENCHMARK.md was taken again: main is flagged for the callees and constants that changed, escape_count for one literal a refactor no longer writes — the noise a constants comparison carries, and the decisive signal on main. Review artefacts under .onus/changes/207/: the interface diffs are regen gaining different_findings, target_finding, def_named, shape_difference and push_difference with audit taking the targets, interface gaining the twelve callee, constant and effect helpers, and idiff.ItemChange gaining callees_added and callees_removed (breaking, as a record field is); the ledger delta is interface 61 → 67 and regen 219 → 223 (ten checked obligations added: the helpers’ index arithmetic), nothing regressed. The suite under stage2: 495 passed, 3 skipped; every pinned interface document gains callees. Fixed point reached from bootstrap/, native stage agrees; promoted.

208. Views and the DOM capability (M17; spec §22; docs/CHANGE-LOG-04.md). std/dom.onus: the capability Root granting dom.read, dom.write and dom.event, and subtree; std/view.onus: the immutable tree View[Msg] (Element, Text, Keyed) and Attr[Msg] (Attribute, On carrying a message, Property) over the closed vocabularies Tag, AttrName, PropName and EventKind, the constructors, the spellings, descendants, the predicates (is_element, has_handler, attribute_of, has_label, is_interactive), the accessibility conditions (buttons_have_handlers, inputs_have_labels, images_have_alt, no_nested_interactive, together accessible) and claim accessible; the intrinsics patch and run, both claiming host.js. The JavaScript runtime’s dom.ts implements them against globalThis.document — a browser’s, or a fake a test supplies: patch diffs two trees and applies the minimal mutations (keyed children by key, unkeyed positionally, attributes, properties and listeners reconciled), run renders and on every message updates and re-renders, installed on the host’s loop and returning at once. dom.Root is a root capability of main (§8.3) on the JavaScript target, supplied as the document’s body; the native emitter refuses a main that takes one with E0800. Three deviations from the change log, each marked in §22: the element’s field is element, not tag, since a union’s discriminant is tag in the JavaScript representation; run has no diverge effect, since it installs the loop and returns; and the accessibility properties use predicate functions rather than v is Element(tag: Button, ..), since patterns with field values are not in the grammar (deferred). The variant Input of EventKind is Edited and Option of Tag is OptionItem, since a module’s variants share one namespace. The milestone is M17 in the implementation spec (the change log said M15). Fixtures: test/paths/e0413_dom_write (a view function that patches the document itself, under forbid { dom.write }) and test/paths/ok_view_pure (a path from a view function forbidding every dom effect); test/stdlib/view_ops (the spellings, the predicates, the conditions and descendants as examples, keyed lists accessible as a property); test/native/e0800_dom_root; the counter in test/examples and, in test/codegen, run from the JavaScript target against the fake document fake_dom.mjs (via fake_dom.sh), the tree after each click pinned in counter_dom.out. Review artefacts under .onus/changes/208/: interface diffs of capabilities, lowerir, native (and, unchanged, ir, build, nativebuild, jsemit, codes), ledger.md; no obligation of self/ changed status. Fixed point reached from bootstrap/, native stage agrees; promoted.

209. std.view for documents: the vocabulary, to_html, no style attribute (spec §22.2, §22.6). Preparing the review page to be a view (docs/CHANGE-LOG-04.md, M10): Tag gains H4, H5, Article, Details, Summary, Em, Strong, Small, Br and the inline SVG subset Svg, G, Rect, Path, Line, Circle, SvgText; AttrName gains Open, Hidden, Colspan, the geometry Width, Height, X, Y, Rx, D, Transform, ViewBox and the hooks DataId, DataModule, DataItem, DataView, DataStatus; EventKind gains Toggle; the constructor prop joins attr and on. is_svg, is_void and is_boolean describe the vocabulary; std.html (escape, to_html) writes a tree as HTML text (handlers unwritten, boolean attributes bare, void elements unclosed, a depth beyond 64 cut), so the function that describes a live view also pre-renders a static page. The style attribute of item 208 is removed: §22.6 lists inline styles as strings among what is absent, and nothing used it. The runtime creates the SVG elements in their namespace when the document offers createElementNS; the fake document of the counter fixture offers it. Fixtures: test/stdlib/view_ops (the new spellings, to_html over nesting, escaping, a keyed child, a boolean attribute, a void element and a handler). No compiler module changed; review artefacts under .onus/changes/209/: the interface documents of std.view and std.html after the change and README.md listing the delta, since change-review.mjs covers self/ only. Fixed point reached from bootstrap/, native stage agrees; promoted.

210. The workbench in Onus (M10 redefined; spec §15, §22; docs/CHANGE-LOG-04.md). self/workbench.onus is the review page as a program against std.view: State (the review bundle, the view shown, the ledger filter, the bodies opened), the closed Msg (Show, Filter, Toggled), update, and page, a pure function of the state returning the tree — the graph layout and every view of item 86 ported from text to View values, one function per part. main(args, root) parses the bundle from its argument and hands the three to view.run. self/review.onus keeps the data assembly and writes the shell: the stylesheet, the page pre-rendered through std.html.to_html from the same function, the bundle as a JSON script, and a module script that boots main; the hand-written view switcher, filter and counter are gone. scripts/bundle.mjs builds the workbench with stage0 and carries its JavaScript under workbench/; onus review writes it beside the page with the runtime, so the directory is the live page. The view parameter of std.view.run admits mutate (§22.3): a tree of any size is built with builders. The module is in the draft zone (no manifest names it). Fixtures: the review cases of test/cli re-pinned from the view with the program’s files expected, and workbench_dom (a script case): the live page under the fake document switches views, filters the ledger and counts an opened body. Review artefacts under .onus/changes/210/: the interface diffs of review (the renderers removed, render_page kept) and cli (unchanged surface), the interface of the new workbench, ledger.md; no obligation of self/ changed status, and every obligation of workbench is proved or checked under stage0. Fixed point reached from bootstrap/, native stage agrees; promoted.

Deferred, not changed

• Decided 2026-09-06, to apply in M15.5: generics compile natively by monomorphisation (impl spec §6.1). The rule it needs, polymorphic recursion as a checker error, is item 171 (applied the same day).

• Noted 2026-09-06, not scheduled: definitional unfolding of proved-terminating functions in the verifier (impl spec §12), so that a shape invariant stated as a recursive predicate can be proved where a nested type would have enforced it.

• Stream[T] ! e as a type (§3.11) is not parsed: -> Stream[T] ! e is ambiguous between the stream’s effect and the function’s. To be settled when streams land.

• Multi-binder quantifiers and tuple comparisons in §4.1 (forall px: Int, py: Int where (px, py) != (x, y)) are not in the grammar; nested quantifiers (§5.3 allows depth two) express the same thing.

• budget annotations (§12.3) and proves float (§3.2) have no syntax yet.

• Generated tests import vitest and fast-check by name and resolve them from the nearest node_modules; a project outside this repository needs both installed.