val dcid_len (h: header) : Tot U32.t
let dcid_len
  (h: header)
: Tot U32.t
= match h with
  | BShort rb spin phase cid cid_len packet_number_length ->
    cid_len
  | BLong version dcid dcil scid scil spec -> dcil
val dcid_len (h: header) : Tot U32.t
let dcid_len (h: header) : Tot U32.t =
match h with
| BShort rb spin phase cid cid_len packet_number_length -> cid_len
| BLong version dcid dcil scid scil spec -> dcil
QUIC.Impl.Header.Base.fst.checked
QUIC.UInt62.fst.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Base.fst.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.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.Int.Cast.fst.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
QUIC.Impl.Header.Base.fst
QUIC.Impl.Header.Base.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 QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Impl.Header.Base.long_header_specifics
module QUIC.Impl.Header.Base
open QUIC.Spec.Header.Base
include QUIC.Impl.Base

module B = LowStar.Buffer
module U8 = FStar.UInt8
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module Spec = QUIC.Spec.Header.Base
module PN = QUIC.Spec.PacketNumber.Base
module U62 = QUIC.UInt62
module Secret = QUIC.Secret.Int

/// Information stored in a QUIC header. This is a Low* type passed by value --
/// it's a little expensive. Consider passing it by reference in ``encrypt``?
///
/// Note that we try to follow the convention of buffer arguments followed by
/// their lengths.

(* NOTE: in the following header type, payload_and_pn_length contains the
length of the actual payload AND of the packet number. *)

(* NOTE: the header no longer contains the packet number, which is
part of the state, so that the client no longer needs to take care of
it *)

noeq type long_header_specifics =
  | BInitial:
    reserved_bits: secret_bitfield 2 ->
    payload_and_pn_length: payload_and_pn_length_t ->
    packet_number_length: PN.packet_number_length_t ->
    token: B.buffer U8.t -> (* I reordered those so that the extracted code for this type is a tagged union with common prefixes *)
    token_length: U32.t { let v = U32.v token_length in v == B.length token /\ 0 <= v /\ v <= token_max_len  } ->
    long_header_specifics
  | BZeroRTT:
    reserved_bits: secret_bitfield 2 ->
    payload_and_pn_length: payload_and_pn_length_t ->
    packet_number_length: PN.packet_number_length_t ->
    long_header_specifics
  | BHandshake:
    reserved_bits: secret_bitfield 2 ->
    payload_and_pn_length: payload_and_pn_length_t ->
    packet_number_length: PN.packet_number_length_t ->
    long_header_specifics
  | BRetry:
    unused: secret_bitfield 4 ->
    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 =
  | BLong:
    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
  | BShort:
    reserved_bits: secret_bitfield 2 ->
    spin: bool ->
    phase: secret_bitfield 1 -> // no secret bools in HACL*
    cid: B.buffer U8.t ->
    cid_len: U32.t{
      let l = U32.v cid_len in
      l == B.length cid /\
      0 <= l /\ l <= 20
    } ->
    packet_number_length: PN.packet_number_length_t ->
    header

let dcid_len
  (h: header)
val dcid_len (h: header) : Tot U32.t
h: QUIC.Impl.Header.Base.header -> FStar.UInt32.t