mldsa-native icon indicating copy to clipboard operation
mldsa-native copied to clipboard
Published 2 months ago • verified publisher icon pq-code-package

HOL-Light: Rewrite specification in a way that does not hardcode any code-length constants

Open jakemas opened this issue 2 months ago • 0 comments

We should aim to rewrite the specs in a way that does not hardcode any code-length constants; see e.g. https://github.com/pq-code-package/mlkem-native/blob/main/proofs/hol_light/arm/proofs/mlkem_ntt.ml#L539 for how we do it in mlkem-native.

See also https://github.com/pq-code-package/mldsa-native/issues/648

jakemas avatar Nov 11 '25 20:11 jakemas