let sub #a #len = Lib.Sequence.sub #a #len
let sub #a #len =
Lib.Sequence.sub #a #len
Vale.Poly1305.Equiv.fst.checked
Vale.Poly1305.Math.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Impl.Poly1305.Lemmas.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Poly1305.Equiv.fst
Lib.IntTypes.size_nat Lib.Sequence.sub Lib.Sequence.lseq Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_Addition Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.slice Prims.l_Forall Prims.op_LessThan Prims.l_or FStar.Seq.Base.index Lib.Sequence.index
module Vale.Poly1305.Equiv
open FStar.Mul

module BSeq = Lib.ByteSequence

// REVIEW: S and V use different smtencoding flags,
// so some equalities between S and V definitions aren't as obvious to Z3 as we might want.

unfold let pow2_128 = Vale.Def.Words_s.pow2_128
unfold let nat64 = Vale.Def.Words_s.nat64
unfold let iand #n = Vale.Def.Types_s.iand #n
unfold let size_nat = Lib.IntTypes.size_nat
unfold let uint_v #t #l = Lib.IntTypes.uint_v #t #l
unfold let uint8 = Lib.IntTypes.uint8
unfold let u64 = Lib.IntTypes.u64
unfold let logand #t #l = Lib.IntTypes.logand #t #l
unfold let repeati = Lib.LoopCombinators.repeati
unfold let repeat_blocks = Lib.Sequence.repeat_blocks
val sub : s1: Lib.Sequence.lseq a len ->
    start: n: Prims.nat{n <= Prims.pow2 32 - 1} ->
    n: (n: Prims.nat{n <= Prims.pow2 32 - 1}){start + n <= len}
  -> s2:
    Lib.Sequence.lseq a n
      { Lib.Sequence.to_seq s2 == FStar.Seq.Base.slice (Lib.Sequence.to_seq s1) start (start + n) /\
        (forall (k: Prims.nat{k < n}). {:pattern Lib.Sequence.index s2 k}
            Lib.Sequence.index s2 k == Lib.Sequence.index s1 (start + k)) }

    s1: Lib.Sequence.lseq a len ->
    start: n: Prims.nat{n <= Prims.pow2 32 - 1} ->
    n: (n: Prims.nat{n <= Prims.pow2 32 - 1}){start + n <= len}
  -> s2:
    Lib.Sequence.lseq a n
      { Lib.Sequence.to_seq s2 == FStar.Seq.Base.slice (Lib.Sequence.to_seq s1) start (start + n) /\
        (forall (k: Prims.nat{k < n}). {:pattern Lib.Sequence.index s2 k}
            Lib.Sequence.index s2 k == Lib.Sequence.index s1 (start + k)) }