val msgHash2:b: lbuffer uint8 32ul {recallable b}
let msgHash2: b:lbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0x4b; 0x68; 0x8d; 0xf4; 0x0b; 0xce; 0xdb; 0xe6; 0x41; 0xdd; 0xb1; 0x6f; 0xf0; 0xa1; 0x84; 0x2d;
      0x9c; 0x67; 0xea; 0x1c; 0x3b; 0xf6; 0x3f; 0x3e; 0x04; 0x71; 0xba; 0xa6; 0x64; 0x53; 0x1d; 0x1a ]) in
  assert_norm (List.Tot.length l == 32);
  createL_mglobal l
val msgHash2:b: lbuffer uint8 32ul {recallable b}
let msgHash2:b: lbuffer uint8 32ul {recallable b} =
[@@ inline_let ]let l:list uint8 =
  normalize_term (List.Tot.map u8
        [
          0x4b; 0x68; 0x8d; 0xf4; 0x0b; 0xce; 0xdb; 0xe6; 0x41; 0xdd; 0xb1; 0x6f; 0xf0; 0xa1; 0x84;
          0x2d; 0x9c; 0x67; 0xea; 0x1c; 0x3b; 0xf6; 0x3f; 0x3e; 0x04; 0x71; 0xba; 0xa6; 0x64; 0x53;
          0x1d; 0x1a
        ])
in
assert_norm (List.Tot.length l == 32);
createL_mglobal l
Hacl.Test.K256.fst.checked
prims.fst.checked Lib.PrintBuffer.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.K256.ECDSA.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.All.fst.checked C.String.fsti.checked C.fst.checked
Hacl.Test.K256.fst
Lib.Buffer.createL_mglobal Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.buffer Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int FStar.List.Tot.Base.length Lib.Buffer.lbuffer_t Lib.Buffer.MUT FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.recallable Prims.list FStar.Pervasives.normalize_term FStar.List.Tot.Base.map Prims.nat Prims.b2t Prims.op_LessThan Hacl.Test.K256.u8 Prims.Cons Prims.Nil
module Hacl.Test.K256

open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.PrintBuffer

module K256 = Hacl.K256.ECDSA

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

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

///  Test1

let pk1: b:lbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0xb8; 0x38; 0xff; 0x44; 0xe5; 0xbc; 0x17; 0x7b; 0xf2; 0x11; 0x89; 0xd0; 0x76; 0x60; 0x82; 0xfc;
      0x9d; 0x84; 0x32; 0x26; 0x88; 0x7f; 0xc9; 0x76; 0x03; 0x71; 0x10; 0x0b; 0x7e; 0xe2; 0x0a; 0x6f;
      0xf0; 0xc9; 0xd7; 0x5b; 0xfb; 0xa7; 0xb3; 0x1a; 0x6b; 0xca; 0x19; 0x74; 0x49; 0x6e; 0xeb; 0x56;
      0xde; 0x35; 0x70; 0x71; 0x95; 0x5d; 0x83; 0xc4; 0xb1; 0xba; 0xda; 0xa0; 0xb2; 0x18; 0x32; 0xe9 ]) in
  assert_norm (List.Tot.length l == 64);
  createL_mglobal l


let msg1: b:lbuffer uint8 6ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [ 0x31; 0x32; 0x33; 0x34; 0x30; 0x30]) in
  assert_norm (List.Tot.length l == 6);
  createL_mglobal l


let sgnt1: b:lbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0x81; 0x3e; 0xf7; 0x9c; 0xce; 0xfa; 0x9a; 0x56; 0xf7; 0xba; 0x80; 0x5f; 0x0e; 0x47; 0x85; 0x84;
      0xfe; 0x5f; 0x0d; 0xd5; 0xf5; 0x67; 0xbc; 0x09; 0xb5; 0x12; 0x3c; 0xcb; 0xc9; 0x83; 0x23; 0x65;
      0x6f; 0xf1; 0x8a; 0x52; 0xdc; 0xc0; 0x33; 0x6f; 0x7a; 0xf6; 0x24; 0x00; 0xa6; 0xdd; 0x9b; 0x81;
      0x07; 0x32; 0xba; 0xf1; 0xff; 0x75; 0x80; 0x00; 0xd6; 0xf6; 0x13; 0xa5; 0x56; 0xeb; 0x31; 0xba ]) in
  assert_norm (List.Tot.length l == 64);
  createL_mglobal l


///  Test2

let sk2: b:lbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0xeb; 0xb2; 0xc0; 0x82; 0xfd; 0x77; 0x27; 0x89; 0x0a; 0x28; 0xac; 0x82; 0xf6; 0xbd; 0xf9; 0x7b;
      0xad; 0x8d; 0xe9; 0xf5; 0xd7; 0xc9; 0x02; 0x86; 0x92; 0xde; 0x1a; 0x25; 0x5c; 0xad; 0x3e; 0x0f ]) in
  assert_norm (List.Tot.length l == 32);
  createL_mglobal l


let pk2: b:lbuffer uint8 64ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0x77; 0x9d; 0xd1; 0x97; 0xa5; 0xdf; 0x97; 0x7e; 0xd2; 0xcf; 0x6c; 0xb3; 0x1d; 0x82; 0xd4; 0x33;
      0x28; 0xb7; 0x90; 0xdc; 0x6b; 0x3b; 0x7d; 0x44; 0x37; 0xa4; 0x27; 0xbd; 0x58; 0x47; 0xdf; 0xcd;
      0xe9; 0x4b; 0x72; 0x4a; 0x55; 0x5b; 0x6d; 0x01; 0x7b; 0xb7; 0x60; 0x7c; 0x3e; 0x32; 0x81; 0xda;
      0xf5; 0xb1; 0x69; 0x9d; 0x6e; 0xf4; 0x12; 0x49; 0x75; 0xc9; 0x23; 0x7b; 0x91; 0x7d; 0x42; 0x6f ]) in
  assert_norm (List.Tot.length l == 64);
  createL_mglobal l


let nonce2: b:lbuffer uint8 32ul{ recallable b } =
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0x49; 0xa0; 0xd7; 0xb7; 0x86; 0xec; 0x9c; 0xde; 0x0d; 0x07; 0x21; 0xd7; 0x28; 0x04; 0xbe; 0xfd;
      0x06; 0x57; 0x1c; 0x97; 0x4b; 0x19; 0x1e; 0xfb; 0x42; 0xec; 0xf3; 0x22; 0xba; 0x9d; 0xdd; 0x9a ]) in
  assert_norm (List.Tot.length l == 32);
  createL_mglobal l
val msgHash2:b: lbuffer uint8 32ul {recallable b}
b:
Lib.Buffer.lbuffer_t Lib.Buffer.MUT
  (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC)
  (FStar.UInt32.uint_to_t 32 <: FStar.UInt32.t) {Lib.Buffer.recallable b}