Merge pull request #974 from toposware/stack_bound

Set `stack_len_bounds_aux` properly
This commit is contained in:
Daniel Lubarov 2023-04-13 14:40:30 -07:00 committed by GitHub
commit b896f9b2da
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 23 additions and 10 deletions

View File

@ -141,8 +141,6 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
{
let local_values = vars.local_values.borrow();
let next_values = vars.next_values.borrow();
// TODO: Some failing constraints temporarily disabled by using this dummy consumer.
let mut dummy_yield_constr = ConstraintConsumer::new(vec![], P::ZEROS, P::ZEROS, P::ZEROS);
bootstrap_kernel::eval_bootstrap_kernel(vars, yield_constr);
contextops::eval_packed(local_values, next_values, yield_constr);
control_flow::eval_packed_generic(local_values, next_values, yield_constr);
@ -157,7 +155,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
shift::eval_packed(local_values, yield_constr);
simple_logic::eval_packed(local_values, yield_constr);
stack::eval_packed(local_values, yield_constr);
stack_bounds::eval_packed(local_values, &mut dummy_yield_constr);
stack_bounds::eval_packed(local_values, yield_constr);
syscalls::eval_packed(local_values, next_values, yield_constr);
}
@ -169,10 +167,6 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
) {
let local_values = vars.local_values.borrow();
let next_values = vars.next_values.borrow();
// TODO: Some failing constraints temporarily disabled by using this dummy consumer.
let zero = builder.zero_extension();
let mut dummy_yield_constr =
RecursiveConstraintConsumer::new(zero, vec![], zero, zero, zero);
bootstrap_kernel::eval_bootstrap_kernel_circuit(builder, vars, 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);
@ -187,7 +181,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
shift::eval_ext_circuit(builder, local_values, yield_constr);
simple_logic::eval_ext_circuit(builder, local_values, yield_constr);
stack::eval_ext_circuit(builder, local_values, yield_constr);
stack_bounds::eval_ext_circuit(builder, local_values, &mut dummy_yield_constr);
stack_bounds::eval_ext_circuit(builder, local_values, yield_constr);
syscalls::eval_ext_circuit(builder, local_values, next_values, yield_constr);
}

View File

@ -26,13 +26,13 @@ pub const MAX_USER_STACK_SIZE: usize = 1024;
// Other operations that have a minimum stack size (e.g. `MULMOD`, which has three inputs) read
// all their inputs from memory. On underflow, the cross-table lookup fails, as -1, ..., -17 are
// invalid memory addresses.
const DECREMENTING_FLAGS: [usize; 1] = [COL_MAP.op.pop];
pub(crate) const DECREMENTING_FLAGS: [usize; 1] = [COL_MAP.op.pop];
// Operations that increase the stack length by 1, but excluding:
// - privileged (kernel-only) operations (superfluous; doesn't affect correctness),
// - operations that from userspace to the kernel (required for correctness).
// TODO: This list is incomplete.
const INCREMENTING_FLAGS: [usize; 2] = [COL_MAP.op.pc, COL_MAP.op.dup];
pub(crate) const INCREMENTING_FLAGS: [usize; 2] = [COL_MAP.op.pc, COL_MAP.op.dup];
/// Calculates `lv.stack_len_bounds_aux`. Note that this must be run after decode.
pub fn generate<F: Field>(lv: &mut CpuColumnsView<F>) {

View File

@ -4,6 +4,7 @@ use plonky2::field::types::Field;
use crate::cpu::columns::CpuColumnsView;
use crate::cpu::kernel::aggregator::KERNEL;
use crate::cpu::stack_bounds::{DECREMENTING_FLAGS, INCREMENTING_FLAGS, MAX_USER_STACK_SIZE};
use crate::generation::state::GenerationState;
use crate::memory::segments::Segment;
use crate::witness::errors::ProgramError;
@ -258,6 +259,24 @@ fn try_perform_instruction<F: Field>(state: &mut GenerationState<F>) -> Result<(
fill_op_flag(op, &mut row);
let check_underflow: F = DECREMENTING_FLAGS.map(|i| row[i]).into_iter().sum();
let check_overflow: F = INCREMENTING_FLAGS.map(|i| row[i]).into_iter().sum();
let no_check = F::ONE - (check_underflow + check_overflow);
let disallowed_len = check_overflow * F::from_canonical_usize(MAX_USER_STACK_SIZE) - no_check;
let diff = row.stack_len - disallowed_len;
let user_mode = F::ONE - row.is_kernel_mode;
let rhs = user_mode + check_underflow;
row.stack_len_bounds_aux = match diff.try_inverse() {
Some(diff_inv) => diff_inv * rhs, // `rhs` may be a value other than 1 or 0
None => {
assert_eq!(rhs, F::ZERO);
F::ZERO
}
};
perform_op(state, op, row)
}