Henrik Böving: Automated Bit-Level Reasoning in Lean 4

Stream: Lean Together 2025

[Jireh Loreaux]

Discussion thread for this talk.

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/Q1LDavBJ94A

[Kevin Buzzard]

A question I asked in the chat during the talk: where did the scary 1844... constant go (you can see it at about 4 minutes in, now I've finally got the talk online (sorry for the delay))

[Henrik Böving]

The short answer is that one of the rewrite rule saw it was a magic value and removed it for us. Namely if you view the binary representation this is just:

0b1111111111111111111111111111111111111111111111111111111111111111

and
x - y is equivalent to x + ~~~y + 1 so the rewriter reordered this into

18446744073709551615 + 1 + ~~~y

and 18446744073709551615 + 1 = 0

[Henrik Böving]

The preprocessing is really one of the things that makes bitwuzla shine so much, you can take a look at the bitvec related rules in the comments in this file: https://github.com/bitwuzla/bitwuzla/blob/main/src/rewrite/rewrites_bv.cpp they have ton's of fancy rules.

[Jason Rute]

In your talk you mentioned there were a bunch of rules from another system you didn’t implement yet. What is the major barrier? Is it translating them to Lean or is it proving them?

[Henrik Böving]

Proving the Bitwuzla rules just takes a while as they are not trivial

[Vlad Tsyrklevich]

Is there a ranking of which ones are most effective, e.g. reducing benchmark proving times or some other measure? Just thinking that this may be a fun thing for others to contribute to, if it's cleanly modularized and doesn't get in your way somehow

[Vlad Tsyrklevich]

(I've spent enough time playing with bit flipping tricks that this seems like it could be fun)

[Henrik Böving]

Bitwuzla splits them into 3 levels iirc. I do have a google sheet laying around somewhere that I can dig out where I already tried a best effort translation of most of them to Lean statements (though not proofs) that I can post here if you want to take a look

[Vlad Tsyrklevich]

Yeah, I'd be curious. And since I'm not familiar with where to look, a reference to where the existing translations for the tactic are would also be useful.

[Henrik Böving]

https://docs.google.com/spreadsheets/d/1QFgtrqc9IXtYn0sa9gkmteUhIKTsOo-idYoeKx6nj-I/edit?gid=0#gid=0

[Henrik Böving]

right so this is the list of rules in general, the middle column is filled out if we have ported them already. There's also a bit of a consideration to be had here with respect to the simp normal form of the bv_normalize simp set so this stuff is not necessarily translatable one to one to production ruels in bv_decid but it's at least the correct statements even though we potentially need them in a slightly different but equivalent form.

The implementation currently dwells in https://github.com/leanprover/lean4/tree/master/src/Std/Tactic/BVDecide/Normalize and https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean

[Kevin Buzzard]

Is the plan to port them all? Is this the sort of task which can be given to a student?

[Henrik Böving]

We definitely want to have as many as possible. Its not a task that can be given to a student just like that because there are some things to consider when porting a rule but with a bit of communication definitely.

[Vlad Tsyrklevich]

I think some of the rules would also be nice in greater generality, e.g. there are lots of variants with unary operators ! and ~~~ applied, but probably we should try to match against all unary operators if we could. Of course, for this use case, that can be ignored, but I'm just thinking that I don't think Lean allows us to easily match against all unary operators, right?

[Henrik Böving]

The vast majorit of lemmas that are used don't rely on something being a unary operator but specifically being the not operator for bool/bitvec respectively.

[Vlad Tsyrklevich]

Yes, what I mean to say, is it that for bv_decide it is enough to have those rules for NOT, but given that some of these rewrite rules are actually nice to have more generally, it would be nice if we could apply them to the wider set of unary operators that you encounter elsewhere as well. But I don't think there's a way to generalize for all unary operators

[Vlad Tsyrklevich]

Anyways, I've gone through and saved some notes about some lemmas I'd like to try to contribute. I'll give them a shot and start a thread elsewhere when I have something to report.