Add invariants for while loops.

[maximebuyse]

This PR adds invariants to while loops (using the macro hax_lib::loop_invariant that is already used in for loops). It also adds a macro to prove termination (hax_lib::loop_decreases), that takes a decreasing hax_lib::Int .

[W95Psp]

Thanks, as we discussed there's a few thing we should change (rought notes from what we cahtted about):

• make the loop invariant macro produce two different calls to hax_lib according to wether we gave it a closure or not
• add a loop_annotation_kind type e.g. | LoopInvariant of { index_pat: pat option } | LoopDecreaseMeasure`
• remove extract_loop_variant and extract_loop_invariant, instead have a extract_loop_annotation that takes out a let _ = ..; body and produces (expr * expr * loop_annotation_kind)
• we should accept annotations in any order

Also, why is the decrease clause nat? You can use the << operator in F* too reason about decreasing of any type. Then the default decreasing clause can be ().

[maximebuyse]

Thanks, as we discussed there's a few thing we should change (rought notes from what we cahtted about):

* make the loop invariant macro produce two different calls to hax_lib according to wether we gave it a closure or not

* add a `loop_annotation_kind type e.g. `| LoopInvariant of { index_pat: pat option } | LoopDecreaseMeasure`

* remove `extract_loop_variant` and `extract_loop_invariant`, instead have a `extract_loop_annotation` that takes out a `let _ = ..; body` and produces `(expr * expr * loop_annotation_kind)`

* we should accept annotations in any order

Also, why is the decrease clause nat? You can use the << operator in F* too reason about decreasing of any type. Then the default decreasing clause can be ().

Thanks, I pushed a new version which resolves all 4 points. About nat versus <<, I tried that at first but it seemed to be a problem for signed integer types, but maybe I did something wrong. I modified the macro so that the conversion to a hax_lib int is automatically inserted from any rust integer expression, so this should be nice to use. Maybe switching to << can be kept for later as a possible improvement?

[karthikbhargavan]

This PR is needed for some applications. Let's get this in?

[W95Psp]

Thanks!
I have two last comments, but mainly about style and readability.

If you can improve the code there a bit that'd be nice.

[maximebuyse]

Thanks! I have two last comments, but mainly about style and readability.

If you can improve the code there a bit that'd be nice.

Thanks, I made some style improvements where you pointed and it is indeed much nicer. Merging now.

[maximebuyse]

Two jobs failed in the merge queue:

• Bertie: this one seems to be failing for all PRs recently so this is probably not a problem
• ml-kem: fails because we have a breaking change in how while loops are encoded, but I checked and using both hax and hax-lib from this PR it lax-checks.
  @W95Psp Should we force the merge?

[karthikbhargavan]

Let's revisit this again tomorrow. I would like to understand the bertie failure, and if it is an atomic update issue for ML-KEM, yes we can force the merge here.

[W95Psp]

I spawned https://github.com/cryspen/libcrux/actions/runs/14623000394

[maximebuyse]

I spawned https://github.com/cryspen/libcrux/actions/runs/14623000394

This failed but it also uses hax-lib from main so that is expected

[maximebuyse]

Let's revisit this again tomorrow. I would like to understand the bertie failure, and if it is an atomic update issue for ML-KEM, yes we can force the merge here.

The Bertie failure is a dependency issue that I documented in cryspen/bertie#151. This is unrelated, should we wait for this to be fixed or force the merge anyway?

[karthikbhargavan]

Ok, after reviewing Bertie failure. I agree that this can be merged.