Skip to content

docs: past-present-future doctrine (STATUS + PROOF-NEEDS rewrite + README banner + L3 diagram + .v signposts) #184

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 27, 2026
Merged

docs: past-present-future doctrine (STATUS + PROOF-NEEDS rewrite + README banner + L3 diagram + .v signposts) #184

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
296 changes: 251 additions & 45 deletions PROOF-NEEDS.md
View file
Open in desktop

Large diffs are not rendered by default.

249 changes: 213 additions & 36 deletions README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,47 @@ repo*, one Rust crate, one AST, two structural disciplines. **`ephapax-affine`
is not AffineScript.** When ambiguous, write "ephapax-affine sublanguage"
vs "AffineScript language".

Canonical disambiguation:
Canonical disambiguation (read this before applying any cross-repo
lesson):
link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md[nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md].
====

A dyadic linear+affine type system for compile-time WebAssembly
memory safety. Resources are tracked through the type system so the
compiler can guarantee — without a garbage collector — that no value
is used after being freed, no resource is leaked, and region-scoped
allocations are deallocated in bulk at scope exit.
[WARNING]
.🔄 Foundational redesign in progress — read `STATUS.adoc` before opening any `.v` file
====
On 2026-05-26 a verified Coq counterexample
(link:formal/Counterexample.v[`formal/Counterexample.v`], 5 Qed
lemmas) showed that preservation as stated in the legacy typing
judgment is **provably false**. The repo is in the middle of a
*four-layer principled redesign* (regions / modality / echo / dyadic
mode) where preservation is *re-derived per layer* from explicit
invariants rather than forced through the old judgment.

Anything in this README dated before 2026-05-26 that describes a
"preservation closure plan" or counts "910 → 22 → 12 open goals" is
**archaeology, not instructions**. The authoritative status is in
link:STATUS.adoc[`STATUS.adoc`] (past / present / future map),
link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`]
(four-layer architecture), and link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]
(per-sublanguage proof debt with explicit do-not-do list).

Quick read: **L1** (region capabilities) substantially complete;
**L2** (Linear/Affine modality) core landed with zero axioms; **L3**
(echo / residue) calculus done locally, integration into the typing
judgment is the next-block work; **L4** (dyadic mode) not started.
====

Ephapax is a research language for **principled handling of
irreversible boundaries** (region exits, drops, key erasure, audit
trails) in compile-time-memory-safe WebAssembly. Real systems are
irreversible — operating systems deallocate, databases drop tables,
security systems erase keys, compilers collapse high-level
distinctions. Ephapax gives a disciplined, machine-checkable
framework to handle those boundaries responsibly: the type system
tracks not just *what is owned* but *what was lost when it was given
up*, so reclamation can carry mandatory evidence where it matters
(audit, compliance, cryptographic erasure) and degrade to free where
it doesn't (inference loops, hot paths).

The core calculus is mechanically formalised. Soundness theorems on
the dynamic side (Coq) and structural-safety theorems on the type
Expand Down Expand Up @@ -95,6 +127,94 @@ Ephapax is a programming language with:
reference counting, no allocator-per-object metadata.
|===

== Three superpowers

The L3 echo / residue layer (Ephapax's contribution to the four-layer
design) opens three things proper reversible programming struggles
with:

[cols="1,3"]
|===
| Superpower | What it gives you

| **A. Accountability of irreversible reclamation**
| You can free memory (`S_Region_Exit`, `S_Drop`) and the type system
*knows* you lost the data — and tracks what depended on it. Under
the Linear modality the reclamation event carries a mandatory
evidence-bearing `Echo` value; under Affine you opt out for
performance. Pairs cleanly with region-based memory management
(deterministic bulk free) to deliver high-assurance reclamation
that tracing GC cannot — by design, tracing GC *hides* the
reclamation evidence.

| **B. Selective reversibility (thin-poset)**
| Linear ≤ Affine is a two-point thin poset at the L2 modality. You
pick per-region (or per-project) which discipline applies. Same
code shape, different evidence obligations. Concrete examples:
*Linear* during backpropagation (must keep the gradient residue);
*Affine* during inference (drop the residue, save memory). You get
the safety of reversibility where you need it, and the performance
of irreversibility where you don't.

| **C. Debugging + provenance**
| Attach Linear Echoes to critical state changes. The type system
guarantees the receipt (preimage) of that state change was retained
— so when a bug fires, the inputs that produced the error are
recoverable by construction. In Affine mode you opt out of this
debugging info, with the same code shape. The evidence is a
*theorem-level guarantee*, not a runtime convention.
|===

[CAUTION]
.Echo Types are NOT a tracing-GC replacement
====
Echo Types do **not** solve reachability or cycles. They are not a
"fire-and-forget" automatic memory manager. Their strength is
*accountability of irreversible reclamation* in systems that already
know when and how to deallocate (regions, explicit drop, deterministic
ownership). Treating them as competition for mark-and-sweep or
generational GC is a category error.

The committed v1 direction is *Linear Echo + Region-Based Memory
Management* (deterministic bulk free with mandatory certified
evidence). A speculative future direction is an optional Linear
discipline on deterministic Rust-style drop for critical resources
(keys, sensitive buffers requiring provable erasure) — flagged but
not committed.
====

== What this enables

The three superpowers translate to concrete use cases the type
system can *prove* properties about:

* **Mandatory evidence for critical actions.** By making certain
echoes Linear (mandatory observation), the type system guarantees
that a region exit *always* emits an audit trail, or that a drop
*always* triggers a required cleanup.

* **GDPR "right to be forgotten" with certified evidence of
erasure.** Linear-echo discipline on the `S_Drop` of a personal-data
resource is a type-level proof that erasure happened *and* that the
required notification / log was produced. Auditors get a
machine-checkable artefact instead of a process attestation.

* **Verified resource management for keys, secrets, and sensitive
buffers.** Linear-echo on the deallocation of a key buffer
guarantees provable erasure; the typing rule cannot be silenced.

* **Selective reversibility without redesigning your language.**
The thin-poset means you don't redesign the runtime to be
bijective. You add *one* type former (the fiber) and layer
existing L2 modalities over it. Orthogonal and compositional.

* **Machine-checkable foundation for policy enforcement.** The
thin-poset Linear ≤ Affine + the proven non-invertibility
(`EchoResidue.no-section-collapse-to-residue`) gives sharp,
proof-relevant reasoning: *weakening obligations is allowed*,
*strengthening them back is impossible*. Clean logical foundation
for compliance work.

== What this isn't

* **Not Rust.** Rust uses ownership + borrowing with a single discipline
Expand Down Expand Up @@ -226,25 +346,46 @@ Two complementary formalisations, both run on every push:
=== Coq (`formal/`)

Operational semantics with small-step reduction over a substitution-
based calculus. Proves dynamic properties (no stuck states, region
exits free everything, substitution preserves typing).

Currently `Qed`-closed: `no_leaks`, `subst_preserves_typing`,
`typing_ctx_transfer`, `region_env_perm_typing`, `region_add_typing`,
`region_shrink_preserves_typing`, plus 70+ supporting lemmas.

Currently `Admitted`: `preservation`. **12 open goals remain** after
the reduction chain — down from **910** at the start of the campaign
(98.7% reduction across PRs #92 / #102 / #104 / #106 / #114 / #116 /
#117 / #121, 2026-05-20 → 2026-05-21). Phase 1 scaffold of the
closure plan (Lemma B `step_output_context_eq`) landed; per-case
discharges next. The remaining 12 are 11 congruence cases (blocked
on Lemma B's per-case proofs — linearity-context drift between IH
and sibling) + 1 `S_Region_Step + T_Region_Active` case (blocked on
region-env weakening for non-values). Canonical closure path:
**`ROADMAP.adoc` §"Preservation closure plan"** (5 phases, ~3
sessions of focused work). See also `formal/PRESERVATION-HANDOFF.md`
for the per-case diagnostic record.
based calculus. Post-2026-05-26 the formalisation is layered:

* **Legacy** (`formal/Semantics.v`, `formal/Typing.v`) — the original
pre-discovery judgment. `Theorem preservation` here is **provably
false** (the counterexample at `formal/Counterexample.v` is 5 Qed
lemmas proving it). The `Admitted.` is correct. **Do not extend.**
Treat as archaeology — see link:STATUS.adoc[`STATUS.adoc`] for the
pre-discovery PR list and the explicit do-not-do reasoning.

* **Layer 1 — region capabilities** (`formal/TypingL1.v`,
`formal/Semantics_L1.v`). The new judgment is modality-indexed
(`has_type_l1 m : ...`) and threads a capability environment `R`
through compound rules. Judgment 100% (0 admits, 2 Qed); semantics
carries 9 supporting-lemma admits that are *L2-integration debt*
(bullet-structure rewrites for new Affine-only constructors), not
legacy patching.

* **Layer 2 — structural modality** (`formal/Modality.v`). Linear
vs Affine as a K-free thin-poset decoration. `linear_to_affine`
is **Qed with zero axioms**. Landed via PRs #176 + #177.

* **Layer 3 — echo / residue** (`formal/Echo.v`). 12 Qed lemmas
covering the fiber calculus, degrade map, and the
`no-section-collapse-to-residue` irreversibility theorem (mirrors
the upstream Agda development at
https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`]).
Calculus is done; *wiring into the typing rules* (`T_Observe`,
collapse-function emission on irreversible steps,
`G`-context threading) is the next-block work.

* **Layer 4 — dyadic interaction**. Design in
link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md §7`].
Not started.

Per-sublanguage proof debt with explicit do-not-do list lives in
link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]. The four-layer architecture
rationale is in
link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`].
The counterexample itself is
link:formal/Counterexample.v[`formal/Counterexample.v`] (5 Qed).

[source,bash]
----
Expand Down Expand Up @@ -379,9 +520,25 @@ generics, effects, traits, comptime, contracts) lives on
| ✅ Qed
|

| Coq `preservation`
| 🟡 Admitted (22 open / 910 closed)
| Multi-day proof-engineering campaign in flight
| Coq legacy `preservation`
| 🛑 Admitted — provably false
| Counterexample at `formal/Counterexample.v` (5 Qed). Not closable. Archaeology.

| Coq L1 (region capabilities)
| ✅ Judgment 100%; 🟡 semantics 9 admits
| 9 admits = L2-integration debt. See `PROOF-NEEDS.md`.

| Coq L2 (modality)
| ✅ Core landed (PRs #176 + #177); 0 axioms
| `linear_to_affine` Qed. Integration debt absorbed by L1 admits above.

| Coq L3 (echo / residue calculus)
| ✅ 12 Qed, 0 admits
| Calculus done locally; integration into typing rules pending.

| Coq L4 (dyadic interaction)
| 🔲 Not started
| Design in `formal/PRESERVATION-DESIGN.md §7`.

| Idris2 region-linearity theorems
| ✅ Complete (zero unsafe)
Expand All @@ -405,21 +562,41 @@ generics, effects, traits, comptime, contracts) lives on
| link:README.adoc[README]
| You are here. Overview + quickstart.

| link:STATUS.adoc[STATUS.adoc]
| **Past / present / future map.** Single page that answers "where
are we?" Read this before any `.v` file or any PR comment dated
before 2026-05-26.

| link:PROOF-NEEDS.md[PROOF-NEEDS.md]
| Per-sublanguage proof debt audit. What's done (Qed), what's todo,
what's banned (anti-pattern detector). Separated for ephapax-linear
and ephapax-affine sublanguages.

| link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md]
| **Canonical four-layer design doctrine.** Why the counterexample
forced the redesign, the four orthogonal concerns, per-layer plans.

| link:formal/Counterexample.v[formal/Counterexample.v]
| The 5 Qed lemmas that pin the soundness gap of the legacy judgment.
Authoritative source of the gap; future proofs must coexist with it.

| link:CLAUDE.md[CLAUDE.md]
| Agent guidance. Carries the 2026-05-27 owner directive,
anti-pattern detector, escalation rule.

| link:EXPLAINME.adoc[EXPLAINME.adoc]
| "Show me the receipts" — every claim in this README backed by a
specific file, test, or proof.

| link:ROADMAP.adoc[ROADMAP.adoc]
| Quantitative milestones (v0.1.0 → v1.0.0), per-version checklists,
current open work.

| link:PROOF-NEEDS.md[PROOF-NEEDS.md]
| Outstanding proof obligations: what's `Admitted` / `covering` /
`partial` and why.
| Milestones (v0.1.0 → v1.0.0), per-version checklists, current open
work. Note: any pre-2026-05-26 closure-plan content is superseded
by STATUS.adoc + PRESERVATION-DESIGN.md.

| link:formal/PRESERVATION-HANDOFF.md[formal/PRESERVATION-HANDOFF.md]
| Per-case checklist for the 22 remaining preservation goals. Read
this if you're picking up the Coq proof work.
| **Archaeology only** — historical diagnostic record of the
pre-counterexample closure attempts. Reads as a closure plan; isn't
one. Useful only for understanding *why* the redesign happened.

| link:RUST-SPARK-STANCE.adoc[RUST-SPARK-STANCE.adoc]
| Stance on Rust + SPARK interop and where Ephapax fits.
Expand Down
Loading
Loading