val length_aux3 (b: uint8_p) (n: nat)
    : Lemma (requires B.length b = 16 * n) (ensures DV.length (get_downview b) % 16 = 0)
let length_aux3 (b:uint8_p) (n:nat) : Lemma
  (requires B.length b = 16 * n)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db;
    FStar.Math.Lemmas.cancel_mul_mod n 16
val length_aux3 (b: uint8_p) (n: nat)
    : Lemma (requires B.length b = 16 * n) (ensures DV.length (get_downview b) % 16 = 0)
let length_aux3 (b: uint8_p) (n: nat)
    : Lemma (requires B.length b = 16 * n) (ensures DV.length (get_downview b) % 16 = 0) =
let db = get_downview b in
DV.length_eq db;
FStar.Math.Lemmas.cancel_mul_mod n 16
Vale.Wrapper.X64.GCTR.fst.checked
Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Decls.fsti.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Stdcalls.X64.GCTR.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.UInt8.fsti.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.Calc.fsti.checked
Vale.Wrapper.X64.GCTR.fst
Vale.Wrapper.X64.GCTR.uint8_p Prims.nat FStar.Math.Lemmas.cancel_mul_mod Prims.unit 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.b2t Prims.op_Equality Prims.int LowStar.Monotonic.Buffer.length FStar.Mul.op_Star Prims.squash Prims.op_Modulus LowStar.BufferView.Down.length Prims.Nil FStar.Pervasives.pattern
module Vale.Wrapper.X64.GCTR

open FStar.Mul
open Vale.Stdcalls.X64.GCTR
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 Vale.Arch.Types

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)

let length_aux3 (b:uint8_p) (n:nat) : Lemma
val length_aux3 (b: uint8_p) (n: nat)
    : Lemma (requires B.length b = 16 * n) (ensures DV.length (get_downview b) % 16 = 0)
b: Vale.Wrapper.X64.GCTR.uint8_p -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires LowStar.Monotonic.Buffer.length b = 16 * n)
      (ensures LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview b) % 16 = 0)