val ffdhe_g2:lseq pub_uint8 1
let ffdhe_g2: lseq pub_uint8 1 = of_list list_ffdhe_g2
val ffdhe_g2:lseq pub_uint8 1
let ffdhe_g2:lseq pub_uint8 1 =
of_list list_ffdhe_g2
Spec.FFDHE.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.FFDHE.fst
Lib.Sequence.of_list Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB Spec.FFDHE.list_ffdhe_g2
module Spec.FFDHE

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

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

(** https://tools.ietf.org/html/rfc7919#appendix-A *)

noeq type ffdhe_params_t =
  | Mk_ffdhe_params:
       ffdhe_p_len:size_nat
    -> ffdhe_p:lseq pub_uint8 ffdhe_p_len
    -> ffdhe_g_len:size_nat
    -> ffdhe_g:lseq pub_uint8 ffdhe_g_len
    -> ffdhe_params_t


[@"opaque_to_smt"]
inline_for_extraction
let list_ffdhe_g2: List.Tot.llist pub_uint8 1 =
  [@inline_let]
  let l = [ 0x02uy ] in
  assert_norm (List.Tot.length l == 1);
  l
val ffdhe_g2:lseq pub_uint8 1
Lib.Sequence.lseq (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB) 1