val header_encrypt:
  a:ea ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  c: cbytes' (is_retry h) ->
  GTot packet
val header_encrypt:
  a:ea ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  c: cbytes' (is_retry h) ->
  GTot packet
let header_encrypt
  a hpk h c
=
  assert_norm(max_cipher_length < pow2 62);
  let r = Parse.format_header h `Seq.append` c in
  if is_retry h
  then
    r
  else
    let pn_offset = Parse.pn_offset h in
    let pn_len = Secret.v (pn_length h) - 1 in
    let sample = Seq.seq_hide (Seq.slice c (3-pn_len) (19-pn_len)) in
    let mask = Seq.seq_reveal (block_of_sample (AEAD.cipher_alg_of_supported_alg a) hpk sample) in
    let pnmask = Lemmas.and_inplace (Seq.slice mask 1 (pn_len + 2)) (pn_sizemask pn_len) 0 in
    let f = Seq.index r 0 in
    let protected_bits = if MShort? h then 5 else 4 in
    let f' = BF.set_bitfield (U8.v f) 0 protected_bits (BF.get_bitfield (U8.v f `FStar.UInt.logxor` U8.v (Seq.index mask 0)) 0 protected_bits) in
    let r = Lemmas.xor_inplace r pnmask pn_offset in
    let r = Seq.cons (U8.uint_to_t f') (Seq.slice r 1 (Seq.length r)) in
    r
module QUIC.Spec.Header

module PN = QUIC.Spec.PacketNumber
module Secret = QUIC.Secret.Int
module BF = LowParse.BitFields
module U8 = FStar.UInt8
module Seq = QUIC.Secret.Seq
module U64 = FStar.UInt64
module Parse = QUIC.Spec.Header.Parse

module AEAD = Spec.Agile.AEAD
module Cipher = Spec.Agile.Cipher
module Lemmas = QUIC.Spec.Lemmas

let block_of_sample
  (a: Cipher.cipher_alg)
  (k: Cipher.key a)
  (sample: Seq.lseq Secret.uint8 16)
: GTot (Seq.lseq Secret.uint8 16) =
  let open FStar.Mul in
  let ctr, iv = match a with
    | Cipher.CHACHA20 ->
        let ctr_bytes, iv = Seq.split sample 4 in
        FStar.Endianness.lemma_le_to_n_is_bounded (Seq.seq_reveal ctr_bytes);
        assert_norm (pow2 (8 * 4) = pow2 32);
        FStar.Endianness.le_to_n (Seq.seq_reveal ctr_bytes), iv
    | _ ->
        let iv, ctr_bytes = Seq.split sample 12 in
        FStar.Endianness.lemma_be_to_n_is_bounded (Seq.seq_reveal ctr_bytes);
        assert_norm (pow2 (8 * 4) = pow2 32);
        FStar.Endianness.be_to_n (Seq.seq_reveal ctr_bytes), iv
  in
  (Seq.slice (Cipher.ctr_block a k iv ctr) 0 16)

(*
Decryption of packet number
packet[pn_offset..pn_offset+4] ^= pn_mask &
  match pn_len with
  | 0 -> mask & 0xFF000000
  | 1 -> mask & 0xFFFF0000
  | 2 -> mask & 0xFFFFFF00
  | 3 -> mask & 0xFFFFFFFF
*)
let pn_sizemask' (pn_len: nat { pn_len < 4 }) : Tot (lbytes 4) =
  let open FStar.Endianness in
  FStar.Math.Lemmas.pow2_lt_compat 32 (24 - (8 `op_Multiply` pn_len));
  FStar.Endianness.n_to_be 4 (pow2 32 - pow2 (24 - (8 `op_Multiply` pn_len)))

let pn_sizemask (pn_len: nat { pn_len < 4 }) : Tot (lbytes (pn_len + 1)) =
  Seq.slice (pn_sizemask' pn_len) 0 (pn_len + 1)
/
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.fsti.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fsti.checked
QUIC.Spec.Header.fst

    a: QUIC.Spec.Crypto.ea ->
    hpk: Spec.Agile.Cipher.key (Spec.Agile.AEAD.cipher_alg_of_supported_alg a) ->
    h: QUIC.Spec.Header.Base.header ->
    c: QUIC.Spec.Crypto.cbytes' (QUIC.Spec.Header.Base.is_retry h)
  -> Prims.GTot QUIC.Spec.Crypto.packet
QUIC.Spec.Crypto.ea Spec.Agile.Cipher.key Spec.Agile.AEAD.cipher_alg_of_supported_alg QUIC.Spec.Header.Base.header QUIC.Spec.Crypto.cbytes' QUIC.Spec.Header.Base.is_retry Prims.bool FStar.Seq.Base.seq QUIC.Spec.Base.byte FStar.Seq.Base.cons FStar.UInt8.uint_to_t FStar.Seq.Base.slice FStar.Seq.Base.length QUIC.Spec.Base.bytes QUIC.Spec.Lemmas.xor_inplace FStar.UInt.uint_t LowParse.BitFields.set_bitfield FStar.UInt8.n FStar.UInt8.v LowParse.BitFields.get_bitfield FStar.UInt.logxor FStar.Seq.Base.index Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.PUB Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual QUIC.Spec.Header.Base.uu___is_MShort QUIC.Spec.Lemmas.and_inplace Prims.op_Addition QUIC.Spec.Header.pn_sizemask Lib.IntTypes.int_t QUIC.Secret.Seq.seq_reveal Lib.IntTypes.SEC QUIC.Spec.Header.block_of_sample QUIC.Secret.Seq.seq_hide Prims.op_Subtraction Prims.int QUIC.Secret.Int.Base.v Lib.IntTypes.U32 QUIC.Spec.Header.Base.pn_length Prims.op_LessThan Prims.eq2 Lib.IntTypes.v QUIC.Spec.Header.Base.header_len QUIC.Spec.Header.Parse.pn_offset QUIC.Spec.Crypto.packet FStar.Seq.Base.append QUIC.Spec.Header.Parse.format_header Prims.unit FStar.Pervasives.assert_norm QUIC.Spec.Crypto.max_cipher_length Prims.pow2
let header_encrypt a hpk h c =
  
assert_norm (max_cipher_length < pow2 62);
let r = (Parse.format_header h) `Seq.append` c in
if is_retry h
then r
else
  let pn_offset = Parse.pn_offset h in
  let pn_len = Secret.v (pn_length h) - 1 in
  let sample = Seq.seq_hide (Seq.slice c (3 - pn_len) (19 - pn_len)) in
  let mask = Seq.seq_reveal (block_of_sample (AEAD.cipher_alg_of_supported_alg a) hpk sample) in
  let pnmask = Lemmas.and_inplace (Seq.slice mask 1 (pn_len + 2)) (pn_sizemask pn_len) 0 in
  let f = Seq.index r 0 in
  let protected_bits = if MShort? h then 5 else 4 in
  let f' =
    BF.set_bitfield (U8.v f)
      0
      protected_bits
      (BF.get_bitfield ((U8.v f) `FStar.UInt.logxor` (U8.v (Seq.index mask 0))) 0 protected_bits)
  in
  let r = Lemmas.xor_inplace r pnmask pn_offset in
  let r = Seq.cons (U8.uint_to_t f') (Seq.slice r 1 (Seq.length r)) in
  r