Increment program counter on native instructions (#641)

This commit is contained in:
Jacqueline Nabaglo 2022-07-28 17:30:20 -07:00 committed by GitHub
parent 55d0eddecb
commit 16c2bee4b9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 50 additions and 17 deletions

View File

@ -260,6 +260,7 @@ mod tests {
let mut row: cpu::columns::CpuColumnsView<F> = let mut row: cpu::columns::CpuColumnsView<F> =
[F::ZERO; CpuStark::<F, D>::COLUMNS].into(); [F::ZERO; CpuStark::<F, D>::COLUMNS].into();
row.is_cpu_cycle = F::ONE; row.is_cpu_cycle = F::ONE;
row.program_counter = F::from_canonical_usize(i);
row.opcode = [ row.opcode = [
(logic::columns::IS_AND, 0x16), (logic::columns::IS_AND, 0x16),
(logic::columns::IS_OR, 0x17), (logic::columns::IS_OR, 0x17),
@ -319,10 +320,11 @@ mod tests {
} }
// Pad to a power of two. // Pad to a power of two.
for _ in cpu_trace_rows.len()..cpu_trace_rows.len().next_power_of_two() { for i in 0..cpu_trace_rows.len().next_power_of_two() - cpu_trace_rows.len() {
let mut row: cpu::columns::CpuColumnsView<F> = let mut row: cpu::columns::CpuColumnsView<F> =
[F::ZERO; CpuStark::<F, D>::COLUMNS].into(); [F::ZERO; CpuStark::<F, D>::COLUMNS].into();
row.is_cpu_cycle = F::ONE; row.is_cpu_cycle = F::ONE;
row.program_counter = F::from_canonical_usize(i + num_logic_rows);
cpu_stark.generate(row.borrow_mut()); cpu_stark.generate(row.borrow_mut());
cpu_trace_rows.push(row.into()); cpu_trace_rows.push(row.into());
} }
@ -335,10 +337,6 @@ mod tests {
let last_row: &mut cpu::columns::CpuColumnsView<F> = let last_row: &mut cpu::columns::CpuColumnsView<F> =
cpu_trace_rows[num_rows - 1].borrow_mut(); cpu_trace_rows[num_rows - 1].borrow_mut();
last_row.program_counter = halt_label; last_row.program_counter = halt_label;
let second_last_row: &mut cpu::columns::CpuColumnsView<F> =
cpu_trace_rows[num_rows - 2].borrow_mut();
second_last_row.next_program_counter = halt_label;
} }
trace_rows_to_poly_values(cpu_trace_rows) trace_rows_to_poly_values(cpu_trace_rows)

View File

@ -146,9 +146,6 @@ pub struct CpuColumnsView<T: Copy> {
/// If CPU cycle: the opcode, broken up into bits in **big-endian** order. /// If CPU cycle: the opcode, broken up into bits in **big-endian** order.
pub opcode_bits: [T; 8], pub opcode_bits: [T; 8],
/// If CPU cycle: The program counter for the next instruction.
pub next_program_counter: T,
/// Filter. 1 iff a Keccak permutation is computed on this row. /// Filter. 1 iff a Keccak permutation is computed on this row.
pub is_keccak: T, pub is_keccak: T,

View File

@ -5,9 +5,38 @@ use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget; use plonky2::iop::ext_target::ExtensionTarget;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::CpuColumnsView; use crate::cpu::columns::{CpuColumnsView, COL_MAP};
use crate::cpu::kernel::aggregator::KERNEL; use crate::cpu::kernel::aggregator::KERNEL;
// TODO: This list is incomplete.
const NATIVE_INSTRUCTIONS: [usize; 25] = [
COL_MAP.is_add,
COL_MAP.is_mul,
COL_MAP.is_sub,
COL_MAP.is_div,
COL_MAP.is_sdiv,
COL_MAP.is_mod,
COL_MAP.is_smod,
COL_MAP.is_addmod,
COL_MAP.is_mulmod,
COL_MAP.is_signextend,
COL_MAP.is_lt,
COL_MAP.is_gt,
COL_MAP.is_slt,
COL_MAP.is_sgt,
COL_MAP.is_eq,
COL_MAP.is_iszero,
COL_MAP.is_and,
COL_MAP.is_or,
COL_MAP.is_xor,
COL_MAP.is_not,
COL_MAP.is_byte,
COL_MAP.is_shl,
COL_MAP.is_shr,
COL_MAP.is_sar,
COL_MAP.is_pop,
];
fn get_halt_pcs<F: Field>() -> (F, F) { fn get_halt_pcs<F: Field>() -> (F, F) {
let halt_pc0 = KERNEL.global_labels["halt_pc0"]; let halt_pc0 = KERNEL.global_labels["halt_pc0"];
let halt_pc1 = KERNEL.global_labels["halt_pc1"]; let halt_pc1 = KERNEL.global_labels["halt_pc1"];
@ -26,10 +55,15 @@ pub fn eval_packed_generic<P: PackedField>(
// Once we start executing instructions, then we continue until the end of the table. // Once we start executing instructions, then we continue until the end of the table.
yield_constr.constraint_transition(lv.is_cpu_cycle * (nv.is_cpu_cycle - P::ONES)); yield_constr.constraint_transition(lv.is_cpu_cycle * (nv.is_cpu_cycle - P::ONES));
// If a row is a CPU cycle, then its `next_program_counter` becomes the `program_counter` of the // If a row is a CPU cycle and executing a native instruction (implemented as a table row; not
// next row. // microcoded) then the program counter is incremented by 1 to obtain the next row's program
yield_constr // counter.
.constraint_transition(lv.is_cpu_cycle * (nv.program_counter - lv.next_program_counter)); let is_native_instruction: P = NATIVE_INSTRUCTIONS.iter().map(|&col_i| lv[col_i]).sum();
yield_constr.constraint_transition(
lv.is_cpu_cycle
* is_native_instruction
* (lv.program_counter - nv.program_counter + P::ONES),
);
// If a non-CPU cycle row is followed by a CPU cycle row, then the `program_counter` of the CPU // If a non-CPU cycle row is followed by a CPU cycle row, then the `program_counter` of the CPU
// cycle row is 0. // cycle row is 0.
@ -64,11 +98,15 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
yield_constr.constraint_transition(builder, constr); yield_constr.constraint_transition(builder, constr);
} }
// If a row is a CPU cycle, then its `next_program_counter` becomes the `program_counter` of the // If a row is a CPU cycle and executing a native instruction (implemented as a table row; not
// next row. // microcoded) then the program counter is incremented by 1 to obtain the next row's program
// counter.
{ {
let constr = builder.sub_extension(nv.program_counter, lv.next_program_counter); let is_native_instruction =
let constr = builder.mul_extension(lv.is_cpu_cycle, constr); builder.add_many_extension(NATIVE_INSTRUCTIONS.iter().map(|&col_i| lv[col_i]));
let filter = builder.mul_extension(lv.is_cpu_cycle, is_native_instruction);
let pc_diff = builder.sub_extension(lv.program_counter, nv.program_counter);
let constr = builder.mul_add_extension(filter, pc_diff, filter);
yield_constr.constraint_transition(builder, constr); yield_constr.constraint_transition(builder, constr);
} }