val aead_key_len : Prims.int
let aead_key_len = 16
module Zeta.Steel.Globals
open Steel.ST.Util
module A = Steel.ST.Array
module R = Steel.ST.Reference
module U8 = FStar.UInt8
/
Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.Globals.fsti
Prims.int
let aead_key_len =
  
16