val modp (x: int) : int
let modp (x:int) : int =
  x % (pow2_128 * 4 - 5)
val modp (x: int) : int
let modp (x: int) : int =
x % (pow2_128 * 4 - 5)
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 Prims.op_Modulus Prims.op_Subtraction FStar.Mul.op_Star 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"]
val modp (x: int) : int
x: Prims.int -> Prims.int