Gaussian elimination over F2 for Simon recovery

Input: An $(n-1)\times n$ binary matrix $Y$ over the field ${\mathbb{F}}_2$, with $n\ge 1$. Let $d=n-1$.

Instructions:

1. Set the pivot-row index $k=0$ and an empty ordered list of pivot columns. For columns $j=0,\dots ,n-1$ in order, search the rows $i\ge k$ for the least $i$ with $Y_{ij}=1$. If none exists, continue to the next column.
2. If such $i$ exists, swap rows $i$ and $k$. For every other row $r\mathrm{\ne }k$ with entry $1$ in column $j$, replace row $r$ by its bitwise XOR with row $k$. Record $j$ as a pivot column and increase $k$ by one.
3. After the finite column loop, return FAIL if $k\mathrm{\ne }d$. Otherwise find the sole nonpivot column $q$, set the free variable $x_q=1$, and solve each pivot variable from its reduced row. Return the resulting vector $x\in {\mathbb{F}}_2^n$.

All searches, swaps, row XORs, and loops are finite. The $n=1$ input has zero rows and the algorithm returns the one-bit vector $1$. The operation is a deterministic row-reduction procedure; correctness and bit cost are proved in F2 row reduction returns the unique Simon mask.