val list_ffdhe_p2048:List.Tot.llist pub_uint8 256
let list_ffdhe_p2048: List.Tot.llist pub_uint8 256 =
  [@inline_let]
  let l = [
    0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy;
    0xADuy; 0xF8uy; 0x54uy; 0x58uy; 0xA2uy; 0xBBuy; 0x4Auy; 0x9Auy;
    0xAFuy; 0xDCuy; 0x56uy; 0x20uy; 0x27uy; 0x3Duy; 0x3Cuy; 0xF1uy;
    0xD8uy; 0xB9uy; 0xC5uy; 0x83uy; 0xCEuy; 0x2Duy; 0x36uy; 0x95uy;
    0xA9uy; 0xE1uy; 0x36uy; 0x41uy; 0x14uy; 0x64uy; 0x33uy; 0xFBuy;
    0xCCuy; 0x93uy; 0x9Duy; 0xCEuy; 0x24uy; 0x9Buy; 0x3Euy; 0xF9uy;
    0x7Duy; 0x2Fuy; 0xE3uy; 0x63uy; 0x63uy; 0x0Cuy; 0x75uy; 0xD8uy;
    0xF6uy; 0x81uy; 0xB2uy; 0x02uy; 0xAEuy; 0xC4uy; 0x61uy; 0x7Auy;
    0xD3uy; 0xDFuy; 0x1Euy; 0xD5uy; 0xD5uy; 0xFDuy; 0x65uy; 0x61uy;
    0x24uy; 0x33uy; 0xF5uy; 0x1Fuy; 0x5Fuy; 0x06uy; 0x6Euy; 0xD0uy;
    0x85uy; 0x63uy; 0x65uy; 0x55uy; 0x3Duy; 0xEDuy; 0x1Auy; 0xF3uy;
    0xB5uy; 0x57uy; 0x13uy; 0x5Euy; 0x7Fuy; 0x57uy; 0xC9uy; 0x35uy;
    0x98uy; 0x4Fuy; 0x0Cuy; 0x70uy; 0xE0uy; 0xE6uy; 0x8Buy; 0x77uy;
    0xE2uy; 0xA6uy; 0x89uy; 0xDAuy; 0xF3uy; 0xEFuy; 0xE8uy; 0x72uy;
    0x1Duy; 0xF1uy; 0x58uy; 0xA1uy; 0x36uy; 0xADuy; 0xE7uy; 0x35uy;
    0x30uy; 0xACuy; 0xCAuy; 0x4Fuy; 0x48uy; 0x3Auy; 0x79uy; 0x7Auy;
    0xBCuy; 0x0Auy; 0xB1uy; 0x82uy; 0xB3uy; 0x24uy; 0xFBuy; 0x61uy;
    0xD1uy; 0x08uy; 0xA9uy; 0x4Buy; 0xB2uy; 0xC8uy; 0xE3uy; 0xFBuy;
    0xB9uy; 0x6Auy; 0xDAuy; 0xB7uy; 0x60uy; 0xD7uy; 0xF4uy; 0x68uy;
    0x1Duy; 0x4Fuy; 0x42uy; 0xA3uy; 0xDEuy; 0x39uy; 0x4Duy; 0xF4uy;
    0xAEuy; 0x56uy; 0xEDuy; 0xE7uy; 0x63uy; 0x72uy; 0xBBuy; 0x19uy;
    0x0Buy; 0x07uy; 0xA7uy; 0xC8uy; 0xEEuy; 0x0Auy; 0x6Duy; 0x70uy;
    0x9Euy; 0x02uy; 0xFCuy; 0xE1uy; 0xCDuy; 0xF7uy; 0xE2uy; 0xECuy;
    0xC0uy; 0x34uy; 0x04uy; 0xCDuy; 0x28uy; 0x34uy; 0x2Fuy; 0x61uy;
    0x91uy; 0x72uy; 0xFEuy; 0x9Cuy; 0xE9uy; 0x85uy; 0x83uy; 0xFFuy;
    0x8Euy; 0x4Fuy; 0x12uy; 0x32uy; 0xEEuy; 0xF2uy; 0x81uy; 0x83uy;
    0xC3uy; 0xFEuy; 0x3Buy; 0x1Buy; 0x4Cuy; 0x6Fuy; 0xADuy; 0x73uy;
    0x3Buy; 0xB5uy; 0xFCuy; 0xBCuy; 0x2Euy; 0xC2uy; 0x20uy; 0x05uy;
    0xC5uy; 0x8Euy; 0xF1uy; 0x83uy; 0x7Duy; 0x16uy; 0x83uy; 0xB2uy;
    0xC6uy; 0xF3uy; 0x4Auy; 0x26uy; 0xC1uy; 0xB2uy; 0xEFuy; 0xFAuy;
    0x88uy; 0x6Buy; 0x42uy; 0x38uy; 0x61uy; 0x28uy; 0x5Cuy; 0x97uy;
    0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy
  ] in
  assert_norm (List.Tot.length l == 256);
  l
val list_ffdhe_p2048:List.Tot.llist pub_uint8 256
let list_ffdhe_p2048:List.Tot.llist pub_uint8 256 =
[@@ inline_let ]let l =
  [
    0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy; 0xADuy; 0xF8uy; 0x54uy; 0x58uy;
    0xA2uy; 0xBBuy; 0x4Auy; 0x9Auy; 0xAFuy; 0xDCuy; 0x56uy; 0x20uy; 0x27uy; 0x3Duy; 0x3Cuy; 0xF1uy;
    0xD8uy; 0xB9uy; 0xC5uy; 0x83uy; 0xCEuy; 0x2Duy; 0x36uy; 0x95uy; 0xA9uy; 0xE1uy; 0x36uy; 0x41uy;
    0x14uy; 0x64uy; 0x33uy; 0xFBuy; 0xCCuy; 0x93uy; 0x9Duy; 0xCEuy; 0x24uy; 0x9Buy; 0x3Euy; 0xF9uy;
    0x7Duy; 0x2Fuy; 0xE3uy; 0x63uy; 0x63uy; 0x0Cuy; 0x75uy; 0xD8uy; 0xF6uy; 0x81uy; 0xB2uy; 0x02uy;
    0xAEuy; 0xC4uy; 0x61uy; 0x7Auy; 0xD3uy; 0xDFuy; 0x1Euy; 0xD5uy; 0xD5uy; 0xFDuy; 0x65uy; 0x61uy;
    0x24uy; 0x33uy; 0xF5uy; 0x1Fuy; 0x5Fuy; 0x06uy; 0x6Euy; 0xD0uy; 0x85uy; 0x63uy; 0x65uy; 0x55uy;
    0x3Duy; 0xEDuy; 0x1Auy; 0xF3uy; 0xB5uy; 0x57uy; 0x13uy; 0x5Euy; 0x7Fuy; 0x57uy; 0xC9uy; 0x35uy;
    0x98uy; 0x4Fuy; 0x0Cuy; 0x70uy; 0xE0uy; 0xE6uy; 0x8Buy; 0x77uy; 0xE2uy; 0xA6uy; 0x89uy; 0xDAuy;
    0xF3uy; 0xEFuy; 0xE8uy; 0x72uy; 0x1Duy; 0xF1uy; 0x58uy; 0xA1uy; 0x36uy; 0xADuy; 0xE7uy; 0x35uy;
    0x30uy; 0xACuy; 0xCAuy; 0x4Fuy; 0x48uy; 0x3Auy; 0x79uy; 0x7Auy; 0xBCuy; 0x0Auy; 0xB1uy; 0x82uy;
    0xB3uy; 0x24uy; 0xFBuy; 0x61uy; 0xD1uy; 0x08uy; 0xA9uy; 0x4Buy; 0xB2uy; 0xC8uy; 0xE3uy; 0xFBuy;
    0xB9uy; 0x6Auy; 0xDAuy; 0xB7uy; 0x60uy; 0xD7uy; 0xF4uy; 0x68uy; 0x1Duy; 0x4Fuy; 0x42uy; 0xA3uy;
    0xDEuy; 0x39uy; 0x4Duy; 0xF4uy; 0xAEuy; 0x56uy; 0xEDuy; 0xE7uy; 0x63uy; 0x72uy; 0xBBuy; 0x19uy;
    0x0Buy; 0x07uy; 0xA7uy; 0xC8uy; 0xEEuy; 0x0Auy; 0x6Duy; 0x70uy; 0x9Euy; 0x02uy; 0xFCuy; 0xE1uy;
    0xCDuy; 0xF7uy; 0xE2uy; 0xECuy; 0xC0uy; 0x34uy; 0x04uy; 0xCDuy; 0x28uy; 0x34uy; 0x2Fuy; 0x61uy;
    0x91uy; 0x72uy; 0xFEuy; 0x9Cuy; 0xE9uy; 0x85uy; 0x83uy; 0xFFuy; 0x8Euy; 0x4Fuy; 0x12uy; 0x32uy;
    0xEEuy; 0xF2uy; 0x81uy; 0x83uy; 0xC3uy; 0xFEuy; 0x3Buy; 0x1Buy; 0x4Cuy; 0x6Fuy; 0xADuy; 0x73uy;
    0x3Buy; 0xB5uy; 0xFCuy; 0xBCuy; 0x2Euy; 0xC2uy; 0x20uy; 0x05uy; 0xC5uy; 0x8Euy; 0xF1uy; 0x83uy;
    0x7Duy; 0x16uy; 0x83uy; 0xB2uy; 0xC6uy; 0xF3uy; 0x4Auy; 0x26uy; 0xC1uy; 0xB2uy; 0xEFuy; 0xFAuy;
    0x88uy; 0x6Buy; 0x42uy; 0x38uy; 0x61uy; 0x28uy; 0x5Cuy; 0x97uy; 0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy;
    0xFFuy; 0xFFuy; 0xFFuy; 0xFFuy
  ]
in
assert_norm (List.Tot.length l == 256);
l
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
Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int FStar.List.Tot.Base.length Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB Prims.list Prims.Cons FStar.UInt8.__uint_to_t Prims.Nil
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

let ffdhe_g2: lseq pub_uint8 1 = of_list list_ffdhe_g2


[@"opaque_to_smt"]
inline_for_extraction
val list_ffdhe_p2048:List.Tot.llist pub_uint8 256
FStar.List.Tot.Properties.llist (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB) 256