val shift_right64 (x amt: nat64) : nat64
val shift_right64 (x amt: nat64) : nat64
let shift_right64 (x:nat64) (amt:nat64) : nat64 = Vale.Def.Types_s.ishr x amt
module Vale.Poly1305.Math

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Poly1305.Spec_s

unfold let logand64 (x:nat64) (y:nat64) : nat64 = Vale.Def.Types_s.iand x y
unfold let logand128 (x:nat128) (y:nat128) : nat128 = Vale.Def.Types_s.iand x y
/
Vale.Poly1305.Spec_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Poly1305.Math.fsti
x: Vale.Def.Types_s.nat64 -> amt: Vale.Def.Types_s.nat64 -> Vale.Def.Types_s.nat64
Vale.Def.Types_s.nat64 Vale.Def.Types_s.ishr Vale.Def.Words_s.pow2_64
let shift_right64 (x amt: nat64) : nat64 =
  
Vale.Def.Types_s.ishr x amt