val lemma_seq_nat8_le_seq_quad32_to_bytes_uint32
  (b:buf_t TUInt8 TUInt128)
  (h:HS.mem) : Lemma
  (requires True )
  (ensures (
  DV.length_eq (get_downview b);
  Seq.equal
    (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h (UV.mk_buffer (get_downview b) Vale.Interop.Views.up_view128))))
    (B.as_seq h b)))
let lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b h =
  let s_init = B.as_seq h b in
  let db = get_downview b in
  DV.length_eq db;
  assert (Seq.length s_init == B.length b);
  let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
  let s = UV.as_seq h ub in
  let s' = le_seq_quad32_to_bytes s in
  le_seq_quad32_to_bytes_reveal ();
  //definition given by reveal_opaque
  assert (s' == seq_four_to_seq_LE (seq_map (nat_to_four 8) (seq_four_to_seq_LE s)));
  let s_f = seq_nat8_to_seq_uint8 s' in
  UV.length_eq ub;
  let aux (i:nat{i < Seq.length s_f}) : Lemma (Seq.index s_init i == Seq.index s_f i) =
    reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
    reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
    reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat32);
    let i' = i/16 in
    UV.as_seq_sel h ub i';
    UV.get_sel h ub i';
    same_seq_downview8 b h;
    assert (Seq.index s i' == Vale.Interop.Views.get128 (Seq.slice s_init (i' * 16) (i' * 16 + 16)));
    Vale.Interop.Views.get128_reveal ();
    let s_slice = seq_uint8_to_seq_nat8 (Seq.slice s_init (i' * 16) (i' * 16 +16)) in
    le_bytes_to_quad32_reveal ();
    assert (seq_to_four_LE (seq_map (four_to_nat 8) (seq_to_seq_four_LE s_slice)) ==
            Seq.index s i')
  in Classical.forall_intro aux;
  assert (Seq.equal s_f s_init)
val lemma_seq_nat8_le_seq_quad32_to_bytes_uint32
  (b:buf_t TUInt8 TUInt128)
  (h:HS.mem) : Lemma
  (requires True )
  (ensures (
  DV.length_eq (get_downview b);
  Seq.equal
    (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h (UV.mk_buffer (get_downview b) Vale.Interop.Views.up_view128))))
    (B.as_seq h b)))
let lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b h =
let s_init = B.as_seq h b in
let db = get_downview b in
DV.length_eq db;
assert (Seq.length s_init == B.length b);
let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
let s = UV.as_seq h ub in
let s' = le_seq_quad32_to_bytes s in
le_seq_quad32_to_bytes_reveal ();
assert (s' == seq_four_to_seq_LE (seq_map (nat_to_four 8) (seq_four_to_seq_LE s)));
let s_f = seq_nat8_to_seq_uint8 s' in
UV.length_eq ub;
let aux (i: nat{i < Seq.length s_f}) : Lemma (Seq.index s_init i == Seq.index s_f i) =
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat32);
  let i' = i / 16 in
  UV.as_seq_sel h ub i';
  UV.get_sel h ub i';
  same_seq_downview8 b h;
  assert (Seq.index s i' == Vale.Interop.Views.get128 (Seq.slice s_init (i' * 16) (i' * 16 + 16)));
  Vale.Interop.Views.get128_reveal ();
  let s_slice = seq_uint8_to_seq_nat8 (Seq.slice s_init (i' * 16) (i' * 16 + 16)) in
  le_bytes_to_quad32_reveal ();
  assert (seq_to_four_LE (seq_map (four_to_nat 8) (seq_to_seq_four_LE s_slice)) == Seq.index s i')
in
Classical.forall_intro aux;
assert (Seq.equal s_f s_init)
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
Vale.Interop.Base.buf_t Vale.Arch.HeapTypes_s.TUInt8 Vale.Arch.HeapTypes_s.TUInt128 FStar.Monotonic.HyperStack.mem Prims._assert FStar.Seq.Base.equal FStar.UInt8.t Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.eq2 FStar.Seq.Base.index Vale.Interop.Types.base_typ_as_type Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Vale.Def.Words_s.four Vale.Def.Types_s.nat32 Vale.Def.Words.Seq_s.seq_to_four_LE Vale.Def.Words_s.natN Prims.pow2 FStar.Mul.op_Star Vale.Lib.Seqs_s.seq_map Vale.Def.Words_s.nat8 Vale.Def.Words.Four_s.four_to_nat Vale.Def.Words.Seq_s.seq_to_seq_four_LE Vale.Def.Types_s.quad32 Vale.Def.Types_s.le_bytes_to_quad32_reveal FStar.Seq.Base.seq Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 FStar.Seq.Base.slice Prims.op_Addition Vale.Interop.Views.get128_reveal Vale.Interop.Views.get128 Vale.SHA.Simplify_Sha.same_seq_downview8 LowStar.BufferView.Up.get_sel LowStar.BufferView.Up.as_seq_sel Prims.int Prims.op_Division FStar.Pervasives.reveal_opaque Vale.Def.Words_s.nat32 Vale.Def.Words.Seq_s.seq_four_to_seq_LE Prims.op_Modulus LowStar.BufferView.Up.length_eq Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 Vale.Def.Words.Four_s.nat_to_four Vale.Def.Types_s.le_seq_quad32_to_bytes_reveal Vale.Def.Types_s.le_seq_quad32_to_bytes FStar.Seq.Properties.lseq LowStar.BufferView.Up.length LowStar.BufferView.Up.as_seq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Vale.Interop.Views.up_view128 LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder LowStar.BufferView.Down.length_eq LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview LowStar.Monotonic.Buffer.as_seq
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

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 lemma_seq_nat8_le_seq_quad32_to_bytes_uint32
  (b:buf_t TUInt8 TUInt128)
  (h:HS.mem) : Lemma
  (requires True )
  (ensures (
  DV.length_eq (get_downview b);
  Seq.equal
    (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h (UV.mk_buffer (get_downview b) Vale.Interop.Views.up_view128))))
    (B.as_seq h b)))

    b: Vale.Interop.Base.buf_t Vale.Arch.HeapTypes_s.TUInt8 Vale.Arch.HeapTypes_s.TUInt128 ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
    (ensures
      ([@@ FStar.Pervasives.inline_let ]let _ =
          LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview b)
        in
        FStar.Seq.Base.equal (Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 (Vale.Def.Types_s.le_seq_quad32_to_bytes
                  (LowStar.BufferView.Up.as_seq h
                      (LowStar.BufferView.Up.mk_buffer (Vale.Interop.Types.get_downview b)
                          Vale.Interop.Views.up_view128))))
          (LowStar.Monotonic.Buffer.as_seq h b)))