Skip to content

Commit

Permalink
o1vm/constraint : add a missing constraint for sel
Browse files Browse the repository at this point in the history
the selectors were only constrained to be boolean
We add the constraint that one and only one
of them is activated.
  • Loading branch information
marcbeunardeau88 committed Oct 10, 2024
1 parent 09cf803 commit 895806f
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 5 deletions.
13 changes: 10 additions & 3 deletions o1vm/src/interpreters/mips/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -626,12 +626,19 @@ impl<Fp: Field> Env<Fp> {
/// Each selector must be a boolean.
pub fn get_selector_constraints(&self) -> Vec<E<Fp>> {
let one = <Self as InterpreterEnv>::Variable::one();
(0..N_MIPS_SEL_COLS)
let mut enforce_bool: Vec<E<Fp>> = (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::<Fp>::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<Fp> {
Expand Down
2 changes: 1 addition & 1 deletion o1vm/src/pickles/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
5 changes: 4 additions & 1 deletion o1vm/src/pickles/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,10 @@ fn test_regression_selectors_for_instructions() {
let mips_con_env = mips_constraints::Env::<Fp>::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
Expand Down

0 comments on commit 895806f

Please sign in to comment.