Correctness of the reversible modular multiplier

The DAG's XOR formula is $(u\vee v)\wedge \mathrm{\neg }(u\wedge v)$, which is $u+v$ modulo $2$ for each of the four input pairs. In its adder, $U_i+V_i+d_i=s_i+2d_{i+1}$: if both input bits are $1$ the carry is $1$, if exactly one is $1$ the carry is $d_i$, and if both are $0$ the carry is $0$; the displayed sum bit has the corresponding parity. Multiplying by $2^i$ and summing proves $U+V+d_0=S+2^w{d}_w$. Subtraction therefore represents $U+(2^w-1-V)+1=U-V+2^w$; its carry is $1$ exactly when $U\ge V$, and its low bits are $U-V$ modulo $2^w$. The selector's disjoint branches give $U$ for $h=1$ and $V$ for $h=0$.

After the first $i$ product rows, the accumulator is $z{\sum }_{j<i}{a}_j{2}^j$. This holds initially and is preserved by step 1.1; no overflow occurs because every partial sum is at most $az<2^{2n}$. Thus the final product bits represent $az$ even for invalid input encodings. In the remainder loop, the invariant is that $R$ is the remainder modulo $N$ of the already scanned product prefix and $0\le R<N$. Appending bit $P_{\mathrm{\ell }}$ gives $V=2R+P_{\mathrm{\ell }}<2N$. Subtraction and selection from step 1.1 give $V-N$ if $V\ge N$ and $V$ otherwise, so the next value lies in $[0,N)$ and is the new prefix remainder. It fits $n$ bits, making the discarded high bit zero, even when $N=2^n$. Induction proves the final $R=az<mrow><mi\; mathvariant="normal">m</mi><mi\; mathvariant="normal">o</mi><mi\; mathvariant="normal">d</mi></mrow>N$. The final no-borrow comparison gives $v=1$ exactly when $z<N$, and selection by $c\wedge v$ therefore computes precisely $f_a(c,z)$. The same argument applies to $a^{-1}$.

Fix $c,z$. If $c=0$ or $z\ge N$, the defining function and its inverse-function counterpart both return $z$. If $c=1$ and $z<N$, the first function returns $z^{\mathrm{\prime }}=az<mrow><mi\; mathvariant="normal">m</mi><mi\; mathvariant="normal">o</mi><mi\; mathvariant="normal">d</mi></mrow>N<N$ and the inverse function returns $a^{-1}{z}^{\mathrm{\prime }}<mrow><mi\; mathvariant="normal">m</mi><mi\; mathvariant="normal">o</mi><mi\; mathvariant="normal">d</mi></mrow>N=z$, by [F4]. Thus in every case $f_{a^{-1}}(c,f_a(c,z))=z$.

By [F2] and [F3], the first computation adds $f_a(c,z)$ into a clean target and restores all value-computation work. A bitwise swap made from CNOTs acts as $(u,v)\mapsto (u,u\oplus v)\mapsto (v,u\oplus v)\mapsto (v,u)$, so after the three CNOTs per bit the data register contains $f_a(c,z)$ and the target contains the old $z$.

Apply the clean XOR computation for $f_{a^{-1}}$ to the new data and the target holding old $z$. Step 3.1 says its output is exactly that old $z$, so XOR changes the target to $z\oplus z=0$ and restores its computation work by [F2]. Hence all temporary registers are clean and the data/control action is the claimed one.

On valid residue encodings, multiplication by $a$ is a bijection of the residue register because $a^{-1}$ is its inverse; on invalid encodings and at control $0$ the map is the identity. It is therefore a permutation of the full finite computational basis. A basis permutation is unitary, and [F2] supplies the same action on arbitrary superpositions with clean work. This proves the statement.