Skip to content

ExtrOcamlZBigInt: Use shifts/masks to build and match positive values#281

Open
cpitclaudel wants to merge 1 commit into
rocq-prover:masterfrom
cpitclaudel:cpc/positive-shift
Open

ExtrOcamlZBigInt: Use shifts/masks to build and match positive values#281
cpitclaudel wants to merge 1 commit into
rocq-prover:masterfrom
cpitclaudel:cpc/positive-shift

Conversation

@cpitclaudel

@cpitclaudel cpitclaudel commented Jun 21, 2026

Copy link
Copy Markdown
Contributor

This is particularly valuable for FMapPositive and other structures like stdpp's Pmap that walk a binary number's encoding, because walks can now be done without general-purpose division.

Micro-benchmark on OCaml 5.2.1+flambda:

  Name                              Time/Run     mWd/Run
  FMapPositive.find x100k (stock)    88.04ms   17_403_012w
  FMapPositive.find x100k (is_odd)   57.32ms            6w

@cpitclaudel

Copy link
Copy Markdown
Contributor Author

I guess we could change other definitions as well:

Extract Constant Z.div_eucl => "(fun x y ->
    if Z.equal y Z.zero then (Z.zero, x)
    else let q = Z.fdiv x y in (q, Z.sub x (Z.mul y q)))".
  Extract Constant Z.div => "(fun x y ->
    if Z.equal y Z.zero then Z.zero else Z.fdiv x y)".
  Extract Constant Z.modulo => "(fun x y ->
    if Z.equal y Z.zero then x else Z.sub x (Z.mul y (Z.fdiv x y)))".

Micro-benchmarks suggest that these are 1.3-1.7x faster and use 3x less memory.

@cpitclaudel cpitclaudel force-pushed the cpc/positive-shift branch 3 times, most recently from d268b35 to 05ecd70 Compare June 23, 2026 20:38
This is particularly valuable for FMapPositive and other structures like stdpp's
Pmap that walk a binary number's encoding, because walks can now be done without
general-purpose division.

Micro-benchmark on OCaml 5.2.1+flambda:

  Name                                 Time/Run     mWd/Run
  FMapPositive.find x100k (stock)       88.04ms   17_403_012w
  FMapPositive.find x100k (shift+mask)  57.32ms            6w
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant