Skip to content

Commit

Permalink
replace Instruction Table by Lookup Argument
Browse files Browse the repository at this point in the history 
Replace the Instruction Table with a Lookup Argument, increasing overall performance and lowering the design complexity.

Additionally, the `VMState` now records the condition “halting“ explicitly. Initialized as `false`, only executing instruction `halt` sets it to `true`. This allows de-duplication of logic in the virtual machine's methods `.run()` and `.simulate()` and correctly throws an error whenever the instruction pointer is out of bounds.
  • Loading branch information
@jan-ferdinand
jan-ferdinand authored Jan 30, 2023
2 parents 4462a91 + 576404b commit 543327a
Show file tree
Hide file tree
Showing 29 changed files with 354 additions and 1,105 deletions.
12 changes: 0 additions & 12 deletions constraint-evaluation-generator/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ use triton_vm::table::constraint_circuit::CircuitExpression;
use triton_vm::table::constraint_circuit::ConstraintCircuit;
use triton_vm::table::constraint_circuit::InputIndicator;
use triton_vm::table::hash_table::ExtHashTable;
use triton_vm::table::instruction_table::ExtInstructionTable;
use triton_vm::table::jump_stack_table::ExtJumpStackTable;
use triton_vm::table::op_stack_table::ExtOpStackTable;
use triton_vm::table::processor_table::ExtProcessorTable;
Expand All @@ -32,17 +31,6 @@ fn main() {
);
write(&table_name_snake, source_code);

let (table_name_snake, table_name_camel) = construct_needed_table_identifiers(&["instruction"]);
let source_code = gen(
&table_name_snake,
&table_name_camel,
&mut ExtInstructionTable::ext_initial_constraints_as_circuits(),
&mut ExtInstructionTable::ext_consistency_constraints_as_circuits(),
&mut ExtInstructionTable::ext_transition_constraints_as_circuits(),
&mut ExtInstructionTable::ext_terminal_constraints_as_circuits(),
);
write(&table_name_snake, source_code);

let (table_name_snake, table_name_camel) = construct_needed_table_identifiers(&["processor"]);
let source_code = gen(
&table_name_snake,
Expand Down
Binary file modified specification/cheatsheet.pdf
View file
Binary file not shown.
39 changes: 18 additions & 21 deletions specification/cheatsheet.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,19 +87,18 @@
\rowcolors{2}{row2}{row1}
\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{PI} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB7} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMP} & \texttt{RAMV} \\
OpStack & \texttt{CLK} & \texttt{clk\_di} & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & & \texttt{OSP} & \texttt{OSV} & & & & & \\
RAM & \texttt{CLK} & \texttt{clk\_di} & & \texttt{PI} & & \texttt{bcpc0} & \multicolumn{2}{l}{\texttt{bcpc1}} & & & & & & & & & & \multicolumn{3}{l}{\texttt{RAMP}DiffInv} & \texttt{RAMP} & \texttt{RAMV} \\
JumpStack & \texttt{CLK} & \texttt{clk\_di} & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\
Hash & \multicolumn{4}{l}{RoundNumber} & \texttt{CI} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{r}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\
U32 & \texttt{CF} & \multicolumn{3}{l}{\texttt{Bits\quad Bits-33\_inv}} & \texttt{CI} & \texttt{LHS} & \texttt{RHS} & \texttt{LT} & \texttt{AND} & \texttt{XOR} & \multicolumn{2}{l}{\texttt{Log2Floor}} & \texttt{Pow} & \multicolumn{2}{l}{\texttt{LHS\_inv}} & \multicolumn{2}{l}{RHS\_inv} & & & & & \\ \bottomrule
Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & & \\ \midrule
Program & \multicolumn{3}{l}{Address} & & \multicolumn{2}{l}{Instruction} & \multicolumn{4}{l}{LookupMultiplicity} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & \\
Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{PI} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB7} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMP} & \texttt{RAMV} \\
OpStack & \texttt{CLK} & \texttt{clk\_di} & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & & \texttt{OSP} & \texttt{OSV} & & & & & \\
RAM & \texttt{CLK} & \texttt{clk\_di} & & \texttt{PI} & & \texttt{bcpc0} & \multicolumn{2}{l}{\texttt{bcpc1}} & & & & & & & & & & \multicolumn{3}{l}{\texttt{RAMP}DiffInv} & \texttt{RAMP} & \texttt{RAMV} \\
JumpStack & \texttt{CLK} & \texttt{clk\_di} & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\
Hash & \multicolumn{4}{l}{RoundNumber} & \texttt{CI} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{r}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\
U32 & \texttt{CF} & \multicolumn{3}{l}{\texttt{Bits\quad Bits-33\_inv}} & \texttt{CI} & \texttt{LHS} & \texttt{RHS} & \texttt{LT} & \texttt{AND} & \texttt{XOR} & \multicolumn{2}{l}{\texttt{Log2Floor}} & \texttt{Pow} & \multicolumn{2}{l}{\texttt{LHS\_inv}} & \multicolumn{2}{l}{RHS\_inv} & & & & & \\ \bottomrule
\end{tabular}
} %end scalebox
\begin{tikzpicture}[remember picture, overlay]
\node[anchor=south west,inner sep=0] at (5,-10.6) {\includegraphics[keepaspectratio,width=0.4\textwidth]{src/img/aet-relations.pdf}};
\node[anchor=south west,inner sep=0] at (4,-11) {\includegraphics[keepaspectratio,width=0.45\textwidth]{src/img/aet-relations.pdf}};
\end{tikzpicture}
\begin{minipage}[t][0.6\textheight][s]{0.3\textwidth}
\vfill
Expand All @@ -118,15 +117,14 @@
\begin{tabular}{lrrr}
\toprule
& base & ext & $\sum$ \\ \midrule
Program & 3 & 1 & 4 \\
Instruction & 4 & 2 & 6 \\
Program & 4 & 1 & 5 \\
Processor & 44 & 13 & 57 \\
OpStack & 5 & 2 & 7 \\
RAM & 8 & 6 & 14 \\
JumpStack & 6 & 2 & 8 \\
Hash & 50 & 3 & 53 \\
U32 & 14 & 1 & 15 \\ \bottomrule\bottomrule
$\sum$ & 134 & 30 & 164
$\sum$ & 131 & 28 & 159
\end{tabular}
\end{minipage}%
\hfill%
Expand All @@ -149,16 +147,15 @@
\begin{tabular}{lrrrrr}
\toprule
& init & cons & trans & term & $\sum$ \\ \midrule
Program & 2 & 1 & 3 & 0 & 6 \\
Instruction & 3 & 1 & 5 & 0 & 9 \\
Program & 2 & 1 & 3 & & 6 \\
Processor & 39 & 12 & 77 & 2 & 130 \\
OpStack & 5 & 0 & 6 & 0 & 11 \\
Ram & 8 & 0 & 14 & 1 & 23 \\
JumpStack & 6 & 0 & 8 & 0 & 14 \\
Hash & 5 & 40 & 26 & 0 & 71 \\
OpStack & 5 & & 6 & & 11 \\
Ram & 8 & & 14 & 1 & 23 \\
JumpStack & 6 & & 8 & & 14 \\
Hash & 5 & 40 & 26 & & 71 \\
U32 & 2 & 14 & 22 & 2 & 40 \\
Cross-Table & 0 & 0 & 0 & 1 & 1 \\ \bottomrule\bottomrule
$\sum$ & 70 & 68 & 161 & 6 & 305
Cross-Table & & & & 1 & 1 \\ \bottomrule\bottomrule
$\sum$ & 67 & 67 & 156 & 6 & 296
\end{tabular}
\end{minipage}

Expand Down
1 change: 0 additions & 1 deletion specification/src/SUMMARY.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
- [Arithmetization](arithmetization.md)
+ [Permutation and Evaluation Arguments]()
+ [Program Table](program-table.md)
+ [Instruction Table](instruction-table.md)
+ [Processor Table](processor-table.md)
* [Instruction Groups](instruction-groups.md)
* [Instruction-Specific Transition Constraints](instruction-specific-transition-constraints.md)
Expand Down
54 changes: 23 additions & 31 deletions specification/src/img/aet-relations.ipe
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
<?xml version="1.0"?>
<!DOCTYPE ipe SYSTEM "ipe.dtd">
<ipe version="70218" creator="Ipe 7.2.24">
<info created="D:20200729150742" modified="D:20230119144906"/>
<info created="D:20200729150742" modified="D:20230129181210"/>
<preamble>\usepackage{lmodern}
\renewcommand*\familydefault{\sfdefault}
\usepackage[T1]{fontenc}</preamble>
Expand Down Expand Up @@ -320,23 +320,22 @@ h
<layer name="perm_args"/>
<layer name="multi_perm_arg"/>
<layer name="bezout_args"/>
<view layers="bg table_names eval_args perm_args multi_perm_arg bezout_args" active="perm_args"/>
<view layers="bg table_names eval_args perm_args multi_perm_arg bezout_args" active="table_names"/>
<path layer="bg" fill="white">
80 216 m
80 188 m
80 44 l
280 44 l
280 216 l
280 188 l
h
</path>
<path layer="perm_args" stroke="darkblue" pen="heavier" cap="1" join="1" arrow="fpointed/small" rarrow="pointed/small">
<path layer="perm_args" stroke="darkmagenta" pen="heavier" cap="1" join="1" arrow="fpointed/small" rarrow="pointed/small">
192 138 m
192 154 l
</path>
<text layer="table_names" matrix="1 0 0 1 -16 -32" transformations="translations" pos="208 160" stroke="black" type="label" width="38.135" height="4.407" depth="1.93" halign="center" valign="baseline">processor</text>
<text matrix="1 0 0 1 -16 -32" transformations="translations" pos="208 192" stroke="black" type="label" width="44.029" height="6.531" depth="0" halign="center" valign="baseline">instruction</text>
<text matrix="1 0 0 1 -16 -32" transformations="translations" pos="208 224" stroke="black" type="label" width="34.343" height="4.407" depth="1.93" halign="center" valign="baseline">program</text>
<text matrix="1 0 0 1 -16 -32" transformations="translations" pos="272 224" stroke="darkgray" type="label" width="27.618" height="5.756" depth="1.93" halign="center" valign="baseline">output</text>
<text transformations="translations" pos="128 192" stroke="darkgray" type="label" width="21.42" height="6.538" depth="1.93" halign="center" valign="baseline">input</text>
<text matrix="1 0 0 1 -16 -32" transformations="translations" pos="208 192" stroke="black" type="label" width="34.343" height="4.407" depth="1.93" halign="center" valign="baseline">program</text>
<text matrix="1 0 0 1 -16 -64" transformations="translations" pos="272 224" stroke="darkgray" type="label" width="27.618" height="5.756" depth="1.93" halign="center" valign="baseline">output</text>
<text matrix="1 0 0 1 0 -32" transformations="translations" pos="128 192" stroke="darkgray" type="label" width="21.42" height="6.538" depth="1.93" halign="center" valign="baseline">input</text>
<path layer="eval_args" stroke="darkred" pen="1.6" cap="1" join="1">
176 120 m
176 108 l
Expand All @@ -351,23 +350,19 @@ h
<text matrix="1 0 0 1 -48 -16" transformations="translations" pos="192 96" stroke="black" type="label" width="33.347" height="6.926" depth="1.93" halign="center" valign="baseline">opStack</text>
<text matrix="1 0 0 1 -16 -16" transformations="translations" pos="256 96" stroke="black" type="label" width="21.793" height="6.919" depth="0" halign="center" valign="baseline">RAM</text>
<text matrix="1 0 0 1 -64 16" transformations="translations" pos="160 64" stroke="black" type="label" width="18.901" height="6.919" depth="0" halign="center" valign="baseline">hash</text>
<path layer="eval_args" matrix="1 0 0 1 0 2" stroke="darkred" pen="heavier" cap="1" join="1" arrow="farc/small">
128 184 m
128 132 l
128 128
132 128 c
168 128 l
</path>
<path matrix="1 0 0 1 0 2" stroke="darkred" pen="heavier" cap="1" join="1" rarrow="arc/small">
256 184 m
256 132 l
256 128
252 128 c
216 128 l
</path>
<path matrix="1 0 0 1 0 2" stroke="darkred" pen="heavier" cap="1" join="1" arrow="fnormal/small">
192 184 m
192 168 l
<path layer="eval_args" stroke="darkred" pen="heavier" cap="1" join="1" arrow="farc/small">
128 154 m
128 134 l
128 130
132 130 c
168 130 l
</path>
<path stroke="darkred" pen="heavier" cap="1" join="1" rarrow="arc/small">
256 154 m
256 134 l
256 130
252 130 c
216 130 l
</path>
<path layer="perm_args" stroke="darkblue" pen="heavier" cap="1" join="1" arrow="pointed/small" rarrow="pointed/small">
192 124 m
Expand All @@ -393,13 +388,10 @@ h
144 96 c
144 92 l
</path>
<path layer="eval_args" matrix="1 0 0 1 16 10" stroke="darkred" fill="darkred" pen="heavier" cap="1" join="1">
<path layer="eval_args" matrix="1 0 0 1 40 -46" stroke="darkred" fill="white" pen="heavier" cap="1" join="1">
1.20123 0 0 1.20123 176 176 e
</path>
<path matrix="1 0 0 1 40 -46" stroke="darkred" fill="white" pen="heavier" cap="1" join="1">
1.20123 0 0 1.20123 176 176 e
</path>
<path matrix="1 0 0 1 -48 10" stroke="darkred" fill="darkred" pen="heavier" cap="1" join="1">
<path matrix="1 0 0 1 -48 -22" stroke="darkred" fill="darkred" pen="heavier" cap="1" join="1">
1.20123 0 0 1.20123 176 176 e
</path>
<path stroke="darkred" pen="heavier" cap="1" join="1" arrow="farc/small" rarrow="farc/small">
Expand Down
Binary file modified specification/src/img/aet-relations.pdf
View file
Binary file not shown.
Binary file modified specification/src/img/aet-relations.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading

0 comments on commit 543327a

Please sign in to comment.