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: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 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: 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 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.SHA.Simplify_Sha.fst.checked
Vale.SHA.SHA_helpers.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Interop.Views.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.SHA.Simplify_Sha.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.SHA.Simplify_Sha
open FStar.Mul

friend Vale.SHA.SHA_helpers

#set-options "--z3rlimit_factor 4"

open Vale.Def.Words_s
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq

#set-options "--z3rlimit 100"

open Vale.Lib.Seqs_s
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)