The SHA256 circuit and spec require that the last word be signalled, and
that it has a length greater than 0. The realign also fails to signals
the last word when either the fifo is drained before being flushed
(possibly a correct choice) or if there is 4 bytes in the realign
circuit when being flushed.
The best fix would be to add logic to the fifo & alignment circuits
to handle these cases correctly, and to allow the SHA256 circuit to
receive a 0 length final word. However this would be require large changes to
their proofs, so instead we can fix it locally to HMAC as per this
commit.
The SHA256 circuit and spec require that the last word be signalled, and that it has a length greater than 0. The realign also fails to signals the last word when either the fifo is drained before being flushed (possibly a correct choice) or if there is 4 bytes in the realign circuit when being flushed.
The best fix would be to add logic to the fifo & alignment circuits to handle these cases correctly, and to allow the SHA256 circuit to receive a 0 length final word. However this would be require large changes to their proofs, so instead we can fix it locally to HMAC as per this commit.