Nice catch! We noticed that error as well but didn't want to poke the NIST folks in the eye on the web page -- we're hoping to win them over with Cryptol, not put them on the defense. We're planning to submit an errata report on their website next week.