BitVec: popcount and parity?

Stream: lean4

[François G. Dorais]

Just wondering if there are plans to support popcount and/or parity for BitVec. They are not essential but they are common enough to even get hardware support on some architectures.

[Henrik Böving]

Currently the BitVec API is modelled almost 1:1 after what is found in SMTLIB (which does notably not have a popcount/parity notion afaik). That being said I believe having an RFC that proposes the inclusion of these functions would be sensible, here are a bunch of things to consider:

• should they be defined in terms of other BitVec operations or, like most other current functionality, in terms of the toNat/toInt semantics?
• what about signed/unsigned versions? Does the distinction exists practically or does everyone just assume unsigned?
• should we pull them through to UIntX/IntX? Potentially along with an efficient C implementation?

• We need to support them in bv_decide, this can mean two things:

  • providing lemmas that reduce them to already exists BitVec operations
  • providing lemmas that describe efficient circuits that we can implement in bv_decide
    In particular we can of course also go two steps here, first providing unfolding lemmas and then at a later point integrate with more optimized circuits into bv_decide.

• How do they interact with the rest of the BitVec API? Do we want e.g. lemmas about what happens when you ||| when you &&& when you +?

[François G. Dorais]

Thanks! Before I'm ready to PR to core, I'll incubate in Batteries and answer these questions there.