git.iko.soy/jibb
on master help sign in
Recover every direct initializer by one path

A direct program's initializer had two recoveries: one ran only when the body was a tuple ending in ~, the other only for a ~ sample. This is review question 8: remove the narrow one. +program-init-context, its +program-init-tuple-null gate and the null-sample gate are gone, so +program-plain-init-context checks any body and any closed, tag-free sample of a direct gate. The removed retry did two things the remaining path lacked, and both are kept. +program-init-model takes the model from update's written two-item sample when it can be read, and otherwise from main's own program fit, moved over from the removed retry. Updates written |= input=[message model], |= =input, |= in=input or generic in the model, and generic view and subs samples, still recover their initializer. +program-init-ordinary infers a body that context inference cannot take, such as a branch over a nested call's union, as a whole gate, as the removed retry did. Six fixtures cover these; master accepts each, and each fails without its part of this change. The 'inconsistent message' negative now fails at main instead of at init's pending ~. Because recovery now takes any body, the todo regression for keyed views would have passed through recovery even if the keyed-view skip came back, so its initializer is now a gate under a ^- cast to its full type, which only ordinary inference accepts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U4FzmSdubYxmZGDp2VJRAQ

commit93d6b23e1ae0025e362340a45dac95d09c029936 authorClaude <noreply@anthropic.com> dateMon 2 Nov 2026, 23:13 (8 hours ago) parent839f6b0
14 files changed+218−166
compare with master
unifiedsplit
docs/compiler.md+2−2 docs/status.md+2−2 jibb-dev/lib/jibb.hoon+101−152 tests/lib/jibb-program-init.hoon+32−4 tests/type-program-main/about.txt+1−1 tests/type-program-main/initializer-alias.txt+11 tests/type-program-main/initializer-nested-branch.txt+24 tests/type-program-main/initializer-open-update.txt+10 tests/type-program-main/initializer-open-view.txt+11 tests/type-program-main/initializer-pun.txt+11 tests/type-todo-full/about.txt+1−1 tests/type-todo-full/cast-init.txt+2−2 tools/testdata/ship-selftest+2 tools/type-program-init-test+8−2
docs/compiler.md+2−2
@@ -144,9 +144,9 @@ A store `main` is recognized only as a direct, unqualified `(store init update)`
144144
145145The store interface adds a derived `$-([action $-((unit @t) M)] (cmd M))` poke helper and a generic `$-($-(state M) (ask M))` state request after validating the exact internal `raw-poke`, canonical `cmd`, standard `unit` and `ask` representations. Derived names must not collide with values, imports or other derived names. Once the store's `state` and `poke` molds are unique and nongeneric and `main`'s `store` is the prelude's builder, such a collision is a definite error, reported before other scope conflicts, showing the mold the name derives from and the clashing definition or import face. Store request certificates are distinct from API certificates and retain the exact store path, source, state and action identities across graph merges. `+derived-store-request-member` requires the selected interface's unique state member and action constructor to match freshly derived canonical schemes and the same certificate to occur in both interface and consumer graphs. Store state is watchable by definition only after those checks; page loads continue to accept API evidence alone. Multi-action declarations, lowering and execution are outside this slice.
146146
147−When 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.
147+When only that program's initializer and `main` are unresolved, one transactional retry checks the initializer, which must be a direct gate with a closed, tag-free written sample, against the program's closed model. Update's written two-item sample gives the model when it can be read. Otherwise main's own source-backed program fit gives it: update, view and subs are instantiated above the greatest variable ID in the module and prelude and fitted together against the prelude `program` sample, with the initializer an open variable. Only the initializer's data may stay open, a replay of the fit must not change the substitution, and the model must come out closed and tag-free. So an update written `|= =input`, `|= in=input` or generic in its model, and a view and subs with generic samples, still let the initializer check. The body is inferred with the model as context; a body that context inference cannot take, such as a branch over a nested call's union, is inferred ordinarily as a whole gate instead, and its sample must fit the written one. The 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. This one path replaced a separate retry for bodies ending in null and a gate that took only a null sample (review question 8), so any body and any closed sample of a direct gate check the same way. The fresh `main` inference is what checks that the four components agree: an initializer that fits update's model while view uses another message passes recovery, and `main` then rejects the program. Aliased mains or initializers, non-main libraries, simultaneously unresolved subscriptions and unrelated pending tags decline.
148148
149−Ordinary inference runs for every component before recovery, so a keyed view no longer causes an already-valid initializer to be skipped. Recovery is a fallback for unresolved components, not a replacement for definitions that check normally. The regression uses a call-bodied annotated initializer, which is outside the tuple-bodied initializer recovery shape.
149+Ordinary inference runs for every component before recovery, so a keyed view no longer causes an already-valid initializer to be skipped. Recovery is a fallback for unresolved components, not a replacement for definitions that check normally. The regression's initializer is a gate under a `^-` cast to its full type. Ordinary inference checks it, but recovery, which takes only a direct gate, cannot, so the fixture fails if a keyed view ever skips ordinary inference again.
150150
151151A component-local recovery sequence handles a recognized direct program whose context-dependent definitions cannot resolve ordinarily. Update first derives its result from its inferred two-slot sample and canonical `cmd`/`list` templates. Subscription recovery then checks the same message/model relation and the canonical fourth slot. A narrow keyed-view proof finds exactly one direct `each (turn xs mapper)` site, derives the mapper from the actual `each` and `turn` schemes, and recovers the view before the existing initializer and ordinary `main` retries. Every recovered scheme must be closed and freshly allocated above the current environment and prelude IDs. That bound comes from one unbudgeted pass over the environment and prelude schemes, which treats named recursive types as leaves and declines only when a scheme still holds an unresolved literal tag. Non-gate views and aliases decline without crashing. Final publication still requires all module definitions, the program-mold and gate-free checks, and request-value watchability.
152152
docs/status.md+2−2
@@ -51,13 +51,13 @@ A separate source-backed analysis can prove one named mold gate-free, report a d
5151
5252The 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.
5353
54−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.
54+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 when update, view and subs are already resolved: it infers the initializer against the closed model that update's two-item sample, or else main's own program fit, establishes, then re-infers `main` under all ordinary finalization and kind checks. Any body and closed sample of a direct gate check this way; a body that context inference cannot take is inferred ordinarily as a whole gate. An update sample written as one faced mold, a pun, a named mold or generic in the model, and generic view and subs samples, also check. Non-main libraries, aliased mains or initializers, simultaneously unresolved subscriptions and unrelated pending tags remain rejected.
5555
5656Static and direct data-page `main` checking now completes the unchanged about page, blog index and todo index through the real Hoon readers. Static generic element mains specialize to closed canonical `(element !!)`; direct pages require a closed invariant `page` type and a direct plain derived-request load. Page loads reuse the strict source/member/evidence identity checks used by program watches, rejecting aliases, indirect/hand-built/pure/unknown requests, typed paths, diffs and store paths. The shared eval and ship fixture asserts exact main types and structural downstream imports. Rendering, runtime loading and request execution remain unimplemented.
5757
5858The prelude now has the approved `store` mold and action-checking builder. The runtime envelope is the transparent `raw-poke`; a store's local `+$ poke` remains its ordinary action mold throughout inference. Direct two-wing store mains require closed state and action molds, exact init/state and update relations, and no gate-free-state restriction. Stores export those molds plus derived generic `poke` command and state-request gates. The command helper checks the canonical `raw-poke`, `cmd` and `unit` shapes, takes an action and reply, and returns `(cmd M)` directly. Separate source-bound store certificates prove only the actual imported state member watchable; API evidence checks and page-load rejection remain intact. The unchanged cart and basket pass detailed and legacy checking with exact mains, derived schemes and structural imports, including non-keyed view and null-sample initializer recovery. Multi-action declarations, lowering and runtime execution remain unsupported.
5959
60−Keyed programs no longer skip ordinary component inference: an annotated initializer that checks normally is accepted, with recovery reserved for definitions that still need it. The todo fixture checks a call-bodied annotated initializer outside the tuple recovery shape through detailed and legacy inference, including on the ship.
60+Keyed programs no longer skip ordinary component inference: an annotated initializer that checks normally is accepted, with recovery reserved for definitions that still need it. The todo fixture's initializer is a gate cast to its full type, which only ordinary inference accepts, so it fails if the skip returns; it checks through detailed and legacy inference, including on the ship.
6161
6262Imported Hoon `(unit T)` now converts to the validated canonical prelude `unit` when that template is supplied, instead of remaining an incompatible collection. Conversion recurses through imported unions and collections, and API path/diff/poke analysis uses the same prepared reader. The fixtures prove identity, `fall`, `need`, `(unit @t)` casts, union- and list-nested matching, canonical unit-typed API full/diff marks and a canonical direct-poke export while preserving the no-prelude compatibility report and wrong-collection rejection. Nested public re-export labels also remain `ask`, `qath` and `raw-poke` instead of leaking their private `.internal` suffixes into printed types.
6363
jibb-dev/lib/jibb.hoon+101−152
@@ -13338,21 +13338,6 @@
1333813338 %body ?~(defs.e $(e final.e) e)
1333913339 * e
1334013340 ==
13341−++ program-init-tuple-null
13342− |= d=def
13343− ^- ?
13344− ?. ?=(%value -.d) |
13345− ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
13346− =/ body=expr
13347− ?- -.val.d
13348− %gate body.val.d
13349− %gate-wide body.val.d
13350− * !!
13351− ==
13352− =. body (program-transparent body)
13353− ?. ?=(%tuple -.body) |
13354− ?~ items.body |
13355− (program-empty-null val:(rear items.body))
1335613341::
1335713342:: Recover only the update of an already recognized direct program main.
1335813343:: Its written sample determines the message/model relationship; the canonical
@@ -14169,21 +14154,89 @@
1416914154 ?. ?=(~ (itype-vars typ.u.recovered)) ~
1417014155 `[env.u.added grouped.resolution artifacts.u.added]
1417114156::
14172−++ program-init-null-sample
14173− |= d=def
14174− ^- ?
14175− =/ written=(unit sample) (direct-gate-sample d)
14176− ?~ written |
14177− ?. ?=(%bare -.u.written) |
14178− =/ sh=shape shape.u.written
14179− ?. ?=(%const -.sh) |
14180− =(%null form.lit.sh)
14181−::
14182−:: The tuple-ending-null initializer retry above intentionally keeps its own
14183−:: boundary. A direct null-sample initializer can instead receive the closed
14184−:: model already established by update, view and subscriptions.
14157+:: The model a direct program's initializer must produce. Update's written
14158+:: two-item sample gives it when it can be read. Otherwise main's own program
14159+:: fit does: update, view and subs are fitted together against the prelude
14160+:: program's sample, as main's call will fit them, with the initializer an
14161+:: open variable. Only the initializer's data may stay open, a replay of the
14162+:: fit must not move, and the model must come out closed and tag-free.
14163+++ program-init-model
14164+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv program=ischeme program-def=def initial=istate]
14165+ ^- (unit itype)
14166+ =/ relation=(unit [message=itype model=itype])
14167+ (program-update-relation update.parts ds env)
14168+ ?^ relation `model.u.relation
14169+ =/ args=(unit (list expr)) (program-main-args main)
14170+ ?~ args ~
14171+ =/ written=(unit sample) (direct-gate-sample program-def)
14172+ ?~ written ~
14173+ ?. ?=(%cell -.u.written) ~
14174+ ?~ items.u.written ~
14175+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
14176+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
14177+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
14178+ ?~ update ~
14179+ ?~ view ~
14180+ ?~ subs ~
14181+ =/ instance=[typ=itype state=istate] (instantiate-scheme program initial)
14182+ ?. ?=(%fn -.typ.instance) ~
14183+ ?. ?=(%cell -.sample.typ.instance) ~
14184+ =/ expected-init=(unit itype)
14185+ (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written))
14186+ ?~ expected-init ~
14187+ ?. ?=(%fn -.u.expected-init) ~
14188+ ?. ?=(%var -.sample.u.expected-init) ~
14189+ =/ data=@ud id.sample.u.expected-init
14190+ =/ init-var=itype [%var next.state.instance]
14191+ =/ up=[typ=itype state=istate]
14192+ (instantiate-scheme u.update state.instance(next +(next.state.instance)))
14193+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
14194+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
14195+ =/ st=istate state.sb
14196+ =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
14197+ =/ fit=ifit
14198+ (direct-positional-fit u.args items.u.written actual sample.typ.instance env st sub.st next.st)
14199+ ?. ?=(%ok -.fit) ~
14200+ =/ actual-final=itype (itype-normalize actual sub.fit)
14201+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
14202+ =/ open=(list @ud)
14203+ (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
14204+ ?. (levy open |=(n=@ud =(data n))) ~
14205+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
14206+ =/ replay=ifit
14207+ (direct-positional-fit u.args items.u.written actual sample.typ.instance env st sub.fit next.fit)
14208+ ?. ?=(%ok -.replay) ~
14209+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
14210+ =/ expected=itype (itype-normalize u.expected-init sub.fit)
14211+ ?. ?=(%fn -.expected) ~
14212+ ?^ (itype-vars product.expected) ~
14213+ `product.expected
14214+::
14215+:: The product of an initializer inferred ordinarily, as a whole gate with no
14216+:: expected type, for a body that context inference cannot take, such as a
14217+:: branch over a nested call's union. Its sample must fit the written one.
14218+++ program-init-ordinary
14219+ |= [init-def=def env=ienv sample=itype state=istate]
14220+ ^- iresult
14221+ ?> ?=(%value -.init-def)
14222+ =/ gate=iresult (infer-fragment val.init-def env state)
14223+ =? gate ?=(%| -.gate) (infer-recursive-gate init-def env state)
14224+ ?: ?=(%| -.gate) gate
14225+ ?. ?=(%fn -.typ.p.gate) [%| ["initializer is not a gate" ~]]
14226+ =/ fit=ifit
14227+ (itype-fit sample.typ.p.gate sample sub.state.p.gate next.state.p.gate)
14228+ ?. ?=(%ok -.fit) [%| ["initializer sample differs" ~]]
14229+ [%& product.typ.p.gate state.p.gate(sub sub.fit, next next.fit)]
14230+::
14231+:: Recover a direct program's initializer once update, view and
14232+:: subscriptions are resolved: its body is inferred against their closed
14233+:: model (+program-init-model), under its own closed written sample. This one
14234+:: path replaced a separate retry for bodies ending in null and a gate that
14235+:: took only a null sample, so any body and any closed sample check the same
14236+:: way (review question 8). The fresh ordinary main inference afterwards
14237+:: checks that all four components agree.
1418514238++ program-plain-init-context
14186− |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
14239+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
1418714240 ^- (unit iresolved)
1418814241 =/ env=ienv env.resolution
1418914242 ?^ (ienv-lookup %main env) ~
@@ -14191,15 +14244,11 @@
1419114244 ?~ (ienv-lookup update.parts env) ~
1419214245 ?~ (ienv-lookup view.parts env) ~
1419314246 ?~ (ienv-lookup subs.parts env) ~
14194− =/ relation=(unit [message=itype model=itype])
14195− (program-update-relation update.parts ds env)
14196− ?~ relation ~
1419714247 =/ inits=(list def)
1419814248 (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
1419914249 ?. ?=([* ~] inits) ~
1420014250 =/ init-def=def i.inits
1420114251 ?> ?=(%value -.init-def)
14202− ?. (program-init-null-sample init-def) ~
1420314252 =/ written=(unit sample) (direct-gate-sample init-def)
1420414253 ?~ written ~
1420514254 =/ body=expr
@@ -14209,10 +14258,12 @@
1420914258 * !!
1421014259 ==
1421114260 ?~ prelude.initial ~
14212− ?~ (ienv-lookup %program values.u.prelude.initial) ~
14261+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
14262+ ?~ program ~
1421314263 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
1421414264 ?~ heads ~
14215− ?~ (~(get by gates.u.heads) %program) ~
14265+ =/ program-def=(unit def) (~(get by gates.u.heads) %program)
14266+ ?~ program-def ~
1421614267 =/ checked=(map term def) (direct-checked-gates ds env)
1421714268 =/ templates=ienv
1421814269 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
@@ -14220,130 +14271,31 @@
1422014271 (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
1422114272 ?~ fresh ~
1422214273 =. next.initial u.fresh
14274+ =/ model=(unit itype)
14275+ %: program-init-model
14276+ main parts ds env u.program u.program-def
14277+ initial(gate-defs checked, head-evidence heads)
14278+ ==
14279+ ?~ model ~
1422314280 =/ init-state=istate (reserve-def-caps val.init-def initial)
1422414281 =/ sam=isample-result (infer-sample u.written env init-state)
1422514282 ?: ?=(%| -.sam) ~
1422614283 ?. ?=(~ (itype-vars typ.p.sam)) ~
1422714284 ?: (itype-has-tag typ.p.sam) ~
1422814285 =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)
14286+ =/ contextual=iresult
14287+ (infer-call-context-arg body u.model env.p.sam st (span-of body))
1422914288 =/ inferred=iresult
14230− (infer-call-context-arg body model.u.relation env.p.sam st (span-of body))
14289+ ?: ?=(%& -.contextual) contextual
14290+ (program-init-ordinary init-def env typ.p.sam init-state(gate-defs checked, head-evidence heads))
1423114291 ?: ?=(%| -.inferred) ~
1423214292 =/ product-fit=ifit
14233− (itype-fit typ.p.inferred model.u.relation sub.state.p.inferred next.state.p.inferred)
14293+ (itype-fit typ.p.inferred u.model sub.state.p.inferred next.state.p.inferred)
1423414294 ?. ?=(%ok -.product-fit) ~
1423514295 =/ merged-product=itype
14236− (itype-merge-faces typ.p.inferred model.u.relation sub.product-fit)
14296+ (itype-merge-faces typ.p.inferred u.model sub.product-fit)
1423714297 =/ actual-cast=itype [%fn typ.p.sam merged-product]
14238− =/ closed=itype [%fn typ.p.sam model.u.relation]
14239− =/ cast=ifit
14240− (itype-fit actual-cast closed sub.product-fit next.product-fit)
14241− ?. ?=(%ok -.cast) ~
14242− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
14243− =/ adjusted=iresult
14244− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
14245− =/ added=(unit iadded-definition)
14246− (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
14247− ?~ added ~
14248− =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
14249− ?~ recovered ~
14250− ?. ?=(~ vars.u.recovered) ~
14251− ?. ?=(~ (itype-vars typ.u.recovered)) ~
14252− `[env.u.added grouped.resolution artifacts.u.added]
14253−::
14254−:: Recover only the initializer of an already recognized direct program main.
14255−:: The derived call is evidence for an ordinary init/main retry, never an
14256−:: interface to publish on its own. Any failure returns the original resolution.
14257−++ program-init-context
14258− |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
14259− ^- (unit iresolved)
14260− =/ env=ienv env.resolution
14261− ?^ (ienv-lookup %main env) ~
14262− ?^ (ienv-lookup init.parts env) ~
14263− =/ update=(unit ischeme) (ienv-lookup update.parts env)
14264− =/ view=(unit ischeme) (ienv-lookup view.parts env)
14265− =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
14266− ?~ update ~
14267− ?~ view ~
14268− ?~ subs ~
14269− =/ inits=(list def)
14270− (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
14271− ?. ?=([* ~] inits) ~
14272− =/ init-def=def i.inits
14273− ?> ?=(%value -.init-def)
14274− ?. (program-init-tuple-null init-def) ~
14275− =/ args=(unit (list expr)) (program-main-args main)
14276− ?~ args ~
14277− ?~ prelude.initial ~
14278− =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
14279− ?~ program ~
14280− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
14281− ?~ heads ~
14282− =/ written=(unit def) (~(get by gates.u.heads) %program)
14283− ?~ written ~
14284− =/ written-sample=(unit sample) (direct-gate-sample u.written)
14285− ?~ written-sample ~
14286− ?. ?=(%cell -.u.written-sample) ~
14287− ?~ items.u.written-sample ~
14288− =/ checked=(map term def) (direct-checked-gates ds env)
14289− =/ templates=ienv
14290− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14291− =/ fresh=(unit @ud)
14292− (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
14293− ?~ fresh ~
14294− =. next.initial u.fresh
14295− =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)
14296− ?. ?=(%fn -.typ.instance) ~
14297− ?. ?=(%cell -.sample.typ.instance) ~
14298− =/ expected-init=(unit itype)
14299− (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written-sample))
14300− ?~ expected-init ~
14301− ?. ?=(%fn -.u.expected-init) ~
14302− ?. ?=(%var -.sample.u.expected-init) ~
14303− =/ data=@ud id.sample.u.expected-init
14304− =/ init-var=itype [%var next.state.instance]
14305− =/ st=istate state.instance(next +(next.state.instance))
14306− =/ up=[typ=itype state=istate] (instantiate-scheme u.update st)
14307− =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
14308− =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
14309− =. st state.sb(gate-defs checked, head-evidence heads)
14310− =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
14311− =/ fit=ifit
14312− (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
14313− ?. ?=(%ok -.fit) ~
14314− =/ actual-final=itype (itype-normalize actual sub.fit)
14315− =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
14316− =/ open=(list @ud)
14317− (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
14318− ?. (levy open |=(n=@ud =(data n))) ~
14319− ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
14320− =/ replay=ifit
14321− (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
14322− ?. ?=(%ok -.replay) ~
14323− ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
14324− =/ expected=itype (itype-normalize u.expected-init sub.fit)
14325− ?. ?=(%fn -.expected) ~
14326− =. st st(sub sub.fit, next next.fit)
14327− =/ init-state=istate (reserve-def-caps val.init-def st)
14328− =/ inferred=iresult (infer-fragment val.init-def env init-state)
14329− =? inferred ?=(%| -.inferred) (infer-recursive-gate init-def env init-state)
14330− ?: ?=(%| -.inferred) ~
14331− ?. ?=(%fn -.typ.p.inferred) ~
14332− ?^ (itype-vars sample.typ.p.inferred) ~
14333− =/ data-fit=ifit
14334− (itype-fit sample.typ.p.inferred sample.expected sub.state.p.inferred next.state.p.inferred)
14335− ?. ?=(%ok -.data-fit) ~
14336− =/ closed=itype (itype-normalize expected sub.data-fit)
14337− ?. ?=(%fn -.closed) ~
14338− :: Resolve the ordinary tuple cast first, then check the complete gate.
14339− :: General function fit remains unchanged; only this recovered candidate
14340− :: receives the derived result context before its whole-type cast fit.
14341− =/ product-fit=ifit
14342− (itype-fit product.typ.p.inferred product.closed sub.data-fit next.data-fit)
14343− ?. ?=(%ok -.product-fit) ~
14344− =/ product=itype
14345− (itype-merge-faces product.typ.p.inferred product.closed sub.product-fit)
14346− =/ actual-cast=itype [%fn sample.typ.p.inferred product]
14298+ =/ closed=itype [%fn typ.p.sam u.model]
1434714299 =/ cast=ifit
1434814300 (itype-fit actual-cast closed sub.product-fit next.product-fit)
1434914301 ?. ?=(%ok -.cast) ~
@@ -14847,11 +14799,8 @@
1484714799 ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))
1484814800 =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)
1484914801 =/ initialized=(unit iresolved)
14850− (program-init-context u.main u.main-parts ds with-view state)
14851− =/ with-initialized=iresolved ?~(initialized with-view u.initialized)
14852− =/ plain-init=(unit iresolved)
14853− ?^(initialized ~ (program-plain-init-context u.main-parts ds with-initialized state))
14854− =/ components=iresolved ?~(plain-init with-initialized u.plain-init)
14802+ (program-plain-init-context u.main u.main-parts ds with-view state)
14803+ =/ components=iresolved ?~(initialized with-view u.initialized)
1485514804 (program-main-context u.main ds components state)
1485614805 =. env env.recovered
1485714806 =. artifacts.resolution artifacts.recovered
tests/lib/jibb-program-init.hoon+32−4
@@ -5,6 +5,11 @@
55/* initializer %txt /tests/type-program-main/initializer/txt
66/* initializer-consumer %txt /tests/type-program-main/initializer-consumer/txt
77/* initializer-unfaced %txt /tests/type-program-main/initializer-unfaced/txt
8+/* initializer-pun %txt /tests/type-program-main/initializer-pun/txt
9+/* initializer-alias %txt /tests/type-program-main/initializer-alias/txt
10+/* initializer-open-update %txt /tests/type-program-main/initializer-open-update/txt
11+/* initializer-open-view %txt /tests/type-program-main/initializer-open-view/txt
12+/* initializer-nested-branch %txt /tests/type-program-main/initializer-nested-branch/txt
813/* initializer-error %txt /tests/type-program-main/initializer-error/txt
914/* initializer-earlier %txt /tests/type-program-main/initializer-earlier/txt
1015/* initializer-model %txt /tests/type-program-main/initializer-model/txt
@@ -94,8 +99,22 @@
9499 ^- @t
95100 (show-error:jibb src [at line col (weld "nothing fixes the union of " literal)])
96101::
102+:: Each alternate writes update, view or subs another way (one faced mold,
103+:: a pun, an alias, generic in the model, generic view and subs samples), or
104+:: gives init a body only ordinary inference takes (a branch over a nested
105+:: call's union), and its initializer must check like the island's.
106+++ program-init-alternates
107+ |= [alternates=(list [name=@ta src=@t]) prepared=iprelude:jibb]
108+ ^- (list tape)
109+ ?~ alternates ~
110+ %+ weld
111+ %+ turn
112+ (program-init-positive /tests/program-main/[name.i.alternates]/jibb src.i.alternates ~ prepared)
113+ |=(reason=tape (weld (weld (trip name.i.alternates) ": ") reason))
114+ $(alternates t.alternates)
115+::
97116++ program-init-errors
98− |= [public=@t private=@t island=@t downstream=@t unfaced=@t negatives=(list @t)]
117+ |= [public=@t private=@t island=@t downstream=@t alternates=(list [name=@ta src=@t]) negatives=(list @t)]
99118 ^- (list tape)
100119 =/ prepared=(unit iprelude:jibb) (program-init-prepared public private)
101120 ?~ prepared ~["synthetic program prelude did not prepare for contextual init"]
@@ -103,14 +122,15 @@
103122 =/ positives=(list tape)
104123 %+ weld
105124 (program-init-positive at island `downstream u.prepared)
106− (program-init-positive /tests/program-main/initializer-unfaced/jibb unfaced ~ u.prepared)
125+ (program-init-alternates alternates u.prepared)
107126 ?. =(9 (lent negatives)) ~["contextual negative fixture count differs"]
108127 =/ definitions=@t (crip "module definitions need unsupported inference: {(spud at)}: ++ main")
109128 =/ cases=(list [label=@t at=path src=@t boundary=@t])
110129 :~ ['incompatible error field' at (snag 0 negatives) (program-init-pending at (snag 0 negatives) 6 32 "~")]
111130 ['earlier tuple mismatch' at (snag 1 negatives) (program-init-pending at (snag 1 negatives) 6 34 "~")]
112131 ['inconsistent model' at (snag 2 negatives) (program-init-pending at (snag 2 negatives) 7 32 "~")]
113− ['inconsistent message' at (snag 3 negatives) (program-init-pending at (snag 3 negatives) 9 32 "~")]
132+ :: init checks against update's model; main rejects the other message
133+ ['inconsistent message' at (snag 3 negatives) definitions]
114134 ['missing/generic data sample' at (snag 4 negatives) (program-init-pending at (snag 4 negatives) 6 22 "~")]
115135 ['missing initializer' at (snag 5 negatives) definitions]
116136 ['unrelated pending tag' at (snag 6 negatives) (program-init-pending at (snag 6 negatives) 12 6 "%unrelated")]
@@ -136,5 +156,13 @@
136156 (text initializer-no-main)
137157 (text initializer-subs)
138158 ==
139− (turn (program-init-errors prelude internal (text initializer) (text initializer-consumer) (text initializer-unfaced) negatives) |=(reason=tape leaf+reason))
159+ =/ alternates=(list [name=@ta src=@t])
160+ :~ [%initializer-unfaced (text initializer-unfaced)]
161+ [%initializer-pun (text initializer-pun)]
162+ [%initializer-alias (text initializer-alias)]
163+ [%initializer-open-update (text initializer-open-update)]
164+ [%initializer-open-view (text initializer-open-view)]
165+ [%initializer-nested-branch (text initializer-nested-branch)]
166+ ==
167+ (turn (program-init-errors prelude internal (text initializer) (text initializer-consumer) alternates negatives) |=(reason=tape leaf+reason))
140168--
tests/type-program-main/about.txt+1−1
@@ -1 +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.
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. Initializer recovery takes its model from update's two-item sample, or else from main's own program fit, so the alternate fixtures (update written as one faced mold, a pun, a named mold or generic in the model, and generic view and subs samples) recover their initializer like the island. Another alternate's initializer branches over a nested call's union, which only ordinary whole-gate inference takes. It does not execute a program or establish runtime watchability.
tests/type-program-main/initializer-alias.txtnew file+11
@@ -0,0 +1,11 @@
1++$ model [xs=(list @t) draft=@t error=(unit @t)]
2++$ message
3+ %start
4+ %stop
5++$ input [message model]
6+++ main (program init update view subs)
7+++ init |= ts=(list @t) [ts "" ~]
8+++ update |= in=input
9+ ^- [model (list (cmd message))] [[~ "" ~] ~]
10+++ view |= state=model ^- (element message) (text "view")
11+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-main/initializer-nested-branch.txtnew file+24
@@ -0,0 +1,24 @@
1++$ model [xs=(list @t) draft=@t error=(unit @t)]
2++$ message
3+ %start
4+ %stop
5++$ fill
6+ %none
7+ %some
8+++ main (program init update view subs)
9+++ classify |= n=@ud
10+ ^- fill
11+ ?- (eq n 0)
12+ %.y %none
13+ %.n %some
14+++ init |= ts=(list @t)
15+ [
16+ (?- (classify (lent ts))
17+ %none ~["(empty)"]
18+ %some ts
19+ ""
20+ ~
21+++ update |= [msg=message state=model]
22+ ^- [model (list (cmd message))] [state ~]
23+++ view |= state=model ^- (element message) (text "view")
24+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-main/initializer-open-update.txtnew file+10
@@ -0,0 +1,10 @@
1++$ model [xs=(list @t) draft=@t error=(unit @t)]
2++$ message
3+ %start
4+ %stop
5+++ main (program init update view subs)
6+++ init |= ts=(list @t) [ts "" ~]
7+++ update |= [msg=message state=S]
8+ ^- [S (list (cmd message))] [state ~]
9+++ view |= state=model ^- (element message) (text "view")
10+++ subs |= state=model ^- (list (sub message)) ~
tests/type-program-main/initializer-open-view.txtnew file+11
@@ -0,0 +1,11 @@
1++$ model [xs=(list @t) draft=@t error=(unit @t)]
2++$ message
3+ %start
4+ %stop
5++$ input [message model]
6+++ main (program init update view subs)
7+++ init |= ts=(list @t) [ts "" ~]
8+++ update |= =input
9+ ^- [model (list (cmd message))] [[~ "" ~] ~]
10+++ view |= state ^- (element message) (text "view")
11+++ subs |= state ^- (list (sub message)) ~
tests/type-program-main/initializer-pun.txtnew file+11
@@ -0,0 +1,11 @@
1++$ model [xs=(list @t) draft=@t error=(unit @t)]
2++$ message
3+ %start
4+ %stop
5++$ input [message model]
6+++ main (program init update view subs)
7+++ init |= ts=(list @t) [ts "" ~]
8+++ update |= =input
9+ ^- [model (list (cmd message))] [[~ "" ~] ~]
10+++ view |= state=model ^- (element message) (text "view")
11+++ subs |= state=model ^- (list (sub message)) ~
tests/type-todo-full/about.txt+1−1
@@ -1,3 +1,3 @@
11source: docs/spec/overview.md, worked example 3; my-app/ui/todo-list.jibb must remain byte-identical to tests/type-gate-free/todo.txt.
2−tests: Full detailed and legacy checking of the unchanged todo island through the real Hoon readers and API. Assert the exact closed main type and structural downstream import, plus wrong model/message/result, ambiguous or open mapper, aliased mapper, non-gate view, and wrong watch rejection. The report does not execute Jibb or establish runtime watching.
2+tests: Full detailed and legacy checking of the unchanged todo island through the real Hoon readers and API. Assert the exact closed main type and structural downstream import, plus a variant whose initializer is a gate cast to its full type, which only ordinary inference accepts, so it fails if a keyed view skips ordinary inference again, and wrong model/message/result, ambiguous or open mapper, aliased mapper, non-gate view, and wrong watch rejection. The report does not execute Jibb or establish runtime watching.
33expect: shared eval and ship guards
tests/type-todo-full/cast-init.txt+2−2
@@ -13,8 +13,8 @@
1313++ make-model |= ts=(list item.todo)
1414 ^- model [ts "" ~]
1515
16−++ init |= ts=(list item.todo)
17− ^- model (make-model ts)
16+++ init ^- $-((list item.todo) model)
17+ |= ts=(list item.todo) (make-model ts)
1818
1919++ update |= [=msg m=model]
2020 ?- msg
tools/testdata/ship-selftest+2
@@ -418,6 +418,8 @@ def generator_checks(tmp):
418418 'source', 'consumer', 'gate-model', 'gate-data', 'nonempty-subs',
419419 'mismatched-model', 'arbitrary-main', 'alias-main', 'open-message',
420420 'initializer', 'initializer-consumer', 'initializer-unfaced',
421+ 'initializer-pun', 'initializer-alias', 'initializer-open-update',
422+ 'initializer-open-view', 'initializer-nested-branch',
421423 'initializer-error', 'initializer-earlier', 'initializer-model',
422424 'initializer-message', 'initializer-generic', 'initializer-missing',
423425 'initializer-tag', 'initializer-no-main', 'initializer-subs')} <= set(normal.files))
tools/type-program-init-test+8−2
@@ -15,7 +15,10 @@ def body(name):
1515 text = (root / 'tests/lib' / name).read_text()
1616 return text[text.index('\n|%\n') + 1:]
1717
18−names = ('initializer', 'initializer-consumer', 'initializer-unfaced',
18+alternates = ('initializer-unfaced', 'initializer-pun', 'initializer-alias',
19+ 'initializer-open-update', 'initializer-open-view',
20+ 'initializer-nested-branch')
21+names = ('initializer', 'initializer-consumer') + alternates + (
1922 'initializer-error', 'initializer-earlier', 'initializer-model',
2023 'initializer-message', 'initializer-generic', 'initializer-missing',
2124 'initializer-tag', 'initializer-no-main', 'initializer-subs')
@@ -29,7 +32,10 @@ expression = ('=/ jibb .\n=/ prelude=@t prelude-text\n'
2932 ' (text:suite initializer-message)\n (text:suite initializer-generic)\n'
3033 ' (text:suite initializer-missing)\n (text:suite initializer-tag)\n'
3134 ' (text:suite initializer-no-main)\n (text:suite initializer-subs)\n ==\n'
32− '=/ failures=(list tape) (program-init-errors:suite prelude internal (text:suite initializer) (text:suite initializer-consumer) (text:suite initializer-unfaced) negatives)\n'
35+ '=/ alternates=(list [name=@ta src=@t])\n :~ ' +
36+ '\n '.join("[%" + name + " (text:suite " + name + ")]" for name in alternates) +
37+ '\n ==\n'
38+ '=/ failures=(list tape) (program-init-errors:suite prelude internal (text:suite initializer) (text:suite initializer-consumer) alternates negatives)\n'
3339 '^- @t\n?~ failures \'program initializer checks passed\'\n'
3440 '(of-wain:format (turn failures crip))\n')
3541with tempfile.TemporaryDirectory(prefix='jibb-program-init-') as tmp: