When I said "mod 2^512" in my earlier note, I of course meant "mod p, where p is approximately 2^512". Sorry if for the sloppiness.