val lemma_poly1305_equiv_last (text: bytes) (r hBlocks: felem)
    : Lemma
    (ensures
      (let inp = block_fun text in
        let len = length text in
        let nb = len / size_block in
        let last = Seq.slice text (nb * size_block) len in
        let nExtra = len % size_block in
        let padLast = pow2 (nExtra * 8) in
        modp ((hBlocks + padLast + inp nb % padLast) * r) ==
        S.poly1305_update1 r nExtra last hBlocks))
let lemma_poly1305_equiv_last (text:bytes) (r:felem) (hBlocks:felem) : Lemma
  (ensures (
    let inp = block_fun text in
    let len = length text in
    let nb = len / size_block in
    let last = Seq.slice text (nb * size_block) len in
    let nExtra = len % size_block in
    let padLast = pow2 (nExtra * 8) in
    modp ((hBlocks + padLast + inp nb % padLast) * r) == S.poly1305_update1 r nExtra last hBlocks
  ))
  =
  let inp = block_fun text in
  let len = length text in
  let nb = len / size_block in
  let last = Seq.slice text (nb * size_block) len in
  let nExtra = len % size_block in
  let padLast = pow2 (nExtra * 8) in
  let x = nat_from_bytes_le last in
  Math.Lemmas.pow2_le_compat 128 (8 * nExtra);
  FStar.Math.Lemmas.modulo_lemma x padLast;
  assert_norm (x + padLast < prime);
  calc (==) {
    modp ((hBlocks + padLast + inp nb % padLast) * r);
    == {}
    modp ((x + padLast + hBlocks) * r);
    == {assert_norm (modp ((x + padLast + hBlocks) * r) == (x + padLast + hBlocks) * r % prime)}
    (x + padLast + hBlocks) * r % prime;
    == {FStar.Math.Lemmas.lemma_mod_mul_distr_l (x + padLast + hBlocks) r prime}
    ((x + padLast + hBlocks) % prime) * r % prime;
    == {assert_norm (((x + padLast + hBlocks) % prime) * r % prime == fmul (fadd (x + padLast) hBlocks) r)}
    fmul (fadd (x + padLast) hBlocks) r;
    == { FStar.Math.Lemmas.lemma_mod_plus_distr_l (x + padLast) hBlocks prime }
    fmul (fadd (fadd x padLast) hBlocks) r;
    == {}
    S.poly1305_update1 r nExtra last hBlocks;
  }
val lemma_poly1305_equiv_last (text: bytes) (r hBlocks: felem)
    : Lemma
    (ensures
      (let inp = block_fun text in
        let len = length text in
        let nb = len / size_block in
        let last = Seq.slice text (nb * size_block) len in
        let nExtra = len % size_block in
        let padLast = pow2 (nExtra * 8) in
        modp ((hBlocks + padLast + inp nb % padLast) * r) ==
        S.poly1305_update1 r nExtra last hBlocks))
let lemma_poly1305_equiv_last (text: bytes) (r hBlocks: felem)
    : Lemma
    (ensures
      (let inp = block_fun text in
        let len = length text in
        let nb = len / size_block in
        let last = Seq.slice text (nb * size_block) len in
        let nExtra = len % size_block in
        let padLast = pow2 (nExtra * 8) in
        modp ((hBlocks + padLast + inp nb % padLast) * r) ==
        S.poly1305_update1 r nExtra last hBlocks)) =
let inp = block_fun text in
let len = length text in
let nb = len / size_block in
let last = Seq.slice text (nb * size_block) len in
let nExtra = len % size_block in
let padLast = pow2 (nExtra * 8) in
let x = nat_from_bytes_le last in
Math.Lemmas.pow2_le_compat 128 (8 * nExtra);
FStar.Math.Lemmas.modulo_lemma x padLast;
assert_norm (x + padLast < prime);
calc ( == ) {
  modp ((hBlocks + padLast + inp nb % padLast) * r);
  ( == ) { () }
  modp ((x + padLast + hBlocks) * r);
  ( == ) { assert_norm (modp ((x + padLast + hBlocks) * r) == (x + padLast + hBlocks) * r % prime) }
  (x + padLast + hBlocks) * r % prime;
  ( == ) { FStar.Math.Lemmas.lemma_mod_mul_distr_l (x + padLast + hBlocks) r prime }
  ((x + padLast + hBlocks) % prime) * r % prime;
  ( == ) { assert_norm (((x + padLast + hBlocks) % prime) * r % prime ==
      fmul (fadd (x + padLast) hBlocks) r) }
  fmul (fadd (x + padLast) hBlocks) r;
  ( == ) { FStar.Math.Lemmas.lemma_mod_plus_distr_l (x + padLast) hBlocks prime }
  fmul (fadd (fadd x padLast) hBlocks) r;
  ( == ) { () }
  S.poly1305_update1 r nExtra last hBlocks;
}
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
Vale.Poly1305.Equiv.bytes Vale.Poly1305.Equiv.felem FStar.Calc.calc_finish Prims.int Prims.eq2 Vale.Poly1305.Equiv.modp FStar.Mul.op_Star Prims.op_Addition Prims.op_Modulus Spec.Poly1305.poly1305_update1 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Vale.Poly1305.Equiv.fmul Vale.Poly1305.Equiv.fadd Vale.Poly1305.Equiv.prime FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash FStar.Pervasives.assert_norm FStar.Math.Lemmas.lemma_mod_mul_distr_l FStar.Math.Lemmas.lemma_mod_plus_distr_l Prims.b2t Prims.op_LessThan FStar.Math.Lemmas.modulo_lemma FStar.Math.Lemmas.pow2_le_compat Prims.nat Prims.pow2 Prims.op_Multiply Lib.Sequence.length Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Vale.Poly1305.Equiv.nat_from_bytes_le Prims.pos Vale.Poly1305.Equiv.size_block FStar.Seq.Base.seq FStar.Seq.Base.slice Lib.IntTypes.uint_t Prims.op_Division FStar.Seq.Base.length Vale.Def.Words_s.nat128 Vale.Poly1305.Equiv.block_fun Prims.l_True FStar.Pervasives.pattern
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
unfold let repeat_blocks_f = Lib.Sequence.repeat_blocks_f
unfold let sub #a #len = Lib.Sequence.sub #a #len
unfold let lbytes = Lib.ByteSequence.lbytes
unfold let uint_from_bytes_le #t #l = Lib.ByteSequence.uint_from_bytes_le #t #l
unfold let prime = S.prime
unfold let felem = S.felem
unfold let fadd = S.fadd
unfold let fmul = S.fmul
unfold let to_felem = S.to_felem
unfold let modp = V.modp
unfold let mod2_128 = V.mod2_128

#set-options "--z3rlimit 150 --max_fuel 1 --max_ifuel 1"

let rec lemma_poly1305_equiv_rec (text:bytes) (acc0:felem) (r:felem) (k:nat) : Lemma
  (requires k <= length text / size_block)
  (ensures (
    let f = S.poly1305_update1 r size_block in
    let repeat_f = repeat_blocks_f size_block text f (length text / size_block) in
    let pad = pow2 (8 * size_block) in
    V.poly1305_hash_blocks acc0 pad r (block_fun text) k == repeati k repeat_f acc0
  ))
  (decreases k)
  =
  let inp = block_fun text in
  let f = S.poly1305_update1 r size_block in
  let len = length text in
  let nb = len / size_block in
  let repeat_f = repeat_blocks_f size_block text f nb in
  let pad = pow2 (8 * size_block) in
  assert_norm (pow2 128 + pow2 128 < prime);
  if k = 0 then
    Lib.LoopCombinators.eq_repeati0 nb repeat_f acc0
  else
  (
    let kk = k - 1 in
    let hh = V.poly1305_hash_blocks acc0 pad r inp kk in
    let r0:felem = repeati kk repeat_f acc0 in
    let block = Seq.slice text (kk * size_block) (kk * size_block + size_block) in
    calc (==) {
      V.poly1305_hash_blocks acc0 pad r inp k;
      == {}
      modp ((hh + pad + inp kk) * r);
      == {assert_norm (modp ((hh + pad + inp kk) * r) == (hh + pad + inp kk) * r % prime)}
      (hh + pad + inp kk) * r % prime;
      == {FStar.Math.Lemmas.lemma_mod_mul_distr_l (hh + pad + inp kk) r prime}
      ((hh + pad + inp kk) % prime) * r % prime;
      == {lemma_poly1305_equiv_rec text acc0 r kk}
      ((pad + inp kk + r0) % prime) * r % prime;
      == {assert_norm (fmul (fadd (pad + inp kk) r0) r == ((pad + inp kk + r0) % prime) * r % prime)}
      fmul (fadd (pad + inp kk) r0) r;
      == { FStar.Math.Lemmas.lemma_mod_plus_distr_l (pad + inp kk) r0 prime }
      fmul (fadd (fadd pad (inp kk)) r0) r;
      == {}
      S.poly1305_update1 r size_block block (repeati kk repeat_f acc0);
    };
    calc (==) {
      S.poly1305_update1 r size_block block (repeati kk repeat_f acc0);
      == {}
      f block (repeati kk repeat_f acc0);
      == {}
      repeat_f kk (repeati kk repeat_f acc0);
      == {Lib.LoopCombinators.unfold_repeati nb repeat_f acc0 kk}
      repeati k repeat_f acc0;
    }
  )

let lemma_poly1305_equiv_last (text:bytes) (r:felem) (hBlocks:felem) : Lemma
  (ensures (
    let inp = block_fun text in
    let len = length text in
    let nb = len / size_block in
    let last = Seq.slice text (nb * size_block) len in
    let nExtra = len % size_block in
    let padLast = pow2 (nExtra * 8) in
    modp ((hBlocks + padLast + inp nb % padLast) * r) == S.poly1305_update1 r nExtra last hBlocks
val lemma_poly1305_equiv_last (text: bytes) (r hBlocks: felem)
    : Lemma
    (ensures
      (let inp = block_fun text in
        let len = length text in
        let nb = len / size_block in
        let last = Seq.slice text (nb * size_block) len in
        let nExtra = len % size_block in
        let padLast = pow2 (nExtra * 8) in
        modp ((hBlocks + padLast + inp nb % padLast) * r) ==
        S.poly1305_update1 r nExtra last hBlocks))

    text: Vale.Poly1305.Equiv.bytes ->
    r: Vale.Poly1305.Equiv.felem ->
    hBlocks: Vale.Poly1305.Equiv.felem
  -> FStar.Pervasives.Lemma
    (ensures
      (let inp = Vale.Poly1305.Equiv.block_fun text in
        let len = FStar.Seq.Base.length text in
        let nb = len / Vale.Poly1305.Equiv.size_block in
        let last = FStar.Seq.Base.slice text (nb * Vale.Poly1305.Equiv.size_block) len in
        let nExtra = len % Vale.Poly1305.Equiv.size_block in
        let padLast = Prims.pow2 (nExtra * 8) in
        Vale.Poly1305.Equiv.modp ((hBlocks + padLast + inp nb % padLast) * r) ==
        Spec.Poly1305.poly1305_update1 r nExtra last hBlocks))