Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

Backend simplification & factorization

Related: - cryspen/hax#533 - cryspen/hax-evit#22

Stop relying on F* typeclasses in the F* backend

Still something we want. We will probably get rid of F* TCs when converting the F* backend to the new generic printer.

[META] Frontend completeness

Relevant: - #977

[META] Frontend completeness

We fixed all the issues here, the only one left is https://github.com/hacspec/hax/issues/1046, which is related to GATs The plan is for the engine to move to @Nadrieril's great new enum...

Primitive names: where should `update_at` live?

@cmester0 this is related to what we are discussing those days with the namespacing of your core

Engine: support GATs

Still relevant.

CLI: rename `extraction` into `generated`

Let's close

Engine: introduce an runtime invariant system for phases

I'm adding an example of what this system of invariants would look like. Let's consider the invariant regarding side effects after the `SideEffectHoist` phase. This phase moves side effects to...

Engine: introduce an runtime invariant system for phases

This will be very similar for the Rust engine

Make the engine compile on Windows + CI

@franziskuskiefer shall we close this one? I think we should either close it or plan work on that, otherwise the issue will just stay forever. We have no current need...