Approximate size of image of SHA512

This is unknown but suspected to be the case. If we model SHA-512 as a pseudorandom function that is uniformly distributed on its codomain, a fixed output bin remains empty if all balls miss it.

Here we are throwing $k$ balls into $n$ bins. An output bin remains empty if all the balls miss it which happens with a probability $$ (1-1/n)^k = \left[(1-1/n)^n\right]^{k/n}<e^{-k/n} $$ where $n=2^{512}$ and $k>n$. If we want this probability to be strictly less than $1/n^2$ we need to solve

$$ e^{-k/n}<\frac{1}{n^2}=e^{- 2 \ln n} $$ which gives $k>2 n \ln n.$

We can now apply the union bound (which is weak but the question is about infinite domain size, so this is fine) on the complement of this event and note that since there are $n$ bins the probability that any bin is empty is strictly less than $n(1/n^2)=1/n.$

This gives $$ k>2^{513+\log_2 \ln 512} $$ if I haven’t made a computational error.