Skip to content

Commit

Permalink
Group ecall selectors in CPU table (#1678)
Browse files Browse the repository at this point in the history 
A simple cleanup to make #1610
easier to review.

---------

Co-authored-by: bing <[email protected]>
  • Loading branch information
@matthiasgoergens @spiral-ladder
matthiasgoergens and spiral-ladder authored May 28, 2024
1 parent c6126be commit 89b74f2
Show file tree
Hide file tree
Showing 3 changed files with 95 additions and 101 deletions.
77 changes: 40 additions & 37 deletions circuits/src/cpu/columns.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,6 +142,28 @@ impl From<(u32, mozak_runner::instruction::Instruction)> for Instruction<u32> {
}
}

columns_view_impl!(EcallSelectors);
/// Internal [`Instruction`] of Stark used for transition constraints
#[repr(C)]
#[derive(Clone, Copy, Eq, PartialEq, Debug)]
pub struct EcallSelectors<T> {
// We don't need all of these 'is_<some-ecall>' columns. Because our CPU table (by itself)
// doesn't need to be deterministic. We can assert these things in the CTL-ed
// ecall-specific tables.
// But to make that work, all ecalls need to be looked up; so we can use ops.ecall as the
// filter.
// TODO: implement the above.
pub is_private_tape: T,
pub is_public_tape: T,
pub is_call_tape: T,
pub is_event_tape: T,
pub is_events_commitment_tape: T,
pub is_cast_list_commitment_tape: T,
pub is_halt: T,
pub is_poseidon2: T,
pub is_self_prog_id_tape: T,
}

make_col_map!(CpuState);
columns_view_impl!(CpuState);
/// Represents the State of the CPU, which is also a row of the trace
Expand Down Expand Up @@ -219,21 +241,8 @@ pub struct CpuState<T> {
pub mem_addr: T,
pub io_addr: T,
pub io_size: T,
// We don't need all of these 'is_<some-ecall>' columns. Because our CPU table (by itself)
// doesn't need to be deterministic. We can assert these things in the CTL-ed
// ecall-specific tables.
// But to make that work, all ecalls need to be looked up; so we can use ops.ecall as the
// filter.
// TODO: implement the above.
pub is_private_tape: T,
pub is_public_tape: T,
pub is_call_tape: T,
pub is_event_tape: T,
pub is_events_commitment_tape: T,
pub is_cast_list_commitment_tape: T,
pub is_self_prog_id_tape: T,
pub is_halt: T,
pub is_poseidon2: T,

pub ecall_selectors: EcallSelectors<T>,
}
pub(crate) const CPU: &CpuState<ColumnWithTypedInput<CpuState<i64>>> = &COL_MAP;

Expand Down Expand Up @@ -379,32 +388,23 @@ pub fn lookup_for_fullword_memory() -> TableWithTypedOutput<MemoryCtl<Column>> {
/// [`CpuTable`](crate::cross_table_lookup::CpuTable).
#[must_use]
pub fn lookup_for_storage_tables() -> TableWithTypedOutput<StorageDeviceCtl<Column>> {
let storage = [
CPU.ecall_selectors.is_private_tape,
CPU.ecall_selectors.is_public_tape,
CPU.ecall_selectors.is_call_tape,
CPU.ecall_selectors.is_event_tape,
CPU.ecall_selectors.is_events_commitment_tape,
CPU.ecall_selectors.is_cast_list_commitment_tape,
CPU.ecall_selectors.is_self_prog_id_tape,
];
CpuTable::new(
StorageDeviceCtl {
op: ColumnWithTypedInput::ascending_sum([
CPU.is_private_tape,
CPU.is_public_tape,
CPU.is_call_tape,
CPU.is_event_tape,
CPU.is_events_commitment_tape,
CPU.is_cast_list_commitment_tape,
CPU.is_self_prog_id_tape,
]),
op: ColumnWithTypedInput::ascending_sum(storage),
clk: CPU.clk,
addr: CPU.io_addr,
size: CPU.io_size,
},
[
CPU.is_private_tape,
CPU.is_public_tape,
CPU.is_call_tape,
CPU.is_event_tape,
CPU.is_events_commitment_tape,
CPU.is_cast_list_commitment_tape,
CPU.is_self_prog_id_tape,
]
.iter()
.sum(),
storage.iter().sum(),
)
}

Expand Down Expand Up @@ -465,7 +465,10 @@ pub fn lookup_for_program_rom() -> TableWithTypedOutput<ProgramRom<Column>> {

#[must_use]
pub fn lookup_for_poseidon2_sponge() -> TableWithTypedOutput<Poseidon2SpongeCtl<Column>> {
CpuTable::new(Poseidon2SpongeCtl { clk: CPU.clk }, CPU.is_poseidon2)
CpuTable::new(
Poseidon2SpongeCtl { clk: CPU.clk },
CPU.ecall_selectors.is_poseidon2,
)
}

#[must_use]
Expand Down Expand Up @@ -511,7 +514,7 @@ pub fn lookup_for_skeleton() -> TableWithTypedOutput<CpuSkeletonCtl<Column>> {
clk: CPU.clk,
pc: CPU.inst.pc,
new_pc: CPU.new_pc,
will_halt: CPU.is_halt,
will_halt: CPU.ecall_selectors.is_halt,
},
CPU.is_running(),
)
Expand Down
49 changes: 19 additions & 30 deletions circuits/src/cpu/ecall.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,30 +11,14 @@ pub(crate) fn constraints<'a, P: Copy>(
lv: &CpuState<Expr<'a, P>>,
cb: &mut ConstraintBuilder<Expr<'a, P>>,
) {
let ecalls = &lv.ecall_selectors;
// ECALL is used for HALT, PRIVATE_TAPE/PUBLIC_TAPE or POSEIDON2 system
// call. So when instruction is ECALL, only one of them will be one.
cb.always(lv.is_poseidon2.is_binary());
cb.always(lv.is_halt.is_binary());
cb.always(lv.is_private_tape.is_binary());
cb.always(lv.is_public_tape.is_binary());
cb.always(lv.is_call_tape.is_binary());
cb.always(lv.is_event_tape.is_binary());
cb.always(lv.is_events_commitment_tape.is_binary());
cb.always(lv.is_cast_list_commitment_tape.is_binary());
cb.always(lv.is_self_prog_id_tape.is_binary());
cb.always(
lv.inst.ops.ecall
- (lv.is_halt
+ lv.is_private_tape
+ lv.is_public_tape
+ lv.is_call_tape
+ lv.is_event_tape
+ lv.is_events_commitment_tape
+ lv.is_cast_list_commitment_tape
+ lv.is_self_prog_id_tape
+ lv.is_poseidon2),
);
cb.always(lv.is_halt * (lv.op1_value - i64::from(ecall::HALT)));
for ecall in ecalls {
cb.always(ecall.is_binary());
}
cb.always(lv.inst.ops.ecall - ecalls.iter().sum::<Expr<'a, P>>());
cb.always(lv.ecall_selectors.is_halt * (lv.op1_value - i64::from(ecall::HALT)));
storage_device_constraints(lv, cb);
poseidon2_constraints(lv, cb);
}
Expand All @@ -43,25 +27,30 @@ pub(crate) fn storage_device_constraints<'a, P: Copy>(
lv: &CpuState<Expr<'a, P>>,
cb: &mut ConstraintBuilder<Expr<'a, P>>,
) {
cb.always(lv.is_private_tape * (lv.op1_value - i64::from(ecall::PRIVATE_TAPE)));
cb.always(lv.is_public_tape * (lv.op1_value - i64::from(ecall::PUBLIC_TAPE)));
cb.always(lv.is_call_tape * (lv.op1_value - i64::from(ecall::CALL_TAPE)));
cb.always(lv.is_event_tape * (lv.op1_value - i64::from(ecall::EVENT_TAPE)));
let ecalls = &lv.ecall_selectors;
cb.always(ecalls.is_private_tape * (lv.op1_value - i64::from(ecall::PRIVATE_TAPE)));
cb.always(ecalls.is_public_tape * (lv.op1_value - i64::from(ecall::PUBLIC_TAPE)));
cb.always(ecalls.is_call_tape * (lv.op1_value - i64::from(ecall::CALL_TAPE)));
cb.always(ecalls.is_event_tape * (lv.op1_value - i64::from(ecall::EVENT_TAPE)));
cb.always(
lv.is_events_commitment_tape * (lv.op1_value - i64::from(ecall::EVENTS_COMMITMENT_TAPE)),
ecalls.is_events_commitment_tape
* (lv.op1_value - i64::from(ecall::EVENTS_COMMITMENT_TAPE)),
);
cb.always(
lv.is_cast_list_commitment_tape
ecalls.is_cast_list_commitment_tape
* (lv.op1_value - i64::from(ecall::CAST_LIST_COMMITMENT_TAPE)),
);
cb.always(lv.is_self_prog_id_tape * (lv.op1_value - i64::from(ecall::SELF_PROG_ID_TAPE)));
cb.always(
lv.ecall_selectors.is_self_prog_id_tape
* (lv.op1_value - i64::from(ecall::SELF_PROG_ID_TAPE)),
);
}

pub(crate) fn poseidon2_constraints<'a, P: Copy>(
lv: &CpuState<Expr<'a, P>>,
cb: &mut ConstraintBuilder<Expr<'a, P>>,
) {
cb.always(lv.is_poseidon2 * (lv.op1_value - i64::from(ecall::POSEIDON2)));
cb.always(lv.ecall_selectors.is_poseidon2 * (lv.op1_value - i64::from(ecall::POSEIDON2)));
}

// We are already testing ecall halt with our coda of every `code::execute`.
70 changes: 36 additions & 34 deletions circuits/src/cpu/generation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use plonky2::hash::hash_types::RichField;

use crate::bitshift::columns::Bitshift;
use crate::cpu::columns as cpu_cols;
use crate::cpu::columns::CpuState;
use crate::cpu::columns::{CpuState, EcallSelectors};
use crate::cpu_skeleton::columns::CpuSkeleton;
use crate::expr::PureEvaluator;
use crate::generation::MIN_TRACE_LENGTH;
Expand Down Expand Up @@ -103,41 +103,43 @@ pub fn generate_cpu_trace<F: RichField>(record: &ExecutionRecord<F>) -> Vec<CpuS
xor: generate_xor_row(inst, state),
mem_addr: F::from_canonical_u32(aux.mem.unwrap_or_default().addr),
mem_value_raw: from_u32(aux.mem.unwrap_or_default().raw_value),
is_poseidon2: F::from_bool(aux.poseidon2.is_some()),
io_addr: F::from_canonical_u32(io.addr),
io_size: F::from_canonical_usize(io.data.len()),
is_private_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StorePrivate)
)),
is_public_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StorePublic)
)),
is_call_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreCallTape)
)),
is_event_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreEventTape)
)),
is_events_commitment_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreEventsCommitmentTape)
)),
is_cast_list_commitment_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreCastListCommitmentTape)
)),
is_self_prog_id_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreSelfProgIdTape)
)),
is_halt: F::from_bool(matches!(
(inst.op, state.registers[usize::from(REG_A0)]),
(Op::ECALL, ecall::HALT)
)),
ecall_selectors: EcallSelectors {
is_poseidon2: F::from_bool(aux.poseidon2.is_some()),
is_private_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StorePrivate)
)),
is_public_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StorePublic)
)),
is_call_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreCallTape)
)),
is_event_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreEventTape)
)),
is_events_commitment_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreEventsCommitmentTape)
)),
is_cast_list_commitment_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreCastListCommitmentTape)
)),
is_self_prog_id_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreSelfProgIdTape)
)),
is_halt: F::from_bool(matches!(
(inst.op, state.registers[usize::from(REG_A0)]),
(Op::ECALL, ecall::HALT)
)),
},
..CpuState::default()
};

Expand Down

0 comments on commit 89b74f2

Please sign in to comment.