val poly1305_hash_blocks (h pad r: int) (inp: (int -> nat128)) (k: nat) : int
let rec poly1305_hash_blocks (h pad r:int) (inp:int -> nat128) (k:nat) : int =
  if k = 0 then h
  else
    let hh = poly1305_hash_blocks h pad r inp (k - 1) in
    modp ((hh + pad + inp (k - 1)) * r)
val poly1305_hash_blocks (h pad r: int) (inp: (int -> nat128)) (k: nat) : int
let rec poly1305_hash_blocks (h pad r: int) (inp: (int -> nat128)) (k: nat) : int =
if k = 0
then h
else
  let hh = poly1305_hash_blocks h pad r inp (k - 1) in
  modp ((hh + pad + inp (k - 1)) * r)
Vale.Poly1305.Spec_s.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Poly1305.Spec_s.fst
Prims.int Vale.Def.Words_s.nat128 Prims.nat Prims.op_Equality Prims.bool Vale.Poly1305.Spec_s.modp FStar.Mul.op_Star Prims.op_Addition Prims.op_Subtraction Vale.Poly1305.Spec_s.poly1305_hash_blocks
module Vale.Poly1305.Spec_s

open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Types_s

[@"opaque_to_smt"]
let modp (x:int) : int =
  x % (pow2_128 * 4 - 5)

[@"opaque_to_smt"]
let mod2_128 (x:int) : int =
  x % pow2_128
val poly1305_hash_blocks (h pad r: int) (inp: (int -> nat128)) (k: nat) : int

    h: Prims.int ->
    pad: Prims.int ->
    r: Prims.int ->
    inp: (_: Prims.int -> Vale.Def.Words_s.nat128) ->
    k: Prims.nat
  -> Prims.int