val simplify_le_bytes_to_hash_uint32
  (b:buf_t TUInt32 TUInt128)
  (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 8)
  (ensures
  (reveal_word();
  DV.length_eq (get_downview b);
  Seq.equal
    (le_bytes_to_hash (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 simplify_le_bytes_to_hash_uint32 b h =
  let db = get_downview b in
  let down_s = DV.as_seq h db in
  DV.length_eq db;
  let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
  UV.length_eq ub;
  let s_init = B.as_seq h b in
  let s = UV.as_seq h ub in
  let s' = le_seq_quad32_to_bytes s in
  let sf = le_bytes_to_hash s' in

  // Since Seq.length s' == 32, we have the following by def of le_bytes_to_hash
  assert (sf == seq_map nat32_to_word (seq_nat8_to_seq_nat32_LE s'));
  le_seq_quad32_to_bytes_reveal ();
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat32);
  // After revealing the previous def, the seq_nat8_to_seq_nat32_LE_to_nat8 simplifies
  assert (sf == seq_map nat32_to_word (seq_four_to_seq_LE s));

  let aux (i:nat {i < Seq.length sf}) : Lemma (Seq.index sf i = Seq.index s_init i)
    = let i' = i/4 in
      UV.as_seq_sel h ub i';
      UV.get_sel h ub i';
      reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);

      Vale.Interop.Views.get128_reveal ();
      le_bytes_to_quad32_reveal ();
      // Revealing these definitions gives us the following
      assert (Vale.Interop.Views.get128 (Seq.slice (DV.as_seq h db)
             (i' * 16) (i' * 16 + 16))
             == Mkfour
(four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                               (Seq.slice down_s (i'*16) (i'*16+4)))))
                               (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                               (Seq.slice down_s (i'*16+4) (i'*16+8)))))
                               (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                               (Seq.slice down_s (i'*16+8) (i'*16+12)))))
                               (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                               (Seq.slice down_s (i'*16+12) (i'*16+16))))));

      // Gives us that Seq.slice down_s (i*16) (i*16+4) == Vale.Interop.Views.put32 (Seq.index s (4*i)) and same for other indices
      DV.put_sel h db (4*4*i');
      DV.put_sel h db (4*(4*i'+1));
      DV.put_sel h db (4*(4*i'+2));
      DV.put_sel h db (4*(4*i'+3));

      Vale.Interop.Views.put32_reveal ();

      // Apply the only lemmas without SMTPat to simplify the following patterns:
      // assert (four_to_nat 8 (
      //              seq_to_four_LE (
      //                seq_uint8_to_seq_nat8 (
      //                seq_nat8_to_seq_uint8 (
      //              four_to_seq_LE (
      //         nat_to_four 8 (UInt32.v (Seq.index s (4*i)))))))) ==
      //         UInt32.v (Seq.index s (4*i)));
      seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4*i'))));
      seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4*i'+1))));
      seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4*i'+2))));
      seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4*i'+3))));

      Vale.Interop.Views.get32_128_reveal ();
      assert (UInt32.uint_to_t (four_select (Seq.index s i') (i%4)) ==
        Seq.index (Seq.slice (B.as_seq h b) (i' * 4) (i'*4+4)) (i%4));
      assert (Seq.index (B.as_seq h b) i ==
        Seq.index (Seq.slice (B.as_seq h b) (i' * 4) (i'*4+4)) (i%4))
  in Classical.forall_intro aux;
  assert (Seq.equal sf s_init)
val simplify_le_bytes_to_hash_uint32
  (b:buf_t TUInt32 TUInt128)
  (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 8)
  (ensures
  (reveal_word();
  DV.length_eq (get_downview b);
  Seq.equal
    (le_bytes_to_hash (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 simplify_le_bytes_to_hash_uint32 b h =
let db = get_downview b in
let down_s = DV.as_seq h db in
DV.length_eq db;
let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
UV.length_eq ub;
let s_init = B.as_seq h b in
let s = UV.as_seq h ub in
let s' = le_seq_quad32_to_bytes s in
let sf = le_bytes_to_hash s' in
assert (sf == seq_map nat32_to_word (seq_nat8_to_seq_nat32_LE s'));
le_seq_quad32_to_bytes_reveal ();
reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat32);
assert (sf == seq_map nat32_to_word (seq_four_to_seq_LE s));
let aux (i: nat{i < Seq.length sf}) : Lemma (Seq.index sf i = Seq.index s_init i) =
  let i' = i / 4 in
  UV.as_seq_sel h ub i';
  UV.get_sel h ub i';
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  Vale.Interop.Views.get128_reveal ();
  le_bytes_to_quad32_reveal ();
  assert (Vale.Interop.Views.get128 (Seq.slice (DV.as_seq h db) (i' * 16) (i' * 16 + 16)) ==
      Mkfour
        (four_to_nat 8
            (seq_to_four_LE (seq_uint8_to_seq_nat8 (Seq.slice down_s (i' * 16) (i' * 16 + 4)))))
        (four_to_nat 8
            (seq_to_four_LE (seq_uint8_to_seq_nat8 (Seq.slice down_s (i' * 16 + 4) (i' * 16 + 8)))))
        (four_to_nat 8
            (seq_to_four_LE (seq_uint8_to_seq_nat8 (Seq.slice down_s (i' * 16 + 8) (i' * 16 + 12))))
        )
        (four_to_nat 8
            (seq_to_four_LE (seq_uint8_to_seq_nat8 (Seq.slice down_s (i' * 16 + 12) (i' * 16 + 16)))
            )));
  DV.put_sel h db ((4 * 4) * i');
  DV.put_sel h db (4 * (4 * i' + 1));
  DV.put_sel h db (4 * (4 * i' + 2));
  DV.put_sel h db (4 * (4 * i' + 3));
  Vale.Interop.Views.put32_reveal ();
  seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4 * i'))));
  seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4 * i' + 1))));
  seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4 * i' + 2))));
  seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s_init (4 * i' + 3))));
  Vale.Interop.Views.get32_128_reveal ();
  assert (UInt32.uint_to_t (four_select (Seq.index s i') (i % 4)) ==
      Seq.index (Seq.slice (B.as_seq h b) (i' * 4) (i' * 4 + 4)) (i % 4));
  assert (Seq.index (B.as_seq h b) i ==
      Seq.index (Seq.slice (B.as_seq h b) (i' * 4) (i' * 4 + 4)) (i % 4))
in
Classical.forall_intro aux;
assert (Seq.equal sf s_init)
Vale.Wrapper.X64.Sha.fst.checked
Vale.Stdcalls.X64.Sha.fsti.checked Vale.SHA.Simplify_Sha.fsti.checked Vale.SHA.SHA_helpers.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Base.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Spec.SHA2.Constants.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked Lib.IntTypes.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.Wrapper.X64.Sha.fst
Vale.Interop.Base.buf_t Vale.Arch.HeapTypes_s.TUInt32 Vale.Arch.HeapTypes_s.TUInt128 FStar.Monotonic.HyperStack.mem Prims._assert FStar.Seq.Base.equal Vale.SHA.SHA_helpers.word Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.op_Equality FStar.UInt32.t FStar.Seq.Base.index Vale.Interop.Types.base_typ_as_type Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims.eq2 LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder FStar.Seq.Base.slice FStar.Mul.op_Star Prims.op_Addition Prims.op_Modulus FStar.UInt32.uint_to_t Vale.Def.Words.Four_s.four_select Vale.Def.Types_s.nat32 Vale.Def.Types_s.quad32 Vale.Interop.Views.get32_128_reveal Vale.Def.Words.Seq.seq_to_four_to_seq_LE Vale.Def.Words_s.natN Prims.pow2 Vale.Def.Words.Four_s.nat_to_four FStar.UInt32.v Vale.Interop.Views.put32_reveal LowStar.BufferView.Down.put_sel FStar.UInt8.t Vale.Def.Words_s.four Vale.Interop.Views.get128 LowStar.BufferView.Down.as_seq Vale.Def.Words_s.Mkfour Vale.Def.Words.Four_s.four_to_nat Vale.Def.Words.Seq_s.seq_to_four_LE Vale.Def.Words_s.nat8 Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 Vale.Def.Types_s.le_bytes_to_quad32_reveal Vale.Interop.Views.get128_reveal FStar.Pervasives.reveal_opaque FStar.Seq.Base.seq Prims.int Prims.op_Division Vale.Def.Words.Seq_s.seq_to_seq_four_LE LowStar.BufferView.Up.get_sel LowStar.BufferView.Up.as_seq_sel Vale.Lib.Seqs_s.seq_map Vale.SHA.SHA_helpers.nat32_to_word Vale.Def.Words.Seq_s.seq_four_to_seq_LE Vale.Def.Words_s.nat32 Vale.Def.Types_s.le_seq_quad32_to_bytes_reveal Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE Vale.SHA.SHA_helpers.hash256 Vale.SHA.SHA_helpers.le_bytes_to_hash 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.length_eq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Vale.Interop.Views.up_view128 LowStar.BufferView.Down.length_eq LowStar.BufferView.Down.length LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview
module Vale.Wrapper.X64.Sha
open FStar.Mul

module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Interop.Base
open Vale.AsLowStar.MemoryHelpers
open Vale.Def.Words.Seq_s
open Vale.SHA.Simplify_Sha
open Vale.Def.Types_s
open Vale.Def.Words_s
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq
open Vale.Lib.Seqs_s

friend Lib.IntTypes
friend Vale.SHA.SHA_helpers

#set-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0"

let math_aux (n:nat) : Lemma ( ((64 * n) * 1) / 16 == 4 * n) = ()


val lemma_k_reqs_equiv
  (k_b:ibuf_t TUInt32 TUInt128)
  (h:HS.mem) : Lemma
  (requires IB.live h k_b /\
    IB.length k_b == 64 /\
    Seq.equal (B.as_seq h k_b) (Spec.SHA2.Constants.k224_256))
  (ensures  (
    DV.length_eq (get_downview k_b);
    k_reqs (UV.as_seq h (UV.mk_buffer (get_downview k_b) Vale.Interop.Views.up_view128))))


#push-options "--z3cliopt smt.arith.nl=true"
let lemma_k_reqs_equiv k_b h =
  let db = get_downview k_b in
  DV.length_eq db;
  let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
  let k_seq = UV.as_seq h ub in
  assert (Seq.equal (B.as_seq h k_b) k);
  UV.length_eq ub;
  let aux (i:nat{i < size_k_w_256/4}) : Lemma
    ((k_seq.[i]).lo0 == word_to_nat32 (k.[4 * i]) /\
    (k_seq.[i]).lo1 == word_to_nat32 (k.[4 * i + 1]) /\
    (k_seq.[i]).hi2 == word_to_nat32 (k.[4 * i + 2]) /\
    (k_seq.[i]).hi3 == word_to_nat32 (k.[4 * i + 3]))
    =
    let down_s = DV.as_seq h db in
    let s = B.as_seq h k_b in

    UV.as_seq_sel h ub i;
    // Proves
    // assert (k_seq.[i] == UV.sel h ub i);

    UV.get_sel h ub i;
    //Proves
    //assert (k_seq.[i] == Vale.Interop.Views.get128 (Seq.slice down_s (i*16) (i*16+16)));

    Vale.Interop.Views.get128_reveal ();
    // We get the following by revealing the definition of get128
    // let s_slice = seq_uint8_to_seq_nat8 (Seq.slice down_s (i*16) (i*16+16)) in
    // assert (k_seq.[i] == le_bytes_to_quad32 s_slice);

    le_bytes_to_quad32_reveal ();
    reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
    // Revealing le_bytes_to_quad32 gives us the following
    assert (k_seq.[i] == Mkfour
                 (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                   (Seq.slice down_s (i*16) (i*16+4)))))
                 (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                   (Seq.slice down_s (i*16+4) (i*16+8)))))
                 (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                   (Seq.slice down_s (i*16+8) (i*16+12)))))
                 (four_to_nat 8 (seq_to_four_LE (seq_uint8_to_seq_nat8
                   (Seq.slice down_s (i*16+12) (i*16+16))))));

    // Gives us that Seq.slice down_s (i*16) (i*16+4) == Vale.Interop.Views.put32 (Seq.index s (4*i)) and same for other indices
    DV.put_sel h db (4*4*i);
    DV.put_sel h db (4*(4*i+1));
    DV.put_sel h db (4*(4*i+2));
    DV.put_sel h db (4*(4*i+3));

    Vale.Interop.Views.put32_reveal ();

    // Apply the only lemmas without SMTPat to simplify the following patterns:
    // assert (four_to_nat 8 (
    //              seq_to_four_LE (
    //                seq_uint8_to_seq_nat8 (
    //                seq_nat8_to_seq_uint8 (
    //              four_to_seq_LE (
    //         nat_to_four 8 (UInt32.v (Seq.index s (4*i)))))))) ==
    //         UInt32.v (Seq.index s (4*i)));
    seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s (4*i))));
    seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s (4*i+1))));
    seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s (4*i+2))));
    seq_to_four_to_seq_LE (nat_to_four 8 (UInt32.v (Seq.index s (4*i+3))))

  in Classical.forall_intro aux
#pop-options


val simplify_le_bytes_to_hash_uint32
  (b:buf_t TUInt32 TUInt128)
  (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 8)
  (ensures
  (reveal_word();
  DV.length_eq (get_downview b);
  Seq.equal
    (le_bytes_to_hash (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)))
val simplify_le_bytes_to_hash_uint32
  (b:buf_t TUInt32 TUInt128)
  (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 8)
  (ensures
  (reveal_word();
  DV.length_eq (get_downview b);
  Seq.equal
    (le_bytes_to_hash (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.TUInt32 Vale.Arch.HeapTypes_s.TUInt128 ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires LowStar.Monotonic.Buffer.live h b /\ LowStar.Monotonic.Buffer.length b == 8)
      (ensures
        ([@@ FStar.Pervasives.inline_let ]let _ = Vale.SHA.SHA_helpers.reveal_word () in
          [@@ FStar.Pervasives.inline_let ]let _ =
            LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview b)
          in
          FStar.Seq.Base.equal (Vale.SHA.SHA_helpers.le_bytes_to_hash (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)))