libcrux icon indicating copy to clipboard operation
libcrux copied to clipboard

hax: update proof scripts to use stable identifiers for impl. expressions from cryspen/hax#1749

Open W95Psp opened this issue 2 months ago • 0 comments

cryspen/hax#1749 introduces a change in the naming scheme of the impl expressions; this needs to be reflected in libcrux. Instead of using hashes, we now use indexed names, which should be more stable (e.g. won't change on each rustc updates).

Tasks:

  • [ ] re-run hax and F* on libcrux
    • Job for ML-DSA: https://github.com/cryspen/libcrux/actions/runs/19032719457
    • Job for ML-KEM: https://github.com/cryspen/libcrux/actions/runs/19032721953
  • [ ] replace the names of impl expression, following F* errors

W95Psp avatar Nov 03 '25 10:11 W95Psp