Simon promise decision by sampled rank

Input: an integer $n\ge 1$ and oracle access to a promised function $f:V_n\to V_n$ from Simon injectivity decision promise with XOR-oracle access. Set $m=n+2$. For each of $m$ independent runs, initialize two ordered $n$-qubit registers $X,Y$ to $\mathrm{\mid }{0}^n⟩\mathrm{\mid }{0}^n⟩$, apply $H^{\otimes n}$ to $X$, and query the coherent XOR oracle $U_f$ once on $X,Y$. Apply the computational-basis instrument on $Y$ from Computational-basis instruments and conditional states on two registers, record and discard its classical outcome, apply $H^{\otimes n}$ again to $X$, and measure $X$ in the computational basis using the same instrument. Record the resulting $y_j\in V_n$.

Form the $m\times n$ binary matrix with rows $y_1,\dots ,y_m$. Set the next pivot row to $r=1$ and scan columns $j=1,\dots ,n$ from left to right. In column $j$, search rows $r,\dots ,m$ for the first row with a $1$ in that column. If there is no such row, leave the column without a pivot and continue to the next column. Otherwise swap that row with row $r$, XOR row $r$ into every other row with a $1$ in column $j$, and increase $r$ by one. Accept (declare injective) exactly when the number of pivots is $n$.

The operation counts and correctness of this procedure are established in Simon rank test correctness and linear query cost. A query is charged separately from an implementation of $f$ by Circuit-family and computation cost model. It makes no gate-time separation claim.