anoma / vamp-ir

Vamp-IR is a proof-system-agnostic language for writing arithmetic circuits
https://anoma.github.io/VampIR-Book/
Apache License 2.0
154 stars 44 forks source link

Feature request: handle a large number of local definitions gracefully #94

Open lukaszcz opened 1 year ago

lukaszcz commented 1 year ago

Compiling a file with above ~1000 local definitions results in stack overflow. These kind of files easily result from relatively simple Juvix programs after recursion unrolling (up to ~140 iterations).

test026.pir

AHartNtkn commented 1 year ago

It looks like this overflows during parsing. If this doesn't happen for modules, that suggests that suggests that definitions are parsing let binding in a recursive way that modules aren't.

AHartNtkn commented 1 year ago

Increasing the stack size to 16 MB, which can be done using the following main function for example

fn main() {
    let builder = thread::Builder::new().stack_size(16 * 1024 * 1024);
    let handler = builder.spawn(move || {
        let cli = Cli::parse();
        match &cli.backend {
            Backend::Plonk(plonk_commands) => plonk(plonk_commands),
            Backend::Halo2(halo2_commands) => halo2(halo2_commands),
        }
    }).unwrap();
    handler.join().unwrap();
}

fixes the stack overflow. I don't know if this solution is desirable in general, but fixing it otherwise would likely require either changing the syntax of the language to make parsing this sort of file less recursive, or switching to a completely different parser that doesn't use recursive parsing at all/as much.

AHartNtkn commented 1 year ago

I don't know why I didn't test this before, but the stack overflow is also avoided if one uses a release build rather than a dev build. That is,

cargo build --release
./target/release/vamp-ir halo2 compile -s tests/test026.pir -o circuit.halo2

works fine. I wonder how many other inefficiencies are caused by this.