Hide concrete output expression from the calling circuit #322

When we have a circuit calling a sub-circuit, Clean tries to be compositional but not quite. Because we see goals like

add example

where a very big implementation detail is shown as the output of a sub-circuit.

This issue keeps track of hiding the implementation details of sub-circuit by adding a new variable in the context, together with a hypothesis saying that the variable satisfies the specification of the sub-circuit.

Approaches

• circuit_proof_start can introduce fresh variables for outputs and forget their definitions.
• ConstraintsHold can be modified so that a fresh existentially quantified variable is used instead of the output.

Current experiences

People notice big implementation details sometimes:

• https://github.com/Verified-zkEVM/clean/pull/317/files#r2639747744