Add missing constraints mentioned by auditors (#1499)

This commit is contained in:
Robin Salen 2024-02-05 17:56:49 -05:00 committed by GitHub
parent af0259c5eb
commit 212f29cfb9
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 29 additions and 2 deletions

View File

@ -214,6 +214,10 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
yield_constr.constraint(flag * (flag - P::ONES));
}
// Only a single flag must be activated at once.
let all_flags = op_flags().map(|i| lv[i]).sum::<P>();
yield_constr.constraint(all_flags * (all_flags - P::ONES));
// Check that `OPCODE_COL` holds 0 if the operation is not a range_check.
let opcode_constraint = (P::ONES - lv[columns::IS_RANGE_CHECK]) * lv[columns::OPCODE_COL];
yield_constr.constraint(opcode_constraint);
@ -261,6 +265,11 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
yield_constr.constraint(builder, constraint);
}
// Only a single flag must be activated at once.
let all_flags = builder.add_many_extension(op_flags().map(|i| lv[i]));
let constraint = builder.mul_sub_extension(all_flags, all_flags, all_flags);
yield_constr.constraint(builder, constraint);
// Check that `OPCODE_COL` holds 0 if the operation is not a range_check.
let opcode_constraint = builder.arithmetic_extension(
F::NEG_ONE,

View File

@ -227,11 +227,19 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for LogicStark<F,
{
let lv = vars.get_local_values();
// IS_AND, IS_OR, and IS_XOR come from the CPU table, so we assume they're valid.
let is_and = lv[columns::IS_AND];
let is_or = lv[columns::IS_OR];
let is_xor = lv[columns::IS_XOR];
// Flags must be boolean.
for &flag in &[is_and, is_or, is_xor] {
yield_constr.constraint(flag * (flag - P::ONES));
}
// Only a single flag must be activated at once.
let all_flags = is_and + is_or + is_xor;
yield_constr.constraint(all_flags * (all_flags - P::ONES));
// The result will be `in0 OP in1 = sum_coeff * (in0 + in1) + and_coeff * (in0 AND in1)`.
// `AND => sum_coeff = 0, and_coeff = 1`
// `OR => sum_coeff = 1, and_coeff = -1`
@ -276,11 +284,21 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for LogicStark<F,
) {
let lv = vars.get_local_values();
// IS_AND, IS_OR, and IS_XOR come from the CPU table, so we assume they're valid.
let is_and = lv[columns::IS_AND];
let is_or = lv[columns::IS_OR];
let is_xor = lv[columns::IS_XOR];
// Flags must be boolean.
for &flag in &[is_and, is_or, is_xor] {
let constraint = builder.mul_sub_extension(flag, flag, flag);
yield_constr.constraint(builder, constraint);
}
// Only a single flag must be activated at once.
let all_flags = builder.add_many_extension([is_and, is_or, is_xor]);
let constraint = builder.mul_sub_extension(all_flags, all_flags, all_flags);
yield_constr.constraint(builder, constraint);
// The result will be `in0 OP in1 = sum_coeff * (in0 + in1) + and_coeff * (in0 AND in1)`.
// `AND => sum_coeff = 0, and_coeff = 1`
// `OR => sum_coeff = 1, and_coeff = -1`