Push 4b Wave 1a: three ratified corrections, and a citation that pointed the wrong way
Scoping Push 4b turned up three Chapter 4 defects and four rulings; this lands
the spec half of the first three. `PLAN_PUSH4B_TUNING.md` carries the full
scoping and all four rulings.
**P13-S5, Ruling A -- full register.** `req:pitch:ji-vector-basis` says the
built-in JI spaces order primes ascending *starting with 2* and that
`components.len()` MUST equal the basis size; the catalog table called
`ji-5limit` "Two-dimensional (prime axes 3, 5)", `ji-7limit` three- and
`ji-11limit` four-dimensional -- each exactly one short, the table being
octave-reduced and the requirement full-register. The table moves, the
requirement does not: a `JiVector` is an absolute position, and without the
prime-2 exponent `ji-5limit` cannot distinguish C4 from C5. Each row now states
its basis explicitly so two readers cannot derive different ones.
**P13-S7, Ruling C -- a score selects, it does not define.** `ScalePosition`
pointed at "the score's pitch-space registry", which does not exist: `Score` has
thirteen fields and none is one, and `ScoreTuningContext` carries ids and
accidental extensions, never definitions. So `req:pitch:default-pitch-space`'s
"MUST define / MAY define" was unsatisfiable except by reading define as select.
The requirement moves to *select*, the comment names the built-in catalog, and
score-local definition is recorded as a deferred major with its reason: the
Chapter 4 type surface has never had a consumer, and freezing ~20
never-constructed types under `req:binfmt:frozen-layout` is permanent.
**Ruling D -- `AccidentalEngraving` could not be canonical.** It borrowed
Chapter 7's `BoundingBox`, built on `StaffSpace(f32)` -- correct for the
non-canonical resolved-layout cache, but this field hangs off
`ScoreTuningContext`, which *is* canonical, and
`req:determinism:canonical-floating-point` requires canonical stored floats to
be binary64. Chapter 4 now has `EngravingBoundingBox` over `SpaceUnit`, the type
`advance_width` already used. Chapter 7's `BoundingBox` is untouched.
That defect only surfaced because the first scoping was wrong and got checked.
It claimed `GlyphReference` and `BoundingBox` "exist but live in
epiphany-layout-ir" and recommended moving them down. They are **homonyms**:
Chapter 4's `GlyphReference` is `enum { Smufl(u32), Custom, Composite }`;
layout-ir's is `struct GlyphReference(Cow<'static, str>)`, a glyph *name*. A
move would have relocated the wrong types. The plan is corrected and there is no
crate move.
**Review finding.** The rationale as first written read "Resolved layout is
non-canonical (Requirement req:layoutir:staff-space-coordinates)". That
requirement mandates staff-space units and single precision and says nothing
about canonicality -- a true sentence resting on the wrong authority, the P13-S4
pattern again. No labelled requirement asserts resolved-layout non-canonicality;
it is prose in the Binary Format companion. Each claim now rests on its real
source.
`requirement_labels.rs` is untouched: no requirement was added or removed, so
209/279/279 held, which was the contract's invariant against scope creep. The
checker cannot catch a citation that resolves but does not support its sentence
-- it enforces cited-to-defined, not cited-to-relevant. Second instance today.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
b3449256f9
commit
5dcaa58fd0
|
|
@ -0,0 +1,111 @@
|
||||||
|
# Contract: Push 4b Wave 1a — three ratified spec corrections
|
||||||
|
|
||||||
|
Repo root `/home/jeans/Repos/active/epiphany`. Read this in full before editing
|
||||||
|
anything. The plan is `spec/PLAN_PUSH4B_TUNING.md`; its four rulings are granted
|
||||||
|
and this contract states the three that concern you as law.
|
||||||
|
|
||||||
|
You edit **`spec/core_spec.tex` only**, plus its rebuilt PDF. You write no Rust
|
||||||
|
except possibly one constant (§4), and you touch no other document.
|
||||||
|
|
||||||
|
## Correction 1 — the JI prime basis (P13-S5, Ruling A)
|
||||||
|
|
||||||
|
`req:pitch:ji-vector-basis` (`core_spec.tex:999`) says the built-in JI pitch
|
||||||
|
spaces order primes ascending **starting with 2**, and that `components.len()`
|
||||||
|
MUST equal the basis size. The built-in pitch-space table contradicts it, each
|
||||||
|
row exactly one short:
|
||||||
|
|
||||||
|
| space | table says today | must become |
|
||||||
|
|---|---|---|
|
||||||
|
| `ji-5limit` | "Two-dimensional (prime axes 3, 5)" | three-dimensional, basis {2,3,5} |
|
||||||
|
| `ji-7limit` | "Three-dimensional" | four-dimensional, basis {2,3,5,7} |
|
||||||
|
| `ji-11limit` | "Four-dimensional" | five-dimensional, basis {2,3,5,7,11} |
|
||||||
|
|
||||||
|
**Ratified: full register.** The three table rows change. The requirement is
|
||||||
|
correct as written and **MUST NOT** be edited — it is cited from elsewhere and
|
||||||
|
its text is the thing the table was failing to match.
|
||||||
|
|
||||||
|
State each row's basis explicitly, in ascending prime order including 2, so two
|
||||||
|
readers cannot derive different bases. The reason, if you want it for the prose:
|
||||||
|
a `JiVector` is an absolute *position*, and without the prime-2 exponent
|
||||||
|
`ji-5limit` cannot distinguish C4 from C5.
|
||||||
|
|
||||||
|
## Correction 2 — a score selects, it does not define (P13-S7, Ruling C)
|
||||||
|
|
||||||
|
`ScalePosition`'s listing comment (`core_spec.tex:934`) says the space
|
||||||
|
"References an entry in **the score's pitch-space registry**". No such registry
|
||||||
|
exists: `Score` has thirteen fields and none is one, and `ScoreTuningContext`
|
||||||
|
carries ids plus accidental extensions, never space or system definitions.
|
||||||
|
|
||||||
|
`req:pitch:default-pitch-space` says "Every score MUST **define** at least one
|
||||||
|
pitch space… Scores MAY **define** additional pitch spaces."
|
||||||
|
|
||||||
|
**Ratified: the catalog is closed.** Amend both:
|
||||||
|
|
||||||
|
* the requirement's two "define"s become *select* (from the built-in catalog),
|
||||||
|
preserving everything else it says — including the non-comparability rule and
|
||||||
|
the explicit space-conversion MUST, which are cited elsewhere;
|
||||||
|
* the `ScalePosition` comment names the **built-in** catalog.
|
||||||
|
|
||||||
|
Add a sentence recording that score-local pitch-space definition is deferred to
|
||||||
|
a later schema major, with the reason: the Chapter 4 type surface has never had
|
||||||
|
a consumer, and `req:binfmt:frozen-layout` would freeze it permanently.
|
||||||
|
|
||||||
|
Do **not** add a registry field to any struct. That is the point of the ruling.
|
||||||
|
|
||||||
|
## Correction 3 — `AccidentalEngraving` must be canonical-safe (Ruling D)
|
||||||
|
|
||||||
|
`AccidentalEngraving` (`core_spec.tex`, §"Accidental Engraving Metadata")
|
||||||
|
declares `bounding_box: BoundingBox`. That `BoundingBox` is **Chapter 7's**
|
||||||
|
(`core_spec.tex:8650`), built on `StaffSpace`, which the implementation defines
|
||||||
|
as `pub struct StaffSpace(pub f32)` — single precision, deliberately
|
||||||
|
(`crates/epiphany-layout-ir/src/spatial.rs:3`).
|
||||||
|
|
||||||
|
Resolved layout is **non-canonical**, so single precision is correct there. But
|
||||||
|
Push 4b puts `accidental_extensions` inside `ScoreTuningContext`, which **is**
|
||||||
|
canonical state, and `req:determinism:canonical-floating-point` requires
|
||||||
|
canonical stored floats to be "finite IEEE 754 **binary64**".
|
||||||
|
|
||||||
|
**Ratified: Chapter 4 gets its own bounding box, over `SpaceUnit`** — the type
|
||||||
|
`AccidentalEngraving.advance_width` already uses, which is `CanonicalF64`. Give
|
||||||
|
it a distinct name so it cannot be confused with Chapter 7's, declare its four
|
||||||
|
edges as `SpaceUnit`, and cite `req:determinism:canonical-floating-point` for
|
||||||
|
why. Chapter 7's `BoundingBox` is **not** edited.
|
||||||
|
|
||||||
|
Add a short rationale block: engraving metadata that lives in canonical state
|
||||||
|
must carry canonical precision, and Chapter 7's coordinates are a
|
||||||
|
non-canonical layout cache.
|
||||||
|
|
||||||
|
## What you must not do
|
||||||
|
|
||||||
|
* **Do not touch the built-in tuning-system table.** The 20 tuning systems are
|
||||||
|
another agent's work and are not ratified yet. You change the **pitch-space**
|
||||||
|
table (correction 1) and nothing else in that section.
|
||||||
|
* **Do not edit `req:pitch:ji-vector-basis`**, `binary_format.tex`,
|
||||||
|
`operation_catalog.tex`, or any other companion.
|
||||||
|
* **Do not add or remove a `\begin{requirement}` block.** All three corrections
|
||||||
|
amend existing text. See §4.
|
||||||
|
* **Do not rename or move any existing `\label`.** They are cited by code,
|
||||||
|
tests, and decision records.
|
||||||
|
* Do not run `cargo fmt --all`.
|
||||||
|
|
||||||
|
## Verification
|
||||||
|
|
||||||
|
1. **The requirement counts must not move.** `requirement_labels.rs` pins
|
||||||
|
`CORE_REQUIREMENT_COUNT = 209` and both suite counts at `279`. You add no
|
||||||
|
requirement, so all three stay. If a count changes, you did something the
|
||||||
|
contract did not ask for — stop and report it rather than updating the
|
||||||
|
constant.
|
||||||
|
2. `cargo test -p epiphany-testkit --test requirement_labels` → 6 passed.
|
||||||
|
3. Rebuild `core_spec.pdf` with `latexmk -xelatex` **twice**. Then check the log
|
||||||
|
for `^! `, `Undefined control sequence`, and `Reference .* undefined` — report
|
||||||
|
the actual counts, which must be zero.
|
||||||
|
4. Full workspace gate, because you are in a repo others depend on:
|
||||||
|
`cargo fmt --all --check`; `cargo clippy --workspace --all-targets` → 0;
|
||||||
|
`cargo test --workspace`; `cargo run -q -p epiphany-testkit --example
|
||||||
|
conformance_suite` → 8/8. Zero golden churn is expected — report it if not.
|
||||||
|
|
||||||
|
Report the actual commands and their actual output. On this project an agent
|
||||||
|
once reported "verification passes" while errors pointed into its own file, and
|
||||||
|
another silently deleted a struct field while rewriting the comment above it —
|
||||||
|
so **re-read every listing you edit, in full, after editing it**, and confirm the
|
||||||
|
declarations are still there.
|
||||||
|
|
@ -0,0 +1,358 @@
|
||||||
|
# Push 4b — the Chapter 4 tuning catalog: scope and plan
|
||||||
|
|
||||||
|
Status: **all four rulings granted; ready for dispatch.**
|
||||||
|
Prepared against `master` @ `b344925`. Every claim was checked against the
|
||||||
|
source; where I ran a probe I give the file and line.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 1. The two facts that shape this pass
|
||||||
|
|
||||||
|
**4b is the first schema major 3.** `ScoreTuningContext` is a frozen positional
|
||||||
|
struct carrying **three** of its six specified fields:
|
||||||
|
|
||||||
|
| specified (`core_spec.tex:3380`) | on the wire (`codec.rs:1835`) |
|
||||||
|
|---|---|
|
||||||
|
| `default_pitch_space` | ✓ |
|
||||||
|
| `default_tuning_system` | ✓ |
|
||||||
|
| `reference` | ✓ |
|
||||||
|
| `accidental_extensions` | **absent** |
|
||||||
|
| `smufl` | **absent** |
|
||||||
|
| `overrides` | **absent** |
|
||||||
|
|
||||||
|
`req:binfmt:frozen-layout` is explicit that this is a major: *"Adding a field is
|
||||||
|
a MAJOR change regardless of its type: an `Option` field is not 'optional' in
|
||||||
|
the wire sense… There is no 'downgrade to minor' for an `Option` addition."*
|
||||||
|
Majors 0, 1 and 2 are defined; **3 is unopened**, and `epiphany-bundle/DECISIONS.md:413`
|
||||||
|
already names it as next ("beyond-accept-set tests moved to major 3"). Push 4a
|
||||||
|
deliberately avoided opening it (`binary_format.tex:3272`: "no major~3").
|
||||||
|
|
||||||
|
So 4b opens a major. That is not a cost to minimize — it is a **budget to
|
||||||
|
spend deliberately**, because the next one after it is major 4.
|
||||||
|
|
||||||
|
**And 4b is a spec pass before it is a build.** Zero of Chapter 4's types exist
|
||||||
|
in Rust — not `PitchSpace`, `PositionStructure`, `IntervalAlgebra`,
|
||||||
|
`NominalRegistry`, `AccidentalRegistry`, `AccidentalDefinition`,
|
||||||
|
`PitchSpaceModification`, `TranspositionBehavior`, `SpellingRuleSet`,
|
||||||
|
`TuningSystem`, `TuningResolution`, `TuningOverride`, nor `TuningScope`. Only
|
||||||
|
the `*Id` newtypes exist. There is nothing to extend; there is a chapter to
|
||||||
|
implement. And three defects stand in front of it.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 2. Three spec defects block the build
|
||||||
|
|
||||||
|
Two were verified today from claims this repo had carried as **unverified**
|
||||||
|
through two passes (P13-S5, P13-S6). The third I found while scoping this plan.
|
||||||
|
|
||||||
|
### P13-S5 — the JI prime basis is specified at two lengths
|
||||||
|
|
||||||
|
`req:pitch:ji-vector-basis` says the built-in JI spaces order primes ascending
|
||||||
|
**starting with 2**, and `components.len()` MUST equal the basis size. The
|
||||||
|
built-in table says otherwise, each row exactly one short:
|
||||||
|
|
||||||
|
| space | requirement | table (`core_spec.tex:3496`) |
|
||||||
|
|---|---|---|
|
||||||
|
| `ji-5limit` | {2,3,5} → **3** | "Two-dimensional (prime axes 3, 5)" |
|
||||||
|
| `ji-7limit` | {2,3,5,7} → **4** | "Three-dimensional" |
|
||||||
|
| `ji-11limit` | {2,3,5,7,11} → **5** | "Four-dimensional" |
|
||||||
|
|
||||||
|
Both normative. A 5-limit vector is required to be both length 2 and length 3.
|
||||||
|
The octave-reduction clause does not reconcile them — it *normalizes* the first
|
||||||
|
component, it does not remove it.
|
||||||
|
|
||||||
|
### P13-S6 — no built-in tuning resolution is pinned; 14 of 20 are undefined
|
||||||
|
|
||||||
|
`req:tuning:builtin-tuning-catalog` makes all 20 identifiers MUST-resolve with
|
||||||
|
normative semantics. Only the six `tet-*` are specified, structurally, by
|
||||||
|
`TuningResolution::EqualTemperament`. The other 14 are names:
|
||||||
|
`pythagorean` (3:2 given; fifth-chain construction and wolf placement not),
|
||||||
|
three meantone variants, `werckmeister-iii`/`iv`, `vallotti`,
|
||||||
|
`kirnberger-ii`/`iii`, `young-ii`, three `ji-static-5limit-*`, and
|
||||||
|
`ji-adaptive-5limit`. `TuningResolution::Function` delegates them to a
|
||||||
|
`TuningFunctionId` that Chapter 10 lists as an **extension point**; no built-in
|
||||||
|
is mapped to one, and none is pinned.
|
||||||
|
|
||||||
|
Against `req:tuning:tuning-resolution-determinism` — determinism MUST hold
|
||||||
|
*across platforms* — two conforming implementations may each pick a different
|
||||||
|
published Werckmeister III and both pass. This is the requirement 4b exists to
|
||||||
|
satisfy, so it cannot be deferred past it.
|
||||||
|
|
||||||
|
### P13-S7 — the pitch-space registry does not exist (new; file it)
|
||||||
|
|
||||||
|
`ScalePosition.space` is documented as *"References an entry in **the score's
|
||||||
|
pitch-space registry**"* (`core_spec.tex:934`). `req:pitch:default-pitch-space`
|
||||||
|
says *"Every score MUST **define** at least one pitch space… Scores MAY define
|
||||||
|
additional pitch spaces."*
|
||||||
|
|
||||||
|
**There is no such registry anywhere in the data model.** `Score` has 13 fields
|
||||||
|
(`core_spec.tex:3639`) and none is a pitch-space or tuning-system registry.
|
||||||
|
`ScoreTuningContext`'s six specified fields carry *ids* and accidental
|
||||||
|
*extensions* — no space or system definitions. So a score can **name** an
|
||||||
|
arbitrary `PitchSpaceId` and can never **define** one: the MAY is flatly
|
||||||
|
unsatisfiable and the MUST is satisfiable only by reading "define" as "select".
|
||||||
|
|
||||||
|
This is load-bearing for 4b in a way the other two are not: a registry-backed
|
||||||
|
resolver has nothing to resolve *against* except the built-in catalog until it
|
||||||
|
is answered. **Ruling C answers it by moving the requirement, not the data
|
||||||
|
model** — "define" becomes "select", and the resolver's target is the built-in
|
||||||
|
catalog by ratification rather than by omission.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 3. What I verified
|
||||||
|
|
||||||
|
| claim | result |
|
||||||
|
|---|---|
|
||||||
|
| Chapter 4 types present in Rust | **0 of 13**; only `*Id` newtypes |
|
||||||
|
| `ScoreTuningContext` wire fields | 3 of 6 (`codec.rs:1835`) |
|
||||||
|
| schema majors defined | 0, 1, 2; **3 unopened** |
|
||||||
|
| Chapter 4 labelled requirements | 9, all citable since P13-S1 |
|
||||||
|
| built-in tuning systems specified | **6 of 20** |
|
||||||
|
| score-local pitch-space storage | **none exists** |
|
||||||
|
| deferred items awaiting a major elsewhere | 1 (`epiphany-core/DECISIONS.md:431`, a configurable-order `Score` field with no consumer — not worth riding along) |
|
||||||
|
|
||||||
|
**The P13-S2 interim guard is narrower than it looked.** It refuses any `Cmn`
|
||||||
|
position outside built-in `cmn-12`, and `PLAN_P13S2_CMN24.md`'s Ruling B
|
||||||
|
accepted "false refusal for score-defined 12-chromatic spaces" as its cost.
|
||||||
|
Given P13-S7, that cost is **zero**: no score can define a space at all, so no
|
||||||
|
false-refusal case exists. Ruling C keeps it at zero by ratification rather than
|
||||||
|
by omission — the accepted cost would only become real if score-local definition
|
||||||
|
later lands, and it is now a deliberate deferral with a stated reason.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 4. Rulings
|
||||||
|
|
||||||
|
### Ruling A — P13-S5 — **RATIFIED: full register**
|
||||||
|
|
||||||
|
The built-in table gains prime 2. `ji-5limit` becomes **three**-dimensional
|
||||||
|
(basis {2,3,5}), `ji-7limit` **four**, `ji-11limit` **five**.
|
||||||
|
`req:pitch:ji-vector-basis` is correct as written and does not change; the three
|
||||||
|
catalog rows do.
|
||||||
|
|
||||||
|
The data model forces it: a `JiVector` is an absolute *position*, and without
|
||||||
|
the prime-2 exponent `ji-5limit` cannot distinguish C4 from C5. The requirement
|
||||||
|
already says "Without such a declaration, full register is preserved." The
|
||||||
|
table's "two-dimensional (prime axes 3, 5)" is a *theory* presentation, in which
|
||||||
|
octave equivalence is assumed; the data model cannot assume it. Octave-reduction
|
||||||
|
would additionally have required a separate register carrier on `JiVector` — a
|
||||||
|
new field, and a second major-3 change for no gain.
|
||||||
|
|
||||||
|
### Ruling B — P13-S6 — **RATIFIED: keep all 20, pinned by construction**
|
||||||
|
|
||||||
|
The first scoping priced this as "a musicological ratification, 14 times over."
|
||||||
|
That was wrong, and the error was in *what form a definition takes*.
|
||||||
|
|
||||||
|
These temperaments have standard **constructions** — Vallotti narrows six
|
||||||
|
consecutive fifths by 1/6 Pythagorean comma and leaves the rest pure;
|
||||||
|
quarter-comma meantone narrows every fifth by 1/4 syntonic comma; Werckmeister
|
||||||
|
III narrows four named fifths by 1/4 Pythagorean comma. What varies across
|
||||||
|
published sources is overwhelmingly the **rounding of cents tables**, not the
|
||||||
|
construction. Specifying by construction therefore *removes* the variance that
|
||||||
|
specifying by cents table would *introduce*.
|
||||||
|
|
||||||
|
**The arithmetic-determinism worry is already answered by existing machinery.**
|
||||||
|
`ToleranceClass::AcousticCents` exists in `epiphany-determinism`, and its doc
|
||||||
|
comment names "Chapter 4 reference-pitch frequency resolution" outright.
|
||||||
|
`req:determinism:canonical-floating-point` lists **tuning** among the
|
||||||
|
floating-point contexts while barring floating point "where exact identity is
|
||||||
|
needed (object identifiers, operation ordering, graph membership, hash
|
||||||
|
identity)" — so a resolved frequency never enters canonical bytes. Bit-identity
|
||||||
|
was never achievable in any case: `pow`/`exp` are not correctly-rounded in
|
||||||
|
IEEE 754, so two libms may differ in the last ulp *including* for `tet-12`'s
|
||||||
|
$2^{n/12}$. `req:tuning:tuning-resolution-determinism` forbids dependence on
|
||||||
|
floating-point **rounding modes** — the FPU mode — not libm variance, and the
|
||||||
|
residual is on the order of $10^{-13}$ cents.
|
||||||
|
|
||||||
|
So the split is not 6 specified / 14 unspecified. It is **16 transcription and
|
||||||
|
4 decisions**:
|
||||||
|
|
||||||
|
* **16 pinned by construction** in Chapter 4 — one line each, with a source
|
||||||
|
citation. Transcription work; a decision only where sources genuinely differ.
|
||||||
|
* **3 × `ji-static-5limit-*`** — which 12-note 5-limit scale (the comma choices
|
||||||
|
for the chromatic degrees) is genuinely unsettled and needs one ratification.
|
||||||
|
* **`ji-adaptive-5limit`** — needs a real algorithm under
|
||||||
|
`req:tuning:adaptive-tuning-purity`. Apply the in-house pattern:
|
||||||
|
`req:pitch:spelling-algorithm` pins `SpellingAlgorithmId "default"` at
|
||||||
|
version 1 to a named algorithm and errors on any other identifier. Do the same
|
||||||
|
with a versioned `AdaptiveTuningFunctionId "default"`.
|
||||||
|
|
||||||
|
### Ruling C — P13-S7 — **RATIFIED: the catalog is closed, for now**
|
||||||
|
|
||||||
|
A score **selects** a pitch space and a tuning system from the built-in catalog;
|
||||||
|
it does not define one. Concretely:
|
||||||
|
|
||||||
|
* Amend `req:pitch:default-pitch-space`: "Every score MUST **define** at least
|
||||||
|
one pitch space… Scores MAY **define** additional pitch spaces" becomes
|
||||||
|
*select*, which is the only reading the data model has ever supported.
|
||||||
|
* Correct `ScalePosition`'s comment (`core_spec.tex:934`) — "References an entry
|
||||||
|
in the score's pitch-space registry" — to name the **built-in** catalog. The
|
||||||
|
registry it points at does not exist and, under this ruling, will not.
|
||||||
|
* **No `pitch_spaces` or `tuning_systems` field is added.** Score-local
|
||||||
|
definition is recorded as a deferred major with its reason stated, not left
|
||||||
|
as an unwritten intention.
|
||||||
|
|
||||||
|
This resolves P13-S7 rather than deferring it: the contradiction was between a
|
||||||
|
requirement and a data model, and the requirement moves.
|
||||||
|
|
||||||
|
**Implement all of it; freeze almost none of it.** The ruling does not shrink
|
||||||
|
the *implementation* surface — the 22 Chapter 4 types still need Rust
|
||||||
|
definitions, because the built-in catalog's 13 pitch spaces and 20 tuning
|
||||||
|
systems have to be expressed *somewhere*, and the P13-S2 guard's structural
|
||||||
|
replacement is a lookup from `PitchSpaceId` to `PositionStructure` over exactly
|
||||||
|
that data. What the ruling removes is the **wire** surface: only
|
||||||
|
`accidental_extensions`, `smufl` and `overrides` are encoded (Ruling D). Every
|
||||||
|
other Chapter 4 type stays in-memory and therefore stays **free to change**,
|
||||||
|
instead of being frozen by `req:binfmt:frozen-layout` before it has ever had a
|
||||||
|
consumer.
|
||||||
|
|
||||||
|
That asymmetry is the whole argument. Twenty never-constructed types — including
|
||||||
|
`SpellingRuleSet` and `TranspositionBehavior`, themselves unimplemented — would
|
||||||
|
otherwise be frozen permanently, sight unseen. `NOTEHEAD_ANCHORS` was
|
||||||
|
hand-written, unconsumed, and wrong in two independent ways; it survived
|
||||||
|
precisely because nothing read it. If deferral proves wrong, a later major adds
|
||||||
|
the registries; if committing proves wrong, we live with the frozen structs
|
||||||
|
*and* still need the migration.
|
||||||
|
|
||||||
|
**Consequence for P13-S2.** The interim guard's accepted cost — "false refusal
|
||||||
|
for score-defined 12-chromatic spaces" — stays **zero**, because no score can
|
||||||
|
define a space. Push 4b still replaces the identifier check with structural
|
||||||
|
resolution over the built-in table, as `req:pitch:space-capability-refusal`
|
||||||
|
requires; the fail-closed contract is unchanged and what the core can *prove*
|
||||||
|
widens from one space to thirteen.
|
||||||
|
|
||||||
|
### Ruling D — **RATIFIED: one major, and `accidental_extensions` is in it**
|
||||||
|
|
||||||
|
`ScoreTuningContext` completes to all three missing fields in major 3:
|
||||||
|
`accidental_extensions`, `smufl`, `overrides`. One migration, not two.
|
||||||
|
|
||||||
|
**`accidental_extensions` is a subtree, not a field**, and that is the price of
|
||||||
|
this ruling stated honestly. `ScoreAccidentalExtensions { base, additions,
|
||||||
|
overrides }` carries `Vec<AccidentalDefinition>`, which pulls in
|
||||||
|
`AccidentalEngraving`, `AccidentalCombination`, `PitchSpaceModification`,
|
||||||
|
`GlyphReference`, a bounding box, and `AnchorPoint` — **none of which exists in
|
||||||
|
`epiphany-core`**, which depends only on `epiphany-determinism`.
|
||||||
|
|
||||||
|
### The correction: they are homonyms, not shared types
|
||||||
|
|
||||||
|
The first scoping said `GlyphReference` and `BoundingBox` "exist but live in
|
||||||
|
`epiphany-layout-ir`" and recommended moving them down. **That was wrong**, and
|
||||||
|
a move would have relocated the wrong types:
|
||||||
|
|
||||||
|
* **`GlyphReference`.** Chapter 4's is
|
||||||
|
`enum { Smufl(u32), Custom(CustomGlyphId), Composite(Vec<GlyphReference>) }`
|
||||||
|
(`core_spec.tex:3181`) — a recursive codepoint reference. layout-ir's is
|
||||||
|
`struct GlyphReference(pub Cow<'static, str>)` (`glyph.rs:50`) — a glyph
|
||||||
|
*name*, a rendering concern. Same name, unrelated types.
|
||||||
|
* **`BoundingBox`.** The one layout-ir holds is **Chapter 7's**
|
||||||
|
(`core_spec.tex:8650`), built on `StaffSpace(pub f32)`. It belongs where it is.
|
||||||
|
|
||||||
|
### And a defect: `AccidentalEngraving` cannot be canonical as written
|
||||||
|
|
||||||
|
`AccidentalEngraving` mixes `bounding_box: BoundingBox` — Chapter 7's
|
||||||
|
`StaffSpace`, **single precision** by deliberate choice (`spatial.rs:3`) — with
|
||||||
|
`advance_width: SpaceUnit`, which is `CanonicalF64`. Resolved layout is
|
||||||
|
**non-canonical** (`binary_format.tex:2521`, `:3211`), so f32 is correct there.
|
||||||
|
But this ruling puts `accidental_extensions` inside `ScoreTuningContext`, which
|
||||||
|
**is** canonical state, and `req:determinism:canonical-floating-point` requires
|
||||||
|
canonical floats to be "finite IEEE 754 **binary64**". As specified, the field
|
||||||
|
would put single-precision floats into canonical bytes.
|
||||||
|
|
||||||
|
**RATIFIED: Chapter 4 gets its own `SpaceUnit`-based engraving box.** All four
|
||||||
|
edges become `SpaceUnit`, the type `advance_width` already uses. This makes
|
||||||
|
`AccidentalEngraving` wholly core-typed, removes the backwards Chapter 4 →
|
||||||
|
Chapter 7 dependency, and satisfies Appendix D. Chapter 7's `BoundingBox` is
|
||||||
|
untouched and stays in layout-ir.
|
||||||
|
|
||||||
|
So there is **no crate move**. Step 0 is *define Chapter 4's glyph and engraving
|
||||||
|
vocabulary as new core types*, and layout-ir's homonyms are left alone. The two
|
||||||
|
`GlyphReference`s must not be unified — they are different concepts that happen
|
||||||
|
to share a word.
|
||||||
|
|
||||||
|
Nothing else rides along. The survey found one other deferred field addition
|
||||||
|
(`epiphany-core/DECISIONS.md:431`, a configurable-order `Score` field with **no
|
||||||
|
consumer**), deliberately excluded — a field with no consumer is how the
|
||||||
|
`Staff::default_clef` and `NOTEHEAD_ANCHORS` findings started.
|
||||||
|
|
||||||
|
Ruling C's registries, if granted, must land in **this** major or wait for a
|
||||||
|
later one; they must not split `ScoreTuningContext`'s completion across two
|
||||||
|
migrations.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 5. Work breakdown
|
||||||
|
|
||||||
|
Genuinely large — the first pass in a while that wants a real fan-out, but not
|
||||||
|
until §4 is answered. Sketch, in dependency order:
|
||||||
|
|
||||||
|
1a. **Spec corrections (mechanical).** S5's three catalog rows to full register;
|
||||||
|
S7's "define" → "select" and the `ScalePosition` comment; Chapter 4's
|
||||||
|
`AccidentalEngraving` onto a `SpaceUnit`-based box (Ruling D). No new
|
||||||
|
requirements, so the `requirement_labels.rs` counts **must not move** — if
|
||||||
|
they do, something unintended happened.
|
||||||
|
1b. **S6 temperament constructions, drafted for review.** A non-normative
|
||||||
|
artifact with a cited source per construction, *not* an edit to
|
||||||
|
`core_spec.tex`. An agent writing Werckmeister III from memory into a
|
||||||
|
normative document is the `NOTEHEAD_ANCHORS` failure exactly: hand-written,
|
||||||
|
unverifiable in-tree, and load-bearing. Review gates promotion.
|
||||||
|
2. **Chapter 4 vocabulary in core.** The glyph and engraving types as *new* core
|
||||||
|
types (Ruling D). Do **not** unify with layout-ir's homonyms.
|
||||||
|
3. **Major-3 delta.** Written against the real types once they exist, with the
|
||||||
|
byte-for-byte migration `sec:evolution:migration` requires
|
||||||
|
(`sec:evolution:major1`/`major2` are the models — a major MUST ship a
|
||||||
|
documented byte-for-byte migration per `sec:evolution:migration`).
|
||||||
|
2. **Types (in-memory).** The Chapter 4 type surface, unfrozen: `PitchSpace`,
|
||||||
|
`PositionStructure`, `IntervalAlgebra`, the registries, `TuningSystem`,
|
||||||
|
`TuningResolution` and their kin. **No `Codec` impls** for these — Ruling C
|
||||||
|
keeps them off the wire, which is what keeps them free to change.
|
||||||
|
3. **The built-in catalog as data.** The 13 pitch spaces and 20 tuning systems
|
||||||
|
as constants, with the 16 constructible temperaments expressed *by their
|
||||||
|
construction* (Ruling B) rather than as cent tables, so the spec and the code
|
||||||
|
state the same rule in the same form.
|
||||||
|
4. **Codec — the narrow part.** `ScoreTuningContext`'s three added fields only,
|
||||||
|
with `dec_*_v2` sub-decoders preserving the frozen prior layout exactly as
|
||||||
|
major 2 did for the cross-cutting bodies. This is the entire wire delta.
|
||||||
|
5. **The resolver.** `req:tuning:tuning-resolution-order`'s five-scope walk,
|
||||||
|
per-component and independent; `req:tuning:tuning-system-compatibility`'s
|
||||||
|
rejection rule.
|
||||||
|
6. **Retire the P13-S2 interim guard.** Replace the `cmn-12` identifier check in
|
||||||
|
`Pitch::transposed` and `twelve_tet_semitone` with
|
||||||
|
`PositionStructure::DiatonicOverChromatic` resolution over the built-in
|
||||||
|
table — **replace, not preserve** (`req:pitch:space-capability-refusal`, and
|
||||||
|
Ruling B of `PLAN_P13S2_CMN24.md` says so explicitly). The fail-closed
|
||||||
|
contract stays; what the core can *prove* widens from one space to thirteen.
|
||||||
|
`cmn-24` transposition working end-to-end is this pass's proof of life.
|
||||||
|
7. **Accidental registries and SMuFL.** `req:tuning:smufl-version-fallback`,
|
||||||
|
`req:tuning:accidental-modification-compatibility`, and the engrave-side
|
||||||
|
consumers.
|
||||||
|
8. **Conformance.** A new step gating the built-in catalog: every promised
|
||||||
|
identifier resolves, resolution is reproducible across runs, and each pinned
|
||||||
|
temperament is checked against its construction rather than against a table
|
||||||
|
copied from the implementation.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 6. Traps
|
||||||
|
|
||||||
|
* **A major MUST ship a documented migration.** `sec:evolution:migration` is
|
||||||
|
explicit, and the v0→v1 and v1→v2 entries are the shape to match. A major
|
||||||
|
that lands without one is the defect this project would notice last.
|
||||||
|
* **`ScoreTuningContext` is positional and frozen.** Field *order* is as
|
||||||
|
load-bearing as the field set, and the compiler cannot see it — the same
|
||||||
|
invisibility that made the Text Projection layer verify field order by
|
||||||
|
mechanical `encode_canonical`-vs-`project` diff.
|
||||||
|
* **The interim guard must be deleted, not widened.** Ratified in P13-S2. A 4b
|
||||||
|
that adds registry resolution *beside* the name check has preserved the
|
||||||
|
temporary mechanism as policy.
|
||||||
|
* **`twelve_tet_semitone` becomes a lie once non-12 spaces resolve.** It is
|
||||||
|
public, has six callers across three crates, and renaming it is a breaking
|
||||||
|
change in `epiphany-core` — cheaper now than later.
|
||||||
|
* **The spelling pre-pass stays 12-chromatic.** Line-of-fifths is `7·lof mod 12`
|
||||||
|
in its bones. `cmn-24` positions land in `spelling_unavailable`, which the
|
||||||
|
P13-S2 conformance note already records. 4b should not quietly acquire a
|
||||||
|
microtonal spelling algorithm; that is its own ratification.
|
||||||
|
* **Built-in catalogs are implementation-provided, not serialized.** The 13
|
||||||
|
pitch spaces and 20 tuning systems are referenced by id and do not go on the
|
||||||
|
wire. Only score-*local* definitions and overrides would — which is precisely
|
||||||
|
what Ruling C decides.
|
||||||
Binary file not shown.
|
|
@ -933,7 +933,9 @@ relationships are defined.
|
||||||
\begin{lstlisting}[language=Rust]
|
\begin{lstlisting}[language=Rust]
|
||||||
pub struct ScalePosition {
|
pub struct ScalePosition {
|
||||||
/// The pitch space this position is defined within. References an
|
/// The pitch space this position is defined within. References an
|
||||||
/// entry in the score's pitch-space registry.
|
/// identifier in the built-in pitch-space catalog
|
||||||
|
/// (`sec:tuning:builtin`); a score selects from this catalog and
|
||||||
|
/// does not define its own entries.
|
||||||
pub space: PitchSpaceId,
|
pub space: PitchSpaceId,
|
||||||
|
|
||||||
/// The position within that space. Interpretation is space-defined.
|
/// The position within that space. Interpretation is space-defined.
|
||||||
|
|
@ -1019,17 +1021,32 @@ pub enum PitchSpacePosition {
|
||||||
|
|
||||||
\begin{requirement}
|
\begin{requirement}
|
||||||
\label{req:pitch:default-pitch-space}
|
\label{req:pitch:default-pitch-space}
|
||||||
Every score \MUST{} define at least one pitch space. The default
|
Every score \MUST{} select at least one pitch space from the
|
||||||
|
built-in catalog (Section~\ref{sec:tuning:builtin}). The default
|
||||||
pitch space for CMN scores is \texttt{cmn-12}, which is
|
pitch space for CMN scores is \texttt{cmn-12}, which is
|
||||||
diatonic-over-chromatic in structure (seven diatonic nominals
|
diatonic-over-chromatic in structure (seven diatonic nominals
|
||||||
A--G over twelve chromatic positions), anchored to the score's
|
A--G over twelve chromatic positions), anchored to the score's
|
||||||
reference pitch as resolved through the score tuning context
|
reference pitch as resolved through the score tuning context
|
||||||
(Chapter~\ref{ch:tuning}). Scores \MAY{} define additional pitch
|
(Chapter~\ref{ch:tuning}). Scores \MAY{} select additional pitch
|
||||||
spaces; pitches in different spaces cannot be directly compared
|
spaces from that catalog; pitches in different spaces cannot be
|
||||||
and operations between them \MUST{} go through an explicit
|
directly compared and operations between them \MUST{} go through an
|
||||||
space-conversion mechanism.
|
explicit space-conversion mechanism.
|
||||||
\end{requirement}
|
\end{requirement}
|
||||||
|
|
||||||
|
\begin{rationale}
|
||||||
|
Score-local pitch-space definition --- a score introducing a pitch
|
||||||
|
space of its own, beyond selecting from the built-in catalog --- is
|
||||||
|
deferred to a later schema major. The Chapter~\ref{ch:tuning} type
|
||||||
|
surface (\texttt{PitchSpace}, \texttt{PositionStructure},
|
||||||
|
\texttt{IntervalAlgebra}, and their kin) has never had a consumer;
|
||||||
|
committing a registry for it to the wire now would freeze that
|
||||||
|
surface permanently under \texttt{req:binfmt:frozen-layout}, before
|
||||||
|
any implementation has exercised it. Selecting from the built-in
|
||||||
|
catalog is the only reading the data model has ever supported: neither
|
||||||
|
\texttt{Score} nor \texttt{ScoreTuningContext} carries a pitch-space
|
||||||
|
or tuning-system registry, and none is added here.
|
||||||
|
\end{rationale}
|
||||||
|
|
||||||
\subsection{Octave Convention}
|
\subsection{Octave Convention}
|
||||||
\label{sec:pitch:octave}
|
\label{sec:pitch:octave}
|
||||||
|
|
||||||
|
|
@ -3113,11 +3130,36 @@ pub enum PitchSpaceModification {
|
||||||
|
|
||||||
\subsection{Accidental Engraving Metadata}
|
\subsection{Accidental Engraving Metadata}
|
||||||
|
|
||||||
|
\texttt{AccidentalEngraving} is reachable from canonical score state ---
|
||||||
|
via \texttt{AccidentalDefinition} inside
|
||||||
|
\texttt{ScoreAccidentalExtensions}, which hangs off
|
||||||
|
\texttt{ScoreTuningContext} --- so every field it carries must itself be
|
||||||
|
canonical. Its bounding box therefore cannot reuse
|
||||||
|
Chapter~\ref{ch:layout-ir}'s \texttt{BoundingBox}, which is built on
|
||||||
|
\texttt{StaffSpace} (single-precision \texttt{f32}) and belongs to the
|
||||||
|
non-canonical resolved-layout cache. This chapter defines its own box
|
||||||
|
type over \texttt{SpaceUnit} instead:
|
||||||
|
|
||||||
|
\begin{lstlisting}[language=Rust]
|
||||||
|
/// A bounding box over canonical space units, used for engraving
|
||||||
|
/// metadata that lives in canonical score state. Distinct from
|
||||||
|
/// Chapter 7's `BoundingBox` (built on `StaffSpace`, single precision,
|
||||||
|
/// for the non-canonical resolved-layout cache): this type's edges are
|
||||||
|
/// `SpaceUnit` (`CanonicalF64`), per
|
||||||
|
/// `req:determinism:canonical-floating-point`.
|
||||||
|
pub struct EngravingBoundingBox {
|
||||||
|
pub left: SpaceUnit,
|
||||||
|
pub right: SpaceUnit,
|
||||||
|
pub top: SpaceUnit,
|
||||||
|
pub bottom: SpaceUnit,
|
||||||
|
}
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
\begin{lstlisting}[language=Rust]
|
\begin{lstlisting}[language=Rust]
|
||||||
pub struct AccidentalEngraving {
|
pub struct AccidentalEngraving {
|
||||||
/// Bounding box in staff-space units, relative to the glyph's
|
/// Bounding box in canonical space units, relative to the glyph's
|
||||||
/// anchor point.
|
/// anchor point.
|
||||||
pub bounding_box: BoundingBox,
|
pub bounding_box: EngravingBoundingBox,
|
||||||
|
|
||||||
/// Where the glyph attaches to the note: typically the geometric
|
/// Where the glyph attaches to the note: typically the geometric
|
||||||
/// center or a custom anchor for compound glyphs.
|
/// center or a custom anchor for compound glyphs.
|
||||||
|
|
@ -3136,6 +3178,27 @@ pub struct AccidentalEngraving {
|
||||||
}
|
}
|
||||||
\end{lstlisting}
|
\end{lstlisting}
|
||||||
|
|
||||||
|
\begin{rationale}
|
||||||
|
Engraving metadata that lives in canonical state must carry canonical
|
||||||
|
precision. Chapter~\ref{ch:layout-ir}'s coordinates are
|
||||||
|
single-precision by requirement
|
||||||
|
(Requirement~\ref{req:layoutir:staff-space-coordinates}) and reach the
|
||||||
|
wire in the \texttt{LayoutCache}, which the Binary Format companion
|
||||||
|
defines as an independent \emph{non-canonical} chunk --- so
|
||||||
|
\texttt{StaffSpace} is correct there. But
|
||||||
|
\texttt{accidental\_extensions} lives on
|
||||||
|
\texttt{ScoreTuningContext}, which \emph{is} canonical, and
|
||||||
|
Requirement~\ref{req:determinism:canonical-floating-point} requires
|
||||||
|
canonical stored floats to be finite IEEE~754 binary64.
|
||||||
|
\texttt{EngravingBoundingBox} makes \texttt{AccidentalEngraving}
|
||||||
|
wholly core-typed, over the same \texttt{SpaceUnit} that
|
||||||
|
\texttt{advance\_width} already uses, and removes what would
|
||||||
|
otherwise be a backwards dependency from this chapter onto
|
||||||
|
Chapter~\ref{ch:layout-ir}. Chapter~\ref{ch:layout-ir}'s
|
||||||
|
\texttt{BoundingBox} is unaffected and remains the correct type for
|
||||||
|
resolved-layout coordinates.
|
||||||
|
\end{rationale}
|
||||||
|
|
||||||
\subsection{Combination Behavior}
|
\subsection{Combination Behavior}
|
||||||
|
|
||||||
Most accidentals do not combine; a note carries one accidental at a
|
Most accidentals do not combine; a note carries one accidental at a
|
||||||
|
|
@ -3494,11 +3557,13 @@ identifiers with the specified semantics.
|
||||||
\texttt{edo-72} & 72-tone equal division. Common in research and
|
\texttt{edo-72} & 72-tone equal division. Common in research and
|
||||||
contemporary microtonal practice. \\
|
contemporary microtonal practice. \\
|
||||||
\texttt{ji-5limit} & 5-limit just intonation lattice with HEJI
|
\texttt{ji-5limit} & 5-limit just intonation lattice with HEJI
|
||||||
accidentals. Two-dimensional (prime axes 3, 5). \\
|
accidentals. Three-dimensional; prime basis $\{2, 3, 5\}$ in
|
||||||
|
ascending order (leading component is the octave, prime 2). \\
|
||||||
\texttt{ji-7limit} & 7-limit JI lattice with HEJI accidentals.
|
\texttt{ji-7limit} & 7-limit JI lattice with HEJI accidentals.
|
||||||
Three-dimensional. \\
|
Four-dimensional; prime basis $\{2, 3, 5, 7\}$ in ascending order. \\
|
||||||
\texttt{ji-11limit} & 11-limit JI lattice with HEJI accidentals.
|
\texttt{ji-11limit} & 11-limit JI lattice with HEJI accidentals.
|
||||||
Four-dimensional. \\
|
Five-dimensional; prime basis $\{2, 3, 5, 7, 11\}$ in ascending
|
||||||
|
order. \\
|
||||||
\texttt{maqam-base} & Skeletal maqam framework with quarter-flat
|
\texttt{maqam-base} & Skeletal maqam framework with quarter-flat
|
||||||
and quarter-sharp \texttt{CmnChromatic} accidentals, denominated by the
|
and quarter-sharp \texttt{CmnChromatic} accidentals, denominated by the
|
||||||
space's chromatic layer under Requirement~\ref{req:pitch:alteration-unit}.
|
space's chromatic layer under Requirement~\ref{req:pitch:alteration-unit}.
|
||||||
|
|
@ -3508,6 +3573,16 @@ identifiers with the specified semantics.
|
||||||
\bottomrule
|
\bottomrule
|
||||||
\end{longtable}
|
\end{longtable}
|
||||||
|
|
||||||
|
\begin{rationale}
|
||||||
|
The three JI spaces include prime 2 in their basis, per
|
||||||
|
Requirement~\ref{req:pitch:ji-vector-basis}, rather than assuming octave
|
||||||
|
equivalence. A \texttt{JiVector} is an absolute position, not a pitch
|
||||||
|
class: without the prime-2 exponent, \texttt{ji-5limit} could not
|
||||||
|
distinguish C4 from C5. None of these three declares octave-reduced
|
||||||
|
equivalence, so full register is preserved, as that requirement's
|
||||||
|
default already states.
|
||||||
|
\end{rationale}
|
||||||
|
|
||||||
\paragraph{Conformance note.}
|
\paragraph{Conformance note.}
|
||||||
At this revision the default spelling pre-pass is structurally
|
At this revision the default spelling pre-pass is structurally
|
||||||
12-chromatic and therefore reports \texttt{spelling\_unavailable} for
|
12-chromatic and therefore reports \texttt{spelling\_unavailable} for
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue