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
StylusNeat! I feel as though I should try to learn lean one of these days.
Previously I've used CBMC to prove the equivalence of these two C implementations of popcnt (under the assumption that unsigned is uint32_t or smaller, I guess)
int pop(unsigned x) {
x = x - ((x >> 1) & 0x55555555);
x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
x = (x + (x >> 4)) & 0x0F0F0F0F;
x = x + (x >> 8);
x = x + (x >> 16);
return x & 0x0000003F;
}
inline int proof_popcnt(uint64_t u)
{
int r = 0;
for(int i=0; i<64; i++)
if(u & (1ull << i)) r ++;
return r;
}
using code like
int main() {
unsigned u = nondet_unsigned();
int i = pop(u);
assert(i == proof_popcnt(u));
}
but when the assertion holds it provides no insight into why, and when CBMC fails to prove or disprove an assertion in a reasonable length of time, it's not clear to me how to guide it.
@stylus yeah... I think the future of verified software is less "write it in C/C++/Rust and then prove it correct" and more "write it in Lean or some other mathematical specification language and then extract an implementation"
George Pîrlea@regehr @stylus I'd one-up this and say that's the future of software period, not just verified software.
It will be a 10+ year transition, but people will increasingly move to writing software in languages with built-in support for meta-programming & verification. A language like Rust already feels crippling. If it all compiles down to LLVM anyway and you (can) get good performance, why would you use a less powerful language? Even if you don't intend to verify, having the option to is good.
@regehr @stylus And having external verification tools (Verus, CBMC, etc.) doesn't cut it, in terms of user experience, in my view. I think verification has to be embedded in the language for it to not be a total pain, as per Ranjit Jhala: https://www.youtube.com/watch?v=elHEye-nau4
Ranjit Jhala - Language-Integrated Verification
ash
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 :)
Andrew Furrow@regehr I love your colors