Tutorial track for the echo-types identity claim. Lane 5 closed
2026-05-30 with Walkthrough 1 formally accepted as the killer-app
example, satisfying the second branch of the unblocking condition
in roadmap.adoc §"Closed lanes" without waiting for Lane 1.
The tutorial tree lives at the repo root rather than under
proofs/agda/. Build it with the repo root added to the Agda
include path:
agda --library-file=/tmp/agda-libs -i . -i proofs/agda \
tutorial/All.agda
agda --library-file=/tmp/agda-libs -i . -i proofs/agda \
tutorial/region_exit_audit/Smoke.agdaBoth must exit 0 under --safe --without-K with zero postulates.
Directory names use underscores (not hyphens) so they are valid
Agda module-path components.
When Lane 5 unparks, three walkthroughs land in this directory in
priority order. The order reflects the user’s suggestion captured
in roadmap.adoc §Lane 5: the certified region-exit audit comes
first because it ties to an active adjacent project (ephapax L3),
demonstrates the affine-mode discipline at a real audit boundary,
and is the candidate killer-application example.
Status. Design-doc only. Agda lands at unpark time.
Adjacent project. hyperpolymath/ephapax — programming language
with linear types guaranteeing memory safety for WebAssembly. The
"L3" layer in CLAUDE.md memory entries refers to ephapax’s
region-based memory discipline.
The pedagogy. Model an ephapax-style region as an Agda type
Region with a freshen/exit pair. Every S_Region_Exit step
produces a consumed LEcho affine whose payload is the audit
receipt — what was released and to whom. The Echo’s
no-section-weaken provides the machine-checked guarantee that no
post-exit caller can reconstruct the un-degraded source from the
audit receipt alone. The walkthrough closes by exhibiting the
honest bound: the audit guarantee is about the type-level witness,
NOT about in-memory bytes being zeroed. (See Walkthrough 2 for the
matched-negative on that category error.)
Files when landed.
-
tutorial/region_exit_audit/README.adoc— narrative walkthrough with the design rationale and the bound disclosure up front. -
tutorial/region_exit_audit/RegionExitAudit.agda— the worked example. Builds under--safe --without-K, zero postulates. -
tutorial/region_exit_audit/Smoke.agda— per-walkthrough Smoke pins (ownusingblock, header comment) per CLAUDE.md "Working rules".
Why this is the killer-app candidate. Tied to an active adjacent project (real consumer pressure), concrete (one named audit boundary, not a class of boundaries), exhibits the affine mode at the interesting discipline (consumed-on-exit, not just weakened-once), and the matched-negative (no-zeroing claim) is honest about the category error a sceptic would catch.
Status. LANDED 2026-05-27. See
tutorial/epistemic_erasure/EpistemicErasure.agda for the worked
example and tutorial/epistemic_erasure/README.adoc for the
narrative.
The pedagogy. Model a key-derivation function kdf : Seed → Key
where the visible output is the derived Key and the hidden source
is the Seed. Echo kdf k retains the seed at the type level;
no-section-collapse (factored through EchoResidue) is the
machine-checked guarantee that no pure-Agda function recovers the
seed from the key alone.
The crucial honest disclosure. This is not a claim that
in-memory bytes of the seed have been zeroed. Conflating the two
is a category error a sceptic will catch — exactly the kind of
mistake the project’s retraction discipline (docs/retractions.adoc)
exists to prevent. The walkthrough opens with the disclosure, then
states the actual claim (no-section at the type level), then walks
the proof.
Files when landed.
-
tutorial/epistemic_erasure/README.adoc— narrative with the bound disclosure as the opening sentence, not a footnote. -
tutorial/epistemic_erasure/EpistemicErasure.agda— the worked example with theno-sectionlemma front and centre. -
tutorial/epistemic_erasure/Smoke.agda— per-walkthrough Smoke pins.
Why this walkthrough exists. Sceptics walking into the repo will ask "so does echo-types prove key zeroing?". The honest answer is "no, and the walkthrough exists to explain what it does prove instead, before that miscommunication takes root in any write-up of echo for an applied audience."
Status. LANDED 2026-05-27. See
tutorial/provenance_debugging/ProvenanceDebugging.agda for the
worked example and tutorial/provenance_debugging/README.adoc for
the narrative.
The pedagogy. A 4-element State with two orthogonal sign bits.
The visible output of the echo is the first sign (firstSign :
State → Bool); the residue carrier at layer 1 is the second sign
(secondSign : State → Bool). The walkthrough walks the source
through three layers — full echo, class residue, trivial residue
— and exhibits the load-bearing contrast: at layer 1 a section
exists (recover-from-class is a right inverse of
state-to-class); at layer 2 no section exists
(no-recovery-from-trivial, mirroring the structural argument of
EchoResidue.no-section-collapse-to-residue). The pair is
packaged as provenance-walk-contrast. The mechanical content:
secondSign is injective within each firstSign-fibre, which is
exactly the property that makes the layer-1 recovery work.
The crucial honest disclosure. This walkthrough is not a
runtime debugger. It is a type-level statement about which
residue layer carries the load-bearing information for source
reconstruction in a fixed 4-element domain. Conflating it with
operational debugging is a category error — exactly the kind of
mistake the project’s retraction discipline
(docs/retractions.adoc) exists to prevent. The walkthrough opens
with the disclosure, then states the actual claims (layer-1
section + layer-2 no-section), then walks the proofs.
Files when landed.
-
tutorial/provenance_debugging/README.adoc— narrative with the bound disclosure as the opening sentence, not a footnote. -
tutorial/provenance_debugging/ProvenanceDebugging.agda— the worked example, building onEchoExampleProvenance.agda
EchoResidue.agda. -
tutorial/provenance_debugging/Smoke.agda— per-walkthrough Smoke pins. -
tutorial/provenance_debugging/All.agda— walkthrough-local aggregator, imported bytutorial/All.agda.
Why this walkthrough exists. The two harder walkthroughs (audit, erasure) both ship as one-sided no-section content where information is not recoverable. This third walkthrough exhibits the dual: a positive recovery result paired with the negative, making explicit which residue layer is load-bearing for reconstruction. It is the gentlest of the three; readers who bounce off the audit and erasure walkthroughs land here.
The same constraints that govern the rest of the repo apply verbatim:
-
--safe --without-Kthroughout. -
Zero postulates, zero escape pragmas, no funext.
-
Every headline theorem pinned in the per-walkthrough Smoke (own
usingblock, header comment). -
Every new Agda module imported into the walkthrough’s
All.agda(and optionally into the top-levelproofs/agda/All.agdaif the walkthrough exposes a reusable lemma). -
Per-walkthrough
README.adocopens with the honest bound, not with the punchline. -
Cross-references to
docs/retractions.adocwhere a narrowed claim is being used (e.g. walkthrough 2’s no-key-zeroing disclosure is the same discipline as the R-2026-05-18 narrowings).
roadmap.adoc §"Closed lanes" records the killer-app branch of the
unblocking condition as fired: Walkthrough 1
(tutorial/region_exit_audit/RegionExitAudit.agda) is formally
accepted as the killer-app example. The acceptance rests on the
three items in §"Walkthrough 1 > Why this is the killer-app
candidate" — concrete audit boundary, ephapax-L3 corroboration,
machine-checked Linear-Echo discipline. Lane 5 closed on that basis
without waiting for Lane 1.
-
roadmap.adoc§"Closed lanes" — Lane 5 close-out entry -
CLAUDE.md§"Ecosystem context" — ephapax row -
proofs/agda/EchoLinear.agda—LEcho,weaken,no-section-weaken -
proofs/agda/EchoResidue.agda—EchoR,collapse-to-residue,no-section-collapse-to-residue -
proofs/agda/EchoExampleProvenance.agda— provenance example walkthrough 3 builds on -
docs/retractions.adoc— the discipline walkthrough 2’s honest-bound disclosure inherits