doc: add arithmetization overview page

Add 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.
TritonVM · May 8, 2024 · c5b7eec · c5b7eec
2 parents 6e5443e + 2811b3b
commit c5b7eec
Show file tree

Hide file tree

Showing 6 changed files with 414 additions and 1 deletion.
diff --git a/Cargo.toml b/Cargo.toml
@@ -29,6 +29,7 @@ colored = "2.1"
 clap = { version = "4", features = ["derive", "cargo", "wrap_help", "unicode", "string"] }
 criterion = { version = "0.5", features = ["html_reports"] }
 directories = "5"
+fs-err = "2.11.0"
 get-size = "0.1.4"
 itertools = "0.12"
 lazy_static = "1.4"

diff --git a/specification/src/SUMMARY.md b/specification/src/SUMMARY.md
@@ -5,6 +5,7 @@
     + [Registers](registers.md)
     + [Instructions](instructions.md)
 - [Arithmetization](arithmetization.md)
+    + [Arithmetization Overview](arithmetization-overview.md)
     + [Program Table](program-table.md)
     + [Processor Table](processor-table.md)
         * [Instruction Groups](instruction-groups.md)

diff --git a/specification/src/arithmetization-overview.md b/specification/src/arithmetization-overview.md
@@ -0,0 +1,63 @@
+# Arithmetization Overview
+
+## Tables
+
+<!-- auto-gen info spec_has_correct_table_overview -->
+<!-- To reproduce this code, please run `cargo run spec_has_correct_table_overview`. -->
+| table name                                 | #main cols | #aux cols | total width |
+|:-------------------------------------------|-----------:|----------:|------------:|
+| [ProgramTable](program-table.md)           |          7 |         3 |          16 |
+| [ProcessorTable](processor-table.md)       |         39 |        11 |          72 |
+| [OpStackTable](operational-stack-table.md) |          4 |         2 |          10 |
+| [RamTable](random-access-memory-table.md)  |          7 |         6 |          25 |
+| [JumpStackTable](jump-stack-table.md)      |          5 |         2 |          11 |
+| [HashTable](hash-table.md)                 |         67 |        20 |         127 |
+| [CascadeTable](cascade-table.md)           |          6 |         2 |          12 |
+| [LookupTable](lookup-table.md)             |          4 |         2 |          10 |
+| [U32Table](u32-table.md)                   |         10 |         1 |          13 |
+| DegreeLowering                             |        217 |        36 |         325 |
+| Randomizers                                |          0 |         1 |           3 |
+| **TOTAL**                                  |    **366** |    **86** |     **624** |
+<!-- auto-gen info stop -->
+
+## Constraints
+
+The following table captures the state of affairs in terms of constraints before automatic degree lowering.
+In particular, automatic degree lowering introduces new columns, modifies the constraint set (in a way that
+is equivalent to what was there before), and lowers the constraints' maximal degree.
+
+<!-- auto-gen info spec_has_correct_constraints_overview -->
+<!-- To reproduce this code, please run `cargo run spec_has_correct_constraints_overview`. -->
+
+Before automatic degree lowering:
+
+| table name                                     | #initial | #consistency | #transition | #terminal | max degree |
+|:-----------------------------------------------|---------:|-------------:|------------:|----------:|-----------:|
+| [ProgramTable](program-table.md)               |        6 |            4 |          10 |         2 |          4 |
+| [ProcessorTable](processor-table.md)           |       29 |           10 |          69 |         1 |         19 |
+| [OpStackTable](operational-stack-table.md)     |        3 |            0 |           5 |         0 |          4 |
+| [RamTable](random-access-memory-table.md)      |        7 |            0 |          12 |         1 |          5 |
+| [JumpStackTable](jump-stack-table.md)          |        6 |            0 |           6 |         0 |          4 |
+| [HashTable](hash-table.md)                     |       22 |           45 |          47 |         2 |          9 |
+| [CascadeTable](cascade-table.md)               |        2 |            1 |           3 |         0 |          4 |
+| [LookupTable](lookup-table.md)                 |        3 |            1 |           4 |         1 |          3 |
+| [U32Table](u32-table.md)                       |        1 |           15 |          22 |         2 |         12 |
+| [Grand Cross-Table Argument](table-linking.md) |        0 |            0 |           0 |        14 |          1 |
+| **TOTAL**                                      |   **79** |       **76** |     **178** |    **23** |     **19** |
+
+After automatically lowering degree to 4:
+
+| table name                                     | #initial | #consistency | #transition | #terminal |
+|:-----------------------------------------------|---------:|-------------:|------------:|----------:|
+| [ProgramTable](program-table.md)               |        6 |            4 |          10 |         2 |
+| [ProcessorTable](processor-table.md)           |       31 |           10 |         252 |         1 |
+| [OpStackTable](operational-stack-table.md)     |        3 |            0 |           5 |         0 |
+| [RamTable](random-access-memory-table.md)      |        7 |            0 |          13 |         1 |
+| [JumpStackTable](jump-stack-table.md)          |        6 |            0 |           6 |         0 |
+| [HashTable](hash-table.md)                     |       22 |           52 |          84 |         2 |
+| [CascadeTable](cascade-table.md)               |        2 |            1 |           3 |         0 |
+| [LookupTable](lookup-table.md)                 |        3 |            1 |           4 |         1 |
+| [U32Table](u32-table.md)                       |        1 |           26 |          34 |         2 |
+| [Grand Cross-Table Argument](table-linking.md) |        0 |            0 |           0 |        14 |
+| **TOTAL**                                      |  **158** |      **152** |     **356** |    **46** |
+<!-- auto-gen info stop -->
diff --git a/triton-vm/Cargo.toml b/triton-vm/Cargo.toml
@@ -42,6 +42,7 @@ unicode-width.workspace = true
 [dev-dependencies]
 assert2.workspace = true
 cargo-husky.workspace = true
+fs-err.workspace = true
 pretty_assertions.workspace = true
 proptest.workspace = true
 proptest-arbitrary-interop.workspace = true

diff --git a/triton-vm/src/table/constraint_circuit.rs b/triton-vm/src/table/constraint_circuit.rs
@@ -912,7 +912,7 @@ impl<II: InputIndicator> ConstraintCircuitMonad<II> {
     }
 
     /// Returns the maximum degree of all circuits in the multicircuit.
-    fn multicircuit_degree(multicircuit: &[ConstraintCircuitMonad<II>]) -> isize {
+    pub(crate) fn multicircuit_degree(multicircuit: &[ConstraintCircuitMonad<II>]) -> isize {
         multicircuit
             .iter()
             .map(|circuit| circuit.circuit.borrow().degree())