[amavect]

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.