let lbytes len = lbuffer uint8 len
let lbytes len =
lbuffer uint8 len
Hacl.Impl.K256.Verify.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.K256.Scalar.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Qinv.fst.checked Hacl.Impl.K256.PointMul.fsti.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.K256.GLV.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.K256.Verify.fst
Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8
module Hacl.Impl.K256.Verify

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST

module S = Spec.K256
module KL = Spec.K256.Lemmas

open Hacl.K256.Field
open Hacl.Impl.K256.Point
open Hacl.Impl.K256.PointMul
open Hacl.Impl.K256.GLV

module QA = Hacl.K256.Scalar
module QI = Hacl.Impl.K256.Qinv
module BL = Hacl.Spec.K256.Field52.Lemmas
module BSeq = Lib.ByteSequence

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val lbytes : len: Lib.IntTypes.size_t -> Type0
len: Lib.IntTypes.size_t -> Type0