cryspen
Propagate ML-DSA pre- and post-conditions for encoding in `traits.rs`
https://github.com/cryspen/libcrux/pull/997 added pre/posts and proofs to AVX2 encoding, but we still need to propagate the pre/post to traits.rs, and make sure the pre/posts are compatible and easy to propagate.
See https://github.com/cryspen/libcrux/pull/997#discussion_r2123032029.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
@W95Psp @karthikbhargavan what's the state here? It's not part of the follow up and the parent is closed.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
We discussed that last week, we had a couple of meetings, and now @clementblaudeau is looking at it. We should have a first PR that adds admits in the proof soon, so that we can identify whatever needs to be proven.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.
