val ffdhe_precomp_p:
    #t:limb_t
  -> a:S.ffdhe_alg
  -> len:size_pos
  -> ke:BE.exp t ->
  ffdhe_precomp_p_st t a len ke
let ffdhe_precomp_p #t a len ke p_r2_n =
  push_frame ();
  let nLen = blocks len (size (numbytes t)) in
  let p_n = sub p_r2_n 0ul nLen in
  let r2_n = sub p_r2_n nLen nLen in

  let p_s = create len (u8 0) in
  ffdhe_p_to_ps a p_s;
  let h0 = ST.get () in
  BN.bn_from_bytes_be len p_s p_n;
  let h1 = ST.get () in
  SB.bn_from_bytes_be_lemma #t (v len) (as_seq h0 p_s);
  assert (bn_v h1 p_n == BSeq.nat_from_bytes_be (as_seq h0 p_s));
  S.ffdhe_p_lemma a;
  Lemmas.ffdhe_p_bits_lemma a;
  ke.BE.precompr2 (8ul *! len -! 1ul) p_n r2_n;
  SM.bn_precomp_r2_mod_n_lemma (8 * v len - 1) (as_seq h1 p_n);
  pop_frame ()
val ffdhe_precomp_p:
    #t:limb_t
  -> a:S.ffdhe_alg
  -> len:size_pos
  -> ke:BE.exp t ->
  ffdhe_precomp_p_st t a len ke
let ffdhe_precomp_p #t a len ke p_r2_n =
push_frame ();
let nLen = blocks len (size (numbytes t)) in
let p_n = sub p_r2_n 0ul nLen in
let r2_n = sub p_r2_n nLen nLen in
let p_s = create len (u8 0) in
ffdhe_p_to_ps a p_s;
let h0 = ST.get () in
BN.bn_from_bytes_be len p_s p_n;
let h1 = ST.get () in
SB.bn_from_bytes_be_lemma #t (v len) (as_seq h0 p_s);
assert (bn_v h1 p_n == BSeq.nat_from_bytes_be (as_seq h0 p_s));
S.ffdhe_p_lemma a;
Lemmas.ffdhe_p_bits_lemma a;
ke.BE.precompr2 (8ul *! len -! 1ul) p_n r2_n;
SM.bn_precomp_r2_mod_n_lemma (8 * v len - 1) (as_seq h1 p_n);
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.Exponentiation.exp Hacl.Bignum.Definitions.lbignum Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Bignum.Definitions.blocks Lib.IntTypes.size Lib.IntTypes.numbytes FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Spec.Bignum.Montgomery.bn_precomp_r2_mod_n_lemma Lib.IntTypes.v Prims.op_Subtraction FStar.Mul.op_Star Lib.Buffer.as_seq Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Hacl.Bignum.Exponentiation.__proj__Mkexp__item__precompr2 Lib.IntTypes.op_Subtraction_Bang Lib.IntTypes.op_Star_Bang FStar.UInt32.__uint_to_t Hacl.Spec.FFDHE.Lemmas.ffdhe_p_bits_lemma Spec.FFDHE.ffdhe_p_lemma Prims._assert Prims.eq2 Prims.nat Hacl.Bignum.Definitions.bn_v Lib.ByteSequence.nat_from_bytes_be Lib.IntTypes.SEC Lib.IntTypes.uint8 Hacl.Spec.Bignum.bn_from_bytes_be_lemma FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Bignum.bn_from_bytes_be Hacl.Impl.FFDHE.ffdhe_p_to_ps Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.Buffer.create Lib.IntTypes.u8 Lib.Buffer.lbuffer Lib.Buffer.sub Prims.int Prims.l_or Lib.IntTypes.range Prims.l_and Prims.b2t Prims.op_GreaterThan Prims.op_LessThanOrEqual Prims.pow2 Prims.op_Multiply Lib.IntTypes.mk_int Hacl.Spec.Bignum.Definitions.blocks FStar.HyperStack.ST.push_frame
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
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 ()


inline_for_extraction noextract
let ffdhe_precomp_inv (#t:limb_t) (#len:size_nat{0 < len /\ len + len <= max_size_t})
  (a:S.ffdhe_alg) (p_r2_n:SD.lbignum t (len + len))
 =
  let p_n = LSeq.sub p_r2_n 0 len in
  let r2_n = LSeq.sub p_r2_n len len in
  SD.bn_v p_n == BSeq.nat_from_bytes_be (S.Mk_ffdhe_params?.ffdhe_p (S.get_ffdhe_params a)) /\
  0 < SD.bn_v p_n /\ SD.bn_v r2_n == pow2 (2 * bits t * len) % SD.bn_v p_n


inline_for_extraction noextract
let ffdhe_precomp_p_st (t:limb_t) (a:S.ffdhe_alg) (len:size_pos) (ke:BE.exp t) =
  let nLen = blocks len (size (numbytes t)) in
  p_r2_n:lbignum t (nLen +! nLen) ->
  Stack unit
  (requires fun h ->
    live h p_r2_n /\

    v len = S.ffdhe_len a /\ ke.BE.bn.BN.len == nLen)
  (ensures  fun h0 _ h1 -> modifies (loc p_r2_n) h0 h1 /\
    ffdhe_precomp_inv #t #(v nLen) a (as_seq h1 p_r2_n))


inline_for_extraction noextract
val ffdhe_precomp_p:
    #t:limb_t
  -> a:S.ffdhe_alg
  -> len:size_pos
  -> ke:BE.exp t ->
  ffdhe_precomp_p_st t a len ke
val ffdhe_precomp_p:
    #t:limb_t
  -> a:S.ffdhe_alg
  -> len:size_pos
  -> ke:BE.exp t ->
  ffdhe_precomp_p_st t a len ke
a: Spec.FFDHE.ffdhe_alg -> len: Hacl.Impl.FFDHE.size_pos -> ke: Hacl.Bignum.Exponentiation.exp t
  -> Hacl.Impl.FFDHE.ffdhe_precomp_p_st t a len ke