val header_encrypt_ct_correct
      (a: ea)
      (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
      (h: Spec.header)
      (c: cbytes' (Spec.is_retry h))
    : Lemma ((header_encrypt_ct a hpk h c) `Seq.equal` (Spec.header_encrypt a hpk h c))
val header_encrypt_ct_correct
      (a: ea)
      (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
      (h: Spec.header)
      (c: cbytes' (Spec.is_retry h))
    : Lemma ((header_encrypt_ct a hpk h c) `Seq.equal` (Spec.header_encrypt a hpk h c))
let header_encrypt_ct_correct
  (a:ea)
  (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
  (h: Spec.header)
  (c: cbytes' (Spec.is_retry h))
: Lemma
  (header_encrypt_ct a hpk h c `Seq.equal` Spec.header_encrypt a hpk h c)
=
  assert_norm(max_cipher_length < pow2 62);
  let r = Parse.format_header h `Seq.append` c in
  if Spec.is_retry h
  then ()
  else begin
    let pn_offset = Parse.pn_offset h in
    let pn_len = Secret.v (Parse.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 (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk sample) in
    let pnmask_ct = Lemmas.and_inplace (Seq.slice mask 1 5) (pn_sizemask_ct pn_len) 0 in
    let pnmask_naive = Lemmas.and_inplace (Seq.slice mask 1 (pn_len + 2)) (Spec.pn_sizemask pn_len) 0 in
    Lemmas.pointwise_op_split U8.logand (Seq.slice mask 1 5) (pn_sizemask_ct pn_len) 0 (pn_len + 1);
    assert (pnmask_naive `Seq.equal` Seq.slice pnmask_ct 0 (pn_len + 1));
    Seq.lemma_split r (pn_offset + pn_len + 1);
    Lemmas.pointwise_op_split U8.logxor r pnmask_ct pn_offset (pn_offset + pn_len + 1);
    Lemmas.pointwise_op_split U8.logxor r pnmask_naive pn_offset (pn_offset + pn_len + 1);
    Lemmas.pointwise_op_empty U8.logxor (Seq.slice r (pn_offset + pn_len + 1) (Seq.length r)) (Seq.slice pnmask_naive (pn_len + 1) (Seq.length pnmask_naive)) 0;
    Lemmas.xor_inplace_zero (Seq.slice r (pn_offset + pn_len + 1) (Seq.length r)) (Seq.slice pnmask_ct (pn_len + 1) 4)
      (fun i ->
        Lemmas.and_inplace_zero
          (Seq.slice mask (pn_len + 2) 5)
          (Seq.slice (pn_sizemask_ct pn_len) (pn_len + 1) 4)
          (fun j -> index_pn_sizemask_ct_right pn_len (j + (pn_len + 1)))
          i
      )
      0
  end
module QUIC.Impl.Header
friend QUIC.Spec.Header

open QUIC.Impl.Header.Base

module Parse = QUIC.Spec.Header.Parse
module ParseImpl = QUIC.Impl.Header.Parse
module Spec = QUIC.Spec.Header
module PN = QUIC.Spec.PacketNumber.Base

module B = LowStar.Buffer

module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF

module U8 = FStar.UInt8
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module G = FStar.Ghost
module Seq = QUIC.Secret.Seq
module Secret = QUIC.Secret.Int
module SecretBuffer = QUIC.Secret.Buffer

module Lemmas = QUIC.Impl.Lemmas
module BF = LowParse.BitFields

module SCipher = Spec.Agile.Cipher
module SAEAD = Spec.Agile.AEAD

(* There are a few places where EverCrypt needs public data whereas it
could/should be secret. Thus, we may need some declassification
locally using Lib.RawIntTypes, but we definitely don't want to make
secret integers globally transparent using friend *)

module ADMITDeclassify = Lib.RawIntTypes

let block_len (a: SCipher.cipher_alg):
  x:U32.t { U32.v x = SCipher.block_length a }
=
  let open SCipher in
  match a with | CHACHA20 -> 64ul | _ -> 16ul

#push-options "--z3rlimit 256"
inline_for_extraction
let block_of_sample (a: SCipher.cipher_alg)
  (dst: B.buffer Secret.uint8)
  (s: CTR.state a)
  (k: B.buffer Secret.uint8)
  (sample: B.buffer Secret.uint8):
  HST.Stack unit
    (requires fun h0 ->
      B.(all_live h0 [ buf dst; buf k; buf sample ]) /\
      CTR.invariant h0 s /\
      B.(all_disjoint
        [ CTR.footprint h0 s; loc_buffer dst; loc_buffer k; loc_buffer sample ]) /\
      SCipher.(a == AES128 \/ a == AES256 \/ a == CHACHA20) /\
      B.length k = SCipher.key_length a /\
      B.length dst = 16 /\
      B.length sample = 16)
    (ensures fun h0 _ h1 ->
      B.(modifies (loc_buffer dst `loc_union` CTR.footprint h0 s) h0 h1) /\
      B.as_seq h1 dst `Seq.equal`
        Spec.block_of_sample a (B.as_seq h0 k) (B.as_seq h0 sample) /\
      CTR.footprint h0 s == CTR.footprint h1 s /\
      CTR.invariant h1 s)
=
  HST.push_frame ();
  (**) let h0 = HST.get () in
  let zeroes' = B.alloca (Secret.to_u8 0uy) 64ul in
  let zeroes = B.sub zeroes' 0ul (block_len a) in
  let dst_block' = B.alloca (Secret.to_u8 0uy) 64ul in
  let dst_block = B.sub dst_block' 0ul (block_len a) in
  begin match a with
  | SCipher.CHACHA20 ->
      let ctr = SecretBuffer.load32_le (B.sub sample 0ul 4ul) in
      let iv = B.sub sample 4ul 12ul in
      (**) let h1 = HST.get () in
      (* EverCrypt currently does not support secret counters,
         so we need to declassify the counter value here and only here. *)
      CTR.init (G.hide a) s k iv 12ul (ADMITDeclassify.u32_to_UInt32 ctr);
      CTR.update_block (G.hide a) s dst_block zeroes;
      (**) let h2 = HST.get () in
      (**) Lemmas.seq_map2_xor0 (B.as_seq h1 dst_block)
      (**)   (SCipher.ctr_block a (B.as_seq h0 k) (B.as_seq h1 iv) (Secret.v ctr));
      (**) assert (B.as_seq h2 dst_block `Seq.equal`
      (**)   SCipher.ctr_block a (B.as_seq h0 k) (B.as_seq h1 iv) (Secret.v ctr));
      let dst_slice = B.sub dst_block 0ul 16ul in
      (**) assert (B.as_seq h2 dst_slice `Seq.equal` Seq.slice (
      (**)   SCipher.ctr_block a (B.as_seq h0 k) (B.as_seq h1 iv) (Secret.v ctr)
      (**) ) 0 16);
      B.blit dst_slice 0ul dst 0ul 16ul
  | _ ->
      let ctr = SecretBuffer.load32_be (B.sub sample 12ul 4ul) in
      let iv = B.sub sample 0ul 12ul in
      (**) let h1 = HST.get () in
      (* EverCrypt currently does not support secret counters,
         so we need to declassify the counter value here and only here. *)
      CTR.init (G.hide a) s k iv 12ul (ADMITDeclassify.u32_to_UInt32 ctr);
      CTR.update_block (G.hide a) s dst_block zeroes;
      (**) let h2 = HST.get () in
      (**) Lemmas.seq_map2_xor0 (B.as_seq h1 dst_block)
      (**)   (SCipher.ctr_block a (B.as_seq h0 k) (B.as_seq h1 iv) (Secret.v ctr));
      (**) assert (B.as_seq h2 dst_block `Seq.equal`
      (**)   SCipher.ctr_block a (B.as_seq h0 k) (B.as_seq h1 iv) (Secret.v ctr));
      let dst_slice = B.sub dst_block 0ul 16ul in
      (**) assert (B.as_seq h2 dst_slice `Seq.equal` Seq.slice (
      (**)   SCipher.ctr_block a (B.as_seq h0 k) (B.as_seq h1 iv) (Secret.v ctr)
      (**) ) 0 16);
      B.blit dst_slice 0ul dst 0ul 16ul
  end;
  HST.pop_frame ()
#pop-options

(* A more careful version of header_encrypt wrt. constant-time issues, which does not test or truncate on pn_len *)

let pn_sizemask_ct (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 index_pn_sizemask_ct_right
  (pn_len: nat { pn_len < 4 })
  (i: nat {i > pn_len /\ i < 4})
: Lemma
  (Seq.index (pn_sizemask_ct pn_len) i == 0uy)
= let open FStar.Endianness in
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  pow2_lt_compat 32 (24 - (8 `op_Multiply` pn_len));
  pow2_plus (24 - (8 * pn_len)) (8 * (pn_len + 1));
  Lemmas.index_n_to_be_zero_right 4 (pow2 32 - pow2 (24 - (8 * pn_len))) i

let header_encrypt_ct
  (a:ea)
  (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
  (h: Spec.header)
  (c: cbytes' (Spec.is_retry h))
: GTot packet
= 
  assert_norm(max_cipher_length < pow2 62);
  let r = Parse.format_header h `Seq.append` c in
  if Spec.is_retry h
  then
    r
  else
    let pn_offset = Parse.pn_offset h in
    let pn_len = Secret.v (Spec.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 (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk sample) in
    let pnmask = Lemmas.and_inplace (Seq.slice mask 1 5) (pn_sizemask_ct pn_len) 0 in
    let f = Seq.index r 0 in
    let protected_bits = if Spec.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"
/
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.fst.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.Lemmas.fsti.checked QUIC.Impl.Header.Parse.fsti.checked QUIC.Impl.Header.Base.fst.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.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.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.Impl.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)
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.equal (QUIC.Impl.Header.header_encrypt_ct a hpk h c)
        (QUIC.Spec.Header.header_encrypt a hpk h c))
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 QUIC.Spec.Lemmas.xor_inplace_zero FStar.Seq.Base.slice QUIC.Spec.Base.byte Prims.op_Addition FStar.Seq.Base.length Prims.nat Prims.b2t Prims.op_LessThan QUIC.Spec.Lemmas.and_inplace_zero Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.PUB QUIC.Impl.Header.pn_sizemask_ct QUIC.Impl.Header.index_pn_sizemask_ct_right Prims.unit QUIC.Spec.Lemmas.pointwise_op_empty FStar.UInt8.logxor QUIC.Spec.Lemmas.pointwise_op_split FStar.Seq.Properties.lemma_split Prims._assert FStar.Seq.Base.equal FStar.UInt8.logand QUIC.Spec.Base.bytes QUIC.Spec.Lemmas.and_inplace QUIC.Spec.Header.pn_sizemask FStar.Seq.Base.seq 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.l_and Prims.eq2 Lib.IntTypes.v QUIC.Spec.Header.Base.header_len QUIC.Spec.Header.Parse.pn_offset FStar.Seq.Base.append QUIC.Spec.Header.Parse.format_header FStar.Pervasives.assert_norm QUIC.Spec.Crypto.max_cipher_length Prims.pow2 Prims.l_True Prims.squash QUIC.Impl.Header.header_encrypt_ct QUIC.Spec.Header.header_encrypt Prims.Nil FStar.Pervasives.pattern
let header_encrypt_ct_correct
      (a: ea)
      (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
      (h: Spec.header)
      (c: cbytes' (Spec.is_retry h))
    : Lemma ((header_encrypt_ct a hpk h c) `Seq.equal` (Spec.header_encrypt a hpk h c)) =
  
assert_norm (max_cipher_length < pow2 62);
let r = (Parse.format_header h) `Seq.append` c in
if Spec.is_retry h
then ()
else
  let pn_offset = Parse.pn_offset h in
  let pn_len = Secret.v (Parse.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 (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk sample)
  in
  let pnmask_ct = Lemmas.and_inplace (Seq.slice mask 1 5) (pn_sizemask_ct pn_len) 0 in
  let pnmask_naive =
    Lemmas.and_inplace (Seq.slice mask 1 (pn_len + 2)) (Spec.pn_sizemask pn_len) 0
  in
  Lemmas.pointwise_op_split U8.logand (Seq.slice mask 1 5) (pn_sizemask_ct pn_len) 0 (pn_len + 1);
  assert (pnmask_naive `Seq.equal` (Seq.slice pnmask_ct 0 (pn_len + 1)));
  Seq.lemma_split r (pn_offset + pn_len + 1);
  Lemmas.pointwise_op_split U8.logxor r pnmask_ct pn_offset (pn_offset + pn_len + 1);
  Lemmas.pointwise_op_split U8.logxor r pnmask_naive pn_offset (pn_offset + pn_len + 1);
  Lemmas.pointwise_op_empty U8.logxor
    (Seq.slice r (pn_offset + pn_len + 1) (Seq.length r))
    (Seq.slice pnmask_naive (pn_len + 1) (Seq.length pnmask_naive))
    0;
  Lemmas.xor_inplace_zero (Seq.slice r (pn_offset + pn_len + 1) (Seq.length r))
    (Seq.slice pnmask_ct (pn_len + 1) 4)
    (fun i ->
        Lemmas.and_inplace_zero (Seq.slice mask (pn_len + 2) 5)
          (Seq.slice (pn_sizemask_ct pn_len) (pn_len + 1) 4)
          (fun j -> index_pn_sizemask_ct_right pn_len (j + (pn_len + 1)))
          i)
    0