search

pq-code-package / mlkem-c-aarch64

ML-KEM implementation optimized for aarch64
https://pq-code-package.github.io/mlkem-c-aarch64/dev/bench
Apache License 2.0
9 stars 6 forks source link

New macros for CBMC contracts #176

Closed rod-chapman closed 1 day ago

rod-chapman commented 1 day ago

This PR provides a draft proposal for new macros to make the CBMC contracts less verbose and easier to read.

Fixes #169

New macros are in mlkem/cbmc.h

I went for UPPERCASE for the new macros, since this appears to be a common convention in C, and also minimizes the change of creating name-clashes in the future.

I have applied these in mlkem/poly.[hc] to see how they look. All for discussion.

Tests and proofs all pass on this branch locally.

hanno-becker commented 1 day ago

Ran the CI manually and it passed.