Cool! And somewhat scary, shifting the work of the human to verify and understand machine-generated code.
Also, obligatory nitpick: the example naive C implementation uses bitwise AND (&) when it means boolean AND (&&), the line that starts:
return
(n00 == n01) & (n00 == n02)
This is bad, since bitwise AND in C isn't short-circuiting. It's also bad since it's semantically weird, the things being AND:ed are obviously truth values (the results of lots of == operators), which are not necessarily the same as "raw" bits.
You're right, at least in that == produces 0 or 1. I was sure it had been "ported" to produce _Bool when that was added (which then of course automatically converts to 0 or 1 as needed), but that seems not to be the case.
I still think the ANDs should be boolean (i.e. &&) though, but perhaps your hunch about branchlessness is right.
Also, obligatory nitpick: the example naive C implementation uses bitwise AND (&) when it means boolean AND (&&), the line that starts:
This is bad, since bitwise AND in C isn't short-circuiting. It's also bad since it's semantically weird, the things being AND:ed are obviously truth values (the results of lots of == operators), which are not necessarily the same as "raw" bits.