2394 lines
125 KiB
TeX
2394 lines
125 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
|
|
}
|
|
% Numbered within chapter (this document has chapters); see core_spec.tex's
|
|
% requirement box for why a plain counter + `code=` step is used instead of
|
|
% tcolorbox's own "auto counter, number within=..." keys.
|
|
\newcounter{requirement}[chapter]
|
|
\renewcommand{\therequirement}{\thechapter.\arabic{requirement}}
|
|
\newtcolorbox{requirement}[1][]{
|
|
enhanced, breakable,
|
|
colback=white, colframe=epiphanygold,
|
|
fonttitle=\bfseries\color{white}, code={\refstepcounter{requirement}}, title={\scshape\hspace{2pt}Requirement~\therequirement},
|
|
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.14.0 --- Pickup/anacrusis: what a partial measure actually costs (P13-S19)}\\[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}.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.8.0 (Push~4a, transpose algebra).} Adds one
|
|
operation kind, \texttt{TransposeInterval}
|
|
(Section~\ref{sec:k0:transpose-interval}), carrying the existing
|
|
\texttt{TranspositionInterval} of core Chapter~2. It transposes scale
|
|
position, refuses
|
|
atomically rather than saturating, takes a genuine \emph{set} of targets, and
|
|
propagates the resulting spelling. \texttt{Transpose}
|
|
(Section~\ref{sec:k0:transpose}) is \textbf{frozen}: its saturation, its
|
|
nominal-blindness, and its duplicate-sensitivity are pinned as normative
|
|
replay semantics and no longer authored. This supersedes the 0.6.0 pin of the
|
|
Transpose prototype (P12-K2), which anticipated a payload schema-major landing
|
|
with the tuning catalog; neither proved necessary. Appended vocabulary (minor,
|
|
append-only): \texttt{AcousticRealizationPinned} (14) and
|
|
\texttt{TranspositionOutOfRange} (15) in \texttt{PreconditionFailureReason};
|
|
\texttt{PitchSpaceMismatch} (6) is un-reserved and now produced for a
|
|
non-\texttt{Cmn} position. That case reads the position discriminant and does
|
|
not require a pitch-space registry.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.9.0 (P13-S2, space-relative CMN).} Broadens the
|
|
\texttt{PitchSpaceMismatch} (6) case for \texttt{TransposeInterval}: a
|
|
\texttt{Cmn} target whose enclosing chromatic structure or nominal mapping
|
|
cannot be established now refuses under core requirement
|
|
\texttt{req:pitch:space-capability-refusal}, rather than receiving guessed
|
|
12-chromatic arithmetic. This capability check is distinct from the 0.8.0
|
|
non-\texttt{Cmn} discriminant check and is replaced by structural registry
|
|
resolution in Push~4b. No payload bytes change and no
|
|
\texttt{PreconditionFailureReason} is appended; assignments 10 through 15
|
|
remain exactly as ratified.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.10.0, first half (genesis tranche G1,
|
|
retroactively recorded).} \texttt{CreateInstrument}
|
|
(Section~\ref{sec:k0:create-instrument}) landed at commit \texttt{3b09595}
|
|
without a version bump or a changelog paragraph, against this document's own
|
|
convention above --- an omission genesis tranche G2a repairs here rather than
|
|
silently. Adds one operation kind, \texttt{CreateInstrument}, mint-only
|
|
(set-union creation, no delete in this catalogue revision) on the score root,
|
|
carrying the full \texttt{Instrument} value. It is the single missing link
|
|
between an empty score (\texttt{Score::empty}) and a note: \texttt{CreateStaff}
|
|
already demands a live \texttt{Instrument}, and nothing else could mint one.
|
|
Schema major~2 unconditionally (\texttt{Instrument}'s major-2 appends are
|
|
mandatory fields, not \texttt{Option}-hidden).
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.10.0, second half (genesis tranche G2a).} Adds two
|
|
operation kinds, \texttt{SetCanvasLayoutDefaults}
|
|
(Section~\ref{sec:k0:set-canvas-layout-defaults}) and
|
|
\texttt{SetSpellingPrecedence} (Section~\ref{sec:k0:set-spelling-precedence}),
|
|
on exactly the \texttt{SetMetadata} advisory-LWW pattern
|
|
(Section~\ref{sec:k0:score-settings}): the canvas's default layout advisories
|
|
and the score's spelling-precedence configuration join the operation-authored
|
|
surfaces. Both are schema major~0 unconditionally --- neither carried type's
|
|
canonical encoding, taken as a standalone payload, has ever been versioned.
|
|
No accept-set change: the third genesis-ladder setter,
|
|
\texttt{SetTuningContext}, is schema major~3 and is deliberately deferred to
|
|
its own rung (G2b) rather than anticipated here.
|
|
|
|
The \emph{Value restoration} passage
|
|
(Section~\ref{sec:k0:undo}) and the \emph{Retired slots} closing note both
|
|
gain a repair alongside this addition: the former's LWW-family enumeration
|
|
now names both new setters, and the latter's ``outside the operation set''
|
|
clause is narrowed to the canvas object itself, per
|
|
\texttt{spec/RULING\_GENESIS\_PERSISTENCE.md} --- the score's \emph{contents}
|
|
are no longer outside the operation set; the canvas is still never
|
|
op-minted.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.11.0 (genesis tranche G2b,
|
|
\texttt{spec/CONTRACT\_GENESIS\_G2B\_TUNING.md}).} Adds one operation kind,
|
|
\texttt{SetTuningContext} (Section~\ref{sec:k0:set-tuning-context}), the
|
|
third and final genesis-ladder setter deferred at 0.10.0. Carries
|
|
\texttt{TuningContextSettings}, the authored subset of
|
|
\texttt{ScoreTuningContext} --- exactly its five wire-bearing fields, byte-
|
|
identical to the existing schema-major-3 wire walk (Binary Format companion
|
|
\sectionsc{Schema Major 3}) --- rather than the full graph type, so that
|
|
\texttt{accidental\_extensions} (staged off the wire) cannot diverge between
|
|
a live-authored session and the same document reloaded from bytes.
|
|
|
|
\textbf{The sole accept-set-raising surface among the nine genesis
|
|
settings/creates.} \texttt{SetTuningContext} is schema major~3
|
|
\emph{unconditionally} (\texttt{ScoreTuningContext}'s \texttt{smufl}/
|
|
\texttt{overrides} appends are mandatory, so no lower-major layout for this
|
|
payload exists at any value), which is why it alone --- not
|
|
\texttt{CreateInstrument} at major~2, and not either G2a setter at major~0 ---
|
|
drags the \texttt{OperationEnvelopeBlock} accept-set from \texttt{[0, 2]} to
|
|
\texttt{[0, 3]} (Binary Format companion \sectionsc{The Chunk-Level Gate}).
|
|
This is the reason the genesis ladder split \texttt{SetTuningContext} into
|
|
its own rung rather than landing it alongside \texttt{SetCanvasLayoutDefaults}
|
|
/ \texttt{SetSpellingPrecedence}: a one-way accept-set door is not something
|
|
to bury inside two unrelated major-0 setters.
|
|
|
|
Undo restores the \textbf{seeded base} settings --- default or non-default
|
|
alike --- exactly as \texttt{SetMetadata} does; the never-authored /
|
|
authored-to-default distinction stays unobservable
|
|
(Section~\ref{sec:k0:set-tuning-context}). This closes P13-S13: the
|
|
canonical operation log is now the sole canonical carrier of the tuning
|
|
context (the canonical base embeds no \texttt{Score} field value for any
|
|
setting, \texttt{metadata} included), on the same reasoning that already
|
|
applied to \texttt{SetMetadata}.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.12.0 (genesis tranche G3a,
|
|
\texttt{spec/CONTRACT\_GENESIS\_G3A\_ENTITIES.md}).} Adds four operation
|
|
kinds --- \texttt{CreateStaffGroup} (Section~\ref{sec:k0:create-staff-group}),
|
|
\texttt{CreatePartDefinition} (Section~\ref{sec:k0:create-part-definition}),
|
|
\texttt{CreateAnalysisLayer} (Section~\ref{sec:k0:create-analysis-layer}),
|
|
\texttt{CreateView} (Section~\ref{sec:k0:create-view}) --- completing the
|
|
root-level \texttt{Score} entity mints: every remaining vector a Chapter~5
|
|
top-level structure declares (\texttt{staff\_groups}, \texttt{parts},
|
|
\texttt{analysis\_layers}, \texttt{views}) is now operation-authored. All
|
|
four are mint-only (set-union creation, no delete in this catalogue
|
|
revision), schema major~0 unconditionally, epoch~11.
|
|
|
|
\textbf{The defect this closes, and what it does not close.} Until this
|
|
rung, all four object kinds became live \emph{only} through canonical-base
|
|
ingest; no operation minted any of them. Consequently \texttt{CreateStaff}'s
|
|
\texttt{group} precondition (Section~\ref{sec:k0:create-staff}) was
|
|
\textbf{unsatisfiable} under from-empty reduction --- a document built only
|
|
from operations could never author a grouped staff. G3a closes exactly this
|
|
satisfiability half. It does \textbf{not} make a bidirectionally consistent
|
|
staff group authorable: with mints only, and no modify or delete operation
|
|
for either side, no authoring order can bring \texttt{Staff.group} and
|
|
\texttt{StaffGroup.members} into agreement once they disagree.
|
|
|
|
\textbf{Ruled (disposition A, P13-S16; supersedes disposition B):
|
|
\texttt{Staff.group} is the sole authority for group membership, and
|
|
\texttt{StaffGroup.members} is a projection maintained from it by reduction.}
|
|
\texttt{CreateStaffGroup} \textbf{refuses} a non-empty carried \texttt{members}
|
|
(\texttt{ContainerNotEmpty}) --- the operation authors the group, not its
|
|
membership --- and \texttt{CreateStaff} carrying \texttt{group: Some(g)}
|
|
appends the new staff to \texttt{g}'s \texttt{members} in the graph. The two
|
|
\MUST{} agree in both directions, and graph invariant~21 (core specification
|
|
\sectionsc{Graph Invariants}) flags any disagreement between live objects.
|
|
Every consumer \MUST{} read group membership from \texttt{Staff.group}; core
|
|
specification Chapter~5's \texttt{Staff}/\texttt{StaffGroup} declarations
|
|
(\sectionsc{Top-Level Score Structure}) state this normatively, and
|
|
Section~\ref{sec:k0:create-staff} above states the corresponding
|
|
authoring-order consequence for \texttt{CreateStaff}.
|
|
|
|
\textbf{What disposition B ruled, and why it no longer holds.} Genesis tranche
|
|
G3a ratified disposition B: \texttt{members} was stored exactly as carried and
|
|
\textbf{neither maintained nor trusted}, and \textbf{both} stale forms were
|
|
permitted outcomes rather than defects --- a \textbf{missing} member
|
|
(\texttt{Staff.group} naming a group whose \texttt{members} omits that staff)
|
|
and a \textbf{spurious} member (\texttt{StaffGroup.members} naming a staff
|
|
whose own \texttt{Staff.group} is absent or names a different group). That
|
|
ruling was sound while the tranche minted only: with no modify or delete
|
|
operation for either side, no authoring order could bring the two into
|
|
agreement once they disagreed. Disposition A was recorded there as the later
|
|
maintenance/enforcement fix, sequenced after G3b; \textbf{P13-S16 is that
|
|
fix}, and neither stale form is authorable any more.
|
|
|
|
\textbf{Referential preconditions, graph-aware only, mirroring
|
|
\texttt{CreateStaff} exactly.} \texttt{CreatePartDefinition.staves}
|
|
preconditions every named id resolves to a live \texttt{Staff};
|
|
\texttt{CreateView.active\_layers}
|
|
preconditions every named id resolves to a live analysis layer;
|
|
\texttt{CreateAnalysisLayer} carries no outbound reference and needs no
|
|
referential precondition at all, the \texttt{CreateInstrument} shape rather
|
|
than the \texttt{CreateStaff} shape. Base-free reduction enforces none of
|
|
these, exactly as for \texttt{CreateStaff}: there is no universe to check
|
|
against. No new \texttt{PreconditionFailureReason} --- every referential
|
|
refusal reuses \texttt{TargetMissing} (discriminant 0).
|
|
|
|
\textbf{\texttt{CreateStaffGroup} is deliberately not in that list (P13-S16).}
|
|
Its \texttt{members} check is an \textbf{empty-container} precondition on the
|
|
carried value, not a referential one, and the distinction is normative: a
|
|
graph-aware precondition asks about the \emph{universe} (``is this id live?'')
|
|
and therefore cannot run base-free, whereas an empty-container precondition asks
|
|
only about the \emph{carried value} (``is \texttt{members} empty?'') and
|
|
therefore \MUST{} be enforced everywhere, base-free included. It refuses with
|
|
\texttt{ContainerNotEmpty}, and the sentence above about base-free reduction
|
|
enforcing none of these does \textbf{not} extend to it.
|
|
|
|
No accept-set change: all four carried types have exactly one wire layout
|
|
(core specification's \sectionsc{Binary Format Companion} confirms no
|
|
versioned walk exists for any of the four), so none gains a
|
|
\texttt{schema\_major()} arm beyond the existing catch-all.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.13.0 (genesis tranche G3b,
|
|
\texttt{spec/CONTRACT\_GENESIS\_G3B\_MEASURE.md}), the final rung of the
|
|
genesis operation tranche (\texttt{spec/PLAN\_GENESIS\_OPS.md}).} Adds one
|
|
operation kind, \texttt{CreateMeasure} (Section~\ref{sec:k0:create-measure}):
|
|
\texttt{StaffInstance.measures} joins the operation-authored surfaces, on the
|
|
\texttt{CreateStaffInstance} parent-carrying mint pattern rather than the
|
|
bare-value shape the four G3a families above use --- \texttt{Measure} is a
|
|
nested container child, not a \texttt{Score}-root vector, and carries no
|
|
back-pointer to its parent. Schema major~0 unconditionally, epoch~12.
|
|
|
|
Also adds graph invariant 20 (core specification \sectionsc{Graph
|
|
Invariants}) --- measure/meter agreement and boundary consistency --- and
|
|
three \texttt{PreconditionFailureReason} appends, all epoch~12:
|
|
\texttt{MeasureMeterMismatch} (16), \texttt{MeasureOutOfOrder} (17), and
|
|
\texttt{MeasureOrderUnverifiable} (18). \texttt{CreateMeasure} itself refuses
|
|
whenever the comparison or delta invariant 20 needs is not computable
|
|
(\texttt{MeasureOrderUnverifiable}); invariant 20 instead \emph{abstains} ---
|
|
emits no violation --- over the same incomputable cases, because base-ingested
|
|
data may predate the rule. This is a deliberate split, not an inconsistency:
|
|
fail closed at the operation, abstain at the invariant.
|
|
|
|
\textbf{Two existing operations now preserve invariant 20.} \texttt{SetMetricGrid}
|
|
(Section~\ref{sec:k0:meter-tempo}) and \texttt{SetTimeSignature}
|
|
(Section~\ref{sec:k0:meter-tempo}) both gain prospective preconditions,
|
|
covering agreement and boundary consistency, on their forward paths and on
|
|
both undo restoration policies (\texttt{StrictInverse}/\texttt{Cascade}
|
|
conflict on an unsafe restoration set; \texttt{BestEffort} applies the
|
|
maximal safe subset under a documented canonical-order greedy). Every check
|
|
runs before any mint, so a refused write leaves no residue in \texttt{objects},
|
|
any carried-value map, or the graph.
|
|
|
|
No accept-set change: \texttt{Measure} has never been versioned as a
|
|
standalone value --- its only non-scalar field, \texttt{TimeAnchor}, has a
|
|
hand-written codec with no version branching of its own --- so
|
|
\texttt{OperationEnvelopeBlock} stays at \texttt{3} where genesis tranche
|
|
G2b left it. This closes the genesis ladder
|
|
(\texttt{spec/PLAN\_GENESIS\_OPS.md} \S4): G1 $\rightarrow$ G2a $\rightarrow$
|
|
G-minor $\rightarrow$ G2b $\rightarrow$ G3a $\rightarrow$ G3b.
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.14.0 (P13-S19, correction and observation,
|
|
\texttt{spec/CONTRACT\_P13S19\_PARTIAL.md}).} No payload byte changes, no
|
|
behaviour change: \texttt{create\_measure} and graph invariant 20 are
|
|
byte-identical to 0.13.0. Corrects this section's ordering and
|
|
boundary-distance description above, which read as though a pickup/anacrusis
|
|
first measure --- and everything downstream of it --- were simply exempt. A
|
|
first measure skips only the \emph{predecessor-dependent} clauses (ordering
|
|
and boundary distance) for lack of a predecessor, and the agreement clause
|
|
only when it declares \texttt{None} or a signature that agrees with the
|
|
governing grid; a disagreeing declared signature is refused
|
|
(\texttt{MeasureMeterMismatch}) even on a first measure, since agreement is
|
|
not predecessor-dependent. Independently of what the pickup itself declares,
|
|
its \textbf{successor} is measured against the governing signature's full
|
|
\texttt{measure\_duration()} regardless, and is refused
|
|
(\texttt{MeasureMeterMismatch}) and flagged by invariant 20 whenever the
|
|
pickup's actual length is shorter than a full bar --- which, for an authored
|
|
pickup, it always is. The same gap applies to any partial measure at any
|
|
position, not only a first one: a mid-score partial measure is itself
|
|
unexamined at creation (nothing checks its own length), while \emph{its}
|
|
successor is refused the identical way. Closing this needs a per-measure
|
|
duration concept this rung does not introduce
|
|
(\texttt{spec/PASS13\_CANDIDATES.md}, P13-S19, still open).
|
|
|
|
\medskip
|
|
|
|
\noindent\textbf{Version 0.15.0 (P13-S16, the maintained projection,
|
|
\texttt{spec/CONTRACT\_P13S16\_PROJECTION.md}).} No payload byte changes ---
|
|
\texttt{CreateStaffGroupOp} and \texttt{CreateStaffOp} encode exactly as in
|
|
0.12.0 --- but a \textbf{behaviour change on two operations}, replacing genesis
|
|
tranche G3a's ratified \textbf{disposition~B} with \textbf{disposition~A}.
|
|
\texttt{StaffGroup.members} stops being a non-authoritative field stored as
|
|
carried and becomes a projection \emph{maintained} from \texttt{Staff.group}:
|
|
|
|
\begin{itemize}[leftmargin=1.2em]
|
|
\item \texttt{CreateStaffGroup} (Section~\ref{sec:k0:create-staff-group})
|
|
now \textbf{refuses} a non-empty carried \texttt{members} with
|
|
\texttt{ContainerNotEmpty} (discriminant~10, no new
|
|
\texttt{PreconditionFailureReason}). This \textbf{replaces} the
|
|
graph-aware precondition that every id in \texttt{members} resolve to a
|
|
live \texttt{Staff} (\texttt{TargetMissing}). The new check is an
|
|
\emph{empty-container} precondition on the carried value, so unlike the
|
|
check it replaces it is \textbf{not graph-gated and is enforced base-free}
|
|
--- the one place where the sibling mints' ``referential preconditions are
|
|
graph-aware only'' rule does not extend.
|
|
\item \texttt{CreateStaff} (Section~\ref{sec:k0:create-staff}) carrying
|
|
\texttt{group: Some(g)} now appends the minted staff to \texttt{g}'s
|
|
\texttt{members} in the graph, idempotently per staff id. Undo of a staff
|
|
strips the id back out.
|
|
\end{itemize}
|
|
|
|
\noindent Both formerly \textbf{permitted} stale forms --- the missing member
|
|
and the spurious member --- are therefore \textbf{unauthorable}, and the core
|
|
specification gains graph invariant~21
|
|
(\texttt{StaffGroupMembershipAgreement}) requiring the two to agree in both
|
|
directions between live objects, abstaining on dangling membership because an
|
|
undeclared member is invariant~10's concern.
|
|
|
|
\textbf{This breaks documents authored under 0.12.0--0.14.0 only in what they
|
|
may newly assert}, not in what they may read: an existing blob carrying a
|
|
disagreeing pair still decodes, and no stored bytes are reinterpreted.
|
|
|
|
\textbf{A canonical base materialized before this rung \MUST{} be rebuilt rather
|
|
than reused}, and the two operations oblige that for \emph{different} reasons,
|
|
either of which alone would suffice:
|
|
|
|
\begin{itemize}[leftmargin=1.2em]
|
|
\item \texttt{CreateStaffGroup} changes its \textbf{reduction verdict} --- a
|
|
non-empty carried \texttt{members} now reduces to a no-op where it
|
|
previously applied, so the recorded effect differs.
|
|
\item \texttt{CreateStaff} changes \textbf{canonical reduced state} --- its
|
|
verdict is unchanged (it still applies), but the graph the reduction
|
|
produces now carries the maintained \texttt{members}.
|
|
\end{itemize}
|
|
|
|
\noindent Accordingly
|
|
\texttt{epiphany\_ops::CURRENT\_REDUCTION\_ALGORITHM\_VERSION} moves
|
|
\texttt{0}~$\rightarrow$~\texttt{1}, and P13-S27's authority check refuses a
|
|
base declaring the older version. Core specification \sectionsc{Canonical
|
|
Document Identity} requires the bump for either class of change.
|
|
|
|
% ===========================================================================
|
|
\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 (frozen; replay only)}
|
|
\label{sec:k0:transpose}
|
|
|
|
\begin{requirement}
|
|
\label{req:opcat:transpose-frozen}
|
|
\texttt{Transpose} is \textbf{frozen}. Its reduction rule is fixed at the
|
|
semantics described in this section, including the saturation and the
|
|
duplicate-sensitivity, for as long as any stored operation carries it. A
|
|
conforming implementation \MUST{} reduce it exactly as specified here and
|
|
\MUSTNOT{} emit it from new authoring; new transpositions are authored as
|
|
\texttt{TransposeInterval} (Section~\ref{sec:k0:transpose-interval}).
|
|
\end{requirement}
|
|
|
|
\textbf{Payload schema.} \texttt{TransposeOp \{ targets: Vec<PitchId>,
|
|
chromatic\_steps: i32 \}}. Pitch identifiers are preserved. The operation
|
|
rewrites \emph{scale position} (the \texttt{Cmn} alteration), not acoustic
|
|
content.
|
|
|
|
\textbf{Canonical encoding.} \texttt{targets} in ascending canonical-byte order,
|
|
then \texttt{chromatic\_steps} as a little-endian \texttt{i32}. The sequence is
|
|
\emph{sorted but not deduplicated}: it is a multiset on the wire.
|
|
|
|
\textbf{Reduction rule.} An order-dependent content overwrite. For each live,
|
|
non-system target \emph{occurrence} in \texttt{targets}, the target's \texttt{Cmn}
|
|
\texttt{alteration} is shifted by \texttt{chromatic\_steps} and clamped to the
|
|
\texttt{i8} bound. Consequences, all normative for replay:
|
|
|
|
\begin{itemize}
|
|
\item A target appearing $k$ times is shifted $k$ times.
|
|
\item The nominal and octave never change: transposing C4 by $+12$ yields C4
|
|
with \texttt{alteration} $= 12$, not C5.
|
|
\item A shift past the \texttt{i8} bound saturates silently, and the operation
|
|
still reports \texttt{Applied}. Transposition under this rule is therefore
|
|
not invertible.
|
|
\item A target whose position is not \texttt{Cmn} is left unchanged, and the
|
|
operation still reports \texttt{Applied}.
|
|
\end{itemize}
|
|
|
|
\begin{rationale}
|
|
Every bullet above is a defect (P12-K2), and none of them may be repaired in
|
|
place. An operation is history: a replica replaying a stored
|
|
\texttt{Transpose} must reconstruct the state its author saw, and a
|
|
``corrected'' reduction rule would silently rewrite every score that ever
|
|
used one. The defects are therefore \emph{pinned}, not fixed, and the repair
|
|
ships as a new operation kind whose discriminant no historical operation
|
|
carries. Ratified Push~4a; supersedes the Pass~12 pin, which anticipated a
|
|
payload schema-major and a dependency on the tuning catalog. Neither proved
|
|
necessary: transposition acts on scale position, and appending an operation
|
|
kind is a schema \emph{minor} (Binary Format companion, requirement
|
|
\texttt{req:binfmt:kind-discriminants}).
|
|
\end{rationale}
|
|
|
|
\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, and it records no write into
|
|
the pitch's value chain, so \emph{value-restoring undo does not restore it
|
|
either}: undoing a transaction containing a \texttt{Transpose} leaves the shifted
|
|
pitch shifted. An inverse-interval undo does not exist (under saturation the
|
|
inverse is not a function) and remains a deferred refinement (P11-C8).
|
|
|
|
\textbf{This too is frozen.} Making \texttt{Transpose} record into the value
|
|
chain would not change its own reduction rule, but it \emph{would} change what a
|
|
stored history $\{\texttt{Transpose}, \texttt{UndoTransaction}\}$ replays to ---
|
|
from "the pitch stays shifted" to "the pitch returns" --- which is a change in
|
|
what an existing document means. \texttt{TransposeInterval} records its write and
|
|
\emph{is} undoable (Section~\ref{sec:k0:transpose-interval}); the frozen
|
|
operation is permanently not. That asymmetry is another reason never to author
|
|
it.
|
|
|
|
\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{TransposeInterval}
|
|
\label{sec:k0:transpose-interval}
|
|
|
|
\textbf{Payload schema.} \texttt{TransposeIntervalOp \{ targets:
|
|
CanonicalSet<PitchId>, interval: TranspositionInterval \}}, reusing the
|
|
diatonic/chromatic pair the core specification defines in Chapter~2,
|
|
\sectionsc{Transposition and the Interval Type} --- the same value an
|
|
\texttt{Instrument} carries as its written-versus-sounding interval. Pitch
|
|
identifiers are preserved; the operation rewrites scale position and leaves
|
|
acoustic realization untouched.
|
|
|
|
\begin{requirement}
|
|
\label{req:opcat:transpose-interval-targets}
|
|
\texttt{targets} is a \textbf{set}. It \MUST{} be encoded as a sequence in
|
|
ascending canonical-byte order with \emph{strictly increasing} elements; a
|
|
decoder \MUST{} reject a sequence containing a duplicate rather than
|
|
normalize it. A transposition is a function of \emph{which} pitches it names,
|
|
never of how many times it names them.
|
|
\end{requirement}
|
|
|
|
\textbf{Canonical encoding.} The strictly-increasing \texttt{targets} sequence,
|
|
then \texttt{interval.diatonic\_steps} and \texttt{interval.chromatic\_steps},
|
|
each a little-endian \texttt{i32}.
|
|
|
|
\textbf{Reduction rule.} An order-dependent content overwrite. Tombstoned and
|
|
\texttt{SYSTEM\_DERIVED} targets are skipped, exactly as for \texttt{Transpose};
|
|
if no mutable target remains the operation reduces as the corresponding
|
|
precondition no-op. Otherwise, every remaining target \MUST{} be transposable
|
|
under core specification requirement \texttt{req:pitch:transposition}, and each
|
|
is transposed by \texttt{interval}.
|
|
|
|
\begin{requirement}
|
|
\label{req:opcat:transpose-interval-atomic}
|
|
If any mutable target is \emph{not} transposable, the operation \MUST{}
|
|
reduce to a no-op that changes no pitch, reporting the precondition failure
|
|
of the first such target in canonical order. It \MUSTNOT{} transpose the
|
|
remaining targets. The four cases and their
|
|
\texttt{PreconditionFailureReason} discriminants:
|
|
\begin{itemize}
|
|
\item a non-\texttt{Cmn} \texttt{scale\_position.position} $\Rightarrow$
|
|
\texttt{PitchSpaceMismatch} (6);
|
|
\item a \texttt{Cmn} position whose enclosing chromatic structure or
|
|
nominal mapping cannot be established $\Rightarrow$
|
|
\texttt{PitchSpaceMismatch} (6);
|
|
\item an \texttt{AcousticRealization::AbsoluteHz} realization
|
|
$\Rightarrow$ \texttt{AcousticRealizationPinned} (14);
|
|
\item an \texttt{alteration}$'$ or \texttt{octave}$'$ that does not fit
|
|
its field $\Rightarrow$ \texttt{TranspositionOutOfRange} (15).
|
|
\end{itemize}
|
|
\end{requirement}
|
|
|
|
\begin{requirement}
|
|
\label{req:opcat:transpose-interval-spelling}
|
|
A \texttt{TransposeInterval} \MUST{} record the spelling its interval
|
|
determined as a \texttt{SpellingAttachment} with source
|
|
\texttt{SpellingSource::Propagated}, per the core specification's Chapter~2,
|
|
\sectionsc{Spelling Sources}. The attachment's \texttt{from} is the
|
|
transposed pitch's own identifier, which the operation preserves.
|
|
|
|
That attachment alone is \emph{not sufficient}, because the default
|
|
precedence ranks \texttt{UserChosen} and \texttt{Imported} above
|
|
\texttt{Propagated} (Chapter~2, \sectionsc{Configurable Precedence}). A
|
|
\texttt{TransposeInterval} \MUST{} therefore also \textbf{move} every
|
|
engraved-layer, pitch-scoped, explicit spelling attachment on each target
|
|
that is not itself \texttt{Propagated}, preserving each attachment's
|
|
\texttt{source}, \texttt{priority}, and \texttt{layer}. A spelling is moved
|
|
by transposing its \emph{nominal} diatonically and taking whatever accidental
|
|
the transposed pitch then requires at that staff position. If any such
|
|
attachment cannot be written at the transposed position, the operation
|
|
\MUST{} refuse, atomically, with \texttt{TranspositionOutOfRange}.
|
|
\end{requirement}
|
|
|
|
\begin{rationale}
|
|
Two different failures hide here, and the propagated attachment addresses only
|
|
the first.
|
|
|
|
For a pitch with \emph{no} authored spelling, the pre-pass would re-infer, and
|
|
may pick the enharmonic the interval did not choose. The propagated attachment
|
|
pins the interval's determination.
|
|
|
|
For a pitch \emph{with} an authored spelling, the propagated attachment is
|
|
outranked and changes nothing: a C4 the author spelled ``C'', sharpened to
|
|
C-sharp~4, would still resolve to \texttt{Authored(UserChosen)} and engrave a
|
|
C natural --- the accidental simply disappears, and the notehead names a pitch
|
|
that is not there. So the authored spelling is moved instead of being left or
|
|
discarded. It is moved by its \textbf{nominal}, because the nominal is what
|
|
carries the author's enharmonic decision: an author who wrote B-sharp~3 rather
|
|
than C4 chose the letter B, and a perfect fifth up must give F-double-sharp~4,
|
|
not G. Discarding the attachment would silently lose that decision; re-inferring
|
|
it from the transposed pitch would give G.
|
|
|
|
A transposed \texttt{UserChosen} spelling is still the user's choice, so its
|
|
source is preserved. \texttt{Imported} likewise: an imported attachment asserts
|
|
``this pitch is written thus'', and once the pitch moves that assertion must
|
|
move with it or become false. Import fidelity is a property of the source file,
|
|
which a transposition does not touch.
|
|
\end{rationale}
|
|
|
|
\textbf{Conflict cases.} None --- composition is deterministic in canonical order.
|
|
|
|
\textbf{Undo semantics.} Nothing is minted. \texttt{TransposeInterval}
|
|
\MUST{} record each transposed pitch's new value into that pitch's value chain,
|
|
and that pitch's resulting \emph{engraved spelling set} into the spelling-set
|
|
chain, so that value-restoring undo recovers the pre-transpose pitch \emph{and}
|
|
its pre-transpose spelling. Restoring the pitch alone would leave a notehead
|
|
spelled for a pitch that no longer exists. This is where
|
|
\texttt{TransposeInterval} departs from the frozen \texttt{Transpose}, which
|
|
records nothing and is therefore not undoable.
|
|
|
|
\begin{requirement}
|
|
\label{req:opcat:spelling-set-chain}
|
|
The pitch's engraved spelling set is a single undo key with \emph{more than
|
|
one writer}. Every operation that changes it --- \texttt{RespellPitch} and
|
|
\texttt{TransposeInterval} alike --- \MUST{} record a write on that key.
|
|
Consequently a \texttt{RespellPitch} causally prior to a transposed
|
|
transaction is that transaction's chain-predecessor and is restored by its
|
|
undo; and a \texttt{RespellPitch} canonically \emph{later} supersedes the
|
|
transaction's write, so a \texttt{StrictInverse} undo conflicts rather than
|
|
erasing it, per the general superseded-writer rule.
|
|
|
|
A pitch's value and its engraved spelling set \MUST{} undo as one unit: if
|
|
either is superseded, neither is restored. A \texttt{BestEffort} undo
|
|
\MUSTNOT{} restore a pitch's earlier value while leaving a spelling authored
|
|
against the value it has since taken.
|
|
|
|
This unit is keyed on the \emph{pitch}, and on which keys the
|
|
\emph{transaction} wrote --- not on which operation wrote them, and not on
|
|
\texttt{TransposeInterval} in particular. A transaction whose members write
|
|
the two halves separately is coupled the same way: an editor's ``move note''
|
|
is a \texttt{ModifyIdentifiedPitch} (the value) together with a
|
|
\texttt{RespellPitch} (the spelling set), and a later respell makes a
|
|
\texttt{BestEffort} undo skip both. That breadth is intended. A transaction
|
|
that wrote only one of the two keys is unaffected, since an unwritten key
|
|
yields no supersession.
|
|
\end{requirement}
|
|
|
|
\begin{rationale}
|
|
Ratified as P13-S3. An implementation may keep the spelling-set chain
|
|
physically separate from whatever chain drives \texttt{RespellPitch}'s
|
|
last-writer-wins conflict detection --- the reference implementation does,
|
|
because folding transposes into that chain would make a concurrent respell
|
|
\emph{conflict} with a transpose and would move the canonical bytes of every
|
|
existing history. What it may not do is let one writer own the key. A chain
|
|
with a single writer cannot see the other's prior value (so undo erases it) and
|
|
cannot see the other's later value (so undo overwrites it).
|
|
\end{rationale}
|
|
|
|
An inverse interval usually exists ($(-d, -c)$), because the reduction never
|
|
saturates --- but not always: $\texttt{i32::MIN}$ has no negation. Undo does not
|
|
rely on it.
|
|
|
|
\textbf{Re-anchoring.} As \texttt{Transpose}.
|
|
|
|
\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{Membership maintenance (P13-S16, disposition A; supersedes genesis
|
|
tranche G3a's disposition B).} \texttt{Staff.group} is the \textbf{sole
|
|
authority} for group membership, and \texttt{StaffGroup.members}
|
|
(Section~\ref{sec:k0:create-staff-group}) is a projection \textbf{maintained
|
|
from it} under graph-aware reduction. \texttt{CreateStaff} carrying
|
|
\texttt{group: Some(g)} therefore appends the newly minted staff to \texttt{g}'s
|
|
\texttt{members} in the graph. The append is set-union and idempotent per staff
|
|
id --- convergence replays operations, so appending an id already present
|
|
\MUSTNOT{} duplicate it --- and base-free reduction has no graph to maintain and
|
|
writes nothing. The two \MUST{} agree in both directions, and graph
|
|
invariant~21 (core specification \sectionsc{Graph Invariants}) flags any
|
|
disagreement between live objects.
|
|
|
|
\textbf{What this replaced.} Under disposition B, \texttt{CreateStaff} authored
|
|
a \textbf{permitted} \textbf{missing-member} stale form: a
|
|
\texttt{CreateStaffGroup(g, members: [])} followed by a
|
|
\texttt{CreateStaff(s, group: Some(g))} left \texttt{s.group == Some(g)} while
|
|
\texttt{g.members} omitted \texttt{s}, because that tranche minted only and no
|
|
operation maintained the projection. \textbf{That outcome is no longer
|
|
reachable}: the identical sequence now yields agreement. The mirror-image
|
|
\textbf{spurious} form is likewise unauthorable --- \texttt{CreateStaffGroup}
|
|
refuses a non-empty carried \texttt{members} outright; see
|
|
Section~\ref{sec:k0:create-staff-group}.
|
|
|
|
\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{Undo also strips the removed staff's id from every live group's
|
|
\texttt{members} (P13-S16)}: the projection is maintained from
|
|
\texttt{Staff.group}, so a staff leaving the graph \MUST{} leave the projection
|
|
with it. Without that strip the undo would leave a group naming a staff that no
|
|
longer exists. Note this is the \emph{unguarded} direction of the pair --- undo
|
|
of a \texttt{CreateStaffGroup} is refused while a live staff still names the
|
|
group (Section~\ref{sec:k0:create-staff-group}), but nothing refuses undoing the
|
|
staff itself.
|
|
|
|
\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{CreateInstrument}
|
|
\label{sec:k0:create-instrument}
|
|
|
|
Ratified with the genesis operation tranche's first rung (G1;
|
|
\texttt{spec/CONTRACT\_GENESIS\_G1\_INSTRUMENT.md}, executing
|
|
\texttt{spec/RULING\_GENESIS\_PERSISTENCE.md}). \texttt{CreateStaff}
|
|
(Section~\ref{sec:k0:create-staff}) already requires a live
|
|
\texttt{Instrument}, and until this primitive existed nothing could mint one
|
|
except a canonical base --- so a document created empty
|
|
(\texttt{Score::empty}) and given only operations could reach a
|
|
\texttt{CreateStaff} but never satisfy it. \texttt{CreateInstrument} is the
|
|
single missing link between an empty score and a note: with it, the chain
|
|
\texttt{CreateInstrument} $\rightarrow$ \texttt{CreateStaff} $\rightarrow$
|
|
\texttt{CreateRegion} $\rightarrow$ \texttt{CreateStaffInstance}
|
|
$\rightarrow$ \texttt{CreateVoice} $\rightarrow$ \texttt{InsertEvent}
|
|
materializes a note-bearing score from operations alone.
|
|
|
|
\textbf{Payload schema.} \texttt{CreateInstrumentOp \{ instrument: Instrument
|
|
\}} --- the full abstract-instrument value (schema major 2): identity, name,
|
|
declared pitch range, abbreviation, sound configuration, transposition
|
|
interval, default clef, default staff-line configuration, and unpitched
|
|
members. Unlike every carried type in
|
|
Section~\ref{sec:k0:structural-containers} and
|
|
Section~\ref{sec:k0:create-staff}, \texttt{Instrument} holds no outbound
|
|
entity reference, so this primitive needs no referential precondition at
|
|
all --- only mint and idempotence.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{instrument}. \texttt{Instrument}'s schema-major-2 appends
|
|
(\texttt{sound\_config}, \texttt{default\_clef},
|
|
\texttt{default\_staff\_lines}, and the rest) are mandatory fields, not
|
|
\texttt{Option}-hidden, so no lower-major layout for this payload exists:
|
|
under minimal stamping (Binary Format companion \sectionsc{Schema Major 2})
|
|
a block carrying a \texttt{CreateInstrument} is \emph{born at v2}, exactly
|
|
as \texttt{CreateStaff} is --- not the value-dependent shape
|
|
\texttt{CreateRegion}/\texttt{SetStaffLayout} use.
|
|
|
|
\textbf{Reduction rule.} Set-union creation of an \texttt{Instrument} on the
|
|
score root, mirroring \texttt{CreateStaff}'s discipline exactly since
|
|
neither carried type references another entity: a create mints the
|
|
instrument live if its id is fresh; a repeat create carrying a
|
|
byte-identical value reduces idempotently
|
|
(\texttt{NoOpReason::AlreadyApplied}); a create whose id is already live
|
|
with a \emph{differing} value is a precondition no-op with
|
|
\texttt{RecreateContentMismatch}; and a create naming a tombstoned id is a
|
|
precondition no-op with \texttt{TargetTombstoned}. There is no
|
|
graph-aware reference-resolution block, because there is nothing for one to
|
|
check.
|
|
|
|
\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 instrument;
|
|
\texttt{StrictInverse} conflicts if a live staff references it (tombstoning
|
|
it would strand the staff).
|
|
|
|
\textbf{Re-anchoring.} Not applicable, for the same reason as
|
|
\texttt{CreateStaff}: an instrument mint references no tombstonable anchor.
|
|
There is no \texttt{DeleteInstrument} in this catalogue revision ---
|
|
\texttt{CreateStaff} ships today with no \texttt{DeleteStaff} either, and
|
|
full delete/modify coverage of the genesis-authored fields is later
|
|
tranche work (\texttt{spec/PLAN\_GENESIS\_OPS.md} G3).
|
|
|
|
\section{SetCanvasLayoutDefaults}
|
|
\label{sec:k0:set-canvas-layout-defaults}
|
|
|
|
Ratified with the genesis operation tranche's G2a rung (\texttt{spec/CONTRACT\_
|
|
GENESIS\_G2A\_SETTINGS.md}, executing \texttt{spec/RULING\_GENESIS\_
|
|
PERSISTENCE.md}): the canvas's default layout advisories
|
|
(\texttt{Canvas.layout\_defaults}) join the operation-authored surfaces, on
|
|
exactly the \texttt{SetMetadata} pattern (Section~\ref{sec:k0:score-settings}).
|
|
|
|
\textbf{Payload schema.} \texttt{SetCanvasLayoutDefaultsOp \{ layout\_defaults:
|
|
CanvasLayoutDefaults \}} --- the full page-size-and-margins value.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{layout\_defaults}. \texttt{CanvasLayoutDefaults} carries no
|
|
schema-major-1-or-higher appends of its own --- the versioning that labels the
|
|
type ``schema major 1'' lives in the \emph{containing} \texttt{Canvas} walk,
|
|
not in this leaf --- so, as a standalone payload, it has exactly one layout
|
|
and this operation is schema major~0 unconditionally.
|
|
|
|
\textbf{Reduction rule.} An advisory last-writer-wins field overwrite,
|
|
identical in discipline to \texttt{SetMetadata}: the latest write in canonical
|
|
order silently wins and the operation always applies --- no working state, no
|
|
conflict, and no idempotence short-circuit (a re-write of an identical value
|
|
is a legitimate new write, not a no-op). Graph-aware reduction overwrites
|
|
\texttt{Canvas.layout\_defaults}.
|
|
|
|
\textbf{Conflict cases.} None (advisory LWW).
|
|
|
|
\textbf{Undo semantics.} A value-restoring field overwrite
|
|
(Section~\ref{sec:k0:undo}): the write chain is seeded from the base value at
|
|
ingest, so undoing the first operational write restores the pre-operational
|
|
state rather than absence.
|
|
|
|
\textbf{Re-anchoring.} Not applicable: the field is a score singleton with no
|
|
tombstonable anchor.
|
|
|
|
\section{SetSpellingPrecedence}
|
|
\label{sec:k0:set-spelling-precedence}
|
|
|
|
Ratified with the genesis operation tranche's G2a rung, alongside
|
|
\texttt{SetCanvasLayoutDefaults} above: the score's spelling-precedence
|
|
configuration (\texttt{Score.spelling\_precedence}) joins the
|
|
operation-authored surfaces, on the same \texttt{SetMetadata} pattern.
|
|
|
|
\textbf{Payload schema.} \texttt{SetSpellingPrecedenceOp \{ precedence:
|
|
SpellingPrecedence \}} --- the full total-ordering value over the five
|
|
spelling-source kinds.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{precedence}. \texttt{SpellingPrecedence} has never been versioned ---
|
|
every codec walk that reads it, frozen and live alike, reads it through the
|
|
plain unversioned codec --- so this operation is schema major~0
|
|
unconditionally, exactly as \texttt{SetCanvasLayoutDefaults} is.
|
|
|
|
\textbf{Reduction rule.} An advisory last-writer-wins field overwrite,
|
|
identical in discipline to \texttt{SetMetadata} and
|
|
\texttt{SetCanvasLayoutDefaults}: no working state, no conflict, no
|
|
idempotence short-circuit. Graph-aware reduction overwrites
|
|
\texttt{Score.spelling\_precedence}.
|
|
|
|
\textbf{Conflict cases.} None (advisory LWW).
|
|
|
|
\textbf{Undo semantics.} A value-restoring field overwrite
|
|
(Section~\ref{sec:k0:undo}): the write chain is seeded from the base value at
|
|
ingest, so undoing the first operational write restores the pre-operational
|
|
state rather than absence.
|
|
|
|
\textbf{Re-anchoring.} Not applicable: the field is a score singleton with no
|
|
tombstonable anchor.
|
|
|
|
\section{SetTuningContext}
|
|
\label{sec:k0:set-tuning-context}
|
|
|
|
Ratified with the genesis operation tranche's G2b rung (\texttt{spec/
|
|
CONTRACT\_GENESIS\_G2B\_TUNING.md}, executing \texttt{spec/
|
|
RULING\_GENESIS\_PERSISTENCE.md}): the score's tuning context settings
|
|
(\texttt{Score.tuning\_context}) join the operation-authored surfaces, on
|
|
the same \texttt{SetMetadata} pattern as \texttt{SetCanvasLayoutDefaults}
|
|
and \texttt{SetSpellingPrecedence} above. Unlike either sibling,
|
|
\texttt{SetTuningContext} is the \textbf{sole genesis payload born at
|
|
schema major~3} and is the surface that raises the
|
|
\texttt{OperationEnvelopeBlock} accept-set from \texttt{[0, 2]} to
|
|
\texttt{[0, 3]} (Binary Format companion \sectionsc{The Chunk-Level Gate}).
|
|
|
|
\textbf{Payload schema.} \texttt{SetTuningContextOp \{ settings:
|
|
TuningContextSettings \}}. \texttt{TuningContextSettings} is the
|
|
\textbf{authored subset} of \texttt{ScoreTuningContext}: exactly its five
|
|
wire-bearing fields (\texttt{default\_pitch\_space},
|
|
\texttt{default\_tuning\_system}, \texttt{reference}, \texttt{smufl},
|
|
\texttt{overrides}), in the codec's existing order --- not the full
|
|
six-field graph type. \texttt{accidental\_extensions} is deliberately
|
|
\textbf{not} a field of the carried payload: it is staged out of schema
|
|
major~3 (Binary Format companion \sectionsc{Schema Major 3}) and
|
|
\texttt{OperationSet::accept} stores the authored envelope as a
|
|
\emph{value}, so a payload carrying the full \texttt{ScoreTuningContext}
|
|
would let \texttt{accidental\_extensions} reach the graph on the authoring
|
|
replica while decoding to empty on every replica that received the
|
|
document through serialization --- the same document in two graph states,
|
|
depending only on whether it was just authored or just reloaded. The
|
|
subset type makes this divergence unrepresentable: a field the payload
|
|
does not carry cannot be set inconsistently.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{settings}. \texttt{TuningContextSettings}'s encoding is
|
|
\textbf{byte-identical} to \texttt{ScoreTuningContext}'s existing
|
|
five-field wire walk --- a type-level narrowing, not a new wire form. Since
|
|
\texttt{ScoreTuningContext}'s \texttt{smufl} and \texttt{overrides} appends
|
|
are mandatory (not \texttt{Option}-hidden), no lower-major layout for this
|
|
payload exists at any value: \texttt{SetTuningContext} is \textbf{born at
|
|
schema major~3 unconditionally}, the same shape as \texttt{CreateInstrument}'s
|
|
unconditional birth at major~2 (Section~\ref{sec:k0:create-instrument}), not
|
|
the value-dependent shape \texttt{CreateRegion}/\texttt{SetStaffLayout} use.
|
|
|
|
\textbf{Reduction rule.} An advisory last-writer-wins field overwrite,
|
|
identical in discipline to \texttt{SetMetadata}: no working state, no
|
|
conflict, and no idempotence short-circuit. Graph-aware reduction writes
|
|
exactly the five subset fields onto \texttt{Score.tuning\_context} and
|
|
\textbf{leaves \texttt{accidental\_extensions} untouched} --- preserving
|
|
whatever the graph already held, since the operation carries no
|
|
information about that field and normalizing it away (clearing it at
|
|
construction, or rejecting a populated in-memory value) would either make
|
|
correctness depend on a clearing discipline the compiler cannot see, or
|
|
turn an in-memory-only field into an authoring error for callers who never
|
|
opted into its persistence.
|
|
|
|
\textbf{Conflict cases.} None (advisory LWW).
|
|
|
|
\textbf{Undo semantics.} A value-restoring field overwrite
|
|
(Section~\ref{sec:k0:undo}), with the chain's value type the \textbf{subset}
|
|
\texttt{TuningContextSettings}, not \texttt{ScoreTuningContext}: the write
|
|
chain is seeded from the base's five wire-bearing fields at ingest, so
|
|
undoing the first operational write restores the pre-operational settings
|
|
rather than absence, identically whether the base was seeded with the type
|
|
default or a genuine non-default value --- the never-authored /
|
|
authored-to-default distinction is unobservable and stays so, since
|
|
\texttt{ScoreTuningContext} is an always-valued \texttt{Score} field, like
|
|
\texttt{metadata}, with no absent state to return to. \texttt{accidental\_
|
|
extensions} never participates in undo: no operation ever writes it, so
|
|
undo leaves it exactly as it found it.
|
|
|
|
\textbf{Re-anchoring.} Not applicable: the field is a score singleton with no
|
|
tombstonable anchor.
|
|
|
|
\section{CreateStaffGroup}
|
|
\label{sec:k0:create-staff-group}
|
|
|
|
Ratified with the genesis operation tranche's G3a rung (\texttt{spec/
|
|
CONTRACT\_GENESIS\_G3A\_ENTITIES.md}, executing \texttt{spec/RULING\_
|
|
GENESIS\_PERSISTENCE.md}): a global staff grouping (\texttt{Score.
|
|
staff\_groups}) joins the operation-authored surfaces, on the
|
|
\texttt{CreateStaff} set-union mint pattern (Section~\ref{sec:k0:create-staff}).
|
|
|
|
\textbf{Payload schema.} \texttt{CreateStaffGroupOp \{ group: StaffGroup \}}
|
|
--- the full staff-group value: identity, optional name, kind (grand staff,
|
|
bracket, sub-bracket, choral, or a registered extension kind), and the
|
|
carried \texttt{members} list.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{group}. \texttt{StaffGroup} has never been versioned, so this
|
|
operation is schema major~0 unconditionally.
|
|
|
|
\textbf{Reduction rule.} Set-union creation, mirroring \texttt{CreateStaff}
|
|
exactly: a create mints the group live if its id is fresh; a repeat create
|
|
carrying a byte-identical value reduces idempotently
|
|
(\texttt{NoOpReason::AlreadyApplied}); a create whose id is already live with
|
|
a differing value is a precondition no-op with \texttt{RecreateContentMismatch};
|
|
a create naming a tombstoned id is a precondition no-op with
|
|
\texttt{TargetTombstoned}.
|
|
|
|
\textbf{A non-empty carried \texttt{members} is refused (P13-S16).} This
|
|
operation authors the group, not its membership, so reduction preconditions that
|
|
the carried \texttt{members} is \textbf{empty}, refusing with
|
|
\texttt{ContainerNotEmpty} (discriminant 10) --- no new
|
|
\texttt{PreconditionFailureReason}. \textbf{This precondition is not
|
|
graph-gated}: it asks only about the carried value, so unlike the sibling mints'
|
|
member-liveness checks it holds \textbf{base-free as well}. Membership is
|
|
maintained from \texttt{Staff.group} instead
|
|
(Section~\ref{sec:k0:create-staff}).
|
|
|
|
\textbf{This replaced a graph-aware liveness precondition.} Under disposition B
|
|
this operation accepted a carried \texttt{members} and graph-aware reduction
|
|
additionally preconditioned that every id in it resolved to a live
|
|
\texttt{Staff}, reusing \texttt{TargetMissing} (discriminant 0) and skipped
|
|
entirely base-free. Both halves are gone: liveness is never consulted, because
|
|
the container must be empty before the question could arise.
|
|
|
|
\textbf{Membership maintenance (P13-S16, disposition A; supersedes disposition
|
|
B).} \texttt{Staff.group} (Section~\ref{sec:k0:create-staff}) is the
|
|
\textbf{sole authority} for group membership, and \texttt{members} here is a
|
|
projection \textbf{maintained from it} by reduction. The two \MUST{} agree in
|
|
both directions; graph invariant~21 (core specification \sectionsc{Graph
|
|
Invariants}) flags any disagreement between live objects, and no consumer may
|
|
read \texttt{members} to decide membership in preference to
|
|
\texttt{Staff.group}.
|
|
|
|
\textbf{What this replaced.} Under disposition B, \texttt{members} was stored
|
|
exactly as carried and \textbf{neither maintained nor trusted}, and this
|
|
operation authored a \textbf{permitted spurious-member} stale form: a
|
|
\texttt{CreateStaff(s, group: None)} followed by
|
|
\texttt{CreateStaffGroup(g, members: [s])} left \texttt{g.members == [s]} while
|
|
\texttt{s.group} stayed \texttt{None} (or named a different group).
|
|
\textbf{That sequence now refuses} the second operation with
|
|
\texttt{ContainerNotEmpty}, minting no group at all, so the form is
|
|
unauthorable rather than merely discouraged.
|
|
|
|
\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 group
|
|
(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if a live staff
|
|
still names it (a stale reference, not a strand --- \texttt{Staff.group}
|
|
degrading to point at a tombstoned id is the same shape core Chapter~6's
|
|
re-anchoring rule table already treats for other dangling references).
|
|
|
|
\textbf{Re-anchoring.} Not applicable (a staff-group mint references no
|
|
tombstonable anchor; there is no \texttt{DeleteStaffGroup} in this catalogue
|
|
revision, mirroring \texttt{CreateStaff}'s own absent delete).
|
|
|
|
\section{CreatePartDefinition}
|
|
\label{sec:k0:create-part-definition}
|
|
|
|
Ratified with genesis tranche G3a, alongside \texttt{CreateStaffGroup} above:
|
|
a part-extraction view definition (\texttt{Score.parts}) joins the
|
|
operation-authored surfaces, on the same \texttt{CreateStaff} set-union mint
|
|
pattern.
|
|
|
|
\textbf{Payload schema.} \texttt{CreatePartDefinitionOp \{ part:
|
|
PartDefinition \}} --- identity, name, and the carried \texttt{staves} list.
|
|
Parts are projections, not storage (core specification Chapter~5
|
|
\sectionsc{Parts}): only references and overrides.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{part}. \texttt{PartDefinition} has never been versioned, so this
|
|
operation is schema major~0 unconditionally.
|
|
|
|
\textbf{Reduction rule.} Set-union creation, mirroring \texttt{CreateStaff}
|
|
exactly (mint/idempotence/mismatch/tombstone as above). Graph-aware reduction
|
|
additionally preconditions that every id in \texttt{staves} resolves to a
|
|
live \texttt{Staff} (\texttt{TargetMissing}, no new failure reason), skipped
|
|
base-free.
|
|
|
|
\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 part
|
|
(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if concurrently
|
|
mutated.
|
|
|
|
\textbf{Re-anchoring.} Not applicable (a part mint references no tombstonable
|
|
anchor; there is no \texttt{DeletePartDefinition} in this catalogue
|
|
revision).
|
|
|
|
\section{CreateAnalysisLayer}
|
|
\label{sec:k0:create-analysis-layer}
|
|
|
|
Ratified with genesis tranche G3a: a first-class analysis layer
|
|
(\texttt{Score.analysis\_layers}) joins the operation-authored surfaces, on
|
|
the \texttt{CreateInstrument} mint pattern
|
|
(Section~\ref{sec:k0:create-instrument}) --- not \texttt{CreateStaff}'s,
|
|
since \texttt{AnalysisLayer} holds no outbound entity reference.
|
|
|
|
\textbf{Payload schema.} \texttt{CreateAnalysisLayerOp \{ layer:
|
|
AnalysisLayer \}} --- identity and name only (core specification Chapter~5
|
|
\sectionsc{Analysis Layers and Views}).
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{layer}. \texttt{AnalysisLayer} has never been versioned, so this
|
|
operation is schema major~0 unconditionally.
|
|
|
|
\textbf{Reduction rule.} Set-union creation, mirroring \texttt{CreateInstrument}
|
|
exactly: mint/idempotence/mismatch/tombstone as above, with \textbf{no}
|
|
graph-aware reference-resolution block --- there is nothing for one to check.
|
|
|
|
\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 layer
|
|
(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if a live view
|
|
still names it in \texttt{active\_layers} (Section~\ref{sec:k0:create-view}).
|
|
|
|
\textbf{Re-anchoring.} Not applicable (an analysis-layer mint references no
|
|
tombstonable anchor; there is no \texttt{DeleteAnalysisLayer} in this
|
|
catalogue revision).
|
|
|
|
\section{CreateView}
|
|
\label{sec:k0:create-view}
|
|
|
|
Ratified with genesis tranche G3a, the fourth and final root-level mint of
|
|
this rung: a view recipe (\texttt{Score.views}) joins the operation-authored
|
|
surfaces, on the \texttt{CreateStaff} set-union mint pattern.
|
|
|
|
\textbf{Payload schema.} \texttt{CreateViewOp \{ view: ViewDefinition \}} ---
|
|
identity, name, and the carried \texttt{active\_layers} list. The
|
|
view-\emph{kind} detail (core specification Chapter~7) is out of scope for
|
|
this baseline.
|
|
|
|
\textbf{Canonical encoding.} The length-framed canonical bytes of
|
|
\texttt{view}. \texttt{ViewDefinition} has never been versioned, so this
|
|
operation is schema major~0 unconditionally.
|
|
|
|
\textbf{Reduction rule.} Set-union creation, mirroring \texttt{CreateStaff}
|
|
exactly (mint/idempotence/mismatch/tombstone as above). Graph-aware reduction
|
|
additionally preconditions that every id in \texttt{active\_layers} resolves
|
|
to a live \texttt{AnalysisLayer} (\texttt{TargetMissing}, no new failure
|
|
reason), skipped base-free. \textbf{This packet is self-contained}: a
|
|
\texttt{CreateView}'s precondition target can be minted by a
|
|
\texttt{CreateAnalysisLayer} earlier in the same operation set, so the
|
|
ordering is testable end-to-end without a canonical base.
|
|
|
|
\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 view
|
|
(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if concurrently
|
|
mutated.
|
|
|
|
\textbf{Re-anchoring.} Not applicable (a view mint references no tombstonable
|
|
anchor; there is no \texttt{DeleteView} in this catalogue revision).
|
|
|
|
\section{CreateMeasure}
|
|
\label{sec:k0:create-measure}
|
|
|
|
Ratified with genesis tranche G3b (\texttt{spec/CONTRACT\_GENESIS\_G3B\_MEASURE.md}),
|
|
the final rung of the genesis operation tranche
|
|
(\texttt{spec/PLAN\_GENESIS\_OPS.md}): a staff instance's measure sequence
|
|
(\texttt{StaffInstance.measures}) joins the operation-authored surfaces.
|
|
Unlike Section~\ref{sec:k0:create-staff-group} through
|
|
Section~\ref{sec:k0:create-view}, \texttt{Measure} is a \textbf{nested
|
|
container child} of \texttt{StaffInstance}, not a \texttt{Score}-root vector
|
|
--- so \texttt{CreateMeasure} rides \texttt{CreateStaffInstance}'s
|
|
parent-carrying shape (Section~\ref{sec:k0:structural-containers}), not the
|
|
four G3a families' bare-value shape.
|
|
|
|
\textbf{Payload schema.} \texttt{CreateMeasureOp \{ instance: StaffInstanceId,
|
|
measure: Measure \}} --- the owning staff instance's identifier beside the
|
|
full \texttt{Measure} value. \texttt{Measure} carries no back-pointer to its
|
|
parent, so the parent must ride along, exactly like
|
|
\texttt{CreateStaffInstanceOp::region}.
|
|
|
|
\textbf{Canonical encoding.} \texttt{instance} (canonical bytes), then the
|
|
length-framed canonical bytes of \texttt{measure}. \texttt{Measure} has never
|
|
been versioned --- its only non-scalar field, \texttt{TimeAnchor}, has a
|
|
hand-written codec with no version branching of its own --- so this operation
|
|
is schema major~0 unconditionally.
|
|
|
|
\textbf{Reduction rule.} Set-union creation, on the same discipline as
|
|
\texttt{CreateStaffInstance}: a create mints the measure live, appended to the
|
|
\textbf{end} of \texttt{instance.measures} (\texttt{Measure} order is
|
|
append-only), if its id is fresh; a repeat create carrying a byte-identical
|
|
value under the \textbf{same} owning instance reduces idempotently
|
|
(\texttt{NoOpReason::AlreadyApplied}); a create whose id is already live with a
|
|
differing value, \textbf{or the same measure value under a different owning
|
|
instance}, is a precondition no-op with \texttt{RecreateContentMismatch} ---
|
|
the owning instance is part of identity here, since a \texttt{Measure} carries
|
|
no parent reference of its own; a create naming a tombstoned id is a
|
|
precondition no-op with \texttt{TargetTombstoned}.
|
|
|
|
Referential preconditions: the parent \texttt{StaffInstance} must be live
|
|
(ungated --- checked graph-aware and base-free alike, mirroring
|
|
\texttt{CreateStaffInstance}'s own region check: a mint into a non-existent
|
|
parent has nowhere to go even base-free); graph-aware only, a resolving
|
|
\texttt{measure.time\_signature} must name a live \texttt{TimeSignature}, and
|
|
every non-\texttt{WallClock} referent of \texttt{measure.start} (an
|
|
\texttt{Event}, another \texttt{Measure}, or a \texttt{Region}) must resolve.
|
|
|
|
\textbf{Ordering and boundary-distance preconditions (core specification
|
|
\sectionsc{Graph Invariants}, invariant 20).} Graph-aware, against the current
|
|
last live measure of the same instance (vacuous for an instance's first
|
|
measure's own ordering and boundary-distance clauses, for lack of a
|
|
predecessor to compare against --- but \textbf{not} for that same pickup's own
|
|
successor, which is checked against this same governing signature's full
|
|
\texttt{measure\_duration()} from the pickup's start, and refuses with
|
|
\texttt{MeasureMeterMismatch} when the pickup's actual, shorter length
|
|
disagrees with it): the carried \texttt{start} must be \textbf{comparable} to
|
|
the predecessor's start and \textbf{strictly after} it (else
|
|
\texttt{MeasureOutOfOrder}), and, when a governing time signature is
|
|
determinable, the \textbf{musical delta} between the two starts must equal
|
|
that signature's \texttt{measure\_duration()} (else
|
|
\texttt{MeasureMeterMismatch}). Either comparison being \textbf{unverifiable}
|
|
--- the two starts are not comparable, or the delta is not computable ---
|
|
refuses with \texttt{MeasureOrderUnverifiable} rather than silently permitting
|
|
an unverifiable mint. A resolving \texttt{time\_signature} that
|
|
\textbf{disagrees} with the effective grid's active signature at the
|
|
measure's start also refuses with \texttt{MeasureMeterMismatch} --- this
|
|
agreement check is \textbf{not} predecessor-dependent and applies to a first
|
|
measure like any other; \texttt{time\_signature: None} skips only this
|
|
agreement check, not the boundary-distance check above.
|
|
|
|
\textbf{The effective grid} is \texttt{StaffInstance.local\_metric\_grid} when
|
|
present, else the enclosing region's default metric grid, reconstructed from
|
|
the same operational write chains (\texttt{SetMetricGrid}'s whole-grid writes
|
|
layered under \texttt{SetTimeSignature}'s per-key changes, in canonical write
|
|
order, folding in any prospective undo restoration) in both graph-aware and
|
|
base-free reduction, so the two modes never disagree.
|
|
|
|
\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 measure and
|
|
removes it from the owning instance's \texttt{measures} vector
|
|
(Section~\ref{sec:k0:undo}). \texttt{StrictInverse} conflicts if a live
|
|
reference would be stranded, across \textbf{seven} inbound surface classes: a
|
|
spanner endpoint, a repeat structure's anchor sites, another measure's
|
|
\texttt{start}, a meter change, a system-break advisory, a page-break
|
|
advisory, or a tempo segment's \texttt{start} or optional \texttt{end}. Six of
|
|
the seven surfaces are owned (the referencing object must be live and not
|
|
itself part of the transaction being undone); a score-level
|
|
(\texttt{region: None}) tempo segment has no owning object and blocks on the
|
|
reference itself. Five of the seven are restoration-aware --- a prospective
|
|
undo restoration that would \emph{reinstate} a reference to the measure still
|
|
blocks, and one that would \emph{remove} a reference does not; the remaining
|
|
two (another measure's \texttt{start}, and a repeat structure's anchors) are
|
|
immutable value maps with no modify operation, so restoration-awareness does
|
|
not apply to them. Also closes a pre-existing hole: a minted
|
|
\texttt{TimeSignature} still named by a live \texttt{Measure.time\_signature}
|
|
now blocks its own undo, exactly as a live meter-change reference already did.
|
|
|
|
\textbf{Re-anchoring.} Not applicable (a measure mint references no
|
|
tombstonable anchor of its own; there is no \texttt{DeleteMeasure} in this
|
|
catalogue revision).
|
|
|
|
\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, canvas layout defaults,
|
|
spelling precedence, tuning context settings, 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); and
|
|
\texttt{Cascade}'s dependent-closure computation --- \texttt{Cascade} remains
|
|
\texttt{StrictInverse} over the same set. \texttt{Transpose} inversion is no
|
|
longer listed: \texttt{TransposeInterval} is undone by value restoration, not by
|
|
applying an inverse interval (Push~4a, closing P12-K2). An inverse
|
|
$(-d, -c)$ does exist wherever both components are negatable --- the reduction
|
|
never saturates --- but $\texttt{i32::MIN}$ has none, so the inverse is partial
|
|
and undo does not depend on it. The frozen \texttt{Transpose} is undone by
|
|
neither.
|
|
|
|
% ===========================================================================
|
|
\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; narrowed by
|
|
\texttt{spec/RULING\_GENESIS\_PERSISTENCE.md}]
|
|
The document root and the canvas remain \emph{structural givens}, not
|
|
operation products: \texttt{TypedObjectId} has no Canvas kind, and the
|
|
root is never op-minted (core specification, Chapter~5
|
|
\sectionsc{The Canvas}). \texttt{RULING\_GENESIS\_PERSISTENCE} reverses
|
|
only the wider claim this slot's description used to carry --- that the
|
|
score's \emph{contents} arrive outside the operation set. They do not:
|
|
the genesis tranche makes every mutable \texttt{Score} field
|
|
operation-authored, \texttt{Canvas.layout\_defaults} among them
|
|
(Section~\ref{sec:k0:set-canvas-layout-defaults}). What survives, and is
|
|
load-bearing, is the narrower claim above --- the canvas \emph{itself} is
|
|
still never minted, addressed, or deleted by any operation, and no
|
|
\texttt{TypedObjectId} kind exists for it. 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}
|