Simulator integration

How crucible-prover connects to crucible-simulator — the boundary, the seams, and the adapter crate that translates between the two repositories.

The boundary

The polyrepo split is strict:

crucible-simulator owns the state and execution model. crucible-prover owns proving.

This repository therefore contains no state engine: no balances, no ledger, no execution. It answers one question — can I construct and verify the proof for this state transition? — given the state a simulator provides. Duplicating the simulator’s state engine here is an explicit anti-goal (docs/architecture.md).

Seams

Everything the simulator touches is defined in the interface crate, not in any backend:

• ProofProvider — the contract every backend (mock, ultrahonk) implements. The simulator never depends on a concrete prover.
• Prover — the client-facing facade (ProverService) that validates, dispatches, and round-trip-verifies.
• ProofRequest / ProofResponse — the wire shapes, versioned and privacy-correct: requests carry private witness bags (no Serialize, only a redacted view for simulator logs), responses are public and traceable (docs/proving-model.md).
• StateReference — the (root, sequence) pair that lets the simulator name which state a proof applies to, and lets the verifier reject stale/replayed proofs structurally (docs/verification.md).

The adapter (adapters/simulator)

adapters/simulator implements the simulator’s proof seam over the real prover, without importing the simulator’s state engine. The simulator depends on this crate only through its own [ProofProvider] trait:

Simulator flow ──► ProofRequest (simulator) ──► ProofRequest (prover)
       ──► ProverService ──► ProofResponse ──► ProofReference

Its job is mapping — simulator account/commitment/operation types onto the circuit’s named public/private inputs (docs/public-inputs.md) and routing through the Prover trait with the backend chosen per test depth. The translation binds the real circuit ABI: every public parameter and private witness the circuit declares (see [crucible_interfaces::circuit::expectations]). Translation differs by backend:

• Mock backend (ProverBackedProvider::mock): deterministic digest encodings of the request. The mock enforces structure, not cryptography — witnesses the request does not carry become reproducible placeholders.
• Real UltraHonk backend (ProverBackedProvider::ultrahonk): the circuit’s exact values. Witnesses come from the simulator model’s witness material — the acting account’s secret scalar, the openings (value, blinding nonce) of spent commitments, and the fresh blindings for new commitments, all carried on the simulator’s ProofRequest. Public parameters the circuit constrains (addresses, spent commitments) are derived with the circuit’s own hashes through the circuit oracle (CircuitOracle): a tiny Noir package (circuits/hashlib) executed by the pinned nargo that returns key_hash(secret) and commit(amount, blinding) — exact by construction, never a reimplementation. Anything the model does not carry is rejected with a precise reason, never fabricated.
• State binding is real on both paths: the transfer flow names the state root/sequence it transitions, and the adapter binds its root_hi / root_lo halves as the circuit requires.

Wiring it up

#![allow(unused)]
fn main() {
// Fast, deterministic, no toolchain: TEST-ONLY crypto on the real code path.
let mut provider = crucible_simulator_adapter::ProverBackedProvider::mock();
sim.execute_with_proof_provider(operation, auth, Some(&mut provider))?;

// Real UltraHonk proving: requires nargo + bb on PATH and the circuits
// workspace (see scripts/check-bb.sh).
let mut real = crucible_simulator_adapter::ProverBackedProvider::ultrahonk(
    circuits_root,           // the circuits workspace (contains hashlib + target bytecode)
    vk_store_dir,
)?;
sim.execute_with_proof_provider(operation, auth, Some(&mut real))?;
}

Circuit-shape rules the real backend enforces

The protocol circuits consume a fixed number of spent commitments per operation (transfer and deposit/withdraw: one; merge: two). The simulator’s transfer flow spends all of a sender’s active commitments, so a sender holding several must merge first — the real translation rejects a multi-commitment transfer with a precise reason rather than proving an unsatisfiable witness. The end-to-end real test funds the sender with a single deposit for exactly this reason.

Verification

The end-to-end integration test (adapters/simulator/tests/end_to_end.rs) drives a full lifecycle — register, deposit, transfer — against the pinned crucible-simulator revision. The transfer runs twice:

1. through the mock backend — fast, toolchain-free coverage of the whole wiring; and
2. through the real UltraHonk backend — the same simulator lifecycle produces a real proof with bb that the real verifier accepts. This is the polyrepo-level proof that the three repositories speak one contract: simulator state → witness material → real circuit ABI → real UltraHonk proof → verification. It is gated on nargo + bb on PATH (CI installs both in the noir circuits job) and each run pays for real proving.

Honesty contract

• Mock backend by default. [ProverBackedProvider::mock] wires the prover’s deterministic MockProver/MockVerifier — TEST ONLY, not cryptographically secure. It exercises the real code path (real request/response/envelope types, real preflight validation, real verification round-trips) with honest mock crypto, which is exactly what a fast, deterministic simulator layer needs.
• Real proving is real. [ProverBackedProvider::ultrahonk] proves with bb through crucible-ultrahonk — the same backend an on-chain verifier accepts. The simulator model carries the witness material (secrets, openings, blindings); where the model genuinely has no value (e.g. the change blinding of an exact-balance transfer, whose zero-value change commitment the ledger discards), a deterministic request-derived value is used and documented — never fabricated public context.
• Reject, never fabricate. A real translation request missing material a circuit constrains fails with a precise reason before any proving work starts.
• Field values are fields. The adapter encodes only values below the BN254 scalar field modulus; FieldValue rejects anything at or above it on construction (a “field” that does not fit the field cannot be fed to the circuits).
• Determinism preserved. Proofs derive purely from the request and the deterministic oracle, so the same simulator operation always yields the same proof bytes and the same proof reference — the simulator’s determinism guarantee holds through the real prover crate.