3As of 2026-11-03. This file lists what Jibb does now, whether each part is done, partial or missing, and the test or check that proves it, then the known gaps. History is in git (`git log --oneline`). The plan is [spec/implementation-plan.md](spec/implementation-plan.md), and each milestone ends with its checks passing on a fake ship.
7| # | Milestone | Status |
9| 1 | Parser and mark | Done (7c739b7; the doc's grammar decisions of 2026-10-30 in ab797a9) |
10| 2 | Types and prelude | In progress: the checker and the Hoon importer are partial. [prompts/milestone-2.md](prompts/milestone-2.md) briefs it. The [milestone 2 review](reviews/2026-11-03-milestone-2-review.md) of 2026-11-03 lists what the done-criteria still need, briefed in [prompts/milestone-2-finish.md](prompts/milestone-2-finish.md) |
11| 3 | Core language | Not started |
12| 4 | Host and static pages: the first release | Not started |
13| 5 | Published pages | Not started |
14| 6 | Islands | Not started |
15| 7 | Tooling | Not started |
16| 8 | Polish | Not started |
18The plan sets no dates ("agree them after milestone 1, once it shows how fast the Hoon work goes"), and none have been agreed yet. Milestone 1's commits ran from 2026-10-29 18:13 to 2026-10-30 11:50 UTC.
20Decisions the Claude doc does not have yet, such as dropping `$?` ([prompts/drop-union-rune.md](prompts/drop-union-rune.md)), explicit `proj`, the `like` gate and backtick units, are rows of [spec/decisions.md](spec/decisions.md) whose Synced column says No (rows of 2026-10-30 say Check: nobody has compared them yet). The parser already follows the `$?` decision. Until the doc is synced, the repository copy wins.
24- Done: works as the row says, and the linked test or check proves it. Partial: works for the shapes named, and the words after the colon say what is left out or unproved. Missing: not implemented, or rejected on purpose; the link shows the current failure where a test pins it.
25- Suite names link to `tests/lib/<suite>.hoon`, and case names to `tests/golden/<case>/`; a name with `*` stands for every case it matches. Every suite runs under `urbit eval` and on the fake ship.
26- The checker has two entry points, and they can disagree. The full-module check, in its detailed and legacy forms, decides whether a module checks, and "checks" in this file means it. The partial inference report, which all 304 golden `types.txt` files print, starts "partial inference; module not checked" and declines more. For example, its report on the cart store leaves the store's kind and scope unresolved ([doc-grammar-06-cart-store](../tests/golden/doc-grammar-06-cart-store/)) and its report on the Grammar's buttons example says only "tag needs context" ([doc-grammar-02-buttons](../tests/golden/doc-grammar-02-buttons/)), while the full check passes the cart store ([jibb-store](../tests/lib/jibb-store.hoon)) and reports the buttons error exactly ([jibb-buttons](../tests/lib/jibb-buttons.hoon)).
30These rows cover milestone 1. The plan's three done-when criteria are the rows on the doc examples, the lexical rules and `|commit`.
32| Area | Status | Proved by |
34| The `%jibb` mark: grab `mime`, `noun` and `txt`, grow `mime`, `txt` and `noun`, grad `%txt` | Done | [jibb-dev/mar/jibb.hoon](../jibb-dev/mar/jibb.hoon), `tools/ship check-commit` |
35| `\|commit` stores `.jibb` files on a fake ship: 7 checks, from reading every `/ui` file back byte for byte to three-way merges and conflicts | Done | `tools/ship check-commit` |
36| Layout pass: `+layout` (library section 2) emits INDENT, DEDENT and NEWLINE | Done | `lex-layout-*`, `lex-indent-*`, `lex-rune-layout-*` |
37| Lexical rules: for each rule, inputs that break it, with the error's expected place, and inputs that keep it | Done: 148 `-bad-` and 57 `-ok-` cases; the left-out closers, blob and `@c` literals have only `-bad-` cases, and so does `lex-char` | `lex-*` |
38| Parser: `+parse` and `+parse-tokens` (library section 3) turn the Grammar tab's EBNF into a syntax tree | Done | every golden `tree.txt` |
39| Unions without `$?`: a `+$` takes its cases on the lines below, and `$?` is an error | Done | [inline-union-wide](../tests/golden/inline-union-wide/), [inline-union-one-case](../tests/golden/inline-union-one-case/), `inline-hoon-union-*` |
40| Spans: every node keeps its start and end, and `+golden` appends `SPAN ERROR` when `+check-spans` fails | Done | [jibb-check-spans](../tests/lib/jibb-check-spans.hoon), `tools/golden` |
41| Parse errors: file, line, column, message, excerpt and caret (`+show-error`), at the first character where the text stops being the start of any valid module (library section 2.0) | Done: each failing case's `about.txt` states the position, except the unclear case below | `lex-*-bad-*`, `inline-*-bad` |
42| Underlining with span ends | Partial: parse errors give a start only, and type errors name both sites with excerpts but mark each with one caret at its start | [jibb-check-spans](../tests/lib/jibb-check-spans.hoon), [types-multi-call](../tests/golden/types-multi-call/) |
43| Type holes: `_` in mold positions and typed path segments (`[id=_]`), each with its own span; `_` stays a literal knot in `/_` and `%/_` | Done: holes in parameters, patterns and values are rejected | `parser-hole-*`, `types-hole-*` |
44| Doc examples: the 14 `jibb` blocks in [spec/](spec/) (6 in grammar.md, 7 in overview.md, 1 in core-language.md) are golden cases, and all parse | Done | `doc-*`, `tools/doc-blocks docs/spec` |
45| Golden corpus: 691 cases, 462 that parse and 229 that fail, each failure pinned to a line and column | Partial: eight `types-*` cases have no `expect:` line in their `about.txt`, which [development.md](development.md#golden-cases) asks for | `tools/golden` |
46| The expected result of [inline-leftout-signed-float-auras](../tests/golden/inline-leftout-signed-float-auras/) | Partial: its `about.txt` says "expect: unclear" (grammar question 13); the outputs pin the layout pass's error at 1:7 | [inline-leftout-signed-float-auras](../tests/golden/inline-leftout-signed-float-auras/) |
47| The 13 grammar questions never put to the doc's author | Partial: the parser follows provisional readings, listed in [open-questions.md](open-questions.md#grammar-questions-never-put-to-the-docs-author) | [inline-import-root-bad](../tests/golden/inline-import-root-bad/), [lex-indent-bad-3](../tests/golden/lex-indent-bad-3/) and others |
48| Forms the parser leaves to the checker: `!! a`, the module kinds and an empty change `m()` | Partial: the partial checker reports an empty change ("a change takes at least one field") | [inline-crash-call](../tests/golden/inline-crash-call/), [inline-kinds](../tests/golden/inline-kinds/), [types-record-change](../tests/golden/types-record-change/) |
49| `[]` as an error and `[a]` as `a`, as [spec/decisions.md](spec/decisions.md) decides (Cells) | Partial: the checker types `[a]` as `a`, but `[]` parses and the checker calls it unsupported, not an error; no case writes `[]` | [lex-tight-opener-bad-1](../tests/golden/lex-tight-opener-bad-1/) |
50| Long and deeply nested input | Partial: library section 3 records 100,000 nested brackets and a 20,000-line module parsing, but no case, suite or check exercises them | none |
52Two independent audits came before 7c739b7: one compared the library with a reference parser written in Python from the doc, over about 19,000 generated programs. Before ab797a9, a second Python parser, written from the decisions, agreed with the library on 8,000 generated programs and 900 hand-written probes. Neither audit's code nor its results are in the repository.
54## Types and prelude: full-module checks
56| Area | Status | Proved by |
58| Program `main`: a direct four-wing `(program init update view subs)`, closed and matching the canonical `program` mold invariantly | Done: generic mains, open messages, mismatched models, arbitrary mains, store paths and an aliased `program` are rejected | [jibb-program-main](../tests/lib/jibb-program-main.hoon), [type-program-main/source.txt](../tests/type-program-main/source.txt) |
59| Initializer data and model: closed and gate-free, with `%yes` verdicts inside one shared 256-node budget | Done: a gate in the model or the data is rejected; no test exhausts the shared budget | [jibb-program-main](../tests/lib/jibb-program-main.hoon), [jibb-gate-free-guards](../tests/lib/jibb-gate-free-guards.hoon) |
60| Initializer recovery: with update, view and subs resolved, a direct initializer is inferred against the model, then `main` is inferred again | Done: also when update's sample is a faced mold, a pun, a named mold or generic in the model, and with generic view and subs samples; the recovered model must be closed and tag-free | [jibb-program-init](../tests/lib/jibb-program-init.hoon), [type-program-main/initializer-unfaced.txt](../tests/type-program-main/initializer-unfaced.txt) |
61| Recovery boundaries: non-main sources, init and subs unresolved together, unrelated pending tags, a `program` alias, a main that is not a program | Partial: all rejected in detailed and legacy checks; no fixture tries an aliased initializer (`++ init other`) | [jibb-program-init](../tests/lib/jibb-program-init.hoon), [jibb-program-main](../tests/lib/jibb-program-main.hoon) |
62| Update recovery: an unannotated two-slot update takes its result type from the program, through a union and a loobean branch | Done: a wrong result, model or message, a malformed or three-slot sample, a non-main source, an unrelated tag, a missing `cmd` or `list`, and API and store paths are rejected | [jibb-program-update](../tests/lib/jibb-program-update.hoon) |
63| Program `subs`: null, or one unfaced `[%watch (case.face \|=%callback)]` whose request has the exact derived scheme and matches the API's path, case names and source, with no scry, diffs or parameters | Done | [jibb-program-watch](../tests/lib/jibb-program-watch.hoon), [jibb-program-main](../tests/lib/jibb-program-main.hoon) |
64| Other watches: pure or hand-built requests, helpers, aliases, typed paths, diff folds, several watches, unknown or ambiguous evidence | Missing: all rejected, but only unknown or ambiguous evidence by decision (settled question 33 in [spec/decisions.md](spec/decisions.md)); re-exports have no test | [jibb-program-watch](../tests/lib/jibb-program-watch.hoon) |
65| Program interfaces keep their source evidence and work in downstream imports | Done | [jibb-program-main](../tests/lib/jibb-program-main.hoon), [jibb-program-watch](../tests/lib/jibb-program-watch.hoon), [jibb-todo-full](../tests/lib/jibb-todo-full.hoon) |
66| The unchanged todo island: exact closed `main`, a cast-initializer variant and a structural downstream import | Done: wrong model, message, result, mapper, key, alias, watch and non-gate view are rejected | [jibb-todo-full](../tests/lib/jibb-todo-full.hoon), [type-todo-full/cast-init.txt](../tests/type-todo-full/cast-init.txt) |
67| Component-local recovery of update, subs, one keyed `each`/`turn` mapper and view, before init and `main` | Partial: fresh allocation and the `element` and singleton-list guards are not asserted separately | [jibb-todo-full](../tests/lib/jibb-todo-full.hoon) |
68| The partial report on the todo island, with its real API and readers | Done: missing or duplicate marks and a missing `/sur` are rejected; the report still declines `main`, init, update, subs, view and row-of | [jibb-todo-partial](../tests/lib/jibb-todo-partial.hoon), [type-todo-partial/expected.txt](../tests/type-todo-partial/expected.txt) |
69| Pages: the unchanged about page, blog index and index page, with exact `main` types and downstream imports; the about page is `(element !!)` | Done | [jibb-page-main](../tests/lib/jibb-page-main.hoon) |
70| Page loads, through the same derived-request identity check as program watches | Done: builder aliases, indirect, pure, hand-built and unknown requests, typed paths, diffs and store paths are rejected; no test puts a request alias in a load | [jibb-page-main](../tests/lib/jibb-page-main.hoon) |
71| Stores: the unchanged cart store and basket, as direct two-wing mains with exact schemes and structural imports | Done: wrong init, action or result, name collisions, aliases and forged evidence are rejected; state holding gates is accepted | [jibb-store](../tests/lib/jibb-store.hoon) |
72| Store exports: state and action molds, a derived generic `poke` command helper returning `(cmd M)`, and state requests | Done: a noncanonical `cmd`, `unit` or `raw-poke` is rejected | [jibb-store](../tests/lib/jibb-store.hoon) |
73| Store watchability: source-bound store evidence, merged into the basket's graph | Partial: indirect state requests and a store state used as a page load are rejected | [jibb-store](../tests/lib/jibb-store.hoon), [jibb-api-evidence](../tests/lib/jibb-api-evidence.hoon) |
74| Store scope: a definite duplicate `+$ poke` or unrelated prelude shadowing | Partial: reported as a conflict; a possible root API's `poke` is left unchecked, and no test asserts the "module kind or scope" message | [jibb-store](../tests/lib/jibb-store.hoon), [types-scope-store-duplicate](../tests/golden/types-scope-store-duplicate/), [types-scope-store-shadow](../tests/golden/types-scope-store-shadow/), [types-scope-root-api](../tests/golden/types-scope-root-api/) |
75| Theme: the real `my-app/ui/theme.jibb`, with backtick units, against the prelude's `theme` | Done: absent dark tones check; a wrong nested aura, a missing field and a wrong font or dark type are rejected | [jibb-theme](../tests/lib/jibb-theme.hoon), [doc-overview-02-theme](../tests/golden/doc-overview-02-theme/) |
76| Buttons: `labelled` and `wide` with exact generic schemes, and the unchanged module's "nothing fixes the union of %add" at 3:16 with its excerpt | Done: the retry that finds the tag runs only on an incomplete module, and its fuel of 64 counts every definition visited | [jibb-buttons](../tests/lib/jibb-buttons.hoon), [type-buttons/error.txt](../tests/type-buttons/error.txt) |
77| Doc fragments: the import-only module (real `/sur`, mark and Jibb module), `view-day`, `step` (`describe: $-(step @t)`) and the `cmd`/`sub` block at the prelude path | Done: missing `/sur`, mark or module inputs are rejected | [jibb-doc-examples](../tests/lib/jibb-doc-examples.hoon) |
78| Generic-alias unions: a bounded local source proof of cases with different literal heads, then the ordinary mold checks | Done: the full check accepts the module, though its partial report says "mold not checked" | [jibb-union-source](../tests/lib/jibb-union-source.hoon), [type-union-source/good.txt](../tests/type-union-source/good.txt) |
79| Generic-alias unions through nested or qualified aliases, structured or pending states, recursive-index states or the deferred transaction | Missing: declined | [jibb-union-source](../tests/lib/jibb-union-source.hoon) |
80| Generic-alias overlaps: a bounded witness reports proven collisions with both case sites, and the module stays rejected | Done: unknown or opaque payload intersections, wrong arity, duplicate and qualified owners and short fuel decline | [jibb-union-alias-overlap](../tests/lib/jibb-union-alias-overlap.hoon), [jibb-full-overlap-basic](../tests/lib/jibb-full-overlap-basic.hoon), [jibb-full-overlap-graph](../tests/lib/jibb-full-overlap-graph.hoon) |
81| Full-module overlap evidence: the first failing mold's source-bound evidence, through imports, with both excerpts in the legacy text | Partial: not on the specialized API and prelude paths | [jibb-full-overlap-basic](../tests/lib/jibb-full-overlap-basic.hoon), [jibb-full-overlap-graph](../tests/lib/jibb-full-overlap-graph.hoon) |
82| Complete private module checking, other API shapes, root API and kind checking, complete `ask` and `pure` checking | Missing | none |
84## Types and prelude: requests and API analysis
86| Area | Status | Proved by |
88| API paths: supported path declarations and their full and diff mark types, including the todo paths | Done: unknown scry parameters, bad marks, a wrong path, a missing prelude, private imports and cycles fail closed; it creates no requests | [jibb-api-paths](../tests/lib/jibb-api-paths.hoon), [type-api-paths/expected.txt](../tests/type-api-paths/expected.txt) |
89| Path evidence: source, prepared prelude, reader graphs and dependencies; a unique declaration is watchable, not watchable (scry) or unknown | Partial: declaration evidence only, not proof about a request value | [jibb-api-evidence](../tests/lib/jibb-api-evidence.hoon) |
90| Request parts: ordered typed parameters, a full-state reply sample and a one-diff fold | Done: several diffs, a missing or duplicate case, missing evidence and unknown auras fail closed | [jibb-api-evidence](../tests/lib/jibb-api-evidence.hoon) |
91| Supporting definitions: ordinary API molds and values, and every declared mark with its source and mark-graph evidence | Partial: unused `/-` cores are not validated, dependence on derived gates is unsupported (noted only in code), and the whole API is neither checked nor exported | [jibb-api-evidence](../tests/lib/jibb-api-evidence.hoon) |
92| Request gates through ordinary imports: several API paths, one typed segment before the reply or one diff fold after it; the todo's plain, typed and diff requests, including a named closed fold | Done | [jibb-todo-api](../tests/lib/jibb-todo-api.hoon), [jibb-request-guards](../tests/lib/jibb-request-guards.hoon), [types-request-normal](../tests/golden/types-request-normal/) |
93| Request gates for Jibb module imports in an API, scry paths, two or more parameters or diffs, a parameter with a fold | Missing: only two parameters and two diffs are tested; the rest is rejected in code (`api-request-gates`, `multi-request-interface-graph`) | [module-import-api-request-reason](../tests/golden/module-import-api-request-reason/), [type-todo-api/unsupported.txt](../tests/type-todo-api/unsupported.txt) |
94| Request evidence through diamond and transitive imports and cached interfaces | Done: changed sources, stale caches and duplicates fail closed or rebuild | [jibb-request-guards](../tests/lib/jibb-request-guards.hoon) |
95| API exports: the real todo API's checked definitions, mark molds and derived poke and request members, with a request certificate | Partial: unselected `/sur` bindings are not validated | [jibb-todo-api](../tests/lib/jibb-todo-api.hoon), [jibb-poke-bridge](../tests/lib/jibb-poke-bridge.hoon) |
96| API poke export: one mark and a matching direct `+$ poke` give a `(cmd ...)` constructor with agent and mark metadata | Partial: one mark only; wrong payloads, marks and cases are rejected | [jibb-poke-bridge](../tests/lib/jibb-poke-bridge.hoon), `module-import-api-poke-*` |
97| The todo's `subs` with an explicit type: `~[[%watch (todos.api \|=%got)]]` infers `(list (sub msg))` | Done | [jibb-todo-api](../tests/lib/jibb-todo-api.hoon), [jibb-todo-full](../tests/lib/jibb-todo-full.hoon) |
98| A todo request under explicit `(ask msg)` context infers `\|=%got` and reports an absent tag | Partial: without context, the full check accepts it in the todo's `main`, but the partial report does not | [jibb-program-watch](../tests/lib/jibb-program-watch.hoon), [jibb-todo-full](../tests/lib/jibb-todo-full.hoon), [type-todo-partial/expected.txt](../tests/type-todo-partial/expected.txt) |
99| Gate-free analysis of one named mold: gate-free, a gate with its field path, or unknown | Partial: capped at 256 nodes; API, store and private roots are rejected, and it checks no module or island and proves no watchability | [jibb-gate-free-source](../tests/lib/jibb-gate-free-source.hoon), [jibb-gate-free-guards](../tests/lib/jibb-gate-free-guards.hoon) |
100| Request lowering, checked decoding, runtime validation, general island watch checking | Missing: only the direct program watch and page loads are proved | none |
101| `ask` receivers for agents and stores | Missing: they take raw nouns (`state=(unit *)`, `fact=*`), so they prove no schema validity or watchability | [internal.jibb](../jibb-dev/lib/jibb/internal.jibb) |
103## Types and prelude: checker
105### Atoms, literals, holes and capitals
107| Area | Status | Proved by |
109| Unification: the library's own `+itype-unify-test` cases | Done | [jibb-typecheck](../tests/lib/jibb-typecheck.hoon) |
110| Atoms: `@`, one-way widening to aura-family parents, branch widening to a present parent, atom constraints from capitals or bare binders | Partial: generic joins needing a common-type rule are unsupported | [types-partial-atom-widening](../tests/golden/types-partial-atom-widening/), [types-partial-aura-family](../tests/golden/types-partial-aura-family/), [types-partial-branch-widening](../tests/golden/types-partial-branch-widening/), [types-partial-bare-atom](../tests/golden/types-partial-bare-atom/), [types-partial-many-atom-constraints](../tests/golden/types-partial-many-atom-constraints/) |
111| Decimal defaulting: unfixed decimals become `@ud` in gate-free types, including tuples and polymorphic calls | Partial: gate types still report "unresolved aura-variable inference" | [types-partial-decimal-default](../tests/golden/types-partial-decimal-default/) |
112| Literal heads: `%$` matches null-, loobean-zero- and term-zero-headed cases, and equal heads with disjoint payloads select a unique case | Partial: overlapping same-noun cases decline | [types-literal-constructor-nouns](../tests/golden/types-literal-constructor-nouns/), [types-equal-head-disjoint](../tests/golden/types-equal-head-disjoint/), [types-loobean-singleton-source](../tests/golden/types-loobean-singleton-source/) |
113| String interpolation: known auras, `@`, tapes and isolated decimals; a known cell asks for a printer, a generic atom for an aura | Partial: a gate or non-tape list, which the Grammar makes a printer error, pending tags, generic or unknown types and a type fixed only later are unsupported | [types-string-interpolation](../tests/golden/types-string-interpolation/) |
114| Annotation holes: each value or local definition resolves its own `_` before generalization, and later uses cannot repair it | Done: independent decimal holes default to `@ud`, captured and written-capital variables don't, and structural named molds report the hole's site | `types-hole-*`, [jibb-hole-guards](../tests/lib/jibb-hole-guards.hoon) |
115| Holes in complex molds (`(list _)`), mutual recursive groups and inferred path segments | Missing: the first two fail closed; path-segment holes are only parsed and have no type test | [types-hole-named-complex](../tests/golden/types-hole-named-complex/), [types-hole-local-boundary](../tests/golden/types-hole-local-boundary/), [types-hole-unbound-mold](../tests/golden/types-hole-unbound-mold/), [parser-hole-path](../tests/golden/parser-hole-path/) |
116| Written capitals: collected per `++`, shared with locals even when written later, generalized locally otherwise, independent across siblings | Done | [types-local-capitals](../tests/golden/types-local-capitals/), [types-generic-local-parameter](../tests/golden/types-generic-local-parameter/) |
117| Forcing two distinct written capitals equal, by a call or a cast | Done: both sites are reported; forcing one to a concrete type is unsupported | [types-capital-distinct](../tests/golden/types-capital-distinct/), [types-multi-call](../tests/golden/types-multi-call/) |
118| Empty types: `!!`, proven-empty cell positions and union cases; empty list or unit payload arms are rejected | Done: opaque reachability and spent budgets decline | [jibb-empty](../tests/lib/jibb-empty.hoon) |
120### Records, lists and units
122| Area | Status | Proved by |
124| Duplicate field names in a written record, including nested records, samples and expressions | Done: both sites are shown | [types-record-field-nested-mold](../tests/golden/types-record-field-nested-mold/), [types-record-field-expr-duplicate](../tests/golden/types-record-field-expr-duplicate/), [types-record-field-sample-duplicate](../tests/golden/types-record-field-sample-duplicate/) |
125| Acyclic local definitions with captures, simple and nonrecursive generic mold aliases, faced record casts and field reads | Partial: selected shapes only | `types-local-*`, `types-generic-*`, `types-record-*` |
126| Record changes: uniquely named fields, nested wings, field context for replacements | Done: unknown or partly unfaced spines are unsupported, and mismatches point at the edit, not the field's declaration | [types-record-change](../tests/golden/types-record-change/) |
127| Record initializers under a known record cast, including nested list and union fields | Partial: mismatches point at the cast mold | [types-record-cast-context](../tests/golden/types-record-cast-context/) |
128| A value of type variable `A` in a field typed `A`, including union payloads and nested or repeated fields | Partial: faces of differing variables don't merge | [types-generic-face-inference](../tests/golden/types-generic-face-inference/) |
129| `proj`: explicit `(proj record)` with a known closed record type, keeping field-axis evidence for lowering; `proj` is reserved in definitions, samples, patterns and imports | Partial: same-order fields only; no context, a bare or aliased `proj` and the wrong arity fail closed | [jibb-proj-guards](../tests/lib/jibb-proj-guards.hoon), `types-proj-*` |
130| `proj` with reordered fields or in nested unit, list or call contexts; `proj` lowering and execution | Missing: field order is open (question 32 in [open-questions.md](open-questions.md)) | [types-proj-explicit-context](../tests/golden/types-proj-explicit-context/), [types-proj-nested-no-implicit](../tests/golden/types-proj-nested-no-implicit/) |
131| List literals without context, empty and nested, generalized independently | Partial: unresolved item tags and uncertain widening fail closed | [types-list-open](../tests/golden/types-list-open/), [types-list-open-constraints](../tests/golden/types-list-open-constraints/) |
132| List literals with the validated prelude list and a known cast or sample: empty, nonempty, nested and cons, contextual tags, imported-list contexts | Done: a bad element, head or tail names both sites | [types-list-context](../tests/golden/types-list-context/), [types-list-cons](../tests/golden/types-list-cons/), [types-list-imported](../tests/golden/types-list-imported/), [types-list-zero-fit](../tests/golden/types-list-zero-fit/) |
133| Gate sample context for one tuple or record argument, including nested cells and empty lists | Partial: a bound zero constant is unsupported, an unknown callee gives no context, and faced or three-item cons cells fail closed | [types-tuple-context](../tests/golden/types-tuple-context/), [types-list-zero-fit](../tests/golden/types-list-zero-fit/), [types-list-cons](../tests/golden/types-list-cons/) |
134| List branches: a known list result gives context through complete loobean, unit-shaped and list-shaped branches, and `~` / `[item rest]` infers element and tail in either order | Done: unknown or non-list subjects, sets and incomplete patterns are unsupported | [types-list-branch](../tests/golden/types-list-branch/), [types-list-patterns](../tests/golden/types-list-patterns/), [types-list-pattern-imported](../tests/golden/types-list-pattern-imported/) |
135| Unit construction with backticks, `some`, and `bind`, `biff`, `both`, `clap`, `clef` and `flit` under result annotations | Done: an unrelated union in unit context, a forced capital and an incompatible `clef` gate are unsupported | [types-unit-construction](../tests/golden/types-unit-construction/), [types-prelude-unit-helpers](../tests/golden/types-prelude-unit-helpers/) |
136| Unit context: a known unit in a cast, call, list item or record field gives its payload context | Partial: unrelated union identities, some variable-dependent fits and a missing or altered unit template are unsupported | [types-unit-context](../tests/golden/types-unit-context/) |
137| Nulls stay pending until resolved, and a known `~` / null-headed-cell union takes a complete `~` / `[~ value]` branch in either order | Partial: unknown subjects, missing or duplicate arms and unresolved results are not accepted | `types-null-*`, [types-unit-patterns](../tests/golden/types-unit-patterns/) |
138| Loobean result context through complete list, unit and binder-only cell branches | Partial: binder-only arms over union subjects are unsupported | [types-flag-branch-context](../tests/golden/types-flag-branch-context/) |
140### Unions and patterns
142| Area | Status | Proved by |
144| Contextual tags, `~` and constructors for closed disjoint and direct nonrecursive generic unions, through complete and nested loobean branches | Partial: no test carries union context through a unit-shaped `~` / `[~ x]` branch | [types-union-tags](../tests/golden/types-union-tags/), [types-union-context-flow](../tests/golden/types-union-context-flow/), [types-union-branch-context](../tests/golden/types-union-branch-context/), [types-generic-union-local](../tests/golden/types-generic-union-local/), [types-nested-union-context](../tests/golden/types-nested-union-context/) |
145| Result context: a known result type, including a same-origin generic union, reaches a call before its arguments are inferred | Partial: unknown targets and calls stay unsupported; wrong payloads and proven missing tags report errors | [types-constructor-context](../tests/golden/types-constructor-context/), [types-generic-result-context](../tests/golden/types-generic-result-context/), [jibb-constructor-fit-guards](../tests/lib/jibb-constructor-fit-guards.hoon) |
146| Tuple payload context: a two-item literal-headed tuple whose payload is a shallow call, from a known union of uniquely headed cells | Partial: inference that already fits wins; the path has no complexity bound | [types-nested-union-context](../tests/golden/types-nested-union-context/), [types-nested-noun-context](../tests/golden/types-nested-noun-context/), [types-nested-shallow-preserve](../tests/golden/types-nested-shallow-preserve/), [types-prelude-sub-nested](../tests/golden/types-prelude-sub-nested/), [jibb-nested-union-guards](../tests/lib/jibb-nested-union-guards.hoon) |
147| Missing tags: a bare tag absent from a known union reports both sites in casts, calls, unit payloads, list items, branch arms and nested tuples | Done | `types-missing-tag-*`, [types-nested-missing-tag](../tests/golden/types-nested-missing-tag/) |
148| Union printing: by in-scope name or imported alias; unnamed unions that escape print their cases, and generic unions keep their arguments | Done | `types-union-print-*`, [types-generic-union-escaping](../tests/golden/types-generic-union-escaping/), [types-generic-union-transitive](../tests/golden/types-generic-union-transitive/) |
149| Different import faces for one union origin are compatible, and distinct origins stay distinct | Partial: compatibility across distinct origins and some generic-argument comparisons are unsupported | [types-union-print-same-origin](../tests/golden/types-union-print-same-origin/), [types-union-print-distinct](../tests/golden/types-union-print-distinct/) |
150| Generic aliases may reorder, repeat or omit parameters, keeping a union's origin through scopes and library interfaces | Done: generic unions declared in a body and constraints on differing variables' faces are unsupported | [types-generic-union-alias](../tests/golden/types-generic-union-alias/), [types-generic-union-transitive](../tests/golden/types-generic-union-transitive/), [jibb-generic-alias](../tests/lib/jibb-generic-alias.hoon) |
151| Nested unions compare by runtime noun; an empty field empties a cell, and unknown inhabitation stays unresolved | Done | [types-partial-union-nested-nouns](../tests/golden/types-partial-union-nested-nouns/) |
152| Union patterns: whole-case arms, payload binders, imported and generic cases and binder-free catch-alls; missing cases and covered arms are reported | Done | [types-union-patterns](../tests/golden/types-union-patterns/), [types-union-patterns-generic](../tests/golden/types-union-patterns-generic/), [types-union-patterns-import](../tests/golden/types-union-patterns-import/) |
153| Partial boolean patterns: `?` positions split into at most 64 alternatives across the union | Done: past the limit the report says "union pattern expansion needs unsupported inference" | [types-union-finite](../tests/golden/types-union-finite/), [types-union-finite-limit](../tests/golden/types-union-finite-limit/), [types-union-finite-generic](../tests/golden/types-union-finite-generic/) |
154| Other partial patterns, binders spanning cases, some complex two-arm subjects | Missing: fail closed | [types-union-finite-limit](../tests/golden/types-union-finite-limit/), [types-union-patterns-generic](../tests/golden/types-union-patterns-generic/) |
155| Union pattern result context from a cast or call sample, for a union reached by a wing, grouped wing or shallow call | Partial: other subject forms are unsupported | [types-union-pattern-result-context](../tests/golden/types-union-pattern-result-context/), [types-union-pattern-result-controls](../tests/golden/types-union-pattern-result-controls/), [types-union-finite-context](../tests/golden/types-union-finite-context/) |
156| Branch result joins: `?-` arms unify, then widen only to a present parent aura or `@`, in any arm order | Done: sibling auras without a parent stay distinct, and distinct variables forced equal get a two-site error | [types-partial-branch-widening](../tests/golden/types-partial-branch-widening/), [types-union-finite](../tests/golden/types-union-finite/), [types-union-finite-generic](../tests/golden/types-union-finite-generic/), [jibb-deferred](../tests/lib/jibb-deferred.hoon) |
157| Recursive local branches, such as `rec-widen` | Done: arms over a known union whose results are all pending tags still fail closed as unsupported | [types-recursive-branch](../tests/golden/types-recursive-branch/), [types-local-error-order](../tests/golden/types-local-error-order/), [types-recursion-scc-local](../tests/golden/types-recursion-scc-local/), [types-union-patterns-generic](../tests/golden/types-union-patterns-generic/) |
158| Cell patterns: a single arm with two or more binders, the last taking the tail | Done: duplicate and shadowed binders and definite non-cell subjects fail | `types-cell-pattern-*` |
159| Structured single-arm patterns on a known non-union cell, with nested sub-patterns, wildcards and literal heads | Partial: intermediate union or collection tails and faced-record patterns are unsupported | [types-cell-pattern-many](../tests/golden/types-cell-pattern-many/), [types-cell-pattern-tail](../tests/golden/types-cell-pattern-tail/), [types-single-case-pattern](../tests/golden/types-single-case-pattern/) |
160| Closed cell context through a bounded loobean branch, keeping value faces and rolling back on failure | Partial: open or uncertain substitutions and nested retries are unsupported | [jibb-cell-branch](../tests/lib/jibb-cell-branch.hoon), [types-cell-branch-context](../tests/golden/types-cell-branch-context/) |
162### Gates, recursion and imports
164| Area | Status | Proved by |
166| Multi-argument calls: a right-nested sample keeping faces and shared variables, giving context to list and union arguments | Done: unknown-callee contexts and pending tags are unsupported | [types-multi-call](../tests/golden/types-multi-call/) |
167| Positional calls unify a variable argument with a faced sample slot without passing the face on | Done: `labelled` checks as `$-([label=@t msg=A] (element A))` | [jibb-buttons](../tests/lib/jibb-buttons.hoon), [jibb-positional-face-guards](../tests/lib/jibb-positional-face-guards.hoon), [jibb-closed-gate-guards](../tests/lib/jibb-closed-gate-guards.hoon), [types-positional-faces](../tests/golden/types-positional-faces/) |
168| Named unions through unconstrained polymorphic gates, keeping origin, arguments and faces | Partial: different origins, explicit-capital forcing and pending tags are unsupported | [types-union-polymorphic-identity](../tests/golden/types-union-polymorphic-identity/) |
169| Direct gate sample fit: a directly named, checked root gate against a generic gate sample in a direct prelude call | Partial: other cases fall back to ordinary inference, and it proves no island or watchability | [jibb-direct-gate-guards](../tests/lib/jibb-direct-gate-guards.hoon), [jibb-direct-gate-source](../tests/lib/jibb-direct-gate-source.hoon) |
170| Single self-recursive gates, top-level and local: a monomorphic self reference, then generalization; bad recursive arguments name both sites | Done: polymorphic recursion, explicit-capital forcing and local name collisions are unsupported | [types-recursive-sample](../tests/golden/types-recursive-sample/), [types-recursive-gate](../tests/golden/types-recursive-gate/), [types-local-recursive](../tests/golden/types-local-recursive/) |
171| A closed base type seeds the result of a complete loobean branch with one direct self-call arm | Done: open or pending bases don't seed it | [types-recursive-branch](../tests/golden/types-recursive-branch/) |
172| Top-level mutual recursion: gate groups inferred together, generalized after the group checks, instantiated independently downstream | Partial: conservative dependency edges can reject valid programs | `types-recursion-scc-*` |
173| Local mutual recursion: shared monomorphic seeds, captured outer variables kept shared | Partial: distinct forced captures, unresolved tags, shadowing and mixed gate/value cycles fail closed | [types-local-scc](../tests/golden/types-local-scc/), [types-local-scc-adversarial](../tests/golden/types-local-scc-adversarial/), [types-recursion-scc-local](../tests/golden/types-recursion-scc-local/) |
174| Non-gate value cycles, reported with a dependency site when an explicit atom or loobean cast establishes them | Partial: bare aliases, branches and nested-local edges decline | [types-value-cycles](../tests/golden/types-value-cycles/), [types-value-cycle-shadow](../tests/golden/types-value-cycle-shadow/), [types-value-cycle-unsupported](../tests/golden/types-value-cycle-unsupported/) |
175| Other mixed gate/value cycles, polymorphic recursion, unresolved literal constraints and unresolved branch joins | Missing | [types-recursion-scc-failures](../tests/golden/types-recursion-scc-failures/), [types-value-cycle-unsupported](../tests/golden/types-value-cycle-unsupported/) |
176| Library imports: supplied Jibb sources in dependency order, a per-run interface cache, missing-source and cycle reports, nested fields of imported values | Partial: a library with a recursive mold yields no interface | `module-import-*`, `module-cache-*`, `types-module-field-*` |
178### Bounded and experimental routes
180| Area | Status | Proved by |
182| Generic recursive trees: a source-proven tree in an import-free owner module keeps its nominal identity across imports and aliases | Partial: a narrow test tree, not `element`; different origins and unproved casts decline | [jibb-generic-recursion](../tests/lib/jibb-generic-recursion.hoon) |
183| Tree construction one source-proven layer at a time under a known type | Partial: wrong-owner, wrong-argument and bad-child cases report "list item constraint is not supported", not an error | [jibb-generic-construction](../tests/lib/jibb-generic-construction.hoon) |
184| Flat tree matches with explicit tags or nonbinding catch-alls, and a missing-case error for a single-arm match | Done: 128 arms are screened and 129 decline | [jibb-generic-pattern](../tests/lib/jibb-generic-pattern.hoon) |
185| Whole-case binders, nested patterns, general structural fits and gate-free proof for these trees | Missing: declined | [jibb-generic-pattern](../tests/lib/jibb-generic-pattern.hoon), [jibb-generic-recursion](../tests/lib/jibb-generic-recursion.hoon) |
186| Tree limits: 4,096 face and substitution visits per scan, 128 arms per pattern, unfolding fuel per attempt | Partial: the 4,096 and 128-arm boundaries are tested; the suites test fuel 0 to 4, not the 256-step `jrec-fuel` | [jibb-generic-construction](../tests/lib/jibb-generic-construction.hoon), [jibb-generic-pattern](../tests/lib/jibb-generic-pattern.hoon) |
187| `qath`: source identity, null and cell construction and matching, static application-path literals, faces and identity across imports | Partial: the suites test fuel 0 to 2, not the 256-step limit | `types-qath-*`, [jibb-qath-fuel](../tests/lib/jibb-qath-fuel.hoon), [jibb-qath-source](../tests/lib/jibb-qath-source.hoon) |
188| `qath` for other recursive shapes, broader patterns and dynamic path segments; route and static-file checks | Missing: dynamic segments need unsupported inference, and routes wait for milestone 4 | [types-qath-recursive](../tests/golden/types-qath-recursive/) |
189| Deferred constructor transaction: unsafe shapes decline, so a later substitution cannot undo a face check | Partial: experimental; no test isolates each declined category | [jibb-deferred](../tests/lib/jibb-deferred.hoon) |
190| Deferred retries once later dependencies exist; a two-arm boolean branch keeps literal obligations until a closed context resolves them | Partial: faced targets, unions with a case that is not a constant or a cell, list literals and general union-pattern branches decline | [jibb-deferred-context](../tests/lib/jibb-deferred-context.hoon), [jibb-deferred](../tests/lib/jibb-deferred.hoon) |
191| Deferred direct-constructor constraints in an import-free library without a prepared prelude, published only when everything closes | Partial: experimental; stores, preludes, imports, recursive groups, open interfaces and `%grec` scans are rejected | [jibb-deferred](../tests/lib/jibb-deferred.hoon), [jibb-deferred-resolver](../tests/lib/jibb-deferred-resolver.hoon) |
192| Prepared-prelude initializer recovery: a non-main library tuple initializer deferred to a later exact result cast | Partial: needs exact value, mold and interface inventories, and the report keeps "partial inference; module not checked"; list literals are not deferred | [jibb-deferred-prepared](../tests/lib/jibb-deferred-prepared.hoon) |
193| Prepared recovery guards: API and store paths, `main` and imports are excluded; wrong fields, unrelated tags and mold collisions fail closed | Done | [jibb-deferred-prepared](../tests/lib/jibb-deferred-prepared.hoon) |
195## Types and prelude: prelude
197| Area | Status | Proved by |
199| Shared interface: every vendored name reserved, only inferred entries exposed, such as `list`, `unit`, `same`, `fall`, `need`, `bond`, `lure`, `weld`, `snoc`, `turn` and `lent` | Partial: backend validation is outstanding | [jibb-module-scope](../tests/lib/jibb-module-scope.hoon), [jibb-list-alias-guards](../tests/lib/jibb-list-alias-guards.hoon), [types-prelude-interface](../tests/golden/types-prelude-interface/) |
200| One prelude origin for all callers, so a library can export a type with unqualified `(unit A)` | Done | [types-prelude-interface](../tests/golden/types-prelude-interface/), [jibb-module-scope](../tests/lib/jibb-module-scope.hoon) |
201| Preparation: `+prepare-prelude` rejects malformed, conflicting and import-bearing source, and `+prepare-prelude-with-internal` takes the private internal import | Done: that prepared values are trusted is a contract, which no test checks | [jibb-poke-bridge](../tests/lib/jibb-poke-bridge.hoon), [jibb-module-scope](../tests/lib/jibb-module-scope.hoon) |
202| The validated `list` template for the prelude's own gates and mold aliases; an altered, omitted, duplicate or malformed `list` doesn't leak through aliases | Done | [jibb-list-alias-guards](../tests/lib/jibb-list-alias-guards.hoon), [types-prelude-list-alias](../tests/golden/types-prelude-list-alias/), [types-prelude-list-functions](../tests/golden/types-prelude-list-functions/) |
203| The prelude `list` and imported Hoon lists unify both ways | Partial: other Jibb-written collection molds and most collection operations are unsupported | [types-list-imported](../tests/golden/types-list-imported/), [types-list-pattern-imported](../tests/golden/types-list-pattern-imported/), [jibb-bridge](../tests/lib/jibb-bridge.hoon) |
204| With `list` or `unit` missing or altered, independent private molds (`qath`) stay available and dependent ones (`ask`) don't | Done | [jibb-qath-source](../tests/lib/jibb-qath-source.hoon), [jibb-ask-guards](../tests/lib/jibb-ask-guards.hoon) |
205| Module scope: the prepared and source-taking prelude paths compared against the real prelude | Partial: does not establish complete shadowing coverage | [jibb-module-scope](../tests/lib/jibb-module-scope.hoon), [types-prelude-interface](../tests/golden/types-prelude-interface/) |
206| `fall` and `need` | Done | [prelude-list-unit](../tests/golden/prelude-list-unit/), [types-prelude-direct](../tests/golden/types-prelude-direct/) |
207| `drop`, `skim`, `skip`, `murn`, `join`, `snip`, `rear` and a shared-type `clap` | Partial: no test calls `rear` | [types-prelude-list-helpers](../tests/golden/types-prelude-list-helpers/), [types-prelude-unit-helpers](../tests/golden/types-prelude-unit-helpers/) |
208| `bond`, `levy`, `lien`, and gate composition and currying | Partial: currying a faced sample is unsupported | [types-prelude-bond](../tests/golden/types-prelude-bond/), [types-prelude-predicates](../tests/golden/types-prelude-predicates/), [types-prelude-functional](../tests/golden/types-prelude-functional/) |
209| `hunt`, with the ordering gate first | Done: both ordering outcomes and absent units infer; a mismatched payload or ordering-gate sample names both sites | [types-prelude-unit-helpers](../tests/golden/types-prelude-unit-helpers/), [prelude-unit-list-transforms](../tests/golden/prelude-unit-list-transforms/) |
210| `like`: the value gate maps a `(like A)` result with a gate, and `like` is still a mold | Partial: an incompatible converter is reported as unsupported, not as an error | [types-prelude-like](../tests/golden/types-prelude-like/) |
211| `eq` and `mate`, with a gate-free variable; `set`, `map`, `mop`, `jar` and `jug` constrain only their keys | Partial: backend equality and crash behavior are unverified | [jibb-gate-free-guards](../tests/lib/jibb-gate-free-guards.hoon), [types-prelude-unit-helpers](../tests/golden/types-prelude-unit-helpers/) |
212| `lent` | Done | [types-prelude-lent](../tests/golden/types-prelude-lent/) |
213| `succ` through `add`, keeping its non-loobean atom constraint | Done: a Hoon translation agrees with Hoon's `succ` on ten inputs | [types-prelude-succ](../tests/golden/types-prelude-succ/), [jibb-hoon-reference](../tests/lib/jibb-hoon-reference.hoon) |
214| `lead` and `late`, curried | Done: a Hoon translation agrees with Hoon's on 25 pairs of five nouns, a gate among them | [types-prelude-lead-late](../tests/golden/types-prelude-lead-late/), [jibb-hoon-reference](../tests/lib/jibb-hoon-reference.hoon) |
215| `zing` over `weld` | Done: a Hoon translation matches Hoon's `zing` on 4 inputs | [types-prelude-zing](../tests/golden/types-prelude-zing/), [jibb-hoon-reference](../tests/lib/jibb-hoon-reference.hoon) |
216| `lth`, `gte` and `lte` over `gth` and `not` | Partial: complete import checking is unfinished | [types-prelude-comparison](../tests/golden/types-prelude-comparison/) |
217| Private `gth`, `add` and `dec` schemes that ordinary imports cannot reach; `add` and `dec` reject loobeans | Done | [types-prelude-arithmetic](../tests/golden/types-prelude-arithmetic/), [types-arithmetic-module](../tests/golden/types-arithmetic-module/), [jibb-arithmetic-guards](../tests/lib/jibb-arithmetic-guards.hoon) |
218| `trip` and `tuba` over private primitives: `$-(@t (list @tD))` and `$-((list @tD) (list @c))` | Partial: no test compares them with Hoon's definitions | [types-prelude-text](../tests/golden/types-prelude-text/) |
219| `cmd`, the doc's generic union with five cases | Partial: the prelude inventory is incomplete | [types-prelude-cmd](../tests/golden/types-prelude-cmd/) |
220| `sub`, with `%watch` payloads of type `(ask M)` | Done: building a `sub` proves no watchability | [types-prelude-sub](../tests/golden/types-prelude-sub/), [types-prelude-sub-nested](../tests/golden/types-prelude-sub-nested/), [jibb-sub-guards](../tests/lib/jibb-sub-guards.hoon) |
221| `ask`, with pure, agent and store cases, and `pure` | Partial: receiver mismatches and path, `qath` and erased-fact casts are unsupported | [jibb-ask-guards](../tests/lib/jibb-ask-guards.hoon), [types-prelude-ask](../tests/golden/types-prelude-ask/) |
222| `qath`, `~` or `[i=@ta t=qath]` in the internal prelude, re-exported | Done | [jibb-qath-source](../tests/lib/jibb-qath-source.hoon), [types-qath-module-identity](../tests/golden/types-qath-module-identity/) |
223| `raw-poke`, defined in the internal prelude and re-exported as a transparent type | Done | [jibb-poke-bridge](../tests/lib/jibb-poke-bridge.hoon) |
224| Printed types say `ask`, `qath` and `raw-poke`, without `.internal` | Done | [types-prelude-ui](../tests/golden/types-prelude-ui/), [jibb-theme](../tests/lib/jibb-theme.hoon), [types-prelude-cmd](../tests/golden/types-prelude-cmd/) |
225| `store` mold and builder; a store's local `+$ poke` stays its own action mold | Done: multi-action declarations are unsupported | [jibb-store](../tests/lib/jibb-store.hoon), [jibb-poke-bridge](../tests/lib/jibb-poke-bridge.hoon) |
226| UI length and attribute molds, the 19 element constructors, and `program` and `page` records and builders, with exact schemes | Done | [types-prelude-ui](../tests/golden/types-prelude-ui/) |
227| `element`: a nonrecursive 19-case union with `*` children, and `island` giving `(element !!)` | Partial: a child-message mismatch (`bad-child`) is reported as unsupported, not as an error | [types-prelude-ui](../tests/golden/types-prelude-ui/) |
228| Raw-constructor encapsulation, duplicate-attribute checks, rendering, storage and navigation | Missing: a raw `[%text "raw"]` element infers | [types-prelude-ui](../tests/golden/types-prelude-ui/) |
229| `theme`: required text tokens, an optional `qath` font and optional dark tones | Done: no theme behavior is implemented | [jibb-theme](../tests/lib/jibb-theme.hoon), [doc-overview-02-theme](../tests/golden/doc-overview-02-theme/) |
230| Execution and jet recognition of prelude gates and primitives | Missing | none |
232## Types and prelude: Hoon importer
234| Area | Status | Proved by |
236| The bridge into inference: `*`, selected atoms, singletons, nested cells, disjoint unions and opaque standard collections from `/sur` molds and marks | Partial: supported shapes only, with `*` only in nonrecursive molds; the mark bridge mainly tests that only the declared aura mark resolves | [jibb-bridge](../tests/lib/jibb-bridge.hoon), [jibb-tlon-bridge](../tests/lib/jibb-tlon-bridge.hoon), [type-import/expected.txt](../tests/type-import/expected.txt), [jibb-mark-bridge](../tests/lib/jibb-mark-bridge.hoon) |
237| Bridged collections keep their names and arguments, including nested union arguments | Partial: the bridge trusts unchanged source-aware reader results, which is documented, not testable | [jibb-bridge](../tests/lib/jibb-bridge.hoon) |
238| A Hoon `(unit T)` becomes the prelude `unit`, also inside unions and lists, API marks and poke exports | Done | [jibb-bridge](../tests/lib/jibb-bridge.hoon), [jibb-api-paths](../tests/lib/jibb-api-paths.hoon) |
239| Repeated faces in imported record spines | Partial: fail closed with a generic diagnostic, and may reject valid names in scopes Hoon erased | [jibb-bridge](../tests/lib/jibb-bridge.hoon) |
240| Reader coverage: mark samples, Ford-verified recursive molds, nested collections, direct ordered maps (Tlon `notes.log`), disjoint direct `$^` unions, one explicit union argument in a collection | Done | [jibb-import](../tests/lib/jibb-import.hoon), [jibb-mark-bridge](../tests/lib/jibb-mark-bridge.hoon), [types-import-tlon-notes](../tests/golden/types-import-tlon-notes/) |
241| Tagged `$%` cases with local named payload molds, bare `~` fields and one level of nested tagged unions, as in the real Tlon notes | Partial: other nested unions are unfinished | [types-import-tlon-notes](../tests/golden/types-import-tlon-notes/), [jibb-import](../tests/lib/jibb-import.hoon) |
242| Self-recursive `/sur` molds, including Tlon `notes.import-node`, as opaque module-and-name identities | Partial: aliases, foreign references, recursive marks, unfolding and construction are unsupported | [types-import-tlon-notes](../tests/golden/types-import-tlon-notes/), [jibb-import](../tests/lib/jibb-import.hoon) |
243| Explicit `$%`, `$?` and `$^` unions checked from source, including cases Hoon would collapse | Partial: ambiguous recursive origins fail closed | [jibb-import](../tests/lib/jibb-import.hoon), [jibb-import-overlap](../tests/lib/jibb-import-overlap.hoon), [jibb-import-structural](../tests/lib/jibb-import-structural.hoon) |
244| Other nested unions, nested ordered maps, general union disjointness, complete import integration | Missing: reported as disjointness that could not be verified | [jibb-import](../tests/lib/jibb-import.hoon) |
245| Collection recognition checks the originating core and rejects shadows, missing provenance and forged subjects, samples and tails | Done | [jibb-import](../tests/lib/jibb-import.hoon), the Tlon fixtures [importer/tlon-epic.txt](../tests/importer/tlon-epic.txt), [importer/tlon-presence.txt](../tests/importer/tlon-presence.txt) and [importer/tlon-docs.txt](../tests/importer/tlon-docs.txt) |
246| `$?` overlaps, proved by comparing each case's runtime noun and reported at the Jibb use site | Partial: Hoon case locations are not reported, and the mark reader reports no overlaps | [jibb-import-overlap](../tests/lib/jibb-import-overlap.hoon), [jibb-import-structural](../tests/lib/jibb-import-structural.hoon) |
247| Overlap budgets: 128 cases and 4,096 source nodes per union, and 4,096 nodes each for dependencies and the witness | Done: they don't bound chapter lookup, Hoon evaluation or graph walks | [jibb-import-overlap](../tests/lib/jibb-import-overlap.hoon), [jibb-import-structural](../tests/lib/jibb-import-structural.hoon) |
248| `$~` default wrappers in the tagged-union proof: the Tlon saga mold and a labelled saga envelope | Done: overlap, recursive, shadow and malformed controls are rejected | [jibb-import-default](../tests/lib/jibb-import-default.hoon) |
249| Consecutive default wrappers | Partial: four are peeled and five rejected; no test shows that defaults in dependency proofs spend the node budget | [jibb-import-default](../tests/lib/jibb-import-default.hoon) |
250| Structured reader APIs (`read-named-diagnostic`, `read-mark-diagnostic`) keep graphs and tell definite aura and core errors from unprovable ones | Partial: unverified union disjointness and name-only vase recognition are unsupported | [jibb-import-diagnostic](../tests/lib/jibb-import-diagnostic.hoon), [jibb-import](../tests/lib/jibb-import.hoon) |
251| Reader errors at Jibb use sites, replayed into nested samples, casts and same-module aliases | Partial: imported union molds, generic applications and transitive modules keep the generic message, as do duplicate, missing or clashing inputs | [jibb-import-diagnostic](../tests/lib/jibb-import-diagnostic.hoon), [type-import-diagnostic/nested.txt](../tests/type-import-diagnostic/nested.txt) |
252| The importer golden: 221 projections | Done | [jibb-import](../tests/lib/jibb-import.hoon), [importer/tree.txt](../tests/importer/tree.txt) |
253| Clay: the example `/sur` files and marks built through Clay, a recursive Ford import's origin, a Ford-built nested union into partial inference | Done: 14 threads, each with an expected file | `tools/clay-fixtures`, [clay-fixtures/](../tests/clay-fixtures/) |
257| Area | Status | Proved by |
259| `tools/golden`: the golden corpus under `urbit eval` | Done | `tools/testdata/selftest` |
260| `tools/test-arms`: the 62 `test-` arms of the 58 `tests/lib` suites under eval, chosen by name, glob or shard, with `--list`, `--report` and `--update` | Done | `tools/testdata/selftest` |
261| `tools/ship test`: the same arms and one arm per golden case on the fake ship, 753 in all | Done | `tools/testdata/ship-selftest` |
262| `tools/check`: every check, with the suites in four cost-balanced shards (`arms-1` to `arms-4`) | Done | `nix flake check` runs the same groups ([flake.nix](../flake.nix)); nothing tests the runner itself |
263| `nix build` and `nix flake check`: the four desks, and every check in the Nix sandbox | Done | [flake.nix](../flake.nix) |
264| The tools' own tests: `tools/testdata/selftest` (23 checks) and `tools/testdata/ship-selftest` | Done | the two scripts |
265| `tools/hoon --no-debug` builds the library without `!:`, for timings | Done | `tools/testdata/selftest` |
266| A UI runtime and the shared host | Missing: the `jibb` desk holds only `desk.bill` and `sys.kelvin` | none |
270- Nothing runs yet: with no lowering, backend, UI runtime or jet recognition, programs, pages, stores, islands and prelude gates are checked statically only ([type-todo-full/about.txt](../tests/type-todo-full/about.txt)).
271- Requests have no lowering, checked decoding or runtime validation, nothing proves an arbitrary request value watchable, agent and store `ask` receivers take raw nouns, and API request gates don't take Jibb module imports, scry paths, more than one parameter or diff, or a parameter with a fold ([internal.jibb](../jibb-dev/lib/jibb/internal.jibb), [module-import-api-request-reason](../tests/golden/module-import-api-request-reason/)).
272- Complete private module checking, other API shapes, root API and module kind checking, complete `ask` and `pure` checking and multi-action stores are not implemented (Kinds, Agent APIs and Shared state in [spec/decisions.md](spec/decisions.md)), and the partial report every golden `types.txt` prints declines modules the full check accepts.
273- The `my-app` modules are checked with Hoon types read by `ride`, not through Clay as [prompts/milestone-2.md](prompts/milestone-2.md) asks; the Clay threads run only the partial checker, on synthetic modules ([clay-fixtures/](../tests/clay-fixtures/)).
274- The parser still accepts `[]` and `m()`, which the decisions make errors (where to reject them waits for [review ruling 19](open-questions.md#review-rulings-waiting-for-iko)), and the 13 unasked grammar questions follow [provisional readings](open-questions.md#grammar-questions-never-put-to-the-docs-author).
275- The prelude's inventory and signatures are not specified yet (question 3 in [open-questions.md](open-questions.md)), most collection operations are unsupported, the UI prelude has no raw-constructor encapsulation or duplicate-attribute check, and themes have no contrast check, rendering or font routing ([types-prelude-ui](../tests/golden/types-prelude-ui/), [jibb-theme](../tests/lib/jibb-theme.hoon)).
276- Inference declines many shapes it should decide, and the Partial and Missing rows name them. The largest are `proj` with reordered fields (question 32 in [open-questions.md](open-questions.md)) or in nested contexts, patterns past 64 boolean alternatives or across cases, polymorphic recursion and other mixed gate/value cycles, holes in complex molds, and dynamic `qath` segments.
277- Some definite errors come out as "unsupported": a child-message mismatch in UI composition, a gate or non-tape list in interpolation, union branch arms whose results are all pending tags, and wrong-owner tree construction ([types-prelude-ui](../tests/golden/types-prelude-ui/), [types-string-interpolation](../tests/golden/types-string-interpolation/), [types-union-patterns-generic](../tests/golden/types-union-patterns-generic/), [jibb-generic-construction](../tests/lib/jibb-generic-construction.hoon)). Diagnostics are coarse in places: one caret per site, record mismatches at the cast or edit, generic messages for imported union molds and repeated faces, and no Hoon case locations ([types-multi-call](../tests/golden/types-multi-call/), [type-import-diagnostic/about.txt](../tests/type-import-diagnostic/about.txt)).
278- The Hoon importer leaves other nested unions, nested ordered maps, general disjointness, mark-reader overlap diagnostics, recursive aliases and marks, unfolding and complete import integration unfinished, and peels at most four `$~` wrappers ([compiler.md](compiler.md), [importer/tree.txt](../tests/importer/tree.txt), [jibb-import-default](../tests/lib/jibb-import-default.hoon)).
279- No test reaches some stated limits: the 256-step `jrec-fuel`, program `main`'s shared 256-node budget, the 64-definition pending-tag retry behind the buttons error, defaults inside `$~` dependency proofs, and the rejection of re-exported watches and of aliased initializers ([jibb-dev/lib/jibb.hoon](../jibb-dev/lib/jibb.hoon)).
280- No test or check measures performance. The timings in [compiler.md](compiler.md) and the library's notes are single runs, the brief's timings of the corpus and the `my-app` desk ([prompts/milestone-2.md](prompts/milestone-2.md)) are not recorded, and neither the tuple payload context nor reader diagnostic replay has a complexity bound.
284[Before pushing](development.md#before-pushing) in development.md says how to run every check (`tools/check`; `tools/check --list` prints them), and [The test suites](development.md#the-test-suites) says what each suite checks. The [README](../README.md) gives each tool's commands: the [golden tests](../README.md#golden-tests), the [test suites](../README.md#test-suites), the [fake ship](../README.md#fake-ship) and [Nix](../README.md#building-and-checking-with-nix). `tools/test-arms --shard 2/4 --list` prints the suites of one shard.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list