val gcm_simplify2 (b:buf_t TUInt8 TUInt128) (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 16)
  (ensures (
    DV.length_eq (get_downview b);
    assert (DV.length (get_downview b) / 16 == 1);
    Seq.equal
      (seq_uint8_to_seq_nat8 (B.as_seq h b))
      (le_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h b 0))
  ))
let gcm_simplify2 b h =
  let view = Vale.Interop.Views.up_view128 in
  let s_init = B.as_seq h b in
  let db = get_downview b in
  let s_down = DV.as_seq h db in
  DV.length_eq db;
  assert (DV.length (get_downview b) / 16 = 1);
  let b_v = UV.mk_buffer db view in
  UV.length_eq b_v;
  UV.get_sel h b_v 0;
  let aux (i:nat{i < B.length b}) : Lemma (Seq.index s_init i == Seq.index s_down i) =
    DV.as_seq_sel h db i;
    DV.get_sel h db i;
    Vale.Interop.Views.get8_reveal ()
  in Classical.forall_intro aux;
  assert (Seq.equal (DV.as_seq h db) (B.as_seq h b));
  Vale.Interop.Views.get128_reveal ();
  le_quad32_to_bytes_to_quad32 (seq_uint8_to_seq_nat8 s_init)
val gcm_simplify2 (b:buf_t TUInt8 TUInt128) (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 16)
  (ensures (
    DV.length_eq (get_downview b);
    assert (DV.length (get_downview b) / 16 == 1);
    Seq.equal
      (seq_uint8_to_seq_nat8 (B.as_seq h b))
      (le_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h b 0))
  ))
let gcm_simplify2 b h =
let view = Vale.Interop.Views.up_view128 in
let s_init = B.as_seq h b in
let db = get_downview b in
let s_down = DV.as_seq h db in
DV.length_eq db;
assert (DV.length (get_downview b) / 16 = 1);
let b_v = UV.mk_buffer db view in
UV.length_eq b_v;
UV.get_sel h b_v 0;
let aux (i: nat{i < B.length b}) : Lemma (Seq.index s_init i == Seq.index s_down i) =
  DV.as_seq_sel h db i;
  DV.get_sel h db i;
  Vale.Interop.Views.get8_reveal ()
in
Classical.forall_intro aux;
assert (Seq.equal (DV.as_seq h db) (B.as_seq h b));
Vale.Interop.Views.get128_reveal ();
le_quad32_to_bytes_to_quad32 (seq_uint8_to_seq_nat8 s_init)
Vale.AES.Gcm_simplify.fst.checked
Vale.SHA.Simplify_Sha.fsti.checked Vale.Lib.Seqs_s.fst.checked Vale.Interop.Views.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AES.GCM_helpers.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.AES.Gcm_simplify.fst
Vale.Interop.Base.buf_t Vale.Arch.HeapTypes_s.TUInt8 Vale.Arch.HeapTypes_s.TUInt128 FStar.Monotonic.HyperStack.mem Vale.Arch.Types.le_quad32_to_bytes_to_quad32 Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 Prims.unit Vale.Interop.Views.get128_reveal Prims._assert FStar.Seq.Base.equal FStar.UInt8.t LowStar.BufferView.Down.as_seq LowStar.Monotonic.Buffer.as_seq Vale.Interop.Types.base_typ_as_type LowStar.Buffer.trivial_preorder FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan LowStar.Monotonic.Buffer.length Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Vale.Interop.Views.get8_reveal LowStar.BufferView.Down.get_sel LowStar.BufferView.Down.as_seq_sel LowStar.BufferView.Up.get_sel Vale.Def.Types_s.quad32 LowStar.BufferView.Up.length_eq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Prims.op_Equality Prims.int Prims.op_Division LowStar.BufferView.Down.length Vale.Interop.Types.get_downview LowStar.BufferView.Down.length_eq FStar.Seq.Properties.lseq LowStar.BufferView.Down.buffer FStar.Seq.Base.seq LowStar.BufferView.Up.view Vale.Interop.Views.up_view128
module Vale.AES.Gcm_simplify

open FStar.Mul
open Vale.SHA.Simplify_Sha

let le_bytes_to_seq_quad32_uint8_to_nat8_length s =
  reveal_opaque (`%le_bytes_to_seq_quad32) le_bytes_to_seq_quad32

let gcm_simplify1 b h n =
  let db = get_downview b in
  DV.length_eq db;
  let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
  UV.length_eq ub;
  lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b h
val gcm_simplify2 (b:buf_t TUInt8 TUInt128) (h:HS.mem) : Lemma
  (requires B.live h b /\ B.length b == 16)
  (ensures (
    DV.length_eq (get_downview b);
    assert (DV.length (get_downview b) / 16 == 1);
    Seq.equal
      (seq_uint8_to_seq_nat8 (B.as_seq h b))
      (le_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h b 0))
  ))

    b: Vale.Interop.Base.buf_t Vale.Arch.HeapTypes_s.TUInt8 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 == 16)
      (ensures
        ([@@ FStar.Pervasives.inline_let ]let _ =
            LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview b)
          in
          [@@ FStar.Pervasives.inline_let ]let _ =
            assert (LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview b) / 16 == 1)
          in
          FStar.Seq.Base.equal (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (LowStar.Monotonic.Buffer.as_seq
                    h
                    b))
            (Vale.Def.Types_s.le_quad32_to_bytes (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                    Vale.Arch.HeapTypes_s.TUInt128
                    h
                    b
                    0))))