Skip to content

perf: speed up Nat.powMod kernel reduction - #15167

Draft
kim-em wants to merge 4 commits into
masterfrom
perf-nat-powmod-kernel
Draft

perf: speed up Nat.powMod kernel reduction#15167
kim-em wants to merge 4 commits into
masterfrom
perf-nat-powmod-kernel

Conversation

@kim-em

@kim-em kim-em commented Sep 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

This PR speeds up kernel evaluation of Nat.powMod, preserving its GMP runtime implementation and public theorem statements.

Use four-bit windows through 512-bit moduli and three-bit windows through 1024 bits. Above that, reduced bases below 2^64 use two-bit windows through 4096-bit moduli, then one-bit windows for exponents of at least 2^64. Other inputs retain the binary accumulator. Every path is proved correct, including modulus zero.

Kernel-check medians for b^(m-1) mod m, with m = 2^bits - 19 and b = 2 (the large-base row uses b = m/3):

Bits Upstream (ms) PrimeCert-style (ms) This PR (ms) Path
31 1.260 0.182 0.093 4-bit
61 1.759 0.366 0.110 4-bit
127 3.774 0.799 0.214 4-bit
255 7.608 1.621 0.450 4-bit
512 15.326 3.306 1.132 4-bit
1024 34.318 7.448 3.110 3-bit
2048 — 18.872 9.882 2-bit
4096 — 62.196 38.489 2-bit
8192 — 644.152 169.015 1-bit
8192, large base — 262.585 262.037 binary

“PrimeCert-style” is the accumulator adapted from Bhavik Mehta's powModK; these are modular-power timings, not complete primality certificates. Four adjacent AB/BA blocks per comparison retain all 1,216 samples. This PR's column uses upstream-paired samples through 1024 bits and PrimeCert-paired samples above; — means unmeasured. Reproduction and upstream samples; PrimeCert-style samples.

The base-dependent choice avoids the large-base regressions of unconditional windows. On additional irregular moduli through 12288 bits, long sparse exponents can favor binary by about 15%; short-exponent dispatch costs can add tens of microseconds. Boundary, module-import, and large-exponent kernel tests cover the new paths; benchmarks include the binary fallback.

Closes #15166. Follow-up to #13490.

🤖 Implemented with Codex assistance.

@kim-em kim-em added the changelog-library Library label Sep 15, 2026
@kim-em
kim-em marked this pull request as draft September 15, 2026 09:07
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 15, 2026
@kim-em

kim-em commented Sep 15, 2026

Copy link
Copy Markdown
Collaborator Author

Implementation: 4865d81 (all 4,215 tests and the full build pass locally).

Base-aware tuning: PrimeCert-style comparison. All completed samples are retained (four adjacent AB/BA blocks, CPU 7 on chungus2). Each call uses a fresh kernel checker after draining asynchronous work; expected values use the GMP runtime outside the timer. These are kernel modular-power measurements.

Patterns 0–7 respectively use (base, exponent): (2,m-1), (m/3,2^bits), (m/3,65537), (m/3,(2^bits-1)/3), (m/3,m-1), (2,2^bits), (17,(2^bits-1)/3), (2,65537). Every modulus is m=2^bits-19. Separate matched-base and irregular-modulus experiments motivated the dispatch; the large-modulus small-base path trades some sparse-exponent speed for faster dense and mixed powers. A full density-counting selector added enough kernel work to reject it.

All raw samples, nanoseconds 
block,bits,pattern,pair,arm,kernel_ns
0,31,0,1,primeCertLoop,177764
0,31,0,1,Nat.powMod,64105
0,31,1,1,primeCertLoop,166417
0,31,1,1,Nat.powMod,63725
0,31,2,1,primeCertLoop,97525
0,31,2,1,Nat.powMod,44596
0,31,3,1,primeCertLoop,160558
0,31,3,1,Nat.powMod,60279
0,31,4,1,primeCertLoop,175009
0,31,4,1,Nat.powMod,60861
0,31,5,1,primeCertLoop,167047
0,31,5,1,Nat.powMod,59929
0,31,6,1,primeCertLoop,161520
0,31,6,1,Nat.powMod,59478
0,31,7,1,primeCertLoop,97404
0,31,7,1,Nat.powMod,44486
0,61,0,1,primeCertLoop,350940
0,61,0,1,Nat.powMod,105637
0,61,1,1,primeCertLoop,323229
0,61,1,1,Nat.powMod,103393
0,61,2,1,primeCertLoop,101941
0,61,2,1,Nat.powMod,46259
0,61,3,1,primeCertLoop,331892
0,61,3,1,Nat.powMod,100939
0,61,4,1,primeCertLoop,353083
0,61,4,1,Nat.powMod,108661
0,61,5,1,primeCertLoop,322137
0,61,5,1,Nat.powMod,103753
0,61,6,1,primeCertLoop,332553
0,61,6,1,Nat.powMod,101841
0,61,7,1,primeCertLoop,100099
0,61,7,1,Nat.powMod,45437
0,127,0,1,primeCertLoop,784072
0,127,0,1,Nat.powMod,207448
0,127,1,1,primeCertLoop,712046
0,127,1,1,Nat.powMod,201659
0,127,2,1,primeCertLoop,107819
0,127,2,1,Nat.powMod,48682
0,127,3,1,primeCertLoop,740838
0,127,3,1,Nat.powMod,221678
0,127,4,1,primeCertLoop,781879
0,127,4,1,Nat.powMod,227928
0,127,5,1,primeCertLoop,709461
0,127,5,1,Nat.powMod,203452
0,127,6,1,primeCertLoop,738414
0,127,6,1,Nat.powMod,203571
0,127,7,1,primeCertLoop,102412
0,127,7,1,Nat.powMod,47130
0,255,0,1,primeCertLoop,1622024
0,255,0,1,Nat.powMod,437638
0,255,1,1,primeCertLoop,1437481
0,255,1,1,Nat.powMod,432080
0,255,2,1,primeCertLoop,105136
0,255,2,1,Nat.powMod,56364
0,255,3,1,primeCertLoop,1490650
0,255,3,1,Nat.powMod,526300
0,255,4,1,primeCertLoop,1559101
0,255,4,1,Nat.powMod,574271
0,255,5,1,primeCertLoop,1518961
0,255,5,1,Nat.powMod,440302
0,255,6,1,primeCertLoop,1498821
0,255,6,1,Nat.powMod,437659
0,255,7,1,primeCertLoop,105717
0,255,7,1,Nat.powMod,47691
0,511,0,1,primeCertLoop,3391356
0,511,0,1,Nat.powMod,1119780
0,511,1,1,primeCertLoop,2998554
0,511,1,1,Nat.powMod,1108783
0,511,2,1,primeCertLoop,110804
0,511,2,1,Nat.powMod,62923
0,511,3,1,primeCertLoop,3132814
0,511,3,1,Nat.powMod,1697686
0,511,4,1,primeCertLoop,3360601
0,511,4,1,Nat.powMod,2008226
0,511,5,1,primeCertLoop,2970633
0,511,5,1,Nat.powMod,1104708
0,511,6,1,primeCertLoop,3136108
0,511,6,1,Nat.powMod,1122243
0,511,7,1,primeCertLoop,107129
0,511,7,1,Nat.powMod,49393
0,512,0,1,primeCertLoop,3294072
0,512,0,1,Nat.powMod,1117336
0,512,1,1,primeCertLoop,2957483
0,512,1,1,Nat.powMod,1111637
0,512,2,1,primeCertLoop,111856
0,512,2,1,Nat.powMod,62944
0,512,3,1,primeCertLoop,3104111
0,512,3,1,Nat.powMod,1437691
0,512,4,1,primeCertLoop,3317007
0,512,4,1,Nat.powMod,1979824
0,512,5,1,primeCertLoop,2965184
0,512,5,1,Nat.powMod,1105528
0,512,6,1,primeCertLoop,3109519
0,512,6,1,Nat.powMod,1114331
0,512,7,1,primeCertLoop,106668
0,512,7,1,Nat.powMod,49012
0,521,0,1,primeCertLoop,3435642
0,521,0,1,Nat.powMod,1167961
0,521,1,1,primeCertLoop,3149829
0,521,1,1,Nat.powMod,1176303
0,521,2,1,primeCertLoop,111725
0,521,2,1,Nat.powMod,60540
0,521,3,1,primeCertLoop,3219732
0,521,3,1,Nat.powMod,1392553
0,521,4,1,primeCertLoop,3420951
0,521,4,1,Nat.powMod,1576436
0,521,5,1,primeCertLoop,3043300
0,521,5,1,Nat.powMod,1159258
0,521,6,1,primeCertLoop,3214925
0,521,6,1,Nat.powMod,1159408
0,521,7,1,primeCertLoop,107720
0,521,7,1,Nat.powMod,54030
0,1024,0,1,primeCertLoop,7437834
0,1024,0,1,Nat.powMod,3072865
0,1024,1,1,primeCertLoop,6259778
0,1024,1,1,Nat.powMod,3279661
0,1024,2,1,primeCertLoop,116122
0,1024,2,1,Nat.powMod,74420
0,1024,3,1,primeCertLoop,6841651
0,1024,3,1,Nat.powMod,4290709
0,1024,4,1,primeCertLoop,7384204
0,1024,4,1,Nat.powMod,6337113
0,1024,5,1,primeCertLoop,6681473
0,1024,5,1,Nat.powMod,3140034
0,1024,6,1,primeCertLoop,6909541
0,1024,6,1,Nat.powMod,3084882
0,1024,7,1,primeCertLoop,108121
0,1024,7,1,Nat.powMod,53599
0,2048,0,1,primeCertLoop,19031296
0,2048,0,1,Nat.powMod,9857149
0,2048,1,1,primeCertLoop,14335988
0,2048,1,1,Nat.powMod,14271241
0,2048,2,1,primeCertLoop,141680
0,2048,2,1,Nat.powMod,135911
0,2048,3,1,primeCertLoop,16094864
0,2048,3,1,Nat.powMod,16275232
0,2048,4,1,primeCertLoop,17943815
0,2048,4,1,Nat.powMod,17982022
0,2048,5,1,primeCertLoop,14278923
0,2048,5,1,Nat.powMod,9771894
0,2048,6,1,primeCertLoop,16399937
0,2048,6,1,Nat.powMod,10195401
0,2048,7,1,primeCertLoop,143402
0,2048,7,1,Nat.powMod,83574
0,4096,0,1,primeCertLoop,63358945
0,4096,0,1,Nat.powMod,37920142
0,4096,1,1,primeCertLoop,40436351
0,4096,1,1,Nat.powMod,39764566
0,4096,2,1,primeCertLoop,229640
0,4096,2,1,Nat.powMod,188379
0,4096,3,1,primeCertLoop,48637396
0,4096,3,1,Nat.powMod,50914962
0,4096,4,1,primeCertLoop,59895893
0,4096,4,1,Nat.powMod,58319026
0,4096,5,1,primeCertLoop,40328091
0,4096,5,1,Nat.powMod,42941524
0,4096,6,1,primeCertLoop,52759296
0,4096,6,1,Nat.powMod,47331561
0,4096,7,1,primeCertLoop,253315
0,4096,7,1,Nat.powMod,104595
0,8192,0,1,primeCertLoop,643389670
0,8192,0,1,Nat.powMod,165096943
0,8192,1,1,primeCertLoop,157406725
0,8192,1,1,Nat.powMod,156437268
0,8192,2,1,primeCertLoop,469587
0,8192,2,1,Nat.powMod,353154
0,8192,3,1,primeCertLoop,205112872
0,8192,3,1,Nat.powMod,205905126
0,8192,4,1,primeCertLoop,263568660
0,8192,4,1,Nat.powMod,258648097
0,8192,5,1,primeCertLoop,409957315
0,8192,5,1,Nat.powMod,168988391
0,8192,6,1,primeCertLoop,208564617
0,8192,6,1,Nat.powMod,168349955
0,8192,7,1,primeCertLoop,251863
0,8192,7,1,Nat.powMod,147148
1,31,0,1,Nat.powMod,84625
1,31,0,1,primeCertLoop,181128
1,31,1,1,Nat.powMod,70294
1,31,1,1,primeCertLoop,166367
1,31,2,1,Nat.powMod,51236
1,31,2,1,primeCertLoop,97525
1,31,3,1,Nat.powMod,67851
1,31,3,1,primeCertLoop,163292
1,31,4,1,Nat.powMod,71906
1,31,4,1,primeCertLoop,171364
1,31,5,1,Nat.powMod,66108
1,31,5,1,primeCertLoop,164424
1,31,6,1,Nat.powMod,66809
1,31,6,1,primeCertLoop,164524
1,31,7,1,Nat.powMod,49373
1,31,7,1,primeCertLoop,96543
1,61,0,1,Nat.powMod,116533
1,61,0,1,primeCertLoop,373604
1,61,1,1,Nat.powMod,113719
1,61,1,1,primeCertLoop,334255
1,61,2,1,Nat.powMod,53089
1,61,2,1,primeCertLoop,102391
1,61,3,1,Nat.powMod,109683
1,61,3,1,primeCertLoop,335998
1,61,4,1,Nat.powMod,118545
1,61,4,1,primeCertLoop,355137
1,61,5,1,Nat.powMod,109873
1,61,5,1,primeCertLoop,323880
1,61,6,1,Nat.powMod,106007
1,61,6,1,primeCertLoop,328897
1,61,7,1,Nat.powMod,51977
1,61,7,1,primeCertLoop,99337
1,127,0,1,Nat.powMod,228649
1,127,0,1,primeCertLoop,804262
1,127,1,1,Nat.powMod,212375
1,127,1,1,primeCertLoop,714479
1,127,2,1,Nat.powMod,63795
1,127,2,1,primeCertLoop,105587
1,127,3,1,Nat.powMod,235950
1,127,3,1,primeCertLoop,744103
1,127,4,1,Nat.powMod,244403
1,127,4,1,primeCertLoop,785584
1,127,5,1,Nat.powMod,215630
1,127,5,1,primeCertLoop,707699
1,127,6,1,Nat.powMod,213967
1,127,6,1,primeCertLoop,737343
1,127,7,1,Nat.powMod,55212
1,127,7,1,primeCertLoop,102743
1,255,0,1,Nat.powMod,455816
1,255,0,1,primeCertLoop,1619650
1,255,1,1,Nat.powMod,433032
1,255,1,1,primeCertLoop,1442658
1,255,2,1,Nat.powMod,60049
1,255,2,1,primeCertLoop,104154
1,255,3,1,Nat.powMod,558638
1,255,3,1,primeCertLoop,1502126
1,255,4,1,Nat.powMod,599409
1,255,4,1,primeCertLoop,1570437
1,255,5,1,Nat.powMod,446441
1,255,5,1,primeCertLoop,1439143
1,255,6,1,Nat.powMod,442506
1,255,6,1,primeCertLoop,1490048
1,255,7,1,Nat.powMod,68482
1,255,7,1,primeCertLoop,105846
1,511,0,1,Nat.powMod,1140380
1,511,0,1,primeCertLoop,3378608
1,511,1,1,Nat.powMod,1132849
1,511,1,1,primeCertLoop,2963192
1,511,2,1,Nat.powMod,72428
1,511,2,1,primeCertLoop,108391
1,511,3,1,Nat.powMod,1706720
1,511,3,1,primeCertLoop,3113085
1,511,4,1,Nat.powMod,2014676
1,511,4,1,primeCertLoop,3287203
1,511,5,1,Nat.powMod,1131096
1,511,5,1,primeCertLoop,2938956
1,511,6,1,Nat.powMod,1146019
1,511,6,1,primeCertLoop,3114206
1,511,7,1,Nat.powMod,62393
1,511,7,1,primeCertLoop,106057
1,512,0,1,Nat.powMod,1144807
1,512,0,1,primeCertLoop,3300933
1,512,1,1,Nat.powMod,1126159
1,512,1,1,primeCertLoop,2952426
1,512,2,1,Nat.powMod,70084
1,512,2,1,primeCertLoop,108901
1,512,3,1,Nat.powMod,1456228
1,512,3,1,primeCertLoop,3107937
1,512,4,1,Nat.powMod,1976199
1,512,4,1,primeCertLoop,3298208
1,512,5,1,Nat.powMod,1118989
1,512,5,1,primeCertLoop,2932907
1,512,6,1,Nat.powMod,1180199
1,512,6,1,primeCertLoop,3476873
1,512,7,1,Nat.powMod,62142
1,512,7,1,primeCertLoop,111776
1,521,0,1,Nat.powMod,1200269
1,521,0,1,primeCertLoop,3458025
1,521,1,1,Nat.powMod,1199398
1,521,1,1,primeCertLoop,3074377
1,521,2,1,Nat.powMod,70384
1,521,2,1,primeCertLoop,114340
1,521,3,1,Nat.powMod,1413585
1,521,3,1,primeCertLoop,3237929
1,521,4,1,Nat.powMod,1617368
1,521,4,1,primeCertLoop,3411686
1,521,5,1,Nat.powMod,1175773
1,521,5,1,primeCertLoop,3072814
1,521,6,1,Nat.powMod,1185406
1,521,6,1,primeCertLoop,3219102
1,521,7,1,Nat.powMod,67039
1,521,7,1,primeCertLoop,107360
1,1024,0,1,Nat.powMod,3076940
1,1024,0,1,primeCertLoop,7420097
1,1024,1,1,Nat.powMod,3088157
1,1024,1,1,primeCertLoop,6262472
1,1024,2,1,Nat.powMod,83634
1,1024,2,1,primeCertLoop,113819
1,1024,3,1,Nat.powMod,4521511
1,1024,3,1,primeCertLoop,7341811
1,1024,4,1,Nat.powMod,5541053
1,1024,4,1,primeCertLoop,7512545
1,1024,5,1,Nat.powMod,3071893
1,1024,5,1,primeCertLoop,6237815
1,1024,6,1,Nat.powMod,3079014
1,1024,6,1,primeCertLoop,6716584
1,1024,7,1,Nat.powMod,63073
1,1024,7,1,primeCertLoop,105146
1,2048,0,1,Nat.powMod,9899512
1,2048,0,1,primeCertLoop,18338390
1,2048,1,1,Nat.powMod,14186116
1,2048,1,1,primeCertLoop,14196762
1,2048,2,1,Nat.powMod,150523
1,2048,2,1,primeCertLoop,123263
1,2048,3,1,Nat.powMod,16048146
1,2048,3,1,primeCertLoop,16023499
1,2048,4,1,Nat.powMod,17909394
1,2048,4,1,primeCertLoop,17845609
1,2048,5,1,Nat.powMod,9757732
1,2048,5,1,primeCertLoop,14348526
1,2048,6,1,Nat.powMod,9835117
1,2048,6,1,primeCertLoop,16147192
1,2048,7,1,Nat.powMod,91846
1,2048,7,1,primeCertLoop,109032
1,4096,0,1,Nat.powMod,41803087
1,4096,0,1,primeCertLoop,61356037
1,4096,1,1,Nat.powMod,41059385
1,4096,1,1,primeCertLoop,40944274
1,4096,2,1,Nat.powMod,285383
1,4096,2,1,primeCertLoop,179907
1,4096,3,1,Nat.powMod,55399810
1,4096,3,1,primeCertLoop,50107365
1,4096,4,1,Nat.powMod,58051329
1,4096,4,1,primeCertLoop,58183375
1,4096,5,1,Nat.powMod,40586915
1,4096,5,1,primeCertLoop,42168638
1,4096,6,1,Nat.powMod,37711983
1,4096,6,1,primeCertLoop,49253259
1,4096,7,1,Nat.powMod,128370
1,4096,7,1,primeCertLoop,120349
1,8192,0,1,Nat.powMod,168959989
1,8192,0,1,primeCertLoop,629743624
1,8192,1,1,Nat.powMod,153165399
1,8192,1,1,primeCertLoop,152874658
1,8192,2,1,Nat.powMod,444980
1,8192,2,1,primeCertLoop,324471
1,8192,3,1,Nat.powMod,204167220
1,8192,3,1,primeCertLoop,215826420
1,8192,4,1,Nat.powMod,261938223
1,8192,4,1,primeCertLoop,260072989
1,8192,5,1,Nat.powMod,174244331
1,8192,5,1,primeCertLoop,412824194
1,8192,6,1,Nat.powMod,169914664
1,8192,6,1,primeCertLoop,214172980
1,8192,7,1,Nat.powMod,311722
1,8192,7,1,primeCertLoop,143843
2,31,0,1,primeCertLoop,182731
2,31,0,1,Nat.powMod,63734
2,31,1,1,primeCertLoop,167379
2,31,1,1,Nat.powMod,62092
2,31,2,1,primeCertLoop,97775
2,31,2,1,Nat.powMod,44867
2,31,3,1,primeCertLoop,164013
2,31,3,1,Nat.powMod,60189
2,31,4,1,primeCertLoop,180328
2,31,4,1,Nat.powMod,61451
2,31,5,1,primeCertLoop,164944
2,31,5,1,Nat.powMod,58517
2,31,6,1,primeCertLoop,162410
2,31,6,1,Nat.powMod,59578
2,31,7,1,primeCertLoop,98275
2,31,7,1,Nat.powMod,45297
2,61,0,1,primeCertLoop,365051
2,61,0,1,Nat.powMod,106909
2,61,1,1,primeCertLoop,326063
2,61,1,1,Nat.powMod,102051
2,61,2,1,primeCertLoop,102502
2,61,2,1,Nat.powMod,46118
2,61,3,1,primeCertLoop,335738
2,61,3,1,Nat.powMod,103764
2,61,4,1,primeCertLoop,358381
2,61,4,1,Nat.powMod,110974
2,61,5,1,primeCertLoop,324400
2,61,5,1,Nat.powMod,106978
2,61,6,1,primeCertLoop,354796
2,61,6,1,Nat.powMod,100710
2,61,7,1,primeCertLoop,101160
2,61,7,1,Nat.powMod,45638
2,127,0,1,primeCertLoop,793285
2,127,0,1,Nat.powMod,209821
2,127,1,1,primeCertLoop,731004
2,127,1,1,Nat.powMod,210432
2,127,2,1,primeCertLoop,105666
2,127,2,1,Nat.powMod,49002
2,127,3,1,primeCertLoop,743271
2,127,3,1,Nat.powMod,227937
2,127,4,1,primeCertLoop,790742
2,127,4,1,Nat.powMod,230922
2,127,5,1,primeCertLoop,723753
2,127,5,1,Nat.powMod,203221
2,127,6,1,primeCertLoop,740568
2,127,6,1,Nat.powMod,205875
2,127,7,1,primeCertLoop,103143
2,127,7,1,Nat.powMod,47040
2,255,0,1,primeCertLoop,1612029
2,255,0,1,Nat.powMod,443006
2,255,1,1,primeCertLoop,1448677
2,255,1,1,Nat.powMod,427274
2,255,2,1,primeCertLoop,106468
2,255,2,1,Nat.powMod,51997
2,255,3,1,primeCertLoop,1544058
2,255,3,1,Nat.powMod,547762
2,255,4,1,primeCertLoop,1611949
2,255,4,1,Nat.powMod,586619
2,255,5,1,primeCertLoop,1451792
2,255,5,1,Nat.powMod,439581
2,255,6,1,primeCertLoop,1508826
2,255,6,1,Nat.powMod,445341
2,255,7,1,primeCertLoop,106388
2,255,7,1,Nat.powMod,48201
2,511,0,1,primeCertLoop,3463834
2,511,0,1,Nat.powMod,1112820
2,511,1,1,primeCertLoop,3049470
2,511,1,1,Nat.powMod,1117967
2,511,2,1,primeCertLoop,110644
2,511,2,1,Nat.powMod,62533
2,511,3,1,primeCertLoop,3164480
2,511,3,1,Nat.powMod,1691517
2,511,4,1,primeCertLoop,3343476
2,511,4,1,Nat.powMod,2017570
2,511,5,1,primeCertLoop,2975480
2,511,5,1,Nat.powMod,1109594
2,511,6,1,primeCertLoop,3129919
2,511,6,1,Nat.powMod,1127291
2,511,7,1,primeCertLoop,106919
2,511,7,1,Nat.powMod,54772
2,512,0,1,primeCertLoop,3317777
2,512,0,1,Nat.powMod,1119679
2,512,1,1,primeCertLoop,2988079
2,512,1,1,Nat.powMod,1102655
2,512,2,1,primeCertLoop,110784
2,512,2,1,Nat.powMod,62262
2,512,3,1,primeCertLoop,3175337
2,512,3,1,Nat.powMod,1441106
2,512,4,1,primeCertLoop,3332099
2,512,4,1,Nat.powMod,1967626
2,512,5,1,primeCertLoop,2981188
2,512,5,1,Nat.powMod,1106590
2,512,6,1,primeCertLoop,3151972
2,512,6,1,Nat.powMod,1116305
2,512,7,1,primeCertLoop,105947
2,512,7,1,Nat.powMod,50736
2,521,0,1,primeCertLoop,3456503
2,521,0,1,Nat.powMod,1191847
2,521,1,1,primeCertLoop,3071833
2,521,1,1,Nat.powMod,1169103
2,521,2,1,primeCertLoop,109813
2,521,2,1,Nat.powMod,59538
2,521,3,1,primeCertLoop,3318759
2,521,3,1,Nat.powMod,1401307
2,521,4,1,primeCertLoop,3472036
2,521,4,1,Nat.powMod,1669615
2,521,5,1,primeCertLoop,3093575
2,521,5,1,Nat.powMod,1153249
2,521,6,1,primeCertLoop,3237729
2,521,6,1,Nat.powMod,1349209
2,521,7,1,primeCertLoop,107609
2,521,7,1,Nat.powMod,53880
2,1024,0,1,primeCertLoop,7458755
2,1024,0,1,Nat.powMod,3077171
2,1024,1,1,primeCertLoop,6295450
2,1024,1,1,Nat.powMod,3070681
2,1024,2,1,primeCertLoop,115882
2,1024,2,1,Nat.powMod,73970
2,1024,3,1,primeCertLoop,6813719
2,1024,3,1,Nat.powMod,4302617
2,1024,4,1,primeCertLoop,7387149
2,1024,4,1,Nat.powMod,5436798
2,1024,5,1,primeCertLoop,6266678
2,1024,5,1,Nat.powMod,3068728
2,1024,6,1,primeCertLoop,7011802
2,1024,6,1,Nat.powMod,3092784
2,1024,7,1,primeCertLoop,106878
2,1024,7,1,Nat.powMod,53269
2,2048,0,1,primeCertLoop,18728137
2,2048,0,1,Nat.powMod,9864370
2,2048,1,1,primeCertLoop,15220889
2,2048,1,1,Nat.powMod,15011810
2,2048,2,1,primeCertLoop,193486
2,2048,2,1,Nat.powMod,147028
2,2048,3,1,primeCertLoop,16480045
2,2048,3,1,Nat.powMod,16572863
2,2048,4,1,primeCertLoop,18211051
2,2048,4,1,Nat.powMod,18048670
2,2048,5,1,primeCertLoop,14285923
2,2048,5,1,Nat.powMod,9813124
2,2048,6,1,primeCertLoop,16129766
2,2048,6,1,Nat.powMod,9823079
2,2048,7,1,primeCertLoop,117874
2,2048,7,1,Nat.powMod,77605
2,4096,0,1,primeCertLoop,60149438
2,4096,0,1,Nat.powMod,38260827
2,4096,1,1,primeCertLoop,40772089
2,4096,1,1,Nat.powMod,40161754
2,4096,2,1,primeCertLoop,207668
2,4096,2,1,Nat.powMod,182941
2,4096,3,1,primeCertLoop,49022558
2,4096,3,1,Nat.powMod,53832607
2,4096,4,1,primeCertLoop,59684119
2,4096,4,1,Nat.powMod,58378424
2,4096,5,1,primeCertLoop,43785275
2,4096,5,1,Nat.powMod,42449495
2,4096,6,1,primeCertLoop,52362988
2,4096,6,1,Nat.powMod,37698443
2,4096,7,1,primeCertLoop,154629
2,4096,7,1,Nat.powMod,83313
2,8192,0,1,primeCertLoop,648764677
2,8192,0,1,Nat.powMod,169069401
2,8192,1,1,primeCertLoop,159635028
2,8192,1,1,Nat.powMod,161530838
2,8192,2,1,primeCertLoop,459831
2,8192,2,1,Nat.powMod,396738
2,8192,3,1,primeCertLoop,209569167
2,8192,3,1,Nat.powMod,209975249
2,8192,4,1,primeCertLoop,262111350
2,8192,4,1,Nat.powMod,262136548
2,8192,5,1,primeCertLoop,410380694
2,8192,5,1,Nat.powMod,168946109
2,8192,6,1,primeCertLoop,210474849
2,8192,6,1,Nat.powMod,169941393
2,8192,7,1,primeCertLoop,231543
2,8192,7,1,Nat.powMod,146637
3,31,0,1,Nat.powMod,87540
3,31,0,1,primeCertLoop,182460
3,31,1,1,Nat.powMod,69744
3,31,1,1,primeCertLoop,166226
3,31,2,1,Nat.powMod,50925
3,31,2,1,primeCertLoop,98055
3,31,3,1,Nat.powMod,69133
3,31,3,1,primeCertLoop,162421
3,31,4,1,Nat.powMod,69063
3,31,4,1,primeCertLoop,172997
3,31,5,1,Nat.powMod,70104
3,31,5,1,primeCertLoop,163663
3,31,6,1,Nat.powMod,66929
3,31,6,1,primeCertLoop,161610
3,31,7,1,Nat.powMod,48832
3,31,7,1,primeCertLoop,100328
3,61,0,1,Nat.powMod,116713
3,61,0,1,primeCertLoop,367796
3,61,1,1,Nat.powMod,112397
3,61,1,1,primeCertLoop,325793
3,61,2,1,Nat.powMod,52218
3,61,2,1,primeCertLoop,101771
3,61,3,1,Nat.powMod,111204
3,61,3,1,primeCertLoop,333874
3,61,4,1,Nat.powMod,118326
3,61,4,1,primeCertLoop,355928
3,61,5,1,Nat.powMod,111946
3,61,5,1,primeCertLoop,328547
3,61,6,1,Nat.powMod,107149
3,61,6,1,primeCertLoop,340094
3,61,7,1,Nat.powMod,52097
3,61,7,1,primeCertLoop,101711
3,127,0,1,Nat.powMod,229470
3,127,0,1,primeCertLoop,806155
3,127,1,1,Nat.powMod,218193
3,127,1,1,primeCertLoop,728580
3,127,2,1,Nat.powMod,57195
3,127,2,1,primeCertLoop,103744
3,127,3,1,Nat.powMod,238043
3,127,3,1,primeCertLoop,740518
3,127,4,1,Nat.powMod,247246
3,127,4,1,primeCertLoop,781098
3,127,5,1,Nat.powMod,218063
3,127,5,1,primeCertLoop,761388
3,127,6,1,Nat.powMod,217512
3,127,6,1,primeCertLoop,731335
3,127,7,1,Nat.powMod,54741
3,127,7,1,primeCertLoop,103223
3,255,0,1,Nat.powMod,450358
3,255,0,1,primeCertLoop,1660832
3,255,1,1,Nat.powMod,438320
3,255,1,1,primeCertLoop,1443229
3,255,2,1,Nat.powMod,61171
3,255,2,1,primeCertLoop,117033
3,255,3,1,Nat.powMod,539489
3,255,3,1,primeCertLoop,1500704
3,255,4,1,Nat.powMod,608441
3,255,4,1,primeCertLoop,1587483
3,255,5,1,Nat.powMod,435616
3,255,5,1,primeCertLoop,1430821
3,255,6,1,Nat.powMod,456016
3,255,6,1,primeCertLoop,1500404
3,255,7,1,Nat.powMod,66919
3,255,7,1,primeCertLoop,105146
3,511,0,1,Nat.powMod,1155693
3,511,0,1,primeCertLoop,3430204
3,511,1,1,Nat.powMod,1132929
3,511,1,1,primeCertLoop,2972506
3,511,2,1,Nat.powMod,72468
3,511,2,1,primeCertLoop,109773
3,511,3,1,Nat.powMod,1724366
3,511,3,1,primeCertLoop,3144321
3,511,4,1,Nat.powMod,2032493
3,511,4,1,primeCertLoop,3320501
3,511,5,1,Nat.powMod,1127882
3,511,5,1,primeCertLoop,2985595
3,511,6,1,Nat.powMod,1142203
3,511,6,1,primeCertLoop,3119273
3,511,7,1,Nat.powMod,59468
3,511,7,1,primeCertLoop,104655
3,512,0,1,Nat.powMod,1135794
3,512,0,1,primeCertLoop,3310858
3,512,1,1,Nat.powMod,1138838
3,512,1,1,primeCertLoop,2964234
3,512,2,1,Nat.powMod,72087
3,512,2,1,primeCertLoop,108981
3,512,3,1,Nat.powMod,1463429
3,512,3,1,primeCertLoop,3118312
3,512,4,1,Nat.powMod,2026433
3,512,4,1,primeCertLoop,3317307
3,512,5,1,Nat.powMod,1128633
3,512,5,1,primeCertLoop,2974318
3,512,6,1,Nat.powMod,1132069
3,512,6,1,primeCertLoop,3103810
3,512,7,1,Nat.powMod,59068
3,512,7,1,primeCertLoop,104244
3,521,0,1,Nat.powMod,1196193
3,521,0,1,primeCertLoop,3492166
3,521,1,1,Nat.powMod,1176714
3,521,1,1,primeCertLoop,3045965
3,521,2,1,Nat.powMod,69624
3,521,2,1,primeCertLoop,111275
3,521,3,1,Nat.powMod,1405713
3,521,3,1,primeCertLoop,3230839
3,521,4,1,Nat.powMod,1601383
3,521,4,1,primeCertLoop,3490834
3,521,5,1,Nat.powMod,1178376
3,521,5,1,primeCertLoop,3046526
3,521,6,1,Nat.powMod,1207330
3,521,6,1,primeCertLoop,3245641
3,521,7,1,Nat.powMod,67199
3,521,7,1,primeCertLoop,106949
3,1024,0,1,Nat.powMod,3137530
3,1024,0,1,primeCertLoop,7530682
3,1024,1,1,Nat.powMod,3112483
3,1024,1,1,primeCertLoop,6424792
3,1024,2,1,Nat.powMod,85006
3,1024,2,1,primeCertLoop,115822
3,1024,3,1,Nat.powMod,4355786
3,1024,3,1,primeCertLoop,6911834
3,1024,4,1,Nat.powMod,5482496
3,1024,4,1,primeCertLoop,7395782
3,1024,5,1,Nat.powMod,3064492
3,1024,5,1,primeCertLoop,6309211
3,1024,6,1,Nat.powMod,3153995
3,1024,6,1,primeCertLoop,7202134
3,1024,7,1,Nat.powMod,65527
3,1024,7,1,primeCertLoop,106979
3,2048,0,1,Nat.powMod,10040822
3,2048,0,1,primeCertLoop,19014923
3,2048,1,1,Nat.powMod,14667819
3,2048,1,1,primeCertLoop,14488484
3,2048,2,1,Nat.powMod,157544
3,2048,2,1,primeCertLoop,131195
3,2048,3,1,Nat.powMod,16300048
3,2048,3,1,primeCertLoop,16137198
3,2048,4,1,Nat.powMod,18293934
3,2048,4,1,primeCertLoop,18255006
3,2048,5,1,Nat.powMod,9862347
3,2048,5,1,primeCertLoop,14430748
3,2048,6,1,Nat.powMod,9914134
3,2048,6,1,primeCertLoop,16333218
3,2048,7,1,Nat.powMod,93588
3,2048,7,1,primeCertLoop,109613
3,4096,0,1,Nat.powMod,38717675
3,4096,0,1,primeCertLoop,63035486
3,4096,1,1,Nat.powMod,42362145
3,4096,1,1,primeCertLoop,43613621
3,4096,2,1,Nat.powMod,291362
3,4096,2,1,primeCertLoop,210592
3,4096,3,1,Nat.powMod,53123436
3,4096,3,1,primeCertLoop,52078426
3,4096,4,1,Nat.powMod,61000100
3,4096,4,1,primeCertLoop,61583254
3,4096,5,1,Nat.powMod,39063106
3,4096,5,1,primeCertLoop,42115951
3,4096,6,1,Nat.powMod,38609323
3,4096,6,1,primeCertLoop,51679915
3,4096,7,1,Nat.powMod,135901
3,4096,7,1,primeCertLoop,127689
3,8192,0,1,Nat.powMod,178479999
3,8192,0,1,primeCertLoop,644913429
3,8192,1,1,Nat.powMod,155061420
3,8192,1,1,primeCertLoop,165635993
3,8192,2,1,Nat.powMod,505409
3,8192,2,1,primeCertLoop,344270
3,8192,3,1,Nat.powMod,211111813
3,8192,3,1,primeCertLoop,205945607
3,8192,4,1,Nat.powMod,262747254
3,8192,4,1,primeCertLoop,263058074
3,8192,5,1,Nat.powMod,168690630
3,8192,5,1,primeCertLoop,414367943
3,8192,6,1,Nat.powMod,167795714
3,8192,6,1,primeCertLoop,213541174
3,8192,7,1,Nat.powMod,301226
3,8192,7,1,primeCertLoop,151985

@kim-em kim-em mentioned this pull request Sep 15, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

perf: reduce Nat.powMod kernel replay cost

1 participant

@kim-em