pickles: the proof cache records a chain's links and verification keys - #376
Merged
Merged
Conversation
The proof cache's value was the proof's serde JSON and nothing else, with the
verification key recoverable only by parsing the bucket key, which is itself a
JSON blob. A consumer that wants to verify a cached proof — rather than feed it
back to the prover that made it — needs the key as data.
The entry becomes `{ proof, vk }`, so every cached proof is a self-contained
(vk, public input, proof) triple: the public input is already the inner key.
The typed accessors keep their signatures, so nothing downstream changes.
Regenerated: a stale cache fails to decode, which `loadStore` reports as an
empty store, so the suite repopulates it.
`VerifierIndex::digest()` is the value the kimchi verifier absorbs at the top of
its Fiat–Shamir transcript. Nothing transmits it — it is a function of the key
alone, and every verifier recomputes it — but Lean declares it an input rather
than transcribing it, so a Lean consumer of a cached proof cannot derive it.
`verifierIndexDigest` computes it in PureScript, where the prover already holds
the `VerifierIndex`. The absorption order is production's, and it is NOT the
order `verifierIndexColumnComms` returns: all 7 sigma commitments first — the 6
it carries plus `sigmaCommLast` — then the 15 coefficient commitments, then the
6 selectors, each chunk by chunk as a point.
That reordering is the only thing here that could be silently wrong, so it is
checked rather than argued: `LeanInputsSpec` compares the computed digest for
simple_chain's wrap key against the value Rust recorded for that key in
`formal/kimchi/fixtures/kimchi_proof_pallas_pickles.json`. The same value now
appears in `SimpleChain.json`, written by an ordinary prover run.
The entry becomes `{ proof, vk, digest }`, so a cached proof is self-describing:
key, digest, public input (the inner key) and proof. Regenerated.
…rapped
The cache bucketed on the verification key's full JSON — ~10 KB repeated as
every entry's `vk` field — and recorded nothing about which proof consumed
which. A consumer walking a chain had to pair a step proof with the wrap it
finalized by rediscovering a fact the prover had in hand when it wrote.
Now `{ "<vkDigest>": { "<publicInput>": Entry } }`, with the digest as the
bucket and `Entry = { vk, proof, step? }`: a step proof's entry is its key and
its proof; a wrap proof's entry adds `step`, the `(vkDigest, publicInput)` of
the step proof it wrapped, which the wrap prover holds when it writes. The
wrap→step link is 1:1, so a step's wraps are the entries pointing at it.
The accessors take the digest as the key; the two provers compute it once with
`verifierIndexDigest`, and `Prove.Compile` threads the step's key into the
wrap context. `loadStore` drops any bucket whose key is not a decimal digest,
so a store written under an older keying cannot survive beside the new one — a
stale cache decoded cleanly into the new record (`step` is optional) and its
buckets stayed on disk next to the regenerated ones until this filter.
The "mirrors OCaml `proof_cache.ml`" rationale goes with the keying: nothing
shares the file with OCaml. Regenerated from empty.
A step entry gains prevs: one entry per slot, in slot order, the cache key of the wrap proof the slot verified or null on a base-case slot. The wrap-side finalize_other_proof runs on a step statement's slot and the wrap proof it verified, and that pairing is data the step prover has, like the wrap entry's step link. StepRef becomes ProofRef, the step prover's context carries the per-slot refs, and the cache is regenerated from empty. The snarky-kimchi round-trip test keys by a decimal digest stand-in, as the store has required since it was keyed by digest.
![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.
martyall
commented
Sep 17, 2026
…rgument Review of #376. An entry links either to the step proof it wrapped or, per slot, to the wrap proofs it verified: Links is that sum, so no entry writes an always-empty field; the flat step/prevs keys stay the on-disk shape, an entry with neither or both reading as a miss. The per-proof refs reach the step prover as an argument of stepSolveAndProve rather than through a placeholder field of the per-shape context.
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.
The pickles test suite's proof cache becomes a record a downstream consumer can verify a chain from, not only a memo the prover reads back.
What changes
vkRawToJson: camelCase, uncompressed[x, y]little-endian hex points). Downstream decoders deal with what they get.VerifierIndex::digest()(the value the verifier absorbs first), computed in PureScript byPickles.VerificationKey.verifierIndexDigestand checked against the recorded fixture value inLeanInputsSpec.loadStoredrops buckets whose key is not a decimal digest, so a store written under the old keying cannot survive beside the new one.step: {vkDigest, publicInput}); a step entry records, per slot, the wrap proof it verified there (prevs,nullon a base-case slot). Both are data the prover has at the write site;StepRefbecomesProofRef.packages/pickles/test/fixtures/proof-cache/is regenerated from empty (58 entries, 11 files).snarky-kimchiround-trip test keys by a decimal stand-in, as the store requires since the digest keying.Why
formal/runs the Lean circuit halves andkimchiVerifyon these proofs (stacked PR). That needs, per proof, its key, its public input, and which proof it is built on — none of which the old{vk-json -> public-input -> proof}memo made recoverable.Testing
ps:pickles(243 s, regenerates the cache) andps:snarky-kimchigreen.