0xMiden / 0xMiden/air-script

modularity for boundary constraints

未關閉
#240 1 則留言 2 個 reaction 已指派 0 人 在 GitHub 檢視
主要語言
Rust
星號
96
分支
39
PR 合併指標
30 天內沒有已合併 PR

描述

I think we should think through modularity for boundary constraints. Evaluator functions aren't supported for boundary constraints (at least in our current design), and whatever method we use for enforcing boundary constraints in a modular way needs to be able to make use of public inputs. Therefore, enabling evaluator functions for boundary constraints wouldn't be sufficient in itself.

The problem is demonstrated by considering how the top-level Miden VM AIR could look if we define it in a modular way, as shown below. With modularity for boundary constraints, the main AIR definition is ~50 lines and very readable. Without it, we'll have ~100+ constraints in the boundary constraints section, and it will become the main part of the file.

```
use system::system_constraints
use decoder::decoder_constraints
use stack::stack_constraints
use range::range_checker_constraints
use chiplets::chiplet_constraints

def MidenVmAir

# --- Declarations --------------------------------------------------------------------------------

trace_columns:
main: [system_cols[2], decoder_cols[23], stack_cols[19], range_cols[4], chiplet_cols[18]]
aux: [decoder_tables[3], stack_table, range_table, range_bus, chiplets_table, chiplets_bus]

public_inputs:
program_hash: [4]
stack_inputs: [16]
stack_outputs: [16]

# --- Constraints ---------------------------------------------------------------------------------

boundary_constraints:
# enforce the system boundary constraints on the system trace columns (2 constraints)
# enforce the decoder boundary constraints on the decoder trace columns
# enforce the stack boundary constraints on the stack trace columns (34 constraints)
# enforce the range checker boundary constraints on the range checker trace columns
# enforce the boundary constraints for the hasher, bitwise, and memory chiplets

integrity_constraints:
# enforce the system constraints on the system trace columns
enf system_constraints([system_cols])

# enforce the decoder constraints on the decoder trace columns
enf decoder_constraints([decoder_cols], [decoder_tables])

# enforce the stack constraints on the stack trace columns
enf stack_constraints([stack_cols], [stack_table])

# enforce the range checker constraints on the range checker trace columns
enf range_checker_constraints([range_cols], [range_table, range_bus])

# enforce the constraints for the hasher, bitwise, and memory chiplets on the chiplets columns
enf chiplet_constraints([chiplet_cols], [chiplets_table, chiplets_bus])
```

貢獻指南

開啟貢獻指南

評估

這個 Issue 還沒有評估資料。

把新 issue 寄到你的電子郵件信箱

精選適合新手參與的 GitHub issue 摘要。