val short_dcid_len_prop (short_dcid_len: short_dcid_len_t) (h: header) : GTot Type0
val short_dcid_len_prop (short_dcid_len: short_dcid_len_t) (h: header) : GTot Type0
let short_dcid_len_prop
  (short_dcid_len: short_dcid_len_t)
  (h: header)
: GTot Type0
= (PShort? h ==> dcid_len h == U32.v short_dcid_len)
module QUIC.Spec.Header.Public
include QUIC.Spec.Base

module LP = LowParse.Spec.Base
module U32 = FStar.UInt32
module U62 = QUIC.UInt62
module U64 = FStar.UInt64
module U8 = FStar.UInt8
module LPB = LowParse.BitFields
module FB = FStar.Bytes
module Cast = FStar.Int.Cast

noeq
type long_header_specifics =
| PInitial:
  (token: vlbytes 0 token_max_len) -> // arbitrary bound
  (payload_and_pn_length: payload_and_pn_length_t) ->
  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: vlbytes 0 20) -> // TODO: change bounds to drop instead of rejecting as invalid
  long_header_specifics

noeq
type header =
| PLong:
  (protected_bits: bitfield 4) ->
  (version: U32.t) ->
  (dcid: vlbytes 0 20) ->
  (scid: vlbytes 0 20) ->
  (spec: long_header_specifics) ->
  header
| PShort:
  (protected_bits: bitfield 5) ->
  (spin: bool) ->
  (dcid: vlbytes 0 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 nat =
  match h with
  | PLong _ _ dcid _ _ -> FB.length dcid
  | PShort _ _ dcid -> FB.length dcid
/
QUIC.UInt62.fst.checked QUIC.Spec.Base.fst.checked prims.fst.checked LowParse.Spec.Base.fsti.checked LowParse.BitFields.fsti.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.Bytes.fsti.checked
QUIC.Spec.Header.Public.fsti
short_dcid_len: QUIC.Spec.Base.short_dcid_len_t -> h: QUIC.Spec.Header.Public.header
  -> Prims.GTot Type0
QUIC.Spec.Base.short_dcid_len_t QUIC.Spec.Header.Public.header Prims.l_imp Prims.b2t QUIC.Spec.Header.Public.uu___is_PShort Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n QUIC.Spec.Header.Public.dcid_len FStar.UInt32.v
let short_dcid_len_prop (short_dcid_len: short_dcid_len_t) (h: header) : GTot Type0 =
  
(PShort? h ==> dcid_len h == U32.v short_dcid_len)