val ffdhe_p_bits_lemma: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let len = ffdhe_len a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  let p_n = nat_from_bytes_be p in
  pow2 (8 * len - 1) < p_n)
let ffdhe_p_bits_lemma a =
  let ffdhe_p = get_ffdhe_params a in
  let len = ffdhe_len a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  let p_n = nat_from_bytes_be p in

  nat_from_intseq_be_slice_lemma p 1;
  assert (p_n == nat_from_bytes_be (slice p 1 len) + pow2 (8 * (len - 1)) * nat_from_bytes_be (slice p 0 1));
  nat_from_intseq_be_lemma0 (slice p 0 1);
  assert (p_n == nat_from_bytes_be (slice p 1 len) + pow2 (8 * (len - 1)) * v p.[0]);
  assert (pow2 (8 * (len - 1)) * v p.[0] <= p_n);
  ffdhe_p_lemma_len a;
  assert (pow2 (8 * (len - 1)) * (pow2 8 - 1) <= p_n);
  pow2_lt_len len
val ffdhe_p_bits_lemma: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let len = ffdhe_len a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  let p_n = nat_from_bytes_be p in
  pow2 (8 * len - 1) < p_n)
let ffdhe_p_bits_lemma a =
let ffdhe_p = get_ffdhe_params a in
let len = ffdhe_len a in
let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
let p_n = nat_from_bytes_be p in
nat_from_intseq_be_slice_lemma p 1;
assert (p_n ==
    nat_from_bytes_be (slice p 1 len) + pow2 (8 * (len - 1)) * nat_from_bytes_be (slice p 0 1));
nat_from_intseq_be_lemma0 (slice p 0 1);
assert (p_n == nat_from_bytes_be (slice p 1 len) + pow2 (8 * (len - 1)) * v p.[ 0 ]);
assert (pow2 (8 * (len - 1)) * v p.[ 0 ] <= p_n);
ffdhe_p_lemma_len a;
assert (pow2 (8 * (len - 1)) * (pow2 8 - 1) <= p_n);
pow2_lt_len len
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 Hacl.Spec.FFDHE.Lemmas.pow2_lt_len Prims.unit Prims._assert Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.pow2 Prims.op_Subtraction Hacl.Spec.FFDHE.Lemmas.ffdhe_p_lemma_len Lib.IntTypes.v Lib.IntTypes.U8 Lib.IntTypes.PUB Lib.Sequence.op_String_Access Lib.IntTypes.pub_uint8 Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p_len Prims.eq2 Prims.int Prims.op_Addition Lib.ByteSequence.nat_from_bytes_be Lib.Sequence.slice Lib.ByteSequence.nat_from_intseq_be_lemma0 Lib.ByteSequence.nat_from_intseq_be_slice_lemma Prims.nat Prims.op_LessThan Prims.op_Multiply Lib.Sequence.length Lib.IntTypes.int_t Lib.Sequence.lseq Spec.FFDHE.__proj__Mk_ffdhe_params__item__ffdhe_p Prims.pos Spec.FFDHE.ffdhe_len 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)

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)


// the proof should be somehow simpler
val pow2_lt_len: len:size_pos -> Lemma (pow2 (8 * len - 1) < pow2 (8 * (len - 1)) * (pow2 8 - 1))
let pow2_lt_len len =
  let a = pow2 (8 * len - 1) in
  let b = pow2 (8 * (len - 1)) * (pow2 8 - 1) in
  calc (==) {
    b / a;
    (==) { Math.Lemmas.pow2_plus (8 * len - 8) 7 }
    b / (pow2 (8 * len - 8) * pow2 7);
    (==) { Math.Lemmas.division_multiplication_lemma b (pow2 (8 * len - 8)) (pow2 7) }
    b / pow2 (8 * len - 8) / pow2 7;
    (==) { Math.Lemmas.cancel_mul_div (pow2 8 - 1) (pow2 (8 * len - 8)) }
    (pow2 8 - 1) / pow2 7;
    (==) { Math.Lemmas.pow2_plus 7 1 }
    (pow2 7 * 2 - 1) / pow2 7;
    (==) { }
    1;
    };
  //  assert (b / a * a <= b);
  //  assert (a <= b)

  calc (>) {
    pow2 (8 * len - 8) * (pow2 8 - 1) % pow2 (8 * len - 1);
    (==) { Math.Lemmas.pow2_plus (8 * len - 8) 8 }
    (pow2 (8 * len) - pow2 (8 * len - 8)) % pow2 (8 * len - 1);
    (==) { Math.Lemmas.lemma_mod_plus_distr_l (pow2 (8 * len)) (- pow2 (8 * len - 8)) (pow2 (8 * len - 1)) }
    (pow2 (8 * len) % pow2 (8 * len - 1) - pow2 (8 * len - 8)) % pow2 (8 * len - 1);
    (==) { Math.Lemmas.pow2_multiplication_modulo_lemma_1 1 (8 * len - 1) (8 * len) }
    (0 - pow2 (8 * len - 8)) % pow2 (8 * len - 1);
    //(==) { Math.Lemmas.pow2_lt_compat (8 * len - 1) (8 * len - 8) }
    //pow2 (8 * len - 1) - pow2 (8 * len - 8);
    (>) { Math.Lemmas.pow2_lt_compat (8 * len - 1) (8 * len - 8) }
    0;
    };

  assert (a < b)


val ffdhe_p_bits_lemma: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let len = ffdhe_len a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  let p_n = nat_from_bytes_be p in
  pow2 (8 * len - 1) < p_n)
val ffdhe_p_bits_lemma: a:ffdhe_alg -> Lemma
 (let ffdhe_p = get_ffdhe_params a in
  let len = ffdhe_len a in
  let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
  let p_n = nat_from_bytes_be p in
  pow2 (8 * len - 1) < p_n)
a: Spec.FFDHE.ffdhe_alg
  -> FStar.Pervasives.Lemma
    (ensures
      (let ffdhe_p = Spec.FFDHE.get_ffdhe_params a in
        let len = Spec.FFDHE.ffdhe_len a in
        let p = Mk_ffdhe_params?.ffdhe_p ffdhe_p in
        let p_n = Lib.ByteSequence.nat_from_bytes_be p in
        Prims.pow2 (8 * len - 1) < p_n))