feat(coprocessor): Phase 6B — Dsp + Io + Graphics + Audio + Fpga backends

Completes the coprocessor kind ladder begun in Phase 0 + 6A.  All 11
CoprocessorKind variants (Math, Vector, Tensor, Crypto, Physics,
FlintMath, Dsp, Io, Graphics, Audio, Fpga) now have full Rust impls
with no stubs.

Dsp (src/rust/coprocessor/dsp.rs):
- 4 ops: DspFft, DspIfft, DspHannWindow, DspHammingWindow.
- Backed by rustfft 6 (Apache-2.0 / MIT).  FFT input/output uses
  FloatVec with re/im interleaved (avoids inventing a Complex outcome
  variant).  IFFT scales by 1/N for round-trip identity — verified to
  1e-9 over a sine-wave test.  Length checks classify odd-length
  spectra as Failure.  Tier 3 (LibraryWrapped).

Io (src/rust/coprocessor/io.rs):
- 3 ops: IoReadAll (16 MiB cap, returns Hex), IoLineCount (BigInt),
  IoSha256OfFile (streams 64 KiB chunks, returns Hex).  Async via
  tokio::fs.  Missing files return Empty; permission errors return
  Failure with diagnostic.  RFC SHA-256("abc") test vector green.
  Tier 3.

Graphics (src/rust/coprocessor/graphics.rs):
- 2 ops: GraphicsProofGraphSvg (depth-aware vertical-waterfall layout
  with edges + rounded-rect nodes), GraphicsBarChartSvg (normalised
  heights, escaped labels).  Pure Rust, no GPU dependency, no svg
  crate — emits SVG strings directly and Hex-wraps for wire safety.
  XML escape verified against `<dangerous & "chars">` input.  Tier 3.

Audio (src/rust/coprocessor/audio.rs):
- 2 ops: AudioSineWave (frequency + duration + sample_rate → WAV bytes,
  Nyquist-checked, sample_rate range [8 kHz, 192 kHz]),
  AudioCompletionChime (pre-baked C5/E5/G5 100 ms each).  Pure Rust
  PCM-16 + RIFF packing — no audio library dep.  RIFF/WAVE/fmt /data
  chunk magic numbers verified.  Tier 3.

Fpga (src/rust/coprocessor/fpga.rs):
- 1 op: FpgaYosysSynth — subprocess to `yosys -p "synth -top X; write_verilog"`.
  Health flips Unhealthy at construction if yosys not on PATH so the
  MetaController can route around.  top_module name validated against
  shell-injection (alphanum + underscore, no leading digit).  Tier 1
  (ExternalSubprocess) — yosys is a witness oracle, not certifying.

Wiring:
- CoprocessorKind: + Dsp, Io, Graphics, Audio, Fpga.  CoprocessorFactory
  ::native dispatches all five.  julia_bridge kind_name covers all
  eleven kinds.
- src/abi/CoprocessorForeign.idr: + 6 kind discriminants (5..10),
  extended kindEncodeDecodeId proof — case analysis still discharges
  every variant constructively.  Zero believe_me.
- Cargo.toml: + rustfft 6.

Also: `tptp_output.rs` was orphan-tracked in cbd9449 (used by 4 HO-ATPs
but missing from the commit) — fixed in 1ad49f8 alongside this work.

Tests: 54 coprocessor tests green (10 Math + 6 Vector + 6 Tensor + 6
Crypto + 4 Physics + 1 factory + 5 Dsp + 4 Io + 4 Graphics + 4 Audio
+ 4 Fpga).  panic-attack assail clean on all five new files (the
Graphics 1 "weak point" is allocation-counting noise, not a defect).

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -79,10 +79,10 @@ notes = "4 new CoprocessorKind variants (Vector / Tensor / Crypto / Physics) wit
 [[expansion-roadmap.phase]]
 id = "phase-6b"
 title = "Coprocessor wiring — DSP + IO + Graphics + Audio + FPGA"
-status = "available-for-claim"
+status = "complete"
+landed = "2026-04-26"
 adds-backends = []
-target-claim-id = "echidna-phase6b-coproc-rest"
-notes = "Each kind lands with full implementation. DSP: rustfft (FFT/IFFT/window). IO: tokio::fs (read/write/line-count). Graphics: SVG ProofGraph render (no GPU dep). Audio: pure Rust sine-wave / completion chime. FPGA: subprocess to yosys (synth flow). Tier 3 for native; Tier 1 for FPGA subprocess."
+notes = "5 new CoprocessorKind variants (Dsp/Io/Graphics/Audio/Fpga) with full Rust impls. New deps: rustfft 6 (Apache-2.0/MIT) for DSP. Dsp: 4 ops (FFT/IFFT/Hann/Hamming) — FFT round-trip identity verified to 1e-9. Io: 3 ops (ReadAll/LineCount/Sha256OfFile) — RFC SHA-256 vector green, 16 MiB read cap. Graphics: 2 ops (ProofGraphSvg/BarChartSvg) — depth-aware DAG layout, XML escape verified. Audio: 2 ops (SineWave/CompletionChime) — RIFF header validated, Nyquist enforced, three-note C5/E5/G5 chime. Fpga: 1 op (YosysSynth) Tier 1 — health flips Unhealthy when yosys absent, top_module name validated against shell injection. Idris2 ABI extended with 6 new kind discriminants (5..10) and constructive round-trip proof. 21 new tests (54 total coprocessor)."
 
 [[expansion-roadmap.phase]]
 id = "phase-7"

Cargo.lock

@@ -94,6 +94,9 @@ sha2 = "0.10"
 # Ed25519 signature verification (Apache-2.0 / MIT, MPL-2.0 compat).
 ed25519-dalek = { version = "2", default-features = false, features = ["std"] }
 
+# DSP coprocessor — FFT/IFFT (Apache-2.0 / MIT).
+rustfft = "6"
+
 # TypedWasm engine — standalone crate at crates/typed_wasm.
 # Provides the pure parse/analyse engine; provers/typed_wasm.rs is a thin
 # adapter that maps its `Analysis` onto echidna core types, and routes the

Cargo.toml

@@ -87,47 +87,71 @@ encodeDecodeId PureFormal         = Refl
 --------------------------------------------------------------------------------
 
 ||| The kind of a coprocessor backend.  Only variants with a fully
-||| functional Rust + Idris2 implementation appear here.  Phase 6A adds
-||| Vector / Tensor / Crypto / Physics; Phase 6B will add Dsp / Fpga /
-||| Graphics / Audio / Io alongside their implementations.
+||| functional Rust + Idris2 implementation appear here.  Phase 6A added
+||| Vector / Tensor / Crypto / Physics; Phase 6B adds Dsp / Io / Graphics /
+||| Audio / Fpga.  FlintMath (Phase 2A) is feature-gated in Rust but the
+||| ABI surface is unconditional.
 public export
 data CoprocessorKind : Type where
-  Math    : CoprocessorKind  -- Phase 0  (num-bigint + num-integer)
-  Vector  : CoprocessorKind  -- Phase 6A (auto-vectorised f64 loops)
-  Tensor  : CoprocessorKind  -- Phase 6A (nalgebra dense linalg)
-  Crypto  : CoprocessorKind  -- Phase 6A (sha2 + blake3 + ed25519-dalek)
-  Physics : CoprocessorKind  -- Phase 6A (RK4 + harmonic energy oracles)
-
-||| Encoding to u8 — pinned for FFI stability.
+  Math      : CoprocessorKind  -- Phase 0  (num-bigint + num-integer)
+  Vector    : CoprocessorKind  -- Phase 6A (auto-vectorised f64 loops)
+  Tensor    : CoprocessorKind  -- Phase 6A (nalgebra dense linalg)
+  Crypto    : CoprocessorKind  -- Phase 6A (sha2 + blake3 + ed25519-dalek)
+  Physics   : CoprocessorKind  -- Phase 6A (RK4 + harmonic energy oracles)
+  FlintMath : CoprocessorKind  -- Phase 2A (FLINT C library FFI, --features flint)
+  Dsp       : CoprocessorKind  -- Phase 6B (rustfft FFT/IFFT + windows)
+  Io        : CoprocessorKind  -- Phase 6B (tokio::fs file ops)
+  Graphics  : CoprocessorKind  -- Phase 6B (SVG rendering, no GPU)
+  Audio     : CoprocessorKind  -- Phase 6B (PCM/WAV synthesis)
+  Fpga      : CoprocessorKind  -- Phase 6B (yosys subprocess, Tier 1)
+
+||| Encoding to u8 — pinned for FFI stability.  Reordering is an ABI break.
 public export
 coprocessorKindToU8 : CoprocessorKind -> Bits8
-coprocessorKindToU8 Math    = 0
-coprocessorKindToU8 Vector  = 1
-coprocessorKindToU8 Tensor  = 2
-coprocessorKindToU8 Crypto  = 3
-coprocessorKindToU8 Physics = 4
+coprocessorKindToU8 Math      = 0
+coprocessorKindToU8 Vector    = 1
+coprocessorKindToU8 Tensor    = 2
+coprocessorKindToU8 Crypto    = 3
+coprocessorKindToU8 Physics   = 4
+coprocessorKindToU8 FlintMath = 5
+coprocessorKindToU8 Dsp       = 6
+coprocessorKindToU8 Io        = 7
+coprocessorKindToU8 Graphics  = 8
+coprocessorKindToU8 Audio     = 9
+coprocessorKindToU8 Fpga      = 10
 
 public export
 coprocessorKindFromU8 : Bits8 -> Maybe CoprocessorKind
-coprocessorKindFromU8 0 = Just Math
-coprocessorKindFromU8 1 = Just Vector
-coprocessorKindFromU8 2 = Just Tensor
-coprocessorKindFromU8 3 = Just Crypto
-coprocessorKindFromU8 4 = Just Physics
-coprocessorKindFromU8 _ = Nothing
+coprocessorKindFromU8 0  = Just Math
+coprocessorKindFromU8 1  = Just Vector
+coprocessorKindFromU8 2  = Just Tensor
+coprocessorKindFromU8 3  = Just Crypto
+coprocessorKindFromU8 4  = Just Physics
+coprocessorKindFromU8 5  = Just FlintMath
+coprocessorKindFromU8 6  = Just Dsp
+coprocessorKindFromU8 7  = Just Io
+coprocessorKindFromU8 8  = Just Graphics
+coprocessorKindFromU8 9  = Just Audio
+coprocessorKindFromU8 10 = Just Fpga
+coprocessorKindFromU8 _  = Nothing
 
 ||| Round-trip on the kind discriminant.  Constructive — case-analysis
-||| discharges every variant.  Together with `coprocessorKindFromU8` this
-||| guarantees the kind ABI is well-formed end-to-end.
+||| discharges every variant.  Zero believe_me.
 public export
 kindEncodeDecodeId :
   (k : CoprocessorKind) ->
   coprocessorKindFromU8 (coprocessorKindToU8 k) = Just k
-kindEncodeDecodeId Math    = Refl
-kindEncodeDecodeId Vector  = Refl
-kindEncodeDecodeId Tensor  = Refl
-kindEncodeDecodeId Crypto  = Refl
-kindEncodeDecodeId Physics = Refl
+kindEncodeDecodeId Math      = Refl
+kindEncodeDecodeId Vector    = Refl
+kindEncodeDecodeId Tensor    = Refl
+kindEncodeDecodeId Crypto    = Refl
+kindEncodeDecodeId Physics   = Refl
+kindEncodeDecodeId FlintMath = Refl
+kindEncodeDecodeId Dsp       = Refl
+kindEncodeDecodeId Io        = Refl
+kindEncodeDecodeId Graphics  = Refl
+kindEncodeDecodeId Audio     = Refl
+kindEncodeDecodeId Fpga      = Refl
 
 --------------------------------------------------------------------------------
 -- Health
@@ -172,8 +196,14 @@ healthFromU8 _ = Unhealthy
 ||| Unhealthy.  Currently a placeholder until libechidna_coprocessor lands.
 public export
 coprocessorHealthOf : CoprocessorKind -> CoprocessorHealth
-coprocessorHealthOf Math    = Healthy
-coprocessorHealthOf Vector  = Healthy
-coprocessorHealthOf Tensor  = Healthy
-coprocessorHealthOf Crypto  = Healthy
-coprocessorHealthOf Physics = Healthy
+coprocessorHealthOf Math      = Healthy
+coprocessorHealthOf Vector    = Healthy
+coprocessorHealthOf Tensor    = Healthy
+coprocessorHealthOf Crypto    = Healthy
+coprocessorHealthOf Physics   = Healthy
+coprocessorHealthOf FlintMath = Healthy
+coprocessorHealthOf Dsp       = Healthy
+coprocessorHealthOf Io        = Healthy
+coprocessorHealthOf Graphics  = Healthy
+coprocessorHealthOf Audio     = Healthy
+coprocessorHealthOf Fpga      = Unhealthy  -- subprocess; runtime probe required