val put8_def (x: U8.t) : GTot (Seq.lseq U8.t 1)
let put8_def (x:U8.t) : GTot (Seq.lseq U8.t 1) =
  let contents (i:nat{i<1}) = x in
  Seq.init 1 contents
val put8_def (x: U8.t) : GTot (Seq.lseq U8.t 1)
let put8_def (x: U8.t) : GTot (Seq.lseq U8.t 1) =
let contents (i: nat{i < 1}) = x in
Seq.init 1 contents
Vale.Interop.Views.fsti.checked
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
FStar.UInt8.t FStar.Seq.Base.init Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Properties.lseq
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
val put8_def (x: U8.t) : GTot (Seq.lseq U8.t 1)
x: FStar.UInt8.t -> Prims.GTot (FStar.Seq.Properties.lseq FStar.UInt8.t 1)