[Language/Verifier][Research] Add typed zero-knowledge verifier contracts without a circuit DSL

[a19q3]

Summary

Design and implement a first-class, typed contract for verifying externally
generated zero-knowledge proofs in CellScript CKB artifacts.

The proposed boundary is deliberately narrower than "add ZK to the language":

• proving and circuit execution remain off chain;
• scheme-specific cryptography remains in a separately built, reviewed, and
  hash-bound CKB RISC-V verifier;
• CellScript owns the security-critical composition layer: verifier identity,
  verification-key identity, canonical proof/public-input codecs, public-input
  binding to the CKB state transition, bounded Spawn/IPC execution, ProofPlan
  coverage, builder contracts, and evidence.

CellScript should not become a circuit DSL, a finite-field language, or an
on-chain prover. The product goal is to make a ZK-backed state transition as
auditable and fail-closed as an ordinary typed CellScript transition.

This issue is an RFC/design candidate, not a release commitment. The active
nightly-0.26 bounded consensus-runtime work should remain scoped to its
current Cell-group and output-correspondence closure while Phase 0 of this issue
can proceed independently.

Why this belongs at the language and artifact boundary

CKB is a crypto-agnostic RISC-V verification platform. Its design explicitly
supports deploying new cryptographic primitives, including zkSNARKs and
zkSTARKs, as ordinary VM code rather than protocol precompiles. CKB-VM v2 also
identifies zero-knowledge verification as a performance motivation and adds
isolated child execution through Spawn.

CellScript already has most of the generic substrate:

• typed transaction and Script Group views;
• fixed-width values and bounded witness/runtime contracts;
• spawn, pipe, wait, and file-descriptor flow checking;
• ckb::require_cell_data_hash for runtime CellDep preflight;
• a frozen BIP340 verifier CellDep ABI as one concrete external-verifier path;
• ProofPlan evidence tiers and strict production gates;
• verified lowering records, source maps, and a standalone artifact checker;
• Registry runtime_verifier artifacts with TCB consumption mode;
• builder, CKB-VM, stateful, deployment, and chain evidence kept distinct.

What is missing is a generic semantic contract connecting those pieces. An
author can manually spawn a verifier today, but the compiler cannot answer:

1. Which exact verifier binary and ABI were intended?
2. Which verification key and circuit/statement identity were used?
3. What is the canonical proof and public-input encoding?
4. Which public input binds the proof to the consumed Cells, proposed output
   Cells, current action, current Script, and replay domain?
5. Was the verifier result actually checked on every accepting path?
6. Are proof size, public-input size, process count, memory, and cycles bounded?
7. Can the independent checker connect the source-level claim to the final
   CellDep preflight, IPC envelope, Spawn/Wait path, and rejecting branch?

Those are language, artifact, and builder questions rather than elliptic-curve
implementation questions.

Current gap

The BIP340 path proves that a fixed external-verifier ABI can be made
executable and fail-closed, but it is intentionally scheme-specific:

• the source namespace is verifier::btc::bip340;
• the type checker fixes one message/key/signature shape;
• codegen constructs one 144-byte NovaSeal envelope;
• a literal CellDep index is required for the explicit form;
• message construction, domain separation, replay policy, and authority
  binding remain application responsibilities.

Generic Spawn/IPC is lower level still. It exposes process and descriptor
mechanics, but not a typed cryptographic statement. Treating raw spawn() as
"ZK support" would leave the most dangerous bindings invisible to interfaces,
ProofPlan, strict production checks, generated builders, and artifact review.

There is also a terminology hazard: CellScript ProofPlan is an audit and
enforcement plan for compiler obligations. It is not a cryptographic proof.
The proposed metadata and documentation must keep ProofPlan and ZkProof
unambiguously separate.

Design principles

1. Exact profile first. Ship one exact verifier/profile contract before any
   open scheme registry or compatibility-based dispatch.
2. No ambient verifier authority. A source name or Registry coordinate is
   not authority. On-chain execution must bind the resolved CellDep bytes.
3. Typed statement, opaque proof. CellScript understands the statement
   schema and source bindings, but does not interpret proof internals.
4. Canonical encoding only. No free-form bytes, implicit field reduction,
   alternative endianness, ignored trailing data, or permissive decoding.
5. No inferred security context. The compiler never infers replay,
   authorization, or state-transition bindings from action/field names.
6. Bound every runtime dimension. Proof length, public-input length,
   statement field count, verifier processes, IPC bytes, memory profile, and
   measured cycles need explicit limits.
7. Fail closed before codegen when incomplete. A production build with a
   missing verifier, key, codec, statement binding, or executable ProofPlan
   record must stop before ASM/ELF generation.
8. Separate evidence levels. Structural checker acceptance, CKB-VM
   execution, builder dry-run, deployment identity, and live-chain acceptance
   must never collapse into one verified flag.
9. No privacy overclaim. Verifying a succinct proof does not by itself
   establish that the circuit, prover, setup, or application provides a
   specific zero-knowledge/privacy property.

Target architecture

flowchart LR
    OLD["Input Cells / old state"] --> STMT["Typed public-input constructor"]
    NEW["Output Cells / new state"] --> STMT
    CTX["action + Script + replay context"] --> STMT

    WIT["Bounded proof witness"] --> PARENT["CellScript parent artifact"]
    STMT --> PARENT
    HANDLE["Exact verifier handle\nABI + ELF hash + VK hash"] --> PARENT

    PARENT --> PREFLIGHT["Resolve named CellDep\nand check exact identity"]
    PREFLIGHT --> IPC["Canonical bounded Molecule IPC request"]
    IPC --> CHILD["Isolated CKB-VM verifier child"]
    CHILD --> RESULT{"exit 0?"}
    RESULT -- "no / syscall failure" --> REJECT["Stable fail-closed runtime error"]
    RESULT -- "yes" --> TOKEN["Checked-runtime verifier evidence"]

    TOKEN --> TRANSITION["Permit the declared transition path"]

    META["Typed semantics + ProofPlan + lowering + source map"] --> CHECKER["Standalone structural checker"]
    PARENT --> META

Loading

The child verifier owns scheme-specific cryptography. The parent owns exact
identity, statement construction, CKB source selection, bounded transport, and
result enforcement.

Proposed source model

The final spelling requires an accepted RFC. This strawman illustrates the
semantic information; it does not preselect parser syntax:

verifiers {
    verifier state_transition: ZkVerifier<StateTransitionPublicInputs> {
        profile: "candidate-zk-profile-v1"
        abi: "cellscript-zk-ipc-v1"
        dependency: state_transition_verifier
        verification_key: 0x...
        max_proof_bytes: 512
        max_public_input_bytes: 256
    }
}

struct StateTransitionPublicInputs {
    domain: Hash
    script_hash: Hash
    action: Hash
    old_state: Hash
    new_state: Hash
    nonce: Hash
}

action update(
    before: State,
    witness proof: ZkProof<StateTransitionPublicInputs>,
    witness nonce: Hash,
) -> after: State {
    transition before -> after

    verification
        let public_inputs = StateTransitionPublicInputs {
            domain: ZK_STATE_TRANSITION_DOMAIN,
            script_hash: ckb::current_script_hash(),
            action: UPDATE_ACTION_ID,
            old_state: hash_blake2b_packed(before),
            new_state: hash_blake2b_packed(after),
            nonce,
        }

        zk::require_valid(state_transition, proof, public_inputs)
}

An accepted design may place the verifier declaration in Cell.toml and emit a
typed source handle instead of adding a top-level block. The non-negotiable
contract is the information and evidence, not the syntax.

Required nominal types

The first version should model at least:

• ZkProof<Statement, Profile>: opaque, bounded transaction evidence;
• ZkPublicInputs<Statement, Profile> or a registered ordinary struct whose
  canonical public-input codec is part of its identity;
• VerificationKeyCommitment<Profile>: exact fixed-width commitment, never an
  untrusted witness-selected authority;
• VerifierHandle<Interface>: exact verifier artifact/deployment/ABI binding,
  aligned with [Language/ABI] Bind runtime Script values to verified package interfaces #11 rather than a second handle system;
• optionally VerifiedStatement<Statement, Profile>: an ephemeral,
  non-serializable, non-escaping value produced only by the generated
  fail-closed verifier path.

ZkProof is not a Cell-backed resource and grants no lifecycle capability.
Copy/borrow behavior should be conservative and driven by its bounded byte
representation. VerifiedStatement must not be constructible, serializable,
stored in a Cell, accepted from a witness, or preserved across an entry.

The RFC must decide whether require_valid returns Unit and directly
discharges a named ProofPlan obligation, or returns VerifiedStatement for
explicit flow-sensitive discharge. A boolean-returning API is not sufficient
because ignoring the result must be impossible.

Verifier identity contract

The first production-capable path must bind one exact verifier contract:

verifier_contract_id = H(
    verifier-profile ID and version
    || IPC ABI ID and version
    || exact RISC-V executable/data hash
    || target and CKB-VM profile
    || verification-key commitment
    || statement/public-input schema hash
    || proof and public-input codec IDs
    || declared runtime limits
)

The exact canonical hashing profile must be specified and versioned rather than
copied from this illustrative formula.

Source code refers to a stable policy name. Package metadata declares the
required identity. Deployment records resolve that policy to a network-specific
outpoint. The builder places the dependency at a resolved index, and the parent
Script verifies the selected code/data identity before Spawn.

Required rules:

• a Registry package name is discovery metadata, not consensus authority;
• a raw CellDep index is not a verifier identity;
• data_hash, type_hash, Type ID, and outpoint policies remain distinct;
• DepGroup resolution must bind the actual spawned member, not merely the
  container name;
• a verification key supplied solely by witness cannot define the accepted
  verifier contract;
• an upgradeable verifier requires the explicit receipt/upgrade model from
  [Language/ABI] Bind runtime Script values to verified package interfaces #11; exact hash-bound deployment ships first;
• unknown profiles, ABI versions, codec versions, or reserved flags reject.

This work should update or supersede the existing draft named-CellDep RFC rather
than introducing a ZK-only positional binding.

Public-input and replay binding

The central security property is not merely "the proof verifies." It is:

The exact reviewed verifier accepted a canonical proof for the exact typed
statement that authorizes this exact CKB state transition and context.

The compiler cannot guess a universally correct statement. It can require that
the selected verifier profile explicitly declares and fills its binding classes:

Binding class	Examples	Required behavior
application domain	protocol/version/domain tag	fixed or manifest-bound, never witness-selected by default
verifier/circuit identity	profile, VK/circuit commitment	part of the verifier contract
current verifier context	current Script hash, Lock/Type role, action ID	typed source with explicit codec
consumed state	input Cell data hash, typed state commitment, outpoint/nonce	exact declared source and index/scope
proposed state	output Cell data hash, typed successor commitment	exact output role and correspondence
replay context	nonce, nullifier, epoch, transaction component, protocol sequence	application-defined but explicit
authority	key/credential/member commitment where applicable	independently tied to state/Script policy

Not every profile needs every field, but every omitted class must be explicit in
metadata and justified by the use case. The production gate should reject a
profile whose mandatory binding classes are unresolved.

Public inputs require:

• a versioned schema hash;
• deterministic field order and exact widths;
• explicit integer endianness and range checks;
• strict canonical field-element encoding with no implicit modular reduction;
• exact handling of optional/list fields with compile-time or runtime bounds;
• no ignored trailing bytes or duplicate aliases;
• source-span and expression-origin retention for every field;
• one evaluation of state-producing expressions before serialization;
• shared vectors across compiler, builder, child verifier, simulator, CKB-VM,
  and independent checker fixtures.

The transport envelope may use Molecule while scheme-specific scalar encodings
remain registered sub-codecs. The documentation must not call an ad hoc packed
field encoding "Molecule."

Canonical Spawn/IPC verifier ABI

Phase 0 must specify a bounded cellscript-zk-ipc-v1 request. At minimum, the
strict Molecule envelope should bind:

• magic and ABI version;
• verifier-profile ID/hash;
• statement schema hash;
• verification-key commitment;
• flags, all reserved bits required to be zero;
• proof codec ID and exact proof byte length;
• public-input codec ID and exact public-input byte length/count;
• optional explicit application-domain/replay-context identity;
• exact payload bytes.

The ABI must define maximum byte and element counts before decoding. Unknown
fields/versions, noncanonical Molecule offsets, truncated reads, extra bytes,
overflowing counts, partial pipe operations, wrong descriptor direction,
double close, unclosed descriptors, Spawn failure, child rejection, Wait
failure, or scheduler deadlock all reject with stable parent runtime errors.

The parent must:

1. validate and materialize all bounded sources;
2. verify the exact named CellDep identity;
3. create the pipe and child with explicit descriptor ownership;
4. write the complete canonical envelope;
5. close the writer;
6. wait for the exact child PID;
7. accept only child exit code 0;
8. reject every failure path before allowing the protected transition path to
   return success.

The first version should spawn at most one child per verifier call and impose a
small compile-time bound on verifier calls per entry. Batch or recursive proof
verification is a later profile, not an implicit loop over witness data.

ProofPlan, typed semantics, and independent checking

Add a dedicated category such as cryptographic-verifier-call, not a generic
require record. Each record should contain:

• entry/origin/source span;
• exact verifier-contract identity;
• profile, ABI, proof codec, public-input codec, and VK commitment;
• proof source, witness placement, and byte bound;
• statement schema and every public-input source binding;
• application domain and replay-policy declarations;
• named CellDep policy and resolved-index requirement;
• Spawn/IPC process, descriptor, byte, and memory limits;
• stable runtime-error mapping;
• generated lowering helper/block identities;
• codegen coverage and final ELF ranges;
• evidence tier and unresolved assumptions;
• measured/allowed cycle evidence and fixture identities.

checked-runtime is allowed only when the selected entry's lowering contains
the exact verifier preflight, canonical request construction, Spawn/Wait path,
and rejection branch. A declaration without that executable path remains
runtime-helper-required or metadata-only and must fail production gates.

The standalone artifact checker should validate bounded structural properties:

• metadata, typed semantics, lowering, source map, and ELF identities agree;
• the verifier-call block is reachable from the entry;
• required preflight, IPC, Spawn, Wait, and rejection edges are present;
• declared request sizes and stack ranges are respected;
• the checked child result dominates every accepting continuation that claims
  the verifier evidence;
• mutation of verifier identity, VK hash, statement hash, source binding,
  request length, call edge, branch, or runtime error is rejected.

The checker must not claim cryptographic implementation correctness, circuit
correctness, zero knowledge, trusted-setup integrity, or complete
source-to-machine semantic equivalence.

Builder and prover boundary

The compiler should emit a versioned prover/builder contract containing:

• statement schema and canonical public-input vectors;
• proof codec and maximum size;
• verifier/VK/circuit identities;
• exact witness placement;
• named CellDep/deployment requirements;
• transaction roles used to derive each public input;
• required dry-run and resource evidence.

An off-chain adapter may invoke an external prover SDK, but the core compiler
must not contain proving keys or execute untrusted prover plugins during normal
compilation. Prover integrations require explicit process/tool boundaries,
input/output size limits, pinned versions, and reproducible statement vectors.

Generated builders should recompute the public inputs from the candidate
transaction, compare them with prover output, place the proof, resolve the exact
verifier CellDep, then dry-run the final serialized transaction. Builder success
is still not consensus evidence; the on-chain parent and child checks remain
authoritative.

For multi-Script protocols, #9 ProtocolBundle should carry the verifier role,
statement inputs, witness ownership, CellDep resolution, and per-Script cycle
evidence without merging trust boundaries.

Registry may later add hash-bound circuit, proving-key, verification-key, or
setup-transcript artifact roles. Registry presence or an audited label must
not be treated as on-chain identity or proof of cryptographic soundness.

Resource and performance contract

CKB charges cycles for ordinary RISC-V cryptography, and Spawn has explicit
process/VM limits. Scheme selection therefore requires measurement, not a
language-design assumption.

Every admitted profile should declare and test:

• maximum proof bytes;
• maximum public-input count and bytes;
• maximum verification-key bytes loaded by the child;
• maximum IPC bytes and calls;
• parent stack/scratch use;
• child memory configuration;
• maximum verifier calls and live processes per entry;
• valid worst-case, invalid worst-case, and malformed-input cycles;
• total transaction size and occupied-capacity effects;
• the exact CKB/CKB-VM version used for evidence.

Phase 0 should benchmark real RISC-V implementations of candidate systems such
as Groth16, PLONK-family, STARK-family, or zkVM receipts without preselecting a
winner. Admission criteria include strict decoding, no_std/RISC-V portability,
determinism, reproducible builds, acceptable license, test vectors, auditability,
and bounded CKB-VM resources. Only one profile should advance first.

Threat model and adversarial matrix

Case	Expected result
valid proof, exact verifier/VK, exact state transition	pass
invalid proof	stable child rejection
valid proof for different public inputs	reject
public inputs reordered or re-encoded	reject
noncanonical field element or implicit modular reduction	reject
proof truncated, oversized, or contains trailing bytes	reject
public-input count/bytes exceed declared bound	reject before/inside child with stable error
same proof replayed for another action or Script	reject when the profile claims those bindings
old state bound correctly but proposed output omitted or changed	reject
correct state roots but wrong nonce/nullifier/replay domain	reject
verifier CellDep index points to different bytes	parent preflight rejects
correct Registry package name but wrong on-chain CellDep	reject
matching DepGroup container but wrong resolved verifier member	reject
valid verifier binary with wrong VK/circuit	reject
compatible name/version but unapproved verifier upgrade	reject
verification key selected solely from witness	production rejection unless independently committed by the exact profile
child exits nonzero or Wait uses wrong PID	reject
partial write/read, descriptor misuse, or deadlock	stable fail-closed error
verifier result computed but ignored on one branch	compiler/checker rejection
metadata claims checked-runtime but ELF call/branch is removed	standalone checker rejection
valid fast proof but malformed input takes excessive cycles	profile rejected until bounded/measured
proof is sound but circuit omits an application rule	outside compiler proof; profile/security review must state the gap

Implementation phases

Phase 0 — use case, threat model, benchmarks, and RFC

• select one concrete primary use case, such as a rollup/state-root transition,
  privacy-preserving credential spend, or cross-chain validity proof;
• specify the exact statement and replay bindings for that use case;
• benchmark candidate verifier implementations in the pinned CKB-VM;
• choose one exact initial profile;
• specify verifier/VK/circuit identity, codecs, IPC, bounds, errors, upgrades,
  and evidence;
• decide source syntax versus manifest declaration;
• update/supersede the named CellDep draft and align with [Language/ABI] Bind runtime Script values to verified package interfaces #11;
• add the capability to the ledger proposed by [Docs/strategy] Separate executable-surface closure from product capability completeness #14 as research, not
  implemented.

No positive production lowering should land in this phase.

Phase 1 — generic exact-verifier infrastructure

• implement exact VerifierHandle/named dependency resolution;
• add opaque bounded proof and typed statement representations;
• add the canonical bounded IPC envelope and generated fail-closed call path;
• add typed-semantics, ProofPlan, lowering-record, source-map, and checker
  schemas;
• add stable errors and FD/process/resource validation;
• use a deliberately simple deterministic test verifier to exercise the
  infrastructure without making a ZK security claim;
• complete parser/formatter/type/IR/codegen/LSP/VS Code/Playground-summary/docs
  closure for the admitted surface.

Phase 2 — first real ZK verifier profile

• pin one reproducible, reviewed RISC-V verifier implementation;
• pin the exact verification key, circuit/statement identity, ABI, codecs, and
  runtime limits;
• add canonical upstream and CellScript-owned positive/negative vectors;
• add real CKB-VM and stateful transaction fixtures;
• measure cycles, memory, transaction bytes, witness bytes, and capacity;
• add generated builder plus one bounded external prover adapter;
• independently review the verifier TCB and the parent statement-binding path;
• keep deployment and chain evidence separate from local CKB-VM results.

Only after this phase may documentation describe the selected profile as an
executable ZK verification path.

Phase 3 — composition and ecosystem closure

• integrate with ProtocolBundle and multi-Script transaction roles;
• add Registry artifact roles only where identity/evidence contracts justify
  them;
• add CI/release gates for reproducible verifier builds and pinning;
• publish SDK vectors and audit templates;
• evaluate batched or additional verifier profiles only from measured demand.

Completion criteria

• An accepted RFC defines the first use case, exact scheme/profile, verifier
  identity, VK/circuit identity, statement, replay policy, codecs, ABI,
  resource limits, errors, and upgrade policy.
• The source/manifest model uses a named exact verifier dependency, not a
  bare positional authority.
• Proofs are opaque and bounded; public inputs are typed and canonically
  encoded.
• Every public input retains its source expression/span through typed
  semantics, ProofPlan, lowering, and checker records.
• Invalid, ignored, or partially checked verifier results cannot reach a
  successful entry return.
• Production compilation rejects missing verifier identity, VK identity,
  statement binding, executable coverage, or resource bounds before
  codegen.
• The verifier and parent artifacts build reproducibly with pinned hashes.
• Standalone-checker mutations cover identity, statement, ABI, request,
  control-flow, stack, and result-binding changes.
• Positive and adversarial CKB-VM fixtures execute the exact RISC-V child
  verifier.
• A stateful CKB transaction fixture binds old state, new state, action,
  Script, and replay context as specified by the selected use case.
• Builder/prover vectors produce byte-identical public inputs and proof
  envelopes across supported SDKs.
• Cycle, memory, proof/witness bytes, transaction bytes, and occupied
  capacity evidence are recorded with exact environment identity.
• Parser, formatter, type checker, IR, metadata, LSP, VS Code, generated
  builders, Registry profile, docs, website summary, and gates agree.
• An independent security review covers verifier substitution, VK/circuit
  substitution, codec ambiguity, public-input omission/reordering, replay,
  CKB source selection, IPC failure, and resource exhaustion.
• Documentation distinguishes cryptographic proof, ProofPlan evidence,
  structural checker evidence, CKB-VM execution, and chain evidence.

Non-goals

• a CellScript circuit DSL;
• on-chain proof generation;
• general finite-field, elliptic-curve, pairing, FFT, or polynomial syntax;
• compiling arbitrary Circom/Halo2/zkVM programs inside the CellScript compiler;
• a universal verifier plugin mechanism in the first version;
• implicit download or execution of Registry artifacts during consensus;
• deriving public inputs or replay policy from action/field names;
• proving circuit correctness, zero knowledge, trusted-setup integrity, or
  application privacy from successful verification alone;
• recursive, aggregated, or unbounded proof lists in the first profile;
• treating a Type ID or interface compatibility result as automatic approval of
  future verifier upgrades;
• weakening the active nightly-0.26 bounded-runtime gates or scope.

Dependencies and relationship to existing work

• [Language/ABI] Bind runtime Script values to verified package interfaces #11 should provide the exact VerifierHandle/artifact-interface binding; this
  issue adds the ZK statement, VK, codec, and execution contract.
• [Architecture][Builder] Add an artifact-only multi-Script ProtocolBundle #9 should carry verifier roles and builder/evidence composition for
  multi-Script transactions.
• [Language design] Model typed cross-Script transaction roles without runtime linkage #10 may use verified statements in typed foreign-role protocols, but ZK
  success must not be mistaken for peer behavioral equivalence.
• [Language design] Add explicit typed openings for digest-committed substate #13 supplies typed commitment/opening principles useful for state-root and
  committed-substate public inputs.
• [Candidate][Consensus runtime] Implement executable bounded Cell-group consumption #7 and [Candidate][Consensus runtime] Implement executable bounded output-plan correspondence #8 define bounded Cell-group and output-plan correspondence that ZK
  statements may reference; a proof must not bypass their lifecycle authority.
• [Docs/strategy] Separate executable-surface closure from product capability completeness #14 should track this as a product capability outside the currently admitted
  executable surface until implementation closure is real.

Open RFC decisions

1. Source declaration block, manifest-only declaration, or a combination?
2. Does require_valid return Unit or an ephemeral VerifiedStatement?
3. Which exact first use case and verifier profile justify implementation?
4. Where is the verification key stored: embedded in the child, separate exact
   CellDep, or another committed profile artifact?
5. Which bindings are mandatory for the first statement, and how are omissions
   represented and gated?
6. What is the exact Molecule transport envelope and scheme-specific scalar
   codec?
7. How are proof bytes placed in WitnessArgs without conflicting with entry
   witness and other Script roles?
8. What compile-time and runtime call-count bounds are acceptable under CKB
   Spawn limits?
9. What cycle/memory threshold makes a candidate profile admissible?
10. How are trusted setup, circuit source, proving key, VK, verifier source, and
    audit evidence packaged without making Registry a consensus dependency?
11. What exact verifier upgrade model is allowed after the hash-bound first
    version?

References

• CellScript BIP340 verifier CellDep ABI
• CellScript named CellDep binding draft
• CellScript ProofPlan tutorial
• CellScript verified artifact boundary
• CKB RFC 0002: Cell Model and crypto-agnostic VM
• CKB RFC 0049: CKB-VM version 2
• CKB RFC 0050: Spawn/IPC syscalls

[a19q3]

Related implementation evidence: groth16-ckb and zk-Lock

before opening this issue, I also reviewed Cecilia Mulandi’s related CKB work in more detail:

• groth16-ckb, including its threat model and Molecule schema;
• the zk-Lock M1 implementation and its Spark proposal;
• her broader research notes on ZK applications in the CKB Cell Model.

This work provides concrete implementation evidence for one important integration profile:

1. Creation-committed, spend-time proof-gated Lock

   The locked Cell commits to vk_hash and a public-input commitment in its Lock args. At spend time, the Lock resolves the VK from CellDeps, reads the proof and public inputs from the witness, checks the commitment, and invokes the Groth16 verifier.

Issue #22 is also exploring a related but distinct profile:

2. Dynamic CellScript transition verifier

   CellScript derives canonical public inputs from the actual consumed Cells, proposed outputs, action, current Script identity, and application-defined replay context, then requires successful verification before the transition may complete.

The second profile is a CellScript design direction prompted by comparing the two models; it is not a claim that zk-Lock itself implements dynamic transition binding. Keeping them separate avoids forcing a creation-bound Lock abstraction onto state-transition protocols, while still allowing both profiles to share verifier/VK identity rules, codecs, witness contracts, resource evidence, and builder tooling.

This comparison sharpens several Phase 0 requirements:

• treat proof/VK codecs and WitnessArgs placement as part of a versioned profile;
• distinguish verifier-code identity from VK identity and CellDep resolution;
• record when each statement component becomes binding: Cell creation, transaction construction, or Script execution;
• separate CKB-native checks from facts that genuinely need proof-system enforcement;
• benchmark the exact verifier artifact and execution architecture rather than assuming equivalent costs across direct linking and Spawn/IPC.

groth16-ckb’s Groth16/BN254 implementation is therefore a strong candidate for the first interoperability experiment and resource baseline. This does not yet select it as a production CellScript profile: the current work is explicitly experimental/audit-gated, and a Spawn-based CellScript profile may require an adapter rather than treating the existing verifier integration as a drop-in child ABI.

Credit: Cecilia Mulandi for the verifier, threat-model, schema, and zk-Lock implementation work that made these distinctions concrete.