Has any crypto hash function been proven to be surjective? This answer claims that "it is not proven that all outputs of SHA-1 are possible." Has any crypto hash function been proven to produce all possible outputs (i.e., to be surjective over the codomain of all possible numbers $[0, 2^n]$, where $n$ is the number of bits of the hash)?
The answer is YES for constructions of hash functions that are not used in practice. For example, there is a construction by Damgård that is based on the discrete log problem and works by computing $h(x_1\|x_2)=g^{x_1}\cdot h^{x_2}$, where $g$ is a generator of the group. If $h$ is chosen randomly in the group, then it is hard to find a collision in this function, unless you can solve the discrete log problem. By applying the Merkle-Damgård transform, you get a hash function that takes inputs of any length. Thus, this is a collision resistant hash function.

It is easy to see that this function is surjective. Specifically, $g$ is a generator of the group, so for every $h'\in\mathbb{G}$ and for every $x_2$ there exists a value $x_1$ such that $g^{x_1}\cdot h^{x_2} = h'$.