val aead_key_buffer_t : Type0
let aead_key_buffer_t = k:A.array U8.t { A.length k == aead_key_len }
module Zeta.Steel.Globals
open Steel.ST.Util
module A = Steel.ST.Array
module R = Steel.ST.Reference
module U8 = FStar.UInt8

let aead_key_len = 16
/
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
Type0
Steel.ST.Array.array FStar.UInt8.t Prims.eq2 Prims.int Steel.ST.Array.length Zeta.Steel.Globals.aead_key_len
let aead_key_buffer_t =
  
k: A.array U8.t {A.length k == aead_key_len}