O zkEVM é uma espécie de aplicação complicada de Prova de Conhecimento Zero, vale a pena ler e aprender seu código fonte repetidamente.
https://github.com/appliedzkp/zkevm-circuits.git
A última versão de commit (refere-se ao processo de tornar permanente um conjunto de alterações, ou seja, de efetivar as alterações) do código-fonte usado neste artigo é mostrada abaixo:
commit 1ec38f207f150733a90081d3825b4de9c3a0a724 (HEAD -> main)
Author: z2trillion <[email protected]>
Date: Thu Mar 24 15:42:09 2022 -0400
O Circuito zkEVM consiste principalmente em 2 circuitos: Circuito EVM e Circuito de Estado. Primeiramente o código fonte do Circuito EVM será explicado neste artigo. A outra parte será explicada em um artigo posterior. Vamos analisar o design de cada coluna, como restringir cada Código de operação (Opcode) e como restringir e combinar vários Códigos de operação em detalhes.
Estrutura do Circuito
Abaixo está a estrutura do circuito EVM:
Do ponto de vista da Coluna, o Circuito EVM é dividido em 3 partes: 1/Seletor de Steps (incluindo o step atual, primeiro step, último step, etc.) 2/Circuito de Steps e 3/ Tabela Fixa (tabela de consulta fixa). A lógica do circuito de steps é a parte central. Step é a etapa de execução do ponto de vista das restrições do circuito. Esta seção está dividida em 2 partes: a/ Estado de execução (Seletor de estados de step) b/ Restrições dos estados de execução. Os módulos de restrição são rotulados com as linhas tracejadas na figura.
Para entender o Circuito EVM, é mais fácil começar com o código Configure (Configurar) e Assign (Atribuir).
Circuito EVM Configure
O Circuito EVM é implementado em zkevm-circuits/src/evm_circuit.rs. Vamos começar a partir de sua função configure:
pub fn configure<TxTable, RwTable, BytecodeTable, BlockTable>(
meta: &mut ConstraintSystem<F>,
power_of_randomness: [Expression<F>; 31],
tx_table: TxTable,
rw_table: RwTable,
bytecode_table: BytecodeTable,
block_table: BlockTable,
) -> Self
where
TxTable: LookupTable<F, 4>,
RwTable: LookupTable<F, 11>,
BytecodeTable: LookupTable<F, 4>,
BlockTable: LookupTable<F, 3>,
A restrição do Circuito EVM tem 2 partes: 1/ fixed_table 2/ ExecutionConfig. Fixed_table são algumas informações fixas da tabela, ocupando 4 colunas e correspondendo a tag/value1/value2/result.
Existem 10 tipos de tag, suas definições estão em zkevm-circuits/src/evm_circuit/table.rs:
pub enum FixedTableTag {
Range5 = 1,
Range16,
Range32,
Range256,
Range512,
SignByte,
BitwiseAnd,
BitwiseOr,
BitwiseXor,
ResponsibleOpcode,
}
Vejamos a seguir a seção Execução. A função configure do ExecutionConfig define outras restrições do circuito:
pub(crate) fn configure<TxTable, RwTable, BytecodeTable, BlockTable>(
meta: &mut ConstraintSystem<F>,
power_of_randomness: [Expression<F>; 31],
fixed_table: [Column<Fixed>; 4],
tx_table: TxTable,
rw_table: RwTable,
bytecode_table: BytecodeTable,
block_table: BlockTable,
) -> Self
where
TxTable: LookupTable<F, 4>,
RwTable: LookupTable<F, 11>,
BytecodeTable: LookupTable<F, 4>,
BlockTable: LookupTable<F, 3>,
{
q_step — Seletor de step
q_step_first — primeiro seletor de step
q_step_last — último seletor do step
qs_byte_lookup — seletor de verificação de intervalo de bytes
Para um Step, definimos suas restrições com 32 Colunas.
let q_step = meta.complex_selector();
let q_step_first = meta.complex_selector();
let q_step_last = meta.complex_selector();
let qs_byte_lookup = meta.advice_column();
let advices = [(); STEP_WIDTH].map(|_| meta.advice_column());
O que é um Step?
Do ponto de vista das funções, um Step é a execução de “um-Step”. Do ponto de vista do circuito, um Step é um circuito com 32 colunas por 16 linhas, os parâmetros de step são definidos em zkevm-circuits/src/evm_circuit/param.rs:
const STEP_WIDTH: usize = 32;
const STEP_HEIGHT: usize = 16;
A definição de um step pode ser encontrado em zkevm-circuits/src/evm_circuit/step.rs:
pub(crate) struct Step<F> {
pub(crate) state: StepState<F>,
pub(crate) rows: Vec<StepRow<F>>,
}
Um Step consiste de StepState e 16 StepRows. Primeiro, um Step Row contém todas as informações envolvidas em uma determinada Row de um Step:
pub(crate) struct StepRow<F> {
pub(crate) qs_byte_lookup: Cell<F>,
pub(crate) cells: [Cell<F>; STEP_WIDTH],
}
Para uma Row específica em um Step, exceto para os dados das células (cells), também deve haver o qs_byte_lookup correspondente para essa Row para verificar se os dados da célula Row devem ser restritos por Range256 (qs_byte_lookup será explicado posteriormente em detalhes ).
A estrutura de dados do StepState contém informações de estado do Step:
pub(crate) struct StepState<F> {
/// O estado de execução do step
pub(crate) execution_state: Vec<Cell<F>>,
/// O contador de leitura/escrita
pub(crate) rw_counter: Cell<F>,
/// O identificador único de chamada em toda a prova, usando o
/// `rw_counter` no step de chamada.
pub(crate) call_id: Cell<F>,
/// Whether the call is root call
pub(crate) is_root: Cell<F>,
/// Se a chamada é uma createt call
pub(crate) is_create: Cell<F>,
// Este é o identificador do bytecode atual executado, que é usado para
// procurar o código executado atualmente e usado para fazer cópia de código. Na maior parte do tempo,
// seria bytecode_hash, mas quando se trata de chamada de criação root, o
// executado pela bytecode é na verdade a partir de calendários de transações, portanto pode ser
// tx_id se decidirmos procurar em outra tabela.
// Entretanto, como lidar com a chamada de criação root ainda está por ser determinada, veja
// a questão https://github.com/appliedzkp/zkevm-specs/issues/73 para mais
// discussão.
pub(crate) code_source: Cell<F>,
/// O contador do programa
pub(crate) program_counter: Cell<F>,
/// O ponteira da pilha
pub(crate) stack_pointer: Cell<F>,
/// A quantidade de gás restante
pub(crate) gas_left: Cell<F>,
/// Tamanho da memória em palavras (32 bytes)
pub(crate) memory_word_size: Cell<F>,
/// O contador para gravações de estado
pub(crate) state_write_counter: Cell<F>,
}
Vamos verificar a definição de cada variável StepState.
- Execution_state — estado de execução do Step atual, que é definido em step.rs:
pub enum ExecutionState {
// Estado Interno
BeginTx,
EndTx,
EndBlock,
CopyToMemory,
// Casos de sucesso de código de operação
STOP,
ADD, // ADD, SUB
...
// Casos de erro
ErrorInvalidOpcode,
ErrorStackOverflow,
ErrorStackUnderflow,
...
}
O estado de execução do Step inclui o estado interno (transações em um bloco isolado por BeginTX e EndTx), o estado de execução bem-sucedida e o estado de erro do Código de operação. O estado de execução bem-sucedida do Código de operação pode ser representado por uma restrição adequada ao caso. Em outras palavras, pela mesma restrição, os estados de execução de vários código de operação podem ser representados. Por exemplo, se os Código de operação ADD e SUB usarem uma restrição, eles poderão aplicar a mesma restrição a cada estado de execução.
- rw_counter — use rw_counter para distinguir o mesmo endereço ao visitar Stack/Memory
- call_id — cada chamada de funções recebe um id para distinguir uma da outra
- is_root — se é root ou não
- is_create — se a chamada de create é chamada
- code_source — o rótulo para chamar um programa (geralmente o resultado de hash de um programa)
- program_counter — PC
- stack_point — Ponteiro da pilha
- gas_left — o montante de gás restante
- memory_word_size — tamanho da memória (unidade como uma palavra (32 bytes))
- state_write_counter — contador de gravação de estado
Uma análise mais detalhada da função de construção Step (nova) mostra que StepState e StepRow são criadas separadamente ao criar um Step.
pub(crate) fn new(
meta: &mut ConstraintSystem<F>,
qs_byte_lookup: Column<Advice>,
advices: [Column<Advice>; STEP_WIDTH],
is_next_step: bool,
) -> Self {
A lógica para criar um StepState é mostrada abaixo:
let num_state_cells = ExecutionState::amount() + N_CELLS_STEP_STATE;
let mut cells = VecDeque::with_capacity(num_state_cells);
meta.create_gate("Query state for step", |meta| {
for idx in 0..num_state_cells {
let column_idx = idx % STEP_WIDTH;
let rotation = idx / STEP_WIDTH + if is_next_step { STEP_HEIGHT } else { 0 };
cells.push_back(Cell::new(meta, advices[column_idx], rotation));
}
vec![0.expr()]
});
StepState {
execution_state: cells.drain(..ExecutionState::amount()).collect(),
rw_counter: cells.pop_front().unwrap(),
call_id: cells.pop_front().unwrap(),
is_root: cells.pop_front().unwrap(),
is_create: cells.pop_front().unwrap(),
code_source: cells.pop_front().unwrap(),
program_counter: cells.pop_front().unwrap(),
stack_pointer: cells.pop_front().unwrap(),
gas_left: cells.pop_front().unwrap(),
memory_word_size: cells.pop_front().unwrap(),
state_write_counter: cells.pop_front().unwrap(),
}
N_CELLS_STEP_STATE=10 é o número de Células no StepState que não seja o operation_state.
De acordo com as 32 colunas por 16 linhas, crie as Células correspondentes para aconselhar essas Colunas. É fundamental entender o que essas Células representam, a Rotation(offset) é usada para distinguir diferentes Células na mesma Coluna. Ao escrever circuitos, preste atenção especial à abstração e descrição das Células, esses circuitos modularizados podem usar várias instâncias. Agora, as restrições do circuito de uma etapa podem ser descritas com precisão com essas células para o StepState e seus seletores q_step correspondentes. Basicamente, os seletores q_step restringem as linhas e a Célula na Etapa é localizada por Rotation (offset relativo).
A lógica para criar um StepRow é mostrada abaixo:
let mut rows = Vec::with_capacity(STEP_HEIGHT - rotation_offset);
meta.create_gate("Query rows for step", |meta| {
for rotation in rotation_offset..STEP_HEIGHT {
let rotation = rotation + if is_next_step { STEP_HEIGHT } else { 0 };
rows.push(StepRow {
qs_byte_lookup: Cell::new(meta, qs_byte_lookup, rotation),
cells: advices.map(|column| Cell::new(meta, column, rotation)),
});
}
vec![0.expr()]
});
Cada linha sob o StepState é chamada StepRow.
Restrições de portas personalizadas
As limitações de portões personalizados são mais complicadas, inclusive:
a. O execution_state de cada Step possui apenas um estado válido:
let sum_to_one = (
"Only one of execution_state should be enabled",
step_curr
.state
.execution_state
.iter()
.fold(1u64.expr(), |acc, cell| acc - cell.expr()), // expressão -> 1 - sum(células do estado)
);
A implementação consiste em somar os valores de todos os estados da célula. O sum_to_one é uma expressão 1-sum.
b. Cada execution_state de Step é booleano:
let bool_checks = step_curr.state.execution_state.iter().map(|cell| {
(
"Representation for execution_state should be bool",
cell.expr() * (1u64.expr() - cell.expr()),
)
});
Portanto, é um método comum verificar o valor booleano com a expressão x*(1-x).
c. O ExecutionState de dois Steps adjacentes deve satisfazer as restrições de transição: por exemplo, o ExecutionState deve ser BeginTx ou EndBlock após o EndTx.
[
(
"EndTx can only transit to BeginTx or EndBlock",
ExecutionState::EndTx,
vec![ExecutionState::BeginTx, ExecutionState::EndBlock],
),
(
"EndBlock can only transit to EndBlock",
ExecutionState::EndBlock,
vec![ExecutionState::EndBlock],
),
]
.map(|(name, from, to)| {
(
name,
step_curr.execution_state_selector([from])
* (1.expr() - step_next.execution_state_selector(to)),
)
}),
Observe que o ExecutionState da última etapa não precisa satisfazer essas restrições adjacentes.
.map(move |(name, poly)| (name, (1.expr() - q_step_last.clone()) * poly))
d. O ExecutionState do primeiro Step deve ser BeginTx, e o último deve ser EndBlock:
let _first_step_check = {
let begin_tx_selector =
step_curr.execution_state_selector([ExecutionState::BeginTx]);
iter::once((
"First step should be BeginTx",
q_step_first * (1.expr() - begin_tx_selector),
))
};
let _last_step_check = {
let end_block_selector =
step_curr.execution_state_selector([ExecutionState::EndBlock]);
iter::once((
"Last step should be EndBlock",
q_step_last * (1.expr() - end_block_selector),
))
};
Observe que essas restrições de porta personalizadas mostradas acima são apenas para um Step. Portanto, as restrições q_step devem ser adicionadas a todas as restrições.
iter::once(sum_to_one)
.chain(bool_checks)
.chain(execution_state_transition)
.map(move |(name, poly)| (name, q_step.clone() * poly))
// TODO: Habilite-os após o teste de CALLDATACOPY estar completo.
// .chain(first_step_check)
// .chain(last_step_check)
A versão atual do código não é a final, first_step_check e last_step_check estão comentadas. De TODO, podemos dizer que essas restrições serão adicionadas após o término do teste CALLDATACOPY.
Restrição de intervalo de dados para a Coluna Advice
As restrições de cada advice estão dentro do intervalo de bytes (Range256). Porque a restrição de intervalo é realizada em fixed_table e composta por 4 colunas fixas. Portanto, a restrição de intervalo de Range256 corresponde a 4 partes — tag/valor, etc.
for advice in advices {
meta.lookup_any("Qs byte", |meta| {
let advice = meta.query_advice(advice, Rotation::cur());
let qs_byte_lookup = meta.query_advice(qs_byte_lookup, Rotation::cur());
vec![
qs_byte_lookup.clone() * FixedTableTag::Range256.expr(), //restrição de tags
qs_byte_lookup * advice, //restrição de valor
0u64.expr(), //ignorar
0u64.expr(), //ignorar
]
.into_iter()
.zip(fixed_table.table_exprs(meta).to_vec().into_iter())
.collect::<Vec<_>>()
});
}
Até agora, temos a estrutura básica do circuito, incluindo 3 tipos principais de colunas, faixa de circuito de cada etapa, restrições internas de cada estado de execução e restrições de transição entre dois estados de execução.
Restrição de Gadget
Para cada tipo de Opcode, existe uma restrição de Gadget correspondente, que é implementada na função configure_gadget:
fn configure_gadget<G: ExecutionGadget<F>>(
meta: &mut ConstraintSystem<F>,
q_step: Selector,
q_step_first: Selector,
power_of_randomness: &[Expression<F>; 31],
step_curr: &Step<F>,
step_next: &Step<F>,
independent_lookups: &mut Vec<Vec<Lookup<F>>>,
presets_map: &mut HashMap<ExecutionState, Vec<Preset<F>>>,
) -> G {
Para cada restrição de Gadget, há uma classe de ConstraintBuilder:
let mut cb = ConstraintBuilder::new(
step_curr,
step_next,
power_of_randomness,
G::EXECUTION_STATE,
);
let gadget = G::configure(&mut cb);
let (constraints, constraints_first_step, lookups, presets) = cb.build();
debug_assert!(
presets_map.insert(G::EXECUTION_STATE, presets).is_none(),
"execution state already configured"
);
Então, primeiro podemos criar uma instância do ConstraintBuilder usando ConstraintBuilder::new. Para cada tipo de Gadget, use sua função configure correspondente e, em seguida, use a função build do ConstraintBuilder para concluir a configuração da restrição.
Vamos começar com a definição do ConstraintBuilder. A definição do ConstraintBuilder está em zkevm-circuits/src/evm_circuit/util/constraint_builder.rs:
pub(crate) struct ConstraintBuilder<'a, F> {
pub(crate) curr: &'a Step<F>, //Step atual
pub(crate) next: &'a Step<F>, //next Step
power_of_randomness: &'a [Expression<F>; 31],
execution_state: ExecutionState, //estado de execução
cb: BaseConstraintBuilder<F>, //construtor de base
constraints_first_step: Vec<(&'static str, Expression<F>)>,
lookups: Vec<(&'static str, Lookup<F>)>,
curr_row_usages: Vec<StepRowUsage>, // StepRow atual
next_row_usages: Vec<StepRowUsage>, // próximo StepRow
rw_counter_offset: Expression<F>, //
program_counter_offset: usize, //PC
stack_pointer_offset: i32, //栈指针
in_next_step: bool, //
condition: Option<Expression<F>>,
}
a. ConstraintBuilder::new
Crie uma instância ConstraintBuilder.
b. G::configure
Todos os códigos de Gadget relacionados ao Código de operação estão em zkevm-circuits/src/evm_circuit/execution/. Atualmente, há suporte para mais de trinta tipos de Gadget, o que significa que há suporte para mais de trinta tipos de execution_states. A seguir está a implementação de AddGadget.
pub(crate) struct AddGadget<F> {
same_context: SameContextGadget<F>,
add_words: AddWordsGadget<F, 2, false>,
is_sub: PairSelectGadget<F>,
}
O AddGadget depende de 3 outros Gadgets: SameContextGadget (restrição de contexto), AddWordsGadget (palavras somadas) e PairSelectGadget (escolha a ou b). Através da função configure do AddGadget, podemos verificar as restrições relacionadas.
1/ Acesse o código de operação e o a/b/c em cada Cell via cb.query_cell e cb.query_word
let opcode = cb.query_cell();
let a = cb.query_word();
let b = cb.query_word();
let c = cb.query_word();
2/ Construar restrição aditiva (transformar subtração em adição)
let add_words = AddWordsGadget::construct(cb, [a.clone(), b.clone()], c.clone());
3/ Verifique se o código de operação é ADD ou SUB
let is_sub = PairSelectGadget::construct(
cb,
opcode.expr(),
OpcodeId::SUB.expr(),
OpcodeId::ADD.expr(),
);
4/ Restrinja as mudanças de Stack
cb.stack_pop(select::expr(is_sub.expr().0, c.expr(), a.expr()));
cb.stack_pop(b.expr());
cb.stack_push(select::expr(is_sub.expr().0, a.expr(), c.expr()));
5/ Restrinja a transição de Context
let step_state_transition = StepStateTransition {
rw_counter: Delta(3.expr()),
program_counter: Delta(1.expr()),
stack_pointer: Delta(1.expr()),
gas_left: Delta(-OpcodeId::ADD.constant_gas_cost().expr()),
..StepStateTransition::default()
};
let same_context = SameContextGadget::construct(cb, opcode, step_state_transition);
Esteja ciente de que todas as restrições são armazenadas na variável cb.constraints no final.
c. cb.build
cb.build é para corrigir e editar cada Gadget. Para cada linha na etapa atual:
1/ Se não houver célula usada, restrinja a célula para ser 0
2/ Se precisar verificar o intervalo, use qs_byte_lookup para verificar
for (row, usage) in self.curr.rows.iter().zip(self.curr_row_usages.iter()) {
if usage.is_byte_lookup_enabled {
constraints.push(("Enable byte lookup", row.qs_byte_lookup.expr() - 1.expr()));
}
presets.extend(
row.cells[usage.next_idx..]
.iter()
.map(|cell| (cell.clone(), F::zero())),
);
presets.push((
row.qs_byte_lookup.clone(),
if usage.is_byte_lookup_enabled {
F::one()
} else {
F::zero()
},
));
}
Para as restrições ou tabela de pesquisa da Step atual, adicione seu seletor execution_state.
let execution_state_selector = self.curr.execution_state_selector([self.execution_state]);
(
constraints
.into_iter()
.map(|(name, constraint)| (name, execution_state_selector.clone() * constraint))
.collect(),
self.constraints_first_step
.into_iter()
.map(|(name, constraint)| (name, execution_state_selector.clone() * constraint))
.collect(),
self.lookups
.into_iter()
.map(|(name, lookup)| (name, lookup.conditional(execution_state_selector.clone())))
.collect(),
presets,
)
Agora, temos a estrutura de restrição Step. ExecuteState é um possível estado de execução. Para qs_step, o local relativo/correspondente de execute_state é fixo. Além disso, cada valor de Célula execute_state deve ser booleano e apenas 1 estado de execução é válido. Cada estado de execução tem seu próprio circuito Gadget correspondente. O sequence_state_selector deve ser adicionado a todos os circuitos Gadget na função cb.build. Em outras palavras, todo o Circuito EVM contém todas as restrições de execution_state.
Antes de examinar as restrições de pesquisa, vamos falar sobre restrições de stack (pilha) e restrições de contexto.
Restrições de Stack
Olhando para trás na restrição AddGadget, usamos as funções cb.stack_pop e cb.stack_push para executar as restrições de pilha correspondentes.
pub(crate) fn stack_pop(&mut self, value: Expression<F>) {
self.stack_lookup(false.expr(), self.stack_pointer_offset.expr(), value);
self.stack_pointer_offset += 1;
}
pub(crate) fn stack_push(&mut self, value: Expression<F>) {
self.stack_pointer_offset -= 1;
self.stack_lookup(true.expr(), self.stack_pointer_offset.expr(), value);
}
stack_pop e stack_push têm implementações semelhantes, ambos editam stack_pointer_offset e restringem o valor no local de stack_pointer_offset em Stack por meio de stack_lookup.
pub(crate) fn stack_lookup(
&mut self,
is_write: Expression<F>, //operação de gravação?
stack_pointer_offset: Expression<F>, //stack offset
value: Expression<F>,
) {
self.rw_lookup(
"Stack lookup",
is_write,
RwTableTag::Stack,
[
self.curr.state.call_id.expr(),
0.expr(),
self.curr.state.stack_pointer.expr() + stack_pointer_offset,
0.expr(),
value,
0.expr(),
0.expr(),
0.expr(),
],
);
}
A parte principal é rw_loopup e a implementação de rw_loopup é baseada em rw_lookup_with_counter. O acesso a Stack consiste em call_id, Stack_offset e rw count. No mesmo Step State, é possível ler e escrever várias vezes no mesmo Stack_offset, portanto é necessário restringir os tempos de leitura e gravação.
Como implementar rw_loopup_with_counter? A tabela de pesquisa é registrada na variável de pesquisa ConstraintBuilder por meio de add_lookup para o Configure da tabela de pesquisa.
fn rw_lookup_with_counter(
&mut self,
name: &'static str,
counter: Expression<F>,
is_write: Expression<F>,
tag: RwTableTag,
values: [Expression<F>; 8],
) {
self.add_lookup(
name,
Lookup::Rw {
counter,
is_write,
tag: tag.expr(),
values,
},
);
}
Exceto para a tabela de pesquisa RW, atualmente, mais tipos de tabelas de pesquisa são suportados. Os tipos de enumeração de pesquisa são definidos em zkevm-circuits/src/evm_circuit/table.rs:
pub(crate) enum Lookup<F> {
/// Procure a tabela fixa que contém tabelas pré-construídas do servidor, tais como
/// tabelas de intervalo ou tabelas bitwise.
Fixed {
...
},
Tx {
...
},
Rw {
...
},
Bytecode {
...
},
Block {
...
},
Conditional {
...
}
Tabela de restrições de transação Tx, tabela de restrições de pesquisa RW de dados legíveis e graváveis (Stack/Memory), programas de execução de restrições Bytecode, e dados de bloqueio de restrições de blocos.
Olhando para trás na implementação da restrição Stack. Para cada Step, é possível operar Stack ou Memory. Para restringir essas operações, também precisamos atribuir Stack Pointer diferente de Cells para os dados. Quando o Stack Pointer é atribuído, a operação de stack em um step pode ser restrita independentemente. Além disso, as Células relacionadas ao Stack Pointer podem ser localizadas no Step via q_step. Em outras palavras, as restrições podem ser expressas independentemente para um Step. Obviamente, além das restrições para um único step, existem restrições de stack de consistência e precisão de dados entre vários Steps. Essas restrições podem ser definidas por “Restrições de pesquisa” (consulte o capítulo Restrições de pesquisa).
Restrições de Contexto
As restrições anteriores se concentram no único Estado de Execução. SameContextGadget são usados para restrições entre vários Estados de Execução.
pub(crate) struct SameContextGadget<F> {
opcode: Cell<F>,
sufficient_gas_left: RangeCheckGadget<F, N_BYTES_GAS>,
}
A restrição específica é implementada na função de construção:
pub(crate) fn construct(
cb: &mut ConstraintBuilder<F>,
opcode: Cell<F>,
step_state_transition: StepStateTransition<F>,
) -> Self {
cb.opcode_lookup(opcode.expr(), 1.expr());
cb.add_lookup(
"Responsible opcode lookup",
Lookup::Fixed {
tag: FixedTableTag::ResponsibleOpcode.expr(),
values: [
cb.execution_state().as_u64().expr(),
opcode.expr(),
0.expr(),
],
},
);
// Verifica se gas_left é suficiente
let sufficient_gas_left = RangeCheckGadget::construct(cb, cb.next.state.gas_left.expr());
// Transição de estado
cb.require_step_state_transition(step_state_transition);
Self {
opcode,
sufficient_gas_left,
}
}
A lógica é simples e clara, tendo as seguintes restrições:
1/ opcode_lookup — restringir o PC (Program Counter) tem os mesmos códigos de operação correspondentes
2/ add_lookup — restringe a consistência entre o código de operação e o estado de execução no Step
3/ Verifica se o gas_left é suficiente
4/ require_step_state_transition — restringe a transição de estado entre dois steps, por exemplo, as relações entre PCs, Stack Pointers, Call ids, etc.
Verifique o código-fonte se estiver interessado.
Restrições de consulta
Quando as restrições de cada estado de execução estiverem prontas, vamos começar a processar todas as restrições de consultas.
Self::configure_lookup(
meta,
q_step,
fixed_table,
tx_table,
rw_table,
bytecode_table,
block_table,
independent_lookups,
);
A implementação é simples. Todas as restrições de consulta não precisam apenas adicionar restrições q_step, mas também adicionar várias restrições de tabela. Independent_lookups é a restrição extra em um Step.
Atribuição de Circuito EVM
O circuito EVM usa assign_block para provar todas as transações em um bloco.
pub fn assign_block(
&self,
layouter: &mut impl Layouter<F>,
block: &Block<F>,
) -> Result<(), Error> {
self.execution.assign_block(layouter, block)
}
Em assign_block, configura q_step_first e q_step_last, também restringe cada Tx no bloco.
self.q_step_first.enable(&mut region, offset)?;
for transaction in &block.txs {
for step in &transaction.steps {
let call = &transaction.calls[step.call_index];
self.q_step.enable(&mut region, offset)?;
self.assign_exec_step(&mut region, offset, block, transaction, call, step)?;
offset += STEP_HEIGHT;
}
}
self.q_step_last.enable(&mut region, offset - STEP_HEIGHT)?;
Os steps de um Tx são armazenados na variável steps. Para cada step, use assign_exec_step para atribuir. Com base no entendimento do Configure, essas partes são mais fáceis de processar. Se você estiver interessado, verifique os códigos-fonte.
Isso é tudo para o Circuito EVM. Os próximos artigos falarão sobre State Circuit ( Circuito de Estado) e Bytecode Circuit (Circuito Bytecode).
Artigo escrito por Trapdoor-Tech e traduzido por Marcelo Panegali
Top comments (0)