val length_aux (b: uint8_p)
    : Lemma (requires B.length b = 176) (ensures DV.length (get_downview b) % 16 = 0)
let length_aux (b:uint8_p) : Lemma
  (requires B.length b = 176)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db
val length_aux (b: uint8_p)
    : Lemma (requires B.length b = 176) (ensures DV.length (get_downview b) % 16 = 0)
let length_aux (b: uint8_p)
    : Lemma (requires B.length b = 176) (ensures DV.length (get_downview b) % 16 = 0) =
let db = get_downview b in
DV.length_eq db
Vale.Wrapper.X64.GCMdecryptOpt.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Interop.Base.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.OptPublic.fsti.checked Vale.AES.GHash_s.fst.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Vale.Wrapper.X64.GCMdecryptOpt.fsti
Vale.Wrapper.X64.GCMdecryptOpt.uint8_p LowStar.BufferView.Down.length_eq FStar.UInt8.t LowStar.BufferView.Down.buffer 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 Prims.op_Modulus LowStar.BufferView.Down.length Prims.Nil FStar.Pervasives.pattern
module Vale.Wrapper.X64.GCMdecryptOpt

open Vale.X64.CPU_Features_s
open FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
open Vale.AsLowStar.MemoryHelpers
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.AES.GCM_helpers
open Vale.AES.AES_s
open Vale.AES.GCM_s
open Vale.AES.GHash_s
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.Interop.Base
open Vale.Arch.Types
open Vale.AES.OptPublic

let uint8_p = B.buffer UInt8.t
let uint64 = UInt64.t

let disjoint_or_eq (b1 b2:uint8_p) = B.disjoint b1 b2 \/ b1 == b2

let length_aux (b:uint8_p) : Lemma
val length_aux (b: uint8_p)
    : Lemma (requires B.length b = 176) (ensures DV.length (get_downview b) % 16 = 0)
b: Vale.Wrapper.X64.GCMdecryptOpt.uint8_p
  -> FStar.Pervasives.Lemma (requires LowStar.Monotonic.Buffer.length b = 176)
      (ensures LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview b) % 16 = 0)