On my way to review, about lookup -1

let is_first: col = |i| if i == 0 { 1 } else { 0 };

the above line, defines fix column, fix columns are columns known during circuit setup, independent of the what the witness will be. “i” represent the row number. check here for more details.

let alpha1: expr = challenge(0, 1);

challenge built in function, Constructs a challenge object, essentially asking the verifier for a random number.The first argument is the proof stage and the second is the identifier of the challenge.

some more explanation of challenger from Tibo “So basically you can think of witgen and proving as the same process:witgen phase 0 -> prove phase 0 -> witgen phase 1 -> prove phase 1

at the end of phase 0 proving, we draw randomness from the verifier

and we use this randomness to run witness generation for phase 1

the API we use is this thing called a witgen callback: it takes the entire witness so far (for example, phase 0) as well as values for the challenges, and returns the entire witness after the next stage was run,so basically when you request a challenge in PIL, you are calling the prover directly”

let unpack_lookup_constraint: Constr -> (expr, expr[], expr, expr[]) = |lookup_constraint| match lookup_constraint {
    Constr::Lookup((lhs_selector, rhs_selector), values) => (
        unwrap_or_else(lhs_selector, || 1),
        map(values, |(lhs, _)| lhs),
        unwrap_or_else(rhs_selector, || 1),
        map(values, |(_, rhs)| rhs)
    ),
    _ => panic("Expected lookup constraint")
};

remember in stwo code, when transfer polynomials to stwo expression, there is a match function to tell the polynomial belongs to which group:

these types are defined by Constr, it is a built in type, Constr

and this is actually a function

let unpack_lookup_constraint: Constr -> (expr, expr[], expr, expr[]) = |lookup_constraint| ...

explain:

The only way to declare a function in pil is by assigning a lambda function to a symbol.

the name of the function here is unpack_lookup_constraint

If you want to specify the types of parameters or return values explicitly, you have to do it on the symbol, you cannot do it on the parameters:

the input and return type is

input: Constr
output: (expr, expr[], expr, expr[])

|lookup_constraint| match lookup_constraint {
    ...
};

the above is a match function, the syntax is:

match term {matching_term_1 => output1, matching_term_2 => output2 …}

it checks if term matching any of the matching terms in side {}

|lookup_constraint| match lookup_constraint {
    Constr::Lookup((lhs_selector, rhs_selector), values) => ...,
    _ => panic("Expected lookup constraint")
};

the matching term in this case is either Constr::Lookup((lhs_selector, rhs_selector), values) or panic.

in Constr, the lookup type is defined as

 /// A lookup constraint with selectors.
    Lookup((Option<expr>, Option<expr>), (expr, expr)[]),

in this case, it matches:

Lookup((lhs_selector, rhs_selector), values)

lhs_selector –> Option<expr>

rhs_selector –> Option<expr>

the values —> (expr,expr)[]

now look at the code

let unpack_lookup_constraint: Constr -> (expr, expr[], expr, expr[]) = |lookup_constraint| match lookup_constraint {
    Constr::Lookup((lhs_selector, rhs_selector), values) => (
        unwrap_or_else(lhs_selector, || 1),
        map(values, |(lhs, _)| lhs),
        unwrap_or_else(rhs_selector, || 1),
        map(values, |(_, rhs)| rhs)
    ),
    _ => panic("Expected lookup constraint")
};

Continue in next post

On my way to review, about lookup –1

Leave a Reply Cancel reply