Check for overflow in validate_u32_array
Check for overflow in validate_u32_array

Confirmed that it's necessary to check, otherwise the length comparison
doesn't work out correctly.

FStarLang/FStar,A-Manning/FStar,A-Manning/FStar,FStarLang/FStar,FStarLang/FStar,A-Manning/FStar