Skip to content

Range-check multiplicities wherever needed for soundness - #1017

Merged
RobinJadoul merged 3 commits into
spec/mainfrom
spec/mult-rangecheck
Oct 12, 2026
Merged

RobinJadoul merged 3 commits into
spec/mainfrom
spec/mult-rangecheck

Conversation

@RobinJadoul

Copy link
Copy Markdown
Collaborator

No description provided.

@RobinJadoul RobinJadoul self-assigned this Oct 7, 2026
@RobinJadoul RobinJadoul added the spec Updates and improvements to the spec document label Oct 7, 2026
@github-actions

github-actions Bot commented Oct 7, 2026

Copy link
Copy Markdown

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401


Automated review by Kimi (Moonshot AI)

@github-actions

github-actions Bot commented Oct 7, 2026

Copy link
Copy Markdown

Codex Code Review

No actionable issues found in the PR diff. The changes are confined to specification constraints and rendering; all 19 modified TOML files parse successfully.

@RobinJadoul

Copy link
Copy Markdown
Collaborator Author

Not a full fix yet, needs more checks for situations where you'd have e.g. μ = var = -1, and IS_BYTE<μ> = ARE_BYTES[-1, 0] with mult 1, but you get IS_BYTE<var> = ARE_BYTES[-1, 0]  with mult μ = -1 to make that negative μ work

@erik-3milabs erik-3milabs left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One more observations while reviewing: MEMW's constraints 01-04 and 05-08 are duplicates.

But maybe this is something best addressed somewhere else.

Comment thread spec/src/eq.toml Resolved
Comment thread spec/src/dvrm.toml Resolved
Comment thread spec/src/is_wh.toml

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, fair point, we may need some bound on total number of tables (or tables per epoch)

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

added it as a note

@RobinJadoul

Copy link
Copy Markdown
Collaborator Author

MEMW's constraints 01-04 and 05-08 are duplicates.

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.

@RobinJadoul
RobinJadoul merged commit 9ed2b6c into spec/main Oct 12, 2026
2 checks passed
@RobinJadoul
RobinJadoul deleted the spec/mult-rangecheck branch October 12, 2026 14:20
@jotabulacios jotabulacios mentioned this pull request Oct 15, 2026
jotabulacios added a commit that referenced this pull request Oct 15, 2026
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

spec Updates and improvements to the spec document

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants