val poly1305_hash_all (h: int) (key_r key_s: nat128) (inp: (int -> nat128)) (len: nat) : int
let poly1305_hash_all (h:int) (key_r key_s:nat128) (inp:int -> nat128) (len:nat) : int =
  let nBlocks = len / 16 in
  let nExtra = len % 16 in
  let hBlocks = poly1305_hash_blocks h pow2_128 (make_r key_r) inp nBlocks in
  if nExtra = 0 then
    mod2_128 (hBlocks + key_s)
  else
    let padLast = pow2 (nExtra * 8) in
    let hLast = modp ((hBlocks + padLast + inp nBlocks % padLast) * (make_r key_r)) in
    mod2_128 (hLast + key_s)
val poly1305_hash_all (h: int) (key_r key_s: nat128) (inp: (int -> nat128)) (len: nat) : int
let poly1305_hash_all (h: int) (key_r key_s: nat128) (inp: (int -> nat128)) (len: nat) : int =
let nBlocks = len / 16 in
let nExtra = len % 16 in
let hBlocks = poly1305_hash_blocks h pow2_128 (make_r key_r) inp nBlocks in
if nExtra = 0
then mod2_128 (hBlocks + key_s)
else
  let padLast = pow2 (nExtra * 8) in
  let hLast = modp ((hBlocks + padLast + inp nBlocks % padLast) * (make_r key_r)) in
  mod2_128 (hLast + key_s)
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 Vale.Poly1305.Spec_s.mod2_128 Prims.op_Addition Prims.bool Vale.Poly1305.Spec_s.modp FStar.Mul.op_Star Prims.op_Modulus Vale.Poly1305.Spec_s.make_r Prims.pos Prims.pow2 Vale.Poly1305.Spec_s.poly1305_hash_blocks Vale.Def.Words_s.pow2_128 Prims.op_Division
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

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)

let make_r (key_r:nat128) : nat128 =
  iand key_r 0x0ffffffc0ffffffc0ffffffc0fffffff
val poly1305_hash_all (h: int) (key_r key_s: nat128) (inp: (int -> nat128)) (len: nat) : int

    h: Prims.int ->
    key_r: Vale.Def.Words_s.nat128 ->
    key_s: Vale.Def.Words_s.nat128 ->
    inp: (_: Prims.int -> Vale.Def.Words_s.nat128) ->
    len: Prims.nat
  -> Prims.int