Commit 9af87ba
feat(coprocessor): Phase 6A — Vector + Tensor + Crypto + Physics backends
Adds 4 native Rust coprocessor backends under the Phase 0 abstraction.
Each backend is fully implemented with no stubs; CoprocessorKind only
grows when a working impl lands.
Vector (src/rust/coprocessor/vector.rs):
- 4 ops: VectorAdd, VectorDot, VectorNorm, VectorScale.
- Pure Rust auto-vectorisable f64 loops; std::simd avoided to keep us
off nightly. Length mismatches return CoprocessorOutcome::Failure
rather than panicking. Trust tier: LibraryWrapped (Tier 3).
- Backs the GNN inference path's batch arithmetic and aggregate
reasoning over node-embedding vectors.
Tensor (src/rust/coprocessor/tensor.rs):
- 4 ops: TensorMatMul, TensorTranspose, TensorTrace, TensorDeterminant.
- nalgebra DMatrix for dense linalg. Ragged input + non-square +
dimension-mismatch each classified as Failure with diagnostic.
- Backs node-embedding aggregation, Pareto-frontier dominance, and
matrix kernels in cross-prover proof-certificate exchange.
Crypto (src/rust/coprocessor/crypto.rs):
- 3 ops: CryptoSha256, CryptoBlake3, CryptoEd25519Verify.
- Backed by RustCrypto sha2 + the existing blake3 dep + ed25519-dalek.
Ed25519 keys/sigs strictly bounds-checked (32 / 64 bytes) per RFC
8032. RFC 8032 §7.1 test vector 1 passes; tamper detection passes.
- Pairs with the symbolic-crypto provers (Tamarin, ProVerif) and the
future computational-crypto backends (EasyCrypt, CryptoVerif) as
the concrete byte-level oracle for symbolic claims.
Physics (src/rust/coprocessor/physics.rs):
- 2 ops: PhysicsRk4Step (closed kernel set: harmonic-oscillator,
exponential-decay, linear), PhysicsHarmonicEnergy.
- Pure Rust RK4 integrator. ω=1 harmonic oscillator integrated for
2π over dt=0.001 (6283 steps) returns to start within 1e-3. Half-
life decay ẋ = -λx with λ = ln 2 closes within 1e-6. Closures don't
cross the Serde wire — kernels are name+params, encoded by build_kernel.
- Pairs with the future KeYmaera X backend as the numerical sanity-
check oracle for symbolically-proven hybrid-system trajectories.
Wiring:
- CoprocessorKind: + Vector, Tensor, Crypto, Physics. CoprocessorFactory
::native dispatches all four. CoprocessorOutcome: + Float, FloatVec,
FloatMatrix, Hex variants. Math backend gets a catch-all Failure arm
for ops it doesn't own — same pattern propagated to all backends.
- Cargo.toml: + nalgebra 0.33 (BSD-3), ed25519-dalek 2 (Apache-2.0/MIT).
sha2 un-gated from the `verisim` feature (it's now a Crypto-backend
hard dep).
- src/abi/CoprocessorForeign.idr: + 4 kind variants with pinned u8
discriminants (Math=0, Vector=1, Tensor=2, Crypto=3, Physics=4) and
a constructive `kindEncodeDecodeId` proof for the round-trip. Health
table extended. Zero believe_me.
- src/rust/coprocessor/julia_bridge.rs: kind_name covers the new kinds.
- STATE.a2ml [expansion-roadmap]: Phase 6A marked complete; Phase 6B
(DSP + IO + Graphics + Audio + FPGA) split out as next claimable.
Tests: 32 coprocessor tests green (10 Math + 6 Vector + 6 Tensor + 6
Crypto + 4 Physics). panic-attack assail clean on all four new files
(0 weak points). Validation done with parallel Phase 1 prover work-in-
progress git-stashed so the lib could compile in isolation; restored
afterwards.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>1 parent 41b26b9 commit 9af87ba
12 files changed
Lines changed: 1357 additions & 16 deletions
File tree
- .machine_readable/6a2
- src
- abi
- rust/coprocessor
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
68 | 68 | | |
69 | 69 | | |
70 | 70 | | |
71 | | - | |
72 | | - | |
73 | | - | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
74 | 82 | | |
75 | | - | |
| 83 | + | |
| 84 | + | |
76 | 85 | | |
77 | 86 | | |
78 | 87 | | |
| |||
0 commit comments