git.iko.soy/jibb
on master help sign in
Prove direct request watchability for programs

Allow a program subscription to be one direct imported plain request whose member has the exact derived-gate scheme and whose unique evidence is present in the interface's own merged graph. Check API source and case-name identity, and reject scry paths, diffs, parameters, aliases, and hand-built requests. Run the kind check after graph merging and cover forged, detached, ambiguous, indirect, and runtime-unverified cases under eval and ship.

commit642d2c0457ad60c833895bb44a943d2c8dc19f75 authoriko <mail@iko.soy> dateSun 1 Nov 2026, 04:49 (1 day ago) parent26bf7a7
10 files changed+344−14
compare with master
unifiedsplit
README.md+1−1 docs/compiler.md+1−1 docs/development.md+1 docs/status.md+6−5 jibb-dev/lib/jibb.hoon+69−4 tests/lib/jibb-program-main.hoon+3−3 tests/lib/jibb-program-watch.hoon+210 tests/type-program-watch/about.txt+1 tools/testdata/ship-selftest+4 tools/type-program-watch-test+48
README.md+1−1
@@ -44,7 +44,7 @@ tools/hoon --raw --cord src=tests/golden/foo/source.jibb 'tree:(golden /a/b/jibb
4444
4545`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.
4646
47−The focused `tools/type-program-main-test` checks the narrow closed, subscription-free `main` slice and its shared fake-ship fixture. `tools/type-program-init-test` checks transactional initializer recovery for a synthetic direct program, including exact exported and imported types and rejection boundaries. Neither runs an island or claims runtime watchability.
47+The focused `tools/type-program-main-test` checks the narrow closed, subscription-free `main` slice and its shared fake-ship fixture. `tools/type-program-init-test` checks transactional initializer recovery for a synthetic direct program, including exact exported and imported types and rejection boundaries. `tools/type-program-watch-test` uses the real todo readers with synthetic program components to check one direct request value against merged API-source evidence and reject hand-built, indirect, parameterized, diff and ambiguous subscriptions. These are static checks only: they do not run an island or establish runtime watching.
4848
4949### The doc's examples
5050
docs/compiler.md+1−1
@@ -128,7 +128,7 @@ A two-item tuple with an explicit term, null or loobean head can receive payload
128128
129129`+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.
130130
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.
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 may syntactically return null through transparent casts, groups and definition-free bodies. Alternatively, after a successful request-graph merge, it may return one singleton list containing an unfaced `[%watch request]` pair whose request is a direct `case.face` call with one direct constructor callback. The face must resolve to an imported interface whose member has the exact plain derived-request scheme. Exactly one merged request evidence must match its API path and case, agree with the declaration's inner name, and appear in that interface's own graph; the interface source must equal the evidence's API source. The declaration must have no scry, diffs or path parameters. Pure or hand-built requests, helpers, aliases, re-exports, typed paths, folds, multiple subscriptions and missing or ambiguous evidence fail closed. Arbitrary or aliased mains, API/store kinds, and gates or unknowns in data/model also fail closed. This retains source and graph evidence and permits ordinary downstream imports; it neither executes the program nor implements runtime watching.
132132
133133When only that program's initializer and `main` are unresolved, a bounded transactional retry can derive the initializer's expected gate from the resolved update, view and subscription components. It instantiates all schemes above the greatest variable ID in the module and prelude, reuses the source-backed positional fit and stable replay, and leaves only the initializer's data variable open. The named initializer must be a direct gate whose transparent body is a tuple ending in null. Its own sample fixes data; ordinary inference, product and whole-gate fits, pending-tag and finalization checks, and a fresh ordinary `main` inference must all succeed before the ordinary kind and graph checks publish anything. Aliases, non-main libraries, simultaneous unresolved subscriptions, nonempty subscriptions and unrelated pending tags decline.
134134
docs/development.md+1
@@ -93,6 +93,7 @@ git clone https://github.com/urbit/tools /root/src/tools
9393| `tools/type-direct-gate-test` | Checks a synthetic source-backed program report and direct gate provenance under eval and on the ship |
9494| `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 |
9595| `tools/type-program-init-test` | Checks transactional direct-program initializer recovery, exact exported/imported types and fail-closed boundaries under eval and on the ship |
96+| `tools/type-program-watch-test` | Checks direct singleton request-value watchability against merged real-todo evidence, exact types/imports and rejection boundaries under eval and on the ship |
9697| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |
9798| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |
9899| `tools/type-nested-union-guards-test` | Checks nested tagged-union case selection and uncertainty under eval and on the ship |
docs/status.md+6−5
@@ -35,7 +35,7 @@ A prepared-prelude partial report can recover a narrow import-free, non-main ord
3535
3636Closed cell context can now flow through a bounded loobean branch while preserving the inferred value faces and original failed-inference behavior. Open or structurally uncertain substitutions and nested retry shapes remain unsupported. This does not by itself provide the missing text and UI prelude definitions, cross-definition context, island-kind checks, or watchability evidence needed by the unchanged todo island.
3737
38−The internal prelude defines a transparent generic `ask` with pure, agent and store cases, re-exported alongside the Jibb-written `pure` gate. The partial checker infers supported constructors and exhaustive matches. Agent and store receivers operate on raw nouns; their fields do not prove schema validity or watchability. The public prelude now defines the documented source-backed `sub` union; supported `%watch` payloads retain the public `(ask M)` type. Constructing a `sub` does not prove that its request is watchable. Request lowering, checked decoding, runtime validation and island watch checking remain unimplemented.
38+The internal prelude defines a transparent generic `ask` with pure, agent and store cases, re-exported alongside the Jibb-written `pure` gate. The partial checker infers supported constructors and exhaustive matches. Agent and store receivers operate on raw nouns; their fields do not prove schema validity or watchability. The public prelude now defines the documented source-backed `sub` union; supported `%watch` payloads retain the public `(ask M)` type. Constructing a `sub` does not prove that its request is watchable. Request lowering, checked decoding, runtime validation and general island watch checking remain unimplemented; the separate direct-program proof below covers only one narrow static value shape.
3939
4040Known same-origin generic-union result context can now constrain a call before its arguments are inferred. An unresolved or opaque constructor target stays unsupported rather than producing a definite mismatch; proven missing tags still report errors. A todo request with explicit `(ask msg)` context can infer `|=%got`; its uncontextualized form remains unsupported. A two-item literal-headed tuple can receive payload context from a known union of uniquely headed literal cells when its payload is a shallow wing-headed call with literal, wing or constructor arguments. Existing inference takes precedence when it fits; otherwise the checker tries the contextual path once. It conservatively declines that path when any substitution has a structural root, as well as for duplicate or opaque competitors. The guard scans substitutions per eligible tuple and may add one shallow inference; no global linear-time bound is claimed. This allows an explicitly typed todo subscription body to infer, but does not check the island or prove request watchability.
4141
@@ -43,9 +43,9 @@ A separate source-backed analysis can prove one named mold gate-free, report a d
4343
4444The 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.
4545
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. A transactional extension can recover a direct initializer whose transparent tuple body ends in null when update, view and subs are already resolved. It derives the expected gate through the ordinary positional program fit with fresh IDs and stable replay, then re-infers the actual initializer and `main` under all ordinary finalization and kind checks. Non-main libraries, aliases, nonempty or simultaneously unresolved subscriptions, and unrelated pending tags remain rejected.
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. `subs` may syntactically return null through transparent forms, or one direct imported request watch after the request graph merges. The latter is only an unfaced two-item `[%watch (case.face |=%callback)]` singleton: the imported member must have the exact plain derived-request scheme, a unique merged request must match the API path and both case names and occur in the interface's own graph, the API source must be identical, and scry, diffs and parameters must be absent. Pure or hand-built values, helpers, aliases, re-exports, typed paths, folds, multiple watches and unknown or ambiguous evidence remain rejected. Checked interfaces retain source evidence and support ordinary downstream imports; no program execution or runtime watching is claimed. A transactional extension can recover a direct initializer whose transparent tuple body ends in null when update, view and subs are already resolved. It derives the expected gate through the ordinary positional program fit with fresh IDs and stable replay, then re-infers the actual initializer and `main` under all ordinary finalization and kind checks. Non-main libraries, aliases, nonempty or simultaneously unresolved subscriptions, and unrelated pending tags remain rejected.
4747
48−The 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.
48+The 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. This remains declaration evidence rather than proof about an arbitrary request value. The narrow direct-program check above composes it with final value syntax, resolved imports and merged evidence for one plain request. Prepared artifacts and reader results remain trusted host inputs.
4949
5050For 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.
5151
@@ -96,7 +96,7 @@ What the plan asks for, and where it is:
9696Besides the plan's list:
9797
9898- 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.
99−- The 659-case corpus passed under `urbit eval` in 92.8 s while other checks were running. The fake ship passed all 708 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 93.1 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 92.8 s while other checks were running. The fake ship passed all 709 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 91.9 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.
100100- `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.
101101- 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.
102102- 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).
@@ -212,7 +212,8 @@ Besides the plan's list:
212212| ab6fdc1 | 2026-10-31 | Add source-backed text conversion wrappers |
213213| aa277c9 | 2026-10-31 | Recover prepared tuple initializers in partial reports |
214214| b4703e7 | 2026-11-01 | Check narrow closed subscription-free program mains |
215−| This change | 2026-11-01 | Recover narrow direct-program initializer contexts |
215+| 26bf7a7 | 2026-11-01 | Recover narrow direct-program initializer contexts |
216+| This change | 2026-11-01 | Prove direct request-value watchability for program subscriptions |
216217
217218## Checking it
218219
jibb-dev/lib/jibb.hoon+69−4
@@ -12668,8 +12668,73 @@
1266812668 ?~ (ienv-lookup %main env.completed) ~
1266912669 `[env.completed grouped.resolution artifacts.completed]
1267012670::
12671+++ program-subs-watch
12672+ |= [d=def imports=ijimports graph=irequest-graph prelude=ifile]
12673+ ^- ?
12674+ ?. ?=(%value -.d) |
12675+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
12676+ =/ body=expr
12677+ ?- -.val.d
12678+ %gate body.val.d
12679+ %gate-wide body.val.d
12680+ * val.d
12681+ ==
12682+ =. body (program-transparent body)
12683+ ?. ?=(%list -.body) |
12684+ ?. ?=([* ~] items.body) |
12685+ =/ watch=expr (program-transparent i.items.body)
12686+ ?. ?=(%tuple -.watch) |
12687+ ?. ?=([* * ~] items.watch) |
12688+ =/ tag=item i.items.watch
12689+ =/ payload=item i.t.items.watch
12690+ ?. &(?=(~ face.tag) ?=(~ face.payload)) |
12691+ =/ tag-expr=expr (program-transparent val.tag)
12692+ ?. ?=(%lit -.tag-expr) |
12693+ ?. &(?=(%term form.lit.tag-expr) =(%watch val.lit.tag-expr)) |
12694+ =/ request=expr (program-transparent val.payload)
12695+ ?. ?=(%call -.request) |
12696+ ?. ?=([* ~] args.request) |
12697+ =/ head=expr (program-transparent head.request)
12698+ ?. ?=(%wing -.head) |
12699+ ?. ?=([@ @ ~] names.head) |
12700+ =/ case=term i.names.head
12701+ =/ face=term i.t.names.head
12702+ =/ callback=expr (program-transparent i.args.request)
12703+ ?. ?=(%ctor -.callback) |
12704+ ?. ?=(%term form.tag.callback) |
12705+ =/ selected=(list [face=term interface=ifile])
12706+ (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
12707+ ?. ?=([* ~] selected) |
12708+ =/ iface=ifile interface.i.selected
12709+ =/ member=(unit ischeme) (ienv-lookup case values.iface)
12710+ ?~ member |
12711+ ?~ source.iface |
12712+ =/ evidence=(list irequest-evidence)
12713+ (skim requests.graph |=(r=irequest-evidence &(=(api-at.r at.iface) =(name.r case))))
12714+ ?. ?=([* ~] evidence) |
12715+ =/ request-evidence=irequest-evidence i.evidence
12716+ ?. =(u.source.iface api-source.request-evidence) |
12717+ ?. =(name.path.path.request-evidence case) |
12718+ ?~ graph.iface |
12719+ ?. (lien requests.u.graph.iface |=(r=irequest-evidence =(r request-evidence))) |
12720+ ?. ?=(~ scry.path.path.request-evidence) |
12721+ ?. &(?=(~ diffs.path.request-evidence) ?=(~ diffs.path.path.request-evidence)) |
12722+ ?: (lien segments.path.path.request-evidence |=(p=pseg !?=(%knot -.p))) |
12723+ ?. ?=([@ ~] vars.u.member) |
12724+ =/ message=@ud i.vars.u.member
12725+ ?. ?=(%fn -.typ.u.member) |
12726+ ?. ?=(%fn -.sample.typ.u.member) |
12727+ ?. =(sample.sample.typ.u.member full.path.request-evidence) |
12728+ ?. =(product.sample.typ.u.member [%var message]) |
12729+ =/ prep=iprelude [prelude prelude-values.graph prelude-molds.graph]
12730+ =/ ask=(unit ischeme) (request-compatible-ask prep)
12731+ ?~ ask |
12732+ =/ result=(unit itype) (template-apply u.ask ~[[%var message]])
12733+ ?~ result |
12734+ =(product.typ.u.member u.result)
12735+::
1267112736++ program-main-closed
12672− |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile)]
12737+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
1267312738 ^- ?
1267412739 ?~ prelude |
1267512740 ?~ (ienv-lookup %program values.u.prelude) |
@@ -12695,7 +12760,7 @@
1269512760 =/ subs=(list def)
1269612761 (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
1269712762 ?. ?=([* ~] subs) |
12698− (program-subs-empty i.subs)
12763+ |((program-subs-empty i.subs) (program-subs-watch i.subs imports graph u.prelude))
1269912764::
1270012765++ infer-jibb-file
1270112766 |= [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)]
@@ -12804,11 +12869,11 @@
1280412869 env
1280512870 ?. (module-values-complete defs.mod env)
1280612871 [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
12807− ?. ?~(main & ?~(main-parts | (program-main-closed u.main-parts defs.mod env prelude)))
12808− [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
1280912872 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
1281012873 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
1281112874 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
12875+ ?. ?~(main & ?~(main-parts | (program-main-closed u.main-parts defs.mod env prelude resolved.p.js u.graph)))
12876+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
1281212877 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
1281312878 [%& [iface [[at iface] cache.p.js]]]
1281412879::
tests/lib/jibb-program-main.hoon+3−3
@@ -54,6 +54,7 @@
5454 =/ detailed=jfile-detailed-result:jibb (program-main-detailed at island ~ u.prepared)
5555 ?: ?=(%| -.detailed) ~["direct closed program main was rejected"]
5656 =/ checked=ifile:jibb iface.p.detailed
57+ ?~ graph.checked ~["program request graph evidence is missing"]
5758 =/ legacy=jfile-result:jibb (program-main-legacy at island ~ u.prepared)
5859 ?: ?=(%| -.legacy) ~["legacy adapter rejected a closed program main"]
5960 ?. =(values.checked values.iface.p.legacy) ~["structured and legacy interface values differ"]
@@ -73,7 +74,7 @@
7374 ?~ main-def ~["program main definition is missing"]
7475 =/ parts (program-main-parts:jibb u.main-def)
7576 ?~ parts ~["program main parts are missing"]
76− ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked ~)
77+ ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked ~ ~ u.graph.checked)
7778 ~["program kind was accepted without its source-backed prelude"]
7879 =/ program-scheme=(unit ischeme:jibb) (ienv-lookup:jibb %program values.iface.u.prepared)
7980 ?~ program-scheme ~["synthetic program scheme is missing"]
@@ -93,7 +94,7 @@
9394 =/ other-values=ienv:jibb
9495 (skim values.checked |=(entry=[name=term scheme=ischeme:jibb] !=(%main name.entry)))
9596 =/ 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+ ?: (program-main-closed:jibb u.parts defs.p.parsed open-values `iface.u.prepared ~ u.graph.checked)
9798 ~["generic main scheme passed the closure check"]
9899 =/ model=itype:jibb [%face %count [%atom %ud]]
99100 ?. =(u.init [[%fn [%atom %t] model] ~]) ~["init interface type differs"]
@@ -107,7 +108,6 @@
107108 ~["main component fields differ"]
108109 ?~ source.checked ~["program source evidence is missing"]
109110 ?. =(u.source.checked island) ~["program source evidence differs"]
110− ?~ graph.checked ~["program request graph evidence is missing"]
111111 =/ consumer-at=path /tests/program-main/consumer/jibb
112112 =/ imported=jfile-detailed-result:jibb
113113 (program-main-detailed consumer-at downstream ~[[at island]] u.prepared)
tests/lib/jibb-program-watch.hoonnew file+210
@@ -0,0 +1,210 @@
1+:: Direct request-value watchability for a synthetic program over the real todo API.
2+/+ jibb, jibb-import
3+/* prelude %jibb /lib/jibb/prelude/jibb
4+/* internal %jibb /lib/jibb/internal/jibb
5+/* sur %txt /tests/type-api-paths/todo-sur/txt
6+/* action %txt /tests/type-api-paths/todo-action/txt
7+/* todos %txt /tests/type-api-paths/todos/txt
8+/* update %txt /tests/type-api-paths/todo-update/txt
9+/* item %txt /tests/type-api-paths/todo-item/txt
10+/* api %txt /tests/type-api-paths/api/txt
11+|%
12+++ text
13+ |= lines=wain
14+ ^- @t
15+ (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))
16+::
17+++ program-watch-prepared
18+ |= [public=@t private=@t]
19+ ^- (unit iprelude:jibb)
20+ =/ 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'
21+ (prepare-prelude-with-internal:jibb (cat 3 public extra) private)
22+::
23+++ program-watch-detailed
24+ |= [at=path src=@t externals=iexternals:jibb marks=imark-externals:jibb modules=jbundle:jibb prepared=iprelude:jibb]
25+ ^- jfile-detailed-result:jibb
26+ (infer-jibb-file-detailed:jibb at src externals marks modules ~[at] values.prepared molds.prepared ~ `iface.prepared)
27+::
28+++ program-watch-source
29+ |= [extra=@t subscriptions=@t]
30+ ^- @t
31+ %+ rap 3
32+ :~ '/= api /ui/api/todo\0a'
33+ '+$ model [count=@ud]\0a'
34+ '+$ msg\0a [%got todos=(list item.api)]\0a [%one item=todo-item.api]\0a %other\0a'
35+ extra
36+ '++ main (program init update view subs)\0a'
37+ '++ init |= input=@t ^- model [count=0]\0a'
38+ '++ update |= [m=msg state=model]\0a ^- [model (list (cmd msg))] [state ~]\0a'
39+ '++ view |= state=model ^- (element msg) [%node %other]\0a'
40+ subscriptions
41+ ==
42+::
43+++ program-watch-agent-source
44+ ^- @t
45+ %+ rap 3
46+ :~ '/= api /ui/api/todo\0a'
47+ '+$ model [count=@ud]\0a'
48+ '++ receive |= input=[mark=@tas state=(unit *) fact=*]\0a ^- [state=* message=@t] [state=0 message="ok"]\0a'
49+ '++ request-path ^- path ~[%todos]\0a'
50+ '++ request ^- (ask @t)\0a [%agent api="/ui/api/todo" case=%todos agent=%todo path=request-path scry=~ receive=receive]\0a'
51+ '++ main (program init update view subs)\0a'
52+ '++ init |= input=@t ^- model [count=0]\0a'
53+ '++ update |= [m=@t state=model]\0a ^- [model (list (cmd @t))] [state ~]\0a'
54+ '++ view |= state=model ^- (element @t) [%node "ok"]\0a'
55+ '++ subs |= state=model\0a ^- (list (sub @t))\0a ~[[%watch request]]\0a'
56+ ==
57+::
58+++ program-watch-errors
59+ |= [public=@t private=@t sur=@t action=@t todos=@t update=@t item=@t api=@t]
60+ ^- (list tape)
61+ =/ prepared=(unit iprelude:jibb) (program-watch-prepared public private)
62+ ?~ prepared ~["synthetic program prelude did not prepare"]
63+ =/ todo=type -:(ride -:!>(..zuse) sur)
64+ =/ subject=type [%cell [%face %todo todo] -:!>(..zuse)]
65+ =/ ma=* (read-mark:jibb-import %todo-action -:(ride subject action))
66+ =/ mt=* (read-mark:jibb-import %todos -:(ride subject todos))
67+ =/ mu=* (read-mark:jibb-import %todo-update -:(ride subject update))
68+ =/ mi=* (read-mark:jibb-import %todo-item -:(ride subject item))
69+ =/ marks=imark-externals:jibb ~[[%todo-action ma] [%todos mt] [%todo-update mu] [%todo-item mi]]
70+ =/ item-input=* (read-named:jibb-import %todo %item todo)
71+ =/ externals=iexternals:jibb ~[[%todo %item item-input]]
72+ =/ api-at=path /ui/api/todo/jibb
73+ =/ api-result=jfile-detailed-result:jibb
74+ (program-watch-detailed api-at api externals marks ~ u.prepared)
75+ ?: ?=(%| -.api-result) ~["real todo API did not check"]
76+ =/ api-iface=ifile:jibb iface.p.api-result
77+ ?~ graph.api-iface ~["real todo API evidence is missing"]
78+ =/ direct-subs=@t '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[[%watch (todos.api |=%got)]]\0a'
79+ =/ island=@t (program-watch-source '' direct-subs)
80+ =/ at=path /tests/program-watch/island/jibb
81+ =/ modules=jbundle:jibb ~[[api-at api]]
82+ =/ detailed=jfile-detailed-result:jibb
83+ (program-watch-detailed at island externals marks modules u.prepared)
84+ ?: ?=(%| -.detailed) ~[(weld "direct request watch was rejected: " (trip message.p.detailed))]
85+ =/ checked=ifile:jibb iface.p.detailed
86+ ?~ graph.checked ~["program request graph evidence is missing"]
87+ =/ legacy=jfile-result:jibb
88+ (infer-jibb-file:jibb at island externals marks modules ~[at] values.u.prepared molds.u.prepared ~ `iface.u.prepared)
89+ ?: ?=(%| -.legacy) ~["legacy adapter rejected a direct request watch"]
90+ ?. =(values.checked values.iface.p.legacy) ~["structured and legacy interface values differ"]
91+ =/ subs=(unit ischeme:jibb) (ienv-lookup:jibb %subs values.checked)
92+ =/ main=(unit ischeme:jibb) (ienv-lookup:jibb %main values.checked)
93+ ?~ subs ~["subs interface is missing"]
94+ ?~ main ~["main interface is missing"]
95+ ?. &(?=(~ vars.u.subs) ?=(~ (itype-vars:jibb typ.u.subs))) ~["subs interface is not closed"]
96+ =/ subs-fields=(list itype:jibb) (record-fields-named:jibb %subs typ.u.main ~)
97+ ?. ?=([* ~] subs-fields) ~["closed program does not have one subs field"]
98+ =/ model=(unit ischeme:jibb) (find-jibb-mold:jibb %model checked)
99+ =/ msg=(unit ischeme:jibb) (find-jibb-mold:jibb %msg checked)
100+ =/ list-template=(unit ischeme:jibb) (find-jibb-mold:jibb %list iface.u.prepared)
101+ =/ sub=(unit ischeme:jibb) (find-jibb-mold:jibb %sub iface.u.prepared)
102+ ?~ model ~["model mold is missing"]
103+ ?~ msg ~["message mold is missing"]
104+ ?~ list-template ~["list mold is missing"]
105+ ?~ sub ~["sub mold is missing"]
106+ =/ message-sub=(unit itype:jibb) (template-apply:jibb u.sub ~[typ.u.msg])
107+ ?~ message-sub ~["message subscription type did not instantiate"]
108+ =/ subs-result=(unit itype:jibb) (template-apply:jibb u.list-template ~[u.message-sub])
109+ ?~ subs-result ~["subscription list type did not instantiate"]
110+ =/ expected-subs=itype:jibb [%fn typ.u.model u.subs-result]
111+ ?. =(typ.u.subs expected-subs) ~["subs interface has the wrong exact type"]
112+ ?. =((lent requests.u.graph.checked) (lent requests.u.graph.api-iface)) ~["merged API evidence count differs"]
113+ ?. (levy requests.u.graph.checked |=(r=irequest-evidence:jibb (lien requests.u.graph.api-iface |=(a=irequest-evidence:jibb =(r a))))) ~["merged API evidence differs"]
114+ =/ matching=(list irequest-evidence:jibb)
115+ (skim requests.u.graph.checked |=(r=irequest-evidence:jibb &(=(api-at.r api-at) =(%todos name.r))))
116+ ?. ?=([* ~] matching) ~["direct todos evidence is not unique"]
117+ =/ evidence=irequest-evidence:jibb i.matching
118+ ?. =(api-source.evidence api) ~["request evidence does not retain the exact API source"]
119+ ?. &(?=(~ scry.path.path.evidence) ?=(~ diffs.path.evidence) ?=(~ diffs.path.path.evidence))
120+ ~["plain todos evidence acquired scry or diffs"]
121+ ?: (lien segments.path.path.evidence |=(p=pseg:jibb !?=(%knot -.p))) ~["plain todos evidence acquired parameters"]
122+ =/ consumer-at=path /tests/program-watch/consumer/jibb
123+ =/ consumer=@t '/= island /tests/program-watch/island\0a++ imported subs.island\0a'
124+ =/ imported=jfile-detailed-result:jibb
125+ (program-watch-detailed consumer-at consumer externals marks [[at island] modules] u.prepared)
126+ ?: ?=(%| -.imported) ~["downstream program import was rejected"]
127+ =/ imported-subs=(unit ischeme:jibb) (ienv-lookup:jibb %imported values.iface.p.imported)
128+ ?~ imported-subs ~["downstream imported subs is missing"]
129+ =/ expected-import=itype:jibb (itype-in-import:jibb typ.u.subs checked %island `iface.u.prepared)
130+ ?. &(?=(~ vars.u.imported-subs) =(typ.u.imported-subs expected-import)) ~["downstream imported subs type differs"]
131+ =/ parsed (parse:jibb at island)
132+ ?: ?=(%| -.parsed) ~["program source no longer parses"]
133+ =/ main-def=(unit def:jibb) (program-main-def:jibb defs.p.parsed)
134+ ?~ main-def ~["program main definition is missing"]
135+ =/ parts (program-main-parts:jibb u.main-def)
136+ ?~ parts ~["program main parts are missing"]
137+ =/ resolved=ijimports:jibb ~[[%api api-iface]]
138+ =/ others=(list irequest-evidence:jibb)
139+ (skim requests.u.graph.checked |=(r=irequest-evidence:jibb !&(=(api-at.r api-at) =(%todos name.r))))
140+ =/ missing=irequest-graph:jibb u.graph.checked(requests others)
141+ =/ mismatch=irequest-graph:jibb u.graph.checked(requests [evidence(api-source 'mismatched') others])
142+ =/ scry=irequest-graph:jibb u.graph.checked(requests [evidence(scry.path.path `~[[%knot ~.peek]]) others])
143+ =/ ambiguous=irequest-graph:jibb u.graph.checked(requests [evidence requests.u.graph.checked])
144+ =/ evidence-cases=(list [label=tape graph=irequest-graph:jibb])
145+ :~ ["missing evidence" missing]
146+ ["API-source mismatch" mismatch]
147+ ["scry declaration evidence" scry]
148+ ["ambiguous evidence" ambiguous]
149+ ==
150+ =/ evidence-failures=(list tape)
151+ %+ murn evidence-cases
152+ |= c=[label=tape graph=irequest-graph:jibb]
153+ ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked `iface.u.prepared resolved graph.c)
154+ `label.c
155+ ~
156+ ?^ evidence-failures ~[(weld "bad evidence passed watchability: " i.evidence-failures)]
157+ =/ ordinary-values=ienv:jibb
158+ (skim values.api-iface |=(entry=[name=term scheme=ischeme:jibb] !=(%todos name.entry)))
159+ =/ forged=ifile:jibb
160+ api-iface(values [[%todos [[%fn [%atom %t] [%atom %t]] ~]] ordinary-values])
161+ ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked `iface.u.prepared ~[[%api forged]] u.graph.checked)
162+ ~["same-named non-derived member passed watchability"]
163+ =/ detached=ifile:jibb api-iface(graph `u.graph.api-iface(requests ~))
164+ ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked `iface.u.prepared ~[[%api detached]] u.graph.checked)
165+ ~["evidence outside the selected interface passed watchability"]
166+ =/ incoherent=irequest-evidence:jibb evidence(name.path.path %other)
167+ =/ api-others=(list irequest-evidence:jibb)
168+ (skim requests.u.graph.api-iface |=(r=irequest-evidence:jibb !&(=(api-at.r api-at) =(%todos name.r))))
169+ =/ incoherent-api=ifile:jibb api-iface(graph `u.graph.api-iface(requests [incoherent api-others]))
170+ =/ incoherent-graph=irequest-graph:jibb u.graph.checked(requests [incoherent others])
171+ ?: (program-main-closed:jibb u.parts defs.p.parsed values.checked `iface.u.prepared ~[[%api incoherent-api]] incoherent-graph)
172+ ~["inconsistent request case names passed watchability"]
173+ =/ kind-error=@t (crip "module kind needs unsupported inference: {(spud at)}")
174+ =/ negatives=(list [label=tape src=@t])
175+ :~ :- "pure watch"
176+ (program-watch-source '' '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[[%watch (pure %other)]]\0a')
177+ :- "correctly typed hand-built agent"
178+ program-watch-agent-source
179+ :- "request helper"
180+ (program-watch-source '++ request ^- (ask msg) (todos.api |=%got)\0a' '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[[%watch request]]\0a')
181+ :- "request alias"
182+ (program-watch-source '++ request todos.api\0a' '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[[%watch (request |=%got)]]\0a')
183+ :- "parameterized todo-by-id"
184+ (program-watch-source '' '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[[%watch (todo-by-id.api 1 |=%one)]]\0a')
185+ :- "diff changes"
186+ (program-watch-source '++ fold |= [d=[%todo-update todo-update.api] s=todos.api] s\0a' '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[[%watch (changes.api |=%got fold)]]\0a')
187+ :- "multi-item subscriptions"
188+ (program-watch-source '++ first ^- (sub msg) [%watch (todos.api |=%got)]\0a++ second ^- (sub msg) [%watch (pure %other)]\0a' '++ subs |= state=model\0a ^- (list (sub msg))\0a ~[first second]\0a')
189+ ==
190+ %+ weld (turn evidence-failures |=(reason=tape reason))
191+ %+ murn negatives
192+ |= c=[label=tape src=@t]
193+ =/ bad=jfile-detailed-result:jibb
194+ (program-watch-detailed at src.c externals marks modules u.prepared)
195+ ?: ?=(%& -.bad) `[(weld label.c ": accepted")]
196+ ?. =(message.p.bad kind-error) `[(weld label.c ": did not reach watchability")]
197+ ~
198+::
199+++ test-program-watch
200+ ^- tang
201+ ?~ sur ~[leaf+"program-watch fixture sur is missing"]
202+ ?~ action ~[leaf+"program-watch fixture action is missing"]
203+ ?~ todos ~[leaf+"program-watch fixture todos is missing"]
204+ ?~ update ~[leaf+"program-watch fixture update is missing"]
205+ ?~ item ~[leaf+"program-watch fixture item is missing"]
206+ ?~ api ~[leaf+"program-watch fixture api is missing"]
207+ =/ failures=(list tape)
208+ (program-watch-errors prelude internal (text sur) (text action) (text todos) (text update) (text item) (text api))
209+ (turn failures |=(reason=tape leaf+reason))
210+--
tests/type-program-watch/about.txtnew file+1
@@ -0,0 +1 @@
1+tests: A synthetic closed program uses the real todo API and Hoon readers with synthetic init, update and view definitions. A singleton direct todos.api watch must match exact merged source-backed request evidence; the fixture checks its closed subs type and downstream import. Pure and hand-built requests, helpers and aliases, scry, missing, mismatched or ambiguous evidence, typed paths, diffs and multiple subscriptions are rejected. It does not execute the todo UI or establish runtime watching.
tools/testdata/ship-selftest+4
@@ -326,6 +326,7 @@ def generator_checks(tmp):
326326 'tests/lib/jibb-direct-gate-source.hoon',
327327 'tests/lib/jibb-program-main.hoon',
328328 'tests/lib/jibb-program-init.hoon',
329+ 'tests/lib/jibb-program-watch.hoon',
329330 'tests/lib/jibb-todo-api.hoon',
330331 'tests/lib/jibb-todo-partial.hoon',
331332 'tests/lib/jibb-constructor-fit-guards.hoon',
@@ -405,6 +406,9 @@ def generator_checks(tmp):
405406 'initializer-error', 'initializer-earlier', 'initializer-model',
406407 'initializer-message', 'initializer-generic', 'initializer-missing',
407408 'initializer-tag', 'initializer-no-main', 'initializer-subs')} <= set(normal.files))
409+ check('program watch shared fixture is assembled',
410+ {'tests/lib/jibb-program-watch.hoon', 'tests/type-program-watch/about.txt'}
411+ <= set(normal.files))
408412 check('todo partial golden and reused sources are assembled',
409413 {'tests/type-todo-partial/expected.txt', 'tests/type-gate-free/todo.txt',
410414 'tests/type-api-paths/api.txt'} <= set(normal.files))
tools/type-program-watch-testnew file+48
@@ -0,0 +1,48 @@
1+#!/usr/bin/env python3
2+"""Run direct request-value watchability 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+fixture = root / 'tests/type-api-paths/api.txt'
14+actual = root / 'my-app/ui/api/todo.jibb'
15+if fixture.read_bytes() != actual.read_bytes():
16+ sys.exit('todo API fixture differs from my-app/ui/api/todo.jibb')
17+reader = (root / 'jibb-dev/lib/jibb-import.hoon').read_text()
18+tests = (root / 'tests/lib/jibb-program-watch.hoon').read_text()
19+tests = tests[tests.index('\n|%\n') + 1:]
20+names = ('sur', 'action', 'todos', 'update', 'item', 'api')
21+program = ('=/ jibb .\n=/ jibb-import\n' + reader + '\n' +
22+ ''.join('=/ ' + name + '=wain (to-wain:format ' + name + '-text)\n'
23+ for name in names) +
24+ '=/ suite\n' + tests +
25+ '\n=/ failures=(list tape) (program-watch-errors:suite prelude internal (text:suite sur) (text:suite action) (text:suite todos) (text:suite update) (text:suite item) (text:suite api))\n'
26+ '^- @t\n?~ failures \'program request-value watchability passed\'\n'
27+ '(of-wain:format (turn failures crip))\n')
28+fixtures = {'sur': 'tests/type-api-paths/todo-sur.txt',
29+ 'action': 'tests/type-api-paths/todo-action.txt',
30+ 'todos': 'tests/type-api-paths/todos.txt',
31+ 'update': 'tests/type-api-paths/todo-update.txt',
32+ 'item': 'tests/type-api-paths/todo-item.txt',
33+ 'api': 'tests/type-api-paths/api.txt'}
34+with tempfile.TemporaryDirectory(prefix='jibb-program-watch-') as tmp:
35+ path = Path(tmp) / 'program-watch.hoon'
36+ path.write_text(program)
37+ command = [str(root / 'tools/hoon'), '--lib', args.lib, '--raw', '-f', str(path),
38+ '--cord', 'prelude=' + str(root / 'jibb-dev/lib/jibb/prelude.jibb'),
39+ '--cord', 'internal=' + str(root / 'jibb-dev/lib/jibb/internal.jibb')]
40+ for name, filename in fixtures.items():
41+ command += ['--cord', name + '-text=' + str(root / filename)]
42+ result = subprocess.run(command, stdout=subprocess.PIPE)
43+if result.returncode:
44+ sys.exit(result.returncode)
45+if result.stdout != b'program request-value watchability passed\n':
46+ sys.stderr.buffer.write(result.stdout)
47+ sys.exit(1)
48+print('direct request-value watchability and rejection guards passed')