142f2e2 · 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-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.

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-import-structural-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

@@ -100,7 +100,9 @@ The partial checker also recognizes a source-proven Jibb recursive mold consisti

100

101Callers 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.

103+For supported source-aware Hoon `$?` unions, the reader can prove a definite overlap by independently evaluating and projecting the original cases, verifying each projected head against its source tag, and finding a shared runtime noun in a pair. Its positive witness traverses faces, named nodes, forks, cells, supported atom forms and `*`; `!!`, opaque references, applications and unproved aura intersections cannot themselves establish a witness. It compares singleton noun values independently of aura, and requires inhabited positions throughout a cell. Unknown or exhausted proof remains unsupported, while existing disjoint-source recovery still handles proven distinct cases. The source screen admits at most 128 cases and 4,096 raw noun nodes; dependency checking and the pair/type witness each have their own 4,096-node budget. Hoon evaluation, projected-graph validation, chapter lookup, atom byte sizes and other type-graph walks remain outside those budgets. The error points at the Jibb use; source case locations are unavailable. This is a partial named-reader analysis, not general imported-union checking or a mark-reader overlap diagnostic.

104+

105+In single startup-inclusive runs of eight Hoon reads, a benign three-case union used 37.78 seconds of user CPU with the earlier narrow witness and 39.99 seconds with the structural witness; a repeated-head union used 39.84 and 40.97 seconds. Other checks ran concurrently, so these measurements do not establish a production bound.

104

106

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.

107The 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.

106

108

docs/development.md+2

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

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 |

66+| `tools/type-import-structural-test` | Checks multi-case and nested Hoon union overlap witnesses under eval and on the ship |

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 |

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

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

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

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

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

@@ -106,6 +107,7 @@ tools/importer-test # Hoon importer fixture projections match

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

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

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

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

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

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

110+tools/type-import-structural-test # nested and multi-case Hoon overlap controls

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

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

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

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

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

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

docs/status.md+5−3

@@ -51,7 +51,7 @@ An eval and ship fixture now reports partial inference for the unchanged todo is

51

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

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

55

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.

57

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

72Besides the plan's list:

73

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.

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.

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

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.

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.

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

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

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

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

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

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

176+| 179d717 | 2026-10-31 | Diagnose source-proven Hoon union overlaps |

177+| This change | 2026-10-31 | Prove structural overlaps across Hoon union cases |

177

178

178## Checking it

179## Checking it

179

180

@@ -185,6 +186,7 @@ tools/importer-test # the Hoon importer fixture projection

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

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

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

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

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

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

189+tools/type-import-structural-test # structural overlap and multi-case source fixture

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

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

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

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

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

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

jibb-dev/lib/jibb-import.hoon+121−44

@@ -385,29 +385,35 @@

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

386

387::

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

388+:: Unlike the disjoint-reader fallback, source overlap may have repeated

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

389+:: tags. Bound both raw case traversal and the number of pair attempts.

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

390+++ overlap-source-cases

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

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

392−++ witness-atom-values

393− |= node=imported

394− ^- (unit (list @))

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

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

393+ ?~ cases `~

396− ?~ value.node ~

394+ ?: =(left 0) ~

397− `~[u.value.node]

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

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

396+ ?~ remaining ~

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

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

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

398+ ?~ tag ~

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

399+ =/ rest $(cases t.cases, fuel u.remaining, left (dec left))

400+ ?~ rest ~

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

402+++ overlap-repeated-tag

403+ |= cases=(list tagged-case)

404+ ^- ?

405+ ?~ cases |

406+ ?: (lien t.cases |=(c=tagged-case =(tag.c tag.i.cases))) &

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

407+ $(cases t.cases)

403−++ witness-tagged-case

408+++ overlap-projections-match

404− |= node=imported

409+ |= [xs=(list tagged-case) ys=(list imported)]

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

410+ ^- ?

411+ ?~ xs ?=(~ ys)

412+ ?~ ys |

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

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

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

414+ ?. =(tag.i.xs u.value.head.i.ys) |

408− ?~ middle ~

415+ $(xs t.xs, ys t.ys)

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

416+++ overlap-source-witness

410−++ overlap-zero-source

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

417 |= [module=term name=term cor=type]

412 ^- ?

418 ^- ?

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

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

@@ -417,29 +423,100 @@

417 ?~ shape |

423 ?~ shape |

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

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

419 ?~ body |

425 ?~ body |

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

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

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

427+ =/ cases=(unit (list tagged-case)) (overlap-source-cases p.u.body 4.096 128)

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

428+ ?~ cases |

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

429+ ?. (overlap-repeated-tag u.cases) |

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+ ?. ?=(^ (safe-source-tagged-fuel-mode u.cases cor ~[name] 4.096 |)) |

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

431 =/ tried=(each (list type) tang)

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

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

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

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

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

434 =/ projected=(each (list imported) tang)

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

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

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

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

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

437 ?^ (first-bads p.projected) |

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

438+ ?. (overlap-projections-match u.cases p.projected) |

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

439+ =/ witness=(unit overlap-proof-result) (overlap-case-pairs p.projected 4.096)

439− ?~ a |

440+ ?~ witness |

440− ?~ b |

441+ found.u.witness

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

442+::

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

443+:: Positive overlap evidence only: false means no proof, not disjointness.

444+:: Fuel is shared across all examined nodes and sibling alternatives.

445++$ overlap-proof-result [found=? left=@ud]

446+++ overlap-known-atom

447+ |= aura=term

448+ ^- ?

449+ (lien `(list term)`~[%t %tas %ud %f] |=(n=term =(n aura)))

450+++ overlap-inhabited-list

451+ |= [xs=(list imported) fuel=@ud]

452+ ^- (unit overlap-proof-result)

453+ ?~ xs `[| fuel]

454+ ?: =(0 fuel) ~

455+ =/ one=(unit overlap-proof-result) (overlap-inhabited i.xs (dec fuel))

456+ ?~ one ~

457+ ?: found.u.one one

458+ $(xs t.xs, fuel left.u.one)

459+++ overlap-inhabited

460+ |= [x=imported fuel=@ud]

461+ ^- (unit overlap-proof-result)

462+ ?: =(0 fuel) ~

463+ =. fuel (dec fuel)

464+ ?- x

465+ [%noun *] `[& fuel]

466+ [%void *] `[| fuel]

467+ [%atom *] `[|(?=(^ value.x) (overlap-known-atom aura.x)) fuel]

468+ [%face *] $(x body.x)

469+ [%named *] $(x body.x)

470+ [%fork *] (overlap-inhabited-list cases.x fuel)

471+ [%cell *]

472+ =/ a=(unit overlap-proof-result) $(x head.x)

473+ ?~ a ~

474+ ?. found.u.a a

475+ $(x tail.x, fuel left.u.a)

476+ * `[| fuel]

477+ ==

478+++ overlap-pair-list

479+ |= [xs=(list imported) y=imported fuel=@ud]

480+ ^- (unit overlap-proof-result)

481+ ?~ xs `[| fuel]

482+ ?: =(0 fuel) ~

483+ =/ p=(unit overlap-proof-result) (overlap-pair i.xs y (dec fuel))

484+ ?~ p ~

485+ ?: found.u.p p

486+ $(xs t.xs, fuel left.u.p)

487+++ overlap-pair

488+ |= [a=imported b=imported fuel=@ud]

489+ ^- (unit overlap-proof-result)

490+ ?: =(0 fuel) ~

491+ =. fuel (dec fuel)

492+ ?: ?=([%face *] a) $(a body.a)

493+ ?: ?=([%face *] b) $(b body.b)

494+ ?: ?=([%named *] a) $(a body.a)

495+ ?: ?=([%named *] b) $(b body.b)

496+ ?: ?=([%fork *] a) (overlap-pair-list cases.a b fuel)

497+ ?: ?=([%fork *] b) (overlap-pair-list cases.b a fuel)

498+ ?: ?=([%noun *] a) (overlap-inhabited b fuel)

499+ ?: ?=([%noun *] b) (overlap-inhabited a fuel)

500+ ?: &(?=([%cell *] a) ?=([%cell *] b))

501+ =/ p=(unit overlap-proof-result) $(a head.a, b head.b)

502+ ?~ p ~

503+ ?. found.u.p p

504+ $(a tail.a, b tail.b, fuel left.u.p)

505+ ?. &(?=([%atom *] a) ?=([%atom *] b)) `[| fuel]

506+ ?^ value.a

507+ ?^ value.b `[=(u.value.a u.value.b) fuel]

508+ `[&(=(u.value.a 0) (overlap-known-atom aura.b)) fuel]

509+ ?^ value.b `[&(=(u.value.b 0) (overlap-known-atom aura.a)) fuel]

510+ `[&((overlap-known-atom aura.a) (overlap-known-atom aura.b)) fuel]

511+++ overlap-case-pairs

512+ |= [xs=(list imported) fuel=@ud]

513+ ^- (unit overlap-proof-result)

514+ ?~ xs `[| fuel]

515+ ?: =(0 fuel) ~

516+ =/ p=(unit overlap-proof-result) (overlap-pair-list t.xs i.xs (dec fuel))

517+ ?~ p ~

518+ ?: found.u.p p

519+ $(xs t.xs, fuel left.u.p)

443::

520::

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

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

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

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

@@ -455,7 +532,7 @@

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -557,7 +634,7 @@

557 [%unsupported p.result]

634 [%unsupported p.result]

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

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

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

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

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

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

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

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

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

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

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

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

tests/importer/about.txt+2−1

@@ -10,7 +10,8 @@ are 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

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

13+for `@t`, so its source cases can be proved disjoint. `explicit-wut-overlap` and `explicit-collapsed`

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

14+now have positive overlap witnesses from the original source cases. Tagged source cases exercise bare null payloads, overlapping tags and hidden

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

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

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

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

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

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

tests/importer/tree.txt+2−2

@@ -74,8 +74,8 @@ explicit-graph: error: Hoon union disjointness could not be verified

74explicit-graph-unsupported: error: signed and float auras cannot be imported

75explicit-wut-safe: (union [ok @ud] [err @t])

76explicit-percent-overlap: error: Hoon union disjointness could not be verified

77−explicit-wut-overlap: error: Hoon union disjointness could not be verified

77+explicit-wut-overlap: error: Hoon union cases overlap

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

78+explicit-collapsed: error: Hoon union cases overlap

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

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

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

tests/lib/jibb-import-structural.hoonnew file+82

@@ -0,0 +1,82 @@

1+/+ jibb, jibb-import

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

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

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

5+|%

6+++ text

7+ |= lines=wain

8+ ^- @t

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

10+++ test-import-structural

11+ ^- tang

12+ ?~ sur ~[leaf+"structural overlap /sur is missing"]

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

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

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

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

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

18+ ~

19+++ structural-output

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

21+ ^- @t

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

23+ =/ names=(list term)

24+ ~[%same-alias %separate-alias %deep-match %deep-distinct %tail-distinct %later-overlap %many-safe %open-atoms %different-aura]

25+ =/ cases=wall

26+ %+ turn names

27+ |= n=term

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

29+ =/ ext=(list [module=term name=term result=*])

30+ :~ [%fixture %deep-match (read-named-diagnostic:jibb-import %fixture %deep-match cor)]

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

32+ [%fixture %different-aura (read-named-diagnostic:jibb-import %fixture %different-aura cor)]

33+ [%fixture %later-overlap (read-named-diagnostic:jibb-import %fixture %later-overlap cor)]

34+ ==

35+ =/ report=@t (golden-types-with-reader-diagnostics:jibb /ui/structural/jibb src ext ~)

36+ =/ zero=imported:jibb-import [%atom %tas `0]

37+ =/ one=imported:jibb-import [%atom %tas `1]

38+ =/ two=imported:jibb-import [%atom %tas `2]

39+ =/ txt=imported:jibb-import [%atom %t ~]

40+ =/ ship=imported:jibb-import [%atom %p ~]

41+ =/ flag=imported:jibb-import [%atom %f ~]

42+ =/ opaque=imported:jibb-import [%ref %m %x]

43+ =/ named=imported:jibb-import [%named %m %x zero]

44+ =/ arm (local-arm-source:jibb-import cor %later-overlap)

45+ ?~ arm !!

46+ =/ shape (local-mold-spec:jibb-import u.arm %later-overlap)

47+ ?~ shape !!

48+ =/ body (tagged-default-union:jibb-import u.shape 4)

49+ ?~ body !!

50+ ?> ?=([%bcwt *] u.body)

51+ =/ specs=(list spec) p.u.body

52+ ?~ specs !!

53+ =/ checks=(list [label=@t ok=?])

54+ :~ ['same literal' ?=([~ [%.y *]] (overlap-pair:jibb-import zero zero 20))]

55+ ['different literals' ?=([~ [%.n *]] (overlap-pair:jibb-import one two 20))]

56+ ['named expands' ?=([~ [%.y *]] (overlap-pair:jibb-import named zero 20))]

57+ ['opaque declines' ?=([~ [%.n *]] (overlap-pair:jibb-import opaque opaque 20))]

58+ ['opaque versus noun' ?=([~ [%.n *]] (overlap-pair:jibb-import opaque [%noun ~] 20))]

59+ ['unknown aura' ?=([~ [%.n *]] (overlap-pair:jibb-import ship txt 20))]

60+ ['open admits zero' ?=([~ [%.y *]] (overlap-pair:jibb-import flag zero 20))]

61+ ['different tail' ?=([~ [%.n *]] (overlap-pair:jibb-import [%cell zero one] [%cell zero two] 20))]

62+ ['nested face' ?=([~ [%.y *]] (overlap-pair:jibb-import [%face %a [%cell named one]] [%face %b [%cell zero one]] 20))]

63+ ['fork later case' ?=([~ [%.y *]] (overlap-pair:jibb-import [%fork ~[one zero]] zero 20))]

64+ ['empty fuel' ?=(~ (overlap-pair:jibb-import zero zero 0))]

65+ ['cell needs both' ?=(~ (overlap-pair:jibb-import [%cell zero one] [%cell zero one] 2))]

66+ ['later pair' ?=([~ [%.y *]] (overlap-case-pairs:jibb-import ~[one two zero zero] 100))]

67+ ['pair fuel' ?=(~ (overlap-case-pairs:jibb-import ~[one two zero zero] 2))]

68+ ['void' ?=([~ [%.n *]] (overlap-pair:jibb-import [%void ~] [%noun ~] 20))]

69+ ['void position' ?=([~ [%.n *]] (overlap-pair:jibb-import [%cell zero [%void ~]] [%cell zero [%noun ~]] 20))]

70+ ['opaque apply' ?=([~ [%.n *]] (overlap-pair:jibb-import [%apply %list ~[txt]] [%noun ~] 20))]

71+ ['source node fuel' ?=(~ (overlap-source-cases:jibb-import specs 1 128))]

72+ ['source case cap' ?=(~ (overlap-source-cases:jibb-import specs 4.096 3))]

73+ ['wrong projected head' !(overlap-projections-match:jibb-import ~[[%a i.specs]] ~[[%cell [%atom %tas `%b] txt]])]

74+ ['wrong case count' !(overlap-projections-match:jibb-import ~[[%a i.specs]] ~)]

75+ ==

76+ =/ results=wall

77+ %+ turn checks

78+ |= c=[label=@t ok=?]

79+ "{(trip label.c)}: {?:(ok.c "ok" "BAD")}"

80+ =/ lines=(list @t) (turn (weld cases results) |=(line=tape (crip line)))

81+ (cat 3 (of-wain:format lines) (cat 3 '\0a' report))

82+--

tests/type-import-overlap/about.txt+6−6

@@ -1,12 +1,12 @@

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

2proves 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

3+positive overlap witness checks supported projected atoms, cells, faces and

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

4+forks across the original cases. It compares singleton noun values regardless

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

5+of aura. Some overlap shapes remain unsupported.

7

6

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

7+The mixed-aura zero and nonzero controls prove actual overlap. Boolean tails

8+share loobean nouns, and `~` is the null singleton, which overlaps `@t`; unequal,

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

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

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

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

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

tests/type-import-overlap/expected.txt+2−2

@@ -11,8 +11,8 @@ unsupported-gate: unsupported: a Hoon union needs a source-level disjointness ch

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

12identical: invalid/overlap: Hoon union cases overlap

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

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

14+boolean-tail: invalid/overlap: Hoon union cases overlap

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

15+empty-tail: invalid/overlap: Hoon union cases overlap

16bounded source screen controls passed

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

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

tests/type-import-structural/about.txtnew file+14

@@ -0,0 +1,14 @@

1+The actual Hoon source includes local aliases, nested cells, equal and unequal

2+singleton nouns, open auras and three-/four-case unions. The reader reports a

3+definite overlap only when its bounded structural witness finds a shared noun;

4+otherwise ordinary source-aware disjointness checks can still recover a union,

5+or the outcome remains unsupported. The checker report is partial and points

6+to the Jibb mold use; source-case positions are unavailable here.

7+

8+Low-level controls exercise void at the root and in a cell, opaque references

9+and applications, named and faced nodes, nested alternatives, source/tag

10+mismatches and source, pair and type-node fuel. The attempted Hoon source form

11+`+$ never !!` did not compile, so the void controls use an actual `%void`

12+reader node and do not claim a source-level empty mold. The positive proof

13+only bounds specific traversals; Hoon play, projection, chapter lookup, atom

14+byte sizes and the preexisting whole-graph checks are outside those budgets.

tests/type-import-structural/expected.txtnew file+41

@@ -0,0 +1,41 @@

1+same-alias: invalid/overlap: Hoon union cases overlap

2+separate-alias: (union [tag [one @t]] [tag [two @t]])

3+deep-match: invalid/overlap: Hoon union cases overlap

4+deep-distinct: (union [tag [[inner [one three]] @t]] [tag [[inner [two three]] @t]])

5+tail-distinct: unsupported: a Hoon union needs a source-level disjointness check

6+later-overlap: invalid/overlap: Hoon union cases overlap

7+many-safe: (union [tag [one @t]] [tag [two @t]] [tag [three @t]])

8+open-atoms: invalid/overlap: Hoon union cases overlap

9+different-aura: unsupported: Hoon union disjointness could not be verified

10+same literal: ok

11+different literals: ok

12+named expands: ok

13+opaque declines: ok

14+opaque versus noun: ok

15+unknown aura: ok

16+open admits zero: ok

17+different tail: ok

18+nested face: ok

19+fork later case: ok

20+empty fuel: ok

21+cell needs both: ok

22+later pair: ok

23+pair fuel: ok

24+void: ok

25+void position: ok

26+opaque apply: ok

27+source node fuel: ok

28+source case cap: ok

29+wrong projected head: ok

30+wrong case count: ok

31+partial inference; module not checked

32+++ overlap: Hoon union cases overlap

33+/ui/structural.jibb:2:20: invalid imported mold

34+++ overlap |= x=deep-match.fixture x

35+ ^

36+++ distinct: $-(([%tag [%one @t]] [%tag [%two @t]]) ([%tag [%one @t]] [%tag [%two @t]]))

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

38+++ multi: Hoon union cases overlap

39+/ui/structural.jibb:5:18: invalid imported mold

40+++ multi |= x=later-overlap.fixture x

41+ ^

tests/type-import-structural/source.txtnew file+5

@@ -0,0 +1,5 @@

1+/- fixture

2+++ overlap |= x=deep-match.fixture x

3+++ distinct |= x=separate-alias.fixture x

4+++ unknown |= x=different-aura.fixture x

5+++ multi |= x=later-overlap.fixture x

tests/type-import-structural/sur.txtnew file+12

@@ -0,0 +1,12 @@

1+|%

2++$ scalar ?(%$ %one)

3++$ same-alias $?([%tag scalar @t] [%tag %$ @t])

4++$ separate-alias $?([%tag %one @t] [%tag %two @t])

5++$ deep-match $?([%tag [%inner [%.y %three]] @t] [%tag [%inner [%$ %three]] @t])

6++$ deep-distinct $?([%tag [%inner [%one %three]] @t] [%tag [%inner [%two %three]] @t])

7++$ tail-distinct $?([%tag %$ %one] [%tag %.y %two])

8++$ later-overlap $?([%x %one @t] [%y %one @t] [%tag %.y @t] [%tag %$ @t])

9++$ many-safe $?([%tag %one @t] [%tag %two @t] [%tag %three @t])

10++$ open-atoms $?([%tag @t @ud] [%tag @tas @t])

11++$ different-aura $?([%tag @p @t] [%tag @t @t])

12+--

tests/type-import/about.txt+2−1

@@ -31,6 +31,7 @@ through -test on the fake ship.

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

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

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

34+controls. The reader also reports definite overlap for the collapsed source

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

35+whose two cases are both `[%x @ud]`. The overlap error points at the Jibb use site; the Hoon source case

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

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

36reads and the checker report remains partial.

37reads and the checker report remains partial.

tests/type-import/expected.txt+1−1

@@ -110,7 +110,7 @@ partial inference; module not checked

110 ^

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

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

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

113+reader-collapsed: error: Hoon union cases overlap

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

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

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

tools/testdata/ship-selftest+2

@@ -304,6 +304,8 @@ def generator_checks(tmp):

304 check('default assembly keeps the repository test programs',

305 {'tests/lib/jibb.hoon', 'tests/lib/jibb-import.hoon',

306 'tests/lib/jibb-import-default.hoon',

307+ 'tests/lib/jibb-import-overlap.hoon',

308+ 'tests/lib/jibb-import-structural.hoon',

307 'tests/lib/jibb-typecheck.hoon', 'tests/lib/jibb-bridge.hoon',

309 'tests/lib/jibb-typecheck.hoon', 'tests/lib/jibb-bridge.hoon',

308 'tests/lib/jibb-arithmetic-guards.hoon',

310 'tests/lib/jibb-arithmetic-guards.hoon',

309 'tests/lib/jibb-positional-face-guards.hoon',

311 'tests/lib/jibb-positional-face-guards.hoon',

tools/type-import-structural-testnew file+36

@@ -0,0 +1,36 @@

1+#!/usr/bin/env python3

2+"""Run the shared structural source-overlap fixture 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-structural'

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

12+tests = (root / 'tests/lib/jibb-import-structural.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'

16+ '=/ source=wain (to-wain:format source-text)\n'

17+ '=/ expected=wain (to-wain:format expected-text)\n'

18+ '=/ bridge\n' + tests + '\n(structural-output:bridge sur-text source-text)\n')

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

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

21+ path.write_text(program)

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

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

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

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

26+if result.returncode:

27+ sys.exit(result.returncode)

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

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

30+ sys.exit()

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

32+if result.stdout != expected:

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

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

35+ sys.exit(1)

36+print('structural source-overlap bridge passed')