\documentclass[12pt]{article}

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

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={A Haskell Reference Semantics for CatDB Schema Mappings},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{protocol}[theorem]{Protocol}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
\newtheorem{counterexample}[theorem]{Counterexample}

\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\accepted}{{\normalfont\textsc{accepted computational}}}
\newcommand{\reproduced}{{\normalfont\textsc{live reproduced}}}
\newcommand{\later}{{\normalfont\textsc{later evidence}}}
\newcommand{\candidate}{{\normalfont\textsc{unreviewed candidate}}}
\newcommand{\structural}{{\normalfont\textsc{structural-only}}}
\newcommand{\nonclaim}{{\normalfont\textsc{nonclaim}}}
\newcommand{\openclaim}{{\normalfont\textsc{open}}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Evidence status.} #1.}\par}
\newcommand{\Ob}{\mathsf{Ob}}
\newcommand{\Arr}{\mathsf{Arr}}
\newcommand{\Attr}{\mathsf{Attr}}
\newcommand{\Eqn}{\mathsf{Eq}}
\newcommand{\Path}{\mathsf{Path}}
\newcommand{\Actual}{\mathsf{actual}}
\newcommand{\Expected}{\mathsf{expected}}
\newcommand{\Eval}{\mathsf{eval}}
\newcommand{\Norm}{\mathsf{norm}}
\newcommand{\DirectEq}{\mathrel{\equiv_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{haskellblue}{RGB}{229,237,250}
\definecolor{rustorange}{RGB}{252,235,216}
\definecolor{fixturegreen}{RGB}{230,244,230}
\definecolor{limitred}{RGB}{250,229,229}
\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-haskell\quad
       [\,cs.DB, cs.PL\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{A Haskell Reference Semantics for \CatDB{} Schema Mappings:\\
Bounded Laws, Closed Fixtures, and a Rust Comparison}
\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 Result status: \accepted{} at source \code{abd655f}}
\end{center}

\begin{abstract}
An executable reference model is useful only when its authority and limits are
visible. This paper reports the accepted Slice 2 Haskell reference for
\CatDB{}, a research system for typed, versioned schema mappings. The program
models a finite profile of schemas, typed paths, and total schema mappings. It
validates names, endpoints, map totality, attribute types, and direct
equation-preservation obligations; constructs identity mappings; and composes
mappings by path substitution. Its fixture codec rejects unknown fields and
round-trips every accepted JSON document exactly.

The result is tied to one reviewed source revision and one 24-case corpus. The
Haskell program independently computed 16 semantic outcomes: three schema
parsing, three path typing, two path composition, two identity mapping, and
six mapping composition cases. Eight migration, information-loss, and
schema-diff cases were decoded and round-tripped but explicitly reported as
structural-only with no semantic output. Seven deterministic QuickCheck
properties completed 1,550 successful trials over bounded linear-schema
generators. A Rust process separately computed the same 16 outcomes, both
implementations passed their own golden checks, and the comparator reported
zero disagreements. An independent review of the exact source range found no
blocker or major issue and issued a pass verdict. An isolated author rerun
reproduced the accepted Haskell JSON byte-for-byte.

The evidence is computational, not deductive. The accepted equality procedure
uses syntactic equality plus one directly declared equation; the property
generators are narrow; and the accepted package had reproducibility and
temporary-file hardening gaps. Later repository work adds finite instance
validation and bounded pullback migration, but it does not retroactively widen
this result. A still later working-tree candidate adds information-loss and
schema-diff analysis, but it remains uncommitted and unreviewed. This paper
claims no full migration semantics, query semantics, backend execution,
distributed behavior, performance result, general Rust/Haskell equivalence
theorem, or proof of a categorical law.
\end{abstract}

\tableofcontents

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

\subsection{What an oracle must not conceal}

Suppose a schema mapping sends a source arrow to a two-step path in a target
schema. A production compiler and a small reference program both return the
same normalized JSON. That agreement is encouraging, but it leaves several
questions open. Did the reference program actually traverse the path, or did
it copy the fixture's expected result? Did both programs reject an incomplete
object map? Did they silently ignore an unknown field? Were migration-shaped
documents evaluated or merely decoded? Which equality procedure justified a
mapped path equation? Which input family was used when an associativity
property passed?

Calling one program an ``oracle'' does not answer any of these questions. A
test oracle is a role in a protocol, not an intrinsic property of a language.
Haskell does not make a computation authoritative, and agreement between two
programs does not make a theorem.

This paper therefore starts from an evidence boundary rather than a language
preference. The accepted result is attached to:

\begin{itemize}
  \item source commit
  \code{abd655f4db31f1e0a9e78de8bbe83c71805f46c7};
  \item fixture capability set \code{slice-1};
  \item a closed 24-case fixture corpus;
  \item seven fixed-seed QuickCheck properties;
  \item exact Haskell and Rust golden gates;
  \item an exact computed-output comparison; and
  \item a read-only review of the complete source range.
\end{itemize}

Within that boundary, the Haskell program is compact enough to audit and
independent enough to catch implementation disagreement. Outside it, the
program has no automatic authority. Its intended roles are semantic oracle,
research compiler, and property-testing reference. It is neither a production
dependency nor proof authority.

\subsection{Research question}

The broad P16 question is whether a compact functional model can serve as a
semantic oracle for mappings and migrations. The accepted Slice 2 result
answers the narrower question:

\begin{quote}
Can an independently implemented Haskell program decode the shared \CatDB{}
fixture contract, compute the admitted finite schema, path, and mapping
operations, reject selected invalid values, and agree exactly with a separate
Rust implementation?
\end{quote}

The bounded answer is yes. The migration half of the broader question remained
outside Slice 2. At the accepted revision, migration and instance modules
contained structural envelope types and canonical ordering only. Their
fixtures were not semantic passes.

\subsection{Contribution and prior-art boundary}

Schemas as categories, instances as set-valued functors, schema mappings as
functors, and the induced migration functors are established
results \citep{maclane1998categories,spivak2012functorial}. Relational
encodings, composition, and executable categorical data integration also
predate this work
\citep{spivak2015relational,schultz2017integration,schultz2017algebraic}.
Schema mappings and data exchange have their own mature semantic literature
\citep{fagin2005exchange,fagin2005composition}. CQL already provides an
executable categorical database language \citep{cql2026}.

Nor is the validation method new in kind. QuickCheck introduced random
property-based testing for Haskell \citep{claessen2000quickcheck};
SmallCheck made bounded exhaustive testing an explicit alternative
\citep{runciman2008smallcheck}; and differential testing long predates this
comparator \citep{mckeeman1998differential}.

The contribution reported here is consequently repository-specific:

\begin{enumerate}
  \item a readable executable model of the selected \CatDB{} schema, path, and
  mapping fragment;
  \item a closed language-neutral fixture boundary with exact normalized
  outcomes and diagnostics;
  \item an honest split between semantic computation and structural envelope
  handling;
  \item deterministic, law-oriented bounded properties;
  \item source-audited independence from the Rust implementation and fixture
  expected values;
  \item two independent golden gates followed by a computed-output comparison;
  and
  \item an immutable acceptance record with threats and nonclaims.
\end{enumerate}

\status{\accepted{} for the exact Slice 2 result above; established categorical
and testing foundations are attributed to prior work.}

\section{Evidence vocabulary and snapshot discipline}
\label{sec:evidence-vocabulary}

\begin{definition}[Evidence labels]
This paper uses five labels:

\begin{description}
  \item[\accepted] A gate passed at the reviewed source and corpus, and the
  result was internally accepted after independent review.
  \item[\reproduced] The author pass reran an accepted command from an isolated
  extraction and observed the recorded result.
  \item[\later] A result exists in a later repository revision but is not part
  of the accepted Slice 2 claim.
  \item[\candidate] A result exists only in the current working tree and has
  not passed the required terminal code-review and release-acceptance gate.
  \item[\nonclaim] The manuscript explicitly excludes the statement.
\end{description}
\end{definition}

This distinction matters because the repository contains accepted Slice 4
code and a dirty Slice 5 candidate. Reading only current module exports would
wrongly attribute instance validation, \(\Delta\) migration,
information-loss analysis, and schema diff to the earlier result. Conversely,
reading only the historical commit would conceal later repairs and separately
bounded extensions.

\begin{table}[htbp]
\centering
\caption{Snapshot identities used in this paper.}
\label{tab:snapshots}
\begin{tabularx}{\textwidth}{L{0.21\textwidth} Y L{0.29\textwidth}}
\toprule
Snapshot & Role & Result boundary \\
\midrule
\code{377d383} & Parent research-contract baseline & Before Haskell Slice 2 \\
\code{abd655f} & Reviewed and accepted source & 24 fixtures; 16 semantic; 8
structural; 1,550 trials \\
\code{907914f} & Acceptance commit & Records review pass and internal
acceptance \\
\code{0569158} & Later accepted Slice 4 & 33 fixtures; 29 semantic under
\code{slice-4}; 4 structural; 2,350 trials \\
\code{e2f7cd7} plus dirty tree & Author-audit Slice 5 candidate & 42 fixtures;
analysis code and focused tests; uncommitted and unreviewed \\
\bottomrule
\end{tabularx}
\end{table}

Two roadmap files still label Slice 2/F2 as \code{OPEN}. Those labels predate
the acceptance commit. This manuscript treats the dated release record and
exact review range as the result authority and reports the stale roadmap text
as an artifact-consistency defect. It does not edit the shared roadmaps or
pretend that the discrepancy is absent.

\section{Finite schema and path semantics}
\label{sec:schema-path}

\subsection{Profile representation}

For the accepted profile, a schema is a finite presentation
\[
  S=(\Ob_S,\Arr_S,\Attr_S,\Eqn_S).
\]
Each generating arrow \(f\in\Arr_S\) has declared source and target objects.
Each attribute has a source object, scalar tag, and
\code{required=true}. Each equation contains two serialized paths.

A path is a pair
\[
  p=(A,[f_1,\ldots,f_n]),
\]
where \(A\) is the declared start. The empty list is the identity path at
\(A\). The Haskell representation uses closed algebraic data types and Aeson
record codecs. The language is Haskell 2010 plus the package's declared GHC
extensions and dependencies \citep{marlow2010haskell,aeson2026}.

Schema validation checks, in order relevant to this slice:

\begin{enumerate}
  \item identifier syntax and profile-required attributes;
  \item duplicate identifiers;
  \item arrow and attribute endpoint resolution; and
  \item typing and parallel endpoints for both sides of every equation.
\end{enumerate}

Diagnostics contain a code, phase, RFC 6901 JSON Pointer, and sorted related
semantic references \citep{rfc6901}. Free-form host exceptions are not the
comparison surface.

\subsection{Path typing}

The typing judgment
\[
  S\vdash p:A\rightsquigarrow B
\]
is computed by a finite left-to-right traversal. The identity rule is
\[
  \frac{A\in\Ob_S}
       {S\vdash (A,[]):A\rightsquigarrow A}.
\]
For a nonempty path, the validator resolves each named arrow and requires its
source to equal the current endpoint. An unknown arrow or source mismatch
produces a typed diagnostic rather than an empty result or exception.

For
\[
  S\vdash p:A\rightsquigarrow B,\qquad
  S\vdash q:B\rightsquigarrow C,
\]
composition is represented in traversal order:
\[
  q\circ p=(A,\mathit{arrows}(p)\mathbin{+\!\!+}\mathit{arrows}(q)).
\]
The function validates the schema and both paths before requiring the shared
endpoint. Thus mathematical notation reads \(q\circ p\), while serialized
arrows list \(p\) first.

\begin{example}[Accepted positive and negative coverage]
The path fixtures include an identity, a valid chain, a valid chain
composition, a source mismatch, and a composition endpoint mismatch. These
examples cover both returned endpoints and exact diagnostics. They do not
enumerate all graph shapes.
\end{example}

\subsection{The accepted equality procedure}

The target-path relation used during mapping validation is:
\[
p\DirectEq_S q
\quad\Longleftrightarrow\quad
p=q
\ \lor\
(p,q)\in\Eqn_S
\ \lor\
(q,p)\in\Eqn_S.
\]
Only one exact declared equation is consulted. The relation is
orientation-insensitive but is not closed under transitivity, congruence,
context, or substitution.

\begin{counterexample}[No transitive closure]
If \(S\) declares \(p=q\) and \(q=r\) but not \(p=r\), the accepted procedure
need not conclude \(p\DirectEq_S r\). It is therefore not a complete equality
decision for a finitely presented category.
\end{counterexample}

This limit is central. A mapping accepted by the program preserves equations
under \(\DirectEq\), not under an arbitrary complete equational theory.

\status{\accepted{} for finite representation validation, path typing,
composition, normalization, and direct equation checking at
\code{abd655f}. General presented-category equality is \nonclaim{}.}

\section{Mapping validation, identity, and composition}
\label{sec:mappings}

\subsection{Closed mapping data}

A mapping \(F:S\to T\) has three finite total assignment arrays:

\[
\begin{aligned}
F_0 &: \Ob_S\to\Ob_T,\\
F_1 &: \Arr_S\to\Path_T,\\
F_a &: \Attr_S\to(\Path_T\times\Attr_T).
\end{aligned}
\]

An arrow image \(F_1(f)\) must start at \(F_0(\mathrm{src}(f))\) and end at
\(F_0(\mathrm{tgt}(f))\). An attribute image \((p,a)\) first navigates a target
path and then selects a target attribute. The path endpoint must be the
attribute source, and the source and target scalar tags must match.

Validation rejects:

\begin{itemize}
  \item a mismatched source or target schema ID;
  \item a missing or duplicate object, arrow, or attribute assignment;
  \item an unknown mapped object, arrow, or attribute;
  \item an arrow path with the wrong endpoints;
  \item an attribute expression with the wrong endpoint or scalar tag; and
  \item a source equation whose substituted sides are not related by
  \(\DirectEq_T\).
\end{itemize}

The arrays are normalized by source identifier. Duplicate evidence is rejected
before normalization rather than collapsed.

\subsection{Identity mapping}

For a validated schema \(S\), the constructor \(\mathrm{id}_S\) emits:

\[
\begin{aligned}
(\mathrm{id}_S)_0(A) &= A,\\
(\mathrm{id}_S)_1(f:A\to B) &= (A,[f]),\\
(\mathrm{id}_S)_a(a\text{ at }A) &= ((A,[]),a).
\end{aligned}
\]

The complete mapping is normalized and returned with a caller-supplied
artifact identifier. Fixture equality includes that identifier. Law properties
instead use an extensional comparator that ignores only
\code{mapping\_id}.

\subsection{Composition by substitution}

Let \(F:S\to T\) and \(G:T\to U\). The accepted implementation first validates
both mappings and requires the target schema ID of \(F\) to equal the source
schema ID of \(G\).

For a \(T\)-path \(p=(A,[f_1,\ldots,f_n])\), define bounded substitution:
\[
G^\ast(p)=
\left(G_0(A),
  \mathit{arrows}(G_1(f_1))\mathbin{+\!\!+}\cdots
  \mathbin{+\!\!+}\mathit{arrows}(G_1(f_n))\right).
\]
Then:
\[
\begin{aligned}
(G\circ F)_0(A) &= G_0(F_0(A)),\\
(G\circ F)_1(f) &= G^\ast(F_1(f)).
\end{aligned}
\]

If \(F_a(a)=(p,b)\) and \(G_a(b)=(q,c)\), then
\[
  (G\circ F)_a(a)=
  \bigl(G^\ast(p)\mathbin{;\!}q,c\bigr),
\]
where \(\mathbin{;\!}\) appends the arrow list of \(q\) to the substituted
prefix. The result is normalized and validated again against \(S\) and \(U\).

\begin{lstlisting}[language=Haskell,caption={Accepted path substitution core, lightly elided.},label={lst:substitute}]
substitutePath :: Mapping -> Path -> Either Diagnostic Path
substitutePath mapping path = do
  start <- lookupObjectImage mapping (path_start path)
  imageArrows <-
    traverse
      (fmap path_arrows . lookupArrowImage mapping)
      (path_arrows path)
  pure (Path start (concat imageArrows))
\end{lstlisting}

Here \code{lookupObjectImage} returns the mapped object identifier, while
\code{lookupArrowImage} returns a \code{Path}. Applying
\code{path\_arrows} inside the traversal therefore produces a list of arrow
lists before \code{concat}; the displayed signature has no unused arrow-map
parameter.

The implementation is finite and total in the Haskell sense that semantic
failures are returned in \code{Either Diagnostic}. This does not imply
termination or bounded resources for every arbitrarily large decoded input,
nor does it establish categorical lawfulness beyond the implemented checks.

\status{\accepted{} for the closed mapping representation, selected validator,
identity constructor, finite substitution, and composition.}

\section{Fixture semantics and honest structural boundaries}
\label{sec:fixtures}

\subsection{Closed documents}

Every fixture contains:

\begin{itemize}
  \item schema version \code{1.0.0};
  \item stable fixture ID and one of eight categories;
  \item description and ordered assumptions;
  \item category-specific input; and
  \item one deterministic \code{ok}, \code{error}, or admissible
  \code{unsupported} expected outcome.
\end{itemize}

JSON object member order is not semantic, while normalized set-like arrays and
path arrow arrays have explicit rules. The accepted program compares parsed
JSON values, not source bytes. JSON syntax follows the shared interchange
contract \citep{rfc8259}; later schema-diff rules also refer to canonical JSON
\citep{rfc8785}, although Slice 2 does not execute schema diff.

Closure is enforced in two ways. Generic record codecs set
\code{rejectUnknownFields=True}, and manually decoded envelopes call explicit
\code{closed} and \code{requireFields} checks. The decoder parses and re-encodes
the category-specific input before rebuilding the complete fixture. Exact
parsed-value equality between source and rebuilt fixture catches unknown or
lossy fields.

The test suite constructs a path-typing fixture with an unknown field inside
the nested schema. Successful decoding would fail the test.

\subsection{Semantic versus structural cases}

\begin{table}[htbp]
\centering
\caption{Exact accepted Slice 2 classification.}
\label{tab:classification}
\begin{tabularx}{\textwidth}{Y r L{0.24\textwidth} Y}
\toprule
Category & Cases & Classification & Operation \\
\midrule
Schema parsing & 3 & semantic & Normalize or return exact parse/shape/type
diagnostic \\
Path typing & 3 & semantic & Return start, endpoint, and arrow count, or
diagnostic \\
Path composition & 2 & semantic & Return composed path or endpoint diagnostic \\
Identity mapping & 2 & semantic & Return canonical identity or schema
diagnostic \\
Mapping composition & 6 & semantic & Return composed mapping or validation
diagnostic \\
Migration validation & 4 & \structural & Closed round trip only; no result \\
Information-loss detection & 2 & \structural & Closed round trip only; no
result \\
Schema diff & 2 & \structural & Closed round trip only; no result \\
\midrule
Total & 24 & 16 semantic, 8 structural & \\
\bottomrule
\end{tabularx}
\end{table}

The Haskell evaluator dispatches by category. For one of the five admitted
categories it computes a complete JSON outcome. For any of the other three it
returns the internal marker \code{structural-only}. The case report then sets:

\[
\begin{array}{lll}
\text{semantic:} &
\Actual=\Eval(\mathrm{input}),&
\mathrm{golden\_match}=(\Actual=\Expected),\\[2mm]
\text{structural:} &
\Actual=\mathtt{null},&
\mathrm{classification}=\mathtt{structural\mbox{-}only}.
\end{array}
\]

The structural case still requires closed decoding and exact round trip. It
does not compare a computed semantic result because none exists.

\begin{counterexample}[An envelope is not an evaluator]
The accepted Haskell type includes constructors named \code{Delta},
\code{Sigma}, and \code{Pi}. This permits a migration fixture to be decoded.
At Slice 2, it does not imply that any of those operators is evaluated.
Treating the four migration documents as semantic agreements would change the
accepted count from 16 to 20 and would be false.
\end{counterexample}

\status{\accepted{} for 24 closed round trips and exactly 16 semantic
evaluations. Migration, information-loss, and diff semantics are
\nonclaim{} for Slice 2.}

\section{The two-implementation comparison}
\label{sec:comparison}

\subsection{Data flow}

\Cref{fig:comparison} shows the accepted protocol. The expected outcome is a
gate for each implementation, not an input to the Haskell evaluator. Only
computed actual values cross the final semantic comparison.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[
  node distance=7mm and 12mm,
  >=Latex,
  box/.style={draw,rounded corners,align=center,minimum height=9mm,
              text width=31mm,font=\small},
  gate/.style={draw,diamond,aspect=2,align=center,font=\scriptsize,
               inner sep=1.5pt},
  line/.style={->,thick}
]
  \node[box,fill=fixturegreen] (fixture) {closed fixture\\input + expected};
  \node[box,fill=rustorange,below left=13mm and 18mm of fixture] (rust)
       {Rust decode, round trip,\\and semantic evaluator};
  \node[box,fill=haskellblue,below right=13mm and 18mm of fixture] (hs)
       {Haskell decode, round trip,\\and semantic evaluator};
  \node[gate,below=8mm of rust] (rgate) {actual = expected?};
  \node[gate,below=8mm of hs] (hgate) {actual = expected?};
  \node[box,fill=fixturegreen,below=17mm of fixture,text width=38mm] (compare)
       {classification and\\actual-versus-actual compare};
  \node[box,fill=limitred,below=8mm of compare,text width=38mm] (result)
       {nonzero on any failure;\\otherwise exact summary};

  \draw[line] (fixture) -- node[left,font=\scriptsize] {same input} (rust);
  \draw[line] (fixture) -- node[right,font=\scriptsize] {same input} (hs);
  \draw[line] (rust) -- (rgate);
  \draw[line] (hs) -- (hgate);
  \draw[line] (rgate) -- node[below left,font=\scriptsize] {computed actual} (compare);
  \draw[line] (hgate) -- node[below right,font=\scriptsize] {report actual} (compare);
  \draw[line] (compare) -- (result);
\end{tikzpicture}
\caption{Accepted comparator data flow. Both implementations share the written
fixture and golden value, but compute through separate source paths.}
\label{fig:comparison}
\end{figure}

The Rust side decodes and round-trips the fixture, computes its actual outcome,
and aborts on a golden mismatch. It then launches the selected Cabal program
in the Haskell package directory, passes the selected GHC path, and requests a
JSON report.

The report parser rejects:

\begin{itemize}
  \item a failed or unstartable Haskell process;
  \item an unreadable or malformed report;
  \item wrong implementation or capability identity;
  \item a failed Haskell round trip or golden check;
  \item a missing or duplicate case;
  \item a category or classification difference;
  \item null semantic actuals or non-null structural actuals; and
  \item a Rust/Haskell computed-output difference.
\end{itemize}

For a structural case, both sides must classify it as structural and carry no
semantic output. The comparator prints every disagreement and exits nonzero.

\subsection{What independence means}

The accepted source and review establish:

\begin{itemize}
  \item no Rust dependency, FFI, process call, or Rust linkage in Haskell;
  \item no \code{unsafe} use in the Haskell tree;
  \item no dispatch by fixture ID;
  \item no use of \code{fixture\_expected} inside the evaluator;
  \item semantic \code{report\_actual} populated only from the Haskell
  computation; and
  \item a separate OS process and JSON report.
\end{itemize}

This is implementation independence, not specification independence. Both
programs use the same fixture definition and expected output. Both may share a
misreading, an incomplete corpus, a platform bug, or a flawed golden.

\begin{remark}[Redundancy of the final comparison]
Once Rust has proved only that its actual equals the fixture expected, and
Haskell has proved only that its actual equals the same expected, equality of
the two actuals follows. The final actual-versus-actual check is still useful
defense against report association, transport, and comparator defects, but it
does not add mathematical falsification power after both golden gates pass.
\end{remark}

\status{\accepted{} for source-audited independent computation across the
recorded process boundary. Independent specification and general
implementation equivalence are \nonclaim{}.}

\section{Law-oriented property tests}
\label{sec:properties}

\subsection{Seven accepted properties}

\begin{table}[htbp]
\centering
\caption{Deterministic accepted QuickCheck schedule.}
\label{tab:properties}
\begin{tabularx}{\textwidth}{r r Y}
\toprule
Seed & Successful trials & Property \\
\midrule
1729 & 250 & Left and right identity for composed paths \\
1730 & 250 & Piecewise path composition returns the full path and endpoint \\
1731 & 250 & Three-segment path associativity \\
1732 & 200 & Left and right mapping identity under extensional mapping equality \\
1733 & 200 & Three-mapping substitution associativity under extensional equality \\
1734 & 200 & One corrupted path source yields
\code{PATH\_SOURCE\_MISMATCH} \\
1735 & 200 & One omitted object assignment yields
\code{INCOMPLETE\_OBJECT\_MAP} \\
\midrule
 & 1,550 & Total successful trials; no counterexample reported \\
\bottomrule
\end{tabularx}
\end{table}

The runner sets both \code{maxSuccess} and a replay generator for each
property. GHC warnings are enabled with \code{-Wall -Wcompat}; the manual
\code{strict} flag adds \code{-Werror}. The release command disables
documentation so missing Haddock coverage is not confused with a source
warning gate. GHC documents the warning-to-error behavior
\citep{ghc2026warnings}.

\subsection{Generator boundary}

The generator varies an integer size and constructs lawful values before
testing a law. A generated schema is a chain:
\[
E_0\xrightarrow{a_0}E_1\xrightarrow{a_1}\cdots
\xrightarrow{a_{n-1}}E_n
\]
with one required string attribute at \(E_0\), no equations, and no branching.
A generated mapping renames the corresponding entities, arrows, and attribute.

This construction avoids discarding mostly invalid random inputs and exercises
composition over several finite lengths. It also creates a narrow sample
space. In particular, generated properties do not cover:

\begin{itemize}
  \item branching or cyclic schemas;
  \item multiple attributes or scalar tags;
  \item equation-bearing generated schemas;
  \item nontrivial attribute navigation;
  \item arbitrary lawful path images;
  \item simultaneous faults; or
  \item identifier punctuation at the canonical-order boundary.
\end{itemize}

The fixture corpus supplies some equation and error examples, but fixture
examples do not widen the QuickCheck distribution.

\begin{counterexample}[Passing trials are not universal quantification]
An implementation can pass all 1,550 trials and still fail on a lawful
branching schema, a two-equation target presentation, or an identifier
containing punctuation. The accepted review found precisely such a latent
ordering divergence for path keys containing \code{.} or \code{-}; the
generated family did not expose it.
\end{counterexample}

QuickCheck's contribution is automated random testing of stated properties,
not proof \citep{claessen2000quickcheck}. The fixed schedule makes this run
replayable under the recorded dependency version; it does not make the sample
exhaustive. SmallCheck's explicit exhaustive-small-value model illustrates
the distinction \citep{runciman2008smallcheck}.

\status{\accepted{} for the exact seven properties, seeds, counts, and
generators. Any universally quantified categorical law remains \nonclaim{}.}

\section{Results}
\label{sec:results}

\subsection{Accepted retained evidence}

The retained Haskell report has SHA-256:
\[
\code{d4725f04d8e3c908c3d11030936d4fdfeab9f174ed0b8b829f4c7c7316b33a6f}.
\]
Programmatic inspection found that every semantic case had non-null
\code{actual}, \code{round\_trip=true}, and
\code{golden\_match=true}. Every structural case had \code{actual=null} and
both Boolean gates true.

\begin{table}[htbp]
\centering
\caption{Accepted Slice 2 result.}
\label{tab:accepted-result}
\begin{tabular}{lr}
\toprule
Measure & Result \\
\midrule
Closed fixture round trips & 24 / 24 \\
Independently computed Haskell outcomes & 16 \\
Structural-only outcomes & 8 \\
Haskell golden mismatches & 0 \\
Failed Haskell cases & 0 \\
QuickCheck successful trials & 1,550 \\
QuickCheck counterexamples & 0 \\
Rust/Haskell semantic comparisons & 16 \\
Rust/Haskell disagreements & 0 \\
Independent review blockers / majors & 0 / 0 \\
Independent review verdict & PASS \\
\bottomrule
\end{tabular}
\end{table}

The exact accepted comparator summary was:

\begin{lstlisting}
summary left=rust right=haskell capability_set=slice-1 total=24 semantic-compared=16 structural-compared=8 disagreements=0
\end{lstlisting}

The release record and review have SHA-256 values
\code{db2405a7...e3d84} and \code{a9f8debc...c95},
respectively \citep{catdbslice2,catdbslice2review}.

\subsection{Isolated historical rerun}

The author pass extracted \code{abd655f} with \code{git archive}; it did not
check out over the working tree. Cabal compilation and testing used a fresh
build directory. With Cabal 3.16.1.0 and GHC 9.14.1, the following gates exited
zero:

\begin{lstlisting}
/opt/homebrew/bin/cabal check
/opt/homebrew/bin/cabal build all -fstrict --disable-documentation \
  --project-file=cabal.project \
  --with-compiler=/opt/homebrew/bin/ghc \
  --builddir=<fresh-directory>
/opt/homebrew/bin/cabal test all -fstrict --disable-documentation \
  --project-file=cabal.project \
  --with-compiler=/opt/homebrew/bin/ghc \
  --builddir=<same-directory> --test-show-details=direct
\end{lstlisting}

The test emitted the expected \(250,250,250,200,200,200,200\) property counts
and the \(24/16/8/0\) fixture summary. A standalone Haskell verification
produced a report byte-identical to the accepted retained report. The exact
historical Rust comparison also exited zero with the accepted summary.

\status{\reproduced{} on 23 July 2026 for the exact historical source, fixture
corpus, and observed dependency resolution.}

\subsection{Later accepted Slice 4, not retroactive evidence}

Accepted Slice 4 source \code{0569158} adds finite instance validation and
bounded pullback migration \citep{catdbslice4}. It also repairs or mitigates
several Slice 2 review findings: that accepted tree has a Cabal freeze,
explicit path-key equation ordering, owned temporary report files,
per-comparison Cabal build isolation, and 11 properties.

\begin{table}[htbp]
\centering
\caption{Accepted Slice 4 observations, not Slice 2 results.}
\label{tab:later-results}
\begin{tabularx}{\textwidth}{Y r r r}
\toprule
Capability over accepted 33-case corpus & Semantic & Structural & Disagreements \\
\midrule
\code{slice-1} & 16 & 17 & 0 \\
\code{slice-4} & 29 & 4 & 0 \\
\bottomrule
\end{tabularx}
\end{table}

The accepted Slice 4 strict Haskell tests completed 2,350 successful trials
over 11 properties. Slice 4 makes all 13 migration cases semantic, including
two finite \(\Delta\) successes, validation errors, and exact unsupported
\(\Sigma/\Pi\) results. Information loss and schema diff remain structural at
that accepted boundary.

These observations demonstrate evolution, not a timeless equivalence theorem.
They do not alter the accepted Slice 2 counts or make general migration
available.

\subsection{Current Slice 5 working-tree candidate}

The author-audit working tree is based on \code{e2f7cd7} and contains
uncommitted Slice 5 changes. Its Cabal package has been renamed from the
historical \code{catdb-reference.cabal} manifest and
\code{catdb-reference} package to \code{catdb-semantics.cabal} and
\code{catdb-semantics}; the executable remains \code{catdb-reference}. The
candidate adds \code{CatDB.Analysis} and nine fixtures---five
information-loss fixtures and four schema-diff fixtures---expanding the
corpus to seven information-loss cases and six schema-diff cases. It also adds
a focused \code{loss-and-diff-properties} test suite.

The current corpus has 42 fixtures. Under \code{slice-1}, 16 are semantic and
26 are structural. Under \code{slice-4}, 29 are semantic and 13 are
structural. Under \code{slice-5}, all 42 are semantic; 13 of these are
information-loss and schema-diff cases. The full strict Haskell test command
runs 13 properties and 2,750 trials. The focused candidate test runs two
properties for 200 trials each and recomputes all 13 selected goldens.

\status{\candidate{} only. These observations are author-side verification,
not an accepted Slice 5 result. They must not be promoted until terminal
Claude code review and release acceptance.}

\section{Rust comparison and the role of Haskell}
\label{sec:rust}

\subsection{Different roles, shared contract}

The Rust code is the production-oriented implementation for the admitted
profile. It owns the shipping parser, diagnostic and normalization behavior,
and later compiler/runtime boundaries. The Haskell package is a small readable
calculation over the shared serialized profile. It serves as a semantic oracle,
research compiler, and property-testing reference. Production deployment does
not depend on it, and machine-checked claims belong to the separately scoped
Lean formalization.

This division yields three useful failure classes:

\begin{enumerate}
  \item both disagree with the fixture, suggesting two defects or a fixture
  issue;
  \item one disagrees with the fixture and the other, localizing an
  implementation candidate; or
  \item both agree with the fixture but the written definition or golden is
  wrong, a common-mode failure that comparison cannot detect.
\end{enumerate}

A resolution must appeal to the written definition and recorded intent, not
majority vote. Two programs agreeing against a definition do not redefine the
definition silently.

\subsection{Why Haskell is useful but not necessary}

The accepted model benefits from ordinary functional-programming properties:
small algebraic data types, explicit \code{Either} failures, pure finite
transformations, and direct construction of law properties. These make the
code convenient to inspect. They do not show that Haskell is uniquely suited
to categorical database semantics. CQL's implementation history alone is
enough to reject a language-necessity argument \citep{cql2026}.

Nor does Haskell purity validate external effects. The comparison still
depends on process launch, paths, environment variables, a temporary report,
package resolution, files, and compilers. Backend queries, transactions,
streaming, retries, and distributed faults are outside the Haskell program.

\status{\accepted{} that the Haskell source is an independently implemented
finite reference for the selected operations. Haskell necessity, production
deployment, and operational superiority are \nonclaim{}.}

\section{Threat model and review findings}
\label{sec:threats}

\subsection{Threats addressed by the protocol}

\begin{longtable}{L{0.31\textwidth} L{0.61\textwidth}}
\caption{Threats addressed at the accepted boundary.}
\label{tab:addressed-threats}\\
\toprule
Threat & Accepted control \\
\midrule
\endfirsthead
\toprule
Threat & Accepted control \\
\midrule
\endhead
Expected-value replay & Source and data-flow audit; expected used only for
golden comparison \\
Rust reuse from Haskell & No Rust dependency, FFI, process use, or linkage in
Haskell \\
Fixture-specific behavior & Category dispatch; no fixture-ID semantic branch \\
Unknown or lossy JSON & Closed typed codecs, exact parsed-value round trip,
negative nested-field probe \\
Silent golden mismatch & Nonzero Rust and Haskell gates \\
Wrong report identity & Required implementation and capability fields \\
Missing or duplicate report case & Comparator rejection \\
Semantic/structural confusion & Required classification and nullability of
\code{actual} \\
Computed-output difference & Exact parsed JSON comparison and nonzero exit \\
Tool selection ambiguity & \code{CATDB\_CABAL}/\code{CATDB\_GHC}; negative
Cabal-path integration test \\
\bottomrule
\end{longtable}

\subsection{Accepted review findings}

The independent review found no blocker or major issue. It retained five minor
findings:

\begin{enumerate}
  \item the temporary report name used process ID and nanosecond time rather
  than exclusive creation;
  \item derived Haskell \code{Ord Path} could disagree with the written
  slash-separated path-key order for valid identifiers containing
  \code{.} or \code{-};
  \item the accepted package had no Cabal freeze or index-state pin;
  \item package distribution metadata declared Apache-2.0 without a bundled
  package license file and omitted author/copyright metadata; and
  \item property generators covered only a narrow linear family.
\end{enumerate}

The review also noted inherited child stdout, a repository-root working
directory assumption, declaration-order rather than written within-phase
diagnostic tie-breaking, and a transient Cabal artifact race.

The first finding is a local attack surface. On a hostile shared temporary
directory, an attacker who predicts and pre-creates the report path as a
symlink may redirect the Haskell write. The accepted review judged the primary
macOS per-user temporary directory mitigating but did not declare the design
safe. Current Slice 4 code uses an owned temporary file; the historical result
retains the finding.

The second finding is a specification-conformance gap masked by common-mode
agreement: both languages used tuple-like order for the accepted corpus.
Identifiers in the corpus did not exercise the separator boundary. This is a
clear example of why zero cross-language disagreement is not full contract
conformance.

The third finding concerns replay stability. Cabal freeze files record a
dependency solution for a project \citep{cabal2026}. The isolated historical
rerun resolved and passed, but that does not guarantee the same package graph
at a future index state. Current code has a freeze; accepted Slice 2 did not.

\subsection{Residual threats}

The protocol does not eliminate:

\begin{itemize}
  \item common errors in definitions or goldens;
  \item omitted fixture shapes or generator distributions;
  \item compiler, library, package-index, platform, or hardware defects;
  \item compromised tools or dependencies;
  \item resource exhaustion from very large finite inputs;
  \item multi-fault diagnostic-order divergences;
  \item Unicode, numeric, locale, and JSON edges outside the corpus;
  \item errors hidden by normalization;
  \item lack of mutation coverage or generator-distribution measurement; or
  \item the absence of organizationally independent specification authors.
\end{itemize}

\status{\accepted{} after review with the five minor findings retained. The
protocol is not a supply-chain, sandbox, or hostile-environment security
result.}

\section{Falsification contract}
\label{sec:falsifiers}

The bounded result should be rejected or narrowed if any of these conditions
is demonstrated at the accepted source and corpus:

\begin{enumerate}
  \item strict build or test failure under the recorded resolved toolchain;
  \item inability to regenerate the retained report from accepted source and
  fixtures;
  \item data flow from fixture expected values into a computed Haskell actual;
  \item Haskell invocation or linkage of Rust;
  \item fixture-ID-specific semantic behavior;
  \item a golden mismatch in any of the 16 admitted semantic cases;
  \item a changed parsed-value round trip in any accepted fixture;
  \item acceptance of the nested unknown-field probe;
  \item a Rust/Haskell actual difference in an admitted semantic case;
  \item a semantic output attached to an accepted structural-only case;
  \item comparator acceptance of a missing, duplicate, or misidentified report
  case;
  \item a reproducible counterexample in the exact accepted property schedule;
  or
  \item evidence that the review did not cover the stated source range.
\end{enumerate}

An example outside the declared profile does not change the historical run,
but it falsifies a generalization. For example, the accepted path-key ordering
finding does not change the 24 results; it does falsify a claim of contract
conformance for every valid identifier.

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

The following are part of the result, not small-print qualifications:

\begin{enumerate}
  \item QuickCheck trials are not proofs.
  \item Rust and Haskell are not proved generally equivalent.
  \item Two implementations do not establish specification correctness.
  \item Haskell is not required by categorical database semantics.
  \item Haskell is not a production dependency or service in this result.
  \item Slice 2 does not semantically validate instances.
  \item Slice 2 does not implement \(\Delta\), \(\Sigma\), or \(\Pi\).
  \item Later bounded \(\Delta\) is not full migration semantics.
  \item General Kan extensions, quotients, and infinite instances are absent.
  \item Slice 2 does not execute information-loss analysis or schema diff.
  \item Query syntax, denotation, rewriting, and planning are absent.
  \item SQL generation and backend equivalence are untested.
  \item SQLite, PostgreSQL, API, file, and warehouse connectors are absent.
  \item Transactions, cutover, rollback, CDC, and online schema change are
  unmodeled.
  \item Cost, latency, throughput, scale, and memory are unmeasured.
  \item Distributed execution, consistency, availability, and fault tolerance
  are unmodeled.
  \item Equality modulo arbitrary path equations is not decided.
  \item The direct-equation check is not complete.
  \item Nulls, optional attributes, partial functions, bag semantics, and
  richer typesides are not represented by the accepted fragment.
  \item Fixture agreement is not kernel-checked evidence.
  \item Compiler and dependency trust are not eliminated.
  \item A passing golden does not establish intended business meaning.
  \item The accepted temporary report path is not claimed safe in a hostile
  shared directory.
  \item The accepted Haskell dependency graph is not fully pinned.
  \item Diagnostic priority is not generally equivalent on multi-fault inputs.
  \item Accepted equation ordering is not generally conformant outside the
  accepted identifiers.
  \item Structural fixture categories are not semantic P16 results.
  \item The reference model does not replace database, security, integration,
  or user evaluation.
\end{enumerate}

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

The accompanying \code{reproducibility.md} records exact commands, tools,
temporary directories, artifact hashes, and manuscript-build inspection. The
minimum semantic reproduction has four stages:

\begin{enumerate}
  \item extract the exact accepted Git object without modifying the working
  tree;
  \item build and test the Haskell package with strict warnings in an isolated
  Cabal directory;
  \item run the standalone verifier and compare its complete JSON hash; and
  \item run the exact Rust/Haskell comparator from the extracted repository
  root.
\end{enumerate}

Reproduction should preserve raw stdout, stderr, exit codes, tool versions,
resolved dependency information, report JSON, fixture manifest and case
hashes, repository revision, and dirty-state record. A future extension should
also record distribution or exhaustive-small-model coverage rather than
reporting only successful trial counts.

The accepted package lacked a freeze. For historical reconstruction, the best
available record combines the source bounds, GHC 9.14.1, retained build logs,
and the byte-identical report reproduced on 23 July 2026. The later freeze
belongs to Slice 4 and must not be inserted into the historical source while
claiming a byte-identical build recipe. Current package-qualified commands use
\code{catdb-semantics}; historical commands retain the package name present in
the accepted source. The executable remains \code{catdb-reference}.

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

The useful part of this result is not the sentence ``we wrote it in Haskell.''
It is the chain of observable boundaries around the program.

At one reviewed source revision, the Haskell implementation decoded a closed
24-case corpus, round-tripped every case, computed 16 schema/path/mapping
outcomes, and marked eight later-slice cases as structural-only. Its seven
fixed-seed properties completed 1,550 trials. The Rust implementation computed
the same admitted outcomes through separate source, both programs passed exact
golden gates, and the comparator found no disagreement. The author pass
reproduced the Haskell report byte-for-byte and reran the historical
comparison. Independent review found no blocker or major issue.

The same evidence also says what did not happen. Slice 2 did not evaluate a
migration, prove a law, decide general path equality, execute a query, contact
a backend, measure performance, or model a distributed system. Later finite
instance and \(\Delta\) work is accepted but separate. Current
information-loss and schema-diff work remains an unreviewed candidate. Review
findings expose common-mode ordering, dependency pinning, generator breadth,
package metadata, and temporary-file risks.

A bounded executable oracle earns trust by making these distinctions easy to
audit. Its strongest claim is exact agreement inside a named profile, not
correctness everywhere else.

\bibliographystyle{plainnat}
\bibliography{references}

\end{document}
