Cryptographic Foundations

dregg's proof system is built on the Effect VM and the constraint DSL. The Effect VM proves arbitrary turns in a single STARK (24 effects per turn, Custom dispatch for application-defined logic). The constraint DSL compiles CircuitDescriptor definitions to multiple proof systems from a single source. The base STARK path uses BabyBear-field FRI with Poseidon2 as the in-circuit hash — hash-based, no elliptic-curve assumptions at this layer. Recursion and EVM-verification paths use Kimchi (Mina/Pasta) and SP1/Groth16 respectively, both of which depend on elliptic curves; the end-to-end stack is therefore not post-quantum until those composition layers are themselves migrated to a hash-based recursion scheme.

BabyBear Field

The BabyBear prime field (p = 2^31 − 2^27 + 1 = 2,013,265,921) is the working field for the entire STARK stack. It fits in a 32-bit machine word, so addition and subtraction lower to native CPU instructions with cheap reductions. A single BabyBear element carries about 31 bits of entropy — not enough on its own to bind a cryptographic commitment, which is why state commitments are being widened to a 4-BabyBear digest (~124-bit binding, Stage 1 in flight per EFFECT-VM-SHAPE-A.md).

Poseidon2

Poseidon2 is the algebraic hash function used inside circuits. It operates natively over BabyBear field elements, making Merkle tree operations and fact commitments cheap inside the AIR (Algebraic Intermediate Representation).

• hash_fact(predicate, terms) -- Commit a Datalog fact to a single field element
• hash_2_to_1(left, right) -- Binary Merkle node hash
• hash_many(inputs) -- Variable-width sponge hash

Eight Poseidon2-hashed leaves climb to a single root. The amber path is the authentication proof for the third leaf — log2(8) = 3 sibling hashes plus the leaf itself.

STARK Proof System

The STARK prover/verifier is based on FRI (Fast Reed-Solomon Interactive Oracle Proofs of Proximity). Key properties:

• Proof size: ~24 KiB (constant regardless of computation size)
• Verification time: ~2ms
• Generation time: 200ms-500ms depending on mode
• Security: Hash-based at this layer (FRI + Poseidon2), 128-bit security level. End-to-end stack is not post-quantum — see recursion notes above.
• Transparency: No trusted setup required

Effect VM (Primary Proof Mechanism)

The Effect VM is the sovereign proof mechanism. It proves an entire turn in a single STARK regardless of how many effects the turn contains. The runtime defines 41 effect variants; the AIR currently constrains 24, with the rest tracked under the Shape A coverage plan (see callout below). Effects break down by group:

• State / authority: SetField, CreateCell, IncrementNonce, SetPermissions, SetVerificationKey, GrantCapability, RevokeCapability, RevokeDelegation, SpawnWithDelegation
• Value: Transfer (conservation-checked), NoteCreate, NoteSpend (with nullifier)
• Sealing: CreateSealPair, Seal, Unseal
• Messaging / CapTP: Introduce (three-party), PipelinedSend, CreateObligation, FulfillObligation, SlashObligation, ExportSturdyRef, EnlivenRef, DropRef, ValidateHandoff
• Bridge: BridgeLock, BridgeMint, BridgeFinalize, BridgeCancel
• Escrow (×6): deposit, claim, refund, dispute, resolve, expire
• Queues / events: EmitEvent, EnqueueMessage, DequeueMessage, ResizeQueue, AtomicQueueTx, PipelineStep
• Sovereignty: MakeSovereign, CreateCellFromFactory, ExerciseViaCapability
• Custom: dispatch to CellProgram-defined logic (up to MAX_CUSTOM_EFFECTS per turn)

The VM enforces state continuity (each effect’s post-state = next pre-state), conservation (final accumulator = 0), authority (EffectMask subset of the actor’s c-list), and atomicity (all-or-nothing via completion flag). IVC compression chains turn proofs into constant-size attestations.

DSL Circuit Architecture

All proof logic is defined through the constraint DSL (circuit/src/dsl/). The former standalone _air.rs files have been deleted -- the DSL is the single source of truth. Each CircuitDescriptor compiles to trace generators and constraint evaluators for all supported backends.

Key circuit descriptors:

• Poseidon2 -- Hash permutation verification
• MerkleMembership -- 4-ary Merkle path proof
• FoldChain -- Monotonic capability attenuation
• MultiStepDerivation -- N-step Datalog derivation
• IvcAccumulation -- Fold chain compression (constant-size)
• NoteSpending -- Private note spending + nullifier
• NonRevocation -- Credential non-revocation proof
• RecursiveVerifier -- STARK-in-STARK recursive verification
• Presentation -- Full private credential presentation
• EffectVm -- Multi-effect turn proving
• SovereignTransition -- Sovereign cell state transition
• Predicate / Temporal / Arithmetic / Relational / Compound -- Various predicate proofs
• Schnorr / NativeSignature -- In-circuit signature verification

Composition operators combine multiple circuit proofs: compose_and, compose_or, compose_chain, compose_aggregate. Sub-proofs are cryptographically bound via VK hashes and public-input linking.

Three Production Provers

Additional Backends (via DSL)

• SP1 -- Succinct's RISC-V zkVM. Groth16 wrapping for EVM verification (~200k gas)
• Midnight/ZKIR v3 -- Compilation for Cardano/Midnight proof server
• Datalog -- Rule fragment for lightweight policy evaluation
• Rust -- Runtime evaluator function (trusted-mode fast path)
• AIR -- Constraint descriptor for custom STARK integration

IVC (Incrementally Verifiable Computation)

The IVC system compresses receipt chains to a constant-size proof. Each new turn extends the IVC accumulator. The final proof covers the entire state transition history regardless of chain length. Verification is O(1): check the IVC proof, check the final state commitment, check nullifier freshness.

STARK-in-Pickles Composition

The STARK-in-Pickles pipeline wraps a BabyBear STARK proof in a Kimchi verifier circuit (~30K gates) to produce a Pickles recursive SNARK (constant-size, Pasta curves):

1. Generate STARK proof over BabyBear (fast, PQ-secure, ~24 KiB)
2. Commit the STARK proof via Poseidon2 (pre-hash and post-hash binding)
3. Verify the STARK algebraically inside a Kimchi circuit (FRI folding + Fiat-Shamir replay)
4. Produce a Pickles recursive proof (constant-size, Mina-compatible)

Status: BabyBear hash-chain IVC is operational. Pickles assisted recursion (unbounded depth) is operational for individual STARK circuits. The STARK-in-Pickles wrapping path exists and produces constant-size recursive SNARKs for the implemented circuits. Full heterogeneous AIR composition — derivation, fold, membership, and the Effect VM together in one recursive proof — is structurally supported but not yet end-to-end operational for arbitrary combinations; this is gated on Effect VM Shape A landing.

Signature Schemes

• Ed25519 -- Agent identity, turn signing, federation consensus messages
• BLS12-381 -- Threshold signatures for attested roots
• X25519-ChaCha20Poly1305 -- Sealed capabilities (encrypt under token)
• HMAC-SHA256 -- Macaroon token chain binding
• BLAKE3 -- Domain-separated key derivation, fast Merkle trees

Bridge Layer

EVM Bridge (SP1 Groth16)

The dregg-chain crate wraps dregg STARK proofs in SP1's zkVM to produce Groth16 proofs verifiable on Base Sepolia at ~200k gas:

1. dregg STARK proof (large, not EVM-friendly) is the input
2. SP1 guest program verifies the STARK inside a RISC-V zkVM execution
3. SP1 produces a compact Groth16 proof
4. Groth16 proof is verified by SP1 Verifier Gateway contract on Base

Includes Foundry deployment scripts, incremental Merkle tree for deposits (O(log n) insertions), VK registry with governance, and commit-reveal frontrunning protection. Status: Architecture complete; Foundry scripts for Base Sepolia deployed. Guest program regeneration against Plonky3 backend in progress.

Midnight Bridge

Two-level bridge to Cardano/Midnight:

• Level 1 (implemented): Attestation bridge. dregg state roots are attested on Midnight as observation-based data. Midnight validators can verify that a dregg state existed at a given height.
• Level 2 (designed): Proof-carrying bridge. The DSL's ZKIR v3 backend compiles dregg circuits into Midnight-compatible programs, enabling a Midnight validator to verify dregg proofs natively via the FRI verifier in ZKIR.

Mina Bridge

Native Pickles recursion via the STARK-in-Pickles pipeline. A dregg STARK proof is verified inside a Kimchi circuit, producing a Pickles recursive proof compatible with Mina's verification infrastructure. Enables Mina zkApps to natively verify dregg state transitions.

Concrete parameter rationale (FRI folding factor, blowup, query count vs. claimed security bits) lives in the design notes alongside the prover crate — see docs/recursive-proof-architecture.md for the reasoning behind the choices listed above and how they trade off proof size against verifier cost.