Circuit monad

[mitschabaude]

prototype of a circuit monad "DSL"

to be merged with several issues unresolved, including:

• right now concrete witness values have to be inputs to the circuit definition. this is wrong because, for example, the circuit can pass the same input value to two different witness calls, and that makes the prover less powerful than it would be in reality, because they have to use the same value for two different witnesses
• there are issues & a hack when going from the output of a subcircuit back to the calling circuit
• there is no guarantee that a circuit doesn't create a variable with some arbitrary index (not connected to one of the input witnesses) and so, again, and uses it in an expression. this again makes the prover not powerful

in the final framework the goal is that you really shouldn't have to carefully look at a circuit to see that it's sound. so there should be no options at all to the circuit developer to make the prover less powerful