let ecdsa_sign_p256_st (alg:S.hash_alg_ecdsa) =
    signature:lbuffer uint8 64ul
  -> msg_len:size_t{v msg_len >= S.min_input_length alg}
  -> msg:lbuffer uint8 msg_len
  -> private_key:lbuffer uint8 32ul
  -> nonce:lbuffer uint8 32ul ->
  Stack bool
  (requires fun h ->
    live h signature /\ live h msg /\ live h private_key /\ live h nonce /\
    disjoint signature msg /\ disjoint signature private_key /\ disjoint signature nonce)
  (ensures fun h0 flag h1 -> modifies (loc signature) h0 h1 /\
    (let sgnt = S.ecdsa_signature_agile alg (v msg_len)
      (as_seq h0 msg) (as_seq h0 private_key) (as_seq h0 nonce) in
     (flag <==> Some? sgnt) /\ (flag ==> (as_seq h1 signature == Some?.v sgnt))))
let ecdsa_sign_p256_st (alg: S.hash_alg_ecdsa) =

    signature: lbuffer uint8 64ul ->
    msg_len: size_t{v msg_len >= S.min_input_length alg} ->
    msg: lbuffer uint8 msg_len ->
    private_key: lbuffer uint8 32ul ->
    nonce: lbuffer uint8 32ul
  -> Stack bool
      (requires
        fun h ->
          live h signature /\ live h msg /\ live h private_key /\ live h nonce /\
          disjoint signature msg /\ disjoint signature private_key /\ disjoint signature nonce)
      (ensures
        fun h0 flag h1 ->
          modifies (loc signature) h0 h1 /\
          (let sgnt =
              S.ecdsa_signature_agile alg
                (v msg_len)
                (as_seq h0 msg)
                (as_seq h0 private_key)
                (as_seq h0 nonce)
            in
            (flag <==> Some? sgnt) /\ (flag ==> (as_seq h1 signature == Some?.v sgnt))))
Hacl.P256.fsti.checked
Spec.P256.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.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.fsti
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 FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Lib.Buffer.disjoint Lib.Buffer.modifies Lib.Buffer.loc Prims.l_iff FStar.Pervasives.Native.uu___is_Some Lib.ByteSequence.lbytes Prims.l_imp Prims.eq2 Lib.Sequence.lseq Lib.Buffer.as_seq FStar.Pervasives.Native.__proj__Some__item__v FStar.Pervasives.Native.option Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.P256.ecdsa_signature_agile
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

module S = Spec.P256
module BSeq = Lib.ByteSequence

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

// TODO?: change API for `ecdsa_verify`, namely, take `signature` as an argument

inline_for_extraction noextract
val ecdsa_sign_p256_st : alg: Spec.P256.hash_alg_ecdsa -> Type0
alg: Spec.P256.hash_alg_ecdsa -> Type0