\documentclass[12pt]{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usepackage{tikz-cd}
\usetikzlibrary{arrows.meta,positioning,shapes.geometric}
\usepackage{graphicx}
\usepackage[margin=1in]{geometry}
\usepackage{everypage}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}
\usepackage{booktabs}
\usepackage{longtable}
\usepackage{tabularx}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage{listings}
\usepackage{pdflscape}
\usepackage{url}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={Distributed CatDB: Typed Operation Algebra and Coordination Boundaries},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}

\newcommand{\prior}{\textsc{established externally}}
\newcommand{\paperproved}{\textsc{proved in model}}
\newcommand{\enghyp}{\textsc{engineering hypothesis}}
\newcommand{\openclaim}{\textsc{open}}
\newcommand{\obstructed}{\textsc{obstructed}}
\newcommand{\rejected}{\textsc{rejected}}
\newcommand{\nonclaim}{\textsc{nonclaim}}
\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Status.} #1.}\par}
\newcommand{\Op}{\mathsf{Operation}}
\newcommand{\State}{\mathsf{State}}
\newcommand{\Apply}{\mathsf{apply}}
\newcommand{\scope}{\mathsf{scope}}
\newcommand{\deps}{\mathsf{dependencies}}
\newcommand{\versions}{\mathsf{versions}}
\newcommand{\frontier}{\mathsf{frontier}}
\newcommand{\Conflict}{\mathsf{Conflict}}
\newcommand{\Deferred}{\mathsf{Deferred}}
\newcommand{\Applied}{\mathsf{Applied}}
\newcommand{\Duplicate}{\mathsf{Duplicate}}
\newcommand{\Rejected}{\mathsf{Rejected}}
\newcommand{\JOIN}{\mathsf{JOIN}}
\newcommand{\CAUSAL}{\mathsf{CAUSAL}}
\newcommand{\MULTIVALUE}{\mathsf{MULTIVALUE}}
\newcommand{\ESCROW}{\mathsf{ESCROW}}
\newcommand{\ORDERED}{\mathsf{ORDERED}}
\newcommand{\ADMIN}{\mathsf{ADMIN}}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}
\newcolumntype{Y}{>{\RaggedRight\arraybackslash}X}

\setlength{\emergencystretch}{3em}
\setlist{itemsep=0.25em,topsep=0.4em}
\lstset{
  basicstyle=\ttfamily\footnotesize,
  breaklines=true,
  breakatwhitespace=false,
  columns=fullflexible,
  frame=single,
  rulecolor=\color{black!20},
  showstringspaces=false
}

\definecolor{grokgray}{RGB}{110,110,110}
\definecolor{joinblue}{RGB}{226,238,250}
\definecolor{conflictorange}{RGB}{252,237,216}
\definecolor{orderedred}{RGB}{250,227,227}
\AddEverypageHook{%
  \ifnum\value{page}=1
    \begin{tikzpicture}[remember picture,overlay]
      \node[
        rotate=90,
        anchor=south,
        font=\Large\sffamily\bfseries\color{grokgray},
        inner sep=0pt
      ] at ([xshift=38pt,yshift=0.52\paperheight]current page.south west)
      {GrokRxiv:2026.07.distributed-catdb\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{Distributed \CatDB{}: Typed Operation Algebra and Coordination Boundaries}
\author{Matthew Long \\
\textit{The YonedaAI Collaboration} \\
\textit{YonedaAI Research Collective} \\
Chicago, IL \\
\texttt{matthew@yonedaai.com} $\cdot$ \url{https://yonedaai.com}}
\date{23 July 2026}

\begin{document}
\maketitle

\begin{abstract}
A database catalog is fairly easy to replicate while every site only adds
unrelated, immutable objects.  The hard cases begin when one site activates a
schema while another edits a mapping that depends on the old schema, or when
two sites move the same branch head during a partition.  Delivering every
update everywhere does not tell us whether the updates commute.  It also does
not protect an invariant or identify the authorized semantic choice.

This paper gives a provisional distributed contract for \CatDB{}.  The contract
uses typed operation envelopes, explicit causal dependencies, component-level
merge laws, conflict records, escrow rights, and named ordered transitions.
It deliberately does not assign one merge operation to the whole catalog.
Immutable content-addressed artifacts are candidates for join-based
replication.  Dependent additions may use causal delivery.  Concurrent
alternatives can converge as an explicit multi-value conflict.  Active schema
or mapping replacement, policy replacement, branch publication, membership,
and unsafe checkpointing generally require conflict preservation or
coordination.

We define the operation and state model, give a 25-operation classification,
and work through twelve finite counterexamples.  Ordinary add/remove semantics
already fail under reorder.  The later examples cover last-writer-wins branch
heads, unchecked uniqueness, mapping composition, scalar logical clocks, and
forking hash chains.  None supplies a general semantic merge.  The CAP result
also remains unchanged: category-theoretic typing can expose preservation
obligations, but it cannot move messages across a partition or make a
noncommutative update commute.

The result is a research contract, not a distributed system.  The repository
has no distribution crate, causal metadata implementation, replicated
operation log, conflict resolver, partition simulator, convergence fixture, or
distributed benchmark.  Its direct P9 workspace and P13 provenance
dependencies are unresolved.  Runtime, recovery, convergence, availability,
and performance claims are therefore \obstructed{}.  The proposed typed
classification is an \enghyp{}, and each unimplemented bounded component
remains \openclaim{} until executable and formal evidence exists.
\end{abstract}

\tableofcontents

\section{Introduction}
\label{sec:introduction}

\subsection{The problem in plain language}

Suppose three \CatDB{} replicas share a customer schema.  Replica \(A\) creates
a new schema version that renames \code{amount} to \code{total}.  Replica \(B\),
which has not seen that change, edits a mapping so that \code{amount} is
converted from cents to dollars.  Replica \(C\) publishes a branch whose
materialization still names the old schema and mapping.  The network then
partitions.

Each edit can be valid against the version its author saw.  That does not make
the edits interchangeable.  If the rename is applied first, a name-based
mapping edit may find nothing to change.  If the unit edit is applied first,
the renamed field carries the new scale.  Once the partition heals, a system
that merely sorts operations by timestamp will produce one answer everywhere,
but the timestamp did not establish that answer's meaning or authority.

The same split appears elsewhere in the catalog.  Adding an immutable schema
version is different from making it active.  Recording two semantic commits
does not choose one branch head.  Assertion and retraction events can both be
retained without deciding which assertion is authoritative.  Content sets,
conflict sets, escrow counters, and consensus-backed pointers are all
replicated objects, but they need different consistency mechanisms.

\subsection{Research question and bounded thesis}

The research question is:

\begin{quote}
Which typed \CatDB{} operations commute, converge, conflict, or require
coordination under duplicate, reordered, delayed, and partitioned delivery?
\end{quote}

The bounded thesis is an \enghyp{}:

\begin{quote}
\CatDB{} may execute an operation without foreground coordination only when
the operation's typed effect, preconditions, invariants, delivery assumptions,
and conflict policy establish the required commutativity, idempotence, or
join-semilattice conditions.  Other operations preserve an explicit conflict,
consume reserved rights, or use a named ordering mechanism.
\end{quote}

This is not the claim that \CatDB{} ``is a CRDT.''  It is an operation-specific
classification.  The full state is decomposed into components that may use
different protocols.  A regime requested by an operation is not
self-certifying; a checker must derive or validate it from the payload,
preconditions, authority, invariants, and evidence for that operation class.

\subsection{Contributions}

This provisional paper contributes:

\begin{enumerate}
  \item a typed operation envelope, causal context, application result, and
  decomposed replicated state;
  \item state-based, operation-based, and delta-state compatibility conditions
  for a declared \CatDB{} subset;
  \item a 25-operation matrix spanning schemas, mappings, provenance,
  identity, policies, branch heads, materializations, checkpoints, and
  membership;
  \item twelve finite counterexamples that preserve conflicts hidden by
  generic merge slogans;
  \item a precise CAP and category-theory boundary;
  \item a deterministic history, Haskell, Lean, Rust, backend, and benchmark
  roadmap with falsification gates; and
  \item an implementation audit that keeps every current distributed claim
  \openclaim{} or \obstructed{}.
\end{enumerate}

\subsection{Paper organization}

\Cref{sec:status} fixes the evidence boundary.
\Cref{sec:prior-art} locates the proposed work in the distributed-systems
literature.  \Cref{sec:example} gives a running example.
\Cref{sec:formal,sec:crdt,sec:clocks} define the formal contract.
\Cref{sec:matrix} gives the operation classification.
\Cref{sec:schema-mapping,sec:partitions} examine semantic evolution and
coordination.  \Cref{sec:counterexamples} proves the finite counterexamples.
\Cref{sec:replay,sec:implementation,sec:evaluation} specify replay,
implementation, and evaluation work.  The paper ends with limitations, open
questions, exact nonclaims, and reproducibility requirements.

\section{Evidence vocabulary and current status}
\label{sec:status}

\subsection{Status discipline}

The manuscript separates external results, paper reasoning, and \CatDB{}
behavior.

\begin{longtable}{L{0.22\textwidth}L{0.70\textwidth}}
\toprule
Label & Meaning \\
\midrule
\endfirsthead
\toprule
Label & Meaning \\
\midrule
\endhead
\prior{} & A primary source establishes the result under its own model.  It is
not evidence that \CatDB{} implements the result. \\
\paperproved{} & A definition, calculation, or finite counterexample in this
paper establishes the bounded statement.  It is not runtime evidence. \\
\enghyp{} & A proposed design relation whose implementation and acceptance
evidence do not yet exist. \\
\openclaim{} & The claim has a specified test, but no accepted result. \\
\obstructed{} & A prerequisite definition, implementation, or fixture is
absent, so the claim cannot yet be tested honestly. \\
\rejected{} & The claim contradicts a theorem, counterexample, or the local
evidence cut. \\
\bottomrule
\end{longtable}

The operational labels requested for candidate \CatDB{} behavior are
\enghyp{}, \openclaim{}, and \obstructed{}.  A paper proof does not promote an
implementation claim.  An external system result does not promote one either.

\subsection{Local evidence cut}

The repository revision inspected for this paper is:
\begin{center}
\small\code{79b654fd456257865a1fe0e64a776807a012a277}.
\end{center}
The Rust workspace names exactly six crates: \code{catdb-core},
\code{catdb-ir}, \code{catdb-schema}, \code{catdb-mapping},
\code{catdb-migration}, and \code{catdb-cli}.  There is no
\code{catdb-distribution} workspace member or source directory.

Searches over the Rust, Haskell, Lean, and fixture surfaces found no accepted
P10 operation log, causal metadata type, conflict resolver, partition
simulator, convergence fixture, or benchmark.  The accepted fixture profile
covers eight bounded semantic categories but excludes distributed behavior.
The accepted Lean coverage explicitly excludes distributed execution.  The
shared roadmap marks distribution slice 13 and \code{SYS-DIST-01}
\openclaim{}.

\begin{longtable}{L{0.25\textwidth}L{0.32\textwidth}L{0.35\textwidth}}
\toprule
Local artifact & What it establishes & What it does not establish \\
\midrule
\endfirsthead
\toprule
Local artifact & What it establishes & What it does not establish \\
\midrule
\endhead
Fixture schema v1 & Eight bounded semantic categories and exact local
structural or semantic outcomes & Replication, causal delivery, conflict,
partition healing, or convergence \\
Rust semantic slice & Bounded schema, path, mapping, and migration behavior
for its fixture profile & Distribution, replay, checkpointing, or consensus \\
Haskell reference slice & Independent outcomes for the same bounded semantic
profile & A distributed oracle or CRDT implementation \\
Lean F3 coverage & Typed paths and mapping identity or composition laws under
stated assumptions & Operation commutativity, storage, liveness, or
distributed execution \\
\code{SYS-DIST-01} & A future acceptance statement for a declared convergent
subset & A passing implementation \\
Roadmap slice 13 & Proposed distribution commands and test names & Existing
crates, tests, or results \\
D6/F benchmark plan & Future distributed-history dimensions and properties &
Measurements or accepted convergence evidence \\
\bottomrule
\end{longtable}

\subsection{Dependency boundary}

P10 depends directly on P9 and P13.  P9 must define semantic commits,
workspace state, stable artifact identity, branch references, diffs, and merge
conflicts.  P13 must define provenance identity, causal and execution events,
replay references, redaction, and evidence attached to conflict decisions.
Neither prerequisite has supplied an accepted interface for P10.  The
operation envelope and state space are therefore provisional.  Runtime and
convergence claims are \obstructed{}.

P10 feeds P11, which will assign consistency guarantees to the operation
classes.  P11 cannot be treated as an already accepted global model without
reversing that dependency.

\section{Prior art and the bounded CatDB delta}
\label{sec:prior-art}

\subsection{Order, causality, and snapshots}

Lamport's happened-before relation and scalar logical clocks provide a
consistent way to reason about partial order and to construct a total order
when one is required \cite{Lamport1978TimeClocks}.  Fidge and Mattern developed
vector-time accounts that retain more causal information
\cite{Fidge1991LogicalTime,Mattern1989VirtualTime}.  Causal memory formalizes
which writes an execution must observe \cite{AhamadEtAl1995CausalMemory}.
Distributed snapshots record a consistent global state under explicit process
and channel assumptions \cite{ChandyLamport1985Snapshots}.  None of these
results supplies a semantic winner for concurrent schema or mapping edits.

\subsection{Convergence and replicated datatypes}

State- and operation-based CRDTs have precise algebraic and delivery
conditions \cite{ShapiroEtAl2011CRDT,ShapiroEtAl2011Comprehensive}.  Delta-state
replication changes dissemination granularity but preserves semilattice and
anti-entropy obligations \cite{AlmeidaEtAl2018DeltaState}.  Replicated JSON
shows that a structured datatype can preserve concurrent changes and converge
under a formal semantics \cite{KleppmannBeresford2017JSON}.  Mechanized work
has verified strong eventual consistency for selected algorithms and supplied
sequential OpSet specifications
\cite{GomesEtAl2017SEC,KleppmannEtAl2018OpSets}.  These are datatype results,
not a proof that an arbitrary semantic catalog has one merge.

\subsection{Availability and coordination}

Gilbert and Lynch prove the atomic-consistency and availability incompatibility
for an asynchronous network with partitions
\cite{GilbertLynch2002CAP}.  CALM-style results characterize monotone
computations within a formal transducer model
\cite{AmelootEtAl2013Transducers}.  Invariant confluence asks whether a
transaction set preserves a named invariant under merge
\cite{BailisEtAl2014Coordination}, while highly available transaction results
separate guarantees that are and are not achievable under a precise
availability definition \cite{BailisEtAl2013HAT}.  Abstract-datatype
commutativity can depend on state, arguments, and results
\cite{Weihl1988Commutativity}.  Escrow reserves rights for suitable bounded
invariants \cite{ONeil1986Escrow}.  RedBlue consistency demonstrates an
operation-specific split between coordinated and uncoordinated work
\cite{LiEtAl2012RedBlue}.  P10 must instantiate these models, not borrow their
conclusions by analogy.

\subsection{Systems precedents}

Bayou uses dependency checks and application-specific conflict handling
\cite{TerryEtAl1995Bayou}.  Gray and collaborators analyze hazards in
update-anywhere replication \cite{GrayEtAl1996Dangers}.  Dynamo exposes
versioning and application reconciliation in a service-specific highly
available store \cite{DeCandiaEtAl2007Dynamo}.  COPS and Cure demonstrate
causal storage under different models and system assumptions
\cite{LloydEtAl2011COPS,AkkoorathEtAl2016Cure}.  Raft provides replicated-log
consensus \cite{OngaroOusterhout2014Raft}; Spanner provides externally
consistent transactions using a coordinated system design
\cite{CorbettEtAl2012Spanner}.  These systems are precedent for mechanisms,
not evidence that \CatDB{} implements them.

\subsection{Schema, mapping, and replay}

F1 performs online schema change through compatible intermediate states and
bounded version skew \cite{RaeEtAl2013F1Schema}.  Mapping adaptation under
schema evolution can produce several valid candidates while preserving
earlier choices where possible \cite{VelegrakisEtAl2003MappingAdaptation}.
Event sourcing reconstructs state from a specified event sequence
\cite{Fowler2005EventSourcing}; it does not define a concurrent merge.
Linearizability gives a correctness condition for concurrent objects
\cite{HerlihyWing1990Linearizability}, but it does not become
partition-available under the Gilbert-Lynch boundary.

\subsection{Plausible contribution}

The plausible \CatDB{}-specific delta is an \enghyp{}:

\begin{quote}
A typed operation algebra over co-versioned schemas, mappings, semantic
commits, identity decisions, provenance, authority, and materializations can
emit a checkable per-operation coordination class, preserve finite
counterexample conflicts, and reproduce its classifications across Lean,
Haskell, Rust, and deterministic backend histories.
\end{quote}

This is narrower than a new CRDT theory.  Logical clocks, causal consistency,
CRDT convergence, CAP, CALM, invariant confluence, escrow, consensus, staged
schema rollout, mapping adaptation, and event sourcing are established prior
art.

\section{Running example}
\label{sec:example}

\subsection{Three replicas and one semantic change}

Replica \(A\) owns workspace branch \code{schema-modernization}.  Starting
from schema \(S_1\), it creates immutable version \(S_2\), where stable object
\code{sales.amount} keeps its identity but its display name becomes
\code{sales.total}.  Replica \(B\) owns branch \code{currency-fix}.  It creates
mapping \(M_2\), which changes the unit conversion on the stable object from
cents to dollars.  Replica \(C\) publishes materialization \(Q_1\), derived
from \(S_1\) and \(M_1\).  Each version is immutable and content-addressed.

If the operations name stable identities and carry their version
dependencies, the system can retain \(S_2\), \(M_2\), and \(Q_1\) as immutable
artifacts.  Publication is the difficult step.  Activating \(M_2\) before
receiving \(S_2\) leaves a missing dependency.  Moving the production branch
to \(S_2\) while another replica moves it to \(Q_1\)'s parent creates two
concurrent heads.  A refresh of \(Q_1\) is only meaningful if it records the
schema and mapping snapshot it used.

The example uses three possible outcomes:

\begin{enumerate}
  \item an immutable addition returns \(\Applied\) or \(\Duplicate\);
  \item a dependent activation returns \(\Deferred\) until its declared
  versions are present;
  \item concurrent publication returns \(\Conflict\) or enters an ordered
  compare-and-swap protocol.
\end{enumerate}

A timestamp does not decide the business meaning.  A deterministic tie-break
may make every replica display the same head, but it hides the discarded
proposal.  The conflict record must retain both candidates, their causal
contexts, their authorities, and the evidence needed for a later decision.

\subsection{Partition and healing history}

At time \(t_0\), all replicas have \(S_1\), \(M_1\), and branch head \(h_0\).
The partition isolates \(A\) from \(B\) and \(C\).

\begin{align*}
A &: \operatorname{put}(S_2);
     \operatorname{moveHead}(h_0,h_A),\\
B &: \operatorname{put}(M_2);
     \operatorname{moveHead}(h_0,h_B),\\
C &: \operatorname{publish}(Q_1,S_1,M_1).
\end{align*}

When the partition heals, all three immutable artifacts can enter the shared
artifact component.  The two head moves have the same precondition
\(h_0\), so neither dominates the other.  They become a multi-value conflict.
The materialization remains valid only for the named \(S_1,M_1\) snapshot and
must not be relabeled as current under \(S_2,M_2\).

\status{\paperproved{} for the finite history under the definitions below;
\obstructed{} for any \CatDB{} execution of it}

\section{Formal state and operation semantics}
\label{sec:formal}

This section fixes a finite specification model.  It does not assert a
particular wire protocol, storage engine, or production membership system.

\subsection{Primitive types}

\begin{lstlisting}
ReplicaId       := stable identifier for a replica
Counter         := nonnegative integer local to one ReplicaId
OpId            := (ReplicaId, Counter)
Digest          := collision-resistant content digest
ArtifactId      := Digest
VersionId       := Digest
ScopeKey        := typed semantic conflict domain
AuthorityId     := stable authority-policy reference
InvariantId     := stable invariant reference
SnapshotId      := source or catalog snapshot identity
\end{lstlisting}

\code{OpId} supplies duplicate identity, not semantic order.
\code{ArtifactId} and \code{VersionId} identify immutable canonical content.
A mutable display name is not a replica or artifact identity.

\subsection{Causal context}

\begin{definition}[Finite causal context]
For a finite replica set \(R\), a causal context is a version vector
\[
V:R\to\mathbb{N}.
\]
Define
\[
V\preceq W
\quad\Longleftrightarrow\quad
\forall r\in R,\;V(r)\leq W(r),
\]
and
\[
(V\sqcup W)(r)=\max(V(r),W(r)).
\]
Contexts are concurrent, written \(V\parallel W\), when neither dominates the
other.
\end{definition}

\begin{proposition}[Vector-context semilattice]
\label{prop:vector-semilattice}
For a fixed finite replica domain, \(\preceq\) is a partial order and
\(\sqcup\) is an associative, commutative, idempotent least upper bound.
\end{proposition}

\begin{proof}
Reflexivity, antisymmetry, and transitivity follow pointwise from the natural
number order.  Pointwise maximum is associative, commutative, and idempotent.
It dominates each operand.  Any vector that dominates both operands also
dominates their pointwise maximum, so the maximum is the least upper bound.
\end{proof}

\status{\paperproved{} for the fixed finite model; dynamic membership,
compaction, dotted vectors, and Byzantine identities remain \openclaim{}}

\subsection{Typed operation envelope}

\begin{lstlisting}
Operation<K> = {
  op_id: OpId,
  kind: K,
  author_replica: ReplicaId,
  causal_context: CausalContext,
  dependencies: Set<VersionId>,
  semantic_scope: Set<ScopeKey>,
  precondition_digest: Digest,
  authority: AuthorityId,
  invariants: Set<InvariantId>,
  payload: Payload<K>,
  idempotence_key: Digest,
  requested_regime: Regime,
  provenance_ref: VersionId
}
\end{lstlisting}

The provisional regimes are:

\begin{longtable}{L{0.19\textwidth}L{0.73\textwidth}}
\toprule
Regime & Intended contract \\
\midrule
\endfirsthead
\toprule
Regime & Intended contract \\
\midrule
\endhead
\(\JOIN\) & State-based inflationary update and component join \\
\(\CAUSAL\) & Operation delivery after declared dependencies \\
\(\MULTIVALUE\) & Preserve concurrent alternatives as a conflict \\
\(\ESCROW\) & Consume preallocated invariant-preserving rights \\
\(\ORDERED\) & Total-order or consensus-backed transition \\
\(\ADMIN\) & Membership, checkpoint, or garbage-collection barrier \\
\bottomrule
\end{longtable}

\subsection{State decomposition}

\begin{lstlisting}
DistributedState = {
  artifacts: ArtifactJoinState,
  append_events: EventJoinState,
  causal_frontier: CausalContext,
  pending: Map<OpId, Operation>,
  conflicts: ConflictJoinState,
  coordinated_refs: OrderedReferenceState,
  rights: EscrowState,
  checkpoint: CheckpointState
}
\end{lstlisting}

There is deliberately no proposed total function
\[
\mathsf{join}:
\State\times\State\to\State
\]
for this whole record.  Only a component with a justified join receives one.
Ordered references, escrow rights, and administrative state use different
contracts.

\subsection{Application result}

\begin{lstlisting}
apply : State x Operation<K> -> ApplyResult

ApplyResult =
    Applied(State, Evidence)
  | Duplicate(State, ExistingEvidence)
  | Deferred(MissingDependencies)
  | Conflict(ConflictRecord)
  | Rejected(Violation)
\end{lstlisting}

An implementation must not translate \(\Deferred\), \(\Conflict\), or
\(\Rejected\) into silent success.  A partial update before one of those
outcomes is a correctness failure unless the operation contract declares a
compensatable multi-stage transition.

\subsection{Conditional commutativity}

\begin{definition}[Conditional commutativity]
Operations \(a\) and \(b\) commute at state \(s\) under observational
equivalence \(\approx\) when both orders are defined and
\[
\Apply(\Apply(s,a),b)
\approx
\Apply(\Apply(s,b),a).
\]
\end{definition}

The relation can depend on state, parameters, authority, invariants, and
results.  An operation name such as \code{add}, \code{rename}, or
\code{merge} is not enough.  A conservative first-slice witness may require
\[
\scope(a)\cap\scope(b)=\varnothing
\]
plus proof that neither operation changes the typing context, invariant set,
authority, or interpretation needed by the other.  Disjoint serialized keys
alone do not establish semantic noninterference.

\subsection{Duplicate safety and causal readiness}

Duplicate safety requires
\[
\Apply(\Apply(s,o),o)\approx\Apply(s,o).
\]
It can follow from an idempotent effect or durable \code{OpId}
deduplication.  At-most-once transport is not assumed.

An operation is causally ready only when
\[
\deps(o)\subseteq\versions(s)
\quad\text{and}\quad
\mathsf{causalContext}(o)\preceq\frontier(s).
\]
This check prevents dependency inversion.  It neither orders concurrent
operations nor proves their semantic compatibility.

\begin{proposition}[Order-independent finite replay]
\label{prop:replay}
Let \(H\) be a finite set of deterministic operations.  Suppose every replay
order is a linear extension of the same finite dependency relation; every pair
that is incomparable in that relation commutes whenever adjacent in an
admitted replay; duplicate application is idempotent; and all preconditions
remain enabled under permitted adjacent swaps.  Then all duplicate-free linear
extensions of \(H\) produce observationally equivalent states.
\end{proposition}

\begin{proof}
Any two linear extensions of a finite partial order are connected by a finite
sequence of swaps of adjacent incomparable elements.  Each permitted swap
preserves observational equivalence by the commutativity hypothesis and
preserves later definedness by the precondition hypothesis.  Induction over
the swap sequence gives equivalent final states.  Duplicate insertions can be
removed without changing the result by idempotence.
\end{proof}

\status{\paperproved{} for the stated finite assumptions; identifying a
nontrivial \CatDB{} subset satisfying them is \openclaim{}}

\subsection{Convergence target}

Let \(H_r\) be the admitted operation set delivered to replica \(r\).  For a
declared subset \(C\), the bounded strong-eventual-consistency target requires:

\begin{enumerate}
  \item every nonfaulty replica eventually receives the same finite admitted
  set \(H\subseteq C\);
  \item dependencies precede dependent effects where the operation contract
  requires causal order;
  \item duplicate delivery has no additional effect;
  \item deterministic interpretation terminates; and
  \item resulting states are observationally equivalent.
\end{enumerate}

Thus
\[
\forall r_1,r_2,\quad
H_{r_1}=H_{r_2}=H
\Longrightarrow
s_{r_1}\approx s_{r_2}.
\]
The implication begins after equal admitted delivery.  It does not prove that
partitions heal, messages arrive, data are fresh, or the converged state
matches business intent.

\status{\enghyp{} as a specification; \obstructed{} as a \CatDB{} runtime
claim}

\section{CRDT compatibility contract}
\label{sec:crdt}

\subsection{State-based component}

A state component \(X\) is a candidate state CRDT only if:

\begin{enumerate}
  \item \((X,\sqsubseteq)\) is a join-semilattice;
  \item local mutations are inflationary;
  \item merge computes the least upper bound;
  \item replicas eventually exchange sufficient state or deltas; and
  \item serialization preserves the order and join exactly.
\end{enumerate}

Associativity, commutativity, and idempotence of join are mandatory.  An
immutable artifact set is a plausible first component if an equal digest must
identify equal canonical bytes and any collision or mismatch is rejected as
an integrity failure.

\subsection{Operation-based component}

An operation component is a candidate operation CRDT only if its effects are
deterministic, concurrent effects commute under the declared equivalence,
delivery satisfies the required reliability and causal assumptions,
duplicates are suppressed or idempotent, and dependencies and preconditions
survive delivery.

The state-based and operation-based assumptions differ
\cite{ShapiroEtAl2011CRDT}.  P10 cannot borrow the smaller messages of
operation replication while assuming the weaker dissemination conditions of
state replication.

\subsection{Delta-state component}

A delta-state design still needs a join-semilattice and an anti-entropy
protocol whose delta intervals preserve convergence and causal conditions
\cite{AlmeidaEtAl2018DeltaState}.  A small payload is neither an operation nor
a proof of idempotence.

\subsection{Three meanings of monotonicity}

The following statements are distinct:

\begin{enumerate}
  \item a local transition is inflationary in a chosen semilattice;
  \item a query is monotone under its input order; and
  \item an operation set preserves a named application invariant under merge.
\end{enumerate}

No item implies the other two without additional definitions.  CALM has a
specified network model \cite{AmelootEtAl2013Transducers}; invariant
confluence is relative to transactions and invariants
\cite{BailisEtAl2014Coordination}.  ``Monotone'' is not a universal
coordination exemption.

\section{Logical clocks and causal metadata}
\label{sec:clocks}

\subsection{Scalar logical clocks}

A Lamport clock can satisfy
\[
a\to b\Longrightarrow C(a)<C(b).
\]
The converse is false.  \(C(a)<C(b)\) does not establish \(a\to b\), and a
scalar clock alone cannot detect concurrency \cite{Lamport1978TimeClocks}.
Adding a replica-ID tie-break produces a deterministic total order, but its
extra order is policy, not causality.

\subsection{Vector-style context}

For the fixed finite model, \(V_a\prec V_b\) can represent causal precedence,
while incomparable vectors expose concurrency
\cite{Fidge1991LogicalTime,Mattern1989VirtualTime}.  The vector does not
provide synchronized wall time, freshness, a single global snapshot, a
conflict winner, membership compaction, or causal delivery unless the
transport uses it correctly.

\subsection{Causal consistency}

Causal memory, COPS, and Cure show stronger ordering than bare eventual
consistency without one global order over every operation
\cite{AhamadEtAl1995CausalMemory,LloydEtAl2011COPS,AkkoorathEtAl2016Cure}.
Their data models and protocols differ.  P10 may use causal delivery for
dependent schema and mapping operations, but causal consistency is not
serializability or linearizability.

\section{Candidate operation and coordination matrix}
\label{sec:matrix}

The regime abbreviations are \(J=\JOIN\), \(C=\CAUSAL\),
\(M=\MULTIVALUE\), \(E=\ESCROW\), \(O=\ORDERED\), and
\(A=\ADMIN\).  Every row is an \enghyp{}.  The last column records whether the
corresponding \CatDB{} result is \openclaim{} or \obstructed{}.

\begin{landscape}
\scriptsize
\begin{longtable}{L{1.55in}L{1.85in}L{2.55in}L{0.62in}L{1.35in}}
\caption{Candidate P10 operation classification.}
\label{tab:operation-matrix}\\
\toprule
Operation & Conditional duplicate behavior & Concurrent relation &
Regime & CatDB status \\
\midrule
\endfirsthead
\toprule
Operation & Conditional duplicate behavior & Concurrent relation &
Regime & CatDB status \\
\midrule
\endhead
Put immutable artifact by content hash &
Same hash and bytes are idempotent; same hash and different bytes is a fatal
integrity failure &
Commutes with distinct content hashes &
\(J\) & \openclaim{} \\

Append semantic commit with immutable ID and parent set &
Duplicate ID must reproduce identical canonical bytes &
Commutes as DAG-node addition if parents exist; branch publication is
separate &
\(C/J\) & \obstructed{} on P9 \\

Append provenance event with stable ID &
Duplicate must return existing evidence &
Commutes as event-set addition; a single predecessor hash chain may fork &
\(C/J\) & \obstructed{} on P13 \\

Record immutable validation receipt &
Idempotent by receipt digest &
Commutes when it names fixed input versions and checker revision &
\(J\) & \openclaim{} \\

Add schema declaration under fresh stable ID &
Duplicate must match bytes &
Commutes only if namespaces, equations, types, and active invariants remain
independent &
\(C/M\) & \openclaim{} \\

Add schema equation or constraint proposal &
Duplicate proposal is idempotent &
Proposal append may commute; activation can invalidate data or mappings &
\(M/O\) & \obstructed{} \\

Replace active schema version &
Compare-and-swap can reject a duplicate stale request &
Generally noncommutative with schema, mapping, query, and data operations &
\(O\) & \obstructed{} \\

Rename or delete schema object &
Operation ID can deduplicate replay &
Noncommutative with references, mappings, constraints, and queries &
\(M/O\) & \obstructed{} \\

Add immutable mapping version under fresh ID &
Duplicate must match canonical mapping &
Version addition may commute after dependencies; activation is separate &
\(C/J\) & \openclaim{} \\

Replace or activate mapping for a scope &
Compare-and-swap can reject stale replay &
Generally noncommutative with schema evolution and other replacements &
\(M/O\) & \obstructed{} \\

Compose mappings &
Same derived-version request can be idempotent by digest &
Composition order matters and the reverse may be ill-typed &
\(C\) & \openclaim{} \\

Add assertion under a fresh assertion ID &
Duplicate must match assertion and evidence &
Event addition commutes; authoritative current-state projection may not &
\(C/J\) & \obstructed{} on P13 \\

Retract or invalidate assertion &
Replay can deduplicate by event ID &
Concurrent assertion and retraction need observed-remove or authority policy &
\(C/M\) & \obstructed{} \\

Add identity equivalence edge &
Duplicate edge is idempotent &
Set union converges, but closure can violate authority or cardinality policy &
\(C/M/O\) & \obstructed{} on P7/P13 \\

Reverse or split identity decision &
Replay can deduplicate event &
Nonmonotone against prior merges and dependent derivations &
\(M/O\) & \obstructed{} \\

Increment unbounded counter &
Increment needs deduplication or a per-replica component &
Concurrent increments commute &
\(J/C\) & \openclaim{} \\

Decrement bounded quota &
Duplicate debit is unsafe without deduplication &
Concurrent debits can violate a lower bound &
\(E/O\) & \openclaim{} \\

Advance single-source cursor &
Repeated exact position may be idempotent &
Maximum works only in one comparable epoch with no fork &
\(C/J\) & \obstructed{} on P6 \\

Invalidate materialization version &
Duplicate invalidation is idempotent &
Set addition can commute when it names an immutable version &
\(J/C\) & \obstructed{} on P6 \\

Publish refreshed materialization &
Duplicate result digest is idempotent &
Noncommutative across snapshots, mappings, and active pointer &
\(M/O\) & \obstructed{} \\

Change authority or semantic policy &
Replay can deduplicate request &
Grant, revoke, and replacement are order-sensitive &
\(O\) & \obstructed{} \\

Approve a fixed immutable proposal &
Duplicate approval can be idempotent &
Approval-set addition may commute; thresholds and revocation may not &
\(C/J/O\) & \obstructed{} \\

Move branch head &
Compare-and-swap can make stale replay fail &
Concurrent moves conflict; last-writer-wins discards a branch decision &
\(M/O\) & \obstructed{} on P9 \\

Checkpoint and truncate operation history &
Same certificate may be idempotent &
Unsafe against lagging replicas or unobserved tombstones &
\(A/O\) & \obstructed{} \\

Change replica membership &
Duplicate configuration ID can be recognized &
Concurrent changes alter quorum and causal-metadata interpretation &
\(O/A\) & \obstructed{} \\
\bottomrule
\end{longtable}
\normalsize
\end{landscape}

The matrix is a research hypothesis.  It is not accepted behavior.  In
particular, a slash lists candidate mechanisms to investigate; it does not
assert that they are interchangeable.

\section{Schema and mapping replication}
\label{sec:schema-mapping}

\subsection{Immutable versions and active references}

The candidate design separates two layers:

\begin{enumerate}
  \item immutable schema and mapping versions are content-addressed artifacts;
  adding independent versions may be a monotone replicated operation; and
  \item active references identify the version that governs a workspace,
  branch, query, or write path; changing an active reference is a publication
  decision that may require conflict preservation or ordering.
\end{enumerate}

Convergence of the version set does not imply convergence of the active
semantic interpretation.

\subsection{Checked independent schema addition}

Adding declarations \(d_1\) and \(d_2\) under fresh stable identifiers is a
candidate commuting pair only when:

\begin{enumerate}
  \item neither reuses an identifier or namespace key;
  \item neither changes the type or interpretation of an existing
  declaration;
  \item their equations and constraints do not create a joint inconsistency;
  \item existing mappings, queries, data, and policies remain well-typed;
  \item activation is not implicit; and
  \item the combined schema has a deterministic canonical representation.
\end{enumerate}

The first slice should treat this list as a checked noninterference condition,
not as a law for all operations named \code{Add}.

\status{\enghyp{}; the checker and executable histories are \openclaim{}}

\subsection{Deletion, rename, and type change}

Deletion, rename, and type change can invalidate mapping images, schema
equations, constraints, queries, materializations, connectors, identity rules,
provenance explanations, and policies.  A tombstone can make replication state
monotone, but it does not make the semantic transition commute.  The system
still needs a rule for concurrent references and for every derived artifact
that used the old schema.

\subsection{Mapping addition, activation, and composition}

An immutable mapping version can be added after its source schema, target
schema, and validation dependencies arrive.  Activating it can change query
answers, migration behavior, information-loss status, write authority, and
provenance.

Mapping composition is associative where the typed categorical construction
and preservation assumptions hold.  It is not commutative:
\[
G\circ F\neq F\circ G
\]
in general, and the reverse composition may not be typed.  Associativity of
sequential transformations is not a concurrent merge rule.

\subsection{Mapping adaptation as a search result}

Schema evolution can invalidate mappings, and adaptation may produce several
valid candidates \cite{VelegrakisEtAl2003MappingAdaptation}.  A candidate P10
adaptation record is:

\begin{lstlisting}
MappingAdaptation = {
  old_mapping: VersionId,
  source_schema_before: VersionId,
  source_schema_after: VersionId,
  target_schema_before: VersionId,
  target_schema_after: VersionId,
  candidate_mapping: VersionId,
  preserved_choices: Set<ChoiceId>,
  changed_choices: Set<ChoiceId>,
  obligations: Set<InvariantId>,
  authority: AuthorityId,
  status: proposed | validated | approved | rejected
}
\end{lstlisting}

Two valid candidates remain a conflict until an authorized policy chooses,
composes, or rejects them.  Deterministic enumeration does not create that
authority.

\subsection{Staged compatibility}

F1 uses pairwise-compatible intermediate schemas and bounded version skew
because abrupt schema changes can corrupt data or produce incorrect results
while old and new servers coexist \cite{RaeEtAl2013F1Schema}.  The result does
not justify arbitrary asynchronous merge.  Its shared-storage architecture,
stateless-server assumptions, and schema semantics are not \CatDB{} evidence.

For adjacent versions \(v_i\) and \(v_{i+1}\), the provisional relation
\[
v_i\mathrel{\mathsf{compatible}}v_{i+1}
\]
requires a witness:

\begin{lstlisting}
CompatibilityWitness = {
  before: VersionId,
  after: VersionId,
  readers: Set<ComponentVersion>,
  writers: Set<ComponentVersion>,
  preserved_operations: Set<OperationKind>,
  blocked_operations: Set<OperationKind>,
  data_backfill: Optional<BackfillPlan>,
  mapping_adaptations: Set<VersionId>,
  invariants_checked: Set<InvariantId>,
  maximum_version_skew: NonnegativeInteger,
  evidence: Set<EvidenceRef>
}
\end{lstlisting}

\status{\obstructed{} because no such \CatDB{} witness type or checker exists}

\section{Partitions, availability, and coordination}
\label{sec:partitions}

\subsection{Per-operation partition contracts}

CAP terminology is useful only after its meanings are fixed.  For each
operation class \(K\), P10 requires:

\begin{lstlisting}
PartitionContract<K> = {
  safety_property: exact named property,
  availability_property: exact response/termination property,
  failure_model: crash | omission | partition | other,
  reachable_replicas_required: integer or quorum rule,
  accepted_partition_result: value | conflict | stale |
                             rejection | timeout,
  healing_rule: anti_entropy | replay |
                consensus_catch_up | repair,
  freshness_bound: optional and separately justified
}
\end{lstlisting}

There is no platform-wide answer.  Immutable artifact addition, bounded quota
debit, schema activation, and a linearizable branch-head update may use
different contracts.

\subsection{CAP boundary}

\begin{corollary}[Typing does not remove the CAP execution]
\label{cor:cap}
Suppose a \textup{\CatDB{}} object and its clients satisfy the network, failure,
availability, and atomic-consistency definitions of Gilbert and Lynch
\cite{GilbertLynch2002CAP}.  Replacing an untyped update with a typed morphism
or a functorially checked operation does not permit both atomic consistency and
availability in the partition execution covered by their theorem.
\end{corollary}

\begin{proof}
The type annotation does not add a communication edge to the partitioned
execution.  If both sides must respond, neither can learn the other side's
concurrent choice.  If the responses must behave as operations on one atomic
object, the indistinguishability argument remains.  At least one side must
wait, reject, or otherwise fail the theorem's availability condition.
\end{proof}

\status{\prior{} for the impossibility result and \paperproved{} for the
model-preservation inference; any claim that \CatDB{} ``beats CAP'' is
\rejected{}}

\subsection{Named coordination mechanisms}

\begin{longtable}{L{0.25\textwidth}L{0.31\textwidth}L{0.36\textwidth}}
\toprule
Need & Candidate mechanism & Evidence boundary \\
\midrule
\endfirsthead
\toprule
Need & Candidate mechanism & Evidence boundary \\
\midrule
\endhead
Same immutable content set & State join or delta anti-entropy &
Needs a semilattice and eventual exchange \\
Causal dependency order & Causal broadcast or buffering &
Does not choose a concurrent winner \\
Preserve concurrent alternatives & Multi-value register or conflict set &
Converges on conflicts, not one semantic value \\
Maintain numeric bound & Escrow or reservation rights &
Allocation and recovery are part of correctness \\
Select active schema or branch head & Consensus-backed compare-and-swap &
Loses partition-time availability for that operation \\
Safe schema rollout & Staged compatible versions &
Needs a proved compatibility relation and skew bound \\
Compact tombstones or history & Stable causal frontier and checkpoint
certificate & Unsafe while unseen operations can arrive \\
Byzantine resistance & Outside the first P10 profile &
Crash and partition evidence does not transfer \\
\bottomrule
\end{longtable}

\subsection{Event sourcing boundary}

Event sourcing can reconstruct state by replaying one specified history
\cite{Fowler2005EventSourcing}.  It does not supply a merge law for concurrent
histories, causal delivery, duplicate safety, invariant preservation, or
agreement on one authoritative order.  ``Append-only'' is not a CRDT proof.

\section{Counterexample histories}
\label{sec:counterexamples}

Each history is a paper-level result under its displayed definitions.  None is
evidence of a \CatDB{} runtime.

\subsection{CE-01: naive add and remove diverge}

Let \(S_A=S_B=\varnothing\), and consider concurrent operations
\[
a=\operatorname{add}(x),
\qquad
b=\operatorname{remove}(x)
\]
with ordinary sequential set semantics.  Then
\[
b(a(\varnothing))=\varnothing
\quad\text{but}\quad
a(b(\varnothing))=\{x\}.
\]
The operations do not commute.  An observed-remove, add-wins, remove-wins,
tombstone, or explicit-conflict design must change the semantics.

\status{\paperproved{}; \CatDB{} implementation \obstructed{}}

\subsection{CE-02: schema rename and mapping-unit edit}

Let
\[
s=(\mathit{name},\mathit{scale})=(\code{amount},100).
\]
Define
\[
r(n,k)=
\begin{cases}
(\code{total},k) & n=\code{amount},\\
(n,k) & \text{otherwise},
\end{cases}
\]
and
\[
u(n,k)=
\begin{cases}
(n,1) & n=\code{amount},\\
(n,k) & \text{otherwise}.
\end{cases}
\]
Direct calculation gives
\[
r(u(s))=(\code{total},1),
\qquad
u(r(s))=(\code{total},100).
\]
Both edits are valid against the base version, but they do not commute.
Stable identifiers may help detect or translate the edit.  The translation
rule is the missing conflict protocol, not a consequence of replication.

\status{\paperproved{}; \CatDB{} implementation \obstructed{}}

\subsection{CE-03: uniqueness is not merge-closed}

Define
\[
I(S)\Longleftrightarrow
\text{\code{email} is unique in }S.
\]
From one valid ancestor, replica \(A\) inserts customer 1 with
\code{a@example.org}; replica \(B\) inserts customer 2 with the same email.
Each local state satisfies \(I\), while their set union does not.  The
operation and invariant pair is not invariant-confluent under this merge.
Coordination, ownership, reservation, or an explicit conflicting state is
required.

\status{\paperproved{}; \CatDB{} implementation \obstructed{}}

\subsection{CE-04: last-writer-wins loses a branch}

Let the initial branch head be \(h_0\).  During a partition:
\[
A:h_0\mapsto h_A,
\qquad
B:h_0\mapsto h_B.
\]
A timestamp and replica-ID tie-break can select \(h_B\) everywhere, but
\(h_A\) disappears from the active reference without a merge or recorded
conflict.  Determinism establishes convergence, not preservation or semantic
correctness.  A multi-value head can retain \(\{h_A,h_B\}\); choosing one then
requires an authorized merge or ordered compare-and-swap.

\status{\paperproved{}; \CatDB{} implementation \obstructed{} on P9}

\subsection{CE-05: activation before a schema dependency}

Let mapping \(M_2\) refer to schema \(S_2\).  Replica \(A\) receives
\(\operatorname{activate}(M_2)\) before \(S_2\).  Immediate application either
creates a dangling active mapping or interprets it against the wrong schema.
The operation must declare \(S_2\) and return \(\Deferred\) until the
dependency is present.  Receipt-time sorting does not repair the missing
version.

\status{\paperproved{} for the typed precondition; \CatDB{} implementation
\obstructed{}}

\subsection{CE-06: checkpoint truncation breaks duplicate safety}

Replica \(A\) applies operation \(o\), records its \code{OpId}, checkpoints,
and deletes both the log entry and the deduplication marker.  Replica \(B\),
partitioned before the checkpoint, later replays \(o\).  If the effect is not
intrinsically idempotent, \(A\) applies it twice.

A safe checkpoint must retain an idempotence summary or prove that every
replica and durable message source has crossed a stable frontier.

\status{\paperproved{}; \CatDB{} implementation \obstructed{}}

\subsection{CE-07: tombstone collection resurrects deletion}

Replica \(A\) observes \(\operatorname{add}(x)\), then
\(\operatorname{remove}(x)\), and garbage-collects the remove tombstone.
Replica \(B\), partitioned since before the remove, later sends old state
containing \(\operatorname{add}(x)\).  Merge without the tombstone restores
\(x\).  Collection therefore needs a stable causal frontier or another design
that retains the remove information required by its semantics.

\status{\paperproved{}; \CatDB{} implementation \obstructed{}}

\subsection{CE-08: identity union and split are not one join}

Let \(a,b,c\) be source identities.  Replica \(A\) records \(a\sim b\);
replica \(B\) records \(b\sim c\).  Union followed by equivalence closure
yields \(a\sim c\).  A later authoritative decision that \(a\not\sim c\)
cannot be expressed as another equivalence edge.  It retracts or qualifies
earlier closure and may invalidate derived results.

Identity-edge union can be a CRDT component.  Governed identity history,
reversal, and current authoritative equivalence are not thereby solved.

\status{\paperproved{}; \CatDB{} implementation \obstructed{} on P7/P13}

\subsection{CE-09: mapping composition is not concurrent merge}

Given
\[
F:S\to T,
\qquad
G:T\to U,
\]
\(G\circ F:S\to U\) may be defined.  \(F\circ G\) is not typed unless
\(U=S\), and even then it need not equal \(G\circ F\).  A replicated set
containing both mappings does not specify their intended pipeline order.

\status{\paperproved{} by typing; bounded mapping model \openclaim{} and
replication \obstructed{}}

\subsection{CE-10: scalar logical order invents a winner}

Concurrent operations \(a\) and \(b\) can receive scalar logical times 7 and
9 without \(a\to b\).  Ordering by \code{(clock, replica\_id)} applies \(a\)
before \(b\) everywhere, but the winner follows from tie-breaking policy
rather than causality.  For concurrent schema replacements, that choice
requires authority.

\status{\prior{} for the logical-clock boundary, \paperproved{} for the finite
policy example, and \CatDB{} implementation \obstructed{}}

\subsection{CE-11: policy grant and revoke invert authority}

Assume actor \(p\) initially lacks merge authority.  Concurrently:
\[
g=\operatorname{grant}(p,\mathit{merge}),
\qquad
r=\operatorname{revoke}(p,\mathit{merge}).
\]
Grant followed by revoke denies; revoke followed by grant allows.  A
last-writer rule needs a trusted order and still encodes a policy decision.
Union of the policy events can preserve the conflict, but it cannot decide
whether an intervening merge was authorized.

\status{\paperproved{}; \CatDB{} implementation \obstructed{}}

\subsection{CE-12: a hash chain forks}

Two replicas share event hash \(h_0\).  During a partition they append
\(e_A\) and \(e_B\), each naming \(h_0\):
\[
h_A=H(h_0,e_A),
\qquad
h_B=H(h_0,e_B).
\]
Both links are valid, so the result is a fork.  A Merkle DAG can preserve both
branches; one canonical chain requires ordering or later selection.  Hash
chaining makes represented links tamper-evident.  It does not prove that
events were not omitted or that one global order exists.

\status{\paperproved{}; \CatDB{} implementation \obstructed{} on P13}

\begin{proposition}[No universal merge follows from the twelve histories]
\label{prop:no-universal-merge}
There is no single operation-order-insensitive interpretation of the
unmodified sequential operations in CE-01, CE-02, CE-04, CE-09, CE-11, and
CE-12 that both preserves their stated sequential meanings and identifies
every delivery order.
\end{proposition}

\begin{proof}
CE-01, CE-02, and CE-11 each display two orders with different results under
the stated sequential semantics.  CE-09 shows that one reverse order may be
ill-typed.  CE-04 shows that selecting one value without retaining the other
loses a valid concurrent branch.  CE-12 shows that two valid successors of one
hash do not form one chain.  Any order-insensitive interpretation must
therefore change at least one operation's semantics, preserve multiple
outcomes, reject an order, or introduce coordination.
\end{proof}

\section{Replay, checkpoint, and recovery model}
\label{sec:replay}

\subsection{A history is more than an event sequence}

A deterministic P10 history contains:

\begin{lstlisting}
History = {
  replica_set: MembershipEpoch,
  initial_states: Map<ReplicaId, Digest>,
  operations: Map<OpId, Operation>,
  deliveries: Sequence<DeliveryEvent>,
  partitions: Sequence<PartitionEvent>,
  crashes: Sequence<CrashEvent>,
  durable_boundaries: Sequence<DurabilityEvent>,
  checkpoints: Sequence<CheckpointEvent>,
  expected_results: Map<StepId, ApplyResultClass>
}
\end{lstlisting}

The delivery schedule, duplicate events, and durability boundaries are part of
the input.  Wall-clock races are not an adequate fixture.  Replaying the same
canonical history must expose the same result class at every step.

\subsection{Dependency buffering}

When an operation's declared dependency is absent, the interpreter places the
operation in \code{pending} and returns \(\Deferred\).  Receipt of a missing
version rechecks only operations indexed by that dependency.  A dependency
cycle, unknown membership epoch, failed authority check, or invalid
precondition remains distinct from temporary absence.

\begin{proposition}[Dependency readiness is not conflict resolution]
If two operations \(a\) and \(b\) are both causally ready and their contexts
are concurrent, readiness alone does not imply that they commute.
\end{proposition}

\begin{proof}
In CE-02, both the rename and unit edit are defined against the same base
state, so each can be causally ready after that base version is present.  The
calculation still gives different outcomes under the two orders.
\end{proof}

\subsection{Deduplication and durable effects}

The abstract apply protocol requires a durable relationship among:

\begin{enumerate}
  \item canonical operation-log append;
  \item state effect or conflict record;
  \item deduplication identity;
  \item response evidence; and
  \item replay after crash.
\end{enumerate}

A backend that writes the effect before the deduplication marker can apply an
operation twice after a crash.  A backend that writes the marker before the
effect can lose the effect.  An implementation may use one atomic database
transaction, a write-ahead protocol, or a proved idempotent effect, but it must
name the choice.

\subsection{Checkpoint certificate}

A candidate certificate records:

\begin{lstlisting}
CheckpointCertificate = {
  checkpoint_id: SnapshotId,
  state_digest: Digest,
  causal_frontier: CausalContext,
  membership_epoch: VersionId,
  retained_dedup_summary: Digest,
  retained_tombstone_summary: Digest,
  acknowledged_replicas: Set<ReplicaId>,
  operation_classes: Set<OperationKind>,
  authority: AuthorityId,
  evidence: Set<EvidenceRef>
}
\end{lstlisting}

The certificate is not proof of safety until the membership, lagging-replica,
durable-message, tombstone, and deduplication assumptions are established.
Checkpoint and garbage collection remain \obstructed{}.

\subsection{Tamper evidence}

Canonical hashes can detect later alteration of represented bytes.  A
predecessor link can make a path tamper-evident.  Neither property proves
completeness, one global order, or protection against deletion.  P13 must
define what an evidence reference attests before P10 can use it in a recovery
claim.

\section{Implementation status and staged roadmap}
\label{sec:implementation}

\subsection{Current result}

There is no distributed \CatDB{} implementation.  This paper introduces no
Rust, Haskell, Lean, fixture, backend, or benchmark artifact.  The candidate
operation algebra is an \enghyp{}.  The runtime claim that a bounded subset
converges after duplicate, reordered, and partitioned delivery is
\obstructed{}.

\subsection{Gate R0: freeze prerequisites}

Implementation begins only after:

\begin{enumerate}
  \item P9 supplies accepted semantic commit, workspace, branch, and conflict
  types;
  \item P13 supplies accepted operation and provenance identity;
  \item P3 and P4 supply bounded schema and mapping version semantics;
  \item P7 supplies identity authority and reversal semantics;
  \item P6 supplies cursor and materialization semantics;
  \item P11 names guarantees for the regimes P10 exposes; and
  \item the crash, partition, membership, and delivery models are fixed.
\end{enumerate}

\status{\obstructed{}}

\subsection{Gate R1: language-neutral fixtures}

The proposed closed, versioned artifacts are:

\begin{lstlisting}
fixtures/distribution/operation-v1.schema.json
fixtures/distribution/history-v1.schema.json
fixtures/distribution/expected-v1.schema.json
fixtures/distribution/cases/*.json
\end{lstlisting}

Each fixture records the membership epoch, initial state digests, typed
operations, causal dependencies, delivery schedule, partitions, healing,
duplicates, crashes, restarts, expected step results, final canonical states,
and conflict sets.  It distinguishes \code{conflict}, \code{deferred},
\code{rejected}, and \code{unsupported} from a skipped test.

\status{\openclaim{} after R0}

\subsection{Gate R2: independent Haskell reference semantics}

The proposed modules are:

\begin{lstlisting}
haskell/catdb-reference/src/CatDB/Distribution/Types.hs
haskell/catdb-reference/src/CatDB/Distribution/Causal.hs
haskell/catdb-reference/src/CatDB/Distribution/Apply.hs
haskell/catdb-reference/src/CatDB/Distribution/History.hs
haskell/catdb-reference/src/CatDB/Distribution/Properties.hs
\end{lstlisting}

The interpreter should compute canonical states, conflicts, pending
operations, and step results for deterministic schedules.  Property tests
should check conditional commutativity and idempotence and shrink failing
histories.  Shared generated decision logic with Rust would weaken the oracle
and must be disclosed.

\status{\openclaim{}; Haskell tests would be computational evidence, not
theorem proof}

\subsection{Gate R3: bounded Lean core}

\begin{longtable}{L{0.15\textwidth}L{0.39\textwidth}L{0.37\textwidth}}
\toprule
ID & Target statement & Required assumptions \\
\midrule
\endfirsthead
\toprule
ID & Target statement & Required assumptions \\
\midrule
\endhead
DIST-L01 & Version-vector dominance is a partial order &
Finite replica identifiers and pointwise natural order \\
DIST-L02 & Pointwise maximum is associative, commutative, and idempotent &
Same replica domain \\
DIST-L03 & Immutable artifact-set union is a join-semilattice &
Collision-free or integrity-rejecting identity \\
DIST-L04 & Reapplying admitted immutable-artifact insertion is idempotent &
Canonical bytes and exact digest equality \\
DIST-L05 & Pairwise commuting deterministic operations give
order-independent finite replay &
Swapped pairs remain enabled and preserve preconditions \\
DIST-L06 & Causal topological replays agree for the declared subset &
Finite acyclic dependencies and concurrent commutativity \\
DIST-L07 & Ordinary add and remove do not commute &
CE-01 sequential set semantics \\
DIST-L08 & Rename and unit edit do not commute &
CE-02 state and functions \\
DIST-L09 & Uniqueness is not closed under merge &
CE-03 union and uniqueness invariant \\
DIST-L10 & Checkpoint safety needs retained deduplication or stable frontier &
Explicit replay and truncation model \\
\bottomrule
\end{longtable}

The build must report axiom assumptions and reject \code{sorry},
\code{admit}, declaration-level axioms, and untracked classical assumptions.
These theorems would not prove transport liveness, backend durability, CAP
escape, or production performance.

\status{\openclaim{} and blocked on a shared operation model}

\subsection{Gate R4: Rust distribution crate}

The first proposed Rust slice is:

\begin{lstlisting}
crates/catdb-distribution/
  operation.rs
  causal.rs
  apply.rs
  conflict.rs
  replay.rs
  checkpoint.rs
  history.rs
  canonical.rs
\end{lstlisting}

Its initial admitted subset should include only immutable artifact addition,
immutable commit or event addition with dependency buffering, durable
\code{OpId} deduplication in the simulator, explicit multi-value conflicts,
deterministic replay, and stable canonical serialization.  Schema activation,
mapping activation, identity reversal, policy replacement, membership, and
checkpoint truncation should return
\code{UNSUPPORTED\_OPERATION\_CLASS} until their protocols exist.

\status{\obstructed{} on R0 through R3}

\subsection{Gates R5 through R8}

R5 adds a deterministic simulator with controlled delivery, duplicate, delay,
omission, partition, healing, crash, durable-state, membership, checkpoint,
and seed events.  R6 compares Haskell and Rust at every step.  R7 adds backend
failpoints before and after every durability boundary.  R8 runs system
acceptance commands:

\begin{lstlisting}
cargo test -p catdb-distribution --test duplicate_reorder_replay
cargo test -p catdb-distribution --test partition_heal_convergence
cargo test -p catdb-distribution --test coordination_required
cargo test -p catdb-distribution --test operation_log_recovery
cargo test -p catdb-distribution --test stale_materialization_visibility
cargo test -p catdb-distribution --test causal_dependency_buffering
cargo test -p catdb-distribution --test schema_mapping_noncommutativity
cargo test -p catdb-distribution --test conflict_set_convergence
cargo test -p catdb-distribution --test checkpoint_frontier
cargo test -p catdb-distribution --test membership_epoch_rejection
cabal test catdb-reference
lake build
\end{lstlisting}

These commands are acceptance targets.  They do not currently run because the
referenced distribution artifacts do not exist.

\status{\obstructed{}}

\section{Evaluation and falsification plan}
\label{sec:evaluation}

\subsection{Correctness before timing}

The study begins with deterministic histories over 2, 3, 5, and 9 replicas.
Operation streams range from 10 to 100,000 operations where feasible and mix
data, schema, mapping, identity, policy, provenance, cursor, and
materialization changes.  Schedules include overlapping semantic scopes,
multiple partitions, duplicate and reordered delivery, crash and restart,
version skew, stale materializations, administrative operations, checkpoints,
and intentionally unsafe garbage collection.

\subsection{Baselines}

\begin{longtable}{L{0.14\textwidth}L{0.29\textwidth}L{0.49\textwidth}}
\toprule
ID & Baseline & Purpose \\
\midrule
\endfirsthead
\toprule
ID & Baseline & Purpose \\
\midrule
\endhead
P10-BL01 & Single serial interpreter &
Canonical sequential result where one exists \\
P10-BL02 & Consensus-ordered log &
Strong-order correctness and coordination cost \\
P10-BL03 & State-based full-state CRDT &
Convergence and message-size comparison \\
P10-BL04 & Delta-state CRDT &
Incremental dissemination comparison \\
P10-BL05 & Causal operation CRDT &
Operation payload and causal-metadata comparison \\
P10-BL06 & Multi-value conflict register &
Conflict preservation without semantic classification \\
P10-BL07 & Last-writer-wins register &
Negative baseline for hidden conflicts and lost proposals \\
P10-BL08 & Event-log replay without concurrent merge &
Negative baseline for event-sourcing overclaim \\
P10-BL09 & Invariant-confluence classifier &
Coordination-decision baseline \\
P10-BL10 & Escrow bounded counter &
Rights-based invariant baseline \\
P10-BL11 & Staged F1-style schema profile &
Compatibility baseline for supported online changes \\
\bottomrule
\end{longtable}

Brand names are not equivalent baselines.  Each implementation must disclose
its operation, conflict, failure, and delivery semantics.

\subsection{Exact correctness measurements}

The correctness record includes:

\begin{itemize}
  \item canonical-state disagreement after equal admitted delivery;
  \item conflicts missed, invented, or silently resolved;
  \item duplicate operations with an additional effect;
  \item lost accepted operations and forbidden causal inversions;
  \item invariant violations;
  \item stale results reported as current;
  \item checkpoint resurrection and replay errors;
  \item cross-language semantic disagreements; and
  \item minimized counterexample size.
\end{itemize}

Any nonzero value in an excluded category is a correctness failure, not a
performance tradeoff.

\subsection{Performance after correctness}

Only a passing correctness profile may report local and coordinated latency,
partition-time rejection or unavailability, time to convergence after
healing, messages and bytes per operation, causal metadata size, pending
buffer residence, conflict rate and record size, checkpoint and replay cost,
CPU, memory, disk writes, network transfer, classification overhead, and
throughput.

Performance runs need exact source revisions, environment capture, repeated
runs, cold or warm labels, and uncertainty intervals.  A fast finite history
does not prove all histories, and a large random campaign does not replace a
bounded proof.

\subsection{Falsification anchors}

The thesis fails for any admitted profile if:

\begin{enumerate}
  \item a pair classified as commutative yields observably different states
  under the two orders;
  \item an operation classified as idempotent changes state on replay;
  \item a join violates associativity, commutativity, or idempotence;
  \item a schema or mapping operation is accepted without its dependencies;
  \item Rust, Haskell, and Lean use incompatible equality or error semantics;
  \item replicas receive the same admitted set and do not converge;
  \item partition healing loses an accepted operation;
  \item a lagging replica resurrects collected state;
  \item recovery reapplies an effect or loses deduplication;
  \item a causal dependency appears in a forbidden order;
  \item conflict sets differ after equal delivery;
  \item membership or checkpointing admits a history excluded by the proof;
  \item a noncommutative semantic transition silently chooses a winner;
  \item uniqueness, authority, or quota is violated by a
  coordination-free classification;
  \item an available API blocks indefinitely on an unreachable quorum;
  \item a linearizable API returns mutually incompatible completed results;
  \item escrow rights are duplicated, lost, or overspent;
  \item the paper reports performance without raw histories and environment
  evidence;
  \item a theorem omits a delivery, failure, finiteness, or equality
  assumption used by its proof;
  \item category theory is used to claim escape from CAP or consensus;
  \item an external system result is reported as \CatDB{} behavior; or
  \item a last-writer-wins result is called conflict-free without recording
  the discarded value.
\end{enumerate}

Every failure should become a minimized immutable regression fixture.

\section{Limitations}
\label{sec:limitations}

There is no distributed runtime to evaluate.  The paper can reject invalid
universal claims and state a typed design, but it cannot show that the proposed
boundary is practical.  No history has passed through a \CatDB{} network.  No
crash has tested a durable deduplication path, and no benchmark has measured
the cost of causal or semantic metadata.

The finite replica model is deliberately small.  Dynamic membership,
long-lived partitions, replica retirement, causal-context compaction, and
checkpoint certification are unresolved.  The initial failure model excludes
Byzantine behavior.  Content hashes are treated as integrity identities under
a collision-rejecting assumption; the paper does not supply a cryptographic
threat model.

The operation matrix also depends on unfinished semantic work.  P9 must say
what a branch head and semantic commit mean.  P13 must say what event identity
and provenance evidence attest.  P7, P6, and P11 affect identity reversal,
materialization state, and consistency contracts.  Those dependencies can
change the payloads or move an operation between candidate regimes.

Explicit conflicts do not resolve themselves.  A multi-value result can
converge and still leave a difficult human or policy decision.  A controlled
study is needed to learn whether typed conflict records improve diagnosis;
richer metadata by itself is not evidence.

\section{Open questions}
\label{sec:open-questions}

\begin{enumerate}
  \item What is the smallest useful semantic scope language that is stronger
  than byte or key overlap but still decidable and cheap?
  \item Which immutable schema and mapping additions admit a compositional
  noninterference proof?
  \item Can compatibility witnesses support staged rollouts across mapping,
  provenance, and authority versions as well as schemas?
  \item Which causal-context representation supports dynamic membership
  without weakening the replay proof?
  \item How should a checkpoint certificate account for offline replicas and
  durable messages outside the service?
  \item Which invariants admit escrow or ownership partitioning, and which
  require one ordered authority?
  \item Can a conflict record remain compact while preserving both proposals,
  dependencies, policy, and provenance?
  \item How should redaction interact with hash-linked replay evidence and
  conflict reproduction?
  \item Can Lean, Haskell, and Rust share a fixture vocabulary without sharing
  decision logic that undermines oracle independence?
  \item What false-positive and false-negative rates result from semantic
  operation classification compared with manual invariant-confluence or
  RedBlue classification?
  \item When is deterministic last-writer-wins an explicitly authorized
  policy rather than a hidden default?
  \item Which P11 guarantees should be exposed per operation without
  collapsing them into one platform label?
\end{enumerate}

\section{Conclusion}
\label{sec:conclusion}

A distributed \CatDB{} design has to classify operations before it can promise
a merge.  Immutable content addition, causal dependency delivery, explicit
conflict preservation, escrow, ordered publication, and administrative
barriers solve different problems.  The typed envelope proposed here records
those differences and gives each claim a test.

The counterexamples need only a few operations.  Ordinary add and remove do
not commute.  Two locally valid inserts can break uniqueness, and a branch
tie-break can erase a valid proposal.  Mapping composition has a direction.
A logical clock is not causality.  A hash chain can fork.  Categorical
language does not change any of these results.

The next credible result is a narrow fixture-backed slice: immutable
artifacts, dependency buffering, durable duplicate identity, explicit
multi-value conflicts, and deterministic replay.  An independent executable
model, a bounded formal model, Rust, and backend recovery histories must agree
on that slice.  Until they do, the design remains an \enghyp{}, its testable
components remain \openclaim{}, and its runtime claims remain \obstructed{}.

\appendix

\section{Exact nonclaims}
\label{app:nonclaims}

The following statements are part of the paper's claim boundary.

\begin{enumerate}
  \item \CatDB{} does not currently implement distributed replication.
  \item \CatDB{} has no accepted CRDT operation subset.
  \item \CatDB{} has no accepted causal delivery or logical-clock
  implementation.
  \item \CatDB{} has no accepted consensus, membership, checkpoint, or
  garbage-collection protocol.
  \item \CatDB{} has no measured partition-time availability, convergence
  time, throughput, or latency.
  \item Category theory does not eliminate CAP-style tradeoffs.
  \item Category theory does not make arbitrary schema or mapping changes
  commute.
  \item Functor composition is not a concurrent merge law.
  \item Event sourcing does not by itself guarantee convergence.
  \item Append-only storage does not by itself guarantee idempotence or causal
  order.
  \item A Lamport timestamp is not a concurrency detector, wall clock, or
  freshness proof.
  \item Vector clocks do not choose a winner for concurrent semantic updates.
  \item Causal consistency is not serializability or linearizability.
  \item Deterministic last-writer-wins resolution is not proof of correct
  business meaning.
  \item Replica convergence does not imply invariant preservation.
  \item Replica convergence does not imply that source data or
  materializations are fresh.
  \item A tombstone does not repair mappings, queries, or policies invalidated
  by schema deletion.
  \item A content hash does not establish one global append order.
  \item A hash chain does not prevent event omission or concurrent forks.
  \item An immutable version set does not determine one active schema,
  mapping, or branch head.
  \item Exactly-once delivery is not assumed.
  \item Network partitions are not assumed to heal within a fixed time.
  \item Byzantine faults, malicious replicas, and cryptographic consensus are
  outside the initial P10 profile.
  \item Haskell property tests would be computational evidence, not theorem
  proof.
  \item Lean proofs over a finite model would not prove transport liveness,
  backend durability, or production performance.
  \item External CRDT, database, and consensus systems are precedent, not
  \CatDB{} implementation evidence.
  \item No universal consistency label describes the proposed platform.
  \item No automatic conflict resolver may silently infer business authority.
\end{enumerate}

\section{Claim-status ledger}
\label{app:claims}

\scriptsize
\begin{longtable}{L{0.09\textwidth}L{0.42\textwidth}L{0.16\textwidth}L{0.20\textwidth}}
\toprule
ID & Claim & Evidence & Status \\
\midrule
\endfirsthead
\toprule
ID & Claim & Evidence & Status \\
\midrule
\endhead
P10-C01 & State-based CRDT convergence has semilattice and inflationary-update
conditions & Literature & \prior{} \\
P10-C02 & Operation-based convergence needs effect commutativity and delivery
assumptions & Literature & \prior{} \\
P10-C03 & Atomic consistency and availability conflict during partitions in
the Gilbert-Lynch model & Theorem & \prior{} \\
P10-C04 & The inspected repository has no P10 distribution implementation &
Local audit & \obstructed{} implementation \\
P10-C05 & Digest-addressed immutable insertion can be an idempotent join
component under integrity assumptions & Design & \openclaim{} \\
P10-C06 & The whole distributed state should not receive one unproved join &
Safety restriction & \enghyp{} \\
P10-C07 & The stated rename and unit edit do not commute & Counterexample &
\paperproved{} \\
P10-C08 & Mapping composition is not an order-independent concurrent merge &
Typing & \paperproved{} \\
P10-C09 & Causal dependencies can buffer mapping activation until its schema
arrives & Design & \openclaim{} \\
P10-C10 & Scalar Lamport clocks cannot detect concurrency by themselves &
Literature & \prior{} \\
P10-C11 & Unique-key inserts are not invariant-confluent under set union &
Counterexample & \paperproved{} \\
P10-C12 & A bounded \CatDB{} subset converges through duplicate, reorder, and
partitions & Runtime & \obstructed{} \\
P10-C13 & Noncommutative operations always conflict or use named coordination &
Runtime & \obstructed{} \\
P10-C14 & Recovery preserves operations and deduplication facts & Runtime &
\obstructed{} \\
P10-C15 & Causal metadata overhead is acceptable & Performance &
\obstructed{} \\
P10-C16 & Semantic classification reduces coordination or improves throughput &
Performance & \obstructed{} \\
P10-C17 & Lean can prove the bounded core & Formal target & \openclaim{} \\
P10-C18 & Haskell can provide an independent finite-history oracle &
Computational target & \openclaim{} \\
P10-C19 & Rust and backend histories match the reference model & Runtime &
\obstructed{} \\
P10-C20 & Category theory eliminates CAP-style tradeoffs & Broad claim &
\rejected{} \\
P10-C21 & Event sourcing alone guarantees convergence & Broad claim &
\rejected{} \\
P10-C22 & Convergence implies correct business meaning & Broad claim &
\rejected{} \\
\bottomrule
\end{longtable}
\normalsize

\section{Reproducibility contract}
\label{app:reproducibility}

\subsection{Manuscript reproduction}

The manuscript source and bibliography are the only publication artifacts
created for this author pass.  A clean build copies those two files to a new
temporary directory and runs:

\begin{lstlisting}
latexmk -cd -pdf -interaction=nonstopmode -halt-on-error paper.tex
\end{lstlisting}

The repository contains no generated PDF, cover, auxiliary file, review
artifact, distribution source, or benchmark result from this pass.  The
paper-local \code{reproducibility.md} records the exact temporary build
directory, tool versions, hashes, warning inventory, page count, and all-page
render inspection.

\subsection{Future execution bundle}

Every future distributed run archives:

\begin{lstlisting}
benchmarks/runs/<run_id>/
  pre-registration.md
  source.json
  build.json
  environment.json
  baseline-manifest.json
  history-schema.json
  histories/
  delivery-schedules/
  raw-observations/
  canonical-states/
  conflicts/
  minimized-failures/
  statistics.json
  provenance.json
\end{lstlisting}

Seeds, source revisions, membership epochs, delivery schedules, crash points,
durability boundaries, canonical states, and minimized failures are required.
Convergence and invariant checks are exact per finite history.  Performance
claims require repeated runs and uncertainty reporting.

\bibliographystyle{plain}
\bibliography{references}

\end{document}
