following the first post
got two tasks:
- generate trace from pil to stwo
- implement FrameworkEval trait, which is used by stwo to define constraint, to PowdrCircuit
let’s talk about generate trace first.
in stwo, the trace is in this format as showed in last post
ColumnVec<CircleEvaluation<SimdBackend, BaseField, BitReversedOrder>>how powdr in plonky3 does it?
the “into_p3_field()” transfer the witness to plonky3 field.
for fibonacci example, the input witness looks like this
Map { iter: Chain { a: Some(Iter([(
"Fibonacci::ISLAST", [GoldilocksField(0), GoldilocksField(0), GoldilocksField(0), GoldilocksField(1)])])), b: Some(Iter([("Fibonacci::y", [GoldilocksField(0), GoldilocksField(0), GoldilocksField(0), GoldilocksField(1)])])) } } the output RowMajorMatrix it becomes:
the plonky3 rowmajormatrix values are [0, 0, 0, 0, 0, 0, 1, 1]it re-organized based on rows. concatenate rows one by one. The trace is re-organized like this probably is because how the plonky3 do the constraints evaluation. namely, how in eval function in the air related traits evaluation the trace. so I will check this part
in PowdrCircuit there is a constraintSystem and it has an identities element which is made from AlgebraicExpression
The to_plonky3_expr seems working on translating algebraicExpression to plonky3 expression.
print the input for to_plonky3_expr , e, I can see the format of algebraicExpression from pil look like:
check how the same thing is done in halo2, it also use this algebraicExpression
This identity in halo2 comes from analyzed directly
so now I want to check more about the format that algebraicExpresssion extracts polynomials from pil.
So I check hello_world_opt.pil file and the extracted algebraicExpression
you see, the polynomial about block_enforcer_last_step in left side pil to right side algebraicExpression
before analyzing the structure, let see the definition of algebraicExpression in powdr
quite good structure to net algbraicExpression
come back to the example, for the polynomial below
(1 - main::_block_enforcer_last_step) * (1 - main::instr_return) * (main::_operation_id' - main::_operation_id) = 0;and into algebraicExpression, it is:
exactly matches the polynomial.