val ffdhe_p_lemma_len: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  Seq.index p 0 == 0xffuy)
let ffdhe_p_lemma_len a =
  let ffdhe_p = get_ffdhe_params a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in

  allow_inversion ffdhe_alg;
  match a with
  | FFDHE2048 ->
    assert (p == of_list list_ffdhe_p2048);
    assert_norm (List.Tot.index list_ffdhe_p2048 0 == 0xffuy);
    assert (Seq.index (Seq.seq_of_list list_ffdhe_p2048) 0 == 0xffuy)
  | FFDHE3072 ->
    assert (p == of_list list_ffdhe_p3072);
    assert_norm (List.Tot.index list_ffdhe_p3072 0 == 0xffuy);
    assert (Seq.index (Seq.seq_of_list list_ffdhe_p3072) 0 == 0xffuy)
  | FFDHE4096 ->
    assert (p == of_list list_ffdhe_p4096);
    assert_norm (List.Tot.index list_ffdhe_p4096 0 == 0xffuy);
    assert (Seq.index (Seq.seq_of_list list_ffdhe_p4096) 0 == 0xffuy)
  | FFDHE6144 ->
    assert (p == of_list list_ffdhe_p6144);
    assert_norm (List.Tot.index list_ffdhe_p6144 0 == 0xffuy);
    assert (Seq.index (Seq.seq_of_list list_ffdhe_p6144) 0 == 0xffuy)
  | FFDHE8192 ->
    assert (p == of_list list_ffdhe_p8192);
    assert_norm (List.Tot.index list_ffdhe_p8192 0 == 0xffuy);
    assert (Seq.index (Seq.seq_of_list list_ffdhe_p8192) 0 == 0xffuy)
val ffdhe_p_lemma_len: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  Seq.index p 0 == 0xffuy)
let ffdhe_p_lemma_len a =
let ffdhe_p = get_ffdhe_params a in
let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
allow_inversion ffdhe_alg;
match a with
| FFDHE2048 ->
  assert (p == of_list list_ffdhe_p2048);
  assert_norm (List.Tot.index list_ffdhe_p2048 0 == 0xffuy);
  assert (Seq.index (Seq.seq_of_list list_ffdhe_p2048) 0 == 0xffuy)
| FFDHE3072 ->
  assert (p == of_list list_ffdhe_p3072);
  assert_norm (List.Tot.index list_ffdhe_p3072 0 == 0xffuy);
  assert (Seq.index (Seq.seq_of_list list_ffdhe_p3072) 0 == 0xffuy)
| FFDHE4096 ->
  assert (p == of_list list_ffdhe_p4096);
  assert_norm (List.Tot.index list_ffdhe_p4096 0 == 0xffuy);
  assert (Seq.index (Seq.seq_of_list list_ffdhe_p4096) 0 == 0xffuy)
| FFDHE6144 ->
  assert (p == of_list list_ffdhe_p6144);
  assert_norm (List.Tot.index list_ffdhe_p6144 0 == 0xffuy);
  assert (Seq.index (Seq.seq_of_list list_ffdhe_p6144) 0 == 0xffuy)
| FFDHE8192 ->
  assert (p == of_list list_ffdhe_p8192);
  assert_norm (List.Tot.index list_ffdhe_p8192 0 == 0xffuy);
  assert (Seq.index (Seq.seq_of_list list_ffdhe_p8192) 0 == 0xffuy)
Hacl.Spec.FFDHE.Lemmas.fst.checked
Spec.FFDHE.fst.checked prims.fst.checked Lib.Sequence.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.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.FFDHE.Lemmas.fst
Spec.FFDHE.ffdhe_alg Prims._assert Prims.eq2 FStar.UInt8.t FStar.Seq.Base.index Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB FStar.Seq.Properties.seq_of_list Spec.FFDHE.list_ffdhe_p2048 FStar.UInt8.__uint_to_t Prims.unit FStar.Pervasives.assert_norm FStar.List.Tot.Base.index Lib.Sequence.seq Lib.IntTypes.pub_uint8 Prims.l_or Prims.nat FStar.Seq.Base.length Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p_len Prims.l_and FStar.List.Tot.Base.length FStar.Seq.Base.seq Lib.Sequence.to_seq Lib.Sequence.of_list Spec.FFDHE.list_ffdhe_p3072 Spec.FFDHE.list_ffdhe_p4096 Spec.FFDHE.list_ffdhe_p6144 Spec.FFDHE.list_ffdhe_p8192 FStar.Pervasives.allow_inversion Lib.Sequence.lseq Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p Spec.FFDHE.ffdhe_params_t Spec.FFDHE.get_ffdhe_params
module Hacl.Spec.FFDHE.Lemmas

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence
open Spec.FFDHE

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


val ffdhe_p_lemma_len: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  Seq.index p 0 == 0xffuy)
val ffdhe_p_lemma_len: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  Seq.index p 0 == 0xffuy)
a: Spec.FFDHE.ffdhe_alg
  -> FStar.Pervasives.Lemma
    (ensures
      (let ffdhe_p = Spec.FFDHE.get_ffdhe_params a in
        let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
        FStar.Seq.Base.index p 0 == 0xffuy))