Skip to content

Instantly share code, notes, and snippets.

@kim-em

kim-em/KernelBench.lean

Last active September 16, 2026 04:51
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save kim-em/f1c14186fd455e84c514a37c9721c1be to your computer and use it in GitHub Desktop.
Download ZIP
Nat popcount: compiled runtime and fresh kernel checks versus bit and SWAR counts
Raw
README.md

Nat population count: kernel and compiled runtime evidence

This artifact measures the initial kernel-primitive implementation at 134218dd34. The current PR uses a transparent Lean definition; its measurements and reproducible drivers are separate.

On the popcount PR branch, copy KernelBench.lean to tests/elab_bench/popcount_bench.lean and NativeBench.lean to tests/compile/popcount_bench.lean. Create an empty tests/compile/popcount_bench.lean.no_interpret_test so the compile test executes only the C-compiled binary, then run:

POPCOUNT_SAMPLES=/tmp/kernel.csv tests/with_stage1_test_env.sh tests/elab_bench/run_bench.sh popcount_bench.lean
POPCOUNT_NATIVE_SAMPLES=/tmp/native.csv tests/with_stage1_test_env.sh tests/compile/run_test.sh popcount_bench.lean

Both drivers use four adjacent AB/BA blocks on the same shared host. Dense inputs are 2^width−1; sparse inputs contain the highest and lowest bits. CSV fields: block,width,dense,reference arm,measured arm,nanoseconds. Runtime samples contain 100 calls; kernel samples contain one fresh Kernel.check, excluding imports, input construction, and expected-result calculation. Wrong-result controls are required to fail. The runtime driver is compiled to C and linked by Lean's standard compile-test harness, not timed through the interpreter.

bits is the original bit-by-bit counting recurrence. chunks adapts the masked 64-bit parallel count from Bhavik Mehta's PrimeCert #156, applying it only to masked words and summing into Nat (counts above 255 do not wrap). These are comparison implementations, not exported APIs. The new primitive scans stored limbs. kernel-record.json and native-record.json retain CPU affinity and host load; all completed samples are included.

The earlier samples.csv/record.json run is retained. Its native100 rows ran in elaborator evaluation and are not compiled-runtime evidence; use native-samples.csv for that comparison.

Raw
kernel-record.json
{
"cpu": 93,
"host": "chungus2",
"load_before": [
23.47119140625,
10.66162109375,
11.1904296875
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab_bench/run_bench.sh",
"nat_popcount.lean"
],
"returncode": 0,
"stdout": "",
"stderr": "++ /home/kim/worktrees/lean4/lean4-nat-popcount/tests/measure.py -t elab/nat_popcount -o nat_popcount.lean.measurements.jsonl -a -d -- lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true nat_popcount.lean\n",
"load_after": [
23.47119140625,
10.66162109375,
11.1904296875
]
}
Raw
kernel-samples.csv
0 64 false bits bits 913174
0 64 false bits primitive 5749
0 64 false chunks chunks 75983
0 64 false chunks primitive 4417
0 64 true bits bits 883970
0 64 true bits primitive 5078
0 64 true chunks chunks 73759
0 64 true chunks primitive 4266
0 256 false bits bits 3578326
0 256 false bits primitive 5568
0 256 false chunks chunks 169512
0 256 false chunks primitive 4316
0 256 true bits bits 3582172
0 256 true bits primitive 5348
0 256 true chunks chunks 169121
0 256 true chunks primitive 4267
0 4096 false bits bits 63599398
0 4096 false bits primitive 7281
0 4096 false chunks chunks 2048838
0 4096 false chunks primitive 5418
0 4096 true bits bits 62469212
0 4096 true bits primitive 6489
0 4096 true chunks chunks 2102728
0 4096 true chunks primitive 5457
1 64 false bits primitive 5078
1 64 false bits bits 944621
1 64 false chunks primitive 6941
1 64 false chunks chunks 90334
1 64 true bits primitive 5358
1 64 true bits bits 901807
1 64 true chunks primitive 6189
1 64 true chunks chunks 85897
1 256 false bits primitive 5258
1 256 false bits bits 3576763
1 256 false chunks primitive 7792
1 256 false chunks chunks 188700
1 256 true bits primitive 5688
1 256 true bits bits 3574801
1 256 true chunks primitive 7691
1 256 true chunks chunks 195880
1 4096 false bits primitive 5728
1 4096 false bits bits 65595348
1 4096 false chunks primitive 22203
1 4096 false chunks chunks 2196657
1 4096 true bits primitive 9264
1 4096 true bits bits 65964735
1 4096 true chunks primitive 21341
1 4096 true chunks chunks 2237318
2 64 false bits bits 965262
2 64 false bits primitive 7802
2 64 false chunks chunks 95932
2 64 false chunks primitive 5248
2 64 true bits bits 907446
2 64 true bits primitive 6459
2 64 true chunks chunks 86949
2 64 true chunks primitive 4878
2 256 false bits bits 3593278
2 256 false bits primitive 7982
2 256 false chunks chunks 191884
2 256 false chunks primitive 5378
2 256 true bits bits 3585667
2 256 true bits primitive 7932
2 256 true chunks chunks 195069
2 256 true chunks primitive 5247
2 4096 false bits bits 83656870
2 4096 false bits primitive 35402
2 4096 false chunks chunks 2697220
2 4096 false chunks primitive 23856
2 4096 true bits bits 85236692
2 4096 true bits primitive 29524
2 4096 true chunks chunks 2354582
2 4096 true chunks primitive 13490
3 64 false bits primitive 5748
3 64 false bits bits 978191
3 64 false chunks primitive 6840
3 64 false chunks chunks 94080
3 64 true bits primitive 5738
3 64 true bits bits 906985
3 64 true chunks primitive 6049
3 64 true chunks chunks 86459
3 256 false bits primitive 5469
3 256 false bits bits 3647389
3 256 false chunks primitive 8012
3 256 false chunks chunks 191314
3 256 true bits primitive 5488
3 256 true bits bits 3598837
3 256 true chunks primitive 8002
3 256 true chunks chunks 192956
3 4096 false bits primitive 5708
3 4096 false bits bits 69153094
3 4096 false chunks primitive 22863
3 4096 false chunks chunks 2247122
3 4096 true bits primitive 10896
3 4096 true bits bits 65765470
3 4096 true chunks primitive 20701
3 4096 true chunks chunks 2247873
Raw
KernelBench.lean
module
import Lean
meta import Lean
/-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES.
The old BitVec bit loop and the Nat primitive 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 v := v - ((v >>> 1) &&& 0x5555555555555555)
let v := (v &&& 0x3333333333333333) + ((v >>> 2) &&& 0x3333333333333333)
let v := (v + (v >>> 4)) &&& 0x0f0f0f0f0f0f0f0f
((v * 0x0101010101010101) >>> 56) &&& 255
@[expose] public def chunkCount (n : Nat) : Nat → Nat :=
Nat.rec 0 (fun i acc => acc + wordCount ((n >>> (64*i)) &&& 0xffffffffffffffff))
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] 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 == "primitive" 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 ["bits", "chunks"] do
for arm in (if block % 2 == 0 then [candidate, "primitive"] else ["primitive", 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": 84,
"host": "chungus2",
"load_before": [
5.16015625,
6.24072265625,
11.71484375
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/compile/run_test.sh",
"popcount_bench.lean"
],
"returncode": 0,
"stdout": "Compiling and executing lean file\n",
"stderr": "++ ./popcount_bench.lean.out\n",
"load_after": [
5.287109375,
6.18701171875,
11.55126953125
]
}
Raw
native-samples.csv
0 64 false bits bits 226386
0 64 false bits primitive 8863
0 64 false chunks chunks 52488
0 64 false chunks primitive 6099
0 64 true bits bits 209781
0 64 true bits primitive 6019
0 64 true chunks chunks 47900
0 64 true chunks primitive 6100
0 256 false bits bits 1771416
0 256 false bits primitive 6400
0 256 false chunks chunks 97935
0 256 false chunks primitive 6380
0 256 true bits bits 1791116
0 256 true bits primitive 6239
0 256 true chunks chunks 191233
0 256 true chunks primitive 6189
0 4096 false bits bits 38457699
0 4096 false bits primitive 12930
0 4096 false chunks chunks 1369090
0 4096 false chunks primitive 12749
0 4096 true bits bits 39007174
0 4096 true bits primitive 12799
0 4096 true chunks chunks 3237410
0 4096 true chunks primitive 12749
0 65536 false bits bits 2925946544
0 65536 false bits primitive 122992
0 65536 false chunks chunks 57914878
0 65536 false chunks primitive 122051
0 65536 true bits bits 3026532625
0 65536 true bits primitive 122813
0 65536 true chunks chunks 91554363
0 65536 true chunks primitive 122462
1 64 false bits primitive 6039
1 64 false bits bits 205826
1 64 false chunks primitive 5929
1 64 false chunks chunks 39027
1 64 true bits primitive 5758
1 64 true bits bits 204784
1 64 true chunks primitive 5969
1 64 true chunks chunks 47460
1 256 false bits primitive 5918
1 256 false bits bits 1759168
1 256 false chunks primitive 6229
1 256 false chunks chunks 97695
1 256 true bits primitive 5889
1 256 true bits bits 1778076
1 256 true chunks primitive 5909
1 256 true chunks chunks 191665
1 4096 false bits primitive 12429
1 4096 false bits bits 38264022
1 4096 false chunks primitive 12688
1 4096 false chunks chunks 1429650
1 4096 true bits primitive 12378
1 4096 true bits bits 38784834
1 4096 true chunks primitive 12759
1 4096 true chunks chunks 3245021
1 65536 false bits primitive 122151
1 65536 false bits bits 3012089367
1 65536 false chunks primitive 122913
1 65536 false chunks chunks 60551728
1 65536 true bits primitive 122251
1 65536 true bits bits 3016428157
1 65536 true chunks primitive 124664
1 65536 true chunks chunks 92648497
2 64 false bits bits 215630
2 64 false bits primitive 5989
2 64 false chunks chunks 40259
2 64 false chunks primitive 6089
2 64 true bits bits 217012
2 64 true bits primitive 6119
2 64 true chunks chunks 48582
2 64 true chunks primitive 6109
2 256 false bits bits 1811245
2 256 false bits primitive 6350
2 256 false chunks chunks 98236
2 256 false chunks primitive 6230
2 256 true bits bits 1827319
2 256 true bits primitive 6289
2 256 true chunks chunks 194859
2 256 true chunks primitive 6270
2 4096 false bits bits 38756733
2 4096 false bits primitive 12669
2 4096 false chunks chunks 1430170
2 4096 false chunks primitive 12759
2 4096 true bits bits 39507887
2 4096 true bits primitive 12819
2 4096 true chunks chunks 3299843
2 4096 true chunks primitive 12809
2 65536 false bits bits 2984894731
2 65536 false bits primitive 122732
2 65536 false chunks chunks 60786566
2 65536 false chunks primitive 121951
2 65536 true bits bits 3022216502
2 65536 true bits primitive 122631
2 65536 true chunks chunks 100184920
2 65536 true chunks primitive 146237
3 64 false bits primitive 9284
3 64 false bits bits 345522
3 64 false chunks primitive 6820
3 64 false chunks chunks 67270
3 64 true bits primitive 9284
3 64 true bits bits 313815
3 64 true chunks primitive 9324
3 64 true chunks chunks 82222
3 256 false bits primitive 9975
3 256 false bits bits 2143338
3 256 false chunks primitive 6190
3 256 false chunks chunks 101901
3 256 true bits primitive 5919
3 256 true bits bits 1741962
3 256 true chunks primitive 6239
3 256 true chunks chunks 198083
3 4096 false bits primitive 12358
3 4096 false bits bits 37663792
3 4096 false chunks primitive 12359
3 4096 false chunks chunks 1394417
3 4096 true bits primitive 12318
3 4096 true bits bits 38770644
3 4096 true chunks primitive 12659
3 4096 true chunks chunks 3349396
3 65536 false bits primitive 121781
3 65536 false bits bits 3018237499
3 65536 false chunks primitive 122342
3 65536 false chunks chunks 61527024
3 65536 true bits primitive 121840
3 65536 true bits bits 3027340072
3 65536 true chunks primitive 122562
3 65536 true chunks chunks 98462877
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 [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, "primitive"] else ["primitive", 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 == "primitive" 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
record.json
{
"cpu": 12,
"host": "chungus2",
"load_before": [
4.607421875,
7.16650390625,
13.1337890625
],
"command": [
"tests/with_stage1_test_env.sh",
"tests/elab_bench/run_bench.sh",
"nat_popcount.lean"
],
"returncode": 0,
"stdout": "nat_popcount.lean:9:2-9:8: warning: Redundant `[expose]` attribute, it is meaningful on public definitions only\n",
"stderr": "++ /home/kim/worktrees/lean4/lean4-nat-popcount/tests/measure.py -t elab/nat_popcount -o nat_popcount.lean.measurements.jsonl -a -d -- lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true nat_popcount.lean\n",
"load_after": [
4.63916015625,
7.13037109375,
13.08984375
]
}
Raw
samples.csv
kernel 0 64 false false 925632
native100 0 64 false false 1177546
kernel 0 64 false true 6179
native100 0 64 false true 27511
kernel 0 64 true false 901306
native100 0 64 true false 1110286
kernel 0 64 true true 5318
native100 0 64 true true 27461
kernel 0 256 false false 3594720
native100 0 256 false false 5318674
kernel 0 256 false true 5368
native100 0 256 false true 25017
kernel 0 256 true false 3583763
native100 0 256 true false 5347438
kernel 0 256 true true 5198
native100 0 256 true true 25077
kernel 0 4096 false false 63955884
native100 0 4096 false false 96707288
kernel 0 4096 false true 7141
native100 0 4096 false true 34361
kernel 0 4096 true false 63414381
native100 0 4096 true false 94872658
kernel 0 4096 true true 6529
native100 0 4096 true true 32709
kernel 1 64 false true 5799
native100 1 64 false true 25067
kernel 1 64 false false 1004079
native100 1 64 false false 1111779
kernel 1 64 true true 8372
native100 1 64 true true 25318
kernel 1 64 true false 927214
native100 1 64 true false 1114012
kernel 1 256 false true 7581
native100 1 256 false true 25428
kernel 1 256 false false 3664433
native100 1 256 false false 5310063
kernel 1 256 true true 8653
native100 1 256 true true 25378
kernel 1 256 true false 3627307
native100 1 256 true false 5333057
kernel 1 4096 false true 8162
native100 1 4096 false true 32117
kernel 1 4096 false false 68784102
native100 1 4096 false false 94901110
kernel 1 4096 true true 33920
native100 1 4096 true true 33720
kernel 1 4096 true false 69471260
native100 1 4096 true false 95940440
kernel 2 64 false false 1032671
native100 2 64 false false 1126530
kernel 2 64 false true 13139
native100 2 64 false true 39168
kernel 2 64 true false 926273
native100 2 64 true false 1124787
kernel 2 64 true true 7211
native100 2 64 true true 24586
kernel 2 256 false false 3688608
native100 2 256 false false 5338104
kernel 2 256 false true 8753
native100 2 256 false true 25478
kernel 2 256 true false 3644763
native100 2 256 true false 5368629
kernel 2 256 true true 8422
native100 2 256 true true 25678
kernel 2 4096 false false 64461844
native100 2 4096 false false 93829281
kernel 2 4096 false true 29714
native100 2 4096 false true 32187
kernel 2 4096 true false 63510554
native100 2 4096 true false 98848242
kernel 2 4096 true true 21162
native100 2 4096 true true 31677
kernel 3 64 false true 6479
native100 3 64 false true 23935
kernel 3 64 false false 1004229
native100 3 64 false false 1174421
kernel 3 64 true true 9103
native100 3 64 true true 24056
kernel 3 64 true false 922067
native100 3 64 true false 1176985
kernel 3 256 false true 7050
native100 3 256 false true 24195
kernel 3 256 false false 3825622
native100 3 256 false false 5547514
kernel 3 256 true true 11006
native100 3 256 true true 29434
kernel 3 256 true false 3635690
native100 3 256 true false 5602446
kernel 3 4096 false true 9163
native100 3 4096 false true 30975
kernel 3 4096 false false 65361128
native100 3 4096 false false 94539033
kernel 3 4096 true true 23335
native100 3 4096 true true 31947
kernel 3 4096 true false 66491714
native100 3 4096 true false 96612428
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment