Rolfe Schmidt
f2589fef85
Update dependencies
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
2026-03-23 09:49:11 -06:00
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
f8788e9c74
Proptests of chain building block behavior.
2026-01-16 12:51:06 -08:00
gram-signal
d310c99c57
Partial fix for cryspen/libcrux#1275
...
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>
2026-01-14 13:20:36 -08:00
gram-signal
d6f9eb9cf8
Log v1 state transitions for SPQR.
2026-01-07 11:40:33 -08:00
hackerbirds
05fb3f2dcf
Fix message deserialization issues and strengthen hax panic freedom proofs
2025-12-25 00:06:22 -08:00
Rolfe Schmidt
46e387458d
Upgrade to libcrux 0.0.4, spqr version to 1.3.0.
...
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: Graeme Connell <gram@signal.org>
2025-12-04 11:53:53 -08:00
Jordan Rose
d48aa6f158
Make raw protobuf types non-pub, update to prost 0.14
...
Co-authored-by: Rolfe Schmidt <141083381+rolfe-signal@users.noreply.github.com>
2025-11-21 21:00:58 -07:00
Alex Bakon
ff78d035d9
Bump libcrux deps to the latest version
2025-10-02 10:13:34 -07:00
maximebuyse
506ff9cf94
Hax update and proof improvements.
2025-10-02 09:29:32 -07:00
gram-signal
99a759a3fd
Log SPQR initial (and possibly renogiated) versions on session initiation.
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-07-24 11:59:03 -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
maximebuyse
0623ccc229
Switch to hax 0.3.1.
2025-05-30 15:30:55 -07:00
Graeme Connell
ea2d65a896
Update some dependencies, clean deps up.
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-22 16:36:03 -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
