val loc_includes_union_l_footprint_s (l1 l2: B.loc) (#a: alg) (s: state_s a)
    : Lemma (requires (B.loc_includes l1 (footprint_s s) \/ B.loc_includes l2 (footprint_s s)))
      (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s s)))
      [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s s))]
let loc_includes_union_l_footprint_s
  (l1 l2: B.loc) (#a: alg) (s: state_s a)
: Lemma
  (requires (
    B.loc_includes l1 (footprint_s s) \/ B.loc_includes l2 (footprint_s s)
  ))
  (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s s)))
  [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s s))]
= B.loc_includes_union_l l1 l2 (footprint_s s)
val loc_includes_union_l_footprint_s (l1 l2: B.loc) (#a: alg) (s: state_s a)
    : Lemma (requires (B.loc_includes l1 (footprint_s s) \/ B.loc_includes l2 (footprint_s s)))
      (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s s)))
      [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s s))]
let loc_includes_union_l_footprint_s (l1 l2: B.loc) (#a: alg) (s: state_s a)
    : Lemma (requires (B.loc_includes l1 (footprint_s s) \/ B.loc_includes l2 (footprint_s s)))
      (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s s)))
      [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s s))] =
B.loc_includes_union_l l1 l2 (footprint_s s)
EverCrypt.AEAD.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.TargetConfig.fsti.checked EverCrypt.Error.fsti.checked
EverCrypt.AEAD.fsti
LowStar.Monotonic.Buffer.loc Spec.Agile.AEAD.alg EverCrypt.AEAD.state_s LowStar.Monotonic.Buffer.loc_includes_union_l EverCrypt.AEAD.footprint_s Prims.unit Prims.l_or LowStar.Monotonic.Buffer.loc_includes Prims.squash LowStar.Monotonic.Buffer.loc_union Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module EverCrypt.AEAD

/// The new AEAD interface for EverCrypt, which supersedes the functions found
/// in EverCrypt.fst
///
/// The expected usage for this module is as follows:
/// - client expands key, obtaining an ``expanded_key a``
/// - client uses ``encrypt``/``decrypt`` with the same ``expanded_key a`` repeatedly.
///
/// This usage protocol is enforced for verified F* clients but, naturally,
/// isn't for C clients.

module S = FStar.Seq
module G = FStar.Ghost

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module B = LowStar.Buffer

open FStar.HyperStack.ST
open FStar.Integers

open Spec.Agile.AEAD
module Spec = Spec.Agile.AEAD
open EverCrypt.Error

/// Note: if the fst and the fsti are running on different fuel settings,
/// something that works in the interactive mode for the fsti, when
/// "re-interpreted" in the fst, might stop working!
#set-options "--max_fuel 0 --max_ifuel 0"


/// Abstract footprints, with the same machinery as EverCrypt.Hash
/// --------------------------------------------------------------
///
/// Differences from EverCrypt.Hash include: combined framing lemma, the
/// equivalent of the ``repr`` function does *not* require the memory, and order
/// of arguments to be in line with ``B.as_seq``, etc. which take the memory
/// first.

[@@ CAbstractStruct; Comment "Both encryption and decryption require a state that holds the key.
The state may be reused as many times as desired."]
val state_s: alg -> Type0

inline_for_extraction noextract
let state alg = B.pointer (state_s alg)

inline_for_extraction noextract
val freeable_s: #(a: alg) -> state_s a -> Type0

inline_for_extraction noextract
let freeable (#a: alg) (h: HS.mem) (p: state a) =
  B.freeable p /\ freeable_s (B.deref h p)

inline_for_extraction noextract
let preserves_freeable #a (s: state a) (h0 h1: HS.mem): Type0 =
  freeable h0 s ==> freeable h1 s

val footprint_s: #a:alg -> state_s a -> GTot B.loc
let footprint (#a:alg) (m: HS.mem) (s: state a) =
  B.(loc_union (loc_addr_of_buffer s) (footprint_s (B.deref m s)))

// TR: the following pattern is necessary because, if we generically
// add such a pattern directly on `loc_includes_union_l`, then
// verification will blowup whenever both sides of `loc_includes` are
// `loc_union`s. We would like to break all unions on the
// right-hand-side of `loc_includes` first, using
// `loc_includes_union_r`.  Here the pattern is on `footprint_s`,
// because we already expose the fact that `footprint` is a
// `loc_union`. (In other words, the pattern should be on every
// smallest location that is not exposed to be a `loc_union`.)

let loc_includes_union_l_footprint_s
  (l1 l2: B.loc) (#a: alg) (s: state_s a)
: Lemma
  (requires (
    B.loc_includes l1 (footprint_s s) \/ B.loc_includes l2 (footprint_s s)
  ))
  (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s s)))
val loc_includes_union_l_footprint_s (l1 l2: B.loc) (#a: alg) (s: state_s a)
    : Lemma (requires (B.loc_includes l1 (footprint_s s) \/ B.loc_includes l2 (footprint_s s)))
      (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s s)))
      [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s s))]
l1: LowStar.Monotonic.Buffer.loc -> l2: LowStar.Monotonic.Buffer.loc -> s: EverCrypt.AEAD.state_s a
  -> FStar.Pervasives.Lemma
      (requires
        LowStar.Monotonic.Buffer.loc_includes l1 (EverCrypt.AEAD.footprint_s s) \/
        LowStar.Monotonic.Buffer.loc_includes l2 (EverCrypt.AEAD.footprint_s s))
      (ensures
        LowStar.Monotonic.Buffer.loc_includes (LowStar.Monotonic.Buffer.loc_union l1 l2)
          (EverCrypt.AEAD.footprint_s s))
      [
        SMTPat (LowStar.Monotonic.Buffer.loc_includes (LowStar.Monotonic.Buffer.loc_union l1 l2)
              (EverCrypt.AEAD.footprint_s s))
      ]