GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-23 22:27:25 +03:00
Code Issues Projects Releases Wiki Activity

Remove trailing whitespace

Browse Source
This commit is contained in:
Brian Huffman 2016-02-19 10:08:20 -08:00
parent 9809e176eb
commit 1322156d28
45 changed files with 143 additions and 188 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
bench/data/AES.cry
View File

@ -32,7 +32,7 @@ type AESKeySize = (Nk*32)
type GF28 = [8]
type State = [4][Nb]GF28
type RoundKey = State
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
// GF28 operations
gf28Add : {n} (fin n) => [n]GF28 -> GF28
gf28Add ps = sums ! 0
@ -196,7 +196,7 @@ aesDecrypt : ([128], [AESKeySize]) -> [128]
aesDecrypt (ct, key) = stateToMsg (AESFinalInvRound (kFinal, rounds ! 0))
where (kFinal, ks, kInit) = ExpandKey key
state0 = AddRoundKey(kInit, msgToState ct)
rounds = [state0] # [ AESInvRound (rk, s)
rounds = [state0] # [ AESInvRound (rk, s)
| rk <- reverse ks
| s <- rounds
]

2
cryptol-server/Cryptol/Aeson.hs
View File

@ -5,7 +5,7 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol
-- types. Since these are meant to be consumed over a wire, they are
-- mostly focused on base values and interfaces rather than a full

4
docs/ProgrammingCryptol/aes/AES.cry
View File

@ -32,7 +32,7 @@ type AESKeySize = (Nk*32)
type GF28 = [8]
type State = [4][Nb]GF28
type RoundKey = State
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
// GF28 operations
gf28Add : {n} (fin n) => [n]GF28 -> GF28
gf28Add ps = sums ! 0
@ -196,7 +196,7 @@ aesDecrypt : ([128], [AESKeySize]) -> [128]
aesDecrypt (ct, key) = stateToMsg (AESFinalInvRound (kFinal, rounds ! 0))
where (kFinal, ks, kInit) = ExpandKey key
state0 = AddRoundKey(kInit, msgToState ct)
rounds = [state0] # [ AESInvRound (rk, s)
rounds = [state0] # [ AESInvRound (rk, s)
| rk <- reverse ks
| s <- rounds
]

114
examples/ChaChaPolyCryptolIETF.md
View File

@ -1,4 +1,4 @@
% ChaCha20 and Poly1305 for IETF protocols
% ChaCha20 and Poly1305 for IETF protocols
% Y. Nir (Check Point), A. Langley (Google Inc), D. McNamee (Galois, Inc)
% July 28, 2014
@ -178,7 +178,7 @@ leaving the others alone:
```
Note that this run of quarter round is part of what is called a
"column round".
"column round".
### Test Vector for the Quarter Round on the ChaCha state
@ -208,8 +208,8 @@ After applying QUARTERROUND(2,7,8,13)
Note that only the numbers in positions 2, 7, 8, and 13 changed.
In the Cryptol implementation of ChaCha20, the ChaChaQuarterround is called on four elements at a time,
and there is no destructive state modification, so it would be artificial to reproduce the
In the Cryptol implementation of ChaCha20, the ChaChaQuarterround is called on four elements at a time,
and there is no destructive state modification, so it would be artificial to reproduce the
above example of the partially-destructively modified matrix. Instead, we show the output of
calling ChaChaQuarterround on the diagonal elements identified above:
@ -726,7 +726,7 @@ Next, divide the message into 16-byte blocks. The last block might be shorter:
* Add the current block to the accumulator.
* Multiply by "r"
* Set the accumulator to the result modulo p. To summarize:
* Set the accumulator to the result modulo p. To summarize:
``accum[i+1] = ((accum[i]+block)*r) % p``.
```cryptol
@ -773,7 +773,7 @@ using AES, and assume that we got the following keying material:
03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b
```cryptol
Poly1305TestKey = join (parseHexString
Poly1305TestKey = join (parseHexString
( "85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8:01:"
# "03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b."
) )
@ -808,7 +808,7 @@ values of the accumulator:
```cryptol
// TODO: refactor the Poly function in terms of this AccumBlocks
// challenge: doing so while maintaining the clean literate correspondence with the spec
AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
=> [256] -> [m][8] -> ([_][136], [136])
AccumBlocks key msg = (accum, lastAccum) where
@ -864,7 +864,7 @@ Acc + block = 2d8adaf23b0337fa7cccfb4ea344ca153
```
```cryptol
property polyBlocksOK =
property polyBlocksOK =
(blocks @ 1 == 0x02c88c77849d64ae9147ddeb88e69c83fc) &&
(blocks @ 2 == 0x02d8adaf23b0337fa7cccfb4ea344b30de) &&
(lastBlock == 0x028d31b7caff946c77c8844335369d03a7) where
@ -876,7 +876,7 @@ Adding s we get this number, and serialize if to get the tag:
Acc + s = 2a927010caf8b2bc2c6365130c11d06a8
Tag: a8:06:1d:c1:30:51:36:c6:c2:2b:8b:af:0c:01:27:a9
```cryptol
// Putting it all together and testing:
@ -904,7 +904,7 @@ SK_a* or *_write_MAC_key is only for stand-alone Poly1305.
The method is to call the block function with the following
parameters:
* The 256-bit session integrity key is used as the ChaCha20 key.
* The block counter is set to zero.
* The protocol will specify a 96-bit or 64-bit nonce. This MUST be
@ -929,7 +929,7 @@ encryption algorithms (often called Initialization Vectors, or IVs),
they usually don't have such a provision for the MAC function. In
that case the per-invocation nonce will have to come from somewhere
else, such as a message counter.
### Poly1305 Key Generation Test Vector
For this example, we'll set:
@ -966,7 +966,7 @@ PolyChaChaState_testVector = [
0x37b633a8, 0xa50dfde3, 0xe2b8db08, 0x46a6d1fd,
0x7da03782, 0x9183a233, 0x148ad271, 0xb46773d1,
0x3cc1875a, 0x8607def1, 0xca5c3086, 0x7085eb87 ]
property PolyChaCha_correct = ChaCha20Block PolyKeyTest PolyNonceTest 0 ==
PolyChaChaState_testVector
```
@ -978,7 +978,7 @@ PolyOutput = join (parseHexString (
"8a d5 a0 8b 90 5f 81 cc 81 50 40 27 4a b2 94 71 " #
"a8 33 b6 37 e3 fd 0d a5 08 db b8 e2 fd d1 a6 46 "))
GeneratePolyKeyUsingChaCha k n i = join [littleendian (groupBy`{8}b)
GeneratePolyKeyUsingChaCha k n i = join [littleendian (groupBy`{8}b)
| b <- take `{8}(ChaCha20Block k n i) ]
property Poly_passes_test = GeneratePolyKeyUsingChaCha PolyKeyTest PolyNonceTest 0 == PolyOutput
@ -1048,7 +1048,7 @@ takes a 256-bit key and 96-bit nonce as follows:
counter set to 1.
```cryptol
ct = ChaCha20EncryptBytes p k nonce 1
ct = ChaCha20EncryptBytes p k nonce 1
```
* Finally, the Poly1305 function is called with the Poly1305 key
@ -1071,12 +1071,12 @@ takes a 256-bit key and 96-bit nonce as follows:
```cryptol
ptlen : [8][8]
ptlen = groupBy`{8}(littleendian (groupBy`{8}(`m:[64])))
ptlen = groupBy`{8}(littleendian (groupBy`{8}(`m:[64])))
adlen : [8][8]
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
// compute padding
tag = Poly1305 PolyKey (AeadConstruction aad ct)
//ct in this function has tag removed
AeadConstruction (AAD : [n][8]) (CT : [m][8]) = (AAD # padding1 # CT # padding2 # adlen # ptlen) where
padding1 = (zero:[(16-n%16)%16][8])
@ -1100,7 +1100,7 @@ AEAD_CHACHA20_POLY1305_DECRYPT : {m, n} (fin m, fin n
,64 >= width m, 64 >= width n)
=> [256] -> [96]
-> [m+16][8] -> [n][8]
-> ([m][8], Bit)
-> ([m][8], Bit)
AEAD_CHACHA20_POLY1305_DECRYPT k nonce ct ad = (pt, valid) where
inTag = drop`{m}ct
inCt = take`{m}ct
@ -1185,7 +1185,7 @@ AeadPolyOneTimeKey_testVector = [
0x93929190, 0x97969594, 0x9b9a9998, 0x9f9e9d9c,
0x00000000, 0x00000007, 0x43424140, 0x47464544 ]
property AeadPolyKeyBuildState_correct =
property AeadPolyKeyBuildState_correct =
BuildState AeadKey AeadNonce 0 == AeadPolyOneTimeKey_testVector
```
@ -1198,7 +1198,7 @@ AeadPolyOneTimeKeyState = [
0xdecc7ea2, 0xb44ddbad, 0xe49c17d1, 0xd8430bc9,
0x8c94b7bc, 0x8b7d4b4b, 0x3927f67d, 0x1669a432]
property AeadPolyChaCha_correct =
property AeadPolyChaCha_correct =
ChaCha20Block AeadKey AeadNonce 0 == AeadPolyOneTimeKeyState
```
@ -1262,7 +1262,7 @@ AeadTagTestVector = parseHexString "1a:e1:0b:59:4f:09:e2:6a:7e:90:2e:cb:d0:60:06
```
```cryptol
property AeadTag_correct = AeadTag == AeadTagTestVector
property AeadTag_correct = AeadTag == AeadTagTestVector
property AeadConstruction_correct = (AeadConstruction AeadAAD AeadCT) == AeadConstructionTestVector
@ -1458,12 +1458,12 @@ Email: dylan@galois.com
```cryptol
// helper macros for higher-up properties
TV_block_correct key nonce blockcounter result = ChaCha20Block key nonce blockcounter == result
TV_block_Keystream_correct key nonce blockcounter keystream =
take`{0x40} (groupBy`{8} (join (join (ChaCha20ExpandKey key nonce blockcounter)))) == keystream
ChaCha20_block_correct key nonce blockcounter result keystream =
TV_block_correct key nonce blockcounter result &&
ChaCha20_block_correct key nonce blockcounter result keystream =
TV_block_correct key nonce blockcounter result &&
TV_block_Keystream_correct key nonce blockcounter keystream
```
@ -1489,7 +1489,7 @@ TV1_block_KeyStream = [
property TV1_block_correct = ChaCha20_block_correct TV1_block_Key TV1_block_Nonce TV1_block_BlockCounter TV1_block_After20 TV1_block_KeyStream
```
### Test Vector #2
```cryptol
@ -1511,7 +1511,7 @@ TV2_block_KeyStream = [
property TV2_block_correct = ChaCha20_block_correct TV2_block_Key TV2_block_Nonce TV2_block_BlockCounter TV2_block_After20 TV2_block_KeyStream
```
### Test Vector #3
@ -1526,11 +1526,11 @@ TV3_block_After20 = [
0xe8252083, 0x60818b01, 0xf38422b8, 0x5aaa49c9,
0xbb00ca8e, 0xda3ba7b4, 0xc4b592d1, 0xfdf2732f,
0x4436274e, 0x2561b3c8, 0xebdd4aa6, 0xa0136c00]
TV3_block_KeyStream = [
0x3a, 0xeb, 0x52, 0x24, 0xec, 0xf8, 0x49, 0x92, 0x9b, 0x9d, 0x82, 0x8d, 0xb1, 0xce, 0xd4, 0xdd,
0x83, 0x20, 0x25, 0xe8, 0x01, 0x8b, 0x81, 0x60, 0xb8, 0x22, 0x84, 0xf3, 0xc9, 0x49, 0xaa, 0x5a,
0x8e, 0xca, 0x00, 0xbb, 0xb4, 0xa7, 0x3b, 0xda, 0xd1, 0x92, 0xb5, 0xc4, 0x2f, 0x73, 0xf2, 0xfd,
0x3a, 0xeb, 0x52, 0x24, 0xec, 0xf8, 0x49, 0x92, 0x9b, 0x9d, 0x82, 0x8d, 0xb1, 0xce, 0xd4, 0xdd,
0x83, 0x20, 0x25, 0xe8, 0x01, 0x8b, 0x81, 0x60, 0xb8, 0x22, 0x84, 0xf3, 0xc9, 0x49, 0xaa, 0x5a,
0x8e, 0xca, 0x00, 0xbb, 0xb4, 0xa7, 0x3b, 0xda, 0xd1, 0x92, 0xb5, 0xc4, 0x2f, 0x73, 0xf2, 0xfd,
0x4e, 0x27, 0x36, 0x44, 0xc8, 0xb3, 0x61, 0x25, 0xa6, 0x4a, 0xdd, 0xeb, 0x00, 0x6c, 0x13, 0xa0]
property TV3_block_correct = ChaCha20_block_correct TV3_block_Key TV3_block_Nonce TV3_block_BlockCounter TV3_block_After20 TV3_block_KeyStream
@ -1549,11 +1549,11 @@ TV4_block_After20 = [
0xa78dea8f, 0x5e269039, 0xa1bebbc1, 0xcaf09aae,
0xa25ab213, 0x48a6b46c, 0x1b9d9bcb, 0x092c5be6,
0x546ca624, 0x1bec45d5, 0x87f47473, 0x96f0992e]
TV4_block_KeyStream = [
0x72, 0xd5, 0x4d, 0xfb, 0xf1, 0x2e, 0xc4, 0x4b, 0x36, 0x26, 0x92, 0xdf, 0x94, 0x13, 0x7f, 0x32,
0x8f, 0xea, 0x8d, 0xa7, 0x39, 0x90, 0x26, 0x5e, 0xc1, 0xbb, 0xbe, 0xa1, 0xae, 0x9a, 0xf0, 0xca,
0x13, 0xb2, 0x5a, 0xa2, 0x6c, 0xb4, 0xa6, 0x48, 0xcb, 0x9b, 0x9d, 0x1b, 0xe6, 0x5b, 0x2c, 0x09,
0x72, 0xd5, 0x4d, 0xfb, 0xf1, 0x2e, 0xc4, 0x4b, 0x36, 0x26, 0x92, 0xdf, 0x94, 0x13, 0x7f, 0x32,
0x8f, 0xea, 0x8d, 0xa7, 0x39, 0x90, 0x26, 0x5e, 0xc1, 0xbb, 0xbe, 0xa1, 0xae, 0x9a, 0xf0, 0xca,
0x13, 0xb2, 0x5a, 0xa2, 0x6c, 0xb4, 0xa6, 0x48, 0xcb, 0x9b, 0x9d, 0x1b, 0xe6, 0x5b, 0x2c, 0x09,
0x24, 0xa6, 0x6c, 0x54, 0xd5, 0x45, 0xec, 0x1b, 0x73, 0x74, 0xf4, 0x87, 0x2e, 0x99, 0xf0, 0x96]
property TV4_block_correct = ChaCha20_block_correct TV4_block_Key TV4_block_Nonce TV4_block_BlockCounter TV4_block_After20 TV4_block_KeyStream
@ -1572,7 +1572,7 @@ TV5_block_After20 = [
0x88228b1a, 0x96a4dfb3, 0x5b76ab72, 0xc727ee54,
0x0e0e978a, 0xf3145c95, 0x1b748ea8, 0xf786c297,
0x99c28f5f, 0x628314e8, 0x398a19fa, 0x6ded1b53]
TV5_block_KeyStream = [
0xc2, 0xc6, 0x4d, 0x37, 0x8c, 0xd5, 0x36, 0x37, 0x4a, 0xe2, 0x04, 0xb9, 0xef, 0x93, 0x3f, 0xcd,
0x1a, 0x8b, 0x22, 0x88, 0xb3, 0xdf, 0xa4, 0x96, 0x72, 0xab, 0x76, 0x5b, 0x54, 0xee, 0x27, 0xc7,
@ -1586,8 +1586,8 @@ property all_block_tests_correct =
TV2_block_correct &&
TV3_block_correct &&
TV4_block_correct &&
TV5_block_correct
TV5_block_correct
```
## ChaCha20 Encryption
@ -1610,7 +1610,7 @@ TV1_enc_cyphertext = [
0xbd, 0xd2, 0x19, 0xb8, 0xa0, 0x8d, 0xed, 0x1a, 0xa8, 0x36, 0xef, 0xcc, 0x8b, 0x77, 0x0d, 0xc7,
0xda, 0x41, 0x59, 0x7c, 0x51, 0x57, 0x48, 0x8d, 0x77, 0x24, 0xe0, 0x3f, 0xb8, 0xd8, 0x4a, 0x37,
0x6a, 0x43, 0xb8, 0xf4, 0x15, 0x18, 0xa1, 0x1c, 0xc3, 0x87, 0xb6, 0x69, 0xb2, 0xee, 0x65, 0x86]
property TV1_enc_correct = ChaCha20_enc_correct TV1_enc_Key TV1_enc_Nonce TV1_enc_BlockCounter TV1_enc_plaintext TV1_enc_cyphertext
```
@ -1647,7 +1647,7 @@ IETF_submission_text = [
0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x20, 0x6f, 0x72, 0x20, 0x70, 0x6c, 0x61, 0x63, 0x65, 0x2c,
0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61, 0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65,
0x73, 0x73, 0x65, 0x64, 0x20, 0x74, 0x6f ]
TV2_enc_plaintext = IETF_submission_text
@ -1676,7 +1676,7 @@ TV2_enc_cyphertext = [
0x14, 0xea, 0x99, 0x82, 0xcc, 0xaf, 0xb3, 0x41, 0xb2, 0x38, 0x4d, 0xd9, 0x02, 0xf3, 0xd1, 0xab,
0x7a, 0xc6, 0x1d, 0xd2, 0x9c, 0x6f, 0x21, 0xba, 0x5b, 0x86, 0x2f, 0x37, 0x30, 0xe3, 0x7c, 0xfd,
0xc4, 0xfd, 0x80, 0x6c, 0x22, 0xf2, 0x21]
property TV2_enc_correct = ChaCha20_enc_correct TV2_enc_Key TV2_enc_Nonce TV2_enc_BlockCounter TV2_enc_plaintext TV2_enc_cyphertext
```
@ -1699,7 +1699,7 @@ jabberwock_text = [
0x65, 0x72, 0x65, 0x20, 0x74, 0x68, 0x65, 0x20, 0x62, 0x6f, 0x72, 0x6f, 0x67, 0x6f, 0x76, 0x65,
0x73, 0x2c, 0x0a, 0x41, 0x6e, 0x64, 0x20, 0x74, 0x68, 0x65, 0x20, 0x6d, 0x6f, 0x6d, 0x65, 0x20,
0x72, 0x61, 0x74, 0x68, 0x73, 0x20, 0x6f, 0x75, 0x74, 0x67, 0x72, 0x61, 0x62, 0x65, 0x2e]
TV3_enc_plaintext = jabberwock_text
@ -1712,13 +1712,13 @@ TV3_enc_cyphertext = [
0x1a, 0x55, 0x32, 0x05, 0x57, 0x16, 0xea, 0xd6, 0x96, 0x25, 0x68, 0xf8, 0x7d, 0x3f, 0x3f, 0x77,
0x04, 0xc6, 0xa8, 0xd1, 0xbc, 0xd1, 0xbf, 0x4d, 0x50, 0xd6, 0x15, 0x4b, 0x6d, 0xa7, 0x31, 0xb1,
0x87, 0xb5, 0x8d, 0xfd, 0x72, 0x8a, 0xfa, 0x36, 0x75, 0x7a, 0x79, 0x7a, 0xc1, 0x88, 0xd1]
property TV3_enc_correct = ChaCha20_enc_correct TV3_enc_Key TV3_enc_Nonce TV3_enc_BlockCounter TV3_enc_plaintext TV3_enc_cyphertext
property all_enc_tests_correct =
TV1_enc_correct &&
TV2_enc_correct &&
TV3_enc_correct
TV3_enc_correct
```
## Poly1305 Message Authentication Code
@ -1857,7 +1857,7 @@ exactly 2^130-6?
TV9_MAC_Key = 0x02 # zero:[256]
TV9_MAC_text =
TV9_MAC_text =
[0xFD, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF]
TV9_MAC_tag = [0xFA, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF]: [16][8]
@ -1898,7 +1898,7 @@ TV11_MAC_text = [
0xE3, 0x35, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0xB9, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0x33, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0x79, 0xCD, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
TV11_MAC_tag = split(0x13 # 0): [16][8]
property TV11_MAC_correct = poly1305_MAC_correct TV11_MAC_Key TV11_MAC_text TV11_MAC_tag
@ -1914,7 +1914,7 @@ property all_MAC_tests_correct =
TV8_MAC_correct &&
TV9_MAC_correct &&
TV10_MAC_correct &&
TV11_MAC_correct
TV11_MAC_correct
```
@ -1967,7 +1967,7 @@ property TV3_key_correct = Poly1305_key_correct TV3_key_Key TV3_key_Nonce TV3_ke
property all_key_tests_correct =
TV1_key_correct &&
TV2_key_correct &&
TV3_key_correct
TV3_key_correct
```
## ChaCha20-Poly1305 AEAD Decryption
@ -2004,7 +2004,7 @@ TV1_AEAD_known_otk = join([
//sent
TV1_AEAD_tag = [0xee, 0xad, 0x9d, 0x67, 0x89, 0x0c, 0xbb, 0x22, 0x39, 0x23, 0x36, 0xfe, 0xa1, 0x85, 0x1f, 0x38]
TV1_AEAD_cypherText = [
0x64, 0xa0, 0x86, 0x15, 0x75, 0x86, 0x1a, 0xf4, 0x60, 0xf0, 0x62, 0xc7, 0x9b, 0xe6, 0x43, 0xbd,
0x5e, 0x80, 0x5c, 0xfd, 0x34, 0x5c, 0xf3, 0x89, 0xf1, 0x08, 0x67, 0x0a, 0xc7, 0x6c, 0x8c, 0xb2,
@ -2049,7 +2049,7 @@ TV1_AEAD_Poly_input = [
First, we calculate the one-time Poly1305 key
```cryptol
//generate and check the one time key (leaving out the given states from the document, they will be correct if this is correct)
property TV1_otk_correct = Poly1305_key_correct TV1_AEAD_key TV1_AEAD_nonce TV1_AEAD_known_otk
@ -2069,7 +2069,7 @@ We calculate the Poly1305 tag and find that it matches
```cryptol
property TV1_tag_correct = poly1305_MAC_correct TV1_AEAD_known_otk (AeadConstruction TV1_AEAD_AAD TV1_AEAD_cypherText) TV1_AEAD_tag
```
```cryptol
TV1_plaintext = [
0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x73, 0x20,
@ -2089,14 +2089,14 @@ TV1_plaintext = [
0x6d, 0x20, 0x6f, 0x74, 0x68, 0x65, 0x72, 0x20, 0x74, 0x68, 0x61, 0x6e, 0x20, 0x61, 0x73, 0x20,
0x2f, 0xe2, 0x80, 0x9c, 0x77, 0x6f, 0x72, 0x6b, 0x20, 0x69, 0x6e, 0x20, 0x70, 0x72, 0x6f, 0x67,
0x72, 0x65, 0x73, 0x73, 0x2e, 0x2f, 0xe2, 0x80, 0x9d]
TV1_calculate_plaintext = AEAD_CHACHA20_POLY1305_DECRYPT TV1_AEAD_key TV1_AEAD_nonce (TV1_AEAD_cypherText # TV1_AEAD_tag) TV1_AEAD_AAD
property TV1_plaintext_correct = isValid && pt == TV1_plaintext where
(pt,isValid) = TV1_calculate_plaintext
property decryption_vector_correct =
property decryption_vector_correct =
TV1_plaintext_correct &&
TV1_tag_correct &&
TV1_otk_correct
@ -2146,7 +2146,7 @@ property parseHexString_check =
"14:15:16:17:18:19:1a:1b:1c:1d:1e:1f.")) ==
0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
property AllPropertiesPass =
property AllPropertiesPass =
ChaChaQuarterround_passes_test &&
ChaChaQuarterround_passes_column_test &&
FirstRow_correct &&
@ -2182,7 +2182,7 @@ by loading it into a Cryptol interpreter, and running the AllPropertiesPass
function, like this:
```example
$ cryptol ChaChaPolyCryptolIETF.md
$ cryptol ChaChaPolyCryptolIETF.md
_ _
___ _ __ _ _ _ __ | |_ ___ | |
/ __| '__| | | | '_ \| __/ _ \| |
@ -2193,10 +2193,8 @@ $ cryptol ChaChaPolyCryptolIETF.md
Loading module Cryptol
Loading module ChaCha20
... a bunch of warnings about the use of ambiguous-width constants
ChaCha20> AllPropertiesPass
ChaCha20> AllPropertiesPass
True
```
This check verifies the implementation of `ChaCha`, `Poly1305` and the `AEAD`
construction all work with the provided test vectors.

5
examples/DES.cry
View File

@ -9,12 +9,12 @@ import Cipher
// DES API
DES : Cipher 64 64
DES =
DES =
{ encrypt key pt = des pt (expandKey key)
, decrypt key ct = des ct (reverse (expandKey key))
}
// Encryption
// Encryption
des pt keys = (swap (split last)) @@ FPz
where
@ -169,4 +169,3 @@ sbox8 = [[13, 2, 8, 4, 6, 15, 11, 1, 10, 9, 3, 14, 5, 0, 12, 7],
[7, 11, 4, 1, 9, 12, 14, 2, 0, 6, 10, 13, 15, 3, 5, 8],
[2, 1, 14, 7, 4, 10, 8, 13, 15, 12, 9, 0, 3, 5, 6, 11]
]

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

@ -6,7 +6,7 @@ module Base64 where
import Cryptol::Extras
type Enc64 n = 4*(((3-(n%3))%3) + n)/3
type Enc64 n = 4*(((3-(n%3))%3) + n)/3
base64enc : {n,m,padZ} (4*(padZ + n)/3 == m, fin n, fin m, padZ == (3-(n%3))%3, 2>=padZ)
=> [n][8] -> [Enc64 n][8]

3
examples/MiniLock/prim/Blake2s.cry
View File

@ -162,7 +162,7 @@ updateVector orig idxNew = vs
vs = [if i == idx then new else orig@i | i <- [0..a-1]]
property katsPass = ~zero ==
property katsPass = ~zero ==
[ nthKat `{0}
, nthKat `{1}
, nthKat `{2}
@ -685,4 +685,3 @@ kats = [ 0x69217a3079908094e11121d042354a7c1f55b6482ca1a51e1b250dfd1ed0eef9
, 0xc08aa1c286d709fdc7473744977188c895ba011014247e4efa8d07e78fec695c
, 0xf03f5789d3336b80d002d59fdf918bdb775b00956ed5528e86aa994acb38fe2d
]

18
examples/MiniLock/prim/Poly1305.md
View File

@ -1,4 +1,4 @@
% Poly1305 for IETF protocols
% Poly1305 for IETF protocols
% Y. Nir (Check Point), A. Langley (Google Inc), D. McNamee (Galois, Inc)
% July 28, 2014
%
@ -70,7 +70,7 @@ The inputs to Poly1305 are:
The output is a 128-bit tag.
```cryptol
Poly1305 : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
Poly1305 : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
=> [256] -> [m][8] -> [16][8]
```
@ -114,7 +114,7 @@ Next, divide the message into 16-byte blocks. The last block might be shorter:
* Add the current block to the accumulator.
* Multiply by "r"
* Set the accumulator to the result modulo p. To summarize:
* Set the accumulator to the result modulo p. To summarize:
``accum[i+1] = ((accum[i]+block)*r) % p``.
```cryptol
@ -161,7 +161,7 @@ using AES, and assume that we got the following keying material:
03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b
```cryptol
Poly1305TestKey = join (parseHexString
Poly1305TestKey = join (parseHexString
( "85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8:01:"
# "03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b."
) )
@ -196,7 +196,7 @@ values of the accumulator:
```cryptol
// TODO: refactor the Poly function in terms of this AccumBlocks
// challenge: doing so while maintaining the clean literate correspondence with the spec
AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
=> [256] -> [m][8] -> ([_][136], [136])
AccumBlocks key msg = (accum, lastAccum) where
@ -252,7 +252,7 @@ Acc + block = 2d8adaf23b0337fa7cccfb4ea344ca153
```
```cryptol
property polyBlocksOK =
property polyBlocksOK =
(blocks @ 1 == 0x02c88c77849d64ae9147ddeb88e69c83fc) &&
(blocks @ 2 == 0x02d8adaf23b0337fa7cccfb4ea344b30de) &&
(lastBlock == 0x028d31b7caff946c77c8844335369d03a7) where
@ -264,7 +264,7 @@ Adding s we get this number, and serialize if to get the tag:
Acc + s = 2a927010caf8b2bc2c6365130c11d06a8
Tag: a8:06:1d:c1:30:51:36:c6:c2:2b:8b:af:0c:01:27:a9
```cryptol
// Putting it all together and testing:
@ -292,7 +292,7 @@ SK_a* or *_write_MAC_key is only for stand-alone Poly1305.
The method is to call the block function with the following
parameters:
* The 256-bit session integrity key is used as the ChaCha20 key.
* The block counter is set to zero.
* The protocol will specify a 96-bit or 64-bit nonce. This MUST be
@ -317,7 +317,7 @@ encryption algorithms (often called Initialization Vectors, or IVs),
they usually don't have such a provision for the MAC function. In
that case the per-invocation nonce will have to come from somewhere
else, such as a message counter.
### Poly1305 Key Generation Test Vector
For this example, we'll set:

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

@ -45,7 +45,7 @@ mod_div(p,x,y) = egcd(p,0,y,x)
egcd(a, ra, b >> 1, mod_half(p, rb))
else if a < b then
egcd(a, ra, (b - a) >> 1, mod_half(p, mod_sub(p, rb, ra)))
else
else
egcd(b, rb, (a - b) >> 1, mod_half(p, mod_sub(p, ra, rb)))
mod_pow : {a} (fin a, a >= 1) => ([a] , [a] , [a]) -> [a]

6
examples/SHA1.cry
View File

@ -12,7 +12,7 @@ sha1 msg = sha1' pmsg
sha1' : {chunks} (fin chunks) => [chunks][512] -> [160]
sha1' pmsg = join (Hs!0)
where
where
Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] #
[ block(H, split(M))
| H <- Hs
@ -38,7 +38,7 @@ pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
type padding = (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
f (t, x, y, z) =
if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z)
| (20 <= t) && (t <= 39) then x ^ y ^ z
| (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
@ -54,7 +54,7 @@ Ks = [ 0x5a827999 | t <- [0..19] ]
block : ([5][32], [16][32]) -> [5][32]
block ([H0, H1, H2, H3, H4], M) =
[(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)]
where
where
Ws : [80][32]
Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1
| W16 <- drop`{16 - 16} Ws

4
examples/SIV-rfc5297.md
View File

@ -321,7 +321,7 @@ E(K,X) = aesEncrypt (X,K)
// 8. Return T.
aesCMAC : {m} (fin m) => Key -> [m] -> [128]
aesCMAC K m =
aesCMAC K m =
cmacBlocks K ((`m%128) == 0 && `m > 0) (split `{each=128,parts=blocks} full)
where
pd = [True] # zero : [128]
@ -501,7 +501,7 @@ S2V K S1 S2 = res
else aesCMAC K (dbl D1 ^ pad S2)
private
// The length of 'p' is >= 128, but Cryptol lacks
// The length of 'p' is >= 128, but Cryptol lacks
// dependent types and can not infer this fact. We
// Provide a no-op computation that results in a
// new type for 'p' that is at least 128 bits

2
examples/TripleDES.cry
View File

@ -8,7 +8,7 @@ module TripleDES where
import DES
blockEncrypt : ([64],[64],[64],[64]) -> [64]
blockEncrypt (k1,k2,k3,data) = result where
blockEncrypt (k1,k2,k3,data) = result where
ex = DES.encrypt k1 data
dx = DES.decrypt k2 ex
result = DES.encrypt k3 dx

14
examples/contrib/A51.cry
View File

@ -11,13 +11,13 @@ A51_stream R1 R2 R3 = R1s ^ R2s ^ R3s
(R2s, R2f) = lfsrki <| x^^22 + x^^21 + 1 |> R2c R2
(R3s, R3f) = lfsrki <| x^^23 + x^^22 + x^^21 + x^^8 + 1 |> R3c R3
majvs = [ majv (r1@8) (r2@10) (r3@10) | r1 <- R1f | r2 <- R2f | r3 <- R3f ]
R1c = [ r1@8 == m | r1 <- R1f | m <- majvs ]
R1c = [ r1@8 == m | r1 <- R1f | m <- majvs ]
R2c = [ r2@10 == m | r2 <- R2f | m <- majvs ]
R3c = [ r3@10 == m | r3 <- R3f | m <- majvs ]
R3c = [ r3@10 == m | r3 <- R3f | m <- majvs ]
type N = 128
A51 : ([19], [22], [23]) -> [N]Bit
A51(reg1, reg2, reg3) = keystream
A51(reg1, reg2, reg3) = keystream
where
keystream = take`{N} (A51_stream reg1 reg2 reg3)
@ -38,14 +38,14 @@ lfsrki poly conds init = (stream, fills)
prefix f xs = ys!0
where ys = [xs@0] # [ f y x | y <- ys | x <- tail xs ]
majv a b c = (a && b) || (a && c) || (b && c)
/***********************************************************************/
iv1 = 0b1010111011101011101
iv2 = 0b1010111011101010101110
iv3 = 0b10100000111100110011011
iv1 = 0b1010111011101011101
iv2 = 0b1010111011101010101110
iv3 = 0b10100000111100110011011
test_keystream = 0b00100100111010001110101110101100010100110111110101000101110000011101000111110101010000010011001111110101110001011010100000010001

9
examples/contrib/bivium.cry
View File

@ -7,11 +7,11 @@ Russian Academy of Sciences
Bivium_stream : [93] -> [84] -> [inf]
Bivium_stream R1 R2 = stream
where
(stream, ra, rb) = shift_regs R1 R2
(stream, ra, rb) = shift_regs R1 R2
type N = 200
Bivium : ([93], [84]) -> [N]Bit
Bivium (reg1, reg2) = keystream
Bivium (reg1, reg2) = keystream
where
keystream = take`{N} (Bivium_stream reg1 reg2)
@ -29,10 +29,10 @@ shift_regs r1 r2 = (stream, regA, regB)
s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB]
stream = s1 ^ s2
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
f2 <- regB |
f1 <- regA ]
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f1 @ 68) |
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f1 @ 68) |
f1 <- regA |
f2 <- regB ]
@ -51,4 +51,3 @@ suffix = 0b000000001000000000000000000001
property Bivium_correct = (Bivium(iv1, iv2)) == test_keystream
property Bivium_search (x, y) = (Bivium(x, y)) == test_keystream
property Bivium_search_with_suffix (x, y) = (Bivium(x, y#suffix)) == test_keystream

7
examples/contrib/trivium.cry
View File

@ -24,16 +24,16 @@ shift fill bit = fills
shift_regs : {d,e,f} (fin d, fin e, fin f, d >=1, e >=1, f>=1) => [d] -> [e] -> [f] -> ([inf],[inf][d],[inf][e],[inf][f])
shift_regs r1 r2 r3 = (stream, regA, regB, regC)
where
s1 = [(f1 @ 65) ^ (f1 @ 92) | f1 <- regA]
s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB]
s3 = [(f3 @ 65) ^ (f3 @ 110) | f3 <- regC]
stream = s1 ^ s2 ^ s3
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
f2 <- regB |
f1 <- regA ]
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) |
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) |
f2 <- regB |
f3 <- regC ]
t3 = [(f3 @ 65) ^ ((f3 @ 108) && (f3 @ 109)) ^ (f3 @ 110) ^ (f1 @ 68)|
@ -54,4 +54,3 @@ test_keystream = 0b0111111101111011111101000011100000000000001000100000000000000
property Trivium_correct = (Trivium(iv1, iv2, iv3)) == test_keystream
property Trivium_search (x, y, z) = (Trivium(x, y, z)) == test_keystream

3
examples/funstuff/NQueens.cry
View File

@ -9,7 +9,7 @@
where n is the board-size
You may find that cvc4 takes a long time for solutions bigger than 5.
For those sizes, we have had good luck with both Yices and Z3.
For those sizes, we have had good luck with both Yices and Z3.
To do that,
@ -54,4 +54,3 @@ inRange : {n} (fin n, n >= 1) => Board n -> Position n -> Bit
inRange qs x = x <= `(n - 1)
property nQueensProve x = (nQueens x) == False

7
examples/funstuff/marble.cry
View File

@ -66,8 +66,8 @@ validBoard : Board -> Bit
validBoard b = join (b && ~posns) == zero
validRowJump : Board -> Board -> Bit
validRowJump a a' = validBoard a
&& validBoard a'
validRowJump a a' = validBoard a
&& validBoard a'
&& validRowMove (differentRow a a')
differentRow : Board -> Board -> ([7], [7])
@ -83,7 +83,7 @@ validRowMove (r, r') = (xors == 0b0000111 ||
xors == 0b0001110 ||
xors == 0b0011100 ||
xors == 0b0111000 ||
xors == 0b1110000)
xors == 0b1110000)
&& (
rxors == 0b0000011 ||
rxors == 0b0000110 ||
@ -105,4 +105,3 @@ validMoveSequence moves = all [validMove a b | a <- moves | b <- drop`{1} moves]
solutionInNmoves : {n} (fin n) => [n] Board -> Bit
property solutionInNmoves ms = validMoveSequence ([start] # ms # [second])

15
examples/maliciousSHA/malicious_SHA1.cry
View File

@ -24,7 +24,7 @@ malicious_sha1 msg k = malicious_sha1' rmsg k
malicious_sha1' : {chunks} (fin chunks) => [chunks][512] -> [4][32] -> [160]
malicious_sha1' pmsg k = join (Hs!0)
where
where
Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] #
[ malicious_block (H, split(M)) k
| H <- Hs
@ -53,7 +53,7 @@ eve1 = [
//hexdump of file available at http://malicioussha1.github.io/pocs/eve2.sh
//when executed will print "hello world"
//The ascii cow and hello world can be switched out in both files
//The ascii cow and hello world can be switched out in both files
//and the hashes will still collide. The next example shows this
eve2 = [
0x1d23, 0x921b, 0x4014, 0xac09, 0x4d98, 0xd3a6, 0xe1bc, 0x4910,
@ -94,7 +94,7 @@ eve1_galois = [
0x6365, 0x6f68, 0x2220, 0x6147, 0x6f6c, 0x7369, 0x3b22, 0x660a,
0x0a69]
//hexdump malicious/eve1.sh
//hexdump malicious/eve1.sh
eve2_galois = [
0x1d23, 0x921b, 0x4014, 0xac09, 0x4d98, 0xd3a6, 0xe1bc, 0x4910,
0x8570, 0x1812, 0x786f, 0xb926, 0x37bd, 0xac2b, 0x50ae, 0x6a08,
@ -135,15 +135,15 @@ pad : {msgLen,contentLen,chunks,padding}
pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
f (t, x, y, z) =
if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z)
| (20 <= t) && (t <= 39) then x ^ y ^ z
| (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
| (60 <= t) && (t <= 79) then x ^ y ^ z
else error "f: t out of range"
Ks : [4][32] -> [80][32]
Ks : [4][32] -> [80][32]
Ks k = [ k@0 | t <- [0..19] ]
# [ k@1 | t <- [20..39] ]
# [ k@2 | t <- [40..59] ]
@ -152,7 +152,7 @@ Ks k = [ k@0 | t <- [0..19] ]
malicious_block : ([5][32], [16][32]) -> [4][32]-> [5][32]
malicious_block ([H0, H1, H2, H3, H4], M) k =
[(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)]
where
where
Ws : [80][32]
Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1
| W16 <- drop`{16 - 16} Ws
@ -172,4 +172,3 @@ malicious_block ([H0, H1, H2, H3, H4], M) k =
| W <- Ws | K <- (Ks k)
| t <- [0..79]
]

2
lib/Cryptol.cry
View File

@ -67,7 +67,7 @@ primitive (^^) : {a} (Arith a) => a -> a -> a
/**
* Log base two.
*
*
* For words, computes the ceiling of log, base 2, of a number.
* Over structured values, operates element-wise.
*/

4
src/Cryptol/ModuleSystem/Monad.hs
View File

@ -280,7 +280,7 @@ runModuleT :: Monad m
=> ModuleEnv
-> ModuleT m a
-> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleT env m =
runModuleT env m =
runWriterT
$ runExceptionT
$ runStateT env
@ -444,5 +444,3 @@ getSolverConfig :: ModuleM T.SolverConfig
getSolverConfig = ModuleT $ do
me <- get
return (meSolverConfig me)

2
src/Cryptol/ModuleSystem/NamingEnv.hs
View File

@ -243,7 +243,7 @@ instance BindsNames ImportIface where
namingEnv (ImportIface imp Iface { .. }) =
return (interpImport imp ifPublic)
-- | Introduce the name
-- | Introduce the name
instance BindsNames (InModule (Bind PName)) where
namingEnv (InModule ns b) =
do let Located { .. } = bName b

5
src/Cryptol/Parser/Lexer.x
View File

@ -6,7 +6,7 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- At present Alex generates code with too many warnings.
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE OverloadedStrings #-}
@ -246,6 +246,3 @@ primLexer cfg cs = run inp Normal
-- vim: ft=haskell
}

2
src/Cryptol/Prims/Eval.hs
View File

@ -192,7 +192,7 @@ divModPoly xs xsLen ys ysLen
todoBits = map (testBit xs) (downIxes (xsLen - degree))
-- | Create a packed word
-- | Create a packed word
modExp :: Integer -- ^ bit size of the resulting word
-> Integer -- ^ base
-> Integer -- ^ exponent

5
src/Cryptol/REPL/Monad.hs
View File

@ -343,7 +343,7 @@ getPutStr = fmap ePutStr getRW
rPutStr :: String -> REPL ()
rPutStr str = do
rw <- getRW
io $ ePutStr rw str
io $ ePutStr rw str
-- | Use the configured output action to print a string with a trailing newline
rPutStrLn :: String -> REPL ()
@ -730,6 +730,3 @@ z3exists = do
case mPath of
Nothing -> return (Just Z3NotFound)
Just _ -> return Nothing

2
src/Cryptol/TypeCheck/Infer.hs
View File

@ -569,7 +569,7 @@ inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
inferBinds isTopLevel isRec binds =
mdo let dExpr (DExpr e) = e
dExpr DPrim = panic "[TypeCheck]" [ "primitive in a recursive group" ]
exprMap = Map.fromList [ (x,inst (EVar x) (dExpr (dDefinition b)))
| b <- genBs, let x = dName b ] -- REC.

3
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -486,7 +486,7 @@ instance PP (WithNames Error) where
AmbiguousType xs ->
text "The inferred type for" <+> commaSep (map pp xs)
<+> text "is ambiguous."
<+> text "is ambiguous."
where
nested x y = x $$ nest 2 y
@ -564,4 +564,3 @@ instance PP Solved where
where suDoc = maybe empty pp mb
Unsolved -> text "unsolved"
Unsolvable -> text "unsolvable"

4
src/Cryptol/TypeCheck/Sanity.hs
View File

@ -326,7 +326,7 @@ convertible t1 t2
convertible t1 t2 = go t1 t2
where
go ty1 ty2 =
let err = reportError $ TypeMismatch (tMono ty1) (tMono ty2)
let err = reportError $ TypeMismatch (tMono ty1) (tMono ty2)
other = tNoUser ty2
goMany [] [] = return ()
@ -533,5 +533,3 @@ lookupVar x =
case Map.lookup x (roVars ro) of
Just s -> return s
Nothing -> reportError $ UndefinedVariable x

4
src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs
View File

@ -5,7 +5,7 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- Simplification of `fin` constraints.
{-# LANGUAGE PatternGuards #-}
@ -89,5 +89,3 @@ cryIsFinType varInfo g ty =
where
solved ps = Solved Nothing [ g { goal = p } | p <- ps ]

3
src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
View File

@ -125,7 +125,7 @@ importProp prop =
_ :>= _ -> Nothing
a :> b -> Just (b :>= a)
_ :==: _ -> Nothing
a :>: b -> Just (b :>= a)
a :>: b -> Just (b :>= a)
-- XXX: Do we need to add Fin on `a` and 'b'?
@ -168,4 +168,3 @@ importType = go
t2 <- go y
t3 <- go z
return (app f [t1,t2,t3])

7
src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs
View File

@ -5,7 +5,7 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- An interval interpretation of types.
{-# LANGUAGE PatternGuards #-}
@ -337,8 +337,3 @@ iLenFromThenTo i j k
| Just x <- iIsExact i, Just y <- iIsExact j, Just z <- iIsExact k
, Just r <- nLenFromThenTo x y z = iConst r
| otherwise = iAnyFin

12
src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs
View File

@ -5,12 +5,12 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- Separate Non-Linear Constraints
-- When we spot a non-linear expression, we name it and add it to a map.
--
--
-- If we see the same expression multiple times, then we give it the same name.
--
--
-- The body of the non-linear expression is not processed further,
-- so the resulting map should not contain any of the newly minted names.
@ -78,7 +78,7 @@ lookupNL x NonLinS { .. } = Map.lookup x nonLinExprs
runNL :: NonLinS -> NonLinM a -> ((a, [Prop]), NonLinS)
runNL s m = runId
$ runStateT s
$ runStateT s
$ do a <- m
ps <- finishTodos
return (a,ps)
@ -279,7 +279,3 @@ finishTodos =
p' <- nonLinPropM p
ps' <- finishTodos
return (p' : ps')

4
src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs
View File

@ -173,7 +173,7 @@ smtName a = case a of
name p n = case divMod n 26 of
(q,r) -> p ++ toEnum (fromEnum 'a' + r) :
(if q == 0 then "" else show q)
-- | The name of a boolean variable, representing `fin x`.
smtFinName :: Name -> String
@ -515,5 +515,3 @@ linRel (x1,y1) (x2,y2) =
let b = y1 - a * x1
guard $ not $ a < 0 && b < 0 -- No way this will give a natural number.
return (a,b)

5
src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
View File

@ -5,7 +5,7 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- TODO:
-- - Putting in a normal form to spot "prove by assumption"
-- - Additional simplification rules, namely various cancelation.
@ -841,6 +841,3 @@ cryNatOp op x y =
Impossible -> PFalse -- It doesn't matter, but @false@ might anihilate.
Return p -> p
If p t e -> p :&& toProp t :|| Not p :&& toProp e

10
src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs
View File

@ -5,16 +5,16 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
--
-- Simplification.
-- The rules in this module are all conditional on the expressions being
-- well-defined.
--
--
-- So, for example, consider the formula `P`, which corresponds to `fin e`.
-- `P` says the following:
--
--
-- if e is well-formed, then will evaluate to a finite natural number.
--
--
-- More concretely, consider `fin (3 - 5)`. This will be simplified to `True`,
-- which does not mean that `3 - 5` is actually finite.
@ -509,5 +509,3 @@ eNoInf expr =
(_, K Inf, _) -> Impossible
(_, _, K Inf) -> Impossible
_ -> return (f x' y' z')

7
src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs
View File

@ -9,9 +9,9 @@
-- Simplification of expressions.
-- The result of simplifying an expression `e`, is a new expression `e'`,
-- which satisfies the property:
--
--
-- if e is well-defined then e and e' will evaluate to the same type.
--
--
{-# LANGUAGE Safe, BangPatterns #-}
module Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr where
@ -211,6 +211,3 @@ crySimpExprStep1 expr =
case (x,y,z) of
(K a, K b, K c) -> K `fmap` IN.nLenFromThenTo a b c
_ -> Nothing

2
tests/issues/issue187.cry
View File

@ -8,7 +8,7 @@ enigmaLoop = undefined
// Encryption/Decryption
enigma : {n, m} (fin n, fin m) => ([n], [m]) -> [m]
enigma (m, pt) = tail [ True | _ <- rcs ]
where rcs = [ (m, True)] #
where rcs = [ (m, True)] #
[ (enigmaLoop, True)
| _ <- pt
| (_,_) <- rcs

4
tests/issues/issue212.cry
View File

@ -7,7 +7,7 @@
width_eq_geq : {n} (32 == width n, n >= 1) => [n]Bit
width_eq_geq = [True | _ <- [1..n] : [_][32] ]
// Want: const >= width (x+1) ==> const > width x
// Want: const >= width (x+1) ==> const > width x
// or any monotonic function, not just addition.
//
// Also Want: const >= width n ==> fin n
@ -19,7 +19,7 @@ can_not_width = zero # (`n : [width n])
// Want: Honestly, I don't know what's going on here. It seems to relate to some of our regressions though.
// Tell me if there should be another ticket - probably one that already exists. -TMD
// Issue: Cryptol 2.3 wants 'n == 4 + (?a3 - n % 4)'
// Issue: Cryptol 2.3 wants 'n == 4 + (?a3 - n % 4)'
take_knows_no_bounds : {n} (fin n, n >= 4) => [n][8] -> [4 - (n%4)][8]
take_knows_no_bounds ns = foo
where

3
tests/issues/issue225.cry
View File

@ -1,4 +1,4 @@
module EnigmaBroke where
module EnigmaBroke where
type Rotor = [26](Char, Bit)
@ -20,4 +20,3 @@ joinRotors (rotors, inputChar) = (rotors', outputChar)
]
rotors' = tail [ r | (_, _, r) <- ncrs ]
(_, outputChar, _) = ncrs ! 0

2
tests/issues/issue289.cry
View File

@ -1,6 +1,6 @@
average33 : [32] -> [32] -> [32]
average33 x y = drop`{1}(z'/2)
where
where
z' : [33]
z' = (0b0 # x) + (0b0 # y)

4
tests/issues/simon.cry2
View File

@ -52,7 +52,7 @@ f x = ((x <<< 1) && (x <<< 8)) ^ (x <<< 2)
// encryption / decryption
///////////////////////////////////////////////////////////////////////
encrypt : {n, m, T, j}
encrypt : {n, m, T, j}
( fin n, fin m, fin T, fin j
, n >= 2, T - 1 >= m, T >= 1
) => [m][n] -> ([n], [n]) -> ([n], [n])
@ -62,7 +62,7 @@ encrypt k0 p0 = ps ! 0
ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)
decrypt : {n, m, T, j}
decrypt : {n, m, T, j}
( fin n, fin m, fin T, fin j
, n >= 2, T - 1 >= m, T >= 1
) => [m][n] -> ([n], [n]) -> ([n], [n])

2
tests/parser/nested-where.cry
View File

@ -1,4 +1,4 @@
/* This is
/* This is
a block comment */
test1 = 1 where x = 2

2
tests/parser/pat1.cry
View File

@ -14,7 +14,7 @@ let {} in a : [10]
case a : [10] of { }
// f (a :# b :: Int) =
// f (a :# b :: Int) =
(fa,fb) = f6

4
tests/regression/AES.cry
View File

@ -23,7 +23,7 @@ type AESKeySize = (Nk*32)
type GF28 = [8]
type State = [4][Nb]GF28
type RoundKey = State
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
// GF28 operations
gf28Add : {n} (fin n) => [n]GF28 -> GF28
gf28Add ps = sums ! 0
@ -213,5 +213,3 @@ sbox = [
0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e, 0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf,
0x8c, 0xa1, 0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0, 0x54, 0xbb, 0x16
]

4
tests/regression/check09.cry
View File

@ -5,7 +5,7 @@ initL = [0]
ss = [ (s + a + b) <<< 3 | s <- initS # ss
| a <- [1] # ss
| b <- [0] # ls ]
ls = [ (l + a + b) <<< (a + b)
ls = [ (l + a + b) <<< (a + b)
| l <- initL # ls
| a <- ss
| b <- [0] # ls ]
@ -30,7 +30,7 @@ keyX key = ss @@ [ 0 .. 6 ]
| b <- [0] # ls ]
// NOTE different endianness from Cryptol 1 test
check9b = keyX (reverse "abcd") ==
check9b = keyX (reverse "abcd") ==
[0x00000008, 0x1b134ba3, 0x11ae69b1, 0xb7b3f42f,
0xc9eb1fdc, 0x008b5f36, 0x8991bc8c]

2
tests/regression/check23.cry
View File

@ -1,4 +1,4 @@
pad : {msgLen, padding, contentLen, chunks}
pad : {msgLen, padding, contentLen, chunks}
( fin msgLen
, fin padding
, contentLen == msgLen + 65