Backend simplification & factorization

[W95Psp]

@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]

Related:

• cryspen/hax#252
• cryspen/hax#355

[W95Psp]

Related:

• cryspen/hax#533
• cryspen/hax-evit#22

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[maximebuyse]

This is obsolete with the new Rust infrastructure