search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
84 stars 18 forks source link

Concretization tactic #24

Closed Vtec234 closed 2 years ago

Vtec234 commented 2 years ago

The purpose of concretize is to beat polymorphic terms into a sufficiently FOL-like monomorphic shape that smt can then deal with them. For some simple examples, see the polyAdd Boolean circuits at the end which the tactic instantiates at a concrete width. The tactic is in an early state and fails often, but PRing now as it was at least able to concretize one goal I care about. I would appreciate if you tried it on some examples and looked at whether the output is smt-friendly enough.

abdoo8080 commented 2 years ago

I would appreciate if you tried it on some examples and looked at whether the output is smt-friendly enough.

Yes! I just tried the example you showed and I think it is possible (maybe easy?) to directly translate it into an SMT query!

To get a better idea, I think we should define a subset of the BitVec interface in Lean and translate it into SMT to have a "fully" working example.

Vtec234 commented 2 years ago

Also, I am going to assume that this is idiomatic metaprogramming code and learn from it.

😅 to an extent, but there are many hacks. I haven't really figured out a clean way to implement the whole expression traversal. Maybe a conv traversal would be better, but for now it works, so I won't change it unless needed.

To get a better idea, I think we should define a subset of the BitVec interface in Lean and translate it into SMT to have a "fully" working example.

Oh yes, I have a full definition here and some functions that use it in GF2BV.lean - e.g. polyMul there should concretize to an smt-compatible expression. I didn't want to upstream the BV interface until it definitely works. We could either add it here or to mathlib4 and depend on mathlib4. I am slightly in favour of the latter as then the community can use them, although it is slightly more across-repo churn.

abdoo8080 commented 2 years ago

I see... In that case, we only need the translation to SMT. We don't need to depend on the source code. Just the signature should be enough for testing purposes (as you already did in this PR).