Weird CirC behavior when working with the sample_challenge function.

[sashafrolov]

I have been experimenting with the sample_challenge function, specifically building off of examples/ZoKrates/pf/chall/simple.zok.

If I modify the program to return the sampled challenge like this:

from "EMBED" import sample_challenge

def main(private field x, private field y) -> field:
    field a = sample_challenge([x, y])
    assert(a * x == a * y)
    return a

or like this:

from "EMBED" import sample_challenge

def main(private field x, private field y) -> field:
    field a = sample_challenge([x, y])
    assert(a * x == a * y)
    field result = a
    return result

I get the same error:

sasha@Alexanders-MacBook-Air-6 circ % RUST_BACKTRACE=info ./target/release/examples/circ examples/ZoKrates/pf/chall/simple.zok r1cs --proof-impl mirage --action setup
Running frontend
Running IR optimizations
Running backend
Running r1cs optimizations 

thread 'main' panicked at src/target/r1cs/mod.rs:1076:13:
assertion failed: !vars.contains_key(c)
stack backtrace:
   0: __rustc::rust_begin_unwind
             at /rustc/17067e9ac6d7ecb70e50f92c1944e545188d2359/library/std/src/panicking.rs:697:5
   1: core::panicking::panic_fmt
             at /rustc/17067e9ac6d7ecb70e50f92c1944e545188d2359/library/core/src/panicking.rs:75:14
   2: core::panicking::panic
             at /rustc/17067e9ac6d7ecb70e50f92c1944e545188d2359/library/core/src/panicking.rs:145:5
   3: circ::target::r1cs::R1cs::verifier_data
             at ./src/target/r1cs/mod.rs:1076:13
   4: circ::target::r1cs::R1cs::finalize
             at ./src/target/r1cs/mod.rs:1111:18
   5: circ::main
             at ./examples/circ.rs:345:48
   6: core::ops::function::FnOnce::call_once
             at /Users/sasha/.rustup/toolchains/stable-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
sasha@Alexanders-MacBook-Air-6 circ % 

However, if I do this:

from "EMBED" import sample_challenge

def main(private field x, private field y) -> field:
    field a = sample_challenge([x, y])
    assert(a * x == a * y)
    field result = x + a - x
    return result

Compilation succeeds.

There is still a weird error once I get past compilation though. When I try to prove the circuit using the existing inputs, I get this error:

sasha@Alexanders-MacBook-Air-6 circ % ./target/release/examples/zk --inputs examples/ZoKrates/pf/chall/simple.zok.pin --proof-impl mirage --action prove                 
Proving

thread 'main' panicked at src/ir/term/eval.rs:72:32:
Missing var: zx_chall_0 in {"x": #f7m52435875175126190479447740508185965837690552500527637822603658699938581184513, "y": #f7m52435875175126190479447740508185965837690552500527637822603658699938581184513}
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
sasha@Alexanders-MacBook-Air-6 circ % 

From reading the code, it looks like CirC is looking for the value of the challenge inside the prover input rather than from a challenge. It looks like these issues both revolve around public outputs and challenge variables not playing well together in the CirC IR. I was writing code like this to try to see fi the random challenges were actually random.