b4703e7 · jibb · git.iko.soy

README.md+2

@@ -44,6 +44,8 @@ tools/hoon --raw --cord src=tests/golden/foo/source.jibb 'tree:(golden /a/b/jibb

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-import-structural-test`, `tools/type-union-source-test`, `tools/type-union-alias-overlap-test`, `tools/type-full-overlap-test`, `tools/type-generic-recursion-test`, `tools/type-generic-construction-test`, `tools/type-generic-pattern-test`, `tools/type-deferred-test`, `tools/type-deferred-prepared-test`, `tools/type-deferred-resolver-test`, `tools/type-deferred-context-test`, `tools/type-empty-test`, `tools/type-cell-branch-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 focused `tools/type-program-main-test` checks the narrow closed, subscription-free `main` slice and its shared fake-ship fixture; it does not run an island or claim runtime watchability.

48+

47### The doc's examples

49### The doc's examples

48

50

49Every code block the design doc labels `jibb` is a golden case, `doc-<tab>-<n>-<what>`, where `<n>` counts the tab's code blocks, labelled or not. To check that none is missing or stale, export the doc's tabs as Markdown and pass the files, or a folder of them:

51Every code block the design doc labels `jibb` is a golden case, `doc-<tab>-<n>-<what>`, where `<n>` counts the tab's code blocks, labelled or not. To check that none is missing or stale, export the doc's tabs as Markdown and pass the files, or a folder of them:

docs/compiler.md+2

@@ -128,6 +128,8 @@ A two-item tuple with an explicit term, null or loobean head can receive payload

128

129`+gate-free-type` is a separate three-way proof over normalized checker types: it reports a gate-free result, a gate-bearing witness with its field path, or unknown. It tracks conservative inhabitance before reporting a gate in a cell, spends one shared node budget, and treats opaque recursion, open variables, unknown collection forms and `*` conservatively. Source-proven `qath` and the recognized list/unit representations have dedicated proofs. `+gate-free-mold-source` parses and resolves one named mold with a fresh active-root graph, retaining the complete prepared prelude, source bundle, trusted reader inputs, dependency cache and inferred mold. It caps classification at 256 nodes; parsing, import resolution and type inference are not covered by that cap. The host must canonicalize paths and bind trusted sources and reader results to their versions. API, store and private roots decline; other definitions and unused imported Hoon bindings are not fully checked. This is mold analysis, not a module, kind, island, watchability or runtime check, and it does not infer general gate-free constraints.

130

131+A full ordinary module may export a narrow checked program `main` only as a direct, unqualified `(program init update view subs)` call with four simple wing arguments, modulo transparent grouping. The canonical prepared prelude must supply both the `program` value and mold. The ordinary source-backed program fit and all normal mold, value and request-graph checks complete first. The inferred `main` must be closed and invariantly match an instantiated `program` mold from that prelude. The initializer must have a closed gate scheme; its data and model contain no open variables and share the existing 256-node gate-free budget, with `%yes` required for both. The named subscription gate must syntactically return null through transparent casts, groups and definition-free bodies. Arbitrary or aliased mains, API/store kinds, gates or unknowns in data/model, and nonempty subscriptions fail closed. This retains source and graph evidence and permits ordinary downstream imports; it neither executes the program nor proves runtime watchability.

132+

131Each case's canonical API identity and source-derived schema travel across imports in a nonrecursive graph certificate containing the exact source bundle, prelude, reserved scope and trusted reader results. Cached interfaces must match those inputs and cannot hide an active ancestor; unknown legacy entries are rebuilt from their unique supplied source. Request-bearing closures are limited to 256 paths and requests. Closed gate samples can also fit when an unnamed input slot corresponds to a named one, provided products are identical and nested value faces and ambiguous cell tails remain intact. This is type inference only: request lowering, runtime schema validation and value watchability proofs are not implemented.

133Each case's canonical API identity and source-derived schema travel across imports in a nonrecursive graph certificate containing the exact source bundle, prelude, reserved scope and trusted reader results. Cached interfaces must match those inputs and cannot hide an active ancestor; unknown legacy entries are rebuilt from their unique supplied source. Request-bearing closures are limited to 256 paths and requests. Closed gate samples can also fit when an unnamed input slot corresponds to a named one, provided products are identical and nested value faces and ambiguous cell tails remain intact. This is type inference only: request lowering, runtime schema validation and value watchability proofs are not implemented.

132

134

133`+golden-types-with-prelude` accepts case-local Jibb module sources alongside `/sur` and mark results and the vendored prelude source. It resolves reachable ordinary library modules in dependency order, caching completed interfaces per invocation and exporting supported closed value schemes, direct generic unions, and simple or nonrecursive generic mold aliases whose bodies the fragment supports. It detects missing sources and cycles and rejects a dependency if its interface cannot be inferred by the fragment. Qualified wings can also read nested fields of an imported value, instantiating that value’s scheme independently at each use; missing, ambiguous and non-record fields remain unsupported.

135`+golden-types-with-prelude` accepts case-local Jibb module sources alongside `/sur` and mark results and the vendored prelude source. It resolves reachable ordinary library modules in dependency order, caching completed interfaces per invocation and exporting supported closed value schemes, direct generic unions, and simple or nonrecursive generic mold aliases whose bodies the fragment supports. It detects missing sources and cycles and rejects a dependency if its interface cannot be inferred by the fragment. Qualified wings can also read nested fields of an imported value, instantiating that value’s scheme independently at each use; missing, ambiguous and non-record fields remain unsupported.

docs/development.md+2

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

91| `tools/type-todo-partial-test` | Reports partial inference of the unchanged todo island through the real API and readers under eval and on the ship |

92| `tools/type-todo-api-test` | Exercises the actual todo API through the real Hoon readers and partial checker |

93| `tools/type-direct-gate-test` | Checks a synthetic source-backed program report and direct gate provenance under eval and on the ship |

94+| `tools/type-program-main-test` | Checks the narrow closed subscription-free program-main interface, downstream import and rejection guards under eval and on the ship |

94| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |

95| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |

95| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |

96| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |

96| `tools/type-nested-union-guards-test` | Checks nested tagged-union case selection and uncertainty under eval and on the ship |

97| `tools/type-nested-union-guards-test` | Checks nested tagged-union case selection and uncertainty under eval and on the ship |

@@ -139,6 +140,7 @@ tools/type-qath-guards-test # qath source and unfolding guards pass

139tools/type-todo-partial-test # unchanged todo partial report and reader failure controls

140tools/type-todo-partial-test # unchanged todo partial report and reader failure controls

140tools/type-todo-api-test # real todo API partial inference and reader guards pass

141tools/type-todo-api-test # real todo API partial inference and reader guards pass

141tools/type-direct-gate-test # direct gate source and provenance guards pass

142tools/type-direct-gate-test # direct gate source and provenance guards pass

143+tools/type-program-main-test # closed program-main interface and rejection guards pass

142tools/type-generic-recursion-test # source-backed recursive identities and provenance

144tools/type-generic-recursion-test # source-backed recursive identities and provenance

143tools/type-generic-construction-test # source-backed recursive construction and bounds

145tools/type-generic-construction-test # source-backed recursive construction and bounds

144tools/type-generic-pattern-test # source-backed recursive patterns and bounds

146tools/type-generic-pattern-test # source-backed recursive patterns and bounds

docs/status.md+6−2

@@ -43,6 +43,8 @@ A separate source-backed analysis can prove one named mold gate-free, report a d

43

44The partial checker can also match a directly named, checked root gate against a generic gate sample in a direct, unshadowed source-backed prelude call. It uses the written two-slot sample layouts to preserve nested record faces, then requires the complete call samples to be closed and tag-free and repeats the fit under the final substitution. The proof falls back to existing inference for unavailable or ambiguous source layouts, local or dynamic gates, aliases, recursive placeholders and open generic caller types. It preserves written-capital checks and projection evidence; it does not add `program`, check islands or prove request watchability. Prepared prelude source and interface remain a trusted pair.

45

46+A narrow full-module path now checks direct four-wing `(program init update view subs)` definitions named `main`. It requires the canonical prepared `program` value and mold, reuses ordinary source-backed program fitting, and publishes only after all ordinary module and request-graph checks. The inferred `main` must be closed and invariantly match the instantiated `program` mold. Initializer data and model must be closed and gate-free with `%yes` verdicts inside a shared 256-node budget, and `subs` must syntactically return null through transparent forms. Aliases, arbitrary mains, API/store kinds, gate-bearing or unknown data/model, mismatched programs and nonempty subscriptions remain rejected. Checked interfaces retain source evidence and support ordinary downstream imports; no program execution or runtime watchability is claimed.

47+

46The API path analyzer can retain its source, complete prepared prelude, reader results and resolved dependencies as evidence, and classify a unique declaration as watchable, not watchable or unknown. It does not yet prove the provenance of request values or check island subscriptions. Prepared artifacts and reader results remain trusted host inputs.

48The API path analyzer can retain its source, complete prepared prelude, reader results and resolved dependencies as evidence, and classify a unique declaration as watchable, not watchable or unknown. It does not yet prove the provenance of request values or check island subscriptions. Prepared artifacts and reader results remain trusted host inputs.

47

49

48For a unique supported path declaration, the request-parts analysis derives ordered typed path parameters, a full-state reply sample and a fold type for one diff mark. Multiple diffs and unsupported or ambiguous evidence fail closed. By itself it does not create request gates or establish watchability of values.

50For a unique supported path declaration, the request-parts analysis derives ordered typed path parameters, a full-state reply sample and a fold type for one diff mark. Multiple diffs and unsupported or ambiguous evidence fail closed. By itself it does not create request gates or establish watchability of values.

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

94Besides the plan's list:

96Besides the plan's list:

95

97

96- 659 golden cases: 439 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.

98- 659 golden cases: 439 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.

97−- The 659-case corpus passed under `urbit eval` in 98.7 s while other checks were running. The fake ship passed all 706 tests, including the source-overlap, structural-overlap, generic-union source and alias-overlap, full-module overlap, deferred-context, generic-recursion, generic-construction, generic-pattern, deferred-inference, empty-mold and cell-branch fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 94.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.

99+- The 659-case corpus passed under `urbit eval` in 90.4 s while other checks were running. The fake ship passed all 707 tests, including the source-overlap, structural-overlap, generic-union source and alias-overlap, full-module overlap, deferred-context, generic-recursion, generic-construction, generic-pattern, deferred-inference, empty-mold and cell-branch fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 86.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.

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

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

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

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

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

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

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

208| 2826c93 | 2026-10-31 | Report generic-alias overlaps and retain deferred branch contexts |

210| 2826c93 | 2026-10-31 | Report generic-alias overlaps and retain deferred branch contexts |

209| b5cdc80 | 2026-10-31 | Preserve full-module overlap source evidence |

211| b5cdc80 | 2026-10-31 | Preserve full-module overlap source evidence |

210| ab6fdc1 | 2026-10-31 | Add source-backed text conversion wrappers |

212| ab6fdc1 | 2026-10-31 | Add source-backed text conversion wrappers |

211−| This change | 2026-10-31 | Recover prepared tuple initializers in partial reports |

213+| aa277c9 | 2026-10-31 | Recover prepared tuple initializers in partial reports |

214+| This change | 2026-10-31 | Check narrow closed subscription-free program mains |

212

215

213## Checking it

216## Checking it

214

217

@@ -246,6 +249,7 @@ tools/type-qath-guards-test # qath source and unfolding guards

246tools/type-ask-guards-test # ask source and bootstrap guards

249tools/type-ask-guards-test # ask source and bootstrap guards

247tools/type-proj-guards-test # projection evidence and scope guards

250tools/type-proj-guards-test # projection evidence and scope guards

248tools/type-module-scope-test # module and prelude scope fixture

251tools/type-module-scope-test # module and prelude scope fixture

252+tools/type-program-main-test # closed program-main interface and rejection guards

249tools/hoon check-spans-test # prints <<>> when the span checker works

253tools/hoon check-spans-test # prints <<>> when the span checker works

250tools/testdata/selftest # the tools themselves

254tools/testdata/selftest # the tools themselves

251tools/doc-blocks docs/spec # the doc's examples are golden cases

255tools/doc-blocks docs/spec # the doc's examples are golden cases

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

@@ -12448,6 +12448,97 @@

12448 [env exports file derived.u.poke elaborations.support ~ `src `graph]

12449 [%& [iface dependencies.ev]]

12450::

12451+:: A checked program main is only the direct four-component source call.

12452+:: Grouping is transparent, but aliases, qualified wings and other module

12453+:: kinds remain outside this slice.

12454+++ program-main-def

12455+ |= ds=(list def)

12456+ ^- (unit def)

12457+ ?~ ds ~

12458+ ?: &(?=(%value -.i.ds) =(%main name.i.ds)) `i.ds

12459+ $(ds t.ds)

12460+::

12461+++ program-main-wing

12462+ |= e=expr

12463+ ^- (unit term)

12464+ ?: ?=(%group -.e) $(e inner.e)

12465+ ?. ?=(%wing -.e) ~

12466+ ?. ?=([@ ~] names.e) ~

12467+ `i.names.e

12468+::

12469+++ program-main-parts

12470+ |= d=def

12471+ ^- (unit [init=term update=term view=term subs=term])

12472+ ?. ?=(%value -.d) ~

12473+ |-

12474+ ?: ?=(%group -.val.d) $(val.d inner.val.d)

12475+ ?. ?=(%call -.val.d) ~

12476+ =/ head=(unit term) (program-main-wing head.val.d)

12477+ ?~ head ~

12478+ ?. =(%program u.head) ~

12479+ ?. ?=([* * * * ~] args.val.d) ~

12480+ =/ args=(list expr) args.val.d

12481+ ?> ?=([* * * * ~] args)

12482+ =/ init=(unit term) (program-main-wing i.args)

12483+ =/ update=(unit term) (program-main-wing i.t.args)

12484+ =/ view=(unit term) (program-main-wing i.t.t.args)

12485+ =/ subs=(unit term) (program-main-wing i.t.t.t.args)

12486+ ?~ init ~

12487+ ?~ update ~

12488+ ?~ view ~

12489+ ?~ subs ~

12490+ `[u.init u.update u.view u.subs]

12491+::

12492+++ program-empty-null

12493+ |= e=expr

12494+ ^- ?

12495+ ?- -.e

12496+ %lit =(%null form.lit.e)

12497+ %cast $(e val.e)

12498+ %group $(e inner.e)

12499+ %body ?~(defs.e $(e final.e) |)

12500+ * |

12501+ ==

12502+::

12503+++ program-subs-empty

12504+ |= d=def

12505+ ^- ?

12506+ ?. ?=(%value -.d) |

12507+ ?- -.val.d

12508+ %gate (program-empty-null body.val.d)

12509+ %gate-wide (program-empty-null body.val.d)

12510+ * |

12511+ ==

12512+::

12513+++ program-main-closed

12514+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile)]

12515+ ^- ?

12516+ ?~ prelude |

12517+ ?~ (ienv-lookup %program values.u.prelude) |

12518+ =/ program=(unit ischeme) (find-jibb-mold %program u.prelude)

12519+ ?~ program |

12520+ =/ main=(unit ischeme) (ienv-lookup %main env)

12521+ ?~ main |

12522+ ?. ?=(~ vars.u.main) |

12523+ ?. ?=(~ (itype-vars typ.u.main)) |

12524+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program *istate)

12525+ =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)

12526+ ?. ?=(%ok -.main-fit) |

12527+ =/ init=(unit ischeme) (ienv-lookup init.parts env)

12528+ ?~ init |

12529+ ?. ?=(~ vars.u.init) |

12530+ ?. ?=(%fn -.typ.u.init) |

12531+ ?. ?=(~ (itype-vars sample.typ.u.init)) |

12532+ ?. ?=(~ (itype-vars product.typ.u.init)) |

12533+ =/ data=igate-free (gate-free-type sample.typ.u.init 256 ~)

12534+ ?. =(%yes verdict.data) |

12535+ =/ model=igate-free (gate-free-type product.typ.u.init left.data ~)

12536+ ?. =(%yes verdict.model) |

12537+ =/ subs=(list def)

12538+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))

12539+ ?. ?=([* ~] subs) |

12540+ (program-subs-empty i.subs)

12541+::

12451++ infer-jibb-file

12542++ infer-jibb-file

12452 |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]

12543 |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]

12453 ^- jfile-result

12544 ^- jfile-result

@@ -12464,6 +12555,8 @@

12464 =/ mod=module p.parsed

12555 =/ mod=module p.parsed

12465 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)

12556 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)

12466 ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]

12557 ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]

12558+ ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))

12559+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]

12467 ?: ?=([%ui %api *] at)

12560 ?: ?=([%ui %api *] at)

12468 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)

12561 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)

12469 ?^ iface

12562 ?^ iface

@@ -12491,7 +12584,10 @@

12491 [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]

12584 [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]

12492 [%| [(crip "module has conflicting names: {(spud at)}") ~]]

12585 [%| [(crip "module has conflicting names: {(spud at)}") ~]]

12493 =/ vals=(list term) (global-value-names defs.mod)

12586 =/ vals=(list term) (global-value-names defs.mod)

12494− ?: (lien vals |=(n=term =(n %main)))

12587+ =/ main=(unit def) (program-main-def defs.mod)

12588+ =/ main-parts=(unit [init=term update=term view=term subs=term])

12589+ ?~(main ~ (program-main-parts u.main))

12590+ ?. ?~(main & &(!?=([%ui %stores *] at) ?=(^ main-parts)))

12495 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]

12591 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]

12496 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)

12592 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)

12497 ?: ?=(%| -.js) [%| p.js]

12593 ?: ?=(%| -.js) [%| p.js]

@@ -12543,6 +12639,8 @@

12543 env

12639 env

12544 ?. (module-values-complete defs.mod env)

12640 ?. (module-values-complete defs.mod env)

12545 [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]

12641 [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]

12642+ ?. ?~(main & ?~(main-parts | (program-main-closed u.main-parts defs.mod env prelude)))

12643+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]

12546 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]

12644 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]

12547 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))

12645 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))

12548 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]

12646 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]

tests/lib/jibb-program-main.hoonnew file+142

@@ -0,0 +1,142 @@

1+:: Narrow closed program-main checking, without execution or watchability claims.

2+/+ jibb

3+/* prelude %jibb /lib/jibb/prelude/jibb

4+/* internal %jibb /lib/jibb/internal/jibb

5+/* source %txt /tests/type-program-main/source/txt

6+/* consumer %txt /tests/type-program-main/consumer/txt

7+/* gate-model %txt /tests/type-program-main/gate-model/txt

8+/* gate-data %txt /tests/type-program-main/gate-data/txt

9+/* nonempty-subs %txt /tests/type-program-main/nonempty-subs/txt

10+/* mismatched-model %txt /tests/type-program-main/mismatched-model/txt

11+/* arbitrary-main %txt /tests/type-program-main/arbitrary-main/txt

12+/* alias-main %txt /tests/type-program-main/alias-main/txt

13+/* open-message %txt /tests/type-program-main/open-message/txt

14+|%

15+++ text

16+ |= lines=wain

17+ ^- @t

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

19+::

20+++ program-prepared

21+ |= [public=@t private=@t]

22+ ^- (unit iprelude:jibb)

23+ =/ extra=@t '\0a+$ element |$ [M] [%node item=M]\0a+$ program |$ [D X M]\0a [init=$-(D X) update=$-([M X] [X (list (cmd M))]) view=$-(X (element M)) subs=$-(X (list (sub M)))]\0a++ program |= [init=$-(D X) update=$-([M X] [X (list (cmd M))]) view=$-(X (element M)) subs=$-(X (list (sub M)))]\0a ^- (program D X M) [init update view subs]\0a'

24+ (prepare-prelude-with-internal:jibb (cat 3 public extra) private)

25+::

26+++ program-main-detailed

27+ |= [at=path src=@t modules=jbundle:jibb prepared=iprelude:jibb]

28+ ^- jfile-detailed-result:jibb

29+ (infer-jibb-file-detailed:jibb at src ~ ~ modules ~[at] values.prepared molds.prepared ~ `iface.prepared)

30+::

31+++ program-main-legacy

32+ |= [at=path src=@t modules=jbundle:jibb prepared=iprelude:jibb]

33+ ^- jfile-result:jibb

34+ (infer-jibb-file:jibb at src ~ ~ modules ~[at] values.prepared molds.prepared ~ `iface.prepared)

35+::

36+++ program-main-negative-errors

37+ |= [label=@t at=path src=@t prepared=iprelude:jibb]

38+ ^- (list tape)

39+ =/ detailed=jfile-detailed-result:jibb (program-main-detailed at src ~ prepared)

40+ ?: ?=(%& -.detailed) ~[(weld (trip label) ": structured check accepted")]

41+ ?. ?=(~ overlap.p.detailed) ~[(weld (trip label) ": unexpected overlap evidence")]

42+ =/ legacy=jfile-result:jibb (program-main-legacy at src ~ prepared)

43+ ?: ?=(%& -.legacy) ~[(weld (trip label) ": legacy check accepted")]

44+ ?. =(p.legacy message.p.detailed) ~[(weld (trip label) ": adapter messages differ")]

45+ ~

46+::

47+++ program-main-errors

48+ |= [public=@t private=@t island=@t downstream=@t negatives=(list @t)]

49+ ^- (list tape)

50+ =/ prepared=(unit iprelude:jibb)

51+ (program-prepared public private)

52+ ?~ prepared ~["synthetic program prelude did not prepare"]

53+ =/ at=path /tests/program-main/island/jibb

54+ =/ detailed=jfile-detailed-result:jibb (program-main-detailed at island ~ u.prepared)

55+ ?: ?=(%| -.detailed) ~["direct closed program main was rejected"]

56+ =/ checked=ifile:jibb iface.p.detailed

57+ =/ legacy=jfile-result:jibb (program-main-legacy at island ~ u.prepared)

58+ ?: ?=(%| -.legacy) ~["legacy adapter rejected a closed program main"]

59+ ?. =(values.checked values.iface.p.legacy) ~["structured and legacy interface values differ"]

60+ =/ init=(unit ischeme:jibb) (ienv-lookup:jibb %init values.checked)

61+ =/ update=(unit ischeme:jibb) (ienv-lookup:jibb %update values.checked)

62+ =/ view=(unit ischeme:jibb) (ienv-lookup:jibb %view values.checked)

63+ =/ subs=(unit ischeme:jibb) (ienv-lookup:jibb %subs values.checked)

64+ =/ main=(unit ischeme:jibb) (ienv-lookup:jibb %main values.checked)

65+ ?~ init ~["init interface is missing"]

66+ ?~ update ~["update interface is missing"]

67+ ?~ view ~["view interface is missing"]

68+ ?~ subs ~["subs interface is missing"]

69+ ?~ main ~["main interface is missing"]

70+ =/ parsed (parse:jibb at island)

71+ ?: ?=(%| -.parsed) ~["program source no longer parses"]

72+ =/ main-def=(unit def:jibb) (program-main-def:jibb defs.p.parsed)

73+ ?~ main-def ~["program main definition is missing"]

74+ =/ parts (program-main-parts:jibb u.main-def)

75+ ?~ parts ~["program main parts are missing"]

76+ ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked ~)

77+ ~["program kind was accepted without its source-backed prelude"]

78+ =/ program-scheme=(unit ischeme:jibb) (ienv-lookup:jibb %program values.iface.u.prepared)

79+ ?~ program-scheme ~["synthetic program scheme is missing"]

80+ ?. ?=(%fn -.typ.u.program-scheme) ~["synthetic program value is not a gate"]

81+ =/ broken-values=ienv:jibb

82+ (skim values.iface.u.prepared |=(entry=[name=term scheme=ischeme:jibb] !=(%program name.entry)))

83+ =/ broken=ifile:jibb

84+ iface.u.prepared(values [[%program [[%fn sample.typ.u.program-scheme [%atom %ud]] vars.u.program-scheme]] broken-values])

85+ =/ malformed=jfile-detailed-result:jibb

86+ (infer-jibb-file-detailed:jibb at island ~ ~ ~ ~[at] values.u.prepared molds.u.prepared ~ `broken)

87+ ?: ?=(%& -.malformed) ~["program result was not checked against the program mold"]

88+ =/ kind-error=@t (crip "module kind needs unsupported inference: {(spud at)}")

89+ ?. =(message.p.malformed kind-error) ~["malformed program failed before the kind check"]

90+ =/ open=jfile-detailed-result:jibb

91+ (program-main-detailed at (snag 6 negatives) ~ u.prepared)

92+ ?: ?=(%& -.open) ~["open program message was accepted"]

93+ =/ other-values=ienv:jibb

94+ (skim values.checked |=(entry=[name=term scheme=ischeme:jibb] !=(%main name.entry)))

95+ =/ open-values=ienv:jibb [[%main u.main(vars ~[0])] other-values]

96+ ?: (program-main-closed:jibb u.parts defs.p.parsed open-values `iface.u.prepared)

97+ ~["generic main scheme passed the closure check"]

98+ =/ model=itype:jibb [%face %count [%atom %ud]]

99+ ?. =(u.init [[%fn [%atom %t] model] ~]) ~["init interface type differs"]

100+ ?. ?=(~ vars.u.main) ~["main interface is not closed"]

101+ =/ init-fields=(list itype:jibb) (record-fields-named:jibb %init typ.u.main ~)

102+ =/ update-fields=(list itype:jibb) (record-fields-named:jibb %update typ.u.main ~)

103+ =/ view-fields=(list itype:jibb) (record-fields-named:jibb %view typ.u.main ~)

104+ =/ subs-fields=(list itype:jibb) (record-fields-named:jibb %subs typ.u.main ~)

105+ ?. =(init-fields ~[typ.u.init]) ~["main initializer field differs"]

106+ ?. &(=(1 (lent update-fields)) =(1 (lent view-fields)) =(1 (lent subs-fields)))

107+ ~["main component fields differ"]

108+ ?~ source.checked ~["program source evidence is missing"]

109+ ?. =(u.source.checked island) ~["program source evidence differs"]

110+ ?~ graph.checked ~["program request graph evidence is missing"]

111+ =/ consumer-at=path /tests/program-main/consumer/jibb

112+ =/ imported=jfile-detailed-result:jibb

113+ (program-main-detailed consumer-at downstream ~[[at island]] u.prepared)

114+ ?: ?=(%| -.imported) ~["ordinary downstream program import was rejected"]

115+ =/ use=(unit ischeme:jibb) (ienv-lookup:jibb %imported values.iface.p.imported)

116+ ?~ use ~["downstream imported initializer is missing"]

117+ ?. =(u.use u.init) ~["downstream imported initializer type differs"]

118+ ?. =(7 (lent negatives)) ~["focused negative fixture count differs"]

119+ =/ cases=(list [label=@t at=path src=@t])

120+ :~ ['gate in model' at (snag 0 negatives)]

121+ ['gate in data' at (snag 1 negatives)]

122+ ['nonempty subs' at (snag 2 negatives)]

123+ ['mismatched model' at (snag 3 negatives)]

124+ ['arbitrary main' at (snag 4 negatives)]

125+ ['store path' /ui/stores/program-main/jibb island]

126+ ['program alias' at (snag 5 negatives)]

127+ ==

128+ (zing (turn cases |=(c=[label=@t at=path src=@t] (program-main-negative-errors label.c at.c src.c u.prepared))))

129+::

130+++ test-program-main

131+ ^- tang

132+ =/ negatives=(list @t)

133+ :~ (text gate-model)

134+ (text gate-data)

135+ (text nonempty-subs)

136+ (text mismatched-model)

137+ (text arbitrary-main)

138+ (text alias-main)

139+ (text open-message)

140+ ==

141+ (turn (program-main-errors prelude internal (text source) (text consumer) negatives) |=(reason=tape leaf+reason))

142+--

tests/type-program-main/about.txtnew file+1

@@ -0,0 +1 @@

1+tests: A direct four-wing program main uses the ordinary source-backed program fit. Its init data and model are closed and gate-free within the shared 256-node budget, and subs syntactically returns null through transparent forms. The fixture checks exported and downstream imported types, source evidence, structured and legacy adapters, and fail-closed controls. It does not execute a program or establish runtime watchability.

tests/type-program-main/alias-main.txtnew file+11

@@ -0,0 +1,11 @@

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud]

5+++ main (program-alias init update view subs)

6+++ init |= input=@t ^- model [count=0]

7+++ update |= [msg=message state=model]

8+ ^- [model (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model ^- (list (sub message)) ~

11+++ program-alias program

tests/type-program-main/arbitrary-main.txtnew file+10

@@ -0,0 +1,10 @@

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud]

5+++ main init

6+++ init |= input=@t ^- model [count=0]

7+++ update |= [msg=message state=model]

8+ ^- [model (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model ^- (list (sub message)) ~

tests/type-program-main/consumer.txtnew file+2

@@ -0,0 +1,2 @@

1+/= island /tests/program-main/island

2+++ imported init.main.island

tests/type-program-main/gate-data.txtnew file+10

@@ -0,0 +1,10 @@

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud]

5+++ main (program init update view subs)

6+++ init |= input=$-(@t @t) ^- model [count=0]

7+++ update |= [msg=message state=model]

8+ ^- [model (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model ^- (list (sub message)) ~

tests/type-program-main/gate-model.txtnew file+11

@@ -0,0 +1,11 @@

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud callback=$-(@t @t)]

5+++ main (program init update view subs)

6+++ init |= input=@t ^- model [count=0 callback=echo]

7+++ update |= [msg=message state=model]

8+ ^- [model (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model ^- (list (sub message)) ~

11+++ echo |= input=@t input

tests/type-program-main/mismatched-model.txtnew file+10

@@ -0,0 +1,10 @@

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud]

5+++ main (program init update view subs)

6+++ init |= input=@t ^- model [count=0]

7+++ update |= [msg=message state=@p]

8+ ^- [@p (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model ^- (list (sub message)) ~

tests/type-program-main/nonempty-subs.txtnew file+12

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

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud]

5+++ main (program init update view subs)

6+++ init |= input=@t ^- model [count=0]

7+++ update |= [msg=message state=model]

8+ ^- [model (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model

11+ ^- (list (sub message))

12+ ~[[%watch (pure %start)]]

tests/type-program-main/open-message.txtnew file+7

@@ -0,0 +1,7 @@

1++$ model [count=@ud]

2+++ main (program init update view subs)

3+++ init |= input=@t ^- model [count=0]

4+++ update |= [msg=M state=model]

5+ ^- [model (list (cmd M))] [state ~]

6+++ view |= state=model ^- (element M) [%node !!]

7+++ subs |= state=model ^- (list (sub M)) ~

tests/type-program-main/source.txtnew file+12

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

1++$ message

2+ %start

3+ %stop

4++$ model [count=@ud]

5+++ main (program (init) update view subs)

6+++ init |= input=@t ^- model [count=0]

7+++ update |= [msg=message state=model]

8+ ^- [model (list (cmd message))] [state ~]

9+++ view |= state=model ^- (element message) [%node %start]

10+++ subs |= state=model

11+ ^- (list (sub message))

12+ (~)

tools/testdata/ship-selftest+5

@@ -324,6 +324,7 @@ def generator_checks(tmp):

324 'tests/lib/jibb-closed-gate-guards.hoon',

325 'tests/lib/jibb-direct-gate-guards.hoon',

326 'tests/lib/jibb-direct-gate-source.hoon',

327+ 'tests/lib/jibb-program-main.hoon',

327 'tests/lib/jibb-todo-api.hoon',

328 'tests/lib/jibb-todo-api.hoon',

328 'tests/lib/jibb-todo-partial.hoon',

329 'tests/lib/jibb-todo-partial.hoon',

329 'tests/lib/jibb-constructor-fit-guards.hoon',

330 'tests/lib/jibb-constructor-fit-guards.hoon',

@@ -395,6 +396,10 @@ def generator_checks(tmp):

395 check('direct gate source and golden are assembled',

396 check('direct gate source and golden are assembled',

396 {'tests/type-direct-gate/source.txt', 'tests/type-direct-gate/expected.txt'}

397 {'tests/type-direct-gate/source.txt', 'tests/type-direct-gate/expected.txt'}

397 <= set(normal.files))

398 <= set(normal.files))

399+ check('program main sources and shared fixture are assembled',

400+ {f'tests/type-program-main/{name}.txt' for name in (

401+ 'source', 'consumer', 'gate-model', 'gate-data', 'nonempty-subs',

402+ 'mismatched-model', 'arbitrary-main', 'alias-main', 'open-message')} <= set(normal.files))

398 check('todo partial golden and reused sources are assembled',

403 check('todo partial golden and reused sources are assembled',

399 {'tests/type-todo-partial/expected.txt', 'tests/type-gate-free/todo.txt',

404 {'tests/type-todo-partial/expected.txt', 'tests/type-gate-free/todo.txt',

400 'tests/type-api-paths/api.txt'} <= set(normal.files))

405 'tests/type-api-paths/api.txt'} <= set(normal.files))

tools/type-program-main-testnew file+46

@@ -0,0 +1,46 @@

1+#!/usr/bin/env python3

2+"""Run the shared closed program-main checks under eval."""

3+from pathlib import Path

4+import argparse

5+import subprocess

6+import sys

7+import tempfile

8+

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

10+parser = argparse.ArgumentParser(description=__doc__)

11+parser.add_argument('--lib', default=str(root / 'jibb-dev/lib/jibb.hoon'))

12+args = parser.parse_args()

13+

14+def body(name):

15+ text = (root / 'tests/lib' / name).read_text()

16+ return text[text.index('\n|%\n') + 1:]

17+

18+names = ('source', 'consumer', 'gate-model', 'gate-data', 'nonempty-subs',

19+ 'mismatched-model', 'arbitrary-main', 'alias-main', 'open-message')

20+expression = ('=/ jibb .\n=/ prelude=@t prelude-text\n'

21+ '=/ internal=@t internal-text\n' +

22+ ''.join('=/ ' + name + '=wain (to-wain:format ' + name + '-text)\n'

23+ for name in names) +

24+ '=/ expected=wain ~\n=/ suite\n' + body('jibb-program-main.hoon') +

25+ '\n=/ negatives=(list @t)\n :~ (text:suite gate-model)\n'

26+ ' (text:suite gate-data)\n (text:suite nonempty-subs)\n'

27+ ' (text:suite mismatched-model)\n (text:suite arbitrary-main)\n'

28+ ' (text:suite alias-main)\n (text:suite open-message)\n ==\n'

29+ '=/ failures=(list tape) (program-main-errors:suite prelude internal (text:suite source) (text:suite consumer) negatives)\n'

30+ '^- @t\n?~ failures \'program main checks passed\'\n'

31+ '(of-wain:format (turn failures crip))\n')

32+with tempfile.TemporaryDirectory(prefix='jibb-program-main-') as tmp:

33+ program = Path(tmp) / 'program-main.hoon'

34+ program.write_text(expression)

35+ command = [str(root / 'tools/hoon'), '--lib', args.lib, '--raw', '-f', str(program),

36+ '--cord', 'prelude-text=' + str(root / 'jibb-dev/lib/jibb/prelude.jibb'),

37+ '--cord', 'internal-text=' + str(root / 'jibb-dev/lib/jibb/internal.jibb')]

38+ for name in names:

39+ command += ['--cord', name + '-text=' + str(root / 'tests/type-program-main' / (name + '.txt'))]

40+ result = subprocess.run(command, stdout=subprocess.PIPE)

41+if result.returncode:

42+ sys.exit(result.returncode)

43+if result.stdout != b'program main checks passed\n':

44+ sys.stderr.buffer.write(result.stdout)

45+ sys.exit(1)

46+print('closed program-main interface and rejection guards passed')