CBMC: Add proofs atop of native functions

[mkannwischer]

[willieyz]

• Related: Add Runtime dispatch based on custom CPU capabilities function #607
• Related: Runtime dispatch based on custom CPU capabilities function mlkem-native#1152

During PR #607, the runtime-dispatch mechanism was ported from mlkem-native: pq-code-package/mlkem-native#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