val 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))]
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)
val 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))]
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)
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
FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.loc QUIC.State.index QUIC.State.state_s LowStar.Monotonic.Buffer.loc_includes_union_l QUIC.State.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 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)))
val 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))]

    m: FStar.Monotonic.HyperStack.mem ->
    l1: LowStar.Monotonic.Buffer.loc ->
    l2: LowStar.Monotonic.Buffer.loc ->
    s: QUIC.State.state_s a
  -> FStar.Pervasives.Lemma
      (requires
        LowStar.Monotonic.Buffer.loc_includes l1 (QUIC.State.footprint_s m s) \/
        LowStar.Monotonic.Buffer.loc_includes l2 (QUIC.State.footprint_s m s))
      (ensures
        LowStar.Monotonic.Buffer.loc_includes (LowStar.Monotonic.Buffer.loc_union l1 l2)
          (QUIC.State.footprint_s m s))
      [
        SMTPat (LowStar.Monotonic.Buffer.loc_includes (LowStar.Monotonic.Buffer.loc_union l1 l2)
              (QUIC.State.footprint_s m s))
      ]