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 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;
};
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) }
  0;
};
assert (a < b)
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
Lib.IntTypes.size_pos Prims._assert Prims.b2t Prims.op_LessThan Prims.unit FStar.Calc.calc_finish Prims.int Prims.op_GreaterThan Prims.op_Modulus FStar.Mul.op_Star Prims.pow2 Prims.op_Subtraction Prims.Cons FStar.Preorder.relation Prims.eq2 Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.pow2_plus Prims.squash FStar.Math.Lemmas.lemma_mod_plus_distr_l Prims.op_Minus FStar.Math.Lemmas.pow2_multiplication_modulo_lemma_1 FStar.Math.Lemmas.pow2_lt_compat Prims.op_Division FStar.Math.Lemmas.division_multiplication_lemma FStar.Math.Lemmas.cancel_mul_div Prims.pos
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))
len: Lib.IntTypes.size_pos
  -> FStar.Pervasives.Lemma
    (ensures Prims.pow2 (8 * len - 1) < Prims.pow2 (8 * (len - 1)) * (Prims.pow2 8 - 1))