CI: Check that 'ramified' functions _must_ be called by contract

[hanno-becker]

In #1445, @mkannwischer found a function with a) a fixed specification, but b) config-dependent implementations. A function with such 'ramified' behavior must always be called by contract, or the call-site must have multiple proofs (one per behavior of the inlined function) as well.

Task: Brainstorm ways for automatically detecting or manually marking functions with multiple implementations but fixed spec. Based on that, devise a way to check that those functions are always called by contract.

[mkannwischer]

Can't we simplyify this to all functions with a contract must be called by contract? Sounds easier to check and I cannot think of a place in mlkem-native/mldsa-native where this shouldn't hold.

[mkannwischer]

A first approximation would be to make sure that each function with a contract (that is not in a top-level-API whitelist) needs to occur in at least one USE_FUNCTION_CONTRACTS=.

[hanno-becker]

@mkannwischer Yes, that's true. But for functions with only one behavior, not calling them by contract is an efficiency, not a soundness gap.

[mkannwischer]

@mkannwischer Yes, that's true. But for functions with only one behavior, not calling them by contract is an efficiency, not a soundness gap.

Of course, but I can't think of an example right now where this approach would not be good enough for us right now.

The only valid reason for not calling it by contract would be a function that has multiple call sites which require different contracts. The best example I can think of right now is an old version of the montgomery_reduce that required a different contract for use in the NTT and the basemul - if I remember correctly we inlined it in one function and called by contract in the other. While this is not a soundness gap, it is still very confusing - which is why we eliminated this eventually.
If we do catch more similar cases, then those likely should be reconsidered as well.

Is there a way to stop CBMC from automatically inlining functions altogether and only letting it inline a given list of functions? I think that would solve the problem of unintentionally inlining.

[hanno-becker]

cflow seems fairly easy to use for the extraction of call graph information, see c265e7d