module Spec.SHA2.Constants

// K shuffling vectors

[@"opaque_to_smt"]
inline_for_extraction
let k224_256_l: List.llist UInt32.t 64 =
  [@inline_let]
  let l =
    [0x428a2f98ul; 0x71374491ul; 0xb5c0fbcful; 0xe9b5dba5ul;
     0x3956c25bul; 0x59f111f1ul; 0x923f82a4ul; 0xab1c5ed5ul;
     0xd807aa98ul; 0x12835b01ul; 0x243185beul; 0x550c7dc3ul;
     0x72be5d74ul; 0x80deb1feul; 0x9bdc06a7ul; 0xc19bf174ul;
     0xe49b69c1ul; 0xefbe4786ul; 0x0fc19dc6ul; 0x240ca1ccul;
     0x2de92c6ful; 0x4a7484aaul; 0x5cb0a9dcul; 0x76f988daul;
     0x983e5152ul; 0xa831c66dul; 0xb00327c8ul; 0xbf597fc7ul;
     0xc6e00bf3ul; 0xd5a79147ul; 0x06ca6351ul; 0x14292967ul;
     0x27b70a85ul; 0x2e1b2138ul; 0x4d2c6dfcul; 0x53380d13ul;
     0x650a7354ul; 0x766a0abbul; 0x81c2c92eul; 0x92722c85ul;
     0xa2bfe8a1ul; 0xa81a664bul; 0xc24b8b70ul; 0xc76c51a3ul;
     0xd192e819ul; 0xd6990624ul; 0xf40e3585ul; 0x106aa070ul;
     0x19a4c116ul; 0x1e376c08ul; 0x2748774cul; 0x34b0bcb5ul;
     0x391c0cb3ul; 0x4ed8aa4aul; 0x5b9cca4ful; 0x682e6ff3ul;
     0x748f82eeul; 0x78a5636ful; 0x84c87814ul; 0x8cc70208ul;
     0x90befffaul; 0xa4506cebul; 0xbef9a3f7ul; 0xc67178f2ul] in
  assert_norm (List.length l = 64);
  l

let k224_256 = Seq.seq_of_list k224_256_l

[@"opaque_to_smt"]
inline_for_extraction
let k384_512_l: List.llist UInt64.t 80 =
  [@inline_let]
  let l =
    [0x428a2f98d728ae22uL; 0x7137449123ef65cduL; 0xb5c0fbcfec4d3b2fuL; 0xe9b5dba58189dbbcuL;
     0x3956c25bf348b538uL; 0x59f111f1b605d019uL; 0x923f82a4af194f9buL; 0xab1c5ed5da6d8118uL;
     0xd807aa98a3030242uL; 0x12835b0145706fbeuL; 0x243185be4ee4b28cuL; 0x550c7dc3d5ffb4e2uL;
     0x72be5d74f27b896fuL; 0x80deb1fe3b1696b1uL; 0x9bdc06a725c71235uL; 0xc19bf174cf692694uL;
     0xe49b69c19ef14ad2uL; 0xefbe4786384f25e3uL; 0x0fc19dc68b8cd5b5uL; 0x240ca1cc77ac9c65uL;
     0x2de92c6f592b0275uL; 0x4a7484aa6ea6e483uL; 0x5cb0a9dcbd41fbd4uL; 0x76f988da831153b5uL;
     0x983e5152ee66dfabuL; 0xa831c66d2db43210uL; 0xb00327c898fb213fuL; 0xbf597fc7beef0ee4uL;
     0xc6e00bf33da88fc2uL; 0xd5a79147930aa725uL; 0x06ca6351e003826fuL; 0x142929670a0e6e70uL;
     0x27b70a8546d22ffcuL; 0x2e1b21385c26c926uL; 0x4d2c6dfc5ac42aeduL; 0x53380d139d95b3dfuL;
     0x650a73548baf63deuL; 0x766a0abb3c77b2a8uL; 0x81c2c92e47edaee6uL; 0x92722c851482353buL;
     0xa2bfe8a14cf10364uL; 0xa81a664bbc423001uL; 0xc24b8b70d0f89791uL; 0xc76c51a30654be30uL;
     0xd192e819d6ef5218uL; 0xd69906245565a910uL; 0xf40e35855771202auL; 0x106aa07032bbd1b8uL;
     0x19a4c116b8d2d0c8uL; 0x1e376c085141ab53uL; 0x2748774cdf8eeb99uL; 0x34b0bcb5e19b48a8uL;
     0x391c0cb3c5c95a63uL; 0x4ed8aa4ae3418acbuL; 0x5b9cca4f7763e373uL; 0x682e6ff3d6b2b8a3uL;
     0x748f82ee5defb2fcuL; 0x78a5636f43172f60uL; 0x84c87814a1f0ab72uL; 0x8cc702081a6439ecuL;
     0x90befffa23631e28uL; 0xa4506cebde82bde9uL; 0xbef9a3f7b2c67915uL; 0xc67178f2e372532buL;
     0xca273eceea26619cuL; 0xd186b8c721c0c207uL; 0xeada7dd6cde0eb1euL; 0xf57d4f7fee6ed178uL;
     0x06f067aa72176fbauL; 0x0a637dc5a2c898a6uL; 0x113f9804bef90daeuL; 0x1b710b35131c471buL;
     0x28db77f523047d84uL; 0x32caab7b40c72493uL; 0x3c9ebe0a15c9bebcuL; 0x431d67c49c100d4cuL;
     0x4cc5d4becb3e42b6uL; 0x597f299cfc657e2auL; 0x5fcb6fab3ad6faecuL; 0x6c44198c4a475817uL
    ] in
  assert_norm (List.length l = 80);
  l

let k384_512 = Seq.seq_of_list k384_512_l

// H0 vectors, i.e. initial values of the accumulator

[@"opaque_to_smt"]
inline_for_extraction
let h224_l: List.llist UInt32.t 8 =
  [@inline_let]
  let l = [
    0xc1059ed8ul; 0x367cd507ul; 0x3070dd17ul; 0xf70e5939ul;
    0xffc00b31ul; 0x68581511ul; 0x64f98fa7ul; 0xbefa4fa4ul
  ] in
  assert_norm (List.length l = 8);
  l

let h224 = Seq.seq_of_list h224_l

[@"opaque_to_smt"]
inline_for_extraction
let h256_l: List.llist UInt32.t 8 =
  [@inline_let]
  let l =
    [0x6a09e667ul; 0xbb67ae85ul; 0x3c6ef372ul; 0xa54ff53aul;
     0x510e527ful; 0x9b05688cul; 0x1f83d9abul; 0x5be0cd19ul]
  in
  assert_norm (List.length l = 8);
  l

let h256 = Seq.seq_of_list h256_l

[@"opaque_to_smt"]
inline_for_extraction
let h384_l: List.llist UInt64.t 8 =
  [@inline_let]
  let l = [
    0xcbbb9d5dc1059ed8uL; 0x629a292a367cd507uL; 0x9159015a3070dd17uL; 0x152fecd8f70e5939uL;
    0x67332667ffc00b31uL; 0x8eb44a8768581511uL; 0xdb0c2e0d64f98fa7uL; 0x47b5481dbefa4fa4uL
  ] in
  assert_norm (List.length l = 8);
  l

let h384 = Seq.seq_of_list h384_l

[@"opaque_to_smt"]
inline_for_extraction
let h512_l: List.llist UInt64.t 8 =
  [@inline_let]
  let l = [
    0x6a09e667f3bcc908uL; 0xbb67ae8584caa73buL; 0x3c6ef372fe94f82buL; 0xa54ff53a5f1d36f1uL;
    0x510e527fade682d1uL; 0x9b05688c2b3e6c1fuL; 0x1f83d9abfb41bd6buL; 0x5be0cd19137e2179uL
  ] in
  assert_norm (List.length l = 8);
  l

let h512 = Seq.seq_of_list h512_l