hacspec / hax

A Rust verification tool

https://hacspec.org/blog

Apache License 2.0

179 stars 20 forks source link

Backend simplification & factorization #154

Open W95Psp opened 1 year ago

W95Psp commented 1 year ago

@cmester0 and I were discussing how we could simplify & factorize backends, let's summarize things here.

There's a lot of boilerplate for implementing a backend currently:

tuples are Construct nodes with a particular name
field projections (ie x.field) are applications of one arg to a particularly named function
operators are function applications we need to re-structure in the backend
need to prefix/rename global names according to their kind (eg type, constructors, function names...)
other things, TODO

Status / Roadmap

We are experimenting with a generic printer, that is now in main.

[ ] Drop the "Rustish" printer, replace it with the generic printer
[x] Add ProVerif backend: it is in main, and @jschneider-bensch is actively working on it!
[ ] Write a F* backend based on the generic printer
[ ] Drop the existing F* backend and the [fstar-surface-ast](https://github.com/hacspec/hax/tree/main/engine/backends/fstar/fstar-surface-ast) folder (that contains a part of F*'s OCaml sources)

W95Psp commented 10 months ago

Related:

252
355

W95Psp commented 2 weeks ago

Related:

533
942