Air/src/cpu#23
Conversation
…tion, and sign extension.
… and return multiple constraints.
…decomposition, selection, and zero extension, and add a full test.
…ll logic and added a dedicated test.
…ition, offset verification, and memory update, and add a comprehensive test.
…composition and update logic, and add a new test case.
…d values and return a vector of constraints.
…ition witnesses and return multiple constraints, and update its test.
…and add comprehensive tests for alignment.
…limbs and carries.
…logic, including carries, signs, and overflow factor, and update its test.
…lication and add its test.`
…tion logic and update its test, and correct carry calculation in related multiplication tests.
… with carry witnesses and update tests.
…` using limb arithmetic and carries.
…iables and returning multiple constraints for verification.
…emainder (REMU) using intermediate product and carry witnesses.
…y checks and return multiple constraints.
… test for the not-taken case.
…onstraint` signed branch instructions with witness parameters.
…t witnesses for unsigned comparison and return multiple constraints.
…turn a vector of constraints.
…d correctly implement next PC alignment.
There was a problem hiding this comment.
Copilot wasn't able to review any files in this pull request.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Copilot wasn't able to review any files in this pull request.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
Suggested follow-up (blocking for soundness): memory byte/half decomposition witnesses need explicit range checks—only constraining \ is not unique in-field; constrain each unpacked byte to 8 bits and each unpacked halfword to 16 bits (same for \ / ). I’m blocked from pushing a patch from this chat until Agent mode is enabled; happy to apply the fix directly once that’s cleared. |
|
Follow-up on soundness: unpacked memory limbs used in LB/LBU/LH/LHU/SB/SH need explicit bit-range witnesses (each byte limb in [0,255], each halfword in [0,65535]); the word reconstruction equation alone admits non-physical field witnesses. Likewise constrain the stored byte and halfword values. Earlier comment may have truncated due to shell quoting—this is the full note. |
Add 8-bit (resp. 16-bit) bit witnesses for each unpacked mem limb and for SB/SH stored values so reconstruction is unique in-range, not just consistent mod p. Unit tests updated; cargo test -p zp1-air passes. Made-with: Cursor
|
Pushed commit a70ca45: LB/LBU/LH/LHU/SB/SH gadgets now attach 8-bit (or 16-bit) bit witnesses to every unpacked memory limb and to the stored byte/halfword, so the decomposition is physically unique—not only consistent with mem_value modulo the field. Tests for these gadgets updated; zp1-air test suite passes locally. |
# Conflicts: # crates/air/src/cpu.rs
|
Resolved the merge conflict with current main in commit 00b01ef and pushed it to air/src/cpu. Kept the witness-based CPU alignment constraints and adapted main's alignment tests to provide explicit low-bit witnesses. Local verification: cargo test -p zp1-air passes (103 tests). |
|
Security follow-up pushed in cf1990a: the LB/LBU/LH/LHU/SB/SH gadgets no longer bind byte/halfword decompositions to a single full-word M31 element. They now bind to 16-bit word limbs, so 32-bit words that collide modulo p = 2^31 - 1 cannot reuse the wrong byte decomposition. Added a regression test for the 0 vs 0x7fffffff collision. Local verification: cargo test -p zp1-air passes (104 tests). |
|
Performance follow-up pushed in a19e075: added Criterion coverage for the memory load/store gadgets changed by the security fix. Verification run locally: cargo test -p zp1-air --release, cargo bench -p zp1-air --bench constraint_bench, cargo bench -p zp1-air --bench constraint_bench Memory_Gadgets, and cargo test -p zp1-air --benches. Targeted Memory_Gadgets medians were approximately LB 200.9 ns, LBU 193.2 ns, LH 211.8 ns, LHU 211.2 ns, SB 295.2 ns, SH 293.1 ns. |
No description provided.