on master help sign in
Recover direct program update context

Derive an unannotated update's result from its inferred two-slot sample and canonical cmd/list templates. Check the candidate and whole program invariantly with fresh IDs and stable replay, then infer the body with that result context and run ordinary finalization and kind checks. Cover union and nested boolean branches, exact exported and imported types, malformed samples, and missing canonical evidence under eval and on the ship. The unchanged todo still needs subscription and row context.

commita163965396cd4229126852bb8d04367ee47b632c authoriko <mail@iko.soy> dateSun 1 Nov 2026, 09:15 (12 hours ago) parent2e4d582
18 files changed+458−3
unifiedsplit
README.md+1−1 docs/compiler.md+2 docs/development.md+2 docs/status.md+6−2 jibb-dev/lib/jibb.hoon+142 tests/lib/jibb-program-update.hoon+139 tests/type-program-update/consumer.txt+2 tests/type-program-update/malformed-sample.txt+9 tests/type-program-update/missing-list.txt+15 tests/type-program-update/non-main.txt+14 tests/type-program-update/source.txt+15 tests/type-program-update/three-slot-sample.txt+9 tests/type-program-update/unrelated-tag.txt+16 tests/type-program-update/wrong-message.txt+10 tests/type-program-update/wrong-model.txt+12 tests/type-program-update/wrong-result.txt+12 tools/testdata/ship-selftest+6 tools/type-program-update-test+46
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. `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.
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-update-test` checks derived result context for an unannotated two-slot update, including a union/boolean branch, downstream types and fail-closed controls under eval with a shared fake-ship arm. `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+2
@@ -132,6 +132,8 @@ A full ordinary module may export a narrow checked program `main` only as a dire
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
135+A sibling retry handles only a missing direct `update` and `main` with the other three components resolved. It infers the update sample ordinarily, requires exactly two right-nested positions, and derives message and model from their types rather than binder names. Canonical `cmd` and `list` templates produce the expected `[model (list (cmd message))]` result. The complete candidate gate is invariantly checked against the instantiated canonical update slot, and the whole program call must close and replay stably above a shared fresh-ID high water. Body inference uses the ordinary post-sample state with that high water and the derived product context, then ordinary result finalization and `main` inference run. Missing canonical evidence, malformed samples, inconsistent types, unrelated pending tags, aliases and non-main modules decline the transaction.
136+
135137Each 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.
136138
137139`+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
@@ -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-update-test` | Checks transactional direct-program update result recovery, union/boolean context, exact exported/imported types and fail-closed boundaries under eval and on the ship |
9697| `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 |
9798| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |
9899| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |
@@ -145,6 +146,7 @@ tools/type-todo-api-test # real todo API partial inference and reader
145146tools/type-direct-gate-test # direct gate source and provenance guards pass
146147tools/type-program-main-test # closed program-main interface and rejection guards pass
147148tools/type-program-init-test # transactional direct-program initializer context guards pass
149+tools/type-program-update-test # transactional direct-program update context guards pass
148150tools/type-generic-recursion-test # source-backed recursive identities and provenance
149151tools/type-generic-construction-test # source-backed recursive construction and bounds
150152tools/type-generic-pattern-test # source-backed recursive patterns and bounds
docs/status.md+6−2
@@ -47,6 +47,8 @@ The partial checker can also match a directly named, checked root gate against a
4747
4848A 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.
4949
50+A sibling transactional path recovers an unannotated two-slot direct update only when `update` and `main` are missing and the other components are resolved. It derives message/model from the inferred sample types, builds the result with canonical `cmd`/`list` templates, invariantly checks the candidate and stable whole-program call above shared fresh IDs, and finalizes through ordinary update/main inference. A synthetic union branch with a nested boolean branch and exact exported/downstream types pass; wrong constructors, inconsistent types, malformed samples, non-main modules, unrelated tags and missing canonical evidence fail closed. The unchanged full todo still fails with `module definitions need unsupported inference: /ui/todo-list/jibb`; its unchanged partial report's next blockers remain `subs` call context and `row-of` tag context, so it is not checked.
51+
5052The 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.
5153
5254For 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.
@@ -98,7 +100,7 @@ What the plan asks for, and where it is:
98100Besides the plan's list:
99101
100102- 660 golden cases: 440 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.
101−- The 660-case corpus passed under `urbit eval` in 103.0 s while other checks were running. The fake ship passed all 710 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 101.4 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.
103+- The 660-case corpus passed under `urbit eval` in 101.7 s while other checks were running. The fake ship passed all 711 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 98.7 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.
102104- `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.
103105- 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.
104106- 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).
@@ -216,7 +218,8 @@ Besides the plan's list:
216218| b4703e7 | 2026-11-01 | Check narrow closed subscription-free program mains |
217219| 26bf7a7 | 2026-11-01 | Recover narrow direct-program initializer contexts |
218220| 642d2c0 | 2026-11-01 | Prove direct request-value watchability for program subscriptions |
219−| This change | 2026-11-01 | Add the source-backed UI, program and page prelude slice |
221+| 2e4d582 | 2026-11-01 | Add the source-backed UI, program and page prelude slice |
222+| This change | 2026-11-01 | Recover direct-program update result contexts |
220223
221224## Checking it
222225
@@ -256,6 +259,7 @@ tools/type-proj-guards-test # projection evidence and scope guards
256259tools/type-module-scope-test # module and prelude scope fixture
257260tools/type-program-main-test # closed program-main interface and rejection guards
258261tools/type-program-init-test # transactional direct-program initializer context guards
262+tools/type-program-update-test # transactional direct-program update context guards
259263tools/hoon check-spans-test # prints <<>> when the span checker works
260264tools/testdata/selftest # the tools themselves
261265tools/doc-blocks docs/spec # the doc's examples are golden cases
jibb-dev/lib/jibb.hoon+142
@@ -12558,6 +12558,145 @@
1255812558 ?~ items.body |
1255912559 (program-empty-null val:(rear items.body))
1256012560::
12561+:: Recover only the update of an already recognized direct program main.
12562+:: Its written sample determines the message/model relationship; the canonical
12563+:: cmd and list molds determine the result context. Every candidate is checked
12564+:: against the complete program call before an ordinary update/main retry.
12565+++ program-update-context
12566+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12567+ ^- (unit iresolved)
12568+ =/ env=ienv env.resolution
12569+ ?^ (ienv-lookup %main env) ~
12570+ ?^ (ienv-lookup update.parts env) ~
12571+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
12572+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
12573+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
12574+ ?~ init ~
12575+ ?~ view ~
12576+ ?~ subs ~
12577+ =/ updates=(list def)
12578+ (skim ds |=(d=def &(?=(%value -.d) =(update.parts name.d))))
12579+ ?. ?=([* ~] updates) ~
12580+ =/ update-def=def i.updates
12581+ ?> ?=(%value -.update-def)
12582+ =/ written-update=(unit sample) (direct-gate-sample update-def)
12583+ ?~ written-update ~
12584+ ?. ?=(%cell -.u.written-update) ~
12585+ ?. ?=([* * ~] items.u.written-update) ~
12586+ =/ args=(unit (list expr)) (program-main-args main)
12587+ ?~ args ~
12588+ ?~ prelude.initial ~
12589+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12590+ ?~ program ~
12591+ =/ command=(unit ischeme) (find-jibb-mold %cmd u.prelude.initial)
12592+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12593+ ?~ command ~
12594+ ?~ list-template ~
12595+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12596+ ?~ heads ~
12597+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12598+ ?~ written ~
12599+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12600+ ?~ written-sample ~
12601+ ?. ?=(%cell -.u.written-sample) ~
12602+ ?. ?=([* * * * ~] items.u.written-sample) ~
12603+ =/ checked=(map term def)
12604+ (~(put by (direct-checked-gates ds env)) update.parts update-def)
12605+ =/ templates=ienv
12606+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12607+ =/ scanned=(unit dgscan)
12608+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12609+ ?~ scanned ~
12610+ =. next.initial (dg-next-id ids.u.scanned 0)
12611+ =/ update-state=istate (reserve-def-caps val.update-def initial)
12612+ =/ sam=isample-result (infer-sample u.written-update env update-state)
12613+ ?: ?=(%| -.sam) ~
12614+ =/ actual-sample=itype (itype-normalize typ.p.sam sub.state.p.sam)
12615+ ?. ?=(%cell -.actual-sample) ~
12616+ =/ message=(unit itype)
12617+ (direct-slot-body hed.actual-sample (direct-sample-name i.items.u.written-update))
12618+ =/ model=(unit itype)
12619+ (direct-slot-body tal.actual-sample (direct-sample-name i.t.items.u.written-update))
12620+ ?~ message ~
12621+ ?~ model ~
12622+ =/ cmd=(unit itype) (template-apply u.command ~[u.message])
12623+ ?~ cmd ~
12624+ =/ cmds=(unit itype) (template-apply u.list-template ~[u.cmd])
12625+ ?~ cmds ~
12626+ =/ product=itype [%cell u.model u.cmds]
12627+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program state.p.sam)
12628+ ?. ?=(%fn -.typ.instance) ~
12629+ ?. ?=(%cell -.sample.typ.instance) ~
12630+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12631+ =/ expected-update=(unit itype)
12632+ (direct-slot-body hed.tal.sample.typ.instance (direct-sample-name i.t.items.u.written-sample))
12633+ ?~ expected-update ~
12634+ ?. ?=(%fn -.u.expected-update) ~
12635+ :: Sample binders are not value faces. Strip only those two slot faces
12636+ :: for the invariant canonical-gate proof; the source-faced gate is still
12637+ :: used by the complete positional call and final ordinary result cast.
12638+ =/ canonical-candidate=itype [%fn [%cell u.message u.model] product]
12639+ =/ gate-fit=ifit
12640+ (direct-invariant canonical-candidate u.expected-update sub.state.instance next.state.instance)
12641+ ?. ?=(%ok -.gate-fit) ~
12642+ =/ st=istate state.instance(sub sub.gate-fit, next next.gate-fit)
12643+ =/ ini=[typ=itype state=istate] (instantiate-scheme u.init st)
12644+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.ini)
12645+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
12646+ =. st state.sb(gate-defs checked, head-evidence heads)
12647+ =/ expected=itype [%fn typ.p.sam product]
12648+ =/ actual=itype [%cell typ.ini [%cell expected [%cell typ.vw typ.sb]]]
12649+ =/ fit=ifit
12650+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
12651+ ?. ?=(%ok -.fit) ~
12652+ =/ actual-final=itype (itype-normalize actual sub.fit)
12653+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
12654+ ?^ (itype-vars actual-final) ~
12655+ ?^ (itype-vars expected-final) ~
12656+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
12657+ =/ replay=ifit
12658+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
12659+ ?. ?=(%ok -.replay) ~
12660+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
12661+ =/ closed=itype (itype-normalize expected sub.fit)
12662+ ?. ?=(%fn -.closed) ~
12663+ :: The closed product no longer needs the canonical call substitutions.
12664+ :: Start the body at its ordinary sample state so existing branch retries
12665+ :: keep their substitution guards, but retain the shared fresh-ID high water.
12666+ =. st state.p.sam(next next.fit)
12667+ =/ body=expr
12668+ ?- -.val.update-def
12669+ %gate body.val.update-def
12670+ %gate-wide body.val.update-def
12671+ * !!
12672+ ==
12673+ =/ inferred=iresult
12674+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12675+ ?: ?=(%| -.inferred) ~
12676+ =/ product-fit=ifit
12677+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12678+ ?. ?=(%ok -.product-fit) ~
12679+ =/ merged-product=itype
12680+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12681+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12682+ =/ cast=ifit
12683+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12684+ ?. ?=(%ok -.cast) ~
12685+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12686+ =/ adjusted=iresult
12687+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12688+ =/ added=(unit iadded-definition)
12689+ (add-supported-result update-def adjusted update-state env checked artifacts.resolution)
12690+ ?~ added ~
12691+ =/ recovered=(unit ischeme) (ienv-lookup update.parts env.u.added)
12692+ ?~ recovered ~
12693+ ?. ?=(~ vars.u.recovered) ~
12694+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12695+ =/ completed=[env=ienv artifacts=(list iwidth-definition)]
12696+ (add-supported-defs-core ~[main] ds checked.u.added heads env.u.added molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.u.added grec-index.initial)
12697+ ?~ (ienv-lookup %main env.completed) ~
12698+ `[env.completed grouped.resolution artifacts.completed]
12699+::
1256112700:: Recover only the initializer of an already recognized direct program main.
1256212701:: The derived call is evidence for an ordinary init/main retry, never an
1256312702:: interface to publish on its own. Any failure returns the original resolution.
@@ -12853,6 +12992,9 @@
1285312992 =/ recovered=(unit iresolved)
1285412993 ?~ main ~
1285512994 ?~ main-parts ~
12995+ =/ updated=(unit iresolved)
12996+ (program-update-context u.main u.main-parts defs.mod resolution state)
12997+ ?^ updated updated
1285612998 (program-init-context u.main u.main-parts defs.mod resolution state)
1285712999 =. env ?~(recovered env env.u.recovered)
1285813000 =. artifacts.resolution
tests/lib/jibb-program-update.hoonnew file+139
@@ -0,0 +1,139 @@
1+:: Transactional direct-program update result context, without UI execution.
2+/+ jibb
3+/* prelude %jibb /lib/jibb/prelude/jibb
4+/* internal %jibb /lib/jibb/internal/jibb
5+/* source %txt /tests/type-program-update/source/txt
6+/* consumer %txt /tests/type-program-update/consumer/txt
7+/* wrong-result %txt /tests/type-program-update/wrong-result/txt
8+/* wrong-model %txt /tests/type-program-update/wrong-model/txt
9+/* wrong-message %txt /tests/type-program-update/wrong-message/txt
10+/* malformed-sample %txt /tests/type-program-update/malformed-sample/txt
11+/* three-slot-sample %txt /tests/type-program-update/three-slot-sample/txt
12+/* non-main %txt /tests/type-program-update/non-main/txt
13+/* unrelated-tag %txt /tests/type-program-update/unrelated-tag/txt
14+/* missing-list %txt /tests/type-program-update/missing-list/txt
15+|%
16+++ text
17+ |= lines=wain
18+ ^- @t
19+ (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))
20+::
21+++ program-update-prepared
22+ |= [public=@t private=@t]
23+ ^- (unit iprelude:jibb)
24+ (prepare-prelude-with-internal:jibb public private)
25+::
26+++ program-update-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-update-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-update-positive
37+ |= [at=path src=@t downstream=@t prepared=iprelude:jibb]
38+ ^- (list tape)
39+ =/ detailed=jfile-detailed-result:jibb (program-update-detailed at src ~ prepared)
40+ ?: ?=(%| -.detailed) ~["contextual direct program update was rejected"]
41+ =/ checked=ifile:jibb iface.p.detailed
42+ =/ legacy=jfile-result:jibb (program-update-legacy at src ~ prepared)
43+ ?: ?=(%| -.legacy) ~["legacy adapter rejected contextual update"]
44+ ?. =(values.checked values.iface.p.legacy) ~["contextual structured and legacy values differ"]
45+ =/ update=(unit ischeme:jibb) (ienv-lookup:jibb %update values.checked)
46+ =/ main=(unit ischeme:jibb) (ienv-lookup:jibb %main values.checked)
47+ ?~ update ~["contextual update interface is missing"]
48+ ?~ main ~["contextual main interface is missing"]
49+ ?. ?=(~ vars.u.update) ~["contextual update interface is not closed"]
50+ =/ expected=tape "$-([event=message current=[count=@ud]] [count=@ud (list (cmd message))])"
51+ ?. =((show-itype:jibb typ.u.update ~) expected) ~["contextual update interface type differs"]
52+ ?. ?=(~ vars.u.main) ~["contextual main interface is not closed"]
53+ =/ fields=(list itype:jibb) (record-fields-named:jibb %update typ.u.main ~)
54+ ?. ?=([* ~] fields) ~["contextual main update field is missing"]
55+ =/ main-expected=tape "$-([message count=@ud] [count=@ud (list (cmd message))])"
56+ ?. =((show-itype:jibb i.fields ~) main-expected) ~["contextual main update field differs"]
57+ ?~ source.checked ~["contextual program source evidence is missing"]
58+ ?. =(u.source.checked src) ~["contextual program source evidence differs"]
59+ ?~ graph.checked ~["contextual program request graph is missing"]
60+ =/ consumer-at=path /tests/program-update/consumer/jibb
61+ =/ imported=jfile-detailed-result:jibb
62+ (program-update-detailed consumer-at downstream ~[[at src]] prepared)
63+ ?: ?=(%| -.imported) ~[(weld "downstream contextual update import was rejected: " (trip message.p.imported))]
64+ =/ use=(unit ischeme:jibb) (ienv-lookup:jibb %imported values.iface.p.imported)
65+ ?~ use ~["downstream contextual update is missing"]
66+ =/ imported-expected=tape "$-([message.island-prog count=@ud] [count=@ud (list (cmd message.island-prog))])"
67+ ?. =((show-itype:jibb typ.u.use ~) imported-expected) ~["downstream contextual update type differs"]
68+ ?. ?=(~ vars.u.use) ~["downstream contextual update is not closed"]
69+ ~
70+::
71+++ program-update-negative
72+ |= [label=@t at=path src=@t boundary=@t prepared=iprelude:jibb]
73+ ^- (list tape)
74+ =/ detailed=jfile-detailed-result:jibb (program-update-detailed at src ~ prepared)
75+ ?: ?=(%& -.detailed) ~[(weld (trip label) ": structured check accepted")]
76+ ?. ?=(~ overlap.p.detailed) ~[(weld (trip label) ": unexpected overlap evidence")]
77+ ?. =(message.p.detailed boundary) ~[(weld (trip label) ": rejected at the wrong boundary")]
78+ =/ legacy=jfile-result:jibb (program-update-legacy at src ~ prepared)
79+ ?: ?=(%& -.legacy) ~[(weld (trip label) ": legacy check accepted")]
80+ ?. =(p.legacy boundary) ~[(weld (trip label) ": legacy boundary differs")]
81+ ~
82+::
83+++ program-update-negative-cases
84+ |= [cases=(list [label=@t at=path src=@t boundary=@t prepared=iprelude:jibb])]
85+ ^- (list tape)
86+ ?~ cases ~
87+ %+ weld
88+ (program-update-negative label.i.cases at.i.cases src.i.cases boundary.i.cases prepared.i.cases)
89+ $(cases t.cases)
90+::
91+++ program-update-errors
92+ |= [public=@t private=@t island=@t downstream=@t negatives=(list @t)]
93+ ^- (list tape)
94+ =/ prepared=(unit iprelude:jibb) (program-update-prepared public private)
95+ ?~ prepared ~["synthetic program prelude did not prepare for contextual update"]
96+ ?. =(8 (lent negatives)) ~["contextual update negative fixture count differs"]
97+ =/ at=path /tests/program-update/island/jibb
98+ =/ definitions=@t (crip "module definitions need unsupported inference: {(spud at)}")
99+ =/ without-cmd=iprelude:jibb
100+ =/ kept=imold-types:jibb
101+ (skim molds.iface.u.prepared |=(m=[name=term template=ischeme:jibb] !=(%cmd name.m)))
102+ [iface.u.prepared(molds kept) values.u.prepared molds.u.prepared]
103+ =/ without-list=iprelude:jibb
104+ =/ kept=imold-types:jibb
105+ (skim molds.iface.u.prepared |=(m=[name=term template=ischeme:jibb] !=(%list name.m)))
106+ [iface.u.prepared(molds kept) values.u.prepared molds.u.prepared]
107+ =/ cases=(list [label=@t at=path src=@t boundary=@t prepared=iprelude:jibb])
108+ :~ ['wrong result constructor' at (snag 0 negatives) definitions u.prepared]
109+ ['inconsistent model' at (snag 1 negatives) definitions u.prepared]
110+ ['inconsistent message' at (snag 2 negatives) definitions u.prepared]
111+ ['malformed sample' at (snag 3 negatives) definitions u.prepared]
112+ ['non-two-slot sample' at (snag 4 negatives) definitions u.prepared]
113+ ['non-main same source' at (snag 5 negatives) definitions u.prepared]
114+ ['unrelated pending tag' at (snag 6 negatives) definitions u.prepared]
115+ ['missing canonical cmd' at island definitions without-cmd]
116+ ['missing canonical list' at (snag 7 negatives) definitions without-list]
117+ :- 'API path'
118+ [/ui/api/program-update/jibb island 'module kind needs unsupported inference: /ui/api/program-update/jibb' u.prepared]
119+ :- 'store path'
120+ [/ui/stores/program-update/jibb island 'module kind needs unsupported inference: /ui/stores/program-update/jibb' u.prepared]
121+ ==
122+ %+ weld
123+ (program-update-positive at island downstream u.prepared)
124+ (program-update-negative-cases cases)
125+::
126+++ test-program-update
127+ ^- tang
128+ =/ negatives=(list @t)
129+ :~ (text wrong-result)
130+ (text wrong-model)
131+ (text wrong-message)
132+ (text malformed-sample)
133+ (text three-slot-sample)
134+ (text non-main)
135+ (text unrelated-tag)
136+ (text missing-list)
137+ ==
138+ (turn (program-update-errors prelude internal (text source) (text consumer) negatives) |=(reason=tape leaf+reason))
139+--
tests/type-program-update/consumer.txtnew file+2
@@ -0,0 +1,2 @@
1+/= island-prog /tests/program-update/island
2+++ imported update.main.island-prog
tests/type-program-update/malformed-sample.txtnew file+9
@@ -0,0 +1,9 @@
1++$ model [count=@ud]
2++$ message %noop
3+++ main (program init update view subs)
4+++ init |= input=@t ^- model [count=0]
5+++ update |= event=message
6+ ?- event
7+ %noop [[count=0] ~]
8+++ view |= state=model ^- (element message) (text "view")
9+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-update/missing-list.txtnew file+15
@@ -0,0 +1,15 @@
1++$ model [count=@ud]
2++$ message
3+ %noop
4+ [%set value=@ud]
5+++ main (program init update view subs)
6+++ init |= input=@t ^- model [count=0]
7+++ update |= [event=message current=model]
8+ ?- event
9+ %noop [current ~]
10+ [%set value]
11+ ?- (gth value 10)
12+ %.y [current(count=value) ~]
13+ %.n [current ~]
14+++ view |= state=model ^- (element message) (text "view")
15+++ subs !!
tests/type-program-update/non-main.txtnew file+14
@@ -0,0 +1,14 @@
1++$ model [count=@ud]
2++$ message
3+ %noop
4+ [%set value=@ud]
5+++ init |= input=@t ^- model [count=0]
6+++ update |= [event=message current=model]
7+ ?- event
8+ %noop [current ~]
9+ [%set value]
10+ ?- (gth value 10)
11+ %.y [current(count=value) ~]
12+ %.n [current ~]
13+++ view |= state=model ^- (element message) (text "view")
14+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-update/source.txtnew file+15
@@ -0,0 +1,15 @@
1++$ model [count=@ud]
2++$ message
3+ %noop
4+ [%set value=@ud]
5+++ main (program init update view subs)
6+++ init |= input=@t ^- model [count=0]
7+++ update |= [event=message current=model]
8+ ?- event
9+ %noop [current ~]
10+ [%set value]
11+ ?- (gth value 10)
12+ %.y [current(count=value) ~]
13+ %.n [current ~]
14+++ view |= state=model ^- (element message) (text "view")
15+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-update/three-slot-sample.txtnew file+9
@@ -0,0 +1,9 @@
1++$ model [count=@ud]
2++$ message %noop
3+++ main (program init update view subs)
4+++ init |= input=@t ^- model [count=0]
5+++ update |= [event=message current=model extra=@ud]
6+ ?- event
7+ %noop [current ~]
8+++ view |= state=model ^- (element message) (text "view")
9+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-update/unrelated-tag.txtnew file+16
@@ -0,0 +1,16 @@
1++$ model [count=@ud]
2++$ message
3+ %noop
4+ [%set value=@ud]
5+++ main (program init update view subs)
6+++ init |= input=@t ^- model [count=0]
7+++ update |= [event=message current=model]
8+ ?- event
9+ %noop [current ~]
10+ [%set value]
11+ ?- (gth value 10)
12+ %.y [current(count=value) ~]
13+ %.n [current ~]
14+++ view |= state=model ^- (element message) (text "view")
15+++ subs |= state=model ^- (list (sub message)) ~
16+++ dangling |=%unrelated
tests/type-program-update/wrong-message.txtnew file+10
@@ -0,0 +1,10 @@
1++$ model [count=@ud]
2++$ message %noop
3++$ other-message %other
4+++ main (program init update view subs)
5+++ init |= input=@t ^- model [count=0]
6+++ update |= [event=other-message current=model]
7+ ?- event
8+ %other [current ~]
9+++ view |= state=model ^- (element message) (text "view")
10+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-update/wrong-model.txtnew file+12
@@ -0,0 +1,12 @@
1++$ model [count=@ud]
2++$ message
3+ %noop
4+ [%set value=@ud]
5+++ main (program init update view subs)
6+++ init |= input=@t ^- model [count=0]
7+++ update |= [event=message current=model]
8+ ?- event
9+ %noop [current ~]
10+ [%set value] [[count="wrong"] ~]
11+++ view |= state=model ^- (element message) (text "view")
12+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-update/wrong-result.txtnew file+12
@@ -0,0 +1,12 @@
1++$ model [count=@ud]
2++$ message
3+ %noop
4+ [%set value=@ud]
5+++ main (program init update view subs)
6+++ init |= input=@t ^- model [count=0]
7+++ update |= [event=message current=model]
8+ ?- event
9+ %noop [current ~]
10+ [%set value] [current `%noop]
11+++ view |= state=model ^- (element message) (text "view")
12+++ subs |= state=model ^- (list (sub message)) ~
tools/testdata/ship-selftest+6
@@ -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-update.hoon',
329330 'tests/lib/jibb-program-watch.hoon',
330331 'tests/lib/jibb-todo-api.hoon',
331332 'tests/lib/jibb-todo-partial.hoon',
@@ -406,6 +407,11 @@ def generator_checks(tmp):
406407 'initializer-error', 'initializer-earlier', 'initializer-model',
407408 'initializer-message', 'initializer-generic', 'initializer-missing',
408409 'initializer-tag', 'initializer-no-main', 'initializer-subs')} <= set(normal.files))
410+ check('program update sources and shared fixture are assembled',
411+ {f'tests/type-program-update/{name}.txt' for name in (
412+ 'source', 'consumer', 'wrong-result', 'wrong-model', 'wrong-message',
413+ 'malformed-sample', 'three-slot-sample', 'non-main', 'unrelated-tag', 'missing-list')}
414+ <= set(normal.files))
409415 check('program watch shared fixture is assembled',
410416 {'tests/lib/jibb-program-watch.hoon', 'tests/type-program-watch/about.txt'}
411417 <= set(normal.files))
tools/type-program-update-testnew file+46
@@ -0,0 +1,46 @@
1+#!/usr/bin/env python3
2+"""Run transactional direct-program update context 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', 'wrong-result', 'wrong-model', 'wrong-message',
19+ 'malformed-sample', 'three-slot-sample', 'non-main', 'unrelated-tag', 'missing-list')
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+ '=/ suite\n' + body('jibb-program-update.hoon') +
25+ '\n=/ negatives=(list @t)\n :~ (text:suite wrong-result)\n'
26+ ' (text:suite wrong-model)\n (text:suite wrong-message)\n'
27+ ' (text:suite malformed-sample)\n (text:suite three-slot-sample)\n'
28+ ' (text:suite non-main)\n (text:suite unrelated-tag)\n (text:suite missing-list)\n ==\n'
29+ '=/ failures=(list tape) (program-update-errors:suite prelude internal (text:suite source) (text:suite consumer) negatives)\n'
30+ '^- @t\n?~ failures \'program update checks passed\'\n'
31+ '(of-wain:format (turn failures crip))\n')
32+with tempfile.TemporaryDirectory(prefix='jibb-program-update-') as tmp:
33+ program = Path(tmp) / 'program-update.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-update' / (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 update checks passed\n':
44+ sys.stderr.buffer.write(result.stdout)
45+ sys.exit(1)
46+print('transactional direct-program update context guards passed')