142f2e2 · jibb · git.iko.soy

git.iko.soy/jibb

Prove structural Hoon union overlaps

Compare independently evaluated source cases for shared runtime nouns through supported nested shapes. Bound source and pair analysis and retain unsupported results for unproven cases.

commit142f2e26d76a32feb778b2fbfed61844698d9369 authoriko <mail@iko.soy> dateSat 31 Oct 2026, 13:37 (10 hours ago) parent179d717

18 files changed+339−62

compare with master

unifiedsplit

README.md+1−1 docs/compiler.md+3−1 docs/development.md+2 docs/status.md+5−3 jibb-dev/lib/jibb-import.hoon+121−44 tests/importer/about.txt+2−1 tests/importer/tree.txt+2−2 tests/lib/jibb-import-structural.hoon+82 tests/type-import-overlap/about.txt+6−6 tests/type-import-overlap/expected.txt+2−2 tests/type-import-structural/about.txt+14 tests/type-import-structural/expected.txt+41 tests/type-import-structural/source.txt+5 tests/type-import-structural/sur.txt+12 tests/type-import/about.txt+2−1 tests/type-import/expected.txt+1−1 tools/testdata/ship-selftest+2 tools/type-import-structural-test+36

README.md+1−1

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

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

4343```

4444

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.

4646

4747### The doc's examples

4848

docs/compiler.md+3−1

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

100100

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

102102

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.

104106

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

106108

docs/development.md+2

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

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

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

6565| `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 |

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

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

6869| `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

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

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

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

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

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

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

111113tools/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

5151

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

5353

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.

5555

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

5757

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

7272Besides the plan's list:

7373

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

7676- `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.

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

7878- 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:

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

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

175175| 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 |

177178

178179## Checking it

179180

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

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

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

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

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

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

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

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

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

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

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

386386

387387::

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

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

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

390+++ overlap-source-cases

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

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

393+ ?~ cases `~

394+ ?: =(left 0) ~

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

396+ ?~ remaining ~

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

398+ ?~ tag ~

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

407+ $(cases t.cases)

408+++ overlap-projections-match

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

410+ ^- ?

411+ ?~ xs ?=(~ ys)

412+ ?~ ys |

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

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

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

416+++ overlap-source-witness

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

412418 ^- ?

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

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

417423 ?~ shape |

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

419425 ?~ 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 |)) |

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

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

428+ ?~ cases |

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

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

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

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

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

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

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

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

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

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

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

436437 ?^ (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)))))

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

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

440+ ?~ witness |

441+ found.u.witness

442+::

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)

443520::

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

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

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

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

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

457534 [%| '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)))

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

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

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

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

557634 [%unsupported p.result]

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

559636 ?. ?=(%& -.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)))

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

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

563640 ?. ?=(%& -.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

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

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

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

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

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

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

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

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

1617jug 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

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

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

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

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

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

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

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

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

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

8181explicit-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 @@

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

22proves 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.

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

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

5+of aura. Some overlap shapes remain unsupported.

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

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

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+opaque and other unproven payloads remain unsupported. The structured diagnostic

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

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

1212locations 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

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

1212identical: invalid/overlap: Hoon union cases overlap

1313cross-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

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

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

1616bounded source screen controls passed

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

1818missing: 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.

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.

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

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

3333`%$`/`?` 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

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

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

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

3637reads and the checker report remains partial.

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

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

110110 ^

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

112112++ 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

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

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

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

tools/testdata/ship-selftest+2

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

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

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

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

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

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

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

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

309311 '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

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