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
Graeme Connell
b647f499b4
Fix formatting.
2026-01-07 15:57:09 -08:00
gram-signal
d6f9eb9cf8
Log v1 state transitions for SPQR.
2026-01-07 11:40:33 -08:00
hackerbirds
896ec61f1c
Use constant to define max epoch length, and strengthen post-condition for decoding varints
2025-12-25 12:22:09 -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
gram-signal
0fc9abbc90
Clean up some unused functions.
2025-12-04 09:07:15 -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
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
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
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
Rolfe Schmidt
7939191aa0
comment out compromises for faster execution.
2025-05-30 16:22:10 -07:00
Rolfe Schmidt
f941e02eaf
fix time query
2025-05-30 16:32:56 -06:00
maximebuyse
0623ccc229
Switch to hax 0.3.1.
2025-05-30 15:30:55 -07:00
gram-signal
cff58d922a
Don't provide keys when we could version-negotiate to v0.
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-30 10:46:26 -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
gram-signal
e1918a86fc
Change discard-epoch logic to be based on send epoch.
2025-05-22 15:42:45 -07:00
maximebuyse
246944b3e7
Fix hax proofs.
2025-05-22 10:18:25 -07:00
gram-signal
5f54d921ec
Make the SPQR chain configurable by the requester.
2025-05-16 14:21:56 -07:00
gram-signal
1b1811d3fb
Clean up unused errors.
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-15 11:29:44 -07:00
gram-signal
bf340caccc
Add an empty() constructor for SerializedState.
2025-05-15 11:29:38 -07:00
gram-signal
4db079990e
Clear send keys for old epochs when we start sending in a new one.
2025-05-08 16:05:09 -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
