Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

DCN Verifiable Inference

Status

Implementation architecture 0.1. This document defines the DCN-native path from a model artifact to a computation attestation. It complements COMPUTATION_ATTESTATION.md.

Goal

DCN SHALL support independently verifiable model inference without depending on any one proving vendor. The first implementation target is a small transformer and then Gemma-family inference. Attestable MAY later plug in as one backend, but the DCN proof contract MUST remain provider-neutral.

Design principle

DCN does not prove a framework invocation such as "PyTorch ran." It proves a precisely identified computation:

(model identity, numeric semantics, input, generation semantics)
                         ↓
                 verifiable inference
                         ↓
                       output

The statement being proved MUST bind all semantics capable of changing the result.

Verifiable Inference Representation

The proof compiler uses a Verifiable Inference Representation (VIR). VIR is a deterministic tensor graph plus an immutable model manifest.

VIRModel
├── ModelManifest
│   ├── family
│   ├── variant
│   ├── architecture_commitment
│   ├── weights_commitment
│   ├── tokenizer_commitment
│   ├── numeric_semantics
│   ├── quantization
│   ├── operator_semantics
│   ├── generation_semantics
│   └── compiler_commitment
└── TensorGraph
    ├── embedding
    ├── normalization
    ├── linear / matmul
    ├── rotary position encoding
    ├── attention
    ├── nonlinear / lookup operations
    ├── residual
    └── output projection

A backend MAY lower VIR to ONNX, a native proving IR, a zkVM guest, or another proof representation, but it MUST preserve the committed semantics.

Model identity

A model name alone is not sufficient identity. DCN defines model identity as a commitment over all execution-relevant semantics:

ModelIdentity = H(
    weights,
    architecture,
    tokenizer,
    numeric semantics,
    quantization,
    operator semantics,
    generation semantics,
    compiler/lowering version
)

A proof for an INT8 or fixed-point lowering MUST NOT be represented as proof of a BF16 reference model unless an independently verifiable equivalence relation is supplied.

Proof backends

A proof backend implements the following lifecycle:

prepare(model manifest + graph)
prove(prepared model + committed input)
verify(proof + public bindings)
normalize → ComputationAttestation

The backend boundary is deliberately narrower than the Cognitive ABI. Backends produce proof artifacts; DCN verifies their bindings and converts valid results into dcn.ca.inference.v1 attestations.

Baseline backend identifiers:

dcn.proof.fixture.v1
dcn.proof.jolt-atlas.v1
dcn.proof.ezkl.v1
dcn.proof.native.v1

dcn.proof.native.v1 is reserved for a future DCN-native tensor prover.

JOLT Atlas backend

The first external proving backend SHOULD be JOLT Atlas because its public implementation operates on ONNX tensor graphs and provides transformer, nanoGPT, MiniGPT/MicroGPT, and GPT-2 prove/verify examples.

The initial DCN integration has two stages:

  1. jolt-atlas-smoke: independently run a pinned JOLT Atlas transformer proof and verify it locally.
  2. jolt-atlas-model: lower a DCN VIR model to the supported ONNX subset and retain a native proof artifact whose verifier result is bound into a DCN ComputationAttestation.

The Git commit of JOLT Atlas used by an execution MUST be part of the backend/verifier identity.

Gemma roadmap

Gemma support SHALL be introduced incrementally.

G0 — operator coverage

Prove isolated operators needed by Gemma: RMSNorm, linear layers, rotary embeddings, attention, nonlinear activation, residual operations, and output projection.

G1 — transformer block

Prove and verify one complete Gemma-compatible transformer block using deterministic fixed inputs.

G2 — real checkpoint block

Use a real, immutable Gemma checkpoint and the model implementation's own decoder layer. Commit the exact checkpoint revision, weights, tokenizer, exported proving graph, reference inputs and numeric semantics. Measure fixed-point drift against the reference execution and require both semantic-admission and native proof-verification gates before emitting dcn.ca.inference.v1 evidence.

The first G2 target is google/gemma-3-270m, decoder layer 0, sequence length one. G2 proves the real decoder block, not the complete autoregressive model.

G3 — one-token model forward and deterministic token selection

Prove one complete next-token logits computation across embeddings, all 18 decoder layers, final norm and the complete LM head. The G3 baseline is one monolithic proof under the explicitly committed jolt-atlas-fixed-i32-scale-12 semantics.

The complete logits vector is proved. Because the pinned JOLT Atlas backend does not expose a general proved ArgMax operator, deterministic greedy selection is recomputed outside the proof and bound to the proved logits with greedy-argmax-over-proved-logits-v1; the attestation explicitly records selection_inside_zk_proof = false.

Qualification has two independent gates: native verification establishes correctness of the fixed-point graph, while a separately recorded drift evaluation admits that graph against the committed Transformers eager FP32 reference only when NRMSE is at most 0.08, cosine similarity is at least 0.99, and the greedy token agrees. This is not a claim that FP32 execution was proved or that the two executions are bit-equivalent. See adapters/verifiable-inference/gemma-g3/README.md and its machine-readable qualification report for the exact baseline and Atlas compatibility changes.

G4 — autoregressive generation

Link token steps recursively or through a backend-supported accumulator so a single final receipt commits the prompt, complete generated output, model identity, and every generation parameter.

G5 — privacy and scale

Add private prompt/output/model modes as supported by proof systems, streaming proving, parallel layer/token proofs, recursive aggregation, and GPU acceleration.

Specialized native backend

The long-term DCN backend SHOULD avoid general CPU instruction emulation for the dominant LLM tensor workload. It SHOULD exploit specialized proof techniques for:

  • matrix multiplication and linear layers;
  • lookup-based nonlinear functions;
  • attention and softmax;
  • streaming witness generation;
  • layer/token partitioning;
  • recursive proof aggregation.

The architecture is compatible with public techniques such as lookup-centric tensor proving and specialized attention arguments, but DCN does not inherit the security assumptions of any research system merely by adopting a similar optimization.

Proof receipt

Every successful backend execution MUST be normalized to a receipt binding at least:

execution_id
backend_id
backend_version / source commitment
model_commitment
architecture_commitment
tokenizer_commitment
numeric_semantics
input_commitment
output_commitment
generation/sampling commitment
proof_system
proof commitment/reference
verifier commitment/reference
verification status
limitations

Only a locally verified valid result can satisfy mandatory computation assurance.

Actum

Actum SHOULD finalize commitments to the normalized attestation, proof artifact, verifier identity, execution identity, and settlement-relevant predicates. Large proof payloads and private inputs/outputs MAY remain content-addressed off-chain.

Actum finality does not replace native proof verification.

Self-verifying cognitive capital

The Compiler Society MAY target proof-producing artifacts. A compiled K-line implementation can therefore carry both an execution artifact and a proving representation:

KLineTemplate
      ↓
compiled cognitive artifact
      ├── executable representation
      └── verifiable representation
                 ↓
        execution + proof
                 ↓
      ComputationAttestation

This is the DCN definition of self-verifying cognitive capital.