val gcm_simplify1 (b:buf_t TUInt8 TUInt128) (h:HS.mem) (n:nat) : Lemma
  (requires B.length b = n)
  (ensures (
    DV.length_eq (get_downview b);
    let s = (le_seq_quad32_to_bytes (UV.as_seq h (UV.mk_buffer (get_downview b) Vale.Interop.Views.up_view128))) in
    n <= Seq.length s ==>
      Seq.equal
        (seq_uint8_to_seq_nat8 (B.as_seq h b))
        (Seq.slice s 0 n)
  ))
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_simplify1 (b:buf_t TUInt8 TUInt128) (h:HS.mem) (n:nat) : Lemma
  (requires B.length b = n)
  (ensures (
    DV.length_eq (get_downview b);
    let s = (le_seq_quad32_to_bytes (UV.as_seq h (UV.mk_buffer (get_downview b) Vale.Interop.Views.up_view128))) in
    n <= Seq.length s ==>
      Seq.equal
        (seq_uint8_to_seq_nat8 (B.as_seq h b))
        (Seq.slice s 0 n)
  ))
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
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 Prims.nat Vale.SHA.Simplify_Sha.lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 Prims.unit LowStar.BufferView.Up.length_eq Vale.Def.Types_s.quad32 LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer FStar.UInt8.t Vale.Interop.Views.up_view128 LowStar.BufferView.Down.length_eq LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview LowStar.Buffer.trivial_preorder Vale.Interop.Types.base_typ_as_type
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
val gcm_simplify1 (b:buf_t TUInt8 TUInt128) (h:HS.mem) (n:nat) : Lemma
  (requires B.length b = n)
  (ensures (
    DV.length_eq (get_downview b);
    let s = (le_seq_quad32_to_bytes (UV.as_seq h (UV.mk_buffer (get_downview b) Vale.Interop.Views.up_view128))) in
    n <= Seq.length s ==>
      Seq.equal
        (seq_uint8_to_seq_nat8 (B.as_seq h b))
        (Seq.slice s 0 n)
  ))

    b: Vale.Interop.Base.buf_t Vale.Arch.HeapTypes_s.TUInt8 Vale.Arch.HeapTypes_s.TUInt128 ->
    h: FStar.Monotonic.HyperStack.mem ->
    n: Prims.nat
  -> FStar.Pervasives.Lemma (requires LowStar.Monotonic.Buffer.length b = n)
      (ensures
        ([@@ FStar.Pervasives.inline_let ]let _ =
            LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview b)
          in
          let s =
            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))
          in
          n <= FStar.Seq.Base.length s ==>
          FStar.Seq.Base.equal (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (LowStar.Monotonic.Buffer.as_seq
                    h
                    b))
            (FStar.Seq.Base.slice s 0 n)))