UIP-0122.md

uip	title	description	author	status	type	category	created
0122	%wild: Stateless jet registration	Propose a new system for deriving jet registrations and hinting which requires no stored state in the interpreter.	~ritpub-sipsyl (@eamsden)	Draft	Standards Track	Hoon, Nock	2024-03-25

Abstract

This proposal introduces a stateless approach to jet registration in Nock interpreters, utilizing a dynamic hint labeled %wild. The %wild hint directly contains the necessary slice of "cold state" (labels for nested core batteries) for the hinted Nock, thereby avoiding issues with state maintenance and preservation. This approach offers a simple solution to the problems of state in jet registration.

The %wild hint can be composed by Hoon and can be implemented using existing information in the subject type, extended only by labels from existing %fast-hint runes. It also provides a scoping mechanism which prevents user code from altering kernel code registrations.

An additional advantage of this approach is its potential to fix the jet mismatch of +mink, without requiring any injection of state. Presently, the jet for +mink will not return stack traces from jetted Nock, though the hoon implementation specifies returning all stack traces without regard to jets.

Motivation

Currently Vere and Ares both handle jet registrations provided by %fast hints. By convention and implementation, a %fast hint wraps the production of a core, and registers that core's battery (axis 2) along with a registered hierarchy of already-registered batteries which match a parent core, whose axis in the newly-registered core is given in the hint. The label provided in a %fast hint is appended onto the labels of the parent cores, producing a $path for each core registered. This allows us to recognize cores as having a particular label. This ability is fundamental to practical jetting systems.

To correctly implement core labeling with %fast hints, an interpreter must maintain state. The state directly assembled from %fast hints is conventionally referred to as the "cold" state (contrasted with the "hot" state which is shipped with the interpreter binary and maps labels to jets, or the "warm" state, the ephemeral join between hot and cold state).

(For a more thorough treatment of the current core-labeling and jetting system see "Fast Hints and Jets").

Cold state is accumulated throughout the lifetime of the pier: once the %fast hint wrapping the introduction of a core is evaluated, it is gone and cannot, in general, be recovered. Therefore, in general, there is no safe way for the interpreter to recognize that registrations can be deleted. The technical term for such a design is a memory leak. (Thank you to ~fodwyt-ragful for this insight.)

Further, it is not, in general, possible to assume the inter-pier portability of core-based state machines (Arvo, Ares codegen, Gall agents, etc). The only way in which this is possible at all is to provide the introduction forms (usually typed as (trap vase) in Hoon) which will run the fast hints in the target pier.

The practical implications of the above are that cold state is stored in non-noun structures on the loom. There is no guarantee of that these structures can be located or reused when migrating a pier between interpreters (e.g. Vere & Ares). Therefore, the cold state cannot be migrated without either interpreter-specific pier migration functions, or special introduction forms to re-run the %fast hints and regenerate cold state. The useless existing cold state may be permanently stuck in the loom as a memory leak.

A simpler, stateless approach is to embrace the referential transparency of a declarative approach and simply state the necessary registrations when running Nock. Being able to do so would avoid the necessity of the interpreter to maintain state and ship introduction forms between piers. (Interpreters may cache registrations and relations derived from them, but this is not necessary for feasibility.)

Specification

Nock interpreters SHOULD respect a dynamic hint labeled %wild, whose clue molds to the $wilt structure as defined below.

|%
+$  cape  $@(? [cape cape])    ::  noun mask; & means known, | unknown
+$  sock  [=cape data=*]       ::  core with mask; only & values need to match
+$  wilt  (list [l=* s=sock])  ::  list of labeled masked cores
--

l SHOULD be interpreted as a core label. Although l will in practice be a $path (as it is now), we make no assumptions about what it is; it can be anything that allows us to match known cores from inside a hint.

The template s SHOULD be interpreted as a noun template to be matched as follows:

• If the cape is & then data is compared to the core and a match is returned if equal.
• If the cape is | then any noun matches the sock.
• If the cape is a cell, then matching is performed recursively
• If the cape of a sock is a cell but data is an atom, then the registration MUST be discarded for an invalid sock.

The list SHOULD be interpreted as the entire set of registered cores for the enclosed Nock. A Nock interpreter will, at each callsite, check if there is a label for the core to be fired. Semantically, each $sock in the list of registrations is checked for a match against the subject (which in Hoon-emitted code is a core). If a matching sock is found, then the label and formula are checked against the interpreter's "hot state" (a mapping from labels and formulas to actual jets) and the jet is invoked in place of direct evaluation of the Nock.

If a match is returned, the interpreter SHOULD treat the matched core as having the given label (l) for purposes of jetting and profiling (this label can be used for anything, but these are the typical uses).

The registrations given in the clue SHOULD only be applied within the hinted Nock. The clue formula MUST be a Nock 1 (constant).

Rationale

The %wild hint contains exactly the same information as the cold state, but takes the simple step of including the necessary slice of "cold state" in the Nock to be executed.. It directly hints the computation to be performed, rather than hinting the production forms of Nock we want hinted everywhere. This trivially sidesteps all of the problems of state, both in the care required to initialize mutable state by side effects of supposedly immutable programs, and the necessity of indefinitely preserving that state. Notably, these slices of "cold state" are also scoped, unlike %fast hints, thus leading to trivially safe userspace jets.

In order to construct the %wild hint, we propose to use the ~% (and ~/) Hoon runes both to produce %fast hints (for backwards compatibility), but also to add labels to core types. This allows us to use all existing Hoon-level core labels without modification.

A separate rune (~. is proposed) can extract core labels from the type of an axis of the subject and only needs to be wrapped around outer entry points (e.g. the outer arms of Arvo.) This composes the %wild hint from the Hoon type of the given axis of the subject.

Thus, no relabeling of cores is necessary, the only Hoon level change is the addition of a simple rune wrapping a fixed number of entry points to Arvo. Hoon can compose the %wild hint's clue entirely from information tracked in the subject type.

Example

Consider the following jetted standard library (vial.hoon)

=>  ~
~%  %vial.100  %vial  ~
~%  %one  +  ~
|%
++  dec
  ~/  %dec
  |=  a=@
  ?<  =(a 0)
  =|  b=@
  |-  ^-  @
  ?:  =(a +(b))  b
  $(b +(b))
--

The %fast hints on lines 1, 2, and 4 are compiled into Nock, but also result in labels in the Hoon type. For the +dec gate, the core is labeled /dec/one/vial.100.

Now consider the following trivial lifecycle door (life.hoon):

/+  vial
=>  vial
|_  many=@
++  this  .
++  peek
  |=  pax=*
  ?>  =(pax /how/<many>)
  many
++  poke
  |=  up=?
  ~.  +7..
  ^-  _this
  ?:  up  this(many +(many))
  this(many (dec many))
--

In this example, the ~. rune would compile to a %wild hint with three elements:

• [l=/vial.100 s=[& %vial]]
• [l=/one/vial.100 s=[[& &] [<one battery> %vial]]
• [l=/dec/one/vial.100 s=[[& | & &] <dec battery> ~ <one battery> %vial]

(In practice the capes would be normalized by rewriting [& &] to &, however here we leave them denormalized for ease of following the example.)

For the entire scope of the ~. rune, a conforming interpreter would use this as the set of registered cores in order to match jets or produce traces. The list is extracted labels from the type of the first subhoon: +7.. and (recursively) the result types of any arms of any cores in the type.

Bonus: fix +mink jet mismatch

There is a long-standing jet mismatch in +mink, stemming from the functionality that +mink returns stack traces for failed Nock computations. Any code run through +mink will obviously produce a shorter stack trace if it contains jetted code, as the jetted code will avoid many of the sub-calls to other Hoon functions. Normally, this wouldn't be an issue, since stack traces are a side-effect for user convenience. However, since +mink makes the stack trace a part of its return value, the exists a jet mismatch for +mink.

A further advantage to the %wild hint, as pointed out by ~master-morzod, is that type-level availability of core labels could be used to fix this jet mismatch in an ergonomic way. If the sample of +mink is extended to contain jet registrations (in the same $wilt mold), its semantics can be fixed to never produce a stack trace underneath a labeled core. The jet for +mink can load the supplied $wilt as its local jet registrations, and the interpreter can likewise refuse to produce stack traces under labeled cores, even if they are in fact unjetted. Of course +mink should also explicitly handle the %wild hint.

A vase-mode wrapper around +mink can then extract the necessary registrations from the type carried by the vase, using the same algorithm as for compiling ~., but at runtime. The extraction would almost certainly need to be persistently memoized for reasonable performance.

Backwards Compatibility

Interpreters are free to ignore %wild hints and use existing jet registration implementations, such as cold state derived from %fast hints. One bonus is that the changes to the type system will allow %fast hints with bad parent indexes to be validated at compile time. However, the extant +mink jet mismatch will remain.

Reference Implementation

A full reference implementation is not offered, as it would entail changes to the hoon compiler and both runtimes. However, the added case required in the type $type of Hoon types and an overview of its introduction and elimination follow.

The type $type of Hoon types is extended with one case:

[%wilt p=path q=@ r=type].

It is introduced by the ~% rune (to which ~/ reduces). When typing ~% p q r s (where h contains the AST children)

• Type s, call it ts and verify that it types to %core. Otherwise fail.
• Mint q:s, call its tqs and verify that it types to %wilt. Otherwise fail. Call its nock nqs and verify that it is [1 0] or [0 <axis>]. Otherwise fail.
• Produce the result type as follows: [%wild [p.h p.tqs] +.nqs ts].

This both records the labeled core hierarchy in the type, and simultaneously checks the consistency of ~% core labeling as part of Hoon typechecking.

TBW: extract core labels by traversing type, producing socks for cores, and recursively minting arms of cores.

TBW: should the $wilt of a nested %wild hint concatenate onto or replace the $wilt of the other %wild hint?

Security Considerations

Jet registration obviously implicates security. There is an obvious improvement in the current proposal over stateful jet registration in that an obvious scoping mechanism exists, and that user code has no possible mechanism to to alter registrations for kernel code.

Copyright

Copyright and related rights waived via CC0.