val get16_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma (ensures Vale.Interop.Views.get16 == Vale.Interop.Views.get16_def)
let get16_reveal = opaque_revealer (`%get16) get16 get16_def
module Vale.Interop.Views

module DV = LowStar.BufferView.Down
module BV = LowStar.BufferView.Up
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Def.Opaque_s
open Vale.Lib.Seqs_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Seq
open Vale.Def.Words.Four_s

module U8 = FStar.UInt8

let get8_def (s:Seq.lseq U8.t 1) = Seq.index s 0
[@"opaque_to_smt"] let get8 = opaque_make get8_def
irreducible let get8_reveal = opaque_revealer (`%get8) get8 get8_def

let put8_def (x:U8.t) : GTot (Seq.lseq U8.t 1) =
  let contents (i:nat{i<1}) = x in
  Seq.init 1 contents
[@"opaque_to_smt"] let put8 = opaque_make put8_def
irreducible let put8_reveal = opaque_revealer (`%put8) put8 put8_def

val inverses8 (u:unit) : Lemma (DV.inverses get8 put8)

let up_view8 = inverses8 (); BV.View 1 get8 put8
let down_view8 = inverses8 (); DV.View 1 put8 get8

let get16_def (s:Seq.lseq U8.t 2) = UInt16.uint_to_t (
  U8.v (Seq.index s 0) +
  U8.v (Seq.index s 1) * 0x100
  )
/
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Interop.Views.fsti
_: Prims.unit
  -> FStar.Pervasives.Lemma (ensures Vale.Interop.Views.get16 == Vale.Interop.Views.get16_def)
Vale.Def.Opaque_s.opaque_revealer FStar.Seq.Properties.lseq FStar.UInt8.t FStar.UInt16.t Vale.Interop.Views.get16 Vale.Interop.Views.get16_def
let get16_reveal =
  
opaque_revealer (`%get16) get16 get16_def