CellVar

A CellVar type is a type that represents an internal variable. Importantly, it is named after the fact that it relates to a specific cell, or even multiple cells if they will have the same value (using some wiring), in the execution trace.

A CellVar looks like this:

#![allow(unused)]
fn main() {
pub struct CellVar {
    index: usize,
    span: Span,
}
}

It is tracked using a usize, which is just a counter that the compiler increments every time a new CellVar is created.

A CellVar is created via the new_internal_var function which does two things: increments the variable counter, and stores some information on how to compute it (which will be useful during witness generation)

#![allow(unused)]
fn main() {
pub fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar {
    // create new var
    let var = CellVar::new(self.next_variable, span);
    self.next_variable += 1;

    // store it in the compiler
    self.witness_vars.insert(var, val);

    var
}
}

a Value tells us how to compute the CellVar during witness generation:

#![allow(unused)]
fn main() {
pub enum Value {
    /// Either it's a hint and can be computed from the outside.
    Hint(Box<dyn Fn(&Compiler, &mut WitnessEnv) -> Result<Field>>),

    /// Or it's a constant (for example, I wrote `2` in the code).
    Constant(Field),

    /// Or it's a linear combination of internal circuit variables (+ a constant).
    LinearCombination(Vec<(Field, CellVar)>, Field),

    /// A public or private input to the function
    /// There's an index associated to a variable name, as the variable could be composed of several field elements.
    External(String, usize),

    /// A public output.
    /// This is tracked separately as public inputs as it needs to be computed later.
    PublicOutput(Option<CellVar>),
}
}

Note: a CellVar is potentially not directly added to the rows of the execution trace. For example, a private input is converted directly to a (number of) CellVar(s), but only added to the rows when it appears in a constraint for the first time.

As the final step of the compilation, we double check that all CellVars have appeared in the rows of the execution trace at some point. If they haven’t, it can mean two things:

  • A private or public input was never used in the circuit. In this case we return an error to the user.
  • There is a bug in the compiler. In this case we panic.

TODO: explain the LinearCombination. I think we only need an Add((Field, Var), (Field, Var), Field)