val lemma_poly1305_equiv_rec (text: bytes) (acc0 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 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;
    }
  )
val lemma_poly1305_equiv_rec (text: bytes) (acc0 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 rec lemma_poly1305_equiv_rec (text: bytes) (acc0 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;
    })
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 Prims.nat Prims.op_Equality Prims.int Lib.LoopCombinators.eq_repeati0 Spec.Poly1305.felem Prims.bool FStar.Calc.calc_finish Prims.eq2 Spec.Poly1305.poly1305_update1 Vale.Poly1305.Equiv.size_block Vale.Poly1305.Equiv.repeati Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Lib.LoopCombinators.unfold_repeati Vale.Poly1305.Spec_s.poly1305_hash_blocks Vale.Poly1305.Equiv.fmul Vale.Poly1305.Equiv.fadd Prims.op_Addition Prims.op_Modulus FStar.Mul.op_Star Vale.Poly1305.Equiv.prime Vale.Poly1305.Equiv.modp FStar.Pervasives.assert_norm FStar.Math.Lemmas.lemma_mod_mul_distr_l Vale.Poly1305.Equiv.lemma_poly1305_equiv_rec FStar.Math.Lemmas.lemma_mod_plus_distr_l FStar.Seq.Base.seq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.Seq.Base.slice Lib.IntTypes.uint_t Prims.op_Subtraction Prims.b2t Prims.op_LessThan Prims.pow2 Prims.pos Vale.Poly1305.Equiv.repeat_blocks_f Prims.op_Division FStar.Seq.Base.length Lib.Sequence.lseq Spec.Poly1305.size_block Vale.Def.Words_s.nat128 Vale.Poly1305.Equiv.block_fun Prims.op_LessThanOrEqual 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
  ))
val lemma_poly1305_equiv_rec (text: bytes) (acc0 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)

    text: Vale.Poly1305.Equiv.bytes ->
    acc0: Vale.Poly1305.Equiv.felem ->
    r: Vale.Poly1305.Equiv.felem ->
    k: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires k <= FStar.Seq.Base.length text / Vale.Poly1305.Equiv.size_block)
      (ensures
        (let f = Spec.Poly1305.poly1305_update1 r Vale.Poly1305.Equiv.size_block in
          let repeat_f =
            Vale.Poly1305.Equiv.repeat_blocks_f Vale.Poly1305.Equiv.size_block
              text
              f
              (FStar.Seq.Base.length text / Vale.Poly1305.Equiv.size_block)
          in
          let pad = Prims.pow2 (8 * Vale.Poly1305.Equiv.size_block) in
          Vale.Poly1305.Spec_s.poly1305_hash_blocks acc0
            pad
            r
            (Vale.Poly1305.Equiv.block_fun text)
            k ==
          Vale.Poly1305.Equiv.repeati k repeat_f acc0))
      (decreases k)