Constrain syscall/exceptions filter to be boolean (#1458)

This commit is contained in:
Robin Salen 2024-01-11 12:05:57 +01:00 committed by GitHub
parent 606732a8b6
commit 233ddd4e0e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -29,6 +29,12 @@ pub(crate) fn eval_packed<P: PackedField>(
let filter_exception = lv.op.exception;
let total_filter = filter_syscall + filter_exception;
// First, constrain filters to be boolean.
// Ensuring they are mutually exclusive is done in other modules
// through the `is_cpu_cycle` variable.
yield_constr.constraint(filter_syscall * (filter_syscall - P::ONES));
yield_constr.constraint(filter_exception * (filter_exception - P::ONES));
// If exception, ensure we are not in kernel mode
yield_constr.constraint(filter_exception * lv.is_kernel_mode);
@ -132,6 +138,14 @@ pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
let filter_exception = lv.op.exception;
let total_filter = builder.add_extension(filter_syscall, filter_exception);
// First, constrain filters to be boolean.
// Ensuring they are mutually exclusive is done in other modules
// through the `is_cpu_cycle` variable.
let constr = builder.mul_sub_extension(filter_syscall, filter_syscall, filter_syscall);
yield_constr.constraint(builder, constr);
let constr = builder.mul_sub_extension(filter_exception, filter_exception, filter_exception);
yield_constr.constraint(builder, constr);
// Ensure that, if exception, we are not in kernel mode
let constr = builder.mul_extension(filter_exception, lv.is_kernel_mode);
yield_constr.constraint(builder, constr);