val ffdhe_p6144:x: glbuffer pub_uint8 768ul {witnessed x S.ffdhe_p6144 /\ recallable x}
let ffdhe_p6144 :x:glbuffer pub_uint8 768ul{witnessed x S.ffdhe_p6144 /\ recallable x} =
  createL_global S.list_ffdhe_p6144
val ffdhe_p6144:x: glbuffer pub_uint8 768ul {witnessed x S.ffdhe_p6144 /\ recallable x}
let ffdhe_p6144:x: glbuffer pub_uint8 768ul {witnessed x S.ffdhe_p6144 /\ recallable x} =
createL_global S.list_ffdhe_p6144
Hacl.Impl.FFDHE.Constants.fst.checked
Spec.FFDHE.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.FFDHE.Constants.fst
Lib.Buffer.createL_global Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB Spec.FFDHE.list_ffdhe_p6144 Lib.Buffer.glbuffer Lib.IntTypes.size FStar.Pervasives.normalize_term Lib.IntTypes.size_nat FStar.List.Tot.Base.length
module Hacl.Impl.FFDHE.Constants

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

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module S = Spec.FFDHE

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

let ffdhe_g2 :x:glbuffer pub_uint8 1ul{witnessed x S.ffdhe_g2 /\ recallable x} =
  createL_global S.list_ffdhe_g2

let ffdhe_p2048 :x:glbuffer pub_uint8 256ul{witnessed x S.ffdhe_p2048 /\ recallable x} =
  createL_global S.list_ffdhe_p2048

let ffdhe_p3072 :x:glbuffer pub_uint8 384ul{witnessed x S.ffdhe_p3072 /\ recallable x} =
  createL_global S.list_ffdhe_p3072

let ffdhe_p4096 :x:glbuffer pub_uint8 512ul{witnessed x S.ffdhe_p4096 /\ recallable x} =
  createL_global S.list_ffdhe_p4096
val ffdhe_p6144:x: glbuffer pub_uint8 768ul {witnessed x S.ffdhe_p6144 /\ recallable x}
x:
(c:
  Lib.Buffer.lbuffer_t Lib.Buffer.CONST
    (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB)
    (FStar.UInt32.uint_to_t 768 <: FStar.UInt32.t)
    {LowStar.ConstBuffer.qual_of c == LowStar.ConstBuffer.IMMUTABLE})
  {Lib.Buffer.witnessed x Spec.FFDHE.ffdhe_p6144 /\ Lib.Buffer.recallable x}