Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

implement TIP 0001: Contiguity Argument for Memory Consistency #80

Merged
merged 23 commits into from
Oct 19, 2022
Merged

implement TIP 0001: Contiguity Argument for Memory Consistency #80

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
52e0a6e
implement TIP 0001: Contiguity Argument for Memory Consistency
jan-ferdinand Oct 7, 2022
31db2ea
limit number of accumulated factors in running product to at most T
jan-ferdinand Oct 11, 2022
e1522c5
add columns and evaluation argument for TIP 0003 (#78)
jan-ferdinand Oct 8, 2022
79fcfa5
link to & from multiple tables using cross-table arguments (#78)
jan-ferdinand Oct 8, 2022
c2a2d07
add multi-table permutation argument for clock jump differences (#78)
jan-ferdinand Oct 8, 2022
96961cf
fill in clock jump differences for processor's base table (#78)
jan-ferdinand Oct 9, 2022
c77b8b8
extend all tables according to new cross-table arguments (#78)
jan-ferdinand Oct 9, 2022
b5e9994
Add columns “InverseOfClkDiffMinusOne” to memory tables. Extend & Pad.
jan-ferdinand Oct 13, 2022
0017c20
treat clock jump differences of magnitude 1 explicitly (#78)
jan-ferdinand Oct 13, 2022
b2410c1
WIP: start adding automatic opcode derivation & adde RAMP to processor
jan-ferdinand Oct 14, 2022
e9956a1
add automatic opcode derivation
aszepieniec Oct 14, 2022
a997118
fix reverse map opcode -> instruction
aszepieniec Oct 14, 2022
e7b0b9c
fix non-unique opcode bug
aszepieniec Oct 14, 2022
6434e74
add ”tests“ to print all opcodes and instruction bucket fill level
jan-ferdinand Oct 16, 2022
d8aaeb4
remove debug code
jan-ferdinand Oct 16, 2022
7f40cd5
activate instruction buckets
aszepieniec Oct 17, 2022
1d73259
add sanity test for op stack
aszepieniec Oct 18, 2022
080fa97
update spec with instruction group keep_ram
aszepieniec Oct 18, 2022
4749dbd
update cheatsheet wrt ramp
aszepieniec Oct 18, 2022
d8ece34
update spec in anticipation of complete RAM arithmetization
aszepieniec Oct 18, 2022
aa3a730
fix links
aszepieniec Oct 19, 2022
e04b397
update cheatsheet wrt ram table
aszepieniec Oct 19, 2022
0d81cc4
Merge pull request #88 from TritonVM/tip3
aszepieniec Oct 19, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file modified specification/cheatsheet.pdf
View file
Open in desktop
Binary file not shown.
22 changes: 11 additions & 11 deletions specification/cheatsheet.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,26 +131,26 @@
Instruction & 4 & 2 & 6 \\
Processor & 38 & 8 & 46 \\
OpStack & 4 & 1 & 5 \\
RAM & 4 & 1 & 5 \\
RAM & 7 & 6 & 5 \\
JumpStack & 5 & 1 & 6 \\
Hash & 49 & 2 & 51 \\ \bottomrule\bottomrule
$\sum$ & 107 & 16 & 123
$\sum$ & 110 & 21 & 131
\end{tabular}
\end{minipage}

\newpage
\hspace*{-4em}%
\scalebox{0.8}{
\scalebox{0.75}{
\rowcolors{2}{row2}{row1}
\begin{tabular}{llllllllllllllllllllll}
\begin{tabular}{lllllllllllllllllllllll}
\toprule
Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & \\ \midrule
Program & \multicolumn{3}{l}{Address} & \multicolumn{2}{l}{Instruction} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & & & & & \\
Instruction & \multicolumn{3}{l}{Address} & \texttt{CI} & \texttt{NIA} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & & & & & \\
Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB6} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMV} & \\
OpStack & \texttt{CLK} & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & \texttt{OSP} & \texttt{OSV} & & & & & & \\
RAM & \texttt{CLK} & & & & & & & & & & & & \multicolumn{4}{l}{\texttt{RAMP} ($\widehat{=}$ \texttt{ST1})} & & & \texttt{RAMV} & \texttt{IORD} & \\
JumpStack & \texttt{CLK} & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\
Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & & \\ \midrule
Program & \multicolumn{3}{l}{Address} & \multicolumn{2}{l}{Instruction} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & & & & & & \\
Instruction & \multicolumn{3}{l}{Address} & \texttt{CI} & \texttt{NIA} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & & & & & & \\
Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB6} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMV} & \texttt{RAMP} & \\
OpStack & \texttt{CLK} & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & \texttt{OSP} & \texttt{OSV} & & & & & & & \\
RAM & \texttt{CLK} & \texttt{RAMP} & \texttt{RAMV} & \texttt{IORD} & \texttt{bcpc0} & \texttt{bcpc1} & \texttt{clk\_di} & \\
JumpStack & \texttt{CLK} & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & & \\
Hash & \multicolumn{4}{l}{RoundNumber} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{l}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\ \bottomrule
\end{tabular}
} %end scalebox
Expand Down
79 changes: 44 additions & 35 deletions specification/src/instruction-groups.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,40 +10,41 @@
| `shrink_stack` | stack's top-most element is removed, rest of the stack remains unchanged. Needs `hv3` |
| `unop` | stack's top-most element is modified, rest of stack remains unchanged |
| `binop` | stack shrinks by one element, new top of the stack is modified. Needs `hv3` |
| `keep_ram` | no memory access: `ramp` and `ramv` do not change. |

A summary of all instructions and which groups they are part of is given in the following table.

| instruction | `has_arg`* | `decompose_arg` | `step_1` | `step_2` | `grow_stack` | `keep_stack` | `shrink_stack` | `unop` | `binop` |
|:-----------------|:-----------|:----------------|:---------|:---------|:-------------|:-------------|:---------------|:-------|:--------|
| `pop` | | | x | | | | x | | |
| `push` + `a` | x | | | x | x | | | | |
| `divine` | | | x | | x | | | | |
| `dup` + `i` | x | x | | x | x | | | | |
| `swap` + `i` | x | x | | x | | | | | |
| `nop` | | | x | | | x | | | |
| `skiz` | | | | | | | x | | |
| `call` + `d` | x | | | | | x | | | |
| `return` | | | | | | x | | | |
| `recurse` | | | | | | x | | | |
| `assert` | | | x | | | | x | | |
| `halt` | | | x | | | x | | | |
| `read_mem` | | | x | | | | | x | |
| `write_mem` | | | x | | | x | | | |
| `hash` | | | x | | | | | | |
| `divine_sibling` | | | x | | | | | | |
| `assert_vector` | | | x | | | x | | | |
| `add` | | | x | | | | | | x |
| `mul` | | | x | | | | | | x |
| `invert` | | | x | | | | | x | |
| `split` | | | x | | | | | | |
| `eq` | | | x | | | | | | x |
| `lsb` | | | x | | | | | | |
| `xxadd` | | | x | | | | | | |
| `xxmul` | | | x | | | | | | |
| `xinvert` | | | x | | | | | | |
| `xbmul` | | | x | | | | | | |
| `read_io` | | | x | | x | | | | |
| `write_io` | | | x | | | | x | | |
| instruction | `has_arg`* | `decompose_arg` | `step_1` | `step_2` | `grow_stack` | `keep_stack` | `shrink_stack` | `unop` | `binop` | `keep_ram` |
|:-----------------|:-----------|:----------------|:---------|:---------|:-------------|:-------------|:---------------|:-------|:--------|------------|
| `pop` | | | x | | | | x | | | x |
| `push` + `a` | x | | | x | x | | | | | x |
| `divine` | | | x | | x | | | | | x |
| `dup` + `i` | x | x | | x | x | | | | | x |
| `swap` + `i` | x | x | | x | | | | | | x |
| `nop` | | | x | | | x | | | | x |
| `skiz` | | | | | | | x | | | x |
| `call` + `d` | x | | | | | x | | | | x |
| `return` | | | | | | x | | | | x |
| `recurse` | | | | | | x | | | | x |
| `assert` | | | x | | | | x | | | x |
| `halt` | | | x | | | x | | | | x |
| `read_mem` | | | x | | | | | x | | |
| `write_mem` | | | x | | | x | | | | |
| `hash` | | | x | | | | | | | x |
| `divine_sibling` | | | x | | | | | | | x |
| `assert_vector` | | | x | | | x | | | | x |
| `add` | | | x | | | | | | x | x |
| `mul` | | | x | | | | | | x | x |
| `invert` | | | x | | | | | x | | x |
| `split` | | | x | | | | | | | x |
| `eq` | | | x | | | | | | x | x |
| `lsb` | | | x | | | | | | | x |
| `xxadd` | | | x | | | | | | | x |
| `xxmul` | | | x | | | | | | | x |
| `xinvert` | | | x | | | | | | | x |
| `xbmul` | | | x | | | | | | | x |
| `read_io` | | | x | | x | | | | | x |
| `write_io` | | | x | | | | x | | | x |

\*
Instruction Group `has_arg` is a _virtual_ instruction group.
Expand Down Expand Up @@ -193,7 +194,6 @@ Below, you can find a list of all 16 indicator polynomials.
1. The stack element in `st15` does not change.
1. The top of the OpStack underflow, i.e., `osv`, does not change.
1. The OpStack pointer does not change.
1. The RAM value `ramv` does not change.

### Polynomials

Expand All @@ -215,7 +215,6 @@ Below, you can find a list of all 16 indicator polynomials.
1. `st15' - st15`
1. `osv' - osv`
1. `osp' - osp`
1. `ramv' - ramv`

## Group `shrink_stack`

Expand Down Expand Up @@ -286,7 +285,6 @@ Since the stack can only change by one element at a time, this prevents stack un
1. The stack element in `st15` does not change.
1. The top of the OpStack underflow, i.e., `osv`, does not change.
1. The OpStack pointer does not change.
1. The RAM value `ramv` does not change.

### Polynomials

Expand All @@ -307,7 +305,6 @@ Since the stack can only change by one element at a time, this prevents stack un
1. `st15' - st15`
1. `osv' - osv`
1. `osp' - osp`
1. `ramv' - ramv`

## Group `binop`

Expand Down Expand Up @@ -350,3 +347,15 @@ Since the stack can only change by one element at a time, this prevents stack un
1. `st15' - osv`
1. `osp' - (osp - 1)`
1. `(osp - 16)·hv3 - 1`

## Group `keep_ram`

### Description

1. The RAM pointer stays the same.
2. The RAM value stays the same.

### Polynomials

1. `ramp' - ramp`
2. `ramv' - ramv`
Loading