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

.github/workflows/zig-ffi.yml

@@ -36,3 +36,6 @@ jobs:
       - name: Test (hash known-answer vectors + Ed25519 round-trip)
         working-directory: ffi/zig
         run: zig build test
+      - name: Runtime link test (C ABI via dlopen — the contract Idris2's FFI uses)
+        working-directory: ffi/zig
+        run: bash test/run_link_test.sh

.machine_readable/6a2/STATE.a2ml

@@ -7,12 +7,12 @@ project = "ochrance"
 version = "0.1.0"
 last-updated = "2026-06-18"
 status = "active"
-session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring + live root-verify soundness; Stage 3.1 pure repair + 3.2 repair⇒verify)"
+session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring + live root-verify soundness; Stage 3.1 pure repair + 3.2 repair⇒verify; crypto FFI wired: libochrance.so built+linked, runtime KAT + Idris→FFI tests)"
 
 [project-context]
 name = "Ochránce"
 purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration."""
-completion-percentage = 66
+completion-percentage = 68
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
@@ -52,7 +52,6 @@ milestones = [
 
 [blockers-and-issues]
 issues = [
-  "No cryptographic-integrity claim yet: Idris stub fallbacks (hashPairStub / blake3Stub / ed25519VerifyStub in FFI/Crypto.idr) remain in the verification flow; libochrance.so not yet built + linked in",
   "Repair (L3) idempotence is property-tested only, not yet proven",
   "ECHIDNA FFI is stubbed (echidnaProve returns 'FFI not yet implemented')",
   "Production round-trip (parse∘lex∘serialize) is honestly bounded by primitive String ops — see docs/PROOFS.adoc",
@@ -66,10 +65,10 @@ actions = [
   "Stage 3.2 DONE — whole-manifest repair ⇒ verify (repairThenVerify, module RepairVerify). repairRefsPure folds repairBlockPure; proof = verifyRefsComplete ∘ repairRefsConsistent; GoodRefs precondition + hashRefl hypothesis, both named",
   "Live-verifier Merkle redesign SOUNDNESS DONE (merkleRootVerifyHashSound) — root-comparing verifier is sound at the Hash level, modulo named CollisionResistant + DecodeInjective",
   "Live-verifier PLUMBING DONE (module VerifyRoot) — padToLength/nextPow2Exp/layoutLeaves pad to power-of-2 leaf Vect; verifyByRoot/verifyByRootHash build tree + compare roots; fsBlockHashes/verifySnapshotRoot = runtime path vs FSSnapshot.rootHash. Executable, total; accept-on-match soundness = merkleRootVerifyHashSound",
-  "Stage 4 DONE (honest isolation) — CollisionResistant cannot be discharged (pigeonhole-false for compressing combiner); isolated as the irreducible crypto assumption + proved it has teeth (constNotCollisionResistant, module MerkleAssumption). Optional follow-on: wire real Zig/FFI combiner + declare CR as its explicit assumption",
+  "Stage 4 DONE (honest isolation) — CollisionResistant cannot be discharged (pigeonhole-false for compressing combiner); isolated as the irreducible crypto assumption + proved it has teeth (constNotCollisionResistant, module MerkleAssumption). Follow-on DONE: real Zig/BLAKE3 combiner wired via libochrance.so (production rootHashBytesIO/hashPairBlake3); CR remains its explicit, supplied-at-boundary assumption",
   "Stage 2.4 DONE — verify↔Merkle proof-level wiring (rootFaithful/rootVerifySound): the root is a faithful fingerprint of the blocks (binding). REMAINING: connect to the live Hash-based verifyRefsHelper via hex Hash<->HashBytes conversion (2.3-bounded) + power-of-two layout (verify-path change, not a proof)",
   "Stage 3.2 (next provable): whole-manifest repairPure ⇒ verifyRefsHelper accepts (distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)",
-  "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)",
+  "DONE — crypto FFI wired: build.zig emits libochrance.so (correct soname); production Idris path (blake3/sha256/sha3_256/hashPairBlake3/rootHashBytesIO/ed25519Verify) calls it via %foreign; dead stubs (blake3Stub/sha256Stub/sha3_256Stub/ed25519VerifyStub) removed; pure XOR combiner renamed xorCombiner (spec instance). Verified: zig build test, C dlopen link test (KAT, CI-gated in zig-ffi.yml), Idris→FFI runtime test tests/ffi/CryptoFFITest.idr (prod Merkle root = BLAKE3 fold ≠ XOR). Residual: CollisionResistant assumption (isolated)",
   "Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access",
 ]
 
@@ -90,4 +89,4 @@ decisions = [
 [maintenance-status]
 last-run-utc = "2026-06-05T14:08:00Z"
 last-result = "pass"  # unknown | pass | warn | fail
-notes = "CI green on main; core builds fully total. A2ML parser 16/16, property 47/47, e2e 22/22; integration suite and Zig FFI build+test green."
+notes = "CI green on main; core builds fully total (idris2 0.8.0, 29/29 modules, --total). A2ML parser 16/16, property 47/47, e2e 22/22; Zig FFI build+test green; C dlopen link test 10/10; Idris→FFI runtime test 6/6 (real BLAKE3 via libochrance.so)."

.machine_readable/agent_instructions/debt.a2ml

@@ -15,13 +15,6 @@ last-updated = "2026-06-05"
 # SHOULD — would fix next wave
 # ============================================================================
 
-[[debt.should]]
-component = "ochrance-core/Ochrance/FFI/Crypto.idr"
-issue = "Idris stub fallbacks (hashPairStub / blake3Stub / ed25519VerifyStub) remain in the verification flow and libochrance.so is not yet built+linked — so no cryptographic-integrity claim can be made (CLAUDE.md rule 4)."
-effort = "hard"
-impact = "high"
-discovered = "2026-06-05"
-
 [[debt.should]]
 component = "ochrance-core/Ochrance/Filesystem/Repair.idr"
 issue = "Repair idempotence is property-tested only, not proven (proof campaign Stage 3)."

CLAUDE.md

@@ -51,7 +51,7 @@ idris2 --repl ochrance.ipkg
 1. **All functions must be total** - use `%default total` in every module
 2. **Structural recursion only** - no partial or assert_total
 3. **Idris2 0.8.0+** required
-4. **BLAKE3/SHA-256 via FFI** - real crypto is implemented in the Zig FFI (`ffi/zig/src/main.zig`: BLAKE3/SHA-256/SHA3-256/Ed25519 via `std.crypto`, with known-answer-vector tests). Still pending before any cryptographic-integrity claim: remove the Idris-side stub fallbacks (`hashPairStub`/`blake3Stub`/`ed25519VerifyStub` in `FFI/Crypto.idr`) and build+link `libochrance.so` into the verification flow.
+4. **BLAKE3/SHA-256 via FFI** - real crypto is implemented in the Zig FFI (`ffi/zig/src/main.zig`: BLAKE3/SHA-256/SHA3-256/Ed25519 via `std.crypto`, with known-answer-vector tests) and wired into the Idris production path (`blake3`/`sha256`/`sha3_256`/`hashPairBlake3`/`rootHashBytesIO`/`ed25519Verify`) via `%foreign "C:...,libochrance"`. `build.zig` emits `libochrance.so` with the correct soname; the runtime C-ABI contract is CI-gated by a dlopen link test (`ffi/zig/test/link_test.c`, KAT vectors), and `tests/ffi/CryptoFFITest.idr` confirms the production Merkle root is the real BLAKE3 fold (≠ the XOR root). The dead stub fallbacks (`blake3Stub`/`sha256Stub`/`sha3_256Stub`/`ed25519VerifyStub`) are removed; the pure XOR combiner is renamed `xorCombiner` — the totality-friendly *spec instance* of the combiner-generic theorems, not a fallback. The one irreducible crypto assumption is `CollisionResistant` (pigeonhole-false, isolated in `Filesystem.MerkleAssumption`).
 5. **Linear types for repair** - repair operations consume old state (Quantity 1)
 
 ## Error Taxonomy

EXPLAINME.adoc

@@ -68,7 +68,7 @@ Also integrates with ECHIDNA for neural proof synthesis — FFI calls to libechi
 
 == Known Limitations & TODOs
 
-* **Hashes**: BLAKE3/SHA-256/SHA3-256 are now implemented in the Zig FFI (`ffi/zig/src/main.zig`, tested via `zig build test`). Remaining: remove the Idris-side XOR/zero stub fallbacks (`hashPairStub`/`blake3Stub`) and build+link `libochrance.so` into the verification flow before claiming cryptographic integrity.
+* **Hashes**: BLAKE3/SHA-256/SHA3-256 are implemented in the Zig FFI (`ffi/zig/src/main.zig`, tested via `zig build test`) and wired into the Idris production path through `%foreign`. `build.zig` emits `libochrance.so`; a C `dlopen` link test (`ffi/zig/test/link_test.c`, KAT vectors, CI-gated in `zig-ffi.yml`) and an Idris→FFI runtime test (`tests/ffi/CryptoFFITest.idr`) confirm real BLAKE3 end to end — the production Merkle root is the BLAKE3 fold, not the XOR root. The dead zero-hash stubs are removed; the pure XOR combiner is renamed `xorCombiner` (the spec instance of the combiner-generic proofs). Residual assumption: `CollisionResistant` (isolated, pigeonhole-false).
 * **Attestation**: Ed25519 verification is implemented (Zig FFI + `validateManifestIO`). Remaining: a trust-root / key-management story and end-to-end integration before claiming full attestation.
 * **Linear repair**: Idris2 linear types framework incomplete for full use-after-repair prevention (ongoing research).
 

Justfile

@@ -32,6 +32,11 @@ build-abi:
 build-ffi:
     cd ffi/zig && zig build
 
+# Build libochrance.so + run the C-ABI runtime link test (KAT vectors via dlopen).
+# This is the runtime contract Idris2's %foreign loader depends on.
+test-ffi-link:
+    bash ffi/zig/test/run_link_test.sh
+
 # Build all components
 build: build-core build-abi build-ffi
 

docs/VALENCE_SHELL_BRIDGE.adoc

@@ -159,24 +159,33 @@ Ochránce is the receipt substrate, but its integrity guarantees are still
 under construction. The following caveats are load-bearing and must be carried
 into any future receipt before it is trusted.
 
-. *No cryptographic filesystem-integrity claim while placeholder hashes remain
-  reachable.* The Zig FFI now implements real primitives — BLAKE3, SHA-256,
+. *Cryptographic filesystem-integrity now rests on real hashing, modulo one
+  named assumption.* The Zig FFI implements real primitives — BLAKE3, SHA-256,
   SHA3-256 and Ed25519 verification via Zig's audited `std.crypto`
-  (`ffi/zig/src/main.zig`) — and the Idris bindings in
-  `ochrance-core/Ochrance/FFI/Crypto.idr` (plus `Merkle.idr`'s `hashPairBlake3`)
-  call them. **But the integrity story is not yet closed:** XOR/zero-hash stub
-  fallbacks (`hashPairStub`, `blake3Stub`, …) still live in the Idris tree, the
-  cryptographic path still depends on `libochrance.so` being built and linked
-  into the verification flow, and the roadmap still lists the Merkle BLAKE3
-  wiring as incomplete. Until the stub paths are removed and the FFI path is the
-  only one, Merkle roots are *structural* commitments, not cryptographic ones.
-
-. *No full-attestation claim until signature verification is integrated.*
-  `ed25519Verify` and `validateManifestIO` exist and can check an Ed25519
-  attestation, but an `ed25519VerifyStub` remains, the pure `validateManifest`
-  path skips signatures entirely, there is no key-management / trust-root
-  story, and the whole path again depends on `libochrance.so`. "Attested"
-  mode is defined; it is not yet an end-to-end trustworthy attestation.
+  (`ffi/zig/src/main.zig`) — and the Idris production path
+  (`ochrance-core/Ochrance/FFI/Crypto.idr` + `Merkle.idr`'s `hashPairBlake3` /
+  `rootHashBytesIO`) calls them through `%foreign "C:...,libochrance"`.
+  `build.zig` emits `libochrance.so` with the correct soname; a C `dlopen` link
+  test (`ffi/zig/test/link_test.c`, KAT vectors, CI-gated) and an Idris→FFI
+  runtime test (`tests/ffi/CryptoFFITest.idr`) confirm the production Merkle root
+  is the real BLAKE3 fold, not the XOR root. The dead zero-hash stubs are gone;
+  the remaining pure XOR combiner is renamed `xorCombiner` — the totality-friendly
+  *spec instance* of the combiner-generic soundness/binding theorems, never a
+  production fallback. The one irreducible assumption is collision resistance,
+  modelled as the explicit, isolated `CollisionResistant` hypothesis
+  (pigeonhole-false, so never dischargeable — see `Filesystem.MerkleAssumption`),
+  supplied at the verification boundary. So Merkle roots are cryptographic
+  commitments *given* a collision-resistant BLAKE3 — the standard, clearly-stated
+  trust root.
+
+. *No full-attestation claim until key management is integrated.*
+  `ed25519Verify` (real Zig `std.crypto`, linked via `libochrance.so`) and
+  `validateManifestIO` can check an Ed25519 attestation, and the
+  `ed25519VerifyStub` has been removed. What remains for "Attested" mode is a
+  trust-root / key-management story (which keys are authorised, and how), plus
+  the fact that the *pure* `validateManifest` path skips signatures by
+  construction. The signature primitive is real and linked; end-to-end
+  trustworthy attestation still needs the key-management layer.
 
 . *No complete-linear-repair claim until that work is actually complete.*
   `Repair.idr` correctly types repair with linear quantities

ffi/zig/build.zig

@@ -23,9 +23,14 @@ pub fn build(b: *std.Build) void {
     b.installArtifact(lib);
 
     // Also create a shared library version (libochrance.so) — this is what the
-    // Idris2 FFI loads at runtime.
+    // Idris2 FFI loads at runtime. The name MUST be "ochrance" so the artifact is
+    // libochrance.so: the Idris bindings declare `%foreign "C:blake3_hash,
+    // libochrance"` (ochrance-core/Ochrance/FFI/Crypto.idr), so the runtime loader
+    // resolves the soname libochrance.so. Any other shared-library name would never
+    // be found. A static libochrance.a and a shared libochrance.so share the base
+    // name without clashing (distinct extensions).
     const shared_lib = b.addSharedLibrary(.{
-        .name = "ochrance-shared",
+        .name = "ochrance",
         .root_source_file = .{ .cwd_relative = "src/main.zig" },
         .target = target,
         .optimize = optimize,