val public_key_uncompressed_from_raw: pk:lbytes 65ul -> pk_raw:lbytes 64ul -> Stack unit
  (requires fun h -> live h pk /\ live h pk_raw /\ disjoint pk pk_raw)
  (ensures  fun h0 _ h1 -> modifies (loc pk) h0 h1 /\
    as_seq h1 pk == S.pk_uncompressed_from_raw (as_seq h0 pk_raw))
let public_key_uncompressed_from_raw pk pk_raw =
  let h0 = ST.get () in
  pk.(0ul) <- u8 0x04;
  update_sub pk 1ul 64ul pk_raw;
  let h1 = ST.get () in
  LSeq.eq_intro (as_seq h1 pk) (S.pk_uncompressed_from_raw (as_seq h0 pk_raw))
val public_key_uncompressed_from_raw: pk:lbytes 65ul -> pk_raw:lbytes 64ul -> Stack unit
  (requires fun h -> live h pk /\ live h pk_raw /\ disjoint pk pk_raw)
  (ensures  fun h0 _ h1 -> modifies (loc pk) h0 h1 /\
    as_seq h1 pk == S.pk_uncompressed_from_raw (as_seq h0 pk_raw))
let public_key_uncompressed_from_raw pk pk_raw =
let h0 = ST.get () in
pk.(0ul) <- u8 0x04;
update_sub pk 1ul 64ul pk_raw;
let h1 = ST.get () in
LSeq.eq_intro (as_seq h1 pk) (S.pk_uncompressed_from_raw (as_seq h0 pk_raw))
Hacl.K256.ECDSA.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Streaming.SHA2.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.K256.Scalar.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Verify.fst.checked Hacl.Impl.K256.Sign.fst.checked Hacl.Impl.K256.PointMul.fsti.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Bignum.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.K256.ECDSA.fst
Hacl.K256.ECDSA.lbytes FStar.UInt32.__uint_to_t Lib.Sequence.eq_intro Lib.IntTypes.uint8 Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Spec.K256.pk_uncompressed_from_raw Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.update_sub Lib.Buffer.op_Array_Assignment Lib.IntTypes.u8
module Hacl.K256.ECDSA

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

module S = Spec.K256
module BDL = Hacl.Spec.K256.Field52.Definitions.Lemmas

module P = Hacl.Impl.K256.Point
module SK = Hacl.Impl.K256.Sign
module VK = Hacl.Impl.K256.Verify

open Hacl.K256.Field
open Hacl.K256.Scalar

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

let ecdsa_sign_hashed_msg signature msgHash private_key nonce =
  SK.ecdsa_sign_hashed_msg signature msgHash private_key nonce


let ecdsa_sign_sha256 signature msg_len msg private_key nonce =
  push_frame ();
  let msgHash = create 32ul (u8 0) in
  Hacl.Streaming.SHA2.hash_256 msg msg_len msgHash;
  let b = ecdsa_sign_hashed_msg signature msgHash private_key nonce in
  pop_frame ();
  b


let ecdsa_verify_hashed_msg m public_key signature =
  VK.ecdsa_verify_hashed_msg m public_key signature


let ecdsa_verify_sha256 msg_len msg public_key signature =
  push_frame ();
  let mHash = create 32ul (u8 0) in
  Hacl.Streaming.SHA2.hash_256 msg msg_len mHash;
  let b = ecdsa_verify_hashed_msg mHash public_key signature in
  pop_frame ();
  b

///  Low-S normalization

let secp256k1_ecdsa_signature_normalize signature =
  push_frame ();
  let s_q = create_qelem () in
  let s = sub signature 32ul 32ul in
  let is_sk_valid = load_qelem_vartime s_q s in
  let b =
    if not is_sk_valid then false
    else begin
      let is_sk_lt_q_halved = is_qelem_le_q_halved_vartime s_q in
      qnegate_conditional_vartime s_q (not is_sk_lt_q_halved);

      let h1 = ST.get () in
      update_sub_f h1 signature 32ul 32ul
        (fun h -> BSeq.nat_to_bytes_be 32 (qas_nat h1 s_q))
        (fun _ -> store_qelem (sub signature 32ul 32ul) s_q);
      true end in
  pop_frame ();
  b


let secp256k1_ecdsa_is_signature_normalized signature =
  push_frame ();
  let s_q = create_qelem () in
  let s = sub signature 32ul 32ul in
  let is_s_valid = load_qelem_vartime s_q s in
  let is_s_lt_q_halved = is_qelem_le_q_halved_vartime s_q in
  pop_frame ();
  is_s_valid && is_s_lt_q_halved


let secp256k1_ecdsa_sign_hashed_msg signature msgHash private_key nonce =
  let b = ecdsa_sign_hashed_msg signature msgHash private_key nonce in
  if b then secp256k1_ecdsa_signature_normalize signature else false


let secp256k1_ecdsa_sign_sha256 signature msg_len msg private_key nonce =
  push_frame ();
  let msgHash = create 32ul (u8 0) in
  Hacl.Streaming.SHA2.hash_256 msg msg_len msgHash;
  let b = secp256k1_ecdsa_sign_hashed_msg signature msgHash private_key nonce in
  pop_frame ();
  b


let secp256k1_ecdsa_verify_hashed_msg msgHash public_key signature =
  let is_s_normalized = secp256k1_ecdsa_is_signature_normalized signature in
  if not is_s_normalized then false
  else ecdsa_verify_hashed_msg msgHash public_key signature


let secp256k1_ecdsa_verify_sha256 msg_len msg public_key signature =
  push_frame ();
  let mHash = create 32ul (u8 0) in
  Hacl.Streaming.SHA2.hash_256 msg msg_len mHash;
  let b = secp256k1_ecdsa_verify_hashed_msg mHash public_key signature in
  pop_frame ();
  b


///  Parsing and Serializing public keys

let public_key_uncompressed_to_raw pk_raw pk =
  let pk0 = pk.(0ul) in
  if Lib.RawIntTypes.u8_to_UInt8 pk0 <> 0x04uy then false
  else begin
    copy pk_raw (sub pk 1ul 64ul);
    true end
val public_key_uncompressed_from_raw: pk:lbytes 65ul -> pk_raw:lbytes 64ul -> Stack unit
  (requires fun h -> live h pk /\ live h pk_raw /\ disjoint pk pk_raw)
  (ensures  fun h0 _ h1 -> modifies (loc pk) h0 h1 /\
    as_seq h1 pk == S.pk_uncompressed_from_raw (as_seq h0 pk_raw))
pk: Hacl.K256.ECDSA.lbytes 65ul -> pk_raw: Hacl.K256.ECDSA.lbytes 64ul
  -> FStar.HyperStack.ST.Stack Prims.unit