John Regehrwow so glad I can extract this minimal and efficient C++ from my verified Kernighan popcount in Lean 😅
https://gist.github.com/regehr/3461027009efbe9452d8a5c343174443
after much struggling I got the code below, which turns into the instructions that I wanted! but that's as much a testament to modern compilers as it is to Lean :)
here's the verified popcount with efficient extracted code if anyone's curious https://github.com/regehr/lean4-popcount/tree/main
Stephen Hoffman@regehr In a conversation about some processor architectural extensions in development, asking about the motivations for the instruction additions including the popcount instruction: “the spooks wanted it.”
Cryptography, presumably. But there are some answers I’d rather not know.
Profiling for which apps and which sites used what instructions and how often was always interesting.
@HoffmanLabs yeah, "the NSA instruction" :)
https://groups.google.com/g/comp.arch/c/UXEi7G6WHuU/m/Z2z7fC7Xhr8J
which seems a bit quaint at this point :)