val header_footprint (h: header) : GTot B.loc
val header_footprint (h: header) : GTot B.loc
let header_footprint (h: header) : GTot B.loc =
  match h with
  | PShort protected_bits spin cid cid_len ->
    B.loc_buffer cid
  | PLong protected_bits version dcid dcil scid scil spec ->
    B.loc_buffer dcid `B.loc_union` B.loc_buffer scid `B.loc_union`
    begin match spec with
    | PInitial payload_and_pn_length token token_length ->
      B.loc_buffer token
    | PRetry odcid odcil ->
      B.loc_buffer odcid
    | _ -> B.loc_none
    end
module QUIC.Impl.Header.Public
include QUIC.Spec.Header.Public
include QUIC.Impl.Base

module LP = LowParse.Low.Base
module U32 = FStar.UInt32
module S = QUIC.Spec.Header.Public
module B = LowStar.Buffer
module U8 = FStar.UInt8
module HS = FStar.HyperStack
module FB = FStar.Bytes
module U64 = FStar.UInt64
module HST = FStar.HyperStack.ST
module Secret = QUIC.Secret.Int

val validate_header
  (short_dcid_len: short_dcid_len_t)
: Tot (LP.validator (parse_header short_dcid_len))

noeq
type long_header_specifics =
| PInitial:
  (payload_and_pn_length: payload_and_pn_length_t) ->
  (token: B.buffer U8.t) ->
  (token_length: U32.t { let v = U32.v token_length in v == B.length token /\ 0 <= v /\ v <= token_max_len }) ->
  long_header_specifics
| PZeroRTT:
  (payload_and_pn_length: payload_and_pn_length_t) ->
  long_header_specifics
| PHandshake:
  (payload_and_pn_length: payload_and_pn_length_t) ->
  long_header_specifics
| PRetry:
  odcid: B.buffer U8.t ->
  odcil: U32.t { let v = U32.v odcil in v = B.length odcid /\ 0 <= v /\ v <= 20 } ->
  long_header_specifics

noeq
type header =
| PLong:
  (protected_bits: secret_bitfield 4) ->
  (version: U32.t) ->
  dcid: B.buffer U8.t ->
  dcil: U32.t { let v = U32.v dcil in v == B.length dcid /\ 0 <= v /\ v <= 20 } ->
  scid: B.buffer U8.t ->
  scil: U32.t { let v = U32.v scil in v == B.length scid /\ 0 <= v /\ v <= 20 } ->
  (spec: long_header_specifics) ->
  header
| PShort:
  (protected_bits: secret_bitfield 5) ->
  (spin: bool) ->
  cid: B.buffer U8.t ->
  cid_len: U32.t{
    let l = U32.v cid_len in
    l == B.length cid /\
    0 <= l /\ l <= 20
  } ->
  header

let is_retry
  (h: header)
: Tot bool
= if PShort? h
  then false
  else
    let spec = PLong?.spec h in
    PRetry? spec

let dcid_len (h: header) : Tot short_dcid_len_t =
  match h with
  | PLong _ _ _ dcil _ _ _ -> dcil
  | PShort _ _ _ dcil -> dcil

let header_live (h: header) (m: HS.mem) : GTot Type0 =
  match h with
  | PShort protected_bits spin cid cid_len ->
    B.live m cid
  | PLong protected_bits version dcid dcil scid scil spec ->
    B.live m dcid /\ B.live m scid /\
    begin match spec with
    | PInitial payload_and_pn_length token token_length ->
      B.live m token
    | PRetry odcid odcil ->
      B.live m odcid
    | _ -> True
    end
/
QUIC.Spec.Header.Public.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.Base.fst.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
QUIC.Impl.Header.Public.fsti
h: QUIC.Impl.Header.Public.header -> Prims.GTot LowStar.Monotonic.Buffer.loc
QUIC.Impl.Header.Public.header QUIC.Spec.Base.secret_bitfield Prims.bool LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t Prims.l_and Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Prims.op_LessThanOrEqual FStar.UInt.uint_t FStar.UInt32.v LowStar.Monotonic.Buffer.loc_buffer QUIC.Impl.Header.Public.long_header_specifics LowStar.Monotonic.Buffer.loc_union QUIC.Spec.Base.payload_and_pn_length_t QUIC.Spec.Base.token_max_len Prims.op_Equality LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.loc
let header_footprint (h: header) : GTot B.loc =
  
match h with
| PShort protected_bits spin cid cid_len -> B.loc_buffer cid
| PLong protected_bits version dcid dcil scid scil spec ->
  ((B.loc_buffer dcid) `B.loc_union` (B.loc_buffer scid))
  `B.loc_union`
  (match spec with
    | PInitial payload_and_pn_length token token_length -> B.loc_buffer token
    | PRetry odcid odcil -> B.loc_buffer odcid
    | _ -> B.loc_none)