proof latency on user devices — 2026-10-14

Owner directive (2026-10-14): proving takes ≤ 1 s — "the product doesn't exist without it". Scope (coordinator, recorded as the gate row in proof-system-repair §0): every proof a user device produces on the product path, end to end through joy prove (process start → envelope written), warm and cold, on Apple Silicon Metal (the gate), also measured on CPU and WebGPU. Constant-size compression of long computations (profile 6, the wrap chain) runs on aggregators off the critical path and is not in this gate.

Stand ~/cyber/.stands/FAST: zheng feat/fast-path 50b3d4d (zheng#64, on release/0.4 15b9549), lens feat/fast-path e240123 (lens#25, on release/0.2 61c2a8f), joy release/0.4 d8cfae9 (no joy change), nox release/0.4, trident release/0.4, bbg 48153b2, hemera cf28a64/main, strata 494df7a, honeycrisp 9cbd480. Apple M4 Max (12P + 4E, 40-core GPU, 48 GB), macOS 26.4, rustc 1.95.0, --release. The machine was shared with other agents. The tables below were taken at 17:29–17:43 with load average 5–18. During the day's runs load reached 36, and Metal medians at 2^18 doubled under it. Proof bytes and sizes are deterministic. Every backend produced the same bytes (SHA-1 per fixture in §3). Android: no device attached (adb absent), not run.

1. inventory — the proofs a user device produces

Read from the default branches on 2026-10-14 (cyb, foculus, mudra, cybergraph, bbg, tru, soft3; joy and zheng on their release lines). No product repository calls the sound prover yet. Every proof a device makes today goes through zheng's retired fold/decide API (feature legacy, unsound: zheng/rs/Cargo.toml, specs/decider.md), and cyb's body prover imports zheng::{prove_spmv, …} without that feature, so it does not build against zheng 0.4. The table therefore maps each product statement to the profile-1 relation that proves what it claims, and that relation is what is measured in §3.

Relation sizes (columns = committed variables after padding): hash-3 2^11, hash-8 2^13, hash-12 2^13 (2^14 rows), batch-4 2^15, merkle-12 2^16 (2^17 rows), merkle-16 2^17, merkle-32 2^18. One hemera hash of a digest costs ~2,700 constrained wires because nox hashes nouns structurally (every atom is decomposed into 64 bits and hashed by two permutations); a Merkle level hashes both children in the circuit (the direction mux makes the sibling a wire), ~5,000 wires a level.

2. what was done

Profile 1 (one relation: Spartan over Fp3 + one WHIR opening) is the user-device profile. The levers, in order of what they bought:

The verifier is unchanged in kind. It reads the WHIR parameters from the proof and admits them only at ≥ 128 proven bits, so earlier proofs still verify. Verifier paths stay CPU-only: the key digest uses Tree::build_on_cpu, and lens's verifier never reached a device.

3. measurements

cold = joy prove in a fresh process (median of 3; prove ms as joy reports it, then wall seconds from /usr/bin/time, then peak RSS), OS shader cache warm. warm = in-process with a held ProvingKey (zheng example fast_path, FAST_KEY=1, median of 5): a device that proves the same statement type again. Size = joy artifact bytes. Verify = joy verify wall time in a fresh process (relation recompiled, CPU). Commands: /tmp/fast-tools/joy_table.sh, warm_table.sh; fixtures via FAST_DUMP (raw .nox + inputs).

profile 1 (succinct), product-shaped statements

Relation-level (no statement type wraps it in profile 1 yet), body SpMV ticket shape, in-process without a key: synthetic-14 65 / 124 / 141 ms (metal / cpu / webgpu), 40,781 B proof; synthetic-16 157 / 329 / 332 ms, 49,805 B.

First process after a kernel change (Metal shader compile, OS cache cold): hash.tri 0.78 s wall (prove 46 ms), veil hash 0.76 s. Every later process: 0.05–0.10 s.

profile 2 (veil, zero knowledge) — P1-shaped

The program's input is secret: hash of a secret preimage; membership with a secret leaf.

before → after (Metal, joy prove, fresh process)

same bytes, ledger, soundness

• Byte identity: profile-1 envelopes for add, hash, chain-4, merkle-3 and synthetic-14 at fixed parameters are SHA-1 equal to release/0.4 on cpu, metal and webgpu. Every row above is SHA-1 equal across the three backends. Held-key proofs equal cold proofs (asserted on every warm run; test a_held_key_proves_the_same_bytes_and_refuses_other_programs).
• Ledger: device_parameters_meet_the_ledger_at_every_size gives ≥ 128 proven bits (ROM, grinding counted) at every size 2^1…2^20. Without grinding the bound is 112 bits up to 2^17, 106 at 2^18 and 104 beyond; it was 104 at every size under the old 24-bit choice.
• Bit-flip scans, 0 accepted: device_params hash.tri 134,048 flips; folding 5 with 16 / 22 grinding bits 155,232 / 152,352 flips; the veil envelope 512,960 flips.
• Suites: zheng 371 passed, 0 failed, 18 ignored; joy 219 passed against the branches; lens rspcs 43 and GPU differential 14 (LENS_GPU_REQUIRE=metal,webgpu).
• Merged 2026-10-14: lens#25 into release/0.2, after rebasing onto lens#26 (kernel speed): differential 15, rspcs 43, bytes unchanged. zheng#64 into release/0.4, after rebasing onto zheng#65: lib 305 and the succinct, veil, key and transcript suites green. One spot check after the rebases (load 20): merkle-32 joy prove Metal 999 ms prove, merkle-16 459 ms, same artifacts.

4. verdict

≤ 1 s on Metal, warm and cold (fresh process): every product-shaped statement up to Merkle depth 16. That covers the ticket, pay σ, tip/fold merge, the 4-ticket settlement seal, the depth-12 balance opening and depth-16 membership in profile 1, plus P1-shaped veil proofs up to depth 12. CPU and WebGPU are also under 1 s for these, except veil depth 16.

Not ≤ 1 s:

• Membership depth 32 (2^18), cold: 1.13 s Metal, 1.6 s CPU, 1.8 s WebGPU. It is 0.61 s warm with a held key on Metal, so only the warm gate is met. Why: one Merkle level costs ~5,000 constrained wires. nox hashes nouns structurally (each atom is bit-decomposed and permuted twice), and the direction mux puts both children in the circuit. At 2^18 the 64 KB cap also forces 22 grinding bits (~0.1–0.2 s of expected grinding, high variance). The remaining cold costs are the relation compile (~200 ms) and the key digest (~60 ms). Next levers: a cheaper relation for structural hashing (a digest-pair hash without per-atom decomposition), or a disk-held proving key in joy.
• Veil (P1) beyond depth 12: depth 16 0.94 s Metal and depth 32 2.0 s. The veil prover is not device-accelerated: ~45 % of it is the hiding commitment's sequential constant-time XOF (mask and salt coins, one permutation per 4 elements) plus single-threaded CT leaf hashing. Its proofs are 295–545 KB, outside 64 KB. Parallel counter-mode coins would change the randomness design and need their own review; this branch does not touch them.
• The first Metal process after a kernel change pays ~0.7 s of shader compilation, once per installed version.
• P2 (stealth/veil balances), P3 (hidden ego-net) and oikos have no defined statement, so they could not be measured. Tickets, pay, seals and tips are still produced by the unsound legacy API in cyb/foculus. Moving them to profile 1 relations like the fixtures above is the product-side work this measures for.
• Peak RSS at 2^17–2^18 on Metal is 0.9–2.1 GB, from staging buffers (codeword copies). This matters on phones; it was not reduced here.

5. follow-up — fast path 2 (same day, 21:30)

zheng#66, lens#27, joy#42, merged into release/0.4 / release/0.2; report zheng/audit/fast-path-2-2026-10.md. Load 24–50.