Found another small bug in the padder while working on the proofs. (No regression test this time because it's only triggered when the input is huge, so just computing the test would take ages.)
The length variable indicates the length of the message in bytes, and is a bit-vector with size 61. At the end of the padding routine, we shift it by 3 to get the length of the message in bits, and want to end up with a 64-bit vector. However, the shift-left routine produces output that is the same size as its input, so it truncates the result to 61 bits here; if the length in bytes is greater than 2^58, the length in bits is > 2^61, and will be improperly truncated. Resizing length to 64 bits before shifting fixes the problem.
Found another small bug in the padder while working on the proofs. (No regression test this time because it's only triggered when the input is huge, so just computing the test would take ages.)
The
lengthvariable indicates the length of the message in bytes, and is a bit-vector with size 61. At the end of the padding routine, we shift it by 3 to get the length of the message in bits, and want to end up with a 64-bit vector. However, the shift-left routine produces output that is the same size as its input, so it truncates the result to 61 bits here; if the length in bytes is greater than 2^58, the length in bits is > 2^61, and will be improperly truncated. Resizinglengthto 64 bits before shifting fixes the problem.