val header_encrypt_post
      (a: ea)
      (hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a))
      (h: header)
      (c: cbytes' (is_retry h))
      (cid_len: nat{cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h)})
    : Lemma
    (let x = Parse.format_header h in
      let y = x `Seq.append` c in
      let z = header_encrypt a hpk h c in
      Parse.header_len h + Seq.length c == Seq.length z /\
      (Seq.slice z (Parse.header_len h) (Seq.length z)) `Seq.equal` c /\
      MShort? h == (BF.get_bitfield (U8.v (Seq.index z 0)) 7 8 = 0) /\
      is_retry h == (not (MShort? h) && BF.get_bitfield (U8.v (Seq.index z 0)) 4 6 = 3) /\
      (if is_retry h then z == y else Parse.putative_pn_offset cid_len z == Some (Parse.pn_offset h)
      ))
val header_encrypt_post
      (a: ea)
      (hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a))
      (h: header)
      (c: cbytes' (is_retry h))
      (cid_len: nat{cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h)})
    : Lemma
    (let x = Parse.format_header h in
      let y = x `Seq.append` c in
      let z = header_encrypt a hpk h c in
      Parse.header_len h + Seq.length c == Seq.length z /\
      (Seq.slice z (Parse.header_len h) (Seq.length z)) `Seq.equal` c /\
      MShort? h == (BF.get_bitfield (U8.v (Seq.index z 0)) 7 8 = 0) /\
      is_retry h == (not (MShort? h) && BF.get_bitfield (U8.v (Seq.index z 0)) 4 6 = 3) /\
      (if is_retry h then z == y else Parse.putative_pn_offset cid_len z == Some (Parse.pn_offset h)
      ))
let header_encrypt_post
  (a:ea)
  (hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a))
  (h: header)
  (c: cbytes' (is_retry h))
  (cid_len: nat { cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h) })
: Lemma (
    let x = Parse.format_header h in
    let y = x `Seq.append` c in
    let z = header_encrypt a hpk h c in
    Parse.header_len h + Seq.length c == Seq.length z /\
    Seq.slice z (Parse.header_len h) (Seq.length z) `Seq.equal` c /\
    MShort? h == (BF.get_bitfield (U8.v (Seq.index z 0)) 7 8 = 0) /\
    is_retry h == (not (MShort? h) && BF.get_bitfield (U8.v (Seq.index z 0)) 4 6 = 3) /\ (
    if is_retry h
    then z == y
    else Parse.putative_pn_offset cid_len z == Some (Parse.pn_offset h)
  ))
= Parse.format_header_is_short h;
  Parse.format_header_is_retry h;
  if is_retry h
  then ()
  else begin
    Parse.format_header_pn_length h;
    let x = Parse.format_header h in
    let y = x `Seq.append` c in
    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 y 0 in
    let protected_bits = if MShort? h then 5 else 4 in
    let bf = BF.get_bitfield (U8.v f `FStar.UInt.logxor` U8.v (Seq.index mask 0)) 0 protected_bits in
    let f' = BF.set_bitfield (U8.v f) 0 protected_bits bf in
    let r = Lemmas.xor_inplace y pnmask pn_offset in
    let z = header_encrypt a hpk h c in
    assert (z == Seq.cons (U8.uint_to_t f') (Seq.slice r 1 (Seq.length r)));
    Lemmas.pointwise_op_slice_other U8.logxor y pnmask pn_offset 0 1;
    Lemmas.pointwise_op_slice_other U8.logxor y pnmask pn_offset 1 pn_offset;
    assert (pn_offset > 0);
    Lemmas.pointwise_op_slice_other U8.logxor y pnmask pn_offset (Parse.header_len h) (Seq.length y);
    assert (Seq.slice z (Parse.header_len h) (Seq.length z) `Seq.equal` Seq.slice y (Parse.header_len h) (Seq.length y));
    assert (U8.uint_to_t f' == Seq.index (Seq.slice z 0 1) 0);
    BF.get_bitfield_set_bitfield_other (U8.v f) 0 protected_bits bf 7 8;
    BF.get_bitfield_set_bitfield_other (U8.v f) 0 protected_bits bf protected_bits 8;
    if MLong? h
    then BF.get_bitfield_set_bitfield_other (U8.v f) 0 protected_bits bf 4 6;
    Parse.putative_pn_offset_correct h cid_len;
    Parse.putative_pn_offset_frame cid_len x y;
    Parse.putative_pn_offset_frame cid_len y z;
    ()
  end
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)

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

#push-options "--z3rlimit 256 --query_stats --z3cliopt smt.arith.nl=false"

#restart-solver
/
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) ->
    cid_len: Prims.nat{cid_len <= 20 /\ (MShort? h ==> cid_len == QUIC.Spec.Header.Base.dcid_len h)}
  -> FStar.Pervasives.Lemma
    (ensures
      (let x = QUIC.Spec.Header.Parse.format_header h in
        let y = FStar.Seq.Base.append x c in
        let z = QUIC.Spec.Header.header_encrypt a hpk h c in
        QUIC.Spec.Header.Base.header_len h + FStar.Seq.Base.length c == FStar.Seq.Base.length z /\
        FStar.Seq.Base.equal (FStar.Seq.Base.slice z
              (QUIC.Spec.Header.Base.header_len h)
              (FStar.Seq.Base.length z))
          c /\
        MShort? h ==
        (LowParse.BitFields.get_bitfield (FStar.UInt8.v (FStar.Seq.Base.index z 0)) 7 8 = 0) /\
        QUIC.Spec.Header.Base.is_retry h ==
        (Prims.op_Negation (MShort? h) &&
        LowParse.BitFields.get_bitfield (FStar.UInt8.v (FStar.Seq.Base.index z 0)) 4 6 = 3) /\
        (match QUIC.Spec.Header.Base.is_retry h with
          | true -> z == y
          | _ ->
            QUIC.Spec.Header.Parse.putative_pn_offset cid_len z ==
            FStar.Pervasives.Native.Some (QUIC.Spec.Header.Parse.pn_offset h))))
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.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.l_imp QUIC.Spec.Header.Base.uu___is_MShort Prims.eq2 QUIC.Spec.Header.Base.dcid_len Prims.bool Prims.unit QUIC.Spec.Header.Parse.putative_pn_offset_frame QUIC.Spec.Header.Parse.putative_pn_offset_correct QUIC.Spec.Header.Base.uu___is_MLong LowParse.BitFields.get_bitfield_set_bitfield_other FStar.UInt8.n FStar.UInt8.v Prims._assert FStar.UInt8.t FStar.UInt8.uint_to_t FStar.Seq.Base.index QUIC.Spec.Base.byte FStar.Seq.Base.slice FStar.Seq.Base.equal QUIC.Spec.Header.Base.header_len FStar.Seq.Base.length QUIC.Spec.Lemmas.pointwise_op_slice_other FStar.UInt8.logxor Prims.op_GreaterThan FStar.Seq.Base.seq FStar.Seq.Base.cons QUIC.Spec.Crypto.packet QUIC.Spec.Header.header_encrypt QUIC.Spec.Base.bytes QUIC.Spec.Lemmas.xor_inplace FStar.UInt.uint_t LowParse.BitFields.set_bitfield LowParse.BitFields.ubitfield Prims.op_Subtraction LowParse.BitFields.get_bitfield FStar.UInt.logxor Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.PUB 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.int QUIC.Secret.Int.Base.v Lib.IntTypes.U32 QUIC.Spec.Header.Base.pn_length Prims.op_LessThan Lib.IntTypes.v QUIC.Spec.Header.Parse.pn_offset FStar.Seq.Base.append QUIC.Spec.Base.lbytes QUIC.Spec.Header.Parse.format_header QUIC.Spec.Header.Parse.format_header_pn_length QUIC.Spec.Header.Parse.format_header_is_retry QUIC.Spec.Header.Parse.format_header_is_short Prims.l_True Prims.squash Prims.op_Equality Prims.op_AmpAmp Prims.op_Negation FStar.Pervasives.Native.option QUIC.Spec.Header.Parse.putative_pn_offset FStar.Pervasives.Native.Some Prims.logical Prims.Nil FStar.Pervasives.pattern
let header_encrypt_post
      (a: ea)
      (hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a))
      (h: header)
      (c: cbytes' (is_retry h))
      (cid_len: nat{cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h)})
    : Lemma
    (let x = Parse.format_header h in
      let y = x `Seq.append` c in
      let z = header_encrypt a hpk h c in
      Parse.header_len h + Seq.length c == Seq.length z /\
      (Seq.slice z (Parse.header_len h) (Seq.length z)) `Seq.equal` c /\
      MShort? h == (BF.get_bitfield (U8.v (Seq.index z 0)) 7 8 = 0) /\
      is_retry h == (not (MShort? h) && BF.get_bitfield (U8.v (Seq.index z 0)) 4 6 = 3) /\
      (if is_retry h then z == y else Parse.putative_pn_offset cid_len z == Some (Parse.pn_offset h)
      )) =
  
Parse.format_header_is_short h;
Parse.format_header_is_retry h;
if is_retry h
then ()
else
  (Parse.format_header_pn_length h;
    let x = Parse.format_header h in
    let y = x `Seq.append` c in
    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 y 0 in
    let protected_bits = if MShort? h then 5 else 4 in
    let bf =
      BF.get_bitfield ((U8.v f) `FStar.UInt.logxor` (U8.v (Seq.index mask 0))) 0 protected_bits
    in
    let f' = BF.set_bitfield (U8.v f) 0 protected_bits bf in
    let r = Lemmas.xor_inplace y pnmask pn_offset in
    let z = header_encrypt a hpk h c in
    assert (z == Seq.cons (U8.uint_to_t f') (Seq.slice r 1 (Seq.length r)));
    Lemmas.pointwise_op_slice_other U8.logxor y pnmask pn_offset 0 1;
    Lemmas.pointwise_op_slice_other U8.logxor y pnmask pn_offset 1 pn_offset;
    assert (pn_offset > 0);
    Lemmas.pointwise_op_slice_other U8.logxor y pnmask pn_offset (Parse.header_len h) (Seq.length y);
    assert ((Seq.slice z (Parse.header_len h) (Seq.length z))
        `Seq.equal`
        (Seq.slice y (Parse.header_len h) (Seq.length y)));
    assert (U8.uint_to_t f' == Seq.index (Seq.slice z 0 1) 0);
    BF.get_bitfield_set_bitfield_other (U8.v f) 0 protected_bits bf 7 8;
    BF.get_bitfield_set_bitfield_other (U8.v f) 0 protected_bits bf protected_bits 8;
    if MLong? h then BF.get_bitfield_set_bitfield_other (U8.v f) 0 protected_bits bf 4 6;
    Parse.putative_pn_offset_correct h cid_len;
    Parse.putative_pn_offset_frame cid_len x y;
    Parse.putative_pn_offset_frame cid_len y z;
    ())