Blame for code/notes/src/0304-failed-proof-to-bug.tex

\documentclass[11pt]{article}
\usepackage{common}
\begin{document}
\notehead{0304}{From failed proof to bug: counterexample search and the soundness\slash completeness asymmetry}{What a failed proof does and does not tell you, how to search for counterexamples (\texttt{decide}, property testing, model finding), and how to turn a counterexample into a \emph{confirmed} bug. Companion notebook: \texttt{notebooks/\allowbreak 0304-failed-proof-to-bug.ipynb}.}

\begin{problem}
\question{When does a failed proof justify the claim that the code has a bug, and what evidence turns the failure into a confirmed one?}
A prover that is asked to verify $S=\forall x.\,\varphi(x)$ (``the code meets its spec'') returns one of three things: a proof, a counterexample, or nothing within the budget. Only the first two are
information, and they are \emph{not symmetric}: a proof is a certificate that no bug exists (relative to the statement, 0301--0302), whereas a failed proof says almost nothing by itself, since the
statement may be true and the prover weak, the annotation may be weak, or the \emph{spec} may be the thing that is wrong. A bug-finding system must therefore convert a failure into evidence \emph{of a different kind}:
a concrete input on which the code visibly does the wrong thing. This note derives when that conversion is valid.
\end{problem}
\stepcounter{section}% the problem box counts as section 1: keeps every \S and notebook cross-reference stable

\section{Notation}
\begin{center}\small\begin{tabular}{@{}lP{10.5cm}@{}}\toprule
Symbol & Meaning\\\midrule
$S=\forall x.\,\varphi(x)$ & statement with $\varphi$ decidable (a $\Pi_1$ sentence over a countable domain)\\
$\vdash_T S$ & $S$ provable in the kernel's theory $T$ (0301)\\
$c$ & a candidate counterexample, $\neg\varphi(c)$\\
$p$ & per-test detection probability $\Pr[\neg\varphi(X)]$ for a random input $X\sim\mathcal D$\\
$N$, $\delta$ & number of tests, tolerated miss probability\\
$\mu(x)$ & shrinking measure (well-founded order on inputs)\\
$\mathrm{Reach}(S,P)$ & states visited by runs from initial states satisfying $P$\\
$(P,Q)$, $I$ & pre/postcondition and loop invariant of 0303\\\bottomrule\end{tabular}\end{center}

\section{Derivation}
\subsection{The verdict asymmetry}
Take a statement $S=\forall x.\varphi(x)$ with $\varphi$ decidable (a bounded numerical or finite-state property of a program is of this kind).
\begin{theorem}[Asymmetry]\label{thm:asym}
(i) If $\vdash_TS$ and $T$ is sound then $S$ is true. (ii) If $\neg\varphi(c)$ for some $c$, then $\vdash_T\neg S$ (the refutation is checkable by evaluation). (iii) The converses fail: $S$ true does not imply $\vdash_TS$, and no counterexample found within a finite budget does not imply $S$.
\end{theorem}
\emph{Proof.} (i) is the kernel-soundness assumption of 0301 (gated-reward theorem). (ii) $\varphi$ is decidable, so $\neg\varphi(c)$ is established by evaluating $\varphi(c)$ (Lean: \texttt{decide}, the kernel runs the \texttt{Decidable} instance, 0302, the lemma \texttt{of\_decide\_eq\_true}); then $S\to\varphi(c)$ is instantiation, so $\neg S$. (iii) By G\"odel's first incompleteness theorem, for every consistent recursively axiomatised $T$ interpreting arithmetic there is a true $\Pi_1$ sentence not provable in $T$ \cite{godel31}; its counterexample search never terminates and neither does its proof search. For finite searches: a counterexample may lie beyond the searched bound. $\square$

So the two searches are \emph{complementary semi-decision procedures} over $\Pi_1$ statements: proof search halts on provable truths, counterexample search halts on falsehoods, and the third region (true but unprovable in $T$, or merely beyond the budget) is covered by neither. The practical corollary: \textbf{a counterexample is certain evidence about the statement; the absence of one is not} (the notebook demonstrates this concretely in C2: \texttt{slim\_check} ``succeeds'' on a true statement and closes the goal with \texttt{sorry}).

VERINA's evaluator \cite{verina} \S4.1 (Fig.~3, Appendix~C.5) is this lattice made operational. Given a soundness/completeness relation $R$: ``prove $R$ and $\neg R$ with an LLM prover; if neither, try \texttt{decide}; else \texttt{plausible}''; outcomes are \emph{R holds} (proof), \emph{R does not hold} (counterexample), \emph{R might hold} (testing passed, no proof) and \emph{unknown}. They report error bars treating \emph{unknown} as the two extremes, and observe that when proofs succeed they always agree with testing while testing certifies $>40\%$ of specs against $<4\%$ proved (App.~C.5, Table~5) -- the asymmetry in numbers.

\subsection{Random testing: what a negative result is worth}
Let tests be i.i.d.\ draws $X_1,X_2,\dots\sim\mathcal D$ and $p=\Pr[\neg\varphi(X)]>0$. Then
\[
\Pr[\text{no failure in }N\text{ tests}]=(1-p)^N,\qquad T=\min\{t:\neg\varphi(X_t)\}\sim\mathrm{Geometric}(p),\ \ \mathbb E[T]=1/p.
\]
\emph{Derivation.} Independence gives $\Pr[\varphi(X_1)\wedge\cdots\wedge\varphi(X_N)]=\prod_t\Pr[\varphi(X_t)]=(1-p)^N$; $\Pr[T=t]=(1-p)^{t-1}p$; $\mathbb E[T]=\sum_{t\ge1}t(1-p)^{t-1}p=1/p$ (differentiate $\sum(1-p)^t=1/p$). Requiring $(1-p)^N\le\delta$:
\[
N\ \ge\ \frac{\ln\delta}{\ln(1-p)}\ \approx\ \frac{\ln(1/\delta)}{p}\qquad(p\ll1;\ \text{error: }\ln(1-p)=-p-p^2/2-\cdots,\ \text{relative error }O(p)).
\]
Consequences. A $1$-in-$1024$ bug needs $N=4714$ tests for $\delta=0.01$; a $1$-in-$2^{32}$ bug (a single bad 32-bit input) needs $N\approx2.97\times10^{10}$ for $\delta=10^{-3}$: no budget finds it, a proof or a solver does. A negative test run is therefore a statement about $p$: with $N$ clean tests the one-sided $1-\delta$ upper confidence bound is $p\le1-\delta^{1/N}\approx\ln(1/\delta)/N$ (the ``rule of three'' $3/N$ at $\delta=0.05$; with a uniform prior the posterior bound is $1-\delta^{1/(N+1)}$); it is \emph{never} $p=0$.
\textbf{Where $p$ comes from matters.} Uniform sampling detects a needle anywhere with probability $1-(1-1/K)^N\approx N/K$. If bugs cluster at small inputs (the \emph{small-scope hypothesis}, an empirical claim, not a theorem \cite{jackson}), enumeration $0,1,\dots,N-1$ detects iff $x_0<N$, i.e.\ with probability $1-(1-q)^N$ for $x_0\sim\mathrm{Geom}(q)$: with $K=2^{16},N=200,q=0.02$ this is $0.982$ versus $0.003$ (notebook B; Monte Carlo $0.9823$). Exhaustive enumeration up to a bound $B$ is \emph{complete within the bound}: if a counterexample of size $\le B$ exists, it finds it.

\subsection{Shrinking}
A random counterexample is large and noisy. Shrinking repeatedly replaces the current failing input $x$ by a smaller failing candidate. Candidates for lists here: delete an element; move an element one step toward $0$. Let $\mu(x)=(\mathrm{len},\sum|x_i|)$ in lexicographic order.
\begin{proposition}[Shrinking terminates in a local minimum]\label{prop:shrink}
If every accepted candidate has $\mu$ strictly smaller, the loop halts, at an $x^*$ that fails and none of whose candidates fails.
\end{proposition}
\emph{Proof.} $\mu$ takes values in $\N\times\N$ with lexicographic order, which is well-founded, so no infinite strictly decreasing chain exists. It halts only when no candidate fails. $\square$\\
\emph{Local is not global.} For the duplicate-dropping sort the global minimum is $[0,0]$, but $[1,1]$ is a local minimum: deleting gives $[1]$ (passes) and moving gives $[0,1]$ (passes). Measured (2000 random failures): final shrunk values $(-2,-2){:}420$, $(2,2){:}408$, $(0,0){:}401$, $(1,1){:}388$, $(-1,-1){:}383$, i.e.\ the global minimum in only $401/2000=20.1\%$ (the five outcomes are about equiprobable). A richer candidate set (``replace by $0$'', ``replace all equal elements at once'') shrinks the gap; the proposition guarantees only $\mu$-local minimality.

\subsection{Model finding: decide, property tests, omega, SMT}
\begin{center}\small\begin{tabular}{@{}P{2.4cm}P{4.7cm}P{4.4cm}P{4cm}@{}}\toprule
Tool & Positive answer & Negative answer & Complete when\\\midrule
\texttt{decide} & proof, kernel-checked & definite refutation ($\varphi(c)$ evaluates to \texttt{false}) & statement is bounded and decidable; slow\\
\texttt{slim\_check} (Plausible on newer pins) & counterexample with shrinking (\texttt{Found problems!}) & ``Success''\,+\,\texttt{sorry} warning (no certificate; $\mathrm{Ax}=\{\texttt{sorryAx}\}$) & never (statistical)\\
\texttt{omega} & proof & ``a possible counterexample may satisfy the constraints'' & \emph{never guaranteed}: no abstracted atoms \emph{and} a complete procedure; Lean's \texttt{omega} lacks dark/grey shadows\\
SMT / model finder & model & unsat = proof & decidable theory\\\bottomrule\end{tabular}\end{center}
\texttt{omega} deserves a derivation because its failure message looks like a counterexample, and there are two independent reasons it may not be one. (i) \emph{Abstraction.} \texttt{omega} abstracts non-linear subterms as fresh atoms: for the TRUE goal $n\le n\cdot n$ it reports $a-b\ge1,\ a\ge0$ with $a:=n,\ b:=n\cdot n$, satisfiable for an unconstrained atom $b$ yet impossible for $b=a^2$ (notebook C4: exhaustive check up to $10^5$ finds none; \texttt{Nat.le\_mul\_self} proves it). (ii) \emph{Incompleteness.} Presburger arithmetic is decidable \cite{presburger} and the full omega test decides it \cite{pugh91}, but only with the exact (``dark'' and ``grey'') shadows; Lean's implementation on this pin does not have them (its docstring: ``not yet a full decision procedure (no `dark' or `grey' shadows)'', \texttt{Init/Tactics.lean}, v4.9.0-rc1). It then falls back to the real relaxation, which can be satisfiable when the integer problem is not. Pugh's system $27\le11x+13y\le45,\ -10\le7x-9y\le4$ has real solutions (a parallelogram with vertices $(\tfrac{113}{190},\tfrac{299}{190}),(\tfrac{59}{38},\tfrac{29}{38}),(\tfrac{55}{38},\tfrac{85}{38}),(\tfrac{457}{190},\tfrac{271}{190})$) but no integer point (checked on its bounding box $[-1,3]^2$), and \texttt{omega} nevertheless answers ``a possible counterexample may satisfy the constraints'' with no atoms to blame (notebook C4b). \emph{A failure message is a counterexample only if the atoms are substituted back and the procedure is complete; otherwise it is a lead.}

\subsection{Turning a counterexample into a confirmed bug}
Fix code $S$, precondition $P$, postcondition $Q$ (0303). Let $\mathrm{run}(S,\sigma_0)$ be the (deterministic) execution.
\begin{lemma}[Witness]\label{lem:wit}
$\sigma_0$ is a bug witness for $[P]\,S\,[Q]$ iff $\sigma_0\models P$ and $\mathrm{run}(S,\sigma_0)$ terminates in $\sigma'\not\models Q$ or does not terminate.
\end{lemma}
\emph{Proof.} Negation of the definition of total correctness. $\square$

\begin{lemma}[What a violated loop VC proves]\label{lem:vc}
Let $s$ violate a loop verification condition and let $\mathrm{Reach}(S,P)$ be the set of loop-head states visited by runs from $P$-states.
(a) If $s\notin\mathrm{Reach}$, no conclusion about $S$ follows.
(b) \emph{Preserve} VC ($I\wedge b\Rightarrow\wpc(c,I)$) violated at a reachable $s$: the successor $s'$ of $s$ (one body execution) is reachable and $s'\not\models I$, so $I$ is not an invariant of this program (annotation or code is wrong), but $Q$ may still hold.
(c) \emph{Exit} VC ($I\wedge\neg b\Rightarrow Q$) violated at a reachable $s$: the loop \emph{exits} in $s$, so the run reaching $s$ ends in a state $\not\models Q$: by Lemma~\ref{lem:wit} this \emph{is} a bug witness (of the code or of the spec $Q$).
\end{lemma}
\emph{Proof.} The VC quantifies over \emph{all} states satisfying its antecedent, not only reachable ones, so a violating $s$ outside $\mathrm{Reach}$ refutes nothing about executions (a). (b) $s\models I\wedge b$, so the body runs from $s$ and, the language being deterministic, the visited successor $s'$ is the state making the consequent false. (c) $s\models\neg b$, so $\langle W,s\rangle\Downarrow s$ (loop rule for $\sigma\not\models b$), and $s\not\models Q$. $\square$\\
An earlier draft of this lemma said that a reachable violation always leaves $Q$ possibly intact; (c) shows that is false for exit VCs (example B of notebook C7: right invariant, right code, wrong postcondition $2s=n(n{+}1)$: 7 reachable exit violations, each a real run violating $Q$). Example D (invariant too strong, $i\le5$): 2 reachable preserve violations, $I$ not invariant, yet $Q$ holds on every run.

Protocol (notebook, last cell):
\begin{enumerate}[nosep]
\item \textbf{Counterexample} $c$ from \texttt{decide}/\texttt{slim\_check}/solver (shrink it, Prop.~\ref{prop:shrink}).
\item \textbf{Admissible?} Does $c$ satisfy the preconditions the statement \emph{really} assumes? ($a-b+b=a$ for $a=0,b=2$: a counterexample to the \emph{statement}; the spec lacks $b\le a$, 0302, the truncated-subtraction lemma.)
\item \textbf{Reachable?} If $c$ is an internal state (a VC counterexample), is it in $\mathrm{Reach}$, and which VC does it violate? (Lemma~\ref{lem:vc}: unreachable $\Rightarrow$ nothing; reachable preserve-violation $\Rightarrow$ the annotation is not invariant; reachable exit-violation $\Rightarrow$ a real run violates $Q$.)
\item \textbf{Evaluate concretely}: run the code on the initial input (Lemma~\ref{lem:wit}); compare with an independent oracle if one exists.
\item \textbf{Intent}: does the specification say what was meant? A violation of a wrong spec is a spec bug (0305).
\item \textbf{Certify and pin}: express the violation as a kernel-checked refutation (below) and add a regression test.
\end{enumerate}

\paragraph{Kernel-certified refutation (notebook C1).} With the loop as a structurally recursive function on fuel (so \texttt{decide} can unfold it):
\begin{lstlisting}
theorem bug_witness : ¬ Post (fun _ => false) 10 (searchBadF (fun _ => false) 10 20 0) := by decide
theorem searchBadF_not_correct :
    ¬ (∀ (P : Nat → Bool) (len : Nat), Post P len (searchBadF P len len 0)) := fun h => by
  have := h (fun _ => false) 10
  revert this
  decide
#print axioms searchBadF_not_correct     -- does not depend on any axioms
\end{lstlisting}
This is Theorem~\ref{thm:asym}(ii) executed: the counterexample \emph{is} a proof of $\neg S$, with an empty axiom set. (For well-founded recursion \texttt{decide} cannot unfold; \texttt{\#eval} still confirms, but is evidence, not a kernel certificate.)

\subsection{A real example: a soundness bug found by a failed proof}
Carneiro's Lean4Lean \cite{lean4lean} \S4.1: to verify \texttt{inferLambda} one must prove that \texttt{cheapBetaReduce} preserves definitional equality; that needs \texttt{hasLooseBVars} (defined as \texttt{looseBVarRange > 0}); \texttt{looseBVarRange} is read from a 20-bit field of a 64-bit \texttt{e.data}. The proof could not be completed because ``what happens on overflow?'' had no good answer: the overflow check used \texttt{panic!}, which \emph{continues with the default value}, $0$ for \texttt{UInt64}, ``the worst possible answer in this case, since it effectively turns on all of the optimizations''. The author describes it as ``a bug that was found entirely theoretically, by failing to prove a theorem and working backwards to an actual exploitable soundness bug'', reported and fixed. In the language of this note: failed proof $\to$ locate the unproved side-condition $\to$ ask what input falsifies it $\to$ reachable? yes $\to$ evaluate $\to$ confirmed. The paper also records the sobering part: the fix (making \texttt{Expr.data} opaque) ``at most masks the performance''.

\section{Boxed result}
\begin{result}
\textbf{R1.} For $S=\forall x.\varphi(x)$, $\varphi$ decidable: proof $\Rightarrow$ true; counterexample $c\Rightarrow\vdash\neg S$ (certain); no proof and no counterexample $\Rightarrow$ nothing (G\"odel; finite budgets).\\
\textbf{R2.} $\Pr[\text{miss after }N]=(1-p)^N$; $\mathbb E[T]=1/p$; $N\ge\ln\delta/\ln(1-p)\approx\ln(1/\delta)/p$.\\
\textbf{R3.} Shrinking with a strictly decreasing well-founded measure terminates in a \emph{local} minimum (not necessarily global).\\
\textbf{R4.} Bug witness $\iff P(\sigma_0)\wedge\mathrm{run}(S,\sigma_0)\not\models Q$; a violated VC proves something only if its state is reachable (preserve: $I$ is not invariant; exit: $Q$ fails in a real run), and a witness is certified by evaluation; \texttt{decide} turns a witness into a kernel-checked $\neg S$.\\
\textbf{R5.} \texttt{omega}'s failure message is a genuine countermodel only if the goal has no abstracted non-linear atoms \emph{and} the procedure is complete; on this pin it is not (Pugh's system), so the message is a lead.
\end{result}

\paragraph{Numerical verification (notebook 0304, all cells executed).}
\begin{center}\small\begin{tabular}{@{}P{7.6cm}P{4.3cm}P{3.6cm}@{}}\toprule
Identity & measured vs predicted & error\\\midrule
R2: exact $p$ by enumeration (19,531 lists; 19,205 failing) & $p=0.498514$ & exact\\
R2: mean tests to failure, 20,000 runs & $1.992\pm0.010$ vs $1/p=2.006$ & $1.43$ s.e.\\
R2: $P(\text{miss after }N)$, $N\in\{1,5,10,20,40,80\}$ & vs $(1-p)^N$ & worst $|z|=1.59$\\
R2 (needle $p=1/1024$): mean tests; $N\in\{256,\dots,4096\}$ & $1015.6\pm18.3$ vs $1024$; worst $|z|=0.89$ & $<1$ s.e.\\
B: enumeration vs random on clustered needle & $0.9823$ vs theory $0.9824$ & $1\times10^{-4}$\\
R3: shrinks always fail and are locally minimal; global minimum reached & 2000/2000; $401/2000$ global & --- (reported, not asserted)\\
R4: Lean \texttt{searchBadF\_not\_correct} & kernel-checked, axioms $\emptyset$ & ---\\
R1: \texttt{slim\_check} on a true goal & ``Success'' + \texttt{sorry}; $\mathrm{Ax}=\{\texttt{sorryAx}\}$ & gate rejects\\
R4/Lemma~\ref{lem:vc}: weakened VC, exhaustive scope ($P\in2^{4},\,len\le4,\,n\le len$) & 111 VC counterexamples, 0 reachable (Python $=$ Lean count $111$); 129 reachable states, 0 violate & 0\\
R4: exhaustive scope, Python vs Lean \texttt{\#eval}: buggy loop violations & $15=15$; correct loop $0=0$ & 0\\
R4/Lemma~\ref{lem:vc}(b,c): sum program, 4 scenarios (weak $I$; wrong $Q$; buggy code; too-strong $I$), VC violations classified by reachability & exit viol.\ 504/0 reachable, 7/7, preserve 28/7, 2/2 & lemma holds in all 4\\
R5: \texttt{omega} on $n\le n\cdot n$; exhaustive $n<10^5$ & fails; no counterexample exists & spurious\\
R5: \texttt{omega} on Pugh's system (no atoms); real polytope non-empty, no integer point in its bounding box & fails with ``possible counterexample'' & spurious (incomplete)\\\bottomrule\end{tabular}\end{center}

\section{What breaks}
\begin{center}\small\begin{tabular}{@{}P{3.6cm}P{6.4cm}P{5.5cm}@{}}\toprule
Failure & Mechanism & Assumption violated\\\midrule
Treating ``no counterexample'' as proof & $(1-p)^N$ never reaches $0$; \texttt{slim\_check} returns \texttt{sorry} & $p$ is large enough for the budget\\
Counterexample to the statement, not the code & $a-b+b=a$ fails at $(0,2)$; the spec forgot $b\le a$ & the statement equals the intended spec\\
Spurious VC counterexample & weak invariant: unreachable state (111/111 unreachable in the scope) & the VC's quantified state is reachable\\
Abstraction / incompleteness in the tool & \texttt{omega} atomises $n\cdot n$; and (no dark/grey shadows) fails on integer-infeasible but real-feasible linear systems & the goal is in the fragment \emph{and} the procedure is complete for it\\
Non-uniform bug distributions & uniform tests miss boundary bugs by factors of $>300$ (B) & the generator matches where bugs live\\
Generator coverage & \texttt{slim\_check} discards samples that violate guards and samples functions and large structures shallowly & the generator reaches the failing region\\
Local-minimum shrinking & reported counterexample not minimal & shrinker explores enough neighbours\\
Non-determinism / environment & a ``bug'' that depends on time, hash seeds, floating point order & the code under test is a deterministic function of its inputs\\
\texttt{decide} limits & wf-recursive or large functions cannot be kernel-evaluated; \texttt{native\_decide} would widen the trusted base (0301) & the computation is kernel-feasible\\\bottomrule\end{tabular}\end{center}

\nextnote{0305: the opposite failure. When a proof \emph{succeeds} but the statement was wrong: LLM-written specs, spec validation by tests and mutation, and the ``proof of the wrong theorem'' (statement rewrite) finding in this repository.}

\begin{small}
\begin{thebibliography}{99}
\bibitem{lean4lean} M.~Carneiro, \emph{Lean4Lean}, arXiv:2403.14064, \S4.1 ``Bit tricks and soundness bugs'' (quotations above are from this section).
\bibitem{verina} Z.~Ye et al., \emph{VERINA}, arXiv:2505.23135, \S4.1 (soundness/completeness of $\hat P,\hat Q$; evaluator of Fig.~3: prove, then \texttt{decide}, then \texttt{plausible}; outcomes ``R holds / does not hold / might hold / unknown''), Appendix~C.5 (Lean implementation; Table~5: proofs $<4\%$ vs testing $>40\%$ on generated specs; the 20 manually inspected disagreements were all correct).
\bibitem{fvapps} Q.~Dougherty, R.~Mehta, \emph{FVAPPS}, arXiv:2502.05714, \S II-B/C: stage 5 filters theorem statements with Lean's property-based testing framework Plausible (``probably true''); 1083 of 4715 samples pass all five stages.
\bibitem{godel31} K.~G\"odel (1931), first incompleteness theorem. \emph{Not on arXiv; not fetched; classical, cited for the named theorem.}
\bibitem{presburger} M.~Presburger (1929), decidability of linear integer arithmetic. \emph{Not on arXiv; not fetched; classical.}
\bibitem{pugh91} W.~Pugh, ``The Omega test'', CACM 1991. \emph{Not on arXiv; not fetched; classical.}
\bibitem{jackson} D.~Jackson, \emph{Software Abstractions} (Alloy; the small-scope hypothesis) and K.~Claessen, J.~Hughes, ``QuickCheck'', ICFP 2000. \emph{Not on arXiv; not fetched. The small-scope hypothesis is empirical; the notebook only quantifies what it buys if true.}
\end{thebibliography}
\end{small}
\end{document}