How Powdr translates PIL to Plonky3 STARK—1

in Powdr, the proving function of Plonky3 is in function prove_with_key, in stark.rs

you can see the inputs for prove_with_key function has “air”, this is what used to define constraints, powdr gives “&circuit” to it, and it is a powdrcircuit, probably powdrcircuit applies the trait of AIR

so at this point I think I need to understand how Plonly3 defines AIR, using this example to learn.

In this example, AIR is defined like this:

// Define your AIR constraints inputs via declaring a Struct with relevant inputs inside it.
pub struct FibonacciAir {
    pub num_steps: usize, // numbers of steps to run the fibonacci iterations
    pub final_value: u32, // precomputed final result after the numbers of steps.
}

// Define your Execution Trace Row size, 
impl<F: Field> BaseAir<F> for FibonacciAir {
    fn width(&self) -> usize {
        2 // Row width for fibonacci program is 2
    }
}

// Define your Constraints
impl<AB: AirBuilder> Air<AB> for FibonacciAir {
    fn eval(&self, builder: &mut AB) {
        let main = builder.main();
        let local = main.row_slice(0); // get the current row
        let next = main.row_slice(1); // get the next row

        // Enforce starting values
        builder.when_first_row().assert_eq(local[0], AB::Expr::zero());
        builder.when_first_row().assert_eq(local[1], AB::Expr::one());

        // Enforce state transition constraints
        builder.when_transition().assert_eq(next[0], local[1]);
        builder.when_transition().assert_eq(next[1], local[0] + local[1]);

        // Constrain the final value
        let final_value = AB::Expr::from_canonical_u32(self.final_value);
        builder.when_last_row().assert_eq(local[1], final_value);
    }
}

I think the most important function should be eval, should be from a trait

BASE AIR and AIR are traits, defined in plonky3/air

And powdr implement AIR for PowdrCircuit

for stwo, the equivalent traits to define the constraints, shoud be FrameworkComponent, FrameworkEval

The conversation to plonky3

in circuit_builder.rs, there is this function to_plonky3_expr()

the constraints derived from analyzed PIL are stored in ConstraintSystem struct, in circuit_builder.rs file.

see, identities are algebraicExpression

but apart from constraint translation, a trace needs to be generated, in powdr for plonky3, this is done in a function in PowdrCircuit

in stwo, the trace is stored in

ColumnVec<CircleEvaluation<SimdBackend, BaseField, BitReversedOrder>>

for example, the trace of wide fibonacci and plonk in stwo

wide fibonacci:

and plonk: