val lowerUpper192_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.Poly1305.Math.lowerUpper192 == Vale.Poly1305.Math.lowerUpper192_def)
let lowerUpper192_reveal = opaque_revealer (`%lowerUpper192) lowerUpper192 lowerUpper192_def
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
unfold let shift_left64 (x:nat64) (amt:nat64) : nat64 = Vale.Def.Types_s.ishl x amt
unfold let shift_right64 (x:nat64) (amt:nat64) : nat64 = Vale.Def.Types_s.ishr x amt

let lowerUpper128_def (l:nat64) (u:nat64) : nat128 =
  0x10000000000000000 * u + l
[@"opaque_to_smt"] let lowerUpper128 = opaque_make lowerUpper128_def
irreducible let lowerUpper128_reveal = opaque_revealer (`%lowerUpper128) lowerUpper128 lowerUpper128_def

let lowerUpper192_def (l:nat128) (u:nat64) : int =
  0x100000000000000000000000000000000 * u + l
/
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
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.Poly1305.Math.lowerUpper192 == Vale.Poly1305.Math.lowerUpper192_def)
Vale.Def.Opaque_s.opaque_revealer Vale.Def.Words_s.nat128 Vale.Def.Types_s.nat64 Prims.int Vale.Poly1305.Math.lowerUpper192 Vale.Poly1305.Math.lowerUpper192_def
let lowerUpper192_reveal =
  
opaque_revealer (`%lowerUpper192) lowerUpper192 lowerUpper192_def