Pickles/proof cache links - #381
Merged
Merged
Conversation
`formal/scripts/check_cs.lean` is a script root, so everything it defines is
private to it. That was fine while it was the only driver laying the dumps'
input layouts out; a second one needs the same production constants, and two
copies of production's Blake2b-sampled coset shifts are two things to drift.
`PicklesFixture` is a `lean_lib` in the pickles package, exactly as
`KimchiFixture` is one in kimchi, and for the same stated reason: checking
against recorded data is not part of the development. It cannot live in
`KimchiFixture` — it requires `Pickles`, and `pickles` requires `kimchi`, not
the reverse.
It holds what more than one driver needs: the two constraint types, the GLV
eigenvalues, both sets of coset shifts, the two block readers, the
`finalize_other_proof` input layout, both parameter records, and the step and
wrap harnesses.
The harnesses now return the gadget's `FopOutput` — the success bit and the
four it is the conjunction of — instead of discarding it. A returned value
emits no ops, so `check_cs.lean` keeps its `PUnit` comparison targets by
discarding it in a wrapper, and the dumped systems are unchanged: compiled
`check-cs` over `finalize_other_proof_{step,wrap}_circuit` reports CS equality.
`check_cs.lean` loses 15 declarations and gains one import.
…costs
The dumps' step layout is 151 flat cells. That is what a byte-comparison
driver wants and the last thing a fixture author should have to count, so
`FopInput` puts names on the same cells: the claims, the mask, the domain, the
evaluation block, `ft(ζω)`, the previous challenges and the digest.
Its `CircuitType` and `CheckedType` both come from `ofEquiv` over the
seven-component product, and the harness reaches the circuit through
`CircuitType.varToFields` — so the bundle's encoding IS the flat layout and the
cell order stays defined in one place. The bundle is unchecked: a fixture
supplies the values, so `check` pays no rows and `post` asserts nothing.
`bench-fop` answers the question that decides whether a satisfiability check
over these halves is affordable. On the step half — 1,407 constraints, 14,128
variables, compiled:
build 2 ms prove 600 ms
against 21,715 ms for the same circuit with the function-shaped `Assignments`
this branch is stacked on. The run reaching the end on a placeholder input also
says the advice code is total there: the five output bits simply read 0.
`KimchiFixture.Cache` decodes the pickles suite's proof cache into the wire records `kimchiVerify` and the circuit halves take: the key from `vkRawToJson`'s shape (camelCase, uncompressed `[x, y]` little-endian hex), the proof from arkworks serde (snake_case, points compressed to 33 bytes: `x`, then a flag byte — `0x80` the larger root, `0x00` the smaller, `0x40` the identity). Decompression is CompElliptic's Tonelli–Shanks root, supplied per curve. A file holds both Pasta curves' proofs; a bucket whose points are not on the requested curve is the other side's and is skipped, with the count reported. Neither reader existed: Lean read only the decimal format `tools/fixture-dump` renders, which is why every Lean proof fixture was a separate 5 MB artifact carrying a copy of the SRS. `parseHexLE`/`hexLEtoNat` in `KimchiFixture.PS` go public to serve this module. `check_cache_decode` validates the decoders against the Rust-produced `kimchi_proof_pallas_pickles.json`, field by field: the key through `SimpleChain.json`'s wrap bucket (14 fields), the proof through the serde file the fixture was rendered from (16 fields, 45 compressed points). No cached proof is that fixture's statement — the sideload fixture and the `SimpleChain` spec prove different chains — which is why the proof goes through the file. `endo` is a curve constant; `lagrangeBasis` is SRS-derived and left empty here.
… cached lake exe check-halves pairs each wrap entry of the proof cache with the step proof it wrapped, lays out finalize_other_proof's input from the two (claims, digest and branch data from the wrap statement; evaluations and accumulators from the step proof), runs the step half through the prover interpreter, decides Index.Satisfies on the table it produced, and reads the five bits back. On SimpleChain's five pairs every table satisfies its system and every bit reads 1. The decision path - reduce the built circuit to kimchi rows, assemble, render the witness, Kimchi.Fixture.PS.build, decide - is PicklesFixture.Satisfies, shared with check_cs, which loses its local copies. The accumulator slots are padded in front: the mask reads slot i as 'at least 2 - i proofs'.
scripts/deadcode.lean imports the fixture modules by name, so KimchiFixture.Cache had been outside the audit since it landed. It is imported now, its script-consumed surface (parseFile, Entry, parseVK, parseProof) is rooted in kimchi/roots.txt, and the public-input parser, consumed only by the module's own entry parser, is private.
… SRS check-halves now also runs the wire verifier on both proofs of each wrap-to-step pair. The SRS is the one the PureScript suite proves against: BulletproofFixture.SRSLoader reads srs-cache/<curve>.srs (MessagePack of arkworks-compressed points) behind one function, loadSRS, cut to the proof's round count; validated against the Rust-dumped srs_g/srs_h of the kimchi fixtures on both curves. The Lagrange basis a wire key needs is computed from it in closed form (coefficients omega^(-ik)/n against the first n generators, one MSM per basis element), validated against the Rust-computed lagrange_basis of the Vesta fixture, and memoised under formal/lagrange-cache/ (gitignored). On SimpleChain's five pairs: every step half satisfies with all bits 1, and kimchiVerify accepts all ten proofs (step at the 2^16 Vesta SRS, wrap at the 2^15 Pallas prefix); about 10 s per pair after the one-time SRS loads.
… cached check-halves now also runs the wrap side of finalize_other_proof: for each slot of a step entry with a prevs link, the input is laid out from that slot of the step statement (a split shifted claim's wrap-field cell is its Type2 register 2*half + parity; the digest and challenges by value) and the wrap proof's evaluations and two accumulators, at the proof's round count. The wrap harness and the dump readers take the round count as a parameter, as real wrap proofs have 15 rounds where the dump fixes 16; FopWrapInput names the wrap layout at a round count. On SimpleChain's four linked slots every table satisfies its system and every bit reads 1, about 8 s each.
… the PureScript suite cached check-halves now also runs Pickles.verifyProof, the step circuit's group half, on each step slot's wrap proof: the wrap statement and proof and the slot's unfinalized proof as cells (GroupStepInput), the wrap key's commitments absorbed into the index sponge and the x_hat tables at the Lagrange bases as constants, the group map's square root supplied so the advice runs. PicklesFixture.Group holds the harness and the step-side x_hat tables, which check_cs now shares. On SimpleChain's four linked slots every table satisfies its system and the opening's success bit reads 1, about 120 s each.
… the PureScript suite cached check-halves now runs Pickles.incrementallyVerifyProof on the wrap side too, for each wrap-to-step pair: x_hat over the step statement's leaves at the Vesta Lagrange bases with in-circuit corrections, the conditional sponge with each of the step proof's accumulators under its keep bit off the wrap statement's branch data (mask_i at bit 1 - i, the accumulators in reverse slot order), the claims from the wrap statement, then the verify block's assertions. GroupWrapInput names the cells at a slot count and a round count; z1 and z2 arrive as their Type1 registers. The key-as-constants helpers are shared with the step side. HALVES and LIMIT narrow a run to a subset of the halves and the first pairs. On SimpleChain the wrap group half satisfies with success = 1 at about 490 s per pair, four times the step group half; the whole corpus is now about 55 min compiled.
…ear time Index.build? decided Function.Bijective on the wiring map through the generic Fintype instance, which proves injectivity by comparing every pair of the 7n cells: 112 s of a 117 s group-half run at n = 8192, and the same bill in check_cs and the index fixture check. It now builds the wiring's predecessor table in one pass and decides the two round trips with the stored map, cell by cell, concluding wiring_bijective from Function.bijective_iff_has_inverse. Same field, same law; a corrupted wire still fails the round trip (the index fixture check's negative case). The group half drops to 6 s and the whole halves corpus to 200 s.
A halves lane in the Lean workflow: the build job compiles the driver beside check-cs so the binary rides the cache, the lane fetches the project's SRS, memoises the Lean Lagrange bases, and runs lake exe check-halves over the whole corpus (200 s). The driver reports each run's phases (build, prove, gate reduction, witness, index build, decide) so a regression like the quadratic index build shows where it sits.
…cache `FixtureKit.swPointOfCoords` is the on-curve constructor `parseSWPoint` was inlining; `Bulletproof.Fixture.pointOfCompressed` decodes the arkworks flag byte once, for the SRS loader and the cache's proof points alike. The cache's bucket skip decides `OnCurve` on the first entry's first sigma commitment instead of matching an error string. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
`reduceBuilt`, `reduceSolved` and `gateDataOf` are `Compile.lean`'s; `kimchiCompile`, `kimchiSolve` and `kimchiGateData` run over them, and so does the satisfiability driver off its `build`/`prove` pair. `PicklesFixture.Satisfies` loses its copies and the unused `provedSatisfies`. The driver unpacks the branch data through one function and reads one-chunk commitments through the one `oneChunk`. Imports per shake. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…the dump `ivpStepInputOf` lays the claims, the `sg_old` list, a key's commitments and a wrap proof block out as the gadget's input; `GroupStepInput.cells` and check_cs's `stepVerifyCells` are it at their offsets. check_cs's dummy key is `dummyKeyComms`, fed to the shared `indexSponge` and `keyRecords`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
formal: the circuit halves are satisfied on the proofs the PureScript suite cached (#373)
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
There was a problem hiding this comment.
Your trial has ended. Reactivate Greptile to resume code reviews.
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
1 participant
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.
No description provided.