let ffdhe_bn_from_g_st (t:limb_t) (a:S.ffdhe_alg) (len:size_pos) =
  g_n:lbignum t (blocks len (size (numbytes t))) ->
  Stack unit
  (requires fun h ->
    live h g_n /\

    v len = S.ffdhe_len a /\
    as_seq h g_n == LSeq.create (v (blocks len (size (numbytes t)))) (uint #t 0))
  (ensures  fun h0 _ h1 -> modifies (loc g_n) h0 h1 /\
    bn_v h1 g_n == BSeq.nat_from_bytes_be (S.Mk_ffdhe_params?.ffdhe_g (S.get_ffdhe_params a)))
let ffdhe_bn_from_g_st (t: limb_t) (a: S.ffdhe_alg) (len: size_pos) =
g_n: lbignum t (blocks len (size (numbytes t)))
  -> Stack unit
      (requires
        fun h ->
          live h g_n /\ v len = S.ffdhe_len a /\
          as_seq h g_n == LSeq.create (v (blocks len (size (numbytes t)))) (uint #t 0))
      (ensures
        fun h0 _ h1 ->
          modifies (loc g_n) h0 h1 /\
          bn_v h1 g_n == BSeq.nat_from_bytes_be (S.Mk_ffdhe_params?.ffdhe_g (S.get_ffdhe_params a)))
Hacl.Impl.FFDHE.fst.checked
Spec.FFDHE.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.FFDHE.Lemmas.fst.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.Exponentiation.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.fsti.checked Hacl.Impl.FFDHE.Constants.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Base.fst.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.FFDHE.fst
Hacl.Bignum.Definitions.limb_t Spec.FFDHE.ffdhe_alg Hacl.Impl.FFDHE.size_pos Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Definitions.blocks Lib.IntTypes.size Lib.IntTypes.numbytes Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Prims.b2t Prims.op_Equality Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U32 Prims.op_GreaterThan Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Lib.IntTypes.v Lib.IntTypes.PUB Spec.FFDHE.ffdhe_len Prims.eq2 Lib.Sequence.lseq Lib.Buffer.as_seq Lib.Sequence.create Lib.IntTypes.uint Lib.IntTypes.SEC Lib.Buffer.modifies Lib.Buffer.loc Prims.nat Hacl.Bignum.Definitions.bn_v Lib.ByteSequence.nat_from_bytes_be Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_g Spec.FFDHE.get_ffdhe_params
module Hacl.Impl.FFDHE

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.FFDHE.Constants
open Hacl.Bignum.Definitions

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module S = Spec.FFDHE
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence
module Lemmas = Hacl.Spec.FFDHE.Lemmas

module BN = Hacl.Bignum
module BM = Hacl.Bignum.Montgomery
module BE = Hacl.Bignum.Exponentiation
module SB = Hacl.Spec.Bignum
module SM = Hacl.Spec.Bignum.Montgomery
module SE = Hacl.Spec.Bignum.Exponentiation
module SD = Hacl.Spec.Bignum.Definitions

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

inline_for_extraction noextract
let size_pos = x:size_t{v x > 0}

[@CInline]
let ffdhe_len (a:S.ffdhe_alg) : x:size_pos{v x = S.ffdhe_len a} =
  allow_inversion S.ffdhe_alg;
  match a with
  | S.FFDHE2048 -> 256ul
  | S.FFDHE3072 -> 384ul
  | S.FFDHE4096 -> 512ul
  | S.FFDHE6144 -> 768ul
  | S.FFDHE8192 -> 1024ul


inline_for_extraction noextract
let get_ffdhe_p (a:S.ffdhe_alg) :x:glbuffer pub_uint8 (ffdhe_len a)
  {witnessed x (S.Mk_ffdhe_params?.ffdhe_p (S.get_ffdhe_params a)) /\ recallable x}
 =
  allow_inversion S.ffdhe_alg;
  match a with
  | S.FFDHE2048 -> ffdhe_p2048
  | S.FFDHE3072 -> ffdhe_p3072
  | S.FFDHE4096 -> ffdhe_p4096
  | S.FFDHE6144 -> ffdhe_p6144
  | S.FFDHE8192 -> ffdhe_p8192


inline_for_extraction noextract
val ffdhe_p_to_ps:
    a:S.ffdhe_alg
  -> p_s:lbuffer uint8 (ffdhe_len a) ->
  Stack unit
  (requires fun h -> live h p_s)
  (ensures  fun h0 _ h1 -> modifies (loc p_s) h0 h1 /\
    BSeq.nat_from_intseq_be (S.Mk_ffdhe_params?.ffdhe_p (S.get_ffdhe_params a)) ==
    BSeq.nat_from_intseq_be (as_seq h1 p_s))

let ffdhe_p_to_ps a p_s =
  let p = get_ffdhe_p a in
  recall_contents p (S.Mk_ffdhe_params?.ffdhe_p (S.get_ffdhe_params a));
  let len = ffdhe_len a in
  mapT len p_s secret p;
  BSeq.nat_from_intseq_be_public_to_secret (v len) (S.Mk_ffdhe_params?.ffdhe_p (S.get_ffdhe_params a))


inline_for_extraction noextract
val ffdhe_bn_from_g_st : t: Hacl.Bignum.Definitions.limb_t -> a: Spec.FFDHE.ffdhe_alg -> len: Hacl.Impl.FFDHE.size_pos
  -> Type0
t: Hacl.Bignum.Definitions.limb_t -> a: Spec.FFDHE.ffdhe_alg -> len: Hacl.Impl.FFDHE.size_pos
  -> Type0