Skip to content

Commit d7d1ace

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Valence Shell / Echo Types bridge docs + implemented Zig crypto FFI (#31)
* docs: bridge Ochránce to valence-shell and echo-types (documentation-only) Document how Ochránce can eventually provide receipts for Valence Shell's accountable state transitions, with Echo Types supplying the semantics of the residue/loss those transitions expose. Documentation and agent orientation only — nothing is mechanised. - docs/VALENCE_SHELL_BRIDGE.adoc: human doc with the explicit trust boundaries, Ochránce integrity caveats (placeholder hashes, attestation not integrated, linear repair incomplete), the four-class residue vocabulary (recoverable/constrained/lossy/obliterative), a design-only ValenceShellReceipt event shape, implementation gating, and explicit non-claims. - .machine_readable/VALENCE_SHELL_BRIDGE.a2ml: structured status note tagged documentation-bridge / not-mechanised / not-production-trust / no-cryptographic-integrity-claim-until-hash-and-attestation-gaps-close. - README.adoc + docs/ARCHITECTURE.md: caveated orientation pointers. No cryptographic-integrity, GDPR, Echidna, or end-to-end-correctness claim is made; RMO is documented as irreversible (no section). https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * fix(tests): make E2E suite path-independent; mark crypto FFI checks pending tests/e2e_test.sh hardcoded BASE=/var/mnt/eclipse/repos/ochrance, an author-local path absent on CI runners, so every file/grep check failed (1 passed, 21 failed) on every PR regardless of content. Resolve BASE from the script's own location so the suite runs anywhere. The four hash-algorithm checks and the blake3_hash-signature check are genuine known gaps: ffi/zig/src/main.zig is still a scaffold with no BLAKE3/SHA-256/SHA3-256/Ed25519. They are now reported as PENDING (they do not fail the suite) and flip to PASS automatically once the FFI lands. This is the same gap that ROADMAP Phase 1 and docs/VALENCE_SHELL_BRIDGE.adoc gate cryptographic-integrity claims on. Result: 17 passed, 0 failed, 5 pending (exit 0). https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * docs: relocate bridge note into .machine_readable/integrations/ Move VALENCE_SHELL_BRIDGE.a2ml to .machine_readable/integrations/valence-shell-bridge.a2ml, matching the lowercase-hyphenated naming of the other integration notes (proven, vexometer, verisimdb, feedback-o-tron). Update the four references in docs/VALENCE_SHELL_BRIDGE.adoc, README.adoc, and docs/ARCHITECTURE.md. https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * feat(ffi): implement Zig crypto FFI (BLAKE3/SHA-256/SHA3-256/Ed25519) Replace the boilerplate scaffold in ffi/zig/src/main.zig with real cryptographic primitives backed by Zig 0.11.0's audited std.crypto, satisfying the C ABI declared in ochrance-core/Ochrance/FFI/Crypto.idr: void blake3_hash (const uint8_t* data, size_t len, uint8_t out[32]); void sha256_hash (const uint8_t* data, size_t len, uint8_t out[32]); void sha3_256_hash (const uint8_t* data, size_t len, uint8_t out[32]); int ed25519_verify(const uint8_t sig[64], const uint8_t pk[32], const uint8_t* msg, size_t msg_len); ed25519_verify returns 0 (never traps) on a malformed key or signature. Add Zig unit tests that call the exported functions directly: known-answer vectors for all three hashes (empty + "abc") and an Ed25519 round-trip (valid accepts; tampered signature and wrong key reject). tests/e2e_test.sh: the five crypto checks return to hard assertions now that the FFI is implemented (previously marked pending). Suite is green: 22 passed, 0 failed. Docs: the bridge caveat is refined — the Zig primitives now exist, but the cryptographic-integrity NON-claim is preserved, since Idris-side XOR/zero stub fallbacks remain reachable and libochrance.so is not yet built and linked into the verification flow. Verification note: this environment has no Zig toolchain and cannot reach ziglang.org (network policy), and no CI job compiles the FFI, so the Zig was checked statically against the pinned 0.11.0 std.crypto API and the repo's own hash_bench.zig rather than by compilation. https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * fix(ffi): make the Zig FFI compile and pass tests under Zig 0.11.0 Installing Zig 0.11.0 and actually compiling ffi/zig revealed that the scaffold main.zig never built (no CI job compiles it). Three pre-existing errors, none in the crypto added in the previous commit: - `Handle` was `opaque { ... fields ... }`; opaque types cannot carry fields in Zig. Made it a struct (it only ever crosses the C ABI as an opaque `?*Handle` pointer, so the C view is unchanged). - `ochrance_version` / `ochrance_build_info` returned `VERSION.ptr` / `BUILD_INFO.ptr` (`[*]const u8`), dropping the `:0` sentinel the return type requires; return the string constants directly. - build.zig never linked libc, but `std.heap.c_allocator` requires it; added linkLibC() to the static lib, shared lib and tests. Also switched the shared library from addStaticLibrary+linkage=.dynamic (which failed to install) to addSharedLibrary. With these fixes `zig build` produces libochrance.so + libochrance.a and `zig build test` is green: all 7 tests pass, including the crypto known-answer vectors and the Ed25519 round-trip. The crypto is now compiler-verified, not only statically reviewed. Also gitignore Zig 0.11.0's `zig-cache/` dir (the existing rule only covered the newer `.zig-cache/`). https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * ci: build and test the Zig FFI on every push Add a Zig FFI workflow that runs `zig build` and `zig build test` in ffi/zig under Zig 0.11.0 (via mlugg/setup-zig, SHA-pinned). This is the only CI job that compiles the FFI, so it is what actually verifies the BLAKE3 / SHA-256 / SHA3-256 / Ed25519 implementations and their known-answer-vector tests; the existing E2E job only greps source. https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * docs: maintainer pass — reflect implemented Zig crypto FFI Now that the Zig FFI implements BLAKE3/SHA-256/SHA3-256/Ed25519 (compiler-verified, tested), update the three status docs that still described hashes as XOR placeholders, while preserving the honest not-yet-done caveats: - CLAUDE.md rule 4: crypto implemented in Zig; still pending before any cryptographic-integrity claim = remove the Idris-side stub fallbacks and build/link libochrance.so into the verification flow. - EXPLAINME.adoc: the Claim-2 caveat and the Hashes/Attestation limitation bullets updated; structure proofs still hold independently of hash strength; no cryptographic-integrity or full-attestation claim yet. - ROADMAP.adoc: Merkle item, critical-next-action and blocker reworded from "needs BLAKE3 FFI" to "FFI implemented; wiring/build pending". No correctness, cryptographic-integrity, attestation, or GDPR claim is made; linear repair remains incomplete. https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX * ci: add SessionStart hook to provision the toolchain on Claude Code web The web container is ephemeral and cloned fresh, so install the repo's toolchains at session start: - Idris2 v0.8.0 — built from GitHub source via the chezscheme bootstrap (not in apt; no prebuilt reachable). Needs chezscheme + libgmp-dev. - Zig 0.11.0 — PyPI `ziglang` package + a `zig` shim (ziglang.org is blocked by the web network policy). - just, Agda 2.6.3 — apt. Idempotent (cached containers skip installs and start fast), best-effort (a single tool's failure is logged, not fatal), and web-only via $CLAUDE_CODE_REMOTE. Network-policy facts are documented inline: apt-get install works off the image's cached lists though apt-get update is blocked; github.com + pypi.org are reachable, ziglang.org + api.github.com are not. .claude/settings.json registers the hook for SessionStart. https://claude.ai/code/session_01UY2rBuVbYaee4NJfPWmDPX --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent ee37c25 commit d7d1ace

14 files changed

Lines changed: 683 additions & 18 deletions

File tree

‎.claude/hooks/session-start.sh‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
#!/bin/bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
#
5+
# SessionStart hook — provision the Ochránce toolchain for Claude Code on the web.
6+
#
7+
# The web container is ephemeral and cloned fresh, so the toolchains this repo
8+
# needs are reinstalled at session start:
9+
# - Idris2 v0.8.0 (core framework, proofs, parser, verification)
10+
# - Zig 0.11.0 (cryptographic FFI in ffi/zig)
11+
# - just (build/recipe runner; `just build`, `just check`, ...)
12+
# - Agda 2.6.3 (estate formal-verification toolchain)
13+
#
14+
# Idempotent: each tool is skipped when already present, so cached containers
15+
# start fast. Best-effort: a failure in one tool is logged but does not abort
16+
# the hook (a partial toolchain beats a blocked session).
17+
#
18+
# Network-policy notes for the web environment (do not "fix" these away):
19+
# - ziglang.org and api.github.com are BLOCKED; github.com and pypi.org are
20+
# reachable. Zig therefore comes from the PyPI `ziglang` package (not
21+
# ziglang.org), and Idris2 is built from GitHub source (not a prebuilt).
22+
# - `apt-get update` fails (the distro index mirror is blocked) but
23+
# `apt-get install` works off the image's cached package lists, so update
24+
# is best-effort only.
25+
set -uo pipefail
26+
27+
# Web-only: on a local machine, use your own toolchain.
28+
if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
29+
exit 0
30+
fi
31+
32+
log() { printf '[session-start] %s\n' "$*" >&2; }
33+
have() { command -v "$1" >/dev/null 2>&1; }
34+
35+
# --- apt packages: just, Agda, and the Idris2 build dependencies ------------
36+
if ! { have just && have agda && have idris2; }; then
37+
log "installing apt packages (just, agda, Idris2 build deps) ..."
38+
apt-get update >/dev/null 2>&1 || true
39+
apt-get install -y --no-install-recommends \
40+
just agda agda-stdlib chezscheme libgmp-dev make gcc git \
41+
|| log "WARN: some apt packages failed to install"
42+
fi
43+
44+
# --- Zig 0.11.0 via the PyPI ziglang package (ziglang.org is blocked) -------
45+
if ! have zig; then
46+
log "installing Zig 0.11.0 via PyPI ziglang ..."
47+
if pip3 install --break-system-packages --quiet "ziglang==0.11.0"; then
48+
cat > /usr/local/bin/zig <<'SH'
49+
#!/bin/sh
50+
# Thin shim exposing the PyPI `ziglang` package as a `zig` command.
51+
exec python3 -m ziglang "$@"
52+
SH
53+
chmod +x /usr/local/bin/zig
54+
else
55+
log "WARN: Zig install failed"
56+
fi
57+
fi
58+
59+
# --- Idris2 v0.8.0, built from GitHub source (not in apt; no reachable bin) --
60+
# Cold build self-hosts the compiler and takes several minutes; cached
61+
# containers skip it. Needs chezscheme + libgmp-dev (installed above).
62+
if ! have idris2; then
63+
log "building Idris2 v0.8.0 from source (several minutes on a cold container) ..."
64+
src=/opt/Idris2-build
65+
if rm -rf "$src" \
66+
&& git clone --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$src" \
67+
&& make -C "$src" bootstrap SCHEME=chezscheme PREFIX=/usr/local \
68+
&& make -C "$src" install PREFIX=/usr/local; then
69+
log "Idris2 installed to /usr/local"
70+
else
71+
log "WARN: Idris2 build failed (see output above)"
72+
fi
73+
fi
74+
75+
# --- Report -----------------------------------------------------------------
76+
log "toolchain status:"
77+
have zig && log " zig $(zig version 2>&1)" || log " zig MISSING"
78+
have just && log " just $(just --version 2>&1)" || log " just MISSING"
79+
have agda && log " agda $(agda --version 2>&1 | head -1)" || log " agda MISSING"
80+
have idris2 && log " idris2 $(idris2 --version 2>&1 | head -1)" || log " idris2 MISSING"
81+
82+
exit 0

‎.claude/settings.json‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
{
2+
"hooks": {
3+
"SessionStart": [
4+
{
5+
"hooks": [
6+
{
7+
"type": "command",
8+
"command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
9+
}
10+
]
11+
}
12+
]
13+
}
14+
}

‎.github/workflows/zig-ffi.yml‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Build and test the Zig cryptographic FFI (ffi/zig).
3+
#
4+
# This is the only CI job that compiles the Zig FFI, so it is what actually
5+
# verifies the BLAKE3 / SHA-256 / SHA3-256 / Ed25519 implementations in
6+
# ffi/zig/src/main.zig (the grep-based E2E job only checks source strings).
7+
name: Zig FFI
8+
9+
on: [push, pull_request]
10+
11+
permissions:
12+
contents: read
13+
14+
jobs:
15+
zig-ffi:
16+
name: Zig FFI build + test
17+
runs-on: ubuntu-latest
18+
steps:
19+
- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
20+
- name: Set up Zig 0.11.0
21+
uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
22+
with:
23+
version: 0.11.0
24+
- name: Build (libochrance.so + libochrance.a)
25+
working-directory: ffi/zig
26+
run: zig build
27+
- name: Test (hash known-answer vectors + Ed25519 round-trip)
28+
working-directory: ffi/zig
29+
run: zig build test

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ htmlcov/
8181
# Zig
8282
**/zig-out/
8383
**/.zig-cache/
84+
**/zig-cache/
8485

8586
# Shared libraries
8687
*.so

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

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# Ochrance <-> Valence Shell <-> Echo Types — cross-repo bridge note.
5+
# Machine-readable companion to docs/VALENCE_SHELL_BRIDGE.adoc.
6+
# This is an ORIENTATION note for agents. It records a documentation-only
7+
# bridge. Nothing here is mechanised, shipped, or trusted.
8+
9+
[bridge]
10+
name = "valence-shell-bridge"
11+
type = "cross-repo-documentation-bridge"
12+
human-doc = "docs/VALENCE_SHELL_BRIDGE.adoc"
13+
created = "2026-06-02"
14+
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."
15+
16+
# Required status tags. ALL hold simultaneously today.
17+
[status]
18+
state = "documentation-bridge"
19+
mechanised = "not-mechanised"
20+
production-trust = "not-production-trust"
21+
cryptographic-integrity = "no-cryptographic-integrity-claim-until-hash-and-attestation-gaps-close"
22+
tags = [
23+
"documentation-bridge",
24+
"not-mechanised",
25+
"not-production-trust",
26+
"no-cryptographic-integrity-claim-until-hash-and-attestation-gaps-close",
27+
]
28+
29+
[participants]
30+
valence-shell = "https://github.com/hyperpolymath/valence-shell"
31+
echo-types = "https://github.com/hyperpolymath/echo-types"
32+
ochrance = "https://github.com/hyperpolymath/ochrance"
33+
34+
[roles]
35+
valence-shell = "operational shell: executes actions, tracks history, undo/redo/checkpoint/restore/diff/replay, RMR/RMO vocabulary"
36+
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"
37+
ochrance = "evidence/receipt substrate: A2ML manifests, Merkle-backed state commitments, repair witnesses, future attestation surfaces"
38+
39+
# The four trust boundaries. Each layer is sound only within its own boundary.
40+
[trust-boundaries]
41+
valence-shell-proofs = "concern modelled shell operations (abstract model); Lean->Rust correspondence is property-tested, not mechanised"
42+
echo-types-scope = "classifies recoverable / constrained / lossy / obliterative information; it is a semantics, not a runtime or evidence store"
43+
ochrance-receipts = "can attest to concrete filesystem state evidence (Merkle commitments, A2ML manifests) once the hash/attestation gaps close"
44+
end-to-end = "none of this currently proves Valence Shell implementation correctness end-to-end"
45+
46+
# Ochrance integrity caveats. Load-bearing; carry into any future receipt.
47+
[caveats]
48+
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"
49+
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)"
50+
linear-repair = "no complete linear repair until that work is actually complete; linear quantities are typed but repair bodies are stubbed/elided"
51+
52+
# Echo Types residue classification used as bridge vocabulary.
53+
# DESIGN CORRESPONDENCE ONLY — a human reading, not a mechanised classifier.
54+
[residue-classes]
55+
recoverable = "reversible map / section exists; RMR-class ops with working undo/redo"
56+
constrained = "recoverable only with retained side-evidence (checkpoint/history/metadata)"
57+
lossy = "genuine collapse with non-trivial observable residue; not invertible"
58+
obliterative = "maximal collapse; Echo Types proves NO section exists (no-section family); RMO-class irreversible erasure"
59+
60+
# Future event shape. DESIGN SKETCH ONLY — no such type exists in this repo.
61+
[event-shape]
62+
name = "ValenceShellReceipt"
63+
implemented = false
64+
implementation-status = "design-only — do not implement until gating conditions are met"
65+
fields = [
66+
"event_id",
67+
"command",
68+
"pre_state_commitment",
69+
"post_state_commitment",
70+
"valence_proof_ref",
71+
"echo_residue_class",
72+
"ochrance_manifest_ref",
73+
"merkle_root",
74+
"attestation_ref",
75+
"trust_boundary",
76+
"status",
77+
]
78+
79+
# All of these must hold before ANY code is written for this bridge.
80+
[gating]
81+
real-hashes = "Ochrance uses real cryptographic hashes end-to-end; no XOR/zero stub path reachable"
82+
real-attestation = "Ochrance attestation does real Ed25519 verification with a defined trust-root/key-management story"
83+
real-repair = "Ochrance linear repair implemented, not stubbed"
84+
valence-proof-ref = "Valence Shell exposes a stable referenceable proof/operation handle with its modelled-vs-implementation boundary stated"
85+
residue-procedure = "a residue-classification procedure exists beyond a human reading, if echo_residue_class is to be machine-trusted"
86+
87+
# Explicit non-claims. This bridge must NOT be cited as asserting any of these.
88+
[non-claims]
89+
ochrance-proves-valence = false # Ochrance does NOT prove Valence Shell correct
90+
echo-proves-ochrance = false # Echo Types does NOT prove Ochrance correct
91+
rmo-undoable = false # RMO is NOT undoable; obliterative = no section
92+
gdpr-compliance = false # no GDPR claim until RMO is implemented AND Ochrance evidence chain is closed
93+
echidna-integration = false # no Echidna claim; no concrete tested integration in this bridge
94+
95+
[cross-references]
96+
architecture = "docs/ARCHITECTURE.md" # existing Reversibility Stack framing this bridge refines
97+
explainme = "EXPLAINME.adoc" # same hash/attestation/repair caveats, honesty pass
98+
roadmap = "ROADMAP.adoc" # open Phase-1 items the gating tracks
99+
crypto-ffi = "ochrance-core/Ochrance/FFI/Crypto.idr"
100+
merkle = "modules/Ochrance/Filesystem/Merkle.idr"
101+
repair = "modules/Ochrance/Filesystem/Repair.idr"

‎CLAUDE.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ idris2 --repl ochrance.ipkg
5555
1. **All functions must be total** - use `%default total` in every module
5656
2. **Structural recursion only** - no partial or assert_total
5757
3. **Idris2 0.8.0+** required
58-
4. **BLAKE3/SHA-256 via FFI** - placeholder XOR hashes in Merkle.idr must be replaced
58+
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.
5959
5. **Linear types for repair** - repair operations consume old state (Quantity 1)
6060

6161
## Error Taxonomy

‎EXPLAINME.adoc‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Three components orchestrate this: A2ML parser/validator (parses filesystem mani
2828

2929
**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.
3030

31-
**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.
31+
**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.
3232

3333
== Dogfooded Across The Account
3434

@@ -69,8 +69,8 @@ Also integrates with ECHIDNA for neural proof synthesis — FFI calls to libechi
6969

7070
== Known Limitations & TODOs
7171

72-
* **Hashes**: Currently XOR (placeholder). Must replace with BLAKE3/SHA-256 via Zig FFI.
73-
* **Attestation**: Cryptographic signature verification not yet integrated (planned).
72+
* **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.
73+
* **Attestation**: Ed25519 verification is implemented (Zig FFI + `validateManifestIO`). Remaining: a trust-root / key-management story and end-to-end integration before claiming full attestation.
7474
* **Linear repair**: Idris2 linear types framework incomplete for full use-after-repair prevention (ongoing research).
7575

7676
== Questions?

‎README.adoc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,18 @@ The two repos are **complementary**, not duplicates:
7575
* **ochrance** (this repo) — concrete filesystem verification implementation (~80% complete)
7676
* **ochrance-framework** — abstract modular framework for all four subsystems (~10% complete)
7777

78+
=== valence-shell & echo-types (Reversibility Stack neighbours)
79+
80+
Ochránce can *eventually* act as the receipt layer for
81+
link:https://github.com/hyperpolymath/valence-shell[valence-shell]'s
82+
accountable state transitions, with
83+
link:https://github.com/hyperpolymath/echo-types[echo-types] supplying the
84+
semantics of the residue/loss those transitions expose. This relationship is
85+
**documentation-only and not mechanised** today — see
86+
link:docs/VALENCE_SHELL_BRIDGE.adoc[`docs/VALENCE_SHELL_BRIDGE.adoc`] (and its
87+
machine-readable companion `.machine_readable/integrations/valence-shell-bridge.a2ml`) for
88+
the trust boundaries and caveats.
89+
7890
== License
7991

8092
SPDX-License-Identifier: MPL-2.0

‎ROADMAP.adoc‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Components:
2828
* [x] Framework Interface (VerifiedSubsystem)
2929
* [x] Proof Witnesses (Lax/Checked/Attested modes)
3030
* [x] Error Taxonomy (q/p/z classification)
31-
* [ ] Merkle Tree Implementation (size-indexed, needs BLAKE3 FFI)
31+
* [ ] Merkle Tree Implementation (size-indexed; BLAKE3 FFI now implemented in Zig — build/link wiring still pending)
3232
* [ ] Filesystem Verification (VerifiedSubsystem instance)
3333
* [ ] Linear Type Repair (consume-old-state semantics)
3434
* [ ] Integration Tests (50+ scenarios)
@@ -37,14 +37,14 @@ Components:
3737

3838
1. Complete A2ML Validator (signature verification via FFI)
3939
2. Implement A2ML Serializer (roundtrip verification)
40-
3. Replace Merkle tree XOR placeholder with BLAKE3 FFI
40+
3. Wire the implemented Zig BLAKE3 FFI into Merkle and remove the XOR stub combiner
4141
4. Implement Filesystem.Verify module
4242
5. Implement Filesystem.Repair with linear types (Quantity 1)
4343

4444
**Blockers:**
4545

4646
* Idris2 0.8.0+ compiler required
47-
* BLAKE3/SHA-256 FFI needed for production hashing
47+
* `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
4848

4949
=== Phase 2: ECHIDNA Integration (v0.2.0) - **Planned**
5050

‎docs/ARCHITECTURE.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,18 @@ The stack is loosely coupled: each layer is independently useful, but together t
100100
provide a complete story from "operations are reversible" through "the shell proves it"
101101
to "the filesystem is verified."
102102

103+
### See also: the receipt / residue reading
104+
105+
A complementary, **documentation-only** reading of this stack treats ochrance as
106+
the *receipt layer* for valence-shell's accountable state transitions, with
107+
[echo-types](https://github.com/hyperpolymath/echo-types) supplying the
108+
*semantics of the residue/loss* those transitions expose (recoverable /
109+
constrained / lossy / obliterative). That bridge is **not mechanised** and makes
110+
no cryptographic-integrity, GDPR, or end-to-end-correctness claim. See
111+
[`VALENCE_SHELL_BRIDGE.adoc`](VALENCE_SHELL_BRIDGE.adoc) and its machine-readable
112+
companion `.machine_readable/integrations/valence-shell-bridge.a2ml` for the trust boundaries
113+
and caveats.
114+
103115
---
104116

105117
## P2: Reposystem Boundary

0 commit comments

Comments
 (0)