val wrap_slice (#a: Type0) (s: Seq.seq a) (i: int) : Seq.seq a
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)
val wrap_slice (#a: Type0) (s: Seq.seq a) (i: int) : Seq.seq a
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)
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
FStar.Seq.Base.seq FStar.Integers.int FStar.Seq.Base.slice Prims.op_AmpAmp FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.Seq.Base.length Prims.bool Prims.nat Prims.b2t Prims.op_LessThanOrEqual
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
val wrap_slice (#a: Type0) (s: Seq.seq a) (i: int) : Seq.seq a
s: FStar.Seq.Base.seq a -> i: FStar.Integers.int -> FStar.Seq.Base.seq a