Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Add INCR privileged instructions #734

Open
wants to merge 14 commits into
base: develop
Choose a base branch
from
2 changes: 1 addition & 1 deletion .env
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ CPU_CIRCUIT_SIZE=8..21
KECCAK_CIRCUIT_SIZE=4..20
KECCAK_SPONGE_CIRCUIT_SIZE=8..17
LOGIC_CIRCUIT_SIZE=4..21
MEMORY_CIRCUIT_SIZE=17..24
MEMORY_CIRCUIT_SIZE=16..24
MEMORY_BEFORE_CIRCUIT_SIZE=16..23
MEMORY_AFTER_CIRCUIT_SIZE=7..23
POSEIDON_CIRCUIT_SIZE=4..25
19 changes: 12 additions & 7 deletions book/src/cpu_execution/privileged_instructions.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,37 +50,42 @@ ecPairing precompiles.
resetting memory sections (by calling MSTORE_32BYTES_32 with the
value 0).

7. `PROVER_INPUT`. Pushes a single prover input onto the stack.
7. `INCR`. Reads the `N`th element of the stack, and increments it in-place
by one without pushing or popping. There are 4 INCR operations, namely
INCR1, INCR2, INCR3, INCR4 to increment respectively the 1st, 2nd, 3rd
and 4th stack elements.

8. `GET_CONTEXT`. Pushes the current context onto the stack. The kernel
8. `PROVER_INPUT`. Pushes a single prover input onto the stack.

9. `GET_CONTEXT`. Pushes the current context onto the stack. The kernel
always has context 0.

9. `SET_CONTEXT`. Pops the top element of the stack and updates the
10. `SET_CONTEXT`. Pops the top element of the stack and updates the
current context to this value. It is usually used when calling
another contract or precompile, to distinguish the caller from the
callee.

10. `MLOAD_32BYTES`. Pops 2 elements from the stack (a Memory address,
11. `MLOAD_32BYTES`. Pops 2 elements from the stack (a Memory address,
and then a length $\ell$), and pushes a value onto the stack. The
pushed value corresponds to the U256 integer read from the
big-endian sequence of length $\ell$ from the memory address being
fetched. Note that an empty length is not valid, nor is a length
greater than 32 (as a U256 consists in at most 32 bytes). Missing
these conditions will result in an unverifiable proof.

11. `EXIT_KERNEL`. Pops 1 element from the stack. This instruction is
12. `EXIT_KERNEL`. Pops 1 element from the stack. This instruction is
used at the end of a syscall, before proceeding to the rest of the
execution logic. The popped element, *kexit_info*, contains several
pieces of information like the current program counter, the current
amount of gas used, and whether we are in kernel (i.e. privileged)
mode or not.

12. `MLOAD_GENERAL`. Pops 1 elements (a Memory address), and pushes the
13. `MLOAD_GENERAL`. Pops 1 elements (a Memory address), and pushes the
value stored at this memory address onto the stack. It can read any
memory location, general (similarly to MLOAD (0x51) instruction) or
privileged.

13. `MSTORE_GENERAL`. Pops 2 elements (a value and a Memory address),
14. `MSTORE_GENERAL`. Pops 2 elements (a value and a Memory address),
and writes the popped value from the stack at the fetched address.
It can write to any memory location, general (similarly to MSTORE
(0x52) / MSTORE8 (0x53) instructions) or privileged.
9 changes: 8 additions & 1 deletion evm_arithmetization/src/all_stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -174,8 +174,15 @@ pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
/// `CrossTableLookup` for `ArithmeticStark`, to connect it with the `Cpu`
/// module.
fn ctl_arithmetic<F: Field>() -> CrossTableLookup<F> {
let cpu_arithmetic_looking = cpu_stark::ctl_arithmetic_base_rows();
let cpu_incr1_looking = cpu_stark::ctl_arithmetic_incr1_op();
let cpu_incr_other_looking = cpu_stark::ctl_arithmetic_incr_op();
CrossTableLookup::new(
vec![cpu_stark::ctl_arithmetic_base_rows()],
vec![
cpu_arithmetic_looking,
cpu_incr1_looking,
cpu_incr_other_looking,
],
arithmetic_stark::ctl_arithmetic_rows(),
)
}
Expand Down
25 changes: 25 additions & 0 deletions evm_arithmetization/src/cpu/columns/general.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ pub(crate) union CpuGeneralColumnsView<T: Copy> {
shift: CpuShiftView<T>,
stack: CpuStackView<T>,
push: CpuPushView<T>,
incr: CpuIncrView<T>,
context_pruning: CpuContextPruningView<T>,
}

Expand Down Expand Up @@ -93,6 +94,18 @@ impl<T: Copy> CpuGeneralColumnsView<T> {
unsafe { &mut self.push }
}

/// View of the columns required for the incr operation.
/// SAFETY: Each view is a valid interpretation of the underlying array.
pub(crate) const fn incr(&self) -> &CpuIncrView<T> {
unsafe { &self.incr }
}

/// Mutable view of the columns required for the incr operation.
/// SAFETY: Each view is a valid interpretation of the underlying array.
pub(crate) fn incr_mut(&mut self) -> &mut CpuIncrView<T> {
unsafe { &mut self.incr }
}

/// View of the column for context pruning.
/// SAFETY: Each view is a valid interpretation of the underlying array.
pub(crate) const fn context_pruning(&self) -> &CpuContextPruningView<T> {
Expand Down Expand Up @@ -217,6 +230,17 @@ pub(crate) struct CpuPushView<T: Copy> {
_padding_columns: [T; NUM_SHARED_COLUMNS - 1],
}

/// View of the first `CpuGeneralColumn` storing the sum of the first 2 opcode
/// bits to filter out `INCR1` instruction from the other ones (INCR2-INCR4).
#[repr(C)]
#[derive(Copy, Clone)]
pub(crate) struct CpuIncrView<T: Copy> {
/// Product of `incr` flag with the sum of the first 2 opcode bits.
pub(crate) is_not_incr1: T,
/// Reserve the unused columns.
_padding_columns: [T; NUM_SHARED_COLUMNS - 1],
}

/// View of the first `CpuGeneralColumn` storing a flag for context pruning.
#[derive(Copy, Clone)]
pub(crate) struct CpuContextPruningView<T: Copy> {
Expand All @@ -243,4 +267,5 @@ const_assert!(size_of::<CpuJumpsView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuShiftView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuStackView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuPushView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuIncrView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuContextPruningView<u8>>() == NUM_SHARED_COLUMNS);
2 changes: 2 additions & 0 deletions evm_arithmetization/src/cpu/columns/ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,8 @@ pub(crate) struct OpsColumnsView<T: Copy> {
pub m_op_general: T,
/// Combines PC and PUSH0
pub pc_push0: T,
/// Flag for INCR_N instructions.
pub incr: T,

/// Flag for syscalls.
pub syscall: T,
Expand Down
1 change: 1 addition & 0 deletions evm_arithmetization/src/cpu/contextops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ const KEEPS_CONTEXT: OpsColumnsView<bool> = OpsColumnsView {
m_op_32bytes: true,
exit_kernel: true,
m_op_general: true,
incr: true,
syscall: true,
exception: true,
};
Expand Down
92 changes: 89 additions & 3 deletions evm_arithmetization/src/cpu/cpu_stark.rs
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A possible optimization to avoid introducing an extra CTL just for INCR1 is to keep the same arithmetic CTL for all cases, with memory channels 1 and 2. Then you add INCR1-specific constraints to check that lv.stack_top == mem_channel[1] and nv.stack_top == mem_channel[2].

It requires using the value columns of some disable channels, but I couldn't find anywhere in the code that it wasn't possible.

Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,14 @@ use starky::lookup::{Column, Filter};
use starky::stark::Stark;

use super::columns::CpuColumnsView;
use super::halt;
use super::kernel::constants::context_metadata::ContextMetadata;
use super::kernel::opcodes::get_opcode;
use super::membus::{NUM_CHANNELS, NUM_GP_CHANNELS};
use crate::all_stark::{EvmStarkFrame, Table};
use crate::cpu::columns::{COL_MAP, NUM_CPU_COLUMNS};
use crate::cpu::{
byte_unpacking, clock, contextops, control_flow, decode, dup_swap, gas, jumps, membus, memio,
modfp254, pc, push0, shift, simple_logic, stack, syscalls_exceptions,
byte_unpacking, clock, contextops, control_flow, decode, dup_swap, gas, halt, incr, jumps,
membus, memio, modfp254, pc, push0, shift, simple_logic, stack, syscalls_exceptions,
};
use crate::memory::segments::Segment;
use crate::memory::VALUE_LIMBS;
Expand Down Expand Up @@ -131,6 +131,90 @@ pub(crate) fn ctl_arithmetic_base_rows<F: Field>() -> TableWithColumns<F> {
)
}

/// Returns the `TableWithColumns` for the CPU rows calling arithmetic
/// `ADD` operations through the `INCR1` privileged instruction.
///
/// It requires a different CTL than `INCR2`-`INCR4` as it does not incur any
/// memory reads.
pub(crate) fn ctl_arithmetic_incr1_op<F: Field>() -> TableWithColumns<F> {
// Instead of taking single columns, we reconstruct the entire opcode value
// directly.
let mut columns = vec![Column::constant(F::from_canonical_u8(get_opcode("ADD")))];

// Read value: current top of the stack
columns.extend(Column::singles(COL_MAP.mem_channels[0].value));

// Fixed second operand (`U256::one()`)
{
columns.push(Column::constant(F::ONE));
for _ in 1..VALUE_LIMBS {
columns.push(Column::constant(F::ZERO));
}
}

// Ignored third operand, `ADD` is a binary operation
for _ in 0..VALUE_LIMBS {
columns.push(Column::constant(F::ZERO));
}

// Returned value: next top of the stack
columns.extend(Column::singles_next_row(COL_MAP.mem_channels[0].value));

TableWithColumns::new(
*Table::Cpu,
columns,
Filter::new(
vec![(
Column::single(COL_MAP.op.incr),
Column::linear_combination_with_constant(
[(COL_MAP.general.incr().is_not_incr1, -F::ONE)],
F::ONE,
),
)],
vec![],
),
)
}

/// Returns the `TableWithColumns` for the CPU rows calling arithmetic
/// `ADD` operations through the `INCR2`-`INCR4` privileged instructions.
pub(crate) fn ctl_arithmetic_incr_op<F: Field>() -> TableWithColumns<F> {
// Instead of taking single columns, we reconstruct the entire opcode value
// directly.
let mut columns = vec![Column::constant(F::from_canonical_u8(get_opcode("ADD")))];

// Read value
columns.extend(Column::singles(COL_MAP.mem_channels[1].value));

// Fixed second operand (`U256::one()`)
{
columns.push(Column::constant(F::ONE));
for _ in 1..VALUE_LIMBS {
columns.push(Column::constant(F::ZERO));
}
}

// Ignored third operand, `ADD` is a binary operation
for _ in 0..VALUE_LIMBS {
columns.push(Column::constant(F::ZERO));
}

// Returned value
columns.extend(Column::singles(COL_MAP.mem_channels[2].value));

TableWithColumns::new(
*Table::Cpu,
columns,
Filter::new(
vec![(
Column::single(COL_MAP.op.incr),
Column::single(COL_MAP.general.incr().is_not_incr1),
)],
vec![],
),
)
}

/// Returns a column containing stale contexts.
pub(crate) fn ctl_context_pruning_looked<F: Field>() -> TableWithColumns<F> {
TableWithColumns::new(
Expand Down Expand Up @@ -612,6 +696,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
dup_swap::eval_packed(local_values, next_values, yield_constr);
gas::eval_packed(local_values, next_values, yield_constr);
halt::eval_packed(local_values, next_values, yield_constr);
incr::eval_packed(local_values, next_values, yield_constr);
jumps::eval_packed(local_values, next_values, yield_constr);
membus::eval_packed(local_values, yield_constr);
memio::eval_packed(local_values, next_values, yield_constr);
Expand Down Expand Up @@ -647,6 +732,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
dup_swap::eval_ext_circuit(builder, local_values, next_values, yield_constr);
gas::eval_ext_circuit(builder, local_values, next_values, yield_constr);
halt::eval_ext_circuit(builder, local_values, next_values, yield_constr);
incr::eval_ext_circuit(builder, local_values, next_values, yield_constr);
jumps::eval_ext_circuit(builder, local_values, next_values, yield_constr);
membus::eval_ext_circuit(builder, local_values, yield_constr);
memio::eval_ext_circuit(builder, local_values, next_values, yield_constr);
Expand Down
5 changes: 3 additions & 2 deletions evm_arithmetization/src/cpu/decode.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsume

use crate::cpu::columns::{CpuColumnsView, COL_MAP};

const OPCODES_LEN: usize = if cfg!(feature = "cdk_erigon") { 6 } else { 5 };
const OPCODES_LEN: usize = if cfg!(feature = "cdk_erigon") { 7 } else { 6 };

/// List of opcode blocks
/// Each block corresponds to exactly one flag, and each flag corresponds to
Expand Down Expand Up @@ -46,7 +46,8 @@ const OPCODES: [(u8, usize, bool, usize); OPCODES_LEN] = [
// JUMPDEST and KECCAK_GENERAL are handled manually here.
(0x56, 1, false, COL_MAP.op.jumps), // 0x56-0x57
(0x80, 5, false, COL_MAP.op.dup_swap), // 0x80-0x9f
(0xf6, 1, true, COL_MAP.op.context_op), //0xf6-0xf7
(0xe0, 2, true, COL_MAP.op.incr), // 0xe0-0xe3
(0xf6, 1, true, COL_MAP.op.context_op), // 0xf6-0xf7
(0xf9, 0, true, COL_MAP.op.exit_kernel),
// MLOAD_GENERAL and MSTORE_GENERAL flags are handled manually here.
];
Expand Down
8 changes: 4 additions & 4 deletions evm_arithmetization/src/cpu/dup_swap.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use crate::cpu::columns::{CpuColumnsView, MemoryChannelView};
use crate::memory::segments::Segment;

/// Constrain two channels to have equal values.
fn channels_equal_packed<P: PackedField>(
pub(crate) fn channels_equal_packed<P: PackedField>(
filter: P,
ch_a: &MemoryChannelView<P>,
ch_b: &MemoryChannelView<P>,
Expand All @@ -23,7 +23,7 @@ fn channels_equal_packed<P: PackedField>(
}

/// Constrain two channels to have equal values.
fn channels_equal_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
pub(crate) fn channels_equal_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
filter: ExtensionTarget<D>,
ch_a: &MemoryChannelView<ExtensionTarget<D>>,
Expand All @@ -41,7 +41,7 @@ fn channels_equal_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
///
/// `offset` is the stack index before this instruction is executed, e.g. `0`
/// for the top of the stack.
fn constrain_channel_packed<P: PackedField>(
pub(crate) fn constrain_channel_packed<P: PackedField>(
is_read: bool,
filter: P,
offset: P,
Expand All @@ -64,7 +64,7 @@ fn constrain_channel_packed<P: PackedField>(
///
/// `offset` is the stack index before this instruction is executed, e.g. `0`
/// for the top of the stack.
fn constrain_channel_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
pub(crate) fn constrain_channel_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
is_read: bool,
filter: ExtensionTarget<D>,
Expand Down
1 change: 1 addition & 0 deletions evm_arithmetization/src/cpu/gas.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ const SIMPLE_OPCODES: OpsColumnsView<Option<u32>> = OpsColumnsView {
m_op_32bytes: KERNEL_ONLY_INSTR,
exit_kernel: None,
m_op_general: KERNEL_ONLY_INSTR,
incr: KERNEL_ONLY_INSTR,
syscall: None,
exception: None,
};
Expand Down
Loading
Loading