module Spec.Blake2.Test #reset-options "--z3rlimit 100 --max_fuel 0" open FStar.Mul open Lib.IntTypes open Lib.RawIntTypes open Lib.Sequence open Lib.ByteSequence // // Test 1 // let test1_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x61uy; 0x62uy; 0x63uy ] let test1_plaintext : lbytes 3 = assert_norm (List.Tot.length test1_plaintext_list = 3); of_list test1_plaintext_list let test1_expected_list = List.Tot.map u8_from_UInt8 [ 0x50uy; 0x8Cuy; 0x5Euy; 0x8Cuy; 0x32uy; 0x7Cuy; 0x14uy; 0xE2uy; 0xE1uy; 0xA7uy; 0x2Buy; 0xA3uy; 0x4Euy; 0xEBuy; 0x45uy; 0x2Fuy; 0x37uy; 0x45uy; 0x8Buy; 0x20uy; 0x9Euy; 0xD6uy; 0x3Auy; 0x29uy; 0x4Duy; 0x99uy; 0x9Buy; 0x4Cuy; 0x86uy; 0x67uy; 0x59uy; 0x82uy; ] let test1_expected : lbytes 32 = assert_norm (List.Tot.length test1_expected_list = 32); of_list test1_expected_list let test2_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy ] let test2_plaintext : lbytes 1 = assert_norm (List.Tot.length test2_plaintext_list = 1); of_list test2_plaintext_list let test2_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy ] let test2_key : lbytes 32 = assert_norm (List.Tot.length test2_key_list = 32); of_list test2_key_list let test2_expected_list = List.Tot.map u8_from_UInt8 [ 0x40uy; 0xd1uy; 0x5fuy; 0xeeuy; 0x7cuy; 0x32uy; 0x88uy; 0x30uy; 0x16uy; 0x6auy; 0xc3uy; 0xf9uy; 0x18uy; 0x65uy; 0x0fuy; 0x80uy; 0x7euy; 0x7euy; 0x01uy; 0xe1uy; 0x77uy; 0x25uy; 0x8cuy; 0xdcuy; 0x0auy; 0x39uy; 0xb1uy; 0x1fuy; 0x59uy; 0x80uy; 0x66uy; 0xf1uy ] let test2_expected : lbytes 32 = assert_norm (List.Tot.length test2_expected_list = 32); of_list test2_expected_list let test3_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2auy; 0x2buy; 0x2cuy; 0x2duy; 0x2euy; 0x2fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3auy; 0x3buy; 0x3cuy; 0x3duy; 0x3euy; 0x3fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4auy; 0x4buy; 0x4cuy; 0x4duy; 0x4euy; 0x4fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5auy; 0x5buy; 0x5cuy; 0x5duy; 0x5euy; 0x5fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7auy; 0x7buy; 0x7cuy; 0x7duy; 0x7euy; 0x7fuy; 0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy; 0x88uy; 0x89uy; 0x8auy; 0x8buy; 0x8cuy; 0x8duy; 0x8euy; 0x8fuy; 0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy; 0x98uy; 0x99uy; 0x9auy; 0x9buy; 0x9cuy; 0x9duy; 0x9euy; 0x9fuy; 0xa0uy; 0xa1uy; 0xa2uy; 0xa3uy; 0xa4uy; 0xa5uy; 0xa6uy; 0xa7uy; 0xa8uy; 0xa9uy; 0xaauy; 0xabuy; 0xacuy; 0xaduy; 0xaeuy; 0xafuy; 0xb0uy; 0xb1uy; 0xb2uy; 0xb3uy; 0xb4uy; 0xb5uy; 0xb6uy; 0xb7uy; 0xb8uy; 0xb9uy; 0xbauy; 0xbbuy; 0xbcuy; 0xbduy; 0xbeuy; 0xbfuy; 0xc0uy; 0xc1uy; 0xc2uy; 0xc3uy; 0xc4uy; 0xc5uy; 0xc6uy; 0xc7uy; 0xc8uy; 0xc9uy; 0xcauy; 0xcbuy; 0xccuy; 0xcduy; 0xceuy; 0xcfuy; 0xd0uy; 0xd1uy; 0xd2uy; 0xd3uy; 0xd4uy; 0xd5uy; 0xd6uy; 0xd7uy; 0xd8uy; 0xd9uy; 0xdauy; 0xdbuy; 0xdcuy; 0xdduy; 0xdeuy; 0xdfuy; 0xe0uy; 0xe1uy; 0xe2uy; 0xe3uy; 0xe4uy; 0xe5uy; 0xe6uy; 0xe7uy; 0xe8uy; 0xe9uy; 0xeauy; 0xebuy; 0xecuy; 0xeduy; 0xeeuy; 0xefuy; 0xf0uy; 0xf1uy; 0xf2uy; 0xf3uy; 0xf4uy; 0xf5uy; 0xf6uy; 0xf7uy; 0xf8uy; 0xf9uy; 0xfauy; 0xfbuy; 0xfcuy; 0xfduy; 0xfeuy ] let test3_plaintext : lbytes 255 = assert_norm (List.Tot.length test3_plaintext_list = 255); of_list test3_plaintext_list let test3_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy ] let test3_key : lbytes 32 = assert_norm (List.Tot.length test3_key_list = 32); of_list test3_key_list let test3_expected_list = List.Tot.map u8_from_UInt8 [ 0x3fuy; 0xb7uy; 0x35uy; 0x06uy; 0x1auy; 0xbcuy; 0x51uy; 0x9duy; 0xfeuy; 0x97uy; 0x9euy; 0x54uy; 0xc1uy; 0xeeuy; 0x5buy; 0xfauy; 0xd0uy; 0xa9uy; 0xd8uy; 0x58uy; 0xb3uy; 0x31uy; 0x5buy; 0xaduy; 0x34uy; 0xbduy; 0xe9uy; 0x99uy; 0xefuy; 0xd7uy; 0x24uy; 0xdduy ] let test3_expected : lbytes 32 = assert_norm (List.Tot.length test3_expected_list = 32); of_list test3_expected_list let test4_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2auy; 0x2buy; 0x2cuy; 0x2duy; 0x2euy; 0x2fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3auy; 0x3buy; 0x3cuy; 0x3duy; 0x3euy; 0x3fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4auy; 0x4buy; 0x4cuy; 0x4duy; 0x4euy; 0x4fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5auy; 0x5buy; 0x5cuy; 0x5duy; 0x5euy; 0x5fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7auy; 0x7buy; 0x7cuy; 0x7duy; 0x7euy; 0x7fuy; 0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy; 0x88uy; 0x89uy; 0x8auy; 0x8buy; 0x8cuy; 0x8duy; 0x8euy; 0x8fuy; 0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy; 0x98uy; 0x99uy; 0x9auy; 0x9buy; 0x9cuy; 0x9duy; 0x9euy; 0x9fuy; 0xa0uy; 0xa1uy; 0xa2uy; 0xa3uy; 0xa4uy; 0xa5uy; 0xa6uy; 0xa7uy; 0xa8uy; 0xa9uy; 0xaauy; 0xabuy; 0xacuy; 0xaduy; 0xaeuy; 0xafuy; 0xb0uy; 0xb1uy; 0xb2uy; 0xb3uy; 0xb4uy; 0xb5uy; 0xb6uy; 0xb7uy; 0xb8uy; 0xb9uy; 0xbauy; 0xbbuy; 0xbcuy; 0xbduy; 0xbeuy; 0xbfuy; 0xc0uy; 0xc1uy; 0xc2uy; 0xc3uy; 0xc4uy; 0xc5uy; 0xc6uy; 0xc7uy; 0xc8uy; 0xc9uy; 0xcauy; 0xcbuy; 0xccuy; 0xcduy; 0xceuy; 0xcfuy; 0xd0uy; 0xd1uy; 0xd2uy; 0xd3uy; 0xd4uy; 0xd5uy; 0xd6uy; 0xd7uy; 0xd8uy; 0xd9uy; 0xdauy; 0xdbuy; 0xdcuy; 0xdduy; 0xdeuy; 0xdfuy; 0xe0uy; 0xe1uy; 0xe2uy; 0xe3uy; 0xe4uy; 0xe5uy; 0xe6uy; 0xe7uy; 0xe8uy; 0xe9uy; 0xeauy; 0xebuy; 0xecuy; 0xeduy; 0xeeuy; 0xefuy; 0xf0uy; 0xf1uy; 0xf2uy; 0xf3uy; 0xf4uy; 0xf5uy; 0xf6uy; 0xf7uy; 0xf8uy; 0xf9uy; 0xfauy ] let test4_plaintext : lbytes 251 = assert_norm (List.Tot.length test4_plaintext_list = 251); of_list test4_plaintext_list let test4_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy ] let test4_key : lbytes 32 = assert_norm (List.Tot.length test4_key_list = 32); of_list test4_key_list let test4_expected_list = List.Tot.map u8_from_UInt8 [ 0xd1uy; 0x2buy; 0xf3uy; 0x73uy; 0x2euy; 0xf4uy; 0xafuy; 0x5cuy; 0x22uy; 0xfauy; 0x90uy; 0x35uy; 0x6auy; 0xf8uy; 0xfcuy; 0x50uy; 0xfcuy; 0xb4uy; 0x0fuy; 0x8fuy; 0x2euy; 0xa5uy; 0xc8uy; 0x59uy; 0x47uy; 0x37uy; 0xa3uy; 0xb3uy; 0xd5uy; 0xabuy; 0xdbuy; 0xd7uy ] let test4_expected : lbytes 32 = assert_norm (List.Tot.length test4_expected_list = 32); of_list test4_expected_list // // Test 5 BLAKE 2B // let test5_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x61uy; 0x62uy; 0x63uy ] let test5_plaintext : lbytes 3 = assert_norm (List.Tot.length test5_plaintext_list = 3); of_list test5_plaintext_list let test5_expected_list = List.Tot.map u8_from_UInt8 [ 0xBAuy; 0x80uy; 0xA5uy; 0x3Fuy; 0x98uy; 0x1Cuy; 0x4Duy; 0x0Duy; 0x6Auy; 0x27uy; 0x97uy; 0xB6uy; 0x9Fuy; 0x12uy; 0xF6uy; 0xE9uy; 0x4Cuy; 0x21uy; 0x2Fuy; 0x14uy; 0x68uy; 0x5Auy; 0xC4uy; 0xB7uy; 0x4Buy; 0x12uy; 0xBBuy; 0x6Fuy; 0xDBuy; 0xFFuy; 0xA2uy; 0xD1uy; 0x7Duy; 0x87uy; 0xC5uy; 0x39uy; 0x2Auy; 0xABuy; 0x79uy; 0x2Duy; 0xC2uy; 0x52uy; 0xD5uy; 0xDEuy; 0x45uy; 0x33uy; 0xCCuy; 0x95uy; 0x18uy; 0xD3uy; 0x8Auy; 0xA8uy; 0xDBuy; 0xF1uy; 0x92uy; 0x5Auy; 0xB9uy; 0x23uy; 0x86uy; 0xEDuy; 0xD4uy; 0x00uy; 0x99uy; 0x23uy ] let test5_expected : lbytes 64 = assert_norm (List.Tot.length test5_expected_list = 64); of_list test5_expected_list // // Test 6 BLAKE 2B // let test6_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy ] let test6_plaintext : lbytes 128 = assert_norm (List.Tot.length test6_plaintext_list = 128); of_list test6_plaintext_list let test6_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy ] let test6_key : lbytes 64 = assert_norm (List.Tot.length test6_key_list = 64); of_list test6_key_list let test6_expected_list = List.Tot.map u8_from_UInt8 [ 0xe4uy; 0x7buy; 0xb6uy; 0xf2uy; 0x0fuy; 0xbfuy; 0x14uy; 0x98uy; 0x4fuy; 0x72uy; 0xa4uy; 0xc3uy; 0xcduy; 0x9fuy; 0x3duy; 0xc0uy; 0xd3uy; 0x89uy; 0x28uy; 0xe5uy; 0x36uy; 0x73uy; 0x3buy; 0xa7uy; 0xc5uy; 0xb1uy; 0x53uy; 0xc7uy; 0x15uy; 0x46uy; 0x58uy; 0x4buy; 0x73uy; 0x71uy; 0xf9uy; 0xb7uy; 0x07uy; 0x07uy; 0x77uy; 0xb9uy; 0xa0uy; 0x94uy; 0x77uy; 0x03uy; 0x40uy; 0x96uy; 0x50uy; 0xfduy; 0x04uy; 0xcfuy; 0xc9uy; 0xa5uy; 0xd5uy; 0x61uy; 0xf9uy; 0x9euy; 0xd1uy; 0x34uy; 0xefuy; 0x26uy; 0x2buy; 0x03uy; 0xdbuy; 0x94uy ] let test6_expected : lbytes 64 = assert_norm (List.Tot.length test6_expected_list = 64); of_list test6_expected_list (*** Blake2s test vectors: *) (* test7_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E" *) let test7_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy ] let test7_plaintext : lbytes 63 = assert_norm(FStar.List.length test7_plaintext_list = 63); of_list test7_plaintext_list (* test7_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *) let test7_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy ] let test7_key : lbytes 32 = assert_norm(FStar.List.length test7_key_list = 32); of_list test7_key_list (* test7_expected = "C65382513F07460DA39833CB666C5ED82E61B9E998F4B0C4287CEE56C3CC9BCD" *) let test7_expected_list = List.Tot.map u8_from_UInt8 [ 0xC6uy; 0x53uy; 0x82uy; 0x51uy; 0x3Fuy; 0x07uy; 0x46uy; 0x0Duy; 0xA3uy; 0x98uy; 0x33uy; 0xCBuy; 0x66uy; 0x6Cuy; 0x5Euy; 0xD8uy; 0x2Euy; 0x61uy; 0xB9uy; 0xE9uy; 0x98uy; 0xF4uy; 0xB0uy; 0xC4uy; 0x28uy; 0x7Cuy; 0xEEuy; 0x56uy; 0xC3uy; 0xCCuy; 0x9Buy; 0xCDuy ] let test7_expected : lbytes 32 = assert_norm(FStar.List.length test7_expected_list = 32); of_list test7_expected_list (* test8_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *) let test8_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy ] let test8_plaintext : lbytes 64 = assert_norm(FStar.List.length test8_plaintext_list = 64); of_list test8_plaintext_list (* test8_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *) let test8_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy ] let test8_key : lbytes 32 = assert_norm(FStar.List.length test8_key_list = 32); of_list test8_key_list (* test8_expected = "8975B0577FD35566D750B362B0897A26C399136DF07BABABBDE6203FF2954ED4" *) let test8_expected_list = List.Tot.map u8_from_UInt8 [ 0x89uy; 0x75uy; 0xB0uy; 0x57uy; 0x7Fuy; 0xD3uy; 0x55uy; 0x66uy; 0xD7uy; 0x50uy; 0xB3uy; 0x62uy; 0xB0uy; 0x89uy; 0x7Auy; 0x26uy; 0xC3uy; 0x99uy; 0x13uy; 0x6Duy; 0xF0uy; 0x7Buy; 0xABuy; 0xABuy; 0xBDuy; 0xE6uy; 0x20uy; 0x3Fuy; 0xF2uy; 0x95uy; 0x4Euy; 0xD4uy ] let test8_expected : lbytes 32 = assert_norm(FStar.List.length test8_expected_list = 32); of_list test8_expected_list (* test9_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F40" *) let test9_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy ] let test9_plaintext : lbytes 65 = assert_norm(FStar.List.length test9_plaintext_list = 65); of_list test9_plaintext_list (* test9_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *) let test9_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy ] let test9_key : lbytes 32 = assert_norm(FStar.List.length test9_key_list = 32); of_list test9_key_list (* test9_expected = "21FE0CEB0052BE7FB0F004187CACD7DE67FA6EB0938D927677F2398C132317A8" *) let test9_expected_list = List.Tot.map u8_from_UInt8 [ 0x21uy; 0xFEuy; 0x0Cuy; 0xEBuy; 0x00uy; 0x52uy; 0xBEuy; 0x7Fuy; 0xB0uy; 0xF0uy; 0x04uy; 0x18uy; 0x7Cuy; 0xACuy; 0xD7uy; 0xDEuy; 0x67uy; 0xFAuy; 0x6Euy; 0xB0uy; 0x93uy; 0x8Duy; 0x92uy; 0x76uy; 0x77uy; 0xF2uy; 0x39uy; 0x8Cuy; 0x13uy; 0x23uy; 0x17uy; 0xA8uy ] let test9_expected : lbytes 32 = assert_norm(FStar.List.length test9_expected_list = 32); of_list test9_expected_list (* test10_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F" *) let test10_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy ] let test10_plaintext : lbytes 128 = assert_norm(FStar.List.length test10_plaintext_list = 128); of_list test10_plaintext_list (* test10_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *) let test10_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy ] let test10_key : lbytes 32 = assert_norm(FStar.List.length test10_key_list = 32); of_list test10_key_list (* test10_expected = "0C311F38C35A4FB90D651C289D486856CD1413DF9B0677F53ECE2CD9E477C60A" *) let test10_expected_list = List.Tot.map u8_from_UInt8 [ 0x0Cuy; 0x31uy; 0x1Fuy; 0x38uy; 0xC3uy; 0x5Auy; 0x4Fuy; 0xB9uy; 0x0Duy; 0x65uy; 0x1Cuy; 0x28uy; 0x9Duy; 0x48uy; 0x68uy; 0x56uy; 0xCDuy; 0x14uy; 0x13uy; 0xDFuy; 0x9Buy; 0x06uy; 0x77uy; 0xF5uy; 0x3Euy; 0xCEuy; 0x2Cuy; 0xD9uy; 0xE4uy; 0x77uy; 0xC6uy; 0x0Auy ] let test10_expected : lbytes 32 = assert_norm(FStar.List.length test10_expected_list = 32); of_list test10_expected_list (* test11_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF" *) let test11_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy; 0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy; 0x88uy; 0x89uy; 0x8Auy; 0x8Buy; 0x8Cuy; 0x8Duy; 0x8Euy; 0x8Fuy; 0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy; 0x98uy; 0x99uy; 0x9Auy; 0x9Buy; 0x9Cuy; 0x9Duy; 0x9Euy; 0x9Fuy; 0xA0uy; 0xA1uy; 0xA2uy; 0xA3uy; 0xA4uy; 0xA5uy; 0xA6uy; 0xA7uy; 0xA8uy; 0xA9uy; 0xAAuy; 0xABuy; 0xACuy; 0xADuy; 0xAEuy; 0xAFuy; 0xB0uy; 0xB1uy; 0xB2uy; 0xB3uy; 0xB4uy; 0xB5uy; 0xB6uy; 0xB7uy; 0xB8uy; 0xB9uy; 0xBAuy; 0xBBuy; 0xBCuy; 0xBDuy; 0xBEuy; 0xBFuy; 0xC0uy; 0xC1uy; 0xC2uy; 0xC3uy; 0xC4uy; 0xC5uy; 0xC6uy; 0xC7uy; 0xC8uy; 0xC9uy; 0xCAuy; 0xCBuy; 0xCCuy; 0xCDuy; 0xCEuy; 0xCFuy; 0xD0uy; 0xD1uy; 0xD2uy; 0xD3uy; 0xD4uy; 0xD5uy; 0xD6uy; 0xD7uy; 0xD8uy; 0xD9uy; 0xDAuy; 0xDBuy; 0xDCuy; 0xDDuy; 0xDEuy; 0xDFuy; 0xE0uy; 0xE1uy; 0xE2uy; 0xE3uy; 0xE4uy; 0xE5uy; 0xE6uy; 0xE7uy; 0xE8uy; 0xE9uy; 0xEAuy; 0xEBuy; 0xECuy; 0xEDuy; 0xEEuy; 0xEFuy; 0xF0uy; 0xF1uy; 0xF2uy; 0xF3uy; 0xF4uy; 0xF5uy; 0xF6uy; 0xF7uy; 0xF8uy; 0xF9uy; 0xFAuy; 0xFBuy; 0xFCuy; 0xFDuy; 0xFEuy; 0xFFuy ] let test11_plaintext : lbytes 256 = assert_norm(FStar.List.length test11_plaintext_list = 256); of_list test11_plaintext_list (* test11_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *) let test11_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy ] let test11_key : lbytes 32 = assert_norm(FStar.List.length test11_key_list = 32); of_list test11_key_list (* test11_expected = "5211D1AEFC0025BE7F85C06B3E14E0FC645AE12BD41746485EA6D8A364A2EAEE" *) let test11_expected_list = List.Tot.map u8_from_UInt8 [ 0x52uy; 0x11uy; 0xD1uy; 0xAEuy; 0xFCuy; 0x00uy; 0x25uy; 0xBEuy; 0x7Fuy; 0x85uy; 0xC0uy; 0x6Buy; 0x3Euy; 0x14uy; 0xE0uy; 0xFCuy; 0x64uy; 0x5Auy; 0xE1uy; 0x2Buy; 0xD4uy; 0x17uy; 0x46uy; 0x48uy; 0x5Euy; 0xA6uy; 0xD8uy; 0xA3uy; 0x64uy; 0xA2uy; 0xEAuy; 0xEEuy ] let test11_expected : lbytes 32 = assert_norm(FStar.List.length test11_expected_list = 32); of_list test11_expected_list (*** Blake2b test vectors: *) let test0_plaintext_list = List.Tot.map u8_from_UInt8 [ ] let test0_plaintext : lbytes 0 = assert_norm (List.Tot.length test0_plaintext_list = 0); of_list test0_plaintext_list let test0_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2auy; 0x2buy; 0x2cuy; 0x2duy; 0x2euy; 0x2fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3auy; 0x3buy; 0x3cuy; 0x3duy; 0x3euy; 0x3fuy ] let test0_key : lbytes 64 = assert_norm (List.Tot.length test0_key_list = 64); of_list test0_key_list let test0_expected_list = List.Tot.map u8_from_UInt8 [ 0x10uy; 0xebuy; 0xb6uy; 0x77uy; 0x00uy; 0xb1uy; 0x86uy; 0x8euy; 0xfbuy; 0x44uy; 0x17uy; 0x98uy; 0x7auy; 0xcfuy; 0x46uy; 0x90uy; 0xaeuy; 0x9duy; 0x97uy; 0x2fuy; 0xb7uy; 0xa5uy; 0x90uy; 0xc2uy; 0xf0uy; 0x28uy; 0x71uy; 0x79uy; 0x9auy; 0xaauy; 0x47uy; 0x86uy; 0xb5uy; 0xe9uy; 0x96uy; 0xe8uy; 0xf0uy; 0xf4uy; 0xebuy; 0x98uy; 0x1fuy; 0xc2uy; 0x14uy; 0xb0uy; 0x05uy; 0xf4uy; 0x2duy; 0x2fuy; 0xf4uy; 0x23uy; 0x34uy; 0x99uy; 0x39uy; 0x16uy; 0x53uy; 0xdfuy; 0x7auy; 0xefuy; 0xcbuy; 0xc1uy; 0x3fuy; 0xc5uy; 0x15uy; 0x68uy ] let test0_expected : lbytes 64 = assert_norm (List.Tot.length test0_expected_list = 64); of_list test0_expected_list (* test12_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E" *) let test12_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy ] let test12_plaintext : lbytes 127 = assert_norm(FStar.List.length test12_plaintext_list = 127); of_list test12_plaintext_list (* test12_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *) let test12_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy ] let test12_key : lbytes 64 = assert_norm(FStar.List.length test12_key_list = 64); of_list test12_key_list (* test12_expected = "76D2D819C92BCE55FA8E092AB1BF9B9EAB237A25267986CACF2B8EE14D214D730DC9A5AA2D7B596E86A1FD8FA0804C77402D2FCD45083688B218B1CDFA0DCBCB" *) let test12_expected_list = List.Tot.map u8_from_UInt8 [ 0x76uy; 0xD2uy; 0xD8uy; 0x19uy; 0xC9uy; 0x2Buy; 0xCEuy; 0x55uy; 0xFAuy; 0x8Euy; 0x09uy; 0x2Auy; 0xB1uy; 0xBFuy; 0x9Buy; 0x9Euy; 0xABuy; 0x23uy; 0x7Auy; 0x25uy; 0x26uy; 0x79uy; 0x86uy; 0xCAuy; 0xCFuy; 0x2Buy; 0x8Euy; 0xE1uy; 0x4Duy; 0x21uy; 0x4Duy; 0x73uy; 0x0Duy; 0xC9uy; 0xA5uy; 0xAAuy; 0x2Duy; 0x7Buy; 0x59uy; 0x6Euy; 0x86uy; 0xA1uy; 0xFDuy; 0x8Fuy; 0xA0uy; 0x80uy; 0x4Cuy; 0x77uy; 0x40uy; 0x2Duy; 0x2Fuy; 0xCDuy; 0x45uy; 0x08uy; 0x36uy; 0x88uy; 0xB2uy; 0x18uy; 0xB1uy; 0xCDuy; 0xFAuy; 0x0Duy; 0xCBuy; 0xCBuy ] let test12_expected : lbytes 64 = assert_norm(FStar.List.length test12_expected_list = 64); of_list test12_expected_list (* test13_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F" *) let test13_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy ] let test13_plaintext : lbytes 128 = assert_norm(FStar.List.length test13_plaintext_list = 128); of_list test13_plaintext_list (* test13_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *) let test13_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy ] let test13_key : lbytes 64 = assert_norm(FStar.List.length test13_key_list = 64); of_list test13_key_list (* test13_expected = "72065EE4DD91C2D8509FA1FC28A37C7FC9FA7D5B3F8AD3D0D7A25626B57B1B44788D4CAF806290425F9890A3A2A35A905AB4B37ACFD0DA6E4517B2525C9651E4" *) let test13_expected_list = List.Tot.map u8_from_UInt8 [ 0x72uy; 0x06uy; 0x5Euy; 0xE4uy; 0xDDuy; 0x91uy; 0xC2uy; 0xD8uy; 0x50uy; 0x9Fuy; 0xA1uy; 0xFCuy; 0x28uy; 0xA3uy; 0x7Cuy; 0x7Fuy; 0xC9uy; 0xFAuy; 0x7Duy; 0x5Buy; 0x3Fuy; 0x8Auy; 0xD3uy; 0xD0uy; 0xD7uy; 0xA2uy; 0x56uy; 0x26uy; 0xB5uy; 0x7Buy; 0x1Buy; 0x44uy; 0x78uy; 0x8Duy; 0x4Cuy; 0xAFuy; 0x80uy; 0x62uy; 0x90uy; 0x42uy; 0x5Fuy; 0x98uy; 0x90uy; 0xA3uy; 0xA2uy; 0xA3uy; 0x5Auy; 0x90uy; 0x5Auy; 0xB4uy; 0xB3uy; 0x7Auy; 0xCFuy; 0xD0uy; 0xDAuy; 0x6Euy; 0x45uy; 0x17uy; 0xB2uy; 0x52uy; 0x5Cuy; 0x96uy; 0x51uy; 0xE4uy ] let test13_expected : lbytes 64 = assert_norm(FStar.List.length test13_expected_list = 64); of_list test13_expected_list (* test14_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F80" *) let test14_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy; 0x80uy ] let test14_plaintext : lbytes 129 = assert_norm(FStar.List.length test14_plaintext_list = 129); of_list test14_plaintext_list (* test14_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *) let test14_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy ] let test14_key : lbytes 64 = assert_norm(FStar.List.length test14_key_list = 64); of_list test14_key_list (* test14_expected = "64475DFE7600D7171BEA0B394E27C9B00D8E74DD1E416A79473682AD3DFDBB706631558055CFC8A40E07BD015A4540DCDEA15883CBBF31412DF1DE1CD4152B91" *) let test14_expected_list = List.Tot.map u8_from_UInt8 [ 0x64uy; 0x47uy; 0x5Duy; 0xFEuy; 0x76uy; 0x00uy; 0xD7uy; 0x17uy; 0x1Buy; 0xEAuy; 0x0Buy; 0x39uy; 0x4Euy; 0x27uy; 0xC9uy; 0xB0uy; 0x0Duy; 0x8Euy; 0x74uy; 0xDDuy; 0x1Euy; 0x41uy; 0x6Auy; 0x79uy; 0x47uy; 0x36uy; 0x82uy; 0xADuy; 0x3Duy; 0xFDuy; 0xBBuy; 0x70uy; 0x66uy; 0x31uy; 0x55uy; 0x80uy; 0x55uy; 0xCFuy; 0xC8uy; 0xA4uy; 0x0Euy; 0x07uy; 0xBDuy; 0x01uy; 0x5Auy; 0x45uy; 0x40uy; 0xDCuy; 0xDEuy; 0xA1uy; 0x58uy; 0x83uy; 0xCBuy; 0xBFuy; 0x31uy; 0x41uy; 0x2Duy; 0xF1uy; 0xDEuy; 0x1Cuy; 0xD4uy; 0x15uy; 0x2Buy; 0x91uy ] let test14_expected : lbytes 64 = assert_norm(FStar.List.length test14_expected_list = 64); of_list test14_expected_list (* test15_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF" *) let test15_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy; 0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy; 0x88uy; 0x89uy; 0x8Auy; 0x8Buy; 0x8Cuy; 0x8Duy; 0x8Euy; 0x8Fuy; 0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy; 0x98uy; 0x99uy; 0x9Auy; 0x9Buy; 0x9Cuy; 0x9Duy; 0x9Euy; 0x9Fuy; 0xA0uy; 0xA1uy; 0xA2uy; 0xA3uy; 0xA4uy; 0xA5uy; 0xA6uy; 0xA7uy; 0xA8uy; 0xA9uy; 0xAAuy; 0xABuy; 0xACuy; 0xADuy; 0xAEuy; 0xAFuy; 0xB0uy; 0xB1uy; 0xB2uy; 0xB3uy; 0xB4uy; 0xB5uy; 0xB6uy; 0xB7uy; 0xB8uy; 0xB9uy; 0xBAuy; 0xBBuy; 0xBCuy; 0xBDuy; 0xBEuy; 0xBFuy; 0xC0uy; 0xC1uy; 0xC2uy; 0xC3uy; 0xC4uy; 0xC5uy; 0xC6uy; 0xC7uy; 0xC8uy; 0xC9uy; 0xCAuy; 0xCBuy; 0xCCuy; 0xCDuy; 0xCEuy; 0xCFuy; 0xD0uy; 0xD1uy; 0xD2uy; 0xD3uy; 0xD4uy; 0xD5uy; 0xD6uy; 0xD7uy; 0xD8uy; 0xD9uy; 0xDAuy; 0xDBuy; 0xDCuy; 0xDDuy; 0xDEuy; 0xDFuy; 0xE0uy; 0xE1uy; 0xE2uy; 0xE3uy; 0xE4uy; 0xE5uy; 0xE6uy; 0xE7uy; 0xE8uy; 0xE9uy; 0xEAuy; 0xEBuy; 0xECuy; 0xEDuy; 0xEEuy; 0xEFuy; 0xF0uy; 0xF1uy; 0xF2uy; 0xF3uy; 0xF4uy; 0xF5uy; 0xF6uy; 0xF7uy; 0xF8uy; 0xF9uy; 0xFAuy; 0xFBuy; 0xFCuy; 0xFDuy; 0xFEuy; 0xFFuy ] let test15_plaintext : lbytes 256 = assert_norm(FStar.List.length test15_plaintext_list = 256); of_list test15_plaintext_list (* test15_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *) let test15_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy ] let test15_key : lbytes 64 = assert_norm(FStar.List.length test15_key_list = 64); of_list test15_key_list (* test15_expected = "B72071E096277EDEBB8EE5134DD3714996307BA3A55AA4733D412ABBE28E909E10E57E6FBFB4EF53B3B960518294FF889A90829254412E2A60B85ADD07A3674F" *) let test15_expected_list = List.Tot.map u8_from_UInt8 [ 0xB7uy; 0x20uy; 0x71uy; 0xE0uy; 0x96uy; 0x27uy; 0x7Euy; 0xDEuy; 0xBBuy; 0x8Euy; 0xE5uy; 0x13uy; 0x4Duy; 0xD3uy; 0x71uy; 0x49uy; 0x96uy; 0x30uy; 0x7Buy; 0xA3uy; 0xA5uy; 0x5Auy; 0xA4uy; 0x73uy; 0x3Duy; 0x41uy; 0x2Auy; 0xBBuy; 0xE2uy; 0x8Euy; 0x90uy; 0x9Euy; 0x10uy; 0xE5uy; 0x7Euy; 0x6Fuy; 0xBFuy; 0xB4uy; 0xEFuy; 0x53uy; 0xB3uy; 0xB9uy; 0x60uy; 0x51uy; 0x82uy; 0x94uy; 0xFFuy; 0x88uy; 0x9Auy; 0x90uy; 0x82uy; 0x92uy; 0x54uy; 0x41uy; 0x2Euy; 0x2Auy; 0x60uy; 0xB8uy; 0x5Auy; 0xDDuy; 0x07uy; 0xA3uy; 0x67uy; 0x4Fuy ] let test15_expected : lbytes 64 = assert_norm(FStar.List.length test15_expected_list = 64); of_list test15_expected_list (* test16_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF" *) let test16_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy; 0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy; 0x88uy; 0x89uy; 0x8Auy; 0x8Buy; 0x8Cuy; 0x8Duy; 0x8Euy; 0x8Fuy; 0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy; 0x98uy; 0x99uy; 0x9Auy; 0x9Buy; 0x9Cuy; 0x9Duy; 0x9Euy; 0x9Fuy; 0xA0uy; 0xA1uy; 0xA2uy; 0xA3uy; 0xA4uy; 0xA5uy; 0xA6uy; 0xA7uy; 0xA8uy; 0xA9uy; 0xAAuy; 0xABuy; 0xACuy; 0xADuy; 0xAEuy; 0xAFuy; 0xB0uy; 0xB1uy; 0xB2uy; 0xB3uy; 0xB4uy; 0xB5uy; 0xB6uy; 0xB7uy; 0xB8uy; 0xB9uy; 0xBAuy; 0xBBuy; 0xBCuy; 0xBDuy; 0xBEuy; 0xBFuy; 0xC0uy; 0xC1uy; 0xC2uy; 0xC3uy; 0xC4uy; 0xC5uy; 0xC6uy; 0xC7uy; 0xC8uy; 0xC9uy; 0xCAuy; 0xCBuy; 0xCCuy; 0xCDuy; 0xCEuy; 0xCFuy; 0xD0uy; 0xD1uy; 0xD2uy; 0xD3uy; 0xD4uy; 0xD5uy; 0xD6uy; 0xD7uy; 0xD8uy; 0xD9uy; 0xDAuy; 0xDBuy; 0xDCuy; 0xDDuy; 0xDEuy; 0xDFuy; 0xE0uy; 0xE1uy; 0xE2uy; 0xE3uy; 0xE4uy; 0xE5uy; 0xE6uy; 0xE7uy; 0xE8uy; 0xE9uy; 0xEAuy; 0xEBuy; 0xECuy; 0xEDuy; 0xEEuy; 0xEFuy; 0xF0uy; 0xF1uy; 0xF2uy; 0xF3uy; 0xF4uy; 0xF5uy; 0xF6uy; 0xF7uy; 0xF8uy; 0xF9uy; 0xFAuy; 0xFBuy; 0xFCuy; 0xFDuy; 0xFEuy; 0xFFuy; 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4Auy; 0x4Buy; 0x4Cuy; 0x4Duy; 0x4Euy; 0x4Fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy; 0x58uy; 0x59uy; 0x5Auy; 0x5Buy; 0x5Cuy; 0x5Duy; 0x5Euy; 0x5Fuy; 0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6Auy; 0x6Buy; 0x6Cuy; 0x6Duy; 0x6Euy; 0x6Fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7Auy; 0x7Buy; 0x7Cuy; 0x7Duy; 0x7Euy; 0x7Fuy; 0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy; 0x88uy; 0x89uy; 0x8Auy; 0x8Buy; 0x8Cuy; 0x8Duy; 0x8Euy; 0x8Fuy; 0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy; 0x98uy; 0x99uy; 0x9Auy; 0x9Buy; 0x9Cuy; 0x9Duy; 0x9Euy; 0x9Fuy; 0xA0uy; 0xA1uy; 0xA2uy; 0xA3uy; 0xA4uy; 0xA5uy; 0xA6uy; 0xA7uy; 0xA8uy; 0xA9uy; 0xAAuy; 0xABuy; 0xACuy; 0xADuy; 0xAEuy; 0xAFuy; 0xB0uy; 0xB1uy; 0xB2uy; 0xB3uy; 0xB4uy; 0xB5uy; 0xB6uy; 0xB7uy; 0xB8uy; 0xB9uy; 0xBAuy; 0xBBuy; 0xBCuy; 0xBDuy; 0xBEuy; 0xBFuy; 0xC0uy; 0xC1uy; 0xC2uy; 0xC3uy; 0xC4uy; 0xC5uy; 0xC6uy; 0xC7uy; 0xC8uy; 0xC9uy; 0xCAuy; 0xCBuy; 0xCCuy; 0xCDuy; 0xCEuy; 0xCFuy; 0xD0uy; 0xD1uy; 0xD2uy; 0xD3uy; 0xD4uy; 0xD5uy; 0xD6uy; 0xD7uy; 0xD8uy; 0xD9uy; 0xDAuy; 0xDBuy; 0xDCuy; 0xDDuy; 0xDEuy; 0xDFuy; 0xE0uy; 0xE1uy; 0xE2uy; 0xE3uy; 0xE4uy; 0xE5uy; 0xE6uy; 0xE7uy; 0xE8uy; 0xE9uy; 0xEAuy; 0xEBuy; 0xECuy; 0xEDuy; 0xEEuy; 0xEFuy; 0xF0uy; 0xF1uy; 0xF2uy; 0xF3uy; 0xF4uy; 0xF5uy; 0xF6uy; 0xF7uy; 0xF8uy; 0xF9uy; 0xFAuy; 0xFBuy; 0xFCuy; 0xFDuy; 0xFEuy; 0xFFuy ] let test16_plaintext : lbytes 512 = assert_norm(FStar.List.length test16_plaintext_list = 512); of_list test16_plaintext_list (* test16_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *) let test16_key_list = List.Tot.map u8_from_UInt8 [ 0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy; 0x08uy; 0x09uy; 0x0Auy; 0x0Buy; 0x0Cuy; 0x0Duy; 0x0Euy; 0x0Fuy; 0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy; 0x18uy; 0x19uy; 0x1Auy; 0x1Buy; 0x1Cuy; 0x1Duy; 0x1Euy; 0x1Fuy; 0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy; 0x28uy; 0x29uy; 0x2Auy; 0x2Buy; 0x2Cuy; 0x2Duy; 0x2Euy; 0x2Fuy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x3Auy; 0x3Buy; 0x3Cuy; 0x3Duy; 0x3Euy; 0x3Fuy ] let test16_key : lbytes 64 = assert_norm(FStar.List.length test16_key_list = 64); of_list test16_key_list (* test16_expected = "31952478E1B6229B6BCA296C643A3FDBE4AA2C2F7FEA466675453D5F7F09427021A77B8625C78070C0F7CE564D8D257D7EB36495BE76950C31A1A7D80FF8B1B4" *) let test16_expected_list = List.Tot.map u8_from_UInt8 [ 0x31uy; 0x95uy; 0x24uy; 0x78uy; 0xE1uy; 0xB6uy; 0x22uy; 0x9Buy; 0x6Buy; 0xCAuy; 0x29uy; 0x6Cuy; 0x64uy; 0x3Auy; 0x3Fuy; 0xDBuy; 0xE4uy; 0xAAuy; 0x2Cuy; 0x2Fuy; 0x7Fuy; 0xEAuy; 0x46uy; 0x66uy; 0x75uy; 0x45uy; 0x3Duy; 0x5Fuy; 0x7Fuy; 0x09uy; 0x42uy; 0x70uy; 0x21uy; 0xA7uy; 0x7Buy; 0x86uy; 0x25uy; 0xC7uy; 0x80uy; 0x70uy; 0xC0uy; 0xF7uy; 0xCEuy; 0x56uy; 0x4Duy; 0x8Duy; 0x25uy; 0x7Duy; 0x7Euy; 0xB3uy; 0x64uy; 0x95uy; 0xBEuy; 0x76uy; 0x95uy; 0x0Cuy; 0x31uy; 0xA1uy; 0xA7uy; 0xD8uy; 0x0Fuy; 0xF8uy; 0xB1uy; 0xB4uy ] let test16_expected : lbytes 64 = assert_norm(FStar.List.length test16_expected_list = 64); of_list test16_expected_list // // Main // #set-options "--z3rlimit 400" // // Main // let blake2s_test num (plain:bytes{Seq.length plain <= max_size_t}) (key:bytes{Seq.length key <= 32}) expected = IO.print_string ("\n\nTEST Blake2s "^(string_of_int num)^":"); let result : lbytes 32 = Spec.Blake2.blake2s plain (Seq.length key) key 32 in let result2 = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in if result2 then begin IO.print_string "\nSuccess!\n"; true end else begin IO.print_string "\nFailure :(\n"; IO.print_string "\n2. Result : "; List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list result); IO.print_string "\n2. Expected: "; List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list expected); false end let blake2b_test num (plain:bytes{Seq.length plain <= max_size_t}) (key:bytes{Seq.length key <= 64}) expected = IO.print_string ("\n\nTEST Blake2b "^(string_of_int num)^":"); let result : lbytes 64 = Spec.Blake2.blake2b plain (Seq.length key) key 64 in let result2 = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in if result2 then begin IO.print_string "\nSuccess!\n"; true end else begin IO.print_string "\nFailure :(\n"; IO.print_string "\n2. Result : "; List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list result); IO.print_string "\n2. Expected: "; List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list expected); false end let test () = let emp_key : lbytes 0 = (assert_norm (List.Tot.length ([] <: list uint8)<= max_size_t); of_list []) in let result1 = blake2s_test 1 test1_plaintext emp_key test1_expected in let result2 = blake2s_test 2 test2_plaintext test2_key test2_expected in let result3 = blake2s_test 3 test3_plaintext test3_key test3_expected in let result4 = blake2s_test 4 test4_plaintext test4_key test4_expected in let result7 = blake2s_test 7 test7_plaintext test7_key test7_expected in let result8 = blake2s_test 8 test8_plaintext test8_key test8_expected in let result9 = blake2s_test 9 test9_plaintext test9_key test9_expected in let result10 = blake2s_test 10 test10_plaintext test10_key test10_expected in let result11 = blake2s_test 11 test11_plaintext test11_key test11_expected in let result0 = blake2b_test 0 test0_plaintext test0_key test0_expected in let result5 = blake2b_test 5 test5_plaintext emp_key test5_expected in let result6 = blake2b_test 6 test6_plaintext test6_key test6_expected in let result12 = blake2b_test 12 test12_plaintext test12_key test12_expected in let result13 = blake2b_test 13 test13_plaintext test13_key test13_expected in let result14 = blake2b_test 14 test14_plaintext test14_key test14_expected in let result15 = blake2b_test 15 test15_plaintext test15_key test15_expected in let result16 = blake2b_test 16 test16_plaintext test16_key test16_expected in // // // RESULT // if result0 && result1 && result2 && result3 && result4 && result5 && result6 && result7 && result8 && result9 && result10 && result11 && result12 && result13 && result14 && result15 && result16 then begin IO.print_string "\n\nAll tests successful !\n"; true end else begin IO.print_string "\n\nSome test failed !\n"; false end