val is_retry (h: header) : Tot bool
let is_retry
  (h: header)
: Tot bool
= if PShort? h
  then false
  else
    let spec = PLong?.spec h in
    PRetry? spec
val is_retry (h: header) : Tot bool
let is_retry (h: header) : Tot bool =
if PShort? h
then false
else
  let spec = PLong?.spec h in
  PRetry? spec
QUIC.Impl.Header.Public.fsti.checked
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
QUIC.Impl.Header.Public.header QUIC.Impl.Header.Public.uu___is_PShort Prims.bool QUIC.Impl.Header.Public.uu___is_PRetry QUIC.Impl.Header.Public.long_header_specifics QUIC.Impl.Header.Public.__proj__PLong__item__spec
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)
val is_retry (h: header) : Tot bool
h: QUIC.Impl.Header.Public.header -> Prims.bool