Skip to content

Commit 546ec4e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(bridge): land canonical Echo Types / Ochrance bridge for Valence Shell
Three-layer architecture document + machine-readable manifest + agent pointer. The bridge is documentation-and-orientation-only, not a mechanised dependency. ## Files - docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc — canonical .adoc, owner-authored. - .machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml — A2ML companion capturing layers, key concepts, valence-shell cases, ochrance roles, agent required-framing rules, and the forbidden-moves list. - .claude/CLAUDE.md — READ-FIRST pointer added at top. ## Forbidden moves (codified) - No "Valence Shell is production-ready" - No "Lean-to-Rust correspondence is mechanised" - No "RMO/GDPR support exists beyond stubs" - No "Echo Types proves Valence Shell implementation correctness" - No "Ochrance cryptographic integrity" while upstream gaps remain - No merging exploratory Echo bridges into core claims without checking echo-types/docs/bridge-status.md ## Editorial cleanup Source had mangled source-block delimiters (== [source,agda] mixing section syntax with language tags). Normalised to proper [source,LANG] + ---- blocks so the doc renders. Text content preserved verbatim. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent cd19c69 commit 546ec4e

3 files changed

Lines changed: 294 additions & 0 deletions

File tree

‎.claude/CLAUDE.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,20 @@
22
SPDX-License-Identifier: MPL-2.0
33
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
44
-->
5+
## Canonical bridge — READ FIRST
6+
7+
Before making claims about reversibility, obliteration, Lean↔Rust mechanisation, or cryptographic attestation, read both:
8+
9+
- `docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc` — three-layer architecture (Valence Shell / Echo Types / Ochrance) + forbidden-moves rules
10+
- `.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml` — machine-readable companion
11+
12+
The bridge is **documentation-and-orientation-only**, not a mechanised dependency. Keep RMR (reversible) and RMO (irreversible + audit residue) distinct.
13+
514
## Machine-Readable Artefacts
615

716
The following files in `.machine_readable/` contain structured project metadata:
817

18+
- `.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml` - Bridge to echo-types + ochrance (READ FIRST)
919
- `.machine_readable/6a2/STATE.a2ml` - Current project state and progress
1020
- `.machine_readable/6a2/META.a2ml` - Architecture decisions and development practices
1121
- `.machine_readable/6a2/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects

‎.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Echo Types / Ochrance Bridge for Valence Shell
3+
#
4+
# Machine-readable companion to docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc.
5+
# Agents should treat both files as the canonical bridge entry points.
6+
7+
[bridge]
8+
name = "echo-types-ochrance-for-valence-shell"
9+
status = "documentation-and-orientation-only"
10+
mechanised = false
11+
doc = "docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc"
12+
13+
[layers]
14+
shell = "valence-shell"
15+
semantics = "echo-types"
16+
receipts = "ochrance"
17+
18+
[upstream-repos]
19+
echo-types = "https://github.com/hyperpolymath/echo-types"
20+
ochrance = "https://github.com/hyperpolymath/ochrance"
21+
22+
[echo-types-required-reading]
23+
readme = "README.md"
24+
identity-suite = "proofs/agda/EchoCanonicalIdentitySuite.agda"
25+
map = "docs/echo-types/MAP.adoc"
26+
bridge-status = "docs/bridge-status.md"
27+
claude = "CLAUDE.md"
28+
29+
[echo-types-key-concepts]
30+
fibre-object = "Echo f y := Σ (x : A) , (f x ≡ y)"
31+
canonical-totality = "A ≃ Σ B (Echo f)"
32+
residue-forms = ["epistemic", "indexed", "search", "cost", "observational"]
33+
collapsing-map = "no-section results; right mental model for irreversible/obliterative actions"
34+
honesty-rule = "bridges can be useful while still not affecting Echo Types' core theorems"
35+
36+
[valence-shell-cases]
37+
38+
[valence-shell-cases.rmr]
39+
name = "Remove-Match-Reverse (reversible)"
40+
echo-reading = "fibre is singleton-like or equivalence-like under stated preconditions"
41+
do-not-claim = "all shell operations are reversible"
42+
43+
[valence-shell-cases.lossy]
44+
name = "Ordinary lossy operation"
45+
echo-reading = "prev state not fully recoverable but residue constrains what could have happened"
46+
do-not-claim = "total erasure"
47+
48+
[valence-shell-cases.rmo]
49+
name = "Remove-Match-Obliterate (irreversible + audit residue)"
50+
echo-reading = "proof-relevant certificate of elimination with permitted audit residue"
51+
do-not-claim = "undoable deletion"
52+
current-status = "stubs only"
53+
54+
[valence-shell-cases.narration]
55+
name = "explain / checkpoint / restore / diff / replay"
56+
echo-reading = "human-facing projections over transitions, residues, and evidence trails"
57+
do-not-claim = "narration is proof without backing artefacts or receipts"
58+
59+
[ochrance-roles]
60+
state-evidence = "A2ML manifests and validators"
61+
snapshot-integrity = "verified Merkle structure (once cryptographic hashing is no longer placeholder)"
62+
repair-evidence = "linear repair operations and proof witnesses"
63+
trust-boundary = "receipts consumable by humans, CI, future Echidna-style validators"
64+
65+
[ochrance-current-gaps]
66+
hash-attestation = "placeholder XOR hashes"
67+
crypto-coverage = "incomplete; production cryptographic guarantees not yet closed upstream"
68+
linear-repair = "ongoing work"
69+
70+
[agent-rules]
71+
72+
[agent-rules.required-framing]
73+
language = ["bridge", "semantic framing", "architecture dependency"]
74+
rmr-vs-rmo = "keep distinct — RMR reversible-under-preconditions; RMO irreversible-with-audit-residue"
75+
echo-types-usage = "name residues and loss modes; do not inflate proof status"
76+
ochrance-usage = "name receipts and attestation surfaces; do not claim crypto guarantees while upstream gaps remain"
77+
78+
[agent-rules.forbidden-moves]
79+
production-ready = "do not claim valence-shell is production-ready"
80+
lean-rust-mechanised = "do not claim the Lean-to-Rust correspondence is mechanised"
81+
rmo-gdpr-beyond-stubs = "do not claim RMO/GDPR support exists beyond stubs"
82+
echo-proves-implementation = "do not claim Echo Types proves Valence Shell implementation correctness"
83+
ochrance-crypto = "do not claim Ochrance cryptographic integrity while hash/attestation gaps remain"
84+
exploratory-as-core = "do not merge exploratory Echo bridges into core claims without checking echo-types/docs/bridge-status.md"
85+
86+
[future-mechanised-shell-event-shape]
87+
fields = [
88+
"pre_state_commitment",
89+
"command",
90+
"post_state_commitment",
91+
"valence_proof_ref",
92+
"echo_residue_class",
93+
"ochrance_receipt_ref",
94+
"trust_boundary",
95+
]
96+
status = "design-shape-only"
97+
becomes-implementation-after = [
98+
"valence-shell has concrete machine-readable event/receipt format",
99+
"ochrance has compatible A2ML/Merkle/attestation object for that event",
100+
"echo-types has stable classification target for the residue class",
101+
"bridge is labelled honestly (exploratory / partial / mechanised)",
102+
]

‎docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc‎

Lines changed: 182 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,182 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= Echo Types / Ochrance Bridge for Valence Shell
4+
:toc:
5+
:icons: font
6+
7+
== Purpose
8+
9+
This document tells humans and LLM agents how to relate Valence Shell to `hyperpolymath/echo-types` and `hyperpolymath/ochrance` without overstating the current implementation.
10+
11+
Valence Shell is the operational shell: it executes filesystem and shell actions, tracks history, supports undo/redo, and proves a substantial reversible-operation core across multiple proof systems.
12+
13+
Echo Types is the semantic theory of structured loss: irreversible computations are not treated as blank erasure, but as maps with proof-relevant residues. Its foundation is:
14+
15+
[source,agda]
16+
----
17+
Echo f y := Σ (x : A) , (f x ≡ y)
18+
----
19+
20+
Ochrance is the receipt and attestation layer: A2ML manifests, verified Merkle structure, linear repair, and subsystem verification give concrete evidence that a filesystem state or repair claim can be checked.
21+
22+
The bridge is not currently a mechanised dependency. It is an architecture and documentation obligation: agents must preserve the distinction between proven Valence Shell claims, Echo Types semantic framing, and Ochrance receipt evidence.
23+
24+
== One-sentence placement
25+
26+
Valence Shell supplies the shell operations; Echo Types supplies the language for what information is preserved, lost, recoverable, or merely constrained by those operations; Ochrance supplies the receipts that make state and repair claims auditable.
27+
28+
== Why Valence Shell needs Echo Types
29+
30+
Valence Shell already has RMR and RMO vocabulary:
31+
32+
* RMR: Remove-Match-Reverse, reversible transactions with undo/redo proof.
33+
* RMO: Remove-Match-Obliterate, irreversible deletion with proof of complete removal; currently stubs only.
34+
35+
Without Echo Types, these can be misread as only implementation features. With Echo Types, they become cases in a broader theory of information change.
36+
37+
For a shell operation modeled as a map:
38+
39+
[source,text]
40+
----
41+
f : PreState -> PostState
42+
----
43+
44+
`Echo f y` is the proof-relevant space of pre-states that could have produced the observed post-state `y`. This lets Valence Shell say more precise things:
45+
46+
[cols="1,2,2"]
47+
|===
48+
| Valence Shell case | Echo Types reading | What not to claim
49+
50+
| Reversible operation / RMR
51+
| The relevant fibre should be singleton-like, equivalence-like, or otherwise controlled enough to reconstruct the previous state under stated preconditions.
52+
| Do not claim all shell operations are reversible.
53+
54+
| Ordinary lossy operation
55+
| The previous state is not fully recoverable, but the residue still constrains what could have happened.
56+
| Do not collapse this into total erasure.
57+
58+
| RMO / obliteration
59+
| The point is not recovery. The point is a proof-relevant certificate that the target information has been eliminated while permitted audit residue remains.
60+
| Do not describe RMO as undoable deletion.
61+
62+
| `explain`, `checkpoint`, `restore`, `diff`, `replay`
63+
| Human-facing projections over state transitions, residues, and evidence trails.
64+
| Do not present narration as proof unless backed by proof artefacts or receipts.
65+
|===
66+
67+
== The specific Echo Types material Claude must know
68+
69+
Read these from `hyperpolymath/echo-types` before changing this bridge:
70+
71+
* `README.md` — canonical foundation, recommended reading order, and the current identity-layer story.
72+
* `proofs/agda/EchoCanonicalIdentitySuite.agda` — curated proof entry point for the load-bearing Echo identity layer.
73+
* `docs/echo-types/MAP.adoc` — status-tagged master map.
74+
* `docs/bridge-status.md` — distinguishes exploratory bridges from core results.
75+
* `CLAUDE.md` — session ledger and working rules.
76+
77+
The concepts that matter most for Valence Shell are:
78+
79+
* `Echo f y := Σ (x : A) , (f x ≡ y)` as the fibre/residue object.
80+
* Canonical total completion: `A ≃ Σ B (Echo f)`.
81+
* Classification of loss/residue forms, especially epistemic, indexed, search, cost, and observational residues.
82+
* No-section / collapsing-map results as the right mental model for irreversible or obliterative shell actions.
83+
* The honesty rule: bridges can be useful while still not affecting Echo Types' core theorems.
84+
85+
== Why Valence Shell needs Ochrance
86+
87+
Ochrance is the natural place for concrete filesystem receipts.
88+
89+
Valence Shell can prove that a modeled operation has a property. Ochrance can help package filesystem evidence that a particular state, manifest, repair, or attestation was checked. In bridge terms:
90+
91+
[cols="1,2"]
92+
|===
93+
| Concern | Ochrance role
94+
95+
| Filesystem state evidence
96+
| A2ML manifests and validators.
97+
98+
| Integrity of snapshots/checkpoints
99+
| Verified Merkle-tree structure, once cryptographic hashing is no longer a placeholder.
100+
101+
| Repair / rollback evidence
102+
| Linear repair operations and proof witnesses.
103+
104+
| Cross-tool trust boundary
105+
| Receipts that can be consumed by humans, CI, or future Echidna-style validators.
106+
|===
107+
108+
Ochrance has its own limitations. Current docs note placeholder XOR hashes, incomplete cryptographic attestation, and ongoing linear-repair work. Therefore Valence Shell must not imply that Ochrance already closes all production trust gaps.
109+
110+
== Three-layer architecture
111+
112+
[source,text]
113+
----
114+
Layer 1: Valence Shell
115+
Executes commands; tracks operation history; exposes explain/checkpoint/diff/replay;
116+
proves reversible-operation properties in the project proof stack.
117+
118+
Layer 2: Echo Types
119+
Interprets operations as maps with fibres/residues; classifies what is
120+
recoverable, constrained, observationally equivalent, or genuinely lost.
121+
122+
Layer 3: Ochrance
123+
Emits/checks receipts: A2ML manifests, Merkle-backed state commitments, repair
124+
witnesses, and future attestation evidence.
125+
----
126+
127+
The key rule is separation of concerns:
128+
129+
* Valence Shell should not absorb Echo Types as shell implementation machinery.
130+
* Echo Types should not become a dumping ground for shell-specific engineering.
131+
* Ochrance should not be used as a magic proof oracle; it is an evidence and verification framework with its own trust boundaries.
132+
133+
== Claude / LLM instructions
134+
135+
When working in Valence Shell, Claude and similar agents must observe these rules.
136+
137+
=== Required framing
138+
139+
* Treat this document and `.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml` as the bridge entry points.
140+
* Say "bridge", "semantic framing", or "architecture dependency" unless a real code/proof dependency has been added.
141+
* Keep RMR and RMO distinct:
142+
** RMR: reversible under preconditions.
143+
** RMO: irreversible/obliterative with audit residue, not undo.
144+
* Use Echo Types to name residues and loss modes, not to inflate the Valence Shell proof status.
145+
* Use Ochrance to name receipts and attestation surfaces, not to claim production cryptographic guarantees until those gaps are closed upstream.
146+
147+
=== Forbidden moves
148+
149+
* Do not claim Valence Shell is production-ready.
150+
* Do not claim the Lean-to-Rust correspondence is mechanised.
151+
* Do not claim RMO/GDPR support exists beyond stubs.
152+
* Do not claim Echo Types proves Valence Shell implementation correctness.
153+
* Do not claim Ochrance cryptographic integrity while its hash/attestation gaps remain open.
154+
* Do not merge exploratory Echo bridges into core claims without checking `docs/bridge-status.md` in echo-types.
155+
156+
== Minimal future implementation shape
157+
158+
A future mechanised bridge could define a typed event like:
159+
160+
[source,text]
161+
----
162+
ShellEvent := {
163+
pre_state_commitment,
164+
command,
165+
post_state_commitment,
166+
valence_proof_ref,
167+
echo_residue_class,
168+
ochrance_receipt_ref,
169+
trust_boundary
170+
}
171+
----
172+
173+
For now this is only a design shape. It becomes implementation work only after:
174+
175+
. Valence Shell has a concrete machine-readable event/receipt format.
176+
. Ochrance has a compatible A2ML/Merkle/attestation object for that event.
177+
. Echo Types has a suitable stable classification target for the residue class.
178+
. The bridge is labelled honestly as exploratory, partial, or mechanised.
179+
180+
== Bottom line
181+
182+
Valence Shell should use Echo Types as its theory of accountable information loss and Ochrance as its evidence substrate. The immediate action is documentation and agent-orientation, not pretending that a mechanised three-repo theorem already exists.

0 commit comments

Comments
 (0)