let get_downview
  (#src:base_typ)
  (#rrel #rel:MB.srel (base_typ_as_type src))
  (b:MB.mbuffer (base_typ_as_type src) rrel rel) =
  DV.mk_buffer_view b (down_view src)
let get_downview
      (#src: base_typ)
      (#rrel #rel: MB.srel (base_typ_as_type src))
      (b: MB.mbuffer (base_typ_as_type src) rrel rel)
     =
DV.mk_buffer_view b (down_view src)
Vale.Interop.Types.fst.checked
Vale.Interop.Views.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Vale.Interop.Types.fst
Vale.Arch.HeapTypes_s.base_typ LowStar.Monotonic.Buffer.srel Vale.Interop.Types.base_typ_as_type LowStar.Monotonic.Buffer.mbuffer LowStar.BufferView.Down.mk_buffer_view FStar.UInt8.t Vale.Interop.Types.down_view LowStar.BufferView.Down.buffer
module Vale.Interop.Types
open FStar.Mul
include Vale.Arch.HeapTypes_s
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module MB = LowStar.Monotonic.Buffer
module DV = LowStar.BufferView.Down
module W = Vale.Def.Words_s
module L = FStar.List.Tot

[@__reduce__]
let base_typ_as_type (t:base_typ) : eqtype =
  let open W in
  let open Vale.Def.Types_s in
  match t with
  | TUInt8 -> UInt8.t
  | TUInt16 -> UInt16.t
  | TUInt32 -> UInt32.t
  | TUInt64 -> UInt64.t
  | TUInt128 -> quad32

[@__reduce__]
unfold // without the unfold, "% view_n t" leads to very slow Z3 performance
let view_n_unfold (t:base_typ) : pos =
  match t with
  | TUInt8 -> 1
  | TUInt16 -> 2
  | TUInt32 -> 4
  | TUInt64 -> 8
  | TUInt128 -> 16

let view_n (t:base_typ) : pos = view_n_unfold t

[@__reduce__]
let down_view (t:base_typ) : DV.view (base_typ_as_type t) UInt8.t = match t with
  | TUInt8 -> Vale.Interop.Views.down_view8
  | TUInt16 -> Vale.Interop.Views.down_view16
  | TUInt32 -> Vale.Interop.Views.down_view32
  | TUInt64 -> Vale.Interop.Views.down_view64
  | TUInt128 -> Vale.Interop.Views.down_view128

let b8_preorder (writeable:bool) (a:Type0) : MB.srel a =
  match writeable with
  | true -> B.trivial_preorder a
  | false -> IB.immutable_preorder a

[@__reduce__]
noeq
type b8 =
| Buffer:
  #src:base_typ ->
  writeable:bool ->
  bsrc:MB.mbuffer (base_typ_as_type src)
    (b8_preorder writeable (base_typ_as_type src))
    (b8_preorder writeable (base_typ_as_type src)) ->
  b8

let disjoint_addr addr1 length1 addr2 length2 =
  (* The first buffer is completely before the second, or the opposite *)
  addr1 + length1 < addr2 ||
  addr2 + length2 < addr1

let get_downview
  (#src:base_typ)
  (#rrel #rel:MB.srel (base_typ_as_type src))
val get_downview : b: LowStar.Monotonic.Buffer.mbuffer (Vale.Interop.Types.base_typ_as_type src) rrel rel
  -> Prims.GTot (LowStar.BufferView.Down.buffer FStar.UInt8.t)
b: LowStar.Monotonic.Buffer.mbuffer (Vale.Interop.Types.base_typ_as_type src) rrel rel
  -> Prims.GTot (LowStar.BufferView.Down.buffer FStar.UInt8.t)