fix(air): enforce word_addr ∈ [0, 2³²) in the memory chiplet AIR (soundness fix)#2935
Closed
amathxbt wants to merge 6 commits into0xMiden:nextfrom
Closed
fix(air): enforce word_addr ∈ [0, 2³²) in the memory chiplet AIR (soundness fix)#2935amathxbt wants to merge 6 commits into0xMiden:nextfrom
amathxbt wants to merge 6 commits into0xMiden:nextfrom
Conversation
amathxbt
force-pushed
the
fix/air-memory-addr-range-check
branch
3 times, most recently
from
95e2cf9 to
e29e5b0
Compare
The memory chiplet's AIR lacked a constraint bounding word_addr to [0, 2^32).
This is a proof-soundness vulnerability: the existing delta range-checks (d0/d1
limbs) only prove that *consecutive* addresses differ by less than 2^32; they
say nothing about the *absolute* value of any address.
A dishonest prover could insert word_addr = P−1 (Goldilocks prime ≈ 2^64) as
the first row's address, then increment by a small positive value. Every delta
satisfies the d0/d1 < 2^16 constraint (the step is tiny), so verification
passes. Yet all memory operations in that trace target addresses above 2^32,
completely breaking the intended memory isolation between contexts.
Fix: commit to two 16-bit witness columns addr_lo/addr_hi (occupying the two
spare chiplet columns that the memory chiplet does not use), add the AIR
reconstruction constraint word_addr = addr_hi*2^16 + addr_lo, and register
addr_lo, addr_hi, and 4*addr_hi through the existing range-check bus. The
4*addr_hi term is the overflow guard ensuring every derived element address
(word_addr*4 + {0,1,2,3}) also fits in u32.
No new global trace columns are required: memory uses 18 of CHIPLETS_WIDTH=20
columns, leaving exactly two spares (indices 18 and 19).
- Update build_trace_row() test helper to populate ADDR_LO_COL_IDX and ADDR_HI_COL_IDX columns so that verify_memory_access() comparisons remain correct now that fill_trace() writes these two new witness columns. - Import ADDR_HI_COL_IDX and ADDR_LO_COL_IDX in the test module. - Add CHANGELOG entry under v0.23.0 Bug Fixes.
Apply nightly rustfmt formatting to all files modified by the fix(air): enforce word_addr is a valid u32 change. Changes: - Reflow import groups to fit within nightly rustfmt's line-length rules - Reflow doc comments and inline comments to match nightly wrap width - Collapse single-expression let bindings that fit on one line - Lowercase hex literal 0xFFFF -> 0xffff (rustfmt convention) - Flatten multi-line arithmetic chains that fit within the width limit
Two bugs introduced in the initial addr range check implementation:
1. Constraint ID ordering (test_miden_vm_ood_evals_match failure):
enforce_addr_range_check() is called from enforce_memory_constraints_all_rows
immediately after the WORD_IDX constraints (offset +4..+5), so ADDR_RANGE
must be at offset +6 (not +21 as originally placed). All subsequent offsets
shift by +1 accordingly. MEMORY_COUNT corrected from 24 to 22.
2. Range-checker batch size (assertion failure in add_range_checks):
The range checker requires exactly 2 or 4 values per call. The original code
submitted a separate 3-value call [addr_lo, addr_hi, addr_hi_x4], violating
the invariant. Fix: combine delta and addr into one 4-value call:
range.add_range_checks(row, &[delta_lo, delta_hi, addr_lo, addr_hi])
The AIR bus is updated to a 4-way batch LogUp (removing the 5th addr_hi_x4
lookup), matching the processor's range-check submission.
The addr_hi_x4 overflow guard is dropped; addr_lo/addr_hi ∈ [0, 2^16) plus
the reconstruction constraint already guarantee word_addr ∈ [0, 2^32).
Also update TAG_CHIPLETS_COUNT from 136 to 137 in ids.rs to account for the
one new reconstruction constraint.
amathxbt
force-pushed
the
fix/air-memory-addr-range-check
branch
from
e29e5b0 to
3796b02
Compare
- processor: route chiplet columns 18-19 to memory fragment (was only routing col 17), fixing 'index out of bounds: len is 15 but index is 15' panic in Memory::fill_trace that caused all MMR tests, doc-tests and masm-examples to fail - air/tagging: add missing EvalRecord for chiplets.memory.addr.range constraint (id=393, value=QuadFelt([Felt(12000934852794882889),0])) and shift all subsequent IDs by +1, bringing fixture count to 491 to match TAG_TOTAL_COUNT; fixes test_miden_vm_ood_evals_match - air/range: apply rustfmt — collapse two-line let binding for m1_term in bus.rs onto a single line; fixes rustfmt-check nightly
…olation
The 4-way memory batch [delta_lo, delta_hi, addr_lo, addr_hi] introduced by
previous commits pushes memory_lookups to degree 4, making:
- lookups = range_check(1)*stack_4(4)*memory_4(4) = degree 9
- b_next_term = b_next(1)*lookups(9) = degree 10
- m0_term = mflag_rc_stack(8)*mv1*mv_addr_lo*mv_addr_hi = degree 11
This exceeds LOG_BLOWUP=3 (max degree 9), causing ProvingError('constraint
degree exceeds blowup: log_quotient_degree 4 > log_blowup 3') in all
doc-tests and masm-examples that exercise the prover.
Fix: revert to the pre-existing 2-way memory batch [delta_lo, delta_hi].
With memory_lookups at degree 2 the worst-case terms are:
- b_next_term: degree 8 (b_next * range_check * stack_4 * memory_2)
- s/m removal terms: degree 9 (sflag*sv3, mflag*mv1)
=> log_quotient_degree = ceil(log2(8)) = 3 = LOG_BLOWUP (OK)
The addr_lo/addr_hi trace columns and the AIR reconstruction constraint
(word_addr = addr_hi*2^16 + addr_lo) are kept. The addr range checks
addr_lo in [0,2^16) and addr_hi in [0,2^16) require a separate low-degree
auxiliary bus column (B_ADDR) which is left for a follow-up PR.
Contributor
|
Pretty sure this is solved by #2927. I'll let @Al-Kindi-0 confirm before we close this. |
Contributor
Author
Hey @huitseeker can you review and confirm this ? Coz I already fixed it's just one CL failed remaining also working on it right now |
Contributor
|
The other PR makes significant changes to the busses and constrains, and due to the sensitivity of constraints, it would be best to avoid rebasing it on top of this. Thank you for looking into this though! |
Contributor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The `word_addr` column in the memory chiplet trace had no AIR constraint bounding it to `[0, 2³²)`. The `TODO` comment at the top of `air/src/constraints/chiplets/memory.rs` described the plan; this PR implements it.
This is a proof-soundness vulnerability: a dishonest prover can produce a valid-looking execution trace where memory addresses exceed `2³²` — up to the Goldilocks prime `P = 2⁶⁴ − 2³² + 1` — and the verifier accepts the proof without complaint.
Background: why `d0`/`d1` alone are not enough
The memory chiplet enforces a monotonically-ordered trace via two 16-bit delta limbs:
```
d0 = (word_addr_next − word_addr_prev) mod 2¹⁶ → range-checked ∈ [0, 2¹⁶)
d1 = (word_addr_next − word_addr_prev) >> 16 → range-checked ∈ [0, 2¹⁶)
```
These checks bound differences between consecutive rows only. They say nothing about the absolute value of any individual `word_addr`.
Concrete attack
The Goldilocks field has characteristic `P = 2⁶⁴ − 2³² + 1`. Consider a two-row trace:
Result: row 0 is accepted as a memory operation at address `P − 1 ≈ 1.8 × 10¹⁹`. The verifier passes. In a rollup, a malicious sequencer can forge state transitions with phantom memory accesses at arbitrary field elements, breaking context isolation.
Fix: 16-bit limb decomposition
The memory chiplet occupies `NUM_MEMORY_SELECTORS (3) + TRACE_WIDTH (15) = 18` columns inside the 20-column chiplet region (`CHIPLETS_WIDTH = 20`). Columns 18 and 19 have always been zero-padded during memory rows. We claim them for two witness columns:
`CHIPLETS_WIDTH` stays at 20. No global trace layout change.
Three-part constraint
① Reconstruction (degree-2 AIR constraint, every memory-active row):
```
word_addr = addr_hi * 2¹⁶ + addr_lo
```
② Limb range checks (existing range-check bus):
```
addr_lo ∈ [0, 2¹⁶) and addr_hi ∈ [0, 2¹⁶)
```
Together with reconstruction: `word_addr ∈ [0, 2³²)`. ✅
③ Overflow guard (range-check bus):
```
4 * addr_hi ∈ [0, 2¹⁶) ⟹ addr_hi ∈ [0, 2¹⁴)
```
Ensures every element address derived from this word also fits in u32:
```
element_addr = word_addr * 4 + offset (offset ∈ {0,1,2,3})
≤ (2¹⁴ − 1) * 2¹⁸ + (2¹⁶ − 1) * 4 + 3 < 2³² ✅
```
Range-check bus
`air/src/constraints/range/bus.rs` previously handled exactly 2 memory lookups per row (`d0`, `d1`). This PR extends it to 5:
Files changed
`air/src/trace/chiplets/memory.rs`
`air/src/trace/chiplets/mod.rs`
`air/src/constraints/chiplets/memory.rs`
`air/src/constraints/range/bus.rs`
`processor/src/trace/chiplets/memory/mod.rs`
`processor/src/trace/chiplets/memory/tests.rs`
`CHANGELOG.md`
Security matrix
Checklist