val lemma_uv_equal (#src #dst: Type) (view: UV.view src dst) (b: DV.buffer src) (h0 h1: HS.mem)
    : Lemma (requires (DV.length b % UV.View?.n view == 0 /\ DV.as_seq h0 b == DV.as_seq h1 b))
      (ensures
        (let bv = UV.mk_buffer b view in
          UV.as_seq h0 bv == UV.as_seq h1 bv))
      [SMTPat (UV.as_seq h0 (UV.mk_buffer b view)); SMTPat (UV.as_seq h1 (UV.mk_buffer b view))]
let lemma_uv_equal
  (#src:Type) (#dst:Type)
  (view:UV.view src dst) (b:DV.buffer src) (h0 h1:HS.mem)
  :Lemma (requires (DV.length b % UV.View?.n view == 0 /\ DV.as_seq h0 b == DV.as_seq h1 b))
         (ensures  (let bv = UV.mk_buffer b view in UV.as_seq h0 bv == UV.as_seq h1 bv))
   [SMTPat (UV.as_seq h0 (UV.mk_buffer b view)); SMTPat (UV.as_seq h1 (UV.mk_buffer b view))]
  = let uv = UV.mk_buffer b view in
    let s0 = UV.as_seq h0 uv in
    let s1 = UV.as_seq h1 uv in
    let aux (i:nat{i < UV.length uv}) : Lemma (Seq.index s0 i == Seq.index s1 i) =
      UV.as_seq_sel h0 uv i;
      UV.as_seq_sel h1 uv i;
      UV.get_sel h0 uv i;
      UV.get_sel h1 uv i
    in Classical.forall_intro aux;
    Seq.lemma_eq_intro s0 s1
val lemma_uv_equal (#src #dst: Type) (view: UV.view src dst) (b: DV.buffer src) (h0 h1: HS.mem)
    : Lemma (requires (DV.length b % UV.View?.n view == 0 /\ DV.as_seq h0 b == DV.as_seq h1 b))
      (ensures
        (let bv = UV.mk_buffer b view in
          UV.as_seq h0 bv == UV.as_seq h1 bv))
      [SMTPat (UV.as_seq h0 (UV.mk_buffer b view)); SMTPat (UV.as_seq h1 (UV.mk_buffer b view))]
let lemma_uv_equal (#src #dst: Type) (view: UV.view src dst) (b: DV.buffer src) (h0 h1: HS.mem)
    : Lemma (requires (DV.length b % UV.View?.n view == 0 /\ DV.as_seq h0 b == DV.as_seq h1 b))
      (ensures
        (let bv = UV.mk_buffer b view in
          UV.as_seq h0 bv == UV.as_seq h1 bv))
      [SMTPat (UV.as_seq h0 (UV.mk_buffer b view)); SMTPat (UV.as_seq h1 (UV.mk_buffer b view))] =
let uv = UV.mk_buffer b view in
let s0 = UV.as_seq h0 uv in
let s1 = UV.as_seq h1 uv in
let aux (i: nat{i < UV.length uv}) : Lemma (Seq.index s0 i == Seq.index s1 i) =
  UV.as_seq_sel h0 uv i;
  UV.as_seq_sel h1 uv i;
  UV.get_sel h0 uv i;
  UV.get_sel h1 uv i
in
Classical.forall_intro aux;
Seq.lemma_eq_intro s0 s1
Vale.Lib.BufferViewHelpers.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.BufferView.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
Vale.Lib.BufferViewHelpers.fst
LowStar.BufferView.Up.view LowStar.BufferView.Down.buffer FStar.Monotonic.HyperStack.mem FStar.Seq.Base.lemma_eq_intro Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan LowStar.BufferView.Up.length Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern LowStar.BufferView.Up.get_sel LowStar.BufferView.Up.as_seq_sel FStar.Seq.Properties.lseq LowStar.BufferView.Up.as_seq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Prims.l_and Prims.int Prims.op_Modulus LowStar.BufferView.Down.length LowStar.BufferView.Up.__proj__View__item__n LowStar.BufferView.Down.as_seq Prims.Cons FStar.Pervasives.smt_pat
module Vale.Lib.BufferViewHelpers
open FStar.Mul

module MB = LowStar.Monotonic.Buffer
module BV = LowStar.BufferView
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
open FStar.HyperStack.ST

open LowStar.Modifies
open LowStar.ModifiesPat

let lemma_dv_equal
  (#src:Type)
  (#rel #rrel:MB.srel src)
  (#dst:Type)
  (view:DV.view src dst)
  (b:MB.mbuffer src rel rrel)
  (h0 h1:HS.mem) : Lemma
  (requires MB.as_seq h0 b == MB.as_seq h1 b)
  (ensures (let dv = DV.mk_buffer_view b view in
    DV.as_seq h0 dv == DV.as_seq h1 dv)) =
    let dv = DV.mk_buffer_view b view in
    let s0 = DV.as_seq h0 dv in
    let s1 = DV.as_seq h1 dv in
    let aux (i:nat{i < DV.length dv}) : Lemma (Seq.index s0 i == Seq.index s1 i) =
      DV.as_seq_sel h0 dv i;
      DV.as_seq_sel h1 dv i;
      DV.get_sel h0 dv i;
      DV.get_sel h1 dv i
    in Classical.forall_intro aux;
    Seq.lemma_eq_intro s0 s1

let lemma_uv_equal
  (#src:Type) (#dst:Type)
  (view:UV.view src dst) (b:DV.buffer src) (h0 h1:HS.mem)
  :Lemma (requires (DV.length b % UV.View?.n view == 0 /\ DV.as_seq h0 b == DV.as_seq h1 b))
         (ensures  (let bv = UV.mk_buffer b view in UV.as_seq h0 bv == UV.as_seq h1 bv))
val lemma_uv_equal (#src #dst: Type) (view: UV.view src dst) (b: DV.buffer src) (h0 h1: HS.mem)
    : Lemma (requires (DV.length b % UV.View?.n view == 0 /\ DV.as_seq h0 b == DV.as_seq h1 b))
      (ensures
        (let bv = UV.mk_buffer b view in
          UV.as_seq h0 bv == UV.as_seq h1 bv))
      [SMTPat (UV.as_seq h0 (UV.mk_buffer b view)); SMTPat (UV.as_seq h1 (UV.mk_buffer b view))]

    view: LowStar.BufferView.Up.view src dst ->
    b: LowStar.BufferView.Down.buffer src ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        LowStar.BufferView.Down.length b % View?.n view == 0 /\
        LowStar.BufferView.Down.as_seq h0 b == LowStar.BufferView.Down.as_seq h1 b)
      (ensures
        (let bv = LowStar.BufferView.Up.mk_buffer b view in
          LowStar.BufferView.Up.as_seq h0 bv == LowStar.BufferView.Up.as_seq h1 bv))
      [
        SMTPat (LowStar.BufferView.Up.as_seq h0 (LowStar.BufferView.Up.mk_buffer b view));
        SMTPat (LowStar.BufferView.Up.as_seq h1 (LowStar.BufferView.Up.mk_buffer b view))
      ]