feat: merge-train/avm#21116
Merged
Merged
Conversation
Mostly documentation changes
Turns out we don't need to commit to the `timestamp` or the `global_addr` columns. Lots of changes mostly in tests to sidestep the fact we no longer have those columns
Cherry-picked from v4 PR: #21066 ## The Bug The AVM's ALU division circuit (`alu.pil`) constrains integer division `a / b = c` with remainder `r` (stored in `helper1`) via: ``` DIV_OPS_NON_U128 * (ib * ic - ia + sel_op_div * helper1) = 0; ``` This enforces `b * c + r = a` (i.e., `a - r = b * c`). A separate greater-than check ensures `r < b`. However, **the remainder `helper1` was never range-checked to fit within the operand's bit-width** (`max_bits`). A malicious prover could set `helper1` to an arbitrarily large field element (e.g., close to the field modulus) that satisfies `b * c + r = a (mod p)` and `r < b` in the field, but does not represent a valid unsigned integer remainder. This would allow forging incorrect division results. ## The Exploit For non-u128 integer division (u8, u16, u32, u64), a prover can choose a remainder `r` that is a large field element (not a valid unsigned integer) but still satisfies: 1. `b * c + r ≡ a (mod p)` — the main division relation 2. `r < b` — the greater-than check (which operates over the full field) Without a range check on `r`, the prover can manipulate the quotient `c` to be any value they want, completely breaking the soundness of integer division. ## The Fix Added a **lookup-based range check** on the remainder: ```pil #[RANGE_CHECK_DIV_REMAINDER] sel_div_no_err { helper1, max_bits } in range_check.sel_alu { range_check.value, range_check.rng_chk_bits }; ``` This ensures `helper1` (the remainder) fits within `max_bits` (e.g., 32 bits for u32), preventing the prover from using oversized field elements as the remainder. The simulation (`alu.cpp`) was also updated to emit the corresponding `assert_range` event, and unit tests were updated to expect the new range check call. --------- Co-authored-by: Jean M <132435771+jeanmon@users.noreply.github.com>
Collaborator
Author
|
🤖 Auto-merge enabled after 4 hours of inactivity. This PR will be merged automatically once all checks pass. |
…pool (#21138) ## Summary AVM simulations previously used `Napi::AsyncWorker` which runs on the **libuv thread pool**. During simulation, C++ calls back to JS for contract data via `BlockingCall`, and those JS callbacks do async I/O (LMDB, WorldState) that also needs libuv threads. With all libuv threads occupied by sims, the callback I/O deadlocks. This PR introduces `ThreadedAsyncOperation` which spawns a **dedicated `std::thread` per simulation** and signals completion back to the JS event loop via `ThreadSafeFunction`. This structurally prevents the deadlock — libuv threads are always available for callback I/O. ### Changes - **`async_op.hpp`**: New `ThreadedAsyncOperation` class — spawns `std::thread`, uses TSFN for completion, self-destructs after resolving/rejecting the promise - **`avm_simulate_napi.cpp`**: Both `simulate` and `simulateWithHintedDbs` now use `ThreadedAsyncOperation` instead of `AsyncOperation` - **`native_module.ts`**: Deadlock-prevention semaphore removed. Optional resource-limit semaphore available via `MAX_CONCURRENT_AVM_SIMULATIONS` env var (default: unlimited) ### Why this helps multi-sequencer tests Previously, running multiple sequencers in one process required careful tuning of `UV_THREADPOOL_SIZE` and concurrent sim limits to avoid deadlock. With this change, AVM sims don't touch the libuv pool at all, so any number of concurrent simulations can run without starving each other's callbacks. ClaudeBox log: http://ci.aztec-labs.com/884501541464780d-1 --------- Co-authored-by: ludamad <adam.domurad@gmail.com>
…ee traces (#20949) Nullifier tree check was a superset of written slots and retrieved bytecodes tree check. Unify all three into the nullifier tree check implementation generalized as "indexed tree check"
Basically just heavily documenting the public inputs
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.
BEGIN_COMMIT_OVERRIDE
fix(avm)!: memory pre-audit (#21058)
fix(avm)!: memory trace changes (#21059)
fix!: AVM was missing range check on remainder for div in ALU (#21074)
feat: run AVM NAPI simulations on dedicated threads instead of libuv pool (#21138)
feat(avm)!: Unify nullifier, written slots and retrieved bytecodes tree traces (#20949)
fix(avm)!: public inputs pre-audit (#21162)
END_COMMIT_OVERRIDE