@@ -1,11 +1,13 @@
11# Status
22
3−As of 2026-11-02. The plan is [spec/implementation-plan.md](spec/implementation-plan.md); each milestone ends with its checks passing on a fake ship.
3+As 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.
4+
5+## Milestones
46
57| # | Milestone | Status |
68| --- | --- | --- |
79| 1 | Parser and mark | Done (7c739b7; the doc's grammar decisions of 2026-10-30 in ab797a9) |
8−| 2 | Types and prelude | In progress. [prompts/milestone-2.md](prompts/milestone-2.md) briefs the developer; the checker and importer are partial |
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 |
911| 3 | Core language | Not started |
1012| 4 | Host and static pages: the first release | Not started |
1113| 5 | Published pages | Not started |
@@ -13,300 +15,270 @@ As of 2026-11-02. The plan is [spec/implementation-plan.md](spec/implementation-
1315| 7 | Tooling | Not started |
1416| 8 | Polish | Not started |
1517
16−The plan sets no dates: "agree them after milestone 1, once it shows how fast the Hoon work goes". They haven't been agreed yet. Milestone 1's commits run from 2026-10-29 18:13 UTC to 2026-10-30 11:50 UTC.
17−
18−On 2026-10-30, @iko decided that Jibb drops `$?`, so a `+$` takes a union's cases on the lines below its name. [prompts/drop-union-rune.md](prompts/drop-union-rune.md) records the change before milestone 2. The repository spec records the decision; the Claude document still needs to be synchronized.
19−
20−## Milestone 2: in progress
21−
22−The parser accepts `_` in mold positions and typed path segments, retaining each hole’s span. The partial checker tracks ordinary annotation holes through inference and requires each value or local definition to resolve its own holes before generalization. A hole can resolve to a concrete type or an explicitly written in-scope type variable; later uses cannot fix an unresolved definition. Independent decimal holes can default, but captured variables are not defaulted prematurely. Structural named molds with an unresolved hole report its site. Complex mold forms, inferred path segments, mutual recursive groups and other unsupported constraints still fail closed, and the fragment does not claim the module is checked. A syntax-tree pass rejects duplicate field names within each written record and reports both sites. The repository spec now records that `ask` and `qath` are transparent; complete request checking remains outstanding.
23−
24−On 2026-10-31, @iko chose explicit, result-directed `(proj record)` to construct a record with exactly the expected fields, and reserved `proj` against definitions and imports. The partial checker handles selected explicit calls with known, closed record types, records field-selection evidence for later lowering, and reserves the name across source bindings. Reordered fields, some nested contexts and several open or recursive cases remain unsupported; lowering and execution are not implemented yet. The field-order question remains open.
25−
26−The internal prelude also defines `qath` as a transparent recursive knot sequence, re-exported by the public prelude. The partial checker recognizes its source identity, supports selected null/cell construction and matching, and types static application-path literals. Construction and matching for other recursive shapes, broader patterns and dynamic application-path segments remain unsupported. A 256-step limit applies per inference attempt, not to parsing or retries; checking routes and static files remains milestone 4.
27−
28−The checker also recognizes a limited source-proven generic recursive tree in an import-free defining module. Its nominal identity retains the defining path, mold name and type arguments, including across supported imports and aliases. With a known expected type it can construct supported tagged cases by checking one source-proven layer at a time. Flat matches with explicit tags or nonbinding catch-alls also work for these source-proven trees, as does a missing-case diagnostic for a supported single-arm match. At most 128 arms are screened per attempt; whole-case binders and nested patterns remain unsupported. Broader pattern matching, general structural fits and gate-free proof remain unsupported; this is not yet the prelude's `element` implementation or island checking. The source index uses fixed-shape checks during mold collection. Each construction or supported pattern attempt has 256 unfolding steps and at most 4,096 face and substitution visits per scan; pattern subject recognition and view validation can each scan separately. Parsing, other inference and retries remain outside those limits. A single startup-inclusive comparison of 1,000 ordinary gates produced identical reports and used 29.12 seconds of user CPU before the shared-resolver refactor and 28.55 seconds after it, with other work running; it is not a general performance bound.
29−
30−A bounded local source proof recognizes a narrow class of generic-alias union cases with different literal heads, then applies the ordinary mold checks. Nested or qualified aliases and several open states remain unsupported, including a valid alias used during the deferred transaction; the partial report states that the mold itself has not been checked. The `jibb-union-source` suite, `tests/lib/jibb-union-source.hoon`, exercises the source and state bounds and failure paths under eval (`tools/test-arms jibb-union-source`) and on the ship (`tools/ship test`). A separate bounded witness now reports proven collisions between supported literal-headed aliases, with both original case sites; unknown payload intersections still decline. The detailed full-module result now carries the first failed mold’s source-bound overlap evidence, including through ordinary Jibb imports; the legacy text result renders both case excerpts. Specialized API and prelude paths remain limited. The shared guards pass under eval and on the ship.
31−
32−The checker can experimentally discharge a narrowly scoped direct-constructor constraint while resolving an import-free library without a prepared prelude. It preserves independent generalized schemes and publishes only after all source molds, values, and recorded constraints close. API/store paths, `main`, imports, prepared preludes, recursive groups, open constraints, projection actions, and `%grec` in the constraint graph remain unsupported by this route. The fallback also declines source shapes outside its bounded direct-call screen. It does not yet typecheck the unchanged todo island or establish watchability.
33−
34−A prepared-prelude partial report can recover a narrow import-free, non-main ordinary library initializer by deferring source-owned literals in a direct tuple until a later exact result cast. The prepared interface and declared-name inventories must agree exactly. API/store paths, `main` and imports remain excluded, and the ordinary full-module resolver does not publish the recovered interface. Wrong field types, unrelated tags and mold collisions fail closed; a no-final-cast control remains unchecked. The `jibb-deferred-prepared` suite, `tests/lib/jibb-deferred-prepared.hoon`, checks the exact recovered types and unchanged `partial inference; module not checked` disclaimer under eval and on the ship. List-literal deferral and import-aware recovery remain unsupported.
35−
36−Closed cell context can now flow through a bounded loobean branch while preserving the inferred value faces and original failed-inference behavior. Open or structurally uncertain substitutions and nested retry shapes remain unsupported. This does not by itself provide the remaining cross-definition context or complete island-kind and watchability checks needed by the unchanged todo island.
37−
38−The internal prelude defines a transparent generic `ask` with pure, agent and store cases, re-exported alongside the Jibb-written `pure` gate. The partial checker infers supported constructors and exhaustive matches. Agent and store receivers operate on raw nouns; their fields do not prove schema validity or watchability. The public prelude now defines the documented source-backed `sub` union; supported `%watch` payloads retain the public `(ask M)` type. Constructing a `sub` does not prove that its request is watchable. Request lowering, checked decoding, runtime validation and general island watch checking remain unimplemented; the separate direct-program proof below covers only one narrow static value shape.
39−
40−The public prelude now contains the source-backed UI length/attribute molds, all element constructors, and exact program/page records and builders. The full 19-case generic `element` union is nonrecursive: nested child, keyed-item and table payloads are `*`, while public constructor schemes preserve typed composition and independent key types. `island` returns `(element !!)` with `[program data]` as its erased payload. The focused UI golden checks exact schemes, static and message-bearing composition, concrete programs/pages/islands, malformed inputs and selected mismatches. A child-message mismatch fails closed as an unsupported constraint. Raw-constructor encapsulation, duplicate-attribute checks, rendering, storage, navigation and execution are not claimed.
41−
42−The remaining doc fragments now also have full detailed and legacy checks: the import-only module resolves its real `/sur`, mark and Jibb-module inputs; `view-day` and `step` check with their exact exported schemes; and the `cmd`/`sub` block checks at the prelude path against the canonical printed schemes. Additional consumers use all three imported names, and the shared eval/ship fixture rejects missing `/sur`, mark and Jibb-module inputs.
43−
44−The documented buttons library now fully checks its valid `labelled` and `wide` definitions with their exact generic element and attribute-list schemes. Ordinary positional calls unify a variable argument with the body of an expected faced sample slot without propagating that slot face. When full checking would otherwise reject an incomplete module, a failure-only retry of at most 64 missing definitions can report a still-pending tag at its source; the unchanged buttons module thus reports that nothing fixes the union of `%add`, with the actual excerpt, through both detailed and legacy inference. Successful checks do not run that retry. The shared eval/ship fixture is type checking only and claims no UI runtime.
45−
46−The public prelude now defines the exact documented `theme` record, including required text tokens, an optional `qath` font and optional dark tones. A shared eval/ship fixture fully checks the byte-identical `my-app/ui/theme.jibb`, checks its exact exported type and structural downstream import, and covers absent dark tones plus wrong nested auras, missing fields and wrong font/dark types. On 2026-11-01, @iko chose explicit backtick syntax for present units, and the documented dark record now uses it. No contrast check, rendering, routing or other theme behavior is implemented.
47−
48−Known same-origin generic-union result context can now constrain a call before its arguments are inferred. An unresolved or opaque constructor target stays unsupported rather than producing a definite mismatch; proven missing tags still report errors. A todo request with explicit `(ask msg)` context can infer `|=%got`; its uncontextualized form remains unsupported. A two-item literal-headed tuple can receive payload context from a known union of uniquely headed literal cells when its payload is a shallow wing-headed call with literal, wing or constructor arguments. Existing inference takes precedence when it fits; otherwise the checker tries the contextual path once. It conservatively declines that path when any substitution has a structural root, as well as for duplicate or opaque competitors. The guard scans substitutions per eligible tuple and may add one shallow inference; no global linear-time bound is claimed. This allows an explicitly typed todo subscription body to infer, but does not check the island or prove request watchability.
49−
50−A separate source-backed analysis can prove one named mold gate-free, report a definite gate with a field path, or return unknown. It retains the prepared prelude, source bundle, reader results and resolved imports; the actual todo model proves gate-free, while a callback field reports its path and `*` remains unknown. Its classifier is capped at 256 nodes, not the surrounding parse and import work. API, store and private roots are unsupported, and the artifact does not check a module or island, infer generalized constraints, or prove watchability.
51−
52−The partial checker can also match a directly named, checked root gate against a generic gate sample in a direct, unshadowed source-backed prelude call. It uses the written two-slot sample layouts to preserve nested record faces, then requires the complete call samples to be closed and tag-free and repeats the fit under the final substitution. The proof falls back to existing inference for unavailable or ambiguous source layouts, local or dynamic gates, aliases, recursive placeholders and open generic caller types. It preserves written-capital checks and projection evidence; it does not add `program`, check islands or prove request watchability. Prepared prelude source and interface remain a trusted pair.
53−
54−A narrow full-module path now checks direct four-wing `(program init update view subs)` definitions named `main`. It requires the canonical prepared `program` value and mold, reuses ordinary source-backed program fitting, and publishes only after all ordinary module and request-graph checks. The inferred `main` must be closed and invariantly match the instantiated `program` mold. Initializer data and model must be closed and gate-free with `%yes` verdicts inside a shared 256-node budget. `subs` may syntactically return null through transparent forms, or one direct imported request watch after the request graph merges. The latter is only an unfaced two-item `[%watch (case.face |=%callback)]` singleton: the imported member must have the exact plain derived-request scheme, a unique merged request must match the API path and both case names and occur in the interface's own graph, the API source must be identical, and scry, diffs and parameters must be absent. Pure or hand-built values, helpers, aliases, re-exports, typed paths, folds, multiple watches and unknown or ambiguous evidence remain rejected. Checked interfaces retain source evidence and support ordinary downstream imports; no program execution or runtime watching is claimed. A transactional extension can recover a direct initializer when update, view and subs are already resolved: it infers the initializer against the closed model that update's two-item sample, or else main's own program fit, establishes, then re-infers `main` under all ordinary finalization and kind checks. Any body and closed sample of a direct gate check this way; a body that context inference cannot take is inferred ordinarily as a whole gate. An update sample written as one faced mold, a pun, a named mold or generic in the model, and generic view and subs samples, also check. Non-main libraries, aliased mains or initializers, simultaneously unresolved subscriptions and unrelated pending tags remain rejected.
55−
56−Static and direct data-page `main` checking now completes the unchanged about page, blog index and todo index through the real Hoon readers. Static generic element mains specialize to closed canonical `(element !!)`; direct pages require a closed invariant `page` type and a direct plain derived-request load. Page loads reuse the strict source/member/evidence identity checks used by program watches, rejecting aliases, indirect/hand-built/pure/unknown requests, typed paths, diffs and store paths. The shared eval and ship fixture asserts exact main types and structural downstream imports. Rendering, runtime loading and request execution remain unimplemented.
57−
58−The prelude now has the approved `store` mold and action-checking builder. The runtime envelope is the transparent `raw-poke`; a store's local `+$ poke` remains its ordinary action mold throughout inference. Direct two-wing store mains require closed state and action molds, exact init/state and update relations, and no gate-free-state restriction. Stores export those molds plus derived generic `poke` command and state-request gates. The command helper checks the canonical `raw-poke`, `cmd` and `unit` shapes, takes an action and reply, and returns `(cmd M)` directly. Separate source-bound store certificates prove only the actual imported state member watchable; API evidence checks and page-load rejection remain intact. The unchanged cart and basket pass detailed and legacy checking with exact mains, derived schemes and structural imports, including non-keyed view and null-sample initializer recovery. Multi-action declarations, lowering and runtime execution remain unsupported.
59−
60−Keyed programs no longer skip ordinary component inference: an annotated initializer that checks normally is accepted, with recovery reserved for definitions that still need it. The todo fixture's initializer is a gate cast to its full type, which only ordinary inference accepts, so it fails if the skip returns; it checks through detailed and legacy inference, including on the ship.
61−
62−Imported Hoon `(unit T)` now converts to the validated canonical prelude `unit` when that template is supplied, instead of remaining an incompatible collection. Conversion recurses through imported unions and collections, and API path/diff/poke analysis uses the same prepared reader. The fixtures prove identity, `fall`, `need`, `(unit @t)` casts, union- and list-nested matching, canonical unit-typed API full/diff marks and a canonical direct-poke export while preserving the no-prelude compatibility report and wrong-collection rejection. Nested public re-export labels also remain `ask`, `qath` and `raw-poke` instead of leaking their private `.internal` suffixes into printed types.
63−
64−Uncontextual `?-` result joining now uses one rule for loobean, unit, list and known-union branches: unify and retain substitutions first, then widen only to an explicitly present parent aura or `@`. Multi-arm folds select an explicitly present parent independently of arm order and bind variables to that final parent; deferred boolean branches retain their pending-literal fallback, and sibling auras remain distinct without a present common parent. Valid recursive local branches that were rejected by the old per-kind screens now infer, while pending tags and distinct type variables retain definite diagnostics.
65−
66−The component-local program recovery now covers update, subscriptions, one direct keyed `each`/`turn` mapper and its view, then the existing initializer and ordinary `main` path. Each recovered scheme is closed and freshly allocated; non-gate views decline safely. Canonical `element` recursion and exact singleton-case list fits are narrowly guarded, with successful ordinary fits taking precedence. The byte-identical unchanged todo now passes both detailed and legacy full-module checks with an exact closed `main` type and structural downstream import. Wrong models, messages, results, mappers, keys, aliases, non-gate views and watches fail closed. This is static checking only: no Jibb execution or runtime watching is claimed.
67−
68−The API path analyzer can retain its source, complete prepared prelude, reader results and resolved dependencies as evidence, and classify a unique declaration as watchable, not watchable or unknown. This remains declaration evidence rather than proof about an arbitrary request value. The narrow direct-program check above composes it with final value syntax, resolved imports and merged evidence for one plain request. Prepared artifacts and reader results remain trusted host inputs.
69−
70−For a unique supported path declaration, the request-parts analysis derives ordered typed path parameters, a full-state reply sample and a fold type for one diff mark. Multiple diffs and unsupported or ambiguous evidence fail closed. By itself it does not create request gates or establish watchability of values.
18+The 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.
7119
72−A separate supporting-definition analysis infers supported ordinary API molds and values and resolves all declared marks, retaining their source and dependency evidence. It fails closed on unsupported helpers or marks; unused `/-` cores are not independently validated, and definitions depending on derived gates remain unsupported. This does not check or export the whole API.
20+Decisions 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.
7321
74−Ordinary imports can infer derived request-gate types for multiple supported API paths. A case may take one typed segment before the reply or one diff fold after it; the unchanged todo API's plain, typed and diff requests infer, including a named closed fold. Checked ordinary API definitions, mark molds and a supported generic poke command helper are exported. Each `/sur` core must have a directly used, successfully read mold; unselected bindings are not independently validated. Jibb module imports, scry paths, multiple parameters or diffs and a parameter together with a fold remain unsupported. Source-qualified request evidence and exact trusted graph inputs survive transitive imports and cached interfaces, while stale or ambiguous evidence fails closed. This is a type-only interface: request execution, schema validation and proof that a request value is watchable remain unimplemented. In one loaded-machine run, the real-todo eval took 195.83 s wall and 67.83 s user CPU; the prior prototype took 111.81 s wall and 64.60 s user. Both include Hoon compilation and reader setup and overlapped other work, so they are not isolated checker benchmarks.
22+## Reading the tables
7523
76−The Hoon reader's tagged-union source proof also handles `$~` default wrappers. A shared eval and ship golden exercises the unmodified Tlon `epic.saga` mold as a named payload in a labeled downstream extension, alongside overlap, recursive, shadow and malformed-wrapper controls. The tagged-source helper peels at most four consecutive defaults; defaults inside dependency proofs spend the existing semantic-node budget. Other unverified nested unions and dependencies remain unsupported.
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)).
7727
78−The repository spec records the subsequent type-system and prelude decisions, including the chosen `like` result-mapping gate; those changes also need synchronization to the Claude document. An initial inference fragment and a standalone Hoon type reader are being tested. The fragment explicitly reports that it does not check a module; partial bridges pass Hoon `*` in supported nonrecursive molds, selected Hoon atoms, term singletons, the null singleton, the two loobean singletons and their exact fork, nested faced or unfaced cells, supported disjoint unions and opaque standard collections from `/sur` molds and marks into inference. Collections retain their names and supported arguments for printing and unification; nested supported union arguments are retained too. The bridge trusts unchanged results from the source-aware reader; a materialized type graph alone cannot reveal cases Hoon already collapsed. The source-validated standard prelude `list` mold shares this representation with imported lists; other Jibb-written collection molds and most prelude collection operations remain unsupported; malformed names and arities fail closed. Selected self-recursive `/sur` molds, including Tlon `notes.import-node` with list-wrapped self references, cross as opaque module-and-name identities; aliases, foreign references, recursive marks, unfolding and construction remain unsupported. The reader handles mark samples, including a source-proved nonrecursive union from a single Ford-imported `/sur` core, recursive molds whose origins can be verified through Ford imports, nested collections, direct ordered maps, including source-validated named operands such as Tlon `notes.log`, certain ordered-map fields, direct `$^` unions whose cases can be proved disjoint, and one verified explicit union argument in a list, set, map or unit. Tagged `$%` cases can additionally use restricted local named payload molds, bare `~` fields and one level of local named tagged unions, as in real Tlon `notes`, with bounded source proof; unsupported or ambiguous dependencies fail closed. Ambiguous recursive origins fail closed; recognizable explicit unions are checked from source before Hoon can collapse their cases, as @iko confirmed for imported `$%`, `$?` and `$^`, while other nested unions, nested ordered maps, general union disjointness and complete import integration remain unfinished. Opt-in structured reader APIs preserve successful graphs and distinguish definite unsupported-aura and core evidence from failures the reader cannot prove; unverified union disjointness and name-only vase recognition remain unsupported. They revalidate and re-walk failed types. An opt-in partial checker entry point consumes unchanged reader results and reports definite aura or core errors at imported mold use sites when their inputs are unique. Ordered replay covers nested cell samples, record and function casts, and non-generic same-module aliases; unsupported prefixes, cycles and shadowing stop it. Union molds, generic applications, transitive modules and unsupported reader outcomes remain generic. Replay repeats inference and may add work. The partial checker resolves a subset of ordinary library imports in dependency order using supplied Jibb sources and a source-derived partial prelude interface, caches completed interfaces per run, detects missing sources and cycles, and resolves nested fields of imported values with independent scheme instantiation. The source-backed internal prelude defines `poke` and the public prelude re-exports it as a transparent type. A dedicated trusted preparation path supplies private comparison and arithmetic schemes to the Jibb-written `gth`, `add` and `dec` wrappers; ordinary imports cannot access them. The public `add` and `dec` wrappers use private arithmetic interfaces; supported inference preserves the shared atom constraint that excludes loobeans. Primitive execution, jet recognition and length remain unfinished. The partial checker resolves its supported source shape and rejects ordinary imports of the private path. An imported API with one mark and a matching direct `+$ poke` declaration can export a constructor and retain agent/mark metadata when the representation has the supported agent case. A separate partial analysis resolves supported API path declarations and their full and diff mark types, including the todo paths; it does not by itself create requests or check an API module. Ordinary imports additionally infer the supported multi-path request-gate types described above. Complete private module checking, other API shapes, request lowering, root API and kind checking, stores, complete `ask` and `pure` checking and runtime effects remain unfinished. A possible store or root API with `+$ poke` reports unsupported kind or scope, while definite duplicates and unrelated shadowing still report conflicts. The prelude includes the doc-exact generic `cmd` union; the prelude inventory is incomplete. The inference fragment supports unrestricted `@`, selected one-way widenings including aura-family ancestors, generalized atom constraints arising from explicit capitals or bare sample binders, acyclic local value definitions with captures, selected single self-recursive top-level and local gates, simple and nonrecursive generic mold aliases, selected faced record casts and field reads, and contextual tags, `~` and constructors for closed disjoint unions, including direct nonrecursive generic unions and propagation through complete loobean and unit-shaped branches in casts and known union-sample calls, including nested branches. Known loobean result context also propagates through supported complete branches and binder-only cell arms; binder-only arms over union subjects remain unsupported. A directly known named union can instantiate an unconstrained generic gate sample with its origin, generic arguments and faces preserved; unnamed, pending, recursive and variable-bound cases remain unsupported. A known gate with an unresolved result variable can receive a known enclosing result type before its arguments are inferred; unknown calls and unresolved targets remain conservative. Multi-argument calls form a right-nested sample, retain known faces and shared type variables, and can use known sample positions to contextualize list and union arguments. A definite mismatch points to the failing argument when the fragment can establish it, otherwise to the combined sample; unsupported contextual forms still fail closed. For a supported recursive gate, the checker infers the sample first and uses its exact type, including field faces, for one monomorphic self reference. It generalizes after the body is checked; subsequent uses instantiate it independently. Incompatible recursive arguments can report the gate and argument sites. For a complete loobean branch with one direct self-call arm, a separately inferred closed base type can seed the recursive result before the whole body is checked. Open or pending base types do not seed it; other branch shapes remain subject to the fragment’s existing limits. A supported single local recursive gate also uses a monomorphic self reference and generalizes variables free of the enclosing environment after checking its body; captured variables remain shared. The checker collects written capitals per `++` before inference, excluding nested definitions: a capital used in an enclosing definition is shared with its locals even when written later, while a capital introduced only in a local definition is generalized there. Sibling locals can introduce independent capitals with the same spelling; generic mold parameters keep their own scope. Top-level groups of syntactic gates are inferred together with monomorphic placeholders and shared substitutions, then generalized only after the whole group checks; downstream uses and library interfaces instantiate those schemes independently. A dependency graph identifies groups with two iterative depth-first passes; its conservative local-reference edges can reject otherwise valid programs. Supported local mutually recursive gate groups also use shared monomorphic placeholders and generalize only after the group checks, preserving captured outer variables. A bounded dependency proof reports certain non-gate cycles through values and gates when an explicit atom or loobean result cast and simple unshadowed expressions establish the cycle. Other mixed gate/value cycles, polymorphic recursion, unresolved literal constraints and unresolved branch joins remain unsupported. Reporting repeats inference for a single recursive gate outside a group; grouped reports use the stored schemes. Its performance cost remains unmeasured. A single-arm cell pattern accepts two or more binders, the last capturing the remaining tail; duplicate and shadowed binders are rejected. A structured single-arm pattern also works for a known non-union cell when coverage is proven, including nested literal and wildcard positions. Intermediate union or collection tails, nested patterns, wildcards and faced records remain unsupported. String interpolation accepts known atom auras, unrestricted `@`, tapes and isolated decimal literals; a known cell asks for a printer, and an explicitly generic atom asks for an aura. Loobeans, term singletons, non-tape collections, open types and a type fixed only later remain unsupported. A known closed union with two or more arms supports patterns that provably cover or exclude each remaining case, including payload binders, imported and generic cases, and binder-free catch-alls. Partial boolean patterns can split known `?` positions into their two noun values, up to 64 alternatives across the union; binders retain their original case type. Missing alternatives and covered arms are reported. Other partial patterns, expansions above the limit, binders spanning distinct cases, differing arm result types and some complex two-arm subjects remain unsupported. A cast or known call sample can supply result context through whole-case arms and supported finite loobean refinements for a known union accessed by a wing, a grouped wing or a supported shallow call, including nested cell and list positions; other partial-pattern contexts and subject forms remain unsupported. The Grammar’s `step` block infers in this fragment, but its module is not yet checked. A bare tag proved absent from a known union reports the union and tag sites in casts, single-argument calls, unit payloads, list items and supported branch arms; imported unnamed unions print their cases. Ordered fit replay can identify a missing tag nested in a syntactic tuple, stopping at an earlier mismatch or uncertainty. Known faced records support uniquely named field changes, including nested wings, with field context passed to replacements and the original record type retained. Missing fields, empty changes and definite mismatches report sites; the expected-type site is the edit because the original field declaration location is not retained. Unknown or partly unfaced spines, ambiguous fields and repeated edits remain unsupported. A known record cast supplies field context to its tuple or record initializer, including nested list and union fields; mismatch diagnostics use the cast mold because the original field declaration location is not retained. Isolated cart-style `init` and `update` expressions infer, while the complete cart-store fails closed because its kind and declaration scope remain unchecked. Uncontextualized list literals infer a fresh element type, including empty and nested lists, with independently generalized uses. Unresolved item tags and uncertain widening remain unsupported. Backtick unit construction uses the validated standard prelude unit template, infers its payload without losing pending constraints, and makes the prelude’s `some` available. Ordinary result annotations also let its `bind`, `biff`, `both`, `clap`, `clef` and `flit` infer. A known unit in a cast, call, list item or record field supplies context to its payload, including nested units and lists; mismatches identify the payload and context. Unrelated union identities, some variable-dependent fits, and missing or altered prelude unit templates remain unsupported. Literal singleton heads compare by runtime noun, so `|=%$` also matches explicit null- and loobean-zero-headed cases. When equal heads have disjoint payloads, the constructor selects a uniquely proven compatible payload; unknown and ambiguous candidates remain unsupported. Unresolved nulls remain pending and are reported separately from tags. A known union of `~` and a null-headed cell supports a complete `~` / `[~ value]` branch in either order, including shadow checks; unknown subjects, missing or duplicate arms, and unresolved branch results remain unsupported. This fragment infers the prelude’s `fall` and `need` signatures. With the validated prelude list and a known cast or gate sample, empty, nonempty and nested list literals infer their element types, including contextual union tags; a mismatched element names both sites. In that context `~` and zero-valued terms fit an empty list, and two-item unfaced cells form cons lists, including nested cons and imported-list contexts; invalid heads or tails name both sites. A known gate sample also supplies context to matching positions in a single tuple or record argument, including nested cells; zero literals can fit list positions. A bound zero constant remains unsupported rather than a definite mismatch, and an unknown callee does not supply context. Faced or longer cells and a missing or altered prelude list fail closed. A known list result also supplies context through complete loobean, unit-shaped and list-shaped branches, including recursive and nested branches. For a known standard list with a supported element type, a complete `~` / `[item rest]` branch infers the element and tail types in either arm order and checks binders for shadowing. Unknown subjects, unsupported element types and other or incomplete list patterns remain unsupported. A value with type variable `A` can fit a field whose type is that same `A`, including in generic union payloads and nested or repeated record fields. Other variable-dependent face merges remain unsupported. Forced equality of distinct written capitals now reports both source sites, following @iko’s decision; forcing one to a concrete type remains unsupported. Imported record spines with repeated faces fail closed where used, but only with a generic unsupported diagnostic. Hoon may erase unfaced nested-cell boundaries, so the check can conservatively reject valid names in distinct erased scopes. Supported closed unions print using an in-scope name or imported alias; an unnamed nongeneric union prints its cases, parenthesized when nested. The latter is print-only. Generic union types retain all arguments in their printed name; if that name is unavailable, the partial printer reports the limitation. Different import faces for the same origin remain compatible; compatibility across distinct union origins and some generic-argument comparisons remain unsupported. Nonrecursive generic aliases can reorder, repeat or omit parameters while retaining a union’s origin, including through local scopes and library interfaces. A generic union declared directly inside a body remains unsupported, as do differing-variable face constraints in a union payload. A transitive generic union whose name is unavailable is reported as unsupported instead of hiding its arguments. Unfixed decimal literals default to `@ud` in gate-free inferred types; recursive molds, general branch tag context, other constraint cases and defaulting inside gate types still need work. Collection recognition checks the originating core and fails closed on shadows or unsupported Ford subject shapes; a wrapper regression also rejects forged subjects, samples and tails. Its golden fixtures include three real Tlon files. A Clay test passes a Ford-built nested union through the reader into partial inference. The partial prelude includes `murn`, `join`, `snip`, `rear` and the agreed shared-type `clap`; supported calls infer, while backend validation remains outstanding, and [prelude-inventory.md](prelude-inventory.md) is a source audit, not the complete inventory or signatures. The milestone remains unfinished.
28+## Parser and mark
7929
80−The prelude now writes `hunt` with the ordering gate first, matching the target Hoon's `(hunt ord a b)`. Its focused golden infers both ordering outcomes and absent units, and reports mismatched unit payloads and ordering-gate samples. Execution and jet recognition remain unverified.
30+These rows cover milestone 1. The plan's three done-when criteria are the rows on the doc examples, the lexical rules and `|commit`.
8131
82−The prelude now also writes `eq` and `mate`. A dedicated constrained variable retains `A contains no gates` through nested unification, canonicalization, instantiation and imports; atom constraints remain stronger. Direct and nested gate arguments fail, while open cell, face, collection and union members receive the constraint with bounded traversal and substitution updates. `set`, `map`, `mop`, `jar` and `jug` constrain only their key positions, leaving map values independent. The shared solver guards cover existing and later gate injection, exact traversal budgets and conservative budget fallback; backend equality and crash behavior remain unverified.
83−
84−The shared prelude interface reserves every name present in the supplied vendored source and makes only supported inferred entries available, including `list`, `unit`, `same`, `fall`, `need`, `bond`, `lure`, `weld`, `snoc`, `turn` and `lent`. The validated standard `list` mold is injected when the prelude’s own gates are inferred; `weld` and `turn` have ordinary explicit result casts. An absent or altered `list` is not injected, and an altered declaration cannot leak through direct or transitive mold aliases. The same validated template is available when prelude mold aliases are prepared, so supported direct and transitive aliases can use it. Unsupported entries such as most list helpers remain reserved but unavailable; backend validation of the helpers remains outstanding. All callers use the same prelude origin, so a library can export a type containing unqualified `(unit A)` to another module. The source-only `+prepare-prelude` rejects empty, malformed, conflicting or import-bearing source; `+prepare-prelude-with-internal` also accepts the supported private internal import. Prepared values are trusted and must come unchanged from the matching preparation arm. When canonical public list or unit templates are missing or altered, independently inferred private molds remain available, while molds that depend on those templates do not. The module-scope fixture compares the prepared and source-taking paths against the real prelude and a two-module golden under eval and on the ship. The source and checker remain incomplete, so this does not establish complete shadowing coverage or a checked module.
85−
86−The prelude has a Jibb-written `succ` gate that increments through `add`; partial inference retains its arithmetic atom constraint. A Hoon translation agrees with Hoon on ten selected inputs. Jibb execution and jet recognition remain unverified.
87−
88−The prelude has Jibb-written curried `lead` and `late` pair constructors, inferred with independent argument types including gate values. Their focused golden passes under eval and on the ship, and a Hoon-reference comparison covers operand order. Jibb backend execution remains unverified.
89−
90−The prelude also has a Jibb-written `zing` that concatenates homogeneous lists via `weld`. Its focused golden infers empty, nested text, ship, generic and gate-element lists and reports a non-list error; the same golden passes on the ship. A Hoon translation agrees with Hoon `zing` on selected finite inputs, not on Jibb execution. Hoon’s raw helper additionally accepts heterogeneous noun lists, which the Jibb signature does not express. Backend lowering and jet recognition remain unverified.
91−
92−The experimental deferred constructor transaction conservatively declines general structural tuple fits, most branches, field reads, nonidentical successful call/cast fits, and multi-argument calls with open argument, sample or result types. This prevents a later substitution from invalidating an earlier face-propagation check; cases requiring deferred structural fits remain unsupported. It can retry source definitions after later dependencies become available, and a two-arm boolean branch can retain separately owned literal-result obligations until a later closed context resolves them. Faced targets or union cases, list literals and general union-pattern branches remain unsupported.
93−
94−The checked inference slice now represents `!!`, proves empty cell positions and filters proven-empty union cases. List and unit payload arms whose elements are empty are rejected as unreachable; fixed opaque cases fail closed when reachability is unknown. The new shared guard covers checked interfaces, partial diagnostics and proof budgets. Its shared guard runs under eval and on the ship.
95−
96−An eval and ship fixture now reports partial inference for the unchanged todo island with its real API and Hoon readers. It verifies that the source fixtures match `my-app` and exercises missing or duplicate imports; the report does not claim the module or island has been checked. The prelude also has a Jibb-written recursive `lent` whose supported generic calls infer `@ud`. Execution and shape-based jet recognition remain future backend work. Nested union tests check equal runtime nouns, different nested tags, empty fields and unknown inhabitation.
97−
98−The prelude now writes `lth`, `gte` and `lte` in Jibb using `gth` and `not`. Supported generic and concrete calls infer, including loobeans; mismatched explicit auras fail. Execution, jet recognition and complete import checking remain unfinished.
99−
100−The prelude also writes `trip` and `tuba` over private primitives, with inferred cord, tape and UTF-32 list types matching the target ship's Hoon 135 definitions. Their composition with `lent` and invalid argument controls pass under eval and on the ship; primitive lowering, execution and jet recognition remain unfinished. In the unchanged todo report, `update` now reaches its remaining branch-context limitation instead of failing on missing text names.
101−
102−The Hoon reader can prove overlaps among supported original `$?` source cases, including nested cells and unions with more than two cases, and report them at a Jibb use site. It evaluates each case independently and compares runtime noun values. Other overlaps, Hoon case locations and mark-reader overlap diagnostics remain unfinished. The source screen allows at most 128 cases and 4,096 source noun nodes; dependency checking and pairwise witness analysis each have a separate 4,096-node budget. These budgets do not bound chapter lookup, Hoon evaluation or graph walks.
103−
104−Restricted-number promotion now skips an environment scan when a definition has no written capitals. In a single startup-inclusive pair on 2,000 independent gates, output was identical and user CPU fell from 71.67 to 38.26 seconds; wall time was 72.80 versus 51.66 seconds with other checks running. This is a partial-inference measurement, not a complete checker or a bound on dependent modules.
105−
106−## Milestone 1: parser and mark
107−
108−What the plan asks for, and where it is:
109−
110−| The plan | Where |
111−| --- | --- |
112−| The `%jibb` mark as the first tab gives it | `jibb-dev/mar/jibb.hoon`, as the doc writes it |
113−| The layout pass, emitting INDENT, DEDENT and NEWLINE | `+layout` in `jibb-dev/lib/jibb.hoon`, designed in its section 2 |
114−| A parser for the Grammar tab's EBNF that returns a syntax tree with source positions | `+parse` and `+parse-tokens`, section 3. Every node has a span, its start and end, and `+check-spans` tests the spans of every tree the golden tests print |
115−| Errors with file, line, column and an excerpt | `+show-error`, section 4.3. Each error points at the first character where the text stops being the start of any valid module (section 2.0) |
116−| Done when every Jibb code block in the doc parses | The doc labels its 14 Jibb blocks `jibb`. Each is a golden case, `tests/golden/doc-*`, and `tools/doc-blocks docs/spec` checks that they match. All parse; the one block written as an error, the Grammar's buttons example, has a type error for milestone 2 |
117−| Done when each lexical rule has a test input that breaks it | The `lex-*` golden cases: for each lexical rule, inputs that break it (`-bad-`), each with the error's expected place, and inputs that keep it (`-ok-`), except for the forms Jibb leaves out (the closers, blob and `@c` literals) |
118−| Done when `\|commit` stores `.jibb` files on a fake ship | `tools/ship check-commit`: 7 checks, from reading every file back byte for byte to three-way merges |
119−
120−Besides the plan's list:
121−
122−- 689 golden cases: 460 that parse and 229 that fail, each failure at a stated line and column. One failing case has an unclear expectation (corpus question 3). The newer type-output cases exercise only the partial inference fragment. Each case's `about.txt` quotes the doc's words it tests.
123−- The 689-case corpus passed under `urbit eval` in 107.0 s while other checks were running. The fake ship passed all 746 tests, including the source-overlap, structural-overlap, generic-union source and alias-overlap, full-module overlap, deferred-context, generic-recursion, generic-construction, generic-pattern, deferred-inference, empty-mold and cell-branch fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 111.2 s and the ship's `-test` run took 316.7 s. The importer golden compares 221 projections; `tools/clay-fixtures` builds the example Hoon fixtures through Clay, checks a recursive Ford import's origin, and passes Clay-built types through the Clay-built importer and partial checker.
124−- `tools/testdata/selftest` (23 checks) and `tools/testdata/ship-selftest` test the tools themselves.
125−- Two independent audits before 7c739b7, one of which 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.
126−- Speed: starting `urbit eval` and building the library takes about 27 s with the dev tools' `!:`, and 24 s without it (`tools/hoon --no-debug`). After that, a 2,000-line module of 400 definitions parses in about a second. Loops over definitions, arms, lines and items grow no stack; nesting costs a few stack frames a level, and 100,000 nested brackets still parse (library section 3).
127−
128−### History
129−
130−| Commit | Date | What |
32+| Area | Status | Proved by |
33+| --- | --- | --- |
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 |
51+
52+Two 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.
53+
54+## Types and prelude: full-module checks
55+
56+| Area | Status | Proved by |
57+| --- | --- | --- |
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 |
83+
84+## Types and prelude: requests and API analysis
85+
86+| Area | Status | Proved by |
87+| --- | --- | --- |
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) |
102+
103+## Types and prelude: checker
104+
105+### Atoms, literals, holes and capitals
106+
107+| Area | Status | Proved by |
108+| --- | --- | --- |
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) |
119+
120+### Records, lists and units
121+
122+| Area | Status | Proved by |
123+| --- | --- | --- |
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/) |
139+
140+### Unions and patterns
141+
142+| Area | Status | Proved by |
143+| --- | --- | --- |
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/) |
161+
162+### Gates, recursion and imports
163+
164+| Area | Status | Proved by |
165+| --- | --- | --- |
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-*` |
177+
178+### Bounded and experimental routes
179+
180+| Area | Status | Proved by |
181+| --- | --- | --- |
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) |
194+
195+## Types and prelude: prelude
196+
197+| Area | Status | Proved by |
198+| --- | --- | --- |
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 |
231+
232+## Types and prelude: Hoon importer
233+
234+| Area | Status | Proved by |
235+| --- | --- | --- |
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/) |
254+
255+## Desks and tools
256+
257+| Area | Status | Proved by |
131258| --- | --- | --- |
132−| 1cb51df | 2026-10-29 | Foundation: the parser's design, the tools, the desks, the vendored base-dev and landscape files, the golden corpus |
133−| 15a5545 | 2026-10-29 | The layout pass |
134−| 3c5f50a | 2026-10-29 | The parser |
135−| 7c739b7 | 2026-10-30 | Fixes from two independent audits; milestone 1 done |
136−| 5a4aa73 | 2026-10-30 | `tools/doc-blocks`, after the doc labelled its Jibb blocks |
137−| ab797a9 | 2026-10-30 | The 12 grammar decisions of 2026-10-30: four changed the parser, eight confirmed it |
138−| aad6ddb | 2026-10-30 | Drop `$?`; `+$` takes union cases below its name |
139−| 1dd92a6 | 2026-10-30 | Begin type inference and Hoon imports |
140−| 51ce4d9 | 2026-10-30 | Extend partial inference and importer, record type and prelude decisions |
141−| be6d2a5 | 2026-10-30 | Add atom widening, nested collections and case-local Hoon import fixtures |
142−| 26554ac | 2026-10-30 | Infer an atom constraint, extend the prelude and read example molds through Clay |
143−| fbeaa83 | 2026-10-30 | Extend atom constraints and nested ordered-map imports; connect Clay types to partial inference |
144−| 47a1f49 | 2026-10-30 | Read validated Ford imports, widen aura families, and show both sites of selected errors |
145−| bd37989 | 2026-10-30 | Read mark samples and test partial mark imports; reject unproven nested `$^`; preserve atom constraints through aliases |
146−| 2d5deb2 | 2026-10-30 | Default gate-free decimal types, validate named Hoon mold lookup, and isolate fixture failures |
147−| 1b7dbae | 2026-10-30 | Infer acyclic local definitions and parse case-local Jibb module fixtures |
148−| 8b9c9ac | 2026-10-30 | Preserve recursive import origins, infer simple local molds, and supply Jibb module sources to the partial checker |
149−| 529736a | 2026-10-30 | Infer supported library import graphs and guard nested Hoon `$^` in collections |
150−| 8bf1b12 | 2026-10-30 | Infer selected record faces and check nested `$^` in static Hoon records |
151−| d8ac47d | 2026-10-30 | Cache library interfaces, preserve imported Hoon record faces, and check nested tagged unions |
152−| edd9277 | 2026-10-30 | Infer nonrecursive generic mold aliases with lexical parameters |
153−| 4406f6f | 2026-10-30 | Resolve selected contextual tags and check explicit imported unions |
154−| 5c73614 | 2026-10-30 | Print supported named and escaping union types |
155−| 0070584 | 2026-10-30 | Propagate union context through loobean branches, read selected unions in Hoon collections, and add `flit` |
156−| 250564c | 2026-10-30 | Infer selected named generic unions, test Hoon collection wrappers, and add list helpers |
157−| e95ef8f | 2026-10-30 | Bridge selected Hoon unions into partial inference and support generic union aliases |
158−| 56a899f | 2026-10-30 | Infer matching variable types in faced fields and bridge opaque Hoon collections |
159−| 4d45d2f | 2026-10-30 | Resolve selected contextual null literals |
160−| e878edc | 2026-10-30 | Infer complete unit-shaped branches and bridge selected recursive Hoon molds |
161−| 743dfd8 | 2026-10-30 | Propagate union context through unit-shaped branches |
162−| 3f90fa8 | 2026-10-30 | Share a partial prelude interface across module inference |
163−| 29bd39f | 2026-10-30 | Infer contextual list literals and validate prelude parity |
164−| a2a6ef5 | 2026-10-30 | Infer complete list-shaped branches |
165−| 671fe72 | 2026-10-30 | Infer contextual list nulls and cons cells |
166−| 7e69436 | 2026-10-30 | Infer selected self-recursive gates |
167−| 9ab52e8 | 2026-10-30 | Infer recursive branches with closed base types |
168−| d782b45 | 2026-10-30 | Propagate list context and apply settled type decisions |
169−| c7082e0 | 2026-10-30 | Infer multi-argument calls |
170−| 918acbd | 2026-10-30 | Infer recursive gates from their samples first |
171−| 1470d18 | 2026-10-30 | Infer selected prelude list helpers |
172−| 10cbf9c | 2026-10-30 | Infer selected local recursive gates and distinguish reader diagnostics |
173−| 45afb13 | 2026-10-30 | Infer local capital scopes and report direct reader diagnostics |
174−| 054e651 | 2026-10-30 | Report nested reader diagnostics |
175−| 98c19cd | 2026-10-30 | Infer known-aura string interpolation |
176−| ddba633 | 2026-10-30 | Infer top-level mutually recursive gates |
177−| 9f1517e | 2026-10-30 | Infer whole-case union patterns and prelude `turn` |
178−| 9dd35c8 | 2026-10-31 | Match finite boolean refinements of union cases |
179−| 54852d4 | 2026-10-31 | Contextualize tuple calls and infer known record changes |
180−| 0bc5113 | 2026-10-31 | Contextualize record initializers and infer unit construction |
181−| 264a436 | 2026-10-31 | Contextualize unit payloads in casts, calls and nested values |
182−| a140383 | 2026-10-31 | Report missing union tags and infer prelude unit helpers |
183−| d69cc52 | 2026-10-31 | Infer longer cell binder patterns and prelude unit helpers |
184−| ae35005 | 2026-10-31 | Import source-verified tagged Hoon unions |
185−| c8f894a | 2026-10-31 | Report nested missing tags and contextualize union branch results |
186−| ef2ea71 | 2026-10-31 | Import Hoon null singleton cases |
187−| 67f900e | 2026-10-31 | Infer local mutual gates and uncontextualized lists |
188−| 7ff15f1 | 2026-10-31 | Contextualize finite union patterns and record the initial poke decision |
189−| c790a9f | 2026-10-31 | Expose transparent `poke` from the internal prelude |
190−| ef4772a | 2026-10-31 | Bridge imported loobeans and loobean singletons |
191−| ad46655 | 2026-10-31 | Bridge selected imported any-noun molds |
192−| beada10 | 2026-10-31 | Import source-proved Ford mark unions, analyze API paths and infer list helpers |
193−| e28f7be | 2026-10-31 | Diagnose proven non-gate cycles and import Tlon null-payload union cases |
194−| fd2f288 | 2026-10-31 | Infer qualified fields of imported values |
195−| ed9291e | 2026-10-31 | Infer term-headed pairs and function helpers, and import nested named unions |
196−| ad0265e | 2026-10-31 | Infer proven single-case patterns and the prelude command union |
197−| 413b12b | 2026-10-31 | Propagate known result context into generic calls and batch ship deletions |
198−| c690076 | 2026-10-31 | Propagate loobean context, infer predicate helpers, and import named ordered-map operands |
199−| 0bf6178 | 2026-10-31 | Bridge recursive Tlon lists and prepare a private comparison interface |
200−| 4e472b5 | 2026-10-31 | Pass known named unions through polymorphic gates |
201−| e3e184f | 2026-10-31 | Parse type holes, reject duplicate written record fields, and extend partial union inference and imports |
202−| 80e221a | 2026-10-31 | Infer supported annotation holes and prelude list aliases |
203−| ba1fec4 | 2026-10-31 | Add the curried `bond` prelude gate |
204−| 0ea700d | 2026-10-31 | Infer a source-defined recursive `qath` subset and record the explicit `proj` decision |
205−| 75f5952 | 2026-10-31 | Check a subset of explicit `proj` calls and retain their lowering evidence |
206−| cf17925 | 2026-10-31 | Infer supported single-field projections |
207−| 1a891e2 | 2026-10-31 | Infer source-backed addition and decrement without loobean operands; record the watchability decision |
208−| 81af5fd | 2026-10-31 | Preserve public names of identity-generic union aliases and record the `like` decision |
209−| 640a442 | 2026-10-31 | Add the source-backed `like` result mapper and infer supported positional calls |
210−| 445a0a1 | 2026-10-31 | Retain source-backed API path evidence and classify declarations |
211−| f69493d | 2026-10-31 | Derive supported request components from API declarations |
212−| f0f6954 | 2026-10-31 | Analyze supported API helper definitions and declared marks |
213−| 3f55af7 | 2026-10-31 | Define source-backed transparent ask and pure |
214−| ae1ec26 | 2026-10-31 | Prove selected default-wrapped Hoon unions from source |
215−| dde791c | 2026-10-31 | Infer a source-backed request-gate type through ordinary imports |
216−| a1c5f35 | 2026-10-31 | Infer supported multi-path requests and named closed folds |
217−| 911ca0c | 2026-10-31 | Propagate union context, define subscriptions and match literal nouns |
218−| 72acdb3 | 2026-10-31 | Infer selected nested union payloads from context |
219−| 706035c | 2026-10-31 | Analyze gate-free source molds with field witnesses |
220−| 651b8ec | 2026-10-31 | Match source-proven gate samples in direct calls |
221−| cc8e389 | 2026-10-31 | Add source-backed list length and real todo regression |
222−| 4da6891 | 2026-10-31 | Add source-backed comparisons and nested Hoon union controls |
223−| 09db390 | 2026-10-31 | Skip unnecessary inference environment scans |
224−| 179d717 | 2026-10-31 | Diagnose source-proven Hoon union overlaps |
225−| 142f2e2 | 2026-10-31 | Prove structural overlaps across Hoon union cases |
226−| c96597d | 2026-10-31 | Track source-proven generic recursive identities |
227−| 190a9d5 | 2026-10-31 | Add source-backed list flattening |
228−| d9d51e6 | 2026-10-31 | Check source-proven recursive tree construction |
229−| 30b0a9e | 2026-10-31 | Match source-proven recursive tree cases |
230−| 72d85ab | 2026-10-31 | Add bounded deferred inference and expand runtime equality coverage |
231−| 22f3788 | 2026-10-31 | Check empty molds and propagate closed cell context into branches |
232−| 341bcb4 | 2026-10-31 | Keep deferred fits stable under later substitutions |
233−| b93a94b | 2026-10-31 | Prove local generic-alias union tags and add successor |
234−| 2826c93 | 2026-10-31 | Report generic-alias overlaps and retain deferred branch contexts |
235−| b5cdc80 | 2026-10-31 | Preserve full-module overlap source evidence |
236−| ab6fdc1 | 2026-10-31 | Add source-backed text conversion wrappers |
237−| aa277c9 | 2026-10-31 | Recover prepared tuple initializers in partial reports |
238−| b4703e7 | 2026-11-01 | Check narrow closed subscription-free program mains |
239−| 26bf7a7 | 2026-11-01 | Recover narrow direct-program initializer contexts |
240−| 642d2c0 | 2026-11-01 | Prove direct request-value watchability for program subscriptions |
241−| 2e4d582 | 2026-11-01 | Add the source-backed UI, program and page prelude slice |
242−| a163965 | 2026-11-01 | Recover direct-program update result contexts |
243−| 46748b0 | 2026-11-01 | Check the unchanged todo island through component recovery |
244−| 1e17d5f | 2026-11-01 | Check static and direct data-page mains |
245−| 0517053 | 2026-11-01 | Add the theme mold and require explicit unit syntax |
246−| This change | 2026-11-01 | Check the unchanged cart store and basket |
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 |
267+
268+## Gaps
269+
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.
247281
248282## Checking it
249283
250−On a machine set up as [development.md](development.md) says:
251−
252−```
253−tools/golden # 660 cases under urbit eval
254−tools/test-arms # the my-app copies, then every tests/lib suite under urbit eval
255−tools/test-arms --list # the suites and their arms; ", report" marks a golden report
256−tools/test-arms --report jibb-import # print a golden-report suite's report
257−tools/test-arms --update jibb-import # write it to the suite's expected file
258−tools/test-arms jibb-import # the Hoon importer fixture projection
259−tools/test-arms jibb-import-default # default-wrapped source proof golden
260−tools/test-arms jibb-bridge # the importer/checker bridge fixture
261−tools/test-arms jibb-import-overlap # source-aware Hoon overlap and provenance fixture
262−tools/test-arms jibb-import-structural # structural overlap and multi-case source fixture
263−tools/test-arms jibb-union-source # local generic-alias union guards
264−tools/test-arms jibb-union-alias-overlap # local generic-alias overlap diagnostics
265−tools/test-arms 'jibb-full-overlap-*' # full-module overlap evidence, in two suites
266−tools/test-arms jibb-tlon-bridge # the real Tlon reader/checker fixture
267−tools/test-arms jibb-mark-bridge # the mark/checker bridge fixture
268−tools/test-arms jibb-poke-bridge # the source-backed poke/API fixture
269−tools/test-arms jibb-api-evidence # API declaration evidence guards
270−tools/test-arms jibb-api-paths # partial API path metadata fixture
271−tools/test-arms jibb-hole-guards # hole defaulting and API interface guards
272−tools/test-arms jibb-list-alias-guards # prelude list-alias guards
273−tools/test-arms jibb-generic-alias # generic union alias guards
274−tools/test-arms jibb-generic-recursion # source-proven generic recursion guards
275−tools/test-arms jibb-generic-construction # source-proven recursive construction guards
276−tools/test-arms jibb-generic-pattern # source-proven recursive pattern guards
277−tools/test-arms jibb-deferred # source-owned deferred inference guards
278−tools/test-arms jibb-deferred-resolver # resolver consistency and failure guards
279−tools/test-arms jibb-deferred-context # deferred source-order and branch guards
280−tools/test-arms jibb-deferred-prepared # prepared initializer reports and failure guards
281−tools/test-arms jibb-empty # empty molds and coverage guards
282−tools/test-arms jibb-cell-branch # branch context and rollback guards
283−tools/test-arms jibb-positional-face-guards # positional sample face guards
284−tools/test-arms 'jibb-qath-*' # qath source and unfolding guards, in two suites
285−tools/test-arms jibb-ask-guards # ask source and bootstrap guards
286−tools/test-arms jibb-proj-guards # projection evidence and scope guards
287−tools/test-arms jibb-buttons # documented buttons schemes and exact pending-tag error
288−tools/test-arms jibb-theme # byte-identical real theme, exact type and rejection guards
289−tools/test-arms jibb-module-scope # module and prelude scope fixture
290−tools/test-arms jibb-program-main # closed program-main interface and rejection guards
291−tools/test-arms jibb-program-init # transactional direct-program initializer context guards
292−tools/test-arms jibb-program-update # transactional direct-program update context guards
293−tools/test-arms jibb-program-watch # direct request-value watchability guards
294−tools/test-arms jibb-todo-full # byte-identical full todo and rejection guards
295−tools/test-arms jibb-check-spans # the span checker catches planted wrong spans
296−tools/test-arms jibb-hoon-reference # Hoon translations of zing, lead, late and succ agree with Hoon's
297−tools/testdata/selftest # the tools themselves
298−tools/doc-blocks docs/spec # the doc's examples are golden cases
299−tools/ship start
300−tools/ship test # the same 660 cases, and every tests/lib suite, as -test arms on the ship
301−tools/testdata/ship-selftest
302−tools/ship check-commit # |commit stores .jibb files
303−tools/clay-fixtures # example /sur files and marks build through Clay
304−```
305−
306−`tools/test-arms` runs the `test-` arms of the `tests/lib` suites under eval, and `tools/ship test` runs the same arms on the ship. [The test suites](development.md#the-test-suites) in development.md says what each suite checks. `tools/check` runs them in four shards balanced by measured cost, `arms-1` to `arms-4`; `tools/check --list` prints its checks, and `tools/test-arms --shard 2/4 --list` the suites in one shard. Where a comment above says byte-identical, the suite reads a copy of the `my-app` file kept under `tests/`. `tools/test-arms --copies`, and `tools/test-arms` with no suite or shard named, check that every copy listed in `tests/my-app-copies.txt` still matches its source; naming a suite skips that check.
307−
308−## What milestone 1 leaves to later milestones
309−
310−- Errors carry a start only. Spans keep each node's end so that milestone 2's type errors can underline both conflicting sites with excerpts (library section 1).
311−- The parser accepts forms for the checker to judge: `[]`, `[a]`, `m()`, `!! a`, and the module kinds. `[]` and `m()` have since been decided to be errors, and `[a]` is `a`; the parser has not changed. The Grammar's buttons example parses, though the doc marks it as a type error.
312−- Grammar questions the doc's author hasn't been asked follow the readings in [open-questions.md](open-questions.md).
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.