Skip to content

Commit 6fd60c1

Browse files
claudeclaude
committed
Merge main into branch: reconcile #32 with merged #31
#31 landed the Zig crypto FFI, zig-ffi.yml, and the e2e_test.sh path fix on main. This merge takes main's versions of the three overlapping files (ffi/zig/build.zig, ffi/zig/src/main.zig, tests/e2e_test.sh) — the CI-validated #31 implementations — and keeps #32's unique work: A2ML parser totality + correctness, the Merkle combiner generalization, PROOFS.adoc, and AFTER-MIGRATION.adoc. Clears the 'dirty' mergeable state. https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
2 parents f40c9e6 + d7d1ace commit 6fd60c1

14 files changed

Lines changed: 666 additions & 113 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
@@ -82,6 +82,7 @@ htmlcov/
8282
**/zig-out/
8383
**/zig-cache/
8484
**/.zig-cache/
85+
**/zig-cache/
8586

8687
# Shared libraries
8788
*.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
@@ -51,7 +51,7 @@ idris2 --repl ochrance.ipkg
5151
1. **All functions must be total** - use `%default total` in every module
5252
2. **Structural recursion only** - no partial or assert_total
5353
3. **Idris2 0.8.0+** required
54-
4. **BLAKE3/SHA-256 via FFI** - placeholder XOR hashes in Merkle.idr must be replaced
54+
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.
5555
5. **Linear types for repair** - repair operations consume old state (Quantity 1)
5656

5757
## 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

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

6969
== Known Limitations & TODOs
7070

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

7575
== 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)