Skip to content

Commit 57d3511

Browse files
claudeclaude
committed
feat(echo): commence AffineScript alignment — Echo Types, proofs-first
Begins moving JtV to AffineScript's maturity/governance position, starting with proofs, and accommodates the echo-types loss taxonomy in the checker. Proofs (first): - jtv_proofs/JtvEcho.lean: formalise JtV's Echo system (spec v2 §8-9) as a bounded join-semilattice (Safe ⊑ Neutral ⊑ Breaking) with the reverse-block admissibility contract (blockEcho_admissible) and the fibre correspondence with the echo-types Agda library (Echo f y := Σ x, f x = y). Wired into lakefile.lean / proof-regression CI. sorry-free. Type checker (accommodate echo-types): - crates/jtv-core/src/echo.rs: executable image of JtvEcho.lean — Echo lattice, join, admissibility, statement classifier (validated against AST stubs). - typechecker.rs: reverse blocks rejected when aggregate echo is Breaking (JtvError::EchoViolation) — realises blockEcho_admissible. + tests. Governance (adopt the AffineScript matrix discipline): - ALIGNMENT-AFFINESCRIPT.adoc: gap analysis + phased roadmap (proofs first). - verification/PROOF-CAPABILITY-MATRIX.adoc: authoritative proof-status matrix. - academic/TODO_GAPS.md: doc-truthing — proofs are sorry-free (PROOF-5 stale). - spec: anchor §8 Echo System to echo-types / JtvEcho.lean / echo.rs. Findings recorded for later phases: jtv-core does not currently compile (ast.rs ControlStmt lacks ReversibleBlock/ReverseToken/AbandonToken used by interpreter/typechecker/cli; unvendored patacl-core path dep) — contradicting STATUS.md "100% complete". https://claude.ai/code/session_01EJLZKDtcF1RGdKx6TcUTQG
1 parent fbdde90 commit 57d3511

10 files changed

Lines changed: 790 additions & 14 deletions

File tree

‎ALIGNMENT-AFFINESCRIPT.adoc‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= Julia the Viper → AffineScript Alignment Plan
4+
:toc:
5+
:toclevels: 3
6+
:revdate: 2026-06-02
7+
8+
Bring *Julia the Viper* (JtV) from its current position to the same level of
9+
*maturity and governance discipline* that `hyperpolymath/affinescript` has
10+
reached — *starting with proofs*. This document is the master plan; it is
11+
deliberately conservative and honest, in the spirit of `ROADMAP.adoc`.
12+
13+
== 1. What "AffineScript's position" means
14+
15+
AffineScript is an alpha-stage but disciplined language project. Its distinctive
16+
strength is not (only) the compiler — it is the *governance model* that keeps
17+
claims honest:
18+
19+
[cols="1,3"]
20+
|===
21+
| Asset | Description
22+
23+
| Compiler pipeline
24+
| `face syntax → core AST → type / effect / ownership checks → backend`
25+
(OCaml; sedlex + Menhir; WASM / typed-wasm backends).
26+
27+
| `docs/CAPABILITY-MATRIX.adoc`
28+
| The *single authoritative source* of feature status, using a precise
29+
six-term vocabulary: `enforced`, `works`, `partial`, `declared-but-unwired`,
30+
`parse-only`, `absent`.
31+
32+
| Doc-truthing
33+
| `tools/check-doc-truthing.sh` mechanically blocks over-claims in docs against
34+
the compiler-as-oracle test gate.
35+
36+
| `docs/TECH-DEBT.adoc`
37+
| A coordination ledger with domain prefixes (DOC / CORE / STDLIB / INT / SAT).
38+
39+
| Honest posture
40+
| Self-describes as alpha; its one known base-language soundness gap is tracked
41+
as an issue (CORE-01 / #177), not hidden.
42+
43+
| Verification locus
44+
| Verification lives at the *typed-wasm target layer*. AffineScript does **not**
45+
use a proof assistant.
46+
|===
47+
48+
== 2. Where JtV is today (honest snapshot, 2026-06-02)
49+
50+
[cols="1,3"]
51+
|===
52+
| Area | Reality
53+
54+
| Mechanized proofs
55+
| *Ahead of AffineScript.* `jtv_proofs/` has 7 Lean 4 libraries (~2,300 LOC)
56+
with *zero* `sorry` / `admit` / `axiom`, plus an Idris2 ABI (`src/abi/`) and a
57+
`proof-regression.yml` CI gate. This is JtV's strongest asset.
58+
59+
| Paper proofs
60+
| `academic/proofs/` — 7 documents (type theory, security, algebra, quantum,
61+
etc.).
62+
63+
| Rust core
64+
| `crates/{jtv-core,jtv-cli,jtv-lsp,jtv-debug}`. *Does not currently compile*
65+
(see TECH-DEBT below): `ast.rs::ControlStmt` lacks the `ReversibleBlock` /
66+
`ReverseToken` / `AbandonToken` variants that `interpreter.rs`,
67+
`typechecker.rs`, and `jtv-cli` already match on; and the workspace has an
68+
unvendored sibling path-dependency `patacl-core` (`../patacl`).
69+
70+
| Conformance
71+
| `conformance/{valid,invalid,coproc}` exists; not yet a compiler-as-oracle
72+
gate.
73+
74+
| Spec
75+
| `spec/` has `grammar.ebnf`, a v2 type system (`jtv_v2_type_system_corrected.adoc`)
76+
that *declares* an Echo system (§8–9, §12) but the checker implements none of it.
77+
78+
| Governance / truthing
79+
| *The main gap.* `STATUS.md` claims "100% Complete – Production Ready" while
80+
`ROADMAP.adoc` honestly says "Phase 0 Alpha", and `academic/TODO_GAPS.md`
81+
claims Lean proofs still use `sorry` when they do not. Docs contradict reality
82+
in *both* directions.
83+
|===
84+
85+
== 3. Gap analysis
86+
87+
The proofs are not the weak point — *governance and build-truth* are. To reach
88+
AffineScript's position JtV must:
89+
90+
. *G1 — Authoritative status.* Adopt a single capability matrix with a precise
91+
status vocabulary; reconcile `STATUS.md` ⇄ `ROADMAP.adoc` ⇄ `TODO_GAPS.md`.
92+
. *G2 — Doc-truthing.* A mechanical check that docs cannot over-claim past the
93+
test/proof gates.
94+
. *G3 — Build truth.* The Rust core must actually compile, and CI must prove it.
95+
. *G4 — Conformance-as-oracle.* Promote `conformance/` to a gate.
96+
. *G5 — Verification locus.* Keep JtV's proof-assistant advantage *and* add the
97+
target-layer (WASM) verification story AffineScript has.
98+
99+
== 4. Phased roadmap (starts with proofs)
100+
101+
=== Phase 1 — Proofs & proof-governance (THIS effort)
102+
103+
Rationale: proofs are JtV's strongest asset and the right place to establish the
104+
truthing discipline, because a mechanized proof cannot lie.
105+
106+
* [x] Inventory every Lean theorem and its status (see
107+
`verification/PROOF-CAPABILITY-MATRIX.adoc`).
108+
* [x] Adopt the AffineScript status vocabulary, specialised for proofs
109+
(`verified` / `partial` / `stated-unproven` / `absent`).
110+
* [x] Doc-truthing pass on the proof layer: correct the stale `sorry` claims in
111+
`academic/TODO_GAPS.md` (the proofs are `sorry`-free).
112+
* [x] *Echo Types alignment (proofs first):* formalise JtV's Echo system in
113+
`jtv_proofs/JtvEcho.lean`, aligned with the `echo-types` Agda library and
114+
`EchoTypes.jl`. This is the formal contract for the type checker.
115+
* [ ] Wire `JtvEcho` into the `proof-regression.yml` gate (already covered by
116+
the `lakefile.lean` default target).
117+
118+
=== Phase 2 — Echo Types in the checker (commenced here)
119+
120+
* [x] Implement the Echo effect lattice in `crates/jtv-core/src/echo.rs`
121+
(`Safe ⊑ Neutral ⊑ Breaking`, join, admissibility) — the executable image of
122+
`JtvEcho.lean`.
123+
* [x] Enforce spec §9 in the type checker: a `reverse` block is rejected when
124+
its aggregate echo is `Breaking` (`JtvError::EchoViolation`).
125+
* [ ] Propagate echo through Data inference as a second effect dimension
126+
(alongside `Purity`); surface `@echo(...)` annotations.
127+
* [ ] Bridge value-level fibres (`echo-types`) to the effect classes for
128+
function calls.
129+
130+
=== Phase 3 — Build truth & governance parity
131+
132+
* [ ] *G3:* repair the `ast.rs ⇄ interpreter/typechecker/cli` drift so
133+
`jtv-core` compiles; vendor or feature-gate `patacl-core`; make
134+
`rust-ci.yml` prove the build.
135+
* [ ] *G1/G2:* create `docs/CAPABILITY-MATRIX.adoc` for the whole project and a
136+
`hooks/check-doc-truthing.sh`; reconcile `STATUS.md`.
137+
* [ ] *G4:* promote `conformance/` to a compiler-as-oracle gate.
138+
139+
=== Phase 4 — Backend / verification locus
140+
141+
* [ ] *G5:* document and test the WASM target-layer verification story to match
142+
AffineScript's typed-wasm contract, while retaining the Lean/Idris assets.
143+
144+
== 5. Echo Types — why this workstream sits in Phase 1
145+
146+
The `echo-types` library (`hyperpolymath/echo-types`, Agda) formalises
147+
*structured loss / non-total erasure*: the echo of `f` at `y` is the fibre
148+
`Echo f y := Σ x, f x ≡ y` — irreversible computation that nonetheless *retains
149+
proof-relevant witnesses* of what was lost. `EchoTypes.jl` is its finite,
150+
executable companion.
151+
152+
This maps exactly onto JtV's already-declared (but unimplemented) Echo system:
153+
154+
[cols="1,1,2"]
155+
|===
156+
| JtV Echo | echo-types | Meaning
157+
158+
| `EchoSafe` | injective `f` (singleton fibre) | no loss; reversible (`+`↔`-`)
159+
| `EchoNeutral` | non-injective, residue retained | structured loss; not invertible
160+
| `EchoBreaking` | total erasure | information destroyed
161+
|===
162+
163+
Because the construct is *itself proof-defined*, the faithful way to "make the
164+
type checker accommodate it" is proofs-first: state the lattice and the
165+
reverse-block contract in Lean (`JtvEcho.lean`), then implement that exact
166+
contract in Rust (`echo.rs`). Both are delivered in this effort.
167+
168+
== 6. Out of scope here
169+
170+
Full echo propagation through inference, the project-wide capability matrix, the
171+
Rust build repair, and the WASM verification locus are *named and sequenced*
172+
above but deferred to their phases to keep this change reviewable.

‎academic/TODO_GAPS.md‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -29,10 +29,14 @@ This document tracks all items marked as TODO in the academic documentation and
2929
| PROOF-2 | Interpreter correctness partial | High | 🔶 Partial |
3030
| PROOF-3 | WASM compilation not verified | Medium | ❌ Not Started |
3131
| PROOF-4 | End-to-end verification chain incomplete | High | 🔶 Partial |
32-
| PROOF-5 | Some Lean proofs use `sorry` | High | 🔶 Partial |
32+
| ~~PROOF-5~~ | ~~Some Lean proofs use `sorry`~~ — **RESOLVED 2026-06-02**: `grep -rc 'sorry\|admit\|axiom' jtv_proofs/*.lean` ⇒ 0. The proof layer is `sorry`-free. | — | ✅ Done |
3333

3434
**Impact:** While core theorems are proven, full verification chain is incomplete.
3535

36+
> **Doc-truthing note (2026-06-02):** This section previously overstated proof
37+
> incompleteness. The authoritative, continuously-checked status now lives in
38+
> [`verification/PROOF-CAPABILITY-MATRIX.adoc`](../verification/PROOF-CAPABILITY-MATRIX.adoc).
39+
3640
### 1.3 Security
3741

3842
| Gap | Description | Priority | Status |
@@ -123,21 +127,19 @@ Line ~460: TODO: Uncertainty quantification
123127

124128
## 3. Lean Proof Gaps
125129

126-
### 3.1 Proofs Using `sorry`
130+
### 3.1 Proofs Using `sorry` — RESOLVED (2026-06-02)
127131

128-
The following proofs in `jtv_proofs/` use `sorry` and need completion:
132+
**No proof in `jtv_proofs/` uses `sorry`, `admit`, or an added `axiom`.** The
133+
claims previously listed here are stale:
129134

130-
```lean
131-
-- JtvOperational.lean:307
132-
theorem data_terminates (e : DataExpr) (σ : State) :
133-
∃ (n : Int), DataStepStar ⟨e, σ⟩ ⟨DataExpr.lit n, σ⟩ := by
134-
-- ... cases use sorry for step composition
135+
* `data_terminates` (now `JtvOperational.lean:~341`) is a *complete* structural
136+
induction over `DataExpr` (lit / var / add / neg), discharged via
137+
`dataStepStar_trans` and the `dataStepStar_*` congruence lemmas. No `sorry`.
138+
* The Control-divergence fact is shown by the fully-proved
139+
`infinite_loop_steps`, not a `sorry`-d example.
135140

136-
-- JtvOperational.lean:362
137-
example (σ : State) :
138-
∃ σ', σ' ≠ σ ∧ CtrlStep ... := by
139-
-- Uses sorry for σ "x" ≠ 42 case
140-
```
141+
Verification: `grep -rc 'sorry\|admit\|axiom' jtv_proofs/*.lean` ⇒ all zero.
142+
See `verification/PROOF-CAPABILITY-MATRIX.adoc` for the authoritative inventory.
141143

142144
### 3.2 Missing Theorems
143145

0 commit comments

Comments
 (0)