Skip to content

Wrap matrix in struct wrapper #737

@hanno-becker

Description

@hanno-becker

Implement step 1 in #736:

Introduce a struct wrapper for the matrix: Instead of mld_polyvecl mat[MLDSA_K], use mld_polymat. This should follow pq-code-package/mlkem-native#1263. Check that tests all still pass. Adjust all CBMC annotations and check the relevant proofs via tests cbmc -p {FUNCTION_NAME}, to be run in the nix develop shell. See tests cbmc --list-functions for the full list of functions.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions