docs(adr): draft ADR-0002 — L0 observational equivalence for TEA erasure (prospective ET-16) - #28
Merged
Merged
Conversation
DRAFT, Status: Proposed. Decides nothing until the owner accepts it.
ET-14 (TEA erasure) lists four things a complete statement must fix. Item (3),
the observational equivalence used at L0, gates the other three -- and through
them anytype Phase 6. It has been blocked because it is not merely a
definition: 01-l0-runtime.adoc commits to L0 having NO independent semantics
in systemet, while an observational equivalence IS a semantics. Hence the
parked "candidate ET-16, deliberately not numbered into the ledger".
This ADR states that tension plainly and offers three real alternatives with
consequences traced through the authority chain (systemet -> anytype ->
AffineScript):
A adopt a concrete L0 semantics strongest, largest, and risks proving
things about a model L0 that is not
anytype's or AffineScript's real target
B parametric L0 observation RECOMMENDED -- an `L0Observation`
interface; ET-14 quantified over every
instantiation; downstream instantiates
C syntactic image identity smallest, almost certainly too strong
to be true of a realistic lowering;
retained as an optional strengthening
B is recommended because it preserves the architectural commitment rather than
reversing it, and because it reuses an idiom already proven green in this repo:
ET-4 is discharged as `Systemet.L2.GradeAlgebra`, "the law set as a class whose
fields ARE the proof obligations", with four instances plus a generic product
construction. Applying the same shape to observation is the house pattern, not
a new invention.
The recommendation is stated with its failure mode, not just its merits: a
too-weak interface makes ET-14 true and vacuous. A vacuity check (one instance,
one non-instance) and the three dropped-letter counterexamples are sequenced
EARLY for exactly that reason -- they are the cheapest test that the interface
is fine enough to be worth proving anything about.
Numbering: this repo's docs/decisions/ holds 0000-template and 0001 only, so
the next number is 0002. (Earlier session notes called this "ADR-006"; that was
wrong for this repo.)
Explicitly NOT decided here, still owner-only: ET-14 items (1), (2) and (4);
the L2 join law; L3 guardedness. Each remains separately ADR-gated.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Owner ruling 2026-07-27: Alternative B, parametric L0 observation.
ADR-0002 Status: Proposed -> Accepted. A and C are retained as the considered
options and marked rejected (C survives as an optional strengthening lemma),
so a future reader can see what was traded away rather than only what won.
Propagated, because an accepted ADR that nothing else reflects is just a file:
OBLIGATIONS.adoc ET-16 leaves "Candidate (deliberately not in the ledger)"
and enters the ledger DELIBERATELY NARROW: every
`L0Observation` instantiation discharges the interface
laws (equivalence; compositional wrt the lowering's image;
separates the three dropped-letter counterexamples).
The broader "lowering preserves L1 conversion" / "grade
erasure is sound" stays UNADOPTED and needs its own ADR.
Status: specified, mechanization not started.
08-l4-effects-tea item (3) marked FIXED: the equivalence is the `≈` of an
arbitrary `L0Observation`, so ET-14 is universally
quantified over instantiations. Items (1), (2), (4) remain
unfixed, and ET-14 itself remains OPEN and unproven -- an
adopted equivalence is a prerequisite for STATING it, not
progress toward proving it. Said explicitly so the amber
claim cannot drift to green on the strength of this ADR.
01-l0-runtime "candidate, not yet adopted" -> adopted narrowly, with the
point that matters spelled out: this does NOT give L0 a
semantics. The observation is a parameter supplied by
whoever owns a real target. Everything in "What L0 is not"
still holds.
Downstream consequence recorded in the ledger: anytype and AffineScript may
implement handlers but still may NOT advertise erasure guarantees on systemet's
authority until they exhibit an instantiation and discharge its laws. ET-16
names that obligation; adopting it does not discharge it.
Cross-file xrefs use link:OBLIGATIONS.adoc#ET-16[] rather than <<ET-16>>, which
does not resolve across documents in AsciiDoc.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft for a ruling, not an implementation. Status is
Proposed; the ADR decides nothing until you accept it.Why this exists
ET-14 (TEA erasure) can't be stated until item (3) — the observational equivalence used at L0 — is fixed. That gates items (1), (2), (4), and through them anytype Phase 6. It has stayed open because it isn't merely a definition:
01-l0-runtime.adoc: "L0 deliberately has no independent semantics within systemet. No typing judgement is defined at L0."Hence
OBLIGATIONS.adocparks "ET-16 (candidate — L0 lowering correctness) … deliberately not numbered into the ledger" pending an ADR. This is that ADR.The tension in one line: ET-14 needs an L0 observation; L0 is defined by having no semantics of its own.
The three alternatives
L0Observationinterface (carrier,≈, laws); ET-14 quantified over every instantiation; anytype/AffineScript instantiate for real targetsWhy B
It preserves the architectural commitment instead of reversing it — the semantics becomes a parameter, never a commitment — and it reuses an idiom already mechanized and green in this repo: ET-4 is 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. The same shape applied to observation is the house pattern.It also puts the WASM/C commitment where the real targets live, which is what the authority chain already says.
Stated with its failure mode: a too-weak interface makes ET-14 true and vacuous. So the sequencing puts a vacuity check (one instance, one non-instance) and the three dropped-letter counterexamples early — they're the cheapest test that the interface is fine enough to be worth proving anything about.
What it does not decide
ET-14 items (1) L4 handler syntax, (2) the T/E/A predicates, (4) the erasure translation — plus the L2 join law and L3 guardedness. All remain owner-only and separately ADR-gated. ET-16, if adopted, enters the ledger narrower than the parked candidate implied.
Note on numbering
docs/decisions/holds0000-templateand0001only → this is 0002. Earlier session notes called it "ADR-006", which was wrong for this repo.Branched from
main, independent of #27 (ET-2 promotion), so the two can be ruled on separately.🤖 Generated with Claude Code