| \documentclass[11pt]{article} |
| \usepackage{common} |
| \begin{document} |
| \notehead{0303}{Hoare logic and refinement: specifying and verifying code}{Pre/postconditions, verification conditions, loop invariants, and a verified linear search in Lean~4. Companion notebook: \texttt{notebooks/\allowbreak 0303-hoare-refinement.ipynb}.} |
|
|
| \begin{problem} |
| \question{How do we turn ``the code does what it should'' into finitely many statements a prover can check, loops included?} |
| Notes 0301--0302 certify mathematical statements. A \emph{program} is not a statement: it is an object that does something. To ask a prover to |
| verify code we must (i) turn ``what the code is supposed to do'' into a \emph{statement} (a specification), (ii) reduce ``the code meets the spec'' |
| to statements about \emph{finitely many} points of the program (verification conditions), and (iii) handle loops, whose behaviour is an unbounded |
| sequence of steps, with one finite object: an \emph{invariant}. Hoare logic does (i)--(iii). Refinement is the converse direction: derive code from a spec |
| so that correctness holds by construction. Every benchmark in note 0306 is, in the end, a Hoare-triple generator and checker. |
| \end{problem} |
| \stepcounter{section} |
|
|
| \section{Notation} |
| \begin{center}\small\begin{tabular}{@{}lP{10.4cm}@{}}\toprule |
| Symbol & Meaning\\\midrule |
| $\sigma$ & state: map from program variables to $\Z$\\ |
| $\sem{e}\sigma$, $\sigma\models B$ & value of expression $e$ in $\sigma$; Boolean assertion $B$ true in $\sigma$\\ |
| $\langle S,\sigma\rangle\Downarrow\sigma'$ & big-step evaluation: running $S$ from $\sigma$ ends in $\sigma'$\\ |
| $\hoare PSQ$ & Hoare triple: \emph{partial} correctness $=$ every terminating run from a $P$-state ends in a $Q$-state\\ |
| $[P]\,S\,[Q]$ & \emph{total} correctness $=$ additionally every run from a $P$-state terminates\\ |
| $Q[e/x]$ & $Q$ with $e$ substituted for $x$\\ |
| $\wpc(S,Q)$ & weakest precondition: $\{\sigma\mid\exists\sigma'.\ \langle S,\sigma\rangle\Downarrow\sigma'\wedge\sigma'\models Q\}$ (total)\\ |
| $I$, $V$ & loop invariant; variant (a $\Z$-valued term, $\ge0$ and strictly decreasing)\\ |
| $S\sqsubseteq T$ & $T$ refines $S$: $\wpc(S,Q)\subseteq\wpc(T,Q)$ for all $Q$\\ |
| $x{:}[\mathit{pre},\mathit{post}]$ & specification statement: ``from a $\mathit{pre}$ state, change $x$ so that $\mathit{post}$ holds''\\\bottomrule\end{tabular}\end{center} |
|
|
| \section{Derivation} |
| \subsection{Language and semantics} |
| $S::=\texttt{skip}\mid x:=e\mid S_1;S_2\mid\texttt{if }b\texttt{ then }S_1\texttt{ else }S_2\mid\texttt{while }b\texttt{ do }c$. Evaluation: |
| \[ |
| \langle x{:=}e,\sigma\rangle\Downarrow\sigma[x{\mapsto}\sem e\sigma],\qquad |
| \frac{\sigma\not\models b}{\langle\texttt{while }b\texttt{ do }c,\sigma\rangle\Downarrow\sigma},\qquad |
| \frac{\sigma\models b\ \ \langle c,\sigma\rangle\Downarrow\sigma'\ \ \langle\texttt{while }b\texttt{ do }c,\sigma'\rangle\Downarrow\sigma''}{\langle\texttt{while }b\texttt{ do }c,\sigma\rangle\Downarrow\sigma''} |
| \] |
| (and the obvious rules for \texttt{skip}, sequence, conditional). The language is deterministic: $\Downarrow$ is a partial function. A loop that never ends has no $\sigma''$. |
|
|
| \subsection{The assignment axiom, derived} |
| \begin{lemma}[Substitution]\label{lem:sub} $\sigma\models Q[e/x]\iff\sigma[x{\mapsto}\sem e\sigma]\models Q$.\end{lemma} |
| \emph{Proof.} Induction on $Q$; the atomic case is induction on terms: $\sem{t[e/x]}\sigma=\sem t{\sigma[x\mapsto\sem e\sigma]}$ because a variable $y\neq x$ evaluates identically in both, and $x$ evaluates to $\sem e\sigma$ on the right and to $\sem{e}\sigma$ on the left. Connectives commute with substitution. $\square$ |
|
|
| \begin{proposition}[Assignment]\label{prop:asg} $\wpc(x{:=}e,Q)=Q[e/x]$, hence $\hoare{Q[e/x]}{x:=e}{Q}$.\end{proposition} |
| \emph{Proof.} $x{:=}e$ always terminates in $\sigma[x\mapsto\sem e\sigma]$; apply Lemma~\ref{lem:sub}. $\square$\\ |
| (The easy-to-get-wrong direction is the arrow: the \emph{postcondition} is rewritten, working backwards. The ``forward'' pattern $\{P\}x{:=}e\{P\wedge x=e\}$ is unsound when $x$ occurs in $e$.) |
|
|
| \subsection{Sequence and conditional} |
| $\wpc(S_1;S_2,Q)=\wpc(S_1,\wpc(S_2,Q))$: from $\sigma$, $S_1$ ends in a unique $\sigma_1$ and then $S_2$ must end in $Q$, which is $\sigma_1\in\wpc(S_2,Q)$, which is $\sigma\in\wpc(S_1,\wpc(S_2,Q))$. For \texttt{if}: $\wpc=(b\wedge\wpc(S_1,Q))\vee(\neg b\wedge\wpc(S_2,Q))$ by splitting on $\sigma\models b$. The notebook checks both by running 300 random programs on 49 states each: $\wpc$ computed by these syntactic rules coincides with the set obtained by \emph{executing}: 0 mismatches over 14,700 pairs. |
|
|
| \subsection{Loops: the weakest precondition is a least fixed point} |
| Let $W=\texttt{while }b\texttt{ do }c$. Unfolding once: $\wpc(W,Q)=(\neg b\wedge Q)\vee(b\wedge\wpc(c,\wpc(W,Q)))$. This is an equation, not a definition, so it does not give a formula. Define the iterates |
| \[ |
| W_0=\emptyset,\qquad W_{k+1}=(\neg b\wedge Q)\vee\bigl(b\wedge\wpc(c,W_k)\bigr),\qquad\wpc(W,Q)=\bigcup_kW_k. |
| \] |
| $W_k$ is ``terminates in $Q$ after $<k$ iterations''. (Proof of the union formula: a terminating run takes some finite $k$ iterations, and then $\sigma\in W_{k+1}$ by induction on $k$ reading the evaluation rules; conversely $\sigma\in W_k$ exhibits a run.) The operator $F(X)=(\neg b\wedge Q)\vee(b\wedge\wpc(c,X))$ is monotone (as $\wpc(c,\cdot)$ is), so $W_k\subseteq W_{k+1}$ by induction. It is also \emph{continuous}: $\wpc(c,\bigcup_kX_k)=\bigcup_k\wpc(c,X_k)$ for an increasing chain, because $c$ is deterministic ($\sigma\in\wpc(c,X)$ means the unique end state $\sigma'$ lies in $X$, and $\sigma'\in\bigcup_kX_k$ means $\sigma'\in X_k$ for some $k$). Hence $F(\bigcup_kW_k)=\bigcup_kF(W_k)=\bigcup_kW_{k+1}=\bigcup_kW_k$ and, by Kleene's argument, $\bigcup_kW_k$ is the \emph{least} fixed point (any fixed point $Y$ contains $W_0=\emptyset$, and $W_k\subseteq Y\Rightarrow W_{k+1}=F(W_k)\subseteq F(Y)=Y$). No closed form exists in general (it can encode the halting problem), which is why we \emph{guess} an $I$. |
|
|
| \begin{theorem}[Total-correctness invariant rule]\label{thm:inv} |
| If (1) $I\wedge\neg b\Rightarrow Q$; (2) $I\Rightarrow V\ge0$; (3) $I\wedge b\wedge V{=}v_0\Rightarrow\wpc(c,I\wedge V{<}v_0)$ ($v_0$ fresh), then $I\Rightarrow\wpc(W,Q)$. |
| \end{theorem} |
| \emph{Proof.} Show: $\sigma\models I\Rightarrow\sigma\in W_{V(\sigma)+1}$, by strong induction on $v=V(\sigma)\ge0$. |
| If $\sigma\not\models b$: by (1) $\sigma\models Q$, so $\sigma\in W_1\subseteq W_{v+1}$. |
| If $\sigma\models b$: by (3) $c$ terminates in some $\sigma'$ with $\sigma'\models I$ and $V(\sigma')<v$. By the IH, $\sigma'\in W_{V(\sigma')+1}\subseteq W_v$ (monotone, as $V(\sigma')+1\le v$). Then $\sigma\in W_{v+1}$ by the definition of $W_{v+1}$. $\square$ |
|
|
| \begin{theorem}[Partial invariant rule]\label{thm:pinv} |
| If $\hoare{I\wedge b}{c}{I}$ then $\hoare{I}{W}{I\wedge\neg b}$. |
| \end{theorem} |
| \emph{Proof.} Let $\langle W,\sigma\rangle\Downarrow\sigma''$ with $\sigma\models I$. Induction on the derivation. Case $\sigma\not\models b$: $\sigma''=\sigma\models I\wedge\neg b$. Case $\sigma\models b$ with $\langle c,\sigma\rangle\Downarrow\sigma'$ and $\langle W,\sigma'\rangle\Downarrow\sigma''$: $\sigma\models I\wedge b$ so $\sigma'\models I$ (premise); the IH on the shorter derivation gives $\sigma''\models I\wedge\neg b$. $\square$ |
|
|
| \subsection{Verification conditions} |
| Annotate every loop with $(I,V)$. Define $\wpc'$ as $\wpc$ with $\wpc'(W,Q):=I$, and the side conditions |
| \[ |
| \mathrm{vc}(x{:=}e,Q)=\emptyset,\ \ \mathrm{vc}(S_1;S_2,Q)=\mathrm{vc}(S_1,\wpc'(S_2,Q))\cup\mathrm{vc}(S_2,Q),\ \ \mathrm{vc}(\texttt{if},Q)=\mathrm{vc}(S_1,Q)\cup\mathrm{vc}(S_2,Q), |
| \] |
| \[ |
| \mathrm{vc}(W,Q)=\{\,I\wedge\neg b\Rightarrow Q,\ \ I\Rightarrow V\ge0,\ \ I\wedge b\wedge V{=}v_0\Rightarrow\wpc'(c,\,I\wedge V{<}v_0)\,\}\cup\mathrm{vc}\bigl(c,\,I\wedge V{<}v_0\bigr), |
| \] |
| with a \emph{fresh ghost} $v_0$ per loop, regarded as a logical constant the program never assigns (the VCs are valid iff they hold for every value of the ghosts; an inner loop's invariant must therefore record the outer ghost; the notebook's nested example does so with $n-i=g_1$). The body is verified against the \emph{single} postcondition $I\wedge V{<}v_0$, not against $I$ and $V{<}v_0$ separately: for a nested loop the separate form never generates the inner exit VC for $V{<}v_0$, and the termination argument of the outer loop is unchecked. (Reporting the $I$-part alone, $I\wedge b\wedge V{=}v_0\Rightarrow\wpc'(c,I)$, is convenient for diagnosis: the notebook calls it \emph{preserve}.) |
| \begin{theorem}[VC soundness]\label{thm:vc} If every formula in $\{P\Rightarrow\wpc'(S,Q)\}\cup\mathrm{vc}(S,Q)$ is valid, then $[P]\,S\,[Q]$.\end{theorem} |
| \emph{Proof.} Structural induction on $S$, showing $\wpc'(S,Q)\subseteq\wpc(S,Q)$ whenever $\mathrm{vc}(S,Q)$ is valid. Assign, \texttt{skip}: equality. Sequence and \texttt{if}: monotonicity of $\wpc$ plus IH. Loop: the IH for $c$ with postcondition $R=I\wedge V{<}v_0$ (its VCs $\mathrm{vc}(c,R)$ are valid) gives $\wpc'(c,R)\subseteq\wpc(c,R)$, so condition (3) of Theorem~\ref{thm:inv} holds; (1) and (2) are the first two VCs; hence $I\subseteq\wpc(W,Q)$. Finally $P\subseteq\wpc'(S,Q)\subseteq\wpc(S,Q)$. $\square$ |
|
|
| \paragraph{Worked example (notebook A2).} $\{n\ge0\}\ i{:=}0;\,s{:=}0;\,\texttt{while }i<n\ \texttt{do }s{:=}s+i;\,i{:=}i+1\ \{2s=n(n-1)\}$ with |
| $I\equiv0\le i\le n\wedge2s=i(i-1)$ and $V=n-i$. Check by hand: init: $\wpc'(i{:=}0;s{:=}0,I)=I[0/s][0/i]=(0\le0\le n\wedge0=0)$, implied by $n\ge0$. Preserve: $\wpc(s{:=}s{+}i;i{:=}i{+}1,I)=0\le i{+}1\le n\wedge2(s{+}i)=(i{+}1)i$; from $I\wedge i<n$: $2s=i(i-1)$ so $2(s+i)=i(i-1)+2i=i(i+1)$. \checkmark\ Exit: $i=n$ (from $i\le n$, $\neg i<n$) and $2s=n(n-1)$. \checkmark\ Variant: $n-i\ge0$, decreases by 1. |
|
|
| \subsection{Five ways a verification attempt can fail, and what each means} |
| \begin{center}\small\begin{tabular}{@{}P{4.2cm}P{4.8cm}P{6.5cm}@{}}\toprule |
| Annotation & Failing VC & Meaning (notebook A3)\\\midrule |
| $I'=0\le i\le n$ (too weak) & exit: counterexample $(n,i,s)=(0,0,-2)$ & program correct; the state is \emph{unreachable} from any $P$-state: a proof artefact, not a bug\\ |
| $I''=\cdots\wedge i<n$ (too strong) & init and preserve & program correct; annotation wrong\\ |
| Right $I$, code $s{:=}s{+}i{+}1$ & preserve: $(n,i,s)=(1,0,0)$ & \emph{real bug}: running from $n=1$ violates $Q$\\ |
| Right $I$, post $2s=n(n{+}1)$ & exit & spec disagrees with code; run violates it too\\ |
| Right $I$ and code, variant $V=i$ (grows) & variant-decrease & program correct and terminating; the \emph{termination argument} is wrong\\\bottomrule\end{tabular}\end{center} |
| A failed VC is therefore a \emph{question}, not a verdict (note 0304 turns it into a decision procedure). |
|
|
| \subsection{Refinement: derive code from the spec} |
| View the specification statement $x{:}[\mathit{pre},\mathit{post}]$ as the predicate transformer $\wpc_{\mathrm{spec}}(Q)(\sigma)=\mathit{pre}(\sigma)\wedge\forall x'.\,\mathit{post}(\sigma,x')\Rightarrow Q(x')$. Refinement $S\sqsubseteq T$ means every postcondition guaranteed by $S$ is guaranteed by $T$. |
| \begin{proposition}[Assignment refinement law]\label{prop:ref} |
| $x{:}[\mathit{pre},\mathit{post}]\sqsubseteq x{:=}e\iff\mathit{pre}\Rightarrow\mathit{post}[e/x]$. |
| \end{proposition} |
| \emph{Proof.} ($\Leftarrow$) Let $\sigma\in\wpc_{\mathrm{spec}}(Q)$: then $\mathit{pre}(\sigma)$, so $\mathit{post}(\sigma,e(\sigma))$, and instantiating $x'=e(\sigma)$ gives $Q(e(\sigma))=\wpc(x{:=}e,Q)(\sigma)$ by Prop.~\ref{prop:asg}. |
| ($\Rightarrow$) Take $Q:=\mathit{post}(\sigma,\cdot)$ at a fixed start state $\sigma$. Then $\wpc_{\mathrm{spec}}(Q)(\sigma)=\mathit{pre}(\sigma)$ (the quantified implication is trivially true), while $\wpc(x{:=}e,Q)(\sigma)=\mathit{post}(\sigma,e(\sigma))$; refinement forces $\mathit{pre}(\sigma)\Rightarrow\mathit{post}(\sigma,e(\sigma))$. $\square$ |
|
|
| \paragraph{Functional specifications.} For a pure function $f$ with pre $P$ and post $Q$ (the VERINA format \cite{verina} \S3.1), ``$f$ meets the spec'' is $\forall x.\ P(x)\Rightarrow Q(x,f(x))$, i.e.\ the triple $\{P(x)\}\,y{:=}f(x)\,\{Q(x,y)\}$ with $x$ a frozen logical variable. CLEVER's form $\exists r.\ \mathrm{impl}\,x=r\wedge\mathrm{spec}\,r$ \cite{clever} Fig.~2 is the same statement with termination built in (total correctness): in Lean every \texttt{def} terminates, so $[P]\,S\,[Q]$ is the default and \texttt{partial def} (no termination proof) is opaque to the kernel. |
|
|
| \subsection{A worked example in Lean 4: verified linear search} |
| Dafny's \texttt{LinearSearch} (DafnyBench Fig.~2 \cite{dafnybench}) has postcondition $0\le n\le|a|$, $n=|a|\vee P(a[n])$, $\forall i<n,\ \neg P(a[i])$ and loop invariants $0\le n\le|a|$ and $\forall i<n,\ \neg P(a[i])$. Abstracting $a[i]$ by a predicate on indices: |
| \begin{lstlisting} |
| def search (P : Nat → Bool) (len n : Nat) : Nat := |
| if n < len then (if P n then n else search P len (n + 1)) else n |
| termination_by len - n -- the VARIANT; Lean demands it |
|
|
| def Post (P : Nat → Bool) (len r : Nat) : Prop := |
| r ≤ len ∧ (r = len ∨ P r = true) ∧ ∀ i, i < r → P i = false |
|
|
| theorem search_inv (P : Nat → Bool) (len : Nat) : |
| ∀ n, n ≤ len → (∀ i, i < n → P i = false) → Post P len (search P len n) |
| -- proof: strong induction on len - n; exit branch: I ∧ ¬b ⇒ Q; recursive branch: I ∧ b ∧ ¬P n ⇒ I[n+1/n] |
|
|
| theorem search_correct (P : Nat → Bool) (len : Nat) : Post P len (search P len 0) |
| \end{lstlisting} |
| The invariant \emph{is} the induction hypothesis of \texttt{search\_inv}: its premise is $I$; the recursive call is the loop back-edge and needs $I[n{+}1/n]$ (preserve); the else-branch is the exit condition. The whole development compiles, and \texttt{\#print axioms search\_correct} gives $\{\texttt{propext},\texttt{Quot.sound}\}$ (notebook B). The off-by-one loop (\texttt{n + 1 < len}) with the \emph{same} proof script is refused: \texttt{omega could not prove the goal} at the exit branch, where $r=len$ would be required; and |
| \texttt{\#eval searchBad (fun \_ => false) 10 0} returns \texttt{9}, \texttt{\#eval decide (Post \dots)} returns \texttt{false} (the correct loop returns \texttt{10}, \texttt{true}). FVAPPS \cite{fvapps} \S III.E observes the practical corollary: solutions written with imperative \texttt{Id.run do} loops hide the inductive structure the proof needs, so verifiable code is written as recursion whose shape mirrors its invariant. |
|
|
| \subsection{Integers: when the spec lives in $\Z$ and the code in $\mathrm{int}_{w}$} |
| Binary search computes $\mathit{mid}=(lo+hi)/2$ with VC $lo\le hi\Rightarrow lo\le\mathit{mid}\le hi$. This is valid over $\Z$. Over $w$-bit unsigned words, $lo+hi$ wraps to $lo+hi-2^w$ when $lo+hi\ge2^w$, so $\mathit{mid}=\lfloor(lo+hi-2^w)/2\rfloor<lo\iff hi-lo<2^w$, which always holds. \emph{Hence the VC fails exactly when $lo+hi\ge2^w$} (for $lo\le hi$). Counting for $w=8$: ordered pairs with $lo+hi\ge256$: $\sum_{lo=1}^{255}lo=32640$; of these $128$ lie on the diagonal ($2lo\ge256$); unordered with $lo\le hi$: $(32640+128)/2=16384$. The safe midpoint $lo+\lfloor(hi-lo)/2\rfloor$ never overflows. |
|
|
| \section{Boxed result} |
| \begin{result} |
| \textbf{R1.} $\wpc(x{:=}e,Q)=Q[e/x]$; $\wpc(S_1;S_2,Q)=\wpc(S_1,\wpc(S_2,Q))$; $\wpc(\texttt{if},Q)=(b\wedge\wpc(S_1,Q))\vee(\neg b\wedge\wpc(S_2,Q))$.\\ |
| \textbf{R2.} $\wpc(\texttt{while }b\texttt{ do }c,Q)=\mathrm{lfp}\,X.\,(\neg b\wedge Q)\vee(b\wedge\wpc(c,X))$; invariant rule: $I\wedge\neg b\Rightarrow Q$, $I\Rightarrow V\ge0$, $I\wedge b\wedge V{=}v_0\Rightarrow\wpc(c,I\wedge V{<}v_0)\ \Longrightarrow\ I\Rightarrow\wpc(W,Q)$.\\ |
| \textbf{R3.} VC soundness: all VCs valid $\Rightarrow[P]\,S\,[Q]$.\\ |
| \textbf{R4.} $x{:}[\mathit{pre},\mathit{post}]\sqsubseteq x{:=}e\iff\mathit{pre}\Rightarrow\mathit{post}[e/x]$.\\ |
| \textbf{R5.} $w$-bit midpoint VC fails iff $lo+hi\ge2^w$ ($lo\le hi$); count $=2^{2w-2}$ for $w=8$ ($16384$). |
| \end{result} |
|
|
| \paragraph{Numerical verification (notebook 0303, all cells executed).} |
| \begin{center}\small\begin{tabular}{@{}P{8.4cm}P{3.5cm}P{3.6cm}@{}}\toprule |
| Identity & size & max abs error / violations\\\midrule |
| R1: $\wpc_{\mathrm{syn}}$ vs executing, 300 random loop-free programs $\times$ 49 states & 14,700 pairs & 0 mismatches\\ |
| R2/R3: all VCs valid (ghost $v_0$ quantified over $[-12,12]$, so the variant-decrease VC is genuinely evaluated) $\Rightarrow$ semantic triple on 48 inputs; $I\wedge V\ge0$ states all terminate in $Q$ & 40 box states & 0 violations\\ |
| A3: five failure modes classified (weak $I$: counterexample unreachable; buggy code: reproduced by a run; wrong variant: only the decrease VC fails) & 5 cases & as predicted 5/5\\ |
| A5: nested loops $s=nm$: all 9 VCs valid on the box and 9 runs end in $Q$; a wrong inner variant is caught by the decrease VC & box $3{\times}3{\times}4{\times}4{\times}10$ & as predicted\\ |
| Lean: \texttt{search\_correct} compiles; \texttt{\#print axioms} & --- & $\{\texttt{propext},\texttt{Quot.sound}\}$\\ |
| Lean: off-by-one rejected; \texttt{\#eval} 9 vs 10; \texttt{decide (Post \dots)} false/true & --- & as predicted\\ |
| R5: violating pairs, Python brute force vs closed form vs Lean \texttt{UInt8 \#eval}; safe midpoint & 32,896 pairs & 16384 = 16384 = 16384; safe 0\\ |
| R5: 32-bit: \texttt{(3000000000+3000000000)/2} in \texttt{UInt32}; \texttt{decide} of $\neg(lo\le mid)$ & --- & mid $=852516352<lo$\\ |
| R4: law vs brute force over all $2^{11}$ postconditions & 80 random pairs (71 refined) & 0 disagreements\\\bottomrule\end{tabular}\end{center} |
| (All quantities are integers or Booleans; ``max abs error'' is $0$ throughout.) Approximation named: the VC checks on a box (A2) are \emph{refutation-complete inside the box only}; they are evidence, not proof. The proofs are the derivations above and the Lean theorem. |
|
|
| \section{What breaks} |
| \begin{center}\small\begin{tabular}{@{}P{3.5cm}P{6.4cm}P{5.5cm}@{}}\toprule |
| Failure & Mechanism & Assumption violated\\\midrule |
| Overflow / wrap-around & VC holds over $\Z$, fails for $\mathrm{int}_w$ (R5). Mistral's Leanstral report \cite{leanstral} (company-reported, primary) describes a real overflow in the zigzag-decoding \texttt{sign} function of \texttt{datrs/varinteger}: \texttt{value + 1} overflows on \texttt{Std.U64.MAX} (secondary coverage: \cite{decoder}) & the model's arithmetic equals the machine's\\ |
| Partial vs total & $\hoare{\mathit{true}}{\texttt{while true do skip}}{\mathit{false}}$ is valid: a diverging loop satisfies every partial spec & termination is required; Lean's \texttt{termination\_by} enforces it, \texttt{partial def} is opaque\\ |
| Vacuous precondition & if $P$ is unsatisfiable every triple holds & $P$ is satisfiable (check by witness, 0302)\\ |
| Weak spec & a spec the wrong code also meets (0305) & $Q$ captures intent\\ |
| Annotation errors & too-weak/too-strong $I$ yields failed VCs on correct code (A3) & the failed VC is a question (0304)\\ |
| Model $\ne$ code & abstracting $a[i]$ to $P(i)$, ignoring aliasing, I/O, floats, concurrency & the abstraction is faithful; heap needs separation logic (not covered)\\ |
| Cheating the harness & DafnyBench counts success only if \texttt{requires}/\texttt{ensures} are preserved and no \texttt{assume false}/\texttt{\{:verify false\}} is used \cite{dafnybench} \S3.2 & the spec given is the spec proved\\\bottomrule\end{tabular}\end{center} |
|
|
| \nextnote{0304: when a proof fails, how to search for a counterexample (\texttt{decide}, property testing, model finding), why a proof is sound but a failed proof is not complete evidence, and how to turn a counterexample into a confirmed bug.} |
|
|
| \begin{small} |
| \begin{thebibliography}{99} |
| \bibitem{dafnybench} C.~Loughridge et al., \emph{DafnyBench}, arXiv:2406.08467, Fig.~2 (\texttt{LinearSearch} with \texttt{invariant}s), \S3.2 (the \texttt{fill\_hints} task: remove \texttt{assert}/\texttt{invariant}, success conditions 1--3). |
| \bibitem{verina} Z.~Ye et al., \emph{VERINA}, arXiv:2505.23135, \S3.1 (a specification is a pre-condition and a post-condition); \S4.1 (soundness/completeness of $\hat P,\hat Q$). |
| \bibitem{clever} A.~Thakur et al., \emph{CLEVER}, arXiv:2505.13938, Fig.~2 (the \texttt{$\exists$ result, implementation x = result $\wedge$ spec result} form; computable specs that leak the implementation). |
| \bibitem{fvapps} Q.~Dougherty, R.~Mehta, \emph{Proving the Coding Interview (FVAPPS)}, arXiv:2502.05714, \S III.E (discussion of \texttt{Id.run do} solutions). |
| \bibitem{leanstral} Mistral AI, \emph{Leanstral} technical report (\texttt{LeanstralReport.pdf}, repository \texttt{mistralai/LeanstralSafeVerify}) and the vendor post ``Leanstral 1.5: Proof Abundance for All'': 47 violated properties, 11 genuine bugs, 5 previously unreported on GitHub; the \texttt{datrs/varinteger} \texttt{sign} example (section numbers not recorded). Company-reported, not independently reproduced. |
| \bibitem{decoder} The Decoder (4 Jul 2026), coverage of Leanstral~1.5: 5 previously unknown bugs in 57 repositories incl.\ a varint zigzag-decode overflow. Secondary, paywall-truncated in our vault copy; used only as corroboration. |
| \bibitem{lean4lean} M.~Carneiro, \emph{Lean4Lean}, arXiv:2403.14064, \S4.1 (a soundness bug found by failing to prove a verification condition for \texttt{inferLambda}/\texttt{cheapBetaReduce}). |
| \bibitem{hoare69} C.~A.~R.~Hoare, ``An axiomatic basis for computer programming'', CACM 12(10), 1969; R.~W.~Floyd, ``Assigning meanings to programs'' (1967); E.~W.~Dijkstra, ``Guarded commands, nondeterminacy and formal derivation of programs'', CACM 18(8), 1975 ($\wpc$); R.-J.~Back, J.~von Wright, \emph{Refinement Calculus} (1998). \emph{Not on arXiv; not fetched; cited for the named calculi. Every rule used above is derived from the big-step semantics in \S3.} |
| \end{thebibliography} |
| \end{small} |
| \end{document} |
|
|
