RFC: Non-branching `Bool` implementations for `not`, `xor` and `toNat`

Proposal

The common Bool operations ! (Bool.not) and ^^ (Bool.xor) should be compiled to non-branching code for efficiency. Bool.toNat should also be essentially a no-op for compilation as detailed below.

The other basic Bool operations && (Bool.and) and || (Bool.or) are compiled to branching code. This is to ensure that the operations short-cut (e.g. if p evaluates to false then p && q doesn't evaluate q and immediately returns false). Note that they are also [macro_inline] to allow for further short-cutting optimizations.

The operations ! (Bool.not) and ^^ (Bool.xor) have no meaningful short-cutting behavior. Since Bool is internally represented as a UInt8 scalar value (tagged or untagged, depending on context), simple non-branching operations are available for compilation purposes (e.g. Bool.xor is the same as UInt8.xor and Bool.not is the same as UInt8.xor 1).

Right now, Bool.toUInt8 is a no-op (ignoring tagged/untagged representations) since Bool is internally represented as UInt8. So (Bool.toUInt8 x).toNat is non-branching. However, Bool.toNat x is implemented using cond, which leads to branching code and is less efficient at runtime.

Note that these issues are for compilation only. The branching definitions are almost surely better for verification in the kernel.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by tracing the compiler handling of Bool.not, Bool.xor, Bool.toNat, and Bool.toUInt8, comparing the current branching behavior with the proposal. Verify that not and xor compile to non-branching operations and that toNat is effectively a no-op, while preserving the existing short-circuiting behavior of and and or and the kernel-friendly definitions.