Email Gateway (Sep 28 2023 at 11:21): Email Gateway (Sep 28 2023 at 11:21):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
We are working on a proof that makes use of the HOL-Word finite machine
word library and the associated AFP Word_Lib library [1]. We have found
working with machine words to be cumbersome with Isabelle's
automation—including Sledgehammer—surprisingly poor at solving problems
involving machine words. Often our proofs devolve into fairly painstaking
manual proof steps, and we have now built up a quite-extensive suite of
project-specific word-related lemmas as a testament to past battles.
Naively, perhaps, we would have thought most if not all problems we are
dealing with are well within the capabilities of a modern SMT solver.
Is this expected, or are we somehow configuring these libraries, or
Sledgehammer, incorrectly? (Fairly old) papers like [2] would suggest that
integration between the various HOL machine word libraries and SMT solvers
maybe should be better than what we are experiencing?
Thanks,
Dominic
[1]: https://www.isa-afp.org/entries/Word_Lib.html
[2]: https://user.it.uu.se/~tjawe125/publications/boehme11reconstruction.pdf
Email Gateway (Sep 28 2023 at 11:34):From: Thomas Sewell <tals4@cam.ac.uk>
Automation for the word library has never been good.
Some of the basics are in the simplifier, but, as I understand it, some default inequality/transitivity reasoning that the simplifier does for integers and naturals is not available. This may be because the relevant logic has more side conditions for words, or just an omission, I'm not sure.
The old work got as far as encoding bitvector problems to SMT consistently, and replaying the proofs of an ancient version of Z3 inconsistently. I don't think there has been further progress on that. Without a reliable replay mechanism, the solver would have to be trusted as an oracle, and this is not done by default. I managed to activate it for a project a couple of years ago. Scanning the relevant theory, it looks like these settings in particular may be relevant:
declare [[smt_oracle, z3_extensions]]
Good luck,
Thomas.
Email Gateway (Sep 28 2023 at 12:58):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Many thanks for the reply and pointing us to those configuration options!
Out of interest: how much work would be needed to get comprehensive SMT
replay support for the machine words library, would you estimate, for
somebody who knows what they are doing?
Thanks,
Dominic
Email Gateway (Sep 28 2023 at 13:20):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all
On Thu, 28 Sept 2023 at 12:34, Thomas Sewell <tals4@cam.ac.uk> wrote:
The old work got as far as encoding bitvector problems to SMT
consistently, and replaying the proofs of an ancient version of Z3
inconsistently.There never was any parsing from SMT-Lib back to Isabelle (and don't let
the paper let you believe there ever was).
I don't think there has been further progress on that. Without a
reliable replay mechanism, the solver would have to be trusted as
an oracle, and this is not done by default. I managed to activate
it for a project a couple of years ago. Scanning the relevant
theory, it looks like these settings in particular may be relevant:declare [[smt_oracle, z3_extensions]]
Good luck,
Thomas.------------------------------------------------------------------------
From: cl-isabelle-users-request@lists.cam.ac.uk
<cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Dominic
Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Sent: 28 September 2023 12:16
To: Isabelle-Users Mailinglist <isabelle-users@cl.cam.ac.uk>
Subject: [isabelle] Status of automation for machine words
Hi,We are working on a proof that makes use of the HOL-Word finite
machine word library and the associated AFP Word_Lib library [1].
We have found working with machine words to be cumbersome with
Isabelle's automation—including Sledgehammer—surprisingly poor at
solving problems involving machine words. Often our proofs
devolve into fairly painstaking manual proof steps, and we have
now built up a quite-extensive suite of project-specific
word-related lemmas as a testament to past battles. Naively,
perhaps, we would have thought most if not all problems we are
dealing with are well within the capabilities of a modern SMT solver.Is this expected, or are we somehow configuring these libraries,
or Sledgehammer, incorrectly? (Fairly old) papers like [2] would
suggest that integration between the various HOL machine word
libraries and SMT solvers maybe should be better than what we are
experiencing?Thanks,
Dominic[1]: https://www.isa-afp.org/entries/Word_Lib.html
[2]:
https://user.it.uu.se/~tjawe125/publications/boehme11reconstruction.pdf
Out of interest: how much work would be needed to get comprehensive
SMT replay support for the machine words library, would you estimate,
for somebody who knows what they are doing?
cvc5 is trying to do that for fixed size vectors (so 32 words or 64
words but not 'a word). There is ongoing work (outside of the Isabelle
tree because there is too much work going on) to make it work. This
involves:
changing parts of SMT: like the current version is assuming
monotonicity in the features (this is not the case if you support
cvc5 and veriT and z3)
adapting the reconstruction of cvc5 proofs in Isabelle
I don't understand exactly how 3 works (Hanna in CC knows everything
about that), but it requires changes in the interface (e.g., with RaRe
rules that "configure" cvc5) and in the output to make it work. As long
as 3 is not fixed, 2 cannot fully work either.
And problem 1 is challenging because of surprising issues. I backport
changes to the distribution around once a year for that.
So all together, not easy to do…
Mathias
Thanks,
DominicOn Thu, 28 Sept 2023 at 12:34, Thomas Sewell <tals4@cam.ac.uk> wrote:
Automation for the word library has never been good.
Some of the basics are in the simplifier, but, as I understand it,
some default inequality/transitivity reasoning that the simplifier
does for integers and naturals is not available. This may be
because the relevant logic has more side conditions for words, or
just an omission, I'm not sure.The old work got as far as encoding bitvector problems to SMT
consistently, and replaying the proofs of an ancient version of Z3
inconsistently. I don't think there has been further progress on
that. Without a reliable replay mechanism, the solver would have
to be trusted as an oracle, and this is not done by default. I
managed to activate it for a project a couple of years ago.
Scanning the relevant theory, it looks like these settings in
particular may be relevant:declare [[smt_oracle, z3_extensions]]
Good luck,
Thomas.------------------------------------------------------------------------
From: cl-isabelle-users-request@lists.cam.ac.uk
<cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Dominic
Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Sent: 28 September 2023 12:16
To: Isabelle-Users Mailinglist <isabelle-users@cl.cam.ac.uk>
Subject: [isabelle] Status of automation for machine words
Hi,We are working on a proof that makes use of the HOL-Word finite
machine word library and the associated AFP Word_Lib library [1].
We have found working with machine words to be cumbersome with
Isabelle's automation—including Sledgehammer—surprisingly poor at
solving problems involving machine words. Often our proofs
devolve into fairly painstaking manual proof steps, and we have
now built up a quite-extensive suite of project-specific
word-related lemmas as a testament to past battles. Naively,
perhaps, we would have thought most if not all problems we are
dealing with are well within the capabilities of a modern SMT solver.Is this expected, or are we somehow configuring these libraries,
or Sledgehammer, incorrectly? (Fairly old) papers like [2] would
suggest that integration between the various HOL machine word
libraries and SMT solvers maybe should be better than what we are
experiencing?Thanks,
Dominic[1]: https://www.isa-afp.org/entries/Word_Lib.html
[2]:
https://user.it.uu.se/~tjawe125/publications/boehme11reconstruction.pdf
Email Gateway (Sep 28 2023 at 14:05):From: Thomas Sewell <tals4@cam.ac.uk>
We did have a somewhat working reconstruction from a Z3 proof format to Isabelle back around 2010. SMT-Lib did not specify a proof format at the time, so it was specific to Z3, and probably specific to an old Z3 version. It's possible it was never in the main Isabelle repository, in which case I no longer know where to find it.
That experiment got thrown together fairly quickly, and could probably be re-done for a new prover, with better engineering, in 1-3 months, I'd guess.
The bigger problem was in the nature of the proofs. When replaying Z3 proofs for boolean problems and integer problems, the proofs were of manageable size and mostly contained simple steps. When bitvectors were present, though, the solver's proof strategy tended toward brute force, and the proofs grew larger. Moreover, some of the steps themselves required brute force on our end. The performance trends didn't look good, and we left the project on hold. If I remember right, the main part of that experiment that got used elsewhere was the bitwise conversion.
Best regards,
Thomas.
Last updated: Apr 29 2024 at 01:08 UTC