diff --git a/README.md b/README.md index 696aa14..2f7229c 100644 --- a/README.md +++ b/README.md @@ -8,15 +8,15 @@ The Aiken ZKP Standards Library takes a pragmatic approach to implementing zero- This implementation is designed for Plutus v3, leveraging its built-in BLS12-381 curve functions to ensure efficient and secure verification of ZKPs. It emphasizes clarity and maintainability, making it suitable for educational/demonstrative purposes without sacrificing security. -## Targeted Features +## Status -### Groth16 +All three verifiers are functional, unit-tested, and build cleanly (`aiken check` / `aiken build`, 37/37 tests passing as of this writing). Each is **verification-only**: proof generation, circuit compilation, and (for Groth16/PLONK) trusted setup are assumed to happen off-chain, using external tooling this library does not provide. Full architecture, security arguments, and known limitations for each are written up in [`zkp/docs/`](./zkp/docs). -Status: Complete +### Groth16 -The Groth16 implementation is largely based on Modulo-P's [ak-381](https://github.com/Modulo-P/ak-381), with some ideas taken from [zarassh's implementation](https://github.com/tarassh/zkSNARK-under-the-hood/blob/main/groth16.py) and an emphasis on explicitness and clarity. This should make this implementation ideal for learning, or for further modification. +Status: Complete (verifier) -Currently, the Groth16 module includes: +The Groth16 implementation ([`zkp/lib/groth`](./zkp/lib/groth)) is largely based on Modulo-P's [ak-381](https://github.com/Modulo-P/ak-381), with some ideas taken from [tarassh's implementation](https://github.com/tarassh/zkSNARK-under-the-hood/blob/main/groth16.py), and operates on native BLS12-381 pairing builtins throughout. It's tested against externally-generated proof/verification-key fixtures, both accepting valid proofs and rejecting a tampered one. [Implementation report](./zkp/docs/groth16-implementation-report.md). - [x] Generic Groth16 proof verifier system - [x] Onchain verification tests @@ -30,9 +30,9 @@ Wishlist: Status: Optimizing -The Plonk implementation is loosely based on perturbing's [plutus-plonk](https://github.com/perturbing/plutus-plonk-example), with several optimizations and restructuring done around point compression to improve performance and clarity. +The Plonk implementation ([`zkp/lib/plonk`](./zkp/lib/plonk)) is loosely based on perturbing's [plutus-plonk-example](https://github.com/perturbing/plutus-plonk-example), with several optimizations and restructuring done around point compression to improve performance and clarity, a batched KZG opening, and a Keccak-256 Fiat–Shamir transcript matching the SnarkJS convention. It's tested against an externally-generated proof/verification-key fixture, including rejection of tampered proofs and mismatched public inputs. [Implementation report](./zkp/docs/plonk-implementation-report.md). -The Plonk module currently includes: +At current measurements, a full verification call is the most expensive of the three verifiers in this library (§7 of the implementation report) and leaves the least headroom against Cardano's per-transaction execution budget — hence "Optimizing" rather than "Complete." - [x] Generic Plonk proof verifier system - [x] Onchain verification tests @@ -45,30 +45,47 @@ Wishlist: ### Bulletproofs -Status: Early Development +Status: Complete (verifier and reference prover) + +The Bulletproofs implementation ([`zkp/lib/bullet`](./zkp/lib/bullet)) is the only one of the three with no trusted setup, so this library implements and tests both a verifier *and* a reference prover directly, with no external fixtures required. [Implementation report](./zkp/docs/bulletproofs-implementation-report.md). + +- [x] Generic Bulletproofs range-proof verifier and reference prover +- [x] Onchain verification tests, including boundary values and tamper rejection + +Wishlist: -The Bulletproofs implementation is in the early stages, with a focus on building out the necessary field arithmetic and point operations required for Bulletproofs. +- [ ] Recursive inner-product-argument (IPA) compression, for `O(log n)` rather than `O(n)` proof size +- [ ] Integration into a merkelized validator ### Helper Functions -- Affine point operations - conversion to/from native types -- Field arithmetic utilities +- Affine point operations - conversion to/from native types (`zkp/lib/common/blst_affine.ak`) +- Field arithmetic utilities (`zkp/lib/common/common.ak`) — largely superseded by native BLS12-381 builtins inside the three verifiers above; see the implementation reports for where and why ## Aspirational ZKP Systems - **Marlin**: Preprocessing zkSNARKs with Universal and Updatable SRS - **Plonky2**: Advanced recursive proof composition -## Contributing +## Implementation -We welcome contributions! Please see our [Contributing Guide](./CONTRIBUTING.md) for: +- Leverages PlutusV3's BLS12-381 curve builtin functions +- Focuses on efficient verification +- Maintains strong security guarantees +- See the per-protocol implementation reports in [`zkp/docs/`](./zkp/docs) for details -- Development guidelines -- Submission process -- Testing requirements +## Getting Started ### Prerequisites - Aiken development environment - Familiarity with ZKP systems - Understanding of Cardano smart contracts + +## Contributing + +We welcome contributions! Please see our [Contributing Guide](./CONTRIBUTING.md) for: + +- Development guidelines +- Submission process +- Testing requirements diff --git a/specification.md b/specification.md index e561be5..e712324 100644 --- a/specification.md +++ b/specification.md @@ -28,22 +28,24 @@ Bulletproofs shine through their versatility. They’re small in size, easily ag The library's scope has been carefully defined through a systematic evaluation process: -### Committed Features +### Delivered Features + +All three verifiers below are implemented, unit-tested (37/37 tests passing, both positive and negative cases), and build cleanly under `aiken check`/`aiken build`. Each is **verification-only**: none of the three includes a proof-generation toolchain, and Groth16/Plonk additionally require a trusted-setup ceremony (circuit-specific and universal, respectively) that this library does not run or provide. Full architecture, design rationale, and security arguments for each are written up in `zkp/docs/`. #### Groth16 -- Provide a generic Groth16 proof verifier system in Aiken which supports user-defined circuits leveraging circom and SnarkJS -- Provide an example circuit and R1CS constraint set for the Groth16 verifier to show the entire process of creating and verifying a Groth16 proof -- Provide a test suite that demonstrates the ability of the proof system to successfully verify the generated proof, while denying validation of invalid proofs +- A generic Groth16 proof verifier in Aiken (`zkp/lib/groth`) that accepts any circuit-specific verification key and proof — including ones produced by an external circom + SnarkJS toolchain — without this library needing any knowledge of the circuit itself +- A test suite verifying real, externally-generated Groth16 proofs, and correctly rejecting a tampered one +- See `zkp/docs/groth16-implementation-report.md` #### Plonk -- Provide a generic Plonk proof verifier system in Aiken which supports user-defined circuits leveraging circom and SnarkJS -- Provide an example circuit and R1CS constraint set for the Plonk verifier to show the entire process of creating and verifying a Plonk proof -- Provide a test suite that demonstrates the ability of the proof system to successfully verify the generated proof, while denying validation of invalid proofs +- A generic Plonk proof verifier in Aiken (`zkp/lib/plonk`), including a batched KZG opening and a Keccak-256 Fiat–Shamir transcript compatible with SnarkJS's Plonk verifier convention +- A test suite verifying a real, externally-generated Plonk proof, and correctly rejecting both a tampered proof and a mismatched public-input list +- See `zkp/docs/plonk-implementation-report.md` #### Bulletproofs -- Provide a generic Bulletproof verifier system in Aiken which supports user-defined circuits leveraging circom and SnarkJS -- Provide an example circuit and R1CS constraint set for the Bulletproof verifier to show the entire process of creating and verifying a Bulletproof -- Provide a test suite that demonstrates the ability of the proof system to successfully verify the generated proof, while denying validation of invalid proofs +- A generic Bulletproofs range-proof verifier *and* reference prover in Aiken (`zkp/lib/bullet`) — the only one of the three with no trusted setup, so this library implements and tests both sides directly, with no external fixtures required +- A test suite covering valid proofs, boundary values (0 and `2^n - 1`), and multiple tampering/rejection cases +- See `zkp/docs/bulletproofs-implementation-report.md` ### Non-Committed / Aspirational Features @@ -55,10 +57,4 @@ The library's scope has been carefully defined through a systematic evaluation p ## Implementation -### On-Chain - -Our on-chain implementation will be supported largely by the new builtin functions provided by PlutusV3 that relate to the BLS12-381 curve. Some of the type signatures for both type definitions and functions of the library can be found within the `.ak` files throughout the rest of the repository. These implementations will focus on efficient verification while maintaining security guarantees. - -### Off-Chain - -Given that this library is specific to Aiken, the off-chain implementation is highly dependent upon the design choices and requirements of the user. We will be providing examples using circom, but support for general purpose proof creation is outside the scope of this work. Users will need to implement their own proof generation infrastructure using tools like circom and SnarkJS while following our provided examples as guidance. +Our implementation will be supported largely by the new builtin functions provided by PlutusV3 that relate to the BLS12-381 curve. Some of the type signatures for both type definitions and functions of the library can be found within the `.ak` files throughout the rest of the repository. These implementations will focus on efficient verification while maintaining security guarantees. See `zkp/docs/` for a full implementation report per protocol, covering architecture, design decisions, and security arguments. diff --git a/zkp/README.md b/zkp/README.md new file mode 100644 index 0000000..a58f167 --- /dev/null +++ b/zkp/README.md @@ -0,0 +1,30 @@ +# zkp + +Aiken package containing this project's three zero-knowledge proof verifiers, targeting Plutus V3 on Cardano. See the repository root [README](../README.md) and [specification.md](../specification.md) for project-level scope and status. + +## Layout + +``` +lib/ + groth/ Groth16 verifier + plonk/ PLONK verifier + bullet/ Bulletproofs range-proof verifier and reference prover + common/ Shared field/point scaffolding (legacy; superseded by native BLS12-381 + builtins inside groth/plonk/bullet — see docs/ for details) + tests/ Test suites for groth and plonk (bullet's tests live alongside bullet.ak) +docs/ + step-by-step.md Protocol-level walkthrough of all three systems + groth16-implementation-report.md Architecture, design decisions, security argument + plonk-implementation-report.md " + bulletproofs-implementation-report.md " +``` + +## Working with this package + +```sh +aiken check # run the test suite +aiken build # compile and generate plutus.json +aiken fmt # format .ak source +``` + +Each implementation report in `docs/` documents what's actually built, how it departs from a naive port of the underlying protocol, and its known limitations — read those before integrating one of these verifiers into a validator. diff --git a/zkp/docs/groth16-implementation-report.md b/zkp/docs/groth16-implementation-report.md new file mode 100644 index 0000000..bfead38 --- /dev/null +++ b/zkp/docs/groth16-implementation-report.md @@ -0,0 +1,96 @@ +# Groth16 Verifier - Implementation Report + +- **Module:** `zkp/lib/groth/groth.ak` +- **Status:** Functional, tested, unaudited +- **Test results:** + - `aiken check` 3/3 (part of 37/37 across the package) + - `aiken fmt` clean + - `aiken build` succeeds + +## 1. Overview + +This module implements a Groth16 zk-SNARK verifier over the BLS12-381 curve, as one of three zero-knowledge proof systems in this repository's `zkp` package for Cardano smart contracts (Aiken, targeting Plutus V3). Given a circuit-specific verification key and a proof `(A, B, C)`, it checks the canonical Groth16 pairing equation against a list of public inputs, without the validator ever seeing the witness. + +Unlike this package's `bullet` module, `groth` implements **verification only**. Groth16 needs a circuit-specific trusted setup and a full R1CS/QAP witness computation to produce a proof; this codebase does not implement a prover or a setup ceremony for either, consistent with this package's own design notes (`docs/step-by-step.md`), which state plainly that proof generation and setup are assumed to happen off-chain. Everything in this module exists to answer one question on-chain: is this proof, for this verification key and these public inputs, valid? + +This report covers the implementation as it stands: what was built, how it works, where it departs from a naive port of the mathematics, and what remains before it is production- or audit-ready. + +## 2. Position within the `zkp` package + +| Module | Proof system | Setup | Core primitive | +|---|---|---|---| +| `lib/groth` | Groth16 | Trusted, circuit-specific | Pairings (`bls12_381_miller_loop`, `bls12_381_final_verify`) | +| `lib/plonk` | PLONK | Universal, trusted | Kate commitments, permutation argument | +| `lib/bullet` | Bulletproofs | Public, trustless | Discrete-log / Pedersen commitments, no pairings | +| `lib/common` | — | — | Shared field/point scaffolding, superseded in this module (see §4) | + +Groth16 sits at the opposite end of the setup-trust spectrum from Bulletproofs: it requires the smallest, cheapest verifier of the three (four pairings, no polynomial commitments, no vector openings) at the cost of a per-circuit trusted ceremony that must be run and attested to outside this codebase. + +## 3. Architecture + +**Types** + +``` +CompressedVK { alpha, beta, gamma, delta, vkIC } // all ByteArray +CompressedProof { a, b, c } // all ByteArray +VerifierKey { alpha: G1Element, beta/gamma/delta: G2Element, vkIC: List } +Proof { a: G1Element, b: G2Element, c: G1Element } +``` + +The `Compressed*` types are the wire/datum format: standard 48-byte (G1) and 96-byte (G2) BLS12-381 compressed point encodings, suitable for storing directly in a redeemer or datum as plain `ByteArray`. `VerifierKey`/`Proof` are the decompressed, native-`G1Element`/`G2Element` working form the pairing check operates on. + +**Entry points** + +- `uncompress_vk(CompressedVK) -> VerifierKey`, `uncompress_proof(CompressedProof) -> Proof` - decode the wire format via native decompression. +- `verify(vk, proof, inputs) -> Bool` - the core verifier, operating on already-decompressed types. +- `verify_compressed(vk, proof, inputs) -> Bool` - convenience wrapper that decompresses then calls `verify`; the function a validator is expected to call. +- `pairing_check(...) -> Bool` and `derive(...) -> G1Element` - the two building blocks `verify` composes. + +## 4. Protocol walkthrough + +**Decompression.** `uncompress_vk`/`uncompress_proof` call `bls12_381_g1_uncompress`/`bls12_381_g2_uncompress` directly - the native Plutus builtins - for every point. This is a deliberate departure from `lib/common/common.ak`, which contains its own hand-rolled `g1_compress`/`g1_decompress` pair built from manual modular arithmetic (`mod_inv`, a Tonelli-Shanks `mod_sqrt`, and a `miller_loop`/`final_exponentiation` pair that are explicitly placeholder stand-ins, by their own comments, for real `Fp12` arithmetic). `groth.ak` does not use any of it. Every point this module handles is validated as a genuine, in-subgroup curve point by the native builtin at decompression time, not by this package's own field simulation. + +**Public-input combination.** `derive` folds the verification key's `vkIC` vector against the public inputs: `K = vkIC[0] + Σ inputs[i] · vkIC[i+1]`. It recurses on both lists in lockstep, terminating when `vkIC` is exhausted. If `vkIC` still has entries once `inputs` runs out, it hits an explicit `fail` - a guard against silently under-supplying public inputs. Note the asymmetric case: if `inputs` has *more* entries than `vkIC - 1` needs, the extra ones are never consumed and are silently ignored, since recursion stops as soon as `vkIC` is empty. This is safe (it cannot forge acceptance of a wrong statement, since the ignored inputs don't appear in the pairing at all) but is a latent inconsistency worth closing before this is exposed to arbitrary caller-supplied input lists (see §8). + +**Pairing check.** `verify` calls `pairing_check(A, B, C, delta, alpha, beta, K, gamma)`, which computes four Miller loops - `e(A,B)`, `e(alpha,beta)`, `e(K,gamma)`, `e(C,delta)` - combines the latter three with `bls12_381_mul_miller_loop_result`, and finishes with a single `bls12_381_final_verify(e(A,B), combined)`. This checks the canonical Groth16 equation `e(A,B) = e(alpha,beta) · e(C,delta) · e(K,gamma)` using the ledger-native pairing builtins throughout - there is no custom `Fp12` code anywhere in this path, unlike `common.ak`'s placeholder pairing functions. + +## 5. Design differentiation from a naive port and from `common.ak` + +**Verifier-only, by design, not by omission.** This module has no `generate_proof` and no setup routine. That is the correct shape for Groth16 in this context: the trusted setup is a circuit-specific ceremony that must be run once, off-chain, by parties independent of this codebase, and the proof itself requires a full R1CS/QAP witness computation this package does not and should not reimplement. Contrast this with `lib/bullet`, which owns both prover and verifier because Bulletproofs' public-parameter model makes that safe to do in one place; Groth16's trust model makes the equivalent choice here unsafe, so it isn't made. + +**Native decompression instead of `common.ak`'s field simulation.** As in §4, every group element in this module is validated by the audited native builtin at the point it enters the system, rather than by this package's own coordinate-wise modular arithmetic. This is the same departure documented in the Bulletproofs report for the `bullet` module, applied identically here: `common.ak` is retained in the package for reference/legacy reasons but is not part of the trusted path this verifier relies on. + +**Tested against externally-generated fixtures, not self-generated proofs.** Because Groth16's setup and proving are out of scope for this codebase, the three tests in `lib/tests/groth_tests.ak` verify fixed, externally-produced `(VK, proof, public_inputs)` triples rather than round-tripping a proof this package generated itself. This is the inverse of the Bulletproofs module's testing posture (§7 of the Bulletproofs report), where prover and verifier are co-tested in-language; here, the verifier is the only thing this codebase owns, so the fixtures stand in for a circuit and ceremony this codebase cannot itself produce. + +**A bare `Bool`, matching the rest of the package.** `verify`/`verify_compressed` return `Bool`, not a typed `Result`, for the same reason given in the Bulletproofs report: a Plutus validator ultimately reduces to accept/reject, and a bespoke error taxonomy per proof system isn't warranted. + +## 6. Security argument + +Soundness rests entirely on two facts holding simultaneously: the trusted setup's toxic waste (`tau`, and the per-circuit secret values it implies) was genuinely destroyed, and the four-pairing equation checked by `pairing_check` is exactly the Groth16 verification equation - no more, no less. This module does not, and cannot, verify the first fact; it is a precondition supplied by whichever ceremony produced the `VerifierKey` this module is given, and is entirely out of scope for on-chain code. What this module is responsible for, and what its tests exercise, is the second fact: that a proof failing to satisfy the true relation is rejected (§7's `groth_verify_fail_1`, where `A` and `C` are swapped relative to a valid proof) and that a genuine proof is accepted (`groth_verify_pass_1`/`_2`, against two different public-input sets on the same verification key). + +Because decompression goes through the native builtins, every `G1Element`/`G2Element` this module operates on is guaranteed by the ledger itself to be a valid, in-subgroup curve point - the small-subgroup and invalid-curve attack classes that a hand-rolled decompression routine would need to defend against explicitly are handled upstream, before this module's own logic ever runs. + +## 7. Testing and verification + +Three tests exercise this module, alongside the Bulletproofs and PLONK suites in the same package: + +| Test | Verifies | +|---|---| +| `groth_verify_pass_1` | A genuine proof against a 2-public-input circuit verifies | +| `groth_verify_fail_1` | A proof with `A` and `C` swapped is rejected (`test ... fail`) | +| `groth_verify_pass_2` | A second genuine proof, different public inputs, same verification key, verifies | + +All three tests measure identically: ~66.9K memory units and ~2.79B CPU units per `verify_compressed` call - comfortably inside Cardano's per-transaction execution budget, and the cheapest of this package's three verifiers by a wide margin, as expected given Groth16's constant-size, pairing-only verification equation. + +## 8. Known limitations and roadmap + +- **No trusted-setup tooling.** This module consumes a `VerifierKey` but has no way to generate or attest to one; that must come from an external, circuit-specific ceremony this package neither runs nor audits. +- **No on-chain prover, by design (§5).** Proof generation is out of scope; a production integration needs its own off-chain Groth16 prover (e.g. `snarkjs`, `arkworks`, or a `gnark` toolchain) feeding this verifier. +- **`derive`'s length-mismatch handling is asymmetric.** Too few public inputs traps (safe); too many are silently truncated rather than rejected (also safe today, but worth tightening to an explicit length check before this function is exposed to less-trusted callers). +- **Only two verification-key shapes have been exercised in tests**, both with `n_public = 2`. Larger `vkIC` vectors (more public inputs) are structurally supported by `derive`'s recursion but are unbenchmarked for execution-unit cost. +- **No on-chain entry point yet.** Like the other two modules in this package, how a validator obtains and trusts a given `VerifierKey`/proof pair (datum/redeemer wiring) is separate, follow-on work. +- **No external cryptographic audit.** As with the rest of this package, internal design review only; not a substitute for a formal audit before mainnet or high-value use. + +## 9. Conclusion + +This module delivers a functional, correctly-rejecting Groth16 verifier built entirely on native BLS12-381 pairing and decompression builtins, deliberately scoped to verification alone. Its narrow scope is itself a design decision: Groth16's trusted-setup and full-witness-computation requirements are two significant pieces of infrastructure this package correctly declines to reimplement, in favor of a small, cheap, auditable verifier that composes with whatever external toolchain a deployment already trusts to produce proofs and keys. diff --git a/zkp/docs/plonk-implementation-report.md b/zkp/docs/plonk-implementation-report.md new file mode 100644 index 0000000..cc66191 --- /dev/null +++ b/zkp/docs/plonk-implementation-report.md @@ -0,0 +1,113 @@ +# PLONK Verifier - Implementation Report + +- **Module:** `zkp/lib/plonk/{preinputs,proofs,raw,raw_affine,verifier}.ak` +- **Status:** Functional, tested, unaudited +- **Test results:** + - `aiken check` 12/12 in `tests/plonk_tests`, plus 12/12 in the closely-related `tests/point_tests` (part of 37/37 across the package) + - `aiken fmt` clean + - `aiken build` succeeds + +## 1. Overview + +This module implements a PLONK zk-SNARK verifier over the BLS12-381 curve, as one of three zero-knowledge proof systems in this repository's `zkp` package for Cardano smart contracts (Aiken, targeting Plutus V3). Given a universal-but-still-trusted verification key, a proof, and a list of public inputs, it checks the standard PLONK gate/permutation/quotient identity via a batched KZG opening, using a Keccak-256 Fiat–Shamir transcript matching the `snarkjs`-style compressed-commitment variant of the protocol. + +Like `lib/groth`, this module implements **verification only** - PLONK's universal SRS still requires a trusted setup, and generating a proof requires a full circuit compiler and witness computation this codebase does not reimplement, consistent with this package's own design notes (`docs/step-by-step.md`). + +This is the most structurally complex of the three modules in this package, spread across five files rather than one, because the verification key and proof each need to flow in through more than one representation before reaching the actual pairing check. + +## 2. Position within the `zkp` package + +| Module | Proof system | Setup | Core primitive | +|---|---|---|---| +| `lib/groth` | Groth16 | Trusted, circuit-specific | Pairings (`bls12_381_miller_loop`, `bls12_381_final_verify`) | +| `lib/plonk` | PLONK | Universal, trusted | Kate (KZG) commitments, permutation argument | +| `lib/bullet` | Bulletproofs | Public, trustless | Discrete-log / Pedersen commitments, no pairings | +| `lib/common` | — | — | Shared field/point scaffolding, superseded in this module (see §4) | + +PLONK's universal SRS (reusable across circuits, unlike Groth16's circuit-specific one) is the reason this module exists alongside `groth`: it trades a one-time-per-circuit ceremony for a one-time-ever ceremony, at the cost of a larger, more expensive verification equation - the most expensive of this package's three verifiers per call (§7). + +## 3. Architecture + +**Files and roles** + +- `preinputs.ak` - `PlonkPreInputs` (compressed-bytes verification key) and `PreparedPlonkPreInputs` (decompressed, with the evaluation-domain data filled in); `plonk_prepare_preinputs` converts one to the other. +- `proofs.ak` - `PlonkProof` (compressed-bytes proof, `Int` evaluations) and `PreparedPlonkProof` (decompressed, `Scalar` evaluations, plus a derived `lagrange_inverses` hint); `plonk_prepare_proof` converts one to the other. +- `raw.ak` / `raw_affine.ak` - two alternate front doors that accept a verification key/proof expressed in this package's own point types rather than raw compressed bytes, and route them into the same `PreparedPlonkPreInputs`/`PlonkProof` pipeline (see §5 for why there are two, and why they aren't equivalent in what they trust). +- `verifier.ak` - `verify_plonk`, the actual pairing-and-permutation check. + +**Key types** + +``` +PlonkPreInputs { power, k1, k2, q_m, q_l, q_r, q_o, q_c, s_sig1, s_sig2, s_sig3, x2 } // compressed bytes + coset scalars +PreparedPlonkPreInputs { n, generator, generators, ...same fields decompressed to G1Element/G2Element } +PlonkProof { commitment_a/b/c/z, t_low/mid/high, w_omega, w_omega_zeta, a_eval, ... } // compressed bytes + Int evals +PreparedPlonkProof { ...same, decompressed, plus lagrange_inverses: List } +``` + +`power` is `log2` of the evaluation-domain size (`n = 2^power`); `k1`/`k2` are the coset generators separating the three permutation copies; `x2` is the SRS's `[x]_2` G2 element the pairing check is anchored to. + +**Entry points** + +- `plonk_prepare_preinputs` / `plonk_prepare_proof` - decompress and derive the working forms from the compressed-bytes types. +- `vkey_to_prepared_preinputs` / `prepare_raw_proof` (`raw.ak`) and `prepare_affine_vkey` / `prepare_affine_proof` (`raw_affine.ak`) - convenience conversions from this package's own point representations. +- `verify_plonk(preinputs, pub_inputs, proof) -> Bool` - the verifier; the only function a validator needs. + +## 4. Protocol walkthrough + +**Transcript.** `verify_plonk` re-serializes every preinput and proof commitment to its compressed byte form (`g1.compress`) and re-derives the full Fiat–Shamir transcript with `keccak_256`, in the same order and grouping a matching off-chain prover would have used: `beta` over all selector/permutation/public-input/wire-commitment bytes, `gamma = keccak256(beta)`, `alpha` additionally over `commitment_z`, `zeta` additionally over the quotient commitments, `v` additionally over all six scalar evaluations, and `u` over the two opening-proof commitments. Nothing about this transcript is trusted from the prover; every challenge is recomputed independently from committed values already fixed earlier in the same transcript. + +**Public-input evaluation.** For each public input position `i`, the verifier needs `L_i(zeta)`, the Lagrange basis polynomial evaluated at the challenge point, whose closed form is `L_i(zeta) = (zeta^n - 1)·ω^i / (n·(zeta - ω^i))`. Computing that division on-chain via modular exponentiation (Fermat's little theorem, `a^(p-2)`) is expensive - roughly 254 scalar multiplications per public input. Instead, `PreparedPlonkProof.lagrange_inverses` carries the *already-computed* inverses as an untrusted, prover-supplied hint (computed off-chain once, in `plonk_prepare_proof`, via exactly that exponentiation), and `verify_plonk` checks each one with a single cheap multiplication: `inv · (n·(zeta - ω^i)) == 1`. This is the same class of optimization as Bulletproofs' disclosed-vector approach documented in this package's other report: replace an expensive on-chain computation with a cheap on-chain check of an off-chain-computed value. + +**Linearization and batching.** The verifier computes the PLONK linearization polynomial `r(zeta)` (folding in the public-input evaluation, the permutation grand-product argument via `alpha`/`beta`/`gamma`, and the quotient polynomial split into low/mid/high parts), then batches every polynomial commitment the identity depends on - the three gate-selector commitments scaled by witness evaluations, the permutation commitment `Z`, the third permutation-sigma commitment, and the quotient commitments - into a single combined commitment via the `v` challenge, following the standard batched-KZG technique that collapses what would otherwise be several separate opening checks into two. + +**Pairing check.** Two Miller loops are computed: one pairs the combined opening-proof commitments (`w_omega + u·w_omega_zeta`) against `x2` (the SRS point), the other pairs a combination of `zeta`-scaled and `u·zeta·ω`-scaled opening commitments plus the batched polynomial/evaluation difference against the G2 generator. `final_exponentiation` on the two combined results is the actual KZG-opening acceptance check. + +**Final acceptance.** `verify_plonk` returns `final_verification && lagrange_check` - both the batched-KZG pairing check *and* the independent verification of every Lagrange-inverse hint must hold. Neither alone is sufficient: the pairing check alone would trust unverified Lagrange inverses (letting a prover misstate the public-input polynomial evaluation), and the Lagrange check alone says nothing about the constraint system itself. + +## 5. Design differentiation and notable implementation choices + +**Two "raw" front doors with different trust postures.** `raw.ak` accepts a verification key/proof expressed in `common/common.ak`'s legacy projective `Point`/`G2Point` types, and converts them to compressed bytes using `common.ak`'s own hand-rolled `g1_compress`/`g2_compress` - which, per §4 of this package's Bulletproofs report, perform manual modular inversion (`mod_inv` via extended Euclidean algorithm) and a Tonelli–Shanks `mod_sqrt` to go from projective to affine to compressed form. `raw_affine.ak` accepts the same data already in affine `G1Affine`/`G2Affine` form (from `common/blst_affine.ak`) and compresses it with `g1_affine_compress`/`g2_affine_compress`, which do no curve arithmetic at all - they only set the two header flag bits on x/y bytes the caller already supplied in affine form. Both paths ultimately hand their output to the native `g1.decompress`/`g2.decompress` builtins inside `plonk_prepare_preinputs`/`plonk_prepare_proof`, which do validate curve membership - but `raw.ak`'s path additionally depends on `common.ak`'s own field arithmetic being correct *before* that native check ever runs, since a bug in that hand-rolled compression could mis-serialize a legitimate point into something that either fails to decompress or - worse - decompresses to the wrong point. `raw_affine.ak` carries no equivalent risk, since it does no arithmetic. New integrations should prefer `raw_affine.ak`, or compressed bytes directly, over `raw.ak` (see §8). + +**Transcript derivation happens twice, deliberately.** `plonk_prepare_proof` (in `proofs.ak`) independently recomputes `beta`, `gamma`, `alpha`, and `zeta` - the same challenges `verify_plonk` will later recompute a second time from scratch - purely to derive the `lagrange_inverses` hint at prepare-time. This is not redundant from a soundness standpoint: `verify_plonk` cannot trust `zeta` (or any other challenge) as supplied by whatever prepared the proof, since a party controlling that value could otherwise choose a favorable challenge. Recomputing the full transcript inside `verify_plonk` itself is what makes the challenges binding; the earlier computation in `plonk_prepare_proof` only exists to produce the (also independently re-checked) Lagrange-inverse hint before the proof is placed in a datum or redeemer. + +**Batched KZG rather than one pairing per polynomial.** A naive implementation of PLONK's verification equation would check each committed polynomial's opening separately - on the order of 7-9 individual pairings. This module follows the standard batching technique (via the `v` and `u` challenges) that folds all of them into exactly two Miller loops and one final exponentiation, which is the difference between an unusably expensive verifier and one that fits a single Cardano transaction (§7). + +**A bare `Bool`, matching the rest of the package.** As with `groth` and `bullet`, `verify_plonk` returns `Bool` rather than a typed error, for the same reason: a Plutus validator ultimately reduces to accept/reject. + +## 6. Security argument + +PLONK's soundness rests on three layers this module is responsible for enforcing together, none of which is sufficient alone: the gate constraints bind `(a, b, c)` to values satisfying the circuit's arithmetic at every domain point; the copy-permutation argument (via `alpha`, `beta`, `gamma`, and the grand-product commitment `Z`) binds those same wire values to a consistent single execution trace across gates; and the batched KZG opening binds every polynomial evaluation the verifier trusts (the constraint identity, the permutation argument, the quotient split) to the actual committed polynomials, under the standard KZG discrete-log assumption over the SRS. All of this is checked at one random point `zeta`, via a Schwartz–Zippel argument: a prover who did not honestly satisfy the constraint and permutation identities as full polynomials would need the identity to coincidentally hold at a point they could not have predicted before committing. + +The two things this module's `verify_plonk` actually asserts - `final_verification` (the batched pairing check) and `lagrange_check` (every Lagrange-inverse hint is a genuine field inverse) - are, together, the complete on-chain expression of that argument. As with Groth16, this module does not and cannot verify that the SRS's toxic waste was destroyed; that is a precondition of whichever ceremony produced `x2`, entirely out of scope for on-chain code. + +## 7. Testing and verification + +Twelve tests in `tests/plonk_tests.ak` exercise this module directly, against a single external test-vector pair (`n_public = 2`, `power = 3`, i.e. an 8-point evaluation domain) presumably produced by an external PLONK toolchain (the code's own transcript ordering explicitly targets "snarkjs's keccak256-compressed transcript variant"), since - as with Groth16 - this codebase implements no PLONK prover or setup of its own: + +| Test | Verifies | +|---|---| +| `test_vkey_g1_compression` / `test_vkey_g2_compression` | Every vkey point compresses without error | +| `test_preinputs_creation` / `test_plonk_prepare_preinputs` | `PlonkPreInputs` construction and preparation succeed | +| `test_prepare_vkey_function` / `test_prepare_affine_proof_function` | The `raw_affine.ak` convenience wrappers succeed | +| `test_generator_value` / `test_power_calculation` / `test_generator_list_creation` | The evaluation-domain scalars (`ω`, `2^power`, `ω^i` list) are computed correctly | +| `test_plonk_verification_with_affine_points` | A genuine proof against the fixture verification key verifies | +| `test_plonk_verification_rejects_tampered_proof` | Mutating `a_eval` by 1 is rejected (`test ... fail`) | +| `test_plonk_verification_rejects_wrong_pub_inputs` | Substituting a different public-input list is rejected (`test ... fail`) | + +`tests/point_tests.ak` (12 further tests, also part of the package's 37) directly exercises `common/blst_affine.ak`'s compression and curve-membership helpers against this same fixture's proof and verification-key points, closing the loop on the affine front door described in §5. + +`test_plonk_verification_with_affine_points` measures approximately 6.68M memory units and 8.63B CPU units - by far the most expensive single call among this package's three verifiers (compare Groth16's ~66.9K mem / 2.79B cpu and Bulletproofs' range proof at ~5.2M mem / 14.2B cpu at `n=8`), and leaves markedly less headroom against Cardano's per-transaction budget than either. Cost scales with `n_public`: each additional public input adds both a Lagrange-inverse check and a term in the public-input polynomial evaluation; only the 2-public-input fixture has been measured. + +## 8. Known limitations and roadmap + +- **No trusted-setup tooling.** This module consumes `x2` (and the rest of the verification key) but has no way to generate or attest to a universal SRS; that must come from an external ceremony (e.g. Perpetual Powers of Tau plus a circuit-specific phase 2) this package neither runs nor audits. +- **No on-chain prover, by design (§5).** Proof generation, circuit compilation, and preprocessing are all out of scope; a production integration needs its own off-chain PLONK toolchain feeding this verifier. +- **`raw.ak`'s legacy compression path carries more risk than `raw_affine.ak`'s (§5).** New integrations should prefer `raw_affine.ak` or pre-compressed bytes; `raw.ak` should be revalidated against `common.ak`'s field-arithmetic correctness, or retired, before further use. +- **Execution-unit cost is only measured at `n_public = 2`.** This is the most expensive verifier in the package per call already; larger public-input counts should be benchmarked before use in a real deployment. +- **No on-chain entry point yet.** Like the other two modules in this package, how a validator obtains and trusts a given verification key/proof pair (datum/redeemer wiring) is separate, follow-on work. +- **No cross-implementation interoperability testing beyond one fixture.** The transcript and batching scheme are documented as matching a `snarkjs`-style variant, but only one externally-produced proof has been used to validate that against this implementation; broader test vectors are future work. +- **No external cryptographic audit.** As with the rest of this package, internal design review only; not a substitute for a formal audit before mainnet or high-value use. + +## 9. Conclusion + +This module delivers a functional PLONK verifier built on native BLS12-381 pairing and decompression builtins, using the standard batched-KZG technique to keep a verification equation that would otherwise require many separate pairings down to two Miller loops and one final exponentiation. Its two-hint design (Lagrange inverses computed off-chain, checked cheaply on-chain) and its two alternate raw-input front doors are documented, deliberate engineering choices; the clearest remaining gaps are the ones every verifier-only module in this package shares - no owned trusted setup, no owned prover, and no external audit - plus one specific to this module: `raw.ak`'s dependency on legacy field arithmetic that `raw_affine.ak` avoids entirely.