val same_seq_downview8 (b:B.buffer UInt8.t) (h:HS.mem) : Lemma
  (DV.as_seq h (DV.mk_buffer_view b (Vale.Interop.Views.down_view8)) == B.as_seq h b)
let same_seq_downview8 b h =
  let db = DV.mk_buffer_view b (Vale.Interop.Views.down_view8) in
  DV.length_eq db;
  let s = B.as_seq h b in
  let sdb = DV.as_seq h db in
  let aux (i:nat{i < B.length b}) : Lemma (Seq.index sdb i == Seq.index s i)
    = DV.as_seq_sel h db i;
      DV.get_sel h db i;
      Vale.Interop.Views.put8_reveal ()
  in
  Classical.forall_intro aux;
  assert (Seq.equal s sdb)
val same_seq_downview8 (b:B.buffer UInt8.t) (h:HS.mem) : Lemma
  (DV.as_seq h (DV.mk_buffer_view b (Vale.Interop.Views.down_view8)) == B.as_seq h b)
let same_seq_downview8 b h =
let db = DV.mk_buffer_view b (Vale.Interop.Views.down_view8) in
DV.length_eq db;
let s = B.as_seq h b in
let sdb = DV.as_seq h db in
let aux (i: nat{i < B.length b}) : Lemma (Seq.index sdb i == Seq.index s i) =
  DV.as_seq_sel h db i;
  DV.get_sel h db i;
  Vale.Interop.Views.put8_reveal ()
in
Classical.forall_intro aux;
assert (Seq.equal s sdb)
Vale.Arch.BufferFriend.fst.checked
Vale.Wrapper.X64.Poly.fsti.checked Vale.Poly1305.Util.fsti.checked Vale.Lib.Seqs_s.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked prims.fst.checked LowStar.BufferView.Up.fst.checked Lib.RawIntTypes.fst.checked Lib.IntTypes.fst.checked Lib.ByteSequence.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Arch.BufferFriend.fst
LowStar.Buffer.buffer FStar.UInt8.t FStar.Monotonic.HyperStack.mem Prims._assert FStar.Seq.Base.equal Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Vale.Interop.Views.put8_reveal LowStar.BufferView.Down.get_sel LowStar.BufferView.Down.as_seq_sel FStar.Seq.Properties.lseq LowStar.BufferView.Down.length LowStar.BufferView.Down.as_seq FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq LowStar.BufferView.Down.length_eq LowStar.BufferView.Down.buffer LowStar.BufferView.Down.mk_buffer_view Vale.Interop.Views.down_view8
module Vale.Arch.BufferFriend
open FStar.Mul
friend Lib.IntTypes
friend Lib.RawIntTypes
friend Lib.ByteSequence
friend LowStar.BufferView.Up
friend FStar.Endianness

module PU = Vale.Poly1305.Util
module IT = Vale.Interop.Types
module PS = Vale.Wrapper.X64.Poly
module BS = Lib.ByteSequence
module Raw = Lib.RawIntTypes

unfold let (.[]) = index

let to_bytes s = s
let of_bytes b = b

let lemma_to_bytes_slice b i j = ()
let lemma_of_bytes_slice b i j = ()

let lemma_up_as_seq_index #b h vb i =
  let s0 = DV.as_seq h (UV.as_down_buffer vb) in
  let v = UV.get_view vb in
  let n = UV.View?.n v in
  let start = i * n in
  let s_i = slice s0 start (start + n) in
  UV.as_seq_sel h vb i;
  assert (index (UV.as_seq h vb) i == UV.View?.get v s_i)
val same_seq_downview8 (b:B.buffer UInt8.t) (h:HS.mem) : Lemma
  (DV.as_seq h (DV.mk_buffer_view b (Vale.Interop.Views.down_view8)) == B.as_seq h b)
b: LowStar.Buffer.buffer FStar.UInt8.t -> h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
    (ensures
      LowStar.BufferView.Down.as_seq h
        (LowStar.BufferView.Down.mk_buffer_view b Vale.Interop.Views.down_view8) ==
      LowStar.Monotonic.Buffer.as_seq h b)