1\section{SHA-256: Mathematical Structure and Reduced-Round Analysis}2\label{sec:sha}34\subsection{Construction}56SHA-256 \citep{nist2015fips180} is a Merkle--Damg\aa rd iteration \citep{merkle1989one,damgard1989design} of a7compression function $f:\{0,1\}^{256}\times\{0,1\}^{512}\to\{0,1\}^{256}$. The message is padded with a 1-bit, zeros and8the 64-bit length to a multiple of 512 bits; the chaining value starts at the fixed IV $H_0$ (fractional parts of9$\sqrt{2},\dots,\sqrt{19}$); and $H_i = f(H_{i-1}, M_i)$ with $f(H,M)=H\boxplus\mathrm{Steps}_{64}(H,M)$, the10``feed-forward'' Davies--Meyer construction that makes $f$ non-invertible. Inside, 32-bit words are combined with11modular addition $\boxplus$, XOR, AND, rotations $\rotr$ and shifts $\shr$ through12\begin{equation}13\begin{aligned}14 \SigZ(x) &= \rotr^{2}(x)\oplus\rotr^{13}(x)\oplus\rotr^{22}(x), & \SigO(x) &= \rotr^{6}(x)\oplus\rotr^{11}(x)\oplus\rotr^{25}(x),\\15 \sigz(x) &= \rotr^{7}(x)\oplus\rotr^{18}(x)\oplus\shr^{3}(x), & \sigo(x) &= \rotr^{17}(x)\oplus\rotr^{19}(x)\oplus\shr^{10}(x),\\16 \Ch(x,y,z) &= (x\wedge y)\oplus(\neg x\wedge z), & \Maj(x,y,z) &= (x\wedge y)\oplus(x\wedge z)\oplus(y\wedge z).17\end{aligned}18\label{eq:shafuncs}19\end{equation}20The message schedule expands $M=W_0\|\cdots\|W_{15}$ by $W_t=\sigo(W_{t-2})\boxplus W_{t-7}\boxplus\sigz(W_{t-15})\boxplus W_{t-16}$21for $16\le t<64$, and step $t$ updates the state $(a,b,c,d,e,f,g,h)$ as in Figure~\ref{fig:sha-arch}:22$T_1 = h\boxplus\SigO(e)\boxplus\Ch(e,f,g)\boxplus K_t\boxplus W_t$, $T_2=\SigZ(a)\boxplus\Maj(a,b,c)$, then23$(a,b,c,d,e,f,g,h)\leftarrow(T_1\boxplus T_2,\,a,\,b,\,c,\,d\boxplus T_1,\,e,\,f,\,g)$.2425\begin{figure}[htbp]26 \centering27 \resizebox{\textwidth}{!}{\input{figures/fig_sha256_architecture}}28 \caption{One step of the SHA-256 compression function (exact data flow of FIPS 180-4; illustrative layout).29 Rotations and shifts are free in hardware and in CNF (they are variable renamings); the nonlinearity comes from30 $\Ch$, $\Maj$ and the carries of the modular additions.}31 \label{fig:sha-arch}32\end{figure}3334\subsection{Elementary structure}3536Three facts, all machine-checked in Section~\ref{sec:formal}, organise the analysis. (i)~$\SigZ,\SigO,\sigz,\sigo$ are37$\F_2$-linear bijections of $\{0,1\}^{32}$---including $\sigz$ and $\sigo$, whose logical shift makes each of their two38summands singular but not their sum (we had conjectured the opposite; the machine-checked refutation is39hypothesis~\Hname{H22}). (ii)~For fixed $(K_t,W_t)$ the step function is a bijection of the 256-bit state, with explicit inverse40$h = T_1\ominus\SigO(e)\ominus\Ch(e,f,g)\ominus K_t\ominus W_t$ where $T_1=a_{t+1}\ominus T_2$; and the41schedule recurrence can be solved for $W_{t-16}$. Hence, without the feed-forward, the 64-step map is invertible42for any chosen message: pseudo-preimages of the compression function (choose the IV) are free, and ``free-start''43collisions are a different, much easier problem than collisions of the hash (hypothesis~\Hname{H20}). (iii)~The44step-$t$ nonlinearity is weak: $\Ch$ and $\Maj$ are bitwise (no inter-bit mixing), so all diffusion across bit45positions comes from the $\Sigma$ functions and from carries.4647\subsection{Generic bounds and the meaning of reduced-step results}4849For an ideal 256-bit hash a preimage costs $\approx2^{256}$ evaluations, a collision $\approx 2^{128}$ by the birthday50paradox, and these are the targets any attack must beat. Reduced-step analysis studies $\mathrm{Steps}_s$ for $s<64$ to51quantify the security margin; a result on $s$ steps says nothing about $64$ steps unless it extends. The published52state of the art (Table~\ref{tab:sha-lit}, Section~\ref{sec:lit}) is: practical collisions for 28 steps53\citep{dobraunig2015analysis} and 31 steps \citep{li2024first}, with a theoretical 37-step collision announced in 2026 \citep{zhang2026collision}; semi-free-start collisions for 38--39 steps54\citep{mendel2013improving,li2024new}; preimages for 43 steps \citep{aoki2009preimages} and 45 steps of the hash55(52 of the compression function) with bicliques \citep{khovratovich2012bicliques}, all far above $2^{128}$ in cost.56Differential attacks use \emph{local collisions}: the 9-step pattern of \citet{chabaud1998differential} adapted to57SHA-256 by \citet{gilbert2003security} injects a difference $\delta$ into $W_t$ and cancels its propagation with58corrections in $W_{t+1},\dots,W_{t+8}$; in the XOR-linearised model the cancellation is exact, and the real step59function follows the pattern with a probability that depends on the carries, which dedicated tools raise by imposing60conditions on message and state bits \citep{nikolic2008collisions,mendel2011finding}.6162\subsection{What we measure}6364Axis~C runs four families of experiments on the reference implementation (verified against \code{hashlib} for all65message lengths): diffusion of single-bit differences through the steps (\Hname{H15}); statistical detectability of66input--output correlations as a function of the step count (\Hname{H16}); SAT (CaDiCaL, Kissat) and SMT (Z3 bit-vector)67preimage and collision searches on step-reduced compression functions with Tseitin encodings68(\Hname{H17}, \Hname{H18}) \citep{mironov2006applications,nejati2017adaptive,alamgir2024sha256}; and the 9-step local69collision in the linearised and the real model (\Hname{H19}). The questions~C1--C5 are answered in70Section~\ref{sec:results}; we state in advance that nothing in these experiments bears on the security of the full7164-step hash, and that our generic SAT encodings are expected to reach far fewer steps than the dedicated72characteristic-search tools of the literature.73