val coerce_iv (i:id) (b:lbytes (iv_length i)) : Tot (iv i)
val coerce_iv (i:id) (b:lbytes (iv_length i)) : Tot (iv i)
let coerce_iv (i:id) (b:lbytes (iv_length i)) : Tot (iv i) = b
module MiTLS.AEADProvider
open MiTLS

open FStar.Heap
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Seq
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
open FStar.UInt32

module HS = FStar.HyperStack
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module E = MiTLS.EverCrypt
module LB = LowStar.Buffer
module CI = MiTLS.Crypto.Indexing
module Plain = MiTLS.Crypto.Plain
module CB = MiTLS.Crypto.Symmetric.Bytes

let iv (i:id) = lbytes (iv_length i)
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.Crypto.Symmetric.Bytes.fst.checked MiTLS.Crypto.Plain.fsti.checked MiTLS.Crypto.Indexing.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Bytes.fsti.checked
MiTLS.AEADProvider.fst
i: MiTLS.AEADProvider.id -> b: FStar.Bytes.lbytes (MiTLS.AEADProvider.iv_length i)
  -> MiTLS.AEADProvider.iv i
MiTLS.AEADProvider.id FStar.Bytes.lbytes MiTLS.AEADProvider.iv_length MiTLS.AEADProvider.iv
let coerce_iv (i: id) (b: lbytes (iv_length i)) : Tot (iv i) =
  
b