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 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
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
Lib.Sequence.lseq Lib.IntTypes.uint64 Hacl.Spec.K256.MathLemmas.lemma_as_nat64_horner Prims.unit Prims._assert Prims.eq2 Prims.int Prims.op_Addition FStar.Mul.op_Star Prims.pow2 Lib.ByteSequence.nat_from_intseq_be_lemma0 Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Seq.Base.slice Lib.ByteSequence.nat_from_intseq_be Lib.ByteSequence.nat_from_intseq_be_slice_lemma Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Multiply Lib.Sequence.length Lib.IntTypes.int_t Lib.IntTypes.range Lib.IntTypes.v Lib.Sequence.index
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)
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)
b: Lib.Sequence.lseq Lib.IntTypes.uint64 4
  -> FStar.Pervasives.Lemma
    (ensures
      Lib.ByteSequence.nat_from_intseq_be b ==
      Lib.IntTypes.v (Lib.Sequence.index b 3) +
      Lib.IntTypes.v (Lib.Sequence.index b 2) * Prims.pow2 64 +
      Lib.IntTypes.v (Lib.Sequence.index b 1) * Prims.pow2 128 +
      Lib.IntTypes.v (Lib.Sequence.index b 0) * Prims.pow2 192)