Skip to content

README.adoc

Latest commit

 

History

History
236 lines (197 loc) · 10.1 KB

README.adoc

File metadata and controls

236 lines (197 loc) · 10.1 KB
Raw

Tutorial track (Lane 5 — CLOSED 2026-05-30)

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.

Important

Lane 5 status (updated 2026-05-30). CLOSED. Walkthroughs 1 (certified region-exit audit), 2 (epistemic erasure with honest bound), and 3 (provenance / debugging with layer-1 section + layer-2 no-section) are all LANDED. The originally-scaffolded triplet is complete in Agda.

  • Walkthrough 1 is the formally-accepted killer-app artefact per the second branch of roadmap.adoc §"Lane 5 [PARKED]" unblocking condition (closed-out 2026-05-30 in roadmap.adoc §"Closed lanes").

  • Walkthrough 2 follows as the second realisation, addressing the "does echo-types prove key zeroing?" category-error question.

  • Walkthrough 3 lands the dual: a positive recovery result at layer 1 paired with the negative at layer 2, making explicit which residue layer carries the load-bearing information for source reconstruction in a small fixed domain.

The Smoke gate (proofs/agda/Smoke.agda), the top-level proofs/agda/All.agda, and the identity-claim gates still do not depend on anything here. Walkthroughs are exercised via their own per-walkthrough All.agda + Smoke.agda, plus a tutorial-level aggregator at tutorial/All.agda.

1. Build

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.agda

Both must exit 0 under --safe --without-K with zero postulates. Directory names use underscores (not hyphens) so they are valid Agda module-path components.

Table of Contents

2. Three walkthroughs (planned)

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.

2.1. Walkthrough 1: certified region-exit audit (PRIORITY — killer-app candidate)

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 (own using block, 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.

2.2. Walkthrough 2: epistemic erasure with honest bound

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 the no-section lemma 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."

2.3. Walkthrough 3: provenance / debugging echo

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 on EchoExampleProvenance.agda
    EchoResidue.agda.

  • tutorial/provenance_debugging/Smoke.agda — per-walkthrough Smoke pins.

  • tutorial/provenance_debugging/All.agda — walkthrough-local aggregator, imported by tutorial/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.

3. Discipline that applies to all three walkthroughs

The same constraints that govern the rest of the repo apply verbatim:

  • --safe --without-K throughout.

  • Zero postulates, zero escape pragmas, no funext.

  • Every headline theorem pinned in the per-walkthrough Smoke (own using block, header comment).

  • Every new Agda module imported into the walkthrough’s All.agda (and optionally into the top-level proofs/agda/All.agda if the walkthrough exposes a reusable lemma).

  • Per-walkthrough README.adoc opens with the honest bound, not with the punchline.

  • Cross-references to docs/retractions.adoc where 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).

4. Killer-app close-out (ACCEPTED 2026-05-30)

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.

5. References

  • 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