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

Merge remote-tracking branch 'origin' into signed-arith

Browse Source
This commit is contained in:
Robert Dockins 2017-08-07 11:55:48 -07:00
commit a6d29c73c7
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/MiniLock/prim/SCrypt.cry
View File

@ -47,6 +47,7 @@ MFcrypt : { pwBytes, saltBytes, dkLen, r, N }
, 512 >= width N, 1+width N >= width (N-1)
, 32 >= width ((255 + 8 * dkLen) / 256)
, 32 >= width (4 + 128 * r)
, N >= 1
)
=> [pwBytes][8] -> [saltBytes][8] -> [dkLen][8]
MFcrypt P S = split DK
@ -63,6 +64,7 @@ SCrypt : {pwBytes, saltBytes, dkBytes, r, N}
, 512 >= width N, 1+width N >= width (N-1)
, 32 >= width (4 + saltBytes)
, 32 >= width (4 + 128 * r)
, N >= 1
)
=> [pwBytes][8] -> [saltBytes][8] -> [dkBytes][8]
SCrypt P S = MFcrypt `{r=r,N=N} P S