val is_gctr_plain_LE (p: seq nat8) : prop0
let is_gctr_plain_LE (p:seq nat8) : prop0 = length p < pow2_32
val is_gctr_plain_LE (p: seq nat8) : prop0
let is_gctr_plain_LE (p: seq nat8) : prop0 =
length p < pow2_32
Vale.AES.GCTR_s.fst.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.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.GCTR_s.fst
FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Vale.Def.Words_s.pow2_32 Vale.Def.Prop_s.prop0
module Vale.AES.GCTR_s

// IMPORTANT: Following NIST's specification, this spec is written assuming a big-endian mapping from bytes to quad32s
//            Since the AES spec (AES_s) is in little-endian, we need to byteswap each time we call AES

open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open Vale.AES.AES_s
open FStar.Seq

// The max length of pow2_32 corresponds to the max length of buffers in Low*
val is_gctr_plain_LE (p: seq nat8) : prop0
p: FStar.Seq.Base.seq Vale.Def.Types_s.nat8 -> Vale.Def.Prop_s.prop0