# Stack arithmetization documentation

How our Nock stack table works. Note that currently we only implement nock 0-5 and cons which is all this document covers.

## Execution
Before getting into the polynomials let's look at how we execute nock. We use two stacks- a compute stack (CS) and a product stack (PS). The CS holds subject-formula pairs which need to be computed. The PS holds the results of the computations. The core loop is this:

Pop S and F off CS.

If op is 0 or a 1:
    Compute it and push the product on PS
    If CS is empty goto end else go back to the start.

else if op != 15:
    Push S [15 op] onto CS where op is the opcode of our instruction or 99 for cons. (op=15 means we finish computing the formula after the subformulae have been computed).
    If op=3 or 4 (so one subformula (SF)):
       Push S SF onto CS.
    else if op=2 or 5 (two subformulae):
       Push S SF1 S SF2 onto CS.
    else F is a cons of [R L]:
       Push S R S L onto CS.
    Go back to start.

else (op=15):
// This means finish computing the op found in the tail of the 15.
    if op=99 (cons):
       Pop the top two nouns off PS (L and R), construct [L R], and push onto PS.
    else if op=2:
       Pop the top two nouns off PS (P1 and P2) and push S P1 S P2 onto CS.
    else if op=3:
       Pop the top noun off PS, check if it's a noun or a cell, and push 0 or 1 onto PS.
    else if op=4:
       Pop the top noun off PS, crash if its a cell (ie abort the trace), increment the atom, encode as noun, and push onto PS.
    else (op=5):
       Pop the top two nouns off PS, compare them, and push 0 or 1 onto PS
    If CS is empty then end. Else return to start.

## State machine
We use a state machine to change rows and select polynomials for each row. We have 10 different modes:

| Mode | Description |
| ------- | ----------------------------------------- |
| %mstart | First row of trace |
| %mend | End of computation and all padding rows |
| %m1 | Start execution loop - pop S and F off CS |
| %mn0 | Evaluate nock 0 |
| %mn1 | Evaluate nock 1 |
| %mn15 | Finish nock evaluation (op=15) |
| %mn15a | Finish nock evaluation on second row |
| %msf | Push subformula onto CS |
| %msfa | Push second subformula onto CS |
| %msfb | Finish pushing second subformula onto CS |

The state machine flow looks like this:

Start in %mstart with CS=S F and PS=~.
Move to %m1.
%m1: Pop S F off CS.
    If op=0 move to %mn0
    If op=1 move to %mn1
    If op=15 move to %mn15
    else move to %msf
%mn0: Evaluate 0, push product onto PS. If CS is empty move to %mend else move to %m1.
%mn1: Evaluate 1, push product onto PS. If CS is empty move to %mend else move to %m1.
%msf: Push S [15 op] onto CS. Move to %msfa.
%msfa: Push S SF1 (subformula 1) onto CS.
    If op=2, 5 or 99 (cons) go to %msfb. Else go to %m1.
%msfab: Push S SF2 onto CS. Go to %m1.
%m15:
    If op=2:
       Pop P1 and P2 off PS, push onto CS, go to %m1.
    else if op=5:
       Pop P1 and P2 off PS. Compare and construct result 0 or 1 and push onto PS. If CS is empty go to %mend else go to %m1.
    else (op is 3, 4, or 99 (cons)): go to %m15a // We use a new row because we need to reuse some registers.
%m15a:
    if op=3:
       Pop the top noun off PS, check if it's an atom or a cell, encode the result 0 or 1, push onto PS. Then if CS is empty goto %mend else go to %m1.
    else if op=4:
       Pop the top noun off PS. Crash if it's a cell. Increment the atom and push onto PS. If CS is empty go to %mend else go to %m1.
    else if op=99 (cons):
       Pop top two nouns L and R off PS. Construct [L R] and push onto PS. If CS is empty go to %mend else go to %m1.
%mend: Stop. This row can be repeated forever for padding.

Note that every new row is a new mode.

## Registers
Here are all the registers. Each is a field element.

### Basic registers

These are all binary flags except for %cs-len and %ps-len.

| Register | Description |
| -------- | ----------------------------------------- |
| %mstart | First row of trace |
| %mend | End of computation and all padding rows |
| %m1 | Start execution loop - pop S and F off CS |
| %mn0 | Evaluate nock 0 |
| %mn1 | Evaluate nock 1 |
| %mn15 | Finish nock evaluation (op=15) |
| %mn15a | Finish nock evaluation on second row |
| %msf | Push subformula onto CS |
| %msfa | Push second subformula onto CS |
| %msfb | Finish pushing second subformula onto CS |
| %op | Opcode |
| %o0 | Nock 0 flag |
| %o1 | Nock 1 flag |
| %o2 | Nock 2 flag |
| %o3 | Nock 3 flag |
| %o4 | Nock 4 flag |
| %o5 | Nock 5 flag |
| %o15 | Nock 15 flag (Finish op) |
| %o99 | Nock 99 flag (CONS) |
| %cons | Flag for whether formula is cons |
| %csempty | 0 if CS is empty, 1 if nonempty |
| %cslen | Length of CS |
| %pslen | Length of PS |

### Extension registers
Note that for all inverses $0^{-1}=0$

| Register | Description |
| ----------- | ----------------------------------------------------------------- |
| %s | Subject |
| %f | Formula |
| %tail1 | Head of tail of decoded formula |
| %tail2 | Tail of tail of decoded formula (equal to tail 1 if tail is atom) |
| %i | General purpose register |
| %i2 | General purpose register |
| %r | General purpose register |
| %r2 | General purpose register |
| %dyck | Noun dyck word |
| %leaf | Noun leaf vector |
| %len | Noun length |
| %leninv | $len^{-1}$ |
| %i-diff-inv | $(I-I2)^{-1}$ |
| %cs | Compute stack |
| %csinv | $CS^{-1}$ |
| %ps | Product stack |
| %decoder | Decoder table multiset |
| %mem | Memory table multiset |
| %exp | Exponent table multiset |
| %e1 | Store exponent valu |
| %e3 | Store exponent valu |
| %e2 | Store exponent valu |

### Mode flags
Each mode register is a binary flag which selects the polynomials for that particular mode. So we have polynomials to force the mode flags to be binary.

$m_{start}(1-m_{start})=0$
$m_{end}(1-m_{end})=0$
$m_1(1-m_1)=0$
$m_{n0}(1-m_{n0})=0$
$m_{n1}(1-m_{n1})=0$
$m_{15}(1-m_{15})=0$
$m_{15a}(1-m_{15a})=0$
$m_{sf}(1-m_{sf})=0$
$m_{sfa}(1-m_{sfa})=0$

We have one polynomial to force exactly one mode flag to be on at a time.
$m_{start}+m_{end}+m_1+m_{n0}+m_{n1}+m_{n15}+m_{n15a}+m_{sf}+m_{sfa} - 1=0$

### Opcodes
%op is the actual opcode (0-5,15,99). Then we have a binary flag for each opcode to select polynomials.

So we have polynomials to force the opcode flags to be binary.
$o_0(1-o_0)=0$
$o_1(1-o_1)=0$
$o_2(1-o_2)=0$
$o_3(1-o_3)=0$
$o_4(1-o_4)=0$
$o_5(1-o_5)=0$
$o_15(1-o_15)=0$
$o_99(1-o_99)=0$

One polynomial to force exactly one opcode flag to be on.
$o_0+o_1+o_2+o_3+o_4+o_5+o_{15}+o_{99}-1=0$

And we have one polynomial to force the correct opcode flag to be turned on based on what the actual %op register contains.
$o_1+2o_2+3o_3+4o_4+5o_5+15o_{15}+99o_{99}-op=0$

### Misc polynomials
CONS flag must be binary.
$CONS(1-CONS)=0$

%csempty is 1 if %cs is empty (ie len=0), else 0. This is used to check if we are finished with our computation.

To do this we constrain csinv to be the inverse of cslen, and then set %csempty to be $1-cslen*csenv$. To force csinv to be the inverse of cslen we can do a trick with two polynomials:

$csinv(cslen*csinv-1)=0$

And then we constraint csempty to be the opposite:

$cslen*csinv+csempty-1=0$

### Eval loop

##### Mode Start
add some polys

##### Mode End
We're finished with the computation and the product is in PS. We just need to constrain the padding rows to keep ps, pslen, and mode unchanged.
$M_{end}(ps-ps')=0$
$M_{end}(pslen-pslen')=0$
$M_{end}(M_{end}-M_{end}')=0$

##### Mode 1
Pop formula and subject off CS:
$M_1'(\alpha^{-2}(cs-s')-\alpha^{-1}f'-cs')=0$

Decrement CS len by 2:
$M_1'((cslen-2)-cslen')=0$

Read CONS, Tail1, Tail2 off decoder output:
$M_1'(decoder*(\beta-(p*f'+q*cons'+r*op'+s*tail_1'+t*tail_2'))-decoder')=0$

Change mode based on opcode and cons:

If op=0 and cons=0 goto mode n0 (nock 0):
$m_1*o_0(1-cons)(m_{n0}'-1)=0'$

else if op=1 and cons=0 goto mode n1 (nock 1):
$m_1*o_1(1-cons)(m_{n1}'-1)=0'$

else if o=15 and cons=0 goto mode n15 (finish opcode):
$m_1*o_{15}(1-cons)(m_{n15}'-1)=0'$

else if cons=1 go to mode sf (subformulae):
$m_1*cons(m_{sf}'-1)=0'$

else go to mode sf (subformulae):
$m_1(o_2+o_3+o_4+o_5)(m_{sf}'-1)=0$

##### Mode 0 (nock 0)
tail1 contains the axis. We multiply [s tail1 i] ont the memory multiset and i will be the subtree.
$m_{n0}'(mem*(\beta - (p*s'+q*tail_1'+r*i'))-mem')=0$

Push i onto PS:
$m_{n0}'(\alpha*ps + i' - ps')=0$
$m_{n0}'((pslen+1)-pslen')=0$

If CS is empty go to mode end else return to mode 1:
$m_{n0}*csempty(m_{end}'-1)=0'$
$m_{n0}*(csempty-1)(m_1'-1)=0'$

cs, decoder, and exp don't change:
$m_{n0}(cs-cs')=0$
$m_{n0}(cslen-cslen')=0$
$m_{n0}(decoder-decoder')=0$
$m_{n0}(exp-exp')=0$

##### Mode 1 (nock 1)

Tail1 is the product. Just push it onto the product stack and return to mode 1 (or end).

$m_{n1}'((\alpha*ps+tail_1')-ps')=0$
$m_{n1}'((pslen+1)-pslen')=0$

If CS is empty go to mode end else return to mode 1:
$m_{n1}*csempty(m_{end}'-1)=0'$
$m_{n1}*(csempty-1)(m_1'-1)=0'$

cs, decoder, and exp don't change:

$m_{n1}(cs-cs')=0$
$m_{n1}(cslen-cslen')=0$
$m_{n1}(decoder-decoder')=0$
$m_{n1}(exp-exp')=0$

##### Mode sf (process subformulae)
Tail1 contains the first subformula and tail2 contains the second (if it exists). Push onto CS: S, [15 op], S, SF1, S, SF2 and return to mode 1 (SF2 may not be necessary). Also op=99 means cons.

First construct [15 op] and push S, [15 op] onto CS.

A noun is a triple of len, dyck, leaf.
$len=2$
$leaf=\alpha*15 + op$
$dyck=1$
We compress the noun as $a*len+b*dyck+c*leaf$ and so our noun will be $2a+b+c*\alpha*15 + c*op$. We push s and this noun onto CS all in one big polynomial:

$m_{sf}'(cons'-1)((\alpha^2*cs+\alpha(2a+b+c*\alpha*15+c*op')+s')-cs')=0$

Else if cons=1 then push S, [15 99] onto CS.
$m_{sf}'cons'((\alpha^2*cs+\alpha(2a+b+c*\alpha*15+c*99)+s')-cs')=0$

Increment CS length by 2:
$m_{sf}'(cslen+2-cslen')=0$

Move to mode sfa to push S, SF1 onto CS:
$m_{sf}(m_{sfa}'-1)=0$

ps, pslen, mem, decoder, s, cons, op, tail1, tail2, and exp don't change:
$m_{sf}'(ps-ps')=0$
$m_{sf}'(pslen-pslen')=0$
$m_{sf}'(mem-mem')=0$
$m_{sf}'(decoder-decoder')=0$
$m_{sf}'(s-s')=0$
$m_{sf}'(cons-cons')=0$
$m_{sf}'(op-op')=0$
$m_{sf}'(tail_1-tail_1')=0$
$m_{sf}'(tail_2-tail_2')=0$
$m_{sf}'(exp-exp')=0$

##### Mode sfa (process subformula 1)
Push S, tail1 onto CS.

$m_{sfa}'((\alpha^2*cs+\alpha*tail_1'+s')-cs')=0$

Increment CS len by 2.
$m_{sfa}'(cslen+2-cslen')=0$

Nock 3 and 4 only have 1 subformula so they're finished. Check if CS is empty and either return to mode 1 or go to mode end.

$m_{sfa}(o_3+o_4)csempty(m_{end}'-1)=0$
$m_{sfa}(o_3+o_4)(csempty-1)(m_1'-1)=0$

Nock 2, 5, and cons have a second subformula so move to mode sfb.

$m_{sfa}(o_2+o_5+cons)(m_{sfb}'-1)=0$

s, tail2, ps, pslen, mem, decoder, and exp don't change.
$m_{sfa}'(s-s')=0$
$m_{sfa}'(tail2-tail2')=0$
$m_{sfa}'(ps-ps')=0$
$m_{sfa}'(pslen-pslen')=0$
$m_{sfa}'(mem-mem')=0$
$m_{sfa}'(decoder-decoder')=0$
$m_{sfa}'(exp-exp')=0$

##### Mode sfb

Push S, tail2 onto CS.

$m_{sfb}'((\alpha^2*cs+\alpha*tail_2'+s')-cs')=0$

Increment CS len by 2.
$m_{sfb}'(cslen+2-cslen')=0$

If CS is empty go to mode end else go to mode 1.
$m_{sfb}csempty(m_{end}'-1)=0$
$m_{sfb}(csempty-1)(m_1'-1)=0$

ps, pslen, mem, decoder, and exp don't change.
$m_{sfb}'(ps-ps')=0$
$m_{sfb}'(pslen-pslen')=0$
$m_{sfb}'(mem-mem')=0$
$m_{sfb}'(decoder-decoder')=0$
$m_{sfb}'(exp-exp')=0$

#### Mode OP15 (select off ocode for 15)

We have evalutaed the subformula(e) and the products are on the product stack. Now we switch off the opcode contained in tail1 to finish the specific opcode. (0 and 1 are evaluated directly and never get here. 99 is cons).

First decode tail1 into len, dyck, and leaf registers. (leaf will contain the opcode).
$m_{n15}((a*len+b*dyck+c*leaf)-tail1)=0$

Now leaf contains the opcode so copy it into op so we can use the opcode flags.
$m_{n15}(op - leaf) = 0$

We compute nock 2 and 5 in the same row. 3, 4, and cons need to decode/construct nouns and so reuse the dyck, leaf, and len registers. So they need a new row of the table and thus a new mode.

##### Finish nock 2.
Pop S and F off PS, push onto CS, return to start.

$m_{n15}'o_2'((\alpha^{-2}(ps-s')-\alpha^{-1}*f')-ps')=0$

Decrement PS len by 2.
$m_{n15}'o_2'((pslen-2)-pslen')=0$

Push S and F onto CS.
$m_{n15}'o_2'((\alpha^2*cs+\alpha*f'+s')-cs')=0$

Increment CS len by 2.
$m_{n15}'o_2'((cslen+2)-cslen')=0$

##### Finish nock 5

We want to pop the top two nouns off PS into i and i2, compare them, then encode 0 if they are equal or 1 if they are unequal and push this onto PS. To do this we have a register idiffinv which contains $(i-i2)^{-1}$ (remember $0^{-1}=0$) and so $(i-i2)*idiffinv$ is our result (encoded as a noun).

First, force idiffenv to contain $(i-i2)^{-1}$ using the two polynomial trick.

$(i-i2)((i-i2)idiffinv-1)=0$
$idiffenv((i-i2)idiffinv-1)=0$

Pop i and i2 off PS, encode $(i-i2)*idiffinv$ as an atom, and pop onto ps. The atom will be $a+c*(i'-i2')*idiffinv'$ because len=1, dyck=0, and leaf=$(i'-i2')*idiffinv$.

$m_{n15}'o_5'(((\alpha^{-1}(ps-i')-i2')+(a+c*(i'-i2')*idiffinv'))-ps')=0$

Decrement ps len.
$m_{n15}'o_5'((pslen-1)-pslen')=0$

###### Change modes.
We've finished nock 2 and 5 so change modes.

Nock 3, 4, and 99 (cons) go to mode 15a.
$m_{n15}(o_3+o_4+o_{99})(m_{15a}'-1)=0$

Nock 2 and 5 are finished so check if cs is empty and either go to mode 1 or end.
$m_{n15}(o_2+o_5)csempty(m_{end}'-1)=0$
$m_{n15}(o_2+o_5)(csempty-1)(m_1'-1)=0$

mem, exp, and decoder are unchanged.
$m_{n15}'(mem-mem')=0$
$m_{n15}'(exp-exp')=0$
$m_{n15}'(decoder-decoder')=0$

CS remains unchanged except for nock 2 (because we wrote to it).
$m_{n15}'(o_2'-1)(cs-cs')=0$

#### Mode 15a
Finish nock 3, 4, and cons.

##### Finish nock 3

We want to pop the noun off the top of the product stack, decode it, compute 0 if it's a cell and 1 if it's a noun, encode the result, and push onto the product stack. Then return to the start.

We want to decode the noun into len, leaf, and dyck. If len==1 we have an atom so write 1 into i. Else write 0 into i.

So first we must write $(len-1)^{-1}$ into leninv.

$(len-1)((len-1)*leninv-1)=0$
$leninv((len-1)*leninv-1)=0$

New $(len-1)*leninv$ is 0 if len=1 (ie an atom) and 1 otherwise, which is the opposite of what we want. So we want $1-(len-1)*leninv$ encoded as an atom and pushed onto PS. An atom encoded as a noun is $a*len+b*dyck+c*leaf=a*1+b*0+c*atom=a+c*atom$. So it will be $a+c*(1-(len-1)*leninv)$. We must pop [len dyck leaf] off PS and push this onto it at the same time.

$m_{n15a}'o_3'((ps-(a*len+b*dyck+c*leaf))+(a+c*(1-(len'-1)*leninv')-ps'))=0$

##### Finish nock 4

Pop PS onto I, decode into len, leaf, and dyck, increment leaf, encode it, and push it into PS.

First decode i into len, leaf, and dyck,
$m_{n15a}o_4((a*len+b*dyck+c*leaf)-i)=0$

Now pop I off PS, increment leaf, encode, and push back onto PS.
$m_{n15a}'o_4'(((ps-i')+(a+c*(leaf'+1)))-ps')=0$

PS len is unchanged for nock 3 or 4.
$m_{n15a}'(o_3'+o_4')(pslen-pslen')=0$

##### Finish cons (op 99)

We want to pop the top two nouns L and R of PS, encode as [L R], and push back onto PS. Instead of L and R registers though we will just reuse the s and f registers.

We will pop the first noun into s and decode into len, dyck, and leaf.
$m_{n15a}o_{99}((a*len+b*dyck+c*leaf)-s)=0$

We will pop the second noun into f and decode it into i, i2, and r.
$m_{n15a}o_{99}((a*i+b*i2+c*r)-f)=0$

CONS: T = [L R]
$leaf(T)=leaf(L)*\alpha^{len(R)}+leaf(r)$
$dyck(T)=dyck(l)*\alpha^{2*len(R)-1}+\alpha^{2*len(R)-2}+dyck(R)$
$len(T)=len(L)+len(R)$

We need to compute $\alpha^{len(R)}$, $\alpha^{2*len(R)-1}$, and $\alpha^{2*len(R)-2}$. We just multiply pairs onto the exp multiset. $len(R)$ is in i, results go in e1, e2, e3.

$m_{n15a}'o_99'(exp(\beta-(p*i+q*e1))(\beta-(p*(2*i-1)+q*e2))(\beta-(p*(2*i-2)+q*e3))-exp')=0$

Now we construct the new cons noun and encode into r2.
$m_{n15a}o_{99}((a(len+i)+b((dyck*e2)+e3+i2)+c(leaf*e1+r))-r2)=0$

Pop s and f off ps and push r2 onto ps.
$m_{n15a}'o_{99}'(((\alpha(ps-s')-f')+r2')-ps')=0$
$m_{n15a}'o_{99}'(((\alpha(ps-s')-f')+(a(len+i)+b((dyck*e2)+e3+i2)+c(leaf*e1+r)))-ps')=0$

Decrement ps length by 1.
$m_{n15a}'o_99'(pslen-pslen')=0$

We've handled all opcodes. If CS is empty go to mode end else go to mode 1.
$m_{n15a}csempty(m_{end}'-1)=0$
$m_{n15a}(csempty-1)(m_1'-1)=0$

cs, cslen, mem, and decoder are unchanged.
$m_{n15a}(cs-cs')=0$
$m_{n15a}(cslen-cslen')=0$
$m_{n15a}(mem-mem')=0$
$m_{n15a}(decoder-decoder')=0$