Discoveries and how the architecture evolved — told as it happened, with the receipts linked.
Starting point: Shielded CSV (Nick–Eagen–Linus). Day-one decisions: anchor to Bitcoin L1 directly (no fork), shielded amounts with public assets and issuers (auditable supply over shielded transfers), and no zkVM — hand-written AIR with in-circuit recursion. First artifacts: the paper and this site.
The transfer circuit verifies two predecessor proofs in-circuit — mint → transfer → transfer — so proof size and verify time are constant in coin history. Later measured: 56,041 bytes, ~3.6 ms verify, identical at hops 1 and 2. See BENCHMARKS.md.
Lean 4: inflation soundness, conservation, nullifier uniqueness, receiver correctness — sorry-free, every assumption a labeled axiom. Later enforced by CI axiom gating: the assumption set can't grow silently.
Core-scaling: 1 core ≈ 4 = 8 = 64 cores at ~3 s per transfer. Single-core speed is all that matters — which unexpectedly makes phones interesting.
On-device benchmarks (opencsv-rs#1): iPhone 16e and 17 Pro Max prove a recursive transfer in ~0.55–0.96 s vs 2.97 s on the 64-core Xeon. Mobile proving is viable.
Physical iPhone: consignment as an E2E Signal attachment → +100 USD · verified rendered natively; the phone proves a 2-in/2-out transfer (~1 s) → CLI verifies. Audits agree on both sides. (issue, PR #2)
CLI side, regenerated weekly by CI from real regtest runs:
A raw anchor record is just bytes: a mempool spy can copy it into their own transaction and front-run it — the copy wins the first-occurrence race and the victim's coins freeze. Burn, not theft. Three redesign rounds begin.
First fix: publish (nf, B = H(nf, ctx)) and check it publicly.
Broken on arrival — both inputs are on-chain, so the griefer recomputes B under
their own context. Caught by the implementing agent, not shipped. The lesson
that shaped everything after: public matchability and copy-forgeability are
the same property.
The payload IS the bound value: P = H("bind" ∥ nf ∥ ctx), and
the raw nullifier never goes on-chain. Copying fails (wrong ctx); recomputing
needs nf (preimage). Later mechanized in Lean in both directions
(griefer_copy_invisible, no_occurrence_without_knowledge).
The demo chain dies: real transactions on regtest end-to-end, then a 100-USD mint confirmed on Mutinynet signet (tx 3282c8ab…, height 3308725), verified by a fresh wallet from scanned blocks. Two backends converge on one ctx derivation after a near dialect split.
Verified against live bitcoind: basic compact filters omit OP_RETURN outputs entirely — anchor records are never filter-matchable. The compact-filter plan dies on contact; SPV (headers + merkle + one block) takes the point check.
The conservation gadget's carry argument — the scariest informal claim in the codebase — is mechanized (b036cf3). Bonus honest finding: the general converse is false (a completeness limitation, not a soundness hole) — documented, not lurking. The living formal page now carries 17 theorems, regenerated weekly from the build.
Anchor-server (demoted) → full node → N-of-M cross-check → finally
scan-first indexing, which made filters useful again: anchors add a
constant marker output (546 sats to OP_0 ∥ sha256(OP_TRUE),
quantum-clean). Filters include it, so phones find anchor blocks trustlessly
at ~KB/block while the record stays ctx-bound. Exclusion becomes a local check;
indexers become optional, spot-verifiable accelerators. Paper §4.7.1 rewritten
the same day.
The formal layer follows deployment: no-false-negatives of filter discovery (trustless absence is provable — and it fell out of the construction in one line), scan-exclusion soundness (scan-first ≡ full-block scanning), marker zero-authority, accelerator fraud-provability. 23 theorems, no new axioms (00edaed). The N-of-M honesty hypothesis is eliminated from the roadmap — the architecture got better, so the assumptions got fewer.
The marker output lands in anchor transactions
(5564502,
verified against real BIP158 filters), the ScanIndex engine follows
(cd37a53),
and the scan FFI completes the stack
(5a21db1):
a real mint consignment verified through the C ABI with no RPC and no
indexer — VERIFIED from the scan alone, double-spend rejected
against the same index. Bandwidth for the test window: 320 filter bytes +
1,140 block bytes.
The iOS provider swap lands on opencsv-wallet
(1fa76d6944):
decision ladder (self-scan → cross-check → demo, throwing rather than
falling back on an unsynced index), scheduled background sync, the
"fully verified by this phone" badge. The interop proof: an anchor
hand-crafted with raw bitcoin-cli from the spec — 64-byte OP_RETURN at
vout 0, 546 sats to OP_0 ∥ sha256(OP_TRUE) at vout 1 — was
discovered by the scan engine purely via the filter walk, under 5 KB across
a 113-block chain. Two implementations, one protocol, zero coordination.
The Track-A thesis landed end to end. opencsv-kernel
(b64bdf4)
carves the pure decision logic out of core in Aeneas shape — 8/8
equivalence tests against the original code. And the new
formal-aeneas
repo (21364ac) holds four sorry-free refinement theorems:
the translated Rust binding, occurrence test, first-occurrence, and supply
equation are each proved equal to the Lean specification. The supply-loop
proof took a real fight (maxRecDepth explosions until the recursive-theorem
style was abandoned for the library's loop induction principle). The
distinction that matters: this is no longer "a model that corresponds to
the code" — it's the code, proved. Adoption (shipping the verified kernel
in core and the FFI) is the next decision.
The iOS host's forensic hunt (five takes, three logging builds) isolated
why every fresh mint verified everywhere except the phone's
crediting path: consignments written while the anchor is still in the
mempool carry a sentinel location, and only the snapshot verify did a
location-strict lookup. The fix
(1616397)
had its own twist: patching locate() alone wouldn't have
worked — the accept driver consults anchor_at and
ctx_at first, so the sentinel resolution now lives in a shared
find() across all three lookups. Their side-effects were just
as valuable: chain-lag rejections reclassified from final to
withheld-retryable (a race mainnet would have made constant), and Signal's
attachment dedup-by-content recorded as a protocol note.
One small function closed the last trust gap in the receive path:
opencsv_scan_export_snapshot
(290c8e0)
projects the phone's own filter-scanned index into the snapshot format the
crediting verifier already consumes. The headline test is the property the
whole project aims at: a real consignment, verified and credited, with
no RPC, no indexer, no anchor server — zero servers anywhere in
frame. Bonus find: a latent ~1% tag-collision flake in fixed-seed test
anchors, hunted down and fixed with a retry harness across the suites.
The feasibility spike for verifying the Rust implementation directly
returned a clean split. Dead: full-crate Aeneas — a charon bug on std
iterator impls our hashing pulls in, dyn-trait and GAT rejection, and an
outright aeneas crash. Alive and proven: a kernel-shaped subset
(loops, no serde/dyn/RNG, opaque hash boundary) translates in 0.9 s, builds,
and proves — binding_eq_spec and well_formed_spec
showed translated Rust equivalent to the Lean model, with only core axioms
plus the opaque hash constant. The path forward (Track A of
ROADMAP.md):
carve opencsv-kernel from opencsv-core and verify it against
the spec in a dedicated Lean 4.31 + mathlib project. The roadmap noted the
honest fork too: Aeneas pins its own Lean toolchain, so the main
dependency-free repo stays untouched.
The first field-found consensus bug: signet header sync died at height 2016
— the client assumed signet allowed min-difficulty blocks, but real signet is
mainnet-style; block 2019 demanded a true target. Fixed
(e137096)
with a regression that syncs all 315,800 signet headers through 156 retargets
in 193 s. Same batch: batching v1 lands
(3d4da5f) —
witness-envelope batches verified via scan with no RPC and no indexer, after a
real standardness lesson (bare OP_TRUE fails CLEANSTACK with junk
items; the witness script is OP_DROP×(n+1) OP_TRUE, still
quantum-clean). Plus a persistent CBF client killing the per-foreground
handshake cost the iPhone measured.
The per-transaction ceiling broke. Paper §4.7.2 adds optional batching:
a coordinator pre-commits a funding outpoint; each sender computes their
payload locally (P_i = H("bind" ∥ nf_i ∥ X)) and hands
over only 24 bytes — so the batcher combines but can never forge (preimage).
Payloads ride a witness envelope (4× cheaper than OP_RETURN, thousands per
envelope), one constant marker per batch keeps filter discovery unchanged,
and occurrence semantics are untouched: a batch is just a busier anchor.
Silent payments was considered for coordination and rejected: ECDH
breaks the quantum-clean anchor layer, and per-output EC scanning is
strictly costlier than GCS filter matching on mobile. The v2 shape is
coinjoin-style co-funded batches — each sender signs their own input.
The GitHub Pages project site originally kept its homepage under
web/ and used a root meta-refresh. The
opencsv.net cutover makes the repository root canonical:
assets stay grouped under web/, while the old
web/index.html becomes a compatibility redirect. Ordering is
part of the design: domain ownership and DNS must verify before the Pages
custom-domain flip, so the working github.io site never
redirects into an unresolved hostname.