Skip to content

Commit b0f5f21

Browse files
committed
Link cross-repo roadmap to absolute-zero Agda bridge slot
1 parent d87781b commit b0f5f21

3 files changed

Lines changed: 5 additions & 0 deletions

File tree

README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,7 @@ Note: `januskey` is not currently nested under `maa-framework` in this workspace
9090
Cross-repo status:
9191

9292
- bridge formalisms live in this repo (`EchoCNOBridge`, `EchoJanusBridge`, tropical-collapse witness work in `EchoTropical`)
93+
- Agda-side adapter slot now exists in `maa-framework/absolute-zero` at `absolute-zero/proofs/agda/EchoBridgeScaffold.agda`
9394
- end-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here
9495
- see `docs/echo-types/roadmap.md` for staged cross-repo verification gates
9596

docs/echo-types/roadmap.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,9 @@ Paths marked **[unblocked]** can proceed today. Paths marked
121121
type infrastructure.
122122
- **[gated on B2]** CNO-equivalence verification across echo-types
123123
and `absolute-zero`. Needs cross-repo access.
124+
Bridge slot now exists on the adjacent side at
125+
`absolute-zero/proofs/agda/EchoBridgeScaffold.agda`; theorem-level
126+
alignment remains open.
124127
- **[gated on B2]** Janus reversible-file-operations bridge
125128
verification against `januskey`'s actual API. Needs cross-repo
126129
access.

readme.adoc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ Note: `januskey` is not currently nested under `maa-framework` in this workspace
9696
Cross-repo status:
9797

9898
* Bridge formalisms live in this repo (`EchoCNOBridge`, `EchoJanusBridge`, tropical-collapse witness work in `EchoTropical`).
99+
* Agda-side adapter slot now exists in `maa-framework/absolute-zero` at `absolute-zero/proofs/agda/EchoBridgeScaffold.agda`.
99100
* End-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here.
100101
* See `docs/echo-types/roadmap.md` for staged cross-repo verification gates.
101102

0 commit comments

Comments
 (0)