GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-01 08:32:23 +03:00
Code Issues Projects Releases Wiki Activity

More precise definition of chunks

Browse Source 
Use `padding` directly in the definition of `chunks`, giving an aligned
value to the division.
This commit is contained in:
Trevor Elliott 2017-03-27 16:37:55 -07:00
parent b93f84cf78
commit 5a43c1d1fe
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/maliciousSHA/malicious_SHA1.cry
View File

@ -127,7 +127,7 @@ pad : {msgLen,contentLen,chunks,padding}
( fin msgLen
, 64 >= width msgLen // message width fits in a word
, contentLen == msgLen + 65 // message + header
, chunks == (contentLen+511) / 512
, chunks == (contentLen+padding) / 512
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
)
=> [msgLen] -> [chunks][512]