Paper 2026/1505

Conditional-Affine Redundant Clauses for SHA-256 Differential SAT

Abstract

Standard Tseitin encodings of the SHA-256 nonlinear functions Ch and Maj can hide conditioned differential projections from Boolean Constraint Propagation (BCP). We materialize them as short, semantically redundant CNF clauses. A cofactor theorem characterizes all controlled differential linear forms; its implemented unit-vector specialization returns exactly all minimum-control projections, yielding four Ch and twelve Maj clauses per bit. The clauses preserve models, introduce no variables, and strictly strengthen BCP on an explicit gate fragment. We claim neither propagation completeness nor a general affine compiler. We evaluate mechanism separately from performance and distinguish the production bundle from the proposed layer. Frozen studies show a fixed-formula bundle benefit, but the matched clause isolation fails its effect gate and an unrestricted control is inconclusive. We therefore show neither a solver-independent speedup nor a new cryptanalytic attack. The restricted weight-15 C15 census passes the CaDiCaL rule but not the Kissat rule. In the stratified C16 extension, the frozen decisions are too censored for CaDiCaL and too censored for Kissat; these solver-stratified labels are not pooled. A pinned three-solver replay validates larger-bundle execution but cannot attribute performance to the clauses. A variable-preserving probe exposes all 32 tested implications only after augmentation.