706035c · jibb · git.iko.soy

git.iko.soy/jibb

Analyze gate-free source molds

Add a bounded, conservative gate-free analysis that records a field path for a definite gate and preserves unknown results for unproved types. Track inhabitation so empty structures do not produce false witnesses. Resolve a selected mold from source with its prelude, reader and import evidence. Exercise the real todo model, callbacks, unknown nouns, recursive shapes and budget boundaries under eval and on the ship. This is mold analysis, not complete island or watchability checking.

commit706035c1395666706cfc845244f7eab0145b8c9e authoriko <mail@iko.soy> dateSat 31 Oct 2026, 11:34 (1 day ago) parent72acdb3

14 files changed+516−3

compare with master

unifiedsplit

docs/compiler.md+2 docs/development.md+4 docs/status.md+5−2 jibb-dev/lib/jibb.hoon+119 tests/lib/jibb-gate-free-guards.hoon+79 tests/lib/jibb-gate-free-source.hoon+95 tests/type-gate-free/about.txt+1 tests/type-gate-free/expected.txt+9 tests/type-gate-free/todo-gate.txt+40 tests/type-gate-free/todo-noun.txt+40 tests/type-gate-free/todo.txt+40 tools/testdata/ship-selftest+3−1 tools/type-gate-free-guards-test+29 tools/type-gate-free-source-test+50

docs/compiler.md+2

@@ -108,6 +108,8 @@ A call whose direct result is a known named generic union can receive a matching

108108

109109A two-item tuple with an explicit term, null or loobean head can receive payload context from a known union when every alternative is a literal-headed cell and its head noun is unique. The payload must be a direct wing-headed call, optionally grouped, with literal, wing or constructor arguments. The checker first retains the original inference if it already fits; otherwise it tries the contextual path once and fits the selected case and enclosing union. It declines this path if any substitution has a structural root, because a caller may have walked away variable provenance. Duplicate heads, opaque competitors and other shapes also stay conservative. The guard scans the substitution for each eligible tuple and may perform one extra shallow inference; it does not guarantee globally linear work. This lets an explicitly typed todo subscription body infer; it does not check an island or prove request watchability.

110110

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

112+

111113Each 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.

112114

113115`+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+4

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

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

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

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

80+| `tools/type-gate-free-guards-test` | Checks bounded gate-free verdicts, inhabitation and witness paths under eval and on the ship |

81+| `tools/type-gate-free-source-test` | Checks source-backed todo mold analysis through the real readers under eval and on the ship |

8082| `tools/type-sub-guards-test` | Checks source-backed subscription mold dependencies under eval and on the ship |

8183| `tools/type-ask-guards-test` | Runs ask origin and canonical list/unit bootstrap guards under eval and on the ship |

8284| `tools/type-request-guards-test` | Runs request evidence, source consistency and cache provenance guards under eval and on the ship |

@@ -115,6 +117,8 @@ tools/type-todo-api-test # real todo API partial inference and reader

115117tools/type-closed-gate-guards-test # closed gate fit guards pass

116118tools/type-constructor-fit-guards-test # constructor fit guards pass

117119tools/type-nested-union-guards-test # nested union selector guards pass

120+tools/type-gate-free-guards-test # bounded gate-free classifier guards pass

121+tools/type-gate-free-source-test # real todo mold analysis and source guards pass

118122tools/type-sub-guards-test # subscription source guards pass

119123tools/type-ask-guards-test # ask source and bootstrap guards pass

120124tools/type-request-guards-test # request evidence and cache guards pass

docs/status.md+5−2

@@ -29,6 +29,8 @@ The internal prelude defines a transparent generic `ask` with pure, agent and st

2929

3030Known same-origin generic-union result context can now constrain a call before its arguments are inferred. An unresolved or opaque constructor target stays unsupported rather than producing a definite mismatch; proven missing tags still report errors. A todo request with explicit `(ask msg)` context can infer `|=%got`; its uncontextualized form remains unsupported. A two-item literal-headed tuple can receive payload context from a known union of uniquely headed literal cells when its payload is a shallow wing-headed call with literal, wing or constructor arguments. Existing inference takes precedence when it fits; otherwise the checker tries the contextual path once. It conservatively declines that path when any substitution has a structural root, as well as for duplicate or opaque competitors. The guard scans substitutions per eligible tuple and may add one shallow inference; no global linear-time bound is claimed. This allows an explicitly typed todo subscription body to infer, but does not check the island or prove request watchability.

3131

32+A separate source-backed analysis can prove one named mold gate-free, report a definite gate with a field path, or return unknown. It retains the prepared prelude, source bundle, reader results and resolved imports; the actual todo model proves gate-free, while a callback field reports its path and `*` remains unknown. Its classifier is capped at 256 nodes, not the surrounding parse and import work. API, store and private roots are unsupported, and the artifact does not check a module or island, infer generalized constraints, or prove watchability.

33+

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

3335

3436For 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.

@@ -60,7 +62,7 @@ What the plan asks for, and where it is:

6062Besides the plan's list:

6163

6264- 649 golden cases: 429 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.

63−- The 649-case corpus passed under `urbit eval` in 96.0 s while other checks were running. The fake ship passed all 676 tests, including the 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 and nested-union guards, with 71.8 s for sync and 85.7 s for tests. 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.

65+- The 649-case corpus passed under `urbit eval` in 91.6 s while other checks were running. The fake ship passed all 678 tests, including the 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 and gate-free guards, with 66.8 s for sync and 81.8 s for tests. 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.

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

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

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

@@ -155,7 +157,8 @@ Besides the plan's list:

155157| dde791c | 2026-10-31 | Infer a source-backed request-gate type through ordinary imports |

156158| a1c5f35 | 2026-10-31 | Infer supported multi-path requests and named closed folds |

157159| 911ca0c | 2026-10-31 | Propagate union context, define subscriptions and match literal nouns |

158−| This change | 2026-10-31 | Infer selected nested union payloads from context |

160+| 72acdb3 | 2026-10-31 | Infer selected nested union payloads from context |

161+| This change | 2026-10-31 | Analyze gate-free source molds with field witnesses |

159162

160163## Checking it

161164

jibb-dev/lib/jibb.hoon+119

@@ -5609,6 +5609,71 @@

56095609 ?. (width-in-order order.source.shape order.target.shape) ~

56105610 (width-fit-fields index.source.shape order.target.shape sub next)

56115611::

5612+:: Provisional, globally budgeted gate-free proof. %no includes a

5613+:: gate-bearing witness; an uninhabited sibling could invalidate it.

5614+:: Input types must be resolved and normalized under valid substitutions,

5615+:: from trusted source-backed interfaces and reader results. Collection

5616+:: list/unit names rely on their existing identity invariant; this arm

5617+:: does not validate fabricated internal types.

5618++$ igf-segment

5619+ $% [%field name=term]

5620+ [%head ~]

5621+ [%tail ~]

5622+ [%item ~]

5623+ [%case index=@ud]

5624+ ==

5625++$ igate-free [verdict=?(%yes %no %unknown) inhabited=? left=@ud path=(unit (list igf-segment))]

5626+++ gate-free-types

5627+ |= [types=(list itype) fuel=@ud path=(list igf-segment) index=@ud]

5628+ ^- igate-free

5629+ ?~ types [%yes | fuel ~]

5630+ ?: =(0 fuel) [%unknown | 0 ~]

5631+ =/ first=igate-free (gate-free-type i.types fuel [[%case index] path])

5632+ ?: =(%no verdict.first) first

5633+ =/ rest=igate-free $(types t.types, fuel left.first, index +(index))

5634+ ?: =(%no verdict.rest) rest

5635+ =/ inhabited=? |(inhabited.first inhabited.rest)

5636+ ?: |(=(%unknown verdict.first) =(%unknown verdict.rest)) [%unknown inhabited left.rest ~]

5637+ [%yes inhabited left.rest ~]

5638+++ gate-free-type

5639+ |= [typ=itype fuel=@ud path=(list igf-segment)]

5640+ ^- igate-free

5641+ ?: =(0 fuel) [%unknown | 0 ~]

5642+ =. fuel (dec fuel)

5643+ ?- -.typ

5644+ %fn [%no & fuel `(flop path)]

5645+ %atom [%yes & fuel ~]

5646+ %any-atom [%yes & fuel ~]

5647+ %flag [%yes & fuel ~]

5648+ %const [%yes & fuel ~]

5649+ %face $(typ body.typ, path [[%field name.typ] path])

5650+ %cell

5651+ =/ head=igate-free $(typ hed.typ, path [[%head ~] path])

5652+ =/ tail=igate-free $(typ tal.typ, fuel left.head, path [[%tail ~] path])

5653+ =/ inhabited=? &(inhabited.head inhabited.tail)

5654+ ?: &(=(%no verdict.head) inhabited.tail) head(left left.tail)

5655+ ?: &(=(%no verdict.tail) inhabited.head) tail

5656+ ?: |(!=(%yes verdict.head) !=(%yes verdict.tail)) [%unknown inhabited left.tail ~]

5657+ [%yes inhabited left.tail ~]

5658+ %collection

5659+ ?. |(=(%list name.typ) =(%unit name.typ)) [%unknown | fuel ~]

5660+ ?. ?=([* ~] args.typ) [%unknown | fuel ~]

5661+ =/ item=igate-free $(typ i.args.typ, path [[%item ~] path])

5662+ item(inhabited &)

5663+ %union

5664+ ?~ cases.typ [%unknown | fuel ~]

5665+ (gate-free-types cases.typ fuel path 0)

5666+ %noun [%unknown & fuel ~]

5667+ %var [%unknown | fuel ~]

5668+ %avar [%yes & fuel ~]

5669+ %rvar [%yes & fuel ~]

5670+ %nvar [%yes & fuel ~]

5671+ %rnvar [%yes & fuel ~]

5672+ %tag [%unknown | fuel ~]

5673+ %recursive [%unknown | fuel ~]

5674+ %jrec [%yes & fuel ~]

5675+ ==

5676+::

56125677+$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile) holes=(list ihole) jrec-fuel=@ud projections=(list iwprojection)]

56135678+$ idiag [msg=tape sites=(list [at=span note=tape])]

56145679+$ iresult (each [typ=itype state=istate] idiag)

@@ -11382,6 +11447,60 @@

1138211447 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]

1138311448 [%& [iface [[at iface] cache.p.js]]]

1138411449::

11450+:: A source-bound analysis of one named mold, not a module, island,

11451+:: request, watchability or runtime check. The host owns the trusted

11452+:: prepared prelude, canonical paths and reader/source version identities.

11453+:: The 256-node cap covers only classification, not source/graph work.

11454++$ igate-free-mold

11455+ [at=path source=@t name=term prepared=iprelude externals=iexternals marks=imark-externals modules=jbundle dependencies=jcache mold=ischeme requested=@ud budget=@ud result=igate-free]

11456+++ gate-free-mold-source

11457+ |= [file=path src=@t name=term externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude) fuel=@ud]

11458+ ^- (each igate-free-mold @t)

11459+ ?~ file [%| 'mold analysis needs a path ending in jibb']

11460+ ?. =(%jibb (rear file)) [%| 'mold analysis needs a path ending in jibb']

11461+ ?: |(=(file /lib/jibb/internal/jibb) =(file /lib/jibb/primitives/jibb))

11462+ [%| 'the prelude internal modules are private']

11463+ ?: ?=([%ui %api *] file) [%| 'API declarations need unsupported mold analysis']

11464+ ?: ?=([%ui %stores *] file) [%| 'store declarations need unsupported mold analysis']

11465+ =/ entries=jbundle (skim modules |=(m=jsource =(file at.m)))

11466+ ?: (gth (lent entries) 1) [%| 'duplicate root module sources']

11467+ =/ wrong-root=? ?~(entries | !=(source.i.entries src))

11468+ ?: wrong-root [%| 'root module source does not match bundle']

11469+ =/ parsed (parse file src)

11470+ ?: ?=(%| -.parsed) [%| 'mold source does not parse']

11471+ =/ mod=module p.parsed

11472+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)

11473+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]

11474+ ?~ prepared [%| 'mold analysis needs the prepared prelude']

11475+ ?. (module-scope-valid mod values.u.prepared molds.u.prepared)

11476+ [%| 'mold source has conflicting or unsupported scope']

11477+ =/ selected=(list def)

11478+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(name.d name))))

11479+ ?~ selected [%| 'selected mold is not declared']

11480+ ?^ t.selected [%| 'selected mold is not unique']

11481+ ?> ?=(%mold -.i.selected)

11482+ =/ public=ifile iface.u.prepared

11483+ =/ js=jimports-result

11484+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)

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

11486+ =/ ms=imolds (collect-simple-molds defs.mod)

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

11488+ =/ globals=(list term) (weld values.u.prepared (weld (import-binding-names imports.mod) vals))

11489+ =/ surs=(list term) (collect-sur-imports imports.mod)

11490+ =/ declared=(list term) (collect-mark-imports imports.mod)

11491+ =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))

11492+ =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))

11493+ =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~]

11494+ =/ inferred=(unit [template=ischeme state=istate])

11495+ (infer-mold-template shape.i.selected state(active ~[name], in-mold &))

11496+ ?~ inferred [%| 'selected mold needs unsupported inference']

11497+ =/ template=ischeme template.u.inferred

11498+ =. typ.template (label-direct-union typ.template shape.i.selected name state)

11499+ =. typ.template (itype-normalize typ.template sub.state.u.inferred)

11500+ =/ cap=@ud (min fuel 256)

11501+ =/ analysis=igate-free (gate-free-type typ.template cap ~)

11502+ [%& [file src name u.prepared externals marks modules cache.p.js template fuel cap analysis]]

11503+::

1138511504:: +golden-types-with-modules fails closed for imports without prelude

1138611505:: scope. +golden-types-with-prelude resolves supported library graphs;

1138711506:: its report remains partial and unreachable sources are not examined.

tests/lib/jibb-gate-free-guards.hoonnew file+79

@@ -0,0 +1,79 @@

1+:: Budgeted gate-free verdicts require a witness and an inhabited sibling.

2+/+ jibb

3+|%

4+++ gate-free-guard-errors

5+ ^- (list tape)

6+ =/ atom=itype:jibb [%atom %t]

7+ =/ flag=itype:jibb [%flag ~]

8+ =/ noun=itype:jibb [%noun ~]

9+ =/ var=itype:jibb [%var 0]

10+ =/ gate=itype:jibb [%fn atom atom]

11+ =/ item=itype:jibb [%cell [%face %id [%atom %ud]] [%cell [%face %done flag] [%face %text atom]]]

12+ =/ model=itype:jibb [%cell [%face %todos [%collection %list ~[item]]] [%cell [%face %draft atom] [%face %error [%union ~[[%const [%null %n 0 '~']] [%cell [%const [%null %n 0 '~']] [%face %u atom]]] ~ ~ ~]]]]

13+ =/ with-callback=itype:jibb [%cell [%face %data atom] [%face %callback gate]]

14+ =/ ask-like=itype:jibb [%union ~[[%cell [%const [%term %tas %pure '%pure']] [%face %value atom]] [%cell [%const [%term %tas %agent '%agent']] [%face %receive gate]]] ~ ~ ~]

15+ =/ sub-like=itype:jibb [%union ~[[%cell [%const [%term %tas %watch '%watch']] [%face %request ask-like]] [%cell [%const [%term %tas %every '%every']] [%face %reply gate]]] ~ ~ ~]

16+ =/ controls=(list [name=@t typ=itype:jibb fuel=@ud want=?(%yes %no %unknown)])

17+ :~ ['atom' atom 8 %yes]

18+ ['flag' flag 8 %yes]

19+ ['atom variable' [%avar 0] 8 %yes]

20+ ['open variable' var 8 %unknown]

21+ ['noun' noun 8 %unknown]

22+ ['raw gate' gate 8 %no]

23+ ['data item' item 30 %yes]

24+ ['todo model' model 100 %yes]

25+ ['callback field' with-callback 30 %no]

26+ ['ask receiver' ask-like 100 %no]

27+ ['subscription receiver' sub-like 100 %no]

28+ ['list of data items' [%collection %list ~[item]] 40 %yes]

29+ ['list of gates' [%collection %list ~[gate]] 20 %no]

30+ ['other collection' [%collection %map ~[atom atom]] 20 %unknown]

31+ ['open list member' [%collection %list ~[var]] 20 %unknown]

32+ ['known-inhabited noun after gate' [%cell gate noun] 30 %no]

33+ ['known-inhabited noun before gate' [%cell noun gate] 30 %no]

34+ ['unknown sibling after gate' [%cell gate var] 30 %unknown]

35+ ['unknown sibling before gate' [%cell var gate] 30 %unknown]

36+ ['nested unknown sibling' [%cell [%face %callback gate] [%face %other var]] 30 %unknown]

37+ ['unknown union and gate union' [%union ~[var gate] ~ ~ ~] 30 %no]

38+ ['empty union' [%union ~ ~ ~ ~] 30 %unknown]

39+ ['validated jrec qath' [%jrec /lib/jibb/internal/jibb %qath ~ %i %ta %t] 30 %yes]

40+ ['jrec gate sibling' [%cell gate [%jrec /lib/jibb/internal/jibb %qath ~ %i %ta %t]] 30 %no]

41+ ['jrec list member' [%collection %list ~[[%jrec /lib/jibb/internal/jibb %qath ~ %i %ta %t]]] 30 %yes]

42+ ['nominal recursion' [%recursive %sur %node ~] 30 %unknown]

43+ ['unknown sibling budget' [%cell gate var] 2 %unknown]

44+ ['known sibling budget' [%cell gate atom] 2 %unknown]

45+ ['zero budget' atom 0 %unknown]

46+ ['one atom budget' atom 1 %yes]

47+ ['cell needs 3 visits' [%cell atom flag] 2 %unknown]

48+ ['cell exact 3 visits' [%cell atom flag] 3 %yes]

49+ ==

50+ =/ errors=(list @t)

51+ %+ turn controls

52+ |= c=[name=@t typ=itype:jibb fuel=@ud want=?(%yes %no %unknown)]

53+ =/ result=igate-free:jibb (gate-free-type:jibb typ.c fuel.c ~)

54+ ?: =(want.c verdict.result) ''

55+ (cat 3 name.c ': wrong verdict')

56+ =/ a=igate-free:jibb (gate-free-type:jibb with-callback 30 ~)

57+ =? errors !=(path.a `~[[%tail ~] [%field %callback]]) ['callback path incorrect' errors]

58+ =/ b=igate-free:jibb (gate-free-type:jibb [%collection %list ~[gate]] 20 ~)

59+ =? errors !=(path.b `~[[%item ~]]) ['list path incorrect' errors]

60+ =/ c=igate-free:jibb (gate-free-type:jibb model 100 ~)

61+ =? errors ?=(^ path.c) ['gate-free result carries witness path' errors]

62+ :: The explicit budget is shared across the entire normalized type.

63+ =/ deep

64+ |= depth=@ud

65+ ^- itype:jibb

66+ =/ out=itype:jibb [%atom %t]

67+ |-

68+ ?: =(0 depth) out

69+ $(depth (dec depth), out [%face %nested out])

70+ =/ fits=igate-free:jibb (gate-free-type:jibb (deep 255) 256 ~)

71+ =/ exceeds=igate-free:jibb (gate-free-type:jibb (deep 256) 256 ~)

72+ =? errors !=(%yes verdict.fits) ['256 node budget rejected exact fit' errors]

73+ =? errors !=(%unknown verdict.exceeds) ['257 node budget did not fail closed' errors]

74+ =/ errors (skim errors |=(x=@t !=(x '')))

75+ (turn errors trip)

76+++ test-gate-free-guards

77+ ^- tang

78+ (turn gate-free-guard-errors |=(reason=tape leaf+reason))

79+--

tests/lib/jibb-gate-free-source.hoonnew file+95

@@ -0,0 +1,95 @@

1+:: Source-backed mold analysis of the actual todo model; not island checking.

2+/+ jibb, jibb-import

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

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

5+/* sur %txt /tests/type-api-paths/todo-sur/txt

6+/* action %txt /tests/type-api-paths/todo-action/txt

7+/* todos %txt /tests/type-api-paths/todos/txt

8+/* update %txt /tests/type-api-paths/todo-update/txt

9+/* item %txt /tests/type-api-paths/todo-item/txt

10+/* api %txt /tests/type-api-paths/api/txt

11+/* source %txt /tests/type-gate-free/todo/txt

12+/* gate-source %txt /tests/type-gate-free/todo-gate/txt

13+/* noun-source %txt /tests/type-gate-free/todo-noun/txt

14+/* expected %txt /tests/type-gate-free/expected/txt

15+|%

16+++ text

17+ |= lines=wain

18+ ^- @t

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

20+++ gate-free-source-report

21+ |= [public=@t private=@t sur-text=@t action-text=@t todos-text=@t update-text=@t item-text=@t api-text=@t source-text=@t gate-text=@t noun-text=@t]

22+ ^- @t

23+ =/ prepared=(unit iprelude:jibb) (prepare-prelude-with-internal:jibb public private)

24+ ?~ prepared 'prelude unavailable'

25+ =/ todo=type -:(ride -:!>(..zuse) sur-text)

26+ =/ subject=type [%cell [%face %todo todo] -:!>(..zuse)]

27+ =/ ma=* (read-mark:jibb-import %todo-action -:(ride subject action-text))

28+ =/ mt=* (read-mark:jibb-import %todos -:(ride subject todos-text))

29+ =/ mu=* (read-mark:jibb-import %todo-update -:(ride subject update-text))

30+ =/ mi=* (read-mark:jibb-import %todo-item -:(ride subject item-text))

31+ =/ marks=imark-externals:jibb ~[[%todo-action ma] [%todos mt] [%todo-update mu] [%todo-item mi]]

32+ =/ item-input=* (read-named:jibb-import %todo %item todo)

33+ =/ inputs=iexternals:jibb ~[[%todo %item item-input]]

34+ =/ modules=jbundle:jibb ~[[/ui/api/todo/jibb api-text]]

35+ =/ at=path /ui/todo-list/jibb

36+ =/ model (gate-free-mold-source:jibb at source-text %model inputs marks modules prepared 256)

37+ ?: ?=(%| -.model) 'todo model unavailable'

38+ ?. =(%yes verdict.result.p.model) 'todo model not proven gate-free'

39+ ?. &(=(at.p.model at) =(source.p.model source-text) =(name.p.model %model) =(prepared.p.model u.prepared) =(externals.p.model inputs) =(marks.p.model marks) =(modules.p.model modules)) 'source evidence changed'

40+ ?~ dependencies.p.model 'resolved dependency evidence missing'

41+ ?. ?=(%cell -.typ.mold.p.model) 'selected model scheme missing'

42+ ?. &(=(256 requested.p.model) =(256 budget.p.model)) 'requested budget not retained'

43+ =/ callback (gate-free-mold-source:jibb at gate-text %model inputs marks modules prepared 256)

44+ ?: ?=(%| -.callback) 'callback model unavailable'

45+ ?. =(%no verdict.result.p.callback) 'callback was not found'

46+ ?~ path.result.p.callback 'callback path missing'

47+ ?. (lien u.path.result.p.callback |=(part=igf-segment:jibb ?=([%field %callback] part))) 'callback field not in witness'

48+ =/ noun (gate-free-mold-source:jibb at noun-text %model inputs marks modules prepared 256)

49+ ?: ?=(%| -.noun) 'noun model unavailable'

50+ ?. =(%unknown verdict.result.p.noun) 'noun model not unknown'

51+ =/ tiny=@t '+$ sample @t\0a'

52+ =/ low (gate-free-mold-source:jibb /tests/tiny/jibb tiny %sample ~ ~ ~ prepared 0)

53+ ?: ?=(%| -.low) 'zero fuel unavailable'

54+ ?. &(=(%unknown verdict.result.p.low) =(0 budget.p.low)) 'zero fuel not unknown'

55+ =/ capped (gate-free-mold-source:jibb /tests/tiny/jibb tiny %sample ~ ~ ~ prepared 999)

56+ ?: ?=(%| -.capped) 'large fuel unavailable'

57+ ?. &(=(999 requested.p.capped) =(256 budget.p.capped) =(%yes verdict.result.p.capped) =(255 left.result.p.capped)) 'fuel cap incorrect'

58+ =/ matched (gate-free-mold-source:jibb /tests/tiny/jibb tiny %sample ~ ~ ~[[/tests/tiny/jibb tiny]] prepared 256)

59+ ?: ?=(%| -.matched) 'matching root source rejected'

60+ =/ unused-sur=@t '/- unused\0a+$ sample @t\0a'

61+ =/ unused (gate-free-mold-source:jibb /tests/tiny/jibb unused-sur %sample ~ ~ ~ prepared 256)

62+ ?: ?=(%| -.unused) 'unused sur source unexpectedly required'

63+ =/ cycle-source=@t '/= child /tests/child\0a+$ sample @t\0a'

64+ =/ child-source=@t '/= root /tests/tiny\0a+$ child @t\0a'

65+ =/ cycle (gate-free-mold-source:jibb /tests/tiny/jibb cycle-source %sample ~ ~ ~[[/tests/child/jibb child-source]] prepared 256)

66+ ?. ?=(%| -.cycle) 'root import cycle accepted'

67+ =/ unprepared (gate-free-mold-source:jibb /tests/tiny/jibb tiny %sample ~ ~ ~ ~ 256)

68+ ?. ?=(%| -.unprepared) 'missing prelude accepted'

69+ =/ cases=(list [name=@t path=path src=@t mold=term external=iexternals:jibb mark=imark-externals:jibb bundle=jbundle:jibb])

70+ :~ ['missing mold' at source-text %missing inputs marks modules]

71+ ['missing API' at source-text %model inputs marks ~]

72+ ['missing mark' at source-text %model inputs (skim marks |=(m=[mark=term result=*] !=(%todo-update mark.m))) modules]

73+ ['root mismatch' at source-text %model inputs marks [[at gate-text] modules]]

74+ ['duplicate root' at source-text %model inputs marks [[at source-text] [at source-text] modules]]

75+ ['duplicate field' at (cat 3 source-text '\0a+$ duplicate [x=@t x=@p]\0a') %model inputs marks modules]

76+ ['invalid syntax' at '++ incomplete |=' %model inputs marks modules]

77+ ['private root' /lib/jibb/internal/jibb source-text %model inputs marks modules]

78+ ['API root' /ui/api/todo/jibb source-text %model inputs marks modules]

79+ ['store root poke' /ui/stores/cart/jibb '+$ poke @t\0a' %poke ~ ~ ~]

80+ ==

81+ =/ errors=(list @t)

82+ %+ turn cases

83+ |= c=[name=@t path=path src=@t mold=term external=iexternals:jibb mark=imark-externals:jibb bundle=jbundle:jibb]

84+ =/ got (gate-free-mold-source:jibb path.c src.c mold.c external.c mark.c bundle.c prepared 256)

85+ ?: ?=(%| -.got) ''

86+ (cat 3 name.c ': unexpectedly succeeded')

87+ =/ errors (skim errors |=(x=@t !=(x '')))

88+ ?^ errors (of-wain:format errors)

89+ 'todo model: gate-free\0acallback model: gate at callback\0anoun model: unknown\0azero fuel: unknown\0aoversized fuel: capped\0ainvalid inputs: rejected\0asource evidence: retained\0amatching root and unused sur: accepted\0aroot import cycle: rejected'

90+++ test-gate-free-source

91+ ^- tang

92+ =/ actual (gate-free-source-report prelude internal (text sur) (text action) (text todos) (text update) (text item) (text api) (text source) (text gate-source) (text noun-source))

93+ ?. =((to-wain:format (cat 3 actual '\0a')) expected) ~[leaf+"gate-free mold report differs from expected"]

94+ ~

95+--

tests/type-gate-free/about.txtnew file+1

@@ -0,0 +1 @@

1+The unchanged todo island source is used only to resolve its model mold through the actual todo API, /sur and mark readers. The eval runner verifies its copy matches the application source. Controls also add a callback or noun field and exercise unavailable, malformed and ambiguous input. This is partial mold analysis only: no complete module, island kind, runtime or watchability claim is made.

tests/type-gate-free/expected.txtnew file+9

@@ -0,0 +1,9 @@

1+todo model: gate-free

2+callback model: gate at callback

3+noun model: unknown

4+zero fuel: unknown

5+oversized fuel: capped

6+invalid inputs: rejected

7+source evidence: retained

8+matching root and unused sur: accepted

9+root import cycle: rejected

tests/type-gate-free/todo-gate.txtnew file+40

@@ -0,0 +1,40 @@

1+/= todo /ui/api/todo

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

5++$ model [todos=(list item.todo) draft=@t error=(unit @t) callback=$-(@t @t)]

6++$ msg

7+ [%typed text=@t]

8+ %submit

9+ [%toggled id=@ud]

10+ [%got todos=(list item.todo)]

11+ [%acked err=(unit @t)]

12+

13+++ init |= ts=(list item.todo)

14+ [ts "" ~]

15+

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

17+ ?- msg

18+ [%typed t]

19+ ?- (gth (lent (tuba (trip t))) 80)

20+ %.y [m(draft=t error=`"Too long") ~]

21+ %.n [m(draft=t error=~) ~]

22+ %submit [m(draft="") ~[[%poke (todo-action.todo [%add draft.m]) |=%acked]]]

23+ [%toggled id] [m ~[[%poke (todo-action.todo [%toggle id]) |=%acked]]]

24+ [%got ts] [m(todos=ts) ~]

25+ [%acked err] [m(error=err) ~]

26+

27+++ subs |= m=model

28+ ~[[%watch (todos.todo |=%got)]]

29+

30+++ view |= m=model

31+ column ~[gap+%s2] ~[

32+ heading 2 "Todos"

33+ each (turn todos.m row-of)

34+ row ~[gap+%s1] ~[

35+ el ~[width+[%fill 1]] (field "New todo" draft.m |=%typed)

36+ button "Add" %submit

37+ el ~[tone+%danger] (text (fall error.m ""))

38+

39+++ row-of |= t=item.todo

40+ [id.t (toggle done.t text.t [%toggled id.t])]

tests/type-gate-free/todo-noun.txtnew file+40

@@ -0,0 +1,40 @@

1+/= todo /ui/api/todo

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

5++$ model [todos=(list item.todo) draft=@t error=(unit @t) opaque=*]

6++$ msg

7+ [%typed text=@t]

8+ %submit

9+ [%toggled id=@ud]

10+ [%got todos=(list item.todo)]

11+ [%acked err=(unit @t)]

12+

13+++ init |= ts=(list item.todo)

14+ [ts "" ~]

15+

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

17+ ?- msg

18+ [%typed t]

19+ ?- (gth (lent (tuba (trip t))) 80)

20+ %.y [m(draft=t error=`"Too long") ~]

21+ %.n [m(draft=t error=~) ~]

22+ %submit [m(draft="") ~[[%poke (todo-action.todo [%add draft.m]) |=%acked]]]

23+ [%toggled id] [m ~[[%poke (todo-action.todo [%toggle id]) |=%acked]]]

24+ [%got ts] [m(todos=ts) ~]

25+ [%acked err] [m(error=err) ~]

26+

27+++ subs |= m=model

28+ ~[[%watch (todos.todo |=%got)]]

29+

30+++ view |= m=model

31+ column ~[gap+%s2] ~[

32+ heading 2 "Todos"

33+ each (turn todos.m row-of)

34+ row ~[gap+%s1] ~[

35+ el ~[width+[%fill 1]] (field "New todo" draft.m |=%typed)

36+ button "Add" %submit

37+ el ~[tone+%danger] (text (fall error.m ""))

38+

39+++ row-of |= t=item.todo

40+ [id.t (toggle done.t text.t [%toggled id.t])]

tests/type-gate-free/todo.txtnew file+40

@@ -0,0 +1,40 @@

1+/= todo /ui/api/todo

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

5++$ model [todos=(list item.todo) draft=@t error=(unit @t)]

6++$ msg

7+ [%typed text=@t]

8+ %submit

9+ [%toggled id=@ud]

10+ [%got todos=(list item.todo)]

11+ [%acked err=(unit @t)]

12+

13+++ init |= ts=(list item.todo)

14+ [ts "" ~]

15+

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

17+ ?- msg

18+ [%typed t]

19+ ?- (gth (lent (tuba (trip t))) 80)

20+ %.y [m(draft=t error=`"Too long") ~]

21+ %.n [m(draft=t error=~) ~]

22+ %submit [m(draft="") ~[[%poke (todo-action.todo [%add draft.m]) |=%acked]]]

23+ [%toggled id] [m ~[[%poke (todo-action.todo [%toggle id]) |=%acked]]]

24+ [%got ts] [m(todos=ts) ~]

25+ [%acked err] [m(error=err) ~]

26+

27+++ subs |= m=model

28+ ~[[%watch (todos.todo |=%got)]]

29+

30+++ view |= m=model

31+ column ~[gap+%s2] ~[

32+ heading 2 "Todos"

33+ each (turn todos.m row-of)

34+ row ~[gap+%s1] ~[

35+ el ~[width+[%fill 1]] (field "New todo" draft.m |=%typed)

36+ button "Add" %submit

37+ el ~[tone+%danger] (text (fall error.m ""))

38+

39+++ row-of |= t=item.todo

40+ [id.t (toggle done.t text.t [%toggled id.t])]

tools/testdata/ship-selftest+3−1

@@ -315,7 +315,9 @@ def generator_checks(tmp):

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

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

317317 'tests/lib/jibb-sub-guards.hoon',

318− 'tests/lib/jibb-nested-union-guards.hoon'}

318+ 'tests/lib/jibb-nested-union-guards.hoon',

319+ 'tests/lib/jibb-gate-free-guards.hoon',

320+ 'tests/lib/jibb-gate-free-source.hoon'}

319321 <= normal_tests, sorted(normal_tests))

320322 for label, kwargs in (('custom library', {'lib': STUB}),

321323 ('custom goldens', {'golden': CASES}),

tools/type-gate-free-guards-testnew file+29

@@ -0,0 +1,29 @@

1+#!/usr/bin/env python3

2+"""Run the shared gate-free type guards under eval."""

3+from pathlib import Path

4+import argparse

5+import subprocess

6+import sys

7+import tempfile

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+tests = (root / 'tests/lib/jibb-gate-free-guards.hoon').read_text()

14+tests = tests[tests.index('\n|%\n') + 1:]

15+expression = ('=/ jibb .\n=/ suite\n' + tests +

16+ '\n=/ failures=(list tape) gate-free-guard-errors:suite\n^- @t\n' +

17+ "?~ failures 'gate-free guards passed'\n" +

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

19+with tempfile.TemporaryDirectory(prefix='jibb-gate-free-guards-') as tmp:

20+ program = Path(tmp) / 'guards.hoon'

21+ program.write_text(expression)

22+ result = subprocess.run([str(root / 'tools/hoon'), '--lib', args.lib,

23+ '--raw', '-f', str(program)], stdout=subprocess.PIPE)

24+if result.returncode:

25+ sys.exit(result.returncode)

26+if result.stdout != b'gate-free guards passed\n':

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

28+ sys.exit(1)

29+print('gate-free type guards passed')

tools/type-gate-free-source-testnew file+50

@@ -0,0 +1,50 @@

1+#!/usr/bin/env python3

2+"""Run real-reader gate-free mold analysis without claiming island checking."""

3+from pathlib import Path

4+import argparse

5+import subprocess

6+import sys

7+import tempfile

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

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

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

12+args = parser.parse_args()

13+fixture = root / 'tests/type-gate-free/todo.txt'

14+if fixture.read_bytes() != (root / 'my-app/ui/todo-list.jibb').read_bytes():

15+ sys.exit('todo source fixture differs from my-app/ui/todo-list.jibb')

16+reader = (root / 'jibb-dev/lib/jibb-import.hoon').read_text()

17+tests = (root / 'tests/lib/jibb-gate-free-source.hoon').read_text()

18+tests = tests[tests.index('\n|%\n') + 1:]

19+names = ('sur', 'action', 'todos', 'update', 'item', 'api', 'source',

20+ 'gate-source', 'noun-source', 'expected')

21+program = ('=/ jibb .\n=/ jibb-import\n' + reader + '\n' +

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

23+ for name in names) +

24+ '=/ suite\n' + tests +

25+ '\n^- @t\n(gate-free-source-report:suite prelude internal sur-text action-text todos-text update-text item-text api-text source-text gate-source-text noun-source-text)\n')

26+fixtures = {'sur': 'tests/type-api-paths/todo-sur.txt',

27+ 'action': 'tests/type-api-paths/todo-action.txt',

28+ 'todos': 'tests/type-api-paths/todos.txt',

29+ 'update': 'tests/type-api-paths/todo-update.txt',

30+ 'item': 'tests/type-api-paths/todo-item.txt',

31+ 'api': 'tests/type-api-paths/api.txt',

32+ 'source': 'tests/type-gate-free/todo.txt',

33+ 'gate-source': 'tests/type-gate-free/todo-gate.txt',

34+ 'noun-source': 'tests/type-gate-free/todo-noun.txt',

35+ 'expected': 'tests/type-gate-free/expected.txt'}

36+with tempfile.TemporaryDirectory(prefix='jibb-gate-free-source-') as tmp:

37+ path = Path(tmp) / 'source.hoon'

38+ path.write_text(program)

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

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

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

42+ for name, filename in fixtures.items():

43+ command += ['--cord', name + '-text=' + str(root / filename)]

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

45+if result.returncode:

46+ sys.exit(result.returncode)

47+if result.stdout != (root / 'tests/type-gate-free/expected.txt').read_bytes():

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

49+ sys.exit('gate-free source report differs from expected')

50+print('real todo gate-free mold analysis passed')