val ecdsa_signature: alg:S.hash_alg_ecdsa -> ecdsa_sign_p256_st alg
let ecdsa_signature alg signature msg_len msg private_key nonce =
  push_frame ();
  let m_q = BN.create_felem () in
  msg_as_felem alg msg_len msg m_q;
  let res = ecdsa_sign_msg_as_qelem signature m_q private_key nonce in
  pop_frame ();
  res
val ecdsa_signature: alg:S.hash_alg_ecdsa -> ecdsa_sign_p256_st alg
let ecdsa_signature alg signature msg_len msg private_key nonce =
push_frame ();
let m_q = BN.create_felem () in
msg_as_felem alg msg_len msg m_q;
let res = ecdsa_sign_msg_as_qelem signature m_q private_key nonce in
pop_frame ();
res
Hacl.P256.fst.checked
Spec.P256.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.Ignore.fsti.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Streaming.SHA2.fst.checked Hacl.Impl.P256.Verify.fst.checked Hacl.Impl.P256.Sign.fst.checked Hacl.Impl.P256.Scalar.fsti.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.DH.fsti.checked Hacl.Impl.P256.Compression.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Hash.SHA2.fsti.checked Hacl.Hash.Definitions.fst.checked Hacl.Bignum.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.P256.fst
Spec.P256.hash_alg_ecdsa Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Spec.P256.min_input_length Prims.bool Prims.unit FStar.HyperStack.ST.pop_frame Hacl.Impl.P256.Sign.ecdsa_sign_msg_as_qelem Hacl.P256.msg_as_felem Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Bignum.create_felem FStar.HyperStack.ST.push_frame
module Hacl.P256

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Spec.Hash.Definitions
open Hacl.Hash.SHA2

open Hacl.Impl.P256.Sign
open Hacl.Impl.P256.Verify

module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

module S = Spec.P256
module BN = Hacl.Impl.P256.Bignum
module P = Hacl.Impl.P256.Point

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

inline_for_extraction noextract
val msg_as_felem:
    alg:S.hash_alg_ecdsa
  -> msg_len:size_t{v msg_len >= S.min_input_length alg}
  -> msg:lbytes msg_len
  -> res:BN.felem ->
  Stack unit
  (requires fun h ->
    live h msg /\ live h res /\ disjoint msg res)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    (let hashM = S.hash_ecdsa alg (v msg_len) (as_seq h0 msg) in
    BN.as_nat h1 res = BSeq.nat_from_bytes_be (LSeq.sub hashM 0 32) % S.order))

let msg_as_felem alg msg_len msg res =
  push_frame ();

  [@inline_let] let sz: size_t =
    match alg with
    | S.NoHash -> 32ul
    | S.Hash a -> Hacl.Hash.Definitions.hash_len a in

  let mHash = create sz (u8 0) in

  begin
  match alg with
    | S.NoHash -> copy mHash (sub msg 0ul 32ul)
    | S.Hash a -> match a with
      | SHA2_256 -> Hacl.Streaming.SHA2.hash_256 msg msg_len mHash
      | SHA2_384 -> Hacl.Streaming.SHA2.hash_384 msg msg_len mHash
      | SHA2_512 -> Hacl.Streaming.SHA2.hash_512 msg msg_len mHash
  end;
  LowStar.Ignore.ignore msg_len;
  let mHash32 = sub mHash 0ul 32ul in
  BN.bn_from_bytes_be4 res mHash32;
  Hacl.Impl.P256.Scalar.qmod_short res res;
  pop_frame ()


inline_for_extraction noextract
val ecdsa_signature: alg:S.hash_alg_ecdsa -> ecdsa_sign_p256_st alg
val ecdsa_signature: alg:S.hash_alg_ecdsa -> ecdsa_sign_p256_st alg
alg: Spec.P256.hash_alg_ecdsa -> Hacl.P256.ecdsa_sign_p256_st alg