Constrain clock (#1343)

This commit is contained in:
Hamy Ratoanina 2023-11-09 16:42:18 -05:00 committed by GitHub
parent 954d1a77c6
commit 01bbf1a058
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 41 additions and 1 deletions

37
evm/src/cpu/clock.rs Normal file
View File

@ -0,0 +1,37 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::CpuColumnsView;
/// Check the correct updating of `clock`.
pub fn eval_packed<P: PackedField>(
lv: &CpuColumnsView<P>,
nv: &CpuColumnsView<P>,
yield_constr: &mut ConstraintConsumer<P>,
) {
// The clock is 0 at the beginning.
yield_constr.constraint_first_row(lv.clock);
// The clock is incremented by 1 at each row.
yield_constr.constraint_transition(nv.clock - lv.clock - P::ONES);
}
/// Circuit version of `eval_packed`.
/// Check the correct updating of `clock`.
pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
lv: &CpuColumnsView<ExtensionTarget<D>>,
nv: &CpuColumnsView<ExtensionTarget<D>>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
// The clock is 0 at the beginning.
yield_constr.constraint_first_row(builder, lv.clock);
// The clock is incremented by 1 at each row.
{
let new_clock = builder.add_const_extension(lv.clock, F::ONE);
let constr = builder.sub_extension(nv.clock, new_clock);
yield_constr.constraint_transition(builder, constr);
}
}

View File

@ -15,7 +15,7 @@ use crate::all_stark::Table;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::{COL_MAP, NUM_CPU_COLUMNS};
use crate::cpu::{
bootstrap_kernel, contextops, control_flow, decode, dup_swap, gas, jumps, membus, memio,
bootstrap_kernel, clock, contextops, control_flow, decode, dup_swap, gas, jumps, membus, memio,
modfp254, pc, push0, shift, simple_logic, stack, stack_bounds, syscalls_exceptions,
};
use crate::cross_table_lookup::{Column, TableWithColumns};
@ -238,6 +238,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
let next_values: &CpuColumnsView<P> = next_values.borrow();
bootstrap_kernel::eval_bootstrap_kernel_packed(local_values, next_values, yield_constr);
clock::eval_packed(local_values, next_values, yield_constr);
contextops::eval_packed(local_values, next_values, yield_constr);
control_flow::eval_packed_generic(local_values, next_values, yield_constr);
decode::eval_packed_generic(local_values, yield_constr);
@ -278,6 +279,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
next_values,
yield_constr,
);
clock::eval_ext_circuit(builder, local_values, next_values, yield_constr);
contextops::eval_ext_circuit(builder, local_values, next_values, yield_constr);
control_flow::eval_ext_circuit(builder, local_values, next_values, yield_constr);
decode::eval_ext_circuit(builder, local_values, yield_constr);

View File

@ -1,4 +1,5 @@
pub(crate) mod bootstrap_kernel;
mod clock;
pub(crate) mod columns;
mod contextops;
pub(crate) mod control_flow;