Email Gateway (Aug 23 2022 at 09:17): Email Gateway (Aug 23 2022 at 09:17):From: mandrykin@ispras.ru
Hello!
A bit of context: we are currently experimenting with an approach to
more reliable SMT proof replay in Isabelle/HOL with the aim to later
apply it to low-level code verification, where there are typically many
similar and fairly uninteresting goals that can be easily discharged by
SMT. The approach is based on deterministic quantifier instantiation in
Isabelle/HOL itself, so that the solver is provided with a
quantifier-free problem, which is always decideble, making the proof
replay very stable and even enabling partial model resonstruction of
counterexamples (a preliminary description, if interesting:
https://forge.ispras.ru/attachments/download/7602/TSMT_Tutorial.pdf, but
for now the reconstruction of deterministic one-liners from normal SMT
proofs is not yet properly implemented (requires manual efforts)). So,
naturally, we explored the possibility to replay the proofs within
Isabelle/HOL itself using its internal solvers such as Metis and Argo
(for the fragment without linear integer arithmetic). While we had some
success with Metis+our instantiation (although it's not consistently
faster than SMT proof replay), we encountered unexpected failures in
Argo, particularly in its congruence closure propagation. I attach a
theory with two goals, where Argo fails with an unexpected exception.
The second goal is in fact valid and can be discharged with Metis. A
more general question is where is it appropriate to reports such
problems and whether Argo is maintained in the upstream or it would be
reasonable to try investigating this ourselves and possibly suggest a
patch
Regards,
Mikhail
Bug.thy
Last updated: Apr 20 2024 at 08:16 UTC