val info : i: Model.AEAD.id -> Type
let info (i:id) =
  info:info'{
    I.ae_id_ginfo i == info.alg /\
    I.ae_id_ghash i == info.halg
  }
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

/// Abbreviations for idealization
/// ------------------------------

// In this module, id is an AEAD id.
let id = I.ae_id

// ea = encryption alg
let alg = I.ea

let is_safe i =
  I.ideal_AEAD && I.is_ae_honest i

let safe_id =
  i:id{is_safe i}

let unsafe_id =
  i:id{~ (is_safe i)}

/// Some redefinitions, using Spec
/// ------------------------------

// Trying to follow the conventions: _len for machine lengths,
// _length for spec (nat) lengths.
let tag_len: x:U32.t { forall (a: alg). {:pattern Spec.tag_length a} U32.v x == Spec.tag_length a } =
  16ul

// This duplicates a fair amount of definitions from Spec.Agile.AEAD, but here
// the bounds are tighter and force plain texts to not overflow 32 bits once
// encrypted and tagged.
//
// Introducing a minimum length allows making sure that there are enough bytes
// to sample out of the ciphertext, as the tag can be too small for that purpose
// for some AEAD ciphersuites.
type plain_length = l:nat{l + U32.v tag_len < pow2 32}
type plain_length_at_least (lmin: plain_length) = l:plain_length{lmin <= l}

/// Packages, info (?)
/// ------------------

noeq
type plain_pkg (min_len:plain_length) (idt: eqtype) (safe: idt -> bool) =
  | PlainPkg:
    plain: (i:idt -> plain_length_at_least min_len -> eqtype) ->
    as_bytes: (i:idt -> l:plain_length_at_least min_len -> plain i l -> GTot (Spec.lbytes l)) ->
    repr: (i:idt{not (safe i)} -> l:plain_length_at_least min_len -> p:plain i l -> Tot (b:Spec.lbytes l{b == as_bytes i l p})) ->
    mk: (i:idt{not (safe i)} -> l:plain_length_at_least min_len -> p:Spec.lbytes l -> p':plain i l { as_bytes i l p' == p }) ->
    plain_pkg min_len idt safe

noeq type info' = {
  alg: alg;
  halg: I.ha;
  min_len: plain_length;
  plain_pkg: plain_pkg min_len id is_safe;
}
/
Spec.Hash.Definitions.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.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked
Model.AEAD.fsti
i: Model.AEAD.id -> Type
Model.AEAD.id Model.AEAD.info' Prims.l_and Prims.eq2 Model.Indexing.ea Model.Indexing.ae_id_ginfo Model.AEAD.__proj__Mkinfo'__item__alg Model.Indexing.ha Model.Indexing.ae_id_ghash Model.AEAD.__proj__Mkinfo'__item__halg
let info (i: id) =
  
info: info'{I.ae_id_ginfo i == info.alg /\ I.ae_id_ghash i == info.halg}