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

Division check for arith component #181

Merged
merged 18 commits into from
Dec 11, 2024
Merged

Division check for arith component #181

merged 18 commits into from
Dec 11, 2024

Conversation

hecmas
Copy link
Contributor

@hecmas hecmas commented Nov 29, 2024

This PR adds the constraint to the arith component where a division check is performed:

// Check that remainder (d) is lower than divisor (b) when division is performed
// Specifically, we ensure that 0 <= |d| < |b|
lookup_assumes(operation_bus_id, [debug_main_step,
                                      (1 - nr) * (1 - nb) * LTU_OP + nr * (1 - nb) * LT_ABS_NP_OP + (1 - nr) * nb * LT_ABS_PN_OP + nr * nb * GT_OP,
                                      (d[0] + CHUNK_SIZE * d[1]), (d[2] + CHUNK_SIZE * d[3]) + m32 * nr * 0xFFFFFFFF, // remainder
                                      (b[0] + CHUNK_SIZE * b[1]), (b[2] + CHUNK_SIZE * b[3]) + m32 * nb * 0xFFFFFFFF, // divisor
                                      1, 0, 
                                      1], sel: div * (1 - div_by_zero));

For this, we needed to implement three new binary operations:

  • LT_ABS_NP_OP: Checks that the first input, assumed to be negative, is strictly lower than the second input, assumed to be positive, in absolute value.
  • LT_ABS_PN_OP: Checks that the first input, assumed to be positive, is strictly lower than the second input, assumed to be negative, in absolute value.
  • GT_OP: Check that the first input is strictly bigger than the second input.

Adding these binary operations incurred in doubling the size of the binary table, so that all possible combinations regarding them are included in the table.

@hecmas hecmas requested a review from zkronos73 November 29, 2024 18:11
@cla-bot cla-bot bot added the cla-signed label Nov 29, 2024
hecmas and others added 3 commits November 29, 2024 18:50
* Custom cols rom (#159)

Custom cols working

---------

Co-authored-by: Xavier Pinsach <[email protected]>

* Cached custom commits

* Updating proofman to 0.0.12

* Cargo fmt

* Cargo fmt

* Fix cargo clippy

* Rom trace is now deterministic

* cargo fmt

* Global constraints verifying again

* Optimizing the binary component (#167)

* Optimizing the binary

* Updating the executor

* Updating to 0.0.13

* Not creating unnecessary instances of arith tables

* Pil2-proofman 0.0.14

---------

Co-authored-by: Xavier Pinsach <[email protected]>
Co-authored-by: Héctor Masip Ardevol <[email protected]>
@hecmas hecmas self-assigned this Dec 3, 2024
@hecmas hecmas changed the base branch from develop to update_proofman December 9, 2024 17:59
@hecmas hecmas marked this pull request as ready for review December 10, 2024 15:53
@hecmas hecmas changed the title LT ABS Division check for arith component Dec 10, 2024
@hecmas hecmas changed the base branch from update_proofman to develop-v0.1.0 December 11, 2024 11:24
@hecmas hecmas merged commit 80192db into develop-v0.1.0 Dec 11, 2024
5 checks passed
@hecmas hecmas mentioned this pull request Dec 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants