GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Simplify some type signatures in examples

Browse Source 
These examples weren't type checking, and now do, with type constraints
that are no more awkward, and arguably less awkward, than before.
This commit is contained in:
Aaron Tomb 2017-06-22 10:09:13 -07:00
parent e282c65a7e
commit 49e847387e
3 changed files with 22 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
examples/MiniLock/prim/CryptoBox.cry
View File

@ -10,20 +10,20 @@ import Salsa20
import Poly1305
import CfrgCurves
crypto_box : {msgBytes} (fin msgBytes, 2^^64 - 1 >= msgBytes + 32) => [msgBytes][8] -> [24][8] -> Public25519 -> Private25519 -> [msgBytes + 16][8]
crypto_box : {msgBytes} (fin msgBytes, 64 >= width (32 + msgBytes)) => [msgBytes][8] -> [24][8] -> Public25519 -> Private25519 -> [msgBytes + 16][8]
crypto_box m n pub priv = crypto_secretbox m k n
where
s = Curve25519 priv pub
k = HSalsa20_bytes `{r=20} s zero
crypto_box_open : {msgBytes} (fin msgBytes, 2^^64 - 1 >= msgBytes + 32) => [msgBytes+16][8] -> [24][8] -> Public25519 -> Private25519 -> (Bit,[msgBytes][8])
crypto_box_open : {msgBytes} (fin msgBytes, 64 >= width (32 + msgBytes)) => [msgBytes+16][8] -> [24][8] -> Public25519 -> Private25519 -> (Bit,[msgBytes][8])
crypto_box_open box n pub priv = crypto_secretbox_open box k n
where
(tag,ct) = splitAt `{16} box
s = Curve25519 priv pub
k = HSalsa20_bytes `{r=20} s zero
crypto_secretbox : {msgBytes} (fin msgBytes, 2^^64 - 1 >= msgBytes + 32)
crypto_secretbox : {msgBytes} (fin msgBytes, 64 >= width (32 + msgBytes))
=> [msgBytes][8] -> [32][8] -> [24][8] -> [msgBytes + 16][8]
crypto_secretbox m k n = box
where
@ -33,7 +33,7 @@ crypto_secretbox m k n = box
authTag = Poly1305 authKey ciphertext
box = authTag # ciphertext
crypto_secretbox_open : {msgBytes} (fin msgBytes, 2^^64 - 1 >= msgBytes + 32)
crypto_secretbox_open : {msgBytes} (fin msgBytes, 64 >= width (32 + msgBytes))
=> [msgBytes + 16][8] -> [32][8] -> [24][8] -> (Bit,[msgBytes][8])
crypto_secretbox_open box k n = (valid,pt)
where

8
examples/MiniLock/prim/PBKDF2.cry
View File

@ -9,13 +9,13 @@ import HMAC
// PBKDF2 specialized to HMAC_SHA256 to avoid monomorphic type issues.
pbkdf2 : {pwBytes, saltBytes, dkLenBits, C}
( 32 >= width (pwBytes*8)
( 64 >= width (8 * pwBytes)
, dkLenBits >= 1
, fin dkLenBits
, 32 >= width (dkLenBits - 1)
, C >= 1
, 16 >= width C
, 32 >= width (4 + saltBytes)
, 32 >= width ((dkLenBits + 255)/256)
)
=> [pwBytes][8] -> [saltBytes][8] -> [dkLenBits]
pbkdf2 P S = take `{dkLenBits} (join Ts)
@ -25,7 +25,7 @@ pbkdf2 P S = take `{dkLenBits} (join Ts)
type len = (dkLenBits + 255)/256
inner : {pwBytes, C}
( 64 >= width (8 * (pwBytes + 32))
( 64 >= width (8 * pwBytes)
, C >= 1, 16 >= width C
)
=> [pwBytes][8] -> [32][8] -> [256]
@ -34,7 +34,7 @@ inner P U0 = (Ts @ 0).0 // XXX should be ! 0
// Ts : [_][([256],[32][8])]
Ts = [(join U0, U0)] # [ F P t u | _ <- [1..C] : [_][16] | (t,u) <- Ts ]
F : {pwBytes} ( 64 >= width (8*(32+pwBytes))
F : {pwBytes} ( 64 >= width (8 * pwBytes)
) => [pwBytes][8] -> [256] -> [32][8] -> ([256],[32][8])
F P Tprev Uprev = (Tnext,Unext)
where

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

@ -39,13 +39,14 @@ SMix B = join (Xs ! 0)
// SCrypt paper, page 11: MFCrypt specialized to sha256 (see the 'pbkdf2' function)
// p = 1
MFcrypt : { pwBytes, saltBytes, dkLen, r, N }
( 4*r >= 1
, 16 >= width (4*r)
, ((dkLen*8 + 255) / 256) >= 1
, 32 >= width (8*pwBytes)
( fin dkLen
, 4*r >= 1
, 8 * dkLen >= 1
, 64 >= width (8 * pwBytes)
, 32 >= width (4 + saltBytes)
, 16 >= width ((255 + 8 * dkLen) / 256)
, N >= 1, 512 >= width N, 1+width N >= width (N-1)
, 512 >= width N, 1+width N >= width (N-1)
, 32 >= width ((255 + 8 * dkLen) / 256)
, 32 >= width (4 + 128 * r)
)
=> [pwBytes][8] -> [saltBytes][8] -> [dkLen][8]
MFcrypt P S = split DK
@ -55,13 +56,13 @@ MFcrypt P S = split DK
DK = pbkdf2 `{dkLenBits=dkLen*8, C=1} P (split B')
SCrypt : {pwBytes, saltBytes, dkBytes, r, N}
( 4*r >= 1, 16 >= width (4*r)
, (dkBytes * 8 + 255) / 256 >= 1
, 16 >= width ((255 + 8 * dkBytes) / 256)
, 8 * dkBytes == 256 * ((255 + 8 * dkBytes) / 256)
, 32 >= width (8 * pwBytes)
, 32 >= width (4 * saltBytes)
, N >= 1, 512 >= width N, 1+width N >= width (N-1)
( fin dkBytes, 4*r >= 1
, 8 * dkBytes >= 1
, 32 >= width ((255 + 8 * dkBytes) / 256)
, 64 >= width (8 * pwBytes)
, 512 >= width N, 1+width N >= width (N-1)
, 32 >= width (4 + saltBytes)
, 32 >= width (4 + 128 * r)
)
=> [pwBytes][8] -> [saltBytes][8] -> [dkBytes][8]
SCrypt P S = MFcrypt `{r=r,N=N} P S