From 22040bd740892f6c13bf63d02fc942c43e1585d1 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 14:31:54 +0100 Subject: [PATCH] docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Seam-analyst sweep after the ephapax bridge package landed (#161 + #162). Three doc surfaces enumerate the bridges and need to include Ephapax-L3: * `docs/bridges/EchoBridges.md` — adds §5 EchoEphapaxBridge to the per-bridge enumeration with the `[NARROW]` tag, cross-repo theorem correspondence table (5 rows: mode order / weaken-collapses / affine-canonical / degrade-mode-comp / no-section-collapse), honest scope (L3 ONLY), and the main entry. Overview line updated to include "Ephapax-L3". * `docs/bridges/cross-repo-bridge-status.md` Tracks table — adds a 6th row "Ephapax L3 bridge (Agda↔Coq)" after the EchoTypes.jl row landed in #161. References Coq side (`ephapax/formal/Echo.v`, 584 lines, 24 Qed, zero Admitted), the two `refl`-renames, the upstream Coq headlines, and the per-bridge-doc follow-up. * `roadmap.adoc` §Lane 4 — appends `EchoEphapaxBridge.agda` to the in-tree bridges list and adds a sentence noting it's NARROW (no Lane 4 CI dependency). Honest-scope discipline preserved across all three: ephapax-affine / L1 / L2 / L4 NOT mechanised to the same standard as L3; cf. MEMORY hooks `feedback_ephapax_affine_proofs_not_done.md`, `feedback_ephapax_no_patching_legacy_preservation.md`. Filed concurrently as follow-up issue: author `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` per-bridge doc (analogous to the existing 461-line `ECHO-CNO-BRIDGE.adoc`). Pre-existing tech-debt unrelated to this PR (NOT touched): * EchoBridges.md §1 EchoJanusBridge still lists the OLD 4-variant `JanusOp` enum; canonical surface in `EchoJanusBridge.agda` is now 8-variant `OpKind`. Drift documented in bridges-status §JanusKey row; doc refresh is the same "JanusKey" entry in §"Immediate next actions". Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/bridges/EchoBridges.md | 33 +++++++++++++++++++++++- docs/bridges/cross-repo-bridge-status.md | 1 + roadmap.adoc | 13 +++++++--- 3 files changed, 42 insertions(+), 5 deletions(-) diff --git a/docs/bridges/EchoBridges.md b/docs/bridges/EchoBridges.md index 573f048..501b77a 100644 --- a/docs/bridges/EchoBridges.md +++ b/docs/bridges/EchoBridges.md @@ -4,7 +4,7 @@ ## Overview -This document provides comprehensive documentation for the echo types bridge modules, which extend the core echo type theory to various domains including JanusKey, CNO, Tropical, and Dyadic systems. +This document provides comprehensive documentation for the echo types bridge modules, which extend the core echo type theory to various domains including JanusKey, CNO, Tropical, Dyadic, and Ephapax-L3 systems. ## Bridge Modules @@ -116,6 +116,37 @@ DyadicEchoBridgeTheorem : Σ (Session Alice) (λ S → Σ (Session Bob) (λ T → EchoSafe S × EchoSafe T × EchoDual S T)) ``` +### 5. EchoEphapaxBridge `[NARROW]` + +**Location**: `proofs/agda/EchoEphapaxBridge.agda` + +**Purpose**: Cross-repo navigability marker for the `hyperpolymath/ephapax` programming-language project, whose L3 layer (`formal/Echo.v`, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) is an explicit Coq port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K`. + +**Scope** (intentionally NARROW, per `/tmp/ephapax-bridge-proposal.md` §4): import-time documentation + two definitional `refl`-renames pinning load-bearing Agda symbols under `ephapax-L3-`-prefixed names. The cross-repo content correspondence is already discharged by `coqc` on the ephapax side; **no Lane 4 CI dependency**. + +**Key Components**: + +- **`ephapax-L3-weaken`**: definitional alias for `EchoLinear.weaken` (Coq counterpart: ephapax `formal/Echo.v` `weaken`) +- **`ephapax-L3-no-section-collapse`**: definitional alias for `EchoResidue.no-section-collapse-to-residue` (Coq counterpart: ephapax `formal/Echo.v:502-517` `no_section_collapse_to_residue`) + +**Cross-repo theorem table** (correspondence catalogued in the module docstring): + +| Agda (echo-types) | Coq (ephapax `formal/Echo.v`) | +|---|---| +| `EchoLinear` mode order (linear ≤ affine) | `mode_le_prop` | +| `EchoLinear.weaken-collapses-distinction` | `weaken_collapses_distinction` | +| Affine canonicality on `LEcho affine` | `affine_canonical`, `affine_all_equal` | +| `EchoLinear.degradeMode-comp` | `degrade_mode_comp` | +| `EchoResidue.no-section-collapse-to-residue` | `no_section_collapse_to_residue` | + +**Scope discipline (honest)**: corroboration claim is **L3 only**. Ephapax-affine has Rust checkers only (no Coq mechanisation); L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet. See `docs/echo-types/paper.adoc` §"Threats to validity" for the full honest-scope statement. + +**Main entry**: +```agda +ephapax-L3-weaken : LEcho linear → LEcho affine +ephapax-L3-weaken = weaken +``` + ## Integration Patterns ### JanusKey Integration diff --git a/docs/bridges/cross-repo-bridge-status.md b/docs/bridges/cross-repo-bridge-status.md index 641294f..df58909 100644 --- a/docs/bridges/cross-repo-bridge-status.md +++ b/docs/bridges/cross-repo-bridge-status.md @@ -16,6 +16,7 @@ touches other repositories. | JanusKey bridge | `proofs/agda/EchoJanusBridge.agda` | `januskey/src/abi/Types.idr` (`OpKind`, `IsFileOp`, `IsKeyOp`); `januskey/PROOF-NEEDS.md` | Name-bridge only — Agda side has a *local* 4-variant `JanusOp = Create \| Delete \| Modify \| Move`; canonical Idris2 ABI defines 8-variant `OpKind = Copy \| Move \| Delete \| Modify \| Obliterate \| KeyGen \| KeyRotate \| KeyRevoke` plus `IsFileOp`/`IsKeyOp` predicates. Already drifted (Create vs Copy; missing Obliterate + 3 key ops). | Decision recorded: structural-mirror the Agda enum to januskey's Idris2 `OpKind`; content-bridge deferred until januskey's `PROOF-NEEDS.md` lands content-bearing semantics. Agda↔Idris2 has no FFI, so any content-bridge must run via shared schema or trusted extraction. | | Tropical alignment | `proofs/agda/EchoTropical.agda` | `tropical-resource-typing/Tropical.thy`, `tropical-resource-typing/TropicalSessionTypes.lean` (and 8 other `.thy` files) | Adjacent repo audit complete (2026-05-20). Repo present at `repos-monorepo/verification-ecosystem/tropical-resource-typing`; remote `hyperpolymath/tropical-resource-typing` active (last push 2026-05-18, language=Isabelle). First alignable theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` ↔ Lean `add_comm_trop`+`add_assoc_trop`. | Agda cannot import `.thy` or `.lean` directly; alignment is citation-level (statement correspondence with build-side independent proof per language), not import-level. Long-game target: `Tropical_Ordinal_Bridge.thy` ↔ echo-types ordinal track. | | EchoTypes.jl executable mirror | Tier-1+Tier-2 spine + unconditional F5 OFS fragment (modules: `Echo`, `EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`, plus 2026-05-27 v0.2.0 additions: `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`, `EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`, `EchoEntropy`, `EchoObservationalEquivalence`) | [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) v0.2.0 (pinned to `e7dded6`); registered in `julia-professional-registry` | **Executable companion shipped.** Mirrors run the finite-domain shadow of the upstream theorems on concrete data and falsify-by-counterexample; the companion makes no proof claims, the Agda here remains the source of truth. R-2026-05-18 retraction surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous. UIP- and truncation-strength upgrades likewise honestly not mirrored. | — (shipped; honest scope holds verbatim from upstream). Future advances on the Tier-1+Tier-2 spine are candidates for new shadows in subsequent EchoTypes.jl releases, but no in-repo CI dependency exists in either direction. | +| Ephapax L3 bridge (Agda↔Coq) | `proofs/agda/EchoEphapaxBridge.agda` | `ephapax/formal/Echo.v` (Coq, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) — explicit port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K` | **Navigability bridge done; content bridge NARROW** (2026-05-30). Two definitional `refl`-renames: `ephapax-L3-weaken = EchoLinear.weaken` and `ephapax-L3-no-section-collapse = EchoResidue.no-section-collapse-to-residue`. Coq headlines `mode_le_prop`, `weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`, `no_section_collapse_to_residue` (line 502-517) each match an Agda counterpart pinned in `Smoke.agda`. Scope: **L3 only** — ephapax-affine has Rust checkers only; L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet (cf. ephapax `formal/PRESERVATION-DESIGN.md`, `docs/echo-types/paper.adoc` §"Threats to validity"). | Per-bridge docs `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` (CNO-equivalent) not yet authored; tracked as follow-up issue. Full content bridge (round-trip CI between Agda + Coq) would require an Agda mirror of ephapax `formal/Echo.v` and is **not foreclosed** by the NARROW stub. | ## Immediate next actions diff --git a/roadmap.adoc b/roadmap.adoc index b24d019..35c558e 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -375,10 +375,15 @@ time, so an unparking session does not re-derive the architecture. Lane 4 itself remains PARKED. *Scope question to resolve when unparking.* End-to-end verified -bridges to Janus, Tropical, CNO, etc. currently sit as in-tree -modules (`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`, -`DyadicEchoBridge.agda`) without CI-verified round-trips against the -target codebases. Two architectural options when unparking: +bridges to Janus, Tropical, CNO, Ephapax-L3, etc. currently sit as +in-tree modules (`EchoJanusBridge.agda`, `EchoTropical.agda`, +`EchoCNOBridge.agda`, `DyadicEchoBridge.agda`, +`EchoEphapaxBridge.agda`) without CI-verified round-trips against +the target codebases. `EchoEphapaxBridge` is intentionally NARROW +(definitional `refl`-renames only, no content claim — the cross-repo +content correspondence is discharged by `coqc` on the ephapax side; +see `docs/echo-types/MAP.adoc` §"Ephapax L3 — linear/affine modality +bridge"). Two architectural options when unparking: * A separate `echo-bridges-ci` repository pulling echo-types and each target as submodules; runs the verified-translation lemmas in its