Fully verify portable ntt and generic ntt/inv_ntt modules

cryspen / libcrux

The formally verified crypto library for Rust

https://cryspen.com/libcrux

Apache License 2.0

89 stars 15 forks source link

Fully verify portable ntt and generic ntt/inv_ntt modules #653

Open mamonet opened 2 weeks ago

mamonet commented 2 weeks ago

nttlayer and inv_nttlayer functions lack conditions and proofs against the spec, this PR proposes completing the proofs and evetually fully verify generic ntt/inv_ntt modules.