#1625 added termination proofs for all C functions except rejection sampling. It also adds some linting to make sure no loops were missed when adding the decreases annotations.
However, it would be cleaner if we could turn on a CBMC flag such that it errors in case termination cannot be proven. @hanno-becker requested such a feature upstream: diffblue/cbmc#8867.
Once that is implemented we should make use of the flag in mlkem-native.
#1625 added termination proofs for all C functions except rejection sampling. It also adds some linting to make sure no loops were missed when adding the
decreasesannotations.However, it would be cleaner if we could turn on a CBMC flag such that it errors in case termination cannot be proven. @hanno-becker requested such a feature upstream: diffblue/cbmc#8867.
Once that is implemented we should make use of the flag in mlkem-native.