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
  | BShort _ spin phase cid cid_len packet_number_length ->
    B.loc_buffer cid
  | BLong version dcid dcil scid scil spec ->
    (B.loc_buffer dcid `B.loc_union` B.loc_buffer scid) `B.loc_union`
    begin match spec with
    | BInitial _ payload_length packet_number_length token token_length ->
      B.loc_buffer token
    | BRetry unused odcid odcil ->
      B.loc_buffer odcid
    | _ -> B.loc_none
    end
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)
: 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

// inline_for_extraction
let is_retry
  (h: header)
: Tot bool
= BLong? h && BRetry? (BLong?.spec h)

// inline_for_extraction
let pn_length
  (h: header {~ (is_retry h)})
: Tot PN.packet_number_length_t
= match h with
  | BShort _ spin phase cid cid_len packet_number_length ->
    packet_number_length
  | BLong version dcid dcil scid scil spec ->
    begin match spec with
    | BInitial _ payload_and_pn_length packet_number_length token token_length ->
      packet_number_length
    | BZeroRTT _ payload_length packet_number_length ->
      packet_number_length
    | BHandshake _ payload_length packet_number_length ->
      packet_number_length
    end

// inline_for_extraction
let has_payload_length
  (h: header)
: Tot bool
= BLong? h && not (BRetry? (BLong?.spec h))

// inline_for_extraction
let payload_and_pn_length
  (h: header { has_payload_length h })
: Tot payload_and_pn_length_t
= match BLong?.spec h with
  | BInitial _ pl _ _ _ -> pl
  | BZeroRTT _ pl _ -> pl
  | BHandshake _ pl _ -> pl

// inline_for_extraction
let payload_length
  (h: header { has_payload_length h })
: Tot U62.secret
= Secret.to_u64 (payload_and_pn_length h) `Secret.sub` Secret.to_u64 (pn_length h)

module HS = FStar.HyperStack

let header_live (h: header) (m: HS.mem) : GTot Type0 =
  match h with
  | BShort _ spin phase cid cid_len packet_number_length ->
    B.live m cid
  | BLong version dcid dcil scid scil spec ->
    B.live m dcid /\ B.live m scid /\
    begin match spec with
    | BInitial _ payload_length packet_number_length token token_length ->
      B.live m token
    | BRetry unused odcid odcil ->
      B.live m odcid
    | _ -> True
    end
/
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
h: QUIC.Impl.Header.Base.header -> Prims.GTot LowStar.Monotonic.Buffer.loc
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 LowStar.Monotonic.Buffer.loc_buffer QUIC.Impl.Header.Base.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
| BShort _ spin phase cid cid_len packet_number_length -> B.loc_buffer cid
| BLong version dcid dcil scid scil spec ->
  ((B.loc_buffer dcid) `B.loc_union` (B.loc_buffer scid))
  `B.loc_union`
  (match spec with
    | BInitial _ payload_length packet_number_length token token_length -> B.loc_buffer token
    | BRetry unused odcid odcil -> B.loc_buffer odcid
    | _ -> B.loc_none)