[pavon]

I wonder if it was 5*64 bits that got mangled in editing. If 256 bits is sufficient for most of their code, I could see there being corner cases that need a few more bits but moving to 512 bits would be overkill.