\chapter{Numbers and Automation: Making the Machine Do the Boring Parts}
\label{ch:automation}

\section{The 90/10 rule of verification}

Here is a trade secret: most of a real verification effort is not clever.
Opening the correctness proof of Ed25519 field multiplication, you will find
that the overwhelming majority of proof obligations are statements like

\[
a < 2^{51} \;\wedge\; b < 2^{51} \;\Longrightarrow\; a + b < 2^{52},
\qquad\qquad
(a + b) \cdot c = a\cdot c + b\cdot c,
\]

--- bookkeeping a patient undergraduate could verify by hand in a minute
each. There are \emph{thousands} of them. The craft of modern verification is
to hand exactly this 90\% to decision procedures --- tactics that implement a
complete algorithm for a well-defined logical fragment --- and save the human
for the 10\% that needs insight. This chapter is your tour of the arsenal.

\section{\texttt{omega}: linear arithmetic, decided}

The tactic you will use more than any other in this book's domain is
\lean{omega}. It completely decides \emph{linear arithmetic} over integers
and naturals: any goal built from variables, constants, $+$, $-$,
multiplication \emph{by constants}, $=$, $<$, $\le$, $\lnot$, $\wedge$,
$\vee$, including the hypotheses in context.

\begin{lstlisting}[language=Lean]
example (a b : Nat) (h1 : a < 2^51) (h2 : b < 2^51) :
    a + b < 2^52 := by omega

example (a b : Nat) (h : a ≤ b) : a + (b - a) = b := by omega
  -- note: truncated Nat subtraction handled CORRECTLY -- omega knows
\end{lstlisting}

That second example deserves a salute: \lean{omega} understands \lean{Nat}
truncation natively, defusing the Chapter~\ref{ch:lean} pitfall by algorithm
rather than by vigilance. When the goal is false, \lean{omega} \emph{fails} ---
it is a decision procedure, so failure on a linear goal means the goal (with
the hypotheses in view) is simply not true. That property turns \lean{omega}
into a \emph{statement-debugging} tool: if it refuses your ``obviously true''
bound, go find the counterexample; there is one.

\begin{worked}{when omega says no --- hunting the boundary by hand}
Train the counterexample reflex on a real-shaped bound. Claim: ``if
$a, b < 2^{51}$ then $a + b < 2^{52} - 2$.'' It \emph{sounds} safely true
--- each term is below half of $2^{52}$, surely the sum clears the bar
with room? \lean{omega} refuses. Instead of doubting the tool, hunt at the
\emph{boundary}, because linear claims fail at corners of the allowed
region: take both variables at their maximum, $a = b = 2^{51} - 1$. Then
\[
a + b \;=\; 2^{52} - 2
\;\not<\; 2^{52} - 2 .
\]
The claim fails by exactly one at exactly one corner --- the true theorem
is $a + b \le 2^{52} - 2$, or strictly $a + b < 2^{52} - 1$. Now recall
Chapter~\ref{ch:why}: the carry bugs that motivated this book are
precisely off-by-a-hair failures at corners of the input region that
sampling never visits. The refusal of a decision procedure is the same
boundary being found for you, before the code ships instead of after.
Standing rule: \textbf{when \lean{omega} refuses a linear goal, the
statement is wrong; evaluate the goal at the extreme values of every
hypothesis, and one of those corners is your counterexample.}
\end{worked}

\begin{worked}{the bound-then-omega pattern at real field scale}
Here is the exact arithmetic that stands between the Ed25519
multiplication routine and a machine-word overflow --- the central safety
computation of the whole field layer, fully pen-and-paper. The bounds
discipline lets limbs grow to $a_i, b_j < 2^{54}$
(Chapter~\ref{ch:rust}). Multiplication forms \emph{column sums} of limb
products (Chapter~\ref{ch:denotation}); the widest column is
\[
c_4 \;=\; a_0 b_4 + a_1 b_3 + a_2 b_2 + a_3 b_1 + a_4 b_0
\qquad\text{(five products).}
\]
The products land in $128$-bit words. Does $c_4$ fit? Work the exponents:
\[
a_i b_j \;<\; 2^{54} \cdot 2^{54} \;=\; 2^{108},
\qquad
c_4 \;<\; 5 \cdot 2^{108} \;<\; 2^{3} \cdot 2^{108} \;=\; 2^{111}
\;<\; 2^{128}. \;\checkmark
\]
Margin: $128 - 111 = 17$ bits to spare --- room for the carry-in each
column also absorbs. Every number in this computation is real: the $54$
comes from the invariant, the $5$ from the limb count, the $128$ from the
hardware. Change any one --- say a hypothetical radix-$58$ variant:
$2 \cdot 58 = 116$, $5 \cdot 2^{116} < 2^{119}$, still fine; radix-$62$:
$5 \cdot 2^{124} < 2^{127}$, one bit from the cliff --- and you can
re-run the audit in your head. \emph{This} is what the automation
divides between itself: \lean{a\_i * b\_j < 2\textasciicircum{}108} is the nonlinear atom you
must name (one monotonicity lemma), and everything after it ---
$5 \cdot 2^{108} < 2^{128}$ with the atom opaque --- is linear, which is
to say, \lean{omega} food. The pattern in the pitfall below is this
computation, industrialized.
\end{worked}

\begin{pitfall}
\lean{omega} does not touch multiplication of two \emph{variables}
($a \cdot b$ is not linear), division in general, or bit-shifts by variables.
For a goal mixing $a \cdot b$ with bounds, you often first name the product
--- \lean{have hab : a * b ≤ 2\textasciicircum{}102 := ...} using a multiplication
monotonicity lemma --- and then let \lean{omega} finish with \lean{hab} as an
opaque atom. This two-step, \emph{bound the nonlinear part, then release the
linear solver}, is the single most-used proof pattern in verified field
arithmetic. You will write it dozens of times, and by Chapter~\ref{ch:field}
it will feel like breathing.
\end{pitfall}

\section{\texttt{decide}: when truth is a computation}

Some propositions can be checked by running an algorithm to completion:
``$97$ is prime,'' ``these two sorted lists are equal,'' ``$x^3 = x$ for all
$x$ in $\Zmod{6}$'' (six cases --- check them all). For any such
\emph{decidable} proposition, the \lean{decide} tactic runs the decision
algorithm inside Lean's kernel and turns the answer into a proof:

\begin{lstlisting}[language=Lean]
example : Nat.Prime 97 := by decide
example : ∀ x : ZMod 6, x^3 = x^3 := by decide   -- finite: try all six
\end{lstlisting}

The magic and the limitation are the same fact: the \emph{kernel itself}
re-executes the computation. That makes \lean{decide} unimpeachable --- and
completely hopeless for our 77-digit prime $2^{255}-19$, where trial division
would outlast the universe. There is a variant, \lean{native_decide}, that
compiles the check to native code first --- fast enough! --- but it makes the
compiler part of your trusted base, an IOU we will scrutinize hard in
Chapters~\ref{ch:prime} and~\ref{ch:honesty}. For now, the rule of the house:
\textbf{\lean{decide} yes, \lean{native_decide} never in a final certificate.}

\section{\texttt{ring} and \texttt{norm\_num}: algebra on tap}

The five-line commutativity shuffle from Chapter~\ref{ch:tactics}? Here is
the grown-up version:

\begin{lstlisting}[language=Lean]
example (a b c : Nat) : a + b + c = c + b + a := by ring

example (a b : ZMod p) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

example : (2:Int)^255 - 19 > 2^254 := by norm_num
\end{lstlisting}

\lean{ring} proves any identity that holds in every commutative ring ---
polynomial rearrangements, binomial expansions, distributivity avalanches ---
by normalizing both sides to a canonical polynomial form and comparing.
\lean{norm_num} evaluates concrete numeric facts, comfortable with numbers of
any size. Between \lean{omega}, \lean{ring}, and \lean{norm_num} you now hold
the three keys that open most arithmetic doors:

\begin{center}
\begin{tikzpicture}[
  key/.style={draw=ink2,thick,rounded corners=3pt,fill=white,align=center,
              minimum width=3.55cm,minimum height=1.5cm},
]
  \node[key,fill=accentsoft] (o) at (0,0)
    {\textbf{\code{omega}}\\[1pt]\small linear $+,-,<,\le$\\\small bounds \& carries};
  \node[key,fill=provensoft] (r) at (4.1,0)
    {\textbf{\code{ring}}\\[1pt]\small polynomial identities\\\small in any comm.\ ring};
  \node[key,fill=warnsoft] (n) at (8.2,0)
    {\textbf{\code{norm\_num}}\\[1pt]\small concrete numerals\\\small any size};
  \node[font=\small\color{ink2},align=center] at (4.1,-1.55)
    {the three keys of verified arithmetic --- learn what each fragment
     \emph{excludes}\\ and you will always know which door you are standing in front of};
\end{tikzpicture}
\end{center}

\section{\texttt{simp}: the rewriting engine, and how to hold it}

\lean{simp} rewrites the goal to exhaustion using a curated database of
thousands of ``simplification'' lemmas ($x + 0 \rightsquigarrow x$,
\lean{List.length (a :: l)} $\rightsquigarrow$ \lean{l.length + 1}, ...). It
is the most powerful tactic in Lean and the easiest to misuse. Used well, it
clears brush so the real argument stands out. Used lazily ---
\lean{simp [*]} with every hypothesis thrown in, in a context of sixty
accumulated facts --- it becomes a search over an enormous rewrite space:
slow, fragile under library updates, and occasionally a memory monster.

This is not hypothetical. During the development this book accompanies, a
single over-broad \lean{simp}-style discharge in a fat context consumed
twelve gigabytes of RAM and took down the machine. The postmortem produced
house rules worth adopting from day one:

\begin{itemize}[leftmargin=1.4em]
\item Prefer \lean{simp only [lemma1, lemma2]} --- an explicit lemma list ---
  in anything you intend to keep.
\item Let \lean{simp?} tell you the list: run it once interactively, then
  paste the \lean{simp only [...]} it suggests into the file.
\item Keep contexts lean (pun intended): a proof with sixty hypotheses in
  scope wants to be five \lean{have}-steps with twelve each.
\end{itemize}

\begin{bigidea}
Automation is a \emph{contract}, not a slot machine. Each tactic decides a
known fragment: \lean{omega} linear arithmetic, \lean{ring} ring identities,
\lean{decide} finite computation, \lean{simp only} a rewrite system you
chose. The professional habit is to know \emph{which} contract you are
invoking --- then failure is information (``this goal is not linear''; ``this
identity needs the modulus''), never mystery.
\end{bigidea}

\begin{tryit}
Open \code{exercises/Ch05.lean}: ten arithmetic goals, each solvable by
exactly one of \lean{omega} / \lean{ring} / \lean{norm_num} / \lean{decide}.
Your task is not just to close them but to close each with the \emph{right}
tool --- the file rejects overkill by design. Goal number ten is the
Chapter~\ref{ch:tactics} cliffhanger:
\lean{a < 2\textasciicircum{}51 → a * 19 < 2\textasciicircum{}56}. (It is not linear --- $19$ is a constant, so
it is! Think, then fire.)
\end{tryit}

\section*{Exercises}

\exercise{For each, name the tactic and predict success before running:
(a) \lean{(a+b)*(a-b) = a*a - b*b} over \lean{Int};
(b) \lean{a < 100 → b < 100 → a*b < 10000} over \lean{Nat};
(c) \lean{Nat.Prime 65537};
(d) \lean{2\textasciicircum{}51 + 2\textasciicircum{}51 = 2\textasciicircum{}52}.}

\exercise{Goal (b) above is nonlinear, yet \lean{omega} alone fails while the
two-step pattern (bound the product with
\lean{Nat.mul_lt_mul} machinery, then \lean{omega}) succeeds. Carry it out.
Time yourself; the pattern should take under five minutes by the second
attempt.}

\exercise{Find a true statement about \lean{Nat} that \emph{no} tactic in
this chapter proves in one shot, and sketch in prose how you would decompose
it. (Anything genuinely inductive works --- automation here decides
arithmetic fragments, not all of mathematics.)}

\exercise{(Paper) Re-run the worked column-sum audit for the
\emph{scalar} arithmetic of the companion projects, which uses radix-52
limbs bounded by $2^{52}$ multiplied into $128$-bit words with
\emph{nine}-term columns at the widest (schoolbook $5\times 5$, column
$k=4$ has five terms, but the Montgomery pass adds four more products).
Does $9 \cdot 2^{104}$ fit in $2^{128}$? With how many bits of margin?}

\section*{Solutions and pathways}
\solutionsintro

\solhead{5.1}
\pathway For each goal, name the \emph{fragment} it lives in before naming
a tactic: linear with constants? polynomial identity? concrete numerals?
finite check? Then the table from this chapter is a lookup, not a guess.
\answer
(a) $(a+b)(a-b) = a\,a - b\,b$ over \lean{Int}: polynomial identity in a
commutative ring $\to$ \lean{ring}. Succeeds. (Over \lean{Nat} it would be
trickier --- truncated subtraction breaks ring reasoning; part of why the
exercise says \lean{Int}.)
(b) $a<100 \to b<100 \to ab < 10000$: \emph{nonlinear} (product of two
variables) $\to$ no single tool from the table; needs the two-step
pattern (5.2).
(c) \lean{Nat.Prime 65537}: decidable, and small enough $\to$
\lean{decide} works (with a noticeable pause); \lean{norm_num} is faster
--- Chapter~\ref{ch:prime} explains the difference as certificate versus
grind.
(d) $2^{51} + 2^{51} = 2^{52}$: concrete numerals $\to$ \lean{norm_num}
(or \lean{decide}; but build the habit of matching tool to fragment, not
firing the biggest gun).

\solhead{5.2}
\pathway The product $ab$ is one opaque quantity as far as linear
reasoning is concerned. So: (i) bound the atom with a monotonicity lemma
--- both factors grow, so the product grows; (ii) hand the bounded atom to
\lean{omega}. Finding the lemma name is part of the exercise:
\lean{exact?} on the goal \lean{a * b < 100 * 100}, or search Mathlib for
``mul\_lt\_mul''.
\answer
\begin{lstlisting}[language=Lean]
example (a b : Nat) (ha : a < 100) (hb : b < 100) : a * b < 10000 := by
  have hab : a * b < 100 * 100 := Nat.mul_lt_mul'' ha hb
  omega
\end{lstlisting}
Two lines, and the division of labor is visible: the \lean{have} names the
one nonlinear fact (with the lemma doing the monotonicity), then
\lean{omega} finishes since \lean{100 * 100} is a numeral and \lean{a * b}
is now an opaque atom below it. Under five minutes by the second attempt
is a realistic bar --- this exact two-line shape appears \emph{dozens} of
times in the field-layer proofs, with $2^{54}$ in place of $100$.

\solhead{5.3}
\pathway Look for statements whose truth genuinely needs induction ---
i.e.\ not expressible in a decided fragment. Anything universally
quantified over \emph{all} \lean{n} about a recursively defined function
qualifies.
\answer (Model answer.) $\forall n,\ \mathtt{fib}(n) < 2^n$ (with
\lean{fib} from Chapter~\ref{ch:lean}). Not linear (contains \lean{fib}
and $2^n$), not a ring identity, not concrete, not finite --- every tool
in this chapter shrugs. Decomposition sketch: induction on $n$ with
\emph{two} base cases ($n = 0, 1$) and a step using
$\mathtt{fib}(n{+}2) = \mathtt{fib}(n{+}1) + \mathtt{fib}(n) <
2^{n+1} + 2^n < 2^{n+2}$ --- where the \emph{final} inequality, with the
induction hypotheses as opaque atoms, IS an \lean{omega} goal. That is the
grown-up division of labor: induction supplies the skeleton, decision
procedures clear each rib.

\solhead{5.4}
\pathway Same three lines as the worked example; only the constants move.
\answer Products: $2^{52} \cdot 2^{52} = 2^{104}$. Nine terms:
$9 \cdot 2^{104} < 2^4 \cdot 2^{104} = 2^{108} < 2^{128}$ --- fits, with
$128 - 108 = 20$ bits of margin ($23$ if you count $9 < 2^{3.17}$ more
tightly). The scalar layer breathes easier than the field layer's $17$
bits, which matches how the two codebases feel to verify. When you meet
the scalar Montgomery proofs in the companion repos, this margin
computation is the first \lean{have} of every multiplication lemma.

\begin{checkpoint}
You should now be able to: match a goal to its decision procedure by the
shape of its operators; execute the bound-then-omega pattern for nonlinear
bounds; explain why \lean{decide} is trustworthy and where it hits its
computational wall; and state the \lean{simp} discipline --- and the story of
why this book is unusually sincere about it.
\end{checkpoint}