interest in isabelle backend?

[stuebinm]

We would be interested in having an Isabelle backend

Hi all! @RaitoBezarius pointed me here a while ago. Originally I was interested in using aeneas to maybe try and verify some of my own rust code (& finally actually use Lean while doing it), but I soon got distracted by that sentence from the readme — and well, having played with Isabelle/HOL things in the past, I accidentally nerdsniped myself into writing the basic parts of such a backend.

The current diff is here: https://github.com/AeneasVerif/aeneas/compare/main...stuebinm:aeneas:isabelle

Current state: it can produce valid Isabelle functions for most simple struct/enum declarations & terms, as long as they do not make any kind of use of traits (as a test case, I used a simplified version of the avl tree verification with uses of traits removed). There's not much testing yet though, so it's very possible to get it to generate invalid code. The primitives lib for Isabelle is also as basic as it can possibly be for the avl tree example (it contains nothing but a u32 type and a less-than operator on it).

Unfortunately I'm not sure how feasible real support for rust's traits in the translation is — while simple traits should easily map to either a reified datatype representation or to Isabelle's own type class system, I don't see any obvious way to have support for associated types in traits (as in Isabelle, types and values are very much distinct things). I've looked into the HOL4 backend a little since I suspect (although i don't know much of HOL4) it has the same issue, and afaict it seems to always fail if associated types are present as well?

I'm opening this issue mostly to ask how much interest you have in an Isabelle/HOL backend overall / if you'd have any use for my code — for me this is currently a pure hobby project, and while I might continue on it until it's a (very little) bit closer to feature-complete I don't really intend to maintain it on my own in the long term.

[sonmarcho]

Sorry for my (very) late answer: I got busy with other things then went to vacations. Thanks for your interest in the project! Just a quick note about the traits and the associated types: we will implement a pass in Charon which lifts the associated types to make them parameters of the traits, so that this is not an issue anymore.

Generally speaking, we are interested in having backends, in particular a backend for Isabelle, but if people need and use them (for instance they're doing a verification project with the backend) and are ready to maintain them, because on our side this is a lot of work.

[stuebinm]

fair — I don't currently have much of a project for which I'd be ready to maintain this backend; should that change I might yet start with that though (of if anyone else is reading this & might be interested in using aeneas with Isabelle, feel free to reach out!)

we will implement a pass in Charon which lifts the associated types to make them parameters of the traits, so that this is not an issue anymore

do I understand this correctly as, associated types will become parameters of the trait itself (instead of fields inside its dictionary-structure), and at use-sites they are resolved by charon already? That would be neat for Isabelle (can't promise I'll look at it again/implement this, but perhaps if I have the time)

[sonmarcho]

do I understand this correctly as, associated types will become parameters of the trait itself (instead of fields inside its dictionary-structure), and at use-sites they are resolved by charon already? That would be neat for Isabelle (can't promise I'll look at it again/implement this, but perhaps if I have the time)

Yes, this is exactly what we intend to do.

As a side note: if you're interested in contributing and learning Lean, there is a lot to do on the Lean backend (including: adding definitions to the standard library, writing and verifying examples to exerce the backend, implementing better automation, etc.). :)