When using the CGen tool to convert the SHA-256 algorithm into Conjunctive Normal Form (CNF), the input and output bits are represented by DMAC literals. However, I am specifically interested in identifying the DMAC literals that represent the internal processes involved in SHA-256, such as the message schedule (W[i]), T1, T2, and other intermediate states.
Could you provide a detailed list of the DMAC literals that represent these internal processes (like the message schedule, intermediate working variables, and round-specific operations) in the CNF conversion performed by the CGen tool? Please describe the sequence of literals involved and how they correlate to the internal transformations of the SHA-256 hashing process.
