val ffdhe_bn_from_g: #t:limb_t -> a:S.ffdhe_alg -> len:size_pos -> ffdhe_bn_from_g_st t a len
let ffdhe_bn_from_g #t a len g_n =
  recall_contents ffdhe_g2 S.ffdhe_g2;
  [@inline_let] let nLen = blocks len (size (numbytes t)) in

  push_frame ();
  let g = create 1ul (u8 0) in
  mapT 1ul g secret ffdhe_g2;
  BSeq.nat_from_intseq_be_public_to_secret 1 S.ffdhe_g2;

  let h0 = ST.get () in
  update_sub_f h0 g_n 0ul 1ul
    (fun h -> SB.bn_from_bytes_be 1 (as_seq h0 g))
    (fun _ -> BN.bn_from_bytes_be 1ul g (sub g_n 0ul 1ul));

  let h1 = ST.get () in
  SD.bn_eval_update_sub #t 1 (SB.bn_from_bytes_be 1 (as_seq h0 g)) (v nLen);
  assert (bn_v h1 g_n == SD.bn_v (SB.bn_from_bytes_be #t 1 (as_seq h0 g)));
  SB.bn_from_bytes_be_lemma #t 1 (as_seq h0 g);
  assert (bn_v h1 g_n == BSeq.nat_from_bytes_be (as_seq h0 g));
  pop_frame ()
val ffdhe_bn_from_g: #t:limb_t -> a:S.ffdhe_alg -> len:size_pos -> ffdhe_bn_from_g_st t a len
let ffdhe_bn_from_g #t a len g_n =
recall_contents ffdhe_g2 S.ffdhe_g2;
[@@ inline_let ]let nLen = blocks len (size (numbytes t)) in
push_frame ();
let g = create 1ul (u8 0) in
mapT 1ul g secret ffdhe_g2;
BSeq.nat_from_intseq_be_public_to_secret 1 S.ffdhe_g2;
let h0 = ST.get () in
update_sub_f h0
  g_n
  0ul
  1ul
  (fun h -> SB.bn_from_bytes_be 1 (as_seq h0 g))
  (fun _ -> BN.bn_from_bytes_be 1ul g (sub g_n 0ul 1ul));
let h1 = ST.get () in
SD.bn_eval_update_sub #t 1 (SB.bn_from_bytes_be 1 (as_seq h0 g)) (v nLen);
assert (bn_v h1 g_n == SD.bn_v (SB.bn_from_bytes_be #t 1 (as_seq h0 g)));
SB.bn_from_bytes_be_lemma #t 1 (as_seq h0 g);
assert (bn_v h1 g_n == BSeq.nat_from_bytes_be (as_seq h0 g));
pop_frame ()
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 FStar.HyperStack.ST.pop_frame Prims.unit Prims._assert Prims.eq2 Prims.nat Hacl.Bignum.Definitions.bn_v Lib.ByteSequence.nat_from_bytes_be Lib.IntTypes.SEC Lib.Buffer.as_seq Lib.Buffer.MUT Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Hacl.Spec.Bignum.bn_from_bytes_be_lemma Hacl.Spec.Bignum.Definitions.bn_v Hacl.Spec.Bignum.Definitions.blocks Hacl.Spec.Bignum.bn_from_bytes_be Hacl.Spec.Bignum.Definitions.bn_eval_update_sub Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.update_sub_f Hacl.Bignum.Definitions.limb Lib.Sequence.lseq Hacl.Bignum.bn_from_bytes_be FStar.UInt32.uint_to_t FStar.UInt32.t Lib.IntTypes.mk_int Lib.Buffer.sub Lib.Buffer.lbuffer_t Lib.ByteSequence.nat_from_intseq_be_public_to_secret Lib.IntTypes.U8 Spec.FFDHE.ffdhe_g2 Lib.Buffer.mapT Lib.Buffer.CONST Lib.IntTypes.int_t Lib.IntTypes.secret Hacl.Impl.FFDHE.Constants.ffdhe_g2 Lib.Buffer.create Lib.IntTypes.u8 Lib.Buffer.lbuffer FStar.HyperStack.ST.push_frame Prims.int Prims.l_or Lib.IntTypes.range Prims.l_and Prims.b2t Prims.op_GreaterThan Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_Multiply Lib.Buffer.recall_contents
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
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)))


inline_for_extraction noextract
val ffdhe_bn_from_g: #t:limb_t -> a:S.ffdhe_alg -> len:size_pos -> ffdhe_bn_from_g_st t a len
val ffdhe_bn_from_g: #t:limb_t -> a:S.ffdhe_alg -> len:size_pos -> ffdhe_bn_from_g_st t a len
a: Spec.FFDHE.ffdhe_alg -> len: Hacl.Impl.FFDHE.size_pos
  -> Hacl.Impl.FFDHE.ffdhe_bn_from_g_st t a len