val hash_is_keysized (#i: _) (s: state_s i)
    : Lemma (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
      [SMTPat (g_traffic_secret s)]
let hash_is_keysized #i (s: state_s i): Lemma
  (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
  [ SMTPat (g_traffic_secret s) ]
=
  assert_norm (512 < pow2 61);
  assert_norm (512 < pow2 125)
val hash_is_keysized (#i: _) (s: state_s i)
    : Lemma (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
      [SMTPat (g_traffic_secret s)]
let hash_is_keysized #i (s: state_s i)
    : Lemma (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
      [SMTPat (g_traffic_secret s)] =
assert_norm (512 < pow2 61);
assert_norm (512 < pow2 125)
QUIC.State.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Crypto.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.Header.Base.fst.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Error.fsti.checked
QUIC.State.fsti
QUIC.State.index QUIC.State.state_s FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 Prims.unit Prims.l_True Prims.squash QUIC.Spec.Crypto.keysized QUIC.State.__proj__Mkindex__item__hash_alg FStar.Seq.Base.length Lib.IntTypes.uint8 QUIC.State.g_traffic_secret Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Spec.Hash.Definitions.bytes_hash Prims.Nil
module QUIC.State

open EverCrypt.Error
include QUIC.Spec.Crypto
include QUIC.Impl.Header.Base

module B = LowStar.Buffer
module HS = FStar.HyperStack
module Seq = QUIC.Secret.Seq
module PN = QUIC.Spec.PacketNumber.Base
module HST = FStar.HyperStack.ST
module Secret = QUIC.Secret.Int
module G = FStar.Ghost
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module Base = QUIC.Impl.Header.Base
module Spec = QUIC.Spec

#set-options "--z3rlimit 16"

/// This is not a cryptographic index; rather, this is just a regular type
/// index, where instead of indexing on a single algorithm (like, say, AEAD), we
/// index on two values.
///
/// The record is here to limit the profileration of hide/reveal in the stateful
/// functions, and to give easier projectors (, ).
type index = {
  hash_alg: ha;
  aead_alg: ea
}


/// Boilerplate
/// -----------

[@CAbstractStruct]
val state_s: index -> Type0

let state i = B.pointer (state_s i)

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

let loc_includes_union_l_footprint_s
  (m: HS.mem)
  (l1 l2: B.loc) (#a: index) (s: state_s a)
: Lemma
  (requires (
    B.loc_includes l1 (footprint_s m s) \/ B.loc_includes l2 (footprint_s m s)
  ))
  (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s m s)))
  [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s m s))]
= B.loc_includes_union_l l1 l2 (footprint_s m s)

/// Ghost accessors (not needing the invariant)
/// -------------------------------------------
///
/// We need to define those, so that we can state a framing lemma for them.
/// Attempting a new convention to distinguish ghost accessors from stateful
/// functions: a ``g_`` prefix.

/// See remark for ``g_initial_packet_number`` below.
val g_traffic_secret: #i:index -> (s: state_s i) ->
  GTot (Spec.Hash.Definitions.bytes_hash i.hash_alg)

#push-options "--max_ifuel 1" // inversion on hash_alg
let hash_is_keysized #i (s: state_s i): Lemma
  (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
  [ SMTPat (g_traffic_secret s) ]
val hash_is_keysized (#i: _) (s: state_s i)
    : Lemma (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
      [SMTPat (g_traffic_secret s)]
s: QUIC.State.state_s i
  -> FStar.Pervasives.Lemma
      (ensures
        QUIC.Spec.Crypto.keysized (Mkindex?.hash_alg i)
          (FStar.Seq.Base.length (QUIC.State.g_traffic_secret s)))
      [SMTPat (QUIC.State.g_traffic_secret s)]