project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Fix bug in SHA-256 padder #922

Closed jadephilipoom closed 3 years ago

jadephilipoom commented 3 years ago

While trying to prove the circuit correct, I found that there was a bug in the case where the circuit needs to switch from the "emit_bit" state directory to "writing_length" (occurs if there's exactly one word between the message and length). This PR fixes the bug and adds a regression test.