gram-signal
63d9b93634
Improve Hax proofs.
...
hax / fstar-type-checking (push) Has been cancelled
proverif / proofs (push) Has been cancelled
CI / cargo test (push) Has been cancelled
CI / MSRV (push) Has been cancelled
CI / cross test polynomial i586 (push) Has been cancelled
CI / cross test polynomial i686 (push) Has been cancelled
CI / cross test polynomial aarch64 (push) Has been cancelled
This PR improves the hax proofs by removing some admitted parts. It focuses on the v1 module and chain.rs. The main improvements come from the use of refinement types, and from some hax improvements around loops and more (not released yet which is why this is a draft PR for now).
Co-authored-by: Maxime Buyse <maxime@cryspen.com>
Co-authored-by: maximebuyse <45398004+maximebuyse@users.noreply.github.com>
2026-02-20 13:27:45 -08:00
gram-signal
2086a70990
Apt-get update before installing.
2025-10-02 09:37:09 -07:00
maximebuyse
506ff9cf94
Hax update and proof improvements.
2025-10-02 09:29:32 -07:00
Jordan Rose
597cfa57ee
Turn off libcrux-ml-kem features we aren't using
...
hax / fstar-type-checking (push) Has been cancelled
proverif / proofs (push) Has been cancelled
CI / cargo test (push) Has been cancelled
CI / MSRV (push) Has been cancelled
CI / cross test polynomial i586 (push) Has been cancelled
CI / cross test polynomial i686 (push) Has been cancelled
CI / cross test polynomial aarch64 (push) Has been cancelled
Co-authored-by: Rolfe Schmidt <rolfe@signal.org>
2025-07-22 15:38:13 -06:00
gram-signal
d6c1073468
Run proverif proofs in GitHub actions.
hax / fstar-type-checking (push) Has been cancelled
proverif / proofs (push) Has been cancelled
CI / cargo test (push) Has been cancelled
CI / MSRV (push) Has been cancelled
CI / cross test polynomial i586 (push) Has been cancelled
CI / cross test polynomial i686 (push) Has been cancelled
CI / cross test polynomial aarch64 (push) Has been cancelled
2025-06-04 09:13:47 -07:00
gram-signal
2d836ec9bd
Update license and Rust min-version.
2025-05-30 16:22:18 -07:00
Graeme Connell
02c99a6b24
Squashed history.
hax / fstar-type-checking (push) Has been cancelled
CI / cargo test (push) Has been cancelled
CI / MSRV (push) Has been cancelled
CI / cross test polynomial i586 (push) Has been cancelled
CI / cross test polynomial i686 (push) Has been cancelled
CI / cross test polynomial aarch64 (push) Has been cancelled
2025-05-01 10:28:23 -07:00
