val wgetinfo: #i:id -> aead_writer i -> Tot (info i)
let wgetinfo #i (u: aead_writer i) =
  if is_safe i then
    dfst (u <: model_writer i)
  else
    fst (u <: unsafe_writer i)
val wgetinfo: #i:id -> aead_writer i -> Tot (info i)
let wgetinfo #i (u: aead_writer i) =
if is_safe i then dfst (u <: model_writer i) else fst (u <: unsafe_writer i)
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.aead_writer Model.AEAD.is_safe FStar.Pervasives.dfst Model.AEAD.info LowStar.Buffer.pointer Model.AEAD.log Model.AEAD.model_writer Prims.bool FStar.Pervasives.Native.fst Spec.Agile.AEAD.kv Model.Indexing.ae_id_ginfo Model.AEAD.unsafe_writer
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

let log #i (u: info i): Type0 =
  Seq.seq (entry i u)

let model_writer i: Type u#1 =
  u:info i & B.pointer (log #i u)

let unsafe_writer i =
  info i & Spec.kv (I.ae_id_ginfo i)

let aead_writer (i: id): Type u#1 =
  if is_safe i then
    model_writer i
  else
    unsafe_writer i

let aead_reader #i (w: aead_writer i) =
  w':aead_writer i { w' == w }
val wgetinfo: #i:id -> aead_writer i -> Tot (info i)
u102: Model.AEAD.aead_writer i -> Model.AEAD.info i