Skip to content

Commit ede406b

Browse files
claudeclaude
committed
docs(wiki): add wiki docs/wikis/ — Home page with proof status + disambiguation
Create docs/wikis/Home.md with Ephapax project overview, the critical ephapax-vs-affinescript disambiguation notice, current four-layer redesign proof status (L1 done, L2 landed, L3 Qed, L4 scaffold), component map, and governance section. Add 0.2-AI-MANIFEST.a2ml for the wikis directory. https://claude.ai/code/session_01PhqGcxCqkMdJtR6NWq56Hx
1 parent 412c0fc commit ede406b

2 files changed

Lines changed: 100 additions & 0 deletions

File tree

‎docs/wikis/0.2-AI-MANIFEST.a2ml‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
---
3+
### [META]
4+
id: "wikis-track"
5+
level: 2
6+
parent: "../0.1-AI-MANIFEST.a2ml"
7+
8+
---
9+
### [AI_MANIFEST]
10+
description: |
11+
Long-form collaborative documentation and project knowledge base.
12+
This directory mirrors the content structure of the project wiki.
13+
14+
invariants:
15+
- "Primary wiki format MUST be Markdown (.md) or AsciiDoc (.adoc)"
16+
- "Ephapax disambiguation notice MUST appear in Home.md"
17+
- "Proof status MUST reflect current four-layer redesign state"

‎docs/wikis/Home.md‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
# Ephapax
3+
4+
_ἐφάπαξ — once for all._
5+
6+
**A research language for principled handling of irreversible boundaries in compile-time-memory-safe WebAssembly.**
7+
8+
> ⚠️ **Not to be confused with AffineScript.** These are sibling projects that share zero AST/compiler/type checker. The word "affine" overlaps because both involve substructural logic — that's a logic-family fact, not a project relationship. Full disambiguation: [`nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md`](https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md).
9+
10+
This wiki is the *signpost* — canonical docs live in the repo. Edit [`docs/wikis/`](https://github.com/hyperpolymath/ephapax/tree/main/docs/wikis) in the code repo, not directly in the wiki UI.
11+
12+
---
13+
14+
## Start here
15+
16+
| If you want to… | Go to |
17+
|---|---|
18+
| Understand what Ephapax is | [README.adoc](https://github.com/hyperpolymath/ephapax/blob/main/README.adoc) |
19+
| See the current proof status | [STATUS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/STATUS.adoc) |
20+
| Understand the four-layer redesign | [formal/PRESERVATION-DESIGN.md](https://github.com/hyperpolymath/ephapax/blob/main/formal/PRESERVATION-DESIGN.md) |
21+
| See the per-sublanguage proof debt | [PROOF-NEEDS.md](https://github.com/hyperpolymath/ephapax/blob/main/PROOF-NEEDS.md) |
22+
| See the counterexample that invalidated the old design | [formal/Counterexample.v](https://github.com/hyperpolymath/ephapax/blob/main/formal/Counterexample.v) |
23+
| See architecture decisions | [docs/specs/DESIGN-DECISIONS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/docs/specs/DESIGN-DECISIONS.adoc) |
24+
| See machine-readable state | [.machine_readable/6a2/STATE.a2ml](https://github.com/hyperpolymath/ephapax/blob/main/.machine_readable/6a2/STATE.a2ml) |
25+
26+
---
27+
28+
## What Ephapax is
29+
30+
Ephapax is a research language for **principled handling of irreversible boundaries** — region exits, key erasure, audit trails, database drops, OS deallocations — in compile-time-memory-safe WebAssembly.
31+
32+
Real systems are irreversible. Ephapax gives a disciplined, machine-checkable framework to handle those boundaries responsibly: the type system knows when something has been consumed, when it can never be undone, and when a "once for all" commitment has been made.
33+
34+
### The dyadic design
35+
36+
Ephapax is internally dyadic — two sublanguages, one AST, one Rust crate:
37+
38+
| Sublanguage | Binding | Semantics |
39+
|---|---|---|
40+
| **ephapax-linear** | `let! x = …` | Use **exactly once**; compile error if dropped without explicit discard |
41+
| **ephapax-affine** | `let x = …` | Use **at most once**; implicit drop allowed |
42+
43+
Both compile to [typed-wasm](https://github.com/hyperpolymath/typed-wasm). The choice of sublanguage is a per-declaration annotation.
44+
45+
## Current formal proof status (2026-06-05)
46+
47+
> 🔄 **Foundational redesign in progress.** On 2026-05-26, a verified Coq counterexample ([`formal/Counterexample.v`](https://github.com/hyperpolymath/ephapax/blob/main/formal/Counterexample.v), 5 Qed lemmas) showed that preservation as stated in the legacy typing judgment is **provably false**. The old `Theorem preservation` in `Semantics.v` stays `Admitted` — this is correct. The work is the **four-layer principled redesign**.
48+
49+
The four layers and their current state:
50+
51+
| Layer | Description | Status |
52+
|---|---|---|
53+
| **L1** — Region capabilities | `R_in`, `R_out`, `In r R` threading | Substantially complete; `preservation_l1` proved conditional on L2 effect-typing |
54+
| **L2** — Structural modality | `m : Modality` in `has_type_l1`; `linear_to_affine` | Core landed (PRs #176+#177); `linear_to_affine` Qed, zero axioms; 6 supporting lemmas regressed to Admitted pending Phase D Stages 2–4 |
55+
| **L3** — Echo residue | What was lost at an irreversible step | `preservation_l3` + two companions Qed (conditional); wired into L1 |
56+
| **L4** — Dyadic mode | Project-level mode declaration | Phase A scaffold landed (`formal/L4.v`): `PModeLinear`/`PModeAffine`/`PModeBoundaryMix` + round-trip; definitions only by design |
57+
58+
**Do not** attempt to close `Theorem preservation` in `formal/Semantics.v`. It is provably false. The authoritative do/do-not list is in [`CLAUDE.md`](https://github.com/hyperpolymath/ephapax/blob/main/CLAUDE.md) under "Owner directive 2026-05-27".
59+
60+
## Component map
61+
62+
| Layer | Technology |
63+
|---|---|
64+
| Language core (type checker, parser) | Rust (`ephapax-linear/src/`) |
65+
| Formal proofs | Coq 8.18.0 (`formal/`) — 12 `.v` files |
66+
| ABI verification | Idris2 (`src/abi/Ephapax/`) |
67+
| Wasm codegen | Target: `hyperpolymath/typed-wasm` |
68+
| Governance | 6-verb contractiles; k9-svc self-validation |
69+
70+
## Relationship to other projects
71+
72+
- **[Gossamer](https://github.com/hyperpolymath/gossamer)** — desktop shell; Ephapax is its backend language
73+
- **[AffineScript](https://github.com/hyperpolymath/affinescript)** — **NOT the same project** (see disambiguation above)
74+
- **[typed-wasm](https://github.com/hyperpolymath/typed-wasm)** — shared compile target
75+
- **[IDApTIK](https://github.com/hyperpolymath/idaptik)** — game using Gossamer (Ephapax-backed) for desktop shell
76+
77+
## Governance
78+
79+
- **Licence**: MPL-2.0
80+
- **Machine-readable state**: [`.machine_readable/6a2/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/6a2/)
81+
- **Contractiles**: 6-verb governance in [`.machine_readable/contractiles/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/contractiles/)
82+
- **Security policy**: [SECURITY.md](https://github.com/hyperpolymath/ephapax/blob/main/SECURITY.md)
83+
- **Open issues**: [github.com/hyperpolymath/ephapax/issues](https://github.com/hyperpolymath/ephapax/issues)

0 commit comments

Comments
 (0)