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_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;
}
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
Prims.unit FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Modulus Prims.pow2 Spec.K256.PointOps.prime Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Mul.op_Star FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.pow2_plus Prims.squash FStar.Math.Lemmas.lemma_mod_mul_distr_l Hacl.Spec.K256.Field52.Definitions.Lemmas.lemma_prime FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality FStar.Math.Lemmas.small_mod
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)
val lemma_pow2_260_mod_prime: unit -> Lemma (pow2 260 % S.prime = 0x1000003D10)
_: Prims.unit
  -> FStar.Pervasives.Lemma (ensures Prims.pow2 260 % Spec.K256.PointOps.prime = 0x1000003D10)