val as_nat (b: B.buffer UInt64.t {B.length b == 4}) (h: HS.mem) : GTot nat
val as_nat (b: B.buffer UInt64.t {B.length b == 4}) (h: HS.mem) : GTot nat
let as_nat (b:B.buffer UInt64.t{B.length b == 4}) (h:HS.mem) : GTot nat =
  let s = B.as_seq h b in
  let s0 = UInt64.v (Seq.index s 0) in
  let s1 = UInt64.v (Seq.index s 1) in
  let s2 = UInt64.v (Seq.index s 2) in
  let s3 = UInt64.v (Seq.index s 3) in
  pow2_four s0 s1 s2 s3
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

unfold
let u256 = b:B.buffer UInt64.t{B.length b == 4}
unfold
let u512 = b:B.buffer UInt64.t{B.length b == 8}
unfold
let u1024 = b:B.buffer UInt64.t{B.length b == 16}
/
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

    b: LowStar.Buffer.buffer FStar.UInt64.t {LowStar.Monotonic.Buffer.length b == 4} ->
    h: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.nat
LowStar.Buffer.buffer FStar.UInt64.t Prims.eq2 Prims.int LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder FStar.Monotonic.HyperStack.mem Vale.Curve25519.Fast_defs.pow2_four FStar.UInt.uint_t FStar.UInt64.v FStar.Seq.Base.index FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq Prims.nat
let as_nat (b: B.buffer UInt64.t {B.length b == 4}) (h: HS.mem) : GTot nat =
  
let s = B.as_seq h b in
let s0 = UInt64.v (Seq.index s 0) in
let s1 = UInt64.v (Seq.index s 1) in
let s2 = UInt64.v (Seq.index s 2) in
let s3 = UInt64.v (Seq.index s 3) in
pow2_four s0 s1 s2 s3