val make_r (key_r: nat128) : nat128
let make_r (key_r:nat128) : nat128 =
  iand key_r 0x0ffffffc0ffffffc0ffffffc0fffffff
val make_r (key_r: nat128) : nat128
let make_r (key_r: nat128) : nat128 =
iand key_r 0x0ffffffc0ffffffc0ffffffc0fffffff
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
Vale.Def.Words_s.nat128 Vale.Def.Types_s.iand Vale.Def.Words_s.pow2_128
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)
val make_r (key_r: nat128) : nat128
key_r: Vale.Def.Words_s.nat128 -> Vale.Def.Words_s.nat128