179d717 · jibb · git.iko.soy

README.md+1−1

compare with master

unifiedsplit

@@ -42,7 +42,7 @@ tools/hoon '(golden /a/b/jibb (crip "++ main view"))'

42tools/hoon --raw --cord src=tests/golden/foo/source.jibb 'tree:(golden /a/b/jibb src)'

43```

44

45−`tools/testdata/selftest` tests both tools against a stub library, and `tools/doc-blocks` against Markdown it writes. `tools/importer-test` compares the partial Hoon importer's fixture projections against their golden file. `tools/type-import-test`, `tools/type-tlon-test`, `tools/type-mark-test`, `tools/type-poke-test` and `tools/type-api-paths-test` check importer/checker, prelude and partial API path analysis boundaries under eval; the ship suite runs the same fixtures.

45+`tools/testdata/selftest` tests both tools against a stub library, and `tools/doc-blocks` against Markdown it writes. `tools/importer-test` compares the partial Hoon importer's fixture projections against their golden file. `tools/type-import-test`, `tools/type-import-overlap-test`, `tools/type-tlon-test`, `tools/type-mark-test`, `tools/type-poke-test` and `tools/type-api-paths-test` check importer/checker, prelude and partial API path analysis boundaries under eval; the ship suite runs the same fixtures.

46

47### The doc's examples

48

docs/compiler.md+3−1

@@ -98,7 +98,9 @@ Self-recursive `/sur` molds can cross the bridge as opaque module-and-name ident

98

99The partial checker also recognizes a source-proven Jibb recursive mold consisting of `~` and one faced cell with a fixed-aura head and direct self tail. Its identity includes the defining path and name. It unfolds this shape for supported null and cell construction and for a two-arm null/cell match; static application-path literals use the verified public `qath` alias. The internal prelude defines `qath` as a transparent knot sequence and the public prelude re-exports it. Each inference attempt has 256 unfolding and static-segment steps; parsing and separate retries are not bounded by that limit. Dynamic application-path segments, broader patterns and other recursive shapes remain unsupported. Route and static-file existence checks remain milestone 4.

100

101−Callers that have a `/sur` core and a name can use `+read-named`: it checks for a locally declared arm before asking Hoon to evaluate the mold, and reports evaluation failures with the final Hoon trace line. `+read-mold-in` remains available when the caller already has the selected type. The opt-in `+read-named-diagnostic` and `+read-mark-diagnostic` preserve successful graphs and distinguish definite `%invalid` aura and core evidence emitted directly by the reader from `%unsupported` failures. Other failures, including unverified union disjointness and vase recognition based only on a name, remain unsupported. These entry points revalidate and re-walk failed types; the opt-in `+golden-types-with-reader-diagnostics` accepts unchanged structured reader results and reports definite aura or core errors at their imported mold use sites, when the import and supplied input are unique. Ordered replay covers direct and nested cell samples, record and function casts, and non-generic same-module aliases; it stops at an unsupported prefix, cycle or shadowing failure. Union molds, generic applications, transitive modules and unsupported reader outcomes still report generic limitations. Replay repeats inference and may add work; this entry point remains partial. Existing checker entry points continue treating failed imports as unsupported. It also fails closed on repeated field faces along an imported record spine, including recursive roots; the diagnostic remains generic. Hoon type graphs can erase unfaced nested-cell boundaries, so the check may conservatively reject a valid source with equal names in distinct erased scopes. Faced nested records and union alternatives keep separate scopes.

101+Callers that have a `/sur` core and a name can use `+read-named`: it checks for a locally declared arm before asking Hoon to evaluate the mold, and reports evaluation failures with the final Hoon trace line. `+read-mold-in` remains available when the caller already has the selected type. The opt-in `+read-named-diagnostic` and `+read-mark-diagnostic` preserve successful graphs and distinguish definite `%invalid` evidence emitted directly by the reader from `%unsupported` failures. Other failures, including unverified union disjointness and vase recognition based only on a name, remain unsupported. These entry points revalidate and re-walk failed types; the opt-in `+golden-types-with-reader-diagnostics` accepts unchanged structured reader results and reports definite aura, core or proven union-overlap errors at their imported mold use sites, when the import and supplied input are unique. Ordered replay covers direct and nested cell samples, record and function casts, and non-generic same-module aliases; it stops at an unsupported prefix, cycle or shadowing failure. Union molds, generic applications, transitive modules and unsupported reader outcomes still report generic limitations. Replay repeats inference and may add work; this entry point remains partial. Existing checker entry points continue treating failed imports as unsupported. It also fails closed on repeated field faces along an imported record spine, including recursive roots; the diagnostic remains generic. Hoon type graphs can erase unfaced nested-cell boundaries, so the check may conservatively reject a valid source with equal names in distinct erased scopes. Faced nested records and union alternatives keep separate scopes.

102+

103+For a narrow two-case Hoon `$?`, the reader can prove an overlap from the original source: both cases must have the same literal head, an intersecting singleton in the next position, and an `@t` tail. It evaluates and projects both branches independently, comparing noun values rather than aura or literal spelling. This proves collisions such as `%$` against `?`; unknown shapes remain unsupported. Distinct literal head tags can also establish disjointness in supported `$?` source cases. The overlap diagnostic points to the Jibb use, since the source case positions are not available. This is not yet a general imported-union check or a mark-reader overlap diagnostic. The overlap proof has a 4,096-node dependency budget. The new `$?` case screen separately permits at most 128 cases and 4,096 source noun nodes; the older `$%` screen retains its existing behavior. Chapter lookup, Hoon evaluation and type-graph walks are outside those budgets.

102

104

103The partial report can diagnose certain non-gate value dependency cycles, including cycles through gates. It requires an explicit atom or loobean result cast and a syntactically proven dependency group with unshadowed simple samples; it identifies the value and a dependency site. Untyped results, branches, nested definitions, qualified wings and complex samples remain unsupported. The proof constructs an additional dependency graph. One 24-case recursive/generic eval run took 19.7 s with it and 18.6 s before it, including startup; these single runs do not isolate the graph cost.

105The partial report can diagnose certain non-gate value dependency cycles, including cycles through gates. It requires an explicit atom or loobean result cast and a syntactically proven dependency group with unshadowed simple samples; it identifies the value and a dependency site. Untyped results, branches, nested definitions, qualified wings and complex samples remain unsupported. The proof constructs an additional dependency graph. One 24-case recursive/generic eval run took 19.7 s with it and 18.6 s before it, including startup; these single runs do not isolate the graph cost.

104

106

docs/development.md+2

@@ -62,6 +62,7 @@ git clone https://github.com/urbit/tools /root/src/tools

62| `tools/importer-test` | Compares the partial Hoon importer's diagnostic trees and errors with `tests/importer/tree.txt` under `urbit eval` |

63| `tools/type-import-default-test` | Compares default-wrapped union source proofs and adversarial cases under eval; the same golden runs on the ship |

64| `tools/type-import-test` | Composes the Hoon importer with the partial checker and compares `tests/type-import/expected.txt` under eval |

65+| `tools/type-import-overlap-test` | Checks source-aware Hoon union overlap, provenance and proof-budget controls under eval; the same fixture runs on the ship |

65| `tools/type-tlon-test` | Runs the real Tlon presence source through the importer and partial checker, comparing `tests/type-tlon/expected.txt` under eval |

66| `tools/type-tlon-test` | Runs the real Tlon presence source through the importer and partial checker, comparing `tests/type-tlon/expected.txt` under eval |

66| `tools/type-import-diagnostic-test` | Compares the structured reader diagnostic bridge report under eval |

67| `tools/type-import-diagnostic-test` | Compares the structured reader diagnostic bridge report under eval |

67| `tools/type-mark-test` | Checks the partial checker’s mark import boundary against `tests/type-mark/expected.txt` under eval |

68| `tools/type-mark-test` | Checks the partial checker’s mark import boundary against `tests/type-mark/expected.txt` under eval |

@@ -104,6 +105,7 @@ tools/golden # all cases pass

104tools/importer-test # Hoon importer fixture projections match

105tools/importer-test # Hoon importer fixture projections match

105tools/type-import-default-test # default-wrapped source proofs match

106tools/type-import-default-test # default-wrapped source proofs match

106tools/type-import-test # importer/checker bridge golden report matches

107tools/type-import-test # importer/checker bridge golden report matches

108+tools/type-import-overlap-test # source-aware Hoon overlap and provenance controls

107tools/type-tlon-test # real Tlon importer/checker report matches

109tools/type-tlon-test # real Tlon importer/checker report matches

108tools/type-import-diagnostic-test # direct structured reader diagnostics match

110tools/type-import-diagnostic-test # direct structured reader diagnostics match

109tools/type-mark-test # mark/checker bridge golden report matches

111tools/type-mark-test # mark/checker bridge golden report matches

docs/status.md+7−3

@@ -49,7 +49,9 @@ The shared prelude interface reserves every name present in the supplied vendore

49

50An 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.

51

52−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. A source-aware Hoon import fixture records that nested mixed-zero overlaps are rejected conservatively and that some disjoint flag cases also remain unsupported. Execution, jet recognition and complete import checking remain unfinished.

52+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.

53+

54+The Hoon reader can prove a narrow two-case overlap from the original `$?` source and report it at a Jibb use site. It independently evaluates each case and compares runtime noun values; supported distinct head tags also prove disjoint. Other overlaps, Hoon case locations and mark-reader overlap diagnostics remain unfinished. The new `$?` case screen allows at most 128 cases and 4,096 source noun nodes; the overlap proof has a separate 4,096-node dependency budget. Neither bounds chapter lookup, Hoon evaluation or graph walks.

53

55

54Restricted-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.

56Restricted-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.

55

57

@@ -70,7 +72,7 @@ What the plan asks for, and where it is:

70Besides the plan's list:

72Besides the plan's list:

71

73

72- 652 golden cases: 432 that parse and 220 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.

74- 652 golden cases: 432 that parse and 220 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.

73−- The 652-case corpus passed under `urbit eval` in 111.5 s while other checks were running. The fake ship passed all 684 tests, including the 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, with 86.5 s for sync and 139.0 s for tests. 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.

75+- The 652-case corpus passed under `urbit eval` in 96.7 s while other checks were running. The fake ship passed all 685 tests, including the source-overlap fixture, 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 92.0 s while other checks were running. 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.

74- `tools/testdata/selftest` (22 checks), `tools/testdata/ship-selftest` and `tools/testdata/clay-fixtures-selftest` test the tools themselves; the last checks temporary Clay fixture cleanup and signal handling without a ship.

76- `tools/testdata/selftest` (22 checks), `tools/testdata/ship-selftest` and `tools/testdata/clay-fixtures-selftest` test the tools themselves; the last checks temporary Clay fixture cleanup and signal handling without a ship.

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

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

76- Speed: starting `urbit eval` and building the library takes about 8 s. 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).

78- Speed: starting `urbit eval` and building the library takes about 8 s. 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).

@@ -170,7 +172,8 @@ Besides the plan's list:

170| 651b8ec | 2026-10-31 | Match source-proven gate samples in direct calls |

172| 651b8ec | 2026-10-31 | Match source-proven gate samples in direct calls |

171| cc8e389 | 2026-10-31 | Add source-backed list length and real todo regression |

173| cc8e389 | 2026-10-31 | Add source-backed list length and real todo regression |

172| 4da6891 | 2026-10-31 | Add source-backed comparisons and nested Hoon union controls |

174| 4da6891 | 2026-10-31 | Add source-backed comparisons and nested Hoon union controls |

173−| This change | 2026-10-31 | Skip unnecessary inference environment scans |

175+| 09db390 | 2026-10-31 | Skip unnecessary inference environment scans |

176+| This change | 2026-10-31 | Diagnose source-proven Hoon union overlaps |

174

177

175## Checking it

178## Checking it

176

179

@@ -181,6 +184,7 @@ tools/golden # 652 cases under urbit eval

181tools/importer-test # the Hoon importer fixture projection

184tools/importer-test # the Hoon importer fixture projection

182tools/type-import-default-test # default-wrapped source proof golden

185tools/type-import-default-test # default-wrapped source proof golden

183tools/type-import-test # the importer/checker bridge fixture

186tools/type-import-test # the importer/checker bridge fixture

187+tools/type-import-overlap-test # source-aware Hoon overlap and provenance fixture

184tools/type-tlon-test # the real Tlon reader/checker fixture

188tools/type-tlon-test # the real Tlon reader/checker fixture

185tools/type-mark-test # the mark/checker bridge fixture

189tools/type-mark-test # the mark/checker bridge fixture

186tools/type-poke-test # the source-backed poke/API fixture

190tools/type-poke-test # the source-backed poke/API fixture

jibb-dev/lib/jibb-import.hoon+104−6

@@ -47,7 +47,7 @@

47 ==

48+$ import-diagnostic

49 $% [%ok value=imported]

50− [%invalid code=?(%aura %core) message=@t]

50+ [%invalid code=?(%aura %core %overlap) message=@t]

51 [%unsupported message=@t]

52 ==

53+$ signatures (list [name=term code=hoon])

@@ -132,6 +132,35 @@

132 =/ rest $(cases t.cases, tags [u.tag tags])

133 ?~ rest ~

134 `[[u.tag i.cases] u.rest]

135+

136+::

137+:: Bound the new $? branch screen independently of the existing $% path.

138+:: Count raw noun nodes across all cases, and cap pairwise tag comparisons.

139+++ bounded-no-spec-unions

140+ |= [h=* fuel=@ud]

141+ ^- (unit @ud)

142+ ?: =(fuel 0) ~

143+ =. fuel (dec fuel)

144+ ?@ h `fuel

145+ ?: ?=([%bckt ^ ^] h) ~

146+ ?: ?=([%bcwt [^ [^ *]]] h) ~

147+ ?: ?=([%bccn [^ [^ *]]] h) ~

148+ =/ left=(unit @ud) $(h -.h)

149+ ?~ left ~

150+ $(h +.h, fuel u.left)

151+++ tagged-bounded-cases

152+ |= [cases=(list spec) tags=(list @) fuel=@ud left=@ud]

153+ ^- (unit (list tagged-case))

154+ ?~ cases `~

155+ ?: =(left 0) ~

156+ =/ remaining=(unit @ud) (bounded-no-spec-unions i.cases fuel)

157+ ?~ remaining ~

158+ =/ tag=(unit @) (tagged-head i.cases)

159+ ?~ tag ~

160+ ?: (lien tags |=(x=@ =(x u.tag))) ~

161+ =/ rest $(cases t.cases, tags [u.tag tags], fuel u.remaining, left (dec left))

162+ ?~ rest ~

163+ `[[u.tag i.cases] u.rest]

135::

164::

136:: Benign source annotations have different typed representations on

165:: Benign source annotations have different typed representations on

137:: Clay and under eval. Inspect the wrapper as a noun, and validate the

166:: Clay and under eval. Inspect the wrapper as a noun, and validate the

@@ -170,11 +199,19 @@

170 ?~ found ~

199 ?~ found ~

171 =/ body=(unit spec) (tagged-default-union u.found 4)

200 =/ body=(unit spec) (tagged-default-union u.found 4)

172 ?~ body ~

201 ?~ body ~

202+ ?- u.body

173− ?. ?=([%bccn *] u.body) ~

203+ [%bccn *]

204+ =/ cases=(list spec) p.u.body

205+ ?~ cases ~

206+ ?~ t.cases ~

207+ (tagged-cases cases ~)

208+ [%bcwt *]

174− =/ cases=(list spec) p.u.body

209+ =/ cases=(list spec) p.u.body

175− ?~ cases ~

210+ ?~ cases ~

176− ?~ t.cases ~

211+ ?~ t.cases ~

177− (tagged-cases cases ~)

212+ (tagged-bounded-cases cases ~ 4.096 128)

213+ * ~

214+ ==

178::

215::

179:: Source proof for dependencies of an explicitly tagged union. Only

216:: Source proof for dependencies of an explicitly tagged union. Only

180:: simple local molds, standard collections and distinct term enums are

217:: simple local molds, standard collections and distinct term enums are

@@ -346,6 +383,63 @@

346 ?. ?=([%cell [%atom %tas [~ @]] *] i.ys) ~

383 ?. ?=([%cell [%atom %tas [~ @]] *] i.ys) ~

347 ?. =(tag.i.xs u.value.head.i.ys) ~

384 ?. =(tag.i.xs u.value.head.i.ys) ~

348 $(xs t.xs, ys t.ys)

385 $(xs t.xs, ys t.ys)

386+

387+::

388+:: A finite, positive witness for two three-field tagged source cases.

389+:: The final @t fields admit noun zero. Each middle field is either an

390+:: explicit singleton or exactly two explicit singletons. Match noun

391+:: values independently of their aura labels; other shapes are unknown.

392+++ witness-atom-values

393+ |= node=imported

394+ ^- (unit (list @))

395+ ?: ?=([%atom *] node)

396+ ?~ value.node ~

397+ `~[u.value.node]

398+ ?. ?=([%fork [* [* ~]]] node) ~

399+ ?. &(?=([%atom *] i.cases.node) ?=([%atom *] i.t.cases.node)) ~

400+ ?~ value.i.cases.node ~

401+ ?~ value.i.t.cases.node ~

402+ `~[u.value.i.cases.node u.value.i.t.cases.node]

403+++ witness-tagged-case

404+ |= node=imported

405+ ^- (unit [head=@ middle=(list @)])

406+ ?. ?=([%cell [%atom %tas [~ @]] [%cell * [%atom %t ~]]] node) ~

407+ =/ middle (witness-atom-values head.tail.node)

408+ ?~ middle ~

409+ `[u.value.head.node u.middle]

410+++ overlap-zero-source

411+ |= [module=term name=term cor=type]

412+ ^- ?

413+ ?. ?=([%core *] cor) |

414+ =/ selected=(unit hoon) (local-arm-source cor name)

415+ ?~ selected |

416+ =/ shape=(unit spec) (local-mold-spec u.selected name)

417+ ?~ shape |

418+ =/ body=(unit spec) (tagged-default-union u.shape 4)

419+ ?~ body |

420+ ?. ?=([%bcwt [* [* ~]]] u.body) |

421+ =/ one=spec i.p.u.body

422+ =/ two=spec i.t.p.u.body

423+ =/ first=(unit @) (tagged-head one)

424+ =/ second=(unit @) (tagged-head two)

425+ ?~ first |

426+ ?~ second |

427+ ?. =(u.first u.second) |

428+ =/ cases=(list tagged-case) ~[[u.first one] [u.second two]]

429+ ?. ?=(^ (safe-source-tagged-fuel-mode cases cor ~[name] 4.096 |)) |

430+ =/ tried=(each (list type) tang)

431+ (mule |.((turn cases |=(c=tagged-case (~(play ut cor) [%kttr branch.c])))))

432+ ?. ?=([%& [* [* ~]]] tried) |

433+ =/ projected=(each (list imported) tang)

434+ (mule |.((turn p.tried |=(t=type (walk module t catalog ~ `cor)))))

435+ ?. ?=([%& [* [* ~]]] projected) |

436+ ?^ (first-bads p.projected) |

437+ =/ a (witness-tagged-case i.p.projected)

438+ =/ b (witness-tagged-case i.t.p.projected)

439+ ?~ a |

440+ ?~ b |

441+ ?. &(=(head.u.a u.first) =(head.u.b u.second) =(head.u.a head.u.b)) |

442+ (lien middle.u.a |=(n=@ (lien middle.u.b |=(m=@ =(n m)))))

349::

443::

350:: +read-mold-in: accept the /sur core as provenance. The core must be

444:: +read-mold-in: accept the /sur core as provenance. The core must be

351:: built against zuse or validated Ford imports, and its selected arm

445:: built against zuse or validated Ford imports, and its selected arm

@@ -361,6 +455,8 @@

361 [%| (crip "Hoon mold `{(trip name)}` is not declared")]

455 [%| (crip "Hoon mold `{(trip name)}` is not declared")]

362 ?. =(typ (~(play ut cor) (ream (cat 3 '*' name))))

456 ?. =(typ (~(play ut cor) (ream (cat 3 '*' name))))

363 [%| 'Hoon module provenance does not match the selected mold']

457 [%| 'Hoon module provenance does not match the selected mold']

458+ =/ overlap=(each ? tang) (mule |.((overlap-zero-source module name cor)))

459+ ?: &(?=(%& -.overlap) p.overlap) [%| 'Hoon union cases overlap']

364 =/ result (read-with module name typ [~ cor])

460 =/ result (read-with module name typ [~ cor])

365 ?: ?=([%& *] result) result

461 ?: ?=([%& *] result) result

366 =/ fallback=(each (unit (each imported @t)) tang)

462 =/ fallback=(each (unit (each imported @t)) tang)

@@ -461,6 +557,8 @@

461 [%unsupported p.result]

557 [%unsupported p.result]

462 =/ selected=(each type tang) (mule |.((~(play ut cor) (ream (cat 3 '*' name)))))

558 =/ selected=(each type tang) (mule |.((~(play ut cor) (ream (cat 3 '*' name)))))

463 ?. ?=(%& -.selected) [%unsupported p.result]

559 ?. ?=(%& -.selected) [%unsupported p.result]

560+ =/ overlap=(each ? tang) (mule |.((overlap-zero-source module name cor)))

561+ ?: &(?=(%& -.overlap) p.overlap) [%invalid %overlap 'Hoon union cases overlap']

464 =/ again=(each imported tang) (mule |.((walk module p.selected catalog ~ [~ cor])))

562 =/ again=(each imported tang) (mule |.((walk module p.selected catalog ~ [~ cor])))

465 ?. ?=(%& -.again) [%unsupported p.result]

563 ?. ?=(%& -.again) [%unsupported p.result]

466 =/ evidence=(unit import-diagnostic) (first-invalid p.again)

564 =/ evidence=(unit import-diagnostic) (first-invalid p.again)

jibb-dev/lib/jibb.hoon+1−1

@@ -6589,7 +6589,7 @@

6589 ?~ found ~

6590 ?^ t.found ~

6591 result.i.found

6592− ?. ?=([%invalid ?(%aura %core) @] raw) ~

6592+ ?. ?=([%invalid ?(%aura %core %overlap) @] raw) ~

6593 `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]

6594::

6595:: Replay only the shape branches whose evaluation order we can prove.

tests/importer/about.txt+2−1

@@ -9,7 +9,8 @@ explicit union argument when the exact call wrapper and collection provenance

9are validated and all union cases are static and pairwise disjoint. Cases

10cover overlap, collapsed branches, multiple or nested unions, dependent

11branches, forged subject, sample and tail wrappers, and a shadowed

12+collection. `explicit-unknown` has distinct outer tags and a local `word` alias

12−collection. Tagged source cases exercise bare null payloads, overlapping tags and hidden

13+for `@t`, so its source cases can be proved disjoint. Tagged source cases exercise bare null payloads, overlapping tags and hidden

13invalid dependencies, named payload dependencies, valid and collapsed enums,

14invalid dependencies, named payload dependencies, valid and collapsed enums,

14direct and transitively aliased overlaps, nested collections, shadowed jar and

15direct and transitively aliased overlaps, nested collections, shadowed jar and

15jug dependencies, Ford-name collisions, zuse local-name precedence and the

16jug dependencies, Ford-name collisions, zuse local-name precedence and the

tests/importer/tree.txt+1−1

@@ -78,7 +78,7 @@ explicit-wut-overlap: error: Hoon union disjointness could not be verified

78explicit-collapsed: error: Hoon union disjointness could not be verified

79explicit-subsumed: error: Hoon union disjointness could not be verified

80explicit-three: (union [a @ud] [b @t] [c @p])

81−explicit-unknown: error: a Hoon union needs a source-level disjointness check

81+explicit-unknown: (union [x @t] [y @t])

82explicit-nested: error: Hoon union disjointness could not be verified

83collection-union-wrapper: valid; forged subject, sample and tail rejected

84collection-union-list: (list (union [x @ud] [y @t]))

tests/lib/jibb-bridge.hoon+2−2

@@ -136,7 +136,7 @@

136 [%fixture %raw-rec [%& [%ref %fixture %chain]]]

137 [%fixture %bad-arity [%& [%apply %list ~[[%atom %t ~] [%atom %ud ~]]]]]

138 [%fixture %bad-argument [%& [%apply %list ~[[%fork ~[[%atom %tas [~ %a]] [%atom %tas [~ %a]]]]]]]]

139− [%fixture %mixed-zero (read %mixed-zero)]

139+ [%fixture %mixed-zero (read-named-diagnostic:jibb-import %fixture %mixed-zero cor)]

140 [%fixture %separate-tags (read %separate-tags)]

141 [%fixture %separate-terms (read %separate-terms)]

142 [%fixture %nested-choice (read %nested-choice)]

@@ -153,7 +153,7 @@

153 [%fixture %duplicate [%& [%atom %ud ~]]]

154 [%missing %title [%& [%atom %t ~]]]

155 ==

156− =/ report=@t (golden-types-imports:jibb /test/jibb src external)

156+ =/ report=@t (golden-types-with-reader-diagnostics:jibb /test/jibb src external ~)

157 =/ dep=@t (crip "/- fixture\0a++ chain-id |= x=chain.fixture x\0a")

158 =/ root=@t (crip "/= helper /ui/helper\0a++ use chain-id.helper\0a")

159 =/ prelude=@t (crip "++ prelude-id |= x x\0a")

tests/lib/jibb-import-overlap.hoonnew file+80

@@ -0,0 +1,80 @@

1+/+ jibb, jibb-import

2+/* sur %txt /tests/type-import-overlap/sur/txt

3+/* source %txt /tests/type-import-overlap/source/txt

4+/* expected %txt /tests/type-import-overlap/expected/txt

5+|%

6+++ text

7+ |= lines=wain

8+ ^- @t

9+ (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))

10+++ test-import-overlap

11+ ^- tang

12+ ?~ sur ~[leaf+"overlap fixture source is missing"]

13+ ?~ source ~[leaf+"overlap fixture client is missing"]

14+ ?~ expected ~[leaf+"overlap fixture expected output is missing"]

15+ =/ got (overlap-output (text sur) (text source))

16+ ?. =((to-wain:format (cat 3 got '\0a')) expected)

17+ ~[leaf+"overlap output differs from expected"]

18+ ~

19+++ bounded-screen-status

20+^- @t

21+?. ?=(~ (bounded-no-spec-unions:jibb-import [1 2] 2)) 'three-node noun exceeded limit'

22+=/ exact (bounded-no-spec-unions:jibb-import [1 2] 3)

23+?. =(exact `0) 'three-node exact budget failed'

24+?. ?=(~ (bounded-no-spec-unions:jibb-import [[[[1 2] 3] 4] 5] 8)) 'deep noun exceeded limit'

25+?. =((bounded-no-spec-unions:jibb-import [[[[1 2] 3] 4] 5] 9) `0) 'deep exact budget failed'

26+?. ?=(~ (bounded-no-spec-unions:jibb-import [1 2 3 4 5] 8)) 'wide noun exceeded limit'

27+?. =((bounded-no-spec-unions:jibb-import [1 2 3 4 5] 9) `0) 'wide exact budget failed'

28+?. ?=(~ (bounded-no-spec-unions:jibb-import [%bcwt [[1 2] [[3 4] 0]]] 100)) 'nested $? accepted'

29+?. ?=(~ (bounded-no-spec-unions:jibb-import [%bccn [[1 2] [[3 4] 0]]] 100)) 'nested $% accepted'

30+?. ?=(~ (bounded-no-spec-unions:jibb-import [%bckt [1 2] [3 4]] 100)) 'nested $^ accepted'

31+=/ very-deep=*

32+ =/ n=@ud 1.000

33+ =/ node=* 0

34+ |-

35+ ?: =(n 0) node

36+ $(n (dec n), node [node n])

37+?. =((bounded-no-spec-unions:jibb-import very-deep 2.001) `0) 'deep 2,001-node exact budget failed'

38+?. ?=(~ (bounded-no-spec-unions:jibb-import very-deep 2.000)) 'deep 2,001-node limit exceeded'

39+=/ xs=(list spec)

40+ (turn (gulf 1 128) |=(n=@ud `spec`[%bccl ~[[%leaf %tas n] [%base [%atom %t]]]]))

41+?~ xs 'generated source cases missing'

42+=/ first=(unit @ud) (bounded-no-spec-unions:jibb-import i.xs 1.000)

43+?~ first 'simple source case unavailable'

44+=/ total=@ud (mul 128 (sub 1.000 u.first))

45+=/ at=(unit (list tagged-case:jibb-import)) (tagged-bounded-cases:jibb-import xs ~ total 128)

46+?~ at '128 exact cases rejected'

47+?. =((lent u.at) 128) 'a source case was omitted'

48+?. ?=(~ (tagged-bounded-cases:jibb-import xs ~ (dec total) 128)) 'source node limit exceeded'

49+=/ over=(list spec) (weld xs ~[`spec`[%bccl ~[[%leaf %tas 129] [%base [%atom %t]]]]])

50+?. ?=(~ (tagged-bounded-cases:jibb-import over ~ 100.000 128)) '129 cases exceeded limit'

51+=/ nested=spec [%bccl ~[[%leaf %tas %x] [%bcwt ~[[%leaf %tas %a] [%leaf %tas %b]]]]]

52+?. ?=(~ (tagged-bounded-cases:jibb-import ~[nested] ~ 1.000 128)) 'nested union case accepted'

53+=/ unknown=spec [%base [%atom %t]]

54+?. ?=(~ (tagged-bounded-cases:jibb-import ~[unknown] ~ 1.000 128)) 'non-tagged source accepted'

55+'bounded source screen controls passed'

56+

57+++ overlap-output

58+ |= [sur-text=@t src=@t]

59+ ^- @t

60+ =/ cor=type -:(ride -:!>(..zuse) sur-text)

61+ =/ names=(list term)

62+ ~[%mixed-zero %nonzero %unequal-singletons %swapped %separate-tags %separate-terms %different-value %different-tail %unknown-middle %unsupported-gate %dollar-percent %identical %cross-zero %boolean-tail %empty-tail]

63+ =/ cases=wall

64+ %+ turn names

65+ |= n=term

66+ "{(trip n)}: {(show-import-diagnostic:jibb-import (read-named-diagnostic:jibb-import %fixture n cor))}"

67+ =/ other=type (~(play ut cor) (ream '*separate-tags'))

68+ =/ provenance=wall

69+ :~ "mismatched-selected: {(show-result:jibb-import (read-mold-in:jibb-import %fixture %mixed-zero other cor))}"

70+ "missing: {(show-result:jibb-import (read-named:jibb-import %fixture %missing cor))}"

71+ "bare-zuse: {(show-result:jibb-import (read-named:jibb-import %fixture %mixed-zero -:!>(..zuse)))}"

72+ ==

73+ =/ external=(list [module=term name=term result=*])

74+ :~ [%fixture %mixed-zero (read-named-diagnostic:jibb-import %fixture %mixed-zero cor)]

75+ [%fixture %separate-tags (read-named-diagnostic:jibb-import %fixture %separate-tags cor)]

76+ [%fixture %unknown-middle (read-named-diagnostic:jibb-import %fixture %unknown-middle cor)]

77+ ==

78+ =/ report=@t (golden-types-with-reader-diagnostics:jibb /ui/test/jibb src external ~)

79+ (cat 3 (of-wain:format (turn (weld cases (weld ~[(trip bounded-screen-status)] provenance)) |=(line=tape (crip line)))) (cat 3 '\0a' report))

80+--

tests/type-import-overlap/about.txtnew file+24

@@ -0,0 +1,24 @@

1+Source-aware Hoon `$?` cases are independently evaluated before the reader

2+proves a shared runtime noun or a disjoint pair of literal outer tags. The

3+positive overlap witness handles exactly two cases, each projecting to three

4+fields: a term singleton, a singleton or two-singleton fork, and an `@t`

5+tail. The singleton comparison uses noun values regardless of aura, and the

6+`@t` tail admits noun zero. Other overlap shapes remain unsupported.

7+

8+The mixed-aura zero and nonzero controls prove actual overlap; unequal, opaque

9+and other unproven payloads remain unsupported. The structured diagnostic

10+bridge reports a definite overlap at the Jibb use site, while the disjoint

11+case infers and an unresolved case stays unsupported. The Hoon source case

12+locations are unavailable in this fixture and are not claimed. This is a

13+partial report and does not prove the whole module was checked. This named

14+reader proof is not a mark-reader overlap diagnostic.

15+

16+The existing 4,096 source-proof fuel limits dependency-spec visits. Chapter

17+lookup, Hoon play, type projection, parsing and all other work are outside

18+that limit. Unknown or exhausted source proof stays unsupported.

19+

20+The added `$?` source screen caps the total raw noun nodes at 4,096 and

21+the case count at 128 before checking tags. The shared guard exercises exact

22+and exceeded budgets, deep and wide inputs, nested union forms, and unknown

23+source cases. These limits do not meter atom sizes, chapter lookup, Hoon play,

24+reader projection or other work. The pre-existing `$%` path is unchanged.

tests/type-import-overlap/expected.txtnew file+26

@@ -0,0 +1,26 @@

1+mixed-zero: invalid/overlap: Hoon union cases overlap

2+nonzero: invalid/overlap: Hoon union cases overlap

3+unequal-singletons: unsupported: a Hoon union needs a source-level disjointness check

4+swapped: invalid/overlap: Hoon union cases overlap

5+separate-tags: (union [left [ @t]] [right [(union @f:0 @f:1) @t]])

6+separate-terms: (union [left [ @t]] [right [yes @t]])

7+different-value: unsupported: a Hoon union needs a source-level disjointness check

8+different-tail: unsupported: a Hoon union needs a source-level disjointness check

9+unknown-middle: unsupported: a Hoon union needs a source-level disjointness check

10+unsupported-gate: unsupported: a Hoon union needs a source-level disjointness check

11+dollar-percent: (union [left [ @t]] [right [yes @t]])

12+identical: invalid/overlap: Hoon union cases overlap

13+cross-zero: invalid/overlap: Hoon union cases overlap

14+boolean-tail: unsupported: a Hoon union needs a source-level disjointness check

15+empty-tail: unsupported: a Hoon union needs a source-level disjointness check

16+bounded source screen controls passed

17+mismatched-selected: error: Hoon module provenance does not match the selected mold

18+missing: error: Hoon mold `missing` is not declared

19+bare-zuse: error: Hoon module provenance is unavailable

20+partial inference; module not checked

21+++ overlap: Hoon union cases overlap

22+/ui/test.jibb:2:17: invalid imported mold

23+++ overlap |= x=mixed-zero.fixture x

24+ ^

25+++ disjoint: $-(([%left [%$ @t]] [%right [? @t]]) ([%left [%$ @t]] [%right [? @t]]))

26+++ unknown: sample mold is not supported by partial inference

tests/type-import-overlap/source.txtnew file+4

@@ -0,0 +1,4 @@

1+/- fixture

2+++ overlap |= x=mixed-zero.fixture x

3+++ disjoint |= x=separate-tags.fixture x

4+++ unknown |= x=unknown-middle.fixture x

tests/type-import-overlap/sur.txtnew file+17

@@ -0,0 +1,17 @@

1+|%

2++$ mixed-zero $?([%tag %$ @t] [%tag ? @t])

3++$ nonzero $?([%tag %.n @t] [%tag ? @t])

4++$ unequal-singletons $?([%tag %.n @t] [%tag %$ @t])

5++$ swapped $?([%tag ? @t] [%tag %$ @t])

6++$ separate-tags $?([%left %$ @t] [%right ? @t])

7++$ separate-terms $?([%left %$ @t] [%right %yes @t])

8++$ different-value $?([%tag %yes @t] [%tag ? @t])

9++$ different-tail $?([%tag %$ @t] [%tag ? @p])

10++$ unknown-middle $?([%tag * @t] [%tag ? @t])

11++$ unsupported-gate $?([%tag %$ @t] [%tag ? $-(@t @t)])

12++$ dollar-percent $%([%left %$ @t] [%right %yes @t])

13++$ identical $?([%tag %$ @t] [%tag %$ @t])

14++$ cross-zero $?([%tag %.y @t] [%tag %$ @t])

15++$ boolean-tail $?([%tag %$ ?] [%tag ? ?])

16++$ empty-tail $?([%tag %$ ~] [%tag ? @t])

17+--

tests/type-import/about.txt+4−3

@@ -29,7 +29,8 @@ claim that the module was checked. The same fixture runs under urbit eval and

29through -test on the fake ship.

30

31The real-reader mixed-zero case places `%$` and `?` under the same outer tag;

32−both allow the noun zero. It must fail closed. The distinct-tag `%$`/`?`

32+both allow the noun zero, so the reader reports definite overlap. The distinct-tag

33−case records the current conservative limitation, while distinct-tag term

34−singletons are a successful reader/checker control. These are source-aware

33+`%$`/`?` case and distinct-tag term singletons are successful reader/checker

34+controls. The overlap error points at the Jibb use site; the Hoon source case

35+positions are not available in this fixture. These are source-aware

35reads and the checker report remains partial.

36reads and the checker report remains partial.

tests/type-import/expected.txt+7−4

@@ -104,12 +104,15 @@ partial inference; module not checked

104++ flag-extra: sample mold is not supported by partial inference

105++ flag-faced: sample mold is not supported by partial inference

106++ flag-malformed: sample mold is not supported by partial inference

107−++ mixed-zero: sample mold is not supported by partial inference

107+++ mixed-zero: Hoon union cases overlap

108−++ separate-tags: sample mold is not supported by partial inference

108+/test.jibb:81:20: invalid imported mold

109+++ mixed-zero |= x=mixed-zero.fixture x

110+ ^

111+++ separate-tags: $-(([%left [%$ @t]] [%right [? @t]]) ([%left [%$ @t]] [%right [? @t]]))

109++ separate-terms: $-(([%left [%$ @t]] [%right [%yes @t]]) ([%left [%$ @t]] [%right [%yes @t]]))

112++ separate-terms: $-(([%left [%$ @t]] [%right [%yes @t]]) ([%left [%$ @t]] [%right [%yes @t]]))

110reader-collapsed: error: Hoon union disjointness could not be verified

113reader-collapsed: error: Hoon union disjointness could not be verified

111−reader-mixed-zero: error: a Hoon union needs a source-level disjointness check

114+reader-mixed-zero: error: Hoon union cases overlap

112−reader-separate-tags: error: a Hoon union needs a source-level disjointness check

115+reader-separate-tags: (union [left [ @t]] [right [(union @f:0 @f:1) @t]])

113reader-separate-terms: (union [left [ @t]] [right [yes @t]])

116reader-separate-terms: (union [left [ @t]] [right [yes @t]])

114partial inference; module not checked

117partial inference; module not checked

115++ use: recursive mold name is not available in this scope

118++ use: recursive mold name is not available in this scope

tools/type-import-overlap-testnew file+33

@@ -0,0 +1,33 @@

1+#!/usr/bin/env python3

2+"""Run the shared source-aware overlap bridge under urbit eval."""

3+from pathlib import Path

4+import difflib

5+import subprocess

6+import sys

7+import tempfile

8+

9+root = Path(__file__).resolve().parent.parent

10+fixture = root / 'tests/type-import-overlap'

11+reader = (root / 'jibb-dev/lib/jibb-import.hoon').read_text()

12+tests = (root / 'tests/lib/jibb-import-overlap.hoon').read_text()

13+tests = tests[tests.index('\n|%\n') + 1:]

14+program = ('=/ jibb .\n=/ jibb-import\n' + reader +

15+ '\n=/ sur=wain (to-wain:format sur-text)\n=/ source=wain (to-wain:format source-text)\n=/ expected=wain (to-wain:format expected-text)\n=/ bridge\n' + tests + '\n(overlap-output:bridge sur-text source-text)\n')

16+with tempfile.TemporaryDirectory(prefix='jibb-import-overlap-') as tmp:

17+ path = Path(tmp) / 'bridge.hoon'

18+ path.write_text(program)

19+ result = subprocess.run([str(root / 'tools/hoon'), '--raw', '-f', str(path),

20+ '--cord', 'sur-text=' + str(fixture / 'sur.txt'),

21+ '--cord', 'source-text=' + str(fixture / 'source.txt'),

22+ '--cord', 'expected-text=' + str(fixture / 'expected.txt')], stdout=subprocess.PIPE)

23+if result.returncode:

24+ sys.exit(result.returncode)

25+if '--capture' in sys.argv:

26+ sys.stdout.buffer.write(result.stdout)

27+ sys.exit()

28+expected = (fixture / 'expected.txt').read_bytes()

29+if result.stdout != expected:

30+ sys.stderr.writelines(difflib.unified_diff(expected.decode().splitlines(keepends=True),

31+ result.stdout.decode().splitlines(keepends=True), fromfile='expected', tofile='actual'))

32+ sys.exit(1)

33+print('source-aware overlap bridge passed')