git.iko.soy/jibb
on master help sign in
Diagnose source-proven Hoon union overlaps

Compare runtime noun witnesses from independently evaluated Hoon cases, and bound the new source screen. Preserve unsupported results when the reader cannot prove a collision or disjointness.

commit179d717dd7f1e89e715769f36ef3fde396246588 authoriko <mail@iko.soy> dateSat 31 Oct 2026, 13:18 (13 hours ago) parent09db390
17 files changed+318−23
compare with master
unifiedsplit
README.md+1−1 docs/compiler.md+3−1 docs/development.md+2 docs/status.md+7−3 jibb-dev/lib/jibb-import.hoon+104−6 jibb-dev/lib/jibb.hoon+1−1 tests/importer/about.txt+2−1 tests/importer/tree.txt+1−1 tests/lib/jibb-bridge.hoon+2−2 tests/lib/jibb-import-overlap.hoon+80 tests/type-import-overlap/about.txt+24 tests/type-import-overlap/expected.txt+26 tests/type-import-overlap/source.txt+4 tests/type-import-overlap/sur.txt+17 tests/type-import/about.txt+4−3 tests/type-import/expected.txt+7−4 tools/type-import-overlap-test+33
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-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.
4646
4747### The doc's examples
4848
docs/compiler.md+3−1
@@ -98,7 +98,9 @@ Self-recursive `/sur` molds can cross the bridge as opaque module-and-name ident
9898
9999The 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.
100100
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.
102104
103105The 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.
104106
docs/development.md+2
@@ -62,6 +62,7 @@ git clone https://github.com/urbit/tools /root/src/tools
6262| `tools/importer-test` | Compares the partial Hoon importer's diagnostic trees and errors with `tests/importer/tree.txt` under `urbit eval` |
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 |
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 |
6566| `tools/type-tlon-test` | Runs the real Tlon presence source through the importer and partial checker, comparing `tests/type-tlon/expected.txt` under eval |
6667| `tools/type-import-diagnostic-test` | Compares the structured reader diagnostic bridge report under eval |
6768| `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
104105tools/importer-test # Hoon importer fixture projections match
105106tools/type-import-default-test # default-wrapped source proofs match
106107tools/type-import-test # importer/checker bridge golden report matches
108+tools/type-import-overlap-test # source-aware Hoon overlap and provenance controls
107109tools/type-tlon-test # real Tlon importer/checker report matches
108110tools/type-import-diagnostic-test # direct structured reader diagnostics match
109111tools/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
4949
5050An 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.
5151
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.
5355
5456Restricted-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.
5557
@@ -70,7 +72,7 @@ What the plan asks for, and where it is:
7072Besides the plan's list:
7173
7274- 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.
7476- `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.
7577- 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.
7678- 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:
170172| 651b8ec | 2026-10-31 | Match source-proven gate samples in direct calls |
171173| cc8e389 | 2026-10-31 | Add source-backed list length and real todo regression |
172174| 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 |
174177
175178## Checking it
176179
@@ -181,6 +184,7 @@ tools/golden # 652 cases under urbit eval
181184tools/importer-test # the Hoon importer fixture projection
182185tools/type-import-default-test # default-wrapped source proof golden
183186tools/type-import-test # the importer/checker bridge fixture
187+tools/type-import-overlap-test # source-aware Hoon overlap and provenance fixture
184188tools/type-tlon-test # the real Tlon reader/checker fixture
185189tools/type-mark-test # the mark/checker bridge fixture
186190tools/type-poke-test # the source-backed poke/API fixture
jibb-dev/lib/jibb-import.hoon+104−6
@@ -47,7 +47,7 @@
4747 ==
4848+$ import-diagnostic
4949 $% [%ok value=imported]
50− [%invalid code=?(%aura %core) message=@t]
50+ [%invalid code=?(%aura %core %overlap) message=@t]
5151 [%unsupported message=@t]
5252 ==
5353+$ signatures (list [name=term code=hoon])
@@ -132,6 +132,35 @@
132132 =/ rest $(cases t.cases, tags [u.tag tags])
133133 ?~ rest ~
134134 `[[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]
135164::
136165:: Benign source annotations have different typed representations on
137166:: Clay and under eval. Inspect the wrapper as a noun, and validate the
@@ -170,11 +199,19 @@
170199 ?~ found ~
171200 =/ body=(unit spec) (tagged-default-union u.found 4)
172201 ?~ body ~
173− ?. ?=([%bccn *] u.body) ~
174− =/ cases=(list spec) p.u.body
175− ?~ cases ~
176− ?~ t.cases ~
177− (tagged-cases cases ~)
202+ ?- u.body
203+ [%bccn *]
204+ =/ cases=(list spec) p.u.body
205+ ?~ cases ~
206+ ?~ t.cases ~
207+ (tagged-cases cases ~)
208+ [%bcwt *]
209+ =/ cases=(list spec) p.u.body
210+ ?~ cases ~
211+ ?~ t.cases ~
212+ (tagged-bounded-cases cases ~ 4.096 128)
213+ * ~
214+ ==
178215::
179216:: Source proof for dependencies of an explicitly tagged union. Only
180217:: simple local molds, standard collections and distinct term enums are
@@ -346,6 +383,63 @@
346383 ?. ?=([%cell [%atom %tas [~ @]] *] i.ys) ~
347384 ?. =(tag.i.xs u.value.head.i.ys) ~
348385 $(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)))))
349443::
350444:: +read-mold-in: accept the /sur core as provenance. The core must be
351445:: built against zuse or validated Ford imports, and its selected arm
@@ -361,6 +455,8 @@
361455 [%| (crip "Hoon mold `{(trip name)}` is not declared")]
362456 ?. =(typ (~(play ut cor) (ream (cat 3 '*' name))))
363457 [%| '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']
364460 =/ result (read-with module name typ [~ cor])
365461 ?: ?=([%& *] result) result
366462 =/ fallback=(each (unit (each imported @t)) tang)
@@ -461,6 +557,8 @@
461557 [%unsupported p.result]
462558 =/ selected=(each type tang) (mule |.((~(play ut cor) (ream (cat 3 '*' name)))))
463559 ?. ?=(%& -.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']
464562 =/ again=(each imported tang) (mule |.((walk module p.selected catalog ~ [~ cor])))
465563 ?. ?=(%& -.again) [%unsupported p.result]
466564 =/ evidence=(unit import-diagnostic) (first-invalid p.again)
jibb-dev/lib/jibb.hoon+1−1
@@ -6589,7 +6589,7 @@
65896589 ?~ found ~
65906590 ?^ t.found ~
65916591 result.i.found
6592− ?. ?=([%invalid ?(%aura %core) @] raw) ~
6592+ ?. ?=([%invalid ?(%aura %core %overlap) @] raw) ~
65936593 `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
65946594::
65956595:: 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
99are 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
12−collection. Tagged source cases exercise bare null payloads, overlapping tags and hidden
12+collection. `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
1314invalid dependencies, named payload dependencies, valid and collapsed enums,
1415direct and transitively aliased overlaps, nested collections, shadowed jar and
1516jug 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
7878explicit-collapsed: error: Hoon union disjointness could not be verified
7979explicit-subsumed: error: Hoon union disjointness could not be verified
8080explicit-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])
8282explicit-nested: error: Hoon union disjointness could not be verified
8383collection-union-wrapper: valid; forged subject, sample and tail rejected
8484collection-union-list: (list (union [x @ud] [y @t]))
tests/lib/jibb-bridge.hoon+2−2
@@ -136,7 +136,7 @@
136136 [%fixture %raw-rec [%& [%ref %fixture %chain]]]
137137 [%fixture %bad-arity [%& [%apply %list ~[[%atom %t ~] [%atom %ud ~]]]]]
138138 [%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)]
140140 [%fixture %separate-tags (read %separate-tags)]
141141 [%fixture %separate-terms (read %separate-terms)]
142142 [%fixture %nested-choice (read %nested-choice)]
@@ -153,7 +153,7 @@
153153 [%fixture %duplicate [%& [%atom %ud ~]]]
154154 [%missing %title [%& [%atom %t ~]]]
155155 ==
156− =/ report=@t (golden-types-imports:jibb /test/jibb src external)
156+ =/ report=@t (golden-types-with-reader-diagnostics:jibb /test/jibb src external ~)
157157 =/ dep=@t (crip "/- fixture\0a++ chain-id |= x=chain.fixture x\0a")
158158 =/ root=@t (crip "/= helper /ui/helper\0a++ use chain-id.helper\0a")
159159 =/ 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
2929through -test on the fake ship.
3030
3131The 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 `%$`/`?`
33−case records the current conservative limitation, while distinct-tag term
34−singletons are a successful reader/checker control. These are source-aware
32+both 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 overlap error points at the Jibb use site; the Hoon source case
35+positions are not available in this fixture. These are source-aware
3536reads and the checker report remains partial.
tests/type-import/expected.txt+7−4
@@ -104,12 +104,15 @@ partial inference; module not checked
104104++ flag-extra: sample mold is not supported by partial inference
105105++ flag-faced: sample mold is not supported by partial inference
106106++ flag-malformed: sample mold is not supported by partial inference
107−++ mixed-zero: sample mold is not supported by partial inference
108−++ separate-tags: sample mold is not supported by partial inference
107+++ mixed-zero: Hoon union cases overlap
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]]))
109112++ separate-terms: $-(([%left [%$ @t]] [%right [%yes @t]]) ([%left [%$ @t]] [%right [%yes @t]]))
110113reader-collapsed: error: Hoon union disjointness could not be verified
111−reader-mixed-zero: error: a Hoon union needs a source-level disjointness check
112−reader-separate-tags: error: a Hoon union needs a source-level disjointness check
114+reader-mixed-zero: error: Hoon union cases overlap
115+reader-separate-tags: (union [left [ @t]] [right [(union @f:0 @f:1) @t]])
113116reader-separate-terms: (union [left [ @t]] [right [yes @t]])
114117partial inference; module not checked
115118++ 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')