Hax extraction and F* lax-checking #2
Conversation
|
|
||
| /// Add an element to this. | ||
| #[inline] | ||
| pub fn push(&mut self, value: u8) { |
There was a problem hiding this comment.
These are public functions. We should keep them. Deleting them would be a breaking change. Let's just ignore them for hax extraction for now.
| @@ -16,6 +16,7 @@ zeroize = { version = "1.8", default-features = false, features = [ | |||
| "alloc", | |||
| "zeroize_derive", | |||
| ] } | |||
| hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-lib"} | |||
There was a problem hiding this comment.
We should track somewhere to move to a released version here.
There was a problem hiding this comment.
The lib changes are merged into evit, and part of the next approval batch. So once we get the approval we can upstream and make a release. I can open an issue to track.
Co-authored-by: Franziskus Kiefer <[email protected]>
There was a problem hiding this comment.
It looks like the CI fails for msrv and no_std. Can you double check what's going on there? If you don't understand why it's broken and think something in the check is bad, let me know and I can have a look. but from the error, it looks there's a breaking change that makes the CI fail.
I fixed that. I also added a CI job for hax extraction + lax-checking. |
Thanks! I think this is a good first step, let's merge. To merge upstream, maybe it is better to wait for the hax-lib changes to be released. |
This PR replaces #1, with the changes described in https://github.com/cryspen/home/issues/399#issuecomment-3160178752.
It implements the necessary workarounds (and adds some infrastructure) to have working hax extraction + F* lax-checking. Extraction can be done with
cargo hax into fstar, and lax-checking withOTHERFLAGS="--admit_smt_queries true" make -C proofs/fstar/extraction/.We have workarounds for:
OP and assignmenthax#1512&mutparameters hax#1584