Hmm. My answer would be “you don’t, unless you are willing to accidentally give stronger guarantees”. I believe that standard C11 permits a function to allocate malloc-style from a big static arena of type array of char. You can even implement free() and reuse the memory. But then all the allocations are really pointers into the arena, and certain operations that should be UB aren’t if you use this type of malloc.
But then you throw something like __attribute__((malloc)) on it, and define that as transforming the return value into a new Pointer that is in a different, fresh allocation. And you declare that access to the range of the arena in use is UB until free() gets called.
I don’t know how well this fits into the formalism, but I think that a complete formal memory model would need to understand that free() is permitted to treat its argument as a pointer into a large array of char, but that free()’s caller is not.