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))))
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
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))))
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;
  UV.get_sel h ub i;
  Vale.Interop.Views.get128_reveal ();
  le_bytes_to_quad32_reveal ();
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  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)))))
    );
  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 (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
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.ibuf_t Vale.Arch.HeapTypes_s.TUInt32 Vale.Arch.HeapTypes_s.TUInt128 FStar.Monotonic.HyperStack.mem FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Division Vale.SHA.SHA_helpers.size_k_w_256 Prims.l_and Prims.eq2 Vale.Def.Words_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__lo0 Vale.Def.Types_s.nat32 Vale.SHA.SHA_helpers.op_String_Access Vale.Def.Types_s.quad32 Vale.SHA.SHA_helpers.word_to_nat32 Vale.SHA.SHA_helpers.word Vale.SHA.SHA_helpers.k FStar.Mul.op_Star Vale.Def.Words_s.__proj__Mkfour__item__lo1 Prims.op_Addition Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Prims.unit Prims.l_True Prims.squash FStar.Seq.Base.index Prims.op_Multiply Prims.Nil FStar.Pervasives.pattern 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.Types.base_typ_as_type Vale.Interop.Views.put32_reveal LowStar.BufferView.Down.put_sel FStar.UInt8.t Prims._assert Vale.Def.Words_s.four 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 FStar.Seq.Base.slice FStar.Pervasives.reveal_opaque FStar.Seq.Base.seq Prims.int Prims.op_Modulus FStar.Seq.Base.length Vale.Def.Words.Seq_s.seq_to_seq_four_LE Vale.Def.Types_s.le_bytes_to_quad32_reveal Vale.Interop.Views.get128_reveal LowStar.BufferView.Up.get_sel LowStar.BufferView.Up.as_seq_sel LowStar.Monotonic.Buffer.as_seq LowStar.ImmutableBuffer.immutable_preorder FStar.Seq.Properties.lseq LowStar.BufferView.Down.length LowStar.BufferView.Down.as_seq LowStar.BufferView.Up.length_eq FStar.Seq.Base.equal LowStar.BufferView.Up.length LowStar.BufferView.Up.as_seq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Vale.Interop.Views.up_view128 LowStar.BufferView.Down.length_eq 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))))
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))))

    k_b: Vale.Interop.Base.ibuf_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 k_b /\ LowStar.Monotonic.Buffer.length k_b == 64 /\
        FStar.Seq.Base.equal (LowStar.Monotonic.Buffer.as_seq h k_b) Spec.SHA2.Constants.k224_256)
      (ensures
        ([@@ FStar.Pervasives.inline_let ]let _ =
            LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview k_b)
          in
          Vale.SHA.SHA_helpers.k_reqs (LowStar.BufferView.Up.as_seq h
                (LowStar.BufferView.Up.mk_buffer (Vale.Interop.Types.get_downview k_b)
                    Vale.Interop.Views.up_view128))))