search

TritonVM / triton-vm

Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system.
https://triton-vm.org
Apache License 2.0
223 stars 35 forks source link

Arithmetization Overview #275

Closed aszepieniec closed 1 month ago

aszepieniec commented 1 month ago

Adds a new page to the specification: arithmetization overview. It contains two automatically generated tables, one summarizing the various (algebraic execution) tables and their columns; the other summarizing the various constraints. The code for generating these tables lives in tests, which also check that the specification is in sync with what was generated.

jan-ferdinand commented 1 month ago

I notice that some lines go far beyond the agreed-upon limit of 100 characters. You can set a ruler as described here. This makes any such violations immediately obvious.

aszepieniec commented 1 month ago

I notice that some lines go far beyond the agreed-upon limit of 100 characters. You can set a ruler as described here. This makes any such violations immediately obvious.

What's the policy about breaking lines containing formatted strings? IMHO, that reduces readability.

aszepieniec commented 1 month ago

What's the policy about breaking lines containing formatted strings? IMHO, that reduces readability.

I guess we don't have much flexibility for all other types of lines because rust formatter.

jan-ferdinand commented 1 month ago

I guess we don't have much flexibility for all other types of lines because rust formatter.

Rust formatter is quite flexible, of course.

What's the policy about breaking lines containing formatted strings? IMHO, that reduces readability.

I don't think we have a policy. In other places I played around with things until it felt nice. :shrug:

aszepieniec commented 1 month ago

We speculated in the office that the failing test could be due to some machine-dependent execution path in the automatic degree-lowering process. Here is a data point in support of that conclusion.

I just ran all tests on my home desktop and lo and behold, spec_has_correct_table_overview fails complaining that the table in the spec is not correct. For reference, here is the table in the spec from the PR, which was produced from my laptop:

table name #main cols #aux cols total width
ProgramTable 7 3 16
ProcessorTable 39 11 72
OpStack 4 2 10
RamTable 7 6 25
JumpStackTable 5 2 11
Hash 67 20 127
Cascade 6 2 12
LookupTable 4 2 10
U32Table 10 1 13
DegreeLowering 220 36 328
Randomizers 0 1 3
TOTAL 369 86 627

And here is what failing test spec_has_correct_table_overview thinks it should be (when run on my home desktop computer):

table name #main cols #aux cols total width
ProgramTable 7 3 16
ProcessorTable 39 11 72
OpStack 4 2 10
RamTable 7 6 25
JumpStackTable 5 2 11
Hash 67 20 127
Cascade 6 2 12
LookupTable 4 2 10
U32Table 10 1 13
DegreeLowering 207 33 306
Randomizers 0 1 3
TOTAL 356 83 605