diff --git a/docs/decisions/0002-l0-observational-equivalence-for-tea-erasure.adoc b/docs/decisions/0002-l0-observational-equivalence-for-tea-erasure.adoc new file mode 100644 index 0000000..a05e358 --- /dev/null +++ b/docs/decisions/0002-l0-observational-equivalence-for-tea-erasure.adoc @@ -0,0 +1,196 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Architecture Decision Record: 0002-l0-observational-equivalence-for-tea-erasure + + + +# 2. L0 observational equivalence for TEA erasure (prospective ET-16) + +Date: 2026-07-27 + +## Status + +**Accepted** — 2026-07-27, owner ruling: **Alternative B (parametric L0 +observation)**. + +Drafted as alternatives-with-a-recommendation; the owner selected B. The +alternatives are retained below as the considered options, per ADR practice — +A and C are recorded as *rejected*, not as live choices. + +## Context + +### The block + +`docs/theory/08-l4-effects-tea.adoc` states ET-14 (TEA erasure) and lists four +things a complete statement must fix. Item (3) is **the observational +equivalence used at L0**. ET-14 cannot be *stated*, let alone proved, until +(3) is settled — so (3) gates the headline open problem, and through it +anytype's Phase 6. + +### Why it is not merely a definition + +`docs/theory/01-l0-runtime.adoc` makes a deliberate architectural commitment: + +> L0 deliberately has *no independent semantics within systemet*. No typing +> judgement is defined at L0. No systemet obligation quantifies over L0 +> programs directly. Obligations reference L0 only through the lowering +> function's image. + +But an observational equivalence *is* a semantics — at minimum a notion of +observation. So item (3) cannot be answered without either reversing that +commitment or finding a formulation that respects it. That is a theory +change, which is why the same document parks a prospective **ET-16** as a +*candidate deliberately not numbered into the ledger*, pending this ADR. + +The tension in one line: **ET-14 needs an L0 observation; L0 is defined by +having no semantics of its own.** + +### Constraints any answer must respect + +1. **The authority chain.** systemet (theory) → anytype (kernel) → + AffineScript (product). systemet has no runnable code by design; anytype + and AffineScript own the real targets (typed WASM, C). A commitment made + here propagates downstream and is expensive to retract. +2. **Honesty rules.** ET-14 may not be described as proven or "in progress" + without a prover-checked artefact under `verification/proofs/`. Whatever is + adopted must be mechanizable, not merely stateable. +3. **The three letters must stay load-bearing.** Dropping any of T, E, A must + admit a counterexample, and the counterexamples are part of the + development — so the chosen equivalence must be *fine enough to + distinguish* those three failures. An equivalence too coarse makes ET-14 + true for the wrong reason. +4. **What "erases" means, per the existing prose:** the handler "contributes + no code and no data to the L0 image beyond what the un-effectful program + would have produced". + +## Decision + +**Adopted: Alternative B (parametric L0 observation).** Alternatives A and C +were considered and rejected; both are recorded below with their reasoning, so +a future reader can see what was traded away. + +### Alternative A — Adopt a concrete L0 semantics *(rejected)* + +Define a small-step operational semantics for a core L0, define contextual +equivalence over it, and adopt ET-16 in its strong form ("lowering preserves +L1 conversion; grade erasure at L0 is sound"). + +* **Positive.** Strongest and most conventional; ET-14 becomes an ordinary + compiler-correctness theorem with abundant prior art. Permits reasoning + about the lowering itself, not just erasure. +* **Negative.** systemet acquires and must maintain an L0 semantics — a large + artefact, and a reversal of the stated architecture. Worse, the model L0 + will not be anytype's or AffineScript's real target, so the proofs risk + being *about a fiction*: green in systemet, not transferable. Largest scope + by a wide margin. + +### Alternative B — Parametric L0 observation *(ADOPTED)* + +Do not fix an L0 semantics. Introduce an **interface** — an `L0Observation` +structure: a carrier of L0 programs, a relation `≈`, and the laws that +relation must satisfy (equivalence; compositionality with respect to the +lowering's image; and a separation law strong enough to distinguish the three +counterexamples). State and prove ET-14 **for every** structure satisfying +that interface. Downstream, anytype and AffineScript instantiate it for their +real targets. + +* **Positive.** Preserves the "no independent L0 semantics" commitment + exactly: the semantics becomes a *parameter*, never a commitment. + **It reuses this repo's own proven idiom** — ET-4 is already discharged as + `Systemet.L2.GradeAlgebra`, "the law set as a class whose fields *are* the + proof obligations", with four instances and a generic product construction, + all mechanized and green. The same trick applied to observation is not a new + invention; it is the house pattern. Scope is bounded and Lean-shaped. + Defers the WASM/C commitment to the repos that actually have targets, which + is what the authority chain already says. +* **Negative.** The theorem is conditional: it bites only once someone + discharges the interface for a real target, so anytype/AffineScript inherit + a proof obligation. The interface must be designed carefully — too weak and + ET-14 becomes vacuous; too strong and no real target satisfies it. **This + design risk is the substance of the work and must not be waved away**; a + vacuity check (exhibit at least one instantiation, and at least one + non-instance) belongs in the development. +* **Neutral.** ET-16 shrinks: instead of adopting "L0 lowering correctness" + wholesale, one adopts *an interface plus the obligation that every + instantiation discharges it*. + +### Alternative C — Syntactic image identity *(rejected as the definition; retained as an optional strengthening lemma)* + +Avoid semantics entirely: define erasure as the lowering of `handle p with h` +being *identical* — up to α and a fixed normal form — to the lowering of the +pure residue. + +* **Positive.** Smallest possible; no observation relation needed; closest to + the literal existing wording ("contributes no code and no data"); soonest to + mechanize. +* **Negative.** Almost certainly too strong to be true of any realistic + lowering (instruction ordering, register allocation, calling conventions all + perturb the image), so it would be provable only for a toy lowering and + would not transfer. It also mis-states the intent: erasure should permit + *equivalent* code, not demand *identical* code. +* **Suggested use.** Not as the definition, but as an **optional strengthening + lemma** where a given instantiation happens to achieve it. + +### The decision + +**B is adopted**, with **C** retained as a lemma-level strengthening. Concretely: + +1. Add `ET-16` to the ledger in a *narrow* form: "every `L0Observation` + instantiation used by a downstream consumer discharges the interface laws", + rather than a general lowering-correctness claim. +2. Fix ET-14 item (3) as: *the equivalence is the `≈` of an arbitrary + `L0Observation`*, making ET-14 a statement universally quantified over + instantiations. +3. Sequence the mechanization: interface → vacuity check (one instance, one + non-instance) → the three dropped-letter counterexamples → the erasure + translation → ET-14 itself. **The counterexamples come early on purpose**: + they are the cheapest test that the interface is fine enough to be worth + proving anything about. + +## Consequences + +### Positive + +- Unblocks ET-14's *statement*, and with it anytype Phase 6 planning. +- Keeps systemet free of runnable code and of a semantics it would have to + maintain against two moving backends. +- Reuses a mechanization pattern already proven green in this repo (ET-4/ET-5). +- Bounded, checkable increments — each step has a `lake build` oracle, the same + property that made ET-2 tractable. + +### Negative + +- anytype and AffineScript inherit an obligation: to claim erasure on + systemet's authority they must exhibit an instantiation and discharge its + laws. Today they may implement handlers but **may not advertise erasure + guarantees** — that restriction stays until an instantiation exists. +- Interface design is the hard part and can fail late: a too-weak interface + yields a true-but-vacuous ET-14. The vacuity check exists to fail fast. + +### Neutral + +- ET-16 enters the ledger narrower than the parked candidate implied; the + broader "lowering preserves L1 conversion" claim remains unadopted and would + need its own ADR. +- No change to L0's status as a lowering target with no typing judgement. + +## What this ADR does not decide + +Explicitly out of scope, and still owner-only: + +- The L4 handler syntax and effect-operation grading — ET-14 item (1). +- The formal content of T, E and A as predicates — ET-14 item (2). +- The erasure translation — ET-14 item (4). +- The **L2 join law**, absent from the grade algebra, and **L3 guardedness**, + sketched in `06-l3-guarded-recursion.adoc`. Both are separately ADR-gated and + neither is resolved here. + +## References + +- `docs/theory/08-l4-effects-tea.adoc` — ET-14 and its four unfixed items +- `docs/theory/01-l0-runtime.adoc` — "What L0 is not"; the parked ET-16 candidate +- `docs/theory/OBLIGATIONS.adoc` — the ledger; ET-16 under "Candidate + (deliberately not in the ledger)" +- `docs/theory/03-l2-grades.adoc`, `09-grade-algebra-catalogue.adoc` — the + ET-4 law-set-as-a-class idiom this recommendation reuses +- `verification/proofs/lean4/Systemet/L2/GradeAlgebra.lean` — that idiom, mechanized diff --git a/docs/theory/01-l0-runtime.adoc b/docs/theory/01-l0-runtime.adoc index c1b8b32..e069438 100644 --- a/docs/theory/01-l0-runtime.adoc +++ b/docs/theory/01-l0-runtime.adoc @@ -37,12 +37,19 @@ observable behaviour. The precise observational equivalence used at L0 is part of ET-14's statement and is recorded in link:08-l4-effects-tea.adoc[08 — TEA]. -== A candidate obligation, not yet adopted +== A candidate obligation — adopted, narrowly (2026-07-27) The prose in the root README and EXPLAINME states no correctness obligation for the lowering itself (e.g. "lowering preserves L1 conversion" or "grade erasure at L0 is sound"). Adding one — call it a prospective *ET-16* — would be a theory change and therefore needs an ADR, per EXPLAINME §"Relationship -to anytype and AffineScript". It is flagged in -link:OBLIGATIONS.adoc[OBLIGATIONS.adoc] as a candidate, deliberately *not* -numbered into the ledger. +to anytype and AffineScript". link:../decisions/0002-l0-observational-equivalence-for-tea-erasure.adoc[ADR-0002] +settled this on 2026-07-27, and deliberately adopted **less** than the +candidate implied. What entered the ledger as link:OBLIGATIONS.adoc#ET-16[ET-16] is an *interface* +obligation — every `L0Observation` instantiation discharges its laws — not a +general lowering-correctness claim. The broader "lowering preserves L1 +conversion" remains unadopted and would need its own ADR. + +Crucially this does **not** give L0 a semantics: the observation relation is a +parameter, supplied by whoever owns a real target (anytype, AffineScript). +Everything in §"What L0 is not" above still holds. diff --git a/docs/theory/08-l4-effects-tea.adoc b/docs/theory/08-l4-effects-tea.adoc index 540b0ab..e68caa7 100644 --- a/docs/theory/08-l4-effects-tea.adoc +++ b/docs/theory/08-l4-effects-tea.adoc @@ -47,11 +47,17 @@ data to the image. A complete statement must fix: 1. the L4 syntax of handlers and the grading of effect operations (in terms of the ET-4 algebra contract); 2. the exact formal content of T, E, and A as predicates on handlers; -3. the observational equivalence used at L0 (see - link:01-l0-runtime.adoc[01 — L0]); +3. the observational equivalence used at L0 — *FIXED 2026-07-27 by + link:../decisions/0002-l0-observational-equivalence-for-tea-erasure.adoc[ADR-0002]*: + it is the `≈` of an arbitrary `L0Observation` (link:OBLIGATIONS.adoc#ET-16[ET-16]), so ET-14 is + universally quantified over instantiations rather than tied to one L0 + semantics (see link:01-l0-runtime.adoc[01 — L0]); 4. the erasure translation itself. -None of 1–4 is fixed yet; fixing them is part of the obligation. What a +Items 1, 2 and 4 are not fixed yet; fixing them is part of the obligation. +Item 3 is fixed (ADR-0002). ET-14 itself remains **OPEN and unproven** — an +adopted equivalence is a prerequisite for *stating* it, not progress toward +proving it. What a proof would have to show, minimally: an erasure-candidate handler can be eliminated by a typed translation whose correctness is proved against the observational equivalence of (3) — and the three letters are each load- diff --git a/docs/theory/OBLIGATIONS.adoc b/docs/theory/OBLIGATIONS.adoc index 6a48267..b169c31 100644 --- a/docs/theory/OBLIGATIONS.adoc +++ b/docs/theory/OBLIGATIONS.adoc @@ -131,9 +131,25 @@ Rules of the ledger: | enforced by the proofs gate's axiom audit |=== -== Candidate (deliberately not in the ledger) - -*ET-16 (candidate — L0 lowering correctness).* The prose states no -obligation for the lowering itself (e.g. lowering preserves conversion; -grade erasure is sound). Adopting one is a theory change → ADR first. See -link:01-l0-runtime.adoc[01 — L0] §"A candidate obligation, not yet adopted". +== ET-16 — adopted 2026-07-27, narrowly (ADR-0002) + +[[ET-16]]*ET-16 (L0 observation interface).* Every `L0Observation` +instantiation used by a downstream consumer discharges the interface laws: +`≈` is an equivalence, is compositional with respect to the lowering's image, +and separates the three dropped-letter counterexamples of ET-14. + +Status: *specified* — mechanization not started. Slot: +`lean4/Systemet/L0/Observation.lean` (interface), then instances. + +This is deliberately **narrower** than the parked candidate. The broader claim +— "lowering preserves L1 conversion" / "grade erasure at L0 is sound" — +remains *unadopted* and would need its own ADR. L0 still has no independent +semantics in systemet: the observation is a *parameter*, supplied by whoever +owns a real target. See link:../decisions/0002-l0-observational-equivalence-for-tea-erasure.adoc[ADR-0002] +and link:01-l0-runtime.adoc[01 — L0]. + +*Consequence for downstream.* anytype and AffineScript may implement effect +handlers, but may not advertise erasure guarantees on systemet's authority +until they exhibit an instantiation and discharge its laws. That restriction +is unchanged by this adoption — ET-16 names the obligation, it does not +discharge it.