val lemma_as_nat_bound_f4_lt_powa: f:felem5 -> a:nat -> Lemma
  (requires (let (f0,f1,f2,f3,f4) = f in
    felem_fits5 f (1,1,1,1,1) /\ v f4 < pow2 a))
  (ensures as_nat5 f <= pow2 (208 + a) - 1)
let lemma_as_nat_bound_f4_lt_powa f a =
  let (f0,f1,f2,f3,f4) = f in
  calc (<=) { //as_nat5 f ==
    v f0 + v f1 * pow52 + v f2 * pow104 + v f3 * pow156 + v f4 * pow208;
    (<=) { }
    pow2 52 - 1 + v f1 * pow52 + v f2 * pow104 + v f3 * pow156 + v f4 * pow208;
    (<=) {
      Math.Lemmas.lemma_mult_le_right pow52 (v f1) (pow2 52 - 1);
      Math.Lemmas.distributivity_sub_left (pow2 52) 1 pow52 }
    pow2 52 * pow52 + v f2 * pow104 + v f3 * pow156 + v f4 * pow208 - 1;
    (<=) {
      Math.Lemmas.lemma_mult_le_right pow104 (v f2) (pow2 52 - 1);
      Math.Lemmas.distributivity_sub_left (pow2 52) 1 pow104;
      Math.Lemmas.pow2_plus 52 52 }
    pow2 52 * pow104 + v f3 * pow156 + v f4 * pow208 - 1;
    (<=) {
      Math.Lemmas.lemma_mult_le_right pow156 (v f3) (pow2 52 - 1);
      Math.Lemmas.distributivity_sub_left (pow2 52) 1 pow156;
      Math.Lemmas.pow2_plus 52 104 }
    pow2 52 * pow156 + v f4 * pow208 - 1;
    (<=) {
      Math.Lemmas.lemma_mult_le_right pow208 (v f4) (pow2 a - 1);
      Math.Lemmas.distributivity_sub_left (pow2 a) 1 pow208;
      Math.Lemmas.pow2_plus 52 156;
      Math.Lemmas.pow2_plus a 208 }
    pow2 (208 + a) - 1;
    }
val lemma_as_nat_bound_f4_lt_powa: f:felem5 -> a:nat -> Lemma
  (requires (let (f0,f1,f2,f3,f4) = f in
    felem_fits5 f (1,1,1,1,1) /\ v f4 < pow2 a))
  (ensures as_nat5 f <= pow2 (208 + a) - 1)
let lemma_as_nat_bound_f4_lt_powa f a =
let f0, f1, f2, f3, f4 = f in
calc ( <= ) {
  v f0 + v f1 * pow52 + v f2 * pow104 + v f3 * pow156 + v f4 * pow208;
  ( <= ) { () }
  pow2 52 - 1 + v f1 * pow52 + v f2 * pow104 + v f3 * pow156 + v f4 * pow208;
  ( <= ) { (Math.Lemmas.lemma_mult_le_right pow52 (v f1) (pow2 52 - 1);
    Math.Lemmas.distributivity_sub_left (pow2 52) 1 pow52) }
  pow2 52 * pow52 + v f2 * pow104 + v f3 * pow156 + v f4 * pow208 - 1;
  ( <= ) { (Math.Lemmas.lemma_mult_le_right pow104 (v f2) (pow2 52 - 1);
    Math.Lemmas.distributivity_sub_left (pow2 52) 1 pow104;
    Math.Lemmas.pow2_plus 52 52) }
  pow2 52 * pow104 + v f3 * pow156 + v f4 * pow208 - 1;
  ( <= ) { (Math.Lemmas.lemma_mult_le_right pow156 (v f3) (pow2 52 - 1);
    Math.Lemmas.distributivity_sub_left (pow2 52) 1 pow156;
    Math.Lemmas.pow2_plus 52 104) }
  pow2 52 * pow156 + v f4 * pow208 - 1;
  ( <= ) { (Math.Lemmas.lemma_mult_le_right pow208 (v f4) (pow2 a - 1);
    Math.Lemmas.distributivity_sub_left (pow2 a) 1 pow208;
    Math.Lemmas.pow2_plus 52 156;
    Math.Lemmas.pow2_plus a 208) }
  pow2 (208 + a) - 1;
}
Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.Field52.Definitions.Lemmas.fst
Hacl.Spec.K256.Field52.Definitions.felem5 Prims.nat Lib.IntTypes.uint64 FStar.Calc.calc_finish Prims.int Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Mul.op_Star Hacl.Spec.K256.Field52.Definitions.pow52 Hacl.Spec.K256.Field52.Definitions.pow104 Hacl.Spec.K256.Field52.Definitions.pow156 Hacl.Spec.K256.Field52.Definitions.pow208 Prims.op_Subtraction Prims.pow2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash FStar.Math.Lemmas.distributivity_sub_left FStar.Math.Lemmas.lemma_mult_le_right FStar.Math.Lemmas.pow2_plus
module Hacl.Spec.K256.Field52.Definitions.Lemmas

open FStar.Mul
open Lib.IntTypes

open Hacl.Spec.K256.Field52.Definitions

module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

module S = Spec.K256
module ML = Hacl.Spec.K256.MathLemmas

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

val lemma_as_nat_mod2: x:felem5 ->
  Lemma (let (x0,x1,x2,x3,x4) = x in as_nat5 x % 2 = v x0 % 2)
let lemma_as_nat_mod2 x =
  let (x0,x1,x2,x3,x4) = x in
  assert (as_nat5 x = v x0 + v x1 * pow52 + v x2 * pow104 + v x3 * pow156 + v x4 * pow208);
  assert (as_nat5 x % 2 = (v x0 + v x1 * pow52 + v x2 * pow104 + v x3 * pow156 + v x4 * pow208) % 2);
  ML.lemma_a_plus_b_pow2_mod2 (v x0 + v x1 * pow52 + v x2 * pow104 + v x3 * pow156) (v x4) 208;
  ML.lemma_a_plus_b_pow2_mod2 (v x0 + v x1 * pow52 + v x2 * pow104) (v x3) 156;
  ML.lemma_a_plus_b_pow2_mod2 (v x0 + v x1 * pow52) (v x2) 104;
  ML.lemma_a_plus_b_pow2_mod2 (v x0) (v x1) 52;
  assert (as_nat5 x % 2 = v x0 % 2)


val lemma_nat_from_bytes_be_mod2: f:LSeq.lseq uint8 32 ->
  Lemma (BSeq.nat_from_bytes_be f % 2 = v (LSeq.index f 31) % 2)

let lemma_nat_from_bytes_be_mod2 f =
  let x0 = LSeq.index f 31 in
  BSeq.nat_from_intseq_be_slice_lemma f 31;
  BSeq.nat_from_intseq_be_lemma0 (LSeq.slice f 31 32);
  assert (BSeq.nat_from_intseq_be f == v x0 + pow2 8 * BSeq.nat_from_intseq_be (LSeq.slice f 0 31));
  ML.lemma_a_plus_b_pow2_mod2 (v x0) (BSeq.nat_from_intseq_be (LSeq.slice f 0 31)) 8


val unfold_nat_from_uint64_four: b:LSeq.lseq uint64 4 ->
  Lemma (BSeq.nat_from_intseq_be b ==
    v (LSeq.index b 3) + v (LSeq.index b 2) * pow2 64 +
    v (LSeq.index b 1) * pow2 128 + v (LSeq.index b 0) * pow2 192)

let unfold_nat_from_uint64_four b =
  let b0 = v (LSeq.index b 0) in
  let b1 = v (LSeq.index b 1) in
  let b2 = v (LSeq.index b 2) in
  let b3 = v (LSeq.index b 3) in

  let res = BSeq.nat_from_intseq_be b in
  BSeq.nat_from_intseq_be_slice_lemma b 3;
  BSeq.nat_from_intseq_be_lemma0 (Seq.slice b 3 4);
  assert (res == b3 + pow2 64 * (BSeq.nat_from_intseq_be (Seq.slice b 0 3)));

  BSeq.nat_from_intseq_be_slice_lemma #U64 #SEC #3 (Seq.slice b 0 3) 2;
  BSeq.nat_from_intseq_be_lemma0 (Seq.slice b 2 3);
  assert (BSeq.nat_from_intseq_be (Seq.slice b 0 3) == b2 + pow2 64 * (BSeq.nat_from_intseq_be (Seq.slice b 0 2)));

  BSeq.nat_from_intseq_be_slice_lemma #U64 #SEC #2 (Seq.slice b 0 2) 1;
  BSeq.nat_from_intseq_be_lemma0 (Seq.slice b 1 2);
  assert (BSeq.nat_from_intseq_be (Seq.slice b 0 2) == b1 + pow2 64 * (BSeq.nat_from_intseq_be (Seq.slice b 0 1)));

  BSeq.nat_from_intseq_be_lemma0 (Seq.slice b 0 1);
  assert (res == b3 + pow2 64 * (b2 + pow2 64 * (b1 + pow2 64 * b0)));
  ML.lemma_as_nat64_horner b3 b2 b1 b0


val lemma_prime : unit -> Lemma (pow2 256 % S.prime = 0x1000003D1)
let lemma_prime () = ()

val lemma_pow2_256_minus_prime : unit -> Lemma (pow2 256 - S.prime = 0x1000003D1)
let lemma_pow2_256_minus_prime () = ()

val lemma_pow2_260_mod_prime: unit -> Lemma (pow2 260 % S.prime = 0x1000003D10)
let lemma_pow2_260_mod_prime () =
  calc (==) {
    pow2 260 % S.prime;
    (==) { Math.Lemmas.pow2_plus 256 4 }
    pow2 256 * pow2 4 % S.prime;
    (==) { Math.Lemmas.lemma_mod_mul_distr_l (pow2 256) (pow2 4) S.prime }
    (pow2 256 % S.prime) * pow2 4 % S.prime;
    (==) { lemma_prime () }
    0x1000003D1 * pow2 4 % S.prime;
    (==) { assert_norm (0x1000003D1 * pow2 4 = 0x1000003D10) }
    0x1000003D10 % S.prime;
    (==) { Math.Lemmas.small_mod 0x1000003D10 S.prime }
    0x1000003D10;
  }


val lemma_as_nat_bound_f4_lt_powa: f:felem5 -> a:nat -> Lemma
  (requires (let (f0,f1,f2,f3,f4) = f in
    felem_fits5 f (1,1,1,1,1) /\ v f4 < pow2 a))
  (ensures as_nat5 f <= pow2 (208 + a) - 1)
val lemma_as_nat_bound_f4_lt_powa: f:felem5 -> a:nat -> Lemma
  (requires (let (f0,f1,f2,f3,f4) = f in
    felem_fits5 f (1,1,1,1,1) /\ v f4 < pow2 a))
  (ensures as_nat5 f <= pow2 (208 + a) - 1)
f: Hacl.Spec.K256.Field52.Definitions.felem5 -> a: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        (let _ = f in
          (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ _ _ _ _ f4 = _ in
            Hacl.Spec.K256.Field52.Definitions.felem_fits5 f (1, 1, 1, 1, 1) /\
            Lib.IntTypes.v f4 < Prims.pow2 a)
          <:
          Type0)) (ensures Hacl.Spec.K256.Field52.Definitions.as_nat5 f <= Prims.pow2 (208 + a) - 1)