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

CBMC: Add proofs atop of native functions

Open mkannwischer opened this issue 7 months ago • 1 comments

mkannwischer avatar Jul 09 '25 05:07 mkannwischer

  • Related: #607
  • Related: https://github.com/pq-code-package/mlkem-native/pull/1152

During PR #607, the runtime-dispatch mechanism was ported from mlkem-native: https://github.com/pq-code-package/mlkem-native/pull/1152 However, several CBMC-related changes for the native functions were not yet ported due to the lack of corresponding CBMC proof contracts.

Add this comment for tracking, adding those CBMC change after we complete native CBMC proof

willieyz avatar Nov 20 '25 17:11 willieyz