val hash_ecdsa:
    a:hash_alg_ecdsa
  -> msg_len:size_nat{msg_len >= min_input_length a}
  -> msg:lseq uint8 msg_len ->
  Tot (r:lbytes
    (if Hash? a then hash_length (match a with Hash a -> a) else msg_len){length r >= 32})
let hash_ecdsa a msg_len msg =
  match a with | NoHash -> msg | Hash a -> Spec.Agile.Hash.hash a msg
val hash_ecdsa:
    a:hash_alg_ecdsa
  -> msg_len:size_nat{msg_len >= min_input_length a}
  -> msg:lseq uint8 msg_len ->
  Tot (r:lbytes
    (if Hash? a then hash_length (match a with Hash a -> a) else msg_len){length r >= 32})
let hash_ecdsa a msg_len msg =
match a with
| NoHash -> msg
| Hash a -> Spec.Agile.Hash.hash a msg
Spec.P256.fst.checked
Spec.P256.PointOps.fst.checked Spec.P256.Lemmas.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Exponentiation.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Spec.P256.fst
Spec.P256.hash_alg_ecdsa Lib.IntTypes.size_nat Prims.b2t Prims.op_GreaterThanOrEqual Spec.P256.min_input_length Lib.Sequence.lseq Lib.IntTypes.uint8 Spec.Hash.Definitions.hash_alg Prims.l_or Prims.eq2 Spec.Hash.Definitions.SHA2_256 Spec.Hash.Definitions.SHA2_384 Spec.Hash.Definitions.SHA2_512 Spec.Agile.Hash.hash Lib.ByteSequence.lbytes Spec.P256.uu___is_Hash Spec.Hash.Definitions.hash_length Prims.op_Negation Spec.Hash.Definitions.is_shake Prims.bool Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC
module Spec.P256

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Hash.Definitions
module M = Lib.NatMod
module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module PL = Spec.P256.Lemmas

include Spec.P256.PointOps

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

(** https://eprint.iacr.org/2013/816.pdf *)

///  Elliptic curve scalar multiplication

let mk_p256_comm_monoid : LE.comm_monoid aff_point = {
  LE.one = aff_point_at_inf;
  LE.mul = aff_point_add;
  LE.lemma_one = PL.aff_point_at_inf_lemma;
  LE.lemma_mul_assoc = PL.aff_point_add_assoc_lemma;
  LE.lemma_mul_comm = PL.aff_point_add_comm_lemma;
}

let mk_to_p256_comm_monoid : SE.to_comm_monoid proj_point = {
  SE.a_spec = aff_point;
  SE.comm_monoid = mk_p256_comm_monoid;
  SE.refl = to_aff_point;
}

val point_at_inf_c: SE.one_st proj_point mk_to_p256_comm_monoid
let point_at_inf_c _ =
  PL.to_aff_point_at_infinity_lemma ();
  point_at_inf

val point_add_c : SE.mul_st proj_point mk_to_p256_comm_monoid
let point_add_c p q =
  PL.to_aff_point_add_lemma p q;
  point_add p q

val point_double_c : SE.sqr_st proj_point mk_to_p256_comm_monoid
let point_double_c p =
  PL.to_aff_point_double_lemma p;
  point_double p

let mk_p256_concrete_ops : SE.concrete_ops proj_point = {
  SE.to = mk_to_p256_comm_monoid;
  SE.one = point_at_inf_c;
  SE.mul = point_add_c;
  SE.sqr = point_double_c;
}

// [a]P
let point_mul (a:qelem) (p:proj_point) : proj_point =
  SE.exp_fw mk_p256_concrete_ops p 256 a 4

// [a]G
let point_mul_g (a:qelem) : proj_point = point_mul a base_point

// [a1]G + [a2]P
let point_mul_double_g (a1 a2:qelem) (p:proj_point) : proj_point =
  SE.exp_double_fw mk_p256_concrete_ops base_point 256 a1 p a2 5


///  ECDSA over the P256 elliptic curve

type hash_alg_ecdsa =
  | NoHash
  | Hash of (a:hash_alg{a == SHA2_256 \/ a == SHA2_384 \/ a == SHA2_512})

let _: squash (inversion hash_alg_ecdsa) = allow_inversion hash_alg_ecdsa

let _: squash (pow2 32 < pow2 61 /\ pow2 32 < pow2 125) =
  Math.Lemmas.pow2_lt_compat 61 32;
  Math.Lemmas.pow2_lt_compat 125 32


let min_input_length (a:hash_alg_ecdsa) : nat =
  match a with | NoHash -> 32 | Hash a -> 0


val hash_ecdsa:
    a:hash_alg_ecdsa
  -> msg_len:size_nat{msg_len >= min_input_length a}
  -> msg:lseq uint8 msg_len ->
  Tot (r:lbytes
    (if Hash? a then hash_length (match a with Hash a -> a) else msg_len){length r >= 32})
val hash_ecdsa:
    a:hash_alg_ecdsa
  -> msg_len:size_nat{msg_len >= min_input_length a}
  -> msg:lseq uint8 msg_len ->
  Tot (r:lbytes
    (if Hash? a then hash_length (match a with Hash a -> a) else msg_len){length r >= 32})

    a: Spec.P256.hash_alg_ecdsa ->
    msg_len: Lib.IntTypes.size_nat{msg_len >= Spec.P256.min_input_length a} ->
    msg: Lib.Sequence.lseq Lib.IntTypes.uint8 msg_len
  -> r:
    Lib.ByteSequence.lbytes (match Hash? a with
        | true ->
          Spec.Hash.Definitions.hash_length (let Spec.P256.Hash a = a in
              a)
        | _ -> msg_len) {Lib.Sequence.length r >= 32}