[Circuit monad] Proper soundness using env function

[mitschabaude]

• remove the possibility of passing in witness value inputs when running a circuit, and instead use the more general and sound notion that the prover can use any env: Nat -> F to determine assignment of values to variables
• modify SubCircuit structure to a form which I think will stand the test of time
• prove a larger part of the underlying justification for replacing subcircuits with their specs
  • reduce the theorem that allows us to use a FormalCircuit as a SubCircuit to the equivalence of flattened and nested constraints
• remove lots of (now) obsolete code

[mitschabaude]

this is the trick I was missing before this PR

[gio54321]

Actually, just using

dsimp [Adversarial.constraints_hold] at h_holds

simplifies things nicely and works as intended

[mitschabaude]

another example of the same trick

[gio54321]

Same thing, just doing

dsimp [Adversarial.constraints_hold] at h_holds

works 🙂

[mitschabaude]

wait what, am I crazy

[mitschabaude]

thanks @gio54321 :D I pushed an update

[gio54321]

lgtm, nice!

I wonder if with the new env we can remove the Provable.eval_env env b_var = b assumption. We could quantify only over all possible beta.var and then introduce in the proofs the values that are the evaluation of those vars, since the env maps every var to a field element. Something like this (not really deeply tested)

  soundness:
    -- for all environments that determine witness generation
    ∀ env: ℕ → F,
    -- for all inputs that satisfy the assumptions
    ∀ b_var : β.var,
    let b := Provable.eval_env env b_var
    assumptions b →
    -- if the constraints hold
    Adversarial.constraints_hold env (main b_var) →
    -- the spec holds on the input and output
    let a := Provable.eval_env env (output (main b_var))
    spec b a

[mitschabaude]

I wonder if with the new env we can remove the Provable.eval_env env b_var = b assumption

I thought it's a good idea and tried it. So far it made the introduction of variables a bit more complicated though, because I still need the same equality assumption and need to introduce it manually (see screenshot). Maybe you can come up with a better way to handle this later