I recently came across a discussion discussing conversion of SHA256 into a SAT instance by modifying the lisp implementation of SHA256 from Ironclad - sha-256 as a boolean function
There is some discussion on this and the modified version was shared, but the link died a long time ago.
The commenter states
It was actually pretty easy -- I took Ironclad SHA-256 implementation and tweaked it a bit to produce formulas instead of numbers
I am a novice at lisp, but found this fascinating. I am unable to figure out how this might have been done.
I can see how to do it by building large string which collects the operations and then later parsing the string into a boolean expression and simplifying, but that doesn't sound easy.
Can someone advise how the SHA256 code could have been modified to collect the formula instead of the result? An implementation with comments on the modifications for this would be amazing.
I really would like to learn to do this myself for other problems as I get better at lisp.
To produce a formula instead of a result, you calculate the expression which, if evaluated, produces the the result. You write a function whose arguments are terms rather than numbers.
As a trivial example, if the function to add together two numbers is given 2 and 3, it returns (+ 2 3) rather than 5. Furthermore, since no evaluation is taking place, the arguments are not necessarily numbers, but themselves formulas. The function can be asked to add together x and (* 2 y), in which case it returns (+ x (* 2 y)).
Because in Lisp we have code that is made of data, it's easy to just use that same representation; and if we use the same operators with the same semantics as Lisp, we can then implant the resulting code into a lambda and compile it.
By carefully introducing this kind of term calculating system into a digest function, we can coax it into producing a large, nested formula which calculates the same thing.
Now suppose we have this, which is similar to what appears in the comments below:
(defun foo (x y) `(* ,x (- 100 ,y)))
we'd like to dynamically obtain a compiled function of z where x is the cube of z and y is the square.
(compile nil `(lambda (z) ,(foo '(* z z z) '(* z z))))
We can funcall the resulting object with a numeric argument to calculate the value.