val as_normal_t (#a: Type) (x: a) : normal a
let as_normal_t (#a:Type) (x:a) : normal a = x
val as_normal_t (#a: Type) (x: a) : normal a
let as_normal_t (#a: Type) (x: a) : normal a =
x
Vale.Stdcalls.X64.Poly.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Poly1305.X64.fsti.checked Vale.Poly1305.Math.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Def.Types_s.fst.checked Vale.AsLowStar.Wrapper.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Vale.Stdcalls.X64.Poly.fsti
Vale.Interop.Base.normal
module Vale.Stdcalls.X64.Poly
open FStar.Mul

val z3rlimit_hack (x:nat) : squash (x < x + x + 1)
#reset-options "--z3rlimit 50"

open FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module DV = LowStar.BufferView.Down
open Vale.Def.Types_s

open Vale.Interop.Base
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module ME = Vale.X64.Memory
module V = Vale.X64.Decls
module IA = Vale.Interop.Assumptions
module W = Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters
module VS = Vale.X64.State
module MS = Vale.X64.Machine_s

module PO = Vale.Poly1305.X64
open Vale.Poly1305.Math

let uint64 = UInt64.t

(* A little utility to trigger normalization in types *)
noextract
let as_t (#a:Type) (x:normal a) : a = x
val as_normal_t (#a: Type) (x: a) : normal a
x: a -> Vale.Interop.Base.normal a