From 542a89a103817a8ed02069bfbb846324bf0d58d5 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 27 May 2026 11:29:43 +0100
Subject: [PATCH] feat(proofs/agda): upstream Echo/CNO bridge files from
 maa-framework vendored copy
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The maa-framework repo carries a vendored copy of absolute-zero with 3
Agda files added directly to proofs/agda/ that were never upstreamed
back to canonical absolute-zero:

- EchoBridgeScaffold.agda — compile-safe interface layer providing
  the `Echo` Σ-shape and `CNOModel` interface, intentionally
  independent of CNO.agda so it stays typecheckable while CNO.agda
  is being completed.
- EchoBridgeCNO.agda — concrete model instantiation from CNO.Program
  and CNO.eval into the scaffold interface. Two bridges: identity via
  CNO.state-eq directly (echo-from-cno-program-rel), and propositional
  equality recovery via Extensionality.
- README.adoc — describes the three-file structure of proofs/agda/.

These files self-identify as absolute-zero artefacts (the README.adoc
title is "Agda Proofs (absolute-zero)" and EchoBridgeScaffold's
comment says "Echo/CNO Agda bridge scaffold"), so canonical home is
here — not in maa-framework. The maa-framework re-vendor in
maa-framework#83 has to use rsync --filter='P ...' to preserve them
across syncs; landing them upstream removes that need.

Discovered while triaging maa-framework's proof-debt classification
(maa-framework#82 / maa-framework#84). The 3-file set has no
postulates; `EchoBridgeCNO.agda` imports `Axiom.Extensionality.Propositional`
as a *type* used as a module parameter (not a postulate). Documented
this false-positive case in docs/proof-debt.md so check-trusted-base.sh
(standards#211) passes without inline annotation.

Refs: maa-framework#82, maa-framework#84, standards#203, standards#211.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 docs/proof-debt.md                  | 15 +++++++
 proofs/agda/EchoBridgeCNO.agda      | 68 +++++++++++++++++++++++++++++
 proofs/agda/EchoBridgeScaffold.agda | 62 ++++++++++++++++++++++++++
 proofs/agda/README.adoc             | 38 ++++++++++++++++
 4 files changed, 183 insertions(+)
 create mode 100644 proofs/agda/EchoBridgeCNO.agda
 create mode 100644 proofs/agda/EchoBridgeScaffold.agda
 create mode 100644 proofs/agda/README.adoc

diff --git a/docs/proof-debt.md b/docs/proof-debt.md
index 337322c..2140f18 100644
--- a/docs/proof-debt.md
+++ b/docs/proof-debt.md
@@ -334,6 +334,21 @@ the bottom.
 4. The `check-trusted-base` CI job (standards#211) ensures markers
    are never un-annotated AND un-enumerated simultaneously.
 
+## False positives (no markers; script over-matches)
+
+### `proofs/agda/EchoBridgeCNO.agda` — `Axiom.Extensionality` import
+
+`check-trusted-base.sh`'s grep matches the line
+`open import Axiom.Extensionality.Propositional using (Extensionality)`
+at L11 as if it were an axiom declaration. It is not — it imports the
+`Extensionality` type, which is then accepted as an *explicit module
+parameter* by every downstream function that needs it
+(`program-state-model`, `program-rel-bridge`, etc.). The file
+introduces zero postulates and zero axioms; extensionality is
+propagated from the caller as a hypothesis.
+
+Listed here to satisfy the script's path-enumeration clause.
+
 ## Companion documents
 
 - [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit.
diff --git a/proofs/agda/EchoBridgeCNO.agda b/proofs/agda/EchoBridgeCNO.agda
new file mode 100644
index 0000000..c1fe97b
--- /dev/null
+++ b/proofs/agda/EchoBridgeCNO.agda
@@ -0,0 +1,68 @@
+-- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval.
+--
+-- Primary bridge: use CNO.state-eq directly as the relation in EchoRel.
+-- Secondary bridge: recover propositional equality with extensionality.
+
+module EchoBridgeCNO where
+
+open import Level using (zero)
+open import Data.Product using (_,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Axiom.Extensionality.Propositional using (Extensionality)
+
+import CNO
+open import EchoBridgeScaffold using
+  ( CNOModel
+  ; Echo
+  ; EchoRel
+  ; echo-from-cno
+  ; echo-from-rel
+  )
+
+echo-from-cno-program-rel :
+  (p : CNO.Program) →
+  CNO.IsCNO p →
+  (s : CNO.ProgramState) →
+  EchoRel (CNO.eval p) CNO.state-eq s
+echo-from-cno-program-rel p cno s =
+  echo-from-rel (CNO.eval p) CNO.state-eq s s
+    (CNO.IsCNO.cno-identity cno s)
+
+absolute-zero-echo-rel :
+  (s : CNO.ProgramState) →
+  EchoRel (CNO.eval CNO.absolute-zero) CNO.state-eq s
+absolute-zero-echo-rel s =
+  echo-from-cno-program-rel CNO.absolute-zero CNO.absolute-zero-is-cno s
+
+state-eq→≡ :
+  Extensionality zero zero →
+  ∀ {s₁ s₂ : CNO.ProgramState} →
+  CNO.state-eq s₁ s₂ → s₁ ≡ s₂
+state-eq→≡ ext {CNO.mk-state m₁ r₁ i₁ pc₁} {CNO.mk-state m₂ r₂ i₂ pc₂}
+             (m-eq , r-eq , io-eq , pc-eq)
+  rewrite ext m-eq | r-eq | io-eq | pc-eq = refl
+
+program-state-model : Extensionality zero zero → CNOModel CNO.ProgramState
+program-state-model ext = record
+  { Op = CNO.Program
+  ; run = CNO.eval
+  ; IsCNO = CNO.IsCNO
+  ; cno-identity = λ cno s →
+      state-eq→≡ ext (CNO.IsCNO.cno-identity cno s)
+  }
+
+echo-from-cno-program-≡ :
+  (ext : Extensionality zero zero) →
+  (p : CNO.Program) →
+  CNO.IsCNO p →
+  (s : CNO.ProgramState) →
+  Echo (CNO.eval p) s
+echo-from-cno-program-≡ ext p cno s =
+  echo-from-cno (program-state-model ext) p cno s
+
+absolute-zero-echo-≡ :
+  (ext : Extensionality zero zero) →
+  (s : CNO.ProgramState) →
+  Echo (CNO.eval CNO.absolute-zero) s
+absolute-zero-echo-≡ ext s =
+  echo-from-cno-program-≡ ext CNO.absolute-zero CNO.absolute-zero-is-cno s
diff --git a/proofs/agda/EchoBridgeScaffold.agda b/proofs/agda/EchoBridgeScaffold.agda
new file mode 100644
index 0000000..60c227a
--- /dev/null
+++ b/proofs/agda/EchoBridgeScaffold.agda
@@ -0,0 +1,62 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Echo/CNO Agda bridge scaffold.
+--
+-- This module is intentionally independent from `CNO.agda` so it can
+-- stay typecheckable while that file is still being completed.
+
+module EchoBridgeScaffold where
+
+open import Agda.Primitive using (Level; lsuc; _⊔_)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (Σ; _,_)
+open import Agda.Builtin.Unit using (⊤; tt)
+
+-- Canonical echo/fiber shape used by echo-types.
+Echo : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Set (a ⊔ b)
+Echo {A = A} f y = Σ A (λ x → f x ≡ y)
+
+-- Relation-indexed fiber shape, useful when identity is stated up to
+-- a semantic relation instead of propositional equality.
+EchoRel :
+  ∀ {a b r} {A : Set a} {B : Set b} →
+  (A → B) → (B → B → Set r) → B → Set (a ⊔ r)
+EchoRel {A = A} f _≈_ y = Σ A (λ x → _≈_ (f x) y)
+
+echo-from-rel :
+  ∀ {a b r} {A : Set a} {B : Set b}
+  (f : A → B) (_≈_ : B → B → Set r)
+  (x : A) (y : B) →
+  _≈_ (f x) y →
+  EchoRel f _≈_ y
+echo-from-rel _ _ x _ rel = x , rel
+
+-- Minimal interface needed to connect a CNO model to echoes.
+record CNOModel {ℓs ℓo : Level} (State : Set ℓs) : Set (lsuc (ℓs ⊔ ℓo)) where
+  field
+    Op           : Set ℓo
+    run          : Op → State → State
+    IsCNO        : Op → Set (ℓs ⊔ ℓo)
+    cno-identity : ∀ {op} → IsCNO op → (s : State) → run op s ≡ s
+
+open CNOModel public
+
+-- Any CNO witness yields an echo at any visible state.
+echo-from-cno :
+  ∀ {ℓs ℓo} {State : Set ℓs}
+  (M : CNOModel {ℓs} {ℓo} State)
+  (op : Op M) → IsCNO M op →
+  (s : State) → Echo (run M op) s
+echo-from-cno M op cno s = s , cno-identity M cno s
+
+-- A tiny closed model kept here as a local smoke witness.
+TrivialModel : CNOModel ⊤
+TrivialModel = record
+  { Op = ⊤
+  ; run = λ _ s → s
+  ; IsCNO = λ _ → ⊤
+  ; cno-identity = λ _ _ → refl
+  }
+
+trivial-echo : Echo (run TrivialModel tt) tt
+trivial-echo = echo-from-cno TrivialModel tt tt tt
diff --git a/proofs/agda/README.adoc b/proofs/agda/README.adoc
new file mode 100644
index 0000000..8dd2f60
--- /dev/null
+++ b/proofs/agda/README.adoc
@@ -0,0 +1,38 @@
+= Agda Proofs (absolute-zero)
+
+This directory currently contains:
+
+* `CNO.agda` — main Agda CNO development (compiles locally).
+* `EchoBridgeScaffold.agda` — compile-safe interface layer for bridging CNO identity witnesses to the echo/fiber shape used in `echo-types`.
+* `EchoBridgeCNO.agda` — concrete model instantiation from `CNO.Program` / `eval` into the scaffold interface.
+
+== Purpose of `EchoBridgeScaffold.agda`
+
+The scaffold avoids importing `CNO.agda` directly so this bridge path can
+remain typecheckable while `CNO.agda` is still being completed.
+
+It provides:
+
+* `Echo` as `Σ x , f x ≡ y`.
+* `CNOModel` interface with `run`, `IsCNO`, and `cno-identity`.
+* `echo-from-cno` conversion from a CNO witness to an echo witness.
+
+== Purpose of `EchoBridgeCNO.agda`
+
+This module imports `CNO.agda` and instantiates `CNOModel` concretely with:
+
+* `Op = Program`
+* `run = eval`
+* `IsCNO = IsCNO`
+
+Because `CNO.cno-identity` is phrased as `state-eq` (with function-valued memory),
+the bridge provides two layers:
+
+* primary: relation-based echoes via `EchoRel ... CNO.state-eq` (no extensionality needed);
+* secondary: propositional `Echo` corollaries via a function-extensionality parameter.
+
+== Integration plan
+
+1. Add reciprocal consistency checks against:
+* `echo-types` (`proofs/agda/EchoCNOBridge.agda`)
+* this repository's Coq/Lean CNO statements.