[Cryptography] What is the current state of useful code for zk-snarks?

[cherry]

To be actually useful, a zk-snark system needs to be a compiler, that 
compiles a program written in what Starkware calls R1CS, and other 
people are calling script, and generates two programs, a prover and a 
verifier.

The prover operates on two blobs, the public blob and private blob, and 
produces a boolean result, true or false, pass or fail, and a proof that 
it did so.

The proof is approximately constant size, regardless of how much 
computation is required and regardless of how large the private blob 
was, but takes a very long time.

The verifier operates on the public blob and the proof, takes a short 
and approximately constant time to do so, regardless of how big the 
computation was, and regardless of how big the private data was and 
determines, with 2^(126) likelihood of error, what result the prover got.

But at present I get the impression that neither script nor R1CS have 
any real existence, though I have seen a script language that operates 
on a stack, and, though it has no variables, can dupe any item on the 
stack to the top of the stack.  It seems to have only been ever used to 
generate one prover and one verifier, because actually creating the 
prover and verifier still required some coding by hand.  Also lacked 
certain control structures.

At present, people seem to be writing the prover and the verifier by 
hand, a very difficult operation with a very high likelihood of bugs. 
The prover and the verifier do very simple tasks like proving the 
encoded inputs to a transaction are greater than or equal to the encoded 
outputs and that no numeric underflow or overflow occurred.

Another problem is that we would really like the public data to be the 
root hash of a merkle tree, and no one seems to have a script language 
that contains a useful hash function  Stackware is built out of hash 
functions, but last time I looked, you could not call a hash function 
from R1CS.

We need a script language that can not merely add and subtract, but can 
also do hashes and elliptic point operations.  zk-stark systems are 
built out of hashes and elliptic point operations, but it seems to be 
uphill trying to generate proofs that prove something about the results 
of hashes and elliptic point operations, making very difficult to 
produce a proof that a pile of proofs in the pre-image of a merkle tree 
have been verified.  I suspect that a prover might take a very very long 
time to produce such a proof.