The lint_serial_number_size check is incorrect. ATIS-1000080.v005 says at least 64 bits of output from a CSPRNG must be used, not that the serial number must be at least 64 bits long. If 64 bits of output from a CSPRNG are used, it is possible that the serial number will be less than 64 bits long.
The
lint_serial_number_sizecheck is incorrect. ATIS-1000080.v005 says at least 64 bits of output from a CSPRNG must be used, not that the serial number must be at least 64 bits long. If 64 bits of output from a CSPRNG are used, it is possible that the serial number will be less than 64 bits long.