let bytes_to_quad_size (num_bytes:nat) =
  ((num_bytes + 15) / 16)
let bytes_to_quad_size (num_bytes: nat) =
((num_bytes + 15) / 16)
Vale.AES.GCM_helpers.fsti.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.AES.GCM_helpers.fsti
Prims.nat Prims.op_Division Prims.op_Addition Prims.int
module Vale.AES.GCM_helpers

open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Four_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 FStar.Math.Lemmas
open Vale.Lib.Seqs
val bytes_to_quad_size : num_bytes: Prims.nat -> Prims.int
num_bytes: Prims.nat -> Prims.int