sbp
Direct compilation for BIP / view for Data.Bits?
Might be quite useful to link Bip/Bin/Biz to un/signed machine words, perhaps by making a covering function for Data.Bits.
One thing that we definitely need for this to happen are the bounded versions (the analogue of Prelude's Fin), so that we could fix the byte length. This however will definitely mess up the arithmetics, wonder if Coq has some solution here? One way out would be to define it as modular arithmetics, just have to figure out if real-world bytes behave like that :)
This looks relevant: https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v
https://github.com/maximedenes/native-coq/tree/master/theories/Numbers also looks fitting
As well as https://github.com/artart78/coq-bits It even has an accompanying paper https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/coq-bitset/flops/paper.pdf