Skip to content

Instantly share code, notes, and snippets.

@kim-em

kim-em/248-KernelBench.lean

Last active September 16, 2026 05:59
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save kim-em/c308db93be8966f18bc2b68c1daddecf to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save kim-em/c308db93be8966f18bc2b68c1daddecf to your computer and use it in GitHub Desktop.
Download ZIP
Proved whole-integer Nat.popcount: standalone kernel and native performance evidence
Raw
248-kernel-record.json
{
"cpu": 73,
"host": "chungus2",
"load_before": [
10.35205078125,
9.05517578125,
9.0205078125
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_swar_bench.lean"
],
"original_runtime": null,
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_swar_bench.lean\n",
"load_after": [
10.00341796875,
9.00439453125,
9.00390625
]
}
Raw
248-kernel-samples.csv
0 64 false count64 count64 43925
0 64 false count64 current 31257
0 64 false count128 count128 27861
0 64 false count128 current 23955
0 64 false chunks chunks 45026
0 64 false chunks current 23134
0 64 true count64 count64 26970
0 64 true count64 current 23986
0 64 true count128 count128 26759
0 64 true count128 current 22974
0 64 true chunks chunks 40560
0 64 true chunks current 22132
0 256 false count64 count64 61391
0 256 false count64 current 33019
0 256 false count128 count128 38857
0 256 false count128 current 31447
0 256 false chunks chunks 80049
0 256 false chunks current 31486
0 256 true count64 count64 59488
0 256 true count64 current 34751
0 256 true count128 count128 40169
0 256 true count128 current 32608
0 256 true chunks chunks 88291
0 256 true chunks current 48022
0 4096 false count64 count64 694200
0 4096 false count64 current 168380
0 4096 false count128 count128 340365
0 4096 false count128 current 165996
0 4096 false chunks chunks 890510
0 4096 false chunks current 166958
0 4096 true count64 count64 693709
0 4096 true count64 current 196542
0 4096 true count128 count128 381096
0 4096 true count128 current 185935
0 4096 true chunks chunks 941136
0 4096 true chunks current 186396
0 65536 false count64 count64 12192017
0 65536 false count64 current 2787834
0 65536 false count128 count128 5955300
0 65536 false count128 current 2788074
0 65536 false chunks chunks 15359554
0 65536 false chunks current 2805460
0 65536 true count64 count64 12695844
0 65536 true count64 current 3276147
0 65536 true count128 count128 6854063
0 65536 true count128 current 3275086
0 65536 true chunks chunks 16229534
0 65536 true chunks current 3338240
1 64 false count64 current 34581
1 64 false count64 count64 35433
1 64 false count128 current 27361
1 64 false count128 count128 30004
1 64 false chunks current 24296
1 64 false chunks chunks 56664
1 64 true count64 current 27722
1 64 true count64 count64 28843
1 64 true count128 current 23705
1 64 true count128 count128 28963
1 64 true chunks current 22874
1 64 true chunks chunks 47130
1 256 false count64 current 37085
1 256 false count64 count64 61792
1 256 false count128 current 33860
1 256 false count128 count128 42223
1 256 false chunks current 32297
1 256 false chunks chunks 90525
1 256 true count64 current 37665
1 256 true count64 count64 63815
1 256 true count128 current 34531
1 256 true count128 count128 45247
1 256 true chunks current 33910
1 256 true chunks chunks 89873
1 4096 false count64 current 178325
1 4096 false count64 count64 654731
1 4096 false count128 current 178755
1 4096 false count128 count128 358231
1 4096 false chunks current 171144
1 4096 false chunks chunks 908327
1 4096 true count64 current 205515
1 4096 true count64 count64 711465
1 4096 true count128 current 198975
1 4096 true count128 count128 398661
1 4096 true chunks current 194768
1 4096 true chunks chunks 962828
1 65536 false count64 current 2803938
1 65536 false count64 count64 11882839
1 65536 false count128 current 2825129
1 65536 false count128 count128 5978554
1 65536 false chunks current 2810668
1 65536 false chunks chunks 15494084
1 65536 true count64 current 3317869
1 65536 true count64 count64 12796865
1 65536 true count128 current 3327925
1 65536 true count128 count128 6883126
1 65536 true chunks current 3301696
1 65536 true chunks chunks 16309913
2 64 false count64 count64 40701
2 64 false count64 current 36103
2 64 false count128 count128 32138
2 64 false count128 current 26159
2 64 false chunks chunks 57285
2 64 false chunks current 26139
2 64 true count64 count64 29354
2 64 true count64 current 25758
2 64 true count128 count128 27871
2 64 true count128 current 23455
2 64 true chunks chunks 46730
2 64 true chunks current 23304
2 256 false count64 count64 62142
2 256 false count64 current 37485
2 256 false count128 count128 44015
2 256 false count128 current 33630
2 256 false chunks chunks 89413
2 256 false chunks current 32829
2 256 true count64 count64 67460
2 256 true count64 current 38577
2 256 true count128 count128 42744
2 256 true count128 current 35042
2 256 true chunks chunks 89182
2 256 true chunks current 34050
2 4096 false count64 count64 653058
2 4096 false count64 current 184804
2 4096 false count128 count128 351621
2 4096 false count128 current 173477
2 4096 false chunks chunks 907646
2 4096 false chunks current 178925
2 4096 true count64 count64 797512
2 4096 true count64 current 311351
2 4096 true count128 count128 560622
2 4096 true count128 current 302249
2 4096 true chunks chunks 1359005
2 4096 true chunks current 308548
2 65536 false count64 count64 14170551
2 65536 false count64 current 2847452
2 65536 false count128 count128 5992445
2 65536 false count128 current 2832560
2 65536 false chunks chunks 15418301
2 65536 false chunks current 2827032
2 65536 true count64 count64 12702395
2 65536 true count64 current 3296978
2 65536 true count128 count128 6869576
2 65536 true count128 current 3296147
2 65536 true chunks chunks 16294872
2 65536 true chunks current 3288847
3 64 false count64 current 34471
3 64 false count64 count64 35613
3 64 false count128 current 26630
3 64 false count128 count128 29453
3 64 false chunks current 24015
3 64 false chunks chunks 58116
3 64 true count64 current 27851
3 64 true count64 count64 28592
3 64 true count128 current 23424
3 64 true count128 count128 27421
3 64 true chunks current 22583
3 64 true chunks chunks 46709
3 256 false count64 current 36835
3 256 false count64 count64 61812
3 256 false count128 current 33590
3 256 false count128 count128 44787
3 256 false chunks current 32238
3 256 false chunks chunks 90294
3 256 true count64 current 38377
3 256 true count64 count64 63444
3 256 true count128 current 34571
3 256 true count128 count128 42332
3 256 true chunks current 33269
3 256 true chunks chunks 89413
3 4096 false count64 current 176391
3 4096 false count64 count64 658166
3 4096 false count128 current 174478
3 4096 false count128 count128 358631
3 4096 false chunks current 174168
3 4096 false chunks chunks 902548
3 4096 true count64 current 209150
3 4096 true count64 count64 707109
3 4096 true count128 current 200607
3 4096 true count128 count128 393283
3 4096 true chunks current 191043
3 4096 true chunks chunks 956959
3 65536 false count64 current 2813733
3 65536 false count64 count64 11874567
3 65536 false count128 current 2820192
3 65536 false count128 count128 5955010
3 65536 false chunks current 2797588
3 65536 false chunks chunks 15394466
3 65536 true count64 current 3295055
3 65536 true count64 count64 12690918
3 65536 true count128 current 3296047
3 65536 true count128 count128 6848685
3 65536 true chunks current 3287164
3 65536 true chunks chunks 16256254
Raw
248-KernelBench.lean
module
import Lean
meta import Lean
/-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES.
The current API and alternative chunk widths count identical numeral inputs. -/
open Lean
@[expose] public def countBits (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + (n.testBit i).toNat)
-- Masked 64-bit parallel count, following Bhavik Mehta's PrimeCert #156.
@[expose] public def wordCount (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight (nat_lit 1)).land (nat_lit 0x5555555555555555))
let b := (a.land (nat_lit 0x3333333333333333)).add
((a.shiftRight (nat_lit 2)).land (nat_lit 0x3333333333333333))
let c := (b.add (b.shiftRight (nat_lit 4))).land (nat_lit 0x0f0f0f0f0f0f0f0f)
((c.mul (nat_lit 0x0101010101010101)).shiftRight (nat_lit 56)).land (nat_lit 0xff)
@[expose] public def chunkCount (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + wordCount ((n >>> (64*i)) &&& 0xffffffffffffffff))
@[expose] public def word64 (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight 1).land 6148914691236517205)
let b := (a.land 3689348814741910323).add ((a.shiftRight 2).land 3689348814741910323)
let c := (b.add (b.shiftRight 4)).land 1085102592571150095
((c.mul 72340172838076673).shiftRight 56).land 255
@[expose] public noncomputable def loop64 : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 18446744073709551615).rec
((word64 (n.land 18446744073709551615)).add (rec (n.shiftRight 64)))
(word64 n))
@[expose] public noncomputable def count64 (n : Nat) : Nat := loop64 n.succ n
@[expose] public def word128 (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight 1).land 113427455640312821154458202477256070485)
let b := (a.land 68056473384187692692674921486353642291).add ((a.shiftRight 2).land 68056473384187692692674921486353642291)
let c := (b.add (b.shiftRight 4)).land 20016609818878733144904388672456953615
((c.mul 1334440654591915542993625911497130241).shiftRight 120).land 255
@[expose] public noncomputable def loop128 : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 340282366920938463463374607431768211455).rec
((word128 (n.land 340282366920938463463374607431768211455)).add (rec (n.shiftRight 128)))
(word128 n))
@[expose] public noncomputable def count128 (n : Nat) : Nat := loop128 n.succ n
run_cmd do
let some output ← IO.getEnv "POPCOUNT_SAMPLES" | return
let file ← IO.FS.Handle.mk output .write
let ready ← IO.mkRef (← getEnv).toKernelEnv
let env := Environment.ofKernelEnv (← ready.get)
for block in [:4] do
for width in [64, 256, 4096, 65536] do
for dense in [false, true] do
let n := if dense then 2^width-1 else 2^(width-1)+1
let expected := if dense then width else 2
let natE := mkConst ``Nat
let mkProof (arm : String) (value : Nat) :=
let lhs := if arm == "count64" then mkApp (mkConst ``count64) (mkRawNatLit n)
else if arm == "count128" then mkApp (mkConst ``count128) (mkRawNatLit n)
else if arm == "current" then mkApp (mkConst ``Nat.popcount) (mkRawNatLit n)
else if arm == "chunks" then
mkApp2 (mkConst ``chunkCount) (mkRawNatLit n) (mkRawNatLit ((width+63)/64))
else mkApp2 (mkConst ``countBits) (mkRawNatLit n) (mkRawNatLit width)
let rhs := mkRawNatLit value
let type := mkApp3 (mkConst ``Eq [.succ .zero]) natE lhs rhs
mkApp (mkLambda `h .default type (mkBVar 0))
(mkApp2 (mkConst ``Eq.refl [.succ .zero]) natE rhs)
for candidate in ["count64", "count128", "chunks"] do
for arm in (if block % 2 == 0 then [candidate, "current"] else ["current", candidate]) do
if block == 0 then
let bad ← IO.mkRef (Kernel.check env {} (mkProof arm (expected+1)))
if (← bad.get).isOk then throwError "wrong-result control accepted"
let input ← IO.mkRef (env, mkProof arm expected)
let (env, term) ← input.get
let start ← IO.monoNanosNow
let result ← IO.mkRef (Kernel.check env {} term)
let result ← result.get
let stop ← IO.monoNanosNow
let _ ← ofExceptKernelException result
file.putStrLn s!"{block},{width},{dense},{candidate},{arm},{stop-start}"
file.flush
Raw
248-README.md

Transparent Nat.popcount: kernel and compiled measurements

The implementation counts 248-bit chunks using existing kernel arithmetic and uses a native C++ limb scan when compiled. These benchmarks are standalone artifacts, outside the repository and CI.

After building the PR's Lean checkout with its documented build command:

python3 run.py --repo /path/to/lean4 --out /tmp/popcount-kernel --kind kernel
python3 run.py --repo /path/to/lean4 --out /tmp/popcount-native --kind native

The runner reserves an affinity CPU, uses Lean's test harness, records host load and all completed samples, and removes its temporary benchmark source. Native timings execute a C-compiled binary; interpreter execution is disabled.

Median microseconds for dense inputs:

Bits Kernel: 64-bit chunks Kernel: Nat.popcount Compiled: 64-bit chunks Compiled: Nat.popcount
64 46.72 23.44 0.489 0.059
256 89.30 34.66 1.947 0.061
4096 959.89 199.79 33.280 0.125
65536 16275.56 3296.10 932.516 1.225

The 64-bit word arithmetic is Bhavik Mehta's raw-Nat popc64K from PrimeCert #156. The reference extracts and masks each 64-bit chunk from a natural number. This measures that chunk-counting implementation, not the complete PrimeCert sieve or a primality proof.

The same kernel run compares the selected 248-bit loop with otherwise identical 64- and 128-bit loops:

Bits 64-bit loop 128-bit loop 248-bit loop
64 28.72 27.65 23.44
256 63.63 42.54 34.66
4096 709.29 395.97 199.79
65536 12699.12 6861.82 3296.10

All three use the same byte-counting operations. 248 bits is the largest multiple of eight whose bit count fits in one byte. The selected public function and the 248-bit prototype have identical reduction bodies.

Kernel samples time a fresh Kernel.check of an equality application. Literal input construction and expected-result calculation occur outside the timer. Every case rejects a wrong-result control before timing. Four blocks alternate adjacent AB/BA arms. current occurs once per comparison pair, so its reported median includes all 12 completed samples per input. Compiled samples time 100 checked calls per row; divide nanoseconds by 100 for per-call times. Sparse cases and a scalar 32-bit native case are included in the raw data. Host-specific timings include fixed checker/call overhead. Chunk extraction and structural-fuel reduction repeatedly copy big naturals; the kernel implementation does not have the native limb scan's linear complexity.

kernel-samples.csv and native-samples.csv contain every completed final-run sample; their matching records include the commands and host context. exploratory-samples.csv and exploratory-log.txt retain an earlier unpinned experiment with missing noncomputable annotations and its diagnostics; the tables above use only the successful final runs.

The division-* files retain the complete earlier run using division/modulo chunk extraction. The primary kernel files and tables use masks and shifts. Native code is identical in both versions; its completed run is retained without repetition.

Raw
README.md

Whole-integer Nat.popcount: kernel and compiled measurements

The proved implementation in Lean PR #15176 uses parallel masks and additions across the whole natural number, then sums the packed counts by a remainder operation. Its kernel reduction uses existing arithmetic primitives. Compiled calls use a C++ limb scan. The byte-counting proof adapts Bhavik Mehta’s PrimeCert work. This artifact is outside the repository and CI.

After building the PR checkout with its documented build command:

python3 run.py --repo /path/to/lean4 --out /tmp/popcount-kernel --kind kernel
python3 run.py --repo /path/to/lean4 --out /tmp/popcount-native --kind native

The runner reserves an affinity CPU, uses Lean’s test harness, records host load and every completed sample, and removes its temporary source. Native timings execute a C-compiled binary, with interpreter execution disabled. The current implementation commit is 8dc7a3fd59.

Dense medians in microseconds:

Bits Kernel: 64-bit chunk reference Kernel: Nat.popcount Compiled: 64-bit chunk reference Compiled: Nat.popcount
64 50.490 23.350 0.489 0.059
256 96.142 35.162 1.947 0.061
4096 1019.581 42.788 33.280 0.125
65536 20888.573 144.229 932.516 1.225

The reference uses Bhavik Mehta’s raw-Nat popc64K arithmetic from PrimeCert #156, extracting and masking 64-bit chunks. This is an arithmetic comparison, not a timing of the full PrimeCert sieve or primality checker. Native code is unchanged by the whole-integer revision, so its completed earlier samples are retained without rerunning it.

Small inputs use precomputed masks through 248 bits. Specialized paths cover 256/4096-bit inputs with 16-bit lanes and 65536-bit inputs with 32-bit lanes. A proved fallback doubles the width bound and combines lanes further as needed. Every lane holds at most the number of original bits it represents; the final modulus strictly exceeds the maximum total. Correctness is proved for arbitrary natural numbers, including the fallback.

Each kernel sample times a fresh Kernel.check of an equality application. Numeral construction and expected counts are outside the timer. Every case rejects a wrong-result control. Four blocks alternate adjacent AB/BA arms. current occurs once for each of three reference comparisons (12 samples/input); every reference has four. All sparse cases are retained. Native rows time 100 checked calls; divide their nanoseconds by 100 for per-call time. These are shared-host observations including checker/call overhead.

BroadBench.lean compares the prior 248-bit implementation with the current public implementation at intermediate sizes and through 1,048,576 bits. To reproduce it, copy it to KernelBench.lean in a separate copy of this artifact and use run.py --kind kernel. The corresponding broad-* files contain every sample and host context.

Retained earlier measurements: 248-* records the 248-bit implementation at 85a0d02447; pre-small-* records the whole-integer implementation before the precomputed small-input path; division-* records earlier division-based chunk extraction; exploratory-* retains the failed initial harness experiment. Older implementations require the matching checkout to reproduce their public-function arm. No completed samples were discarded.

Broad comparison, dense medians in µs:

Bits Previous 248-bit loop Current Nat.popcount
128 33.781 29.279
512 58.261 42.953
1024 76.644 37.551
2048 122.341 36.163
8192 421.836 66.474
16384 868.423 72.978
32768 1746.054 83.790
131072 8213.987 158.315
262144 19740.912 279.730
1048576 184446.505 880.821

The generic-* experiment compares generic lane folding (wide) with fixed-width specializations (special): dense kernel medians were 69.56 versus 40.90 µs at 4096 bits, and 150.22 versus 96.28 µs at 65536 bits. These exploratory sources require checkout 85a0d02447 for their retained chunk-reference helpers. Every completed sample is included. The specialized and generic arithmetic now share the general correctness proof.

Raw
broad-kernel-record.json
{
"cpu": 2,
"host": "chungus2",
"load_before": [
9.310546875,
13.80810546875,
10.62744140625
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_artifact.lean"
],
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_artifact.lean\n",
"load_after": [
9.310546875,
13.80810546875,
10.62744140625
]
}
Raw
broad-kernel-samples.csv
0 128 false previous previous 44596
0 128 false previous current 31637
0 128 true previous previous 30555
0 128 true previous current 22253
0 512 false previous previous 54341
0 512 false previous current 39989
0 512 true previous previous 51386
0 512 true previous current 34932
0 1024 false previous previous 67670
0 1024 false previous current 34291
0 1024 true previous previous 72768
0 1024 true previous current 34951
0 2048 false previous previous 110193
0 2048 false previous current 34711
0 2048 true previous previous 117384
0 2048 true previous current 34691
0 8192 false previous previous 411380
0 8192 false previous current 61471
0 8192 true previous previous 419021
0 8192 true previous current 60340
0 16384 false previous previous 797442
0 16384 false previous current 67059
0 16384 true previous previous 858363
0 16384 true previous current 69112
0 32768 false previous previous 1607313
0 32768 false previous current 74170
0 32768 true previous previous 1748743
0 32768 true previous current 71887
0 131072 false previous previous 7116770
0 131072 false previous current 140318
0 131072 true previous previous 7810138
0 131072 true previous current 135271
0 262144 false previous previous 22833391
0 262144 false previous current 211393
0 262144 true previous previous 19774887
0 262144 true previous current 222369
0 1048576 false previous previous 284775354
0 1048576 false previous current 783421
0 1048576 true previous previous 173089968
0 1048576 true previous current 771794
1 128 false previous current 37495
1 128 false previous previous 47341
1 128 true previous current 28322
1 128 true previous previous 33640
1 512 false previous current 54441
1 512 false previous previous 66869
1 512 true previous current 41571
1 512 true previous previous 56203
1 1024 false previous current 44887
1 1024 false previous previous 72487
1 1024 true previous current 37316
1 1024 true previous previous 75962
1 2048 false previous current 36314
1 2048 false previous previous 110995
1 2048 true previous current 35843
1 2048 true previous previous 121920
1 8192 false previous current 72016
1 8192 false previous previous 383799
1 8192 true previous current 67249
1 8192 true previous previous 424650
1 16384 false previous current 24570186
1 16384 false previous previous 1095674
1 16384 true previous current 95902
1 16384 true previous previous 906094
1 32768 false previous current 87480
1 32768 false previous previous 1597168
1 32768 true previous current 90544
1 32768 true previous previous 1814791
1 131072 false previous current 164754
1 131072 false previous previous 8245414
1 131072 true previous current 164313
1 131072 true previous previous 8343950
1 262144 false previous current 241969
1 262144 false previous previous 18544663
1 262144 true previous current 288868
1 262144 true previous previous 19706936
1 1048576 false previous current 769310
1 1048576 false previous previous 257928273
1 1048576 true previous current 1019191
1 1048576 true previous previous 253760224
2 128 false previous previous 82072
2 128 false previous current 48762
2 128 true previous previous 38367
2 128 true previous current 30235
2 512 false previous previous 71176
2 512 false previous current 60239
2 512 true previous previous 68061
2 512 true previous current 44335
2 1024 false previous previous 76424
2 1024 false previous current 39639
2 1024 true previous previous 81050
2 1024 true previous current 38538
2 2048 false previous previous 114690
2 2048 false previous current 36614
2 2048 true previous previous 124144
2 2048 true previous current 36484
2 8192 false previous previous 393043
2 8192 false previous current 75703
2 8192 true previous previous 429307
2 8192 true previous current 73318
2 16384 false previous previous 781508
2 16384 false previous current 73079
2 16384 true previous previous 878483
2 16384 true previous current 74050
2 32768 false previous previous 1541305
2 32768 false previous current 80900
2 32768 true previous previous 1743365
2 32768 true previous current 86829
2 131072 false previous previous 7631054
2 131072 false previous current 167559
2 131072 true previous previous 8156932
2 131072 true previous current 161490
2 262144 false previous previous 17961038
2 262144 false previous current 281076
2 262144 true previous previous 20288368
2 262144 true previous current 280687
2 1048576 false previous previous 170817569
2 1048576 false previous current 903159
2 1048576 true previous previous 186812703
2 1048576 true previous current 890310
3 128 false previous current 44627
3 128 false previous previous 51487
3 128 true previous current 30986
3 128 true previous previous 33921
3 512 false previous current 48712
3 512 false previous previous 59377
3 512 true previous current 45297
3 512 true previous previous 60319
3 1024 false previous current 40140
3 1024 false previous previous 74080
3 1024 true previous current 37786
3 1024 true previous previous 77325
3 2048 false previous current 36845
3 2048 false previous previous 112347
3 2048 true previous current 36835
3 2048 true previous previous 122762
3 8192 false previous current 73469
3 8192 false previous previous 376808
3 8192 true previous current 65698
3 8192 true previous previous 417238
3 16384 false previous current 70455
3 16384 false previous previous 753848
3 16384 true previous current 71906
3 16384 true previous previous 852694
3 32768 false previous current 76403
3 32768 false previous previous 1521175
3 32768 true previous current 80750
3 32768 true previous previous 1725999
3 131072 false previous current 154029
3 131072 false previous previous 7472648
3 131072 true previous current 155140
3 131072 true previous previous 8271042
3 262144 false previous current 240226
3 262144 false previous previous 17808391
3 262144 true previous current 278773
3 262144 true previous previous 19297458
3 1048576 false previous current 783862
3 1048576 false previous previous 167509495
3 1048576 true previous current 871332
3 1048576 true previous previous 182080307
Raw
BroadBench.lean
module
import Lean
meta import Lean
/-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES.
Master BitVec.cpop, the original kernel primitive, and the transparent implementation count identical inputs. -/
open Lean
-- The master implementation of BitVec.cpop, projected back to Nat.
@[expose] public def masterCount (width n : Nat) : Nat :=
(BitVec.ofNat width ((BitVec.ofNat width n).cpopNatRec width 0)).toNat
namespace Previous
/-- Count a chunk of at most 248 bits. Each byte is replaced by its bit count, then
multiplication adds these counts into the highest byte. The sum is at most 248. -/
@[expose, implicit_reducible] public def word (v : Nat) : Nat :=
let a := v.sub
((v.shiftRight 1).land 0x55555555555555555555555555555555555555555555555555555555555555)
let b := (a.land 0x33333333333333333333333333333333333333333333333333333333333333).add
((a.shiftRight 2).land 0x33333333333333333333333333333333333333333333333333333333333333)
let c := (b.add (b.shiftRight 4)).land
0x0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f
((c.mul 0x01010101010101010101010101010101010101010101010101010101010101).shiftRight 240).land 255
/-- Count chunks using structural recursion. The result is correct when `n < fuel`. -/
@[expose, implicit_reducible] public noncomputable def loop : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff).rec
((word (n.land 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)).add
(rec (n.shiftRight 248)))
(word n))
end Previous
@[expose] public noncomputable def previousCount (n : Nat) : Nat := Previous.loop n.succ n
@[expose] public noncomputable def transparentCount (n : Nat) : Nat :=
((n.shiftRight 64).beq 0).rec
(((n.shiftRight 256).beq 0).rec
(((n.shiftRight 4096).beq 0).rec
(((n.shiftRight 65536).beq 0).rec (Nat.popcount.grow n.succ n 131072) (Nat.popcount.word32 n))
(Nat.popcount.word16 n 4096))
(Nat.popcount.word16 n 256))
(Nat.popcount.small n)
run_cmd do
let some output ← IO.getEnv "POPCOUNT_SAMPLES" | return
let file ← IO.FS.Handle.mk output .write
let ready ← IO.mkRef (← getEnv).toKernelEnv
let env := Environment.ofKernelEnv (← ready.get)
for block in [:4] do
for width in [128, 512, 1024, 2048, 8192, 16384, 32768, 131072, 262144, 1048576] do
for dense in [false, true] do
let n := if dense then 2^width-1 else 2^(width-1)+1
let expected := if dense then width else 2
let natE := mkConst ``Nat
let mkProof (arm : String) (value : Nat) :=
let lhs := if arm == "original" then mkApp (mkConst ``Nat.popcount) (mkRawNatLit n)
else if arm == "previous" then mkApp (mkConst ``previousCount) (mkRawNatLit n)
else if arm == "current" then mkApp (mkConst ``Nat.popcount) (mkRawNatLit n)
else mkApp2 (mkConst ``masterCount) (mkRawNatLit width) (mkRawNatLit n)
let rhs := mkRawNatLit value
let type := mkApp3 (mkConst ``Eq [.succ .zero]) natE lhs rhs
mkApp (mkLambda `h .default type (mkBVar 0))
(mkApp2 (mkConst ``Eq.refl [.succ .zero]) natE rhs)
for candidate in ["previous"] do
for arm in (if block % 2 == 0 then [candidate, "current"] else ["current", candidate]) do
if block == 0 then
let bad ← IO.mkRef (Kernel.check env {} (mkProof arm (expected+1)))
if (← bad.get).isOk then throwError "wrong-result control accepted"
let input ← IO.mkRef (env, mkProof arm expected)
let (env, term) ← input.get
let start ← IO.monoNanosNow
let result ← IO.mkRef (Kernel.check env {} term)
let result ← result.get
let stop ← IO.monoNanosNow
let _ ← ofExceptKernelException result
file.putStrLn s!"{block},{width},{dense},{candidate},{arm},{stop-start}"
file.flush
Raw
division-kernel-record.json
{
"cpu": 19,
"host": "chungus2",
"load_before": [
12.60888671875,
12.89990234375,
10.15185546875
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_swar_bench.lean"
],
"original_runtime": null,
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_swar_bench.lean\n",
"load_after": [
12.60888671875,
12.89990234375,
10.15185546875
]
}
Raw
division-kernel-samples.csv
0 64 false count64 count64 43935
0 64 false count64 current 38317
0 64 false count128 count128 31507
0 64 false count128 current 24576
0 64 false chunks chunks 46088
0 64 false chunks current 24616
0 64 true count64 count64 28352
0 64 true count64 current 24647
0 64 true count128 count128 27120
0 64 true count128 current 22843
0 64 true chunks chunks 40670
0 64 true chunks current 29603
0 256 false count64 count64 57405
0 256 false count64 current 33529
0 256 false count128 count128 38668
0 256 false count128 current 32297
0 256 false chunks chunks 81261
0 256 false chunks current 31767
0 256 true count64 count64 59598
0 256 true count64 current 34611
0 256 true count128 count128 39528
0 256 true count128 current 35072
0 256 true chunks chunks 84575
0 256 true chunks current 33740
0 4096 false count64 count64 666047
0 4096 false count64 current 175751
0 4096 false count128 count128 346073
0 4096 false count128 current 168370
0 4096 false chunks chunks 889068
0 4096 false chunks current 171374
0 4096 true count64 count64 702662
0 4096 true count64 current 193567
0 4096 true count128 count128 385772
0 4096 true count128 current 198665
0 4096 true chunks chunks 935537
0 4096 true chunks current 192776
0 65536 false count64 count64 16093218
0 65536 false count64 current 4064485
0 65536 false count128 count128 8276570
0 65536 false count128 current 3976596
0 65536 false chunks chunks 16091515
0 65536 false chunks current 4016345
0 65536 true count64 count64 16439621
0 65536 true count64 current 4448535
0 65536 true count128 count128 8919473
0 65536 true count128 current 4382327
0 65536 true chunks chunks 16245274
0 65536 true chunks current 4445860
1 64 false count64 current 35993
1 64 false count64 count64 43474
1 64 false count128 current 27741
1 64 false count128 count128 34491
1 64 false chunks current 24125
1 64 false chunks chunks 66007
1 64 true count64 current 27731
1 64 true count64 count64 29173
1 64 true count128 current 23896
1 64 true count128 count128 27621
1 64 true chunks current 22844
1 64 true chunks chunks 48913
1 256 false count64 current 38457
1 256 false count64 count64 63234
1 256 false count128 current 34251
1 256 false count128 count128 42343
1 256 false chunks current 33099
1 256 false chunks chunks 94720
1 256 true count64 current 39579
1 256 true count64 count64 63304
1 256 true count128 current 35743
1 256 true count128 count128 41832
1 256 true chunks current 33910
1 256 true chunks chunks 89673
1 4096 false count64 current 181529
1 4096 false count64 count64 678787
1 4096 false count128 current 179005
1 4096 false count128 count128 356118
1 4096 false chunks current 174469
1 4096 false chunks chunks 904120
1 4096 true count64 current 214277
1 4096 true count64 count64 718816
1 4096 true count128 current 208860
1 4096 true count128 count128 398582
1 4096 true chunks current 199345
1 4096 true chunks chunks 948376
1 65536 false count64 current 4003876
1 65536 false count64 count64 15708528
1 65536 false count128 current 4020150
1 65536 false count128 count128 8121470
1 65536 false chunks current 3966831
1 65536 false chunks chunks 15535150
1 65536 true count64 current 4430048
1 65536 true count64 count64 16311452
1 65536 true count128 current 4432311
1 65536 true count128 count128 8944681
1 65536 true chunks current 4425331
1 65536 true chunks chunks 16463497
2 64 false count64 count64 45167
2 64 false count64 current 39138
2 64 false count128 count128 35393
2 64 false count128 current 26951
2 64 false chunks chunks 59118
2 64 false chunks current 26639
2 64 true count64 count64 29323
2 64 true count64 current 25647
2 64 true count128 count128 27772
2 64 true count128 current 23395
2 64 true chunks chunks 46749
2 64 true chunks current 23114
2 256 false count64 count64 62833
2 256 false count64 current 38106
2 256 false count128 count128 43664
2 256 false count128 current 33709
2 256 false chunks chunks 89703
2 256 false chunks current 33300
2 256 true count64 count64 63224
2 256 true count64 current 40570
2 256 true count128 count128 42203
2 256 true count128 current 34742
2 256 true chunks chunks 89553
2 256 true chunks current 34360
2 4096 false count64 count64 672887
2 4096 false count64 current 189050
2 4096 false count128 count128 358181
2 4096 false count128 current 177243
2 4096 false chunks chunks 902297
2 4096 false chunks current 183913
2 4096 true count64 count64 720197
2 4096 true count64 current 207257
2 4096 true count128 count128 400664
2 4096 true count128 current 200847
2 4096 true chunks chunks 946664
2 4096 true chunks current 205274
2 65536 false count64 count64 15665263
2 65536 false count64 current 4019569
2 65536 false count128 count128 8173167
2 65536 false count128 current 3961172
2 65536 false chunks chunks 15594709
2 65536 false chunks current 3981623
2 65536 true count64 count64 16397960
2 65536 true count64 current 4446642
2 65536 true count128 count128 9024650
2 65536 true count128 current 4471529
2 65536 true chunks chunks 16332182
2 65536 true chunks current 4433924
3 64 false count64 current 35082
3 64 false count64 count64 38127
3 64 false count128 current 27070
3 64 false count128 count128 32398
3 64 false chunks current 23886
3 64 false chunks chunks 61251
3 64 true count64 current 28132
3 64 true count64 count64 28883
3 64 true count128 current 23575
3 64 true count128 count128 27551
3 64 true chunks current 22914
3 64 true chunks chunks 46999
3 256 false count64 current 38437
3 256 false count64 count64 64345
3 256 false count128 current 34491
3 256 false count128 count128 42022
3 256 false chunks current 32809
3 256 false chunks chunks 90314
3 256 true count64 current 38397
3 256 true count64 count64 63414
3 256 true count128 current 38647
3 256 true count128 count128 43004
3 256 true chunks current 34120
3 256 true chunks chunks 89493
3 4096 false count64 current 181198
3 4096 false count64 count64 677764
3 4096 false count128 current 181659
3 4096 false count128 count128 355967
3 4096 false chunks current 174499
3 4096 false chunks chunks 937140
3 4096 true count64 current 212325
3 4096 true count64 count64 721710
3 4096 true count128 current 208128
3 4096 true count128 count128 401845
3 4096 true chunks current 198965
3 4096 true chunks chunks 947595
3 65536 false count64 current 3963385
3 65536 false count64 count64 15728237
3 65536 false count128 current 4050285
3 65536 false count128 count128 8177162
3 65536 false chunks current 3968113
3 65536 false chunks chunks 15669290
3 65536 true count64 current 4420233
3 65536 true count64 count64 16440753
3 65536 true count128 current 4470428
3 65536 true count128 count128 8969387
3 65536 true chunks current 4420404
3 65536 true chunks chunks 17022086
Raw
division-KernelBench.lean
module
import Lean
meta import Lean
/-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES.
The current API and alternative chunk widths count identical numeral inputs. -/
open Lean
@[expose] public def countBits (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + (n.testBit i).toNat)
-- Masked 64-bit parallel count, following Bhavik Mehta's PrimeCert #156.
@[expose] public def wordCount (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight (nat_lit 1)).land (nat_lit 0x5555555555555555))
let b := (a.land (nat_lit 0x3333333333333333)).add
((a.shiftRight (nat_lit 2)).land (nat_lit 0x3333333333333333))
let c := (b.add (b.shiftRight (nat_lit 4))).land (nat_lit 0x0f0f0f0f0f0f0f0f)
((c.mul (nat_lit 0x0101010101010101)).shiftRight (nat_lit 56)).land (nat_lit 0xff)
@[expose] public def chunkCount (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + wordCount ((n >>> (64*i)) &&& 0xffffffffffffffff))
@[expose] public def word64 (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight 1).land 6148914691236517205)
let b := (a.land 3689348814741910323).add ((a.shiftRight 2).land 3689348814741910323)
let c := (b.add (b.shiftRight 4)).land 1085102592571150095
((c.mul 72340172838076673).shiftRight 56).land 255
@[expose] public noncomputable def loop64 : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 18446744073709551615).rec
((word64 (n.mod 18446744073709551616)).add (rec (n.div 18446744073709551616)))
(word64 n))
@[expose] public noncomputable def count64 (n : Nat) : Nat := loop64 n.succ n
@[expose] public def word128 (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight 1).land 113427455640312821154458202477256070485)
let b := (a.land 68056473384187692692674921486353642291).add ((a.shiftRight 2).land 68056473384187692692674921486353642291)
let c := (b.add (b.shiftRight 4)).land 20016609818878733144904388672456953615
((c.mul 1334440654591915542993625911497130241).shiftRight 120).land 255
@[expose] public noncomputable def loop128 : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 340282366920938463463374607431768211455).rec
((word128 (n.mod 340282366920938463463374607431768211456)).add (rec (n.div 340282366920938463463374607431768211456)))
(word128 n))
@[expose] public noncomputable def count128 (n : Nat) : Nat := loop128 n.succ n
run_cmd do
let some output ← IO.getEnv "POPCOUNT_SAMPLES" | return
let file ← IO.FS.Handle.mk output .write
let ready ← IO.mkRef (← getEnv).toKernelEnv
let env := Environment.ofKernelEnv (← ready.get)
for block in [:4] do
for width in [64, 256, 4096, 65536] do
for dense in [false, true] do
let n := if dense then 2^width-1 else 2^(width-1)+1
let expected := if dense then width else 2
let natE := mkConst ``Nat
let mkProof (arm : String) (value : Nat) :=
let lhs := if arm == "count64" then mkApp (mkConst ``count64) (mkRawNatLit n)
else if arm == "count128" then mkApp (mkConst ``count128) (mkRawNatLit n)
else if arm == "current" then mkApp (mkConst ``Nat.popcount) (mkRawNatLit n)
else if arm == "chunks" then
mkApp2 (mkConst ``chunkCount) (mkRawNatLit n) (mkRawNatLit ((width+63)/64))
else mkApp2 (mkConst ``countBits) (mkRawNatLit n) (mkRawNatLit width)
let rhs := mkRawNatLit value
let type := mkApp3 (mkConst ``Eq [.succ .zero]) natE lhs rhs
mkApp (mkLambda `h .default type (mkBVar 0))
(mkApp2 (mkConst ``Eq.refl [.succ .zero]) natE rhs)
for candidate in ["count64", "count128", "chunks"] do
for arm in (if block % 2 == 0 then [candidate, "current"] else ["current", candidate]) do
if block == 0 then
let bad ← IO.mkRef (Kernel.check env {} (mkProof arm (expected+1)))
if (← bad.get).isOk then throwError "wrong-result control accepted"
let input ← IO.mkRef (env, mkProof arm expected)
let (env, term) ← input.get
let start ← IO.monoNanosNow
let result ← IO.mkRef (Kernel.check env {} term)
let result ← result.get
let stop ← IO.monoNanosNow
let _ ← ofExceptKernelException result
file.putStrLn s!"{block},{width},{dense},{candidate},{arm},{stop-start}"
file.flush
Raw
exploratory-log.txt
++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_swar_bench.lean
popcount_swar_bench.lean:29:21-29:27: error: code generator does not support recursor `Bool.rec` yet, consider using 'match ... with' and/or structural recursion
popcount_swar_bench.lean:35:21-35:28: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'loop64', which is 'noncomputable'
popcount_swar_bench.lean:43:21-43:28: error: code generator does not support recursor `Bool.rec` yet, consider using 'match ... with' and/or structural recursion
popcount_swar_bench.lean:49:21-49:29: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'loop128', which is 'noncomputable'
popcount_swar_bench.lean:57:21-57:28: error: code generator does not support recursor `Bool.rec` yet, consider using 'match ... with' and/or structural recursion
popcount_swar_bench.lean:63:21-63:29: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'loop248', which is 'noncomputable'
--- - 2026-09-16 04:29:34.468731010 +0000
+++ popcount_swar_bench.lean.out.produced 2026-09-16 04:29:34.467273192 +0000
@@ -0,0 +1,6 @@
+popcount_swar_bench.lean:29:21-29:27: error: code generator does not support recursor `Bool.rec` yet, consider using 'match ... with' and/or structural recursion
+popcount_swar_bench.lean:35:21-35:28: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'loop64', which is 'noncomputable'
+popcount_swar_bench.lean:43:21-43:28: error: code generator does not support recursor `Bool.rec` yet, consider using 'match ... with' and/or structural recursion
+popcount_swar_bench.lean:49:21-49:29: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'loop128', which is 'noncomputable'
+popcount_swar_bench.lean:57:21-57:28: error: code generator does not support recursor `Bool.rec` yet, consider using 'match ... with' and/or structural recursion
+popcount_swar_bench.lean:63:21-63:29: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'loop248', which is 'noncomputable'
TEST FAILED: Unexpected output
Raw
exploratory-samples.csv
0 64 false count64 count64 39448
0 64 false count64 count248 28111
0 64 false count128 count128 27571
0 64 false count128 count248 26019
0 64 false chunks chunks 77404
0 64 false chunks count248 26569
0 64 true count64 count64 26549
0 64 true count64 count248 26079
0 64 true count128 count128 26519
0 64 true count128 count248 30695
0 64 true chunks chunks 71626
0 64 true chunks count248 25828
0 256 false count64 count64 57305
0 256 false count64 count248 37366
0 256 false count128 count128 38266
0 256 false count128 count248 36344
0 256 false chunks chunks 227026
0 256 false chunks count248 36364
0 256 true count64 count64 59038
0 256 true count64 count248 38798
0 256 true count128 count128 39098
0 256 true count128 count248 37285
0 256 true chunks chunks 165104
0 256 true chunks count248 37545
0 4096 false count64 count64 673558
0 4096 false count64 count248 193626
0 4096 false count128 count128 351230
0 4096 false count128 count248 190933
0 4096 false chunks chunks 2060713
0 4096 false chunks count248 195679
0 4096 true count64 count64 794116
0 4096 true count64 count248 214197
0 4096 true count128 count128 393302
0 4096 true count128 count248 209040
0 4096 true chunks chunks 2109395
0 4096 true chunks count248 213086
0 65536 false count64 count64 16138117
0 65536 false count64 count248 4243937
0 65536 false count128 count128 8126970
0 65536 false count128 count248 4244999
0 65536 false chunks chunks 35230131
0 65536 false chunks count248 4258218
0 65536 true count64 count64 16284754
0 65536 true count64 count248 4687695
0 65536 true count128 count128 8963188
0 65536 true count128 count248 4683789
0 65536 true chunks chunks 39144669
0 65536 true chunks count248 4801733
1 64 false count64 count248 46278
1 64 false count64 count64 46348
1 64 false count128 count248 27381
1 64 false count128 count128 42442
1 64 false chunks count248 26199
1 64 false chunks chunks 118015
1 64 true count64 count248 30144
1 64 true count64 count64 27030
1 64 true count128 count248 26239
1 64 true count128 count128 26599
1 64 true chunks count248 25808
1 64 true chunks chunks 79478
1 256 false count64 count248 44136
1 256 false count64 count64 62132
1 256 false count128 count248 38256
1 256 false count128 count128 42022
1 256 false chunks count248 44326
1 256 false chunks chunks 176271
1 256 true count64 count248 43134
1 256 true count64 count64 62853
1 256 true count128 count248 39078
1 256 true count128 count128 41521
1 256 true chunks count248 38477
1 256 true chunks chunks 173427
1 4096 false count64 count248 201669
1 4096 false count64 count64 677834
1 4096 false count128 count248 199416
1 4096 false count128 count128 364099
1 4096 false chunks count248 195430
1 4096 false chunks chunks 2122725
1 4096 true count64 count248 239756
1 4096 true count64 count64 733997
1 4096 true count128 count248 220035
1 4096 true count128 count128 402887
1 4096 true chunks count248 215689
1 4096 true chunks chunks 2133170
1 65536 false count64 count248 4328392
1 65536 false count64 count64 16003268
1 65536 false count128 count248 4271908
1 65536 false count128 count128 8150494
1 65536 false chunks count248 4249034
1 65536 false chunks chunks 36531879
1 65536 true count64 count248 4781804
1 65536 true count64 count64 16502096
1 65536 true count128 count248 4716657
1 65536 true count128 count128 9044769
1 65536 true chunks count248 4688896
1 65536 true chunks chunks 36492561
2 64 false count64 count64 44636
2 64 false count64 count248 32558
2 64 false count128 count128 31507
2 64 false count128 count248 27401
2 64 false chunks chunks 101630
2 64 false chunks count248 28252
2 64 true count64 count64 28653
2 64 true count64 count248 27081
2 64 true count128 count128 27060
2 64 true count128 count248 26038
2 64 true chunks chunks 79798
2 64 true chunks count248 26279
2 256 false count64 count64 63414
2 256 false count64 count248 40280
2 256 false count128 count128 44526
2 256 false count128 count248 37446
2 256 false chunks chunks 175571
2 256 false chunks count248 37936
2 256 true count64 count64 63113
2 256 true count64 count248 41622
2 256 true count128 count128 41662
2 256 true count128 count248 38817
2 256 true chunks chunks 174599
2 256 true chunks count248 38477
2 4096 false count64 count64 679196
2 4096 false count64 count248 202120
2 4096 false count128 count128 354375
2 4096 false count128 count248 197242
2 4096 false chunks chunks 2052421
2 4096 false chunks count248 209150
2 4096 true count64 count64 720878
2 4096 true count64 count248 222229
2 4096 true count128 count128 394955
2 4096 true count128 count248 218012
2 4096 true chunks chunks 2107743
2 4096 true chunks count248 228368
2 65536 false count64 count64 15824512
2 65536 false count64 count248 4315484
2 65536 false count128 count128 8153339
2 65536 false count128 count248 4244839
2 65536 false chunks chunks 35884630
2 65536 false chunks count248 4325167
2 65536 true count64 count64 16485041
2 65536 true count64 count248 4742476
2 65536 true count128 count128 9008566
2 65536 true count128 count248 4704339
2 65536 true chunks chunks 40043891
2 65536 true chunks count248 4857957
3 64 false count64 count248 42443
3 64 false count64 count64 39729
3 64 false count128 count248 27550
3 64 false count128 count128 33159
3 64 false chunks count248 26198
3 64 false chunks chunks 113949
3 64 true count64 count248 29744
3 64 true count64 count64 26970
3 64 true count128 count248 25979
3 64 true count128 count128 26700
3 64 true chunks count248 26139
3 64 true chunks chunks 79848
3 256 false count64 count248 41842
3 256 false count64 count64 60600
3 256 false count128 count248 37896
3 256 false count128 count128 41371
3 256 false chunks count248 37045
3 256 false chunks chunks 178755
3 256 true count64 count248 42783
3 256 true count64 count64 61912
3 256 true count128 count248 40169
3 256 true count128 count128 41892
3 256 true chunks count248 38457
3 256 true chunks chunks 172675
3 4096 false count64 count248 200818
3 4096 false count64 count64 676612
3 4096 false count128 count248 199215
3 4096 false count128 count128 356558
3 4096 false chunks count248 197583
3 4096 false chunks chunks 2058910
3 4096 true count64 count248 233766
3 4096 true count64 count64 728670
3 4096 true count128 count248 226095
3 4096 true count128 count128 397338
3 4096 true chunks count248 215249
3 4096 true chunks chunks 2112780
3 65536 false count64 count248 4375391
3 65536 false count64 count64 16349942
3 65536 false count128 count248 4334541
3 65536 false count128 count128 8282550
3 65536 false chunks count248 4255424
3 65536 false chunks chunks 42457007
3 65536 true count64 count248 5116710
3 65536 true count64 count64 16885825
3 65536 true count128 count248 4733031
3 65536 true count128 count128 9015195
3 65536 true chunks count248 4683689
3 65536 true chunks chunks 37834148
Raw
generic-kernel-record.json
{
"cpu": 68,
"host": "chungus2",
"load_before": [
3.40380859375,
3.66259765625,
5.53369140625
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_artifact.lean"
],
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_artifact.lean\n",
"load_after": [
3.45166015625,
3.66845703125,
5.525390625
]
}
Raw
generic-kernel-samples.csv
0 64 false wide wide 47941
0 64 false wide current 27671
0 64 false special special 27080
0 64 false special current 23255
0 64 true wide wide 37496
0 64 true wide current 24266
0 64 true special special 26379
0 64 true special current 22583
0 256 false wide wide 47931
0 256 false wide current 33169
0 256 false special special 33910
0 256 false special current 31116
0 256 true wide wide 45497
0 256 true wide current 34151
0 256 true special special 37225
0 256 true special current 32368
0 4096 false wide wide 62984
0 4096 false wide current 168980
0 4096 false special special 37896
0 4096 false special current 172045
0 4096 true wide wide 63384
0 4096 true wide current 191064
0 4096 true special special 40039
0 4096 true special current 190242
0 65536 false wide wide 123123
0 65536 false wide current 2816276
0 65536 false special special 79758
0 65536 false special current 2747965
0 65536 true wide wide 128671
0 65536 true wide current 3248786
0 65536 true special special 80369
0 65536 true special current 3230229
0 1048576 false wide wide 800026
0 1048576 false wide current 227387385
0 1048576 false special special 962226
0 1048576 false special current 233865630
0 1048576 true wide wide 880926
0 1048576 true wide current 170627213
0 1048576 true special special 959692
0 1048576 true special current 180945691
1 64 false wide current 106878
1 64 false wide wide 105767
1 64 false special current 40990
1 64 false special special 52648
1 64 true wide current 34090
1 64 true wide wide 47891
1 64 true special current 29724
1 64 true special special 32718
1 256 false wide current 44346
1 256 false wide wide 59358
1 256 false special current 35413
1 256 false special special 45618
1 256 true wide current 40570
1 256 true wide wide 51477
1 256 true special current 36054
1 256 true special special 36915
1 4096 false wide current 194178
1 4096 false wide wide 88922
1 4096 false special current 199946
1 4096 false special special 54470
1 4096 true wide current 199967
1 4096 true wide wide 67080
1 4096 true special current 192145
1 4096 true special special 40931
1 65536 false wide current 3205883
1 65536 false wide wide 179115
1 65536 false special current 2955862
1 65536 false special special 102942
1 65536 true wide current 3303758
1 65536 true wide wide 153508
1 65536 true special current 3449163
1 65536 true special special 95842
1 1048576 false wide current 190898246
1 1048576 false wide wide 1089755
1 1048576 false special current 192253075
1 1048576 false special special 1171076
1 1048576 true wide current 194267832
1 1048576 true wide wide 1062275
1 1048576 true special current 170801301
1 1048576 true special special 1144136
2 64 false wide wide 58768
2 64 false wide current 37796
2 64 false special special 42844
2 64 false special current 27751
2 64 true wide wide 41842
2 64 true wide current 27521
2 64 true special special 28602
2 64 true special current 24136
2 256 false wide wide 53199
2 256 false wide current 38517
2 256 false special special 45287
2 256 false special current 33920
2 256 true wide wide 50985
2 256 true wide current 38807
2 256 true special special 36214
2 256 true special current 34351
2 4096 false wide wide 72657
2 4096 false wide current 185475
2 4096 false special special 56904
2 4096 false special current 190422
2 4096 true wide wide 72036
2 4096 true wide current 199616
2 4096 true special special 40870
2 4096 true special current 190563
2 65536 false wide wide 145676
2 65536 false wide current 3029903
2 65536 false special special 103123
2 65536 false special current 2895773
2 65536 true wide wide 146928
2 65536 true wide current 3290028
2 65536 true special special 96714
2 65536 true special current 3287634
2 1048576 false wide wide 839986
2 1048576 false wide current 155811177
2 1048576 false special special 1172358
2 1048576 false special current 165494223
2 1048576 true wide wide 1046041
2 1048576 true wide current 164973841
2 1048576 true special special 1125499
2 1048576 true special current 171527577
3 64 false wide current 66528
3 64 false wide wide 90674
3 64 false special current 32298
3 64 false special special 46229
3 64 true wide current 30004
3 64 true wide wide 42923
3 64 true special current 25468
3 64 true special special 28572
3 256 false wide current 39960
3 256 false wide wide 58346
3 256 false special current 35783
3 256 false special special 45918
3 256 true wide current 40120
3 256 true wide wide 50585
3 256 true special current 34772
3 256 true special special 36163
3 4096 false wide current 184623
3 4096 false wide wide 77284
3 4096 false special current 5350383
3 4096 false special special 80039
3 4096 true wide current 224223
3 4096 true wide wide 99137
3 4096 true special current 196041
3 4096 true special special 42794
3 65536 false wide current 3148858
3 65536 false wide wide 160378
3 65536 false special current 2950134
3 65536 false special special 104264
3 65536 true wide current 19215408
3 65536 true wide wide 236441
3 65536 true special current 3585175
3 65536 true special special 113488
3 1048576 false wide current 229379238
3 1048576 false wide wide 1145227
3 1048576 false special current 216689144
3 1048576 false special special 1147791
3 1048576 true wide current 186180181
3 1048576 true wide wide 1104658
3 1048576 true special current 170646972
3 1048576 true special special 1135734
Raw
generic-KernelBench.lean
module
import Lean
meta import Lean
/-! Explore whole-integer and balanced population counting, with kernel wrong-result controls. -/
open Lean
@[expose] public def byteCounts (n ones : Nat) : Nat :=
let a := n.sub ((n.shiftRight 1).land (ones.div 3))
let b := (a.land (ones.div 5)).add ((a.shiftRight 2).land (ones.div 5))
(b.add (b.shiftRight 4)).land (ones.div 17)
@[expose] public noncomputable def foldCounts : Nat → Nat → Nat → Nat → Nat → Nat :=
Nat.rec (fun _ _ _ _ => 0) (fun _ rec width ones lane n =>
(width.blt ((Nat.shiftLeft 1 lane).sub 1)).rec
(rec width ones (lane.add lane)
((n.add (n.shiftRight lane)).land (ones.div ((Nat.shiftLeft 1 lane).add 1))))
(n.mod ((Nat.shiftLeft 1 lane).sub 1)))
@[expose] public noncomputable def wholeWord (n width : Nat) : Nat :=
let ones := (Nat.shiftLeft 1 width).sub 1
foldCounts width width ones 8 (byteCounts n ones)
@[expose] public noncomputable def findWidth : Nat → Nat → Nat → Nat :=
Nat.rec (fun _ _ => 0) (fun _ rec n width =>
((n.shiftRight width).beq 0).rec
(rec n (width.add width)) (wholeWord n width))
@[expose] public noncomputable def wideCount (n : Nat) : Nat := findWidth n.succ n 128
@[expose] public noncomputable def balanced : Nat → Nat → Nat → Nat :=
Nat.rec (fun _ _ => 0) (fun _ rec n width =>
(width.ble 128).rec
((rec (n.land ((Nat.shiftLeft 1 (width.div 2)).sub 1)) (width.div 2)).add
(rec (n.shiftRight (width.div 2)) (width.div 2)))
(Nat.popcount.word n))
@[expose] public noncomputable def findBalanced : Nat → Nat → Nat → Nat :=
Nat.rec (fun _ _ => 0) (fun _ rec n width =>
((n.shiftRight width).beq 0).rec
(rec n (width.add width)) (balanced width n width))
@[expose] public noncomputable def balancedCount (n : Nat) : Nat := findBalanced n.succ n 128
@[expose] public def modWord (n : Nat) : Nat :=
(byteCounts n 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff).mod 255
@[expose] public noncomputable def modLoop : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff).rec
((modWord (n.land 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)).add
(rec (n.shiftRight 248)))
(modWord n))
@[expose] public noncomputable def modCount (n : Nat) : Nat := modLoop n.succ n
@[expose] public def special64 (n : Nat) : Nat :=
let ones := 18446744073709551615
let a := n.sub ((n.shiftRight 1).land (ones.div 3))
let b := (a.land (ones.div 5)).add ((a.shiftRight 2).land (ones.div 5))
let c := (b.add (b.shiftRight 4)).land (ones.div 17)
c.mod 255
@[expose] public def special256 (n : Nat) : Nat :=
let ones := 115792089237316195423570985008687907853269984665640564039457584007913129639935
let a := n.sub ((n.shiftRight 1).land (ones.div 3))
let b := (a.land (ones.div 5)).add ((a.shiftRight 2).land (ones.div 5))
let c := (b.add (b.shiftRight 4)).land (ones.div 17)
let d := (c.add (c.shiftRight 8)).land (ones.div 257)
d.mod 65535
@[expose] public def special4096 (n : Nat) : Nat :=
let ones := ((Nat.shiftLeft 1 4096).sub 1)
let a := n.sub ((n.shiftRight 1).land (ones.div 3))
let b := (a.land (ones.div 5)).add ((a.shiftRight 2).land (ones.div 5))
let c := (b.add (b.shiftRight 4)).land (ones.div 17)
let d := (c.add (c.shiftRight 8)).land (ones.div 257)
d.mod 65535
@[expose] public def special65536 (n : Nat) : Nat :=
let ones := ((Nat.shiftLeft 1 65536).sub 1)
let a := n.sub ((n.shiftRight 1).land (ones.div 3))
let b := (a.land (ones.div 5)).add ((a.shiftRight 2).land (ones.div 5))
let c := (b.add (b.shiftRight 4)).land (ones.div 17)
let d := (c.add (c.shiftRight 8)).land (ones.div 257)
let e := (d.add (d.shiftRight 16)).land (ones.div 65537)
e.mod 4294967295
@[expose] public noncomputable def special (n : Nat) : Nat :=
((n.shiftRight 64).beq 0).rec
(((n.shiftRight 256).beq 0).rec
(((n.shiftRight 4096).beq 0).rec
(((n.shiftRight 65536).beq 0).rec (wideCount n) (special65536 n))
(special4096 n))
(special256 n))
(special64 n)
run_cmd do
let some output ← IO.getEnv "POPCOUNT_SAMPLES" | return
let file ← IO.FS.Handle.mk output .write
let ready ← IO.mkRef (← getEnv).toKernelEnv
let env := Environment.ofKernelEnv (← ready.get)
for block in [:4] do
for width in [64, 256, 4096, 65536, 1048576] do
for dense in [false, true] do
let n := if dense then 2^width-1 else 2^(width-1)+1
let expected := if dense then width else 2
let natE := mkConst ``Nat
let mkProof (arm : String) (value : Nat) :=
let fn := match arm with
| "special" => ``special
| "wide" => ``wideCount
| "balanced" => ``balancedCount
| "mod" => ``modCount
| _ => ``Nat.popcount
let lhs := mkApp (mkConst fn) (mkRawNatLit n)
let rhs := mkRawNatLit value
let type := mkApp3 (mkConst ``Eq [.succ .zero]) natE lhs rhs
mkApp (mkLambda `h .default type (mkBVar 0))
(mkApp2 (mkConst ``Eq.refl [.succ .zero]) natE rhs)
for candidate in ["wide", "special"] do
for arm in (if block % 2 == 0 then [candidate, "current"] else ["current", candidate]) do
if block == 0 then
let bad ← IO.mkRef (Kernel.check env {} (mkProof arm (expected+1)))
if (← bad.get).isOk then throwError "wrong-result control accepted"
let input ← IO.mkRef (env, mkProof arm expected)
let (env, term) ← input.get
let start ← IO.monoNanosNow
let result ← IO.mkRef (Kernel.check env {} term)
let result ← result.get
let stop ← IO.monoNanosNow
let _ ← ofExceptKernelException result
file.putStrLn s!"{block},{width},{dense},{candidate},{arm},{stop-start}"
file.flush
Raw
kernel-record.json
{
"cpu": 90,
"host": "chungus2",
"load_before": [
22.1845703125,
16.34619140625,
11.0712890625
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_artifact.lean"
],
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_artifact.lean\n",
"load_after": [
22.1845703125,
16.34619140625,
11.0712890625
]
}
Raw
kernel-samples.csv
0 64 false count64 count64 49593
0 64 false count64 current 46308
0 64 false count128 count128 39989
0 64 false count128 current 28512
0 64 false chunks chunks 50185
0 64 false chunks current 23265
0 64 true count64 count64 30105
0 64 true count64 current 24797
0 64 true count128 count128 29414
0 64 true count128 current 22383
0 64 true chunks chunks 45026
0 64 true chunks current 22153
0 256 false count64 count64 72357
0 256 false count64 current 37175
0 256 false count128 count128 41942
0 256 false count128 current 33309
0 256 false chunks chunks 88011
0 256 false chunks current 33039
0 256 true count64 count64 65066
0 256 true count64 current 34241
0 256 true count128 count128 42874
0 256 true count128 current 36924
0 256 true chunks chunks 88532
0 256 true chunks current 32738
0 4096 false count64 count64 704314
0 4096 false count64 current 40089
0 4096 false count128 count128 357521
0 4096 false count128 current 36985
0 4096 false chunks chunks 1010037
0 4096 false chunks current 42573
0 4096 true count64 count64 739617
0 4096 true count64 current 39268
0 4096 true count128 count128 402206
0 4096 true count128 current 36974
0 4096 true chunks chunks 994555
0 4096 true chunks current 39819
0 65536 false count64 count64 14317546
0 65536 false count64 current 91695
0 65536 false count128 count128 6773532
0 65536 false count128 current 91335
0 65536 false chunks chunks 18372027
0 65536 false chunks current 93719
0 65536 true count64 count64 15216198
0 65536 true count64 current 90374
0 65536 true count128 count128 7493139
0 65536 true count128 current 85356
0 65536 true chunks chunks 18411505
0 65536 true chunks current 89173
1 64 false count64 current 29794
1 64 false count64 count64 57595
1 64 false count128 current 25949
1 64 false count128 count128 45518
1 64 false chunks current 22633
1 64 false chunks chunks 79698
1 64 true count64 current 25798
1 64 true count64 count64 31607
1 64 true count128 current 22624
1 64 true count128 count128 30235
1 64 true chunks current 21262
1 64 true chunks chunks 49814
1 256 false count64 current 43905
1 256 false count64 count64 67870
1 256 false count128 current 36714
1 256 false count128 count128 45728
1 256 false chunks current 35132
1 256 false chunks chunks 97624
1 256 true count64 current 37086
1 256 true count64 count64 67741
1 256 true count128 current 35602
1 256 true count128 count128 45458
1 256 true chunks current 32989
1 256 true chunks chunks 95211
1 4096 false count64 current 42183
1 4096 false count64 count64 707168
1 4096 false count128 current 43695
1 4096 false count128 count128 372802
1 4096 false chunks current 38908
1 4096 false chunks chunks 973633
1 4096 true count64 current 49303
1 4096 true count64 count64 754759
1 4096 true count128 current 42423
1 4096 true count128 count128 409697
1 4096 true chunks current 43154
1 4096 true chunks chunks 1002105
1 65536 false count64 current 97975
1 65536 false count64 count64 13714752
1 65536 false count128 current 127278
1 65536 false count128 count128 6484383
1 65536 false chunks current 112597
1 65536 false chunks chunks 21092620
1 65536 true count64 current 150894
1 65536 true count64 count64 14891237
1 65536 true count128 current 137554
1 65536 true count128 count128 7725252
1 65536 true chunks current 131524
1 65536 true chunks chunks 19376526
2 64 false count64 count64 81511
2 64 false count64 current 45637
2 64 false count128 count128 52558
2 64 false count128 current 28172
2 64 false chunks chunks 89003
2 64 false chunks current 25258
2 64 true count64 count64 34020
2 64 true count64 current 26830
2 64 true count128 count128 30215
2 64 true count128 current 22172
2 64 true chunks chunks 51166
2 64 true chunks current 22133
2 256 false count64 count64 83444
2 256 false count64 current 56604
2 256 false count128 count128 51115
2 256 false count128 current 37566
2 256 false chunks chunks 98026
2 256 false chunks current 34712
2 256 true count64 count64 68531
2 256 true count64 current 37736
2 256 true count128 count128 45087
2 256 true count128 current 34020
2 256 true chunks chunks 97074
2 256 true chunks current 33209
2 4096 false count64 count64 746998
2 4096 false count64 current 50235
2 4096 false count128 count128 374455
2 4096 false count128 current 40160
2 4096 false chunks chunks 980935
2 4096 false chunks current 55602
2 4096 true count64 count64 756001
2 4096 true count64 current 46629
2 4096 true count128 count128 435005
2 4096 true count128 current 40069
2 4096 true chunks chunks 1037057
2 4096 true chunks current 49723
2 65536 false count64 count64 15515602
2 65536 false count64 current 143783
2 65536 false count128 count128 7113726
2 65536 false count128 current 128380
2 65536 false chunks chunks 22060996
2 65536 false chunks current 170733
2 65536 true count64 count64 17923391
2 65536 true count64 current 158875
2 65536 true count128 count128 9074222
2 65536 true count128 current 149732
2 65536 true chunks chunks 23857098
2 65536 true chunks current 184033
3 64 false count64 current 49924
3 64 false count64 count64 71056
3 64 false count128 current 41472
3 64 false count128 count128 65426
3 64 false chunks current 32959
3 64 false chunks chunks 102633
3 64 true count64 current 28802
3 64 true count64 count64 35733
3 64 true count128 current 25889
3 64 true count128 count128 32818
3 64 true chunks current 24076
3 64 true chunks chunks 58416
3 256 false count64 current 55022
3 256 false count64 count64 77165
3 256 false count128 current 38798
3 256 false count128 count128 47771
3 256 false chunks current 35853
3 256 false chunks chunks 103033
3 256 true count64 current 50024
3 256 true count64 count64 73499
3 256 true count128 current 38147
3 256 true count128 count128 48502
3 256 true chunks current 34722
3 256 true chunks chunks 104616
3 4096 false count64 current 46148
3 4096 false count64 count64 856480
3 4096 false count128 current 54992
3 4096 false count128 count128 439882
3 4096 false chunks current 43564
3 4096 false chunks chunks 1036577
3 4096 true count64 current 58097
3 4096 true count64 count64 817663
3 4096 true count128 current 44146
3 4096 true count128 count128 431290
3 4096 true chunks current 40070
3 4096 true chunks chunks 1162373
3 65536 false count64 current 111946
3 65536 false count64 count64 16921576
3 65536 false count128 current 159856
3 65536 false count128 count128 7959700
3 65536 false chunks current 139788
3 65536 false chunks chunks 22868693
3 65536 true count64 current 172205
3 65536 true count64 count64 17492172
3 65536 true count128 current 165114
3 65536 true count128 count128 8602263
3 65536 true chunks current 138726
3 65536 true chunks chunks 22400619
Raw
KernelBench.lean
module
import Lean
meta import Lean
/-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES.
The current API and alternative chunk widths count identical numeral inputs. -/
open Lean
@[expose] public def countBits (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + (n.testBit i).toNat)
-- Masked 64-bit parallel count, following Bhavik Mehta's PrimeCert #156.
@[expose] public def wordCount (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight (nat_lit 1)).land (nat_lit 0x5555555555555555))
let b := (a.land (nat_lit 0x3333333333333333)).add
((a.shiftRight (nat_lit 2)).land (nat_lit 0x3333333333333333))
let c := (b.add (b.shiftRight (nat_lit 4))).land (nat_lit 0x0f0f0f0f0f0f0f0f)
((c.mul (nat_lit 0x0101010101010101)).shiftRight (nat_lit 56)).land (nat_lit 0xff)
@[expose] public def chunkCount (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + wordCount ((n >>> (64*i)) &&& 0xffffffffffffffff))
@[expose] public def word64 (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight 1).land 6148914691236517205)
let b := (a.land 3689348814741910323).add ((a.shiftRight 2).land 3689348814741910323)
let c := (b.add (b.shiftRight 4)).land 1085102592571150095
((c.mul 72340172838076673).shiftRight 56).land 255
@[expose] public noncomputable def loop64 : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 18446744073709551615).rec
((word64 (n.land 18446744073709551615)).add (rec (n.shiftRight 64)))
(word64 n))
@[expose] public noncomputable def count64 (n : Nat) : Nat := loop64 n.succ n
@[expose] public def word128 (v : Nat) : Nat :=
let a := v.sub ((v.shiftRight 1).land 113427455640312821154458202477256070485)
let b := (a.land 68056473384187692692674921486353642291).add ((a.shiftRight 2).land 68056473384187692692674921486353642291)
let c := (b.add (b.shiftRight 4)).land 20016609818878733144904388672456953615
((c.mul 1334440654591915542993625911497130241).shiftRight 120).land 255
@[expose] public noncomputable def loop128 : Nat → Nat → Nat :=
Nat.rec (fun _ => 0) (fun _ rec n =>
(n.ble 340282366920938463463374607431768211455).rec
((word128 (n.land 340282366920938463463374607431768211455)).add (rec (n.shiftRight 128)))
(word128 n))
@[expose] public noncomputable def count128 (n : Nat) : Nat := loop128 n.succ n
run_cmd do
let some output ← IO.getEnv "POPCOUNT_SAMPLES" | return
let file ← IO.FS.Handle.mk output .write
let ready ← IO.mkRef (← getEnv).toKernelEnv
let env := Environment.ofKernelEnv (← ready.get)
for block in [:4] do
for width in [64, 256, 4096, 65536] do
for dense in [false, true] do
let n := if dense then 2^width-1 else 2^(width-1)+1
let expected := if dense then width else 2
let natE := mkConst ``Nat
let mkProof (arm : String) (value : Nat) :=
let lhs := if arm == "count64" then mkApp (mkConst ``count64) (mkRawNatLit n)
else if arm == "count128" then mkApp (mkConst ``count128) (mkRawNatLit n)
else if arm == "current" then mkApp (mkConst ``Nat.popcount) (mkRawNatLit n)
else if arm == "chunks" then
mkApp2 (mkConst ``chunkCount) (mkRawNatLit n) (mkRawNatLit ((width+63)/64))
else mkApp2 (mkConst ``countBits) (mkRawNatLit n) (mkRawNatLit width)
let rhs := mkRawNatLit value
let type := mkApp3 (mkConst ``Eq [.succ .zero]) natE lhs rhs
mkApp (mkLambda `h .default type (mkBVar 0))
(mkApp2 (mkConst ``Eq.refl [.succ .zero]) natE rhs)
for candidate in ["count64", "count128", "chunks"] do
for arm in (if block % 2 == 0 then [candidate, "current"] else ["current", candidate]) do
if block == 0 then
let bad ← IO.mkRef (Kernel.check env {} (mkProof arm (expected+1)))
if (← bad.get).isOk then throwError "wrong-result control accepted"
let input ← IO.mkRef (env, mkProof arm expected)
let (env, term) ← input.get
let start ← IO.monoNanosNow
let result ← IO.mkRef (Kernel.check env {} term)
let result ← result.get
let stop ← IO.monoNanosNow
let _ ← ofExceptKernelException result
file.putStrLn s!"{block},{width},{dense},{candidate},{arm},{stop-start}"
file.flush
Raw
native-record.json
{
"cpu": 53,
"host": "chungus2",
"load_before": [
12.60888671875,
12.89990234375,
10.15185546875
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/compile/run_test.sh",
"popcount_native_bench.lean"
],
"original_runtime": null,
"returncode": 0,
"stdout": "Compiling and executing lean file\n",
"stderr": "++ ./popcount_native_bench.lean.out\n",
"load_after": [
9.80615234375,
12.21630859375,
9.998046875
]
}
Raw
native-samples.csv
0 32 false bits bits 35402
0 32 false bits current 1302
0 32 false chunks chunks 40960
0 32 false chunks current 451
0 32 true bits bits 26199
0 32 true bits current 431
0 32 true chunks chunks 26619
0 32 true chunks current 431
0 64 false bits bits 208189
0 64 false bits current 6700
0 64 false chunks chunks 42903
0 64 false chunks current 5889
0 64 true bits bits 207889
0 64 true bits current 5859
0 64 true chunks chunks 47961
0 64 true chunks current 5848
0 256 false bits bits 1796583
0 256 false bits current 6090
0 256 false chunks chunks 97365
0 256 false chunks current 6038
0 256 true bits bits 1844324
0 256 true bits current 6079
0 256 true chunks chunks 192425
0 256 true chunks current 6099
0 4096 false bits bits 39481101
0 4096 false bits current 12930
0 4096 false chunks chunks 1380907
0 4096 false chunks current 12469
0 4096 true bits bits 39357207
0 4096 true bits current 12448
0 4096 true chunks chunks 3328364
0 4096 true chunks current 12469
0 65536 false bits bits 2958624881
0 65536 false bits current 122992
0 65536 false chunks chunks 58940329
0 65536 false chunks current 122772
0 65536 true bits bits 3047862823
0 65536 true bits current 123202
0 65536 true chunks chunks 93284765
0 65536 true chunks current 122432
1 32 false bits current 701
1 32 false bits bits 28532
1 32 false chunks current 431
1 32 false chunks chunks 27540
1 32 true bits current 420
1 32 true bits bits 26720
1 32 true chunks current 410
1 32 true chunks chunks 27140
1 64 false bits current 6049
1 64 false bits bits 220137
1 64 false chunks current 5979
1 64 false chunks chunks 39989
1 64 true bits current 5979
1 64 true bits bits 216270
1 64 true chunks current 5979
1 64 true chunks chunks 48912
1 256 false bits current 6170
1 256 false bits bits 1822722
1 256 false chunks current 6170
1 256 false chunks chunks 98826
1 256 true bits current 6129
1 256 true bits bits 1755733
1 256 true chunks current 6129
1 256 true chunks chunks 194518
1 4096 false bits current 12278
1 4096 false bits bits 37524110
1 4096 false chunks current 12228
1 4096 false chunks chunks 1390091
1 4096 true bits current 12269
1 4096 true bits bits 38171339
1 4096 true chunks current 12519
1 4096 true chunks chunks 3269748
1 65536 false bits current 120639
1 65536 false bits bits 3025386617
1 65536 false chunks current 122842
1 65536 false chunks chunks 60921646
1 65536 true bits current 121681
1 65536 true bits bits 3002158505
1 65536 true chunks current 122662
1 65536 true chunks chunks 92829301
2 32 false bits bits 29844
2 32 false bits current 470
2 32 false chunks chunks 27261
2 32 false chunks current 421
2 32 true bits bits 24196
2 32 true bits current 420
2 32 true chunks chunks 26980
2 32 true chunks current 410
2 64 false bits bits 203462
2 64 false bits current 5788
2 64 false chunks chunks 40000
2 64 false chunks current 5729
2 64 true bits bits 206647
2 64 true bits current 5819
2 64 true chunks chunks 48823
2 64 true chunks current 5708
2 256 false bits bits 1705368
2 256 false bits current 5879
2 256 false chunks chunks 102402
2 256 false chunks current 5849
2 256 true bits bits 1738538
2 256 true bits current 5848
2 256 true chunks chunks 194919
2 256 true chunks current 9444
2 4096 false bits bits 37841290
2 4096 false bits current 12399
2 4096 false chunks chunks 1394327
2 4096 false chunks current 12329
2 4096 true bits bits 38387019
2 4096 true bits current 12278
2 4096 true chunks chunks 3327734
2 4096 true chunks current 12288
2 65536 false bits bits 3017811566
2 65536 false bits current 122552
2 65536 false chunks chunks 60953524
2 65536 false chunks current 125016
2 65536 true bits bits 3025649131
2 65536 true bits current 122491
2 65536 true chunks chunks 93218397
2 65536 true chunks current 121740
3 32 false bits current 511
3 32 false bits bits 28001
3 32 false chunks current 431
3 32 false chunks chunks 27511
3 32 true bits current 430
3 32 true bits bits 24637
3 32 true chunks current 400
3 32 true chunks chunks 27381
3 64 false bits current 5978
3 64 false bits bits 208198
3 64 false chunks current 5929
3 64 false chunks chunks 40020
3 64 true bits current 5888
3 64 true bits bits 207908
3 64 true chunks current 5899
3 64 true chunks chunks 49202
3 256 false bits current 6079
3 256 false bits bits 1767049
3 256 false chunks current 6069
3 256 false chunks chunks 98426
3 256 true bits current 6060
3 256 true bits bits 1813408
3 256 true chunks current 6059
3 256 true chunks chunks 200297
3 4096 false bits current 12558
3 4096 false bits bits 38678281
3 4096 false chunks current 12498
3 4096 false chunks chunks 1408108
3 4096 true bits current 12469
3 4096 true bits bits 39438088
3 4096 true chunks current 12499
3 4096 true chunks chunks 3425589
3 65536 false bits current 121640
3 65536 false bits bits 3033311756
3 65536 false chunks current 122361
3 65536 false chunks chunks 60985672
3 65536 true bits current 121640
3 65536 true bits bits 3049395326
3 65536 true chunks current 125736
3 65536 true chunks chunks 94386319
Raw
NativeBench.lean
module
/-! Standalone compiled population-count measurements; requires POPCOUNT_NATIVE_SAMPLES. -/
def countBits (n width : Nat) : Nat :=
(List.range width).foldl (fun s i => s + (n.testBit i).toNat) 0
-- The masked 64-bit parallel count used by PrimeCert #156 (Bhavik Mehta).
def wordCount (v : Nat) : Nat :=
let v := v - ((v >>> 1) &&& 0x5555555555555555)
let v := (v &&& 0x3333333333333333) + ((v >>> 2) &&& 0x3333333333333333)
let v := (v + (v >>> 4)) &&& 0x0f0f0f0f0f0f0f0f
((v * 0x0101010101010101) >>> 56) &&& 255
def chunkCount (n width : Nat) : Nat :=
(List.range ((width + 63) / 64)).foldl
(fun acc i => acc + wordCount ((n >>> (64*i)) &&& 0xffffffffffffffff)) 0
public def main : IO Unit := do
let some output ← IO.getEnv "POPCOUNT_NATIVE_SAMPLES" | return
let file ← IO.FS.Handle.mk output .write
for block in [:4] do
for width in [32, 64, 256, 4096, 65536] do
for dense in [false, true] do
let n := if dense then 2^width-1 else 2^(width-1)+1
let expected := if dense then width else 2
for candidate in ["bits", "chunks"] do
let arms := if block % 2 == 0 then [candidate, "current"] else ["current", candidate]
for arm in arms do
let arg ← IO.mkRef n
let start ← IO.monoNanosNow
for _ in [:100] do
let n ← arg.get
let value := if arm == "current" then n.popcount
else if arm == "chunks" then chunkCount n width else countBits n width
if value != expected then throw <| IO.userError "native mismatch"
let stop ← IO.monoNanosNow
file.putStrLn s!"{block},{width},{dense},{candidate},{arm},{stop-start}"
file.flush
Raw
pre-small-broad-kernel-record.json
{
"cpu": 67,
"host": "chungus2",
"load_before": [
5.96240234375,
11.66162109375,
8.5634765625
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_artifact.lean"
],
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_artifact.lean\n",
"load_after": [
5.96240234375,
11.66162109375,
8.5634765625
]
}
Raw
pre-small-broad-kernel-samples.csv
0 128 false previous previous 40450
0 128 false previous current 38738
0 128 true previous previous 29564
0 128 true previous current 31756
0 512 false previous previous 48041
0 512 false previous current 34482
0 512 true previous previous 50064
0 512 true previous current 33630
0 1024 false previous previous 66388
0 1024 false previous current 33049
0 1024 true previous previous 70705
0 1024 true previous current 34011
0 2048 false previous previous 108380
0 2048 false previous current 33359
0 2048 true previous previous 114339
0 2048 true previous current 33500
0 8192 false previous previous 405250
0 8192 false previous current 59979
0 8192 true previous previous 408336
0 8192 true previous current 59168
0 16384 false previous previous 706627
0 16384 false previous current 62172
0 16384 true previous previous 818122
0 16384 true previous current 63615
0 32768 false previous previous 1450470
0 32768 false previous current 69533
0 32768 true previous previous 1656906
0 32768 true previous current 70294
0 131072 false previous previous 6909503
0 131072 false previous current 131615
0 131072 true previous previous 7662089
0 131072 true previous current 133288
0 262144 false previous previous 22032581
0 262144 false previous current 223271
0 262144 true previous previous 19547237
0 262144 true previous current 213106
0 1048576 false previous previous 262932264
0 1048576 false previous current 774037
0 1048576 true previous previous 166652307
0 1048576 true previous current 756521
1 128 false previous current 49984
1 128 false previous previous 45928
1 128 true previous current 39629
1 128 true previous previous 32228
1 512 false previous current 40710
1 512 false previous previous 56253
1 512 true previous current 39118
1 512 true previous previous 56143
1 1024 false previous current 37736
1 1024 false previous previous 72067
1 1024 true previous current 36254
1 1024 true previous previous 77115
1 2048 false previous current 35863
1 2048 false previous previous 112116
1 2048 true previous current 35253
1 2048 true previous previous 124244
1 8192 false previous current 72648
1 8192 false previous previous 376738
1 8192 true previous current 65828
1 8192 true previous previous 411369
1 16384 false previous current 73559
1 16384 false previous previous 765625
1 16384 true previous current 71857
1 16384 true previous previous 838443
1 32768 false previous current 79378
1 32768 false previous previous 1514705
1 32768 true previous current 80830
1 32768 true previous previous 1711457
1 131072 false previous current 153337
1 131072 false previous previous 26274770
1 131072 true previous current 219044
1 131072 true previous previous 8370829
1 262144 false previous current 254387
1 262144 false previous previous 17952643
1 262144 true previous current 284903
1 262144 true previous previous 19246761
1 1048576 false previous current 811142
1 1048576 false previous previous 241255411
1 1048576 true previous current 936548
1 1048576 true previous previous 233356510
2 128 false previous previous 74260
2 128 false previous current 64896
2 128 true previous previous 35202
2 128 true previous current 43104
2 512 false previous previous 56493
2 512 false previous current 42454
2 512 true previous previous 56083
2 512 true previous current 38497
2 1024 false previous previous 74069
2 1024 false previous current 36985
2 1024 true previous previous 77865
2 1024 true previous current 36574
2 2048 false previous previous 113519
2 2048 false previous current 36223
2 2048 true previous previous 122332
2 2048 true previous current 35522
2 8192 false previous previous 379393
2 8192 false previous current 74060
2 8192 true previous previous 414745
2 8192 true previous current 70384
2 16384 false previous previous 755380
2 16384 false previous current 72638
2 16384 true previous previous 833767
2 16384 true previous current 83093
2 32768 false previous previous 1515317
2 32768 false previous current 81741
2 32768 true previous previous 1713691
2 32768 true previous current 83684
2 131072 false previous previous 7304358
2 131072 false previous current 159026
2 131072 true previous previous 7955684
2 131072 true previous current 161229
2 262144 false previous previous 17590817
2 262144 false previous current 275358
2 262144 true previous previous 19094947
2 262144 true previous current 276981
2 1048576 false previous previous 160828154
2 1048576 false previous current 859554
2 1048576 true previous previous 170536025
2 1048576 true previous current 869359
3 128 false previous current 54681
3 128 false previous previous 47541
3 128 true previous current 42804
3 128 true previous previous 32438
3 512 false previous current 14602467
3 512 false previous previous 98095
3 512 true previous current 60861
3 512 true previous previous 66608
3 1024 false previous current 45798
3 1024 false previous previous 82392
3 1024 true previous current 42913
3 1024 true previous previous 87470
3 2048 false previous current 38657
3 2048 false previous previous 114990
3 2048 true previous current 35873
3 2048 true previous previous 124565
3 8192 false previous current 77886
3 8192 false previous previous 421805
3 8192 true previous current 73719
3 8192 true previous previous 426983
3 16384 false previous current 72257
3 16384 false previous previous 783221
3 16384 true previous current 74070
3 16384 true previous previous 854396
3 32768 false previous current 75612
3 32768 false previous previous 1556287
3 32768 true previous current 82443
3 32768 true previous previous 1744275
3 131072 false previous current 153748
3 131072 false previous previous 7487359
3 131072 true previous current 158465
3 131072 true previous previous 7721586
3 262144 false previous current 233025
3 262144 false previous previous 17471560
3 262144 true previous current 276690
3 262144 true previous previous 18753680
3 1048576 false previous current 766216
3 1048576 false previous previous 223616572
3 1048576 true previous current 955227
3 1048576 true previous previous 219511498
Raw
pre-small-kernel-record.json
{
"cpu": 79,
"host": "chungus2",
"load_before": [
15.06103515625,
14.54833984375,
9.08447265625
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab/run_test.sh",
"popcount_artifact.lean"
],
"returncode": 0,
"stdout": "",
"stderr": "++ lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true -Dcompiler.postponeCompile=false popcount_artifact.lean\n",
"load_after": [
14.3349609375,
14.40625,
9.06787109375
]
}
Raw
pre-small-kernel-samples.csv
0 64 false count64 count64 37135
0 64 false count64 current 29363
0 64 false count128 count128 27771
0 64 false count128 current 23324
0 64 false chunks chunks 45207
0 64 false chunks current 22253
0 64 true count64 count64 27280
0 64 true count64 current 23135
0 64 true count128 count128 26369
0 64 true count128 current 21973
0 64 true chunks chunks 40530
0 64 true chunks current 21552
0 256 false count64 count64 61771
0 256 false count64 current 33139
0 256 false count128 count128 38738
0 256 false count128 current 29864
0 256 false chunks chunks 79879
0 256 false chunks current 30015
0 256 true count64 count64 59208
0 256 true count64 current 30626
0 256 true count128 count128 39679
0 256 true count128 current 29514
0 256 true chunks chunks 84966
0 256 true chunks current 29784
0 4096 false count64 count64 640900
0 4096 false count64 current 36214
0 4096 false count128 count128 338461
0 4096 false count128 current 33741
0 4096 false chunks chunks 886173
0 4096 false chunks current 36405
0 4096 true count64 count64 683614
0 4096 true count64 current 35563
0 4096 true count128 count128 379463
0 4096 true count128 current 34061
0 4096 true chunks chunks 927955
0 4096 true chunks current 35663
0 65536 false count64 count64 12029963
0 65536 false count64 current 82943
0 65536 false count128 count128 5895479
0 65536 false count128 current 78517
0 65536 false chunks chunks 15414680
0 65536 false chunks current 78746
0 65536 true count64 count64 12530014
0 65536 true count64 current 80489
0 65536 true count128 count128 6748764
0 65536 true count128 current 77995
0 65536 true chunks chunks 16103591
0 65536 true chunks current 81641
1 64 false count64 current 29003
1 64 false count64 count64 44686
1 64 false count128 current 25467
1 64 false count128 count128 36274
1 64 false chunks current 23194
1 64 false chunks chunks 57195
1 64 true count64 current 26700
1 64 true count64 count64 29383
1 64 true count128 current 23545
1 64 true count128 count128 27331
1 64 true chunks current 22213
1 64 true chunks chunks 46008
1 256 false count64 current 39128
1 256 false count64 count64 62834
1 256 false count128 current 33629
1 256 false count128 count128 42583
1 256 false chunks current 31266
1 256 false chunks chunks 94861
1 256 true count64 current 34311
1 256 true count64 count64 63835
1 256 true count128 current 31767
1 256 true count128 count128 42513
1 256 true chunks current 30575
1 256 true chunks chunks 88971
1 4096 false count64 current 37856
1 4096 false count64 count64 652858
1 4096 false count128 current 38026
1 4096 false count128 count128 343820
1 4096 false chunks current 35332
1 4096 false chunks chunks 901066
1 4096 true count64 current 42292
1 4096 true count64 count64 702101
1 4096 true count128 current 39619
1 4096 true count128 count128 390319
1 4096 true chunks current 36584
1 4096 true chunks chunks 945842
1 65536 false count64 current 86057
1 65536 false count64 count64 12721417
1 65536 false count128 current 116432
1 65536 false count128 count128 6046303
1 65536 false chunks current 99087
1 65536 false chunks chunks 16363377
1 65536 true count64 current 114610
1 65536 true count64 count64 13158255
1 65536 true count128 current 114059
1 65536 true count128 count128 6940168
1 65536 true chunks current 103974
1 65536 true chunks chunks 16848266
2 64 false count64 count64 59038
2 64 false count64 current 41492
2 64 false count128 count128 44345
2 64 false count128 current 27131
2 64 false chunks chunks 69984
2 64 false chunks current 25398
2 64 true count64 count64 29564
2 64 true count64 current 25738
2 64 true count128 count128 27751
2 64 true count128 current 22814
2 64 true chunks chunks 46740
2 64 true chunks current 22963
2 256 false count64 count64 68621
2 256 false count64 current 41141
2 256 false count128 count128 42954
2 256 false count128 current 33970
2 256 false chunks chunks 89793
2 256 false chunks current 31978
2 256 true count64 count64 63023
2 256 true count64 current 34071
2 256 true count128 count128 43565
2 256 true count128 current 31767
2 256 true chunks chunks 89183
2 256 true chunks current 31447
2 4096 false count64 count64 654340
2 4096 false count64 current 40270
2 4096 false count128 count128 344721
2 4096 false count128 current 36424
2 4096 false chunks chunks 902778
2 4096 false chunks current 41261
2 4096 true count64 count64 705365
2 4096 true count64 current 41512
2 4096 true count128 count128 391891
2 4096 true count128 current 37015
2 4096 true chunks chunks 947275
2 4096 true chunks current 40660
2 65536 false count64 count64 12403847
2 65536 false count64 current 104064
2 65536 false count128 count128 6048567
2 65536 false count128 current 96142
2 65536 false chunks chunks 15958397
2 65536 false chunks current 98135
2 65536 true count64 count64 14493896
2 65536 true count64 current 135310
2 65536 true count128 count128 7392329
2 65536 true count128 current 129772
2 65536 true chunks chunks 18090948
2 65536 true chunks current 137214
3 64 false count64 current 33901
3 64 false count64 count64 51386
3 64 false count128 current 26870
3 64 false count128 count128 44306
3 64 false chunks current 24496
3 64 false chunks chunks 76193
3 64 true count64 current 28322
3 64 true count64 count64 30646
3 64 true count128 current 24136
3 64 true count128 count128 28192
3 64 true chunks current 22964
3 64 true chunks chunks 48152
3 256 false count64 current 43184
3 256 false count64 count64 64576
3 256 false count128 current 34321
3 256 false count128 count128 44436
3 256 false chunks current 31357
3 256 false chunks chunks 91696
3 256 true count64 current 41271
3 256 true count64 count64 64946
3 256 true count128 current 32388
3 256 true count128 count128 43133
3 256 true chunks current 31276
3 256 true chunks chunks 90965
3 4096 false count64 current 39459
3 4096 false count64 count64 673008
3 4096 false count128 current 42403
3 4096 false count128 count128 354526
3 4096 false chunks current 36383
3 4096 false chunks chunks 916960
3 4096 true count64 current 45437
3 4096 true count64 count64 731314
3 4096 true count128 current 40109
3 4096 true count128 count128 399522
3 4096 true chunks current 37155
3 4096 true chunks chunks 958271
3 65536 false count64 current 92527
3 65536 false count64 count64 13064256
3 65536 false count128 current 108801
3 65536 false count128 count128 6270065
3 65536 false chunks current 105476
3 65536 false chunks chunks 17182992
3 65536 true count64 current 120519
3 65536 true count64 count64 13705196
3 65536 true count128 current 119147
3 65536 true count128 count128 7096119
3 65536 true chunks current 109823
3 65536 true chunks chunks 17337120
Raw
run.py
#!/usr/bin/env python3
"""Run the standalone kernel or compiled benchmark using Lean's test harness."""
import argparse
import fcntl
import json
import os
from pathlib import Path
import socket
import subprocess
import tempfile
def pin():
if not hasattr(os, 'sched_getaffinity'):
return None, None
allowed = sorted(os.sched_getaffinity(0))
start = os.getpid() % len(allowed)
for cpu in allowed[start:] + allowed[:start]:
lock = open(Path(tempfile.gettempdir()) / f'powmod-tuning-{cpu}.lock', 'a')
try:
fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB)
except BlockingIOError:
lock.close()
continue
os.sched_setaffinity(0, {cpu})
return cpu, lock
raise SystemExit('All affinity CPUs reserved by other timing runners')
def main():
ap = argparse.ArgumentParser(description=__doc__)
ap.add_argument('--repo', required=True, type=Path)
ap.add_argument('--out', required=True, type=Path)
ap.add_argument('--kind', choices=['kernel', 'native'], required=True)
args = ap.parse_args()
repo, out = args.repo.resolve(), args.out.resolve()
out.mkdir(parents=True, exist_ok=True)
sample = out / f'{args.kind}-samples.csv'
record_path = out / f'{args.kind}-record.json'
if sample.exists() or record_path.exists():
raise SystemExit('Choose a new output directory; completed runs are retained')
pile = 'elab' if args.kind == 'kernel' else 'compile'
name = 'popcount_artifact.lean'
target = repo / 'tests' / pile / name
marker = target.with_name(name + '.no_interpret')
if target.exists() or marker.exists():
raise SystemExit(f'Refusing to overwrite {target} or its marker')
source = Path(__file__).with_name('KernelBench.lean' if args.kind == 'kernel' else 'NativeBench.lean')
cpu, lock = pin()
env = os.environ.copy()
env['POPCOUNT_SAMPLES' if args.kind == 'kernel' else 'POPCOUNT_NATIVE_SAMPLES'] = str(sample)
cmd = ['tests/with_stage1_test_env.sh', f'tests/{pile}/run_test.sh', name]
record = {'cpu': cpu, 'host': socket.gethostname(), 'load_before': os.getloadavg(), 'command': cmd}
try:
target.write_bytes(source.read_bytes())
if args.kind == 'native':
marker.touch()
p = subprocess.run(cmd, cwd=repo, env=env, capture_output=True, text=True)
record.update(returncode=p.returncode, stdout=p.stdout, stderr=p.stderr,
load_after=os.getloadavg())
record_path.write_text(json.dumps(record, indent=2))
print(record_path)
raise SystemExit(p.returncode)
finally:
target.unlink(missing_ok=True)
marker.unlink(missing_ok=True)
if __name__ == '__main__':
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment