Minimize our macro definitions for CBMC proofs

[feliperodri]

In some proofs we use ASSUME_VALID_MEMORY_COUNT to properly allocate a valid memory in proof harnesses.
It's nice to have a new macro that does the malloc + the nullness etc. checks, but we are introducing yet another macro and would have to remember to use it consistently across the preconditions and harness assumptions etc.
We should take a pass and minimize our macro definitions at some point. Otherwise, let's make consistently.

[jmklix]

Closing as not a priority for now. Please let us know if this is still important