val b32slice (b: bytes) (s e: U32.t)
    : Pure bytes
      (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
      (ensures (fun res -> reveal res == Seq.slice (reveal b) (U32.v s) (U32.v e)))
let b32slice
  (b: bytes)
  (s: U32.t)
  (e: U32.t)
: Pure bytes
  (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
  (ensures (fun res -> reveal res == Seq.slice (reveal b) (U32.v s) (U32.v e)))
= slice b s e
val b32slice (b: bytes) (s e: U32.t)
    : Pure bytes
      (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
      (ensures (fun res -> reveal res == Seq.slice (reveal b) (U32.v s) (U32.v e)))
let b32slice (b: bytes) (s e: U32.t)
    : Pure bytes
      (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
      (ensures (fun res -> reveal res == Seq.slice (reveal b) (U32.v s) (U32.v e))) =
slice b s e
LowParse.Bytes32.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
LowParse.Bytes32.fst
FStar.Bytes.bytes FStar.UInt32.t FStar.Bytes.slice Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v FStar.Bytes.length Prims.eq2 FStar.Seq.Base.seq FStar.Bytes.byte FStar.Bytes.reveal FStar.Seq.Base.slice
module LowParse.Bytes32
include FStar.Bytes

module U32 = FStar.UInt32

(* TODO: move to FStar.Bytes *)

inline_for_extraction
let b32slice
  (b: bytes)
  (s: U32.t)
  (e: U32.t)
: Pure bytes
  (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
val b32slice (b: bytes) (s e: U32.t)
    : Pure bytes
      (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
      (ensures (fun res -> reveal res == Seq.slice (reveal b) (U32.v s) (U32.v e)))
b: FStar.Bytes.bytes -> s: FStar.UInt32.t -> e: FStar.UInt32.t -> Prims.Pure FStar.Bytes.bytes