Grant Application: Verified Pasta Curve Operations, Poseidon R1CS Constraints, and Folding-Based Recursive Proof Architecture

[sarinsk629]

I have submitted a grant application to Zcash Community Grants for a project that verifies and packages Zcash’s native Pasta curve operations as R1CS constraints for reuse by the Zcash developer community.

GitHub Application: Grant Application - Verified Pasta Curve Operations, Poseidon R1CS Constraints, and Folding-Based Recursive Proof Architecture · Issue #436 · ZcashCommunityGrants/zcashcommunitygrants · GitHub

Summary: We have built and verified a complete cryptographic proof system over the Pasta curve cycle (Pallas and Vesta) — Zcash’s native curves — including Poseidon-3 as 1,088 R1CS constraints (SAT: YES), homomorphic Pedersen commitments on both curves, a HyperNova multifold core, and a 1,600-byte recursive epoch proof (π_E) verifiable without the witness.

What we’re requesting: $150,000 over 12 months to complete the production instantiation and package the bilingual golden-oracle verification methodology as a reusable toolkit for Zcash developers.

Verification: Clone GitHub - sarinsk629-blip/hsma-core · GitHub and run ./scripts/gate.sh to observe the GATE GREEN verdict (34/34 tests).

I welcome the community’s feedback and questions.

Update on Tachyon/PCD compatibility:

Following community feedback, I want to clarify: our Poseidon R1CS gadget natively produces Rank-1 Constraint System (R1CS) output — the same constraint format used by Tachyon/Ragu (Zcash’s NU7 Proof-Carrying Data framework).

This means the 1,088 verified R1CS constraints for Poseidon-3 are applicable to BOTH:

• The current Halo2 proving system (Orchard, Sapling era)
• The upcoming Tachyon/PCD proving system (NU7, Ragu)

The transition from Halo2 to Tachyon does not eliminate the need for verified R1CS constraint representations of Zcash’s native primitives. It increases it — new constraint code is where implementation bugs live, and our bilingual golden-oracle methodology catches exactly those defects.

The Pasta curve operations (1,032 golden test cases across F_p and F_q) apply to the curve arithmetic that both proving systems depend on — the curves don’t change when the proof system does.

[strahncryptography]

Zcash’s NU7 Tachyon system has already superseded Halo2 for Ragu, a Proof-Carrying Data framework that natively uses Rank-1 Constraint Systems (R1CS). So I feel like this is redundant now, at least for Zcash. Scientifically, totally great, but funded by Zcash specifically? I feel like that’d be a stretch.

[sarinsk629]

@strahncryptography Thank you for confirming that Tachyon/Ragu natively uses R1CS.

Our Poseidon R1CS gadget produces exactly that: 1,088 R1CS constraints for the Poseidon-3 hash (R1CS SAT: YES, 0 unsatisfiable). If Tachyon/Ragu natively uses R1CS, then a verified Poseidon R1CS gadget is directly applicable to the new system — not redundant.

The transition from Halo2 to Tachyon doesn’t eliminate the need for verified R1CS constraint representations of Zcash’s native primitives. It increases it: new constraint code is where implementation bugs live, and the bilingual golden-oracle methodology catches exactly those defects.

Additionally, the Pasta curve operations (1,032 golden test cases across F_p and F_q) apply to the curve arithmetic that both Halo2 and Tachyon depend on — the curves don’t change when the proving system does.

[sarinsk629]

@radbro The Pasta curve IS deployed — we proved both Pallas and Vesta as R1CS constraints with bilingual parity. 34 gates, 165 laws, π_E = 1600 bytes.

The full receipts are in the repo. Run ./scripts/gate.sh and see for yourself

[strahncryptography]

@sarinsk629

The transition to Tachyon/PCD doesn’t reduce the need for verification —
it INCREASES it. A new proving system means new constraint code, new
folding implementations, and new circuit representations — all of which
are exactly where implementation bugs live. Our bilingual golden-oracle
methodology is designed for precisely this moment: verify new
cryptographic code as it’s written, catch defects that self-consistency
testing misses, and maintain an audit trail for every design decision.

First things first, WHY ARE YOU USING AI to write these responses? It does not give me faith in this “verification” because a LARGE number of audits we have seen here in the last year, including auditors I myself solicited, often turn out to just be using AI to “audit” things.

Further, why should Sean Bowe’s team, who is developing Tachyon, not be given the responsibility to audit it?

[sarinsk629]

@strahncryptography These are the right questions, and I’ll answer them directly.

On AI usage:–

You’re correct that AI-audited cryptographic code is a legitimate concern. Let me be precise about how AI is used in this project:

- The AI accelerates code generation and documentation — it is the co-builder, not the verifier.

- The VERIFICATION comes from the bilingual cross-examination: a Python oracle (arbitrary-precision integers, no fixed-width arithmetic) independently computes every operation, and golden vectors pin every intermediate value.

- The gate compares Python output with C++ output bit-for-bit. The AI cannot fake this — a mismatch appears as a test failure.

- The append-only ledger (234 decisions, 163 laws) documents every defect with evidence, fix, and a prevention law. The AI’s contributions are auditable by reading the ledger.

The four defect case studies in the paper (out-of-bounds UB, wrong-power checker, bit-order mismatch, double-canonicalization) were caught by the methodology — not by the AI. The AI accelerated the implementation; the methodology ensured correctness.

That said, I acknowledge that an independent external audit by a firm (not AI, not the original developer) is necessary and is budgeted in this grant proposal. The methodology reduces the audit surface — it doesn’t replace the audit.

On Sean Bowe’s team and Tachyon:–

Sean Bowe’s team is the most qualified to verify Tachyon/PCD, and I agree they should lead that effort. Our work operates at a DIFFERENT layer — the Pasta curve arithmetic, the Poseidon hash, and the R1CS constraint representation exist BELOW the proving system. These primitives don’t change when the proving system transitions.

Specifically:

- The Pasta curve operations (1,032 golden cases across F_p and F_q) verify the field arithmetic that both Halo2 and Tachyon depend on.

- The Poseidon R1CS gadget (1,088 constraints, SAT: YES) provides a constraint representation that applies to any R1CS-based system, including Ragu.

- The bilingual golden-oracle methodology is system-agnostic — it can be applied to Tachyon’s components as they’re developed.

I’m not proposing to replace Sean Bowe’s team’s work. I’m proposing to verify the foundational layers that their work depends on, using a methodology that catches defects at a layer below where they typically operate.

If the committee determines that Tachyon’s internal verification is sufficient and our work is redundant at the Zcash layer, I accept that assessment — and the methodology remains available as an open-source contribution to the broader cryptographic community.

I appreciate the technical depth of your review.

[radbro]