val aad0_len:(x: UInt32.t{UInt32.v x = B.length aad0})
let aad0_len: (x:UInt32.t { UInt32.v x = B.length aad0 }) =
  0ul
val aad0_len:(x: UInt32.t{UInt32.v x = B.length aad0})
let aad0_len:(x: UInt32.t{UInt32.v x = B.length aad0}) =
0ul
Test.Vectors.Aes128Gcm.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.fst.checked
Test.Vectors.Aes128Gcm.fst
FStar.UInt32.__uint_to_t
module Test.Vectors.Aes128Gcm

module B = LowStar.Buffer

#set-options "--max_fuel 0 --max_ifuel 0"

let key0: (b: B.buffer UInt8.t { B.length b = 16 /\ B.recallable b }) =
  [@inline_let] let l = [ 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; ] in
  assert_norm (List.Tot.length l = 16);
  B.gcmalloc_of_list HyperStack.root l

inline_for_extraction let key0_len: (x:UInt32.t { UInt32.v x = B.length key0 }) =
  16ul

let nonce0: (b: B.buffer UInt8.t { B.length b = 12 /\ B.recallable b }) =
  [@inline_let] let l = [ 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; ] in
  assert_norm (List.Tot.length l = 12);
  B.gcmalloc_of_list HyperStack.root l

inline_for_extraction let nonce0_len: (x:UInt32.t { UInt32.v x = B.length nonce0 }) =
  12ul

let aad0: (b: B.buffer UInt8.t { B.length b = 0 /\ B.recallable b }) =
  [@inline_let] let l = [ ] in
  assert_norm (List.Tot.length l = 0);
  B.gcmalloc_of_list HyperStack.root l
val aad0_len:(x: UInt32.t{UInt32.v x = B.length aad0})
x: FStar.UInt32.t{FStar.UInt32.v x = LowStar.Monotonic.Buffer.length Test.Vectors.Aes128Gcm.aad0}