Skip to content

Commit

Permalink
change behavior of instructions read_mem and write_mem
Browse files Browse the repository at this point in the history 
Up until now, both instructions did not modify the operational stack's
length. The new behavior is:

- `read_mem` uses stack element `ST0` as the memory pointer `ramp` and
    pushes the memory value `ramv` to the stack, increasing its size.
- `write_mem` (still) uses stack element `ST1` as the memory pointer
    `ramp` and writes stack element `ST0` to RAM, popping it from the
    stack in the process.
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed Feb 9, 2023
1 parent 4ad6fa2 commit 022245b
Show file tree
Hide file tree
Showing 13 changed files with 214 additions and 172 deletions.
2 changes: 1 addition & 1 deletion opcodes.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ def in_bucket(instruction_bucket, instruction):
if instruction_bucket == InstructionBucket.HasArg:
return instruction in [Instruction.Push, Instruction.Dup, Instruction.Swap, Instruction.Call]
if instruction_bucket == InstructionBucket.ShrinkStack:
return instruction in [Instruction.Pop, Instruction.Skiz, Instruction.Assert, Instruction.WriteIo,
return instruction in [Instruction.Pop, Instruction.Skiz, Instruction.Assert, Instruction.WriteMem, Instruction.WriteIo,
Instruction.Add, Instruction.Mul, Instruction.Eq, Instruction.XbMul]
if instruction_bucket == InstructionBucket.U32:
return instruction in [Instruction.Lt, Instruction.And, Instruction.Xor, Instruction.Log2Floor,
Expand Down
Binary file modified specification/cheatsheet.pdf
View file
Binary file not shown.
36 changes: 18 additions & 18 deletions specification/cheatsheet.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,31 +53,31 @@
\texttt{ 32} & $\ovoid$ & \tcbox[colback=instr-jsp]{\texttt{recurse}} & \texttt{\_} & \texttt{\_} \\
\texttt{ 18} & $\ominus$ & \texttt{assert} & \texttt{\_ st$_0$} & \texttt{\_} \\
\texttt{ 0} & $\ovoid$ & \texttt{halt} & \texttt{\_} & \texttt{\_} \\
\texttt{ 40} & $\ovoid^1$ & \tcbox[colback=instr-mem]{\texttt{read\_mem}} & \texttt{\_ addr st$_0$} & \texttt{\_ addr val} \\
\texttt{ 48} & $\ovoid$ & \tcbox[colback=instr-mem]{\texttt{write\_mem}} & \texttt{\_ addr val} & \texttt{\_ addr val} \\
\texttt{ 56} & $\ovoid^{10}$ & \texttt{hash} & \texttt{\_ st$_9$ $\!\!\dots\!\!$ st$_0$} & \texttt{\_ d$_4$ $\!\!\dots\!\!$ d$_0$ 0 $\!\!\dots\!\!$ 0} \\
\texttt{ 64} & $\ovoid^{11}$ & \texttt{divine\_sibling} & \texttt{\_ idx st$_9$ $\!\!\dots\!\!$ st$_5$ d$_4$ $\!\!\dots\!\!$ d$_0$} & \texttt{\_ idx>>1 r$_4$ $\!\!\dots\!\!$ r$_0$ l$_4$ $\!\!\dots\!\!$ l$_0$} \\
\texttt{ 72} & $\ovoid$ & \texttt{assert\_vector} & \texttt{\_} & \texttt{\_} \\
\texttt{ 80} & $\ovoid$ & \texttt{absorb\_init} & \texttt{\_} & \texttt{\_} \\
\texttt{ 88} & $\ovoid$ & \texttt{absorb} & \texttt{\_} & \texttt{\_} \\
\texttt{ 96} & $\ovoid^{10}$ & \texttt{squeeze} & \texttt{\_ st$_9$ $\dots$ st$_0$} & \texttt{\_ sq$_9$ $\dots$ sq$_0$} \\
\texttt{ 26} & $\ominus^1$ & \texttt{add} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ sum} \\
\texttt{ 34} & $\ominus^1$ & \texttt{mul} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ prod} \\
\texttt{104} & $\ovoid^1$ & \texttt{invert} & \texttt{\_ st$_0$} & \texttt{\_ st$_0^{-1}$} \\
\texttt{ 42} & $\ominus^1$ & \texttt{eq} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ (st$_0$==st$_1$)} \\
\texttt{ 40} & $\ominus$ & \tcbox[colback=instr-mem]{\texttt{read\_mem}} & \texttt{\_ addr st$_0$} & \texttt{\_ addr val} \\
\texttt{ 26} & $\oplus$ & \tcbox[colback=instr-mem]{\texttt{write\_mem}} & \texttt{\_ addr val} & \texttt{\_ addr val} \\
\texttt{ 48} & $\ovoid^{10}$ & \texttt{hash} & \texttt{\_ st$_9$ $\!\!\dots\!\!$ st$_0$} & \texttt{\_ d$_4$ $\!\!\dots\!\!$ d$_0$ 0 $\!\!\dots\!\!$ 0} \\
\texttt{ 56} & $\ovoid^{11}$ & \texttt{divine\_sibling} & \texttt{\_ idx st$_9$ $\!\!\dots\!\!$ st$_5$ d$_4$ $\!\!\dots\!\!$ d$_0$} & \texttt{\_ idx>>1 r$_4$ $\!\!\dots\!\!$ r$_0$ l$_4$ $\!\!\dots\!\!$ l$_0$} \\
\texttt{ 64} & $\ovoid$ & \texttt{assert\_vector} & \texttt{\_} & \texttt{\_} \\
\texttt{ 72} & $\ovoid$ & \texttt{absorb\_init} & \texttt{\_} & \texttt{\_} \\
\texttt{ 80} & $\ovoid$ & \texttt{absorb} & \texttt{\_} & \texttt{\_} \\
\texttt{ 88} & $\ovoid^{10}$ & \texttt{squeeze} & \texttt{\_ st$_9$ $\dots$ st$_0$} & \texttt{\_ sq$_9$ $\dots$ sq$_0$} \\
\texttt{ 34} & $\ominus^1$ & \texttt{add} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ sum} \\
\texttt{ 42} & $\ominus^1$ & \texttt{mul} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ prod} \\
\texttt{ 96} & $\ovoid^1$ & \texttt{invert} & \texttt{\_ st$_0$} & \texttt{\_ st$_0^{-1}$} \\
\texttt{ 50} & $\ominus^1$ & \texttt{eq} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ (st$_0$==st$_1$)} \\
\texttt{ 4} & $\oplus^2$ & \tcbox[colback=instr-u32]{\texttt{split}} & \texttt{\_ st$_0$} & \texttt{\_ hi lo} \\
\texttt{ 12} & $\ominus^1$ & \tcbox[colback=instr-u32]{\texttt{lt}} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ (st$_0$<st$_1$)} \\
\texttt{ 20} & $\ominus^1$ & \tcbox[colback=instr-u32]{\texttt{and}} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ (st$_0$\&st$_1$)} \\
\texttt{ 28} & $\ominus^1$ & \tcbox[colback=instr-u32]{\texttt{xor}} & \texttt{\_ st$_1$ st$_0$} & \texttt{\_ (st$_0$\^{}st$_1$)} \\
\texttt{ 36} & $\ovoid^1$ & \tcbox[colback=instr-u32]{\texttt{log\_2\_floor}} & \texttt{\_ st$_0$} & \texttt{\_ $\lfloor\log_2$(st$_0$)$\rfloor$} \\
\texttt{ 44} & $\ominus^1$ & \tcbox[colback=instr-u32]{\texttt{pow}} & \texttt{\_ e b} & \texttt{\_ b}$^\texttt{e}$ \\
\texttt{ 52} & $\ovoid^2$ & \tcbox[colback=instr-u32]{\texttt{div}} & \texttt{\_ denom num} & \texttt{\_ quot rem} \\
\texttt{112} & $\ovoid^3$ & \texttt{xxadd} & \texttt{\_ y$_2$ y$_1$ y$_0$ x$_2$ x$_1$ x$_0$} & \texttt{\_ y$_2$ y$_1$ y$_0$ z$_2$ z$_1$ z$_0$} \\
\texttt{120} & $\ovoid^3$ & \texttt{xxmul} & \texttt{\_ y$_2$ y$_1$ y$_0$ x$_2$ x$_1$ x$_0$} & \texttt{\_ y$_2$ y$_1$ y$_0$ z$_2$ z$_1$ z$_0$} \\
\texttt{128} & $\ovoid^3$ & \texttt{xinvert} & \texttt{\_ x$_2$ x$_1$ x$_0$} & \texttt{\_ y$_2$ y$_1$ y$_0$} \\
\texttt{ 50} & $\ominus^3$ & \texttt{xbmul} & \texttt{\_ x$_2$ x$_1$ x$_0$ b} & \texttt{\_ y$_2$ y$_1$ y$_0$} \\
\texttt{136} & $\oplus$ & \texttt{read\_io} & \texttt{\_} & \texttt{\_ a} \\
\texttt{ 58} & $\ominus$ & \texttt{write\_io} & \texttt{\_ st$_0$} & \texttt{\_}
\texttt{104} & $\ovoid^3$ & \texttt{xxadd} & \texttt{\_ y$_2$ y$_1$ y$_0$ x$_2$ x$_1$ x$_0$} & \texttt{\_ y$_2$ y$_1$ y$_0$ z$_2$ z$_1$ z$_0$} \\
\texttt{112} & $\ovoid^3$ & \texttt{xxmul} & \texttt{\_ y$_2$ y$_1$ y$_0$ x$_2$ x$_1$ x$_0$} & \texttt{\_ y$_2$ y$_1$ y$_0$ z$_2$ z$_1$ z$_0$} \\
\texttt{120} & $\ovoid^3$ & \texttt{xinvert} & \texttt{\_ x$_2$ x$_1$ x$_0$} & \texttt{\_ y$_2$ y$_1$ y$_0$} \\
\texttt{ 58} & $\ominus^3$ & \texttt{xbmul} & \texttt{\_ x$_2$ x$_1$ x$_0$ b} & \texttt{\_ y$_2$ y$_1$ y$_0$} \\
\texttt{128} & $\oplus$ & \texttt{read\_io} & \texttt{\_} & \texttt{\_ a} \\
\texttt{ 66} & $\ominus$ & \texttt{write\_io} & \texttt{\_ st$_0$} & \texttt{\_}
\end{tabular}
}

Expand Down
4 changes: 2 additions & 2 deletions specification/src/instruction-groups.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,8 @@ A summary of all instructions and which groups they are part of is given in the
| `recurse` | | x | x | | | | | | | | | x | | | |
| `assert` | | x | | x | | | | | | | | | | | x |
| `halt` | | x | | x | | | | | | | | x | | | |
| `read_mem` | | | | x | | | | | | | x | | | | |
| `write_mem` | | | | x | | | | | | | | x | | | |
| `read_mem` | | | | x | | | x | | | | | | | | |
| `write_mem` | | | | x | | | | | | | | | | | x |
| `hash` | | x | | x | | | | | x | | | | | | |
| `divine_sibling` | | x | | x | | | | x | | | | | | | |
| `assert_vector` | | x | | x | | | | | | | | x | | | |
Expand Down
8 changes: 4 additions & 4 deletions specification/src/instruction-specific-transition-constraints.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -333,22 +333,22 @@ Additionally, it defines the following transition constraints.

## Instruction `read_mem`

This instruction uses all constraints defined by [instruction groups](instruction-groups.md) `step_1` and `unary_operation`.
This instruction uses all constraints defined by [instruction groups](instruction-groups.md) `step_1` and `grow_stack`.
Additionally, it defines the following transition constraints.

### Description

1. The RAM pointer is overwritten with stack element `st1`.
1. The RAM pointer is overwritten with stack element `st0`.
1. The top of the stack is overwritten with the RAM value.

### Polynomials

1. `ramp' - st1`
1. `ramp' - st0`
1. `st0' - ramv`

## Instruction `write_mem`

This instruction uses all constraints defined by [instruction groups](instruction-groups.md) `step_1` and `keep_stack`.
This instruction uses all constraints defined by [instruction groups](instruction-groups.md) `step_1` and `shrink_stack`.
Additionally, it defines the following transition constraints.

### Description
Expand Down
Loading

0 comments on commit 022245b

Please sign in to comment.