2^512 exists in binary notation, but not in unary notation (tally marks, successor function). We conflate these ideas of "number", trying to forget the practical differences. Quite frustrating! SHA-512 depends on the fact that computers cannot feasibly increment to 2^512. A loop cannot feasibly run 2^512 times. Strict finitists emphasize those distinctions when they say 2^512 doesn't exist.
> 2^512 exists in binary notation, but not in unary notation (tally marks, successor function).
Sorry, but this is incoherent nonsense. The existence of a number doesn't depend on its representation ... but we can in fact represent any integer 0 <= n < 2^512 with 512 bits.
> SHA-512 depends on the fact that computers cannot feasibly increment to 2^512.
non sequitur
> A loop cannot feasibly run 2^512 times.
non sequitur
> Strict finitists emphasize those distinctions when they say 2^512 doesn't exist.
I don't mean to come off as a crank. I'd like to clarify the strict finitist position in a sensible way (what they mean is that 2^512 unary notation doesn't fit in this universe, and similarly 2^(2^512) in binary notation doesn't fit in this universe and thus "doesn't exist"), but clearly I fail at meeting your requirements, sorry.
Sigh. There was no mention of 2^(2^512),only the set [0, 2^512), each value of which can be represented with a different configuration of 512 bits in any computer (or storage medium) "in this universe". That these values cannot be enumerated within a small amount of time is completely irrelevant (other than that SHA-512 cannot be reversed in practice, which as I said is a non sequitur) ... 2^512 is quite finite, even for finitists.
And "doesn't fit in this universe" is unformalizable crank nonsense.
A few formalizations exist: bounded arithmetic, internal set theory, Nelson's predicative arithmetic.
From Buss's thesis "Bounded Arithmetic": "However, a recursive function may be computable only in a theoretical sense: the time required to compute it may be far larger than the lifespan of the universe. We are more interested in feasibly computable functions, which can be calculated by today's (or tomorrow's) computers."
And then he goes and defines an arithmetic hierarchy for polynomial functions.