GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-27 18:03:42 +03:00
Code Issues Projects Releases Wiki Activity

Fix type signatures in MiniLock SCrypt example

Browse Source
This commit is contained in:
Aaron Tomb 2017-08-07 08:37:20 -07:00
parent 1e453436b2
commit e40b15cc5d
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