open Prims
let (k224_256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x71374491");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xb5c0fbcf");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xe9b5dba5");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x3956c25b");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x59f111f1");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x923f82a4");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xab1c5ed5");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd807aa98");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x12835b01");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x243185be");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x550c7dc3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x72be5d74");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x80deb1fe");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x9bdc06a7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc19bf174");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xe49b69c1");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xefbe4786");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x0fc19dc6");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x240ca1cc");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x2de92c6f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x4a7484aa");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x5cb0a9dc");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x76f988da");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x983e5152");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa831c66d");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xb00327c8");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbf597fc7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc6e00bf3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd5a79147");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x06ca6351");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x14292967");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x27b70a85");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x2e1b2138");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x4d2c6dfc");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x53380d13");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x650a7354");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x766a0abb");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x81c2c92e");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x92722c85");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa2bfe8a1");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa81a664b");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc24b8b70");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc76c51a3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd192e819");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd6990624");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xf40e3585");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x106aa070");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x19a4c116");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x1e376c08");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x2748774c");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x34b0bcb5");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x391c0cb3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x4ed8aa4a");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x5b9cca4f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x682e6ff3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x748f82ee");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x78a5636f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x84c87814");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x8cc70208");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x90befffa");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa4506ceb");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbef9a3f7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc67178f2")]
let (k224_256 : FStar_UInt32.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x71374491");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xb5c0fbcf");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xe9b5dba5");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x3956c25b");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x59f111f1");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x923f82a4");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xab1c5ed5");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd807aa98");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x12835b01");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x243185be");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x550c7dc3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x72be5d74");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x80deb1fe");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x9bdc06a7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc19bf174");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xe49b69c1");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xefbe4786");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x0fc19dc6");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x240ca1cc");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x2de92c6f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x4a7484aa");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x5cb0a9dc");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x76f988da");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x983e5152");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa831c66d");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xb00327c8");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbf597fc7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc6e00bf3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd5a79147");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x06ca6351");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x14292967");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x27b70a85");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x2e1b2138");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x4d2c6dfc");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x53380d13");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x650a7354");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x766a0abb");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x81c2c92e");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x92722c85");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa2bfe8a1");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa81a664b");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc24b8b70");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc76c51a3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd192e819");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd6990624");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xf40e3585");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x106aa070");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x19a4c116");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x1e376c08");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x2748774c");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x34b0bcb5");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x391c0cb3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x4ed8aa4a");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x5b9cca4f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x682e6ff3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x748f82ee");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x78a5636f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x84c87814");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x8cc70208");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x90befffa");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa4506ceb");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbef9a3f7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc67178f2")]
let (k384_512_l : (FStar_UInt64.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt64.uint_to_t (Prims.parse_int "0x428a2f98d728ae22");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x7137449123ef65cd");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xb5c0fbcfec4d3b2f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xe9b5dba58189dbbc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x3956c25bf348b538");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x59f111f1b605d019");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x923f82a4af194f9b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xab1c5ed5da6d8118");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd807aa98a3030242");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x12835b0145706fbe");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x243185be4ee4b28c");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x550c7dc3d5ffb4e2");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x72be5d74f27b896f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x80deb1fe3b1696b1");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x9bdc06a725c71235");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc19bf174cf692694");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xe49b69c19ef14ad2");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xefbe4786384f25e3");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x0fc19dc68b8cd5b5");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x240ca1cc77ac9c65");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x2de92c6f592b0275");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4a7484aa6ea6e483");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5cb0a9dcbd41fbd4");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x76f988da831153b5");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x983e5152ee66dfab");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa831c66d2db43210");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xb00327c898fb213f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xbf597fc7beef0ee4");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc6e00bf33da88fc2");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd5a79147930aa725");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x06ca6351e003826f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x142929670a0e6e70");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x27b70a8546d22ffc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x2e1b21385c26c926");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4d2c6dfc5ac42aed");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x53380d139d95b3df");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x650a73548baf63de");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x766a0abb3c77b2a8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x81c2c92e47edaee6");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x92722c851482353b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa2bfe8a14cf10364");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa81a664bbc423001");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc24b8b70d0f89791");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc76c51a30654be30");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd192e819d6ef5218");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd69906245565a910");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xf40e35855771202a");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x106aa07032bbd1b8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x19a4c116b8d2d0c8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x1e376c085141ab53");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x2748774cdf8eeb99");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x34b0bcb5e19b48a8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x391c0cb3c5c95a63");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4ed8aa4ae3418acb");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5b9cca4f7763e373");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x682e6ff3d6b2b8a3");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x748f82ee5defb2fc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x78a5636f43172f60");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x84c87814a1f0ab72");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x8cc702081a6439ec");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x90befffa23631e28");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa4506cebde82bde9");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xbef9a3f7b2c67915");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc67178f2e372532b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xca273eceea26619c");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd186b8c721c0c207");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xeada7dd6cde0eb1e");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xf57d4f7fee6ed178");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x06f067aa72176fba");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x0a637dc5a2c898a6");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x113f9804bef90dae");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x1b710b35131c471b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x28db77f523047d84");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x32caab7b40c72493");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x3c9ebe0a15c9bebc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x431d67c49c100d4c");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4cc5d4becb3e42b6");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x597f299cfc657e2a");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5fcb6fab3ad6faec");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x6c44198c4a475817")]
let (k384_512 : FStar_UInt64.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt64.uint_to_t (Prims.parse_int "0x428a2f98d728ae22");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x7137449123ef65cd");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xb5c0fbcfec4d3b2f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xe9b5dba58189dbbc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x3956c25bf348b538");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x59f111f1b605d019");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x923f82a4af194f9b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xab1c5ed5da6d8118");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd807aa98a3030242");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x12835b0145706fbe");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x243185be4ee4b28c");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x550c7dc3d5ffb4e2");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x72be5d74f27b896f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x80deb1fe3b1696b1");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x9bdc06a725c71235");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc19bf174cf692694");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xe49b69c19ef14ad2");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xefbe4786384f25e3");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x0fc19dc68b8cd5b5");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x240ca1cc77ac9c65");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x2de92c6f592b0275");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4a7484aa6ea6e483");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5cb0a9dcbd41fbd4");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x76f988da831153b5");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x983e5152ee66dfab");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa831c66d2db43210");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xb00327c898fb213f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xbf597fc7beef0ee4");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc6e00bf33da88fc2");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd5a79147930aa725");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x06ca6351e003826f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x142929670a0e6e70");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x27b70a8546d22ffc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x2e1b21385c26c926");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4d2c6dfc5ac42aed");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x53380d139d95b3df");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x650a73548baf63de");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x766a0abb3c77b2a8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x81c2c92e47edaee6");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x92722c851482353b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa2bfe8a14cf10364");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa81a664bbc423001");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc24b8b70d0f89791");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc76c51a30654be30");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd192e819d6ef5218");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd69906245565a910");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xf40e35855771202a");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x106aa07032bbd1b8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x19a4c116b8d2d0c8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x1e376c085141ab53");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x2748774cdf8eeb99");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x34b0bcb5e19b48a8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x391c0cb3c5c95a63");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4ed8aa4ae3418acb");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5b9cca4f7763e373");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x682e6ff3d6b2b8a3");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x748f82ee5defb2fc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x78a5636f43172f60");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x84c87814a1f0ab72");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x8cc702081a6439ec");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x90befffa23631e28");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa4506cebde82bde9");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xbef9a3f7b2c67915");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc67178f2e372532b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xca273eceea26619c");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd186b8c721c0c207");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xeada7dd6cde0eb1e");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xf57d4f7fee6ed178");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x06f067aa72176fba");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x0a637dc5a2c898a6");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x113f9804bef90dae");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x1b710b35131c471b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x28db77f523047d84");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x32caab7b40c72493");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x3c9ebe0a15c9bebc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x431d67c49c100d4c");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4cc5d4becb3e42b6");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x597f299cfc657e2a");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5fcb6fab3ad6faec");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x6c44198c4a475817")]
let (h224_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt32.uint_to_t (Prims.parse_int "0xc1059ed8");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x367cd507");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x3070dd17");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xf70e5939");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xffc00b31");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x68581511");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x64f98fa7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbefa4fa4")]
let (h224 : FStar_UInt32.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt32.uint_to_t (Prims.parse_int "0xc1059ed8");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x367cd507");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x3070dd17");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xf70e5939");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xffc00b31");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x68581511");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x64f98fa7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbefa4fa4")]
let (h256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt32.uint_to_t (Prims.parse_int "0x6a09e667");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbb67ae85");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x3c6ef372");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa54ff53a");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x510e527f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x9b05688c");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x1f83d9ab");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x5be0cd19")]
let (h256 : FStar_UInt32.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt32.uint_to_t (Prims.parse_int "0x6a09e667");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbb67ae85");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x3c6ef372");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa54ff53a");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x510e527f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x9b05688c");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x1f83d9ab");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x5be0cd19")]
let (h384_l : (FStar_UInt64.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt64.uint_to_t (Prims.parse_int "0xcbbb9d5dc1059ed8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x629a292a367cd507");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x9159015a3070dd17");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x152fecd8f70e5939");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x67332667ffc00b31");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x8eb44a8768581511");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xdb0c2e0d64f98fa7");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x47b5481dbefa4fa4")]
let (h384 : FStar_UInt64.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt64.uint_to_t (Prims.parse_int "0xcbbb9d5dc1059ed8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x629a292a367cd507");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x9159015a3070dd17");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x152fecd8f70e5939");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x67332667ffc00b31");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x8eb44a8768581511");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xdb0c2e0d64f98fa7");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x47b5481dbefa4fa4")]
let (h512_l : (FStar_UInt64.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt64.uint_to_t (Prims.parse_int "0x6a09e667f3bcc908");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xbb67ae8584caa73b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x3c6ef372fe94f82b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa54ff53a5f1d36f1");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
let (h512 : FStar_UInt64.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt64.uint_to_t (Prims.parse_int "0x6a09e667f3bcc908");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xbb67ae8584caa73b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x3c6ef372fe94f82b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa54ff53a5f1d36f1");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
open Prims
let (k224_256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x71374491");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xb5c0fbcf");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xe9b5dba5");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x3956c25b");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x59f111f1");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x923f82a4");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xab1c5ed5");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd807aa98");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x12835b01");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x243185be");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x550c7dc3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x72be5d74");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x80deb1fe");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x9bdc06a7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc19bf174");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xe49b69c1");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xefbe4786");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x0fc19dc6");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x240ca1cc");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x2de92c6f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x4a7484aa");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x5cb0a9dc");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x76f988da");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x983e5152");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa831c66d");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xb00327c8");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbf597fc7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc6e00bf3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd5a79147");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x06ca6351");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x14292967");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x27b70a85");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x2e1b2138");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x4d2c6dfc");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x53380d13");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x650a7354");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x766a0abb");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x81c2c92e");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x92722c85");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa2bfe8a1");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa81a664b");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc24b8b70");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc76c51a3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd192e819");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xd6990624");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xf40e3585");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x106aa070");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x19a4c116");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x1e376c08");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x2748774c");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x34b0bcb5");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x391c0cb3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x4ed8aa4a");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x5b9cca4f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x682e6ff3");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x748f82ee");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x78a5636f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x84c87814");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x8cc70208");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x90befffa");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa4506ceb");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbef9a3f7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xc67178f2")]
let (k224_256 : FStar_UInt32.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x71374491");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xb5c0fbcf");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xe9b5dba5");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x3956c25b");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x59f111f1");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x923f82a4");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xab1c5ed5");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd807aa98");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x12835b01");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x243185be");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x550c7dc3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x72be5d74");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x80deb1fe");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x9bdc06a7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc19bf174");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xe49b69c1");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xefbe4786");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x0fc19dc6");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x240ca1cc");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x2de92c6f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x4a7484aa");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x5cb0a9dc");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x76f988da");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x983e5152");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa831c66d");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xb00327c8");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbf597fc7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc6e00bf3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd5a79147");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x06ca6351");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x14292967");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x27b70a85");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x2e1b2138");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x4d2c6dfc");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x53380d13");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x650a7354");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x766a0abb");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x81c2c92e");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x92722c85");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa2bfe8a1");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa81a664b");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc24b8b70");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc76c51a3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd192e819");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xd6990624");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xf40e3585");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x106aa070");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x19a4c116");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x1e376c08");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x2748774c");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x34b0bcb5");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x391c0cb3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x4ed8aa4a");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x5b9cca4f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x682e6ff3");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x748f82ee");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x78a5636f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x84c87814");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x8cc70208");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x90befffa");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa4506ceb");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbef9a3f7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xc67178f2")]
let (k384_512_l : (FStar_UInt64.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt64.uint_to_t (Prims.parse_int "0x428a2f98d728ae22");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x7137449123ef65cd");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xb5c0fbcfec4d3b2f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xe9b5dba58189dbbc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x3956c25bf348b538");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x59f111f1b605d019");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x923f82a4af194f9b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xab1c5ed5da6d8118");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd807aa98a3030242");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x12835b0145706fbe");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x243185be4ee4b28c");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x550c7dc3d5ffb4e2");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x72be5d74f27b896f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x80deb1fe3b1696b1");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x9bdc06a725c71235");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc19bf174cf692694");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xe49b69c19ef14ad2");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xefbe4786384f25e3");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x0fc19dc68b8cd5b5");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x240ca1cc77ac9c65");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x2de92c6f592b0275");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4a7484aa6ea6e483");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5cb0a9dcbd41fbd4");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x76f988da831153b5");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x983e5152ee66dfab");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa831c66d2db43210");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xb00327c898fb213f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xbf597fc7beef0ee4");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc6e00bf33da88fc2");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd5a79147930aa725");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x06ca6351e003826f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x142929670a0e6e70");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x27b70a8546d22ffc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x2e1b21385c26c926");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4d2c6dfc5ac42aed");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x53380d139d95b3df");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x650a73548baf63de");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x766a0abb3c77b2a8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x81c2c92e47edaee6");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x92722c851482353b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa2bfe8a14cf10364");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa81a664bbc423001");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc24b8b70d0f89791");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc76c51a30654be30");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd192e819d6ef5218");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd69906245565a910");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xf40e35855771202a");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x106aa07032bbd1b8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x19a4c116b8d2d0c8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x1e376c085141ab53");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x2748774cdf8eeb99");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x34b0bcb5e19b48a8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x391c0cb3c5c95a63");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4ed8aa4ae3418acb");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5b9cca4f7763e373");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x682e6ff3d6b2b8a3");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x748f82ee5defb2fc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x78a5636f43172f60");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x84c87814a1f0ab72");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x8cc702081a6439ec");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x90befffa23631e28");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa4506cebde82bde9");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xbef9a3f7b2c67915");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xc67178f2e372532b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xca273eceea26619c");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xd186b8c721c0c207");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xeada7dd6cde0eb1e");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xf57d4f7fee6ed178");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x06f067aa72176fba");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x0a637dc5a2c898a6");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x113f9804bef90dae");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x1b710b35131c471b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x28db77f523047d84");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x32caab7b40c72493");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x3c9ebe0a15c9bebc");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x431d67c49c100d4c");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x4cc5d4becb3e42b6");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x597f299cfc657e2a");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5fcb6fab3ad6faec");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x6c44198c4a475817")]
let (k384_512 : FStar_UInt64.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt64.uint_to_t (Prims.parse_int "0x428a2f98d728ae22");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x7137449123ef65cd");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xb5c0fbcfec4d3b2f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xe9b5dba58189dbbc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x3956c25bf348b538");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x59f111f1b605d019");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x923f82a4af194f9b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xab1c5ed5da6d8118");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd807aa98a3030242");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x12835b0145706fbe");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x243185be4ee4b28c");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x550c7dc3d5ffb4e2");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x72be5d74f27b896f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x80deb1fe3b1696b1");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x9bdc06a725c71235");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc19bf174cf692694");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xe49b69c19ef14ad2");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xefbe4786384f25e3");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x0fc19dc68b8cd5b5");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x240ca1cc77ac9c65");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x2de92c6f592b0275");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4a7484aa6ea6e483");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5cb0a9dcbd41fbd4");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x76f988da831153b5");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x983e5152ee66dfab");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa831c66d2db43210");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xb00327c898fb213f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xbf597fc7beef0ee4");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc6e00bf33da88fc2");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd5a79147930aa725");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x06ca6351e003826f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x142929670a0e6e70");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x27b70a8546d22ffc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x2e1b21385c26c926");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4d2c6dfc5ac42aed");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x53380d139d95b3df");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x650a73548baf63de");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x766a0abb3c77b2a8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x81c2c92e47edaee6");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x92722c851482353b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa2bfe8a14cf10364");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa81a664bbc423001");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc24b8b70d0f89791");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc76c51a30654be30");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd192e819d6ef5218");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd69906245565a910");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xf40e35855771202a");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x106aa07032bbd1b8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x19a4c116b8d2d0c8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x1e376c085141ab53");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x2748774cdf8eeb99");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x34b0bcb5e19b48a8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x391c0cb3c5c95a63");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4ed8aa4ae3418acb");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5b9cca4f7763e373");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x682e6ff3d6b2b8a3");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x748f82ee5defb2fc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x78a5636f43172f60");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x84c87814a1f0ab72");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x8cc702081a6439ec");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x90befffa23631e28");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa4506cebde82bde9");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xbef9a3f7b2c67915");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xc67178f2e372532b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xca273eceea26619c");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xd186b8c721c0c207");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xeada7dd6cde0eb1e");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xf57d4f7fee6ed178");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x06f067aa72176fba");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x0a637dc5a2c898a6");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x113f9804bef90dae");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x1b710b35131c471b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x28db77f523047d84");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x32caab7b40c72493");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x3c9ebe0a15c9bebc");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x431d67c49c100d4c");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x4cc5d4becb3e42b6");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x597f299cfc657e2a");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5fcb6fab3ad6faec");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x6c44198c4a475817")]
let (h224_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt32.uint_to_t (Prims.parse_int "0xc1059ed8");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x367cd507");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x3070dd17");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xf70e5939");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xffc00b31");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x68581511");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x64f98fa7");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbefa4fa4")]
let (h224 : FStar_UInt32.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt32.uint_to_t (Prims.parse_int "0xc1059ed8");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x367cd507");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x3070dd17");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xf70e5939");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xffc00b31");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x68581511");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x64f98fa7");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbefa4fa4")]
let (h256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt32.uint_to_t (Prims.parse_int "0x6a09e667");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xbb67ae85");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x3c6ef372");
  FStar_UInt32.uint_to_t (Prims.parse_int "0xa54ff53a");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x510e527f");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x9b05688c");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x1f83d9ab");
  FStar_UInt32.uint_to_t (Prims.parse_int "0x5be0cd19")]
let (h256 : FStar_UInt32.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt32.uint_to_t (Prims.parse_int "0x6a09e667");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xbb67ae85");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x3c6ef372");
    FStar_UInt32.uint_to_t (Prims.parse_int "0xa54ff53a");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x510e527f");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x9b05688c");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x1f83d9ab");
    FStar_UInt32.uint_to_t (Prims.parse_int "0x5be0cd19")]
let (h384_l : (FStar_UInt64.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt64.uint_to_t (Prims.parse_int "0xcbbb9d5dc1059ed8");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x629a292a367cd507");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x9159015a3070dd17");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x152fecd8f70e5939");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x67332667ffc00b31");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x8eb44a8768581511");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xdb0c2e0d64f98fa7");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x47b5481dbefa4fa4")]
let (h384 : FStar_UInt64.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt64.uint_to_t (Prims.parse_int "0xcbbb9d5dc1059ed8");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x629a292a367cd507");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x9159015a3070dd17");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x152fecd8f70e5939");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x67332667ffc00b31");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x8eb44a8768581511");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xdb0c2e0d64f98fa7");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x47b5481dbefa4fa4")]
let (h512_l : (FStar_UInt64.t, unit) FStar_List_Tot_Properties.llist) =
  [FStar_UInt64.uint_to_t (Prims.parse_int "0x6a09e667f3bcc908");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xbb67ae8584caa73b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x3c6ef372fe94f82b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0xa54ff53a5f1d36f1");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
  FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
let (h512 : FStar_UInt64.t FStar_Seq_Base.seq) =
  FStar_Seq_Properties.seq_of_list
    [FStar_UInt64.uint_to_t (Prims.parse_int "0x6a09e667f3bcc908");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xbb67ae8584caa73b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x3c6ef372fe94f82b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0xa54ff53a5f1d36f1");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]