powdr-labs / powdr

A modular stack for zkVMs, with a focus on productivity, security and performance.
Apache License 2.0
329 stars 65 forks source link

PIL Analyzer does not catch removed challenge used in hint #1371

Open georgwiese opened 3 weeks ago

georgwiese commented 3 weeks ago

To reproduce:

use std::prover::Query;
use std::prover::challenge;
use std::prover::eval;

machine Main with degree: 8 {

    // Need at least one phase-0 witness column
    col witness a(i) query Query::Hint(1);
    a * (a - 1) = 0;

    // beta is not used by any constraint and hence removed by the optimizer
    let beta = challenge(0, 2);
    // The hint still accesses beta (but always returns 0)
    col witness stage(1) b(i) query Query::Hint(eval(beta) * 0);

    // Need to have a challenge if we have a phase-1 witness column
    let alpha = challenge(0, 1);
    b * (b - alpha) = 0;
}
cargo run pil bug.asm -o output -f --field bn254 --prove-with halo2-mock

This fails during witgen, but should fail already when the PIL is being analyzed:

thread 'main' panicked at /Users/georg/coding/powdr/executor/src/witgen/query_processor.rs:156:17:
Challenge 2 not found! Available challenges: [1]
leonardoalt commented 1 week ago

@georgwiese why should it fail? Aren't the stages consistent?

georgwiese commented 1 week ago

What do you mean by consistent?

In this example, one challenge is never used in a constraint, so the optimizer is right to remove it. So the hints shouldn't depend on it and arguably it should be an error it appears there (even though it ends up being multiplied by zero).