let plain_p a = p:B.buffer uint8 { B.length p <= max_length a }
let plain_p a =
p: B.buffer uint8 {B.length p <= max_length a}
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
Spec.Agile.AEAD.supported_alg LowStar.Buffer.buffer Spec.Agile.AEAD.uint8 Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Spec.Agile.AEAD.max_length
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)))
  [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s s))]
= B.loc_includes_union_l l1 l2 (footprint_s s)

/// The configuration preconditions
inline_for_extraction noextract
let config_pre a =
  match a with
  | AES128_GCM
  | AES256_GCM ->
      EverCrypt.TargetConfig.hacl_can_compile_vale /\
      Vale.X64.CPU_Features_s.(aesni_enabled /\ pclmulqdq_enabled /\ avx_enabled /\
                               movbe_enabled /\ sse_enabled)
  | CHACHA20_POLY1305 -> True
  | _ -> True

inline_for_extraction noextract
val invariant_s: (#a:alg) -> HS.mem -> state_s a -> Type0

inline_for_extraction noextract
let invariant (#a:alg) (m: HS.mem) (s: state a) =
  B.live m s /\
  B.(loc_disjoint (loc_addr_of_buffer s) (footprint_s (B.deref m s))) /\
  invariant_s m (B.get m s 0)

val invariant_loc_in_footprint
  (#a: alg)
  (s: state a)
  (m: HS.mem)
: Lemma
  (requires (invariant m s))
  (ensures (B.loc_in (footprint m s) m))
  [SMTPat (invariant m s)]

val frame_invariant: #a:alg -> l:B.loc -> s:state a -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant h0 s /\
    B.loc_disjoint l (footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant h1 s /\
    footprint h0 s == footprint h1 s))
  [ SMTPat (invariant h1 s); SMTPat (B.modifies l h0 h1) ]


/// Actual stateful API
/// -------------------

noextract
let bytes = Seq.seq uint8

[@@ Comment "Return the algorithm used in the AEAD state.

@param s State of the AEAD algorithm.

@return Algorithm used in the AEAD state."]
val alg_of_state (a: G.erased alg) (s: state (G.reveal a)): Stack alg
  (requires (fun h0 -> invariant #(G.reveal a) h0 s))
  (ensures (fun h0 a' h1 ->
    a' == G.reveal a /\
    h0 == h1))

/// The API is constructed in a way that one can always get the original key
/// value behind a state, any any memory.
val as_kv: (#a: alg) -> state_s a -> GTot (kv a)

inline_for_extraction noextract
let create_in_st (a: alg) =
  r:HS.rid ->
  dst:B.pointer (B.pointer_or_null (state_s a)) ->
  k:B.buffer uint8 { B.length k = key_length a } ->
  ST error_code
    (requires fun h0 ->
      ST.is_eternal_region r /\
      B.live h0 k /\ B.live h0 dst)
    (ensures fun h0 e h1 ->
      match e with
      | UnsupportedAlgorithm ->
          B.(modifies loc_none h0 h1)
      | Success ->
          let s = B.deref h1 dst in
          // Sanity
          is_supported_alg a /\
          not (B.g_is_null s) /\
          invariant h1 s /\

          // Memory stuff
          B.(modifies (loc_buffer dst) h0 h1) /\
          B.fresh_loc (footprint h1 s) h0 h1 /\
          B.(loc_includes (loc_region_only true r) (footprint h1 s)) /\
          freeable h1 s /\

          // Useful stuff
          as_kv (B.deref h1 s) == B.as_seq h0 k
      | _ -> False)

/// Same function as above, but in the StackInline effect, so that it is possible
/// to use AES GCM while staying in the Stack effect. In this case, the state should
/// be allocated/deallocated just before/after any encryption or decryption (which
/// is not very problematic during, for example, a handshake).
inline_for_extraction noextract
let alloca_st (a: alg) =
  k:B.buffer uint8 { B.length k = key_length a } ->
  StackInline (B.pointer (state_s a))
    (requires fun h0 ->
      B.live h0 k /\ config_pre a /\ is_supported_alg a)
    (ensures fun h0 s h1 ->
      // Sanity
      invariant h1 s /\

      // Memory stuff
      B.(modifies loc_none h0 h1) /\
      B.fresh_loc (footprint h1 s) h0 h1 /\
      B.live h1 s /\
      B.(loc_includes (loc_region_only true (HS.get_tip h1)) (footprint h1 s)) /\

      // Useful stuff
      as_kv (B.deref h1 s) == B.as_seq h0 k)


/// This function takes a pointer to a caller-allocated reference ``dst`` then,
/// if the algorithm is supported (on this platform), allocates a fresh state
/// and modifies ``dst`` to point to it. The key-value associated with this can
/// be obtained via ``kv (B.deref dst)``; as long as ``dst`` is not modified,
/// then the caller can derive that the ``kv`` remains the same, which will be
/// required for encrypt.
(** @type: true
*)
[@@ Comment "Create the required AEAD state for the algorithm.

Note: The caller must free the AEAD state by calling `EverCrypt_AEAD_free`.

@param a The argument `a` must be either of:
  * `Spec_Agile_AEAD_AES128_GCM` (KEY_LEN=16),
  * `Spec_Agile_AEAD_AES256_GCM` (KEY_LEN=32), or
  * `Spec_Agile_AEAD_CHACHA20_POLY1305` (KEY_LEN=32).
@param dst Pointer to a pointer where the address of the allocated AEAD state will be written to.
@param k Pointer to `KEY_LEN` bytes of memory where the key is read from. The size depends on the used algorithm, see above.

@return The function returns `EverCrypt_Error_Success` on success or
  `EverCrypt_Error_UnsupportedAlgorithm` in case of a bad algorithm identifier.
  (See `EverCrypt_Error.h`.)"]
val create_in: #a:alg -> create_in_st a

inline_for_extraction noextract
val alloca: #a:alg -> alloca_st a

/// Encryption (pre-allocated state)
/// --------------------------------

inline_for_extraction noextract
let iv_p a = iv:B.buffer uint8 { iv_length a (B.length iv)}

inline_for_extraction noextract
let ad_p a = ad:B.buffer uint8 { B.length ad <= max_length a }
val plain_p : a: Spec.Agile.AEAD.supported_alg -> Type0
a: Spec.Agile.AEAD.supported_alg -> Type0