search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
198 stars 20 forks source link

F*: the mechanism that opens implicitly referenced modules is broken #770

Open W95Psp opened 4 months ago

W95Psp commented 4 months ago

The F backend of hax leverages F's own typeclass mechanism to encode traits. This comes with several drawbacks, notably the fact that, in F, a module that defines instances of a typeclass needs to be opened by F before one can use them. To ensure such instances are reachable, the F* frontent inserts automatically a series of open statements at the start of extracted files.

On MLKem, this mechanism doesn't always work, and inserts spurious opens, leading to cyles or pointing to undefined modules. For instance, here it kicks in: https://github.com/cryspen/libcrux/blob/d755e44c477f31266c3000f47feb69e99b7d0017/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti#L6-L11. But it doesn't here: https://github.com/cryspen/libcrux/blob/ml-kem-lax-check/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.fsti (it requires Libcrux_ml_kem.Vector.Portable)

We need a reproducer here

Status

We need to investigate: does this still exist? If yes, let's minimize and add a reproducer.

github-actions[bot] commented 2 months ago

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.

W95Psp commented 2 months ago

I think this is still relevant.

github-actions[bot] commented 3 days ago

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.

W95Psp commented 18 hours ago

@maximebuyse, do you think this is all about automatic derives we skip? If you think so, can you link this issue to the relevant other issues/PRs?

maximebuyse commented 17 hours ago

No here we have traits that are not derived, but I don't understand very well the issue here (the second link is broken). Is it that we open too much or not enough?

W95Psp commented 17 hours ago

Ah, ok. Then that's probably a separate issue, let's investigate. Yeah, the issue was not very understandable, I added more context :) There are too many opens, in this case!

maximebuyse commented 17 hours ago

Ah, ok. Then that's probably a separate issue, let's investigate. Yeah, the issue was not very understandable, I added more context :) There are too many opens, in this case!

The opens seem reasonable in this case. If it creates a cycle then maybe bundling would kick in and solve this with a recent version of hax