93d6b23 · jibb · git.iko.soy

git.iko.soy/jibb

on master help sign in

Recover every direct initializer by one path

93d6b23Claude15 hours ago

docs/compiler.md+2−2

compare with master

unifiedsplit

@@ -144,9 +144,9 @@ A store `main` is recognized only as a direct, unqualified `(store init update)`

144

145The 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.

146

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.

148

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.

150

151A 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.

152

docs/status.md+2−2

@@ -51,13 +51,13 @@ A separate source-backed analysis can prove one named mold gate-free, report a d

52The 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.

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.

56Static 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.

58The 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.

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.

62Imported 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.

jibb-dev/lib/jibb.hoon+101−152

@@ -13338,21 +13338,6 @@

13338 %body ?~(defs.e $(e final.e) e)

13339 * e

13340 ==

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

13356::

13341::

13357:: Recover only the update of an already recognized direct program main.

13342:: Recover only the update of an already recognized direct program main.

13358:: Its written sample determines the message/model relationship; the canonical

13343:: Its written sample determines the message/model relationship; the canonical

@@ -14169,21 +14154,89 @@

14169 ?. ?=(~ (itype-vars typ.u.recovered)) ~

14154 ?. ?=(~ (itype-vars typ.u.recovered)) ~

14170 `[env.u.added grouped.resolution artifacts.u.added]

14155 `[env.u.added grouped.resolution artifacts.u.added]

14171::

14156::

14172−++ program-init-null-sample

14157+:: The model a direct program's initializer must produce. Update's written

14173− |= d=def

14158+:: two-item sample gives it when it can be read. Otherwise main's own program

14174− ^- ?

14159+:: fit does: update, view and subs are fitted together against the prelude

14175− =/ written=(unit sample) (direct-gate-sample d)

14160+:: program's sample, as main's call will fit them, with the initializer an

14176− ?~ written |

14161+:: open variable. Only the initializer's data may stay open, a replay of the

14177− ?. ?=(%bare -.u.written) |

14162+:: fit must not move, and the model must come out closed and tag-free.

14178− =/ sh=shape shape.u.written

14163+++ program-init-model

14179− ?. ?=(%const -.sh) |

14164+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv program=ischeme program-def=def initial=istate]

14180− =(%null form.lit.sh)

14165+ ^- (unit itype)

14181−::

14166+ =/ relation=(unit [message=itype model=itype])

14182−:: The tuple-ending-null initializer retry above intentionally keeps its own

14167+ (program-update-relation update.parts ds env)

14183−:: boundary. A direct null-sample initializer can instead receive the closed

14168+ ?^ relation `model.u.relation

14184−:: model already established by update, view and subscriptions.

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.

14185++ program-plain-init-context

14238++ 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]

14187 ^- (unit iresolved)

14240 ^- (unit iresolved)

14188 =/ env=ienv env.resolution

14241 =/ env=ienv env.resolution

14189 ?^ (ienv-lookup %main env) ~

14242 ?^ (ienv-lookup %main env) ~

@@ -14191,15 +14244,11 @@

14191 ?~ (ienv-lookup update.parts env) ~

14244 ?~ (ienv-lookup update.parts env) ~

14192 ?~ (ienv-lookup view.parts env) ~

14245 ?~ (ienv-lookup view.parts env) ~

14193 ?~ (ienv-lookup subs.parts env) ~

14246 ?~ (ienv-lookup subs.parts env) ~

14194− =/ relation=(unit [message=itype model=itype])

14195− (program-update-relation update.parts ds env)

14196− ?~ relation ~

14197 =/ inits=(list def)

14247 =/ inits=(list def)

14198 (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))

14248 (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))

14199 ?. ?=([* ~] inits) ~

14249 ?. ?=([* ~] inits) ~

14200 =/ init-def=def i.inits

14250 =/ init-def=def i.inits

14201 ?> ?=(%value -.init-def)

14251 ?> ?=(%value -.init-def)

14202− ?. (program-init-null-sample init-def) ~

14203 =/ written=(unit sample) (direct-gate-sample init-def)

14252 =/ written=(unit sample) (direct-gate-sample init-def)

14204 ?~ written ~

14253 ?~ written ~

14205 =/ body=expr

14254 =/ body=expr

@@ -14209,10 +14258,12 @@

14209 * !!

14258 * !!

14210 ==

14259 ==

14211 ?~ prelude.initial ~

14260 ?~ prelude.initial ~

14212− ?~ (ienv-lookup %program values.u.prelude.initial) ~

14261+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)

14262+ ?~ program ~

14213 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)

14263 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)

14214 ?~ heads ~

14264 ?~ heads ~

14215− ?~ (~(get by gates.u.heads) %program) ~

14265+ =/ program-def=(unit def) (~(get by gates.u.heads) %program)

14266+ ?~ program-def ~

14216 =/ checked=(map term def) (direct-checked-gates ds env)

14267 =/ checked=(map term def) (direct-checked-gates ds env)

14217 =/ templates=ienv

14268 =/ templates=ienv

14218 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

14269 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

@@ -14220,130 +14271,31 @@

14220 (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

14271 (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

14221 ?~ fresh ~

14272 ?~ fresh ~

14222 =. next.initial u.fresh

14273 =. 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 ~

14223 =/ init-state=istate (reserve-def-caps val.init-def initial)

14280 =/ init-state=istate (reserve-def-caps val.init-def initial)

14224 =/ sam=isample-result (infer-sample u.written env init-state)

14281 =/ sam=isample-result (infer-sample u.written env init-state)

14225 ?: ?=(%| -.sam) ~

14282 ?: ?=(%| -.sam) ~

14226 ?. ?=(~ (itype-vars typ.p.sam)) ~

14283 ?. ?=(~ (itype-vars typ.p.sam)) ~

14227 ?: (itype-has-tag typ.p.sam) ~

14284 ?: (itype-has-tag typ.p.sam) ~

14228 =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)

14285 =/ 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))

14229 =/ inferred=iresult

14288 =/ 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))

14231 ?: ?=(%| -.inferred) ~

14291 ?: ?=(%| -.inferred) ~

14232 =/ product-fit=ifit

14292 =/ 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)

14234 ?. ?=(%ok -.product-fit) ~

14294 ?. ?=(%ok -.product-fit) ~

14235 =/ merged-product=itype

14295 =/ 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)

14237 =/ actual-cast=itype [%fn typ.p.sam merged-product]

14297 =/ actual-cast=itype [%fn typ.p.sam merged-product]

14238− =/ closed=itype [%fn typ.p.sam model.u.relation]

14298+ =/ closed=itype [%fn typ.p.sam u.model]

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]

14347 =/ cast=ifit

14299 =/ cast=ifit

14348 (itype-fit actual-cast closed sub.product-fit next.product-fit)

14300 (itype-fit actual-cast closed sub.product-fit next.product-fit)

14349 ?. ?=(%ok -.cast) ~

14301 ?. ?=(%ok -.cast) ~

@@ -14847,11 +14799,8 @@

14847 ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))

14799 ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))

14848 =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)

14800 =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)

14849 =/ initialized=(unit iresolved)

14801 =/ initialized=(unit iresolved)

14850− (program-init-context u.main u.main-parts ds with-view state)

14802+ (program-plain-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)

14803+ =/ components=iresolved ?~(initialized with-view u.initialized)

14855 (program-main-context u.main ds components state)

14804 (program-main-context u.main ds components state)

14856 =. env env.recovered

14805 =. env env.recovered

14857 =. artifacts.resolution artifacts.recovered

14806 =. artifacts.resolution artifacts.recovered

tests/lib/jibb-program-init.hoon+32−4

@@ -5,6 +5,11 @@

5/* initializer %txt /tests/type-program-main/initializer/txt

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

7/* 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

8/* initializer-error %txt /tests/type-program-main/initializer-error/txt

13/* initializer-error %txt /tests/type-program-main/initializer-error/txt

9/* initializer-earlier %txt /tests/type-program-main/initializer-earlier/txt

14/* initializer-earlier %txt /tests/type-program-main/initializer-earlier/txt

10/* initializer-model %txt /tests/type-program-main/initializer-model/txt

15/* initializer-model %txt /tests/type-program-main/initializer-model/txt

@@ -94,8 +99,22 @@

94 ^- @t

99 ^- @t

95 (show-error:jibb src [at line col (weld "nothing fixes the union of " literal)])

100 (show-error:jibb src [at line col (weld "nothing fixes the union of " literal)])

96::

101::

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+::

97++ program-init-errors

116++ 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)]

99 ^- (list tape)

118 ^- (list tape)

100 =/ prepared=(unit iprelude:jibb) (program-init-prepared public private)

119 =/ prepared=(unit iprelude:jibb) (program-init-prepared public private)

101 ?~ prepared ~["synthetic program prelude did not prepare for contextual init"]

120 ?~ prepared ~["synthetic program prelude did not prepare for contextual init"]

@@ -103,14 +122,15 @@

103 =/ positives=(list tape)

122 =/ positives=(list tape)

104 %+ weld

123 %+ weld

105 (program-init-positive at island `downstream u.prepared)

124 (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)

107 ?. =(9 (lent negatives)) ~["contextual negative fixture count differs"]

126 ?. =(9 (lent negatives)) ~["contextual negative fixture count differs"]

108 =/ definitions=@t (crip "module definitions need unsupported inference: {(spud at)}: ++ main")

127 =/ definitions=@t (crip "module definitions need unsupported inference: {(spud at)}: ++ main")

109 =/ cases=(list [label=@t at=path src=@t boundary=@t])

128 =/ cases=(list [label=@t at=path src=@t boundary=@t])

110 :~ ['incompatible error field' at (snag 0 negatives) (program-init-pending at (snag 0 negatives) 6 32 "~")]

129 :~ ['incompatible error field' at (snag 0 negatives) (program-init-pending at (snag 0 negatives) 6 32 "~")]

111 ['earlier tuple mismatch' at (snag 1 negatives) (program-init-pending at (snag 1 negatives) 6 34 "~")]

130 ['earlier tuple mismatch' at (snag 1 negatives) (program-init-pending at (snag 1 negatives) 6 34 "~")]

112 ['inconsistent model' at (snag 2 negatives) (program-init-pending at (snag 2 negatives) 7 32 "~")]

131 ['inconsistent model' at (snag 2 negatives) (program-init-pending at (snag 2 negatives) 7 32 "~")]

132+ :: init checks against update's model; main rejects the other message

113− ['inconsistent message' at (snag 3 negatives) (program-init-pending at (snag 3 negatives) 9 32 "~")]

133+ ['inconsistent message' at (snag 3 negatives) definitions]

114 ['missing/generic data sample' at (snag 4 negatives) (program-init-pending at (snag 4 negatives) 6 22 "~")]

134 ['missing/generic data sample' at (snag 4 negatives) (program-init-pending at (snag 4 negatives) 6 22 "~")]

115 ['missing initializer' at (snag 5 negatives) definitions]

135 ['missing initializer' at (snag 5 negatives) definitions]

116 ['unrelated pending tag' at (snag 6 negatives) (program-init-pending at (snag 6 negatives) 12 6 "%unrelated")]

136 ['unrelated pending tag' at (snag 6 negatives) (program-init-pending at (snag 6 negatives) 12 6 "%unrelated")]

@@ -136,5 +156,13 @@

136 (text initializer-no-main)

156 (text initializer-no-main)

137 (text initializer-subs)

157 (text initializer-subs)

138 ==

158 ==

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+ ==

139− (turn (program-init-errors prelude internal (text initializer) (text initializer-consumer) (text initializer-unfaced) negatives) |=(reason=tape leaf+reason))

167+ (turn (program-init-errors prelude internal (text initializer) (text initializer-consumer) alternates negatives) |=(reason=tape leaf+reason))

140--

168--

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 @@

1source: 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.

3expect: shared eval and ship guards

tests/type-todo-full/cast-init.txt+2−2

@@ -13,8 +13,8 @@

13++ make-model |= ts=(list item.todo)

14 ^- model [ts "" ~]

16+++ init ^- $-((list item.todo) model)

16−++ init |= ts=(list item.todo)

17+ |= ts=(list item.todo) (make-model ts)

17− ^- model (make-model ts)

19++ update |= [=msg m=model]

20 ?- msg

tools/testdata/ship-selftest+2

@@ -418,6 +418,8 @@ def generator_checks(tmp):

418 'source', 'consumer', 'gate-model', 'gate-data', 'nonempty-subs',

419 'mismatched-model', 'arbitrary-main', 'alias-main', 'open-message',

420 'initializer', 'initializer-consumer', 'initializer-unfaced',

421+ 'initializer-pun', 'initializer-alias', 'initializer-open-update',

422+ 'initializer-open-view', 'initializer-nested-branch',

421 'initializer-error', 'initializer-earlier', 'initializer-model',

423 'initializer-error', 'initializer-earlier', 'initializer-model',

422 'initializer-message', 'initializer-generic', 'initializer-missing',

424 'initializer-message', 'initializer-generic', 'initializer-missing',

423 'initializer-tag', 'initializer-no-main', 'initializer-subs')} <= set(normal.files))

425 'initializer-tag', 'initializer-no-main', 'initializer-subs')} <= set(normal.files))

tools/type-program-init-test+8−2

@@ -15,7 +15,10 @@ def body(name):

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

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

18+alternates = ('initializer-unfaced', 'initializer-pun', 'initializer-alias',

19+ 'initializer-open-update', 'initializer-open-view',

20+ 'initializer-nested-branch')

18−names = ('initializer', 'initializer-consumer', 'initializer-unfaced',

21+names = ('initializer', 'initializer-consumer') + alternates + (

19 'initializer-error', 'initializer-earlier', 'initializer-model',

22 'initializer-error', 'initializer-earlier', 'initializer-model',

20 'initializer-message', 'initializer-generic', 'initializer-missing',

23 'initializer-message', 'initializer-generic', 'initializer-missing',

21 'initializer-tag', 'initializer-no-main', 'initializer-subs')

24 'initializer-tag', 'initializer-no-main', 'initializer-subs')

@@ -29,7 +32,10 @@ expression = ('=/ jibb .\n=/ prelude=@t prelude-text\n'

29 ' (text:suite initializer-message)\n (text:suite initializer-generic)\n'

32 ' (text:suite initializer-message)\n (text:suite initializer-generic)\n'

30 ' (text:suite initializer-missing)\n (text:suite initializer-tag)\n'

33 ' (text:suite initializer-missing)\n (text:suite initializer-tag)\n'

31 ' (text:suite initializer-no-main)\n (text:suite initializer-subs)\n ==\n'

34 ' (text:suite initializer-no-main)\n (text:suite initializer-subs)\n ==\n'

35+ '=/ alternates=(list [name=@ta src=@t])\n :~ ' +

36+ '\n '.join("[%" + name + " (text:suite " + name + ")]" for name in alternates) +

37+ '\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'

38+ '=/ failures=(list tape) (program-init-errors:suite prelude internal (text:suite initializer) (text:suite initializer-consumer) alternates negatives)\n'

33 '^- @t\n?~ failures \'program initializer checks passed\'\n'

39 '^- @t\n?~ failures \'program initializer checks passed\'\n'

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

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

35with tempfile.TemporaryDirectory(prefix='jibb-program-init-') as tmp:

41with tempfile.TemporaryDirectory(prefix='jibb-program-init-') as tmp: