val down_view (t: base_typ) : DV.view (base_typ_as_type t) UInt8.t
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
val down_view (t: base_typ) : DV.view (base_typ_as_type t) UInt8.t
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
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 Vale.Interop.Views.down_view8 Vale.Interop.Views.down_view16 Vale.Interop.Views.down_view32 Vale.Interop.Views.down_view64 Vale.Interop.Views.down_view128 LowStar.BufferView.Down.view Vale.Interop.Types.base_typ_as_type FStar.UInt8.t
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
val down_view (t: base_typ) : DV.view (base_typ_as_type t) UInt8.t
t: Vale.Arch.HeapTypes_s.base_typ
  -> LowStar.BufferView.Down.view (Vale.Interop.Types.base_typ_as_type t) FStar.UInt8.t