|
| 1 | +// SPDX-License-Identifier: CC-BY-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += Valence Shell / Ochránce accountable-shell bridge — exploratory |
| 4 | +:toc: macro |
| 5 | +:toclevels: 2 |
| 6 | +:sectnums: |
| 7 | +:sectnumlevels: 2 |
| 8 | +:icons: font |
| 9 | + |
| 10 | +[CAUTION] |
| 11 | +==== |
| 12 | +*EXPLORATORY — downstream application evidence, not Gate theory.* |
| 13 | +Not load-bearing for the identity claim. Subject to abandonment. |
| 14 | +Does not constrain Pillar E or any Lane 1–4 close-out. *Core Affect: |
| 15 | +NO.* There is no Agda artefact for this bridge; nothing here is |
| 16 | +imported into `proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, or |
| 17 | +`proofs/agda/EchoCanonicalIdentitySuite.agda`, so the verified suite |
| 18 | +is unaffected by anything in this directory. |
| 19 | +==== |
| 20 | + |
| 21 | +toc::[] |
| 22 | + |
| 23 | +== Scope, in one paragraph |
| 24 | + |
| 25 | +Valence Shell / Ochránce is a *possible downstream consumer* of Echo |
| 26 | +Types' structured-loss semantics. The bridge is exploratory and has |
| 27 | +*Core Affect: NO*. Valence Shell (`hyperpolymath/valence-shell`) is |
| 28 | +an accountable shell with reversible operations, undo/redo, named |
| 29 | +checkpoints, and diff/replay. Ochránce (`hyperpolymath/ochrance`) is |
| 30 | +a filesystem verification framework that produces concrete receipt |
| 31 | +evidence — A2ML manifests, Merkle state commitments, and |
| 32 | +repair/attestation surfaces. This directory records a *candidate* |
| 33 | +observation: that Echo Types' vocabulary for structured loss might |
| 34 | +serve as a semantic language for classifying the information change |
| 35 | +carried by a shell or filesystem state transition, and that Ochránce |
| 36 | +might supply the concrete evidence such a classification would |
| 37 | +consume. The observation is exploratory. It is not a generalisation |
| 38 | +claim, not a new identity claim, not a pillar, not a gate, and not a |
| 39 | +mechanised cross-repo theorem. |
| 40 | + |
| 41 | +== The candidate classification (reading aid only) |
| 42 | + |
| 43 | +A shell or filesystem state transition `s ↦ s'` carries an |
| 44 | +information change. Echo Types already names several shapes of such |
| 45 | +change as *existing* artefacts in this repo, at the K-free honesty |
| 46 | +level: |
| 47 | + |
| 48 | +[cols="1,3", options="header"] |
| 49 | +|=== |
| 50 | +| Informal class | Candidate Echo Types vocabulary (existing modules) |
| 51 | + |
| 52 | +| recoverable |
| 53 | +| a section / left-leg equivalence exists (`EchoTotalCompletion`, |
| 54 | + `EchoLossTaxonomy` EQUIV case) |
| 55 | + |
| 56 | +| constrained |
| 57 | +| injective / graded narrowing (`EchoLossTaxonomy` INJ case, |
| 58 | + `EchoGraded`) |
| 59 | + |
| 60 | +| residue-bearing |
| 61 | +| a lowering carries partial information (`EchoResidue`, |
| 62 | + `EchoResidueTaxonomy`) |
| 63 | + |
| 64 | +| observationally equivalent |
| 65 | +| indistinguishable at the chosen observation mode |
| 66 | + (`EchoObservationalEquivalence`) |
| 67 | + |
| 68 | +| genuinely lost |
| 69 | +| no section over the residue (`EchoNoSectionGeneric`, |
| 70 | + trivial-residue collapse) |
| 71 | +|=== |
| 72 | + |
| 73 | +The mapping is a reading aid only. No claim is made that any Valence |
| 74 | +Shell or Ochránce operation *has been proved* to fall into any class. |
| 75 | +The table records which existing Echo Types theorem each informal |
| 76 | +class would correspond to *if* such a downstream classification were |
| 77 | +ever carried out. The Agda named in the right column is the source |
| 78 | +of truth for what is actually proved; this directory adds nothing to |
| 79 | +it. |
| 80 | + |
| 81 | +== What this bridge does NOT claim |
| 82 | + |
| 83 | +* It does *not* claim Echo Types proves Valence Shell (or Ochránce) |
| 84 | + implementation correctness. |
| 85 | +* It makes *no* claim about POSIX semantics, Rust, the Lean→Rust |
| 86 | + correspondence, secure deletion, GDPR compliance, cryptographic |
| 87 | + integrity, or Ochránce attestation. |
| 88 | +* It does *not* promote any cross-repo statement to core-theorem |
| 89 | + status; *Core Affect: NO*. |
| 90 | +* It adds no postulates and no Agda modules. |
| 91 | +* Valence Shell's own RMR (Remove-Match-Reverse) / RMO |
| 92 | + (Remove-Match-Obliterate) vocabulary is *downstream application |
| 93 | + vocabulary*. Where it appears here it is named only as the |
| 94 | + consumer's own terminology; it is not adopted into, nor mirrored |
| 95 | + by, the Echo Types core. |
| 96 | + |
| 97 | +== Direction of the bridge |
| 98 | + |
| 99 | +The bridge is one-directional by intent: Echo Types is *upstream* |
| 100 | +(the semantic vocabulary), Valence Shell and Ochránce are *downstream* |
| 101 | +(candidate consumers). Downstream consumers must not alter the core |
| 102 | +theory. Any future formal work would live in the consuming repos or |
| 103 | +in a clearly-separated bridge module, never in the canonical identity |
| 104 | +suite, the F5 / OFS universal-property story, or the establishment |
| 105 | +framing. |
| 106 | + |
| 107 | +== Status and termination |
| 108 | + |
| 109 | +Exploratory. The bridge is retired if any of the following hold: the |
| 110 | +downstream repos adopt a different semantic foundation; no concrete |
| 111 | +Valence Shell / Ochránce operation is ever classified against the |
| 112 | +table above; or the relationship is found redundant with the existing |
| 113 | +in-repo residue / loss framing. |
| 114 | + |
| 115 | +Status anchors: |
| 116 | + |
| 117 | +* `docs/bridge-status.md` §7 (concise ledger, Core Affect: NO); |
| 118 | +* `docs/bridges/cross-repo-bridge-status.md` (cross-repo track table). |
0 commit comments