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 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)
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.Sequence.lseq Lib.IntTypes.uint8 Hacl.Impl.Poly1305.Lemmas.uint_from_bytes_le_lemma Lib.Sequence.sub Prims.unit FStar.Classical.forall_intro Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThan Prims.eq2 Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.Sequence.index Lib.ByteSequence.uints_from_bytes_le Lib.ByteSequence.uint_from_bytes_le Lib.IntTypes.U8 FStar.Mul.op_Star Lib.IntTypes.numbytes Lib.ByteSequence.index_uints_from_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])
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])
b: Lib.Sequence.lseq Lib.IntTypes.uint8 64
  -> FStar.Pervasives.Lemma
    (ensures
      (let lo = Lib.ByteSequence.uints_from_bytes_le (Lib.Sequence.sub b 0 32) in
        let hi = Lib.ByteSequence.uints_from_bytes_le (Lib.Sequence.sub b 32 32) in
        let b1 = Lib.ByteSequence.nat_from_bytes_le (Lib.Sequence.sub b 0 16) in
        let b2 = Lib.ByteSequence.nat_from_bytes_le (Lib.Sequence.sub b 16 16) in
        let b3 = Lib.ByteSequence.nat_from_bytes_le (Lib.Sequence.sub b 32 16) in
        let b4 = Lib.ByteSequence.nat_from_bytes_le (Lib.Sequence.sub b 48 16) in
        b1 == Prims.pow2 64 * Lib.IntTypes.uint_v lo.[ 1 ] + Lib.IntTypes.uint_v lo.[ 0 ] /\
        b2 == Prims.pow2 64 * Lib.IntTypes.uint_v lo.[ 3 ] + Lib.IntTypes.uint_v lo.[ 2 ] /\
        b3 == Prims.pow2 64 * Lib.IntTypes.uint_v hi.[ 1 ] + Lib.IntTypes.uint_v hi.[ 0 ] /\
        b4 == Prims.pow2 64 * Lib.IntTypes.uint_v hi.[ 3 ] + Lib.IntTypes.uint_v hi.[ 2 ]))