I've read the sources of ZKBoo where they transformed arithmetic operations of the SHA hash functions into a bunch of boolean ones. Where does this transformation arise from? How do you construct such transformation? How do you prove that these boolean operations are equivalent to arithmetic ones?
I've followed Circuit-based Evaluation of the Arithmetic Transform of Boolean Functions by René Krenz et al. but that seems to go the other way around: constructing arithmetic expression from a circuit.
Thanks in advance!