Powdr Autopre-compile - Shuang's Crypto Notes

From lib.rs, there is test, checking prove simple:

check what this prove simple means

there are some prove and compile, prove recursion basic function in this file.

Table of Contents

Compile:

In the compile function, there are two functions til now I think it is important: instruction_to_airs and customize

in this instruction to air, it does:

get air

translate to powdr algebraic expression

collect all the air

customize is where the instructions get analysed, the block with high repeated frequency is transferred to pre-compile circuit.

let’s check some functions in this basic block:

the exe.program looks like this

I added this code to export_pil to get only the powdr pre-compile constraints:

 if !name.starts_with("PowdrAir") {
                println!("Skipping {} (not a PowdrAir)", name);
                return None;
            }

run command:

 cargo test -r --package powdr-openvm --lib -- tests::guest_prove_simple  --exact --show-output

from the output, you can see the bus_id, bus interactions of each machine

as mentioned by Georg, there are 6 bus interactions, (even though I see bus id 7 in other machine, powdrAir only have 0,1,2,3,6)

it would be good to know how these bus interactions are proved in the backend.

I firstly check the pil code in debug.pil, in powdrAir, you can see the bus interactions are listed as:

each bus interaction has its name:

EXECUTION_BRIDGE,MEMORY,PC_LOOKUP, VARIABLE_RANGE_CHECKER, BITWISE_LOOKUP

let’s analyse a bit of one bus_interaction

a bitwise_lookup

std::protocols::bus::bus_interaction(BITWISE_LOOKUP, [a__0_8, a__0_8, 0, 1], is_valid * 1);

it includes some of these witness, claimed in the beginning of PowdrAir machine

the witnesses are also include in some of the constraints

question: how is the backend handle the bus_interaction? let’s see

digging into the prove function in guest_prove_simple test

in the prove function, generate_app_proof should be the key function

in generate_app_proof—-> app_prover.generate_app_proofs

app_prover.generate_app_proofs —–> ContinuationVmProver::prove(&self.app_prover, input)

ContinuationVmProver::prove(&self.app_prover, input) —–> .in_scope(|| Ok(vm.engine.prove(&self.pk.vm_pk, proof_input)))

probably here, generate_proof_input is building AIR, or witness? prove is the actual proving process.

generate_proof_input:

it seems building air for each chip

in this chip-wise generate_proof_input, you can see it start build

add_air_proof_input, maybe it is not building air, air is built before, here is for witness.

Prove:

in the prove function, I fund the code related to the challenge:

in this file, I found logup related code, I need to dig more here