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.vars_to_value.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)