Document verification status #711
Conversation
|
|
||
| #[inline(always)] | ||
| #[hax_lib::fstar::verification_status(lax)] | ||
| #[hax_lib::requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/ |
There was a problem hiding this comment.
You didn't want to start using string literal expressions to avoid escaping?
There was a problem hiding this comment.
Not yet, but yes, this should be done uniformly everywhere.
| @@ -42,6 +42,218 @@ fn vec_from_i16_array(array: &[i16]) -> SIMD256Vector { | |||
| } | |||
| } | |||
|
|
|||
| #[inline(always)] | |||
There was a problem hiding this comment.
These uglyficiations are really unfortunate. We should have a tracking issue somewhere to track getting this fixed.
There was a problem hiding this comment.
You mean the pulling out of functions from an impl? Yes, we hope that the opaque extensions PR or a follow up will help with this: hacspec/hax#1134
|
|
||
| out | ||
| } | ||
|
|
||
| #[hax_lib::attributes] | ||
| impl<Vector: Operations> PolynomialRingElement<Vector> { |
There was a problem hiding this comment.
Can we reference an issue why this needs to be so ugly?
| # ML-KEM Verification Status | ||
|
|
||
| This file keeps track of the current verification status of the modules in the ML-KEM implementation. | ||
|
|
There was a problem hiding this comment.
Let's make this into a table. Happy to do something to help. But the list is hard to read.
This PR documents the status of various modules in ML-KEM in proofs/verification_status.md. We document any module that
has a TODO or missing proof. This file will be updated over time
as the proofs progress.