hacl-star / hacl-star

HACL*, a formally verified cryptographic library written in F*
Apache License 2.0
1.6k stars 161 forks source link

Bump solver settings on a couple of proofs in Lib #945

Closed nikswamy closed 1 month ago

nikswamy commented 1 month ago

Proposed changes

Some rlimit/restart-solver settings for a few proofs in Lib

Types of changes

What types of changes does your code introduce to HACL*? Put an x in the boxes that apply

Checklist

Put an x in the boxes that apply. You can also fill these out after creating the PR. If you're unsure about any of them, don't hesitate to ask. We're here to help! This is simply a reminder of what we are going to look for before merging your code.

Further comments

If this is a relatively large or complex change, kick off the discussion by explaining why you chose the solution you did and what alternatives you considered, etc...

github-actions[bot] commented 1 month ago

[CI] Important! The code in dist/gcc-compatible, dist/msvc-compatible, and dist/wasm is tested on cryspen/hacl-packages. dist is not automatically re-generated, be sure to do it manually. (A fresh snapshot can also be downloaded from CI by going to the "artifacts" section of your run.) Then check the following tests before merging this PR. Always check the latest run, it corresponds to the most recent version of this branch. All jobs are expected to be successful. In some cases manual intervention is needed. Please ping the hacl-packages maintainers.

nikswamy commented 1 month ago

I don't know, sadly. It seems to be a few isolated proofs in Lib.Sequence/Lib.Vec, which are conceptually simpler than many other proofs in Hacl. I don't (yet) know these proofs well enough to suggest how they might be revised to make them more robust. But, now that (some) of these files are also in FStar/test/hacl maybe we'll be forced to confront any future instability much more proactively.