mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-04 05:45:44 +03:00
Update example cryptol code to use infix syntax.
This commit is contained in:
parent
7e34c25e4d
commit
b107e606a2
@ -1079,8 +1079,8 @@ takes a 256-bit key and 96-bit nonce as follows:
|
|||||||
|
|
||||||
//ct in this function has tag removed
|
//ct in this function has tag removed
|
||||||
AeadConstruction (AAD : [n][8]) (CT : [m][8]) = (AAD # padding1 # CT # padding2 # adlen # ptlen) where
|
AeadConstruction (AAD : [n][8]) (CT : [m][8]) = (AAD # padding1 # CT # padding2 # adlen # ptlen) where
|
||||||
padding1 = (zero:[padding n 16][8])
|
padding1 = (zero:[n %^ 16][8])
|
||||||
padding2 = (zero:[padding m 16][8])
|
padding2 = (zero:[m %^ 16][8])
|
||||||
adlen : [8][8]
|
adlen : [8][8]
|
||||||
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
|
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
|
||||||
ptlen : [8][8]
|
ptlen : [8][8]
|
||||||
|
Loading…
Reference in New Issue
Block a user