val u256 : Type0
let u256 = b:B.buffer UInt64.t{B.length b == 4}
module Vale.Inline.X64.Fmul_inline

open Vale.X64.CPU_Features_s
open FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
open Vale.Curve25519.Fast_defs
open FStar.Mul
/
Vale.X64.CPU_Features_s.fst.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Vale.Inline.X64.Fmul_inline.fsti
Type0
LowStar.Buffer.buffer FStar.UInt64.t Prims.eq2 Prims.int LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder
let u256 =
  
b: B.buffer UInt64.t {B.length b == 4}