feat(ffi): wire real BLAKE3 combiner — build+link libochrance.so, drop dead stubs

[hyperpolymath]

Summary

Closes the cryptographic-integrity gap (CLAUDE.md rule 4): the production verification path now computes real BLAKE3 through libochrance.so, verified end-to-end at runtime — not stubbed, not aspirational.

The root cause was a real, silent bug: build.zig named the shared library ochrance-shared → libochrance-shared.so, but the Idris bindings declare %foreign "C:blake3_hash,libochrance", so the runtime loader looks for libochrance.so. That file was never produced — the FFI could never have loaded at runtime.

Changes

Build/link

• ffi/zig/build.zig: name the shared library ochrance so it emits libochrance.so (the soname the %foreign loader resolves). Static libochrance.a and shared libochrance.so coexist (distinct extensions).

Runtime tests — the contract Idris2's FFI loader actually depends on

• ffi/zig/test/link_test.c + run_link_test.sh: dlopen libochrance.so and call each exported symbol against published KAT vectors (BLAKE3 / SHA-256 / SHA3-256), plus discriminators proving the Merkle combiner is order-sensitive with no XOR self-cancellation — i.e. real BLAKE3, not the XOR stub. Wired into zig-ffi.yml CI (uses cc, already present on the runner).
• tests/ffi/CryptoFFITest.idr: an Idris executable that drives blake3 / sha256 / sha3_256 / rootHashBytesIO across %foreign and checks the production Merkle root equals BLAKE3(leafA ++ leafB) and differs from the XOR spec root. (Local/maintainer recipe just test-ffi-idris; not CI-gated, since CI has no Idris2.)

Idris cleanup

• FFI/Crypto.idr: remove the dead zero/false stubs blake3Stub, sha256Stub, sha3_256Stub, ed25519VerifyStub (superseded by the real FFI functions; were referenced only in docs).
• Rename hashPairStub → xorCombiner across Crypto/Merkle/PropertyTests. It is the totality-friendly pure spec instance of the combiner-generic theorems, not a crypto fallback — a pure BLAKE3 combiner is impossible (BLAKE3 only crosses the FFI boundary in IO). Security rests on the explicit, isolated CollisionResistant assumption (pigeonhole-false; MerkleAssumption).

Docs/state: CLAUDE.md, EXPLAINME.adoc, VALENCE_SHELL_BRIDGE.adoc, STATE.a2ml, debt.a2ml updated to reflect the closed gap honestly (Merkle roots are cryptographic commitments given a collision-resistant BLAKE3 — the standard, clearly-stated trust root).

Verification (run locally — idris2 0.8.0 built from source + zig 0.11.0)

Check	Result
Core proof corpus idris2 --build ochrance.ipkg (--total)	29/29, axiom-free
Property tests	47/47
A2ML + integration suites	green (integration 55/55)
zig build test (Zig KAT + Ed25519 round-trip)	pass
C dlopen link test	10/10
Idris→FFI runtime test (real BLAKE3 via libochrance.so)	6/6
e2e_test.sh (grep guards incl. soname regression)	27/27

What this does not claim

Collision resistance remains the single, irreducible, explicit assumption (CollisionResistant, pigeonhole-false, isolated in MerkleAssumption) — supplied at the verification boundary, never proved. Full Ed25519 attestation still needs a key-management / trust-root layer (the signature primitive is real and linked; the pure validateManifest path skips signatures by construction).

🤖 Generated with Claude Code

---

Generated by Claude Code