mirror of
https://github.com/signalapp/SparsePostQuantumRatchet.git
synced 2026-04-17 22:00:18 +00:00
63d9b93634
Some checks failed
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> |
||
|---|---|---|
| .. | ||
| fstar | ||
| proverif | ||