agda: add concrete echo bridge model for CNO

Author: hyperpolymath

absolute-zero/README.adoc

@@ -210,7 +210,8 @@ See [VERIFICATION.md](VERIFICATION.md) for detailed status and [PROOF-INSIGHTS.m
 Agda bridge note:
 
 * `proofs/agda/EchoBridgeScaffold.agda` is now present as a compile-safe adapter layer to connect CNO identity witnesses to the echo/fiber shape used in `echo-types`.
-* Concrete import-level integration with `CNO.agda` remains gated until unfinished holes in `CNO.agda` are closed.
+* `proofs/agda/EchoBridgeCNO.agda` now provides a concrete `Program`/`eval` model instantiation into that scaffold.
+* This concrete bridge currently uses a function-extensionality parameter to convert `state-eq` into propositional equality for `Echo`.
 
 **Coq Proof Status** (2026-02-05): 81 Qed / 19 Admitted / 6 Defined / 63 Axioms across 10 files. 4 files fully complete (CNO.v, CNOCategory.v, StatMech.v, StatMech_helpers.v).
 

absolute-zero/proofs/agda/EchoBridgeCNO.agda

@@ -0,0 +1,47 @@
+-- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval.
+--
+-- Note: CNO identity is phrased as state-eq, so we parameterize by
+-- function extensionality to recover propositional equality of states.
+
+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; echo-from-cno)
+
+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

absolute-zero/proofs/agda/README.adoc

@@ -2,8 +2,9 @@
 
 This directory currently contains:
 
-* `CNO.agda` — main Agda CNO development (currently includes unfinished holes).
+* `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`
 
@@ -16,10 +17,20 @@ It provides:
 * `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 takes a function-extensionality parameter to derive propositional
+state equality for `Echo`.
+
 == Integration plan
 
-1. Finish the remaining holes in `CNO.agda`.
-2. Add a concrete model instantiation from `CNO.Program` / `eval` into `CNOModel`.
-3. Add reciprocal consistency checks against:
+1. Add reciprocal consistency checks against:
 * `echo-types` (`proofs/agda/EchoCNOBridge.agda`)
 * this repository's Coq/Lean CNO statements.