val uints64_to_bytes_le_lemma: lo:uint64 -> hi:uint64 -> Lemma
  (concat (uint_to_bytes_le lo) (uint_to_bytes_le hi) == nat_to_bytes_le 16 (v hi * pow2 64 + v lo))
let uints64_to_bytes_le_lemma lo hi =
  let lp = nat_to_bytes_le #SEC 16 (v hi * pow2 64 + v lo) in
  let rp = concat (uint_to_bytes_le lo) (uint_to_bytes_le hi) in
  assert (nat_from_bytes_le lp == v hi * pow2 64 + v lo);
  Seq.append_slices (uint_to_bytes_le lo) (uint_to_bytes_le hi);
  nat_from_intseq_le_slice_lemma #U8 #SEC #16 rp 8;
  assert (nat_from_bytes_le rp == nat_from_bytes_le (Seq.slice rp 0 8) + pow2 (8 * 8) * nat_from_bytes_le (Seq.slice rp 8 16));
  assert (nat_from_bytes_le rp == nat_from_bytes_le (uint_to_bytes_le lo) + pow2 64 * nat_from_bytes_le (uint_to_bytes_le hi));
  lemma_uint_to_bytes_le_preserves_value lo;
  lemma_uint_to_bytes_le_preserves_value hi;
  nat_from_intseq_le_inj lp rp
val uints64_to_bytes_le_lemma: lo:uint64 -> hi:uint64 -> Lemma
  (concat (uint_to_bytes_le lo) (uint_to_bytes_le hi) == nat_to_bytes_le 16 (v hi * pow2 64 + v lo))
let uints64_to_bytes_le_lemma lo hi =
let lp = nat_to_bytes_le #SEC 16 (v hi * pow2 64 + v lo) in
let rp = concat (uint_to_bytes_le lo) (uint_to_bytes_le hi) in
assert (nat_from_bytes_le lp == v hi * pow2 64 + v lo);
Seq.append_slices (uint_to_bytes_le lo) (uint_to_bytes_le hi);
nat_from_intseq_le_slice_lemma #U8 #SEC #16 rp 8;
assert (nat_from_bytes_le rp ==
    nat_from_bytes_le (Seq.slice rp 0 8) + pow2 (8 * 8) * nat_from_bytes_le (Seq.slice rp 8 16));
assert (nat_from_bytes_le rp ==
    nat_from_bytes_le (uint_to_bytes_le lo) + pow2 64 * nat_from_bytes_le (uint_to_bytes_le hi));
lemma_uint_to_bytes_le_preserves_value lo;
lemma_uint_to_bytes_le_preserves_value hi;
nat_from_intseq_le_inj lp rp
Hacl.Impl.Poly1305.Lemmas.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Hacl.Impl.Poly1305.Lemmas.fst
Lib.IntTypes.uint64 Lib.ByteSequence.nat_from_intseq_le_inj Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.unit Lib.ByteSequence.lemma_uint_to_bytes_le_preserves_value Lib.IntTypes.U64 Prims._assert Prims.eq2 Prims.int Lib.ByteSequence.nat_from_bytes_le Prims.op_Addition Lib.ByteSequence.uint_to_bytes_le FStar.Mul.op_Star Prims.pow2 FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.ByteSequence.nat_from_intseq_le_slice_lemma FStar.Seq.Properties.append_slices Lib.IntTypes.v Lib.Sequence.lseq Lib.IntTypes.int_t FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.append Lib.Sequence.concat Lib.IntTypes.numbytes Lib.Sequence.seq Prims.l_and Prims.nat Lib.Sequence.length Prims.l_or Prims.b2t Prims.op_LessThan Prims.op_Multiply Lib.ByteSequence.nat_from_intseq_le Lib.ByteSequence.nat_to_bytes_le
module Hacl.Impl.Poly1305.Lemmas

open FStar.Mul

open Lib.IntTypes
open Lib.IntVector
open Lib.Sequence
open Lib.ByteSequence

#set-options "--z3rlimit 50 --max_fuel 1"

val uint_from_bytes_le_lemma: b:lseq uint8 16 -> Lemma
 (let lo = uint_from_bytes_le #U64 (sub b 0 8) in
  let hi = uint_from_bytes_le #U64 (sub b 8 8) in
  nat_from_bytes_le b == pow2 64 * uint_v hi + uint_v lo)

let uint_from_bytes_le_lemma b =
  let r1 = nat_from_bytes_le b in
  let r2 = uints_from_bytes_le #U64 #SEC #2 b in
  uints_from_bytes_le_nat_lemma #U64 #SEC #2 b;
  assert (r1 == nat_from_intseq_le r2);
  nat_from_intseq_le_slice_lemma #U64 #SEC #2 r2 1;
  assert (r1 == nat_from_intseq_le (Seq.slice r2 0 1) + pow2 64 * nat_from_intseq_le #U64 #SEC (Seq.slice r2 1 2));
  nat_from_intseq_le_lemma0 (Seq.slice r2 0 1);
  nat_from_intseq_le_lemma0 (Seq.slice r2 1 2);
  assert (r1 == uint_v r2.[0] + pow2 64 * uint_v r2.[1]);
  Classical.forall_intro (index_uints_from_bytes_le #U64 #SEC #2 b)


val uints_from_bytes_le_lemma64_1: b:lseq uint8 16 -> Lemma
 (let lo:lseq uint64 1 = uints_from_bytes_le (sub b 0 8) in
  let hi:lseq uint64 1 = uints_from_bytes_le (sub b 8 8) in
  nat_from_bytes_le b == pow2 64 * uint_v hi.[0] + uint_v lo.[0])

let uints_from_bytes_le_lemma64_1 b =
  index_uints_from_bytes_le #U64 #SEC #1 (sub b 0 8) 0;
  index_uints_from_bytes_le #U64 #SEC #1 (sub b 8 8) 0;
  uint_from_bytes_le_lemma b


val uints_from_bytes_le_lemma64_2: b:lseq uint8 32 -> Lemma
 (let lo:lseq uint64 2 = uints_from_bytes_le (sub b 0 16) in
  let hi:lseq uint64 2 = uints_from_bytes_le (sub b 16 16) in
  let b1 = nat_from_bytes_le (sub b 0 16) in
  let b2 = nat_from_bytes_le (sub b 16 16) in
  b1 == pow2 64 * uint_v lo.[1] + uint_v lo.[0] /\
  b2 == pow2 64 * uint_v hi.[1] + uint_v hi.[0])

let uints_from_bytes_le_lemma64_2 b =
  Classical.forall_intro (index_uints_from_bytes_le #U64 #SEC #2 (sub b 0 16));
  Classical.forall_intro (index_uints_from_bytes_le #U64 #SEC #2 (sub b 16 16));
  uint_from_bytes_le_lemma (sub b 0 16);
  uint_from_bytes_le_lemma (sub b 16 16)


val uints_from_bytes_le_lemma64_4: b:lseq uint8 64 -> Lemma
 (let lo:lseq uint64 4 = uints_from_bytes_le (sub b 0 32) in
  let hi:lseq uint64 4 = uints_from_bytes_le (sub b 32 32) in
  let b1 = nat_from_bytes_le (sub b 0 16) in
  let b2 = nat_from_bytes_le (sub b 16 16) in
  let b3 = nat_from_bytes_le (sub b 32 16) in
  let b4 = nat_from_bytes_le (sub b 48 16) in
  b1 == pow2 64 * uint_v lo.[1] + uint_v lo.[0] /\
  b2 == pow2 64 * uint_v lo.[3] + uint_v lo.[2] /\
  b3 == pow2 64 * uint_v hi.[1] + uint_v hi.[0] /\
  b4 == pow2 64 * uint_v hi.[3] + uint_v hi.[2])

let uints_from_bytes_le_lemma64_4 b =
  Classical.forall_intro (index_uints_from_bytes_le #U64 #SEC #4 (sub b 0 32));
  Classical.forall_intro (index_uints_from_bytes_le #U64 #SEC #4 (sub b 32 32));
  uint_from_bytes_le_lemma (sub b 0 16);
  uint_from_bytes_le_lemma (sub b 16 16);
  uint_from_bytes_le_lemma (sub b 32 16);
  uint_from_bytes_le_lemma (sub b 48 16)


val uints64_to_bytes_le_lemma: lo:uint64 -> hi:uint64 -> Lemma
  (concat (uint_to_bytes_le lo) (uint_to_bytes_le hi) == nat_to_bytes_le 16 (v hi * pow2 64 + v lo))
val uints64_to_bytes_le_lemma: lo:uint64 -> hi:uint64 -> Lemma
  (concat (uint_to_bytes_le lo) (uint_to_bytes_le hi) == nat_to_bytes_le 16 (v hi * pow2 64 + v lo))
lo: Lib.IntTypes.uint64 -> hi: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
    (ensures
      Lib.Sequence.concat (Lib.ByteSequence.uint_to_bytes_le lo)
        (Lib.ByteSequence.uint_to_bytes_le hi) ==
      Lib.ByteSequence.nat_to_bytes_le 16 (Lib.IntTypes.v hi * Prims.pow2 64 + Lib.IntTypes.v lo))