Retire code generation for pickles constraints - #18939
Open
mrmr1993 wants to merge 4 commits into
Open
Conversation
Bumps the proof-systems submodule to the commit adding fp/fq_linearization_tokens, registers them under Kimchi_bindings.Protocol.Linearization, and regenerates kimchi_types.ml / kimchi_bindings.ml with the polish_token / constant_term types. No behaviour change yet: the tokens are not consumed until the next commit. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replaces the generated plonk_checks/scalars.ml (which embedded an OCaml encoding of the kimchi linearization constant term) with a small stack interpreter over the RPN token stream from the FFI. Tick/Tock.constant_term interpret the fp/fq tokens via the same Env primitives in the same order, so the verification key is unchanged (the blockchain-snark VK golden diff passes). Removes gen_scalars and its build rule. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Member
Author
|
!ci-build-me |
Member
|
Awesome :) Fewer codegen magic the better. |
Member
|
@mrmr1993 I am very grateful for this. But why not against compatible instead? |
Member
martyall
added a commit
to o1-labs/o1js
that referenced
this pull request
Aug 20, 2026
Points src/mina at 43cd17b467a6d01a34e477bffc0bfe9c01affab0, the head of MinaProtocol/mina#18939, to run o1js CI against it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015cYLrWyUV2T8VWVsLnrWzi
martyall
added a commit
to o1-labs/o1js
that referenced
this pull request
Aug 20, 2026
Points src/mina at 18f4bb180b (MinaProtocol/mina branch martyall/scalars-token-interpreter-on-o1js-3.0.0): the two feature commits from MinaProtocol/mina#18939 cherry-picked onto 228c409a1, the mina commit o1js main already pins. This makes the checked-in VK fixtures a meaningful baseline for the feature. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015cYLrWyUV2T8VWVsLnrWzi
martyall
added a commit
that referenced
this pull request
Aug 20, 2026
…f_ocaml fp/fq_linearization_tokens existed only in the native kimchi-stubs, so any js_of_ocaml environment (o1js wasm and native backends) raised on the first proof when ft_eval0 forced the token stream. Bumps proof-systems to the commit adding the kimchi-wasm/kimchi-napi exports, and decodes their JSON token encoding into the jsoo value representation in a new bindings file. Prototype for o1js compatibility of #18939. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015cYLrWyUV2T8VWVsLnrWzi
Member
|
I ran the o1js tests with this feature cherry-picked onto mesa + small modification to process the token stream in js everything looks good, let's merge it after mesa hf |
The branch predates the core v0.16 sweep (MinaProtocol#19119) and the ocamlformat 0.28.1 reformat by 777 commits, and its supporting proof-systems branch was itself behind o1-labs master. proof-systems was merged first: feature/ocaml-ordered-linearization-tokens took upstream/master cleanly (17 commits, no conflicts), giving 62170c390a, and that merge is what this branch now pins. Git could not resolve the submodule itself -- base ab84160fa2, ours 1b3f6685c7, develop's f6d958dc05 "don't follow merge-base" -- but 62170c390a descends from both sides, so it is the anchor. The three file conflicts: * gen_scalars/dune and gen_scalars/gen_scalars.ml: deleted. Develop had ported the generator to core v0.16, but this branch exists to replace code generation with interpretation of the FFI token stream, so the generator stays gone. Modify/delete leaves develop's copy in the tree, hence an explicit git rm rather than a staged resolution. * scalars.ml: ours -- one call to interpret the tick constant-term tokens, against develop's reformatted 4300-line generated body. plonk_checks/dune auto-merged correctly, taking develop's expanded ppx list and -open Core alongside this branch's removal of the gen_scalars rule. scalars.ml needed no v0.16 porting; it already spells Core.Hashable.Make. snarky moves to 517a716 with develop. pickles builds and its full test suite passes, including the chunked circuits that prove and verify for real through the interpreter. Note for review: nothing pins verification-key equality between the interpreted and generated linearizations. test_encoding_regression pins the dummy side-loaded key, which is a constant, and no Rust test covers to_ocaml_ordered_polish. Proofs verifying is good evidence but is not the byte-identical-VK claim the branch makes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
3 participants
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.
This PR builds on o1-labs/proof-systems#3581, replacing the
gen_scalarsmechanism in pickles with an FFI layer supporting the RPN tokens directly. This simplifies the 'plonk checks' part of pickles, and makes it dramatically easier to explore variants using different gate constraints.This PR has been tested to be bit-for-bit compatible with the previous version; the proof-systems PR takes pains to ensure that the RPN matches OCaml's right-to-left evaluations order, so the constraints generated by this PR should be identical.