val lemma_up_as_seq_index (#b:_) (h:HS.mem) (vb:UV.buffer b) (i:nat) : Lemma
  (requires i < length (UV.as_seq h vb) /\ UV.View?.n (UV.get_view vb) == 8) // TODO: generalize this beyond n = 8
  (ensures (
    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
    0 <= start /\ start + n <= length s0 /\
    index (UV.as_seq h vb) i == UV.View?.get v (slice s0 start (start + n))
  ))
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 lemma_up_as_seq_index (#b:_) (h:HS.mem) (vb:UV.buffer b) (i:nat) : Lemma
  (requires i < length (UV.as_seq h vb) /\ UV.View?.n (UV.get_view vb) == 8) // TODO: generalize this beyond n = 8
  (ensures (
    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
    0 <= start /\ start + n <= length s0 /\
    index (UV.as_seq h vb) i == UV.View?.get v (slice s0 start (start + n))
  ))
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)
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
FStar.Monotonic.HyperStack.mem LowStar.BufferView.Up.buffer Prims.nat Prims._assert Prims.eq2 FStar.Seq.Base.index LowStar.BufferView.Up.as_seq LowStar.BufferView.Up.__proj__View__item__get LowStar.BufferView.Up.buffer_src Prims.unit LowStar.BufferView.Up.as_seq_sel FStar.Seq.Base.seq FStar.Seq.Base.slice Prims.op_Addition Prims.int FStar.Mul.op_Star Prims.pos LowStar.BufferView.Up.__proj__View__item__n LowStar.BufferView.Up.view LowStar.BufferView.Up.get_view FStar.Seq.Properties.lseq LowStar.BufferView.Down.length LowStar.BufferView.Up.as_down_buffer LowStar.BufferView.Down.as_seq
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 = ()
val lemma_up_as_seq_index (#b:_) (h:HS.mem) (vb:UV.buffer b) (i:nat) : Lemma
  (requires i < length (UV.as_seq h vb) /\ UV.View?.n (UV.get_view vb) == 8) // TODO: generalize this beyond n = 8
  (ensures (
    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
    0 <= start /\ start + n <= length s0 /\
    index (UV.as_seq h vb) i == UV.View?.get v (slice s0 start (start + n))
  ))
h: FStar.Monotonic.HyperStack.mem -> vb: LowStar.BufferView.Up.buffer b -> i: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        i < FStar.Seq.Base.length (LowStar.BufferView.Up.as_seq h vb) /\
        View?.n (LowStar.BufferView.Up.get_view vb) == 8)
      (ensures
        (let s0 = LowStar.BufferView.Down.as_seq h (LowStar.BufferView.Up.as_down_buffer vb) in
          let v = LowStar.BufferView.Up.get_view vb in
          let n = View?.n v in
          let start = i * n in
          0 <= start /\ start + n <= FStar.Seq.Base.length s0 /\
          FStar.Seq.Base.index (LowStar.BufferView.Up.as_seq h vb) i ==
          View?.get v (FStar.Seq.Base.slice s0 start (start + n))))