Make more modules panic free #713
Conversation
|
I uploaded panic-free polynomial module (some functions have proofs) |
|
This should be against main now. |
|
Yes, I made this into a PR to get CI working on it, but it will go through one more round of work on Monday before I ask for a "real" review. |
I made it into a draft for you |
|
The changes are ready for review, and the branch passes verification process. |
panic freedom improvements
There was a problem hiding this comment.
lgtm with the two nits addressed/commented on.
I checked the C extraction, that's the new functions that were added in polynomial. The eurydice version is newer now, but the code doesn't change with that. So no new extraction needed.
These changes are unfortunate because of the functional style of the code and this causes a bunch of memcpys in the C code. But that's an improvement for another PR.
| #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)] | ||
| #[hax_lib::requires(fstar!(r#"add_vector_pre $lhs $rhs"#))] | ||
| #[hax_lib::ensures(|result| fstar!(r#"add_vector_post $result $lhs $rhs"#))] | ||
| fn add_vector<Vector: Operations>(lhs: Vector, rhs: &Vector) -> Vector { |
There was a problem hiding this comment.
Having to pull out these again is pretty ugly. Please add some comments to both of these functions with some text why it's necessary for the proof right now. And ideally we have an issue on hax for tracking this.
| @@ -286,7 +286,7 @@ pub(crate) fn ntt_at_layer_7<Vector: Operations>(re: &mut PolynomialRingElement< | |||
| } | |||
|
|
|||
| #[inline(always)] | |||
| #[hax_lib::fstar::verification_status(panic_free)] | |||
| #[hax_lib::fstar::verification_status(lax)] | |||
There was a problem hiding this comment.
Do we have issus to get back to panic freedom?
This PR adds runtime safety proofs for
portable/sampling.rsand forpolynomial.rs.Since polynomial now has new preconditions, the verification of NTT and Matrix needs to be updated next.
It also bumps up the Z3 rlimits for IND-CPA to restore verification for that module.