val decrypt
  (i: id)
  (#w: aead_writer i)
  (r: aead_reader w)
  (aad: ad (wgetinfo w))
  (n: nonce)
  (l:at_least (wgetinfo w))
  (c:cipher (wgetinfo w) l)
  : Stack (option (plain (rgetinfo r) l))
  (requires (fun h0 ->
    winvariant w h0))
  (ensures fun h0 res h1 ->
    winvariant w h1 /\
    B.modifies B.loc_none h0 h1 /\
    (is_safe i ==>
      // feels like we should state something more interesting, e.g. if we
      // take all the entries in the log that match this nonce, then there is
      // exactly one
      (match wentry_for_nonce w n h0 with
      | None -> None? res
      | Some (Entry n' aad' #l' p' c') ->
        // We know that n == n' here, owing to the definition of wentry_for_nonce.
        let matches = aad' == aad /\ c' == c /\ l == l' in
        (matches ==> res = Some p') /\
        (~matches ==> res = None)
      )
    ) /\
    (~ (is_safe i) ==> (
      let a: Spec.supported_alg = I.ae_id_ginfo i in
      let k: Spec.kv a = wkey w in
      let iv : Spec.iv a = Helpers.hide n in
      let maybe_plain = Spec.decrypt k iv aad c in
      match maybe_plain with
      | None -> None? res
      | Some p ->
          Some? res /\ (
          let p' = (wgetinfo w).plain_pkg.as_bytes i l (Some?.v res) in
          p == p')
    ))
  )
let decrypt i #w r aad n l c =
  if is_safe i then
    let w: model_writer i = w in
    let log = !*(dsnd w) in
    match Seq.find_l (nonce_filter w n) log with
    | None -> None
    | Some (Entry n' aad' #l' p' c') ->
        assert (n == n');
        if lbytes_eq aad aad' && lbytes_eq c c' && l = l' then
          Some p'
        else
          None
  else
    let a = (wgetinfo w).alg in
    let k: Spec.kv a = wkey w in
    match Spec.decrypt k (Helpers.hide n) aad c with
    | None -> None
    | Some p ->
        Some ((wgetinfo w).plain_pkg.mk i (Seq.length p) p)
val decrypt
  (i: id)
  (#w: aead_writer i)
  (r: aead_reader w)
  (aad: ad (wgetinfo w))
  (n: nonce)
  (l:at_least (wgetinfo w))
  (c:cipher (wgetinfo w) l)
  : Stack (option (plain (rgetinfo r) l))
  (requires (fun h0 ->
    winvariant w h0))
  (ensures fun h0 res h1 ->
    winvariant w h1 /\
    B.modifies B.loc_none h0 h1 /\
    (is_safe i ==>
      // feels like we should state something more interesting, e.g. if we
      // take all the entries in the log that match this nonce, then there is
      // exactly one
      (match wentry_for_nonce w n h0 with
      | None -> None? res
      | Some (Entry n' aad' #l' p' c') ->
        // We know that n == n' here, owing to the definition of wentry_for_nonce.
        let matches = aad' == aad /\ c' == c /\ l == l' in
        (matches ==> res = Some p') /\
        (~matches ==> res = None)
      )
    ) /\
    (~ (is_safe i) ==> (
      let a: Spec.supported_alg = I.ae_id_ginfo i in
      let k: Spec.kv a = wkey w in
      let iv : Spec.iv a = Helpers.hide n in
      let maybe_plain = Spec.decrypt k iv aad c in
      match maybe_plain with
      | None -> None? res
      | Some p ->
          Some? res /\ (
          let p' = (wgetinfo w).plain_pkg.as_bytes i l (Some?.v res) in
          p == p')
    ))
  )
let decrypt i #w r aad n l c =
if is_safe i
then
  let w:model_writer i = w in
  let log = !*(dsnd w) in
  match Seq.find_l (nonce_filter w n) log with
  | None -> None
  | Some (Entry n' aad' #l' p' c') ->
    assert (n == n');
    if lbytes_eq aad aad' && lbytes_eq c c' && l = l' then Some p' else None
else
  let a = (wgetinfo w).alg in
  let k:Spec.kv a = wkey w in
  match Spec.decrypt k (Helpers.hide n) aad c with
  | None -> None
  | Some p -> Some ((wgetinfo w).plain_pkg.mk i (Seq.length p) p)
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.aead_reader Model.AEAD.ad Model.AEAD.wgetinfo Model.AEAD.nonce Model.AEAD.at_least Model.AEAD.cipher Model.AEAD.is_safe FStar.Seq.Properties.find_l Model.AEAD.entry Prims.__proj__Mkdtuple2__item___1 Model.AEAD.info LowStar.Buffer.pointer Model.AEAD.log Model.AEAD.nonce_filter FStar.Pervasives.Native.None Model.AEAD.plain Model.AEAD.rgetinfo Prims.op_AmpAmp Model.Helpers.lbytes_eq Prims.op_Equality Model.AEAD.plain_length Prims.l_or Prims.b2t Prims.op_LessThanOrEqual Model.AEAD.__proj__Mkinfo'__item__min_len FStar.Pervasives.Native.Some Prims.bool FStar.Pervasives.Native.option Prims.unit Prims._assert Prims.eq2 LowStar.BufferOps.op_Bang_Star LowStar.Buffer.trivial_preorder FStar.Pervasives.dsnd Model.AEAD.model_writer Spec.Agile.AEAD.decrypt Model.Helpers.hide Spec.Agile.AEAD.decrypted Model.AEAD.__proj__PlainPkg__item__mk Model.AEAD.__proj__Mkinfo'__item__plain_pkg FStar.Seq.Base.length Spec.Agile.AEAD.uint8 Spec.Agile.AEAD.kv Model.AEAD.wkey Model.AEAD.alg 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 =
  ()

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

let gen_reader #i w =
  w

let coerce #i u kv =
  (u, kv) <: unsafe_writer i

// With QUIC-specific derivation of key from transport secret
let quic_coerce #i u ts =
  coerce u
    (QUIC.Spec.derive_secret u.halg ts
      QUIC.Spec.label_key (Spec.key_length u.alg))

let encrypt i w nonce aad plain_length plain =
  if is_safe i then
    let a = (wgetinfo w).alg in
    let w: model_writer i = w in
    let p = dsnd w in
    let log = !*p in
    let cipher_length = (plain_length <: nat) + Spec.tag_length a in
    let cipher = random cipher_length in
    p *= Seq.snoc log (Entry #i #(wgetinfo w) nonce aad #plain_length plain cipher);
    cipher
  else
    let a = (wgetinfo w).alg in
    let k: Spec.kv a = wkey w in
    let iv = Helpers.hide nonce in
    let p = (wgetinfo w).plain_pkg.repr i plain_length plain in
    Spec.encrypt #a k iv aad p
val decrypt
  (i: id)
  (#w: aead_writer i)
  (r: aead_reader w)
  (aad: ad (wgetinfo w))
  (n: nonce)
  (l:at_least (wgetinfo w))
  (c:cipher (wgetinfo w) l)
  : Stack (option (plain (rgetinfo r) l))
  (requires (fun h0 ->
    winvariant w h0))
  (ensures fun h0 res h1 ->
    winvariant w h1 /\
    B.modifies B.loc_none h0 h1 /\
    (is_safe i ==>
      // feels like we should state something more interesting, e.g. if we
      // take all the entries in the log that match this nonce, then there is
      // exactly one
      (match wentry_for_nonce w n h0 with
      | None -> None? res
      | Some (Entry n' aad' #l' p' c') ->
        // We know that n == n' here, owing to the definition of wentry_for_nonce.
        let matches = aad' == aad /\ c' == c /\ l == l' in
        (matches ==> res = Some p') /\
        (~matches ==> res = None)
      )
    ) /\
    (~ (is_safe i) ==> (
      let a: Spec.supported_alg = I.ae_id_ginfo i in
      let k: Spec.kv a = wkey w in
      let iv : Spec.iv a = Helpers.hide n in
      let maybe_plain = Spec.decrypt k iv aad c in
      match maybe_plain with
      | None -> None? res
      | Some p ->
          Some? res /\ (
          let p' = (wgetinfo w).plain_pkg.as_bytes i l (Some?.v res) in
          p == p')
    ))
  )

    i: Model.AEAD.id ->
    r: Model.AEAD.aead_reader w ->
    aad: Model.AEAD.ad (Model.AEAD.wgetinfo w) ->
    n: Model.AEAD.nonce ->
    l: Model.AEAD.at_least (Model.AEAD.wgetinfo w) ->
    c: Model.AEAD.cipher (Model.AEAD.wgetinfo w) l
  -> FStar.HyperStack.ST.Stack
    (FStar.Pervasives.Native.option (Model.AEAD.plain (Model.AEAD.rgetinfo r) l))