val plain_repr (#i: unsafe_id) (#u: info i) (#l: at_least u) (p: plain u l)
    : Tot (r: Spec.lbytes l {r == plain_as_bytes p})
let plain_repr (#i: unsafe_id) (#u:info i) (#l:at_least u) (p:plain u l) : Tot (r:Spec.lbytes l{r == plain_as_bytes p}) =
  u.plain_pkg.repr i l p
val plain_repr (#i: unsafe_id) (#u: info i) (#l: at_least u) (p: plain u l)
    : Tot (r: Spec.lbytes l {r == plain_as_bytes p})
let plain_repr (#i: unsafe_id) (#u: info i) (#l: at_least u) (p: plain u l)
    : Tot (r: Spec.lbytes l {r == plain_as_bytes p}) =
u.plain_pkg.repr i l p
Model.AEAD.fsti.checked
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
Model.AEAD.unsafe_id Model.AEAD.info Model.AEAD.at_least Model.AEAD.plain Model.AEAD.__proj__PlainPkg__item__repr Model.AEAD.__proj__Mkinfo'__item__min_len Model.AEAD.id Model.AEAD.is_safe Model.AEAD.__proj__Mkinfo'__item__plain_pkg Spec.Agile.AEAD.lbytes Prims.eq2 Model.AEAD.plain_as_bytes
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;
}

let info (i:id) =
  info:info'{
    I.ae_id_ginfo i == info.alg /\
    I.ae_id_ghash i == info.halg
  }

/// Accessors for info
/// ------------------

// Accessor for the info type.
let at_least (#i:id) (u:info i) =
  plain_length_at_least u.min_len

let plain (#i:id) (u:info i) (l: at_least u) =
  u.plain_pkg.plain i l

let plain_as_bytes (#i:id) (#u:info i) (#l:at_least u) (p:plain u l) : GTot (Spec.lbytes l) =
  u.plain_pkg.as_bytes i l p
val plain_repr (#i: unsafe_id) (#u: info i) (#l: at_least u) (p: plain u l)
    : Tot (r: Spec.lbytes l {r == plain_as_bytes p})
p: Model.AEAD.plain u63 l -> r: Spec.Agile.AEAD.lbytes l {r == Model.AEAD.plain_as_bytes p}