Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
zkevm-circuits
zkevm-circuits
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 0
    • Issues 0
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Package Registry
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar

新注册的用户请输入邮箱并保存,随后登录邮箱激活账号。后续可直接使用邮箱登录!

  • zkp
  • zkevm-circuitszkevm-circuits
  • Wiki
    • Zkevm docs
  • 4 core

Last edited by 桂忠 Aug 30, 2024
Page history
This is an old version of this page. You can view the most recent version or browse the history.

4 core

总体布局

本段介绍结构体CoreCircuitConfig的列及其含义。

单功能列 Single-purpose columns

下面是core子电路中最简单的部分,单功能的列:

    /// transaction index, the index inside the block, repeated for rows in one execution state
    pub tx_idx: Column<Advice>,
    /// call id, unique for each call, repeated for rows in one execution state
    pub call_id: Column<Advice>,
    /// contract code address, repeated for rows in one execution state
    pub code_addr: Column<Advice>,
    /// program counter, repeated for rows in one execution state
    pub pc: Column<Advice>,
    /// the opcode, repeated for rows in one execution state
    pub opcode: Column<Advice>,
    /// row counter, decremented for rows in one execution state
    pub cnt: Column<Advice>,
  • tx_idx指交易是区块的第几笔
  • call_id是我们在处理执行轨迹的时候,遇到新的call,就给其分配一个唯一的id。注意不是每次增加1的
  • code_addr是此时运行的合约代码的地址
  • pc是此时程序计数器的位置
  • opcode是此时程序计数器指向的指令
  • 较为难理解的是列cnt,它是为了在执行一步占用多行的情况下设计的。在执行状态这一章会详细讲解。

core子电路中,行数的推进也意味着EVM程序执行轨迹的推进,如果某变化发生,那么下一行的这个列的值就会发生变化,也会有门约束约束这个变化。例如,下一步的pc要加2,那么witness的表中pc这列的值下一行就要加2,并且电路需要约束pc的差为2。

多功能列 Versatile columns

为了减少列的使用,缩减电路规模,我们设计了多功能的列。在不同的执行状态、不同的指令下,这些列起到不同的作用。除了上述单功能的列以外,其他我们需要的状态、变量等等,都使用多功能的列,可以达到重复利用列的效果。

目前设计有32个多功能的列,代码里呈现为

    /// versatile columns that serve multiple purposes
    pub vers: [Column<Advice>; NUM_VERS],

其具体功能在执行状态一章会详细讲解。

执行状态 Execution State in Versatile

概念

执行状态是core子电路中每一步骤的种类,用以区分不同步骤的不同操作。EVM中的步骤的种类是指令(或opcode),而电路中的步骤的种类是执行状态。指令与执行状态基本成一一对应关系。有些相似指令,可以用同一种执行状态概括这些指令的操作。有些指令操作过于复杂,需要用连续的多个执行步骤进行处理。执行步骤的设计理念是使得代码尽量简单。

在代码里,使用enum来标识执行状态。执行状态的种类分为以下几种:

指令可对应的状态

这类状态目的就是处理EVM的指令的执行轨迹。包括但不限于:

pub enum ExecutionState {
    ......
    STOP,
    ADD,
    MUL,
    SUB,
    EXP,
    DIV_MOD,
    ADDMOD,
    MULMOD,
    POP,
    PUSH,
    ISZERO,
    AND_OR_XOR,
    ......
}

我们可以注意到,这两个名称“DIV_MOD”,“AND_OR_XOR”由下划线分隔了,意味着他们可以处理多个功能、逻辑相近的指令(DIV和MOD,AND、OR和XOR)。以逻辑运算指令AND、OR和XOR为例,尽管它们运算不同,但是操作模式相似。因此为了减少重复代码,可以使用一个执行状态处理这三种指令。

zkEVM电路内部的状态

在zkEVM电路中为了处理一些非EVM指令的流程,需要使用一些内部状态。EVM中不存在此概念。包括但不限于:

pub enum ExecutionState {
    ......
    END_PADDING, // it has to be the first state as it is the padding state
    BEGIN_TX_1, // start a tx, part one
    BEGIN_TX_2, // start a tx, part two
    END_BLOCK,
    END_TX,
    BEGIN_BLOCK,
    ......
}

EVM错误状态

对于EVM执行智能合约遇到错误的情况,例如out of gas,stack overflow等等,我们也需要处理。因此需要使用一些状态来表示遇到了EVM的错误。还未设计。

多行布局

一个执行状态,会使用连续的多行多功能列。例如,使用3行,即代码里变量NUM_ROWS=3,那么相当于使用了3*32=96个格子。

这个例子里,不直接使用1行96列的原因是我们想要减少列的使用。

对于一个执行状态的多行,我们对每个格子的使用方法做了统一设计,也设计了cnt列的使用方法。统一设计可以使得不同执行状态的开发变得相似,有利于减少重复代码。同时,还可以合并不同执行状态的约束(主要是查找表约束)。规定如下:

  • 针对一个执行状态,开发时要确定其使用的行数,即代码里变量NUM_ROWS,应为大于0的整数。
  • 执行状态使用的行是连续NUM_ROWS行,这些行里,cnt列的值从NUM_ROWS-1递减至0。下文用cnt=X表示cnt取值为X时的行
  • cnt=0的行的使用方法是:32列的前半部分作为“动态选择器”,后半部分用于“辅助变量”。
  • cnt=1的行的使用方法是,作为操作数及其属性的变量,同时起到可以作为来源进行去向是state子电路的查找表的作用。
  • cnt=2及以上的行的使用方法是,作为除state以外的查找表的作用。暂未完成全部说明。

动态选择器 Dynamic Selector

电路的约束,包括门约束和查找表约束,需要在不同执行状态下开启。例如,都是3个操作数a b c的执行状态,加法ADD和乘法MUL的门约束,一个应是a+b-c=0,一个应是a*b-c=0。那么在ADD执行状态下,我们启用“a+b-c=0”,禁用“a*b-c=0”,MUL执行状态下相反。可以使用halo2的selector来启用、禁用约束,但是这种selector列是静态的,固定的,不像advice列一样是可以作为变量改变,而不改变电路的。因此,我们需要发明一种“动态选择器”,可以通过改变advice列的值来启用、禁用约束。

动态选择器在概念上,是有若干个变量(advice列的格子)作为输入,输出N个0、1表达式的电路的一种组成部分。N个输出是由若干输入进行某种运算得出的,可用于控制启用、禁用N种执行状态的约束。由此可见,N也是执行状态的数目。一种最简单的设计是输入使用的个数也是N个advice列,使用当前行(Rotation::cur())取得N个变量,直接作为N个输出。我们采用了更复杂的方法,使得输入变量的数目减少为2sqrt(N)。具体方法不在这里赘述。

在代码上,我们的动态选择器是如下的结构体:DynamicSelectorConfig和DynamicSelectorChip。这两个结构体区别很小,只是一种代码习惯。结构体的成员就包括2sqrt(N)个advice列。结构体最重要的方法是获取第target个输出的方法:

    pub fn selector(
        &self,
        meta: &mut VirtualCells<F>,
        target: usize,
        at: Rotation,
    ) -> Expression<F>

在创建约束时,使用动态选择器作为启用、禁用的条件的示例如下,以ADD为例(示例代码,非开发代码):

// suppose we have a,b,c
let exec_state = ExecutionState::ADD;
let condition = dynamic_selector.selector(meta, exec_state as usize, Rotation::cur());
return vec![condition*(a+b-c)]

如上所述,我们的动态选择器的设计使用的变量,是来自2sqrt(N)个advice列的同一行的变量,因此,这些格子的布局可以在一行内装下,即cnt=0的行。只需保证2sqrt(N) < 32 即可。

辅助变量

辅助变量是一些表示当前EVM执行的进度或者状态的变量,我们使用cnt=0行里的一些特定位置的格子进行记录。例如,上文所述的动态选择器使用了32列中前20列,那么我们可以设计,辅助变量使用21至32列。辅助变量包括:

pub(crate) struct Auxiliary {
    /// State stamp (counter) at the end of the execution state
    pub(crate) state_stamp: Column<Advice>,
    /// Stack pointer at the end of the execution state
    pub(crate) stack_pointer: Column<Advice>,
    /// Log stamp (counter) at the end of the execution state
    pub(crate) log_stamp: Column<Advice>,
    /// Gas left at the end of the execution state
    pub(crate) gas_left: Column<Advice>,
    /// Refund at the end of the execution state
    pub(crate) refund: Column<Advice>,
    /// Memory usage in chunk at the end of the execution state
    pub(crate) memory_chunk: Column<Advice>,
    /// Read only indicator (0/1) at the end of the execution state
    pub(crate) read_only: Column<Advice>,
}

如果动态选择器使用了前20列,state_stamp就是32列中的第21列,stack_pointer是第22列,以此类推。注意,尽管代码里用了列Column,实际上只在cnt=0的行,这些列才作为辅助变量使用。cnt!=0的行,用作其他用途。

每个执行状态会对于这些变量进行不同的变化,例如ADD会将state_stamp加3,stack_pointer减1。

注:Gas & Refund已有设计,没实现。等待从钉钉文档搬运过来。Memory chunk 和 readonly 暂无。

用于state的查找表格子

在cnt=1行,32个格子用于state的查找表,每个查找表用8个连续的格子,所以总共可以有4个查找表。不到4个,格子填充默认值0。

一个查找表操作在代码里用enum表示,state是enum其中一个。成员即是8个格子,代码里用Expression结构。

pub enum LookupEntry<F> {
    ......
    /// Lookup to state table, which contains read/write of stack, memory, storage,
    /// call context, call data, and return data
    State {
        /// Tag can be stack, memory, storage, call context, call data, and return data
        tag: Expression<F>,
        /// State stamp.
        stamp: Expression<F>,
        /// Value high 128 bits.
        value_hi: Expression<F>,
        /// Value low 128 bits.
        value_lo: Expression<F>,
        /// This item in storage means contract addr. In stack, memory, call context
        /// it means call id.
        call_id_contract_addr: Expression<F>,
        /// Point high is used for storage and means the key's high 128 bits.
        pointer_hi: Expression<F>,
        /// Point lo is used for storage and means the key's low 128 bits.
        /// It also means the pointer for stack, memory, call data, and return data.
        /// It also means the tag for call context.
        pointer_lo: Expression<F>,
        /// A boolean value to specify if the access record is a read or write.
        is_write: Expression<F>,
    }
}

要在代码里创建这种查找表操作,我们要用meta.query_xx将8列变为8个表达式Experssion,然后再创建这种enum。需要注意的是,代码的Rotation我们要用prev,即-1,因为我们设计的参照行是cnt=0行,cnt=1行是其上一行。

约束和分配数值

落实到代码:执行工具 Execution Gadget

/// Execution Gadget for the configure and witness generation of an execution state
pub(crate) trait ExecutionGadget<
    F: Field,
    const NUM_STATE_HI_COL: usize,
    const NUM_STATE_LO_COL: usize,
>
{
    fn name(&self) -> &'static str;
    fn execution_state(&self) -> ExecutionState;
    /// Number of rows this execution state will use in core circuit
    fn num_row(&self) -> usize;
    /// Number of rows before and after the actual witness that cannot be used, which decides that
    /// the selector cannot be enabled
    fn unusable_rows(&self) -> (usize, usize);

    /// Get gate constraints for this execution state (without condition).
    /// Rotation::cur() in the constraints means the row that column config.cnt is 0
    fn get_constraints(
        &self,
        config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
        meta: &mut VirtualCells<F>,
    ) -> Vec<(String, Expression<F>)>;

    /// Get lookups for this execution state, prepared for merging lookups among all states
    /// Rotation::cur() in the lookups means the row that column config.cnt is 0
    fn get_lookups(
        &self,
        config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
        meta: &mut ConstraintSystem<F>,
    ) -> Vec<(String, LookupEntry<F>)>;

    fn gen_witness(&self, trace: &Trace, current_state: &mut CurrentState) -> Witness;
}
  • NUM_STATE_HI_COL+NUM_STATE_LO_COL是动态选择器所需的列数
  • get_constraints类似configure函数,返回值是表达式的向量,用于创建门约束
  • get_lookups类似configure函数不过只负责查找表的部分。为了代码整洁,我们自定义了LookupEntry
  • gen_witness,生成此执行状态的core子电路的NUM_ROWS行的具体数值,为了方便其他子电路,也生成其他子电路需要的行。此方法的输入,Trace是这一步骤的执行轨迹,CurrentState是此时我们程序所需要的EVM的当前状态,目前包括pc, stack, memory等状态。

门约束

每个执行状态有对应的执行工具Gadget,其方法get_constraints返回所有需要创建的门约束,形式为表达式的向量。

在core子电路中,通过循环对每一个执行工具都调用get_constraints并创建其返回的门约束。

查找表约束

每个执行状态有对应的执行工具Gadget,其方法get_lookups返回所有需要创建的查找表约束,形式为LookupEntry的向量。

在core子电路中,通过循环对每一个执行工具都调用get_lookups,并将相同的LookupEntry合并,然后创建查找表约束,即meta.lookup_any(...)。

排列约束

目前没有用到Permutation constraints。

分配数值

因为证据Witness的表格设计和子电路的列的设计基本呈对应关系,分配数值的代码被大大简化。我们只需将表格每一行的数值分配给子电路的相应列的相应行(offset)即可。Witness生成则由每个执行工具的gen_witness方法负责,详见其代码。

例子

形象展示:

/// Add Execution State layout is as follows
/// where STATE means state table lookup,
/// ARITH means arithmetic table lookup,
/// DYNA_SELECTOR is dynamic selector of the state,
/// which uses NUM_STATE_HI_COL + NUM_STATE_LO_COL columns
/// AUX means auxiliary such as state stamp
/// +---+-------+-------+-------+----------+
/// |cnt| 8 col | 8 col | 8 col | not used |
/// +---+-------+-------+-------+----------+
/// | 2 | ARITH  |      |       |          |
/// | 1 | STATE | STATE | STATE |          |
/// | 0 | DYNA_SELECTOR   | AUX            |
/// +---+-------+-------+-------+----------+

代码:https://git.code.tencent.com/chainmaker-zk/zkevm/blob/develop/zkevm-circuits/src/execution/add.rs

Core Execution

JUMP

概述

概述:无条件跳转,跳转到指定PC的位置,JUMP跳转的位置一定是JUMPDEST所在的位置(JUMPDEST:跳转目标标记位,JUMPDEST标记的位置可以使用JUMP进行跳转)

具体操作:从栈顶弹出一个值,作为要跳转的目标PC的值

trace示例:JUMP指令执行时,会从栈中获取一个值,该值即是要跳转的PC,而该PC一定指向的是JUMPDEST的位置

PUSH1 0xa
PUSH30 0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
ADD
PUSH1 0x25
JUMP
JUMPDEST
PUSH1 0x29
JUMP
JUMPDEST
STOP

Core Row

core row中的表格设计如下

/// +---+-------+-------+-------+--------------------------+
/// |cnt| 8 col | 8 col | 8 col |             8col         |
/// +---+-------+-------+-------+--------------------------+
/// | 1 | STATE |       |       |  Bytecode LookUp         |
/// | 0 | DYNA_SELECTOR   | AUX                            |
/// +---+-------+-------+-------+--------------------------+

约束

  1. 当前的OPCODE=JUMP
  2. Stack Value约束(tag、state_stamp、 call_id、stack_pointer、is_write)
  3. Auxiliary字段约束(state_stamp、stack_pointer、log_stamp、read_only)
  4. next_pc=stack_top_value_lo (从栈顶获取的值作为要跳转的值,pc范围是在u64内的,只取value_lo即可)
  5. Stack_top_value_hi=0 (要对value_hi进行约束为0)
  6. lookup_value约束:lookup_pc=stack_top_value_lo (查找表操作,去向为bytecode table, 用来校验next_pc的合法性, lookup_pc一定也是stack_top_value_lo)
  7. lookup_value约束:lookup_bytecode_addr=meta.query_advice(config.code_addr, Rotation::cur()); (JUMP指令只是用来当前合约内部的PC跳转,next_pc_bytecode_addr有一定和当前的code_addr是一致的)
  8. lookup_value约束:lookup_not_code=0 (next_pc所指向的位置上JUMPDEST,是具体的指令,并不是bytecode, 而是opcode)

可参考下面示例代码:

 fn get_constraints(
        &self,
        config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
        meta: &mut VirtualCells<F>,
    ) -> Vec<(String, Expression<F>)> {
        let opcode = meta.query_advice(config.opcode, Rotation::cur());
        let pc_next = meta.query_advice(config.pc, Rotation::next());
        let code_addr = meta.query_advice(config.code_addr, Rotation::cur());

        // AUX字段约束...

        // stack value约束...

        // 其他约束
        let (_, _, value_hi, value_lo, _, _, _, _) = extract_lookup_expression!(state, state_entry);
        let (lookup_addr, expect_next_pc, _, not_code, _, _, _, _) =
            extract_lookup_expression!(bytecode, config.get_bytecode_full_lookup(meta));
        constraints.extend([
            (
                "opcode is JUMP".into(),
                opcode - OpcodeId::JUMP.as_u8().expr(),
            ),
            (
                "next pc = stack top".into(),
                pc_next.clone() - value_lo.clone(),
            ),
            ("stack top value_hi = 0".into(), value_hi - 0.expr()),
            (
                "bytecode lookup pc = stack top value_lo".into(),
                value_lo - expect_next_pc.clone(),
            ),
            (
                "bytecode lookup addr = code addr".into(),
                code_addr - lookup_addr,
            ),
            ("bytecode lookup not_code = 0".into(), not_code),
        ]);
        constraints
    }

LookUp

cnt=1的位置vers[24]~vers[31]的位置用来存放要lookUp的信息(next_pc的合法性,是否在bytecode中存在)

来源:core

去向:bytecode

可参考下面示例代码

insert_bytecode_full_lookup

将要lookup的值放入到core row, cnt=1,vers[24]~vers[31]的位置

fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelper) -> Witness {
  //...
  core_row_1.insert_bytecode_full_lookup(
              next_pc.as_u64(),
              OpcodeId::JUMPDEST,
              core_row_1.code_addr,
              Some(0.into()),
          );
  // ...
}

/// We can skip the constraint by setting code_addr to 0
 pub fn insert_bytecode_full_lookup(
        &mut self,
        pc: u64,
        opcode: OpcodeId,
        code_addr: U256,
        push_value: Option<U256>,
    ) {
        // this lookup must be in the row with this cnt
        assert_eq!(self.cnt, 1.into());

        for (cell, value) in [
            &mut self.vers_24,
            &mut self.vers_25,
            &mut self.vers_26,
            &mut self.vers_27,
            &mut self.vers_28,
            &mut self.vers_29,
            &mut self.vers_30,
            &mut self.vers_31,
        ]
        .into_iter()
        .zip([
            Some(code_addr),
            Some(pc.into()),
            Some(opcode.as_u8().into()),
            Some(0.into()), // non_code must be 0
            push_value.map(|x| (x >> 128).as_u128().into()),
            push_value.map(|x| (x.low_u128().into())),
            Some(opcode.data_len().into()),
            Some((opcode.is_push() as u8).into()),
        ]) {
            // before inserting, these columns must be none
            assert!(cell.is_none());
            *cell = value;
        }
       //....
    }

get_lookups

从core row, cnt=1,vers[24]~vers[31]的位置位置获取值,向Bytecode进行lookup, 这里使用的lookUp类型为BytecodeFull

 fn get_lookups(
        &self,
        config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
        meta: &mut ConstraintSystem<F>,
    ) -> Vec<(String, LookupEntry<F>)> {
        let stack_lookup = query_expression(meta, |meta| config.get_state_lookup(meta, 0));
        let bytecode_loopup = query_expression(meta, |meta| config.get_bytecode_full_lookup(meta));
        vec![
            ("jump_lookup_stack".into(), stack_lookup),
            ("jump_lookup_bytecode".into(), bytecode_loopup),
        ]
    }
    pub(crate) fn get_bytecode_full_lookup(&self, meta: &mut VirtualCells<F>) -> LookupEntry<F> {
        let (addr, pc, opcode, not_code, value_hi, value_lo, cnt, is_push) = (
            meta.query_advice(self.vers[24], Rotation::prev()),
            meta.query_advice(self.vers[25], Rotation::prev()),
            meta.query_advice(self.vers[26], Rotation::prev()),
            meta.query_advice(self.vers[27], Rotation::prev()),
            meta.query_advice(self.vers[28], Rotation::prev()),
            meta.query_advice(self.vers[29], Rotation::prev()),
            meta.query_advice(self.vers[30], Rotation::prev()),
            meta.query_advice(self.vers[31], Rotation::prev()),
        );
        LookupEntry::BytecodeFull {
            addr,
            pc,
            opcode,
            not_code,
            value_hi,
            value_lo,
            cnt,
            is_push,
        }
    }
Clone repository
  • basics
    • evm
    • halo2
  • code notes
    • binary_number_with_real_selector
    • how to use macro
    • simple_lt
    • simple_lt_word
  • Home
  • image
  • zkevm docs
    • 1 introduction
    • 10 public
    • 11 fixed
    • 12 exp
    • 13 keccak
    • 14 comparisons
    • 15 differences
View All Pages

Copyright © 2024 ChainWeaver Org. All Rights Reserved. 版权所有。

京ICP备2023035722号-3

京公网安备 11010802044225号