val gen (i:id) (u:info i) : ST (aead_writer i)
  (requires (fun h -> True))
  (ensures (fun h0 w h1 ->
    winvariant w h1 /\

    B.modifies B.loc_none h0 h1 /\
    B.fresh_loc (wfootprint w) h0 h1 /\
    B.(loc_includes (loc_ae_region ()) (wfootprint w)) /\

    wgetinfo w == u /\
    (I.ideal_AEAD && I.is_ae_honest i ==> wlog w h1 == Seq.empty)))
let gen i u =
  if is_safe i then
    let l: log #i u = Seq.empty #(entry i u) in
    ((| u, B.malloc q_ae_region l 1ul |) <: model_writer i)
  else
    let key_l = Spec.key_length u.alg in
    (u, random key_l) <: unsafe_writer i
val gen (i:id) (u:info i) : ST (aead_writer i)
  (requires (fun h -> True))
  (ensures (fun h0 w h1 ->
    winvariant w h1 /\

    B.modifies B.loc_none h0 h1 /\
    B.fresh_loc (wfootprint w) h0 h1 /\
    B.(loc_includes (loc_ae_region ()) (wfootprint w)) /\

    wgetinfo w == u /\
    (I.ideal_AEAD && I.is_ae_honest i ==> wlog w h1 == Seq.empty)))
let gen i u =
if is_safe i
then
  let l:log #i u = Seq.empty #(entry i u) in
  ((| u, B.malloc q_ae_region l 1ul |) <: model_writer i)
else
  let key_l = Spec.key_length u.alg in
  (u, random key_l) <: 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.info Model.AEAD.is_safe Prims.Mkdtuple2 LowStar.Buffer.pointer Model.AEAD.log Model.AEAD.model_writer LowStar.Buffer.malloc Mem.q_ae_region FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.v Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.freeable FStar.Seq.Base.empty Model.AEAD.entry Model.AEAD.aead_writer Prims.bool FStar.Pervasives.Native.Mktuple2 Spec.Agile.AEAD.kv Model.Indexing.ae_id_ginfo Model.AEAD.unsafe_writer Model.Helpers.random Model.Helpers.lbytes FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite Prims.op_GreaterThanOrEqual Spec.Agile.AEAD.key_length Model.AEAD.__proj__Mkinfo'__item__alg
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 }

let wgetinfo #i (u: aead_writer i) =
  if is_safe i then
    dfst (u <: model_writer i)
  else
    fst (u <: unsafe_writer i)

let rgetinfo #_ #w _ =
  wgetinfo w

let wlog #i w h =
  B.deref h (dsnd (w <: model_writer i))

let wkey #i w =
  snd (w <: unsafe_writer i)

let wfootprint #i w =
  if is_safe i then
    B.loc_addr_of_buffer (dsnd (w <: model_writer i))
  else
    B.loc_none

let winvariant #i w h =
  if is_safe i then
    B.live h (dsnd (w <: model_writer i))
  else
    True

let wframe_invariant #_ w h0 l h1 =
  ()

let frame_log #_ w h0 l h1 =
  ()
val gen (i:id) (u:info i) : ST (aead_writer i)
  (requires (fun h -> True))
  (ensures (fun h0 w h1 ->
    winvariant w h1 /\

    B.modifies B.loc_none h0 h1 /\
    B.fresh_loc (wfootprint w) h0 h1 /\
    B.(loc_includes (loc_ae_region ()) (wfootprint w)) /\

    wgetinfo w == u /\
    (I.ideal_AEAD && I.is_ae_honest i ==> wlog w h1 == Seq.empty)))
i: Model.AEAD.id -> u133: Model.AEAD.info i -> FStar.HyperStack.ST.ST (Model.AEAD.aead_writer i)