Valence Shell / Echo Types bridge docs + implemented Zig crypto FFI

.claude/hooks/session-start.sh

@@ -0,0 +1,82 @@
+#!/bin/bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# SessionStart hook — provision the Ochránce toolchain for Claude Code on the web.
+#
+# The web container is ephemeral and cloned fresh, so the toolchains this repo
+# needs are reinstalled at session start:
+#   - Idris2  v0.8.0  (core framework, proofs, parser, verification)
+#   - Zig     0.11.0  (cryptographic FFI in ffi/zig)
+#   - just            (build/recipe runner; `just build`, `just check`, ...)
+#   - Agda    2.6.3   (estate formal-verification toolchain)
+#
+# Idempotent: each tool is skipped when already present, so cached containers
+# start fast. Best-effort: a failure in one tool is logged but does not abort
+# the hook (a partial toolchain beats a blocked session).
+#
+# Network-policy notes for the web environment (do not "fix" these away):
+#   - ziglang.org and api.github.com are BLOCKED; github.com and pypi.org are
+#     reachable. Zig therefore comes from the PyPI `ziglang` package (not
+#     ziglang.org), and Idris2 is built from GitHub source (not a prebuilt).
+#   - `apt-get update` fails (the distro index mirror is blocked) but
+#     `apt-get install` works off the image's cached package lists, so update
+#     is best-effort only.
+set -uo pipefail
+
+# Web-only: on a local machine, use your own toolchain.
+if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
+  exit 0
+fi
+
+log()  { printf '[session-start] %s\n' "$*" >&2; }
+have() { command -v "$1" >/dev/null 2>&1; }
+
+# --- apt packages: just, Agda, and the Idris2 build dependencies ------------
+if ! { have just && have agda && have idris2; }; then
+  log "installing apt packages (just, agda, Idris2 build deps) ..."
+  apt-get update >/dev/null 2>&1 || true
+  apt-get install -y --no-install-recommends \
+    just agda agda-stdlib chezscheme libgmp-dev make gcc git \
+    || log "WARN: some apt packages failed to install"
+fi
+
+# --- Zig 0.11.0 via the PyPI ziglang package (ziglang.org is blocked) -------
+if ! have zig; then
+  log "installing Zig 0.11.0 via PyPI ziglang ..."
+  if pip3 install --break-system-packages --quiet "ziglang==0.11.0"; then
+    cat > /usr/local/bin/zig <<'SH'
+#!/bin/sh
+# Thin shim exposing the PyPI `ziglang` package as a `zig` command.
+exec python3 -m ziglang "$@"
+SH
+    chmod +x /usr/local/bin/zig
+  else
+    log "WARN: Zig install failed"
+  fi
+fi
+
+# --- Idris2 v0.8.0, built from GitHub source (not in apt; no reachable bin) --
+# Cold build self-hosts the compiler and takes several minutes; cached
+# containers skip it. Needs chezscheme + libgmp-dev (installed above).
+if ! have idris2; then
+  log "building Idris2 v0.8.0 from source (several minutes on a cold container) ..."
+  src=/opt/Idris2-build
+  if rm -rf "$src" \
+     && git clone --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$src" \
+     && make -C "$src" bootstrap SCHEME=chezscheme PREFIX=/usr/local \
+     && make -C "$src" install PREFIX=/usr/local; then
+    log "Idris2 installed to /usr/local"
+  else
+    log "WARN: Idris2 build failed (see output above)"
+  fi
+fi
+
+# --- Report -----------------------------------------------------------------
+log "toolchain status:"
+have zig    && log "  zig    $(zig version 2>&1)"                || log "  zig    MISSING"
+have just   && log "  just   $(just --version 2>&1)"             || log "  just   MISSING"
+have agda   && log "  agda   $(agda --version 2>&1 | head -1)"   || log "  agda   MISSING"
+have idris2 && log "  idris2 $(idris2 --version 2>&1 | head -1)" || log "  idris2 MISSING"
+
+exit 0

.claude/settings.json

@@ -0,0 +1,14 @@
+{
+  "hooks": {
+    "SessionStart": [
+      {
+        "hooks": [
+          {
+            "type": "command",
+            "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
+          }
+        ]
+      }
+    ]
+  }
+}

.github/workflows/zig-ffi.yml

@@ -0,0 +1,29 @@
+# SPDX-License-Identifier: MPL-2.0
+# Build and test the Zig cryptographic FFI (ffi/zig).
+#
+# This is the only CI job that compiles the Zig FFI, so it is what actually
+# verifies the BLAKE3 / SHA-256 / SHA3-256 / Ed25519 implementations in
+# ffi/zig/src/main.zig (the grep-based E2E job only checks source strings).
+name: Zig FFI
+
+on: [push, pull_request]
+
+permissions:
+  contents: read
+
+jobs:
+  zig-ffi:
+    name: Zig FFI build + test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - name: Set up Zig 0.11.0
+        uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
+        with:
+          version: 0.11.0
+      - name: Build (libochrance.so + libochrance.a)
+        working-directory: ffi/zig
+        run: zig build
+      - name: Test (hash known-answer vectors + Ed25519 round-trip)
+        working-directory: ffi/zig
+        run: zig build test

.gitignore

@@ -81,6 +81,7 @@ htmlcov/
 # Zig
 **/zig-out/
 **/.zig-cache/
+**/zig-cache/
 
 # Shared libraries
 *.so

.machine_readable/integrations/valence-shell-bridge.a2ml

@@ -0,0 +1,101 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Ochrance <-> Valence Shell <-> Echo Types — cross-repo bridge note.
+# Machine-readable companion to docs/VALENCE_SHELL_BRIDGE.adoc.
+# This is an ORIENTATION note for agents. It records a documentation-only
+# bridge. Nothing here is mechanised, shipped, or trusted.
+
+[bridge]
+name = "valence-shell-bridge"
+type = "cross-repo-documentation-bridge"
+human-doc = "docs/VALENCE_SHELL_BRIDGE.adoc"
+created = "2026-06-02"
+thesis = "Ochrance is the receipt layer for Valence Shell's accountable state transitions; Echo Types is the semantics of the residue/loss those transitions expose."
+
+# Required status tags. ALL hold simultaneously today.
+[status]
+state = "documentation-bridge"
+mechanised = "not-mechanised"
+production-trust = "not-production-trust"
+cryptographic-integrity = "no-cryptographic-integrity-claim-until-hash-and-attestation-gaps-close"
+tags = [
+  "documentation-bridge",
+  "not-mechanised",
+  "not-production-trust",
+  "no-cryptographic-integrity-claim-until-hash-and-attestation-gaps-close",
+]
+
+[participants]
+valence-shell = "https://github.com/hyperpolymath/valence-shell"
+echo-types    = "https://github.com/hyperpolymath/echo-types"
+ochrance      = "https://github.com/hyperpolymath/ochrance"
+
+[roles]
+valence-shell = "operational shell: executes actions, tracks history, undo/redo/checkpoint/restore/diff/replay, RMR/RMO vocabulary"
+echo-types    = "semantic theory of structured loss: Echo f y := Sigma (x : A), (f x = y) — the proof-relevant fibre/residue over an observed output"
+ochrance      = "evidence/receipt substrate: A2ML manifests, Merkle-backed state commitments, repair witnesses, future attestation surfaces"
+
+# The four trust boundaries. Each layer is sound only within its own boundary.
+[trust-boundaries]
+valence-shell-proofs = "concern modelled shell operations (abstract model); Lean->Rust correspondence is property-tested, not mechanised"
+echo-types-scope     = "classifies recoverable / constrained / lossy / obliterative information; it is a semantics, not a runtime or evidence store"
+ochrance-receipts    = "can attest to concrete filesystem state evidence (Merkle commitments, A2ML manifests) once the hash/attestation gaps close"
+end-to-end           = "none of this currently proves Valence Shell implementation correctness end-to-end"
+
+# Ochrance integrity caveats. Load-bearing; carry into any future receipt.
+[caveats]
+hashes      = "Zig std.crypto primitives (BLAKE3/SHA-256/SHA3-256/Ed25519) are now implemented in ffi/zig/src/main.zig; still no cryptographic filesystem-integrity claim while Idris-side XOR/zero stub fallbacks remain reachable and libochrance.so is not yet built and linked into the verification flow"
+attestation = "no full attestation until Ed25519 signature verification is integrated end-to-end with a trust-root/key-management story (stub + signature-skipping path still present)"
+linear-repair = "no complete linear repair until that work is actually complete; linear quantities are typed but repair bodies are stubbed/elided"
+
+# Echo Types residue classification used as bridge vocabulary.
+# DESIGN CORRESPONDENCE ONLY — a human reading, not a mechanised classifier.
+[residue-classes]
+recoverable  = "reversible map / section exists; RMR-class ops with working undo/redo"
+constrained  = "recoverable only with retained side-evidence (checkpoint/history/metadata)"
+lossy        = "genuine collapse with non-trivial observable residue; not invertible"
+obliterative = "maximal collapse; Echo Types proves NO section exists (no-section family); RMO-class irreversible erasure"
+
+# Future event shape. DESIGN SKETCH ONLY — no such type exists in this repo.
+[event-shape]
+name = "ValenceShellReceipt"
+implemented = false
+implementation-status = "design-only — do not implement until gating conditions are met"
+fields = [
+  "event_id",
+  "command",
+  "pre_state_commitment",
+  "post_state_commitment",
+  "valence_proof_ref",
+  "echo_residue_class",
+  "ochrance_manifest_ref",
+  "merkle_root",
+  "attestation_ref",
+  "trust_boundary",
+  "status",
+]
+
+# All of these must hold before ANY code is written for this bridge.
+[gating]
+real-hashes        = "Ochrance uses real cryptographic hashes end-to-end; no XOR/zero stub path reachable"
+real-attestation   = "Ochrance attestation does real Ed25519 verification with a defined trust-root/key-management story"
+real-repair        = "Ochrance linear repair implemented, not stubbed"
+valence-proof-ref  = "Valence Shell exposes a stable referenceable proof/operation handle with its modelled-vs-implementation boundary stated"
+residue-procedure  = "a residue-classification procedure exists beyond a human reading, if echo_residue_class is to be machine-trusted"
+
+# Explicit non-claims. This bridge must NOT be cited as asserting any of these.
+[non-claims]
+ochrance-proves-valence  = false   # Ochrance does NOT prove Valence Shell correct
+echo-proves-ochrance     = false   # Echo Types does NOT prove Ochrance correct
+rmo-undoable             = false   # RMO is NOT undoable; obliterative = no section
+gdpr-compliance          = false   # no GDPR claim until RMO is implemented AND Ochrance evidence chain is closed
+echidna-integration      = false   # no Echidna claim; no concrete tested integration in this bridge
+
+[cross-references]
+architecture        = "docs/ARCHITECTURE.md"          # existing Reversibility Stack framing this bridge refines
+explainme           = "EXPLAINME.adoc"                 # same hash/attestation/repair caveats, honesty pass
+roadmap             = "ROADMAP.adoc"                   # open Phase-1 items the gating tracks
+crypto-ffi          = "ochrance-core/Ochrance/FFI/Crypto.idr"
+merkle              = "modules/Ochrance/Filesystem/Merkle.idr"
+repair              = "modules/Ochrance/Filesystem/Repair.idr"

CLAUDE.md

@@ -55,7 +55,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** - placeholder XOR hashes in Merkle.idr must be replaced
+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.
 5. **Linear types for repair** - repair operations consume old state (Quantity 1)
 
 ## Error Taxonomy

EXPLAINME.adoc

@@ -28,7 +28,7 @@ Three components orchestrate this: A2ML parser/validator (parses filesystem mani
 
 **How verified**: The Merkle tree is defined as a size-indexed binary tree: `MerkleTree : (size : Nat) → Type`. At compile time, Idris2 verifies that all leaf nodes are at depth `log2(size)`. The tree operations (leaf insertion, hash computation, proof generation) take dependent proofs that structure is maintained. README (§Architecture) claims "Verified Merkle trees — Size-indexed binary trees with compile-time structure proofs." This is proven by the type signature itself: if you try to construct a tree of size 8 with only 7 leaves, the type checker rejects it because the dependent type `MerkleTree 8` requires exactly 8 leaves.
 
-**Caveat**: The placeholder hash functions in `Merkle.idr` use XOR, not cryptographic hashes (BLAKE3/SHA-256). This is noted in the CLAUDE.md as a critical TODO. The structure proofs are valid but cryptographic strength is absent.
+**Caveat**: The size-indexed *structure* proofs are independent of hash strength. Real hashing now exists — the Zig FFI implements BLAKE3/SHA-256/SHA3-256 (`ffi/zig/src/main.zig`, with known-answer-vector tests) and the IO Merkle path calls `hashPairBlake3` — but a pure XOR combiner (`hashPairStub`) remains for totality/offline testing, and `libochrance.so` must be built and linked for the cryptographic path to be live. Until the stub paths are removed and the FFI is wired into the verification flow, the structure proofs hold but cryptographic integrity is not yet claimed.
 
 == Dogfooded Across The Account
 
@@ -69,8 +69,8 @@ Also integrates with ECHIDNA for neural proof synthesis — FFI calls to libechi
 
 == Known Limitations & TODOs
 
-* **Hashes**: Currently XOR (placeholder). Must replace with BLAKE3/SHA-256 via Zig FFI.
-* **Attestation**: Cryptographic signature verification not yet integrated (planned).
+* **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.
+* **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).
 
 == Questions?

README.adoc

@@ -75,6 +75,18 @@ The two repos are **complementary**, not duplicates:
 * **ochrance** (this repo) — concrete filesystem verification implementation (~80% complete)
 * **ochrance-framework** — abstract modular framework for all four subsystems (~10% complete)
 
+=== valence-shell & echo-types (Reversibility Stack neighbours)
+
+Ochránce can *eventually* act as the receipt layer for
+link:https://github.com/hyperpolymath/valence-shell[valence-shell]'s
+accountable state transitions, with
+link:https://github.com/hyperpolymath/echo-types[echo-types] supplying the
+semantics of the residue/loss those transitions expose. This relationship is
+**documentation-only and not mechanised** today — see
+link:docs/VALENCE_SHELL_BRIDGE.adoc[`docs/VALENCE_SHELL_BRIDGE.adoc`] (and its
+machine-readable companion `.machine_readable/integrations/valence-shell-bridge.a2ml`) for
+the trust boundaries and caveats.
+
 == License
 
 SPDX-License-Identifier: MPL-2.0

ROADMAP.adoc

@@ -28,7 +28,7 @@ Components:
 * [x] Framework Interface (VerifiedSubsystem)
 * [x] Proof Witnesses (Lax/Checked/Attested modes)
 * [x] Error Taxonomy (q/p/z classification)
-* [ ] Merkle Tree Implementation (size-indexed, needs BLAKE3 FFI)
+* [ ] Merkle Tree Implementation (size-indexed; BLAKE3 FFI now implemented in Zig — build/link wiring still pending)
 * [ ] Filesystem Verification (VerifiedSubsystem instance)
 * [ ] Linear Type Repair (consume-old-state semantics)
 * [ ] Integration Tests (50+ scenarios)
@@ -37,14 +37,14 @@ Components:
 
 1. Complete A2ML Validator (signature verification via FFI)
 2. Implement A2ML Serializer (roundtrip verification)
-3. Replace Merkle tree XOR placeholder with BLAKE3 FFI
+3. Wire the implemented Zig BLAKE3 FFI into Merkle and remove the XOR stub combiner
 4. Implement Filesystem.Verify module
 5. Implement Filesystem.Repair with linear types (Quantity 1)
 
 **Blockers:**
 
 * Idris2 0.8.0+ compiler required
-* BLAKE3/SHA-256 FFI needed for production hashing
+* `libochrance.so` (Zig crypto FFI) must be built and linked into the Idris2 verification flow; the primitives themselves (BLAKE3/SHA-256/SHA3-256/Ed25519) are now implemented and tested
 
 === Phase 2: ECHIDNA Integration (v0.2.0) - **Planned**
 

docs/ARCHITECTURE.md

@@ -100,6 +100,18 @@ The stack is loosely coupled: each layer is independently useful, but together t
 provide a complete story from "operations are reversible" through "the shell proves it"
 to "the filesystem is verified."
 
+### See also: the receipt / residue reading
+
+A complementary, **documentation-only** reading of this stack treats ochrance as
+the *receipt layer* for valence-shell's accountable state transitions, with
+[echo-types](https://github.com/hyperpolymath/echo-types) supplying the
+*semantics of the residue/loss* those transitions expose (recoverable /
+constrained / lossy / obliterative). That bridge is **not mechanised** and makes
+no cryptographic-integrity, GDPR, or end-to-end-correctness claim. See
+[`VALENCE_SHELL_BRIDGE.adoc`](VALENCE_SHELL_BRIDGE.adoc) and its machine-readable
+companion `.machine_readable/integrations/valence-shell-bridge.a2ml` for the trust boundaries
+and caveats.
+
 ---
 
 ## P2: Reposystem Boundary