Heck, there are several models of C out there where you cannot implement `memcpy`.
Heck, there are several models of C out there where you cannot implement `memcpy`.
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.
malloc() is usually implemented in C [0] and to be honest I'm not sure why do you think it wouldn't be? Of course you need OS API calls to actually get some memory (unless you want to operate on statically defined memory buffer) but well it's still C.
[0] https://github.com/lattera/glibc/blob/master/malloc/malloc.c
Try to implement malloc() on bare metal, without using either Assembly or language extensions.