The "enf match" pattern and the current chiplets design
- Lingua principale
- Rust
- Stelle
- 96
- Fork
- 39
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Descrizione
## `enf match`
- `enf match` multiplies each case body by its guard. For
chiplets, those guards are selector products such as `s0 * s1 * (1 - s2)`.
- Every constraint inside the case inherits the guard. If the evaluator itself also uses selector-based
flags, you end up multiplying selectors twice. Algebraically it’s fine, but the polynomials increase in
degree without a simplification pass, this can be problematic.
- This above is not an issue when the constraints within a chiplet are uniform, as in the example of both the hasher and bitwise chiplets'. This can be seen from the official documentation which assumes throughout the chiplet specific constraints a uniform gating by the chipelt's flag selector and hence this is omitted and is implicit in the constraints description of both the hasher and bitwise chiplets.
- The above is an issue for the ACE chiplet (in practice only one constraint involving the $f_{ace,first}^{'}$ flag which can be moved to the preceding chiplet i.e., bitwise), but a bigger issue is the memory chiplet which relies more on the $f_{mem_nl}$ rather than on the memory chiplet flag $f_{mem}$. This is an extreme example of what we can call non-uniform chiplets' constraints.
## Memory chiplet as an example
- Inside memory chiplet constraints we gate most rules with
`flag_not_last_row = s0 * s1 * (1 - s2')`.
- The outer `enf match` guard is `memory_active = s0 * s1 * (1 - s2)`.
- The final multiplier is `memory_active * flag_not_last_row = (s0 * s1 * (1 - s2)) * (s0 * s1 * (1 - s2'))`.
- Now even if we have a “boolean expressions” simplifier pass, we cannot shrink the degree and hence every constraint it touches becomes higher-degree.
- The above could be an acceptable solution, we can even change the definition of `flag_not_last_row` to be the easier-to-reason-about expression `flag_not_last_row = s0 * s1 * (1 - s_2) * (1 - s2') = memory_active * (1 - s2')`. In this case, we restore the uniformity of the constraints and hence the ease of use of the `enf match` pattern. The main hindrance to adopting this fix is the fact that there are a number of constraints of degree 9 gated by `flag_not_last_row`.
## Potential solution
After thinking about this for some time, and given the current syntax, I think that the best way forward is to split the ACE and Memory chiplets' constraints into two sets, a uniform set and non-uniform set in the above definition of uniformity.
The uniform set of constraints can be handled in a straightforward manner using the `enf match` pattern, while the non-uniform ones could be handled using a simple `enf ... when flag` pattern.
Guida per i contributori
Apri la guida per i contributori
Direzione di ricerca
The issue discusses the 'enf match' pattern and its interaction with chiplets like ACE and Memory in the AIR-Script compiler. It mentions selector products, degree inflation, and non-uniform constraints. To start, examine the chiplet implementations in the codebase, particularly the constraint definitions for memory and ACE. Look for the 'enf match' syntax and how flags like 'flag_not_last_row' are used. Understanding the algebraic simplification passes and the current constraint gating logic is essential before proposing a split into uniform and non-uniform constraint sets.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Valutazione
- Stack tecnologico
- rust
- Ambito
- compilers
- Tipo di issue
- Refactoring
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Stato di attività
- Ferma
- Chiarezza
- Da chiarire
- Idoneità per principianti
- 25/100