Skip to content

Better Sum-check Docstrings For spartan (Stages 1-3)#1270

Open
abiswas3 wants to merge 14 commits intoa16z:mainfrom
abiswas3:docs
Open

Better Sum-check Docstrings For spartan (Stages 1-3)#1270
abiswas3 wants to merge 14 commits intoa16z:mainfrom
abiswas3:docs

Conversation

@abiswas3
Copy link
Copy Markdown
Contributor

@abiswas3 abiswas3 commented Feb 18, 2026

As part of ongoing formal verification of Jolt in Lean, we have had to extract all the sum-checks and constraints in Jolt in their simplest explicit form.
More precisely:

  • Each sum-check is described only in terms of Virtual Or Real Polynomials.
  • The Schwartz-Zippel randomness and Sum-check randomness is explicitly specified.
  • The verifier opening claim is explicitly stated.
  • The caching of prover openings is tracked in the documentations.
  • We will auto-derive a reduction DAG from this, and this will help iron out bugs.

Other stages will follow shortly, this week.
In the near future, these docs will be programmatically autogenerated from the implementation.
For now, they have been hand-checked for accuracy, and then Claudius Caesar did a diff with the code and my notes.

Running

cargo clean --doc &&cargo doc --no-deps --document-private-items -p jolt-core && python3 -m http.server 8080 --directory target/doc

Should auto generate docs that look like the attached screenshots.

Screenshot 2026-02-18 at 19 30 41

@moodlezoup moodlezoup requested a review from Copilot March 5, 2026 16:50
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

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

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

@moodlezoup moodlezoup requested a review from Copilot March 5, 2026 17:13
@moodlezoup
Copy link
Copy Markdown
Collaborator

#1255 removes the IsRdNotZero flag and related constraints, so I believe the docstrings for outer.rs and product.rs need to be updated

Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

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

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

@abiswas3
Copy link
Copy Markdown
Contributor Author

abiswas3 commented Mar 6, 2026

I'll update this early next week with the rest of the sum-checks. Thanks Michael.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants