The "enf match" pattern and the current chiplets design
- 主要語言
- Rust
- 星號
- 96
- 分支
- 39
- PR 合併指標
- 30 天內沒有已合併 PR
描述
## `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.
貢獻指南
研究方向
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.
由索引模型根據 Issue 內容生成。
評估
- 技術堆疊
- rust
- 領域
- compilers
- Issue 類型
- 重構
- 難度
- 5/5
- 預估耗時
- 一週以上
- 活躍度
- 停滯
- 描述清晰度
- 需要釐清
- 新手友好度
- 25/100