val length_div (b: uint8_p)
    : Lemma (requires B.length b = 16) (ensures DV.length (get_downview b) / 16 = 1)
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)
val length_div (b: uint8_p)
    : Lemma (requires B.length b = 16) (ensures DV.length (get_downview b) / 16 = 1)
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)
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 LowStar.BufferView.Down.length_eq FStar.UInt8.t Vale.Interop.Types.get_downview Vale.Arch.HeapTypes_s.TUInt8 LowStar.Buffer.trivial_preorder Prims.unit Prims.b2t Prims.op_Equality Prims.int LowStar.Monotonic.Buffer.length Prims.squash FStar.Integers.op_Slash FStar.Integers.Signed FStar.Integers.Winfinite LowStar.BufferView.Down.length Prims.Nil 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)
val length_div (b: uint8_p)
    : Lemma (requires B.length b = 16) (ensures DV.length (get_downview b) / 16 = 1)
b: Vale.Wrapper.X64.GCMdecryptOpt.uint8_p
  -> FStar.Pervasives.Lemma (requires LowStar.Monotonic.Buffer.length b = 16)
      (ensures LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview b) / 16 = 1)