diff --git a/spec/PASS12_BATCH.md b/spec/PASS12_BATCH.md index f04a03e..0ce1d4f 100644 --- a/spec/PASS12_BATCH.md +++ b/spec/PASS12_BATCH.md @@ -10,6 +10,13 @@ surfaced five candidates, crossing the ≥3 threshold. This file is the running collection; G ratifies (or defers/rejects) the batch when Phase 2's open questions are resolved. F collects, F does not resolve. +**Pass 12 tranche 1 landed (2026-07-02):** the audit *spec-alignment* set — +places where spec text trailed an already-made disposition (catalog, crate +DECISIONS, PHASE2_QUICKSTART) — was ratified directly into `core_spec.tex` / +`operation_catalog.tex` (0.2.0 → 0.3.0); dispositions in +`PASS12_RATIFICATION_LOG.md`. That tranche resolves **none** of the rows +below; they remain open for G. + ## How an item lands here When implementation hits a behavior the ratified spec does not determine, the @@ -31,10 +38,15 @@ code instead is the failure mode this batch exists to prevent. | ~~P12-I3~~ **RESOLVED (I-4a)** | `epiphany-layout-ir` I | The bundled `BRAVURA_METRICS` were *approximations* disagreeing with the renderer's genuine outlines. **Resolved by I-4a:** the metrics table is re-extracted from the **same** SHA-pinned `bravura-1.392` font the outlines come from, with bboxes rounded *outward* so each metric box contains the drawn ink (a `render-svg` test proves containment); `BRAVURA_VERSION = SemVer(1, 392, 0)`. A coupled barline-placement bug it surfaced (bottom-origin glyph floated) was fixed in the same increment. | ✅ done | | P12-K1 | `epiphany-ops` K | A v0 `RespellPitch` carried a `ContentHash` *fingerprint* of the spelling, not the `PitchSpelling`. The v0→v1 migration (Operation Catalog, M1) cannot invert a fingerprint, so it recovers the spelling from the score-graph context (an explicit per-pitch spelling attachment whose canonical bytes hash to the fingerprint) and returns `MigrationError::Irreversible` (bundle opens read-only) when the context lacks it. Every other representative payload migrates self-contained; this is the lone exception. Confirm the read-only fallback is the intended disposition vs. requiring a v0 corpus that preserves spelling pre-images. | G / Pass 12 (migration) | | P12-K2 | `epiphany-ops` K | The `Transpose` op (Operation Catalog, M2 Group 1) carries a minimal `chromatic_steps: i32` interval and `reduce_onto` applies it as a CMN *alteration* shift only. Faithful interval algebra (diatonic vs. chromatic intervals, octave/nominal renormalization, transposition in non-CMN pitch spaces) is the deferred Chapter 4 tuning-catalog territory. The prototype also clamps the shifted alteration to the `i8` range, so an extreme transpose silently saturates instead of renormalizing — another reason the representation needs pinning. Pin the interval representation and transposition semantics when the tuning catalog lands. | G / Pass 12 (tuning) | +| P12-H6 | `epiphany-core` H | Decomposition-attachment precedence: the spec says the decomposition pre-pass uses the "same precedence machinery" as spelling, but spelling's machinery is per-score *configurable* with `priority`/timestamp tie-breaks while `DecompositionAttachment` carries no `priority` and the graph has no `DecompositionPrecedence` field. The audit fix implements the fixed default order (`UserChosen > Imported > Propagated > Inferred`, canonical attachment order as tie-break). Decide whether decomposition precedence is configurable (a canonical-codec change) or fixed. | G / Pass 12 (decomposition) | +| P12-H7 | `epiphany-core` H | Authored decompositions for inference-ineligible events: an authored attachment is exactly how a user would notate an *ungriddable* event, but the derived-annotation surface (mirroring spelling, which likewise ignores attachments on spelling-unavailable pitches) only resolves overrides where inferred output exists. Needs a spec answer for both pre-passes. | G / Pass 12 (pre-passes) | +| P12-K3 | `epiphany-ops` K | Content modification of a `SYSTEM_DERIVED` pitch: `ModifyEvent`/`ModifyIdentifiedPitch` can rewrite a synthetic pitch's intrinsic content in place, silently invalidating the id's content-derivation (Invariant 11). The new reduction-time collision check deliberately does not treat in-place rewrites as mints. Decide whether reduction must refuse them outright. | G / Pass 12 (identity) | +| P12-K4 | `epiphany-ops` K | `ResolveConflict` beyond the concurrent case: the spec pins outcomes only for *concurrent* differing resolves; the implementation applies the same rule to causally-later resolves (so an intentional re-resolution cannot supersede) and reads `AlreadyApplied` for any resolve against a `Dismissed` conflict. Also: the meta-conflict record cannot name the contested conflict in `affected_objects` because `TypedObjectId` has no Conflict kind. Pin the causally-later semantics and decide whether conflict records need an addressable object kind. | G / Pass 12 (conflict resolution) | ## Not yet open elsewhere Agent I (Track A) has contributed P12-I1..I3 above. Track B's Agent K has -contributed P12-K1 (Operation Catalog M1). Agent J (Binary Format companion) has -not yet contributed; when it does, append rows — the batch is already open, so it -joins directly (no new threshold). +contributed P12-K1..K4; H has contributed P12-H1..H7 (H6/H7 from the 2026-07 +spec-compliance audit follow-up, alongside K3/K4). Agent J (Binary Format +companion) has not yet contributed; when it does, append rows — the batch is +already open, so it joins directly (no new threshold). diff --git a/spec/PASS12_RATIFICATION_LOG.md b/spec/PASS12_RATIFICATION_LOG.md new file mode 100644 index 0000000..41a5fbf --- /dev/null +++ b/spec/PASS12_RATIFICATION_LOG.md @@ -0,0 +1,39 @@ +# Pass 12 — Ratification Log + +## Tranche 1 (2026-07-02): audit spec-alignment + +The 2026-07 six-agent spec-compliance audit sorted its findings into code-side +MUST fixes (landed separately; see the crate `DECISIONS.md` files and +`CONFORMANCE.md`) and places where the *spec text* trailed a disposition the +project had already made — a documented crate decision, the ratified Operation +Catalog, or the PHASE2_QUICKSTART model the implementation follows. This +tranche ratifies that second set. **No byte-layout changes; architecture +unchanged.** The main Pass 12 batch (`PASS12_BATCH.md`) stays open: the +P12-H/K rows await G's ratification alongside Phase 2's open questions and are +*not* resolved here. + +`adopt` = blessed the implementation/catalog behavior as normative spec text. +`fixed` = the spec text was contradictory or stale and changed. + +| Item | Disposition | Spec locus | Authority followed | +|---|---|---|---| +| ModifyEvent metric placement | **adopt** — the catalog's §ModifyEvent reduction rule now states: a *metric* move (different `Musical` position/duration) is materialised, re-sorting the owning voice (id-tiebroken), behind a **placement precondition** read from the reducer's canonical voice-occupancy index — a non-positive span or an overlap with another live event refuses as a clean `EventDurationInvalid` no-op; a materialised move updates the occupancy index; non-metric moves and tuplet-member trimming stay deferred; same-placement field edits apply in place | operation_catalog §ModifyEvent | ops DECISIONS "ModifyEvent materializes metric placement changes (trim/move)"; `reduce.rs::modify_event` | +| Slur/Spanner re-anchoring | **fixed (core-spec↔catalog contradiction)** — the rule-table rows now read: re-anchor to the nearest surviving endpoint/anchor while ≥ 1 survives, cascade-delete only when none does; a two-endpoint slur collapses onto its sole survivor (reference-clean degenerate form); proximity-aware re-targeting and per-spanner-kind bounds are deferred refinements (P11-C5 stand-in). Previously the Slur row said "nearest forward event in same voice; cascade if fewer than two members survive" | core_spec §The Re-Anchoring Rule Table | operation_catalog §DeleteEvent Re-anchoring; `reduce.rs` ledger + `materialize_graph_delete` (kept consistent per ops DECISIONS "the graph follows the ledger") | +| RewriteTuplets payload | **adopt (id-only v1)** — core spec drops `TupletRewrite { tuplet, new_ratio, new_members }` for the catalog's `RewriteTuplets { tuplets: Vec }`, and states normatively that graph-aware reduction MUST refuse the variant as an ill-formed compensation rather than fabricate rewritten values; a future value-carrying payload revision reopens it (`ReplaceWithRest`/`CascadeDeleteTuplets` are the applicable compensations until then). Keeps v1 bytes stable; the functionality hole is documented instead of contradictory | core_spec §DeleteEvent (payload, preconditions, effect) | operation_catalog §DeleteEvent; `reduce.rs` refusal (`TupletCompensationInvalid`) | +| Operation-block summaries | **adopt (bundle M4)** — an `OperationEnvelopeBlock` chunk payload is the envelope vector only (the spec'd `block_id` field was unrealizable: a content-addressed chunk cannot embed its own id); `OperationBlockSummary { dvv_summary, min_stamp, max_stamp }` lives in the **manifest**, keyed by the block's `ChunkId`, as opaque ops-supplied, non-canonical, optional metadata; the "writers SHOULD order blocks by min_stamp" line is dropped — the canonical manifest encoding sorts chunk references ascending by encoded form (Appendix D), so stamp-ordered scanning goes through the summaries | core_spec Ch8 §Operation Envelope Blocks + §Manifest | bundle DECISIONS "Operation-envelope block summary metadata is carried (M4 follow-up)"; `manifest.rs::OperationBlockSummary` | +| Pre-pass output model | **fixed (stale Ch2/Ch3 text)** — the spelling and decomposition pre-passes produce **canonical derived annotations**: deterministic functions of (materialized graph, profile, versioned algorithm id), recomputed on materialization, never stored as graph state or serialized into canonical chunks — replacing "the pre-pass MUST produce / write `Inferred`-source attachments" and "stored as an attachment on the event". The pre-pass now MUST NOT mint attachments; promotion to a stored `UserChosen` attachment happens only via explicit editing operations. The incremental-re-run MUST is demoted to MAY (cache/incremental recompute permitted; neither observable in output; cache invalidates on derivation-key change). Ch1 design-principle retitled "notational rhythm is *derived*" | core_spec Ch2 §Spelling Source/Precedence/Pre-Pass + rationale; Ch3 §Notational Decomposition + §Decomposition Pre-Pass; Ch1 design principles | PHASE2_QUICKSTART "Canonical model: derived annotations, not stored objects"; `prepass.rs::derive_annotations` | +| Spelling tie-break | **adopt** — conflicts break by precedence, then attachment `priority` (higher wins), then **canonical attachment order** (earliest in the score's canonical serialization wins); the "attachment creation timestamp" tie-break is deleted — attachments carry no timestamp, and one would hang resolution on non-canonical state | core_spec Ch2 §Configurable Precedence | `prepass.rs::resolve_spelling` | +| Conflict-registry location | **fixed** — `Score.conflicts: ConflictRegistry` removed from the graph root; the registry is a component of canonical **materialized state** (which Ch6's requirement already said), i.e. a reduction product, not authored content; the hierarchy table, chapter overview, and §Conflict Records prose updated to match | core_spec Ch5 §Score root; Ch6 §Conflict Records / §The Conflict Registry | `reduce.rs::MaterializedState.conflicts` | +| SolverTier::Stub | **adopt** — the spec enum gains the code's `Stub` variant: not a conformance tier, an interface-only/passthrough solver ordered below every conformant tier; declaring it makes no conformance claim and satisfies no minimum-tier requirement. Never canonically serialized, so no byte impact | core_spec Ch7 §Conformance Tiers | `layout-ir/solver.rs::SolverTier` | + +**Version movements.** Operation Catalog 0.2.0 → 0.3.0 (ModifyEvent +reduction-rule behavior text). Core spec: revision-history row "Pass 12 +tranche 1 (audit spec-alignment)" appended. + +**Deliberately not touched here** (still open in `PASS12_BATCH.md`): every +P12-H/K row (algorithm-id ratification, decomposition precedence +configurability, authored decompositions for ineligible events, system-pitch +content modification, ResolveConflict beyond the concurrent case, RespellPitch +v0 migration fallback, Transpose interval algebra), plus the audit's Push-3 +wiring tracks (constraints, overrides, validation modes, edit barriers, +operation index) — those are code work, not spec alignment. diff --git a/spec/core_spec.pdf b/spec/core_spec.pdf index f3a9ceb..0aab333 100644 Binary files a/spec/core_spec.pdf and b/spec/core_spec.pdf differ diff --git a/spec/core_spec.tex b/spec/core_spec.tex index 90ddfdd..235a96e 100644 --- a/spec/core_spec.tex +++ b/spec/core_spec.tex @@ -487,7 +487,7 @@ identity. \endhead Score & --- & Document root. Carries metadata, instruments, global staves, staff groups, tuning context, tempo map, - canvas, conflict registry. \\ + canvas. \\ Canvas & --- & Spatial root. Partitioned into regions. \\ Region & \texttt{RegionId} & Spatial-temporal container. Declares time model (metric/proportional/aleatoric) and @@ -661,7 +661,7 @@ orthogonal to file-format profiles \ref{ch:graph} & Score graph, event arena, cross-cutting structures, regions, staff identity (Staff vs. StaffInstance), polymeter via per-staff metric grids, voice - origin, conflict registry, graph invariants. \\ + origin, graph invariants. \\ \ref{ch:semops} & Operation framework, canonical reduction, DVV causal contexts, operation effects, tombstones, conflict records, transactions, re-anchoring, undo, LWW discipline. \\ @@ -1221,8 +1221,9 @@ pub enum SpellingSource { UserChosen, /// Inferred by the spelling pre-pass from key signature and - /// context. Lower precedence; may be revised by re-running the - /// pre-pass. + /// context. Lowest default precedence. The pre-pass does not + /// store attachments (its output is a derived annotation); + /// this variant ranks that output in the precedence order. Inferred, /// Imported from a foreign format. @@ -1240,9 +1241,13 @@ pub enum SpellingSource { Editing operations that respell a pitch \MUST{} produce attachments with source \texttt{UserChosen}. Editing operations that move or transpose a pitch \MUST{} produce attachments with source - \texttt{Propagated}. The spelling pre-pass (Section~\ref{sec:pitch:prepass}) - \MUST{} produce attachments with source \texttt{Inferred}. Foreign-format - importers \MUST{} produce attachments with source \texttt{Imported}. + \texttt{Propagated}. Foreign-format importers \MUST{} produce + attachments with source \texttt{Imported}. The spelling pre-pass + (Section~\ref{sec:pitch:prepass}) \MUSTNOT{} mint attachments: its + inferred spellings are derived annotations reported with + \texttt{Inferred} provenance, promoted to a stored + \texttt{UserChosen} attachment only by an explicit editing + operation. \end{requirement} \subsection{Configurable Precedence} @@ -1266,17 +1271,29 @@ precedence is: default; for example, a workflow that treats MusicXML imports as authoritative may rank \texttt{Imported} above \texttt{UserChosen}. Conflicts are broken first by precedence, then by the \texttt{priority} - field of the attachment, then by attachment creation timestamp. + field of the attachment (higher wins), then by canonical attachment + order (the attachment appearing earliest in the score's canonical + serialization wins). Attachments carry no creation timestamp: a + timestamp tie-break would hang resolution on non-canonical state. \end{requirement} \subsection{The Spelling Pre-Pass} \label{sec:pitch:prepass} -When a score is loaded, edited, or about to be rendered, the spelling -pre-pass produces \texttt{Inferred}-source attachments for every pitch -that lacks a higher-precedence attachment. The pre-pass \MUST{} be -deterministic: given the same score graph and the same precedence -configuration, it \MUST{} produce identical attachments. +When a score is materialized (on load, after an edit, or ahead of +rendering), the spelling pre-pass computes an inferred spelling for +every spelling-eligible pitch. Its output is a \emph{canonical +derived annotation}: a deterministic function of the materialized +score graph, the active profile, and the versioned +\texttt{SpellingAlgorithmId}, recomputed on materialization and +never stored as graph state or serialized into canonical chunks. +Where a stored attachment targets the pitch, the resolved annotation +reports that attachment's spelling and provenance per the precedence +configuration (Section~\ref{sec:pitch:precedence}); the pre-pass +supplies the \texttt{Inferred}-provenance spelling that applies when +no attachment outranks it. The pre-pass \MUST{} be deterministic: +given the same materialized graph, precedence configuration, and +algorithm version, it \MUST{} produce identical annotations. The pre-pass operates as follows: @@ -1293,19 +1310,30 @@ The pre-pass operates as follows: \item The harmonic context (concurrent pitches in other voices). \item Any active scope-level \texttt{Rule} attachments. \end{enumerate} - \item Write an \texttt{Inferred}-source attachment for each pitch. + \item Report an \texttt{Inferred}-provenance derived annotation for + each pitch. \end{enumerate} -The pre-pass \MUST{} be incremental: an edit to a single pitch \MUST{} -re-run the pre-pass only on the affected measure and voice (and forward -through measures whose context is altered, until the context stabilizes). +Because derived annotations are not stored, a change to the algorithm +version deterministically invalidates them without any state +migration. Implementations \MAY{} cache derived annotations and +\MAY{} recompute incrementally (re-running only the affected measure +and voice, and forward through measures whose context is altered, +until the context stabilizes); a cache \MUST{} be invalidated when +the derivation key --- graph, profile, algorithm version --- changes, +and neither caching nor incrementality may be observable in the +annotations produced. \begin{rationale} - Storing inferred spellings as attachments---rather than computing them - at draw time---makes spellings inspectable in the UI, editable by - promotion to \texttt{UserChosen}, and deterministic for serialization - diffs. The cost is one attachment per unspelled pitch, which is - negligible. + Deriving inferred spellings---rather than storing them as + attachments---keeps algorithm output out of canonical state: two + replicas at the same (graph, profile, algorithm version) agree on + annotations byte-for-byte without ever exchanging them, an + algorithm upgrade cannot strand stale inferred state, and + serialization never churns on re-inference. Inferred spellings + remain inspectable in the UI and editable by promotion: accepting + one mints a \texttt{UserChosen} attachment through an editing + operation, which then outranks the pre-pass. \end{rationale} \begin{openquestion} @@ -1491,11 +1519,11 @@ proportional, and aleatoric time models simultaneously. interchangeable. The algebra (position $+$ duration $\rightarrow$ position; position $-$ position $\rightarrow$ duration; position $+$ position is undefined) is enforced at the type level. - \item[Sounding duration is data; notational rhythm is attached.] + \item[Sounding duration is data; notational rhythm is derived.] A note's sounding duration is intrinsic; its notated decomposition (notehead values, ties, dots, tuplet membership) is produced by a deterministic pre-pass analogous to the spelling pre-pass and is - overridable per-event. + overridable per-event by an authored attachment. \item[Multiple time models coexist.] A score \MUST{} support metric, proportional, and aleatoric regions, possibly concurrent on different staves. The region's declared time model determines the @@ -2097,9 +2125,12 @@ Its \emph{notational decomposition} is the sequence of notehead values, augmentation dots, and ties used to draw that duration on the staff. The decomposition is computed from the sounding duration by a -deterministic pre-pass and stored as an attachment on the event. The -attachment is overridable by the user; the pre-pass produces an -inferred decomposition that the user may accept or replace. +deterministic pre-pass as a \emph{canonical derived annotation} --- +recomputed on materialization, never stored graph state --- under the +same output model as the spelling pre-pass +(Section~\ref{sec:pitch:prepass}). The user may accept the inferred +decomposition or override it by authoring a decomposition attachment, +which takes precedence. \subsection{The Notational Decomposition} @@ -2141,9 +2172,10 @@ machinery, same pre-pass discipline. \subsection{The Decomposition Pre-Pass} -When a score is loaded or edited, the decomposition pre-pass produces -inferred decompositions for events that lack a higher-precedence -attachment. The algorithm is, in outline: +When a score is materialized, the decomposition pre-pass computes +inferred decompositions, reported as derived annotations; an authored +higher-precedence attachment overrides the inferred value in the +resolved annotation. The algorithm is, in outline: \begin{enumerate} \item For each event in time order within a voice and measure, @@ -2161,11 +2193,14 @@ attachment. The algorithm is, in outline: \end{enumerate} \begin{requirement} - The decomposition pre-pass \MUST{} be deterministic: given identical - score graph and identical configuration, it \MUST{} produce identical - decompositions. The pre-pass \MUST{} be incremental: an edit to one - event \MUST{} re-run the pre-pass only on the affected voice and - measure, with propagation only as far as the context is altered. + The decomposition pre-pass \MUST{} be deterministic: given + identical materialized graph, configuration, and algorithm + version, it \MUST{} produce identical decompositions. Its output + is a derived annotation, never stored graph state. Implementations + \MAY{} cache and \MAY{} recompute incrementally (re-running only + the affected voice and measure, with propagation only as far as + the context is altered); neither may be observable in the + annotations produced. \end{requirement} \begin{openquestion} @@ -3298,7 +3333,12 @@ Chapters~\ref{ch:pitch}--\ref{ch:tuning} into a coherent whole. \label{sec:graph:score} The score is the root object. All other objects in the specification -exist within or reference into a score. +exist within or reference into a score. Conflict records are +deliberately \emph{not} part of the score graph: the +\texttt{ConflictRegistry} produced by canonical reduction is a +component of the canonical \emph{materialized state} +(Chapter~\ref{ch:semops}), recomputed with it, and persisting there +until resolved or dismissed by explicit operations. \begin{lstlisting}[language=Rust] pub struct Score { @@ -3326,11 +3366,6 @@ pub struct Score { /// graphic gestures, comments, and analytical annotations. pub cross_cutting: CrossCuttingRegistry, - /// Conflict records produced by the canonical reduction - /// (Chapter~\ref{ch:semops}). Conflict records persist until - /// resolved or dismissed by explicit operations. - pub conflicts: ConflictRegistry, - /// Tuning systems, pitch spaces, and reference pitch. pub tuning_context: ScoreTuningContext, @@ -6349,9 +6384,9 @@ yields a deletion record rather than the original object. When an operation cannot apply cleanly, the reduction produces a \texttt{Conflicted} effect referencing a \texttt{ConflictRecord} in -the score's conflict registry. Conflict records are first-class -graph objects: stable, addressable, visible to users, and -addressable by subsequent operations. +the canonical conflict registry (a component of materialized state; +see below). Conflict records are first-class: stable, addressable, +visible to users, and addressable by subsequent operations. \subsection{Conflict Record Type} @@ -6503,8 +6538,9 @@ pub enum ResolutionAction { \subsection{The Conflict Registry} -The score graph carries a top-level conflict registry alongside the -cross-cutting registry: +Canonical materialized state carries a top-level conflict registry +(the score graph does not --- conflict records are a reduction +product, not authored content): \begin{lstlisting}[language=Rust] pub struct ConflictRegistry { @@ -6876,9 +6912,11 @@ table is normative. \endhead Slur & Endpoint event & - Re-anchor to nearest forward event in same voice; cascade-delete - if fewer than two members survive & - proximity max: same voice; direction: forward preferred \\ + Re-anchor to the nearest surviving endpoint; cascade-delete only + when no endpoint survives & + a two-endpoint slur collapses onto its sole survivor (a + reference-clean degenerate form); proximity-aware re-targeting + is a deferred refinement \\ Slur & Interior event & No action & @@ -6899,9 +6937,10 @@ table is normative. --- \\ Spanner & Anchor & - Re-anchor to nearest surviving anchor of same kind; cascade-delete - if no surviving anchor within proximity bound & - proximity max: same staff instance; bound: per-spanner-kind \\ + Re-anchor to the nearest surviving anchor; cascade-delete only + when no anchor survives & + as for slurs (surviving-endpoint collapse); per-spanner-kind + proximity bounds are a deferred refinement \\ Marker & Anchor & Re-anchor to nearest event in same staff instance & @@ -7324,19 +7363,15 @@ pub enum TupletCompensation { ReplaceWithRest { new_rest: Rest }, /// Rewrite the enclosing tuplet(s) to remain structurally - /// consistent. The list specifies the rewritten tuplets in full. - RewriteTuplets { rewrites: Vec }, + /// consistent. The v1 payload names the affected tuplets by + /// id only; it does not carry rewritten values (see the + /// precondition below). + RewriteTuplets { tuplets: Vec }, /// Cascade-delete the entire tuplet group(s) containing the /// target event. The listed tuplet ids are cascaded. CascadeDeleteTuplets { tuplets: Vec }, } - -pub struct TupletRewrite { - pub tuplet: TupletId, - pub new_ratio: TupletRatio, - pub new_members: Vec, -} \end{lstlisting} \textbf{Invariant preconditions:} @@ -7354,9 +7389,17 @@ pub struct TupletRewrite { \item For \texttt{ReplaceWithRest}: the replacement rest's duration \MUST{} equal the deleted event's duration; the rest's voice and position \MUST{} match the deleted event. - \item For \texttt{RewriteTuplets}: every listed tuplet's resulting - member-duration sum \MUST{} match the tuplet's - structurally-required total. + \item For \texttt{RewriteTuplets}: the v1 payload carries only + tuplet ids, not the rewritten ratio and member values a reducer + would need to demonstrate that the resulting structure preserves + the tuplet consistency invariant. Graph-aware reduction \MUST{} + therefore refuse the variant as an ill-formed compensation (a + precondition no-op) rather than fabricate rewritten values. A + future payload revision carrying full rewrites (per-tuplet ratio + and members, each of whose member-duration sums \MUST{} match + the tuplet's structurally-required total) reopens the variant; + until then \texttt{ReplaceWithRest} and + \texttt{CascadeDeleteTuplets} are the applicable compensations. \item For \texttt{CascadeDeleteTuplets}: every tuplet listed \MUST{} contain the target event as a member. \end{itemize} @@ -7366,8 +7409,9 @@ voice's event list. The event's \texttt{EventId} and every contained \texttt{PitchId} are tombstoned in their respective identity indexes: they remain resolvable to ``deleted'' markers and \MUSTNOT{} be reused for new objects. The chosen tuplet compensation is applied -in the same delta: a replacement rest is inserted, the tuplet is -rewritten, or the tuplets are cascade-deleted as specified. +in the same delta: a replacement rest is inserted or the tuplets are +cascade-deleted as specified (a \texttt{RewriteTuplets} compensation +is refused at precondition check; see above). Cross-cutting structures referencing the event or its pitches are re-anchored per the rule table (Section~\ref{sec:semops:reanchor}). Live attachments targeting the event or its pitches transition to @@ -9286,10 +9330,22 @@ pub struct Manifest { /// Operation-envelope blocks defining the canonical document. /// Block ordering is irrelevant for canonical state (envelopes - /// are a set), but writers SHOULD order blocks by min_stamp - /// for predictable scanning. + /// are a set), and the canonical manifest encoding sorts chunk + /// references ascending by their encoded form (Appendix D), so + /// a writer cannot order this list by stamp; stamp-ordered + /// scanning goes through operation_block_summaries below. pub operation_roots: Vec, + /// Per-block summary metadata (Section on operation-envelope + /// blocks below), keyed by the block's ChunkId in canonical + /// ascending order. Supplied by the operation layer and carried + /// opaquely by the storage layer; non-canonical and optional (a + /// block need not have an entry). Lets a reader select or skip + /// a block by causal frontier or stamp range without decoding + /// its envelopes. + pub operation_block_summaries: + BTreeMap, + /// Optional operation index chunk: maps OperationId to /// (block, offset) for fast random access. If absent, /// implementations rebuild on demand by scanning blocks. @@ -9735,20 +9791,30 @@ pub struct ChunkId(pub ContentHash); \label{sec:format:opblocks} The canonical document is stored as operation-envelope blocks. Each -block is a chunk of kind \texttt{OperationEnvelopeBlock} containing -a vector of envelopes, with summary metadata. +block is a chunk of kind \texttt{OperationEnvelopeBlock} whose +payload is a vector of envelopes. A block is identified by its +\texttt{ChunkId}; because chunks are content-addressed, that +identifier cannot appear inside the block payload itself. Summary +metadata for a block travels in the \emph{manifest} +(\texttt{operation\_block\_summaries}), keyed by the block's chunk +id: the summary is computed by the operation layer from the block's +envelopes, and the storage layer carries it as opaque bytes without +interpreting it. \begin{lstlisting}[language=Rust] pub struct OperationEnvelopeBlock { - /// Block identifier (same as its ChunkId in the chunk store). - pub block_id: ChunkId, - /// Operation envelopes in this block. Order within a block is /// not normative for canonical reduction (envelopes are a set) /// but writers SHOULD preserve authoring order within a block /// for diagnostic purposes. pub envelopes: Vec, +} +/// Manifest-side summary of one block, keyed by the block's +/// ChunkId. Non-canonical and optional: a reader MUST NOT rely +/// on a summary being present, and canonical state never depends +/// on one. +pub struct OperationBlockSummary { /// DVV summary covering the envelopes in this block. Enables /// readers to determine causal coverage without parsing every /// envelope. @@ -11099,6 +11165,11 @@ and the two axes are independent. \begin{lstlisting}[language=Rust] pub enum SolverTier { + /// Not a conformance tier: an interface-only / passthrough + /// solver that evaluates no constraints and computes no + /// quality metrics. Ordered below every conformant tier. + Stub, + /// Minimal Layout Solver. Minimal, @@ -11110,6 +11181,11 @@ pub enum SolverTier { } \end{lstlisting} +The \texttt{Stub} variant exists so scaffolding, harnesses, and +not-yet-conformant pipelines can label themselves honestly: it makes +no conformance claim, and a document requiring any conformant tier +is never satisfied by a solver declaring \texttt{Stub}. + \subsection{Minimal Layout Solver} \begin{requirement} @@ -14405,6 +14481,43 @@ layouts they own versus inherit: operation content hash) were golden-locked in code but unpinned in spec text. \\ + \today & Pass 12 tranche 1 (audit spec-alignment) & + Aligned spec text with dispositions the project had already made + and the reference implementation exercises; no byte-layout or + architecture change. The re-anchoring rule table's Slur and + Spanner rows now state the Operation Catalog's surviving-endpoint + semantics (re-anchor while $\geq 1$ endpoint survives, + cascade-delete only when none does; proximity-aware re-targeting + deferred). \texttt{TupletCompensation::RewriteTuplets} adopts the + catalog's id-only v1 payload (\texttt{TupletRewrite} removed): + graph-aware reduction refuses the variant rather than fabricate + rewritten values, and a value-carrying payload revision reopens + it. Operation-envelope blocks are pure envelope vectors (a + content-addressed chunk cannot embed its own id); the per-block + summary metadata + (\texttt{dvv\_summary}/\texttt{min\_stamp}/\texttt{max\_stamp}) + relocated to the manifest's \texttt{operation\_block\_summaries} + map (opaque ops-supplied bytes, non-canonical, ChunkId-keyed), + and the order-blocks-by-\texttt{min\_stamp} \SHOULD{} was dropped + because the canonical manifest encoding sorts chunk references by + encoded form. The spelling and decomposition pre-passes are now + specified as producing \emph{canonical derived annotations} --- + deterministic functions of (materialized graph, profile, + versioned algorithm id), recomputed on materialization and never + stored --- replacing the stored-\texttt{Inferred}-attachment + model; the incremental re-run requirement is demoted from + \MUST{} to \MAY{} with caching and incrementality required to be + unobservable. Spelling-precedence ties now break by canonical + attachment order (attachments carry no creation timestamp). The + \texttt{ConflictRegistry} moved off the \texttt{Score} root into + canonical materialized state, matching Chapter~6. + \texttt{SolverTier} gains the non-conformance \texttt{Stub} + variant. Companion: Operation Catalog 0.2.0 $\rightarrow$ 0.3.0 + (ModifyEvent materializes metric placement changes behind a + voice-occupancy placement precondition). Dispositions logged in + \texttt{spec/PASS12\_RATIFICATION\_LOG.md}; the Pass 12 batch + itself remains open. + \\ \bottomrule \end{longtable} diff --git a/spec/operation_catalog.pdf b/spec/operation_catalog.pdf index e97094e..3c58fea 100644 Binary files a/spec/operation_catalog.pdf and b/spec/operation_catalog.pdf differ diff --git a/spec/operation_catalog.tex b/spec/operation_catalog.tex index 91e4cdc..286b252 100644 --- a/spec/operation_catalog.tex +++ b/spec/operation_catalog.tex @@ -226,7 +226,7 @@ {\Large\scshape\color{epiphanyslate}Operation Catalog}\\[6pt] {\large\itshape\color{epiphanyslate}A companion to the Core Specification}\\[14pt] {\color{epiphanygold}\rule{3in}{0.8pt}}\\[24pt] - {\normalsize\color{epiphanyink}Version 0.2.0 --- Phase 2 (K0 representative + broad-K0 M2 groups)}\\[4pt] + {\normalsize\color{epiphanyink}Version 0.3.0 --- Phase 2 (K0 representative + broad-K0 M2 groups)}\\[4pt] {\small\color{epiphanyslate}Normative for the operation kinds it defines} \vfill \end{titlepage} @@ -493,13 +493,23 @@ is read from the value. Precondition: the event is live. The resolved value is the one carried by the operation latest in canonical order; two causally ordered modifications overwrite intentionally, and two \emph{concurrent} modifications with \emph{equal} value -reduce idempotently. Graph-aware reduction overwrites the event in place. A -modification that \emph{moves} the event (a different region-local position or -duration) is recorded in the bookkeeping but its placement change is \emph{not} -applied to the graph: re-sorting a voice on a placement change is a deferred -refinement, and an in-place move would break \texttt{VoiceEventsSortedNonOverlap} -(Chapter~5 invariant~3). A malformed (empty pitched) replacement is likewise -recorded but not materialised. +reduce idempotently. Graph-aware reduction overwrites the event in place, and a +modification that \emph{moves} a metric event (a different region-local +\texttt{Musical} position or duration) is \emph{materialised}: the owning voice +is re-sorted by ascending position (id-tiebroken --- the same order an insert +maintains), preserving \texttt{VoiceEventsSortedNonOverlap} (Chapter~5 +invariant~3). To keep that invariant, a placement change carries a +\emph{placement precondition}, read from the reducer's canonical voice-occupancy +index (graph-independent, so graph-free and graph-aware reduction agree): a move +with a non-positive span, or one that would overlap another live event in the +voice, is refused as a clean precondition no-op (\texttt{EventDurationInvalid}) +rather than skipped silently. A materialised move updates the occupancy index, +so a later insert sees the freed or changed span. A placement change of a +\emph{non-metric} event is recorded in the bookkeeping but not applied to the +graph (re-sorting a non-metric voice is a deferred refinement); a malformed +(empty pitched) replacement is likewise recorded but not materialised; +same-placement field edits apply in place, preserving voice membership. Partial +trimming of a tuplet member remains a later refinement. \textbf{Conflict cases.} Two concurrent modifications of one event with \emph{differing} values produce a \texttt{StructuralFieldCollision} on the field