Carry the consumed proof bytes in Lean fixture exports - #933
Open
TalDerei wants to merge 4 commits into
Open
Conversation
TalDerei
changed the title
This was referenced Aug 26, 2026
TalDerei
commented
Aug 27, 2026
Comment on lines
+905
to
+939
| // The exact string `VerifyingKey::from_parts` hashed into `transcript_repr`: the compact | ||
| // `Debug` rendering of the pinned key. Emitting it lets a consumer recompute the digest | ||
| // and read the pinned fields, instead of trusting the scalar above. The exporter checks the | ||
| // string is printable ASCII (so `{:?}` adds only the `\"` and `\\` escapes Lean shares) | ||
| // and that hashing it reproduces `transcript_repr`, so the emitted text is the preimage. | ||
| let pinned = format!("{:?}", self.pinned()); | ||
| assert!( | ||
| pinned | ||
| .chars() | ||
| .all(|c| c.is_ascii() && !c.is_ascii_control()), | ||
| "the pinned key description must be printable ASCII" | ||
| ); | ||
| { | ||
| let mut hasher = blake2b_simd::Params::new() | ||
| .hash_length(64) | ||
| .personal(b"Halo2-Verify-Key") | ||
| .to_state(); | ||
| hasher.update(&(pinned.len() as u64).to_le_bytes()); | ||
| hasher.update(pinned.as_bytes()); | ||
| let recomputed = Fp::from_uniform_bytes(hasher.finalize().as_array()); | ||
| assert!( | ||
| recomputed == self.transcript_repr, | ||
| "hashing the pinned key description must reproduce transcript_repr" | ||
| ); | ||
| } | ||
| out.push_str("/-- The exact text `VerifyingKey::from_parts` hashed into `capturedVkTranscriptRepr`:\n"); | ||
| out.push_str("the compact `Debug` rendering of the pinned key (`Halo2-Verify-Key` BLAKE2b over its\n"); | ||
| out.push_str( | ||
| "little-endian `u64` byte length then its bytes, reduced modulo `p`). The exporter\n", | ||
| ); | ||
| out.push_str("re-hashed it and checked the scalar above before emitting. -/\n"); | ||
| out.push_str(&format!( | ||
| "def capturedPinnedKeyDescription : String :=\n {:?}\n\n", | ||
| pinned | ||
| )); |
Contributor
Author
There was a problem hiding this comment.
capturedPinnedKeyDescription is the debug string representing circuit_description_post_nu6_3 (a succinct representation of the raw 28K LOC dump). Fixture.lean now contains both:
capturedPinnedKeyDescription: the exact hash preimage stringcapturedVkTranscriptRepr: the field element digest that's hashed into the transcript (which we can now derive in Lean instead of trusting the fixture)
TalDerei
marked this pull request as ready for review
August 27, 2026 04:41
Add `dump_vesta_lean_fixture_with_proof_bytes` and its match-only sibling (behind `unstable-verifier-fingerprint`): as the existing exporters, but given the proof byte string the verifier consumed, which the fixture then carries hex-encoded as `capturedProofHex`. The exporter fails fast unless re-serializing the recorded proof reads (`write_point`, `write_scalar`, in read order) reproduces the supplied bytes exactly, so the emitted typed proof is their canonical parse and a consumer can check its own proof-string decoder against the bytes the deployed verifier read. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Every fixture now carries `capturedPinnedKeyDescription`, the exact compact `Debug` rendering of the pinned verifying key that `from_parts` hashes into `transcript_repr`. The exporter checks the text is printable ASCII and that re-hashing it reproduces `transcript_repr` before emitting, so a consumer can recompute the key digest and read the pinned fields rather than trust the captured scalar. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
TalDerei
force-pushed
the
fingerprint-proof-bytes
branch
from
August 27, 2026 07:54
74a5c1f to
fbc2dc5
Compare
ebfull
approved these changes
Aug 28, 2026
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #933 +/- ##
==========================================
+ Coverage 84.21% 84.31% +0.10%
==========================================
Files 108 108
Lines 13755 13858 +103
==========================================
+ Hits 11584 11685 +101
- Misses 2171 2173 +2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
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.
Related to zcash/orchard#544 and consumed in zcash/ironwood#215.
New
dump_vesta_lean_fixture_honest_with_proof_bytesanddump_vesta_lean_fixture_match_only_with_proof_bytesfixture exports behindunstable-verifier-fingerprintthat includes exact bytes consumed (proof commitments, polynomial evaluations, the multi-opening proof, and the IPA proof) by the verifier and reject mismatches. It reserializes the points/scalars using existing halo2 encoding, checks they match the original proof bytes, then exports those bytes as hex.