Skip to content

Commit

Permalink
perf: Sum mutually exclusive constraints
Browse files Browse the repository at this point in the history 
Both instructions `swap` and `dup` have many constraints that are
mutually exclusive. It is possible to sum mutually exclusive constraints
without impacting either completeness or soundness, while reducing the
the performance impact of the two instructions.
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed May 30, 2024
1 parent 98dbd9f commit 3e96fac
Show file tree
Hide file tree
Showing 3 changed files with 147 additions and 147 deletions.
12 changes: 6 additions & 6 deletions specification/src/arithmetization-overview.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,9 @@
| [CascadeTable](cascade-table.md) | 6 | 2 | 12 |
| [LookupTable](lookup-table.md) | 4 | 2 | 10 |
| [U32Table](u32-table.md) | 10 | 1 | 13 |
| DegreeLowering | 223 | 36 | 331 |
| DegreeLowering | 216 | 36 | 324 |
| Randomizers | 0 | 1 | 3 |
| **TOTAL** | **372** | **86** | **630** |
| **TOTAL** | **365** | **86** | **623** |
<!-- auto-gen info stop -->

## Constraints
Expand All @@ -34,7 +34,7 @@ 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 |
| [ProcessorTable](processor-table.md) | 29 | 10 | 49 | 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 |
Expand All @@ -43,14 +43,14 @@ Before automatic degree lowering:
| [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** |
| **TOTAL** | **79** | **76** | **158** | **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 | 258 | 1 |
| [ProcessorTable](processor-table.md) | 31 | 10 | 231 | 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 |
Expand All @@ -59,5 +59,5 @@ After automatically lowering degree to 4:
| [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** | **81** | **94** | **417** | **23** |
| **TOTAL** | **81** | **94** | **390** | **23** |
<!-- auto-gen info stop -->
188 changes: 94 additions & 94 deletions specification/src/instruction-specific-transition-constraints.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,41 +27,41 @@ In addition to its [instruction groups](instruction-groups.md), this instruction

### Description

1. If `i` is 0, then `st0` is put on top of the stack.
1. If `i` is 1, then `st1` is put on top of the stack.
1. If `i` is 2, then `st2` is put on top of the stack.
1. If `i` is 3, then `st3` is put on top of the stack.
1. If `i` is 4, then `st4` is put on top of the stack.
1. If `i` is 5, then `st5` is put on top of the stack.
1. If `i` is 6, then `st6` is put on top of the stack.
1. If `i` is 7, then `st7` is put on top of the stack.
1. If `i` is 8, then `st8` is put on top of the stack.
1. If `i` is 9, then `st9` is put on top of the stack.
1. If `i` is 10, then `st10` is put on top of the stack.
1. If `i` is 11, then `st11` is put on top of the stack.
1. If `i` is 12, then `st12` is put on top of the stack.
1. If `i` is 13, then `st13` is put on top of the stack.
1. If `i` is 14, then `st14` is put on top of the stack.
1. If `i` is 15, then `st15` is put on top of the stack.
1. If `i` is 0, then `st0` is put on top of the stack and <br />
if `i` is 1, then `st1` is put on top of the stack and <br />
if `i` is 2, then `st2` is put on top of the stack and <br />
if `i` is 3, then `st3` is put on top of the stack and <br />
if `i` is 4, then `st4` is put on top of the stack and <br />
if `i` is 5, then `st5` is put on top of the stack and <br />
if `i` is 6, then `st6` is put on top of the stack and <br />
if `i` is 7, then `st7` is put on top of the stack and <br />
if `i` is 8, then `st8` is put on top of the stack and <br />
if `i` is 9, then `st9` is put on top of the stack and <br />
if `i` is 10, then `st10` is put on top of the stack and <br />
if `i` is 11, then `st11` is put on top of the stack and <br />
if `i` is 12, then `st12` is put on top of the stack and <br />
if `i` is 13, then `st13` is put on top of the stack and <br />
if `i` is 14, then `st14` is put on top of the stack and <br />
if `i` is 15, then `st15` is put on top of the stack.

### Polynomials

1. `ind_0(hv3, hv2, hv1, hv0)·(st0' - st0)`
1. `ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`
1. `ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`
1. `ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`
1. `ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`
1. `ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`
1. `ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`
1. `ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`
1. `ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`
1. `ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`
1. `ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`
1. `ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`
1. `ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`
1. `ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`
1. `ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`
1. `ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)`
1. `ind_0(hv3, hv2, hv1, hv0)·(st0' - st0)`<br />
`+ ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`<br />
`+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`<br />
`+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`<br />
`+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`<br />
`+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`<br />
`+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`<br />
`+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`<br />
`+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`<br />
`+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`<br />
`+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`<br />
`+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`<br />
`+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`<br />
`+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`<br />
`+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`<br />
`+ ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)`

## Instruction `swap` + `i`

Expand All @@ -70,37 +70,37 @@ In addition to its [instruction groups](instruction-groups.md), this instruction

### Description

1. Argument `i` is not 0.
1. If `i` is 1, then `st0` is moved into `st1`.
1. If `i` is 2, then `st0` is moved into `st2`.
1. If `i` is 3, then `st0` is moved into `st3`.
1. If `i` is 4, then `st0` is moved into `st4`.
1. If `i` is 5, then `st0` is moved into `st5`.
1. If `i` is 6, then `st0` is moved into `st6`.
1. If `i` is 7, then `st0` is moved into `st7`.
1. If `i` is 8, then `st0` is moved into `st8`.
1. If `i` is 9, then `st0` is moved into `st9`.
1. If `i` is 10, then `st0` is moved into `st10`.
1. If `i` is 11, then `st0` is moved into `st11`.
1. If `i` is 12, then `st0` is moved into `st12`.
1. If `i` is 13, then `st0` is moved into `st13`.
1. If `i` is 14, then `st0` is moved into `st14`.
1. If `i` is 15, then `st0` is moved into `st15`.
1. If `i` is 1, then `st1` is moved into `st0`.
1. If `i` is 2, then `st2` is moved into `st0`.
1. If `i` is 3, then `st3` is moved into `st0`.
1. If `i` is 4, then `st4` is moved into `st0`.
1. If `i` is 5, then `st5` is moved into `st0`.
1. If `i` is 6, then `st6` is moved into `st0`.
1. If `i` is 7, then `st7` is moved into `st0`.
1. If `i` is 8, then `st8` is moved into `st0`.
1. If `i` is 9, then `st9` is moved into `st0`.
1. If `i` is 10, then `st10` is moved into `st0`.
1. If `i` is 11, then `st11` is moved into `st0`.
1. If `i` is 12, then `st12` is moved into `st0`.
1. If `i` is 13, then `st13` is moved into `st0`.
1. If `i` is 14, then `st14` is moved into `st0`.
1. If `i` is 15, then `st15` is moved into `st0`.
1. Argument `i` is not 0 and <br />
if `i` is 1, then `st0` is moved into `st1` and <br />
if `i` is 2, then `st0` is moved into `st2` and <br />
if `i` is 3, then `st0` is moved into `st3` and <br />
if `i` is 4, then `st0` is moved into `st4` and <br />
if `i` is 5, then `st0` is moved into `st5` and <br />
if `i` is 6, then `st0` is moved into `st6` and <br />
if `i` is 7, then `st0` is moved into `st7` and <br />
if `i` is 8, then `st0` is moved into `st8` and <br />
if `i` is 9, then `st0` is moved into `st9` and <br />
if `i` is 10, then `st0` is moved into `st10` and <br />
if `i` is 11, then `st0` is moved into `st11` and <br />
if `i` is 12, then `st0` is moved into `st12` and <br />
if `i` is 13, then `st0` is moved into `st13` and <br />
if `i` is 14, then `st0` is moved into `st14` and <br />
if `i` is 15, then `st0` is moved into `st15`.
1. If `i` is 1, then `st1` is moved into `st0` and <br />
if `i` is 2, then `st2` is moved into `st0` and <br />
if `i` is 3, then `st3` is moved into `st0` and <br />
if `i` is 4, then `st4` is moved into `st0` and <br />
if `i` is 5, then `st5` is moved into `st0` and <br />
if `i` is 6, then `st6` is moved into `st0` and <br />
if `i` is 7, then `st7` is moved into `st0` and <br />
if `i` is 8, then `st8` is moved into `st0` and <br />
if `i` is 9, then `st9` is moved into `st0` and <br />
if `i` is 10, then `st10` is moved into `st0` and <br />
if `i` is 11, then `st11` is moved into `st0` and <br />
if `i` is 12, then `st12` is moved into `st0` and <br />
if `i` is 13, then `st13` is moved into `st0` and <br />
if `i` is 14, then `st14` is moved into `st0` and <br />
if `i` is 15, then `st15` is moved into `st0`.
1. If `i` is not 1, then `st1` does not change.
1. If `i` is not 2, then `st2` does not change.
1. If `i` is not 3, then `st3` does not change.
Expand All @@ -121,37 +121,37 @@ In addition to its [instruction groups](instruction-groups.md), this instruction

### Polynomials

1. `ind_0(hv3, hv2, hv1, hv0)`
1. `ind_1(hv3, hv2, hv1, hv0)·(st1' - st0)`
1. `ind_2(hv3, hv2, hv1, hv0)·(st2' - st0)`
1. `ind_3(hv3, hv2, hv1, hv0)·(st3' - st0)`
1. `ind_4(hv3, hv2, hv1, hv0)·(st4' - st0)`
1. `ind_5(hv3, hv2, hv1, hv0)·(st5' - st0)`
1. `ind_6(hv3, hv2, hv1, hv0)·(st6' - st0)`
1. `ind_7(hv3, hv2, hv1, hv0)·(st7' - st0)`
1. `ind_8(hv3, hv2, hv1, hv0)·(st8' - st0)`
1. `ind_9(hv3, hv2, hv1, hv0)·(st9' - st0)`
1. `ind_10(hv3, hv2, hv1, hv0)·(st10' - st0)`
1. `ind_11(hv3, hv2, hv1, hv0)·(st11' - st0)`
1. `ind_12(hv3, hv2, hv1, hv0)·(st12' - st0)`
1. `ind_13(hv3, hv2, hv1, hv0)·(st13' - st0)`
1. `ind_14(hv3, hv2, hv1, hv0)·(st14' - st0)`
1. `ind_15(hv3, hv2, hv1, hv0)·(st15' - st0)`
1. `ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`
1. `ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`
1. `ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`
1. `ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`
1. `ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`
1. `ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`
1. `ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`
1. `ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`
1. `ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`
1. `ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`
1. `ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`
1. `ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`
1. `ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`
1. `ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`
1. `ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)`
1. `ind_0(hv3, hv2, hv1, hv0)`<br />
`+ ind_1(hv3, hv2, hv1, hv0)·(st1' - st0)`<br />
`+ ind_2(hv3, hv2, hv1, hv0)·(st2' - st0)`<br />
`+ ind_3(hv3, hv2, hv1, hv0)·(st3' - st0)`<br />
`+ ind_4(hv3, hv2, hv1, hv0)·(st4' - st0)`<br />
`+ ind_5(hv3, hv2, hv1, hv0)·(st5' - st0)`<br />
`+ ind_6(hv3, hv2, hv1, hv0)·(st6' - st0)`<br />
`+ ind_7(hv3, hv2, hv1, hv0)·(st7' - st0)`<br />
`+ ind_8(hv3, hv2, hv1, hv0)·(st8' - st0)`<br />
`+ ind_9(hv3, hv2, hv1, hv0)·(st9' - st0)`<br />
`+ ind_10(hv3, hv2, hv1, hv0)·(st10' - st0)`<br />
`+ ind_11(hv3, hv2, hv1, hv0)·(st11' - st0)`<br />
`+ ind_12(hv3, hv2, hv1, hv0)·(st12' - st0)`<br />
`+ ind_13(hv3, hv2, hv1, hv0)·(st13' - st0)`<br />
`+ ind_14(hv3, hv2, hv1, hv0)·(st14' - st0)`<br />
`+ ind_15(hv3, hv2, hv1, hv0)·(st15' - st0)`
1. `ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`<br />
`+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`<br />
`+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`<br />
`+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`<br />
`+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`<br />
`+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`<br />
`+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`<br />
`+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`<br />
`+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`<br />
`+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`<br />
`+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`<br />
`+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`<br />
`+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`<br />
`+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`<br />
`+ ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)`
1. `(1 - ind_1(hv3, hv2, hv1, hv0))·(st1' - st1)`
1. `(1 - ind_2(hv3, hv2, hv1, hv0))·(st2' - st2)`
1. `(1 - ind_3(hv3, hv2, hv1, hv0))·(st3' - st3)`
Expand Down
Loading

0 comments on commit 3e96fac

Please sign in to comment.