Function to increment pointer by one word in small fields. #1933

lvella · 2024-10-21T14:44:35Z

Extracted from poseidon_bb, but can be used in poseidon2_bb, sha256bb, keccak16...

std/machines/small_field/pointer_arith.asm

It is most likely too complex for witgen to figure out going backwards.

chriseth · 2024-10-21T14:50:17Z

std/machines/small_field/pointer_arith.asm

@@ -0,0 +1,38 @@
+/// Increments a pointer by one full 32-bit word.


Both this comment and the name of the function: it returns a constraint that forces a difference of one, it does not really increment it. This might be minor and it might also be more complicated to describe, but I was really wondering if this is a prover function that computes a witness, or if it adds/creates a constraint.

On one hand, I agree this is a bi-directional set of constraints, on the other hand, I doubt I can use this function to decrement instead of increment, as it would be too hard for witgen to solve.

Do you have a suggestion for a better name?

I fixed the comment.

I ran the Gröbner Basis, and going on the opposite direction from post_low = 0, I get that I can either get pre_low = 0xfffc with overflow (the correct answer) or pre_low = -4 with no overflow (makes sense, but is forbidden by the invisible pre-condition that pre_low is in range [0, 0xfffc]).

std/machines/small_field/pointer_arith.asm

chriseth · 2024-10-22T13:16:46Z

std/machines/hash/poseidon_bb.asm

+    // Increment the address in every row but the ones it is set.
+    std::array::map(
+        word_increment_ptr(high_addr, low_addr, high_addr', low_addr'),
+        |c| std::constraints::make_conditional(c, (1 - is_addr_set'))


Now I regret putting the condition as second parameter. Maybe we can change that in a future PR.
(because it doesn't fit the "if_else")

chriseth · 2024-10-22T13:19:04Z

std/machines/small_field/pointer_arith.asm

@@ -0,0 +1,35 @@
+/// Creates constraints that increments a pointer by one full 32-bit word.


Suggested change

/// Creates constraints that increments a pointer by one full 32-bit word.

/// Creates constraints that increments a pointer.

(you always increment by the abstract "one" which doesn't have a size, only the pointer has a size)

Oh wait, it increments them by the size of a word?

I increment by 4.

Could be an argument.

std/machines/small_field/pointer_arith.asm

chriseth · 2024-10-22T13:26:15Z

std/machines/small_field/pointer_arith.asm

+let word_increment_ptr: expr, expr, expr, expr -> Constr[] = constr |pre_high, pre_low, post_high, post_low| {
+    // How far away from overflowing the low limb is:
+    let low_diff = pre_low - (0x10000 - 4);
+    // Is one if low limb is about to overflow:


I still don't understand what "about to overflow" means and what the two constraints in lines 20 and 24 do exactly.

"about to overflow" in a sense that in the next step, the low limb will be set to zero and the carry will be added to the high limb.

About lines 20;24-26, it can be seen as an is_not_zero function (could be extracted, if useful somewhere else):

let is_not_zero = constr |value| { // Assumes the inverse of "value" if it is not zero, otherwise undefined. let inverse; // Ensures that inverse * value is either 0 or 1: (inverse * value - 1) * value = 0; inverse * value };

I placed this is_not_zero in utils, and changed is_zero implementation to use it (because it is simpler). Now I am running the tests to see if it will break anything, since it returns a degree 2 expression.

Renamed low_overflow to carry, so its role is more recognizable.

std/machines/small_field/pointer_arith.asm

chriseth · 2024-10-22T13:30:38Z

std/machines/small_field/pointer_arith.asm

+    // Helper to allow low_overflow to be boolean
+    let low_diff_inv;
+
+    low_overflow = 1 - low_diff_inv * low_diff;


The constraints here ensure that low_overflow is 1 if and only if low_diff is zero, otherwise it is 0, right? Should we also extract that into a helper function? Then we can use it for XIsZero.

Yes. Just found utils::is_zero(). Will fix.

onurinanc · 2024-10-22T14:13:53Z

std/machines/hash/poseidon_bb.asm

-    ) = 0;
-    // Set high limb, incremented if low overflowed:
-    (1 - is_addr_set') * (high_addr' - high_addr - low_overflow) = 0;
+    // Increment the address in every row but the ones it is set.


pol commit low_addr[16]; pol commit high_addr[16]; std::utils::fold(16, |i| { let constr_array = word_increment_ptr(high_addr[i], low_addr[i], high_addr[i]', low_addr[i]'); std::array::map(constr_array, |c| std::constraints::make_conditional(c, used)) }, [], |acc, constr_arr| acc + constr_arr);

It's nicely working like this so that we can increment address without overflow

Looks a bit off. Didn't you mean:

let constr_array = word_increment_ptr(high_addr[i], low_addr[i], high_addr[i + 1], low_addr[i + 1]);

?

Co-authored-by: chriseth <[email protected]>

leonardoalt · 2024-10-25T07:12:16Z

Has conflicts.
@chriseth ?

lvella · 2024-10-25T13:11:10Z

Has conflicts.

Fixed.

chriseth · 2024-10-28T13:51:39Z

std/machines/small_field/pointer_arith.asm

@@ -0,0 +1,38 @@
+/// Creates constraints that increments a pointer by amount.
+///


Should we document that post_high does not wrap around?

OK, it's actually obivous from the constraints in the docstring below.

std/machines/small_field/pointer_arith.asm

chriseth · 2024-10-28T13:52:51Z

std/machines/small_field/pointer_arith.asm

+/// - pre_low must be in range [0, 0xffff].
+///
+/// The pointers are given in 2 16-bit limbs. This function returns a set of constraints
+/// ensuring that the following are equal:


Should we also say something about the range of the post limbs?

Should we? I don't think it is needed.

I think the description as 2 16-bit limbs makes it clear.

I'll add a precondition that the arithmetic should not overflow u32::MAX.

std/utils.asm

chriseth · 2024-10-28T13:55:43Z

std/utils.asm

+    let inverse;
+
+    // Ensures that "inverse * x" is either 0 or 1:
+    (inverse * x - 1) * x = 0;


Is this a degree-3 constraint? Is that fine for our backends?

The degree is 3 only if x is degree 1.

The final degree is, of course, 2*deg(x) + 1.

IIRC, 3 is the target degree we support. It works on plonky3.

Also, it seems very wrong that the user has to worry about this. It feels that the breakup of compatible polynomials should be a compilation step, possibly dependent on the constraints of the backend.

Create an issue about this, but I admit the thoughts in there are convoluted and needs refining: #1971

Co-authored-by: chriseth <[email protected]>

georgwiese · 2024-10-29T16:55:29Z

std/machines/small_field/pointer_arith.asm

+| {
+    // Is the low limb at its maximum value?
+    let carry;
+    carry = std::utils::is_zero(pre_low - (0x10000 - amount));


Cool!

I would have done

force_bool(carry); pre_low + amount = carry * 2**16 + post_low; post_high = pre_high + carry;

Needs one less column (no need to store the inverse created in is_zero), but would assume post_low and post_high to be range-constrained! Adding two range constraints would typically be more expensive, so I like this solution more.

Function to increment pointer by one word in small fields.

7e31100

lvella requested a review from onurinanc October 21, 2024 14:44

chriseth reviewed Oct 21, 2024

View reviewed changes

std/machines/small_field/pointer_arith.asm Outdated Show resolved Hide resolved

Removed the comment saying it can be used in reverse direction.

3b80b5b

It is most likely too complex for witgen to figure out going backwards.

chriseth reviewed Oct 21, 2024

View reviewed changes

std/machines/small_field/pointer_arith.asm Outdated Show resolved Hide resolved

lvella added 3 commits October 21, 2024 16:02

Returning constraints instead of expr.

44912f0

Using if_else.

deb2d67

Typo.

3cac288

lvella requested a review from chriseth October 21, 2024 17:09

chriseth reviewed Oct 22, 2024

View reviewed changes

std/machines/small_field/pointer_arith.asm Outdated Show resolved Hide resolved

chriseth reviewed Oct 22, 2024

View reviewed changes

std/machines/small_field/pointer_arith.asm Outdated Show resolved Hide resolved

chriseth reviewed Oct 22, 2024

View reviewed changes

std/machines/small_field/pointer_arith.asm Outdated Show resolved Hide resolved

chriseth reviewed Oct 22, 2024

View reviewed changes

onurinanc reviewed Oct 22, 2024

View reviewed changes

lvella and others added 7 commits October 22, 2024 16:49

Improved explanation.

290228c

Co-authored-by: chriseth <[email protected]>

Improving comments even more.

b44218b

Prettier constraint.

9aa7c17

Co-authored-by: chriseth <[email protected]>

Introduced utils::is_not_zero and simplified utils::is_zero.

8452c50

Merge branch 'incr_addr' of github.com:powdr-labs/powdr into incr_addr

b91742e

Adjusting for the higher degree.

8f90735

Comments and readability.

c07164a

lvella requested a review from chriseth October 23, 2024 13:55

lvella mentioned this pull request Oct 23, 2024

Precompile for Poseidon2 BabyBear #1807

Merged

Merge branch 'main' into incr_addr

14f6bdd

Making the increment amount an argument.

024154d

chriseth reviewed Oct 28, 2024

View reviewed changes

std/machines/small_field/pointer_arith.asm Outdated Show resolved Hide resolved

chriseth reviewed Oct 28, 2024

View reviewed changes

std/utils.asm Outdated Show resolved Hide resolved

chriseth reviewed Oct 28, 2024

View reviewed changes

lvella and others added 2 commits October 28, 2024 14:01

Update std/machines/small_field/pointer_arith.asm

9157714

Co-authored-by: chriseth <[email protected]>

Update std/utils.asm

a4fe19c

Co-authored-by: chriseth <[email protected]>

lvella requested a review from chriseth October 28, 2024 15:03

lvella added 4 commits October 28, 2024 15:19

Improved description.

c161bee

Improved description.

8aa6535

Improved description.

81ee5ff

Merge branch 'incr_addr' of github.com:powdr-labs/powdr into incr_addr

cfac592

chriseth approved these changes Oct 29, 2024

View reviewed changes

chriseth added this pull request to the merge queue Oct 29, 2024

leonardoalt mentioned this pull request Oct 29, 2024

Plonky3 keccak memory #1832

Merged

Merged via the queue into main with commit 60219b2 Oct 29, 2024
14 checks passed

chriseth deleted the incr_addr branch October 29, 2024 12:45

georgwiese reviewed Oct 29, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Function to increment pointer by one word in small fields. #1933

Function to increment pointer by one word in small fields. #1933

lvella commented Oct 21, 2024

chriseth Oct 21, 2024

lvella Oct 21, 2024 •

edited

Loading

lvella Oct 21, 2024

lvella Oct 21, 2024

chriseth Oct 22, 2024 •

edited

Loading

chriseth Oct 22, 2024

chriseth Oct 22, 2024

lvella Oct 22, 2024

chriseth Oct 22, 2024

lvella Oct 22, 2024

lvella Oct 22, 2024 •

edited

Loading

lvella Oct 22, 2024

lvella Oct 22, 2024

chriseth Oct 22, 2024

lvella Oct 22, 2024 •

edited

Loading

lvella Oct 22, 2024

onurinanc Oct 22, 2024

lvella Oct 22, 2024 •

edited

Loading

leonardoalt commented Oct 25, 2024

lvella commented Oct 25, 2024 •

edited

Loading

chriseth Oct 28, 2024

chriseth Oct 28, 2024

chriseth Oct 28, 2024

lvella Oct 28, 2024

chriseth Oct 28, 2024

lvella Oct 28, 2024

lvella Oct 29, 2024

georgwiese Oct 29, 2024

		@@ -0,0 +1,38 @@
		/// Increments a pointer by one full 32-bit word.

		@@ -0,0 +1,35 @@
		/// Creates constraints that increments a pointer by one full 32-bit word.

Function to increment pointer by one word in small fields. #1933

Function to increment pointer by one word in small fields. #1933

Conversation

lvella commented Oct 21, 2024

Choose a reason for hiding this comment

lvella Oct 21, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chriseth Oct 22, 2024 • 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lvella Oct 22, 2024 • 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

lvella Oct 22, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lvella Oct 22, 2024 • edited Loading

Choose a reason for hiding this comment

leonardoalt commented Oct 25, 2024

lvella commented Oct 25, 2024 • 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

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

lvella Oct 21, 2024 •

edited

Loading

chriseth Oct 22, 2024 •

edited

Loading

lvella Oct 22, 2024 •

edited

Loading

lvella Oct 22, 2024 •

edited

Loading

lvella Oct 22, 2024 •

edited

Loading

lvella commented Oct 25, 2024 •

edited

Loading