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.