Handover: remaining OpenCSV work + cloudflarify opencsv.net

[posix4e]

Handover: remaining OpenCSV work + move to opencsv.net (Cloudflare)

This is the master handover issue. Everything is linked; nothing lives in chat.
The plan of record is ROADMAP.md (rev 3); the narrative of record is the journal.

Execution order

1. Coordination and domain preparation
2. A3 reproducible formal build
3. A4 staged kernel adoption and A5 accept-kernel
4. Prover production readiness: D1 → D4 → D3 → D2
5. Batching v2
6. Signet/mainnet readiness
7. iOS — final workstream

A. Domain: cloudflarify opencsv.net (registered on Namecheap)

Goal: the site serves from https://opencsv.net via Cloudflare DNS; everything currently at opencsvnet.github.io/opencsv remains available during the cutover.

Ordered steps (order matters — do not set the Pages custom domain before DNS resolves):

1. Repository preparation: make / the canonical homepage; keep /web/index.html as a compatibility redirect; verify all site paths and relative assets.
2. Cloudflare (owner account): add site opencsv.net (Free plan) and note the two assigned nameservers.
3. GitHub org verification: start verification of opencsv.net at org Settings → Pages and obtain the TXT value. Stage only that TXT record in Cloudflare.
4. Namecheap (owner account): Domain List → opencsv.net → Nameservers → Custom DNS → the two Cloudflare nameservers. There is currently no DS record; if that changes, remove the old DS and wait for expiry before switching.
5. Wait for delegation (dig NS opencsv.net shows only Cloudflare) and the GitHub TXT record; complete organization-domain verification before publishing Pages target records.
6. Cloudflare DNS records, DNS-only initially: apex A/AAAA records to GitHub Pages; www CNAME to opencsvnet.github.io. Do not use a wildcard.
7. Confirm public resolution from multiple resolvers, then GitHub Pages (opencsvnet/opencsv) set custom domain to opencsv.net. Wait for certificate issuance, then enable Enforce HTTPS.
8. Verify /, /web/journal.html, /web/formal.html, /web/story.html, compatibility redirects, screenshots, and animation media. Update remaining github.io public links.
9. After the cutover is stable, optionally enable Cloudflare proxying. Enable Cloudflare DNSSEC and publish its DS record at Namecheap.

The GitHub Pages custom-domain flip is deliberately after verified DNS so the working github.io site never redirects into an unresolved hostname. Organization verification is mandatory before the Pages target records to close the takeover window.

B. Open work board

Formal verification (the moat)

• A2 kernel carve — opencsv-kernel landed at opencsv-rs@b64bdf4; 8/8 kernel≡core tests green.
• A3 reproducibility follow-ups — pin the Aeneas Lean library by Git revision; make CI genuinely runnable; dedupe binding_eq_spec; expand the seven-theorem audit; feed the generated audit into the living formal page.
• A4 staged adoption — dual-run kernel and legacy decisions in tests, add generated differential cases, then switch binding/well-formed/first-occurrence/supply individually. Review diff; no silent merge.
• A5 accept decision-kernel — pure explicit input → deterministic decision/rejection reason; the trait-heavy driver retains proof, chain, storage, and transport I/O.
• Standing: executable-model differential testing remains the drift bridge.

Prover production readiness

Details: opencsv-rs#3.

• D1 setup caching.
• D4 predecessor vk hard-binding.
• D3 AIR-native issuer signature.
• D2 production FRI parameters and final benchmarks, only after D4/D3 freeze the circuit/vk surface.

Batching v2

Details: opencsv-rs#4.

• C0 committed protocol/threat model: commitments, fees/outputs, aborts, coordinator DoS, replay, ordering, serialization.
• C1 coinjoin-style co-funded batches, regtest-proven with adversarial mutations.
• C3 Lean extension against frozen C1 semantics.
• C2 two-round Signal gossip in the CLI. iOS integration waits for the final workstream.

Mainnet path

• E1 signet field validation through the CLI/reference stack: cold/hot sync, bandwidth, latency, reliability, and recovery.
• E2 beta economics: fees, marker dust, and batch amortization.
• E3 security review after A4/A5, D2–D4, and C1.
• E4 reproducible CLI/reference builds, release checklist, and claim receipts.

iOS app — final workstream

Channel: Signal-iOS#3.

• PR blockers B1–B3 and S1–S9 fixed on the feature branch.
• Explorer detail view, deliberate re-verification, persistence/chain-lag fixes, and persistent client landed.
• Regtest/hardware receive measurements and S1–S3/video captures delivered. These are evidence, not the remaining signet gate.
• Final-core integration: durable pending export/import; fee key + watched UTXOs; signed anchor construction/P2P broadcast; final proof parameters; batch envelope evidence.
• Rebase, final review, both build modes, full suites, physical-device two-way flow, crash recovery, and mempool→confirmed validation.
• PR site: make root the canonical homepage #2 upstream-submission decision is the owner's explicit call.

Rules of engagement

• Nothing fake: no mocks or silent fallbacks in product paths; demo chains print a warning.
• Every claim has a receipt: benchmarks measured, screenshots CI-regenerated, formal table CI-regenerated from the build.
• Honesty pages stay honest: when a gap closes, update formal.html the same day.
• The journal gets an entry for every design change or discovery, including failures.
• Every active AI work item records agent, repo, branch, base SHA, and expected files. One writer per branch/worktree; no shared build directories or force pushes.
• Git mutations, PRs, releases, upstream submissions, external posts, and mainnet broadcasts are deliberate actions.

[posix4e]

Codex implementation lease — 2026-08-02

Starting the approved handover plan in isolated clones under /Users/posix4e/Documents/opencsv/worktrees/; Claude's worktrees are out of scope.

Repository	Base	Branch	Initial file/surface lease
opencsvnet/opencsv	c5f63fab	codex/domain-homepage-handover	master handover/roadmap reconciliation; root homepage + compatibility redirect; domain runbook and link verification
opencsvnet/formal-aeneas	21364acd	codex/a3-reproducible-ci	lakefile.toml, manifest/CI, duplicated refinement theorem, axiom audit, README

Execution order remains: domain/coordination → A3 → A4/A5 → D1/D4/D3/D2 → batching v2 → signet/mainnet readiness → iOS last. I will post receipts and PR links per tranche. No opencsv-rs or Signal-iOS files are claimed in this tranche.

[posix4e]

Domain + A3 progress receipt — 2026-08-02

Domain

• Owner added opencsv.net to Cloudflare and completed the Namecheap nameserver change.
• Public delegation now returns only dayana.ns.cloudflare.com and thomas.ns.cloudflare.com.
• No DS record is published yet; DNSSEC remains correctly deferred until after the cutover.
• Owner reports email configured. Public DNS confirms Cloudflare Email Routing MX records (route1, route2, route3) plus the Cloudflare SPF include.
• The apex and www intentionally have no Pages target records yet. This preserves the required ordering: org verification TXT first, Pages DNS second, custom-domain flip last.
• GitHub org-domain verification is waiting on admin:org authorization; the current automation token has repo/workflow/read-org scopes only. The Pages custom domain has not been changed.

Repository preparation is in draft PR #2: #2

Receipt: commit 42a02cb on codex/domain-homepage-handover; local link/asset checks, HTTP smoke tests, and git diff --check passed.

A3

Active isolated checkout: formal-aeneas@21364acd, branch codex/a3-reproducible-ci.

Implemented locally and under validation:

• replaced the absolute /tmp Aeneas dependency with upstream commit daa85d7e89400fa978be83fedbc7e475a83f0889;
• removed the duplicated binding refinement theorem;
• expanded the axiom-audit surface;
• activated cache/build/no-sorry CI checks;
• updated the reproducibility documentation.

Lean 4.31.0/Lake 5 are installed. Manifest regeneration and the full build/audit are the remaining gates before the A3 commit and draft PR. No iOS work has been touched.

[posix4e]

Root homepage live + public formal receipt lease — 2026-08-02

Repository preparation is now complete on main:

• PR site: make root the canonical homepage #2 merged as 7aeae41; follow-up e7ab5a9 points screenshot stamping at root index.html.
• Pages deployment run 30764542325 succeeded.
• https://opencsvnet.github.io/opencsv/ returns HTTP 200 with the canonical homepage.
• /web/index.html returns HTTP 200 with the compatibility redirect to ../.

Starting the public A3 receipt wiring in a separate isolated checkout:

Repository	Base	Branch	File/surface lease
opencsvnet/opencsv	e7ab5a91	codex/a3-formal-receipts	.github/workflows/formal-page.yml, site-owned audit renderer, the generated sections of web/formal.html, and matching journal receipt

This branch will add the formal-aeneas audit as a separately labeled 15-declaration table; it will not inflate the existing 29 model-theorem count or touch domain DNS/Pages settings. A3 implementation is in draft formal-aeneas PR #1: opencsvnet/formal-aeneas#1

[posix4e]

Codex A4 implementation lease — 2026-08-02

A3 implementation and its public receipt are locally green:

• formal-aeneas#1 / 3bcafed: Lean build + 15-declaration axiom audit pass in CI and locally.
• opencsv branch codex/a3-formal-receipts / local commit 2cfe21e: both-proof build gate, deterministic dual-table renderer, CI artifact receipt, formal-page update, and journal entry. This remains unpushed until the A3 dependency PR is approved.

Starting A4 in a fresh isolated clone; Signal-iOS remains untouched.

Repository	Base	Branch	Expected files/surface
opencsvnet/opencsv-rs	b64bdf4	codex/a4-kernel-adoption	core/kernel Cargo edges; kernel hash boundary; core binding, well-formed/occurrence, first-occurrence and supply delegation; deterministic generated differential tests; kernel adoption docs

External CLI/FFI behavior is frozen. The transition will keep a test-only legacy oracle while switching production decisions one surface at a time; no A5/prover/batching/iOS files are claimed in this tranche.

[posix4e]

Domain cutover receipt — 2026-08-02

Completed:

• Added and verified opencsv.net in the opencsvnet GitHub organization using the GitHub Pages challenge TXT record.
• Cloudflare is authoritative at dayana.ns.cloudflare.com and thomas.ns.cloudflare.com.
• Added DNS-only GitHub Pages records: four apex A records, four apex AAAA records, and www CNAME to opencsvnet.github.io. Existing email records were preserved.
• Attached opencsv.net to repository Pages only after the authoritative apex records resolved.
• GitHub Pages reports protected domain verified, DNS check successful, build status built, certificate approved for opencsv.net and www.opencsv.net, and HTTPS enforced.

Live validation:

• https://opencsv.net/ — 200
• /web/journal.html — 200
• /web/formal.html — 200
• /web/story.html — 200
• /web/index.html — 200 compatibility redirect document pointing to ../
• Paper, animation MP4, and three homepage screenshots — 200 with the expected content types
• http://opencsv.net/ redirects to https://opencsv.net/
• https://www.opencsv.net/ redirects to https://opencsv.net/

The current homepage source was already healthy, so no webpage-code rewrite was needed for this repair. Recursive resolvers that cached the earlier NXDOMAIN may take up to the old 30-minute negative TTL to observe the new records; authoritative Cloudflare DNS is already correct.

[posix4e]

Codex A5 implementation lease — 2026-08-02

A4 is locally complete on codex/a4-kernel-adoption at 4274d68 (five staged commits over b64bdf4). Generated valid/mutated differential traces, core, CLI, prover, regtest-backed CBF tests, and the complete FFI suite pass. The only red validation is the separate live signet test: the existing local node on 127.0.0.1:38333 accepts TCP then closes during header sync on two attempts; no local node or other agent process was restarted.

Starting A5 from the A4 tip in another isolated checkout. Signal-iOS remains untouched.

Repository	Base	Branch	Expected files/surface
opencsvnet/opencsv-rs	local A4 4274d68	codex/a5-accept-kernel	pure accept input/result/rejection types and deterministic decision function; trait-heavy driver projection/adaptation; generated decision differential tests; accept-kernel documentation

Networking, proof verification, chain reads, storage, and transport remain in the driver. The kernel receives only explicit already-observed state and returns a stable decision; external CLI/FFI behavior remains unchanged.

[posix4e]

Codex checkpoint — A4 and A5 are locally complete and reviewable; nothing here has been pushed or merged.

A4 staged kernel adoption

• Agent: Codex
• Isolated checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-a4
• Branch: codex/a4-kernel-adoption
• Base: b64bdf4
• Tip: 4274d68
• Commits: 519595b, eaacf10, b9d3c94, 51d0645, 4274d68
• Production switches: binding, occurrence/well-formedness, first occurrence, and supply.
• Evidence: deterministic generated valid/mutated trace differential tests retain a test-only independent legacy oracle; affected crates pass with RUSTFLAGS=-D warnings; the non-CBF workspace, CLI, FFI, proof, batch, scan, and regtest tests pass.
• Compatibility receipt: no source diff under ffi/ or crates/opencsv-cli/.

The only full-workspace failure was the existing live Signet test: the shared node at 127.0.0.1:38333 accepts TCP and closes during the P2P handshake. I did not restart or reconfigure it because separate Bitcoin processes/worktrees are active on this machine.

A5 pure accept boundary

• Agent: Codex
• Isolated checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-a5
• Branch: codex/a5-accept-kernel
• Base: A4 tip 4274d68
• Tip: 8902ac2
• Commits: 905182e (pure input/decision/rejection boundary), 8902ac2 (core-driver projection and differential receipts)
• Expected files: crates/opencsv-kernel/src/accept.rs, kernel exports/docs, crates/opencsv-core/src/accept.rs, and crates/opencsv-core/tests/kernel_differential.rs.
• Boundary: the driver retains proof verification, chain I/O, storage-facing traits, key-derived ownership, and coin construction; the kernel receives explicit observations and deterministically returns accept or a stable machine-readable rejection code.
• Evidence: 512 generated accept states match the frozen legacy precedence; all 27 receiver protocol tests pass; kernel/core pass warning-denied; the complete non-live workspace passes, including CLI, FFI, Signal, and real prover tests; no CLI/FFI source diff.

The warning-denied whole-workspace run also exposed pre-existing warnings in FFI test fixtures (anchor_xfer_retry, anchor_xfer_same_retry, and one unused raw_nf). The normal whole-workspace run is green; A5 files themselves remain warning-clean.

Next lease: D1 setup cache, keyed by complete setup/verification-key identity with cold, warm, invalidation, and concurrency receipts. Reviews of either local tip are welcome before publication.

[posix4e]

D1 lease — Agent: Codex. Fresh isolated checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-d1. Base: 2a4ae4d. Branch: codex/d1-prover-setup-cache. Expected surface: crates/opencsv-pcd setup/prover modules and focused cache tests/docs only. Goal: cache by complete setup plus verification-key identity, with cold, warm, invalidation, and concurrent-access receipts. No iOS or Claude worktree will be touched.

[posix4e]

Correction to the immediately preceding D1 lease: base 2a4ae4d is the opencsv website repository, not opencsv-rs. No files were edited in that checkout. I am discarding that untouched clone and will post the correct opencsv-rs base and lease next.

[posix4e]

D1 corrected lease — Agent: Codex. Fresh isolated opencsv-rs checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-d1. Base: b64bdf49caa3a46a10084e20fc36560bb2b8def3. Branch: codex/d1-prover-setup-cache. Expected surface: crates/opencsv-pcd setup/prover modules and focused cache tests/docs only. Goal: cache by complete setup plus verification-key identity, with cold, warm, invalidation, and concurrent-access receipts. No iOS or Claude worktree will be touched.

[posix4e]

D1 complete locally — Agent: Codex. Checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-d1. Branch: codex/d1-prover-setup-cache. Base: b64bdf49caa3a46a10084e20fc36560bb2b8def3. Tip/commit: ca8ad37. The process-wide caches are bounded to eight LRU entries per base/recursive family and key SHA-256 over canonical circuit structure, packing, AIR/profile, full FRI parameters, crate/upstream pin, and ordered predecessor verification-key identity (metadata, manifest, lookup description, preprocessed commitment and metadata; never proof bytes). Upstream circuits are not Send/Sync, so only preprocessed prover data is shared; local circuits keep witness generation concurrent and the internally mutable schedule cache is mutex-guarded. Receipts: cold/warm reuse, parameter/circuit/parent-vk invalidation, eviction, and 8-way concurrent cold access with one build all pass; opencsv-pcd is green with RUSTFLAGS=-D warnings; the complete non-live workspace is green. Existing unrelated kernel/FFI test warnings remain visible in the normal workspace run. BENCHMARKS keeps the old cold numbers honestly labeled and defers fresh numbers to D2. Next: D4 hard predecessor-vk binding.

[posix4e]

D4 lease — Agent: Codex. Fresh isolated checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-d4. Branch: codex/d4-hard-bind-predecessor-vks. Base: D1 tip ca8ad37bdbaeac6666f55a7677071e7779f4ea86. Expected surface: crates/opencsv-pcd recursive verifier/common-data binding, tests, and docs; a pinned upstream patch only if the audited public API cannot express the invariant. Goal: predecessor verification-key mismatches are rejected by the verification boundary itself, with explicit foreign-key and tampering tests. No iOS or Claude worktree will be touched.

[posix4e]

D4 local implementation and validation checkpoint — Agent: Codex.

• OpenCSV checkout: /Users/posix4e/Documents/opencsv/worktrees/opencsv-rs-d4
• Branch: codex/d4-hard-bind-predecessor-vks
• Base: D1 tip ca8ad37bdbaeac6666f55a7677071e7779f4ea86
• Current OpenCSV changes are intentionally uncommitted until the dependency pin is portable.
• Audited upstream checkout: /Users/posix4e/Documents/opencsv/worktrees/plonky3-recursion-d4
• Upstream base: official b36339709a7a67ee9760fb578b3d4339fd983709
• Minimal accessor patch commit: d6510eb629097d733d631e8e833fc962025f25f5

Implemented invariant:

• Every transfer/redeem parent circuit extracts the recursive verifier preprocessed-commitment targets and constrains each element to the predecessor key selected when that parent circuit is built.
• The binding uses the recompose/coeff WitnessChecks table, so it rejects both changed base-field elements and non-zero extension coefficients.
• Genesis circuits keep the old table manifest; transfer/redeem proofs add the coefficient table. Native and recursive verifiers select the matching manifest dynamically.
• Missing keys and target/value shape mismatches have explicit errors.
• Root proof allowlisting is documented as a separate remaining verifier-configuration boundary; D4 does not overclaim that recursive predecessor binding authorizes arbitrary roots.

Receipts:

• Three focused tests: expected key accepted; changed key element rejected; non-base extension injection rejected.
• Full mint → transfer recursive proof: 45.57 s debug, 56,995 B, 45.85 ms native verify.
• Slow two-hop mint → transfer → transfer: hop 1 46.14 s / 56,995 B / 44.38 ms; hop 2 46.71 s / 57,141 B / 43.76 ms; green.
• Complete non-ignored opencsv-pcd suite green.
• RUSTFLAGS=-D warnings cargo check -p opencsv-pcd --all-targets green.
• Minimal upstream accessor patch passes cargo check -p p3-recursion.

Packaging decision needed before I can commit D4 reproducibly: may I create an opencsvnet/Plonky3-recursion fork, push only d6510eb, and pin all four recursion crates to that immutable commit? I will not open an upstream PR. The alternative is vendoring the patched recursion sources into opencsv-rs, which is larger and less maintainable.