val 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}
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
val 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}
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
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
Spec.FFDHE.ffdhe_alg Hacl.Impl.FFDHE.Constants.ffdhe_p2048 Hacl.Impl.FFDHE.Constants.ffdhe_p3072 Hacl.Impl.FFDHE.Constants.ffdhe_p4096 Hacl.Impl.FFDHE.Constants.ffdhe_p6144 Hacl.Impl.FFDHE.Constants.ffdhe_p8192 Lib.Buffer.glbuffer Lib.IntTypes.pub_uint8 Hacl.Impl.FFDHE.ffdhe_len Prims.l_and Lib.Buffer.witnessed Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p Spec.FFDHE.get_ffdhe_params Lib.Buffer.recallable Lib.Buffer.CONST Prims.unit FStar.Pervasives.allow_inversion
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}
val 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}
a: Spec.FFDHE.ffdhe_alg
  -> x:
    Lib.Buffer.glbuffer Lib.IntTypes.pub_uint8 (Hacl.Impl.FFDHE.ffdhe_len a)
      { Lib.Buffer.witnessed x (Mk_ffdhe_params?.ffdhe_p (Spec.FFDHE.get_ffdhe_params a)) /\
        Lib.Buffer.recallable x }