Direct compilation for BIP / view for Data.Bits?

[clayrat]

Might be quite useful to link Bip/Bin/Biz to un/signed machine words, perhaps by making a covering function for Data.Bits.

[sbp]

Agreed, and this is something that I can work on.

[clayrat]

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 :)

[clayrat]

This looks relevant: https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

[clayrat]

https://github.com/maximedenes/native-coq/tree/master/theories/Numbers also looks fitting

[clayrat]

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