Research Notes: What Zero-Knowledge Proofs Enable on CKB

gm @ArthurZhang,

I’d hoped to respond to this earlier, but life has been doing its thing!

I’ve taken time to go through the CellScript codebase to better understand some of the technical decisions and approaches you’ve taken.

Before going item by item, I’d like us to note three things. Please feel free to correct me or ask for clarification here or via DM.

  1. This post and the issue were both written when zk-Lock was at M1. I’ll respond beyond M1, since I’ve made progress since then and I believe it might be helpful.
  2. I’ve gone through the 2026-09-19 scope clarification, and nothing here is a claim about 0.30 release scope. This is Phase 0 review input, structured along the five items you flagged on the forum.
  3. Your 2026-09-23 remaining-work review on issue #22 landed while I was finalizing this, so the structure below predates it. It maps onto your four Phase 0 deliverables in part:
    • Item a speaks to your first, on which values bind at creation versus construction versus Script execution.
    • Items b, c and d speak to your third, on pinning one exact profile.
    • Item e speaks to your fourth only in part. Your fourth asks for shared vectors and a child fixture covering partial I/O, descriptor ownership, child failure and an ignored result; those need a spawned child, which I have not built. What I have is the adversarial matrix and a negative-fixture suite for the directly linked case.
    • Your second, I can answer in part. I have benchmarked the actual artifact for the directly linked case and measured both locks for item e, but I have not pinned candidate revisions and licenses, and my numbers come from ckb-testtool rather than a selected CKB/VM profile. I can’t speak to a Spawn/IPC adapter at all, for the reason you give there yourself.

a) Proof-gate vs dynamic-transition semantics

The profile split looks clean to me. Since I refer back to it throughout, let me fix the two labels I will be using for the profiles you named:

  • Profile 1, the creation-time proof-gate. vk_hash and the public-input commitment are fixed in the locked Cell’s args when the Cell is created. The proof is checked against values that were decided before the spending transaction existed.
  • Profile 2, the dynamic transition verifier. Public inputs are derived at spend time from the exact old Cells, the proposed outputs, the action, Script identity and replay context. The proof is checked against values that only exist once the transaction is assembled.

The difference that matters downstream is when the public inputs are decided. In profile 1 they are frozen at creation, so the lock only has to compare hashes. In profile 2 the script has to compute them from the transaction in front of it, which is where the codec, the PI schema and the replay binding all stop being conventions and start needing a spec.

Profile 1 is what M1 is (zk-Lock, How it works). I haven’t built profile 2 yet; that one is still your Phase 0 proposal.

With the addition of zk-lock-bound and what it actually does, I think we might need a name for a middle case. I’d propose splitting the axis into three:

Position vk_hash Statement pi Context pi Where it lives
Pure static creation-committed creation-committed via pi_commitment none zk-lock (M1)
Committed VK + spend-derived context creation-committed creation-committed via pi_commitment spend-derived (pi[0]) zk-lock-bound (PR #4)
Full dynamic transition CellDep-resolved fully spend-derived (same) not yet built for profile 2

zk-lock-bound gets to the middle by reserving pi[0] for a transaction-context scalar:

  1. Off-chain, the caller derives:

    pi[0] = blake2b_ckb(input_outpoint || blake2b_ckb(output0_cell || output0_data))[..31] || 0x00
    
    
  2. On-chain, the parent script re-derives that scalar from the tx it runs against and rejects any proof whose pi[0] disagrees.

  3. In the circuit, pi[0] is exposed as a public input but left unconstrained; it flows straight through to the verifier.

The one thing that came out of building this is that there are two different kinds of binding in play, and only one of them needs the circuit.

  • What the proof is about has to be constrained inside the circuit. That is the statement, and there is nowhere else to put it.
  • Which transaction the proof is allowed to be used in does not. That can sit in a public input the circuit declares but never constrains, because the parent script is what checks it: the slot travels with the proof, and the script refuses the spend unless the value in it matches the transaction actually being executed.

The practical payoff is that adding a replay binding costs one public input and a handful of lines in the lock. The circuit is otherwise unchanged.

I flagged this shape in the groth16-ckb threat model, §4.5 Replay:

This is a property of the protocol that uses the verifier, not of the verifier itself. The protocol designer is responsible for adding any per-cell binding they need (for example, mixing the spent OutPoint into the public inputs).

zk-lock-bound is what that pattern looks like once you build it: the circuit proves the statement, and the parent script enforces the tx-context binding. I’m not sure whether that layer split is an axis you’re already thinking about in the source model, but it seemed worth flagging.

b) VK/verifier identity and CellDep resolution

A note on the word first, since I think we may be using it for two different things.

When you say “verifier”, I read it as a separately addressable on-chain contract: the child your transition script Spawns and talks to over IPC, and the thing verifier_contract_id is meant to name. zk-lock has nothing of that kind. The Groth16 proof checking is verifier_core, a Rust crate linked into the lock binary at compile time, so it has no code_hash and no outpoint of its own. It is a function call inside the lock, not a contract the lock calls out to.

So in zk-lock as it stands on main, the verifier in your sense is the lock script itself. No Spawn, no child, no IPC. The verifier_contract_id you sketched collapses to two things:

  1. The lock’s own code_hash and hash_type, chosen at deployment by whoever creates the locked cell.
  2. The vk_hash fixed in lock.args.

Everything else on your list is implicit in the binary the code_hash resolves to. The Groth16/BN254 curve, the pairing engine, the public-input layout and the codec are not separately committed fields; they are whatever the binary that hashes to code_hash actually does.

Here is a mapping onto your contract components as I currently see it:

verifier_contract_id field zk-lock Where it lives
Profile ID + version implicit in the lock binary
IPC ABI + version not applicable no IPC
RISC-V executable hash lock code_hash Script struct on the locked cell
Target + VM profile implicit in the lock binary
VK commitment vk_hash first 32 bytes of lock.args
Statement schema hash implicit in the circuit that produced the VK
Proof + PI codec IDs implicit in the lock binary
Runtime limits not enforced out of scope for zk-lock right now

CellDep resolution for the VK is done by data hash. I iterate Source::CellDep with QueryIter::new(load_cell_data_hash, ...), match against the vk_hash from args, and treat the matching cell’s data as the VK bytes (main.rs).

This gives data_hash-mode binding on the VK cell, with no DepGroup, no positional-index trust and no name lookup. A wrong CellDep at the expected slot fails the match; a matching CellDep at any position resolves. If two CellDeps carry the same vk_hash, the script aborts with VKeyDuplicated rather than picking one, so resolution is either unambiguous or it fails.

Against your required rules:

Rule Status Notes
A verification key supplied solely by witness cannot define the accepted verifier contract. Satisfied VK bytes come from CellDep and must hash to the args-committed vk_hash; a witness cannot rewrite that.
A raw CellDep index is not a verifier identity. Satisfied The index is not trusted; the cell is found by its data hash.
data_hash, type_hash, Type ID and outpoint policies remain distinct. Partial The VK cell is bound by data_hash only. The other three are not modeled.
DepGroup resolution must bind the actual spawned member, not merely the container name. N/A No DepGroup, no Spawn.
Registry package name is discovery metadata, not consensus authority. N/A No Registry lookup happens at spend time.
Upgradeable verifier requires the explicit receipt/upgrade model from #11. N/A The verifier binary is the lock. Any upgrade is a redeployment under a new code_hash, and existing locked cells stay bound to the old one.

The current gap: zk-lock has no separation between “which verifier” and “which lock.” I’d strongly suggest that profile 2 has to reintroduce that separation. The CellScript transition script is one identity and the verifier it spawns is another, so the multi-component verifier_contract_id becomes non-trivial because its components live in different places:

  • source policy name
  • package metadata
  • deployment record
  • resolved CellDep
  • spawned child

zk-lock gets by with a flat identity because the lock and verifier collapse into one. I don’t think profile 2 has that option.

c) Canonical proof/public-input codecs and WitnessArgs placement

zk-lock on main has one wire format and no version byte. Nothing in the on-chain script identifies the curve, the proof system or the codec; those are implicit in the binary that code_hash resolves to.

The CLI enforces protocol == "groth16" and curve == "bn128" when it produces the artifacts (encode.rs), but that check is off-chain. The on-chain script trusts that the bytes handed to it are what verifier_core expects.

Byte layouts

VK

  • Layout: ark_serialize::serialize_compressed on WireVk { alpha: G1Affine, beta: G2Affine, gamma: G2Affine, delta: G2Affine, ic: Vec<G1Affine> }. Compressed BN254 points, arkworks canonical layout.
  • Length: variable; depends on ic.len(), which equals nPublic + 1.
  • Source: encode.rs

Proof

  • Layout: WireProof { a: G1Affine, b: G2Affine, c: G1Affine }, same arkworks compressed layout.
  • Length: fixed 128 bytes.
  • Source: encode.rs; PROOF_LENGTH in main.rs

Public inputs

  • Layout: 4-byte LE u32 count n, then n * 32 bytes of compressed Fr scalars. The count prefix is part of the wire format, not just a framing hint.
  • Length: 4 + n * 32 bytes.
  • Source: encode.rs

WitnessArgs placement

Everything spend-side lives in WitnessArgs.lock on group input 0 (main.rs). The layout is not written down anywhere in the script; it is what the slicing implies, so I am spelling it out here:

witness_args.lock = proof (128 bytes) || pi_count (4 bytes LE) || pi[0..n] (n*32 bytes)

The script rejects a witness lock shorter than 128 + 4, then splits at offset 128. There is no input_type or output_type involvement; the lock slot carries the whole spend-side payload for this script.

What is committed vs. checked

  • vk_hash (first 32 bytes of lock.args) is compared against the CKB data hash (blake2b-256 personalized with ckb-default-hash) of a CellDep cell’s data. A match binds these VK bytes and no others.
  • pi_commitment (next 32 bytes of lock.args) is compared against blake2b_ckb(pi_field_elements), where pi_field_elements is the PI section without the 4-byte count prefix (main.rs). The commitment binds the field-element bytes only; a rewrite of the count would fail the length check on the next line, not the commitment.
  • Proof bytes are handed to verifier_core::verify unchecked at the outer layer; validity is the verifier’s job.
  • verifier_core::verify(&vkey_bytes, proof_bytes, pi_bytes) receives pi_bytes with the count prefix (main.rs). The verifier re-parses it; this is the boundary where the outer layout meets the arkworks deserializer.

What is not present

  • No codec ID or version byte. If arkworks changes its compressed layout, or if I switch curves, existing locked cells silently break. They become unspendable, not unsafe.
  • No curve/protocol identifier on-chain. verifier_core is a linked dependency, so the identifier collapses into code_hash.
  • No proof length declaration in the witness. PROOF_LENGTH = 128 is a compile-time constant, correct for BN254 Groth16 only.
  • No signature or per-user binding on the witness lock. Anyone who has the proof and PIs can post the tx. That is the whole point of a proof-gate, but I flag it so the mapping to profile 2 is honest.

Against profile 2

For a dynamic transition verifier where the VK is CellDep-resolved and the PIs are spend-derived, a fixed-length proof and a bare compressed-Fr array won’t be enough. The transition script has to negotiate at least three things the current codec elides:

  1. Codec identity. Which curve, which serialization, which field-element count. Today those are implicit in code_hash. In profile 2, the transition script and the spawned verifier are separate identities, so the codec ID has to become an explicit component of verifier_contract_id (item b) or an explicit field in the IPC envelope.
  2. PI schema. The transition script produces PIs from tx state and the verifier consumes them. Both need to agree on field order, framing, and which slots are reserved for context bindings (item d).
  3. Witness slot placement. WitnessArgs.lock is already claimed by the outer lock in most CKB scripts. A transition verifier that is not the lock will need input_type or a separate witness carrier, and the ABI has to say which.

None of this is a problem in profile 1 really, because the lock is the verifier and everything is by convention. It becomes the design surface once they separate.

d) Mandatory transition/replay bindings

zk-lock on main enforces no transaction-context binding at all. A valid (proof, pi) pair unlocks any cell that carries the same (vk_hash, pi_commitment) in its args. Two attack classes fall out of that:

  • Mempool witness-copy. An attacker copies the unlock witness from a broadcast tx into their own tx that consumes a different cell locked to the same args, if one exists.
  • Recipient-redirect. An attacker rewrites outputs to pay their own lock, since the proof does not commit to outputs.

This is exactly the gap I flagged in threat-model §4.5 Replay: the verifier proves the statement; per-cell binding is the protocol’s problem, not the verifier’s.

zk-lock-bound (PR #4) is the middle case from item a. It closes both attacks by reserving pi[0] for a transaction-context scalar and re-deriving it on-chain:

expected_pi0 = blake2b_ckb(input_outpoint || blake2b_ckb(output0_cell || output0_data))[..31] || 0x00

The zero top byte keeps the scalar below the BN254 modulus.

The on-chain check (zk-lock-bound/main.rs, PR #4):

  1. Loads input(0, GroupInput).previous_output().
  2. Loads the output(0) cell struct and its data, and hashes them together.
  3. Concatenates the outpoint with that hash and hashes again to get the expected scalar.
  4. Splits the PI section into context_pi = pi[0] and body_pi = pi[1..].
  5. Hashes body_pi (not the whole PI section) and compares it against pi_commitment from args.
  6. Compares context_pi byte-for-byte against the expected scalar.
  7. Falls through to verifier_core::verify(vk, proof, pi_bytes) with the full PI section, context included.

Two commitment surfaces, one witness. The circuit sees pi[0] as a public input but does not constrain it; the parent script binds it. This is what the §4.5 position, that the protocol enforces per-cell binding, looks like in code.

Against your item

Arthur, your fourth forum item asks for a mandatory replay binding on the transition profile. My honest reading of what I have:

Implementation Binding Assessment
zk-lock on main None Acceptable as a profile 1 minimum only under a “one lock cell per proof” deployment convention, which is a strong assumption a protocol should not make.
zk-lock-bound (PR #4) Input outpoint + output(0) cell and its data Works for a single-cell unlock. Does not generalize to multi-cell transitions.
Profile 2 transition verifier Not built Needs coverage over the whole tx that mutates state. Input outpoint alone is not sufficient once the transition consumes and produces N cells.

What “mandatory” should mean, from my side:

  1. The binding lives in the parent script, not solely in the circuit. Circuits enforce the statement; parent scripts enforce the tx context. Mixing them makes the circuit brittle and expensive.
  2. Reserved PI slots are the ABI. pi[0], or whatever range is chosen, is the contract between the transition script and the verifier: this many scalars are context, the rest is the statement. Profile 2 needs that range to be part of verifier_contract_id (item b) or the IPC envelope.
  3. The binding target has to match the transition shape. For a single-cell unlock, (input_outpoint, output(0) + its data) is fine. For a K-cell to M-cell transition, the binding target has to normalize over both sides: a hash of the sorted input outpoints together with a hash of the outputs, using a fixed serialization the prover can mirror off-chain.
  4. Canonicalization matters. Whatever bytes the parent script feeds to blake2b, the prover has to reproduce exactly. zk-lock-bound does this by using CKB Molecule’s as_slice() for the outpoint and the output cell struct, which is stable because Molecule is. Anything ad hoc would drift.

What the tests actually show

Since PR #4 is what I am pointing you at, here is what stands behind the claim. The bound suite covers:

  • args length
  • VK resolution and duplication
  • the missing and too-short witness
  • the PI length invariant
  • a zero PI count
  • a bad body commitment
  • a tampered pi[0]
  • output substitution, output-data substitution and input substitution
  • a generic-layout witness replayed at the bound lock
  • a control that confirms a correct pi[0] gets past every pre-Groth16 check and fails inside the verifier instead
  • a success path that verifies a real proof end to end against the 2-public-input circuit

Two things about how they are written, because I don’t think a passing negative test means much on its own.

Every test asserts a specific script error code rather than is_err(). That matters more than it sounds. A rejection test that only checks for failure still passes when the check it targets is deleted, because some later check fails instead. Pinning the code is what makes the test bind to the behaviour it names.

I verified that by mutation. Deleting the context comparison from the script breaks exactly the four binding tests and nothing else. Deleting the body-commitment, pi_count, duplicate-VK and PI-length checks each breaks only its own tests. Before the error codes were pinned, none of those deletions broke anything at all.

One result worth reporting, because it was not what I expected: a generic zk-lock witness posted at the bound lock fails on the body commitment, not on the context check. The bound lock commits to pi[1..] while the generic args commit over pi[0..], so the two args layouts are not interchangeable at all, quite apart from the binding. That is a stronger argument for treating these as separate profiles than the one I made above, and it is the kind of thing a shared codec ID would make explicit rather than accidental.

What I have not built

The multi-cell case. zk-lock-bound binds output(0) and input(0, GroupInput). If a real transition needs to bind all outputs and all group inputs, the parent script has to normalize them (sort, length-prefix, hash) before folding them into the scalar. That is a small amount of code but a big design question, because the normalization is what protocol authors will get wrong.

The gap I would flag for profile 2 is that there is no shared “context hash” spec. In zk-lock-bound I chose one that works for its shape. If every transition verifier chooses its own, the CellScript source model gains a hidden compatibility axis. A canonical binding envelope, or a small set of them (one per common transition shape), would help.

e) Adversarial and resource-evidence matrix

The groth16-ckb threat model covers the verifier itself. zk-lock inherits everything under “verifier proves the statement” and adds a small lock-side surface on top. In this section I tabulate both against the axes I read out of your Issue #22, marking what I have evidence for and calling out where the evidence stops.

Attacker model

The attacker controls:

  • the witness bytes on any tx they submit
  • the contents and placement of any CellDep they include, subject to CKB’s data_hash binding
  • the transaction structure

They can run unlimited offline computation, observe on-chain state, and craft transactions arbitrarily.

The attacker cannot: break BN254, forge a blake2b_256 collision on cell data, or bypass CKB-VM accounting.

Trusted: CKB consensus, the CKB-VM, ckb-std host calls, and the pinned arkworks crates.

Matrix

1. Forge a (proof, pi) that verifies against a genuine VK

  • Surface: witness lock bytes
  • Mitigation: Groth16 pairing check, plus explicit infinity rejection and subgroup validation on every G1/G2 slot; canonical Fr/Fq decoding; count + 1 == ic_len cross-check before deserialization
  • Evidence: threat model §4.1; differential and property tests; libFuzzer target verify_arkworks.rs

2. Substitute a weaker VK at spend time

  • Surface: CellDep set
  • Mitigation: vk_hash in lock.args compared against the CKB data hash of the resolved CellDep; a wrong VK fails the match, a missing VK fails resolution, and two matching CellDeps fail as VKeyDuplicated
  • Evidence: zk-lock main.rs L47-58; threat model §4.4

3. Panic the script via an oversized length prefix (ic_len, pi_count)

  • Surface: witness bytes; VK bytes
  • Mitigation: length pre-checks with checked_mul against per-element size and buffer length, before any allocation
  • Evidence: threat model §4.2; tests vk_with_oversized_ic_len_is_rejected_without_oom and public_inputs_with_oversized_count_is_rejected_without_oom

4. Exhaust the cycle budget

  • Surface: any oversized input
  • Mitigation: per-PI cost bounded; ~121M cycles measured at N=64 PIs; each additional PI adds ~270-300k cycles
  • Evidence: threat model §4.2; benchmarks in integration-tests/tests/cycles.rs

5. Panic via unwrap/expect/unreachable

  • Surface: any input
  • Mitigation: deny(clippy::unwrap_used / expect_used / panic / unreachable) on verifier-core and wire-decode, plus Result propagation through groth16-ckb’s script entry. The zk-lock lock script is not under those lints and carries one unwrap on a slice the preceding length check already guarantees
  • Evidence: threat model §4.2; zk-lock main.rs L72

6. Exploit the Molecule decoder

  • Surface: witness/VK Molecule payloads (verifier profile with Molecule schema)
  • Mitigation: Reader::from_slice validates offsets, item counts and fixed-array sizes up front; version pinned; union dispatch exhaustive at the type level
  • Evidence: threat model §4.3; fuzz targets decode_vk_molecule.rs, decode_witness_molecule.rs

7. Replay a witness against a different cell locked to the same (vk_hash, pi_commitment)

  • Surface: witness bytes reused across cells
  • Mitigation: zk-lock on main: no mitigation. zk-lock-bound reserves pi[0] for the tx-context scalar above and rejects a witness whose pi[0] disagrees with the tx it runs against
  • Evidence: item d; zk-lock-bound PR #4; tests_bound.rs covers output substitution, output-data substitution, input substitution, a tampered pi[0], a cross-layout witness replay, and a success path on a real proof. Error-code pinned and mutation-verified; see “What the tests actually show” in item d

8. Redirect outputs to the attacker’s own lock while reusing the witness

  • Surface: tx output rewriting
  • Mitigation: zk-lock on main: none. zk-lock-bound folds output(0) and its data into the pi[0] derivation, so any output rewrite invalidates the proof
  • Evidence: same as above

9. Rewrite the PI count to reshape verification

  • Surface: witness bytes
  • Mitigation: length invariant pi_bytes.len() == 4 + pi_count * 32 enforced before the commitment check; the commitment binds field-element bytes only, so a rewritten count fails on length before it can escape via the commitment
  • Evidence: zk-lock main.rs L72-81

10. Substitute a different, similarly shaped VK across a rebuild

  • Surface: build reproducibility
  • Mitigation: pinned --locked arkworks; reproducible-build script that lets a reviewer confirm the audited artifact is the one that runs
  • Evidence: threat model §5 (out of scope, but documented); scripts/verify-reproducible.sh in groth16-ckb; zk-lock CI pins the circuit vk_hash in circuit-vk-hash.yml

11. Break the trusted setup

  • Surface: prover side
  • Mitigation: out of scope. The verifier accepts whatever VK is published; toxic waste and prover correctness are the integrator’s problem
  • Evidence: threat model §5

12. Side-channel on verification time

  • Surface: observed tx execution
  • Mitigation: on-chain verification time is observable and deterministic; constant-time pairing is an arkworks concern
  • Evidence: threat model §5

Resource evidence, condensed

  • Verifier cycle cost. In groth16-ckb: ~121M cycles at N=64 public inputs, linear in N at ~270-300k cycles per additional PI (one G1 scalar mul). That is the verifier crate’s own reference binary, not the lock.

  • Lock cycle cost, measured on the actual artifact. Taking your point from the 2026-09-23 review that a directly linked measurement proves less than it looks, I measured the deployed scripts rather than quoting the crate.

    Build zk-lock (N=1) zk-lock-bound (N=2) Binary size
    Repo default (with -C debug-assertions) ~195M ~203M 167KB
    Without -C debug-assertions ~96M ~101M 94KB
    • My Makefile currently sets -C debug-assertions by default, so the assertion code is roughly half the cost.
    • On the ceiling. I have been quoting these against a 250M ceiling, and I should be careful there, because that figure is my own MAX_CYCLES test constant rather than a consensus parameter. Against it the four numbers are 78%, 81%, 38% and 40%, but the denominator is a budget I picked, not a protocol limit. The groth16-ckb threat model §4.2 quotes the same figure as a “block-vm bound”, which is wording I need to tighten there. If you have a per-transaction figure you consider authoritative for an accepted profile, I would rather use yours.
    • On the build. I am reporting both because the honest answer is that my build configuration, not my code, decides whether the artifact has comfortable headroom or almost none. Pinning that configuration is clearly part of what an exact profile has to fix.
    • On the harness. These are ckb-testtool 1.1 numbers from the success-path tests in the repo, so they come from the simulated VM rather than a node under a stated consensus profile. I am treating them as indicative and would want them re-measured properly before anyone leaned on them.
  • What the replay binding costs. 5,296,473 cycles without debug assertions, and 7,603,296 with them, taking the difference between the two locks on identical flags. That covers one extra public input, two cell loads and two blake2b hashes. For a mandatory binding I think that is cheap, and it is the number I would want in front of anyone arguing the binding belongs in the circuit instead.

  • Not measured. Any Spawn/IPC adapter. Everything above is a directly linked verifier, so for profile 2 these are floors, not estimates.

  • Memory. No unbounded allocations. Length pre-checks precede any Vec::deserialize_compressed, and checked_mul guards element-count arithmetic.

  • Proof size. Fixed 128 bytes (PROOF_LENGTH).

  • VK size. Variable: |IC| = nPublic + 1 compressed G1 points, plus 3 compressed G2 points and 1 compressed G1 point.

  • Fuzzing. Three libFuzzer targets (verify_arkworks, decode_vk_molecule, decode_witness_molecule), millions of executions, no false accept, no panic, no OOM.

  • Static prevention. deny(clippy::unwrap_used / expect_used / panic / unreachable) on the two crates that touch attacker-controlled bytes.

Against your framing

In Issue #22 you ask for an adversarial matrix that names the concrete failure modes, the mitigation and the evidence. My matrix is honest about one gap that lives at the lock layer, not the verifier layer: generic zk-lock has no cross-cell replay mitigation. That is what zk-lock-bound is for, and it is why I would not recommend deploying the generic script for any use case where two cells could plausibly carry the same (vk_hash, pi_commitment).

Everything above the replay row applies to both profile 1 and profile 2, because the verifier is the same code. What changes in profile 2 is the surface. The transition script is a separate identity from the verifier it spawns, so the rows about VK substitution and Molecule decoding grow an extra hop, the IPC boundary, that has to be modeled explicitly. Item b’s verifier_contract_id is the piece of your framing that closes that hop. The matrix does not model it yet because I have not built a spawned verifier.

The audit targets I would surface to a reviewer are the ones the threat model already flags:

  1. Length pre-checks in verifier-core::verify. About 30 lines; a single point of failure for the OOM class.
  2. Subgroup membership for G2, dependent on arkworks’ Validate::Yes default.
  3. Infinity-point rejection coverage across every active G1/G2 slot in the VK and proof.
  4. A long-running fuzz session before audit handover.
  5. A cross-implementation differential (snarkjs on the same inputs) for defense in depth on the soundness claim.

These are the items I would want a Phase 4 audit to close before calling the verifier under zk-lock production-ready.


Well, Arthur, this response has been longer than I anticipated, but I hope I have answered your questions with enough detail and evidence. I’m available for any further discussion. Please feel free to ping me; this time I’ll do my very best to get back to you promptly.

Cheers,
Cecilia Mulandi

4 Likes