val logand128 (x y: nat128) : nat128
val logand128 (x y: nat128) : nat128
let logand128 (x:nat128) (y:nat128) : nat128 = Vale.Def.Types_s.iand x y
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
/
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.Words_s.nat128 -> y: Vale.Def.Words_s.nat128 -> Vale.Def.Words_s.nat128
Vale.Def.Words_s.nat128 Vale.Def.Types_s.iand Vale.Def.Words_s.pow2_128
let logand128 (x y: nat128) : nat128 =
  
Vale.Def.Types_s.iand x y