Identifying the DMAC Literals Representing Internal Processes (Message Schedule, T1, T2, etc.) in SHA-256 CNF Conversion

[pchandra876]

SHA-256 processes a 512-bit input message and generates a 256-bit output hash, involving various internal operations such as the message schedule (W[i]), working variables (A-H), and round transformations like T1, T2, and others. When converting SHA-256 into Conjunctive Normal Form (CNF), the internal processes of the algorithm need to be accurately represented by literals.

I am interested in identifying the DMAC literals that correspond to these internal processes, including the message schedule (W[i]), intermediate states (like T1, T2), and working variables. How do these DMAC literals interact with the input and output bits, and how are they mapped in the CNF conversion? What role do these internal literals play in representing the transformations within the SHA-256 algorithm?