In this post, let's see how the expressions in gate polynomials are encoded into Halo2VerifyingArtifact, and used inside EVM verifier to evaluate gate polynomials.
First, let's look into the following type, EvaluatorDynamic.
EvaluatorDynamicstruct
#[derive(Debug)]
pub(crate) struct EvaluatorDynamic<'a, F: PrimeField> {
cs: &'a ConstraintSystem<F>,
meta: &'a ConstraintSystemMeta,
data: &'a Data,
static_mem_ptr: RefCell<usize>,
encoded_var_cache: RefCell<HashMap<U256, U256>>,
const_cache: RefCell<HashMap<ruint::Uint<256, 4>, Ptr>>,
}EvaluatorDynamic encodes the computation data and tracks free static memory area that EVM verifier will store the results of evaluating these encoded expressions. The order in which expressions are encoded is crucial; EvaluatorDynamic should never skip encoding inner expression. EvaluatorDynamic traverses through expression tree in post-order for encoding.
gate_computations initialization
GateDataEncodedstruct
// Holds the encoded data stored in the VK artifact
// needed to perform the gate computations of
// the quotient evaluation portion of the reusable verifier.
#[derive(Clone, PartialEq, Eq, Default)]
pub struct GateDataEncoded {
pub(crate) length: usize,
pub(crate) packed_expression_words: Vec<U256>,
}GateDataEncoded struct is created in two steps, encoding expressions and packing expressions into words.
There are two types of expressions, expressions for operations with a single operand (query expression, challenge expression, and negated expression), and expressions for operations with two operands (sum expression and product expression).
Query expression is encoded with the following function:
fn encode_single_operand(&self, op: u8, ptr: U256) -> U256 {
U256::from(op) | (ptr << 8)
}op indicates the column type this expression queries for, for Advice/Fixed column op == 0u8 and for Instance column op == 1u8. Depending on op, the verifier will reference the pointer into either calldata(Advice/Fixed) or memory(Instance).
Expressions with two operands are encoded with the following function:
fn encode_operation(&self, op: u8, lhs_ptr: U256, rhs_ptr: U256) -> U256 {
U256::from(op) | (lhs_ptr << 8) | (rhs_ptr << 24)
}op indicates the operation kind of this expression. For sum expression op == 2u8 and for product expression op == 3u8.
Question: It seems that the memory addresses are always in the range of
0x00 ~ 0xFFFF. It seems the range is enough, but if the verifying artifact gets huge, doesn't it overflow?
To avoid allocating the memory to store the evaluation result of the same expression multiple times, EvaluatorDynamic utilizes encoded_var_cache hash map. encoded_var_cache hash map stores the memory address at which EVM verifier will store the evaluation result.
// Return the encoded word and the static memory pointer
fn init_encoded_var(&self, value: U256, var: OperandMem) -> (Vec<U256>, U256) {
match var {
OperandMem::Calldata | OperandMem::StaticMemory => {
if self.encoded_var_cache.borrow().contains_key(&value) {
(vec![], self.encoded_var_cache.borrow()[&value])
} else {
let var = self.next_encoded_var();
self.encoded_var_cache.borrow_mut().insert(value, var);
(vec![value], var)
}
}
OperandMem::Constant => (
vec![],
U256::from(self.const_cache.borrow().get(&value).map_or_else(
|| {
println!("Key not found: {}", value);
0 // Default value, you can change this if needed
},
|entry| entry.value().as_usize(),
)),
),
OperandMem::Instance | OperandMem::Challenge => (vec![], value),
}
}init_encoded_var function takes expression encoding as input and outputs the encoded expression and the memory address that the evaluation result will be stored in. Note that init_encoded_var lookups encoded_var_cache and if the same expression encoding was already evaluated and allocated in the memory, it returns the memory address of it. If not, it allocates new memory slot in which the evaluation result will be stored, and then return the encoded expression and memory address.
Instance polynomial evaluations and challenges will be computed inside verifier, so the expression encoding of them is already the memory address that they will be stored in the future.
fn evaluate_encode(&self, expression: &Expression<F>) -> (Vec<U256>, U256) {
evaluate(
expression,
&|constant| self.init_encoded_var(constant, OperandMem::Constant),
&|query| {
self.init_encoded_var(
self.eval_encoded(Fixed, query.column_index(), query.rotation().0),
OperandMem::Calldata,
)
},
&|query| {
self.init_encoded_var(
self.eval_encoded(Advice::default(), query.column_index(), query.rotation().0),
OperandMem::Calldata,
)
},
&|_| {
self.init_encoded_var(
// instance eval ptr located 17 words after the theta mptr
U256::from((self.data.theta_mptr + 17).value().as_usize()),
OperandMem::Instance,
)
},
&|challenge| {
self.init_encoded_var(
U256::from(
self.data.challenges[challenge.index()]
.ptr()
.value()
.as_usize(),
),
OperandMem::Challenge,
)
},
&|(mut acc, var)| { // negated expression
let (lines, var) = self.init_encoded_var(
self.encode_single_operand(1_u8, var),
OperandMem::StaticMemory,
);
acc.extend(lines);
(acc, var)
},
&|(mut lhs_acc, lhs_var), (rhs_acc, rhs_var)| {
let (lines, var) = self.init_encoded_var(
self.encode_operation(2_u8, lhs_var, rhs_var),
OperandMem::StaticMemory,
);
lhs_acc.extend(rhs_acc);
lhs_acc.extend(lines);
(lhs_acc, var)
},
&|(mut lhs_acc, lhs_var), (rhs_acc, rhs_var)| {
let (lines, var) = self.init_encoded_var(
self.encode_operation(3_u8, lhs_var, rhs_var),
OperandMem::StaticMemory,
);
lhs_acc.extend(rhs_acc);
lhs_acc.extend(lines);
(lhs_acc, var)
},
&|(mut acc, var), scalar| {
// fetch the scalar pointer from the const cache
let scalar_ptr = self.const_cache.borrow()[&scalar];
let (lines, var) = self.init_encoded_var(
self.encode_operation(3_u8, var, U256::from(scalar_ptr.value().as_usize())),
OperandMem::StaticMemory,
);
acc.extend(lines);
(acc, var)
},
)
}evaluate_encode function shows how the encoding works for more complicated expressions. For example, let's say we want to encode the expression -(advice_column(x)). Then, advice column query expression is encoded first and the memory address that advice_column(x) will be stored in is returned. Then, the negated expression is encoded using that memory address and then returned. When EVM verifier decodes this encoded expression, it will first load the memory address that advice_column(x) value is stored in, and then negate that value, and then store -(advice_column(x)) value to the next free static memory address.
After encoding, expression encodings should be packed into multiple EVM words to make them compact.
Now, let's see how EVM verifier unpacks the encoding and evaluate the encoded expressions.
function expression_evals_packed(fsmp, code_ptr, expressions_word) -> ret0, ret1, ret2 {
// Load in the least significant byte of the `expressions_word` word to get the total number of words we will need to load in.
let num_words_shift_up_one := add(mul(0x20, and(expressions_word, BYTE_FLAG_BITMASK)), 0x20)
ret0 := add(code_ptr, mul(0x20, and(expressions_word, BYTE_FLAG_BITMASK)))
// start of the expression encodings
expressions_word := shr(8, expressions_word)
let acc
for { let i := 0x20 } lt(i, num_words_shift_up_one) { i := add(i, 0x20) } {
for { } expressions_word { } {
let mstore_ptr := add(fsmp, acc)
// Load in the least significant byte of the `expression` word to get the operation type
// Then determine which operation to peform and then store the result in the next available memory slot.
switch and(expressions_word, BYTE_FLAG_BITMASK)
// 0x00 => Advice/Fixed expression
case 0x00 {
expressions_word := shr(8, expressions_word)
// Load the calldata ptr from the expression, which come from the 2nd and 3rd least significant bytes.
mstore(mstore_ptr, calldataload(and(expressions_word, PTR_BITMASK)))
// Move to the next expression
expressions_word := shr(16, expressions_word)
}
// 0x01 => Negated expression
case 0x01 {
expressions_word := shr(8, expressions_word)
// Load the memory ptr from the expression, which come from the 2nd and 3rd least significant bytes
mstore(mstore_ptr, sub(R, mload(and(expressions_word, PTR_BITMASK))))
// Move to the next expression
expressions_word := shr(16, expressions_word)
}
// 0x02 => Sum expression
case 0x02 {
expressions_word := shr(8, expressions_word)
// Load the lhs operand memory ptr from the expression, which comes from the 2nd and 3rd least significant bytes
// Load the rhs operand memory ptr from the expression, which comes from the 4th and 5th least significant bytes
mstore(mstore_ptr, addmod(mload(and(expressions_word, PTR_BITMASK)), mload(and(shr(16, expressions_word), PTR_BITMASK)),R))
// Move to the next expression
expressions_word := shr(32, expressions_word)
}
// 0x03 => Product/scalar expression
case 0x03 {
expressions_word := shr(8, expressions_word)
// Load the lhs operand memory ptr from the expression, which comes from the 2nd and 3rd least significant bytes
// Load the rhs operand memory ptr from the expression, which comes from the 4th and 5th least significant bytes
mstore(mstore_ptr, mulmod(mload(and(expressions_word, PTR_BITMASK)),mload(and(shr(16, expressions_word), PTR_BITMASK)),R))
// Move to the next expression
expressions_word := shr(32, expressions_word)
}
// 0x04 => (For lookup expressions) Start accumulator evaluations for the lookup (table or input)
// Will always occur at the end of the last word of the lookup expression.
case 0x04 {
ret0, ret1, ret2 := lookup_input_accum(expressions_word, fsmp, i, code_ptr)
leave
}
acc := add(acc, 0x20)
}
code_ptr := add(code_ptr, 0x20)
expressions_word := mload(code_ptr)
}
ret1 := expressions_word
ret2 := sub(acc, 0x20)
}Parameters:
fsmp: starting address of free static memory pointer (0x00for gate computation)code_ptr: starting address of packed words for the corresponding encoded expressionexpressions_word: starting word for the corresponding encoded expression
Return:
ret0: starting address of packed words for the next encoded expressionret1: starting word for the next expressionret2: the offset fromfsmpto the address where the evaluation result is stored
