val loc_buffer_from_to_if (#t: Type) (b: B.buffer t) (from to: U32.t) : GTot B.loc
val loc_buffer_from_to_if (#t: Type) (b: B.buffer t) (from to: U32.t) : GTot B.loc
let loc_buffer_from_to_if
  (#t: Type)
  (b: B.buffer t)
  (from to: U32.t)
: GTot B.loc
= if U32.v to < U32.v from || U32.v to > B.length b
  then B.loc_none
  else B.loc_buffer (B.gsub b from (to `U32.sub` from))
module QUIC.Secret.Buffer

module Secret = QUIC.Secret.Int
module B = LowStar.Buffer
module U8 = FStar.UInt8
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Seq = QUIC.Secret.Seq
module Ghost = FStar.Ghost

module U32 = FStar.UInt32

#set-options "--z3rlimit 32"
/
QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
QUIC.Secret.Buffer.fsti
b: LowStar.Buffer.buffer t -> from: FStar.UInt32.t -> to: FStar.UInt32.t
  -> Prims.GTot LowStar.Monotonic.Buffer.loc
LowStar.Buffer.buffer FStar.UInt32.t Prims.op_BarBar Prims.op_LessThan FStar.UInt32.v Prims.op_GreaterThan LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.loc_none Prims.bool LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.gsub FStar.UInt32.sub LowStar.Monotonic.Buffer.loc
let loc_buffer_from_to_if (#t: Type) (b: B.buffer t) (from to: U32.t) : GTot B.loc =
  
if U32.v to < U32.v from || U32.v to > B.length b
then B.loc_none
else B.loc_buffer (B.gsub b from (to `U32.sub` from))