From 895806fa81bc38256d72f2f8a9e43b189990e347 Mon Sep 17 00:00:00 2001 From: marcbeunardeau88 Date: Thu, 10 Oct 2024 11:54:03 +0200 Subject: [PATCH] o1vm/constraint : add a missing constraint for sel the selectors were only constrained to be boolean We add the constraint that one and only one of them is activated. --- o1vm/src/interpreters/mips/constraints.rs | 13 ++++++++++--- o1vm/src/pickles/mod.rs | 2 +- o1vm/src/pickles/tests.rs | 5 ++++- 3 files changed, 15 insertions(+), 5 deletions(-) diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs index 48c60195fd..73a0bb59a8 100644 --- a/o1vm/src/interpreters/mips/constraints.rs +++ b/o1vm/src/interpreters/mips/constraints.rs @@ -12,7 +12,7 @@ use crate::{ lookups::{Lookup, LookupTableIDs}, E, }; -use ark_ff::{Field, One}; +use ark_ff::{Field, One, Zero}; use kimchi::circuits::{ expr::{ConstantTerm::Literal, Expr, ExprInner, Operations, Variable}, gate::CurrOrNext, @@ -626,12 +626,19 @@ impl Env { /// Each selector must be a boolean. pub fn get_selector_constraints(&self) -> Vec> { let one = ::Variable::one(); - (0..N_MIPS_SEL_COLS) + let mut enforce_bool: Vec> = (0..N_MIPS_SEL_COLS) .map(|i| { let var = self.variable(MIPSColumn::Selector(i)); (var.clone() - one.clone()) * var.clone() }) - .collect() + .collect(); + let enforce_one_activation = (0..N_MIPS_SEL_COLS).fold(E::::zero(), |res, i| { + let var = self.variable(MIPSColumn::Selector(i)); + res + var.clone() + }); + + enforce_bool.push(enforce_one_activation); + enforce_bool } pub fn get_selector(&self) -> E { diff --git a/o1vm/src/pickles/mod.rs b/o1vm/src/pickles/mod.rs index 4c02ef87c1..328d7d368a 100644 --- a/o1vm/src/pickles/mod.rs +++ b/o1vm/src/pickles/mod.rs @@ -30,7 +30,7 @@ pub const DEGREE_QUOTIENT_POLYNOMIAL: u64 = 7; /// Total number of constraints for all instructions, including the constraints /// added for the selectors. -pub const TOTAL_NUMBER_OF_CONSTRAINTS: usize = 463; +pub const TOTAL_NUMBER_OF_CONSTRAINTS: usize = 464; #[cfg(test)] mod tests; diff --git a/o1vm/src/pickles/tests.rs b/o1vm/src/pickles/tests.rs index cfe2f127c4..c0b6c12d50 100644 --- a/o1vm/src/pickles/tests.rs +++ b/o1vm/src/pickles/tests.rs @@ -43,7 +43,10 @@ fn test_regression_selectors_for_instructions() { let mips_con_env = mips_constraints::Env::::default(); let constraints = mips_con_env.get_selector_constraints(); assert_eq!( - constraints.len(), + // We substract 1 as we have one boolean check per sel + // and 1 constraint to check that one and only one + // sel is activated + constraints.len() - 1, // We could use N_MIPS_SEL_COLS, but sanity check in case this value is // changed. RTypeInstruction::COUNT + JTypeInstruction::COUNT + ITypeInstruction::COUNT