val lemma_slice_uv_extra (b b_start b_extra: uint8_p) (h: HS.mem)
    : Lemma
      (requires
        B.length b_start = (B.length b / 16) * 16 /\
        b_start == B.gsub b 0ul (UInt32.uint_to_t (B.length b_start)) /\ B.length b_extra = 16 /\
        Seq.equal (B.as_seq h b)
          (Seq.slice (Seq.append (B.as_seq h b_start) (B.as_seq h b_extra)) 0 (B.length b)))
      (ensures
        (let b_start_d = get_downview b_start in
          length_aux6 b_start;
          let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
          let b_extra_d = get_downview b_extra in
          length_aux6 b_extra;
          let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
          let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
          let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
          Seq.equal sf (seq_uint8_to_seq_nat8 (B.as_seq h b))))
let lemma_slice_uv_extra (b:uint8_p) (b_start:uint8_p) (b_extra:uint8_p) (h:HS.mem) : Lemma
  (requires
    B.length b_start = B.length b / 16 * 16 /\
    b_start == B.gsub b 0ul (UInt32.uint_to_t (B.length b_start)) /\
    B.length b_extra = 16 /\
    Seq.equal
      (B.as_seq h b)
      (Seq.slice (Seq.append (B.as_seq h b_start) (B.as_seq h b_extra)) 0 (B.length b))
    )
  (ensures (
    let b_start_d = get_downview b_start in
    length_aux6 b_start;
    let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
    let b_extra_d = get_downview b_extra in
    length_aux6 b_extra;
    let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
    let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
    let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
    Seq.equal sf (seq_uint8_to_seq_nat8 (B.as_seq h b))
 ))
 =
 let b_start_d = get_downview b_start in
 length_aux6 b_start;
 let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
 let b_extra_d = get_downview b_extra in
 length_aux6 b_extra;
 let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
 let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
 let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
 let b_f = seq_uint8_to_seq_nat8 (B.as_seq h b) in
 // if B.length b > B.length b_start then (
   calc (==) {
     sf;
     (==) { DV.length_eq b_start_d; lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b_start h;
          le_bytes_to_seq_quad32_to_bytes (UV.as_seq h b_start_u) }
     wrap_slice (le_seq_quad32_to_bytes (Seq.append
       (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_start)))
       (UV.as_seq h b_extra_u)))
     (B.length b);
     (==) { DV.length_eq b_extra_d; lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b_extra h;
       le_bytes_to_seq_quad32_to_bytes (UV.as_seq h b_extra_u) }
     wrap_slice (le_seq_quad32_to_bytes (Seq.append
       (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_start)))
       (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))))
     (B.length b);
     (==) { append_distributes_le_seq_quad32_to_bytes
        (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_start)))
        (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))
        }
     wrap_slice (Seq.append
       (le_seq_quad32_to_bytes (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_start))))
       (le_seq_quad32_to_bytes (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))))
     (B.length b);
     (==) { le_seq_quad32_to_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_start));
            le_seq_quad32_to_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)) }
     wrap_slice (Seq.append
       (seq_uint8_to_seq_nat8 (B.as_seq h b_start))
       (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))
     (B.length b);
     (==) { Seq.lemma_eq_intro b_f
       (wrap_slice (Seq.append
         (seq_uint8_to_seq_nat8 (B.as_seq h b_start))
         (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))
       (B.length b))
     }
     b_f;
   }
val lemma_slice_uv_extra (b b_start b_extra: uint8_p) (h: HS.mem)
    : Lemma
      (requires
        B.length b_start = (B.length b / 16) * 16 /\
        b_start == B.gsub b 0ul (UInt32.uint_to_t (B.length b_start)) /\ B.length b_extra = 16 /\
        Seq.equal (B.as_seq h b)
          (Seq.slice (Seq.append (B.as_seq h b_start) (B.as_seq h b_extra)) 0 (B.length b)))
      (ensures
        (let b_start_d = get_downview b_start in
          length_aux6 b_start;
          let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
          let b_extra_d = get_downview b_extra in
          length_aux6 b_extra;
          let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
          let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
          let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
          Seq.equal sf (seq_uint8_to_seq_nat8 (B.as_seq h b))))
let lemma_slice_uv_extra (b b_start b_extra: uint8_p) (h: HS.mem)
    : Lemma
      (requires
        B.length b_start = (B.length b / 16) * 16 /\
        b_start == B.gsub b 0ul (UInt32.uint_to_t (B.length b_start)) /\ B.length b_extra = 16 /\
        Seq.equal (B.as_seq h b)
          (Seq.slice (Seq.append (B.as_seq h b_start) (B.as_seq h b_extra)) 0 (B.length b)))
      (ensures
        (let b_start_d = get_downview b_start in
          length_aux6 b_start;
          let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
          let b_extra_d = get_downview b_extra in
          length_aux6 b_extra;
          let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
          let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
          let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
          Seq.equal sf (seq_uint8_to_seq_nat8 (B.as_seq h b)))) =
let b_start_d = get_downview b_start in
length_aux6 b_start;
let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
let b_extra_d = get_downview b_extra in
length_aux6 b_extra;
let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
let b_f = seq_uint8_to_seq_nat8 (B.as_seq h b) in
calc ( == ) {
  sf;
  ( == ) { (DV.length_eq b_start_d;
    lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b_start h;
    le_bytes_to_seq_quad32_to_bytes (UV.as_seq h b_start_u)) }
  wrap_slice (le_seq_quad32_to_bytes (Seq.append (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq
                        h
                        b_start)))
            (UV.as_seq h b_extra_u)))
    (B.length b);
  ( == ) { (DV.length_eq b_extra_d;
    lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 b_extra h;
    le_bytes_to_seq_quad32_to_bytes (UV.as_seq h b_extra_u)) }
  wrap_slice (le_seq_quad32_to_bytes (Seq.append (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq
                        h
                        b_start)))
            (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))))
    (B.length b);
  ( == ) { append_distributes_le_seq_quad32_to_bytes (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (
              B.as_seq h b_start)))
    (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra))) }
  wrap_slice (Seq.append (le_seq_quad32_to_bytes (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq
                        h
                        b_start))))
        (le_seq_quad32_to_bytes (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra))
            )))
    (B.length b);
  ( == ) { (le_seq_quad32_to_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_start));
    le_seq_quad32_to_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h b_extra))) }
  wrap_slice (Seq.append (seq_uint8_to_seq_nat8 (B.as_seq h b_start))
        (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))
    (B.length b);
  ( == ) { Seq.lemma_eq_intro b_f
    (wrap_slice (Seq.append (seq_uint8_to_seq_nat8 (B.as_seq h b_start))
            (seq_uint8_to_seq_nat8 (B.as_seq h b_extra)))
        (B.length b)) }
  b_f;
}
Vale.Wrapper.X64.GCMdecryptOpt.fst.checked
Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Decls.fsti.checked Vale.Stdcalls.X64.GCMdecryptOpt.fst.checked Vale.SHA.Simplify_Sha.fsti.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.Gcm_simplify.fsti.checked Vale.AES.GCM_helpers.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Integers.fst.checked FStar.Int.Cast.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Wrapper.X64.GCMdecryptOpt.fst
Vale.Wrapper.X64.GCMdecryptOpt.uint8_p FStar.Monotonic.HyperStack.mem FStar.Calc.calc_finish FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.eq2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Vale.Wrapper.X64.GCMdecryptOpt.wrap_slice Vale.Def.Words_s.nat8 FStar.Seq.Base.append Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 LowStar.Monotonic.Buffer.as_seq FStar.UInt8.t LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.length Vale.Def.Types_s.le_seq_quad32_to_bytes Vale.Def.Types_s.le_bytes_to_seq_quad32 Vale.Def.Types_s.quad32 LowStar.BufferView.Up.as_seq FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes Vale.SHA.Simplify_Sha.lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 LowStar.BufferView.Down.length_eq Prims.squash Vale.Arch.Types.append_distributes_le_seq_quad32_to_bytes Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32 FStar.Seq.Base.lemma_eq_intro LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Vale.Interop.Views.up_view128 Vale.Wrapper.X64.GCMdecryptOpt.length_aux6 LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview Vale.Arch.HeapTypes_s.TUInt8 Prims.l_and Prims.b2t Prims.op_Equality Prims.int FStar.Integers.op_Star FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.op_Slash LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.gsub FStar.UInt32.__uint_to_t FStar.UInt32.uint_to_t FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.Pervasives.pattern
module Vale.Wrapper.X64.GCMdecryptOpt

open FStar.Mul
open Vale.Stdcalls.X64.GCMdecryptOpt
open Vale.AsLowStar.MemoryHelpers
open Vale.X64.MemoryAdapters
module V = Vale.X64.Decls
open Vale.SHA.Simplify_Sha
open Vale.AES.Gcm_simplify
open Vale.AES.GCM_helpers
open FStar.Calc
open FStar.Int.Cast
open FStar.Integers
open Vale.Arch.Types
open Vale.Lib.BufferViewHelpers

let wrap_slice (#a:Type0) (s:Seq.seq a) (i:int) : Seq.seq a =
  Seq.slice s 0 (if 0 <= i && i <= Seq.length s then i else 0)

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

let math_aux (n:nat) : Lemma (n * 1 == n) = ()

let length_div (b:uint8_p) : Lemma
  (requires B.length b = 16)
  (ensures DV.length (get_downview b) / 16 = 1)
  = DV.length_eq (get_downview b)

inline_for_extraction
val gcm128_decrypt_opt':
  key:Ghost.erased (Seq.seq nat32) ->
  iv:Ghost.erased supported_iv_LE ->
  auth_b:uint8_p ->
  auth_bytes:uint64 ->
  auth_num:uint64 ->
  keys_b:uint8_p ->
  iv_b:uint8_p ->
  hkeys_b:uint8_p ->
  abytes_b:uint8_p ->
  in128x6_b:uint8_p ->
  out128x6_b:uint8_p ->
  len128x6:uint64 ->
  in128_b:uint8_p ->
  out128_b:uint8_p ->
  len128_num:uint64 ->
  inout_b:uint8_p ->
  cipher_num:uint64 ->

  scratch_b:uint8_p ->
  tag_b:uint8_p ->

  Stack UInt64.t
    (requires fun h0 ->
      B.disjoint tag_b in128x6_b /\ B.disjoint tag_b out128x6_b /\
      B.disjoint tag_b in128_b /\ B.disjoint tag_b out128_b /\
      B.disjoint tag_b inout_b /\ B.disjoint tag_b scratch_b /\
      B.disjoint tag_b iv_b /\

      B.disjoint iv_b keys_b /\ B.disjoint iv_b auth_b /\
      B.disjoint iv_b abytes_b /\ B.disjoint iv_b in128x6_b /\
      B.disjoint iv_b out128x6_b /\ B.disjoint iv_b in128_b /\
      B.disjoint iv_b out128_b /\ B.disjoint iv_b inout_b /\
      B.disjoint iv_b scratch_b /\ B.disjoint iv_b hkeys_b /\

      B.disjoint scratch_b keys_b /\ B.disjoint scratch_b auth_b /\
      B.disjoint scratch_b abytes_b /\ B.disjoint scratch_b in128x6_b /\
      B.disjoint scratch_b out128x6_b /\ B.disjoint scratch_b in128_b /\
      B.disjoint scratch_b out128_b /\ B.disjoint scratch_b inout_b /\
      B.disjoint scratch_b hkeys_b /\

      B.disjoint inout_b keys_b /\ B.disjoint inout_b auth_b /\
      B.disjoint inout_b abytes_b /\ B.disjoint inout_b in128x6_b /\
      B.disjoint inout_b out128x6_b /\ B.disjoint inout_b in128_b /\
      B.disjoint inout_b out128_b /\ B.disjoint inout_b hkeys_b /\

      B.disjoint out128x6_b keys_b /\ B.disjoint out128x6_b auth_b /\
      B.disjoint out128x6_b abytes_b /\ B.disjoint out128x6_b hkeys_b /\
      B.disjoint out128x6_b in128_b /\ B.disjoint out128x6_b inout_b /\

      B.disjoint in128x6_b keys_b /\ B.disjoint in128x6_b auth_b /\
      B.disjoint in128x6_b abytes_b /\ B.disjoint in128x6_b hkeys_b /\
      B.disjoint in128x6_b in128_b /\ B.disjoint in128x6_b inout_b /\

      B.disjoint out128_b keys_b /\ B.disjoint out128_b auth_b /\
      B.disjoint out128_b abytes_b /\ B.disjoint out128_b hkeys_b /\
      B.disjoint out128_b in128x6_b /\ B.disjoint out128_b out128x6_b /\
      B.disjoint out128_b inout_b /\

      B.disjoint in128_b keys_b /\ B.disjoint in128_b auth_b /\
      B.disjoint in128_b abytes_b /\ B.disjoint in128_b hkeys_b /\
      B.disjoint in128_b in128x6_b /\ B.disjoint in128_b out128x6_b /\
      B.disjoint in128_b inout_b /\

      B.disjoint tag_b abytes_b /\ B.disjoint tag_b auth_b /\
      B.disjoint keys_b abytes_b /\ B.disjoint hkeys_b auth_b /\
      B.disjoint hkeys_b abytes_b /\ B.disjoint auth_b abytes_b /\

      disjoint_or_eq in128x6_b out128x6_b /\
      disjoint_or_eq in128_b out128_b /\
      disjoint_or_eq tag_b hkeys_b /\ disjoint_or_eq tag_b keys_b /\
      disjoint_or_eq keys_b hkeys_b /\ B.disjoint keys_b auth_b /\

      B.live h0 auth_b /\ B.live h0 abytes_b /\ B.live h0 keys_b /\
      B.live h0 iv_b /\ B.live h0 hkeys_b /\
      B.live h0 in128x6_b /\ B.live h0 out128x6_b /\
      B.live h0 in128_b /\ B.live h0 out128_b /\
      B.live h0 inout_b /\ B.live h0 tag_b /\ B.live h0 scratch_b /\

      B.length auth_b = 16 * UInt64.v auth_num /\
      B.length abytes_b == 16 /\
      B.length iv_b = 16 /\
      B.length in128x6_b == 16 * UInt64.v len128x6 /\
      B.length out128x6_b == B.length in128x6_b /\
      B.length in128_b == 16 * UInt64.v len128_num /\
      B.length out128_b == B.length in128_b /\
      B.length inout_b == 16 /\
      B.length scratch_b == 144 /\
      B.length hkeys_b = 128 /\
      B.length tag_b == 16 /\
      B.length keys_b = 176 /\

      UInt64.v cipher_num < pow2_32 /\
      UInt64.v auth_bytes < pow2_32 /\

      UInt64.v len128x6 % 6 == 0 /\
      (UInt64.v len128x6 > 0 ==> UInt64.v len128x6 >= 6) /\
      12 + UInt64.v len128x6 + 6 < pow2_32 /\

      UInt64.v len128x6 * (128/8) + UInt64.v len128_num * (128/8) <= UInt64.v cipher_num /\
      UInt64.v cipher_num < UInt64.v len128x6 * (128/8) + UInt64.v len128_num * (128/8) + 128/8 /\
      UInt64.v auth_num * (128/8) <= UInt64.v auth_bytes /\
      UInt64.v auth_bytes < UInt64.v auth_num * (128/8) + 128/8 /\

      aesni_enabled /\ pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ movbe_enabled /\
      is_aes_key_LE AES_128 (Ghost.reveal key) /\
      (let db = get_downview keys_b in
      length_aux keys_b;
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      Seq.equal (UV.as_seq h0 ub) (key_to_round_keys_LE AES_128 (Ghost.reveal key))) /\

      (let db = get_downview hkeys_b in
       length_aux5 hkeys_b;
       let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
       hkeys_reqs_pub (UV.as_seq h0 ub) (reverse_bytes_quad32 (aes_encrypt_LE AES_128 (Ghost.reveal key) (Mkfour 0 0 0 0)))) /\
      (length_div iv_b;
       (low_buffer_read TUInt8 TUInt128 h0 iv_b 0 ==
         compute_iv_BE (aes_encrypt_LE AES_128 (Ghost.reveal key) (Mkfour 0 0 0 0)) (Ghost.reveal iv))
      )

    )
    (ensures fun h0 c h1 ->
      B.modifies  (B.loc_union (B.loc_buffer iv_b)
                  (B.loc_union (B.loc_buffer scratch_b)
                  (B.loc_union (B.loc_buffer out128x6_b)
                  (B.loc_union (B.loc_buffer out128_b)
                  (B.loc_buffer inout_b))))) h0 h1 /\
      (UInt64.v cipher_num < pow2_32 /\
       UInt64.v auth_bytes < pow2_32 /\ (
       let in128x6_d = get_downview in128x6_b in
       length_aux3 in128x6_b (UInt64.v len128x6);
       let in128x6_u = UV.mk_buffer in128x6_d Vale.Interop.Views.up_view128 in
       let in128_d = get_downview in128_b in
       length_aux3 in128_b (UInt64.v len128_num);
       let in128_u = UV.mk_buffer in128_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let out128x6_d = get_downview out128x6_b in
       length_aux3 out128x6_b (UInt64.v len128x6);
       let out128x6_u = UV.mk_buffer out128x6_d Vale.Interop.Views.up_view128 in
       let out128_d = get_downview out128_b in
       length_aux3 out128_b (UInt64.v len128_num);
       let out128_u = UV.mk_buffer out128_d Vale.Interop.Views.up_view128 in
       let cipher_in =
           Seq.append (Seq.append (UV.as_seq h0 in128x6_u) (UV.as_seq h0 in128_u))
                      (UV.as_seq h0 inout_u)
       in let cipher_bytes = wrap_slice (le_seq_quad32_to_bytes cipher_in) (UInt64.v cipher_num)
       in let plain_out =
           Seq.append (Seq.append (UV.as_seq h1 out128x6_u) (UV.as_seq h1 out128_u))
                      (UV.as_seq h1 inout_u)
       in let plain_bytes = wrap_slice (le_seq_quad32_to_bytes plain_out) (UInt64.v cipher_num)
       in let auth_d = get_downview auth_b in
       length_aux3 auth_b (UInt64.v auth_num);
       let auth_u = UV.mk_buffer auth_d Vale.Interop.Views.up_view128 in
       let abytes_d = get_downview abytes_b in
       length_aux3 abytes_b 1;
       let abytes_u = UV.mk_buffer abytes_d Vale.Interop.Views.up_view128 in
       let auth_in = Seq.append (UV.as_seq h0 auth_u) (UV.as_seq h0 abytes_u) in
       let auth_bytes = wrap_slice (le_seq_quad32_to_bytes auth_in) (UInt64.v auth_bytes) in
      (length_div tag_b;
       let expected_tag = le_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h0 tag_b 0) in
      Seq.length cipher_bytes < pow2_32 /\
      Seq.length auth_bytes < pow2_32 /\
      is_aes_key AES_128 (seq_nat32_to_seq_nat8_LE (Ghost.reveal key)) /\
      (let plain, result = gcm_decrypt_LE AES_128 (seq_nat32_to_seq_nat8_LE (Ghost.reveal key)) (Ghost.reveal iv) cipher_bytes auth_bytes expected_tag in
      Seq.equal plain plain_bytes /\
      (UInt64.v c = 0) == result
      ))))
    )


#push-options "--z3cliopt smt.arith.nl=true --smtencoding.nl_arith_repr boxwrap --ext compat:normalizer_memo_ignore_cfg --retry 3"
#restart-solver
inline_for_extraction
let gcm128_decrypt_opt' key iv auth_b auth_bytes auth_num keys_b iv_b hkeys_b abytes_b
  in128x6_b out128x6_b len128x6 in128_b out128_b len128_num inout_b cipher_num scratch_b tag_b =

  let h0 = get() in
  B.disjoint_neq iv_b auth_b;
  B.disjoint_neq iv_b keys_b;
  B.disjoint_neq iv_b hkeys_b;
  B.disjoint_neq iv_b abytes_b;
  B.disjoint_neq iv_b in128x6_b;
  B.disjoint_neq iv_b out128x6_b;
  B.disjoint_neq iv_b in128_b;
  B.disjoint_neq iv_b out128_b;
  B.disjoint_neq iv_b inout_b;
  B.disjoint_neq iv_b scratch_b;
  B.disjoint_neq iv_b tag_b;


  DV.length_eq (get_downview auth_b);
  DV.length_eq (get_downview keys_b);
  DV.length_eq (get_downview iv_b);
  DV.length_eq (get_downview hkeys_b);
  DV.length_eq (get_downview abytes_b);
  DV.length_eq (get_downview in128x6_b);
  DV.length_eq (get_downview out128x6_b);
  DV.length_eq (get_downview in128_b);
  DV.length_eq (get_downview out128_b);
  DV.length_eq (get_downview inout_b);
  DV.length_eq (get_downview scratch_b);
  DV.length_eq (get_downview tag_b);

  math_aux (B.length auth_b);
  math_aux (B.length keys_b);
  math_aux (B.length iv_b);
  math_aux (B.length hkeys_b);
  math_aux (B.length in128x6_b);
  math_aux (B.length scratch_b);
  math_aux (B.length out128_b);
  FStar.Math.Lemmas.cancel_mul_mod (UInt64.v auth_num) 16;
  assert_norm (176 % 16 = 0);
  assert_norm (16 % 16 = 0);
  assert_norm (144 % 16 = 0);
  FStar.Math.Lemmas.cancel_mul_mod (UInt64.v len128x6) 16;
  FStar.Math.Lemmas.cancel_mul_mod (UInt64.v len128_num) 16;

  calc (<=) {
    256 * ((16 * UInt64.v len128_num) / 16);
    (==) {  FStar.Math.Lemmas.cancel_mul_div (UInt64.v len128_num) 16 }
    256 * (UInt64.v len128_num);
    ( <= ) { assert_norm (256 <= 4096); FStar.Math.Lemmas.lemma_mult_le_right (UInt64.v len128_num) 256 4096 }
    4096 * (UInt64.v len128_num);
  };

  assert (DV.length (get_downview tag_b) % 16 = 0);
  assert (DV.length (get_downview scratch_b) % 16 = 0);
  assert (DV.length (get_downview out128_b) % 16 = 0);

  as_vale_buffer_len #TUInt8 #TUInt128 auth_b;
  as_vale_buffer_len #TUInt8 #TUInt128 keys_b;
  as_vale_buffer_len #TUInt8 #TUInt128 iv_b;
  as_vale_buffer_len #TUInt8 #TUInt128 hkeys_b;
  as_vale_buffer_len #TUInt8 #TUInt128 abytes_b;
  as_vale_buffer_len #TUInt8 #TUInt128 out128x6_b;
  as_vale_buffer_len #TUInt8 #TUInt128 in128x6_b;
  as_vale_buffer_len #TUInt8 #TUInt128 out128x6_b;
  as_vale_buffer_len #TUInt8 #TUInt128 in128_b;
  as_vale_buffer_len #TUInt8 #TUInt128 inout_b;
  as_vale_buffer_len #TUInt8 #TUInt128 scratch_b;
  as_vale_buffer_len #TUInt8 #TUInt128 tag_b;

  bounded_buffer_addrs_all TUInt8 TUInt128 h0 auth_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 in128x6_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 out128x6_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 in128_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 out128_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 inout_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 iv_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 keys_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 hkeys_b;

  let (x, _) = gcm128_decrypt_opt  key iv auth_b auth_bytes auth_num keys_b iv_b hkeys_b abytes_b
  in128x6_b out128x6_b len128x6 in128_b out128_b len128_num inout_b cipher_num scratch_b tag_b () in

  let h1 = get() in
  x
#pop-options

inline_for_extraction
val gcm128_decrypt_opt_alloca:
  key:Ghost.erased (Seq.seq nat32) ->
  iv:Ghost.erased supported_iv_LE ->
  cipher_b:uint8_p ->
  cipher_len:uint64 ->
  auth_b:uint8_p ->
  auth_len:uint64 ->
  iv_b:uint8_p ->
  out_b:uint8_p ->
  tag_b:uint8_p ->
  keys_b:uint8_p ->
  hkeys_b:uint8_p ->

  scratch_b:uint8_p ->
  inout_b : uint8_p ->
  abytes_b : uint8_p ->

  Stack UInt64.t
    (requires fun h0 ->
      B.disjoint scratch_b tag_b /\ B.disjoint scratch_b out_b /\
      B.disjoint scratch_b hkeys_b /\ B.disjoint scratch_b cipher_b /\
      B.disjoint scratch_b auth_b /\ B.disjoint scratch_b iv_b /\
      B.disjoint scratch_b keys_b /\ B.disjoint scratch_b inout_b /\
      B.disjoint scratch_b abytes_b /\

      B.disjoint inout_b tag_b /\ B.disjoint inout_b out_b /\
      B.disjoint inout_b hkeys_b /\ B.disjoint inout_b cipher_b /\
      B.disjoint inout_b auth_b /\ B.disjoint inout_b iv_b /\
      B.disjoint inout_b keys_b /\ B.disjoint inout_b abytes_b /\

      B.disjoint abytes_b tag_b /\ B.disjoint abytes_b out_b /\
      B.disjoint abytes_b hkeys_b /\ B.disjoint abytes_b cipher_b /\
      B.disjoint abytes_b auth_b /\ B.disjoint abytes_b iv_b /\
      B.disjoint abytes_b keys_b /\

      B.disjoint tag_b out_b /\ B.disjoint tag_b hkeys_b /\
      B.disjoint tag_b cipher_b /\ B.disjoint tag_b auth_b /\
      B.disjoint tag_b iv_b /\ disjoint_or_eq tag_b keys_b /\

      B.disjoint iv_b keys_b /\ B.disjoint iv_b out_b /\
      B.disjoint iv_b cipher_b /\ B.disjoint iv_b hkeys_b /\
      B.disjoint iv_b auth_b /\

      B.disjoint out_b keys_b /\ B.disjoint out_b hkeys_b /\
      B.disjoint out_b auth_b /\ disjoint_or_eq out_b cipher_b /\

      B.disjoint cipher_b keys_b /\ B.disjoint cipher_b hkeys_b /\
      B.disjoint cipher_b auth_b /\

      disjoint_or_eq keys_b hkeys_b /\
      B.disjoint keys_b auth_b /\ B.disjoint hkeys_b auth_b /\

      B.live h0 auth_b /\ B.live h0 keys_b /\
      B.live h0 iv_b /\ B.live h0 hkeys_b /\
      B.live h0 out_b /\ B.live h0 cipher_b /\
      B.live h0 tag_b /\

      B.live h0 scratch_b /\ B.live h0 inout_b /\ B.live h0 abytes_b /\

      B.length auth_b = (UInt64.v auth_len / 16) * 16 /\
      B.length iv_b = 16 /\
      B.length cipher_b = (UInt64.v cipher_len / 16) * 16 /\
      B.length out_b = B.length cipher_b /\
      B.length hkeys_b = 128 /\
      B.length tag_b == 16 /\
      B.length keys_b = 176 /\

      B.length scratch_b = 144 /\
      B.length inout_b = 16 /\
      B.length abytes_b = 16 /\

      UInt64.v cipher_len < pow2_32 /\
      UInt64.v auth_len < pow2_32 /\

      aesni_enabled /\ pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ movbe_enabled /\
      is_aes_key_LE AES_128 (Ghost.reveal key) /\
      (Seq.equal (B.as_seq h0 keys_b)
         (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (key_to_round_keys_LE AES_128 (Ghost.reveal key))))) /\

      hkeys_reqs_pub (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b)))
        (reverse_bytes_quad32 (aes_encrypt_LE AES_128 (Ghost.reveal key) (Mkfour 0 0 0 0))) /\

      (length_div iv_b;
       (le_bytes_to_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 iv_b))) ==
         compute_iv_BE (aes_encrypt_LE AES_128 (Ghost.reveal key) (Mkfour 0 0 0 0)) (Ghost.reveal iv)
      )
    )
    (ensures fun h0 c h1 ->
      B.modifies  (B.loc_union (B.loc_buffer iv_b)
                  (B.loc_union (B.loc_buffer scratch_b)
                  (B.loc_union (B.loc_buffer out_b)
                  (B.loc_buffer inout_b)))) h0 h1 /\
      (UInt64.v cipher_len) < pow2_32 /\
      (UInt64.v auth_len) < pow2_32 /\
      (let cipher_d = get_downview cipher_b in
       length_aux3 cipher_b (UInt64.v cipher_len / 16);
       let cipher_u = UV.mk_buffer cipher_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let out_d = get_downview out_b in
       length_aux3 out_b (UInt64.v cipher_len / 16);
       let out_u = UV.mk_buffer out_d Vale.Interop.Views.up_view128 in
       let cipher_in = Seq.append (UV.as_seq h0 cipher_u) (UV.as_seq h0 inout_u) in
       let cipher_bytes = wrap_slice (le_seq_quad32_to_bytes cipher_in) (UInt64.v cipher_len) in
       let plain_out = Seq.append (UV.as_seq h1 out_u) (UV.as_seq h1 inout_u) in
       let plain_bytes = wrap_slice (le_seq_quad32_to_bytes plain_out) (UInt64.v cipher_len) in
       let auth_d = get_downview auth_b in
       length_aux3 auth_b (UInt64.v auth_len / 16);
       let auth_u = UV.mk_buffer auth_d Vale.Interop.Views.up_view128 in
       let abytes_d = get_downview abytes_b in
       length_aux3 abytes_b 1;
       let abytes_u = UV.mk_buffer abytes_d Vale.Interop.Views.up_view128 in
       let auth_in = Seq.append (UV.as_seq h0 auth_u) (UV.as_seq h0 abytes_u) in
       let auth_bytes = wrap_slice (le_seq_quad32_to_bytes auth_in) (UInt64.v auth_len) in
       let expected_tag = seq_uint8_to_seq_nat8 (B.as_seq h0 tag_b) in
      (Seq.length cipher_bytes) < pow2_32 /\
      (Seq.length auth_bytes) < pow2_32 /\
      (let plain, result = gcm_decrypt_LE AES_128 (seq_nat32_to_seq_nat8_LE (Ghost.reveal key)) (Ghost.reveal iv) cipher_bytes auth_bytes expected_tag in
      Seq.equal plain plain_bytes /\
      (UInt64.v c = 0) == result
      )
    ))

let lemma_same_seq_dv (h:HS.mem) (b:uint8_p) : Lemma
  (Seq.equal (B.as_seq h b) (DV.as_seq h (get_downview b))) =
  let db = get_downview b in
  DV.length_eq db;
  let aux (i:nat{i < B.length b}) : Lemma (Seq.index (B.as_seq h b) i == Seq.index (DV.as_seq h db) i) =
    DV.as_seq_sel h db i;
    DV.get_sel h db i;
    Vale.Interop.Views.put8_reveal ()
  in Classical.forall_intro aux

let lemma_uv_split (h:HS.mem) (b:uint8_p) (n:UInt32.t) : Lemma
  (requires B.length b % 16 = 0 /\ UInt32.v n % 16 = 0 /\ UInt32.v n <= B.length b)
  (ensures (
    let b1 = B.gsub b 0ul n in
    let b2 = B.gsub b n (UInt32.uint_to_t (B.length b) - n) in
    let b1_d = get_downview b1 in
    length_aux3 b1 (B.length b1 / 16);
    let b1_u = UV.mk_buffer b1_d Vale.Interop.Views.up_view128 in
    let b2_d = get_downview b2 in
    length_aux3 b2 (B.length b2 / 16);
    let b2_u = UV.mk_buffer b2_d Vale.Interop.Views.up_view128 in
    let b_d = get_downview b in
    length_aux3 b (B.length b / 16);
    let b_u = UV.mk_buffer b_d Vale.Interop.Views.up_view128 in
    let split_bs = Seq.append (UV.as_seq h b1_u) (UV.as_seq h b2_u) in
    let bs = UV.as_seq h b_u in
    Seq.equal bs split_bs)
  ) =
    let b1 = B.gsub b 0ul n in
    let b2 = B.gsub b n (UInt32.uint_to_t (B.length b) - n) in
    let b1_d = get_downview b1 in
    length_aux3 b1 (B.length b1 / 16);
    let b1_u = UV.mk_buffer b1_d Vale.Interop.Views.up_view128 in
    let b2_d = get_downview b2 in
    length_aux3 b2 (B.length b2 / 16);
    let b2_u = UV.mk_buffer b2_d Vale.Interop.Views.up_view128 in
    let b_d = get_downview b in
    length_aux3 b (B.length b / 16);
    let b_u = UV.mk_buffer b_d Vale.Interop.Views.up_view128 in
    let split_bs = Seq.append (UV.as_seq h b1_u) (UV.as_seq h b2_u) in
    let bs = UV.as_seq h b_u in
    calc (==) {
      Seq.length split_bs;
      (==) { }
      Seq.length (UV.as_seq h b1_u) + Seq.length (UV.as_seq h b2_u);
      (==) { UV.length_eq b1_u; UV.length_eq b2_u }
      DV.length b1_d / 16 + DV.length b2_d / 16;
      (==) { DV.length_eq b1_d; DV.length_eq b2_d; math_aux (B.length b1); math_aux (B.length b2) }
      B.length b1 / 16 + B.length b2 / 16;
      (==) { }
      B.length b / 16;
      (==) { DV.length_eq b_d; UV.length_eq b_u; math_aux (B.length b) }
      Seq.length bs;
    };
    assert (Seq.length bs == Seq.length split_bs);
    let aux (i:nat{ i < Seq.length bs}) : Lemma (Seq.index bs i = Seq.index split_bs i)
      =
        UV.length_eq b_u;
        lemma_same_seq_dv h b;
        calc (==) {
          Seq.index bs i;
          (==) { UV.as_seq_sel h b_u i }
          UV.sel h b_u i;
          (==) { UV.get_sel h b_u i }
          Vale.Interop.Views.get128 (Seq.slice (DV.as_seq h b_d) (i * 16) (i * 16 + 16));
          (==) { lemma_same_seq_dv h b }
          Vale.Interop.Views.get128 (Seq.slice (B.as_seq h b) (i * 16) (i * 16 + 16));
          (==) { assert (Seq.equal (B.as_seq h b) (Seq.append (B.as_seq h b1) (B.as_seq h b2))) }
          Vale.Interop.Views.get128 (Seq.slice (Seq.append (B.as_seq h b1) (B.as_seq h b2)) (i * 16) (i * 16 + 16));
        };
        if i < Seq.length (UV.as_seq h b1_u) then (
          lemma_same_seq_dv h b1;
          UV.length_eq b1_u;
          calc (==) {
            Vale.Interop.Views.get128 (Seq.slice (Seq.append (B.as_seq h b1) (B.as_seq h b2)) (i * 16) (i * 16 + 16));
            (==) { }
            Vale.Interop.Views.get128 (Seq.slice (B.as_seq h b1) (i * 16) (i * 16 + 16));
            (==) { UV.get_sel h b1_u i }
            UV.sel h b1_u i;
            (==) { UV.as_seq_sel h b1_u i }
            Seq.index (UV.as_seq h b1_u) i;
            (==) { }
            Seq.index split_bs i;
          }
        ) else (
          lemma_same_seq_dv h b2;
          UV.length_eq b2_u;
          let j = i - UV.length b1_u in
          calc (==) {
            Vale.Interop.Views.get128 (Seq.slice (Seq.append (B.as_seq h b1) (B.as_seq h b2)) (i * 16) (i * 16 + 16));
            (==) { }
            Vale.Interop.Views.get128 (Seq.slice (B.as_seq h b2) (j * 16) (j * 16 + 16));
            (==) { UV.get_sel h b2_u j }
            UV.sel h b2_u j;
            (==) { UV.as_seq_sel h b2_u j }
            Seq.index (UV.as_seq h b2_u) j;
            (==) { }
            Seq.index split_bs i;
          }
       )
    in Classical.forall_intro aux

let math_cast_aux (n:UInt64.t) : Lemma
  (requires UInt64.v n < pow2 32)
  (ensures UInt32.v (uint64_to_uint32 n) = UInt64.v n)
  = FStar.Math.Lemmas.small_mod (UInt64.v n) (pow2 32)

inline_for_extraction
let gcm128_decrypt_opt_alloca key iv cipher_b cipher_len auth_b auth_bytes iv_b
  out_b tag_b keys_b hkeys_b scratch_b inout_b abytes_b =

  let h0 = get() in

  let lemma_uv_key () : Lemma
    (let db = get_downview keys_b in
      length_aux keys_b;
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      Seq.equal (UV.as_seq h0 ub) (key_to_round_keys_LE AES_128 (Ghost.reveal key)))
    = length_aux keys_b;
      let db = get_downview keys_b in
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      le_bytes_to_seq_quad32_to_bytes (key_to_round_keys_LE AES_128 (Ghost.reveal key));
      assert (Seq.equal (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 keys_b)))
         (key_to_round_keys_LE AES_128 (Ghost.reveal key)));
      calc (==) {
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 keys_b));
        (==) { lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 keys_b h0 }
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h0 ub))));
        (==) { le_bytes_to_seq_quad32_to_bytes (UV.as_seq h0 ub) }
        UV.as_seq h0 ub;
      }

  in lemma_uv_key ();

  // Simplify the precondition for hkeys_b
  let lemma_uv_hkey () : Lemma
    (let db = get_downview hkeys_b in
      length_aux5 hkeys_b;
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      UV.as_seq h0 ub == le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b)))
    = length_aux5 hkeys_b;
      let db = get_downview hkeys_b in
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      calc (==) {
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b));
        (==) { lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 hkeys_b h0 }
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h0 ub))));
        (==) { le_bytes_to_seq_quad32_to_bytes (UV.as_seq h0 ub) }
        UV.as_seq h0 ub;
      }

  in lemma_uv_hkey ();

  // Simplify the expression for the iv
  DV.length_eq (get_downview iv_b);
  length_aux4 iv_b;
  calc (==) {
    compute_iv_BE (aes_encrypt_LE AES_128 (Ghost.reveal key) (Mkfour 0 0 0 0))
                  (Ghost.reveal iv);
    (==) { }
    le_bytes_to_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 iv_b));
    (==) { gcm_simplify2 iv_b h0 }
    le_bytes_to_quad32 (le_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h0 iv_b 0));
    (==) { le_bytes_to_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h0 iv_b 0) }
    low_buffer_read TUInt8 TUInt128 h0 iv_b 0;
  };

  // Simplify post condition for tag
  gcm_simplify2 tag_b h0;
  length_div tag_b;

  // Compute length of biggest blocks of 6 * 128-bit blocks
  let len128x6 = UInt64.mul (cipher_len / 96uL) 96uL in
  if len128x6 / 16uL >= 6uL then (
    let len128_num = ((cipher_len / 16uL) * 16uL) - len128x6 in
    // Casting to uint32 is here the equality
    math_cast_aux len128x6;
    math_cast_aux len128_num;
    let in128x6_b = B.sub cipher_b 0ul (uint64_to_uint32 len128x6) in
    let out128x6_b = B.sub out_b 0ul (uint64_to_uint32 len128x6) in

    let in128_b = B.sub cipher_b (uint64_to_uint32 len128x6) (uint64_to_uint32 len128_num) in
    let out128_b = B.sub out_b (uint64_to_uint32 len128x6) (uint64_to_uint32 len128_num) in

    let auth_num = UInt64.div auth_bytes 16uL in
    let len128x6' = UInt64.div len128x6 16uL in
    let len128_num' = UInt64.div len128_num 16uL in

    let c = gcm128_decrypt_opt'
      key
      iv
      auth_b
      auth_bytes
      auth_num
      keys_b
      iv_b
      hkeys_b
      abytes_b
      in128x6_b
      out128x6_b
      len128x6'
      in128_b
      out128_b
      len128_num'
      inout_b
      cipher_len
      scratch_b
      tag_b in

    let h1 = get() in
    lemma_uv_split h0 cipher_b (uint64_to_uint32 len128x6);

    // Still need the two asserts for z3 to pick up seq equality
    assert (
       let in128x6_d = get_downview in128x6_b in
       length_aux3 in128x6_b (UInt64.v len128x6');
       let in128x6_u = UV.mk_buffer in128x6_d Vale.Interop.Views.up_view128 in
       let in128_d = get_downview in128_b in
       length_aux3 in128_b (UInt64.v len128_num');
       let in128_u = UV.mk_buffer in128_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let cipher_d = get_downview cipher_b in
       length_aux3 cipher_b (UInt64.v cipher_len / 16);
       let cipher_u = UV.mk_buffer cipher_d Vale.Interop.Views.up_view128 in
       Seq.equal
         (Seq.append (Seq.append (UV.as_seq h0 in128x6_u) (UV.as_seq h0 in128_u))
           (UV.as_seq h0 inout_u))
         (Seq.append (UV.as_seq h0 cipher_u) (UV.as_seq h0 inout_u)));

    lemma_uv_split h1 out_b (uint64_to_uint32 len128x6);

    assert (
       let out128x6_d = get_downview out128x6_b in
       length_aux3 out128x6_b (UInt64.v len128x6');
       let out128x6_u = UV.mk_buffer out128x6_d Vale.Interop.Views.up_view128 in
       let out128_d = get_downview out128_b in
       length_aux3 out128_b (UInt64.v len128_num');
       let out128_u = UV.mk_buffer out128_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let out_d = get_downview out_b in
       length_aux3 out_b (UInt64.v cipher_len / 16);
       let out_u = UV.mk_buffer out_d Vale.Interop.Views.up_view128 in
       Seq.equal
         (Seq.append (Seq.append (UV.as_seq h1 out128x6_u) (UV.as_seq h1 out128_u))
           (UV.as_seq h1 inout_u))
         (Seq.append (UV.as_seq h1 out_u) (UV.as_seq h1 inout_u)));

    c

  ) else (

    let len128x6 = 0ul in
    // Compute the size of the remaining 128-bit blocks
    let len128_num = ((cipher_len / 16uL) * 16uL) in
    // Casting to uint32 is here the equality
    FStar.Math.Lemmas.small_mod (UInt64.v len128_num) pow2_32;
    let in128x6_b = B.sub cipher_b 0ul len128x6 in
    let out128x6_b = B.sub out_b 0ul len128x6 in
    let in128_b = B.sub cipher_b len128x6 (uint64_to_uint32 len128_num) in
    let out128_b = B.sub out_b len128x6 (uint64_to_uint32 len128_num) in

    let auth_num = UInt64.div auth_bytes 16uL in
    let len128_num' = UInt64.div len128_num 16uL in
    let len128x6' = 0uL in

    let c = gcm128_decrypt_opt'
      key
      iv
      auth_b
      auth_bytes
      auth_num
      keys_b
      iv_b
      hkeys_b
      abytes_b
      in128x6_b
      out128x6_b
      len128x6'
      in128_b
      out128_b
      len128_num'
      inout_b
      cipher_len
      scratch_b
      tag_b in

    let h1 = get() in
    lemma_uv_split h0 cipher_b len128x6;

    // Still need the two asserts for z3 to pick up seq equality
    assert (
       let in128x6_d = get_downview in128x6_b in
       length_aux3 in128x6_b (UInt64.v len128x6');
       let in128x6_u = UV.mk_buffer in128x6_d Vale.Interop.Views.up_view128 in
       let in128_d = get_downview in128_b in
       length_aux3 in128_b (UInt64.v len128_num');
       let in128_u = UV.mk_buffer in128_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let plain_d = get_downview cipher_b in
       length_aux3 cipher_b (UInt64.v cipher_len / 16);
       let plain_u = UV.mk_buffer plain_d Vale.Interop.Views.up_view128 in
       Seq.equal
         (Seq.append (Seq.append (UV.as_seq h0 in128x6_u) (UV.as_seq h0 in128_u))
           (UV.as_seq h0 inout_u))
         (Seq.append (UV.as_seq h0 plain_u) (UV.as_seq h0 inout_u)));

    lemma_uv_split h1 out_b len128x6;

    assert (
       let out128x6_d = get_downview out128x6_b in
       length_aux3 out128x6_b (UInt64.v len128x6');
       let out128x6_u = UV.mk_buffer out128x6_d Vale.Interop.Views.up_view128 in
       let out128_d = get_downview out128_b in
       length_aux3 out128_b (UInt64.v len128_num');
       let out128_u = UV.mk_buffer out128_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let out_d = get_downview out_b in
       length_aux3 out_b (UInt64.v cipher_len / 16);
       let out_u = UV.mk_buffer out_d Vale.Interop.Views.up_view128 in
       Seq.equal
         (Seq.append (Seq.append (UV.as_seq h1 out128x6_u) (UV.as_seq h1 out128_u))
           (UV.as_seq h1 inout_u))
         (Seq.append (UV.as_seq h1 out_u) (UV.as_seq h1 inout_u)));

    c
  )


let lemma_identical_uv (b:uint8_p) (h0 h1:HS.mem) : Lemma
  (requires B.length b % 16 = 0 /\ Seq.equal (B.as_seq h0 b) (B.as_seq h1 b))
  (ensures (
    let b_d = get_downview b in
    length_aux3 b (B.length b / 16);
    let b_u = UV.mk_buffer b_d Vale.Interop.Views.up_view128 in
    Seq.equal (UV.as_seq h0 b_u) (UV.as_seq h1 b_u)))
  = lemma_dv_equal Vale.Interop.Views.down_view8 b h0 h1;
    length_aux3 b (B.length b / 16);
    lemma_uv_equal Vale.Interop.Views.up_view128 (get_downview b) h0 h1


let length_aux6 (b:uint8_p) : Lemma (B.length b = DV.length (get_downview b))
  = DV.length_eq (get_downview b)

#push-options "--z3cliopt smt.arith.nl=true"
let lemma_slice_uv_extra (b:uint8_p) (b_start:uint8_p) (b_extra:uint8_p) (h:HS.mem) : Lemma
  (requires
    B.length b_start = B.length b / 16 * 16 /\
    b_start == B.gsub b 0ul (UInt32.uint_to_t (B.length b_start)) /\
    B.length b_extra = 16 /\
    Seq.equal
      (B.as_seq h b)
      (Seq.slice (Seq.append (B.as_seq h b_start) (B.as_seq h b_extra)) 0 (B.length b))
    )
  (ensures (
    let b_start_d = get_downview b_start in
    length_aux6 b_start;
    let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
    let b_extra_d = get_downview b_extra in
    length_aux6 b_extra;
    let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
    let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
    let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
    Seq.equal sf (seq_uint8_to_seq_nat8 (B.as_seq h b))
val lemma_slice_uv_extra (b b_start b_extra: uint8_p) (h: HS.mem)
    : Lemma
      (requires
        B.length b_start = (B.length b / 16) * 16 /\
        b_start == B.gsub b 0ul (UInt32.uint_to_t (B.length b_start)) /\ B.length b_extra = 16 /\
        Seq.equal (B.as_seq h b)
          (Seq.slice (Seq.append (B.as_seq h b_start) (B.as_seq h b_extra)) 0 (B.length b)))
      (ensures
        (let b_start_d = get_downview b_start in
          length_aux6 b_start;
          let b_start_u = UV.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
          let b_extra_d = get_downview b_extra in
          length_aux6 b_extra;
          let b_extra_u = UV.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
          let suv = Seq.append (UV.as_seq h b_start_u) (UV.as_seq h b_extra_u) in
          let sf = wrap_slice (le_seq_quad32_to_bytes suv) (B.length b) in
          Seq.equal sf (seq_uint8_to_seq_nat8 (B.as_seq h b))))

    b: Vale.Wrapper.X64.GCMdecryptOpt.uint8_p ->
    b_start: Vale.Wrapper.X64.GCMdecryptOpt.uint8_p ->
    b_extra: Vale.Wrapper.X64.GCMdecryptOpt.uint8_p ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        LowStar.Monotonic.Buffer.length b_start = (LowStar.Monotonic.Buffer.length b / 16) * 16 /\
        b_start ==
        LowStar.Buffer.gsub b 0ul (FStar.UInt32.uint_to_t (LowStar.Monotonic.Buffer.length b_start)) /\
        LowStar.Monotonic.Buffer.length b_extra = 16 /\
        FStar.Seq.Base.equal (LowStar.Monotonic.Buffer.as_seq h b)
          (FStar.Seq.Base.slice (FStar.Seq.Base.append (LowStar.Monotonic.Buffer.as_seq h b_start)
                  (LowStar.Monotonic.Buffer.as_seq h b_extra))
              0
              (LowStar.Monotonic.Buffer.length b)))
      (ensures
        (let b_start_d = Vale.Interop.Types.get_downview b_start in
          [@@ FStar.Pervasives.inline_let ]let _ =
            Vale.Wrapper.X64.GCMdecryptOpt.length_aux6 b_start
          in
          let b_start_u = LowStar.BufferView.Up.mk_buffer b_start_d Vale.Interop.Views.up_view128 in
          let b_extra_d = Vale.Interop.Types.get_downview b_extra in
          [@@ FStar.Pervasives.inline_let ]let _ =
            Vale.Wrapper.X64.GCMdecryptOpt.length_aux6 b_extra
          in
          let b_extra_u = LowStar.BufferView.Up.mk_buffer b_extra_d Vale.Interop.Views.up_view128 in
          let suv =
            FStar.Seq.Base.append (LowStar.BufferView.Up.as_seq h b_start_u)
              (LowStar.BufferView.Up.as_seq h b_extra_u)
          in
          let sf =
            Vale.Wrapper.X64.GCMdecryptOpt.wrap_slice (Vale.Def.Types_s.le_seq_quad32_to_bytes suv)
              (LowStar.Monotonic.Buffer.length b)
          in
          FStar.Seq.Base.equal sf
            (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (LowStar.Monotonic.Buffer.as_seq h b))))