1354 lines
68 KiB
TeX
1354 lines
68 KiB
TeX
% !TEX program = xelatex
|
|
%
|
|
% Epiphany --- Operation Catalog (companion specification)
|
|
% Companion to the Core Specification. Compile with XeLaTeX.
|
|
%
|
|
% This document is versioned independently of the Core Specification
|
|
% (independent semver; see the Versioning note in the front matter). Its preamble
|
|
% is intentionally a self-contained copy of the core specification's preamble so
|
|
% the two documents build independently; factoring a shared preamble file is a
|
|
% later cleanup, not a v0.1 deliverable.
|
|
|
|
\documentclass[11pt,letterpaper]{report}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Packages
|
|
% ---------------------------------------------------------------------------
|
|
\usepackage{fontspec}
|
|
\usepackage{geometry}
|
|
\geometry{
|
|
letterpaper,
|
|
top=1.05in,
|
|
bottom=1.05in,
|
|
left=1.15in,
|
|
right=1.15in,
|
|
headheight=15pt
|
|
}
|
|
|
|
\usepackage[english]{babel}
|
|
\usepackage{microtype}
|
|
\usepackage{parskip}
|
|
\usepackage{xcolor}
|
|
\usepackage{hyperref}
|
|
\usepackage{enumitem}
|
|
\usepackage{titlesec}
|
|
\usepackage{fancyhdr}
|
|
\usepackage{booktabs}
|
|
\usepackage{array}
|
|
\usepackage{longtable}
|
|
\usepackage{listings}
|
|
\usepackage{amsmath}
|
|
\usepackage{amssymb}
|
|
\usepackage{tcolorbox}
|
|
\tcbuselibrary{breakable, skins}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Color palette (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\definecolor{epiphanyteal}{HTML}{1A4044}
|
|
\definecolor{epiphanygold}{HTML}{8E6E2E}
|
|
\definecolor{epiphanyink}{HTML}{1F1B16}
|
|
\definecolor{epiphanyslate}{HTML}{6B6660}
|
|
\definecolor{epiphanycream}{HTML}{F8F4ED}
|
|
\definecolor{epiphanymist}{HTML}{ECE8E0}
|
|
\definecolor{epiphanycode}{HTML}{2A2520}
|
|
\definecolor{epiphanycrimson}{HTML}{7A2424}
|
|
|
|
\hypersetup{
|
|
colorlinks=true,
|
|
linkcolor=epiphanyteal,
|
|
citecolor=epiphanyteal,
|
|
urlcolor=epiphanygold,
|
|
pdftitle={Epiphany --- Operation Catalog},
|
|
pdfauthor={The Epiphany Project},
|
|
pdfsubject={Operation Catalog companion for the Epiphany music notation platform},
|
|
pdfkeywords={music notation, operations, CRDT, reduction, serialization},
|
|
bookmarksnumbered=true,
|
|
bookmarksopen=true
|
|
}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Typography (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\setmainfont{TeX Gyre Pagella}[Numbers={OldStyle, Proportional}, Ligatures={TeX, Common}]
|
|
\setsansfont{TeX Gyre Heros}[Scale=0.94, Ligatures={TeX, Common}]
|
|
\setmonofont{TeX Gyre Cursor}[Scale=0.88, Ligatures={TeX}]
|
|
\newfontfamily\titlefont{TeX Gyre Pagella}[Numbers={OldStyle}, Ligatures={TeX, Common}]
|
|
\newcommand{\tablenums}[1]{{\addfontfeatures{Numbers={Lining,Tabular}}#1}}
|
|
\newcommand{\sectionsc}[1]{{\addfontfeatures{Letters=SmallCaps}#1}}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Section styling (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\titleformat{\chapter}[display]
|
|
{\normalfont\filright}
|
|
{\raggedright\color{epiphanygold}\fontsize{14pt}{16pt}\selectfont
|
|
\scshape Chapter\ \thechapter}
|
|
{16pt}
|
|
{\raggedright\color{epiphanyteal}\fontsize{32pt}{36pt}\selectfont\bfseries}
|
|
[\vspace{4pt}{\color{epiphanygold}\rule{2in}{0.6pt}}]
|
|
\titlespacing*{\chapter}{0pt}{-20pt}{30pt}
|
|
\titleformat{\section}
|
|
{\normalfont\Large\bfseries\color{epiphanyteal}}
|
|
{\color{epiphanygold}\thesection}{1em}{}
|
|
\titleformat{\subsection}
|
|
{\normalfont\large\bfseries\color{epiphanyteal}}
|
|
{\color{epiphanygold}\thesubsection}{1em}{}
|
|
\titleformat{\subsubsection}
|
|
{\normalfont\normalsize\bfseries\color{epiphanyink}}
|
|
{\thesubsubsection}{1em}{}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Headers and footers (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\pagestyle{fancy}
|
|
\fancyhf{}
|
|
\renewcommand{\headrulewidth}{0pt}
|
|
\renewcommand{\footrulewidth}{0pt}
|
|
\fancyhead[L]{\small\scshape\color{epiphanyslate}Epiphany --- Operation Catalog}
|
|
\fancyhead[R]{\small\itshape\color{epiphanyslate}\leftmark}
|
|
\fancyfoot[C]{\small\color{epiphanyslate}\thepage}
|
|
\renewcommand{\headrule}{
|
|
\color{epiphanygold!50}\hrule width\headwidth height 0.4pt
|
|
\vspace{1pt}
|
|
\color{epiphanygold!30}\hrule width\headwidth height 0.2pt
|
|
}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Code listing style (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\lstdefinelanguage{Rust}{
|
|
keywords={fn,let,mut,pub,struct,enum,impl,trait,for,in,if,else,match,return,
|
|
use,mod,crate,self,Self,as,where,move,async,await,const,static,
|
|
ref,type,unsafe,extern,dyn,box,break,continue,loop,while},
|
|
keywordstyle=\color{epiphanyteal}\bfseries,
|
|
ndkeywords={i8,i16,i32,i64,i128,u8,u16,u32,u64,u128,f32,f64,bool,char,str,
|
|
String,Vec,Option,Result,Box,Rc,Arc,HashMap,BTreeMap,
|
|
NonZeroU16,NonZeroU32,NonZeroU64,Duration,Timestamp},
|
|
ndkeywordstyle=\color{epiphanygold}\bfseries,
|
|
sensitive=true,
|
|
comment=[l]{//},
|
|
morecomment=[s]{/*}{*/},
|
|
commentstyle=\color{epiphanyslate}\itshape,
|
|
stringstyle=\color{epiphanycrimson},
|
|
morestring=[b]",
|
|
morestring=[b]'
|
|
}
|
|
\lstset{
|
|
basicstyle=\ttfamily\small\color{epiphanycode},
|
|
backgroundcolor=\color{epiphanycream},
|
|
frame=leftline,
|
|
rulecolor=\color{epiphanygold!60},
|
|
framesep=8pt,
|
|
framerule=1.5pt,
|
|
xleftmargin=10pt,
|
|
xrightmargin=4pt,
|
|
breaklines=true,
|
|
showstringspaces=false,
|
|
numberstyle=\tiny\color{epiphanyslate},
|
|
numbersep=10pt,
|
|
captionpos=b,
|
|
aboveskip=10pt,
|
|
belowskip=10pt,
|
|
language=Rust
|
|
}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Custom environments (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\newtcolorbox{openquestion}[1][]{
|
|
enhanced, breakable,
|
|
colback=epiphanymist, colframe=epiphanycrimson,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Open Question},
|
|
coltitle=white, colbacktitle=epiphanycrimson,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
\newtcolorbox{rationale}[1][]{
|
|
enhanced, breakable,
|
|
colback=epiphanymist, colframe=epiphanyteal,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Rationale},
|
|
coltitle=white, colbacktitle=epiphanyteal,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
\newtcolorbox{requirement}[1][]{
|
|
enhanced, breakable,
|
|
colback=white, colframe=epiphanygold,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Requirement},
|
|
coltitle=white, colbacktitle=epiphanygold,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
\newtcolorbox{nongoal}[1][]{
|
|
enhanced, breakable,
|
|
colback=epiphanymist, colframe=epiphanyslate,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Non-Goal},
|
|
coltitle=white, colbacktitle=epiphanyslate,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
|
|
\newcommand{\MUST}{\textbf{MUST}}
|
|
\newcommand{\MUSTNOT}{\textbf{MUST}\nobreak\ \textbf{NOT}}
|
|
\newcommand{\SHOULD}{\textbf{SHOULD}}
|
|
\newcommand{\SHOULDNOT}{\textbf{SHOULD}\nobreak\ \textbf{NOT}}
|
|
\newcommand{\MAY}{\textbf{MAY}}
|
|
|
|
\setlist[itemize]{topsep=2pt, itemsep=3pt, parsep=0pt}
|
|
\setlist[enumerate]{topsep=2pt, itemsep=3pt, parsep=0pt}
|
|
\setlist[description]{topsep=2pt, itemsep=5pt, parsep=0pt}
|
|
\AtBeginDocument{\color{epiphanyink}}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Document
|
|
% ---------------------------------------------------------------------------
|
|
\begin{document}
|
|
|
|
\begin{titlepage}
|
|
\thispagestyle{empty}
|
|
\centering
|
|
\vspace*{2.2in}
|
|
{\color{epiphanygold}\rule{3in}{0.8pt}}\\[18pt]
|
|
{\titlefont\fontsize{34pt}{38pt}\selectfont\color{epiphanyteal}\bfseries Epiphany}\\[10pt]
|
|
{\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.7.0 --- Schema-major-2 repeat authoring (the CreateRepeatStructure / DeleteRepeatStructure pair)}\\[4pt]
|
|
{\small\color{epiphanyslate}Normative for the operation kinds it defines}
|
|
\vfill
|
|
\end{titlepage}
|
|
|
|
\tableofcontents
|
|
|
|
% ===========================================================================
|
|
\chapter{About This Companion}
|
|
\label{ch:about}
|
|
|
|
The \emph{Operation Catalog} is a companion to the Epiphany Core Specification.
|
|
It fulfils the open question the core specification raises in its
|
|
\emph{Operation Catalog Conformance} section (Chapter~6,
|
|
\sectionsc{Semantic Operations and Concurrent Reduction}, the
|
|
\texttt{sec:semops:catalog} open question), which states that the catalog
|
|
``is normative once published; this specification is non-final until the catalog
|
|
is delivered.'' This release delivers the catalog \emph{framework}, the
|
|
\textbf{K0 representative primitive set}, and the \textbf{M2 broad-K0 groups}
|
|
(the event/pitch leaf-field, cross-cutting CRUD, structural-container, and
|
|
score-settings operations the Phase~2 slice exercises) --- the operation kinds
|
|
the Phase~2 visible slice and binary format actually exercise, each fully
|
|
specified in Chapter~\ref{ch:k0}. The remaining items of the full
|
|
$60$--$80$-primitive catalog are drafted as framework slots
|
|
(Chapter~\ref{ch:k1}) and completed in Phase~3.
|
|
|
|
\section{Relationship to the Core Specification}
|
|
|
|
This companion does not restate the operation framework; it \emph{references} it.
|
|
The framework --- operation identity and stamps, the hybrid-logical-clock
|
|
monotonicity rule, the dotted-version-vector causal context, the
|
|
order-independent operation-slot model and equivocation, the canonical reduction
|
|
order, the four-phase lifecycle, conflict records and the conflict registry,
|
|
re-anchoring, transactions, forward undo, and the LWW discipline --- is the core
|
|
specification's Chapter~6. This companion defines, for each operation kind, the
|
|
\emph{payload schema} and how that kind \emph{instantiates} the framework's
|
|
reduction, conflict, undo, and re-anchoring rules.
|
|
|
|
It also consumes, rather than re-deriving, the \textbf{ratified byte-convention
|
|
baseline} (core specification Chapter~8, \sectionsc{Binary Format Companion},
|
|
requirement \texttt{req:format:codec-conventions}, and the
|
|
\sectionsc{Canonical Byte-Layout Reference} appendix): little-endian integers, a
|
|
single discriminant byte per tagged union, \texttt{u32} length prefixes on every
|
|
variable-width leaf, and raw UTF-8 free text. Operation-payload encodings are
|
|
expressed in terms of that baseline; the literal wire layout of each payload is
|
|
the Binary Format companion's (Agent~J's) to pin, in coordination with this
|
|
catalog.
|
|
|
|
\begin{rationale}
|
|
The catalog is versioned \emph{independently} of the core specification
|
|
(independent semver). Operation kinds are added over time; the catalog should
|
|
evolve --- adding primitives, refining conflict cases --- without forcing a core
|
|
specification revision. The core specification changes only when the
|
|
\emph{framework} changes.
|
|
\end{rationale}
|
|
|
|
\section{Conformance Profiles}
|
|
|
|
A \textbf{Phase-2 profile} implementation \MUST{} implement every primitive in
|
|
Chapter~\ref{ch:k0} --- the representative set and the M2 broad-K0 groups --- with
|
|
the schema, reduction rule, conflict cases, undo semantics, and re-anchoring
|
|
behaviour defined there. The former create-score/create-canvas framework slots
|
|
of Chapter~\ref{ch:k1} are \emph{retired} (Pass~12): they are permanently
|
|
outside the operation set, so no operation kind exists to reject.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.6.0 (Pass-12 G-ratification).} No payload byte
|
|
changes. Ratified: ResolveConflict beyond the concurrent case (P12-K4),
|
|
ResolveEquivocation edge semantics (P12-K6) and the profile-policy deferral
|
|
(P12-K5), the RespellPitch migration fallback as long-term (P12-K1), undo
|
|
strand-block conflict-kind reuse (P12-K10) and the idempotence asymmetry
|
|
(P12-K11), the Transpose prototype pin (P12-K2 deferral), the cross-region
|
|
slur AND advisory (P12-K12), and the create-score/canvas retirement (P12-K8).
|
|
Appended vocabulary (minor, append-only):
|
|
\texttt{SystemDerivedContentImmutable} (12, P12-K3) and
|
|
\texttt{RecreateContentMismatch} (13, P12-K9) in
|
|
\texttt{PreconditionFailureReason}.
|
|
|
|
% ===========================================================================
|
|
\chapter{The Catalog Framework}
|
|
\label{ch:framework}
|
|
|
|
\section{Value-Typed Payloads}
|
|
\label{sec:framework:value-typed}
|
|
|
|
Every operation payload in this catalog is \textbf{value-typed}: it carries the
|
|
real graph values its effect introduces, not identifiers that point at values in
|
|
some ambient graph. An \texttt{InsertEvent} carries the whole \texttt{Event}; a
|
|
\texttt{RespellPitch} carries the whole \texttt{PitchSpelling}; a
|
|
\texttt{CreateCrossCutting} carries the whole tie, slur, beam, or spanner.
|
|
|
|
\begin{rationale}
|
|
The v0 prototype carried \emph{identifier-only projections} --- an
|
|
\texttt{InsertEvent} held an \texttt{EventId} plus reduction-relevant scalars; a
|
|
\texttt{RespellPitch} held a content-hash \emph{fingerprint} of the new spelling.
|
|
That was sufficient to make an envelope hashable and to drive reduction, but it
|
|
is \textbf{not durable}: an operation replayed in a fresh context --- a backup
|
|
restore, a cross-tool round-trip --- needs the full value, which an
|
|
identifier-only payload cannot supply. Value-typed payloads are what make an
|
|
Epiphany document portable.
|
|
\end{rationale}
|
|
|
|
\begin{requirement}
|
|
\label{req:catalog:value-encoding}
|
|
A value-typed payload field \MUST{} be encoded by emitting the field's value
|
|
under the core specification's canonical value encoding
|
|
(\texttt{req:format:codec-conventions}), framed by a \texttt{u32} little-endian
|
|
length prefix. Decoding \MUST{} be the exact inverse and \MUST{} reject trailing
|
|
bytes within the framed region. The encoding introduces no byte layout beyond the
|
|
ratified baseline: a value's bytes here are byte-for-byte the bytes the whole
|
|
document codec emits for that value.
|
|
\end{requirement}
|
|
|
|
\section{Per-Primitive Schema Template}
|
|
\label{sec:framework:template}
|
|
|
|
Each catalog primitive is specified under a fixed six-part template. A new
|
|
primitive is a schema-fill against this template, not a fresh design:
|
|
|
|
\begin{description}
|
|
\item[Payload schema] The value-typed fields the operation carries, with their
|
|
core-specification types.
|
|
\item[Canonical encoding] The field order and framing, consuming
|
|
Requirement~\ref{req:catalog:value-encoding}. (The literal byte layout is the
|
|
Binary Format companion's; this catalog fixes the \emph{field set and order}.)
|
|
\item[Reduction rule] How the operation mutates canonical state when it is
|
|
reached in canonical reduction order --- the preconditions it checks, the
|
|
objects it mints or tombstones, and the bookkeeping it records.
|
|
\item[Conflict cases] The conflict records the operation can produce, by
|
|
\texttt{ConflictKind}, and which participant materialises.
|
|
\item[Undo semantics] The compensating effect of undoing a transaction that
|
|
contains the operation, under each \texttt{UndoPolicy}
|
|
(\texttt{StrictInverse} / \texttt{BestEffort} / \texttt{Cascade}).
|
|
\item[Re-anchoring] The behaviour when an object the operation references is
|
|
tombstoned before or concurrently with it.
|
|
\end{description}
|
|
|
|
\section{Reduction-Discipline Coverage}
|
|
|
|
The K0 representative set is chosen so that, between them, the primitives
|
|
exercise \emph{every} reduction discipline the framework defines:
|
|
position-keyed insert with system-voice promotion; delete-wins with tombstones,
|
|
tuplet compensation, and cross-cutting re-anchoring; field-overwrite with
|
|
last-writer-wins and structural-field-collision conflicts; set-union creation;
|
|
structural time-model migration; an LWW advisory; atomic transactions with
|
|
descriptor precedence; and the two meta-operations (conflict resolution and
|
|
forward undo). A primitive added later that reuses one of these disciplines
|
|
inherits its reduction, conflict, undo, and re-anchoring treatment.
|
|
|
|
% ===========================================================================
|
|
\chapter{K0 --- Representative Primitives}
|
|
\label{ch:k0}
|
|
|
|
This chapter is normative under the Phase-2 profile. Each primitive's reduction,
|
|
conflict, undo, and re-anchoring behaviour is the behaviour the core
|
|
specification's Chapter~6 defines for its discipline; the description here states
|
|
how the primitive instantiates it. The reference implementation is
|
|
\texttt{epiphany-ops} (the \texttt{payload}, \texttt{reduce}, and \texttt{migrate}
|
|
modules).
|
|
|
|
\section{InsertEvent}
|
|
\label{sec:k0:insert-event}
|
|
|
|
\textbf{Payload schema.} \texttt{InsertEventOp \{ staff\_instance:
|
|
StaffInstanceId, event: Event \}}. The voice, region-local position, duration,
|
|
and pitch identities are read from the \texttt{Event} value; the
|
|
\texttt{staff\_instance} is retained alongside it so the system-voice promotion
|
|
derivation is total without a containment walk.
|
|
|
|
\textbf{Canonical encoding.} \texttt{staff\_instance}, then the length-framed
|
|
canonical bytes of \texttt{event}.
|
|
|
|
\textbf{Reduction rule.} A position-keyed insert. Preconditions: the event's
|
|
duration is positive; the event id is neither live nor tombstoned; in graph-aware
|
|
reduction the target voice exists in a metric region and the event's pitch ids
|
|
are fresh. The event and its pitches are minted live; the voice is created on
|
|
first use. Concurrent inserts whose half-open duration intervals overlap in the
|
|
same voice are resolved by an order-independent promotion pre-pass: the
|
|
lower-\texttt{OperationId} insert is retained in the original voice, and each
|
|
overlapping loser is promoted to the deterministic system voice
|
|
\texttt{derive\_promoted\_voice\_id(staff\_instance, voice, winner, loser)} and
|
|
tagged \texttt{VoicePromoted}.
|
|
|
|
\textbf{Conflict cases.} None at reduction time; promotion is a deterministic
|
|
repair, not a conflict.
|
|
|
|
\textbf{Undo semantics.} Undoing the enclosing transaction tombstones the minted
|
|
event, its pitches, and any promoted voice. \texttt{StrictInverse} conflicts if
|
|
any was already tombstoned or modified; \texttt{BestEffort} tombstones the
|
|
survivors; \texttt{Cascade} is \texttt{StrictInverse} over the same minted set
|
|
(dependent-closure undo is a Phase-3 refinement).
|
|
|
|
\textbf{Re-anchoring.} Not applicable (the operation mints, it does not
|
|
reference a pre-existing object that could be tombstoned).
|
|
|
|
\section{DeleteEvent}
|
|
\label{sec:k0:delete-event}
|
|
|
|
\textbf{Payload schema.} \texttt{DeleteEventOp \{ event: EventId,
|
|
tuplet\_compensation: TupletCompensation \}}, where \texttt{TupletCompensation}
|
|
is \texttt{NotInTuplet}, \texttt{ReplaceWithRest \{ rest: Rest \}} (value-typed
|
|
replacement rest), \texttt{RewriteTuplets \{ tuplets \}}, or
|
|
\texttt{CascadeDeleteTuplets \{ tuplets \}}.
|
|
|
|
\textbf{Canonical encoding.} \texttt{event}, then the tuplet-compensation
|
|
discriminant and its payload (a length-framed \texttt{Rest} value for
|
|
\texttt{ReplaceWithRest}).
|
|
|
|
\textbf{Reduction rule.} Delete-wins: the event and its contained pitches are
|
|
tombstoned (retaining their identifiers). Tuplet compensation, when present, adds
|
|
the replacement rest live or tombstones the cascaded tuplet group. Concurrent
|
|
deletes of the same event are idempotent.
|
|
|
|
\textbf{Conflict cases.} None for the delete itself. Graph-aware reduction
|
|
refuses an ill-formed tuplet compensation as a precondition failure (no-op).
|
|
|
|
\textbf{Undo semantics.} An insert-shaped compensation re-introduces the
|
|
tombstoned content; for the prototype's minted-object model this is the inverse
|
|
of the tombstone set, with the policy treatment described under InsertEvent.
|
|
|
|
\textbf{Re-anchoring.} Tombstoning the event runs the framework's re-anchoring
|
|
rule table over every cross-cutting structure that referenced it: a tie
|
|
cascade-deletes; a comment or analytical annotation orphans (user content is
|
|
never silently deleted); a beam truncates while $\geq 2$ members survive and
|
|
otherwise cascade-deletes; a slur or spanner re-anchors to the nearest surviving
|
|
endpoint while $\geq 1$ survives and otherwise cascade-deletes.
|
|
|
|
\section{RespellPitch}
|
|
\label{sec:k0:respell-pitch}
|
|
|
|
\textbf{Payload schema.} \texttt{RespellPitchOp \{ pitch: PitchId, spelling:
|
|
PitchSpelling \}} --- the full spelling value (v1), not a fingerprint.
|
|
|
|
\textbf{Canonical encoding.} \texttt{pitch}, then the length-framed canonical
|
|
bytes of \texttt{spelling}.
|
|
|
|
\textbf{Reduction rule.} A last-writer-wins field overwrite, keyed by pitch.
|
|
Precondition: the pitch is live. The resolved spelling is the one carried by the
|
|
operation latest in canonical order. Two respellings of one pitch that are
|
|
causally ordered overwrite intentionally; two \emph{concurrent} respellings with
|
|
\emph{equal} spelling reduce idempotently.
|
|
|
|
\textbf{Conflict cases.} Two concurrent respellings of one pitch with
|
|
\emph{differing} spellings produce a \texttt{StructuralFieldCollision} conflict
|
|
recording the winner (later in canonical order), the loser, and the field
|
|
\texttt{spelling}. The winner materialises and carries the \texttt{Conflicted}
|
|
effect tag.
|
|
|
|
\textbf{Undo semantics.} Value-restoring (Section~\ref{sec:k0:undo}): undo
|
|
restores the pre-operation spelling (or removes the spelling if the operation
|
|
introduced the first one), under the active policy.
|
|
|
|
\textbf{Re-anchoring.} If the target pitch is tombstoned, the respelling is a
|
|
no-op (\texttt{TargetTombstoned}).
|
|
|
|
\emph{Migration (ratified Pass~12, closing P12-K1).} A v0
|
|
\texttt{RespellPitch} carried only a content-hash \emph{fingerprint} of the
|
|
spelling. The fingerprint cannot be inverted to a \texttt{PitchSpelling}
|
|
without a side table, so the v0$\rightarrow$v1 migration
|
|
(Chapter~\ref{ch:migration}) recovers the spelling from the score graph
|
|
context --- an explicit per-pitch spelling attachment whose canonical bytes
|
|
hash to the fingerprint --- and, when the context lacks it, declares the
|
|
envelope unmigratable (the bundle opens read-only). This read-only fallback
|
|
is the \emph{long-term} disposition: no richer v0 corpus is or will be
|
|
required (no production v0 corpus exists). It remains the one representative
|
|
payload that is not self-contained under migration.
|
|
|
|
\section{ModifyEvent}
|
|
\label{sec:k0:modify-event}
|
|
|
|
\textbf{Payload schema.} \texttt{ModifyEventOp \{ event: Event \}} --- the full
|
|
replacement \texttt{Event} value (v1). The identity (and therefore the LWW key)
|
|
is read from the value.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of \texttt{event}.
|
|
|
|
\textbf{Reduction rule.} A last-writer-wins field overwrite keyed by event id.
|
|
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, 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.
|
|
|
|
\emph{System-derived content immutability (ratified Pass~12, closing
|
|
P12-K3).} A modification that would rewrite the \emph{intrinsic content} of a
|
|
pitch whose identifier lives in the \texttt{SYSTEM\_DERIVED} namespace is
|
|
refused as a clean precondition no-op with the appended reason
|
|
\texttt{SystemDerivedContentImmutable} (discriminant 12): the identifier is
|
|
content-derived, and an in-place rewrite would silently invalidate its
|
|
derivation (core specification, Chapter~5 system-derived identity). The same
|
|
precondition applies to \texttt{ModifyIdentifiedPitch}
|
|
(Section~\ref{sec:k0:identified-pitch}). The sanctioned path is minting a
|
|
replacement pitch.
|
|
|
|
\textbf{Conflict cases.} Two concurrent modifications of one event with
|
|
\emph{differing} values produce a \texttt{StructuralFieldCollision} on the field
|
|
\texttt{event}, recording the winner (later in canonical order) and the loser.
|
|
|
|
\textbf{Undo semantics.} Value-restoring (Section~\ref{sec:k0:undo}): undoing
|
|
the enclosing transaction restores the event's chain-predecessor value,
|
|
conflicting (\texttt{StrictInverse}) or skipping (\texttt{BestEffort}) when a
|
|
later modification has superseded it.
|
|
|
|
\textbf{Re-anchoring.} If the target event is tombstoned, the modification is a
|
|
no-op (\texttt{TargetTombstoned}/\texttt{TargetMissing}).
|
|
|
|
\section{Identified-Pitch Operations}
|
|
\label{sec:k0:identified-pitch}
|
|
|
|
\textbf{Payload schema.} \texttt{InsertIdentifiedPitchOp \{ event: EventId,
|
|
pitch: IdentifiedPitch \}} mints a pitch into a live event;
|
|
\texttt{DeleteIdentifiedPitchOp \{ pitch: PitchId \}} tombstones one;
|
|
\texttt{ModifyIdentifiedPitchOp \{ pitch: PitchId, value: Pitch \}} overwrites a
|
|
pitch's acoustic / scale-position value (distinct from \texttt{RespellPitch},
|
|
which overwrites only the \emph{spelling}).
|
|
|
|
\textbf{Canonical encoding.} Insert: \texttt{event}, then the length-framed
|
|
\texttt{pitch} value. Delete: \texttt{pitch}. Modify: \texttt{pitch}, then the
|
|
length-framed \texttt{value}.
|
|
|
|
\textbf{Reduction rule.} The pitch-level analogues of the event-level mint,
|
|
delete, and field overwrite, inheriting their disciplines
|
|
(Sections~\ref{sec:k0:insert-event}, \ref{sec:k0:delete-event}, and this
|
|
chapter's field-overwrite treatment). \textbf{A note and a rest are the same slot
|
|
under pitch add/remove} (normative): deleting the \emph{only} pitch of a
|
|
single-pitch note degrades the event to a \texttt{Rest} of the same
|
|
id/voice/position/duration rather than leaving an empty pitched event (Chapter~5
|
|
forbids the empty chord, \texttt{ArenaError::EmptyPitchedEvent}); inserting a
|
|
pitch into a rest is the dual, promoting it to a one-pitch note. This preserves
|
|
the delete-wins / mint disciplines and keeps the graph consistent with the
|
|
bookkeeping, which tombstones or mints the pitch object either way.
|
|
|
|
\textbf{Conflict cases.} Insert and delete: none (mint is set-union; delete-wins
|
|
is idempotent). Modify: two concurrent differing writes of one pitch produce a
|
|
\texttt{StructuralFieldCollision} on the field \texttt{pitch}.
|
|
|
|
\textbf{Undo semantics.} Insert: undoing the enclosing transaction tombstones
|
|
the minted pitch, re-resting the event if it was the only one
|
|
(Section~\ref{sec:k0:undo}). Modify: value-restoring
|
|
(Section~\ref{sec:k0:undo}) --- the pitch's chain-predecessor value is
|
|
restored unless superseded. Delete: still not inverted (re-introducing a
|
|
tombstoned pitch is the deferred resurrection case, P11-C8).
|
|
|
|
\textbf{Re-anchoring.} An operation whose target event or pitch is tombstoned is
|
|
a no-op; tombstoning a pitch runs the cross-cutting re-anchoring table over any
|
|
structure that referenced it (see DeleteEvent).
|
|
|
|
\section{Transpose}
|
|
\label{sec:k0:transpose}
|
|
|
|
\textbf{Payload schema.} \texttt{TransposeOp \{ targets: Vec<PitchId>,
|
|
chromatic\_steps: i32 \}}. Pitch identifiers are preserved; only acoustic content
|
|
changes.
|
|
|
|
\textbf{Canonical encoding.} The canonically-ordered \texttt{targets} set, then
|
|
\texttt{chromatic\_steps} as a little-endian \texttt{i32}.
|
|
|
|
\textbf{Reduction rule.} An order-dependent content overwrite. Each live target
|
|
pitch is shifted by \texttt{chromatic\_steps}; reduction is order-dependent in the
|
|
general case (interval composition need not commute), so the resolved value is
|
|
the composition in canonical reduction order. In this prototype
|
|
\texttt{chromatic\_steps} is a minimal CMN alteration shift that commutes except
|
|
at the alteration's \texttt{i8} saturation bound; rich interval algebra is
|
|
deferred (Chapter~4 tuning catalog; P12-K2). \emph{Pinned (Pass~12):} the
|
|
prototype semantics --- CMN alteration shift with documented \texttt{i8}
|
|
saturation --- are the declared v1 behavior; replacing the payload with a
|
|
faithful interval representation is a \emph{payload schema-major} under the
|
|
Binary Format companion's evolution rule, landing with the tuning catalog.
|
|
|
|
\textbf{Conflict cases.} None --- composition is deterministic in canonical order
|
|
(a deterministic repair, not a conflict).
|
|
|
|
\textbf{Undo semantics.} Transpose mints nothing, so the prototype's minted-object
|
|
undo (Section~\ref{sec:k0:undo}) does not negate it; an inverse-interval undo is a
|
|
Phase-3 refinement (P11-C8).
|
|
|
|
\textbf{Re-anchoring.} Tombstoned targets are skipped (the transpose applies only
|
|
to live pitches). \texttt{SYSTEM\_DERIVED}-namespace targets are likewise
|
|
\emph{skipped} (ratified Pass~12, P12-K3): their intrinsic content is immutable,
|
|
and an in-place alteration shift would desynchronize the content from the id's
|
|
derivation inputs. A transpose whose live targets are \emph{all} system-derived
|
|
reduces as a precondition no-op (\texttt{SystemDerivedContentImmutable}).
|
|
|
|
\section{CreateCrossCutting}
|
|
\label{sec:k0:create-cross-cutting}
|
|
|
|
\textbf{Payload schema.} \texttt{CreateCrossCuttingOp \{ structure:
|
|
CrossCuttingValue \}}, where \texttt{CrossCuttingValue} is the typed value of a
|
|
\texttt{Tie}, \texttt{Slur}, \texttt{Beam}, or \texttt{Spanner}. Its identity and
|
|
referenced endpoints are read from the value.
|
|
|
|
\textbf{Canonical encoding.} A discriminant for the structure kind, then the
|
|
length-framed canonical bytes of the structure value.
|
|
|
|
\textbf{Reduction rule.} Set-union creation: the structure is minted live if its
|
|
id is not already live and every referenced endpoint is live; a second create of
|
|
a live id is idempotent. Graph-aware reduction materialises the structure with
|
|
its full fields.
|
|
|
|
\textbf{Conflict cases.} None (all-or-nothing creation; union is deterministic).
|
|
|
|
\textbf{Undo semantics.} Undo tombstones the minted structure, under the active
|
|
policy.
|
|
|
|
\textbf{Re-anchoring.} The structure participates in the re-anchoring rule table
|
|
when one of its endpoints is later tombstoned (see DeleteEvent).
|
|
|
|
\textbf{Authoring advisory (ratified Pass~12, closing P12-K12).} The
|
|
slur-spanning advisory reads
|
|
\texttt{Region.permits\_spanning\_slurs} \emph{conjunctively}: a slur (or
|
|
other spanner) whose endpoints lie in different regions passes the advisory
|
|
only when \emph{both} endpoint regions permit spanning. The check is
|
|
authoring-time only and never alters reduction.
|
|
|
|
\textbf{Migration coverage.} The v0$\rightarrow$v1 migration
|
|
(Chapter~\ref{ch:migration}) reconstructs the event-anchored \texttt{Tie},
|
|
\texttt{Slur}, and \texttt{Beam} from the v0 reference (id plus event endpoints).
|
|
A \texttt{Spanner} is anchored by \texttt{TimeAnchor}s rather than a fixed pair
|
|
of event endpoints, so its full value is not reconstructable from the v0
|
|
event-reference projection; a \texttt{Spanner}-create is therefore reported
|
|
unmigratable (read-only), alongside the respell case of P12-K1, and remains so.
|
|
A faithful spanner migration awaits a richer v0 projection that carries the
|
|
anchors --- a Phase-3 / Pass-12 extension, not yet implemented.
|
|
|
|
\section{DeleteCrossCutting}
|
|
\label{sec:k0:delete-cross-cutting}
|
|
|
|
\textbf{Payload schema.} \texttt{DeleteCrossCuttingOp \{ structure: TypedObjectId
|
|
\}} --- the structure named by the same key the set-union creation and the
|
|
re-anchoring table use; it \MUST{} be a cross-cutting kind
|
|
(\texttt{Tie}/\texttt{Slur}/\texttt{Beam}/\texttt{Spanner}).
|
|
|
|
\textbf{Canonical encoding.} The canonical bytes of \texttt{structure}.
|
|
|
|
\textbf{Reduction rule.} Delete-wins: the structure is tombstoned (its identifier
|
|
retained). A second delete of the same structure is idempotent; deleting a
|
|
missing or non-cross-cutting id is a no-op precondition failure. Graph-aware
|
|
reduction removes the structure from the score.
|
|
|
|
\textbf{Conflict cases.} None (delete-wins is idempotent).
|
|
|
|
\textbf{Undo semantics.} A delete mints nothing, so the prototype's minted-object
|
|
undo (Section~\ref{sec:k0:undo}) does not re-introduce the tombstoned structure
|
|
(P11-C8).
|
|
|
|
\textbf{Re-anchoring.} The deletion is direct (the structure is the target, not a
|
|
referenced endpoint); it does not itself trigger the endpoint re-anchoring table.
|
|
|
|
\section{ModifyCrossCutting}
|
|
\label{sec:k0:modify-cross-cutting}
|
|
|
|
\textbf{Payload schema.} \texttt{ModifyCrossCuttingOp \{ structure:
|
|
CrossCuttingValue \}} --- the full replacement value (v1). The replacement keeps
|
|
the structure's identity but may change its endpoints and per-kind fields; the
|
|
LWW key is the structure's \texttt{CrossCuttingValue::id}.
|
|
|
|
\textbf{Canonical encoding.} The discriminant and length-framed bytes of the
|
|
\texttt{CrossCuttingValue} (as for CreateCrossCutting).
|
|
|
|
\textbf{Reduction rule.} A last-writer-wins field overwrite keyed by structure
|
|
id. Precondition: the structure is live. The reduction re-derives the structure's
|
|
endpoints from the new value, so a later re-anchoring sees them. A malformed
|
|
replacement is a precondition no-op --- in particular a beam whose membership
|
|
falls below the two-member minimum is refused rather than materialised.
|
|
Graph-aware reduction overwrites the structure in place.
|
|
|
|
\textbf{Conflict cases.} Two concurrent differing modifications of one structure
|
|
produce a \texttt{StructuralFieldCollision} on the field \texttt{cross\_cutting}.
|
|
|
|
\textbf{Undo semantics.} Value-restoring (Section~\ref{sec:k0:undo}): undo
|
|
restores the structure's chain-predecessor value unless superseded.
|
|
|
|
\textbf{Re-anchoring.} If the target structure is tombstoned, the modification is
|
|
a no-op; re-deriving the endpoints lets a subsequent endpoint tombstone re-anchor
|
|
the structure through the standard table (see DeleteEvent).
|
|
|
|
\section{ChangeRegionTimeModel}
|
|
\label{sec:k0:change-region-time-model}
|
|
|
|
\textbf{Payload schema.} \texttt{ChangeRegionTimeModelOp \{ region: RegionId,
|
|
new\_time\_model: RegionTimeModel, declared\_incompatible: Vec<EventId>,
|
|
remapping: PositionRemapping \}} --- the full target model value (v1).
|
|
|
|
\textbf{Canonical encoding.} \texttt{region}, the length-framed
|
|
\texttt{new\_time\_model} value, the canonically-ordered
|
|
\texttt{declared\_incompatible} set, then \texttt{remapping}.
|
|
|
|
\textbf{Reduction rule.} Structural migration. The region adopts the target time
|
|
model. Graph-aware reduction derives coordinate-kind incompatibilities from the
|
|
region's events (and from the remapping coverage) and refuses a migration that
|
|
would violate the coordinate discipline.
|
|
|
|
\textbf{Conflict cases.} Concurrent same-region migrations produce a
|
|
\texttt{StructuralFieldCollision} on the field \texttt{time\_model}; a migration
|
|
with incompatible events produces a \texttt{TimeModelMigrationFailure} naming the
|
|
region and the incompatible events. A causally-later migration is re-evaluated
|
|
against the first migration's graph rather than conflicting.
|
|
|
|
\textbf{Undo semantics.} Undo restores the region's prior time model under the
|
|
active policy.
|
|
|
|
\textbf{Re-anchoring.} Not applicable.
|
|
|
|
\begin{openquestion}
|
|
\textbf{P11-C6.} The rich migration payload --- a coordinate converter rather than a
|
|
\texttt{declared\_incompatible} list plus a \texttt{PositionRemapping} --- remains
|
|
the catalog's to design when graph-aware migration is the only reduction path.
|
|
\end{openquestion}
|
|
|
|
\section{Structural Containers}
|
|
\label{sec:k0:structural-containers}
|
|
|
|
\textbf{Payload schema.} Three create/delete pairs over the region hierarchy:
|
|
\texttt{CreateRegionOp \{ region: Region \}} /
|
|
\texttt{DeleteRegionOp \{ region: RegionId \}};
|
|
\texttt{CreateStaffInstanceOp \{ region: RegionId, instance: StaffInstance \}} /
|
|
\texttt{DeleteStaffInstanceOp \{ staff\_instance: StaffInstanceId \}};
|
|
\texttt{CreateVoiceOp \{ staff\_instance: StaffInstanceId, voice: Voice \}} /
|
|
\texttt{DeleteVoiceOp \{ voice: VoiceId \}}. Each create carries the full
|
|
container value (v1); the reduction preconditions it bears \emph{no typed child
|
|
object} --- an empty container.
|
|
|
|
\textbf{Canonical encoding.} Create: the parent id (where the schema names one),
|
|
then the length-framed canonical bytes of the container value. Delete: the
|
|
container id.
|
|
|
|
\textbf{Reduction rule.} Set-union creation of an \emph{empty} container, and an
|
|
\emph{empty-only} delete-wins tombstone. A create mints the container live if its
|
|
id is fresh and (for staff instance and voice) its parent is live; it
|
|
preconditions the carried value to bear no typed child object (a region: no staff
|
|
instances, barline-alignment groups, or graphic objects; a staff instance: no
|
|
voices or measures; a voice: no events), since those carry distinct
|
|
\texttt{TypedObjectId}s the reducer mints separately --- so contents are added by
|
|
subsequent operations. A delete is a delete-wins tombstone, but a
|
|
\emph{precondition no-op} (\texttt{ContainerNotEmpty}) unless the container has no
|
|
live children --- the caller deletes contents first. Graph-aware reduction adds
|
|
or removes the container and maintains the region's staff extent so
|
|
\texttt{RegionExtents} stays satisfied.
|
|
|
|
\textbf{Conflict cases.} None at reduction time: creation is set-union (a repeat
|
|
create is idempotent), and the empty-only delete is a deterministic precondition
|
|
gate, not a conflict.
|
|
|
|
\textbf{Undo semantics.} Undo of a \emph{create} tombstones the minted container
|
|
(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if it was
|
|
concurrently mutated, with the policy treatment as for InsertEvent. A
|
|
\emph{delete} mints nothing, so the prototype's minted-object undo does not
|
|
re-introduce it (P11-C8).
|
|
|
|
\textbf{Re-anchoring.} Not applicable (the containers are minted/tombstoned by id;
|
|
the empty-only precondition means a delete never strands live children).
|
|
|
|
\section{CreateStaff}
|
|
\label{sec:k0:create-staff}
|
|
|
|
\textbf{Payload schema.} \texttt{CreateStaffOp \{ staff: Staff \}} --- the full
|
|
global-staff value (v1): identity, name, abbreviation, instrument reference,
|
|
default staff-line configuration, and optional group membership.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{staff}.
|
|
|
|
\textbf{Reduction rule.} Set-union creation of a global \texttt{Staff} on the
|
|
score root, completing the structural-container family
|
|
(Section~\ref{sec:k0:structural-containers}) upward: staff \emph{instances}
|
|
reference global staves, and until this primitive existed a resolvable staff
|
|
could only be base-seeded. A create mints the staff live if its id is fresh; a
|
|
repeat create carrying a byte-identical value reduces idempotently, and a
|
|
create whose id is already live with a \emph{differing} value is a
|
|
precondition no-op with the appended reason
|
|
\texttt{RecreateContentMismatch} (discriminant 13; ratified Pass~12, closing
|
|
P12-K9 --- the former \texttt{TargetMissing} reuse misnamed the situation:
|
|
the target is not missing, its content disagrees). The same reason applies
|
|
to the carried \texttt{TimeSignature} (Section~\ref{sec:k0:meter-tempo}),
|
|
the other re-create site at which the reducer retains the carried value for
|
|
comparison. The structural-container creates
|
|
(Section~\ref{sec:k0:structural-containers}) are plain set-union --- any
|
|
repeat create of a live id reads \texttt{AlreadyApplied} without value
|
|
comparison, since the carried value is preconditioned empty of children. Graph-aware reduction additionally preconditions that the
|
|
referenced instrument is live and, when \texttt{group} is present, that the
|
|
staff group resolves --- the mint must leave the graph satisfying the
|
|
reference-resolution invariants.
|
|
|
|
With staves mintable, \texttt{CreateStaffInstance}
|
|
(Section~\ref{sec:k0:structural-containers}) preconditions that the
|
|
instance's referenced \texttt{Staff} is live (previously the reference was
|
|
satisfiable only from the seeded base, so the check was vacuous).
|
|
|
|
\textbf{Conflict cases.} None at reduction time (set-union; the differing-value
|
|
re-create is a precondition gate, not a conflict).
|
|
|
|
\textbf{Undo semantics.} Undo of a create tombstones the minted staff
|
|
(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if a live staff
|
|
instance references it (tombstoning it would strand the instance).
|
|
|
|
\textbf{Re-anchoring.} Not applicable (a staff mint references no tombstonable
|
|
anchor; there is no \texttt{DeleteStaff} in this catalogue revision --- an
|
|
empty-only staff delete mirroring the container discipline is a later
|
|
schema-fill).
|
|
|
|
\section{Repeat Structures}
|
|
\label{sec:k0:repeat-structures}
|
|
|
|
Ratified with the schema-major-2 revision: the dedicated authoring pair for
|
|
\texttt{RepeatStructure} (core specification Chapter~5
|
|
\sectionsc{Repeat Structures}). Repeats live in the cross-cutting registry
|
|
but are \emph{not} \texttt{CrossCuttingValue} kinds on the wire --- the
|
|
cross-cutting operations admit only
|
|
\texttt{Tie}/\texttt{Slur}/\texttt{Beam}/\texttt{Spanner}
|
|
(Section~\ref{sec:k0:create-cross-cutting}) --- so the pair is a
|
|
first-class primitive mirroring the cross-cutting disciplines.
|
|
|
|
\textbf{Payload schema.} \texttt{CreateRepeatStructureOp \{ repeat:
|
|
RepeatStructure \}} --- the full value (schema major 2): identity, the
|
|
\texttt{start}/\texttt{end} anchors, the \texttt{RepeatKind}, and the
|
|
volta list. \texttt{DeleteRepeatStructureOp \{ repeat: RepeatStructureId
|
|
\}}.
|
|
|
|
\textbf{Canonical encoding.} Create: the length-framed canonical bytes of
|
|
\texttt{repeat} (the schema-major-2 layout). Delete: the bare identifier.
|
|
The create's payload embeds the v2 \texttt{RepeatStructure} layout
|
|
unconditionally (\texttt{kind} and \texttt{voltas} are not optional
|
|
fields), so under minimal stamping a block carrying one stamps schema
|
|
major~2 --- the create is \emph{born at v2}. The delete's payload is an
|
|
identifier --- a major-0 layout --- so minimal stamping gives its blocks
|
|
major~0; the kind discriminant itself is an append-only schema-\emph{minor}
|
|
vocabulary event (the same append mechanism as the Phase-3 tranche; the
|
|
stamp itself always follows minimal stamping over the payload, per the
|
|
Binary Format companion \sectionsc{Schema Major 2}).
|
|
|
|
\textbf{Reduction rule.} Set-union creation and a delete-wins tombstone,
|
|
mirroring the cross-cutting family. A create mints the repeat live if its
|
|
id is fresh and \emph{every} event-referencing anchor site resolves to a
|
|
live event --- \texttt{start}/\texttt{end}, the kind's jump targets
|
|
(\texttt{DaCapo.end\_target},
|
|
\texttt{DalSegno.segno}/\texttt{end\_target}), and each volta's
|
|
\texttt{start}/\texttt{end} --- since the mint must leave the graph
|
|
satisfying the reference-resolution invariants; a dead anchor is a
|
|
precondition no-op (\texttt{TargetMissing}). A repeat create of a live id
|
|
reads \texttt{AlreadyApplied} without value comparison (the cross-cutting
|
|
discipline; the \texttt{RecreateContentMismatch} scope of
|
|
Section~\ref{sec:k0:create-staff} is unchanged). A delete tombstones the
|
|
repeat (idempotent on re-delete, delete-wins); deleting a missing id is a
|
|
no-op precondition failure. Graph-aware reduction adds or removes the
|
|
structure from the cross-cutting registry.
|
|
|
|
\textbf{Conflict cases.} None at reduction time (set-union creation;
|
|
delete-wins is idempotent).
|
|
|
|
\textbf{Undo semantics.} Undo of a create tombstones the minted repeat
|
|
(Section~\ref{sec:k0:undo}). A delete mints nothing, so the prototype's
|
|
minted-object undo does not re-introduce the tombstoned structure
|
|
(P11-C8).
|
|
|
|
\textbf{Re-anchoring.} The structure participates in the re-anchoring rule
|
|
table when a referenced event is later tombstoned: re-anchor to the
|
|
nearest surviving anchor, cascade-delete only when none survives --- as
|
|
for spanners, spanning \emph{every} anchor site
|
|
(\texttt{start}/\texttt{end}, jump targets, volta spans). Among multiple
|
|
surviving candidates --- a case slurs and spanners never present, since
|
|
their sole other endpoint is the forced survivor --- ``nearest'' is
|
|
currently realized as the deterministic identifier-order minimum (the
|
|
same tie-break the two-endpoint collapse already used); proximity-aware
|
|
(four-key) selection over a repeat's surviving sites is a deferred
|
|
refinement, exactly as the spanner row defers per-kind proximity bounds.
|
|
The rule row is the core specification's (Chapter~6 re-anchoring rule
|
|
table, ratified with this pair).
|
|
|
|
\textbf{Authoring advisory.} The volta well-formedness constraints of
|
|
core Chapter~5 (endings non-empty, 1-based, \emph{strictly} ascending) are
|
|
\emph{advisory}: surfaced at authoring time under interactive validation,
|
|
never enforced under reduction.
|
|
|
|
\section{SetUserSystemBreak}
|
|
\label{sec:k0:set-user-system-break}
|
|
|
|
\textbf{Payload schema.} \texttt{SetUserSystemBreakOp \{ region: RegionId,
|
|
anchor: TimeAnchor, present: bool \}} --- the full anchor value (v1).
|
|
|
|
\textbf{Canonical encoding.} \texttt{region}, the length-framed \texttt{anchor}
|
|
value, then the boolean.
|
|
|
|
\textbf{Reduction rule.} A last-writer-wins advisory. The break preference is
|
|
recorded for the region keyed by the anchor's \emph{resolved musical position};
|
|
graph-aware reduction adds or removes the anchor from the region's user
|
|
system-break list.
|
|
|
|
\textbf{Conflict cases.} None (LWW advisory).
|
|
|
|
\textbf{Undo semantics.} Undo restores the prior advisory value for the
|
|
\texttt{(region, resolved-position)} key.
|
|
|
|
\textbf{Re-anchoring.} Not applicable in the prototype (the advisory is keyed by
|
|
resolved position; a tombstoned anchor target degrades to the region origin).
|
|
|
|
\section{Score Settings}
|
|
\label{sec:k0:score-settings}
|
|
|
|
\textbf{Payload schema.} Three score-level field overwrites:
|
|
\texttt{SetMetadataOp \{ metadata: ScoreMetadata \}} overwrites the score
|
|
singleton; \texttt{SetMetricGridOp \{ region: RegionId, grid: Option<MetricGrid>
|
|
\}} overwrites (or clears) a region's default metric grid;
|
|
\texttt{SetUserPageBreakOp \{ region: RegionId, anchor: TimeAnchor, present: bool
|
|
\}} is the page-break sibling of SetUserSystemBreak.
|
|
|
|
\textbf{Canonical encoding.} Metadata: the length-framed \texttt{metadata} value.
|
|
Metric grid: \texttt{region}, then an \texttt{Option} discriminant and (when
|
|
present) the length-framed \texttt{grid} value. Page break: \texttt{region}, the
|
|
length-framed \texttt{anchor} value, then the boolean.
|
|
|
|
\textbf{Reduction rule.} Three field overwrites differing only in discipline.
|
|
\emph{SetMetadata} is an \textbf{advisory} last-writer-wins: the latest write in
|
|
canonical order silently wins and the operation always applies --- no working
|
|
state and no conflict (the same discipline as SetUserSystemBreak, on the score
|
|
singleton). \emph{SetMetricGrid} is a \textbf{structural} field overwrite keyed
|
|
by region: precondition the region is live and staff-based (a FreeGraphic region
|
|
has no metric-grid slot --- the op is a no-op there), and reject a grid whose
|
|
meter sequence names a time signature that is not live (the Chapter~5 invariant
|
|
forbids installing such a grid). \emph{SetUserPageBreak} is a canonical LWW
|
|
advisory keyed by the anchor's resolved musical position, with the same
|
|
staff-based precondition. Graph-aware reduction overwrites the metadata singleton,
|
|
sets the region's default metric grid, or adds/removes the page-break anchor
|
|
under its resolved-position key (so two anchors resolving to one position occupy a
|
|
single slot).
|
|
|
|
\textbf{Conflict cases.} SetMetadata and SetUserPageBreak: none (advisory LWW).
|
|
SetMetricGrid: two concurrent differing grids for one region produce a
|
|
\texttt{StructuralFieldCollision} on the field \texttt{metric\_grid}.
|
|
|
|
\textbf{Undo semantics.} All three are value-restoring field overwrites
|
|
(Section~\ref{sec:k0:undo}): undo restores the prior metadata, grid, or break
|
|
preference from the key's write chain unless superseded.
|
|
|
|
\textbf{Re-anchoring.} The advisory breaks degrade as for SetUserSystemBreak; the
|
|
metric grid and metadata are keyed by region / singleton and do not re-anchor (a
|
|
deleted region's settings are no-ops --- \texttt{TargetMissing}).
|
|
|
|
\section{Meter and Tempo Overwrites}
|
|
\label{sec:k0:meter-tempo}
|
|
|
|
\textbf{Payload schema.} The finer-grained metric-model overwrites beneath the
|
|
whole-grid \texttt{SetMetricGrid} (Section~\ref{sec:k0:score-settings}):
|
|
\texttt{SetTimeSignatureOp \{ region: RegionId, anchor: TimeAnchor,
|
|
time\_signature: Option<TimeSignature> \}} sets, replaces, or (\texttt{None})
|
|
removes the single \texttt{MeterChange} at the anchor's resolved musical
|
|
position in the region's default metric grid, carrying the full
|
|
\texttt{TimeSignature} value (v1); \texttt{SetTempoSegmentOp \{ region:
|
|
Option<RegionId>, start: TimeAnchor, segment: Option<TempoSegment> \}} sets,
|
|
replaces, or removes the single tempo segment starting at the resolved
|
|
position, in the score-level tempo map (\texttt{region: None}) or the region's
|
|
local map (\texttt{Some}; a set on a region with no local map creates one).
|
|
|
|
\textbf{Canonical encoding.} Time signature: \texttt{region}, the
|
|
length-framed \texttt{anchor}, then an \texttt{Option} discriminant and (when
|
|
present) the length-framed \texttt{time\_signature} value. Tempo segment: an
|
|
\texttt{Option} discriminant and (when present) \texttt{region}, then the
|
|
length-framed \texttt{start}, then an \texttt{Option} discriminant and (when
|
|
present) the length-framed \texttt{segment}.
|
|
|
|
\textbf{Reduction rule.} Last-writer-wins structural overwrites keyed by
|
|
\texttt{(region, resolved position)} (time signature) and \texttt{(scope,
|
|
resolved start)} (tempo segment). A carried \texttt{TimeSignature} is minted
|
|
set-union under the same discipline as \texttt{CreateStaff}: fresh id mints;
|
|
byte-identical re-carry is idempotent; a differing value under a live id is a
|
|
precondition no-op (\texttt{RecreateContentMismatch},
|
|
Section~\ref{sec:k0:create-staff}). The time-signature value's beat-group sum is validated at
|
|
construction and again at decode, so a malformed value never reaches
|
|
reduction. A tempo-segment write preconditions that the \emph{resulting} map
|
|
is well-formed (segments ordered and non-overlapping; a non-constant shape
|
|
carries its end data; the carried segment's own start equals the operation's
|
|
\texttt{start} key) --- a write that would malform the map is refused as a
|
|
precondition no-op (\texttt{TempoMapMalformed}). Graph-aware reduction applies
|
|
the meter change to \texttt{default\_metric\_grid.meter\_sequence} and the
|
|
segment to the scoped tempo map.
|
|
|
|
\textbf{Conflict cases.} Two concurrent differing writes of one key produce a
|
|
\texttt{StructuralFieldCollision} on the field \texttt{meter\_sequence} or
|
|
\texttt{tempo\_segments} respectively, with the standard winner/loser
|
|
recording; identical concurrent writes reduce idempotently.
|
|
|
|
\textbf{Undo semantics.} Value-restoring per Section~\ref{sec:k0:undo}: undo
|
|
restores the key's chain-predecessor value (or its absence).
|
|
|
|
\textbf{Re-anchoring.} An event-anchored \texttt{anchor}/\texttt{start} whose
|
|
event is later tombstoned degrades by the framework's anchor rules; the
|
|
overwrite keys on the \emph{resolved} position, so the recorded change
|
|
survives its anchor.
|
|
|
|
\begin{openquestion}
|
|
\textbf{P12-C5.} A mid-region meter change authored by
|
|
\texttt{SetTimeSignature} reduces cleanly and materialises into the grid, but
|
|
the notational-decomposition pre-pass currently honours only a region's
|
|
\emph{first} governing meter (P12-H4's single-meter simplification), so the
|
|
derived notation ignores the change until multi-meter decomposition lands.
|
|
The reduction-level semantics are pinned here; the derived-annotation gap is
|
|
P12-H4's.
|
|
\end{openquestion}
|
|
|
|
\section{SetStaffLayout}
|
|
\label{sec:k0:set-staff-layout}
|
|
|
|
\textbf{Payload schema.} \texttt{SetStaffLayoutOp \{ staff\_instance:
|
|
StaffInstanceId, instrument\_override: Option<InstrumentId>,
|
|
staff\_lines\_override: Option<StaffLineConfiguration>, visible: bool \}} ---
|
|
the non-break layout advisories with a graph home: the staff instance's three
|
|
inline advisory fields, overwritten as a unit.
|
|
|
|
\textbf{Canonical encoding.} \texttt{staff\_instance}, an \texttt{Option}
|
|
discriminant and (when present) \texttt{instrument\_override}, an
|
|
\texttt{Option} discriminant and (when present) the length-framed
|
|
\texttt{staff\_lines\_override}, then the boolean.
|
|
|
|
\textbf{Reduction rule.} A last-writer-wins \emph{advisory} overwrite keyed by
|
|
\texttt{staff\_instance}. Preconditions: the staff instance is live; a present
|
|
\texttt{instrument\_override} resolves to a live instrument under graph-aware
|
|
reduction. The richer engraving-override vocabulary (stem direction, notehead
|
|
shape, custom positions) has no durable graph home yet and remains projected
|
|
layout state --- extending this primitive to cover it is staged with the
|
|
data-model expansion.
|
|
|
|
\textbf{Conflict cases.} None (LWW advisory).
|
|
|
|
\textbf{Undo semantics.} Value-restoring per Section~\ref{sec:k0:undo}.
|
|
|
|
\textbf{Re-anchoring.} If the staff instance is tombstoned, the overwrite is a
|
|
no-op (\texttt{TargetTombstoned}).
|
|
|
|
\section{DeclareTransaction}
|
|
\label{sec:k0:declare-transaction}
|
|
|
|
\textbf{Payload schema.} \texttt{TransactionDescriptor \{ id: TransactionId,
|
|
label: String, category: Option<TransactionCategory> \}}. Value-complete in v0
|
|
and unchanged.
|
|
|
|
\textbf{Reduction rule.} Records the descriptor. Member primitives reference the
|
|
transaction id and \MUST{} causally depend on the descriptor; the members reduce
|
|
atomically (all-or-nothing) in canonical order.
|
|
|
|
\textbf{Conflict cases.} A missing descriptor or a member that does not causally
|
|
follow it produces a \texttt{TransactionConflict}; any member failure rolls back
|
|
the whole transaction and all members read \texttt{NoOp\{TransactionConflict\}}.
|
|
|
|
\textbf{Undo / re-anchoring.} Transactions are the unit of undo
|
|
(Section~\ref{sec:k0:undo}); re-anchoring is per member.
|
|
|
|
\section{ResolveConflict (meta-operation)}
|
|
\label{sec:k0:resolve-conflict}
|
|
|
|
\textbf{Payload schema.} \texttt{ResolveConflictPayload \{ target: ConflictId,
|
|
action: ResolutionAction \}}. Value-complete.
|
|
|
|
\textbf{Reduction rule.} Transitions the target conflict's resolution state. An
|
|
action of \texttt{Dismiss} reaches the \texttt{Dismissed} state; any other action
|
|
reaches \texttt{Resolved}. Re-resolving with the same action is idempotent; two
|
|
concurrent resolves with differing actions produce a meta-conflict.
|
|
|
|
\emph{Beyond the concurrent case (ratified Pass~12, closing P12-K4).} The
|
|
earliest-applied-resolve-governs rule is \emph{universal}: a causally-later
|
|
resolve with a differing action does not supersede the first --- it reduces
|
|
\texttt{AlreadyApplied} --- and \emph{any} resolve targeting a
|
|
\texttt{Dismissed} conflict likewise reads \texttt{AlreadyApplied}.
|
|
Intentional re-resolution is deliberately outside the v1 operation set; a
|
|
future dedicated operation (a \texttt{ReopenConflict}-class primitive) is the
|
|
sanctioned path if it is ever needed. The meta-conflict record names both
|
|
resolver operation ids in \texttt{caused\_by}; conflict records themselves
|
|
have no \texttt{TypedObjectId} kind (deliberate --- they are materialized
|
|
state, not graph objects), so the contested conflict is identified by the
|
|
\texttt{equivocation}-style field key, not an object reference.
|
|
|
|
\begin{rationale}
|
|
Pass~11 added \texttt{ResolutionAction::Dismiss} (item 2.5) precisely so the
|
|
\texttt{Dismissed} state is reachable by an authored operation rather than merely
|
|
representable. The catalog records that \texttt{Dismiss} is the action that
|
|
selects it (resolving the v0 ambiguity P11-C10).
|
|
\end{rationale}
|
|
|
|
\section{ResolveEquivocation (meta-operation)}
|
|
\label{sec:k0:resolve-equivocation}
|
|
|
|
\textbf{Payload schema.} \texttt{ResolveEquivocationPayload \{ target:
|
|
OperationId, chosen: EnvelopeHash \}} --- the equivocated slot and the
|
|
candidate envelope (by canonical-bytes hash) that shall stand. Value-complete.
|
|
|
|
\textbf{Canonical encoding.} \texttt{target} (16 canonical bytes), then
|
|
\texttt{chosen} (32 bytes), per the codec baseline.
|
|
|
|
\textbf{Reduction rule.} Order-independent promotion of an equivocated slot
|
|
(core specification Chapter~6, \sectionsc{Equivocation}): when the operation
|
|
set holds an \texttt{Equivocated} slot for \texttt{target} and \texttt{chosen}
|
|
names one of its candidates, the slot reduces as if it had always been
|
|
\texttt{Single} with the chosen envelope --- the chosen candidate contributes
|
|
to canonical reduction at its own canonical position, and operations that were
|
|
pending on the equivocated id unblock. Among multiple resolves naming the same
|
|
slot, the one earliest in canonical order governs; a later resolve naming the
|
|
\emph{same} candidate reduces idempotently (\texttt{AlreadyApplied}). The
|
|
resolve operation must itself occupy a \texttt{Single} slot; an equivocated
|
|
resolve is excluded from reduction like any other equivocated slot. A resolved
|
|
slot records no \texttt{OperationSlotEquivocated} anomaly; the losing
|
|
candidates remain in the diagnostic candidate store only.
|
|
|
|
\textbf{Conflict cases.} Two resolves of one slot naming \emph{differing}
|
|
candidates produce a \texttt{StructuralFieldCollision} meta-conflict on the
|
|
field \texttt{equivocation\_resolution}, recording the governing resolve
|
|
(earlier in canonical order) as winner and the later as loser, with both
|
|
operations in \texttt{caused\_by} --- the same discipline as
|
|
\texttt{ResolveConflict} meta-conflicts. Preconditions: a resolve whose
|
|
\texttt{target} is not an equivocated slot, or whose \texttt{chosen} is not
|
|
among the slot's candidates, is a precondition no-op.
|
|
|
|
\textbf{Edge semantics (ratified Pass~12, closing P12-K6).} Promotion is
|
|
\emph{single-pass}, not fixpoint: a promoted candidate that is itself a
|
|
\texttt{ResolveEquivocation} does not govern a further promotion in the same
|
|
reduction. A resolve in a \emph{quarantined} replica segment is excluded from
|
|
reduction and never governs. A resolve held \emph{pending} by its own causal
|
|
gaps still governs promotion --- the verdict is a pure function of the slot
|
|
map (set-level), while the resolve's own effect stays pending. The
|
|
invalid-target/invalid-chosen no-op reuses \texttt{TargetMissing}; a dedicated
|
|
reason was considered and rejected (the appended-reason budget is spent where
|
|
a distinct verdict changes caller behavior, which it does not here).
|
|
|
|
\textbf{Undo semantics.} Mints nothing; not inverted under the prototype's
|
|
minted-object undo (P11-C8).
|
|
|
|
\textbf{Re-anchoring.} Not applicable (the payload references an operation
|
|
slot, not a graph object).
|
|
|
|
\begin{rationale}
|
|
The core specification names three resolution paths for an equivocated slot:
|
|
transport-level reconciliation, this explicit operation, and a
|
|
profile-declared deterministic selection policy. This entry pins the schema
|
|
for the explicit-operation path, which the core specification previously named
|
|
only in prose. The profile-policy path is \emph{deferred with a named landing
|
|
site} (Pass~12 disposition of P12-K5): v1 profiles declare \emph{no}
|
|
selection function, and the hook's definition belongs to the Profile
|
|
Conformance companion when it is written --- the reducer deliberately carries
|
|
no policy hook until a profile can declare one.
|
|
\end{rationale}
|
|
|
|
\section{UndoTransaction (meta-operation)}
|
|
\label{sec:k0:undo}
|
|
|
|
\textbf{Payload schema.} \texttt{UndoTransactionPayload \{ target: TransactionId,
|
|
policy: UndoPolicy \}}, with \texttt{UndoPolicy} one of \texttt{StrictInverse},
|
|
\texttt{BestEffort}, \texttt{Cascade}. Value-complete.
|
|
|
|
\textbf{Reduction rule.} A forward compensating edit computed against the
|
|
materialised state at the undo's canonical position (never literal time
|
|
travel). The compensation has two parts.
|
|
|
|
\emph{Minted-object tombstoning} (as before): every object the target
|
|
transaction minted is tombstoned. \texttt{StrictInverse} conflicts
|
|
(\texttt{TombstonedTarget}) if any minted object was already tombstoned;
|
|
\texttt{BestEffort} tombstones the survivors.
|
|
|
|
\emph{Value restoration} (this revision): for every last-writer-wins overwrite
|
|
the target transaction performed --- event and identified-pitch modification,
|
|
respelling, cross-cutting modification, metadata, metric grid, meter change,
|
|
tempo segment, staff layout, and the user break advisories --- the reducer
|
|
maintains, per overwritten key, the \emph{canonical-order write chain} of
|
|
(writer, value) pairs. Undoing the transaction restores each written key to
|
|
its chain-predecessor value (or its absence, where the transaction introduced
|
|
the first value), \emph{provided the transaction's write is still the key's
|
|
last writer}. Because the chain is keyed by canonical order, the restored
|
|
value is a pure function of the operation set: permutation-invariant by
|
|
construction. When a causally-later or canonically-later write has
|
|
superseded the key, \texttt{StrictInverse} refuses the whole undo with a
|
|
\texttt{TransactionConflict} conflict naming the undo and the superseding
|
|
writer; \texttt{BestEffort} restores the still-last-written keys and skips
|
|
the superseded ones. Restorations are expressed in the effect status (a fully
|
|
clean compensation is \texttt{Applied}; a mixed one is
|
|
\texttt{AppliedWithRepair} carrying only the tombstone repairs) --- no new
|
|
repair vocabulary.
|
|
|
|
\emph{Strand-blocks (ratified Pass~12, closing P12-K10).} A
|
|
\texttt{StrictInverse} undo that refuses to tombstone a minted object still
|
|
referenced by a live non-member (e.g., a staff whose instance survives outside
|
|
the transaction) records \texttt{ConflictKind::TransactionConflict} --- the
|
|
reuse is blessed: the strand-block \emph{is} a transaction-scoped conflict of
|
|
the undo, and the conflict record's affected objects and description carry the
|
|
strand detail. No dedicated undo conflict kind is added.
|
|
|
|
\emph{Idempotence asymmetry (ratified Pass~12, closing P12-K11).} An undo's
|
|
value restorations enter the write chains as ordinary writes by the undo
|
|
operation --- no distinguished undo provenance. Consequently a \emph{second}
|
|
undo of the same transaction finds each restored key superseded by the first
|
|
undo and refuses (\texttt{Conflicted} under \texttt{StrictInverse}, skipped
|
|
under \texttt{BestEffort}), while \emph{absence} restorations (not
|
|
representable as chain writes) repeat idempotently. The asymmetry is
|
|
normative, documented behavior; a chain-native undo provenance would be
|
|
revisited only under the deferred undo-as-operation (streaming-consistent
|
|
undo) design, which subsumes this question.
|
|
|
|
\emph{Still deferred} (P11-C8, narrowed): re-introducing content tombstoned by
|
|
\emph{delete} primitives (a deterministic resurrection needs a system-derived
|
|
identifier derivation the ratified closed tag set does not yet include);
|
|
\texttt{Transpose} inversion (interval algebra, P12-K2); and
|
|
\texttt{Cascade}'s dependent-closure computation --- \texttt{Cascade} remains
|
|
\texttt{StrictInverse} over the same set.
|
|
|
|
% ===========================================================================
|
|
\chapter{v0 \texorpdfstring{$\rightarrow$}{->} v1 Payload Migration}
|
|
\label{ch:migration}
|
|
|
|
A v0 envelope carries an identifier-only payload; a v1 envelope carries the
|
|
value-typed payload this catalog defines. The two forms do not coexist as
|
|
permanent dialects (that would double the reducer surface forever); instead the
|
|
catalog ships a \textbf{one-time migration} that lifts a v0 envelope to v1 using
|
|
the score graph as context, applied once on read. Production code carries only v1
|
|
payloads; v0 envelopes survive only as a regression corpus.
|
|
|
|
\begin{requirement}
|
|
\label{req:migration:properties}
|
|
The migration \texttt{migrate\_v0\_envelope(v0, context: \&Score)} \MUST{} be
|
|
\textbf{deterministic} (two implementations migrating the same v0 envelope
|
|
against the same context produce byte-identical v1 envelopes) and
|
|
\textbf{equivalence-preserving} (a v0 envelope and its v1 migration reduce to
|
|
byte-identical canonical \texttt{MaterializedState}). When a value cannot be
|
|
reconstructed from the v0 projection plus the context, the migration \MUST{}
|
|
report the envelope unmigratable rather than fabricate a value, and the bundle
|
|
opens read-only.
|
|
\end{requirement}
|
|
|
|
The reference implementation (\texttt{epiphany-ops::migrate}) reconstructs the
|
|
\texttt{InsertEvent} event, the \texttt{DeleteEvent} compensation, the
|
|
\texttt{ChangeRegionTimeModel} model, the \texttt{SetUserSystemBreak} anchor, and
|
|
the event-anchored cross-cutting structures (\texttt{Tie} / \texttt{Slur} /
|
|
\texttt{Beam}) self-containedly from the v0 projection; a \texttt{Spanner},
|
|
anchored by \texttt{TimeAnchor}s rather than event endpoints, remains unmigratable
|
|
until the projection carries them. It recovers a \texttt{RespellPitch} spelling
|
|
from the context (P12-K1,
|
|
Section~\ref{sec:k0:respell-pitch}). The migration's merge gate
|
|
(\texttt{epiphany-testkit::migration}) drives the inverse direction --- projecting
|
|
a v1 corpus to v0 and migrating it back --- and asserts byte-identical reduction
|
|
plus a non-vacuity guard.
|
|
|
|
% ===========================================================================
|
|
\chapter{K1 --- Framework Slots (Phase 3)}
|
|
\label{ch:k1}
|
|
|
|
This chapter drafted the remaining catalogue items as framework slots. The
|
|
Phase-2 \textbf{M2} expansion (the broad-K0 groups in \texttt{epiphany-ops})
|
|
implemented four groups of them; with the \textbf{M2e} catalogue expansion their
|
|
full per-primitive schemas now appear in Chapter~\ref{ch:k0}, so they are
|
|
\emph{normative under the Phase-2 profile} and an implementation \MUST{}
|
|
\emph{not} reject them. They are cross-referenced first. The genuinely Phase-3
|
|
slots that remain \textbf{unavailable} are listed second: an implementation
|
|
\MUST{} reject an operation of one of \emph{those} kinds. Each remaining slot is a
|
|
schema-fill against the template of Chapter~\ref{ch:framework}; adding one is not
|
|
a fresh design.
|
|
|
|
\section*{Implemented since M2 (now in Chapter~\ref{ch:k0})}
|
|
|
|
\begin{description}
|
|
\item[Modify event; identified-pitch operations; transpose]
|
|
M2 Group~1 --- Sections~\ref{sec:k0:modify-event},
|
|
\ref{sec:k0:identified-pitch}, and \ref{sec:k0:transpose}.
|
|
\item[Delete / modify cross-cutting]
|
|
M2 Group~2 --- Sections~\ref{sec:k0:delete-cross-cutting} and
|
|
\ref{sec:k0:modify-cross-cutting} (creation is
|
|
Section~\ref{sec:k0:create-cross-cutting}).
|
|
\item[Create / delete region / staff instance / voice]
|
|
M2 Group~3 --- Section~\ref{sec:k0:structural-containers} (set-union creation
|
|
and the empty-only delete).
|
|
\item[Set metadata / metric grid / user page break]
|
|
M2 Group~4 --- Section~\ref{sec:k0:score-settings} (advisory metadata,
|
|
structural metric grid, advisory page break).
|
|
\end{description}
|
|
|
|
\section*{Implemented in the Phase-3 first tranche (now in Chapter~\ref{ch:k0})}
|
|
|
|
\begin{description}
|
|
\item[Create staff; set time signature / tempo segment; set layout]
|
|
Sections~\ref{sec:k0:create-staff}, \ref{sec:k0:meter-tempo}, and
|
|
\ref{sec:k0:set-staff-layout}. The disciplines are as drafted: set-union
|
|
creation, LWW structural overwrite, and LWW advisory respectively.
|
|
\end{description}
|
|
|
|
\section*{Added in the schema-major-2 revision (Chapter~\ref{ch:k0})}
|
|
|
|
\begin{description}
|
|
\item[Create / delete repeat structure]
|
|
Section~\ref{sec:k0:repeat-structures} --- net-new primitives (never
|
|
drafted as framework slots). Set-union creation with the
|
|
all-anchors-live precondition and a delete-wins tombstone; the create
|
|
is born at v2, the delete stamps major~0.
|
|
\end{description}
|
|
|
|
\section*{Retired slots (ratified Pass~12: outside the operation set)}
|
|
|
|
\begin{description}
|
|
\item[Create score / canvas --- retired, closing P12-K8]
|
|
The document root and the canvas are \emph{structural givens}, not
|
|
operation products: \texttt{TypedObjectId} has no Canvas kind, the root is
|
|
never op-minted, and genesis is normatively the empty-document constructor
|
|
plus bundle creation, outside the operation set (core specification,
|
|
Chapter~5 \sectionsc{The Canvas}). These are not ``unavailable slots''
|
|
awaiting a design --- no operation kind will be assigned to them. The
|
|
decision is revisited only if an addressable multi-canvas model is adopted
|
|
at a future schema major.
|
|
\end{description}
|
|
|
|
\begin{nongoal}
|
|
The full $60$--$80$-primitive catalogue is not a Phase-2 deliverable. The
|
|
framework (Chapter~\ref{ch:framework}) and the K0 representative set
|
|
(Chapter~\ref{ch:k0}) are sufficient to exercise every reduction discipline; the
|
|
remaining primitives are Phase-3 schema-fill.
|
|
\end{nongoal}
|
|
|
|
\end{document}
|