module Hacl.Test.SHA2

open FStar.HyperStack.All
open FStar.Mul

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer
open Lib.PrintBuffer
open Hacl.Hash.SHA2

#reset-options "--z3rlimit 200 --max_fuel 2 --max_ifuel 2 --using_facts_from '* -FStar.Seq'"

val test_sha2:
    msg_len:size_t
  -> msg:glbuffer uint8 msg_len
  -> expected224:glbuffer uint8 28ul
  -> expected256:glbuffer uint8 32ul
  -> expected384:glbuffer uint8 48ul
  -> expected512:glbuffer uint8 64ul
  -> Stack unit
    (requires fun h ->
      live h msg /\ live h expected224 /\ live h expected256 /\
      live h expected384 /\ live h expected512)
    (ensures  fun h0 r h1 -> True)
let test_sha2 msg_len msg expected224 expected256 expected384 expected512 =
  assert_norm (v msg_len < pow2 32);
  assert_norm (v msg_len < pow2 61);
  assert_norm (v msg_len < pow2 125);
  push_frame();
  assume (v msg_len > 0);
  let msg' = create msg_len (u8 0) in
  copy msg' msg;

  let test224 = create 28ul (u8 0) in
  let test256 = create 32ul (u8 0) in
  let test384 = create 48ul (u8 0) in
  let test512 = create 64ul (u8 0) in
  assert(length test224 == Spec.Hash.Definitions.hash_length Spec.Hash.Definitions.SHA2_224);
  hash_224 msg' msg_len test224;
  assert(length test256 == Spec.Hash.Definitions.hash_length Spec.Hash.Definitions.SHA2_256);
  hash_256 msg' msg_len (test256 <: buffer_t MUT uint8);
  assert(length test384 == Spec.Hash.Definitions.hash_length Spec.Hash.Definitions.SHA2_384);
  hash_384 msg' msg_len (test384 <: buffer_t MUT uint8);
  assert(length test512 == Spec.Hash.Definitions.hash_length Spec.Hash.Definitions.SHA2_512);
  hash_512 msg' msg_len (test512 <: buffer_t MUT uint8);

  print_compare_display 28ul (to_const #uint8 #MUT test224) expected224;
  print_compare_display 32ul (to_const test256) expected256;
  print_compare_display 48ul (to_const test384) expected384;
  print_compare_display 64ul (to_const test512) expected512;
  pop_frame()


val u8: n:nat{n < 0x100} -> uint8
let u8 n = u8 n

//
// Test1_SHA2
//
let test1_plaintext: b:glbuffer uint8 3ul{ recallable b } =
  let open Lib.RawIntTypes in
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
      [0x61; 0x62; 0x63]) in
  assert_norm (List.Tot.length l == 3);
  createL_global l

let test1_expected_sha2_224: b:glbuffer uint8 28ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x23; 0x09; 0x7d; 0x22; 0x34; 0x05; 0xd8; 0x22; 0x86; 0x42; 0xa4; 0x77; 0xbd; 0xa2; 0x55; 0xb3;
     0x2a; 0xad; 0xbc; 0xe4; 0xbd; 0xa0; 0xb3; 0xf7; 0xe3; 0x6c; 0x9d; 0xa7])
  in
  assert_norm (List.Tot.length l == 28);
  createL_global l

let test1_expected_sha2_256: b:glbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xba; 0x78; 0x16; 0xbf; 0x8f; 0x01; 0xcf; 0xea; 0x41; 0x41; 0x40; 0xde; 0x5d; 0xae; 0x22; 0x23;
     0xb0; 0x03; 0x61; 0xa3; 0x96; 0x17; 0x7a; 0x9c; 0xb4; 0x10; 0xff; 0x61; 0xf2; 0x00; 0x15; 0xad])
  in
  assert_norm (List.Tot.length l == 32);
  createL_global l

let test1_expected_sha2_384: b:glbuffer uint8 48ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xcb; 0x00; 0x75; 0x3f; 0x45; 0xa3; 0x5e; 0x8b; 0xb5; 0xa0; 0x3d; 0x69; 0x9a; 0xc6; 0x50; 0x07;
     0x27; 0x2c; 0x32; 0xab; 0x0e; 0xde; 0xd1; 0x63; 0x1a; 0x8b; 0x60; 0x5a; 0x43; 0xff; 0x5b; 0xed;
     0x80; 0x86; 0x07; 0x2b; 0xa1; 0xe7; 0xcc; 0x23; 0x58; 0xba; 0xec; 0xa1; 0x34; 0xc8; 0x25; 0xa7])
  in
  assert_norm (List.Tot.length l == 48);
  createL_global l

let test1_expected_sha2_512: b:glbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xdd; 0xaf; 0x35; 0xa1; 0x93; 0x61; 0x7a; 0xba; 0xcc; 0x41; 0x73; 0x49; 0xae; 0x20; 0x41; 0x31;
     0x12; 0xe6; 0xfa; 0x4e; 0x89; 0xa9; 0x7e; 0xa2; 0x0a; 0x9e; 0xee; 0xe6; 0x4b; 0x55; 0xd3; 0x9a;
     0x21; 0x92; 0x99; 0x2a; 0x27; 0x4f; 0xc1; 0xa8; 0x36; 0xba; 0x3c; 0x23; 0xa3; 0xfe; 0xeb; 0xbd;
     0x45; 0x4d; 0x44; 0x23; 0x64; 0x3c; 0xe8; 0x0e; 0x2a; 0x9a; 0xc9; 0x4f; 0xa5; 0x4c; 0xa4; 0x9f])
  in
  assert_norm (List.Tot.length l == 64);
  createL_global l

//
// Test2_SHA2
//
let test2_plaintext: b:glbuffer uint8 0ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [])
  in
  assert_norm (List.Tot.length l == 0);
  createL_global l

let test2_expected_sha2_224: b:glbuffer uint8 28ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xd1; 0x4a; 0x02; 0x8c; 0x2a; 0x3a; 0x2b; 0xc9; 0x47; 0x61; 0x02; 0xbb; 0x28; 0x82; 0x34; 0xc4;
     0x15; 0xa2; 0xb0; 0x1f; 0x82; 0x8e; 0xa6; 0x2a; 0xc5; 0xb3; 0xe4; 0x2f])
  in
  assert_norm (List.Tot.length l == 28);
  createL_global l

let test2_expected_sha2_256: b:glbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xe3; 0xb0; 0xc4; 0x42; 0x98; 0xfc; 0x1c; 0x14; 0x9a; 0xfb; 0xf4; 0xc8; 0x99; 0x6f; 0xb9; 0x24;
     0x27; 0xae; 0x41; 0xe4; 0x64; 0x9b; 0x93; 0x4c; 0xa4; 0x95; 0x99; 0x1b; 0x78; 0x52; 0xb8; 0x55])
  in
  assert_norm (List.Tot.length l == 32);
  createL_global l

let test2_expected_sha2_384: b:glbuffer uint8 48ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x38; 0xb0; 0x60; 0xa7; 0x51; 0xac; 0x96; 0x38; 0x4c; 0xd9; 0x32; 0x7e; 0xb1; 0xb1; 0xe3; 0x6a;
     0x21; 0xfd; 0xb7; 0x11; 0x14; 0xbe; 0x07; 0x43; 0x4c; 0x0c; 0xc7; 0xbf; 0x63; 0xf6; 0xe1; 0xda;
     0x27; 0x4e; 0xde; 0xbf; 0xe7; 0x6f; 0x65; 0xfb; 0xd5; 0x1a; 0xd2; 0xf1; 0x48; 0x98; 0xb9; 0x5b])
  in
  assert_norm (List.Tot.length l == 48);
  createL_global l

let test2_expected_sha2_512: b:glbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xcf; 0x83; 0xe1; 0x35; 0x7e; 0xef; 0xb8; 0xbd; 0xf1; 0x54; 0x28; 0x50; 0xd6; 0x6d; 0x80; 0x07;
     0xd6; 0x20; 0xe4; 0x05; 0x0b; 0x57; 0x15; 0xdc; 0x83; 0xf4; 0xa9; 0x21; 0xd3; 0x6c; 0xe9; 0xce;
     0x47; 0xd0; 0xd1; 0x3c; 0x5d; 0x85; 0xf2; 0xb0; 0xff; 0x83; 0x18; 0xd2; 0x87; 0x7e; 0xec; 0x2f;
     0x63; 0xb9; 0x31; 0xbd; 0x47; 0x41; 0x7a; 0x81; 0xa5; 0x38; 0x32; 0x7a; 0xf9; 0x27; 0xda; 0x3e])
  in
  assert_norm (List.Tot.length l == 64);
  createL_global l

//
// Test3_SHA2
//
let test3_plaintext: b:glbuffer uint8 56ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x61; 0x62; 0x63; 0x64; 0x62; 0x63; 0x64; 0x65; 0x63; 0x64; 0x65; 0x66; 0x64; 0x65; 0x66; 0x67;
     0x65; 0x66; 0x67; 0x68; 0x66; 0x67; 0x68; 0x69; 0x67; 0x68; 0x69; 0x6a; 0x68; 0x69; 0x6a; 0x6b;
     0x69; 0x6a; 0x6b; 0x6c; 0x6a; 0x6b; 0x6c; 0x6d; 0x6b; 0x6c; 0x6d; 0x6e; 0x6c; 0x6d; 0x6e; 0x6f;
     0x6d; 0x6e; 0x6f; 0x70; 0x6e; 0x6f; 0x70; 0x71])
  in
  assert_norm (List.Tot.length l == 56);
  createL_global l

let test3_expected_sha2_224: b:glbuffer uint8 28ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x75; 0x38; 0x8b; 0x16; 0x51; 0x27; 0x76; 0xcc; 0x5d; 0xba; 0x5d; 0xa1; 0xfd; 0x89; 0x01; 0x50;
     0xb0; 0xc6; 0x45; 0x5c; 0xb4; 0xf5; 0x8b; 0x19; 0x52; 0x52; 0x25; 0x25])
  in
  assert_norm (List.Tot.length l == 28);
  createL_global l

let test3_expected_sha2_256: b:glbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x24; 0x8d; 0x6a; 0x61; 0xd2; 0x06; 0x38; 0xb8; 0xe5; 0xc0; 0x26; 0x93; 0x0c; 0x3e; 0x60; 0x39;
     0xa3; 0x3c; 0xe4; 0x59; 0x64; 0xff; 0x21; 0x67; 0xf6; 0xec; 0xed; 0xd4; 0x19; 0xdb; 0x06; 0xc1])
  in
  assert_norm (List.Tot.length l == 32);
  createL_global l

let test3_expected_sha2_384: b:glbuffer uint8 48ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x33; 0x91; 0xfd; 0xdd; 0xfc; 0x8d; 0xc7; 0x39; 0x37; 0x07; 0xa6; 0x5b; 0x1b; 0x47; 0x09; 0x39;
     0x7c; 0xf8; 0xb1; 0xd1; 0x62; 0xaf; 0x05; 0xab; 0xfe; 0x8f; 0x45; 0x0d; 0xe5; 0xf3; 0x6b; 0xc6;
     0xb0; 0x45; 0x5a; 0x85; 0x20; 0xbc; 0x4e; 0x6f; 0x5f; 0xe9; 0x5b; 0x1f; 0xe3; 0xc8; 0x45; 0x2b])
  in
  assert_norm (List.Tot.length l == 48);
  createL_global l

let test3_expected_sha2_512: b:glbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x20; 0x4a; 0x8f; 0xc6; 0xdd; 0xa8; 0x2f; 0x0a; 0x0c; 0xed; 0x7b; 0xeb; 0x8e; 0x08; 0xa4; 0x16;
     0x57; 0xc1; 0x6e; 0xf4; 0x68; 0xb2; 0x28; 0xa8; 0x27; 0x9b; 0xe3; 0x31; 0xa7; 0x03; 0xc3; 0x35;
     0x96; 0xfd; 0x15; 0xc1; 0x3b; 0x1b; 0x07; 0xf9; 0xaa; 0x1d; 0x3b; 0xea; 0x57; 0x78; 0x9c; 0xa0;
     0x31; 0xad; 0x85; 0xc7; 0xa7; 0x1d; 0xd7; 0x03; 0x54; 0xec; 0x63; 0x12; 0x38; 0xca; 0x34; 0x45])
  in
  assert_norm (List.Tot.length l == 64);
  createL_global l

//
// Test4_SHA2
//
let test4_plaintext: b:glbuffer uint8 112ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x61; 0x62; 0x63; 0x64; 0x65; 0x66; 0x67; 0x68; 0x62; 0x63; 0x64; 0x65; 0x66; 0x67; 0x68; 0x69;
     0x63; 0x64; 0x65; 0x66; 0x67; 0x68; 0x69; 0x6a; 0x64; 0x65; 0x66; 0x67; 0x68; 0x69; 0x6a; 0x6b;
     0x65; 0x66; 0x67; 0x68; 0x69; 0x6a; 0x6b; 0x6c; 0x66; 0x67; 0x68; 0x69; 0x6a; 0x6b; 0x6c; 0x6d;
     0x67; 0x68; 0x69; 0x6a; 0x6b; 0x6c; 0x6d; 0x6e; 0x68; 0x69; 0x6a; 0x6b; 0x6c; 0x6d; 0x6e; 0x6f;
     0x69; 0x6a; 0x6b; 0x6c; 0x6d; 0x6e; 0x6f; 0x70; 0x6a; 0x6b; 0x6c; 0x6d; 0x6e; 0x6f; 0x70; 0x71;
     0x6b; 0x6c; 0x6d; 0x6e; 0x6f; 0x70; 0x71; 0x72; 0x6c; 0x6d; 0x6e; 0x6f; 0x70; 0x71; 0x72; 0x73;
     0x6d; 0x6e; 0x6f; 0x70; 0x71; 0x72; 0x73; 0x74; 0x6e; 0x6f; 0x70; 0x71; 0x72; 0x73; 0x74; 0x75])
  in
  assert_norm (List.Tot.length l == 112);
  createL_global l

let test4_expected_sha2_224: b:glbuffer uint8 28ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xc9; 0x7c; 0xa9; 0xa5; 0x59; 0x85; 0x0c; 0xe9; 0x7a; 0x04; 0xa9; 0x6d; 0xef; 0x6d; 0x99; 0xa9;
     0xe0; 0xe0; 0xe2; 0xab; 0x14; 0xe6; 0xb8; 0xdf; 0x26; 0x5f; 0xc0; 0xb3])
  in
  assert_norm (List.Tot.length l == 28);
  createL_global l

let test4_expected_sha2_256: b:glbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0xcf; 0x5b; 0x16; 0xa7; 0x78; 0xaf; 0x83; 0x80; 0x03; 0x6c; 0xe5; 0x9e; 0x7b; 0x04; 0x92; 0x37;
     0x0b; 0x24; 0x9b; 0x11; 0xe8; 0xf0; 0x7a; 0x51; 0xaf; 0xac; 0x45; 0x03; 0x7a; 0xfe; 0xe9; 0xd1])
  in
  assert_norm (List.Tot.length l == 32);
  createL_global l

let test4_expected_sha2_384: b:glbuffer uint8 48ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x09; 0x33; 0x0c; 0x33; 0xf7; 0x11; 0x47; 0xe8; 0x3d; 0x19; 0x2f; 0xc7; 0x82; 0xcd; 0x1b; 0x47;
     0x53; 0x11; 0x1b; 0x17; 0x3b; 0x3b; 0x05; 0xd2; 0x2f; 0xa0; 0x80; 0x86; 0xe3; 0xb0; 0xf7; 0x12;
     0xfc; 0xc7; 0xc7; 0x1a; 0x55; 0x7e; 0x2d; 0xb9; 0x66; 0xc3; 0xe9; 0xfa; 0x91; 0x74; 0x60; 0x39])
  in
  assert_norm (List.Tot.length l == 48);
  createL_global l

let test4_expected_sha2_512: b:glbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8
    [0x8e; 0x95; 0x9b; 0x75; 0xda; 0xe3; 0x13; 0xda; 0x8c; 0xf4; 0xf7; 0x28; 0x14; 0xfc; 0x14; 0x3f;
     0x8f; 0x77; 0x79; 0xc6; 0xeb; 0x9f; 0x7f; 0xa1; 0x72; 0x99; 0xae; 0xad; 0xb6; 0x88; 0x90; 0x18;
     0x50; 0x1d; 0x28; 0x9e; 0x49; 0x00; 0xf7; 0xe4; 0x33; 0x1b; 0x99; 0xde; 0xc4; 0xb5; 0x43; 0x3a;
     0xc7; 0xd3; 0x29; 0xee; 0xb6; 0xdd; 0x26; 0x54; 0x5e; 0x96; 0xe5; 0x5b; 0x87; 0x4b; 0xe9; 0x09])
  in
  assert_norm (List.Tot.length l == 64);
  createL_global l

val main: unit -> St C.exit_code
let main () =
  C.String.print (C.String.of_literal "\nTEST 1. SHA2\n");
  recall test1_expected_sha2_224;
  recall test1_expected_sha2_256;
  recall test1_expected_sha2_384;
  recall test1_expected_sha2_512;
  recall test1_plaintext;
  test_sha2 3ul test1_plaintext test1_expected_sha2_224 test1_expected_sha2_256 test1_expected_sha2_384 test1_expected_sha2_512;

  C.String.print (C.String.of_literal "\nTEST 2. SHA2\n");
  recall test2_expected_sha2_224;
  recall test2_expected_sha2_256;
  recall test2_expected_sha2_384;
  recall test2_expected_sha2_512;
  recall test2_plaintext;
  test_sha2 0ul test2_plaintext test2_expected_sha2_224 test2_expected_sha2_256 test2_expected_sha2_384 test2_expected_sha2_512;

  C.String.print (C.String.of_literal "\nTEST 3. SHA2\n");
  recall test3_expected_sha2_224;
  recall test3_expected_sha2_256;
  recall test3_expected_sha2_384;
  recall test3_expected_sha2_512;
  recall test3_plaintext;
  test_sha2 56ul test3_plaintext test3_expected_sha2_224 test3_expected_sha2_256 test3_expected_sha2_384 test3_expected_sha2_512;

  C.String.print (C.String.of_literal "\nTEST 4. SHA2\n");
  recall test4_expected_sha2_224;
  recall test4_expected_sha2_256;
  recall test4_expected_sha2_384;
  recall test4_expected_sha2_512;
  recall test4_plaintext;
  test_sha2 112ul test4_plaintext test4_expected_sha2_224 test4_expected_sha2_256 test4_expected_sha2_384 test4_expected_sha2_512;

  C.EXIT_SUCCESS