docs(handover): mirror ~/Desktop/ECHIDNA-*.md into docs/handover/

Makes the production-wiring plan + L1/L2/L3 continuation prompts
part of the repo so a fresh clone has the full handover context
without needing Desktop access.

- docs/handover/PRODUCTION-WIRING-PLAN.md (← ECHIDNA-PRODUCTION-WIRING-PLAN.md)
- docs/handover/L1-CAPNPROTO-PROMPT.md
- docs/handover/L2-CHAPEL-PROMPT.md
- docs/handover/L3-LIVE-PROVER-CI-PROMPT.md
- docs/handover/README.md — drift-handling policy (both copies
  updated in same commit; in-repo copy wins on conflict).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/handover/L1-CAPNPROTO-PROMPT.md

@@ -0,0 +1,92 @@
+# Echidna L1 — Cap'n Proto Protocol Swap — Continuation Prompt
+
+**Context**: Echidna currently uses HTTP + JSON for Rust↔Julia (GNN inference) via
+`src/rust/gnn/client.rs` → `src/julia/api_server.jl` port 8090. This violates the
+`feedback_no_json_emit_a2ml` memory rule and blocks a clean polyglot IPC story. Swap to
+**Cap'n Proto** (chosen over Bebop3 for dependability + maturity + zero-copy reads).
+
+**Master plan**: `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
+**Prerequisite**: L3 Tier-1 green for ≥7 days on main.
+**Follows**: L2 (Chapel) consumes these schemas.
+
+## Deliverables
+
+### Schema
+- `schemas/echidna.capnp` — canonical wire schemas:
+  - `ProofGoal` — a theorem/claim to prove
+  - `ProofResult` — success/failure + metadata
+  - `TacticSuggestion` — ML-suggested tactic
+  - `GnnRankRequest` / `GnnRankResponse` — replaces current HTTP+JSON
+  - `ProverInvocation` — dispatch message to a backend (used later by Chapel in L2)
+  - `TrustedOutcome` — post-trust-pipeline result
+- `schemas/VERSIONING.md` — forward/backward compat rules
+
+### Rust side (hot-path consumer)
+- `src/rust/ipc/mod.rs` — Cap'n Proto transport module
+- `src/rust/ipc/uds.rs` — Unix-domain socket transport (primary)
+- `src/rust/ipc/tcp.rs` — TCP transport (fallback for containerised cases)
+- Replace `src/rust/gnn/client.rs` HTTP calls with Cap'n Proto over UDS
+- Keep `serde_json` out of hot path; retain only for config/log emission (Nickel for config proper)
+
+### Julia side
+- `src/julia/ipc.jl` — Cap'n Proto reader/writer
+- Use `CapnProto.jl` if mature enough; otherwise shim via C-ABI (our Zig FFI layer)
+- `src/julia/api_server.jl` — switch from HTTP to UDS listener
+
+### Idris2 ABI proofs
+- `src/abi/CapnSchemas.idr` — formal proofs that schema round-trip preserves meaning
+- Zero `believe_me` (per estate rule); constructive proofs only
+- Coordinate with `src/abi/Types.idr` / `src/abi/Foreign.idr`
+
+### Zig FFI bridge
+- `ffi/zig/capnp_bridge.zig` — C-ABI bridge for polyglot consumers (esp. Chapel in L2)
+
+### ReScript bindings (UI path)
+- `bindings/rescript/echidna_capnp.res` — typed ReScript bindings for the UI layer
+- Keep the existing 3 API interfaces (GraphQL/gRPC/REST) as external surfaces; Cap'n Proto is the
+  **internal** wire format
+
+### Tooling
+- `just capnp-gen` — regenerates Rust/Julia/Idris2/Zig/ReScript bindings from `.capnp` schemas
+- CI check: `capnp compile` runs clean + generated code is committed
+
+## Acceptance criteria
+
+- Zero `serde_json::to_*` / `serde_json::from_*` calls on the Rust↔Julia hot path
+- `src/rust/gnn/client.rs` uses UDS+Cap'n Proto
+- Benchmarks: Cap'n Proto round-trip ≤ 50% of JSON latency for GNN rank request
+- Idris2 ABI compiles with zero `believe_me`
+- Round-trip property tests on all six schemas (Rust, Julia, Idris2)
+- `schemas/VERSIONING.md` explains migration story
+
+## Open design questions to settle early
+
+1. **UDS path convention** — `/run/echidna/ipc.sock` vs `$XDG_RUNTIME_DIR/echidna/ipc.sock`?
+2. **Authentication** — initial handshake signed with existing BLAKE3/SHAKE3-512 integrity keys?
+3. **Streaming vs request-response** — Cap'n Proto RPC streams for GNN batch inference?
+4. **Multi-locale Chapel** — schemas need to survive locale-to-locale transit; design for that now
+   so L2 doesn't re-spec.
+
+## Hand to L2 when
+
+- Cap'n Proto is the default Rust↔Julia path
+- `ProverInvocation` + `TrustedOutcome` schemas are stable (L2 Chapel will consume them)
+- Zig FFI bridge passes round-trip test
+
+---
+
+## Rules active
+
+- `no_json_emit_a2ml` — the whole reason this phase exists
+- `feedback_verisimdb_policy` — all IPC traffic should be observable as VeriSimDB records
+- `feedback_code_only_grep_for_banned_patterns` — when auditing for `serde_json` removal, use
+  code-only grep (`^[^-|]*serde_json`) to avoid comment/doc noise
+- `feedback_wire_everything` — no stubs; every schema has a live consumer on all sides
+
+## Key files to read first
+
+1. `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
+2. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/rust/gnn/client.rs` (current JSON path)
+3. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/julia/api_server.jl` (Julia server)
+4. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/abi/*.idr` (existing Idris2 ABI)
+5. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/zig_ffi/` (existing Zig FFI layer)

docs/handover/L2-CHAPEL-PROMPT.md

@@ -0,0 +1,101 @@
+# Echidna L2 — Chapel Maximum Integration — Continuation Prompt
+
+**Context**: Echidna has a 420-LoC Chapel POC (`chapel_poc/parallel_proof_search.chpl`) that implements
+30-prover parallel portfolio dispatch but is **not wired into `src/rust/dispatch.rs`**. User directive
+(2026-04-19): "expand Chapel to do EVERYTHING it can — no point investing in hard Chapel code and not
+using it to maximum value."
+
+**Master plan**: `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
+**Prerequisites**: L3 Tier-1+Tier-2 green; L1 Cap'n Proto schemas stable.
+**Scope**: ~5–6 weeks, broken into 7 sub-waves.
+
+---
+
+## What Chapel is actually good at (the full opportunity)
+
+1. **Task parallelism** (`coforall`, `cobegin`, `begin`) — parallel prover dispatch, speculative tactic branches
+2. **Data parallelism** (`forall`) — corpus-wide premise scoring, tactic mining
+3. **Distributed PGAS** (locales, on-clauses) — multi-node proof search with sharded corpus
+4. **Domains & distributions** — data-dependent workload partitioning
+5. **Atomics** — first-wins racing, lock-free coordination
+6. **Reductions** — parallel statistics, confidence aggregation
+7. **GPU support** — Chapel-on-NVIDIA for embedding batches
+8. **NUMA awareness** — locale-aware dispatch on multi-socket machines
+
+## Sub-wave breakdown
+
+### L2.1 — Portfolio dispatch (promote POC) ~1 week
+- `src/chapel/portfolio.chpl` — migrate + adapt from `chapel_poc/parallel_proof_search.chpl`
+- Input: Cap'n Proto `ProverInvocation` batch (from L1)
+- Output: Cap'n Proto `TrustedOutcome[]`
+- Race semantics: atomic first-wins, SIGKILL losers, cancellation within `timeout`
+- Wire into `src/rust/dispatch.rs` behind `--chapel` feature flag via Zig FFI
+- Default: feature-off; default-on flip after L2.7 benchmarks
+
+### L2.2 — Speculative tactic search ~1 week
+- `src/chapel/tactic_search.chpl`
+- Parallel beam search (k parallel beams)
+- Parallel MCTS over tactic trees (UCB1 selection with `coforall` rollouts)
+- Speculative branch execution + cancellation on winner commit
+- Consumes `TacticSuggestion` stream from GNN (L1 schemas)
+
+### L2.3 — Corpus-parallel ops ~1 week
+- `src/chapel/corpus.chpl`
+- `forall` over 66,674-proof corpus
+- Parallel proof replay (re-verify corpus)
+- Parallel premise scoring (vs GNN rankings)
+- Parallel tactic mining + inverted index build
+- Locality-aware: `forall ... with (ref corpusShard)` to avoid cross-locale traffic
+
+### L2.4 — Mutation testing parallelism ~3 days
+- `src/chapel/mutation.chpl`
+- Fan out 1000s of mutants across all cores/locales
+- Integrate with existing Rust `verification/mutation.rs` (consume its mutant stream, run in Chapel)
+
+### L2.5 — Multi-locale distributed ~1.5 weeks
+- PGAS-sharded corpus across locales (`Block` or `Cyclic` distribution)
+- Locale-aware prover dispatch: heavy backends on dedicated locales
+- GPU-locale offload: embedding batches on NVIDIA locale if present
+- Reproducibility: locale seed propagation
+- Single-locale covers 80% of value; multi-locale proven on dev hardware
+
+### L2.6 — Numeric hot paths ~4 days
+- `src/chapel/numeric.chpl`
+- Parallel GNN embedding pre-processing (batch pack + pad)
+- Parallel Pareto frontier computation (`forall` + atomic minimum tracking)
+- Parallel confidence statistics / Bayesian timeout updates
+
+### L2.7 — CI + bench ~3 days
+- `.github/workflows/chapel-live.yml` — runs Chapel-in-dispatch tests
+- Criterion benchmarks: Chapel portfolio vs Rust+Rayon baseline
+- Must show measurable speedup on 8+ core machines to flip default-on
+
+## Acceptance criteria
+
+- Chapel on hot path by default after benchmarks prove it
+- `src/chapel/` has 6+ modules wired via Zig FFI + Cap'n Proto
+- `chapel_poc/` archived (or deleted) with redirect note in its README
+- Multi-locale path proven on at least one dev-hardware config
+- Benchmarks show ≥1.5× speedup for portfolio solving on 8-core machines (or Chapel stays feature-flagged)
+- No Rust code duplicates what Chapel does best (avoid double-paths)
+
+---
+
+## Rules active
+
+- `feedback_wire_everything` — no stubs; POC promoted fully, not re-implemented
+- `feedback_meander_resource_costs` — Chapel builds slow; cache Chapel artefacts in CI, clean after
+- `feedback_rust_means_rust_spark` — Rust side admits SPARK/Ada; Chapel doesn't change that
+- `feedback_verisimdb_policy` — Chapel-dispatched runs still emit VeriSimDB records (via Cap'n Proto
+  back-channel to Rust)
+- `feedback_full_battery_before_claims` — before claiming speedup, full battery: tests + benches +
+  panic-attack + causality + verifiable I/O
+
+## Key files to read first
+
+1. `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
+2. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/chapel_poc/parallel_proof_search.chpl` (420-LoC POC to promote)
+3. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/zig_ffi/chapel_bridge.zig` (existing Zig FFI stub)
+4. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/rust/dispatch.rs` (integration target)
+5. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/.github/workflows/chapel-ci.yml` (current Chapel CI for compile-only)
+6. `schemas/echidna.capnp` (must exist from L1 — if not, L1 isn't done)

docs/handover/L3-LIVE-PROVER-CI-PROMPT.md

@@ -0,0 +1,90 @@
+# Echidna L3 — Live-Prover CI — Continuation Prompt
+
+**Context**: Echidna (`/var/mnt/eclipse/repos/verification-ecosystem/echidna/`) has 48 trait-wired
+prover backends, but CI only tests them with `MockProver`. Mission: make every provisionable
+backend run against a canonical micro-goal on a predictable cadence. Guix primary, Nix fallback.
+
+**Master plan**: `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
+**Order**: L3 (this) → L1 (Cap'n Proto) → L2 (Chapel max).
+
+---
+
+## Where L3 is when this prompt fires
+
+Wave-1 (Tier-1, every PR — 9 backends) DONE in kickoff session, commit `b022bf4`:
+- `manifests/live-provers.scm` — Guix manifest with Tier-1 + Tier-2 provers
+- `flake.nix` — expanded with matching `liveProverDeps`
+- `.github/workflows/live-provers.yml` — tiered workflow (Tier-1 PR, Tier-2 nightly, etc.)
+- `tests/live_prover_suite.rs` — Rust test harness with Tier-1 version-check tests
+
+Wave-2 (Tier-2, nightly — 10 backends) **DONE 2026-04-19** in commits `9a4aeeb` + `6717b12`:
+- Real provisioning commands for coq, agda, why3 (apt); idris2 (source bootstrap
+  against Chez Scheme); lean4 (elan); isabelle (Isabelle2024 tarball); dafny
+  (`dotnet tool install --global Dafny`); fstar (GitHub release tarball, binary
+  `fstar.exe`); tlaps (self-extracting installer for `tlapm`).
+- `hol-light` **deferred** to Wave-3 container path — no prebuilt binary and opam
+  build is ~20 min + camlp5.
+- `tests/live_prover_suite.rs` extended with `live_fstar_version` + `live_tlaps_version`.
+- Local verification (not CI yet): 18/18 tests pass, 13 backends return real versions,
+  5 auto-skip when binaries are absent.
+
+`tests/live_goals/` was listed in the handover-artefacts but not actually created.
+Wave-2 version-check tests do not need it; Wave-2 / Wave-3 goal-check extensions will.
+
+## What to finish in L3 (remaining)
+
+### Wave-2 verification in CI (not just local)
+The Wave-2 provisioning installers are not yet exercised by a real CI run —
+nightly needs to fire (cron `0 3 * * *`) to surface any CI-specific breakage
+(apt mirror changes, GitHub release URL format drift, dotnet sdk availability,
+etc.). Watch the next nightly after merge; fix any red matrix cells in-place.
+
+### Wave-3: Tier-3 backends (Weekly)
+Container/special-env path: Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath.
+These likely need per-backend Containerfiles (Podman, not Docker — per project CLAUDE.md).
+
+### Wave-4: Tier-4 backends (Quarterly, allow-fail)
+Best-effort: Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL, ViPER, NuSMV, Spin,
+TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy. Many will stay mock-only (document why).
+
+### Harden wiring depth for shallow backends
+Audit flagged **Dafny (165 LoC)** as stub-ish — upgrade to deep during L3 so the live test isn't
+measuring a broken subprocess wrapper.
+
+### VeriSimDB integration
+Per `feedback_verisimdb_policy`: the live-prover harness should emit a VeriSimDB record per run
+(prover, goal, outcome, duration, exit code). Schema TBD — coordinate with VeriSimDB repo.
+
+## Acceptance for L3 complete
+
+- Tier-1 green on every PR
+- Tier-2 green on nightly (or documented flaky backends with `continue-on-error: true`)
+- Tier-3 runs weekly with per-backend allow-fail
+- Tier-4 runs quarterly, results archived
+- Dafny upgraded from 165 LoC stub to deep subprocess wiring
+- `guix shell -m manifests/live-provers.scm -- just test-live` works locally
+- VeriSimDB records emitted (if schema ready)
+- Mock tests retained as fast pre-CI smoke
+
+## Hand to L1 when
+
+- All four waves land or are explicitly deferred with rationale in STATE.a2ml
+- Tier-1 has run green on main for ≥7 days
+
+---
+
+## Rules active in this session
+
+- GitHub-only mirroring (per memory `feedback_github_only_mirroring`)
+- Commit ASAP, specific paths (`feedback_commit_asap`)
+- Pre-commit: `panic-attack assail` (`feedback_panic_attack_precommit`)
+- No `.unwrap() → .expect("TODO")` refactor (`feedback_unwrap_to_expect_antipattern`)
+- Session close marker: `SAFE TO CLOSE` literal at end of final message
+
+## Key files to read first
+
+1. `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
+2. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/.machine_readable/6a2/STATE.a2ml`
+3. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/manifests/live-provers.scm`
+4. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/.github/workflows/live-provers.yml`
+5. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/tests/live_prover_suite.rs`