Nock Primer for ZK

Nock is a simple, cons cell-based language. Every computation is a reduction of a "subject" (arbitrary cell or number) and a "formula" (structured cons cell). There is no symbols table or anything external--all "variables" are accessed by manipulating the subject.

Nock provides simple facilities for consing cells, accessing arbitrary parts of a tree, testing for cell/number, incrementing, and equality testing. Those are sufficient for Turing completeness (easy to see how you can use them to "move to points on a tape", "alter the tape", "add a slot to the tape", etc).

Primitives

• atom: a natural number

• cell: a cons cell; head/tail can be atoms or cells

• noun: an atom or a cell

Examples:

• atom: 239

• cell: [[4 5] 9]

• noun: 561

• noun: [29 [31 2]]

How Nock Works

Nock is a pure function that takes two nouns as arguments (the "subject" and the "formula"), and returns one noun (the "result").

nock(subject, formula) -> result

We'll use .* below to mean nock, since that's what the Urbit command line uses.

noun arguments

• subject: any arbitrary noun

• formula

  • must be a cell

  • head must be an opcode from 0-11 or a cell

examples

:: subject 15, formula [0 1]
[15 [0 1]]

:: subject [42 43], formula [4 0 2]
[[42 43] [4 0 2]]

opcode 0: look up a value in a tree

opcode 0 formulas must be followed by exactly one atom, representing the tree index to look up a value in. [0 7] is valid; [0 [1 2]] an invalid formula.

To perform a lookup, treat the index as a binary number; e.g. 14 = 1110. Then do the algorithm:

• if the number is 1, return the current subject

• else branch on the 2nd bit: if it's 0, set subject to the head; if 1, set subject to the tail

• remove the 2nd bit and recur

You can also read this in English from right to left, where 0 is "head of", 1 is "tail of", and the initial 1 is "the noun". So 1110 is "the head of the tail of the tail of the noun."

This is more intuitive in diagram form: the leaves below represent addresses in the tree:

      1
    /   \
   2     3
  / \   / \
 4   5 6   7
          / \
         14 15

simple examples

> .*([42 43] [0 1])
[42 43]

> .*([42 43] [0 2])
42

> .*([42 43] [0 3])
43

> .*([[4 5] [6 7]] [0 4])
4

> .*([[4 5] [6 7]] [0 3])
[6 7]

opcode 1: return constant value

Formulas with 1 at the head ignore the subject, and return the noun following the 1 as the result. Examples:

> .*([42 43] [1 59])
59

> .*([42 43] [1 [[50 51] 19]])
[[50 51] 19]

opcode 2: use a formula stored in the subject

These formulas take the form [2 formula1 formula2]. The "sub-formulas" are used like so:

• result1 = .*(subject formula1)

• result2 = .*(subject formula2)

• result = .*(result1 result2)

In English, both formulas are run against the subject, and result1 is then used as a new subject, and result2 is used as a new formula. We can use the 1 opcode in either formula1 or formula2 to produce a constant subject/formula, regardless of initial subject.

> .*([49 [0 2]] [2 [0 1] [0 3]])
49 

.*([49 [1 5]] [2 [0 1] [0 3]])
5

opcode 3: test for cell/atom

Form: [3 formula1]

- result1 = .*(subject formula1)
- if result1 is a cell, return 0.
- if result1 is an atom, return 1

opcode 4: increment

Form: [4 formula1]

- result1 = .*(subject formula1)
- assert result1 is an atom
- return result1 + 1

opcode 5: equality test

Form: [5 formula1 formula2]. The only slightly weird thing is that 0 is true, and 1 is false (as in Unix/bash scripting).

- result1 = .*(subject formula1)
- result2 = .*(subject formula2)
- if result1 == result2, return 0
- else return 1

opcode 6: if/else

Form: [6 formula1 if-formula else-formula]

- result1 = .*(subject formula1)
- if result1 == 0
  - return .*(subject if-formula)
- if result1 == 1
  - return .*(subject else-formula)

cell cons rule

This isn't an opcode, but it is an evaluation rule. So far, we've seen only formulas where the head is an opcode/atom. However, what if the formula head is itself a cell?

In that case, we treat the formula as [formula1 formula2], and the result of evaluating it is:

result = [.*(subject formula1) .*(subject formula2)]

Examples
> .*([42 43] [[0 3] [0 2]])
[43 42]

> .*([42 43] [[0 3] [1 29]])
[43 29]

> .*([42 43] [[4 [0 3]] [1 29]])
[44 29]

other opcodes

There are additional opcodes 7-10, but they are just sugar on top of 0-6. Finally, there is opcode 11, which can pass unevaluated "hints" to the interpreter (for performance profiling or "jetting").

Jetting

"Jetting" simply refers to the option Nock interpreters have to run a piece of code in an alternate way, if they can evaluate it faster. This is possible because results are purely a function of subject and formula.

Imagine an implementation of (add x y) using base Nock. It would look like this:

- if x == 0, return y
- else decrement x as x', increment y as y'
- return (add x', y')

Now imagine that that pseudocode is represented as long-running-formula, and the interpreter encounters the evaluation .*([19 20] long-running-formula). If it knows that long-running-formula is really just add, it can skip full evaluation and return 19+20.

Jets are a necessary tradeoff for having a tiny language spec.

Proving a Nock evaluation in a ZK environment

I have a small proof-of-concept of this running in Cairo. This is a two-pass process:

1. preprocessing

2. proving

preprocessing

Run the Nock code inside an interpreter in Nock itself, producing non-deterministic hint metadata. The metadata consists mainly of a lookup table in JSON/Python, where nouns are Merkleized, and

• key: [subjectMerkleRoot, formulaMerkleRoot]

• value: hint

For example, .*(subject [0 7]) is preprocessed into a hint of the Merkle proof for index 7 inside the subject, treating the subject noun as a Merkle tree.

proving

The Cairo program is given the hints and a starting subject/formula. It recursively uses the hints to verify that each Nock opcode was run correctly.