Skip to content

Conversation

@hanno-becker
Copy link
Contributor

@hanno-becker hanno-becker commented Oct 31, 2025

  • Change mlk_polyvec back to struct { mlk_poly vec[MLKEM_K]; }
  • Change mlk_polymat to struct { mlk_polyvec vec[MLKEM_K]; }
  • Update all function signatures to use pointer style
  • Fix all implementations to use struct member access
  • Update tests, benchmarks, and CBMC harnesses
  • Add consistent const annotations

@hanno-becker hanno-becker force-pushed the structured branch 3 times, most recently from f300f02 to f18ce9f Compare November 2, 2025 05:36
@hanno-becker hanno-becker changed the title [WIP] Reintroduce struct definitions for mlk_poly{mat,vec} Reintroduce struct definitions for mlk_poly{mat,vec} Nov 2, 2025
@hanno-becker hanno-becker marked this pull request as ready for review November 2, 2025 05:36
@hanno-becker hanno-becker requested a review from a team as a code owner November 2, 2025 05:36
@hanno-becker hanno-becker force-pushed the structured branch 3 times, most recently from 795d96d to 962b08e Compare November 3, 2025 04:46
- Change mlk_polyvec back to struct `{ mlk_poly vec[MLKEM_K]; }`
- Change mlk_polymat to struct `{ mlk_polyvec vec[MLKEM_K]; }`
- Update all function signatures to use pointer style
- Fix all implementations to use struct member access
- Update tests, benchmarks, and CBMC harnesses
- Add consistent const annotations

Somewhat surprisingly and dissatisfyingly, I could not salvage
the CBMC proof for the 'monolithic' polymat_permute_bitrev_to_custom_native
but had to break it in two functions. It would be good to resolve
this as the split causes a lot of code-overhead for an entirely
trivial function.

Signed-off-by: Hanno Becker <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants