A Hoare Proof of Grover Search

Chapter 6 §6.6, printed pages 127–130 (PDF pages 37–40), including Figures 6.6–6.7 and equations 6.35–6.38, were checked visually. We distinguish general success probability from the exact-success special case used to illustrate the textbook derivation.

Registers, specification and angle

There are $N=2^n$ candidates and $1\leq L\leq N/2$ solutions. Let $|\beta\rangle$ and $|\alpha\rangle$ be uniform superpositions of solutions and nonsolutions. Define $\sin(\theta/2)=\sqrt{L/N}$ . The prepared search state is

|u\rangle=\cos(\theta/2)|\alpha\rangle+\sin(\theta/2)|\beta\rangle.

One Grover iteration rotates by $\theta$ in this plane. After $k$ iterations,

p_{\mathrm{succ}}=\sin^2((2k+1)\theta/2).

Choosing the nearest integer to $\pi/(2\theta)-1/2$ gives $p_{\mathrm{succ}}\geq1-L/N$ . Printed page 127 displays $\cos(\theta/2)=\sqrt{(N-L)/2}$ , which can exceed 1. We use denominator $N$ , derived from normalization, rather than silently reproducing this apparent printing error.

The success effect is $P_{\mathrm{sol}}=\sum_{x\text{ solution}}|x\rangle\langle x|$ , extended by identities on auxiliary registers. The goal is $\{p_{\mathrm{succ}}I\}\,\mathrm{Grover}\,\{P_{\mathrm{sol}}\}_t$ , not certain success for arbitrary parameters.

Program and loop body

Initialize the search register, auxiliary qubit and integer counter $r$ to zero, then prepare $|u\rangle\otimes|-\rangle\otimes|0\rangle_r$ . The oracle acts as $|x,b\rangle\mapsto|x,b\oplus f(x)\rangle$ ; the auxiliary minus state converts this into phase marking.

The loop measurement has $M_1=\sum_{l<k}|l\rangle\langle l|$ and $M_0=\sum_{l\geq k}|l\rangle\langle l|$ . Body $D$ applies the oracle, diffusion $H^{\otimes n}(2|0\rangle\langle0|-I)H^{\otimes n}$ and $r:=r+1$ . On the integer space, increment is a bilateral shift unitary. Finally measure the search register in the computational basis.

Invariant and body proof

Write $|u_l\rangle=G^l|u\rangle$ , where $G$ is the Grover iteration. Define

P'=|u_k\rangle\langle u_k|\otimes|-\rangle\langle-|\otimes|k\rangle\langle k|, \quad Q=\sum_{l<k}|u_l\rangle\langle u_l|\otimes|-\rangle\langle-|\otimes|l\rangle\langle l|.

Orthogonal counter blocks make $Q$ a bounded effect. With $R=M_0^\dagger P'M_0+M_1^\dagger QM_1$ , rotation and increment give $D^\dagger RD=Q$ . The unitary and sequential rules yield $\{Q\}D\{R\}_t$ . The initialized state lies in the eigenvalue-one subspace of $R$ .

Termination and a general ranking function

On initialized executions the counter starts at zero and exits after exactly $k$ iterations. Applying (R.LT) on its entire state domain requires more than this reachable-state observation.

A threshold ranking avoids taking a maximum over an infinite counter support. Let $T=\llbracket D\rrbracket\circ\mathcal E_1$ and $A=M_1^\dagger QM_1$ . For every $\epsilon>0$ , define

t_\epsilon(\rho)=\min\{j\in\mathbb N:\ \mathrm{tr}(A T^m(\rho))<\epsilon\text{ for all }m\geq j\}.

Finite trace implies that the negative-integer tail has vanishing mass. Each iteration shifts that tail rightward, so continuing mass tends to zero and the set is nonempty. Removing the first step cannot increase the rank; when current assertion mass reaches the threshold, the rank strictly decreases. Together with the total-correctness premise for the body, (R.LT) gives $\{R\}W\{P'\}_t$ . This establishes almost-sure termination, not a uniform finite bound for arbitrary inputs.

Success probability and final measurement

The final measurement preserves the diagonal success effect: $\sum_xM_x^\dagger P_{\mathrm{sol}}M_x=P_{\mathrm{sol}}$ . Initialization erases the original input, and the loop produces a fixed final state of success weight $p_{\mathrm{succ}}$ . Trace semantics and wp duality therefore give $\mathrm{wp}_{\mathrm{Grover}}(P_{\mathrm{sol}})=p_{\mathrm{succ}}I$ , proving the specification.

For its illustrative qTD proof, the textbook additionally assumes $L=1$ and that $k=\pi/(2\theta)-1/2$ is an integer. Then the final search state is the unique solution and $P'\preceq P_{\mathrm{sol}}$ ; the consequence rule completes the probability-one proof. That extra integer assumption must not be generalized into an unconditional exact-success theorem.

Source and scope

Chapter 6 DOI, §6.6. This entry uses the formal Hoare rules. The threshold ranking replaces boundary-sensitive counter-support expressions and separates the textbook special case from the general probability specification. The model assumes ideal gates and a correct oracle; noise, approximate gates and faulty oracle implementations are outside this proof.