Urbit is a machine for writing and evaluating Nock code. Much of the characteristic nature of Hoon derives directly from the affordances of Nock. Perhaps the most fundamental design decision undergirding Nock is that Nock orients the world around binary trees rather than linear arrays.
Nock 4KA noun is an atom or a cell. An atom is a natural number. A cell is an ordered pair of nouns.Reduce by the first matching pattern; variables match any noun.nock(a) *a[a b c] [a [b c]]?[a b] 0?a 1+[a b] +[a b]+a 1 + a=[a a] 0=[a b] 1/[1 a] a/[2 a b] a/[3 a b] b/[(a + a) b] /[2 /[a b]]/[(a + a + 1) b] /[3 /[a b]]/a /a#[1 a b] a#[(a + a) b c] #[a [b /[(a + a + 1) c]] c]#[(a + a + 1) b c] #[a [/[(a + a) c] b] c]#a #a*[a [b c] d] [*[a b c] *[a d]]*[a 0 b] /[b a]*[a 1 b] b*[a 2 b c] *[*[a b] *[a c]]*[a 3 b] ?*[a b]*[a 4 b] +*[a b]*[a 5 b c] =[*[a b] *[a c]]*[a 6 b c d] *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]*[a 7 b c] *[*[a b] c]*[a 8 b c] *[[*[a b] a] c]*[a 9 b c] *[*[a c] 2 [0 1] 0 b]*[a 10 [b c] d] #[b *[a c] *[a d]]*[a 11 [b c] d] *[[*[a c] *[a d]] 0 3]*[a 11 b c] *[a c]*a *a
(To avoid confusion in Nock versions versus Nock rules, this lesson will refer to Nock rules with a written number, e.g. “Nock Four” refers to *[a 4 b]
rather than to Nock 4K.)
Many aspects of Hoon's nature and Urbit's operating model are natural consequences of Nock's structure and preferences. Hoon acts as a sort of (very glorified) macro assembler over Nock, providing runes and idioms for Nock patterns and a type system which reduces to Nock. However, it is possible to do things in pure Nock which Hoon restricts; this is one motivation for vase mode.
In this lesson, we will begin our study of the Urbit kernel by looking at the wellsprings of Urbit. Nock has evolved substantially; the earliest public record is Nock 13K. However, as of Nock 4K no further revisions are expected to be necessary and the system is very cold.
For clarity, this document will refer to rules with written-out numbers (Nock Four) and versions with Arabic digits (Nock 4K). It will also prefer the shorthand s
for subject (instead of a
) and f
, g
, etc. for formula (instead of b
, c
, etc.).
The Nock Preface
The Nock specification needs to lay some interpretive ground before the rules can be defined. These definitions allow us to settle on an unambiguous interpretation of the rules. Importantly, most of the syntax defined here is unique to Nock and does not bear the same meaning in Hoon, with the exception of [
sel and ]
ser as bounding cells.
nock(a) *a[a b c] [a [b c]]?[a b] 0?a 1+[a b] +[a b]+a 1 + a=[a a] 0=[a b] 1/[1 a] a/[2 a b] a/[3 a b] b/[(a + a) b] /[2 /[a b]]/[(a + a + 1) b] /[3 /[a b]]/a /a#[1 a b] a#[(a + a) b c] #[a [b /[(a + a + 1) c]] c]#[(a + a + 1) b c] #[a [/[(a + a) c] b] c]#a #a*[a [b c] d] [*[a b c] *[a d]]
Evaluation and Structure
nock(a)
→ *a
Nock is an evaluated language, and we write the evaluation of this function as *
. *
represents an attempt to systematically apply the rules of Nock in an inside-out fashion to the given noun. *
runs on a valid [argument function]
pair; i.e. the function
is the formula
and the argument
is the subject
.
It is perhaps an oddity of *
that it “spins forever” instead of merely returning the noun on evaluation.
[a b c]
→ [a [b c]]
For convenience, the pretty-printer elides rightward-branching tuples.
?[a b]
→ 0
?a
→ 1
This represents the ability to tell a cell from an atom. At this point in the preface we actually don't know yet if 0
is TRUE
or FALSE
, merely that they are distinct.
+[a b]
→ +[a b]
+a
→ 1 + a
The increment operation is not distributed across cell entries. (However, note that if *
evaluation leads to the operated-upon cell reducing to an atom then this will proceed.)
=[a a]
→ 0
=[a b]
→ 1
Now we can compare equality with the =
operator that accepts a cell. (No specification of behavior applied to an atom is made here, but Nock is presumptively crash-only.)
/[1 a]
→ a
/[2 a b]
→ /[2 [a b]]
→ a
/[3 a b]
→ /[3 [a b]]
→ b
These three statements define the basic approach to binary tree addressing: namely that there is a root of the tree at 1
, a head at 2
, and a tail at 3
.
/[(a + a) b]
→ /[2 /[a b]]
/[(a + a + 1) b]
→ /[3 /[a b]]
So what do these do? These define the subsequent layers of the tree recursively. Thus the head (2
) of the cell at a
has the address 2×a
, and the tail (3
) of the cell at a
has the address 2×a
+1.
#[1 a b]
→ a
#[(a + a) b c]
→ #[a [b /[(a + a + 1) c]] c]
#[(a + a + 1) b c]
→ #[a [/[(a + a) c] b] c]
These statements define what it means to replace part of one noun with another noun. “Replace addresss x
of z
with y
.” They require a similar sort of tree definition to the slot addressing.
The last definition, distribution, is reserved for later discussion.
The Simple Rules: Nock Zero to Five
Nock is separated into simple rules which span its Turing-complete expressibility and compound rules which give it more terseness. The simple Nock rules span Nock Zero to Nock Five:
*[a 0 b] /[b a]*[a 1 b] b*[a 2 b c] *[*[a b] *[a c]]*[a 3 b] ?*[a b]*[a 4 b] +*[a b]*[a 5 b c] =[*[a b] *[a c]]
A good entry point to the study of these basic Nock rules can be made through their Hoon equivalents. Hoon directly exposes several Nock rules as the .
dot runes.
Nock Rule | Nock Expression | Hoon Equivalent | Comment |
---|---|---|---|
Nock Zero | /[b a] | (some wings) | Address at slot |
Nock One | b | (any data) | Constant |
Nock Two | *[*[a b] *[a c]] | .* dottar | Evaluate |
Nock Three | ?*[a b] | .? dotwut | Distinguish cell from atom |
Nock Four | +*[a b] | .+ dotlus | Increment |
Nock Five | =[*[a b] *[a c]] | .= dottis | Test for equality |
The following paragraphs summarize the reference explanation for these Nock rules. Two runes and one gate will be particularly useful as we analyze Nock:
- We will evaluate Nock statements in Hoon using
.*
dottar or Nock Two. - We can produce the Nock equivalent of a Hoon statement using
!=
zaptis, which takes a singlehoon
for its sample. - We can run a virtualized Nock (with crash data) in
++mock
. An optional hint handler can be supplied but we will typically ignore it.
Nock Zero: Slot
[s 0 f]
→ /[f s]
Nock Zero locates a noun at address f
in subject s
.
./ \/ \/ \. ./ \ / \1 2 3 4[[1 2] [3 4]]> .*([[1 2] [3 4]] [0 2])[1 2]> .*([[1 2] [3 4]] [0 4])1> .*([[1 2] [3 4]] [0 8])dojo: hoon expression failed> (mock [[[1 2] [3 4]] 0 7] ,~)[%0 p=4]> (mock [[[1 2] [3 4]] 0 8] ,~)[%2 p=~]
- Lark notation
- Wing search path
- more on these in
csl02
It is common to see [… 0 6]
in Nock expressions generated from Hoon. What is at address 6 that we'd like to grab?
..arm
is a Nock Zero lookup, for instance.
> !=(..add)[0 2.047]
One of the perennial controversies around Nock has arisen from Nock Zero's binary tree nature. From a processor standpoint, arbitrary data lookup does not take advantage of cache behavior. However, Nock bytecode and subject knowledge analysis (SKA) both work to mitigate this situation.
Nock One: Constant
*[s 1 f]
→ f
Nock One simply yields its formula as a noun.
For instance, a numeric value in Nock can refer to a rule, a slot address, or a numeric value. Nock One would clarify that we intend the latter, a numeric constant.
./ \/ \/ \. ./ \ / \1 2 3 4[[1 2] [3 4]]> .*([[1 2] [3 4]] [1 7])7> .*([[1 2] [3 4]] [1 [7 8 9]])[7 8 9]
Nock Two: Evaluate
*[s 2 f g]
→ *[*[s f] *[s g]]
Nock Two effectively modifies the subject against which a second formula is evaluated. Run formula f
against subject s
to yield noun sf
. Run formula g
against subject s
to yield noun sg
. Run formula sg
against subject sf
.
Nock Two is useful when constructing a formula explicitly, but most of the time you are actually just fetching a formula from your context instead—thus Nock Nine, when we arrive to it. (Thus we seem to use bare Nock Two in practice less frequently than one may at first expect.)
For now, let's build a simple example using only rules Zero and One.
./ \1 2[1 2]> .*([1 2] [2 [0 2] [1 [0 1]]])1
- First, the formula
.*([1 2] [0 2])
yields the single atom1
. - Then the second formula
.*([1 2] [1 [0 1]])
results in[0 1]
. - Finally the formula
.*(1 [0 1])
yields1
.
You can think of Nock Two as a way of storing a subprocedure in a subject, then accessing it for evaluation.
Nock Three: Distinguish
*[s 3 f]
→ ?*[s f]
Does the formula as applied to the subject resolve to a cell?
> .*([[1 2] [3 4]] [3 0 1])0> .*([[1 2] [3 4]] [3 0 4])1
I.e., is the noun at slot 1 a cell? (Yes.) Is the noun at slot 4 a cell? (No.)
Nock Four: Increment
*[s 4 f]
→ +*[s f]
Increment the value. This is the only arithmetic operation.
> .*(5 [4 0 1])6
Note that typically Nock Four is paired with a constant lookup for the formula. You could construct other patterns by hand; what is this doing?
> (mock [5 4 3 0 1] ,~)[%0 p=2]
Nock Five: Equality
*[s 5 f g]
→ =[*[s f] *[s g]]
Are the two nouns, as resolved against the subject, identical? (Compare the result in Nock, not Hoon.) This refers to the structure of the noun, which gives you insight into its behavior in Hoon.
> .*([[1 2] [1 2]] [5 [0 2] [0 3]])0> .*([[1 2] [3 4]] [5 [0 2] [0 3]])1> .*([[1 2] [3 4]] [5 [0 5] [4 0 4]])0
Distribution
*[s [f g] h]
→ [*[s f g] *[s h]]
While not a Nock rule per se, the distributive behavior of Nock (“implicit cons”) requires some attention before we examine the compound rules.
Formulas have a number corresponding to a Nock rule at their head. However, you can also put a cell at the head of a formula. What does this mean?
> .*([[1 2] [3 4]] [[0 3] [4 0 5]])[[3 4] 3]
It means that each entry is itself a formula. So what this means is that [0 3]
resolves against [[1 2] [3 4]]
and [4 0 5]
resolves against [[1 2] [3 4]]
before they together yield a cell of the results [[3 4] 3]
.
In general, we can string many formulas together in a cell to resolve them all sequentially against the same subject.
The Compound Rules: Nock Six to Eleven
Nock Rule | Nock Expression | Hoon Equivalent | Comment |
---|---|---|---|
Nock Six | *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]] | ?: wutcol | Conditional branch |
Nock Seven | *[*[a b] c] | => tisgar | Compose |
Nock Eight | *[[*[a b] a] c] | =+ tislus | Extend |
Nock Nine | *[*[a c] 2 [0 1] 0 b] | Invoke | |
Nock Ten | #[b *[a c] *[a d]] | %= centtis | Replace at address |
Nock Eleven | *[[*[a c] *[a d]] 0 3] , *[a c] | ~ sig runes | Hint |
Nock Six: Conditional Branch
*[s 6 f g h]
→ *[s *[[g h] 0 *[[2 3] 0 *[s 4 4 f]]]]
This expression is straightforward to understand, but the logic of its structure is interesting to follow through. What is being said? If formula f
evaluated against the subject s
evaluates TRUE
(0
), then the result of g
evaluated against the subject is produced. If it evaluates to FALSE
(1
), then the result of h
evaluated against the subject is produced. Otherwise, crash.
- First, at right we evaluate
*[s 4 4 f]
. This means evaluatef
againsts
then increment it twice. This selects either0+2
=2
or1+2
=3
. These are slot addresses into Rule Zero immediately before this expression. [2 3]
is the lookup subject for the0
. Why? This enforces that we have2
(0
) or3
(1
), not any other possible answer fromf
.- Now we use that
2
or3
as a Rule Zero slot address intog
orh
.
The funkiness of the equation is because we have to make sure that the result is 0
or 1
; we must crash on another value or on a cell. The docs demonstrate a simpler version of Nock Six.
- How would you write
?.
wutdot? - How would you write
?~
wutsig? - What do
?^
wutket and?@
wutpat expand to? (Nock Six of Nock Three)
Nock Seven: Compose
*[s 7 f g]
→ *[*[s f] g]
Composition describes the evaluation of one formula against the subject, then using that result as the subject of the next formula.
:: With the subject set to a cell of our and now, return the head.> != => [our now] -[7 [[0 12] 0 26] 0 2]
(Incidentally, although we'll get to this later in ca02
, what are our
and now
?)
Nock Eight: Extend
*[s 8 f g]
→ *[[*[s f] s] g]
Nock Eight allows you to pin a value into the subject. It is very similar to Nock Seven.
The runes =+
tislus, =-
tishep, =/
tisfas, =;
tismic, and =|
tisbar are all instances of Nock Eight. You can use the runes like =+
and =-
with immediate use of -
to refer to the value just added to the subject are Nock Eight followed by Nock Zero.
> =+ 5-5> !=(=+(5 -))[8 [1 5] 0 2]
Faces are not even necessary in Hoon—you can refer to a value using lark notation -
after it has been defined. +>
frequently refers to a helper core in Gall, for instance. (While lark notation is often unsatisfactory, it can be more expressive in simple relational statements like these.)
Nock Nine: Invoke
*[s 9 a f]
→ *[*[s f] 2 [0 1] 0 a]
The underlying rationale for Nock Nine is to invoke a closure or compute over an association of code and data. This is used throughout Urbit in invocation—think gate-building gates, on which more in ca01
. In plain language, produce a noun containing code and data (a core) by evaluating formula g
against the subject s
and then evaluate the formula in it at slot a
.
An arm in any core is accessed through a Nock Nine. For instance, here we have a call to ++dec
, the decrement gate.
> !=((dec 1))[8 [9 2.398 0 2.047] 9 2 10 [6 7 [0 3] 1 1] 0 2]
Compare the actual Hoon:
++ dec~/ %dec:: unsigned decrement by one.|= a=@~_ leaf+"decrement-underflow"?< =(0 a)=+ b=0:: decremented integer|- ^- @?: =(a +(b)) b$(b +(b))
What's actually being said here? What we see in ++dec
that we don't see in the Nock is a Nock Four increment operator. That's a hint that the Nock code resulting from (dec 1)
isn't the equivalent of the gate at all. Check the battery of ++dec
to verify this (it's quite long).
No, something else is going on with this function invocation with Nock Nine. Based on what we've seen so far of the Nock rules:
- The subject of the outer Nock Nine call is
[8 [9 2.398 0 2.047]]
. The subject is extended using Nock Eight by retrieving the axis at constant2.047
within the current subject, then grabbing the noun at slot2.398
within that noun.- Extend the namespace with the lookup of the
battery
of the core at+2047
in the subject. ([9 2 …
is a very common idiom in Nock, resulting from invoking the battery of a core, but here it's not at2
it's more complexly buried in the subject tree.)
- Extend the namespace with the lookup of the
- The formula is
[2 10 [6 7 [0 3] 1 1] 0 2]
.- Use the battery of that (second Nock Nine) as the subject for evaluating an
if
-else
Nock Six. - That has a constant
1
fired inside of a lookup of the+3
(payload
) via Nock Seven (which is the sample). - Finally the slot
2
is accessed which refers to the battery in the subject as received at this point.
- Use the battery of that (second Nock Nine) as the subject for evaluating an
In general, watch for [0 2]
to grab the battery and [0 3]
to grab the payload.
There's another way around this, which will also be illuminating: build it from the ground up.
[8 [1 0] 8 [1 6 [5 [0 7] 4 0 6] [0 6] 9 2 [0 2] [4 0 6] 0 7] 9 2 0 1]
- Why do these look different from each other? The first one is locating a battery somewhere else in the subject and pulling it in. The second is explicitly constructing the operation in Nock and invoking it at the same point.
In another example, see what happens with (add 2 2)
in Nock:
> !=((add 2 2))[8 [9 36 0 2.047] 9 2 10 [6 [7 [0 3] 1 2] 7 [0 3] 1 2] 0 2]
Two Nock Nines again, one to retrieve the battery
of ++add
and another to invoke it.
The core nature of Hoon fits hand-in-glove with Nock Nine. ++arm
is always an arm, and a wing that references it directly always performs a Nock Nine for the lookup.
(In the Vere runtime, Nock Nine corresponds to u3v_poke
, in which a fun
gets a gate
to evaluate. More in ca05
.)
Nock Ten: Replace at Address
*[s 10 [f g] h]
→ #[f *[s g] *[s h]]
%-
centtis resolves to Nock Nine of Nock Ten: it uses Nock Ten to replace the sample of a core, then runs Nock Nine to fire the arm at axis 2.
> != %- add [3 4][8 [9 36 0 2.047] 9 2 10 [6 7 [0 3] 1 3 4] 0 2]
Nock Eleven: Hint
*[s 11 [f g] h]
→ *[[*[s g] *[s h]] 0 3]
*[s 11 f g]
→ *[s g]
The fundamental idea of a hint is that it can provide an arbitrary annotation for a computation without changing the result. In practice, this is used to signal to the runtime that it should do something operationally which Nock doesn't know about.
The first kind of hint is called a dynamic hint. The head of the cell is discarded and the tail is calculated against the current subject, then thrown away. (What is an example of this in practice? ~&
sigpam.) Put another way: the value in a computation is available to the runtime to use as a message.
> !=(~&('hello' ~))[ 11[ 1.735.355.507[1 0]8[9 2.558 0 127]9210[ 67[0 3]8[9 158 0 127]9210[6 7 [0 3] 1 [1.836.020.833 116 0] 478.560.413.032]02]02]10]
which in Pseudo-Hoon is:
> !=(~&('hello' ~))[ 11[ %slog ~8[9 2.558 %127][9 2 10[ 67%38[9 158 %127][9 2 10[6 7 %3 [%atom 't' ~] 'hello'] %2]]]%2]~]
The second kind of hint is a static hint and is simply directly specified. The runtime may pick this up, and if it is a registered hint then it may trigger an appropriate side effect. Put otherwise: the value is passed as a key to a hashmap in the interpreter which can do what it needs, then discard the value.
> !=(~>(%bout ~))[11 1.953.853.282 1 0]
Practical Hints
The most fundamental way to send a hint to the runtime is to simply ~>
siggar a raw hint tag with data. For instance, this is used in the update sequence to %slog
(printf
) a formatted text block. (Note that raw hints use a special .
dot notation.)
~>(%slog.0^leaf/"clay: rebuilding {<syd>} after kernel update" .)
There are a number of ways of signaling a Nock Eleven hint to the runtime. Several have dedicated runes in the ~
sig family, but all of these convenience runes do ultimately unwrap to raw hints and we'll examine them that way. ~>
siggar lets you directly specify a raw hint. Some of these are not in active use; the important ones for you to know at this point have been marked with a *
.
*
%bout
is used to time calculations.*
%fast
corresponds to jet hinting with~%
sigcen and~/
sigfas. (See also ~rivpyl-sidfyl's notes.)%germ
is marked as unused innock.c
but corresponds to~=
sigtis noun duplicate testing.%hand
is mentioned but it's unclear what it does.%hela
is used to unify%slog
traces from all roads. (See the runtime lessons for details on the road.)%hunk
tracks a failed scry in a stack trace.%live
corresponds to~$
sigbuc profiling hit counter.%lose
tracks elided frames in a stack trace.*
%mean
corresponds to~|
sigbar and~_
sigcab debug printing.%meme
prints memory usage.%memo
corresponds to~+
siglus caching.%nara
is used to%slog
the deepest road's trace. (See the runtime lessons for details on the road.)*
%slog
prints a value directly, and corresponds to~&
sigpam and~|
sigzap debug printing .%sole
is superseded, but was for global deduplication.%spot
drives stack traces.%xray
prints bytecode.Enumerate the raw hints used with
~>
siggar. Provide an example of each.
> !=(~>(%slog [0 leaf/"ride: parsing"]))[ 111.735.355.507[1 0][1 1.717.658.988]7[0 1]8[1 1 114 105 100 101 58 32 112 97 114 115 105 110 103 0]9201]
> => 42 ~> %memo.[42] ~> %slog.[3 '42'] 4242> => 42 ~> %memo.[42] ~> %slog.[3 '42'] 4242
- ~timluc-miptev, “The Rest of Nock and Some Real-World Code”↗
- ~timluc-miptev, “Interlude: Some Loose Ends and FAQ”↗
Jet-Accelerated Code
One “problem” with Nock is that although it's formally correct and Turing complete, that doesn't mean that it's computationally efficient for every scenario. How can we solve the problem correctly but quickly in a situation for which this calculation is a bottleneck? We treat the Nock code as a specification of behavior rather than an assertion of method. Jet-accelerated code ("jets" for short) solves our speed problem by allowing the programmer to specify an equivalent algorithm which may (should) be much more efficient than the pure Nock version.
(This is analogous to C's use of the #pragma
preprocessor command to specify to its compiler how to treat certain code.))
We mark certain blocks of code with hints, which suggest to the runtime (Nock interpreter) that an equivalent algorithm may exist in the runtime and that the jet dashboard should be checked for a comparable registration. Such jet dispatch then runs the equivalent fast code and supplies the resulting noun back to the compiled Nock code as if it arisen directly from the Hoon expression. (The jet dashboard handles jet state in the runtime. We don't need to delve into it to understand jet dispatch now, but see the appendix for more details.)
Jets are hashed and checked before they are compiled, and there is an option to run both the Nock and jet and check that they match. One consequence of jetted code is that you can theoretically have a jet mismatch, wherein the jet produces different code than the Hoon expression. This is considered grounds for removing a jet from the runtime since it destroys the deterministic reproducibility of Urbit state.
Today, jets are compiled and linked directly into the Urbit runtime. They are only supplied for code in /sys
. There is not a technical reason for this—any core can be jetted—but it is currently a code hygiene practice to keep things manageable and secure.
- “Writing Jets”
- ~rovnys-ricfer, ~lagrev-nocfep, “Dev-Week: Core School Preview”↗
- ~ritpub-sipsyl, “Notes on Jets”↗
The Fake Rule: Nock Twelve
Nock Rule | Nock Expression | Hoon Equivalent | Comment |
---|---|---|---|
Nock Twelve | *[a 12 b] | .^ dotket | Scry in namespace |
A scry is a pure function mapping from a path to a response. A scry is a referentially transparent way of referring to data. A .^
dotket scry resolves via an artificial Nock instruction, Nock Twelve. De facto, we are attempting to solve the problem that sometimes information is necessary to complete a calculation which may not be present in the subject. The 12
instruction is picked up by the virtual Nock implementation within Arvo and the appropriate value inserted. The scry pattern is read-only and synchronous.
While a scry request does violate function purity, it is reproducible due to the scry namespace, in which immutable values are bound by convention at fixed endpoints. The scry namespace is defined by a unique path for each resource.
/~zod/1/2/c/x/~2023.8.31..12.00.00..0000/base/sys/arvo/hoon/host/rift/life/vane/request-type/revision-number/desk/file-path/mark
When in userspace, we work with a stripped-down version of the full scry namespace, which is supplied by Arvo. Thus scries are a bit mangled in userspace.
The scry interface defined by Arvo and each vane is not intrinsic to the runtime, but is an OS-level convention. (The values eny
and now
are not scries, but atoms provided by Arvo—and thither dynamically by the runtime from the system. More on these in ca02
.)
For instance, consider a namespace scry into Clay:
> !=(.^(* %cx /===/gen/cat/hoon))[ 12[1 139 1.853.189.998]130.8191.685.027.4541.702.060.386161.311.343.539.592.098.933.172.536.971.821.663.896.217.238.133.980.260.425.806.4627.234.9197.627.1071.852.796.7760]
Refactored back into Hoon atoms, we can see:
[ 12[1 139 %noun]1%cx~.~zod~.base~.~2023.7.31..20.39.12..1abd~.gen~.cat~.hoon~]
Virtualized Nock (++mock
)
How does scrying actually work? Hoon can run both Nock and Hoon within itself, and in particular has Nock Twelve implemented in the ++mink
emulator. (++mink
underlies ++mock
, which we've been using.) ++mink
takes a subject and a formula like any Nock interpreter, and also a gate called any time a formula contains Nock Twelve at its head. Userspace code such as Gall agents is run using ++mink
and thus has the ability to fill out nouns using calls into Arvo to construct its nouns.
++mock
and friends work by coordinating with the runtime to virtualize Nock:
With the power of
u3
, we nest arbitrary layers ofmock
without any particular performance cost. Moreover, we simply treat Nock proper as a special case ofmock
. (More precisely, the internal VM loop is++mink
and the error compiler is++mook
. But we call the whole sandbox systemmock
.) The nice thing aboutmock
functions is that (by executing withinu3m_soft_run()
, which as you may recall uses a nested road) they provide both exceptions and the namespace operator -.^
in Hoon, which becomes operator11
inmock
.
For instance, we have been running .*
dottar at the Dojo prompt. In fact, this does produce Nock code—but then that Nock code is evaluated by whatever the interpreter is at that level. In userspace, this is ++mock
; in kernelspace, the runtime evaluates the Nock code directly (not a metacircular interpreter). (What consequence does this have for scries?)
This works in userspace because of the metacircular interpreter, but would not work in kernelspace:
> ;;(@t .*(. !=(.^(* %cx /===/gen/cat/hoon))))':: ConCATenate file listings\0a\0a::\0a:::: /hoon/cat/gen\0a ::\0a/? 310\0a/+ pretty-file, show-dir\0a::\0a::::\0a ::\0a:- %say\0a|= [^ [arg=(listpath)] vane=?(%g %c)]\0a=- tang+(flop `tang`(zing -))\0a%+ turn arg\0a|= pax=path\0a^- tang\0a=+ ark=.^(arch (cat 3 vane %y) pax)\0a?^ fil.ark\0a ?: =(%sched -:(flop pax))\0a [>.^((map @da cord) (cat 3 vane %x) pax)<]~\0a [leaf+(spud pax) (pretty-file .^(noun (cat 3 vane %x) pax))]\0a?- dir.ark:: handle ambiguity\0a ~\0a [rose+[" " `~]^~[leaf+"~" (smyt pax)]]~\0a::\0a [[@t ~] ~ ~]\0a $(pax (welp pax /[p.n.dir.ark]))\0a::\0a *\0a =- [palm+[": " ``~]^-]~\0a :~ rose+[" " `~]^~[leaf+"*" (smyt pax)]\0a `tank`(show-dir vane pax dir.ark)\0a ==\0a==\0a'
The Urbit Lifecycle Function
The core expression in all of Urbit is the lifecycle function.
[2 [0 3] 0 2]
This is replay. The idea of Urbit is a computer whose entire lifecycle is defined by a single small fixed frozen function. We will revisit this function when we examine Arvo.
You can find it instantiated directly in /sys/arvo.hoon
in expressions like [%9 2 %10 [6 %0 3] %0 2]
.
Exercises
- Write your own Nock interpreter in Hoon.
- Write your own jet, following the tutorial↗.
- Optional: Compose a Nock addition gate from scratch. (Solution↗)
Additional Reading
Appendix: The Nock Interpreter
As hinted at by our jetting discussion above, Nock is not directly evaluated by the runtime. There are three key parts of the Nock interpreter:
- Bytecode interpreter
- Jet dashboard
- Allocator
This appendix summarizes some of the considerations and architecture that the current runtime interpreters (Vere and Sword, née Ares) must make in some respect.
Nock Bytecode
The VM doesn't actually execute Nock directly from its noun form. Instead it produces a Nock-based bytecode. Producing computationally efficient bytecode from Nock is one key to building a practical Urbit runtime, and has been a focus of the Sword (née Ares) project. The details of this in Vere are in vere/pkg/noun/nock.c
.
> ~>(%xray (add 2 3)){[fask 1023] [kicb 1] snol head swap tail [lilb 2] swap tail [lilb 3] auto musm [ticb 0] halt}
> ~>(%xray =+(2 [- -])){[litb 2] snol head swap head ault halt}
The %xray
hint on a core doesn't show the core, but it shows the formula that invokes the core.
> ~> %xray.[0 %outer]=| i=@|- ^- @~> %xray.[0 %inner]?:(=(i ^~((bex 0))) ~ $(i +(i)))outer: {lit0 snol [libk i:0] snol [ticb 0] halt}inner{[fabk 6] sam1 [sbin 3] lil0 [sbip 8] copy swap [fabk 6] bump musm [ticb 0] halt}
Core Academy lessons will not further explore the Nock bytecode interpreter.
u3n
: Nock Execution- (no docs exist for the Vere bytecode convention)
- Sword (née Ares), “Codegen Bootstrapping”↗
Jet Dashboard
The jet dashboard is the system in the runtime that registers, validates, and runs jets: specific pieces of Nock code reimplemented in C for performance.
The main part we have to be aware of as developers is jet registration and hinting. However, deeper parts of the jet dashboard do affect performance.
The jet dashboard maintains three jet state systems:
cold
state results from the logical execution history of the pier and consists of nouns.cold
jet state registers jets as they are found.cold
state ignore restarts.hot
state is the global jet dashboard and describes the actual set of jets loaded into the pier for the current running process. Calls tohot
state result from Nock Nine invocations of a core and an axis.hot
state is thus tied to process restart.warm
lists dependencies betweencold
andhot
state.warm
state can be cleared at any time and is cleared on restart.
The jet dashboard will not be explored in detail in Core Academy.
Allocator
The allocator is responsible for memory management. The Vere runtime has some peculiarities, such as the loom/road structure, which are not directly tied to the nature of Nock as a computable language.
Persistence means that we can store events and the event log, and that we can produce the state derived from them as a snapshot.
The allocator will be examined more in the runtime lessons on Vere.