VADCOP design

[leonardoalt]

Overview:

VADCOP is a mechanism where you add challenges (in the sense of "a challenge from the verifier to the prover") and turn lookups into regular polynomial equality constraints. This allows lookups for systems that do not support lookups. It also allows some bigger flexibility with regards to number of rows (you can have columns with different number of rows in the system), and it supports some optimizations (lookups can be combined, etc).

A challenge is always just a random field element, nothing more. One difficulty is that the challenges and the witness columns need to be ordered: In the interactive proof, the prover commits to a set of witness columns and sends those commitments to the verifier. The verifier answers with a random number (the challenge). Then the prover commits to another set of witness columns (whose values then can depend on the challenge).

Things we need to figure out:

Syntax:

Create syntax for creating challenges:

let x = challenge(n), where n is the "stage".

or

col <n> name; / col <n> name[k];

Create syntax for how witness columns depend on a certain challenge or are within a certain stage.

At best, the syntax should not require too big changes to the type system. If we have structs, we could even "just" use some structs that we mark "known" by the compiler.

Language for transforming lookups / links

We need language for specifying how lookups (or more abstractly "links") are transformed into stuff that makes use of challenges. This could just be a PIL function that takes a lookup as argument:

let transform_lookup = |left_sel, left_cols, right_sel, rigt_cols| ...;

This is not too far out - we already support it in the type system.

It would be even nicer if we could have structs for lookups and then use syntactic sugar for destructuring a lookup. This way, we could pass an array of all the lookups in the source:

let transform_lookup = |lookups| std::array::map(|lookup| match lookup {
  lsel { lcols } in rsel { rcols } => ...
  _ => panic("Not a lookup")
});

Another question is how we "call" these transforms once they are defined. They will probably be defined in some standard library, but I guess the idea is that we want the user to be able to choose between different ways to transform lookups.

Maybe it is better to do this at the machine level? Then we could have something like:

machine Main { ... }

transform_machine_to_vadcop(Main);

Witgen:

The witness generator needs to work in stages: It first needs to compute the first-stage witnesses, somehow receive the challenge from the verifier and then compute the next stage of witnesses.

Backend

Integrate this whole thing with polygon's vadcop data structure and halo2's challenges.

Our estark intergation already uses challenges internally and transforms the lookups, we can just reuse that.

[chriseth]

Here is some example code that shows how to transform lookups, how to handle the challenges in constraints and maybe even how to fix the problem with the degree:

enum constr {
    Lookup(Lookup),
    Identity(expr, expr),
}

struct Lookup {
    left: SelectedExpressions,
    right: SelectedExpressions,
}

struct SelectedExpressions {
    sel: expr,
    exprs: expr[],
}

// The arithmetic machine, a 'constr' function.
let arith = constr || {
    let latch = ...;
    let A;
    let B;
    let C;
    ...

    ArithMachine {
        // Query the machine. Returns a lookup.
        // TODO If we call this function twice, we get two lookups. Do we want to prevent that?
        query: |sel, (x, y, z)| Lookup {
            left: SelectedExpressions {
                sel: sel,
                exprs: [x, y, z],
            },
            right: SelectedExpressions {
                sel: latch,
                exprs: [A, B, C]
            },
        },
    }
};

// The main machine.
let main = constr || {
    // This instantiates an arith machine.
    let arith_machine = arith();
    let X;
    let Y;
    let Z;
    // This is still the higher-level code.
    instr add X, Y -> Z = |flag, X, Y, Z| arith_machine.query(flag, (X, Y, Z));
    // It gets desugared to
    // constr (|flag, X, Y, Z| arith_machine.query(flag, (X, Y, Z)))(instr_add, X, Y, Z);
    // which essentially adds the lookup to the list of constraints.
}

// "capture_constraints" is a new builtin function. TODO we still have to find a better name.
//
// It creates a new "constraint context", i.e. the list of constraints is empty.
// We could also say that it creates a new pil namespace (the polygon feature of namespaces),
// taking the degree as an argument.
//
// Then it calls its first argument, which should be a `->()` function, i.e. takes no arguments and returns nothing.
//
// It returns all the constraints generated during the evaluation of the function.
// transform_lookups then takes this list and transforms all lookups into regular polynomial constraints
// (see below).
//
// TODO: Maybe a call to `capture_constraints` also just increments the stage after its return?
// At least it knows which witness cols were defined during its evaluation.
//
// If the evaluation of a pil program does not result in the right type or in a call to `capture_constraints`,
// some default call is added that does not transform the lookups (and does not use challenges).
constr transform_lookups(capture_constraints(main, 2**20));

/// This transforms an array of constrainst such that all lookups
/// are combined into a single identity constraint.
/// This is a 'constr' function, so it returns the constraints only implicitly.
/// NB: This is actually code for permutations. For lookups we somehow need to add multiplicities.
let transform_lookups: constr[] -> = constr |c| {
    let alpha = challenge();
    let beta = challenge();
    let (constrs, left_acc, right_acc, _) = array::fold(c, ([], 1, 1), |(constr_acc, left_acc, right_acc, id), c| {
        match c {
            Lookup(l) => {
                let (left, right) = transform_lookup(alpha, beta, l, id);
                (constr_acc, left_acc * left, right_acc * right, id + 1),
            c => (constr_acc + [c], left_acc, right_acc, id),
        }
    });
    // Now we add the identity constraints again.
    constr constrs;
    // This is a new witness column, and it automatically is in the next stage, since we
    // called `capture_constraints`
    let gprod;
    let L1: col = |i| if i == 0 { 1 } else { 0 };
    // TODO: the "'" here is a "previous row" reference.
    // not sure if we can write this with "next row" only.
    constr gprod * right_acc = ('gprod * (1 - L1) + L1) * left_acc;
    constr L1' * (gprod - 1) = 0;
}

let transform_lookup = |alpha, beta, l, id| {
    std::check::assert_eq(l.left.exprs.len(), l.right.exprs.len());
    let left = compress_selected_exprs(id, (alpha, beta), l.left.sel, l.left.exprs);
    let right = compress_selected_exprs(id, (alpha, beta), l.right.sel, l.right.exprs);
    (left, right)
};

/// Combines one part of a lookup into a single expression
/// using two challenges.
/// The id is the unique id of the lookup.
/// NOTE: We need to ensure that the stage of the expressions is
/// less than the stage of the challenge.
let compress_selected_exprs: int, (challenge, challenge), expr, expr[] = |id, (alpha, beta), sel, exprs|
    sel * (compress_columns(alpha, exprs) + id + beta - 1) + 1;

/// Combines an array of expressions into a single
/// expression using a challenge.
/// NOTE: We need to ensure that the stage of the input
/// is less than the stage of the challenge.
let compress_columns: challenge, expr[] -> expr = |alpha, cols|
    // TODO polygon uses reversed order.
    std::array::fold(cols, 0, |acc, c| (acc + c) * alpha);

[chriseth]

As a summary of the above comment, we need the following features:

Destructuring of constr

constr needs to be an enum types that we can destructure.

Access to constraints of stages

We want the code to be stage-independent, this means there is no way to create a challenge at a specific stage or with a specific ID, there is only the built-in functtion std::prover::new_challenge() that returns a new challenge at the current stage.

There is a built-in function std::prover::next_stage: (->) -> constr[], that takes a constr-function. It evaluates the function and returns the set of constraints generated while evaluating the function. It also increases the current stage.

Add builtins:

std::prover::new_challenge // could have name suggestion, but nothing else
std::prover::next_stage
std::prover::new_witness_column // no stage, but maybe name suggestion

Remove the current builtins:

std::prover::challenge // it has access to the stage
std::prover::new_witness_in_stage

Of course since at the end we want to transform to actual pil again, there needs to be a way to have explicit stages both for challenges and for witness columns, but we could check that in that case, none of the other mechanisms are used.

[chriseth]

Some more ideas about how we could implement VADCOPs using a proof object / struct at the pil level:

https://hackmd.io/@4tYcUGjTRT6U93PllxQGww/rkL3UQyIA/edit