\section{What the Theorems Rely On}
\label{sec:trust}

A kernel-checked theorem is only as good as its statement and its trusted base. This section lists both for the
migration theorems, reports how we tested the semantics, and describes three checks of the theorems: axioms, kernel
replay and a mutation test. We re-checked every number in this paper on a frozen copy of the artifacts. The exceptions are numbers taken from
the records of the sessions that produced the results, and for each of these we name its source.

\subsection{Trusted base}

Each theorem relies on Lean's kernel and its three standard axioms (\code{propext}, \code{Classical.choice},
\code{Quot.sound}), and on what the definitions mean. Table~\ref{tab:trust} lists, per language, the front end that
turns source text into Lean terms, the semantics, the library models and how we tested the semantics. Tactics, lemmas
and program logics are not in it, since the kernel checks everything they produce. For Rust, the trusted base includes
Aeneas's translation, which we test only through our own programs: the native runs of the Rust translations and of the
tiny-regex-c port (Section~\ref{sec:c2rust}) agreed with their Aeneas extractions on every generated case, while the
jsmn and Adler-32 ports were compared with the C code only in native runs.

By contrast, the binary-level proofs about OSS-Fuzz harnesses by the company Theorem~\cite{theoremossverify} rely on a
smaller trusted base. Because
they are about the compiled binary, neither the compiler nor the library sources are part of it. They trust a model of
a Linux process that runs RISC-V code (a model its authors call best effort and not complete), the tools that load a
binary into it, and the Rocq kernel. Our trusted base is larger. It includes a front end, a semantics and library
models per language, and Aeneas's translation of Rust. In return, our theorems are about the source program as our front ends present it, not about a compiled binary. They cover
undefined behaviour that the binary does not show (Section~\ref{sec:ub}), and they relate programs written in different
languages.

For the migration theorems, the statement fixes what is claimed and therefore has to be read. The generated part
follows one template for all programs, whereas the part that is not generated, listed in Table~\ref{tab:programs},
consists of the input domains and the model of the assembler routine COBDATFT. The statement generator, the
definitions of \code{Equiv}, \code{Sim} and \code{Rel}, the record encoders and these parts that the agents wrote
directly are therefore trusted as well. Agents read them during our checks, and we have no record of a line-by-line
review by a person. Last, the theorems abstract file I/O. Each input file is the list of its records, and each output is
the list of records written or rewritten; the semantics represents an indexed file as a list in ascending key order
with unique keys, a documented limit. The file statuses of the semantics are those of operations on these lists, such as end
of file, a missing or duplicate key and the logic errors of IBM's status table, and those reported by the environment for a failing \code{OPEN}. In the migration statements the environment lets every \code{OPEN} succeed, and the
semantics assumes that I/O never fails for physical reasons.

\begin{table}
\caption{What the theorems trust, per language, at the versions of Appendix~\ref{app:pins} and
Table~\ref{tab:fidelity}. Lean lines count
the files that define the language (syntax, values, memory or data layout, evaluation rules, number and string models)
and the library models.}
\label{tab:trust}
\footnotesize
\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{}p{0.12\linewidth}p{0.26\linewidth}p{0.17\linewidth}p{0.20\linewidth}p{0.16\linewidth}@{}}
\toprule
& Front end & Semantics & Library models & Tested against \\
\midrule
COBOL & our front end (\tbCobFe{} lines of Python), Lean loader (\tbCobLoader{} lines) & \tbCobSem{} Lean lines &
\code{CEE3ABD} (an abend); \code{COBDATFT}, from its assembler source & Tables~\ref{tab:fidelity}--\ref{tab:suites} \\
Java & \code{javac} (JDK 17), Soot 4.7.1, our Jimple reader (\tbJavaFe{} lines) & \tbJavaSem{} & \tbJavaRows{}
library methods (\tbJavaLib{} lines) & Tables~\ref{tab:fidelity}--\ref{tab:suites} \\
Rust & Charon \code{de8736f}, Aeneas \code{fdebf20} & Aeneas's library, \tbRustLib{} lines with its lemmas & in Aeneas's library &
native runs \\
C/C++ & ClangIR (llvm-project \code{4955d32b}), our CIR reader (\tbCFe{} lines) & \tbCSem{} & \tbCModels{} library
operations (\tbCLib{} lines) & Tables~\ref{tab:fidelity}--\ref{tab:suites} \\
TypeScript & our front end on the TypeScript 5.9.3 compiler (\tbTsFe{} lines of TypeScript) & \tbTsSem{}, built-ins
included & \tbTsBuiltins{} built-in operations & Tables~\ref{tab:fidelity}--\ref{tab:suites} \\
Statements & the statement generator & \code{Equiv}, \code{Sim}, \code{Rel}, record encoders & the domains and the
COBDATFT model, written directly & mutation test \\

\bottomrule
\end{tabular}
\end{table}

\subsection{Testing the semantics}
\label{sec:validation}

Table~\ref{tab:fidelity} lists the differential tests of each semantics against a reference implementation, and
Table~\ref{tab:suites} two existing collections of test programs and, under a pre-registration, random mutants of
the semantics. The COBOL differential tests run the representation with GnuCOBOL's character set and sign conventions. The theorems
use IBM's conventions, the \emph{IBM variant} of the representation, and only an exploratory run of the same testers
covers it. That run, on 964 generated and hand-written programs of its own, finds no disagreement and declines 11 of them as
outside the modelled subset; some programs agree only up to a negative packed zero or at the same abend. Section~\ref{sec:limits} lists what
the run leaves untested.

The Java and C++ suites were also run at versions other than those of Table~\ref{tab:fidelity}. At the migration version of the Java semantics, 2 of the 41 JVM programs stop at a method without a model. All 41 agree at each later version that we tested. These are the versions of the table, of a sample of Thrift functions in the technical report and of the joint build
(Appendix~\ref{app:pins}), and the termination version. The C++ suite gives the result of the table at five other versions used for C and
C++ theorems that we report. At the earlier version of the first sample run and the security-fix studies, it
had 167 cases, of which 166 agree and 1 is reported as undefined behaviour. Other results, among them some of the re-checks in the technical report, use versions not covered by these runs.

\begin{table}
\caption{Differential tests of the semantics against reference implementations, for COBOL at the coblean snapshot
\code{20261024T2306Z} of the migration theorems and for the others at the versions of the second run on random
samples: cirlean \code{d9ae8e5}, JimpleLean \code{20261025T0300Z} and StrictTS \code{44d6b9b}.}
\label{tab:fidelity}
\footnotesize
\begin{tabular}{@{}p{0.11\linewidth}p{0.15\linewidth}p{0.36\linewidth}p{0.30\linewidth}@{}}
\toprule
Semantics & Reference & Suite & Result \\
\midrule
COBOL & GnuCOBOL 3.2 & random arithmetic, \code{MOVE} and \code{IF} programs, \code{TRUNC(STD)}: 200 & 200 agree (5 only
up to the stored sign) \\
COBOL & GnuCOBOL 3.2 & the same generator, \code{TRUNC(BIN)}: 200 & 198 agree; 2 differ (binary items beyond their \code{PICTURE}, not claimed) \\
COBOL & GnuCOBOL 3.2 & random \code{PERFORM}/\code{GO TO} programs: 100 & 88 agree, 12 declined (recursive or
abandoned \code{PERFORM}) \\
COBOL & GnuCOBOL 3.2 & front end on random programs: 100 arithmetic, 60 control flow & 100 agree (2 only up to a sign);
58 agree, 2 declined \\
COBOL & GnuCOBOL 3.2 & sequential and indexed files: 100; \code{UNSTRING}, \code{INSPECT}, \code{STRING}: 60 each & all
agree (one at the same abend) \\
COBOL & GnuCOBOL 3.2 & CBSTM03A with CBSTM03B on CardDemo's data, without the z/OS walk & both output files equal,
1,212 and 6,082 records \\
C++ & native & \cirDiffCases{} cases (arithmetic, control flow, RAII, exceptions, classes, containers, the C library) &
\cirDiffMatch{} agree, 1 reported as undefined behaviour, none differs \\
Java & JVM (JDK 17) & \jimDiff{} programs & all agree; at the migration version, 39 agree and 2 stop at a method without
a model \\
TypeScript & Node 22 & \tsCorpusProgs{} programs; \tsCorpusReject{} programs outside the subset; \tsFmtChecks{} checks
of number formatting and string methods & all agree; all rejected; no mismatch \\
\bottomrule
\end{tabular}
\end{table}

\begin{table}
\caption{Collections of test programs and mutants of the semantics. The NIST programs ran at the coblean snapshot of the migration theorems and the LLVM programs at cirlean
\code{ffab71e}. Intervals are 95\% Wilson intervals.}
\label{tab:suites}
\footnotesize
\begin{tabular}{@{}p{0.11\linewidth}p{0.15\linewidth}p{0.30\linewidth}p{0.36\linewidth}@{}}
\toprule
Semantics & Reference & Suite & Result \\
\midrule
COBOL & GnuCOBOL 3.2 & NIST COBOL85: 309 programs of six modules (pre-registered) & 84 pass; 152 outside the subset;
46 fail; 25 front-end errors; 1 undefined behaviour; 1 timeout. In the 130 that run to the end, 2,419 of 2,525 test verdicts agree \\
C & native & LLVM test programs: 177 with the reference status natively, of 200 drawn (pre-registered) & 95 same
status (53.7\%, 46.3--60.9); 3 another; 25 undefined behaviour (7 confirmed); 31 outside the subset; 13 \code{exit};
10 timeouts. With a verdict: 95 of 123 (77.2\%, 69.1--83.8) \\
all & differential tests & 30 random mutants of each semantics (pre-registered) & killed: C 7, Java 16, COBOL 15, TypeScript 20; COBOL front end 18 \\
COBOL, Java, C & differential tests & extended suites on 30 fresh mutants each & killed, new suite against old: COBOL 21 vs 19; front end 23 vs 21; Java 24 vs 20; C 24 vs 10 (23 without one
memory-limit kill) \\
\bottomrule
\end{tabular}
\end{table}

\paragraph{The test programs.} None of the constructs that make NIST programs fail or end with errors occurs in the
eight programs of the migration theorems. Because the front end of our version would stop every program at its first
report line, a \code{WRITE \dots{} ADVANCING} statement, these runs treat that statement as a plain \code{WRITE}. Of the 46 failures, 34 are caused by constructs dropped by the front end with only a warning, 33 of them declaratives. Six, in statements with
\code{NOT ON SIZE ERROR} but no \code{ON SIZE ERROR}, arise from IBM's documented rule that a size error without an
\code{ON SIZE ERROR} phrase stores the truncated result, where GnuCOBOL and the suite leave the receiving item unchanged.
The others are due to three front-end bugs, a defect of the semantics in \code{INSPECT}, a file status that our version
could not express and an earlier program that did not run. In an exploratory census, later snapshots pass more of the suite (technical report).
Because our C semantics does not model printed output, the LLVM comparison covers only the exit status and the absence of undefined behaviour. Of the 25 stops at undefined behaviour, the sanitizer confirms 7, and in the others the semantics is
stricter than C or has a gap; our version also reports \code{exit} as undefined behaviour. The three mismatches are due to a front-end bug in hexadecimal floating-point constants of type \code{float} or \code{long double} (the ClangIR of
our theorems contains no such constant), to type punning through a union (Section~\ref{sec:limits}) and to C++ dynamic initializers, which the semantics does not run. Two of the ten timeouts follow a change to the interpreter's
stack, recorded in the deviation log (Appendix~\ref{app:prereg}). Exploratory re-runs on three later versions of the C semantics raise both the share of programs
with the reference status and the share of verdicts that match at each step (technical report).

\paragraph{Mutants of the semantics.} Each mutant changes an operator, a literal or a condition in the definitions of a
semantics, or for COBOL a rounding mode or a file-status code; it was rebuilt with its broken proofs replaced by
\code{sorry} and counted as killed when some differential test failed. The survivors cluster in features the suites
barely exercise: floating-point formatting and parsing in C (13 of 23 survivors), floating-point operations in Java (9
of 14), and less common statements and clauses in COBOL; a few are equivalent to the original. Suites extended in these
areas kill more of a fresh set of 30 mutants each: for COBOL under a pre-registered addendum, for Java and C in runs that
were not pre-registered. An agent whose tool log shows that it had not seen the mutants wrote the C tests.

\subsection{Axioms and kernel replay}

We printed the axioms of every theorem that we report as a result, from our own copies, and only the standard
axioms appear. Printing the
axioms is not enough. In a control, a false theorem added with kernel checking switched off compiled and reported no
axioms at all, and only a kernel replay rejected it. We therefore replayed, with Lean's \code{leanchecker}, every module of our packages and of Aeneas in the import closure of each such theorem, except modules that merely
import others. Where a module and its closure were byte-identical to ones replayed earlier, we reused that result. Mathlib, the packages it
depends on and Lean's core library were not replayed and are at the revisions pinned in the lake manifest. For the migration theorems, the replays cover 924 modules, together with the 68 modules of the COBOL package that
holds the COBOL-side theorems. One theorem of that package uses the native-evaluation axiom of \code{bv\_decide}. We do not report it, and it lies
outside the closure of the migration theorems. The tool that computed the import closures missed the 17 modules of
Aeneas's metaprogramming library. Byte-identical copies of these modules pass a replay for the migration, composite
and CBSTM03A theorems. For the Adler-32, jsmn and Thrift wire-format theorems of Section~\ref{sec:further}, they pass a
replay only in a later build that contains those theorems. The technical report~\cite{fvtechreport} gives the replay behind every result, including
exploratory re-checks on later versions of the semantics.

\subsection{Mutation test of the theorems}

Are the theorems vacuous, or too weak to tell a right translation from a wrong one? We seeded \aMutants{} mutants into
the proved translations, \aMutantsRust{} in Rust and \aMutantsJava{} in Java, five to eight per program and language.
Each mutant is a small edit, usually of one line. The categories are rounding mode, loop bound, truncation width,
swapped fields, and a dropped step, fallback, check or abend; a few mutants change the handling of end of file or the
state carried from one record to the next. For each mutant, a native harness runs the original and the mutant on one
admissible input and shows a difference in the output, while the original run against itself shows none. Since the
statement fixes the outputs on every admissible input, it is false for the mutant and has no proof. At the migration versions, that falsity rests on the native run, not on a Lean proof. When the extraction is
regenerated from the mutant (Aeneas for Rust, \code{javac} and Soot for Java) and checked with the unchanged statement
and proof scripts, the build of the theorem fails. It does so in every run reported by the session that ran these checks, and in each
of the six runs that we repeated. All \aMutants{} mutants are thus rejected, \aMutantsErr{} with an error and \aMutantsTimeout{} because a module did not
finish within the time limit of its run (about 30 minutes for two of them and 83 minutes
for the third). The three mutants that ran out of time are Java mutants. For each, a later exploratory Lean theorem refutes
the mutant's statement on the termination version of JimpleLean, also used by the composite theorems. That statement
is the generated one with the mutant program in place of the translation. On one input with one record per file that meets every premise, a run of the mutant ends with an outcome different
from the COBOL program's. The run is computed in the kernel by an evaluator proved sound for the Jimple
semantics.

The mutation test also checks the domains. Two mutants change the output only on inputs outside the earlier,
restricted domains: the CBACT04C mutant from Section~\ref{sec:example}, and one in which the duplicate-id abend of
CBTRN02C can no longer happen. For the Rust translations, the restricted theorems still check against both mutants,
whereas the full-domain theorems reject them.