Repository navigation
Range-check multiplicities wherever needed for soundness - #1017
Conversation
Kimi Code ReviewAutomated review by Kimi (Moonshot AI) |
Codex Code ReviewNo actionable issues found in the PR diff. The changes are confined to specification constraints and rendering; all 19 modified TOML files parse successfully. |
|
Not a full fix yet, needs more checks for situations where you'd have e.g. |
erik-3milabs
left a comment
There was a problem hiding this comment.
One more observations while reviewing: MEMW's constraints 01-04 and 05-08 are duplicates.
But maybe this is something best addressed somewhere else.
There was a problem hiding this comment.
This IS_B20 got me thinking: what if the prover introduces sufficiently many rows with large, positive μ and have them collectively mimic a single μ= -1?
Given that we're working with a 64-bit prime, this IS_B20 lookup allows this to be achieved with 2^44 rows, which fit in 2^24 tables of 2^20 rows each. 2^24 tables is a lot, but, given that (with the exception of one, maybe) all of these tables are identical, the prover overhead is negligible (right?). Sure, the proof would be large, but that is something you can reduce through recursion.
So: the verifier will have to ensure the number of tables being used during proving are not excessively large.
There was a problem hiding this comment.
Yeah, fair point, we may need some bound on total number of tables (or tables per epoch)
I also caught that one, it's a result of introducing explicit arith constraints for assumptions, and it's actually already handled in my changes for this PR, I think. |
and use them for the KECCAK state_ptr. IS_WH range checks the top 48 bits of an address, with one row per distinct (word, half) pair. Its multiplicity is bounded with IS_B20, as in #1017. KECCAK state_ptr is now DWordWHH: 486 columns and 84 interactions, down from 511 and 134. TableCounts gets an is_wh field, so RECURSION_INPUT_VERSION goes to 4 and the statement tags to V5.
No description provided.