Verified Bit Hacks

A growing reference of low-level tricks and optimizations with machine-checked proofs (Coq/Rocq).
Use the search page, browse by tags, or scan the catalog below.

Tags

• bitcount
• float
• integer
• popcount

Catalog

float

• Fast Division — proof of faster division [float]

bitcount

• Kernighan’s Bitcount — Count set bits by clearing the lowest 1-bit. [bitcount, popcount, integer]