Solve bit decomposition with negative coefficients. #2554

chriseth · 2025-03-14T17:40:29Z

No description provided.

chriseth · 2025-03-14T17:41:48Z

executor/src/witgen/jit/block_machine_processor.rs

+            "\
+S::Y[0] = params[0];
+S::Z[0] = params[1];
+S::X[0] = (-(S::Y[0] + -S::Z[0]) & 0xff);


This looks kind of correct. The only issue is that we have to ensure that the & 0xff is done on the two's complement representation. Maybe we should have a special operation for that.

chriseth · 2025-03-14T17:44:34Z

executor/src/witgen/jit/block_machine_processor.rs

+S::Z[0] = params[1];
+S::X[0] = (-(S::Y[0] + -S::Z[0]) & 0xff);
+S::carry[0] = -((-(S::Y[0] + -S::Z[0]) & 0x100) // 256);
+assert (-(S::Y[0] + -S::Z[0]) & 0xfffffffffffffe00) == 0;


On the other hand, if we use two's complement, then this won't work.

chriseth · 2025-03-18T13:56:18Z

Ok I think this is working. What is still missing:

interpreter (will do in separate PR)
test with negative target value

chriseth · 2025-03-18T14:08:14Z

executor/src/witgen/jit/affine_symbolic_expression.rs

                if r.complete {
                    r
                } else {
                    let negated = -self;
-                    let r = negated.solve_bit_decomposition()?;


The negated version is now covered already by the non-negated check.

chriseth · 2025-03-18T14:09:51Z

executor/src/witgen/jit/affine_symbolic_expression.rs

@@ -280,18 +284,20 @@ impl<T: FieldElement, V: Ord + Clone + Display> AffineSymbolicExpression<T, V> {
        // We need to assert that the masks cover "-offset",
        // otherwise the equation is not solvable.
        // We assert -offset & !masks == 0
+
+        // TODO can this be done even with negative coefficients?


I think if offset.to_integer() & !covered_bits != 0.into(), then we certainly have a failure, but we still have to do runtime checks (which we do). But please double-check.

What if offset is negative?

For example, if we had the constraint -1 = bit0 - 2 * bit1, then I think the covered bits would be 0b11 (because we ignore the signs), but we'd have offset.to_integer() == 0xffff0000 (for Goldilocks), so the check would fail?

Yeah that's the point. So I think I would change this check to only handle the old case where there are no negative coefficients. The rest has to be handled at run time.

georgwiese

Looks cool!

I think it's nice to have an effect for these decompositions.

I think bases other than two could make sense for constraint systems that anyway have a higher degree bound: Instead of bits, we could have limbs in basis 3, for example, range-constrained as limb * (limb - 1) * (limb - 2) = 0. But I think the BitDecomposition effect could be renamed and modified to accommodate for that if needed?

I'm still meditating over what exactly it means to have decomposition with negative coefficients. My current understanding is that it is mainly useful to represent negative numbers, i.e. do something like value = byte0 + 2**8 * byte1 - is_negative * 2**16 (where is_negative is bit-constrained). I wonder if we still need to distinguish whether we have negative coefficients, as we currently do when compiling to Rust?

executor/src/witgen/jit/effect.rs

georgwiese · 2025-03-19T14:00:51Z

executor/src/witgen/jit/effect.rs

+    /// The exponent of two, which forms the coefficient of the variable.
+    pub exponent: u64,
+    /// The bit mask for this component, relative to the value to be decomposed,
+    /// i.e. already scaled by the coefficient.


I'd find this more intuitive if this was the mask before scaling, and I don't see a disadvantage to that!

You mean if this was the mask of the range constraint of the variable?

Hm, I started changing, but it's quite substantial because then we need to shift first and apply the bit mask afterwards. This means we need a signed shift, if I see it correctly.

jit-compiler/src/includes/field_generic_up_to_64.rs

georgwiese · 2025-03-19T14:49:26Z

executor/src/witgen/jit/compiler.rs

+    value: &SymbolicExpression<T, Variable>,
+    components: &[BitDecompositionComponent<T, Variable>],
+) -> String {
+    let mut result = format!("let bit_decomp_value = {};\n", format_expression(value));


Hmm, so one effect compiles to 2 + 3 * <num components> Rust statements. I guess the reason that's not a function is so that we can unroll the loop and select the bitand variant at compile time? Then maybe at least we can add a comment in front of this block (like what format_code outputs)?

I mean we don't group things in functions anywhere (except the prover functions, which are functions to begin with...).

Yeah, but I think we should :) That would produce more readable code (both the code generating the Rust code and the generated Rust code) and I think it would be more friendly to the compiler? But this shouldn't block this PR.

executor/src/witgen/jit/witgen_inference.rs

executor/src/witgen/jit/compiler.rs

georgwiese · 2025-03-19T16:22:43Z

executor/src/witgen/jit/compiler.rs

+    let signed = if components.iter().any(|c| c.is_negative) {
+        "signed"
+    } else {
+        "unsigned"
+    };


Wouldn't we be able to always use the signed version?

With this, solving v = byte0 + 256 * byte1 and -v = -byte0 - 256 * byte1 would result in different code, but the constraints are equivalent.

Why do we still need the unsigned version? I think it doesn't matter as long as we don't get near $(p - 1) / 2$?

Yes, but the signed version is much more expensive.

I see! Please add a comment that that's why :) Wasn't obvious to me, but makes sense.

executor/src/witgen/jit/affine_symbolic_expression.rs

georgwiese · 2025-03-19T16:48:31Z

executor/src/witgen/jit/affine_symbolic_expression.rs

@@ -280,18 +284,20 @@ impl<T: FieldElement, V: Ord + Clone + Display> AffineSymbolicExpression<T, V> {
        // We need to assert that the masks cover "-offset",
        // otherwise the equation is not solvable.
        // We assert -offset & !masks == 0
+
+        // TODO can this be done even with negative coefficients?


What if offset is negative?

For example, if we had the constraint -1 = bit0 - 2 * bit1, then I think the covered bits would be 0b11 (because we ignore the signs), but we'd have offset.to_integer() == 0xffff0000 (for Goldilocks), so the check would fail?

chriseth · 2025-03-20T08:34:19Z

I wonder if we still need to distinguish whether we have negative coefficients, as we currently do when compiling to Rust?

This is just an optimization, the code should be equivalent.

chriseth · 2025-03-20T08:38:14Z

executor/src/witgen/jit/affine_symbolic_expression.rs

-            if (-offset).to_integer() & !covered_bits != 0.into() {
-                return Err(Error::ConflictingRangeConstraints);
+        if !components.iter().any(|c| c.is_negative) {
+            // If all coefficients are positive and the offset is known, we can check


I mean if the offset is a known number, we can actually determine that in all cases, but the ones with negative coefficients are more complicated...

Oh, if the offset is a known constant, we could just "run" the algorithm and make all the components known constants as well. Let's do that if we need it.

Co-authored-by: Georg Wiese <[email protected]>

This reverts commit 0906258.

…on_with_negative_numbers

chriseth commented Mar 14, 2025

View reviewed changes

chriseth added 2 commits March 17, 2025 14:02

Solve bit decomposition with negative coefficients.

5f9c452

Make bit decomposition its own effect.

bf43c73

chriseth force-pushed the solve_bit_decomposition_with_negative_numbers branch from 1c1ca8e to bf43c73 Compare March 17, 2025 14:26

chriseth added 6 commits March 17, 2025 14:46

fixes

99558c2

Remove negative case since this is now also covered.

f4f8a28

Update test expectations.

f5fe3f5

Implement missing functions.

1a378c3

Codegen for bit decomposition.

fcc5190

clippy

7b4780e

chriseth commented Mar 18, 2025

View reviewed changes

chriseth added 3 commits March 18, 2025 14:29

Test with negative value.

94a8cc4

Use shift instead of division.

44bdd08

Fix typo.

d2980dd

georgwiese reviewed Mar 19, 2025

View reviewed changes

Cover check.

589963b

chriseth commented Mar 20, 2025

View reviewed changes

chriseth and others added 9 commits March 20, 2025 09:44

Update executor/src/witgen/jit/compiler.rs

977f106

Co-authored-by: Georg Wiese <[email protected]>

Review.

14647d1

Remove bitand_signed_negated.

2e87944

debugging

0906258

Add comment.

1059fa6

Make all variables to be assigned in the branch mutable.

5cf50ee

Revert "debugging"

00750c8

This reverts commit 0906258.

remove debug

f71190c

Fix expectation.

d398c25

Merge remote-tracking branch 'origin/main' into solve_bit_decompositi…

85a3a4d

…on_with_negative_numbers

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Solve bit decomposition with negative coefficients. #2554

Solve bit decomposition with negative coefficients. #2554

chriseth commented Mar 14, 2025

chriseth Mar 14, 2025

chriseth Mar 14, 2025

chriseth commented Mar 18, 2025 •

edited

Loading

chriseth Mar 18, 2025

chriseth Mar 18, 2025

georgwiese Mar 19, 2025

chriseth Mar 20, 2025

georgwiese left a comment

georgwiese Mar 19, 2025

chriseth Mar 20, 2025

georgwiese Mar 20, 2025

chriseth Mar 20, 2025

georgwiese Mar 19, 2025

chriseth Mar 20, 2025

georgwiese Mar 20, 2025

georgwiese Mar 19, 2025

chriseth Mar 20, 2025

georgwiese Mar 20, 2025

georgwiese Mar 19, 2025

chriseth commented Mar 20, 2025

chriseth Mar 20, 2025

chriseth Mar 20, 2025

Solve bit decomposition with negative coefficients. #2554

Are you sure you want to change the base?

Solve bit decomposition with negative coefficients. #2554

Conversation

chriseth commented Mar 14, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chriseth commented Mar 18, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

georgwiese left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chriseth commented Mar 20, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chriseth commented Mar 18, 2025 •

edited

Loading