Skip to content

Commit

Permalink
add u32 instructions
Browse files Browse the repository at this point in the history 
- ✨ add new instructions:
  - ✨ `log_2_floor` – rounded-down log₂
  - ✨ `pow` – exponentiation
- ♻️ replace pseudo instructions with proper instructions:
  - ♻️ `lt` – less than
  - ♻️ `and` – bit-wise and
  - ♻️ `xor` – bit-wise xor
  - ♻️ `div` – integer division with remainder
- 🗑 remove pseudo instructions:
  - 🗑 `lte` – less than or equal
  - 🗑 `reverse` – bit reversal
  - 🗑 `split_assert` – the deterministic `split`
- ♻️ make instruction `split` deterministic
- ♻️ replace instruction `lsb` with deterministic pseudo instruction
- ♻️ pseudo instruction `is_u32` returns result instead of crashing VM
- ✨ introduce U32 Table to efficiently arithmetize new instructions
  • Loading branch information
@jan-ferdinand
jan-ferdinand authored Jan 12, 2023
2 parents b2b0d84 + d68e551 commit 1f3eae8
Show file tree
Hide file tree
Showing 33 changed files with 2,535 additions and 799 deletions.
14 changes: 13 additions & 1 deletion constraint-evaluation-generator/src/main.rs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use itertools::Itertools;
use std::collections::HashSet;
use std::process::Command;

use itertools::Itertools;
use twenty_first::shared_math::b_field_element::BFieldElement;
use twenty_first::shared_math::x_field_element::XFieldElement;

Expand All @@ -16,6 +16,7 @@ use triton_vm::table::op_stack_table::ExtOpStackTable;
use triton_vm::table::processor_table::ExtProcessorTable;
use triton_vm::table::program_table::ExtProgramTable;
use triton_vm::table::ram_table::ExtRamTable;
use triton_vm::table::u32_table::ExtU32Table;

fn main() {
println!("Generate those constraint evaluators!");
Expand Down Expand Up @@ -98,6 +99,17 @@ fn main() {
);
write(&table_name_snake, source_code);

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

if let Err(fmt_failed) = Command::new("cargo").arg("fmt").output() {
println!("cargo fmt failed: {}", fmt_failed);
}
Expand Down
21 changes: 17 additions & 4 deletions opcodes.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,14 @@ class Instruction(IntEnum):
Add = auto()
Mul = auto()
Invert = auto()
Split = auto()
Eq = auto()
Lsb = auto()
Split = auto()
Lt = auto()
And = auto()
Xor = auto()
Log2Floor = auto()
Pow = auto()
Div = auto()
XxAdd = auto()
XxMul = auto()
XInvert = auto()
Expand All @@ -35,6 +40,7 @@ class Instruction(IntEnum):
class InstructionBucket(IntFlag):
HasArg = auto()
ShrinkStack = auto()
U32 = auto()

# ===

Expand All @@ -44,6 +50,9 @@ def in_bucket(instruction_bucket, instruction):
if instruction_bucket == InstructionBucket.ShrinkStack:
return instruction in [Instruction.Pop, Instruction.Skiz, Instruction.Assert, 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,
Instruction.Pow, Instruction.Div, Instruction.Split]
return False

def flag_set(instruction):
Expand All @@ -60,10 +69,14 @@ def opcode(instruction):

def print_all_opcodes():
for instruction in Instruction:
print(f"{opcode(instruction):>02} {str(instruction)}")
opc = opcode(instruction)
print(f"{opc:> 3} {opc:>07b} {str(instruction)}")

def print_max_opcode():
print(f"highest opcode: {max([opcode(instruction) for instruction in Instruction])}")
max_opc = max([opcode(instruction) for instruction in Instruction])
print(f"highest opcode: {max_opc}")
print(f"#ibs: {len(bin(max_opc)[2:])}")


# ===

Expand Down
Binary file modified specification/cheatsheet.pdf
View file
Binary file not shown.
140 changes: 64 additions & 76 deletions specification/cheatsheet.tex
View file

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions specification/src/SUMMARY.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
+ [Random Access Memory Table](random-access-memory-table.md)
+ [Jump Stack Table](jump-stack-table.md)
+ [Hash Table](hash-table.md)
+ [U32 Table](u32-table.md)
+ [Memory-Consistency](memory-consistency.md)
* [Contiguity of Memory-Pointer Regions](contiguity-of-memory-pointer-regions.md)
* [Clock Jump Differences and Inner Sorting](clock-jump-differences-and-inner-sorting.md)
Expand Down
6 changes: 3 additions & 3 deletions specification/src/arithmetization.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ In the nomenclature of this note, a trace is a special kind of table that tracks

## Algebraic Execution Tables

There are 7 Arithmetic Execution Tables in TritonVM.
There are 8 Arithmetic Execution Tables in TritonVM.
Their relation is described by below figure.
A red arrow indicates an Evaluation Argument, a blue arrow indicates a Permutation Argument, and the green arrow is the Bézout Argument.

Expand All @@ -34,7 +34,7 @@ Together, these columns are referred to as table's _base_ columns, and make up t

The entries of a table's columns corresponding to Permutation, Evaluation, and Bézout Arguments are elements from the _X-field_ $\mathbb{F}_{p^3}$.
These columns are referred to as a table's _extension_ columns, both because the entries are elements of the X-field and because the entries can only be computed using the base tables, through an _extension_ process.
Collectively, a table's base columns with its entries interpreted as elements of the X-field and the table's extension columns make up the _extension table_.
Together, these columns are referred to as a table's _extension_ columns, and make up the _extension table_.

### Padding

Expand All @@ -44,7 +44,7 @@ The height $h$ of the longest AET determines the padded height for all tables, w

## Arithmetic Intermediate Representation

For each table, up to three lists containing constraints of different type are given:
For each table, up to four lists containing constraints of different type are given:
1. Initial Constraints, defining values in a table's first row,
1. Consistency Constraints, establishing consistency within any given row,
1. Transition Constraints, establishing the consistency of two consecutive rows in relation to each other, and
Expand Down
70 changes: 43 additions & 27 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:20221103102957"/>
<info created="D:20200729150742" modified="D:20221229140740"/>
<preamble>\usepackage{lmodern}
\renewcommand*\familydefault{\sfdefault}
\usepackage[T1]{fontenc}</preamble>
Expand Down Expand Up @@ -320,14 +320,18 @@ 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="eval_args"/>
<path layer="bg" matrix="1 0 0 1 0 12" fill="white">
108 204 m
108 32 l
280 32 l
280 204 l
<view layers="bg table_names eval_args perm_args multi_perm_arg bezout_args" active="bg"/>
<path layer="bg" fill="white">
80 216 m
80 44 l
280 44 l
280 216 l
h
</path>
<path layer="eval_args" stroke="darkred" pen="heavier" cap="1" join="1">
172 124 m
172 112 l
</path>
<path layer="perm_args" stroke="darkblue" pen="heavier" cap="1" join="1" arrow="fpointed/small" rarrow="pointed/small">
192 138 m
192 154 l
Expand All @@ -340,7 +344,7 @@ h
<text matrix="1 0 0 1 64 -16" transformations="translations" pos="128 96" stroke="black" type="label" width="44.085" height="6.926" depth="1.93" halign="center" valign="baseline">jumpStack</text>
<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 -32 32" transformations="translations" pos="160 64" stroke="black" type="label" width="18.901" height="6.919" depth="0" halign="center" valign="baseline">hash</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
Expand Down Expand Up @@ -392,29 +396,29 @@ h
<path matrix="1 0 0 1 -48 10" stroke="darkred" fill="darkred" pen="heavier" cap="1" join="1">
1.20123 0 0 1.20123 176 176 e
</path>
<path matrix="1 0 0 1 0 4" stroke="darkred" pen="heavier" cap="1" join="1" rarrow="farc/small">
176 120 m
176 116 l
176 112
172 112 c
136 112 l
132 112
132 108 c
132 104 l
<path stroke="darkred" pen="heavier" cap="1" join="1" rarrow="farc/small">
176 124 m
176 108 l
176 104
172 104 c
102 104 l
98 104
98 100 c
98 92 l
</path>
<path stroke="darkred" pen="heavier" cap="1" join="1" rarrow="farc/small">
124 108 m
124 116 l
124 120
128 120 c
160 120 l
164 120
168 124 c
</path>
<path matrix="1 0 0 1 -8 -52" stroke="darkred" fill="white" pen="heavier" cap="1" join="1">
94 92 m
94 104 l
94 108
98 108 c
168 108 l
172 108
172 112 c
</path>
<path matrix="1 0 0 1 -4 -52" 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 -44 -68" stroke="darkred" fill="white" pen="heavier" cap="1" join="1">
<path matrix="1 0 0 1 -78 -84" stroke="darkred" fill="white" pen="heavier" cap="1" join="1">
1.20123 0 0 1.20123 176 176 e
</path>
<path layer="multi_perm_arg" stroke="darkblue" pen="heavier" cap="1" join="1" rarrow="fpointed/small">
Expand Down Expand Up @@ -451,5 +455,17 @@ h
160 100 m
8 0 0 -8 160 92 152 92 a
</path>
<text layer="table_names" transformations="translations" pos="96 128" stroke="black" type="label" width="15.11" height="6.531" depth="0" halign="center" valign="baseline">u32</text>
<path layer="perm_args" stroke="darkblue" pen="heavier" cap="1" join="1" arrow="fpointed/small" rarrow="fpointed/small">
96 124 m
96 120 l
96 116
100 116 c
156 116 l
160 116
160 120 c
160 124
169.127 126.735 c
</path>
</page>
</ipe>
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.
9 changes: 7 additions & 2 deletions specification/src/instruction-groups.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,9 +55,14 @@ A summary of all instructions and which groups they are part of is given in the
| `add` | | x | | x | | | | | | | | | | x | |
| `mul` | | x | | x | | | | | | | | | | x | |
| `invert` | | x | | x | | | | | | | x | | | | |
| `split` | | x | | x | | x | | | | | | | | | |
| `eq` | | x | | x | | | | | | | | | | x | |
| `lsb` | | x | | x | | x | | | | | | | | | |
| `split` | | x | | x | | x | | | | | | | | | |
| `lt` | | x | | x | | | | | | | | | | x | |
| `and` | | x | | x | | | | | | | | | | x | |
| `xor` | | x | | x | | | | | | | | | | x | |
| `log_2_floor` | | x | | x | | | | | | | x | | | | |
| `pow` | | x | | x | | | | | | | | | | x | |
| `div` | | x | | x | | | | | | x | | | | | |
| `xxadd` | | x | | x | | | | | | x | | | | | |
| `xxmul` | | x | | x | | | | | | x | | | | | |
| `xinvert` | | x | | x | | | | | | x | | | | | |
Expand Down
Loading

0 comments on commit 1f3eae8

Please sign in to comment.