Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Solve bit decomposition with negative coefficients. #2554

Merged
merged 37 commits into from
Mar 26, 2025
Merged
Changes from 1 commit
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
5f9c452
Solve bit decomposition with negative coefficients.
chriseth Mar 14, 2025
bf43c73
Make bit decomposition its own effect.
chriseth Mar 17, 2025
99558c2
fixes
chriseth Mar 17, 2025
f4f8a28
Remove negative case since this is now also covered.
chriseth Mar 17, 2025
f5fe3f5
Update test expectations.
chriseth Mar 17, 2025
1a378c3
Implement missing functions.
chriseth Mar 17, 2025
fcc5190
Codegen for bit decomposition.
chriseth Mar 18, 2025
7b4780e
clippy
chriseth Mar 18, 2025
94a8cc4
Test with negative value.
chriseth Mar 18, 2025
44bdd08
Use shift instead of division.
chriseth Mar 18, 2025
d2980dd
Fix typo.
chriseth Mar 18, 2025
a3b210c
Bit decomposition interpreter.
chriseth Mar 18, 2025
2e7d3a7
Jump through some hoops.
chriseth Mar 19, 2025
4ddae64
Tests and fixes.
chriseth Mar 19, 2025
721cd36
Merge remote-tracking branch 'origin/main' into bit_decomp_interpreter
chriseth Mar 19, 2025
589963b
Cover check.
chriseth Mar 20, 2025
977f106
Update executor/src/witgen/jit/compiler.rs
chriseth Mar 20, 2025
14647d1
Review.
chriseth Mar 20, 2025
2e87944
Remove bitand_signed_negated.
chriseth Mar 20, 2025
0906258
debugging
chriseth Mar 20, 2025
1059fa6
Add comment.
chriseth Mar 20, 2025
5cf50ee
Make all variables to be assigned in the branch mutable.
chriseth Mar 20, 2025
00750c8
Revert "debugging"
chriseth Mar 20, 2025
f71190c
remove debug
chriseth Mar 20, 2025
d398c25
Fix expectation.
chriseth Mar 20, 2025
85a3a4d
Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…
chriseth Mar 21, 2025
1c1eaa2
Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…
chriseth Mar 24, 2025
ea0a974
Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…
chriseth Mar 24, 2025
cbf290f
Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…
chriseth Mar 25, 2025
73f11ce
fix merge.
chriseth Mar 25, 2025
84d05ce
Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…
chriseth Mar 25, 2025
392a6d1
Merge remote-tracking branch 'origin/main' into bit_decomp_interpreter
chriseth Mar 25, 2025
8275be7
Merge branch 'bit_decomp_interpreter' into solve_bit_decomposition_wi…
chriseth Mar 25, 2025
4e70926
Remove "needs_mut"
chriseth Mar 26, 2025
f3d6b63
Review comments.
chriseth Mar 26, 2025
06cf432
Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…
chriseth Mar 26, 2025
f7630b9
Comment about conversion to two's complement.
chriseth Mar 26, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Tests and fixes.
  • Loading branch information
chriseth committed Mar 19, 2025
commit 4ddae64e8cfbdff8f60585a1dca56fdcb8fec750
111 changes: 80 additions & 31 deletions executor/src/witgen/jit/interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -260,33 +260,8 @@ impl<T: FieldElement> EffectsInterpreter<T> {
vars[*idx] = val;
}
InterpreterAction::BitDecompose(value, components, have_negative) => {
let mut val = value.evaluate(&mut eval_stack, &vars[..]);
if *have_negative {
for c in components {
let mut component =
if c.is_negative { (-val) } else { val }.to_integer();
if !val.is_in_lower_half() {
// Convert a signed finite field element into two's complement.
// a regular subtraction would underflow, so we do this.
component =
((T::Integer::MAX - T::modulus()) + component) + 1.into()
};
component = component & c.bit_mask;
vars[c.variable] = T::from(component >> (c.exponent as usize));
if c.is_negative {
val += T::from(component);
} else {
val -= T::from(component);
}
}
} else {
for c in components {
let component = val.to_integer() & c.bit_mask;
vars[c.variable] = T::from(component >> (c.exponent as usize));
val -= T::from(component);
}
}
assert_eq!(val, 0.into());
let value = value.evaluate(&mut eval_stack, &vars[..]);
perform_bit_decomposition(&mut vars, components, *have_negative, value);
}
InterpreterAction::ReadCell(idx, c) => {
vars[*idx] = data
Expand Down Expand Up @@ -347,6 +322,38 @@ impl<T: FieldElement> EffectsInterpreter<T> {
}
}

fn perform_bit_decomposition<T: FieldElement>(
variables: &mut [T],
components: &[IndexedBitDecompositionComponent<T>],
have_negative: bool,
mut value: T,
) {
if have_negative {
for c in components {
let mut component = if c.is_negative { (-value) } else { value }.to_integer();
if component > (T::modulus() - 1.into()) >> 1 {
// Convert a signed finite field element into two's complement.
// a regular subtraction would underflow, so we do this.
component = (T::Integer::MAX - T::modulus() + 1.into()) + component;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
component = (T::Integer::MAX - T::modulus() + 1.into()) + component;
let abs_component = T::modulus() - component;
component = T::Integer::MAX - abs_component + 1.into();

This would be slightly clearer to me, but still pretty confusing.

Maybe this would also give the right result?

                let abs_component = T::modulus() - component;
                component = T::Integer::from(0) - abs_component;

Then we also don't need MAX. We could also require T::Integer to implement Neg.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, the problem is that T::Integer::from(0) - abs_component underflows and thus might panic.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added a comment.

};
component = component & c.bit_mask;
variables[c.variable] = T::from(component >> (c.exponent as usize));
if c.is_negative {
value += T::from(component);
} else {
value -= T::from(component);
}
}
} else {
for c in components {
let component = value.to_integer() & c.bit_mask;
variables[c.variable] = T::from(component >> (c.exponent as usize));
value -= T::from(component);
}
}
assert_eq!(value, 0.into());
}

impl<T: FieldElement> InterpreterAction<T> {
/// variable indexes written by the action
fn writes(&self) -> BTreeSet<usize> {
Expand Down Expand Up @@ -544,18 +551,26 @@ mod test {
use std::fs::read_to_string;

use super::EffectsInterpreter;
use crate::witgen::data_structures::{
finalizable_data::{CompactData, CompactDataRef},
mutable_state::MutableState,
};
use crate::witgen::global_constraints;
use crate::witgen::jit::block_machine_processor::BlockMachineProcessor;
use crate::witgen::jit::effect::{BitDecomposition, BitDecompositionComponent};
use crate::witgen::jit::interpreter::{
perform_bit_decomposition, IndexedBitDecompositionComponent,
};
use crate::witgen::jit::symbolic_expression::SymbolicExpression;
use crate::witgen::jit::test_util::read_pil;
use crate::witgen::jit::variable::Variable;
use crate::witgen::machines::{
machine_extractor::MachineExtractor, KnownMachine, LookupCell, Machine,
};
use crate::witgen::FixedData;
use crate::witgen::{
data_structures::{
finalizable_data::{CompactData, CompactDataRef},
mutable_state::MutableState,
},
jit::effect::Effect,
};

use bit_vec::BitVec;
use itertools::Itertools;
Expand Down Expand Up @@ -651,4 +666,38 @@ mod test {
]
)
}

#[test]
fn bit_decomposition_goldilocks() {
let mut variables = [GoldilocksField::default(); 2];
let components = vec![
IndexedBitDecompositionComponent {
variable: 0,
is_negative: true,
exponent: 0,
bit_mask: From::from(0xffu32),
},
IndexedBitDecompositionComponent {
variable: 1,
is_negative: false,
exponent: 8,
bit_mask: From::from(0xff00u32),
},
];
perform_bit_decomposition(&mut variables, &components, true, 0x1ff.into());
assert_eq!(
&variables,
&[GoldilocksField::from(1), GoldilocksField::from(2)]
);
perform_bit_decomposition(
&mut variables,
&components,
true,
-(GoldilocksField::from(7)),
);
assert_eq!(
&variables,
&[GoldilocksField::from(7), GoldilocksField::from(0)]
);
}
}