prover: enforce load/store memory alignment in AIR#609
Open
Kuhai9801 wants to merge 3 commits into
Open
Conversation
|
All contributors have signed the CLA ✍️ ✅ |
Author
|
I have read the CLA Document and I hereby sign the CLA |
1 similar comment
Author
|
I have read the CLA Document and I hereby sign the CLA |
Author
|
recheck |
Author
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
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.
Context
Fixes #605.
The VM rejects unaligned halfword and word memory accesses, but the load/store AIR did not enforce that same rule. That meant a forged trace could describe memory behavior that the VM itself would reject.
This PR makes the load/store AIR enforce the same alignment semantics as the VM for:
LH,LHU,SHhalfword accessesLW,SWword accessesWhat changed
RamBaseAddrAlignmentQuotient, a small witness for the low byte ofRamBaseAddrdivided by the required alignment.LoadStoreChipconstraints so:addr_low = 2 * qaddr_low = 4 * qRange128Chiplookup to proveqis an actual small integer, not an arbitrary field value.LH,LW, andSH, plus aligned acceptance checks forLHandLW.Review notes
The range check is the key part of the fix. Without it, the equality constraint alone would still allow a forged trace to use a fractional field value for
q. Withqconstrained to[0, 127], the equations force the low address byte to be correctly aligned.RamBaseAddrlimbs are already byte-ranged elsewhere, so enforcing the low byte is enough for these alignment rules.Verification
Ran locally with the pinned
nightly-2025-05-09-x86_64-pc-windows-gnutoolchain:cargo fmt --all --checkcargo test -p nexus-vm-prover aligned -- --nocaptureThe focused test run passed with 4 tests passing and 0 failures. The rejection tests intentionally catch AIR constraint failures from malformed traces, so the panic messages printed during those tests are expected.