val make_gctr_plain_LE (p: seq nat8) : seq nat8
let make_gctr_plain_LE (p:seq nat8) : seq nat8 =
  if length p < pow2_32 then p else empty
val make_gctr_plain_LE (p: seq nat8) : seq nat8
let make_gctr_plain_LE (p: seq nat8) : seq nat8 =
if length p < pow2_32 then p else empty
Vale.AES.GCTR.fsti.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.AES.GCTR.fsti
FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.op_LessThan FStar.Seq.Base.length Vale.Def.Words_s.pow2_32 Prims.bool FStar.Seq.Base.empty
module Vale.AES.GCTR

open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Mul
open FStar.Seq
open Vale.AES.AES_s
open Vale.AES.GCTR_s
open Vale.AES.GCM_helpers
open FStar.Math.Lemmas
open Vale.Lib.Seqs
val make_gctr_plain_LE (p: seq nat8) : seq nat8
p: FStar.Seq.Base.seq Vale.Def.Types_s.nat8 -> FStar.Seq.Base.seq Vale.Def.Types_s.nat8