Where's the code for the reduction from TinyRAM to CircuitSAT?

[analytic-bias]

As mentioned in the email, I'm trying to work on the formal verification (in Coq, presumably) of your SNARKs paper. My first step would be to verify the correctness of the reduction from TinyRAM to CircuitSAT. Can you point me to the code of it?