val log (#i: _) (u: info i) : Type0
let log #i (u: info i): Type0 =
  Seq.seq (entry i u)
val log (#i: _) (u: info i) : Type0
let log #i (u: info i) : Type0 =
Seq.seq (entry i u)
Model.AEAD.fst.checked
Spec.Agile.AEAD.fsti.checked QUIC.Spec.fsti.checked prims.fst.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Mem.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked
Model.AEAD.fst
Model.AEAD.id Model.AEAD.info FStar.Seq.Base.seq Model.AEAD.entry
module Model.AEAD

module HS = FStar.HyperStack
module I = Model.Indexing
module U32 = FStar.UInt32
module U128 = FStar.UInt128
module B = LowStar.Buffer
module Spec = Spec.Agile.AEAD

#set-options "--fuel 0 --ifuel 0"

open Mem
open LowStar.BufferOps
open Model.Helpers
val log (#i: _) (u: info i) : Type0
u95: Model.AEAD.info i -> Type0