val lemma_mod_pow2_sub: x:nat -> a:nat -> b:nat ->
  Lemma (x / pow2 a % pow2 b * pow2 a == x % pow2 (a + b) - x % pow2 a)
let lemma_mod_pow2_sub x a b =
  calc (==) {
    x / pow2 a % pow2 b * pow2 a;
    (==) { Math.Lemmas.pow2_modulo_division_lemma_1 x a (a + b) }
    x % pow2 (a + b) / pow2 a * pow2 a;
    (==) { Math.Lemmas.euclidean_division_definition (x % pow2 (a + b)) (pow2 a) }
    x % pow2 (a + b) - x % pow2 (a + b) % pow2 a;
    (==) { Math.Lemmas.pow2_modulo_modulo_lemma_1 x a (a + b) }
    x % pow2 (a + b) - x % pow2 a;
  }
val lemma_mod_pow2_sub: x:nat -> a:nat -> b:nat ->
  Lemma (x / pow2 a % pow2 b * pow2 a == x % pow2 (a + b) - x % pow2 a)
let lemma_mod_pow2_sub x a b =
calc ( == ) {
  (x / pow2 a % pow2 b) * pow2 a;
  ( == ) { Math.Lemmas.pow2_modulo_division_lemma_1 x a (a + b) }
  (x % pow2 (a + b) / pow2 a) * pow2 a;
  ( == ) { Math.Lemmas.euclidean_division_definition (x % pow2 (a + b)) (pow2 a) }
  x % pow2 (a + b) - x % pow2 (a + b) % pow2 a;
  ( == ) { Math.Lemmas.pow2_modulo_modulo_lemma_1 x a (a + b) }
  x % pow2 (a + b) - x % pow2 a;
}
Hacl.Spec.Ed25519.PrecompTable.fst.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.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.Ed25519.PrecompTable.fst
Prims.nat FStar.Calc.calc_finish Prims.int Prims.eq2 FStar.Mul.op_Star Prims.op_Modulus Prims.op_Division Prims.pow2 Prims.op_Subtraction Prims.op_Addition Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.pow2_modulo_division_lemma_1 Prims.squash FStar.Math.Lemmas.euclidean_division_definition FStar.Math.Lemmas.pow2_modulo_modulo_lemma_1
module Hacl.Spec.Ed25519.PrecompTable

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence

module F51 = Hacl.Impl.Ed25519.Field51
module SF51 = Hacl.Spec.Curve25519.Field51.Definition

module S = Spec.Ed25519
module SC = Spec.Curve25519
module FL = FStar.List.Tot
module SPT = Hacl.Spec.PrecompBaseTable

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


let create5_lseq (x0 x1 x2 x3 x4:uint64) : lseq uint64 5 =
  let l = [x0; x1; x2; x3; x4] in
  assert_norm (FL.length l = 5);
  Seq.seq_of_list l


val create5_lemma (x0 x1 x2 x3 x4:uint64) :
  Lemma (let s = create5_lseq x0 x1 x2 x3 x4 in
    s.[0] == x0 /\ s.[1] == x1 /\ s.[2] == x2 /\ s.[3] == x3 /\ s.[4] == x4)
let create5_lemma x0 x1 x2 x3 x4 =
  Seq.elim_of_list [x0; x1; x2; x3; x4]

//-----------------------------------

noextract
let list_as_felem5 (f:felem_list) : SF51.felem5 =
  let x = Seq.seq_of_list f <: lseq uint64 5 in
  F51.lseq_as_felem x


val felem_to_list_index_lemma: x:SC.elem ->
  Lemma (let (f0, f1, f2, f3, f4) = list_as_felem5 (felem_to_list x) in
    let x0 = x % pow51 in
    let x1 = x / pow51 % pow51 in
    let x2 = x / pow102 % pow51 in
    let x3 = x / pow153 % pow51 in
    let x4 = x / pow204 in
    v f0 == x0 /\ v f1 == x1 /\ v f2 == x2 /\ v f3 == x3 /\ v f4 == x4)

let felem_to_list_index_lemma x =
  let x0 = x % pow51 in
  let x1 = x / pow51 % pow51 in
  let x2 = x / pow102 % pow51 in
  let x3 = x / pow153 % pow51 in
  let x4 = x / pow204 in
  let f = felem_to_list x in

  let (f0, f1, f2, f3, f4) = list_as_felem5 f in
  Math.Lemmas.lemma_div_lt_nat x 255 204;
  create5_lemma (u64 x0) (u64 x1) (u64 x2) (u64 x3) (u64 x4);
  assert (v f0 == x0 /\ v f1 == x1 /\ v f2 == x2 /\ v f3 == x3 /\ v f4 == x4)


val felem_to_list_lemma_fits: x:SC.elem ->
  Lemma (SF51.felem_fits5 (list_as_felem5 (felem_to_list x)) (1, 1, 1, 1, 1))

let felem_to_list_lemma_fits x =
  felem_to_list_index_lemma x;
  let x0 = x % pow51 in
  let x1 = x / pow51 % pow51 in
  let x2 = x / pow102 % pow51 in
  let x3 = x / pow153 % pow51 in
  let x4 = x / pow204 in
  assert (SF51.felem_fits1 (u64 x0) 1);
  assert (SF51.felem_fits1 (u64 x1) 1);
  assert (SF51.felem_fits1 (u64 x2) 1);
  assert (SF51.felem_fits1 (u64 x3) 1);
  Math.Lemmas.lemma_div_lt_nat x 255 204;
  assert (SF51.felem_fits1 (u64 x4) 1)


val lemma_mod_pow2_sub: x:nat -> a:nat -> b:nat ->
  Lemma (x / pow2 a % pow2 b * pow2 a == x % pow2 (a + b) - x % pow2 a)
val lemma_mod_pow2_sub: x:nat -> a:nat -> b:nat ->
  Lemma (x / pow2 a % pow2 b * pow2 a == x % pow2 (a + b) - x % pow2 a)
x: Prims.nat -> a: Prims.nat -> b: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      (x / Prims.pow2 a % Prims.pow2 b) * Prims.pow2 a == x % Prims.pow2 (a + b) - x % Prims.pow2 a)