hacspec
Missing f* files for nat_mod_macro
We are currently implementing KZG polynomial commitment protocol using the Bls12-381 pairing curve. When trying to verify our implementation we are missing some f* files that the curve is depending on (such as Num_bigint). We can't find these in the lib, is it possible to find these from somewhere?
@W95Psp
I think you are using the old hacspec library (https://github.com/hacspec/hacspec/tree/master/lib), however, this library is deprecated and the current version of hax doesn't support it.
I guess you are building on https://github.com/hacspec/specs/tree/main/bls12-381? This was written for hacspec against the deprecated hacspec lib, so sadly this spec will probably not work nicely with hax.
You're correct, we are using https://github.com/hacspec/specs/tree/main/bls12-381. Is there anything we can do to fix this dependency issue, even though it's from the outdated hacspec lib?
It seems everything is translating fine, however, num-bigint does not fully translate to fstar. The required operations are only addition, multiplication and bit access, so writing the fstar lib for this by hand should not be too hard. Any ideas on how to progress? @karthikbhargavan @W95Psp
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.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
Is it still needed @matthiasspielberg1 ? For now, we're closing it as unplanned, but feel free to reopen the issue.
We don’t need it anymore
tors. 21. aug. 2025 kl. 13.54 skrev Clément Blaudeau < @.***>:
clementblaudeau left a comment (cryspen/hax#1452) https://github.com/cryspen/hax/issues/1452#issuecomment-3210282381
Is it still needed @matthiasspielberg1 https://github.com/matthiasspielberg1 ? For now, we're closing it as unplanned, but feel free to reopen the issue.
— Reply to this email directly, view it on GitHub https://github.com/cryspen/hax/issues/1452#issuecomment-3210282381, or unsubscribe https://github.com/notifications/unsubscribe-auth/BGQEJ4FUW4PICU2OHKG6SOD3OWXPRAVCNFSM6AAAAAB455YAR2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTEMJQGI4DEMZYGE . You are receiving this because you were mentioned.Message ID: @.***>
The general issue is to have a Hax compliant hacspec library again. I believe we have another issue for that. In any case, that would still be useful.