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
