\documentclass[12pt]{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,shapes.geometric,fit,calc}
\usepackage[margin=1in]{geometry}
\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}
\usepackage{seqsplit}
\usepackage[numbers,sort&compress]{natbib}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={A Rust Runtime for Categorical Data Systems},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{proposition}{Proposition}[section]
\newtheorem{requirement}[proposition]{Requirement}
\theoremstyle{definition}
\newtheorem{definition}[proposition]{Definition}
\newtheorem{contract}[proposition]{Contract}
\theoremstyle{remark}
\newtheorem{remark}[proposition]{Remark}
\newtheorem{example}[proposition]{Example}
\newtheorem{counterexample}[proposition]{Counterexample}

\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\computational}{\textsc{computational}}
\newcommand{\machinechecked}{\textsc{machine-checked}}
\newcommand{\prior}{\textsc{supported by prior literature}}
\newcommand{\enghyp}{\textsc{engineering hypothesis}}
\newcommand{\openclaim}{\textsc{open}}
\newcommand{\obstructed}{\textsc{obstructed}}
\newcommand{\rejected}{\textsc{rejected as written}}
\newcommand{\nonclaim}{\textsc{nonclaim}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Evidence status.} #1.}\par}
\newcommand{\Schema}{\mathsf{Schema}}
\newcommand{\Mapping}{\mathsf{Mapping}}
\newcommand{\Instance}{\mathsf{Instance}}
\newcommand{\Path}{\mathsf{Path}}
\newcommand{\Diag}{\mathsf{Diagnostic}}
\newcommand{\Validate}{\mathsf{validate}}
\newcommand{\Normalize}{\mathsf{normalize}}
\newcommand{\Compile}{\mathsf{compile}}
\newcommand{\Execute}{\mathsf{execute}}
\newcommand{\Capabilities}{\mathsf{capabilities}}
\newcommand{\Revision}{\mathsf{revision}}
\newcommand{\SchemaRev}{\mathsf{schemaRev}}
\newcommand{\MappingRev}{\mathsf{mappingRev}}
\newcommand{\CapabilitiesRev}{\mathsf{capabilitiesRev}}
\newcommand{\DeltaF}{\Delta_F}
\newcommand{\SigmaF}{\Sigma_F}
\newcommand{\PiF}{\Pi_F}
\newcommand{\hash}[1]{\texttt{\footnotesize\seqsplit{#1}}}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}
\newcolumntype{Y}{>{\RaggedRight\arraybackslash}X}

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

\definecolor{grokgray}{RGB}{110,110,110}
\definecolor{kernelblue}{RGB}{226,238,250}
\definecolor{evidencegreen}{RGB}{226,244,232}
\definecolor{roadmaporange}{RGB}{252,237,216}
\definecolor{boundaryred}{RGB}{250,227,227}
\AddToHook{shipout/background}{%
  \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.catdb-rust-runtime\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{A Rust Runtime for Categorical Data Systems:\\
Implemented Semantic Kernel, Evidence Boundaries, and Production Roadmap}
\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{center}
\fbox{\large Provisional paper status: \obstructed{}}
\end{center}

\begin{abstract}
Categorical database theory supplies an attractive account of schemas,
instances, mappings, and data migration. It does not, by itself, supply a
production runtime. The engineering gap includes serialization, diagnostics,
validation, compilation, physical planning, transactions, cancellation,
connectors, deployment, and evidence that abstraction does not damage
performance. This paper asks which part of that gap the accepted \CatDB{} Rust
evidence actually closes.

The accepted Slice 4 boundary contains six Rust crates and 4,051 lines of Rust
source and tests. It implements closed serialized values; finite schema, path,
mapping, and instance validation; mapping identity and composition; a bounded
finite pullback migration \(\Delta_F\); and fixture verification. Its shared
33-case corpus contains 29 semantic cases and four structural-only cases under
capability set \code{slice-4}. A fresh isolated Rust run passes all 29 semantic
cases. An independently implemented Haskell process computes the same 29
results with zero disagreements. A separate Lean development machine-checks
selected path and mapping laws, but it does not verify the Rust source.

The accepted result is a research kernel, not a production database runtime.
There is
no query IR, physical planner, plan cache, storage connector, SQLite or
PostgreSQL execution path, transaction layer, asynchronous executor, server,
WebAssembly target result, operation-replay engine, or performance experiment
at either boundary. At the accepted Slice 4 boundary, Sigma and Pi return
explicit unsupported outcomes, and information-loss and schema-diff envelopes
are represented but not computed. The direct equation checker is deliberately
incomplete.

We reconstruct the implemented boundary, state exact claim labels, analyze
concrete counterexamples to common overclaims, compare the design with categorical
database implementations and conventional Rust query engines, and specify a
falsifiable path from the semantic kernel to a compiled runtime. The narrow
systems thesis remains an \enghyp{}: a versioned categorical layer may be
compiled into validated native plans and kept outside the hot execution path.
No performance or production-readiness claim is made.
\end{abstract}

\tableofcontents

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

\subsection{The problem in plain language}

A schema mapping is easy to draw and surprisingly hard to execute safely.
Suppose one source stores customers and orders in normalized tables while a
consumer expects one document per customer. A semantic mapping may say that
the consumer's \code{orders} field follows a relationship path, that money is
measured in cents, and that two paths to an account identifier must agree.
Those statements are more informative than a pile of column names. They still
leave a runtime with practical work: reject an ill-typed path, preserve the
equation, choose where the join runs, control a transaction, report why a
mapping failed, and avoid recompiling an unchanged plan.

Category theory helps describe the meaning of the transformation. It does not
make network calls, enforce a database isolation level, estimate a join, or
cancel a remote query. Rust can help structure the implementation and exclude
classes of memory errors. It does not prove that cents were converted to
dollars or that two schemas mean the same thing. A credible runtime paper must
keep these obligations separate.

The distinction matters especially in an ambitious research program.
Architecture diagrams can contain an IR, a planner, connectors, a server, and
a WebAssembly target long before those components exist. Conversely, a small
kernel may contain useful executable evidence even though it is not yet a
system. This paper treats the manifest, source, tests, and release records as
the boundary. Names in a roadmap are not counted as implementation.

\subsection{Research question}

The paper asks:

\begin{quote}
Which semantic and runtime obligations are implemented by the accepted
\CatDB{} Rust boundary, how strong is the evidence for them, which obligations
remain unsupported, and what additional contracts and experiments are required
before the workspace can support production-runtime claims?
\end{quote}

The answer has two parts. First, the accepted kernel implements a meaningful
finite slice: typed schema and mapping operations, finite instances, and
bounded \(\Delta\), connected to shared Rust/Haskell fixtures and selected Lean
laws. Second, nearly every claim involving physical data systems remains
unimplemented. Work after Slice 4 is excluded from the terminal paper evidence.

\subsection{Bounded thesis}

\begin{quote}
For the closed finite profile admitted by \code{slice-4}, the accepted Rust
kernel computes deterministic structured outcomes for schema, path, mapping,
instance, and bounded pullback-migration operations, and its 29 semantic
fixture outcomes agree exactly with an independent Haskell evaluator.
\end{quote}

\status{\computational. The claim is finite and corpus-indexed.}

The corresponding production thesis is weaker and prospective:

\begin{quote}
A future \CatDB{} runtime may compile versioned semantic obligations into
backend-native plans, cache the compiled artifacts, and keep the categorical
layer outside the hot row-processing path.
\end{quote}

\status{\enghyp. No backend, planner, or performance run exists.}

\subsection{Contributions}

This provisional paper contributes:

\begin{enumerate}
  \item a source-grounded reconstruction of the six-crate Rust workspace and
  its exact dependency boundary;
  \item a separation among serialized representation, semantic validation,
  abstract laws, and physical execution;
  \item a release-evidence ladder connecting shared fixtures, Rust
  computation, independent Haskell computation, and selected Lean theorems;
  \item a claim register that rejects production, safety, equivalence, and
  performance overstatements;
  \item adversarial examples showing why safe Rust, cross-language agreement,
  immutable artifacts, async frameworks, and successful WASM compilation do
  not establish database correctness; and
  \item a staged architecture and benchmark contract with falsification gates.
\end{enumerate}

\subsection{Nonclaims}

This paper does not claim that \CatDB{} is production-ready; that Rust proves
semantic correctness; that Lean verifies the Rust implementation; that
cross-language agreement proves general equivalence; that all three
functorial migrations are implemented; that any backend is connected; or that
the semantic layer is free at runtime. It does not report a performance
number.

\section{Background and related systems}
\label{sec:background}

\subsection{Categorical data migration is established prior art}

In the classic functorial account, a schema is a small category and an
instance is a set-valued functor. A schema mapping induces three data migration
functors commonly written \(\Sigma_F\), \(\Delta_F\), and
\(\Pi_F\)~\cite{spivak2012functorial}. Relational foundations connect this
language to executable relational operations and composition
results~\cite{spivak2015relational}. Algebraic data integration and algebraic
databases extend the treatment toward types, equations, queries, and practical
integration~\cite{schultz2017integration,schultz2016algebraic}.

This literature makes several aspects of \CatDB{} non-novel: categories as
schemas, functor-like mappings, path composition, and the existence of the
three data migration directions. Implementations also predate \CatDB{}.
CQL offers an executable categorical query and integration language and
explicitly distinguishes itself from a DBMS~\cite{cql}. Catlab provides finite
category presentations and attributed C-sets in Julia~\cite{catlab}.

The possible \CatDB{} contribution is therefore systems-specific. It would
need to show how versioned categorical semantics interact with storage
connectors, planning, materialization, provenance, workspaces, and
distribution, while comparing directly with existing categorical tools.
Reimplementing a small subset in Rust is useful infrastructure, not by itself
a new database model.

\subsection{Rust narrows some implementation risks, not semantic risk}

Rust's ownership discipline moves many lifetime and aliasing checks into
compilation~\cite{rustownership}. RustBelt gives a machine-checked safety
account for a realistic language subset and selected libraries while making
the obligations of unsafe extensions explicit~\cite{jung2018rustbelt}. These
results justify careful statements about language-level memory safety. They
do not imply that an arbitrary safe Rust program implements its intended
mathematics.

Cargo workspaces share resolution and a lockfile among members
~\cite{cargoworkspaces}. Serde can reject unknown fields in self-describing
formats through \code{deny\_unknown\_fields}~\cite{serdecontainer}. The current
kernel uses both mechanisms. Neither is a proof of protocol compatibility
across future IR versions.

\subsection{Physical execution has its own mature design space}

Volcano's operator interface and extensible dataflow architecture separate
mechanism from operator semantics~\cite{graefe1994volcano}. Cascades adds
rule-based transformation, memoization, and physical-property reasoning
~\cite{graefe1995cascades}. SQLite and PostgreSQL both expose cost-based
planning choices in their documentation~\cite{sqliteplanner,postgresplanner}.
Apache DataFusion is an extensible Rust query engine with logical and physical
optimizer rules and an Arrow-oriented execution architecture
~\cite{datafusion}.

Consequently, a future \CatDB{} compiler should not build an optimizer merely
to have one. It must identify the extra semantic properties that constrain
ordinary rewrites, feed those properties into a proven execution framework or
a justified custom engine, and measure the cost of doing so.

\subsection{Candidate technologies are not current features}

Tokio provides tasks, scheduling, asynchronous I/O, synchronization, and
runtime support~\cite{tokio}. Apache Arrow specifies a language-independent
columnar memory and IPC format~\cite{arrowformat}. WebAssembly specifies a
portable low-level code format~\cite{wasmcore}, and Wasmtime offers a Rust
embedding API~\cite{wasmtime}. These are credible candidates for a runtime
roadmap. None appears in the audited Cargo dependency graph.

\section{Evidence discipline}
\label{sec:evidence}

\subsection{Four distinct questions}

A runtime evaluation becomes clearer when it asks four questions separately:

\begin{enumerate}
  \item \textbf{Representation:} Can a value be decoded, encoded, and
  normalized under a closed contract?
  \item \textbf{Semantics:} Does the implementation validate or compute the
  intended operation?
  \item \textbf{Law:} Does a proof assistant establish a stated invariant in a
  specified formal representation?
  \item \textbf{Execution:} Does a backend plan preserve the semantic result,
  transaction, resource, and failure contracts?
\end{enumerate}

The accepted Slice 4 repository boundary has substantial evidence for the
first two, selected evidence for the third, and no evidence for the fourth.

\subsection{Claim labels}

\begin{longtable}{L{0.22\textwidth} L{0.70\textwidth}}
\toprule
Label & Interpretation in this paper \\
\midrule
\endfirsthead
\toprule
Label & Interpretation in this paper \\
\midrule
\endhead
\computational & Reproduced by executable code over a stated finite surface. \\
\machinechecked & Checked by Lean's kernel for named declarations only. \\
\prior & Established externally; not a CatDB result. \\
\enghyp & Plausible implementation proposition without current CatDB evidence. \\
\openclaim & Well-posed research question without a result. \\
\obstructed & Required component, experiment, or review does not exist. \\
\rejected & Contradicted by the live source or stronger than its evidence. \\
\nonclaim & Explicitly excluded from the result. \\
\bottomrule
\end{longtable}

\subsection{Accepted boundary and method}

The accepted source audit uses the Slice 4 acceptance commit
\begin{center}
\small\code{056915834fcc2f172a4a72efe3629f4f753e45cf}.
\end{center}
That commit closes Slices 1--4 and is the maximum code-evidence boundary used
for every computational claim in this paper. We enumerated every workspace
member and member manifest, resolved the dependency graph, read the
implementation and tests, traced accepted Slice 0--4 commits into the accepted
commit, and reran all accepted gates from an isolated archive. We also searched
the accepted manifests, lockfile, and Rust tree for names associated with the
proposed runtime subsystems. Later working-tree changes are outside the
evidence boundary and are neither counted nor characterized here.

This method prevents two common errors. First, a directory name or roadmap
entry is not implementation evidence. Second, a direct-name textual guard is
not a dependency proof when Cargo permits workspace aliases and inherited
dependencies. The resolved manifest graph is the relevant boundary.

\section{The implemented Rust kernel}
\label{sec:kernel}

\subsection{Workspace shape}

The root manifest declares exactly six members:

\begin{center}
\begin{tikzpicture}[
  node distance=8mm and 11mm,
  crate/.style={draw,rounded corners,fill=kernelblue,minimum width=31mm,
                minimum height=9mm,align=center,font=\small},
  arrow/.style={-{Latex[length=2mm]},thick}
]
\node[crate] (core) {\code{catdb-core}};
\node[crate,right=of core] (ir) {\code{catdb-ir}};
\node[crate,right=of ir] (schema) {\code{catdb-schema}};
\node[crate,below=of schema] (mapping) {\code{catdb-mapping}};
\node[crate,left=of mapping] (migration) {\code{catdb-migration}};
\node[crate,left=of migration] (cli) {\code{catdb-cli}};
\draw[arrow] (ir) -- (core);
\draw[arrow] (schema) -- (ir);
\draw[arrow] (mapping) -- (schema);
\draw[arrow] (mapping) -- (ir);
\draw[arrow] (migration) -- (mapping);
\draw[arrow] (migration) -- (schema);
\draw[arrow] (cli) -- (migration);
\draw[arrow,bend left=25] (cli) to (schema);
\draw[arrow,bend left=35] (cli) to (core);
\end{tikzpicture}
\end{center}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{r l l Y}
\toprule
Rank & Crate & Direct project dependencies & Implemented responsibility \\
\midrule
0 & \code{catdb-core} & none & IDs, scalar envelopes, diagnostic codes and phases \\
1 & \code{catdb-ir} & core & closed serialized IR and structural normalizers \\
2 & \code{catdb-schema} & core, IR & schema, path, and direct-equation validation \\
3 & \code{catdb-mapping} & core, IR, schema & total mapping validation, identity, composition \\
4 & \code{catdb-migration} & core, IR, schema, mapping & finite instance validation and bounded \(\Delta\) \\
9 & \code{catdb-cli} & all five & fixture verification and Rust/Haskell comparison \\
\bottomrule
\end{tabularx}
\caption{Accepted Slice 4 workspace. Rank is architectural reading order, not
a Cargo feature.}
\label{tab:workspace}
\end{table}

The workspace is version 0.1.0, uses Rust edition 2024, and declares an
Apache-2.0 license field. Its direct external dependencies are only Serde,
\code{serde\_json}, and \code{tempfile}. The full Rust source and test surface
contains 4,051 lines at the accepted Slice 4 commit.

\subsection{Core identifiers, scalars, and diagnostics}

The core crate defines a transparent string identifier, a closed scalar type
enumeration, scalar values, diagnostic codes, phases, and structured
diagnostics. Integers are signed 64-bit values at the IR boundary. Diagnostics
contain stable machine fields rather than using host exception prose as the
comparison contract.

This is a sensible kernel boundary. A parser can preserve a submitted JSON
Pointer and semantic references even when the human-readable rendering
changes. Independent implementations can compare the code, phase, pointer,
and references directly. However, the current identifier is not a compact
numeric runtime ID. The program's proposed ``numeric identifiers'' remain
\obstructed{}.

\subsection{Closed language-neutral IR}

The IR crate defines closed Serde values for schemas, paths, mappings,
instances, migration requests and outcomes, information-loss results, schema
diffs, and fixture envelopes. Named records deny unknown fields. Canonical
serialization sorts arrays only after input validation has had an opportunity
to observe duplicates and submitted positions.

\begin{contract}[Representation is not execution]
For every IR operation \(O\), the paper distinguishes a decoder
\(\mathsf{decode}_O\), a normalizer \(\Normalize_O\), a validator
\(\Validate_O\), and, when implemented, an evaluator \(\mathsf{eval}_O\).
Successful decoding or normalization does not imply successful validation or
evaluation.
\end{contract}

This contract catches a real boundary in the accepted source. The instance
normalizer orders carriers and assignments but does not validate them. The
loss and diff normalizers order supplied output structures but do not compute
loss or a diff. A well-formed output envelope can still make a false semantic
assertion if supplied by an untrusted caller.

\subsection{Finite schemas and typed paths}

The schema crate validates the current identifier syntax, duplicate
declarations, arrow endpoints, required attributes, and the parallel typing of
equation paths. A path carries a start object and a sequence of arrows.
Typing folds the arrows from the start object:

\[
  \operatorname{type}_S(A; f_1,\ldots,f_n)
  =
  \begin{cases}
    A \to A, & n=0,\\
    A \to B_n, & \operatorname{src}(f_1)=A
      \land \bigwedge_{i<n}\operatorname{tgt}(f_i)=
      \operatorname{src}(f_{i+1}),\\
    \mathsf{error}, & \text{otherwise.}
  \end{cases}
\]

Binary path composition requires the first path's target to equal the second
path's source and concatenates arrows in traversal order. Deterministic path
keys make canonical order independent of declaration order.

The equation boundary is deliberately small. The checker accepts syntactic
path equality or one directly declared target equation, with orientation
ignored. It does not compute the congruence generated by the equations.

\begin{counterexample}[Transitive equation]
Let the target schema declare \(p=q\) and \(q=r\). A mapped source equation
with images \(p\) and \(r\) is valid in the generated equivalence relation.
The direct checker need not accept it because no single declaration says
\(p=r\).
\end{counterexample}

\status{Schema and path behavior is \computational{} for the admitted fixture
profile. A complete equational decision procedure is \rejected{}.}

\subsection{Mappings}

A raw mapping contains:

\[
  F_0 : \operatorname{Obj}(S)\to\operatorname{Obj}(T),
  \qquad
  F_1(f) : \Path_T(F_0 A,F_0 B),
\]

together with attribute expressions in the current typed profile. The mapping
crate requires total object, arrow, and attribute assignments, checks endpoint
and scalar typing, and uses the bounded equation checker for preservation.
Identity mappings send each object to itself, each arrow to its singleton
path, and each attribute to its direct expression.

Composition substitutes object images, target paths, and attribute
expressions, then validates the result. This design means composition does not
silently bless a malformed intermediate value.

\begin{proposition}[Source-level mapping property]
For every mapping value returned successfully by the current identity or
composition functions, the implementation has rerun its bounded mapping
validator before returning.
\end{proposition}

\begin{proof}
This is a claim about the inspected call paths, not a mathematical theorem of
all Rust executions. The identity constructor builds a total mapping and calls
validation. The composition function validates both inputs, constructs the
substituted result, and validates that result before returning success.
\end{proof}

\status{\computational{} source and test evidence. The general categorical
laws belong to the separate Lean boundary described in
\cref{sec:crosslanguage}.}

\subsection{Finite instances}

The migration crate validates a closed, finite, total instance profile. A
carrier assigns a finite set \(I(A)\) to each schema object. Every arrow
\(f:A\to B\) is interpreted as a total function
\(I(f):I(A)\to I(B)\). Required attributes are total and typed. Path equations
are checked pointwise.

For a path \(p=f_1;\cdots;f_n\), evaluation is ordinary function
composition:

\[
  I(p)(x)=I(f_n)(\cdots I(f_2)(I(f_1)(x))\cdots).
\]

The validator checks exact schema identity, duplicate carrier and generator
records, carrier coverage, assignment coverage and totality, carrier
membership, scalar types, and equations. Error selection retains submitted
array positions in the shared diagnostic contract.

The profile excludes nulls, optional attributes, partial arrows, infinite
carriers, quotient representations, and richer value-domain operations. Those
are not defects hidden by the paper; they define the current admitted domain.

\subsection{Bounded pullback migration}

For a lawful mapping \(F:S\to T\) and a finite \(T\)-instance \(J\), pullback
migration is represented by precomposition:

\[
  \Delta_F(J)=J\circ F.
\]

On objects, the implementation selects \(J(F(A))\). On a source arrow, it
evaluates the mapped target path. On an attribute, it evaluates the admitted
path-then-attribute expression. The result is validated again before success.

\begin{example}[Path attribute]
Suppose \(S\) has \code{Order.customerEmail}, while \(T\) represents the same
value by the path
\code{Order.customer; Customer.email}. The admitted \(\Delta_F\) evaluator
follows the mapped relationship path and then reads the target attribute for
each source carrier element.
\end{example}

Only this finite pullback direction is implemented. Requests for
\(\Sigma_F\) and \(\Pi_F\) return exact unsupported outcomes. The code does not
perform a physical migration, create a table, open a transaction, cut over a
service, or roll back a failed deployment.

\status{\computational{} on thirteen migration fixtures: two successful finite
\(\Delta\) examples, nine validation failures, and two explicit unsupported
outcomes.}

\subsection{Fixture CLI}

The CLI exposes only fixture verification and Rust/Haskell comparison. It
supports capability sets \code{slice-1} and \code{slice-4}. The verifier:

\begin{enumerate}
  \item recursively enumerates JSON fixtures;
  \item closed-decodes and exact-round-trips each fixture;
  \item computes an actual Rust outcome for admitted operations;
  \item compares the computed result with the golden expected value;
  \item marks loss and diff as structural-only; and
  \item reports exact counts.
\end{enumerate}

The comparison command launches Cabal as a process in the Haskell package,
passes explicit tool paths when configured, receives a fresh temporary JSON
report, verifies the report identity and coverage, and compares each
independently computed semantic result.

This is a good research harness. It is not a reusable runtime API. It also
should not be exposed to hostile fixture trees without resolving the retained
symlink-traversal hardening note.

\section{Cross-language and formal evidence}
\label{sec:crosslanguage}

\subsection{Why three implementations?}

The research program uses one shared fixture corpus with three different
roles:

\begin{center}
\begin{tikzpicture}[
  node distance=14mm,
  box/.style={draw,rounded corners,minimum width=42mm,minimum height=12mm,
              align=center},
  arr/.style={<->,thick,{Latex[length=2mm]}-{Latex[length=2mm]}}
]
\node[box,fill=kernelblue] (rust) {Rust\\bounded kernel};
\node[box,fill=evidencegreen,right=of rust] (haskell) {Haskell\\semantic oracle};
\node[box,fill=roadmaporange,below=of $(rust)!0.5!(haskell)$] (lean) {Lean\\selected laws};
\draw[arr] (rust) -- node[above,font=\small]{computed JSON} (haskell);
\draw[arr] (rust) -- node[left,font=\small]{future bridge} (lean);
\draw[arr] (haskell) -- node[right,font=\small]{future bridge} (lean);
\end{tikzpicture}
\end{center}

Rust is the proposed production language. Haskell is an independent
executable semantic oracle. Lean is a proof representation for high-value
laws. The roles do not collapse into one another.

\subsection{Release-evidence ladder}

\begin{longtable}{r L{0.20\textwidth} L{0.30\textwidth} L{0.34\textwidth}}
\toprule
Slice & Artifact & Positive evidence & Retained boundary \\
\midrule
\endfirsthead
\toprule
Slice & Artifact & Positive evidence & Retained boundary \\
\midrule
\endhead
0 & closed fixture contract &
JSON Schema, manifest integrity, reference closure &
no semantic implementation \\
1 & Rust schema, path, and mapping kernel &
16 semantic and 8 structural cases in the original 24-case corpus &
direct equations only; no instance, query, or backend semantics \\
2 & independent Haskell oracle &
exact Slice 1 process-boundary agreement and bounded properties &
computational, not proof; no migration semantics in that slice \\
3 & Lean path and mapping kernel &
kernel checks for \code{PATH-02}, \code{PATH-03}, \code{PATH-04},
\code{MAP-03}, \code{MAP-04}, and \code{MAP-05} &
no Rust equivalence, parsing, migration, SQL, or systems theorem \\
4 & finite instances and \(\Delta\) &
accepted 33 cases: 29 semantic, four structural, zero disagreement &
no Sigma/Pi, physical execution, performance, or distribution \\
\bottomrule
\end{longtable}

The accepted implementation and acceptance commits for Slices 0--4 are
ancestors of the Slice 4 acceptance commit. The release records also retain failed
review rounds and nonblocking findings. Those code reviews are evidence for
the slices; they are not peer review of this manuscript.

\subsection{What differential agreement establishes}

Under capability set \code{slice-4}, both implementations closed-decode all
33 fixtures. They classify 29 as semantic and four as structural-only. On the
29 semantic cases, the fresh comparison reports zero disagreements.

\begin{proposition}[Finite differential result]
For the 29 fixture inputs in the accepted manifest that capability set
\code{slice-4} classifies as semantic, the fresh Rust and Haskell processes
emit equal machine-comparison JSON outcomes.
\end{proposition}

\status{\computational. The equality is finite and tied to the manifest
digest.}

This result is stronger than one implementation comparing itself with a
golden file. It can expose independent parsing, normalization, computation,
or diagnostic differences. It remains weaker than a correctness proof.

\begin{counterexample}[Shared defect]
If both implementations apply the same mistaken ordering rule to equations,
they agree exactly and are both wrong. The Slice 4 history contains a concrete
variant: derived Haskell ordering once disagreed with the normative serialized
path key, and the fixture boundary had to expose and repair it.
\end{counterexample}

\subsection{What Lean establishes}

The separate Lean slice defines indexed typed paths, identity and composition,
typed schema mappings, and lawful mapping composition. Kernel evidence applies
exactly to the six named invariant IDs. It does not parse the JSON fixture
language, reproduce Rust diagnostics, validate finite instances, or compute
\(\Delta\). There is no refinement proof connecting a Rust value to the Lean
representation.

Therefore, the statement ``Lean verifies CatDB's Rust runtime'' is
\rejected{}. The accurate statement is that Lean machine-checks selected
abstract path and mapping laws relevant to the runtime design.

\section{Fresh accepted reproduction}
\label{sec:reproduction}

\subsection{Toolchain and isolation}

The accepted run used Rust 1.94.0, Cargo 1.94.0, Python 3.12.9, Cabal
3.16.1.0, and GHC 9.14.1. Commit \code{0569158} was extracted with
\code{git archive}; build state and captured output were placed in fresh
temporary directories. Existing release evidence was not overwritten.
Explicit Homebrew Cabal and GHC paths avoided obsolete tools elsewhere on the
host.

\subsection{Commands}

\begin{lstlisting}[language=bash]
python3 scripts/validate-fixtures.py \
  --schema fixtures/schema-v1.schema.json \
  --cases fixtures/cases
python3 scripts/audit-fixture-manifest.py fixtures/manifest-v1.json
python3 -m unittest discover -s scripts/tests -p 'test_*.py'

cargo fmt --all --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace --all-features

cargo run -p catdb-cli -- fixtures verify fixtures/cases \
  --implementation rust --capability-set slice-1
cargo run -p catdb-cli -- fixtures verify fixtures/cases \
  --implementation rust --capability-set slice-4

CATDB_CABAL=/opt/homebrew/bin/cabal \
CATDB_GHC=/opt/homebrew/bin/ghc \
cargo run -p catdb-cli -- fixtures compare fixtures/cases \
  --left rust --right haskell --capability-set slice-4
\end{lstlisting}

\subsection{Results}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{Y r r r}
\toprule
Gate & Semantic & Structural & Failure/disagreement \\
\midrule
Fixture schema and manifest & \multicolumn{2}{c}{33 closed cases} & 0 \\
Rust \code{slice-1} on accepted corpus & 16 & 17 & 0 \\
Rust \code{slice-4} & 29 & 4 & 0 \\
Rust/Haskell \code{slice-4} & 29 & 4 & 0 \\
\bottomrule
\end{tabularx}
\caption{Fresh accepted Slice 4 fixture results. The corpus has 12 successful,
19 error, and two unsupported expected outcomes.}
\label{tab:fresh}
\end{table}

The Python suite ran 19 tests. The Rust workspace ran 26 test functions with
no failure or ignored test. Formatting and Clippy with warnings denied passed.
The explicit cross-language path built Haskell and succeeded, but emitted
Haddock missing-documentation warnings. This paper describes the semantic
comparison as successful, not the entire command as warning-free.

\subsection{Why counts are part of the claim}

Reporting only ``all tests pass'' hides capability boundaries. The accepted
\code{slice-1} runner structurally round-trips seventeen cases that it does
not evaluate. The \code{slice-4} runner still has four structural-only cases:
two information-loss and two schema-diff fixtures. Those four are not
semantically evaluated. Totals must be derived from the accepted manifest
rather than frozen as magic numbers.

\section{Runtime claims the code does not support}
\label{sec:negative}

\subsection{Negative dependency and source audit}

At the accepted Slice 4 boundary, the resolved workspace has only Serde,
\code{serde\_json}, and \code{tempfile} as external
dependencies. The manifest, lockfile, and Rust crate tree contain no
occurrence of the
runtime technologies or components \code{tokio}, \code{sqlx},
\code{rusqlite}, PostgreSQL bindings, \code{wasmtime}, service frameworks,
planner, connector, server, storage, replica, or distributed runtime terms.
No \code{async} or \code{await} appears. The absence audit does not prove that
future code cannot implement these components; it establishes that this
snapshot does not.

\begin{landscape}
\begin{longtable}{L{0.25\linewidth} L{0.20\linewidth} L{0.45\linewidth}}
\toprule
Program claim & Current status & Evidence required before promotion \\
\midrule
\endfirsthead
\toprule
Program claim & Current status & Evidence required before promotion \\
\midrule
\endhead
compact semantic IR & \computational, bounded &
profile versioning plus serialization, memory, and lookup baselines \\
numeric identifiers & \rejected &
implemented interning and stable external-identity contract \\
immutable compiled schemas & \obstructed &
compiled artifact type, dependency digest, concurrency and invalidation tests \\
Rust trait boundaries & \obstructed &
connector, planner, and executor traits with compatibility tests \\
async execution & \obstructed &
runtime dependency plus cancellation, backpressure, and blocking-I/O tests \\
SQLite execution & \obstructed &
connector, lowering, transaction, and differential-query evidence \\
PostgreSQL execution & \obstructed &
capability negotiation, dialect, transaction, and differential evidence \\
logical and physical planning & \obstructed &
operator IR, rewrites, physical properties, and result-preservation tests \\
plan caching & \obstructed &
complete cache key, invalidation rules, and stale-plan counterexamples \\
deterministic operation replay & \obstructed &
operation algebra, log, state machine, crash and reorder tests \\
WASM compatibility & \obstructed &
target build, host contract, supported-feature matrix, and measurements \\
embedded deployment & \obstructed &
stable embedding API and reference application \\
server deployment & \obstructed &
protocol, service, authentication, resource and failure tests \\
native-equivalent performance & \obstructed &
pre-registered native SQL comparison with raw observations \\
distributed runtime & \obstructed &
replication implementation and convergence/consistency evidence \\
\bottomrule
\end{longtable}
\end{landscape}

\subsection{``Compact'' and ``immutable'' need operational definitions}

The serialized IR is small in conceptual scope, but no measurement compares
its heap footprint, decode time, lookup cost, or compiled representation with
a baseline. Calling it compact without a metric is \openclaim{}.

Likewise, source values can be treated immutably while a cache points to the
wrong revision. A production compiled artifact should bind at least:

\[
  k =
  H(s,m,c,v,p,b),
\]

where \(s\) is the schema revision, \(m\) the mapping revision, \(c\) the
backend capability profile, \(v\) scalar and collation semantics, \(p\) policy,
and \(b\) compiler build. Omitting one dependency can yield a perfectly
immutable stale plan.

\subsection{No physical execution}

The current \(\Delta\) evaluator operates on finite JSON-shaped in-memory
instances. It does not translate a mapping to SQL. No transaction is opened.
No source capability is negotiated. No cursor, prepared statement, index, or
network connection exists. Accordingly, ``storage-independent execution'' is
a program objective, not a Paper 15 result.

\subsection{No performance evidence}

The fixture suite checks exact results and diagnostics. It does not time the
kernel under a controlled benchmark protocol. The repository has no native
SQL baseline because it has no SQL execution path. The central claim that the
semantic layer can stay outside the hot path remains testable but
\obstructed{}.

\section{Rust safety without category errors}
\label{sec:safety}

\subsection{First-party source observation}

No \code{unsafe} block occurs in the current CatDB crate source. This is a
useful local observation. It is not a whole-program or supply-chain theorem:
the standard library, compiler, operating system, and transitive dependencies
are outside that scan. Future database connectors may introduce FFI.

\subsection{Three kinds of correctness}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.20\textwidth} Y Y}
\toprule
Kind & Example failure & Relevant evidence \\
\midrule
Memory safety & use-after-free in a connector buffer & Rust type system, unsafe audit, fuzzing, dependency review \\
Semantic correctness & cents mapped as dollars & fixtures, differential evaluator, proof or refinement bridge \\
Database correctness & partial target update after failure & transaction tests, isolation model, fault injection \\
\bottomrule
\end{tabularx}
\caption{Different correctness obligations require different evidence.}
\end{table}

\begin{counterexample}[Safe Rust, wrong semantics]
A total safe Rust function copies an integer amount without applying the
mapping's scale conversion. It has no dangling pointer and can pass every
memory-safety check while returning the wrong business value.
\end{counterexample}

\begin{counterexample}[Correct mapping, unsafe cutover]
A future connector computes every mapped row correctly but commits half the
target tables before a process crash. Semantic validity does not establish
transaction atomicity or recovery behavior.
\end{counterexample}

\subsection{Panic and denial-of-service boundaries}

The inspected migration implementation uses internal \code{expect} calls only
after validation establishes the assumed lookup. That pattern can be
reasonable, but this paper does not claim panic freedom. A hostile input tree,
pathological allocation request, dependency bug, or violated future invariant
can still matter. Production gates should include fuzzing, allocation limits,
panic policy, and resource-exhaustion tests.

\section{Adversarial counterexamples}
\label{sec:counterexamples}

This section collects cases that a production architecture must answer before
promoting a claim.

\begin{counterexample}[Agreement is not truth]
Rust and Haskell share a mistaken interpretation of a scalar date. All 29
fixtures avoid the disputed date, so exact agreement remains zero-disagreement
while both implementations fail on the next input.
\end{counterexample}

\begin{counterexample}[Diagnostic equivalence is not general]
The accepted Slice 4 release records two unfixtured multi-fault cases in which Rust and
Haskell may select different first diagnostics. The admitted 33-case
comparison remains true, but general diagnostic equivalence does not follow.
\end{counterexample}

\begin{counterexample}[Accepted Slice 4 structural loss result]
A caller supplies a well-formed information-loss envelope containing an empty
finding list for a many-to-one mapping. At the accepted Slice 4 boundary, the
IR can normalize the envelope; no loss analyzer recomputes whether the
assertion is true.
\end{counterexample}

\begin{counterexample}[Stale capability plan]
A SQLite backend revision stops supporting a collation-preserving pushdown.
If the plan cache key omits the capability revision, the immutable old plan is
reused and returns a different order or comparison result.
\end{counterexample}

\begin{counterexample}[Cancellation without cleanup]
A future federated request times out while a blocking driver call continues on
a worker thread and holds a database connection. Selecting an async runtime
does not define cancellation, cleanup, or source-side interruption.
\end{counterexample}

\begin{counterexample}[WASM target mismatch]
The semantic crates compile for
\code{wasm32}-\code{unknown}-\code{unknown}, but the selected
SQLite connector requires filesystem and native-thread behavior unavailable in
the host. Compilation of a subset is not deployment compatibility.
\end{counterexample}

\begin{counterexample}[Identifier compression changes meaning]
A compiled artifact replaces stable external identifiers with small integers.
After a schema rebuild, integer 17 names a different object. Reusing a plan by
numeric ID alone applies the old mapping to the new object.
\end{counterexample}

\begin{counterexample}[Fast wrong benchmark]
A benchmark compares native SQL with provenance disabled against CatDB output
that omits required provenance fields. Lower latency is achieved by changing
the requested result contract, so the comparison is invalid.
\end{counterexample}

\section{A falsifiable production architecture}
\label{sec:architecture}

\subsection{Separate source, validated, compiled, and physical values}

The proposed runtime should expose four artifact kinds rather than one
overloaded IR:

\[
\boxed{
\begin{array}{c}
\text{source schema and mapping}\\
\downarrow\ \Validate\\
\text{validated semantic artifact}\\
\downarrow\ \Compile_{\Capabilities}\\
\text{backend-independent logical artifact}\\
\downarrow\\
\text{backend-specific physical artifact}
\end{array}}
\]

A source value preserves user evidence and diagnostic positions. A validated
value carries a successful profile and dependency set. A logical artifact
contains normalized operators and semantic obligations. A physical artifact
contains a backend choice, pushed operations, residual operations, parameters,
and a result-reconciliation contract.

\begin{requirement}[No unvalidated constructor path]
Every public function that produces a validated, logical, or physical artifact
must either validate its source inputs or accept only an opaque value whose
constructor already did so.
\end{requirement}

\subsection{Compiled schema representation}

Numeric interning can reduce lookup and storage costs, but external semantic
identity must remain stable. One possible structure is:

\[
  \mathsf{CompiledSchema} =
  (\mathit{sourceDigest}, \mathit{objects}, \mathit{arrows},
   \mathit{attributes}, \mathit{equations}, \mathit{indexes}),
\]

where every numeric ID is local to \(\mathit{sourceDigest}\). Serialization of
an ID without its artifact identity should be rejected.

Compilation should precompute path endpoint tables, attribute-domain tables,
equation-normal-form data for the declared fragment, dependency edges, and
backend-independent statistics. Whether that representation is actually
compact is a measurement question.

\subsection{Trait boundaries}

Rust traits are useful only after their semantic contracts are fixed. A
connector boundary needs more than methods named \code{scan} and \code{join}.
It must expose typed capabilities:

\[
\begin{aligned}
  \Capabilities(B) = (&\text{operators},\text{scalar semantics},
  \text{collation},\text{transactions},\\
  &\text{limits},\text{freshness},\text{failure modes}).
\end{aligned}
\]

A planner may push an operator only when the backend capability witness and
the mapping obligations establish equivalence for the request. Unsupported
work must remain residual or make the plan infeasible.

\subsection{Logical and physical planning}

Conventional logical operators---scan, project, filter, join, aggregate,
union, sort, limit---remain appropriate. \CatDB{} adds metadata rather than
replacing the algebra:

\begin{itemize}
  \item schema and mapping revision dependencies;
  \item path and equation obligations;
  \item identity and reconciliation policy;
  \item provenance requirements;
  \item allowed information loss or approximation;
  \item source authority and update policy; and
  \item result freshness and consistency.
\end{itemize}

These properties constrain transformations. They do not eliminate cost-based
planning. Volcano, Cascades, SQLite, PostgreSQL, and DataFusion remain the
proper baseline family.

\subsection{Plan caching}

A cache entry should record:

\begin{align*}
\mathsf{PlanKey} = H(&\mathsf{LogicalQuery},
\SchemaRev,\MappingRev,\CapabilitiesRev,\\
&\mathsf{ScalarProfile},\mathsf{PolicyRev},
\mathsf{CompilerRev}).
\end{align*}

The result should carry the key and the proof obligations discharged during
lowering. A cache hit is valid only when every dependency is identical or an
explicit compatibility relation has been established.

\subsection{Asynchronous execution}

An async executor requires a contract before an implementation:

\begin{itemize}
  \item parent and child cancellation propagation;
  \item timeout ownership and source-side interruption;
  \item bounded queues and backpressure;
  \item isolation of blocking drivers;
  \item transaction and connection lifetime;
  \item partial-result policy;
  \item deterministic error aggregation; and
  \item provenance for retries and fallback.
\end{itemize}

Tokio is a plausible mechanism, not the contract itself. The runtime should
test cancellation at every await and blocking boundary.

\subsection{Embedded, server, and WASM modes}

Embedded and server deployments expose different failure, trust, and resource
boundaries. They should not be one compile-time flag described as equivalent.
Similarly, WASM compatibility should be reported by feature set:

\begin{longtable}{L{0.28\textwidth} L{0.29\textwidth} L{0.34\textwidth}}
\toprule
Target & Required test & Example limitation \\
\midrule
\endfirsthead
\toprule
Target & Required test & Example limitation \\
\midrule
\endhead
native embedded kernel & library API and host integration & process shares caller resources \\
native server & protocol, auth, quotas, crash recovery & network and tenancy boundary \\
browser WASM & compile, instantiate, deterministic fixture run & no native DB driver \\
WASI component & component interface and allowed host calls & capability and filesystem policy \\
embedded Wasmtime plugin & host import/export and resource limits & runtime and sandbox configuration \\
\bottomrule
\end{longtable}

\section{Implementation roadmap}
\label{sec:roadmap}

\subsection{R1: stabilize the semantic kernel}

The next accepted semantic release should version the IR, define compatibility
rules, expand generative and mutation testing, replace the direct-equation
checker with either a declared decidable fragment or explicit proof
obligations, and implement reviewed information-loss and schema-diff analyses.

Exit gate:

\begin{itemize}
  \item compatibility fixtures across at least two IR versions;
  \item fuzz and mutation reports;
  \item expanded Rust/Haskell properties with adversarial multi-fault cases;
  \item exact Lean theorem coverage and audited translations; and
  \item no semantic claim based only on normalizing a supplied result.
\end{itemize}

\subsection{R2: compiled artifact}

Introduce a validated source value and a compiled schema value with local
numeric interning. Bind every compiled value to content digests and a compiler
revision. Measure memory, serialization, lookup, and compile time against the
current string-keyed IR.

Exit gate: deterministic compilation, stale-artifact rejection fixtures, and
published raw size and timing observations.

\subsection{R3: SQLite reference backend}

SQLite is a useful first backend because it supports embedded evaluation and a
well-documented planner. The implementation should lower a deliberately small
logical subset, preserve bound parameters, use explicit transactions, and
compare every result with a direct native SQL baseline.

Exit gate:

\begin{itemize}
  \item schema creation and reflection contract;
  \item typed projection, selection, and join lowering;
  \item transaction failure and rollback tests;
  \item collation and null-semantics matrix;
  \item \code{EXPLAIN QUERY PLAN} capture; and
  \item differential row and provenance results.
\end{itemize}

\subsection{R4: PostgreSQL and capability negotiation}

PostgreSQL should not be treated as ``SQLite over a socket.'' Its type,
collation, isolation, prepared-statement, extension, and planner behavior
deserve an explicit capability profile. The connector should prove that every
pushed expression lies inside that profile.

Exit gate: dialect and capability fixtures, transaction/isolation tests,
prepared-plan invalidation, and differential results against native SQL.

\subsection{R5: planner, cache, and async executor}

Only after two backends expose real differences should a planner choose among
pushdown, local execution, or materialization. Add a complete plan key and
stale-plan tests before claiming cache reuse. Add asynchronous execution after
cancellation and backpressure semantics are specified.

Exit gate: forced alternative plans with equal results, cache invalidation
counterexamples, deterministic fault injection, and resource-bound tests.

\subsection{R6: deployment and replay}

Embedded, server, and WASM profiles should be separately supported. Operation
replay begins with an operation algebra that states idempotence, order,
authority, and conflict rules; deterministic fixture ordering is not a replay
system.

Exit gate: target build matrix, API compatibility, crash/restart traces,
operation permutations, and linkage to the distributed consistency papers.

\section{Benchmark and evaluation contract}
\label{sec:benchmark}

\subsection{Semantic compilation}

Measure decode, validation, normalization, mapping composition, finite
instance validation, \(\Delta\), and compilation separately. Independent
variables should include:

\begin{itemize}
  \item objects, arrows, attributes, and equations;
  \item path length and equation-fragment complexity;
  \item mapping fan-out and composition depth;
  \item carrier cardinality and assignment count; and
  \item valid versus invalid inputs, including diagnostic position.
\end{itemize}

Report median, tail, distribution, and allocation behavior. Do not infer
asymptotic complexity from the 33 golden fixtures.

\subsection{Backend execution}

For each backend query, compare:

\begin{enumerate}
  \item direct native SQL;
  \item CatDB-compiled SQL with semantic checks disabled after compilation;
  \item cold CatDB compilation plus execution;
  \item warm cached plan execution;
  \item local residual processing;
  \item materialized execution; and
  \item provenance-enabled execution.
\end{enumerate}

All alternatives must bind the same logical query, schema/mapping revisions,
scalar semantics, and result contract. Native baselines should use equivalent
indexes and parameters. Query text, physical plan, data generator, result
digest, and raw timing data must be retained.

\subsection{Falsification}

The ``outside the hot path'' hypothesis is falsified if steady-state execution
requires categorical interpretation per row or if semantic indirection adds
material overhead that cannot be compiled or amortized for the target
workload. The broader performance claim is falsified if CatDB changes results,
omits required provenance, compares different transaction guarantees, or
hides compilation and cache-maintenance costs.

\subsection{Suggested matrix}

\small
\begin{longtable}{L{0.17\textwidth} L{0.18\textwidth} L{0.20\textwidth} L{0.30\textwidth}}
\toprule
Question & Baseline & Metric & Required evidence \\
\midrule
\endfirsthead
\toprule
Question & Baseline & Metric & Required evidence \\
\midrule
\endhead
IR compactness & current JSON/string IR & bytes, allocations, decode/lookup time & raw profiles and artifact digests \\
validation scale & schema, path, and mapping functions & time and peak memory by size & generators and raw samples \\
\(\Delta\) scale & direct reference evaluator & time and memory by carrier/path size & equal result digests \\
compile overhead & direct SQL preparation & cold/warm latency & compile and cache-key traces \\
native preservation & hand-written SQL & latency, throughput, plan shape & equal semantics and indexes \\
connector overhead & native driver & CPU, allocations, transfer bytes & same transaction and result \\
provenance cost & provenance-off CatDB & latency, bytes, storage & same rows plus declared evidence \\
cancellation & native cancellation & cleanup time and leaked resources & fault-injection trace \\
WASM feasibility & native embedded kernel & size, startup, supported fixtures & host and feature matrix \\
\bottomrule
\end{longtable}
\normalsize

\section{Claim register}
\label{sec:claims}

\small
\begin{longtable}{L{0.10\textwidth} L{0.43\textwidth} L{0.17\textwidth} L{0.15\textwidth}}
\toprule
ID & Claim & Status & Basis \\
\midrule
\endfirsthead
\toprule
ID & Claim & Status & Basis \\
\midrule
\endhead
P15-C01 & The workspace has six CatDB crates. & \computational & manifest audit \\
P15-C02 & Named IR records reject unknown fields. & \computational & source/tests \\
P15-C03 & Schema/path validation covers Slice 1 fixtures. & \computational & fixture run \\
P15-C04 & General equational reasoning is complete. & \rejected & direct checker \\
P15-C05 & Mapping identity and composition exist in Rust. & \computational & source/tests \\
P15-C06 & Selected abstract path/mapping laws are checked. & \machinechecked & Slice 3 \\
P15-C07 & Lean verifies the Rust implementation. & \rejected & no bridge \\
P15-C08 & Finite instance validation exists for the profile. & \computational & Slice 4 \\
P15-C09 & Finite pullback \(\Delta\) exists for the profile. & \computational & 13 fixtures \\
P15-C10 & Sigma and Pi are implemented. & \rejected & unsupported \\
P15-C11 & Rust/Haskell agree on 29 semantic fixtures. & \computational & fresh compare \\
P15-C12 & Rust/Haskell are generally equivalent. & \rejected & finite corpus \\
P15-C13 & An async executor exists. & \obstructed & absent source \\
P15-C14 & SQLite/PostgreSQL connectors exist. & \obstructed & absent source \\
P15-C15 & A planner and plan cache exist. & \obstructed & absent source \\
P15-C16 & A server exists. & \obstructed & absent source \\
P15-C17 & WASM deployment is supported. & \obstructed & no build evidence \\
P15-C18 & Deterministic operation replay exists. & \obstructed & no operation engine \\
P15-C19 & Native performance is preserved. & \obstructed & no benchmark \\
P15-C20 & Safe Rust limits classes of memory error. & \prior & Rust literature \\
P15-C21 & First-party crate source has no unsafe block. & \computational & source search \\
P15-C22 & Whole-program memory safety is proved. & \rejected & no such proof \\
P15-C23 & Semantics can stay outside the hot path. & \enghyp & future benchmark \\
P15-C24 & Immutable compiled schemas improve reuse. & \enghyp & future artifact \\
P15-C25 & CatDB is production-ready. & \rejected & research kernel \\
\bottomrule
\end{longtable}
\normalsize

\section{Limitations and threats to validity}
\label{sec:limitations}

\subsection{Small, curated corpus}

The accepted thirty-three fixtures are enough to make a semantic boundary
executable, not
enough to characterize a database runtime. The corpus is curated and
hand-computable. It does not sample large schemas, deep equations, hostile
documents, high-cardinality instances, concurrent use, or backend behavior.

\subsection{Non-independent requirements}

The repository authors designed the fixture contract and implementations. The
Haskell process is independently coded but follows the same written contract.
Shared specification errors remain possible. External paper review has not
run.

\subsection{Separate formal model}

Lean coverage is exact but narrow. Without a verified translation or
refinement proof, a theorem about the Lean mapping representation cannot be
silently transferred to Serde decoding, Rust diagnostics, or the migration
evaluator.

\subsection{Snapshot drift}

This paper records one accepted commit. Other agents were working in the
repository during the broader program, so the live working tree is not an
evidence substitute. Paper 15 review and reproduction must remain pinned to
the Slice 4 acceptance commit.

\subsection{No security or performance study}

No threat model, fuzz campaign, supply-chain audit, memory profile, or backend
benchmark is reported. The absence of first-party unsafe blocks is neither a
security certification nor a performance result.

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

\begin{enumerate}
  \item Which decidable equation fragment offers sufficient modeling power
  without making compilation unpredictable?
  \item How should source-level stable identifiers relate to compiled numeric
  IDs across schema versions?
  \item Can a small logical operator set represent categorical obligations
  without embedding a theorem prover in the executor?
  \item Which semantic properties should be proven during compilation and
  which should remain runtime checks?
  \item Can a refinement bridge relate Lean lawful mappings to serialized Rust
  values without formalizing Serde or the entire engine?
  \item When should CatDB reuse DataFusion or native database optimizers instead
  of building a custom executor?
  \item How should capability negotiation represent collation, nulls, decimal
  rounding, time zones, and approximate vector semantics?
  \item What cache dependencies are sufficient for safe plan reuse?
  \item Can cancellation and provenance be made compositional across connector
  boundaries?
  \item Which WASM profile is useful when native database drivers are absent?
  \item How should deterministic local computation interact with distributed
  operation ordering and reconciliation?
  \item What workload would falsify the claim that semantic compilation is
  outside the hot path?
\end{enumerate}

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

\CatDB{} does not yet have the production Rust runtime described by its full
program. It has something smaller and worth preserving: a six-crate semantic
kernel with a closed fixture contract, exact diagnostics, finite schema and
mapping operations, finite instance validation, and bounded pullback
migration. On the accepted 33-case corpus, Rust computes 29 semantic outcomes,
and an independent Haskell process agrees on all 29. Selected path and mapping
laws are machine-checked in a separate Lean representation.

The boundary is as important as the positive result. The equation checker is
incomplete. Sigma and Pi are unsupported. Information loss and schema diff are
represented but not computed at the accepted boundary. No
query planner, connector, transaction layer, async executor, server, WASM
deployment result, replay engine, or benchmark exists. Rust's language
discipline does not prove CatDB semantics, and differential agreement does not
prove general equivalence.

The next credible step is not to call the kernel production-ready. It is to
stabilize and version the semantic contract, create a compiled artifact with
complete dependency keys, add one transactional SQLite backend, compare
compiled results with native SQL, and retain every negative case. Only then
can the central systems hypothesis be tested: whether categorical semantics
can guide compilation while remaining outside the hot execution path.

\appendix

\section{Audited source digests}
\label{app:hashes}

\begin{longtable}{L{0.43\textwidth} L{0.49\textwidth}}
\toprule
Artifact & SHA-256 \\
\midrule
\endfirsthead
\toprule
Artifact & SHA-256 \\
\midrule
\endhead
\code{Cargo.toml} & \hash{8d639b43fd8806b8b8a5341c86af626d95cc2bb68ed85d9074c1722caea40a34} \\
\code{Cargo.lock} & \hash{117abb87d3ec22ebfd2ce0f97f80f373b72043601b79464fb259de192c2b9643} \\
\code{catdb-core/src/lib.rs} & \hash{119cfdc5d4947b2b05f0bf4e41c842ed87f463717c2596bac1b55d306b3556cd} \\
\code{catdb-ir/src/lib.rs} & \hash{adb3bc7c2fe83ad90a377b49b778de224c340ae65ee899f6353597fe5cb478cc} \\
\code{catdb-schema/src/lib.rs} & \hash{e0560ee95f3de2a2b19936dd53e1f163b02b47c0300eb7fd58169cb58614cd84} \\
\code{catdb-mapping/src/lib.rs} & \hash{8843a40f83b7e6aeb8d33f607e2cc0f30b41aa8be0fffe5e3ae5304df314db5a} \\
\code{catdb-migration/src/lib.rs} & \hash{cd447b21bfeeb237930a323902e851aedecdf278deb2589260d3d285321c944d} \\
\code{catdb-cli/src/main.rs} & \hash{84d661be4b186085b32bcb15a0d1b77f2b13b7b8a7781c2276aacaa1327abdb2} \\
\code{fixtures/manifest-v1.json} & \hash{a817c292e879dcd8eb8f5ec2143dd0029464fde66925cdc8374ce9a599046f54} \\
\code{fixtures/schema-v1.schema.json} & \hash{c00a67aa806c2d28f18c9ed2133870fd75c4494c82951124189d92937f48fba8} \\
\bottomrule
\end{longtable}

\section{Fresh verification log digests}

\begin{longtable}{L{0.38\textwidth} L{0.54\textwidth}}
\toprule
Log & SHA-256 \\
\midrule
\endfirsthead
\toprule
Log & SHA-256 \\
\midrule
\endhead
fixture validator & \hash{96ecc0c1bad6cab3dfe80329a5a3d835c48d57ee781dc5d3737f1eed8c4d4c79} \\
manifest audit & \hash{57d0ab5c2024ca07085c148144bf81eaa67f781f7868c671a2897bad777b31fe} \\
Python tests & \hash{d238d441d1595dacce99a6b5e49c2b9645e5e548f19d16f7a79b0f50b31cfc02} \\
Cargo format & \hash{e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855} \\
Cargo Clippy & \hash{ef28b05c6ac3fd38cfe705b3b871c8e9882901131ea76a7718a1eed898cadfbf} \\
Cargo tests & \hash{8b3477cbb51c6ab66ee9b0da8d584bd8629d417b41961423b3edb8d922cf5519} \\
Rust Slice 1 & \hash{712ef20b795309ef1075d24285fa376f15089ae531b978b1db91c92278b7f36d} \\
Rust Slice 4 & \hash{1a88813b6fff79101fdb01bf81cc015cb4bf05b4b9c203c4c476d2b951a7fe06} \\
cross-language Slice 4 & \hash{3b85deb889761c77f032a8af8c349d2194c4366453cc2fbdd4cfff19e9ddcc92} \\
\bottomrule
\end{longtable}

\section{Review checklist}

Before this manuscript can move beyond provisional status, the program
requires:

\begin{itemize}
  \item one categorical/database domain reviewer;
  \item one database-systems reviewer;
  \item one adversarial reviewer;
  \item one code reviewer tied to the paper's exact source claims;
  \item one reproducibility reviewer;
  \item one citation auditor;
  \item one human-readable editor;
  \item one mathematical typesetting reviewer; and
  \item a final build and page-by-page visual inspection at the accepted
  source commit.
\end{itemize}

No accepted PDF or cover is produced by this provisional workstream.

\bibliographystyle{plainnat}
\sloppy
\Urlmuskip=0mu plus 1mu\relax
\bibliography{references}

\end{document}
