957 lines
46 KiB
TeX
957 lines
46 KiB
TeX
% !TEX program = xelatex
|
|
%
|
|
% Epiphany --- Operation Catalog (companion specification)
|
|
% Companion to the Core Specification. Compile with XeLaTeX.
|
|
%
|
|
% This document is versioned independently of the Core Specification
|
|
% (independent semver; see the Versioning note in the front matter). Its preamble
|
|
% is intentionally a self-contained copy of the core specification's preamble so
|
|
% the two documents build independently; factoring a shared preamble file is a
|
|
% later cleanup, not a v0.1 deliverable.
|
|
|
|
\documentclass[11pt,letterpaper]{report}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Packages
|
|
% ---------------------------------------------------------------------------
|
|
\usepackage{fontspec}
|
|
\usepackage{geometry}
|
|
\geometry{
|
|
letterpaper,
|
|
top=1.05in,
|
|
bottom=1.05in,
|
|
left=1.15in,
|
|
right=1.15in,
|
|
headheight=15pt
|
|
}
|
|
|
|
\usepackage[english]{babel}
|
|
\usepackage{microtype}
|
|
\usepackage{parskip}
|
|
\usepackage{xcolor}
|
|
\usepackage{hyperref}
|
|
\usepackage{enumitem}
|
|
\usepackage{titlesec}
|
|
\usepackage{fancyhdr}
|
|
\usepackage{booktabs}
|
|
\usepackage{array}
|
|
\usepackage{longtable}
|
|
\usepackage{listings}
|
|
\usepackage{amsmath}
|
|
\usepackage{amssymb}
|
|
\usepackage{tcolorbox}
|
|
\tcbuselibrary{breakable, skins}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Color palette (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\definecolor{epiphanyteal}{HTML}{1A4044}
|
|
\definecolor{epiphanygold}{HTML}{8E6E2E}
|
|
\definecolor{epiphanyink}{HTML}{1F1B16}
|
|
\definecolor{epiphanyslate}{HTML}{6B6660}
|
|
\definecolor{epiphanycream}{HTML}{F8F4ED}
|
|
\definecolor{epiphanymist}{HTML}{ECE8E0}
|
|
\definecolor{epiphanycode}{HTML}{2A2520}
|
|
\definecolor{epiphanycrimson}{HTML}{7A2424}
|
|
|
|
\hypersetup{
|
|
colorlinks=true,
|
|
linkcolor=epiphanyteal,
|
|
citecolor=epiphanyteal,
|
|
urlcolor=epiphanygold,
|
|
pdftitle={Epiphany --- Operation Catalog},
|
|
pdfauthor={The Epiphany Project},
|
|
pdfsubject={Operation Catalog companion for the Epiphany music notation platform},
|
|
pdfkeywords={music notation, operations, CRDT, reduction, serialization},
|
|
bookmarksnumbered=true,
|
|
bookmarksopen=true
|
|
}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Typography (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\setmainfont{TeX Gyre Pagella}[Numbers={OldStyle, Proportional}, Ligatures={TeX, Common}]
|
|
\setsansfont{TeX Gyre Heros}[Scale=0.94, Ligatures={TeX, Common}]
|
|
\setmonofont{TeX Gyre Cursor}[Scale=0.88, Ligatures={TeX}]
|
|
\newfontfamily\titlefont{TeX Gyre Pagella}[Numbers={OldStyle}, Ligatures={TeX, Common}]
|
|
\newcommand{\tablenums}[1]{{\addfontfeatures{Numbers={Lining,Tabular}}#1}}
|
|
\newcommand{\sectionsc}[1]{{\addfontfeatures{Letters=SmallCaps}#1}}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Section styling (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\titleformat{\chapter}[display]
|
|
{\normalfont\filright}
|
|
{\raggedright\color{epiphanygold}\fontsize{14pt}{16pt}\selectfont
|
|
\scshape Chapter\ \thechapter}
|
|
{16pt}
|
|
{\raggedright\color{epiphanyteal}\fontsize{32pt}{36pt}\selectfont\bfseries}
|
|
[\vspace{4pt}{\color{epiphanygold}\rule{2in}{0.6pt}}]
|
|
\titlespacing*{\chapter}{0pt}{-20pt}{30pt}
|
|
\titleformat{\section}
|
|
{\normalfont\Large\bfseries\color{epiphanyteal}}
|
|
{\color{epiphanygold}\thesection}{1em}{}
|
|
\titleformat{\subsection}
|
|
{\normalfont\large\bfseries\color{epiphanyteal}}
|
|
{\color{epiphanygold}\thesubsection}{1em}{}
|
|
\titleformat{\subsubsection}
|
|
{\normalfont\normalsize\bfseries\color{epiphanyink}}
|
|
{\thesubsubsection}{1em}{}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Headers and footers (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\pagestyle{fancy}
|
|
\fancyhf{}
|
|
\renewcommand{\headrulewidth}{0pt}
|
|
\renewcommand{\footrulewidth}{0pt}
|
|
\fancyhead[L]{\small\scshape\color{epiphanyslate}Epiphany --- Operation Catalog}
|
|
\fancyhead[R]{\small\itshape\color{epiphanyslate}\leftmark}
|
|
\fancyfoot[C]{\small\color{epiphanyslate}\thepage}
|
|
\renewcommand{\headrule}{
|
|
\color{epiphanygold!50}\hrule width\headwidth height 0.4pt
|
|
\vspace{1pt}
|
|
\color{epiphanygold!30}\hrule width\headwidth height 0.2pt
|
|
}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Code listing style (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\lstdefinelanguage{Rust}{
|
|
keywords={fn,let,mut,pub,struct,enum,impl,trait,for,in,if,else,match,return,
|
|
use,mod,crate,self,Self,as,where,move,async,await,const,static,
|
|
ref,type,unsafe,extern,dyn,box,break,continue,loop,while},
|
|
keywordstyle=\color{epiphanyteal}\bfseries,
|
|
ndkeywords={i8,i16,i32,i64,i128,u8,u16,u32,u64,u128,f32,f64,bool,char,str,
|
|
String,Vec,Option,Result,Box,Rc,Arc,HashMap,BTreeMap,
|
|
NonZeroU16,NonZeroU32,NonZeroU64,Duration,Timestamp},
|
|
ndkeywordstyle=\color{epiphanygold}\bfseries,
|
|
sensitive=true,
|
|
comment=[l]{//},
|
|
morecomment=[s]{/*}{*/},
|
|
commentstyle=\color{epiphanyslate}\itshape,
|
|
stringstyle=\color{epiphanycrimson},
|
|
morestring=[b]",
|
|
morestring=[b]'
|
|
}
|
|
\lstset{
|
|
basicstyle=\ttfamily\small\color{epiphanycode},
|
|
backgroundcolor=\color{epiphanycream},
|
|
frame=leftline,
|
|
rulecolor=\color{epiphanygold!60},
|
|
framesep=8pt,
|
|
framerule=1.5pt,
|
|
xleftmargin=10pt,
|
|
xrightmargin=4pt,
|
|
breaklines=true,
|
|
showstringspaces=false,
|
|
numberstyle=\tiny\color{epiphanyslate},
|
|
numbersep=10pt,
|
|
captionpos=b,
|
|
aboveskip=10pt,
|
|
belowskip=10pt,
|
|
language=Rust
|
|
}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Custom environments (shared with the core specification)
|
|
% ---------------------------------------------------------------------------
|
|
\newtcolorbox{openquestion}[1][]{
|
|
enhanced, breakable,
|
|
colback=epiphanymist, colframe=epiphanycrimson,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Open Question},
|
|
coltitle=white, colbacktitle=epiphanycrimson,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
\newtcolorbox{rationale}[1][]{
|
|
enhanced, breakable,
|
|
colback=epiphanymist, colframe=epiphanyteal,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Rationale},
|
|
coltitle=white, colbacktitle=epiphanyteal,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
\newtcolorbox{requirement}[1][]{
|
|
enhanced, breakable,
|
|
colback=white, colframe=epiphanygold,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Requirement},
|
|
coltitle=white, colbacktitle=epiphanygold,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
\newtcolorbox{nongoal}[1][]{
|
|
enhanced, breakable,
|
|
colback=epiphanymist, colframe=epiphanyslate,
|
|
fonttitle=\bfseries\color{white}, title={\scshape\hspace{2pt}Non-Goal},
|
|
coltitle=white, colbacktitle=epiphanyslate,
|
|
arc=1pt, boxrule=0pt, leftrule=2pt,
|
|
left=10pt, right=10pt, top=8pt, bottom=8pt,
|
|
attach boxed title to top left={xshift=0pt, yshift=0pt},
|
|
boxed title style={arc=0pt, sharp corners, boxrule=0pt, left=6pt, right=8pt, top=2pt, bottom=2pt},
|
|
#1
|
|
}
|
|
|
|
\newcommand{\MUST}{\textbf{MUST}}
|
|
\newcommand{\MUSTNOT}{\textbf{MUST}\nobreak\ \textbf{NOT}}
|
|
\newcommand{\SHOULD}{\textbf{SHOULD}}
|
|
\newcommand{\SHOULDNOT}{\textbf{SHOULD}\nobreak\ \textbf{NOT}}
|
|
\newcommand{\MAY}{\textbf{MAY}}
|
|
|
|
\setlist[itemize]{topsep=2pt, itemsep=3pt, parsep=0pt}
|
|
\setlist[enumerate]{topsep=2pt, itemsep=3pt, parsep=0pt}
|
|
\setlist[description]{topsep=2pt, itemsep=5pt, parsep=0pt}
|
|
\AtBeginDocument{\color{epiphanyink}}
|
|
|
|
% ---------------------------------------------------------------------------
|
|
% Document
|
|
% ---------------------------------------------------------------------------
|
|
\begin{document}
|
|
|
|
\begin{titlepage}
|
|
\thispagestyle{empty}
|
|
\centering
|
|
\vspace*{2.2in}
|
|
{\color{epiphanygold}\rule{3in}{0.8pt}}\\[18pt]
|
|
{\titlefont\fontsize{34pt}{38pt}\selectfont\color{epiphanyteal}\bfseries Epiphany}\\[10pt]
|
|
{\Large\scshape\color{epiphanyslate}Operation Catalog}\\[6pt]
|
|
{\large\itshape\color{epiphanyslate}A companion to the Core Specification}\\[14pt]
|
|
{\color{epiphanygold}\rule{3in}{0.8pt}}\\[24pt]
|
|
{\normalsize\color{epiphanyink}Version 0.2.0 --- Phase 2 (K0 representative + broad-K0 M2 groups)}\\[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 remaining (Phase-3) framework slots of
|
|
Chapter~\ref{ch:k1} are \emph{unavailable} under the Phase-2 profile: an
|
|
implementation \MUST{} reject (not silently ignore) an operation whose kind is one
|
|
of those slots it does not implement.
|
|
|
|
% ===========================================================================
|
|
\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.} 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}).
|
|
|
|
\begin{openquestion}
|
|
\textbf{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 is the one representative payload that is not self-contained
|
|
under migration; the disposition (whether a richer v0 corpus, or a documented
|
|
read-only fallback, is the long-term answer) is a Pass-12 question.
|
|
\end{openquestion}
|
|
|
|
\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. A
|
|
modification that \emph{moves} the event (a different region-local position or
|
|
duration) is recorded in the bookkeeping but its placement change is \emph{not}
|
|
applied to the graph: re-sorting a voice on a placement change is a deferred
|
|
refinement, and an in-place move would break \texttt{VoiceEventsSortedNonOverlap}
|
|
(Chapter~5 invariant~3). A malformed (empty pitched) replacement is likewise
|
|
recorded but not materialised.
|
|
|
|
\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.} Under the prototype's minted-object undo
|
|
(Section~\ref{sec:k0:undo}) a field overwrite mints nothing, so undoing the
|
|
enclosing transaction does not restore the prior event value; a snapshot-and-
|
|
restore inverse is a Phase-3 refinement (P11-C8).
|
|
|
|
\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 is the only minting member: undoing the enclosing
|
|
transaction tombstones the minted pitch, re-resting the event if it was the only
|
|
one (Section~\ref{sec:k0:undo}). The prototype's minted-object undo has nothing
|
|
to tombstone for delete or modify, so neither is inverted under it (re-introducing
|
|
a tombstoned pitch or restoring a prior value is a Phase-3 refinement, P11-C8).
|
|
|
|
\textbf{Re-anchoring.} An operation whose target event or pitch is tombstoned is
|
|
a no-op; tombstoning a pitch runs the cross-cutting re-anchoring table over any
|
|
structure that referenced it (see DeleteEvent).
|
|
|
|
\section{Transpose}
|
|
\label{sec:k0:transpose}
|
|
|
|
\textbf{Payload schema.} \texttt{TransposeOp \{ targets: Vec<PitchId>,
|
|
chromatic\_steps: i32 \}}. Pitch identifiers are preserved; only acoustic content
|
|
changes.
|
|
|
|
\textbf{Canonical encoding.} The canonically-ordered \texttt{targets} set, then
|
|
\texttt{chromatic\_steps} as a little-endian \texttt{i32}.
|
|
|
|
\textbf{Reduction rule.} An order-dependent content overwrite. Each live target
|
|
pitch is shifted by \texttt{chromatic\_steps}; reduction is order-dependent in the
|
|
general case (interval composition need not commute), so the resolved value is
|
|
the composition in canonical reduction order. In this prototype
|
|
\texttt{chromatic\_steps} is a minimal CMN alteration shift that commutes except
|
|
at the alteration's \texttt{i8} saturation bound; rich interval algebra is
|
|
deferred (Chapter~4 tuning catalog; P12-K2).
|
|
|
|
\textbf{Conflict cases.} None --- composition is deterministic in canonical order
|
|
(a deterministic repair, not a conflict).
|
|
|
|
\textbf{Undo semantics.} Transpose mints nothing, so the prototype's minted-object
|
|
undo (Section~\ref{sec:k0:undo}) does not negate it; an inverse-interval undo is a
|
|
Phase-3 refinement (P11-C8).
|
|
|
|
\textbf{Re-anchoring.} Tombstoned targets are skipped (the transpose applies only
|
|
to live pitches).
|
|
|
|
\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{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.} A modification mints nothing, so the prototype's
|
|
minted-object undo (Section~\ref{sec:k0:undo}) does not restore the prior
|
|
structure value (a snapshot-and-restore inverse is Phase-3, P11-C8).
|
|
|
|
\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{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 field overwrites that mint nothing, so the
|
|
prototype's minted-object undo (Section~\ref{sec:k0:undo}) does not restore the
|
|
prior metadata, grid, or break preference (a snapshot-and-restore inverse is a
|
|
Phase-3 refinement, P11-C8).
|
|
|
|
\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{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.
|
|
|
|
\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{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 prototype models the compensation as tombstoning the objects the target
|
|
transaction minted: \texttt{StrictInverse} conflicts (\texttt{TombstonedTarget})
|
|
if any minted object was already tombstoned; \texttt{BestEffort} tombstones the
|
|
survivors; \texttt{Cascade} is \texttt{StrictInverse} over the same set
|
|
(dependent-closure undo is a Phase-3 refinement, P11-C8).
|
|
|
|
% ===========================================================================
|
|
\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*{Remaining framework slots (Phase 3 --- unavailable, MUST reject)}
|
|
|
|
\begin{description}
|
|
\item[Create score / canvas / staff]
|
|
The remaining structural mints (the document root, the canvas, and global
|
|
staves) the Phase-2 slice does not exercise. Discipline: set-union creation.
|
|
\item[Set time signature / tempo segment]
|
|
The finer-grained metric-model overwrites beneath the whole-grid
|
|
\texttt{SetMetricGrid} (Section~\ref{sec:k0:score-settings}): a single meter
|
|
change or tempo segment rather than the region's entire grid. Discipline:
|
|
last-writer-wins structural overwrite.
|
|
\item[Set layout]
|
|
The non-break layout advisories (the page/system-break advisories themselves
|
|
are implemented --- Sections~\ref{sec:k0:set-user-system-break} and
|
|
\ref{sec:k0:score-settings}). Discipline: LWW advisory.
|
|
\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}
|