feat(lean): new setup for bv_decide

[abentkamp]

This PR provides a new setup for using bv_decide and applies it to the lean_barrett example. Instead of using mvcgen and then bv_decide, we apply bv_decide directly. To be able to do that, we create a set of simplification rules (labelled hax_bv_decide) that simplify a Hoare triple goal into a form that bv_decide can handle.

To use the new setup:

• unfold all functions that are not part of the library
• then invoke hax_bv_decide or possibly hax_bv_decide (timeout := 60) for a longer timeout.

For debugging:

• unfold all functions that are not part of the library
• invoke simp only [hax_bv_decide] at *; bv_decide (which is what hax_bv_decide does internally)
• If after simp only [hax_bv_decide] at * there are still RustM-related definitions remaining in the goal, you will likely have to create more simp lemmas tagged with #[hax_bv_decide] to make them go away.

[karthikbhargavan]

Since this is meant to be exemplary