val header_decrypt_aux_ct_correct
      (a: ea)
      (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
      (cid_len: nat{cid_len <= 20})
      (packet: packet)
    : Lemma
    (header_decrypt_aux_ct a hpk cid_len packet == Spec.header_decrypt_aux a hpk cid_len packet)
val header_decrypt_aux_ct_correct
      (a: ea)
      (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
      (cid_len: nat{cid_len <= 20})
      (packet: packet)
    : Lemma
    (header_decrypt_aux_ct a hpk cid_len packet == Spec.header_decrypt_aux a hpk cid_len packet)
let header_decrypt_aux_ct_correct
  (a:ea)
  (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
  (cid_len: nat { cid_len <= 20 })
  (packet: packet)
: Lemma
  (header_decrypt_aux_ct a hpk cid_len packet == Spec.header_decrypt_aux a hpk cid_len packet)
= 
  let open FStar.Math.Lemmas in
  if Seq.length packet = 0
  then ()
  else
    let f = Seq.index packet 0 in
    let is_short = (BF.get_bitfield (U8.v f) 7 8 = 0) in
    let is_retry = not is_short && BF.get_bitfield (U8.v f) 4 6 = 3 in
    if is_retry
    then ()
    else
      match Parse.putative_pn_offset cid_len packet with
      | None -> ()
      | Some pn_offset ->
        let sample_offset = pn_offset + 4 in
        if sample_offset + 16 > Seq.length packet
        then ()
        else begin
          let sample = Seq.slice packet sample_offset (sample_offset+16) in
          let mask = Seq.seq_reveal #Secret.U8 (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk (Seq.seq_hide #Secret.U8 sample)) in
          (* mask the least significant bits of the first byte *)
          let protected_bits = if is_short 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 packet' = Seq.cons (U8.uint_to_t f') (Seq.slice packet 1 (Seq.length packet)) in
          (* now the packet number length is available, so mask the packet number *)
          let pn_len = BF.get_bitfield f' 0 2 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));
          let r = packet' in
          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"

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

#pop-options

#push-options "--z3rlimit 16"

let header_encrypt_ct_secret_preserving_not_retry_spec
  (a:ea)
  (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
  (h: Spec.header { ~ (Spec.is_retry h) })
  (r: Seq.seq Secret.uint8 {
    Seq.length r >= Parse.pn_offset h + 20
  })
: GTot (Seq.seq Secret.uint8)
= 
  let pn_offset = Parse.pn_offset h in
  let pn_len = Secret.v (Spec.pn_length h) - 1 in
  let sample = (Seq.slice r (pn_offset + 4) (pn_offset + 20)) in
  let mask = (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk sample) in
  let pnmask = Lemmas.secret_and_inplace (Seq.slice mask 1 5) (Seq.seq_hide (pn_sizemask_ct pn_len)) 0 in
  let f = Seq.index r 0 in
  let protected_bits = if Spec.MShort? h then 5ul else 4ul in
  let f' = Secret.set_bitfield f 0ul protected_bits (Secret.get_bitfield (f `Secret.logxor` Seq.index mask 0) 0ul protected_bits) in
  let r = Lemmas.secret_xor_inplace r pnmask pn_offset in
  let r = Seq.cons f' (Seq.slice r 1 (Seq.length r)) in
  r

#pop-options

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

#restart-solver

let header_encrypt_ct_secret_preserving_not_retry_spec_correct
  (a:ea)
  (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
  (h: Spec.header)
  (c: cbytes)
: Lemma
  (requires (
    (~ (Spec.is_retry h))
  ))
  (ensures (
    let r = Parse.format_header h `Seq.append` c in
    Seq.length r >= Parse.pn_offset h + 20 /\
    Spec.header_encrypt a hpk h c == Seq.seq_reveal (header_encrypt_ct_secret_preserving_not_retry_spec a hpk h (Seq.seq_hide r))
  ))
= header_encrypt_ct_correct a hpk h c;
  let fmt = Parse.format_header h in
  let len = Seq.length fmt in
  let pr = fmt `Seq.append` c in
  assert (Seq.length pr >= Parse.pn_offset h + 20);
  let pn_len = Secret.v (Spec.pn_length h) - 1 in
  let psample = Seq.slice c (3 - pn_len) (19 - pn_len) in
  assert (c `Seq.equal` Seq.slice pr len (Seq.length pr));
  let pn_off = Parse.pn_offset h in
  assert (pn_off + pn_len + 1 == len);
  assert (c == Seq.slice pr (pn_off + pn_len + 1) (Seq.length pr));
  Seq.slice_slice pr (pn_off + pn_len + 1) (Seq.length pr) (3 - pn_len) (19 - pn_len);
  assert (psample == Seq.slice pr (pn_off + 4) (pn_off + 20));
  let r = Seq.seq_hide #Secret.U8 pr in
  let sample = Seq.slice r (pn_off + 4) (pn_off + 20) in
  assert (sample == Seq.seq_hide #Secret.U8 psample);
  let mask = Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk sample in
  let pmask = Seq.seq_reveal mask in
  assert (mask == Seq.seq_hide pmask);
  let mask15 = Seq.slice mask 1 5 in
  let ppnszmask = pn_sizemask_ct pn_len in
  let pnszmask = Seq.seq_hide ppnszmask in
  let pnmask = Lemmas.secret_and_inplace mask15 pnszmask 0 in
  let pmask15 = Seq.slice pmask 1 5 in
  let ppnmask = Lemmas.and_inplace pmask15 ppnszmask 0 in
  Lemmas.secret_and_inplace_eq mask15 pnszmask 0;
  assert (pnmask == Seq.seq_hide #Secret.U8 ppnmask);
  let f = Seq.index r 0 in
  let pf : Secret.uint_t Secret.U8 Secret.PUB = Seq.index pr 0 in
  assert (f == Secret.hide #Secret.U8 #Secret.PUB pf);
  let protected_bits = if Spec.MShort? h then 5ul else 4ul in
  let pf' = U8.uint_to_t (BF.set_bitfield (U8.v pf) 0 (U32.v protected_bits) (BF.get_bitfield (U8.v pf `FStar.UInt.logxor` U8.v (Seq.index pmask 0)) 0 (U32.v protected_bits))) in
  let f' = Secret.set_bitfield f 0ul protected_bits (Secret.get_bitfield (f `Secret.logxor` Seq.index mask 0) 0ul protected_bits) in
  assert (U8.v pf' == Secret.v f');
  assert (f' == Secret.hide #Secret.U8 pf');
  let pr1 = Lemmas.xor_inplace pr ppnmask pn_off in
  let r1 = Lemmas.secret_xor_inplace r pnmask pn_off in
  Lemmas.secret_xor_inplace_eq r pnmask pn_off;
  assert (r1 == Seq.seq_hide #Secret.U8 pr1);
  let r2 = Seq.cons f' (Seq.slice r1 1 (Seq.length r1)) in
  let pr2 = Seq.cons pf' (Seq.slice pr1 1 (Seq.length pr1)) in
  Seq.cons_seq_hide #Secret.U8 pf' (Seq.slice pr1 1 (Seq.length pr1));
  assert (r2 == Seq.seq_hide #Secret.U8 pr2)

#pop-options

#push-options "--z3rlimit 32"

#restart-solver

[@"opaque_to_smt"]
let pn_sizemask_ct_num
  (pn_len: PN.packet_number_length_t)
: Tot (x: Secret.uint32 { pn_sizemask_ct (Secret.v pn_len - 1) == FStar.Endianness.n_to_be 4 (Secret.v x) })
=
  FStar.Math.Lemmas.pow2_lt_compat 32 (24 - (8 `op_Multiply` (Secret.v pn_len - 1)));
  [@inline_let]
  let n0 = norm [delta; zeta; iota; primops] (pow2 32 - pow2 24) in
  [@inline_let]
  let n1 = norm [delta; zeta; iota; primops] (pow2 32 - pow2 16) in
  [@inline_let]
  let n2 = norm [delta; zeta; iota; primops] (pow2 32 - pow2 8) in
  [@inline_let]
  let n3 = norm [delta; zeta; iota; primops] (pow2 32 - pow2 0) in
  let pn_len_1 = pn_len `Secret.sub` Secret.to_u32 1ul in
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 0ul) `Secret.mul` Secret.to_u32 (U32.uint_to_t n0)) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 1ul) `Secret.mul` Secret.to_u32 (U32.uint_to_t n1)) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 2ul) `Secret.mul` Secret.to_u32 (U32.uint_to_t n2)) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 3ul) `Secret.mul` Secret.to_u32 (U32.uint_to_t n3))

#pop-options

inline_for_extraction
noextract
let pn_sizemask (dst: B.buffer Secret.uint8) (pn_len: PN.packet_number_length_t): HST.Stack unit
  (requires fun h0 ->
    B.live h0 dst /\ B.length dst == 4)
  (ensures fun h0 _ h1 ->
    B.as_seq h1 dst `Seq.equal` Seq.seq_hide (pn_sizemask_ct (Secret.v pn_len - 1)) /\
    B.(modifies (loc_buffer dst) h0 h1))
= let x = pn_sizemask_ct_num pn_len in
  SecretBuffer.store32_be dst x

#push-options "--z3rlimit 512 --query_stats --z3cliopt smt.arith.nl=false --fuel 2 --ifuel 1"

#restart-solver

let header_encrypt_ct_secret_preserving_not_retry
  (a: ea)
  (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (k: B.buffer Secret.uint8)
  (h: Ghost.erased Spec.header)
  (is_short: bool)
  (pn_offset: U32.t)
  (pn_len: PN.packet_number_length_t)
  (dst: B.buffer Secret.uint8)
: HST.Stack unit
  (requires (fun m ->
    let fmt = (Parse.format_header h) in
    let hlen = Seq.length fmt in
    B.all_live m [B.buf k; B.buf dst] /\
    CTR.invariant m s /\
    B.all_disjoint
      [ CTR.footprint m s; B.loc_buffer k; B.loc_buffer dst] /\
    B.length k == SCipher.key_length (SAEAD.cipher_alg_of_supported_alg a) /\
    (~ (Spec.is_retry h)) /\
    is_short == (Spec.MShort? h) /\
    U32.v pn_offset == Parse.pn_offset h /\
    pn_len == Parse.pn_length h /\
    hlen + 19 <= B.length dst /\
    Seq.slice (Seq.seq_reveal #Secret.U8 (B.as_seq m dst)) 0 hlen == fmt
  ))
  (ensures (fun m _ m' ->
    B.modifies (B.loc_buffer dst `B.loc_union` CTR.footprint m s) m m' /\
    CTR.invariant m' s /\
    CTR.footprint m s == CTR.footprint m' s /\
    header_encrypt_ct_secret_preserving_not_retry_spec a (B.as_seq m k) h (B.as_seq m dst) == B.as_seq m' dst
  ))
= assert (U32.v pn_offset + 20 <= B.length dst);
  let m0 = HST.get () in
  HST.push_frame ();
  let m01 = HST.get () in
  let mask = B.alloca (Secret.to_u8 0uy) 16ul in
  B.loc_unused_in_not_unused_in_disjoint m01;
  let m02 = HST.get () in
  B.loc_unused_in_not_unused_in_disjoint m02;
  let pn_sm = B.alloca (Secret.to_u8 0uy) 4ul in
  let m03 = HST.get () in
  assert (B.loc_disjoint (B.loc_buffer mask) (B.loc_buffer pn_sm));
  assert (CTR.footprint m03 s == CTR.footprint m0 s);
  assert (B.loc_disjoint (B.loc_buffer mask `B.loc_union` B.loc_buffer pn_sm) (CTR.footprint m0 s `B.loc_union` B.loc_buffer k `B.loc_union` B.loc_buffer dst));
  let sample = B.sub dst (pn_offset `U32.add` 4ul) 16ul in
  let m1 = HST.get () in
  let gsample = Ghost.hide (Seq.slice (B.as_seq m0 dst) (U32.v pn_offset + 4) (U32.v pn_offset + 20)) in
  assert (B.as_seq m1 sample == Ghost.reveal gsample);
  block_of_sample (SAEAD.cipher_alg_of_supported_alg a) mask s k sample;
  let m2 = HST.get () in
  let gmask = Ghost.hide (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) (B.as_seq m0 k) gsample) in
  assert (B.as_seq m2 mask == Ghost.reveal gmask);
  pn_sizemask pn_sm pn_len;
  let m3 = HST.get () in
  assert (B.as_seq m3 mask == Ghost.reveal gmask);
  let gpn_sm = Ghost.hide (Seq.seq_hide #Secret.U8 (pn_sizemask_ct (Secret.v pn_len - 1))) in
  assert (B.as_seq m3 pn_sm == Ghost.reveal gpn_sm);
  let pnmask = B.sub mask 1ul 4ul in
  Lemmas.op_inplace pnmask pn_sm 4ul 0ul (Secret.logand #Secret.U8 #Secret.SEC);
  let m4 = HST.get () in
  let gpnmask = Ghost.hide (Lemmas.secret_and_inplace (Seq.slice gmask 1 5) gpn_sm 0) in
  assert (B.as_seq m4 pnmask == Ghost.reveal gpnmask);
  let protected_bits = if is_short then 5ul else 4ul in
  let mask_0 = B.index mask 0ul in
  assert (mask_0 == Seq.index (B.as_seq m4 (B.gsub mask 0ul 1ul)) 0);
  assert (mask_0 == Seq.index gmask 0);
  let f_ = B.index dst 0ul in
  assert (f_ == Seq.index (B.as_seq m0 dst) 0);
  let f_logxor = f_ `Secret.logxor` mask_0 in
  let f_get_bf = Secret.get_bitfield f_logxor 0ul protected_bits in
  let f' = Secret.set_bitfield f_ 0ul protected_bits f_get_bf in
  Lemmas.op_inplace dst pnmask 4ul pn_offset (Secret.logxor #Secret.U8 #Secret.SEC);
  let m5 = HST.get () in
  let gr1 = Ghost.hide (Lemmas.secret_xor_inplace (B.as_seq m0 dst) gpnmask (U32.v pn_offset)) in
  assert (B.as_seq m5 dst == Ghost.reveal gr1);
  B.upd dst 0ul f' ;
  HST.pop_frame ();
  let m6 = HST.get () in
  assert (B.as_seq m6 dst `Seq.equal` (f' `Seq.cons` Seq.slice (Ghost.reveal gr1) 1 (B.length dst)))

#restart-solver

let header_encrypt
  a s k dst h is_short is_retry public_len pn_len
= if is_retry
  then ()
  else begin
    let m = HST.get () in
    let hpk = Ghost.hide (B.as_seq m k) in
    let fmt = Ghost.hide (Parse.format_header (G.reveal h)) in
    let cipher = Ghost.hide (Seq.slice (B.as_seq m dst) (Seq.length fmt)  (B.length dst)) in
    assert (B.as_seq m dst `Seq.equal` (fmt `Seq.append` cipher));
    header_encrypt_ct_secret_preserving_not_retry_spec_correct a hpk h cipher;
    assert (U32.v public_len + 20 <= B.length dst);
    let post (cont: Seq.lseq Secret.uint8 (B.length dst)) (m1: HS.mem) : GTot Type0 =
      header_encrypt_ct_secret_preserving_not_retry_spec a hpk h (Seq.seq_hide (B.as_seq m dst)) == cont /\
      CTR.invariant m1 s /\
      CTR.footprint m1 s == CTR.footprint m s
    in
    SecretBuffer.with_whole_buffer_hide_weak_modifies'
      #unit
      dst
      m
      (CTR.footprint m s `B.loc_union` B.loc_buffer k)
      (CTR.footprint m s)
      true
      (fun _ cont m1 ->
        post cont m1
      )
      (fun _ bs ->
        header_encrypt_ct_secret_preserving_not_retry a s k h is_short public_len pn_len bs
      )
    ;
    let m' = HST.get () in
    assert (B.as_seq m' dst == Seq.seq_reveal (header_encrypt_ct_secret_preserving_not_retry_spec a hpk h (Seq.seq_hide (B.as_seq m dst))));
    assert (B.as_seq m' dst == Spec.header_encrypt a (B.as_seq m k) h cipher)
  end

#pop-options


(* A constant-time specification of header_decrypt_aux which does not test or truncate on pn_len *)

let header_decrypt_aux_ct
  (a:ea)
  (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
  (cid_len: nat { cid_len <= 20 })
  (packet: packet)
: GTot (option Spec.header_decrypt_aux_t)
= let open FStar.Math.Lemmas in
  if Seq.length packet = 0
  then None
  else
    let f = Seq.index packet 0 in
    let is_short = (BF.get_bitfield (U8.v f) 7 8 = 0) in
    let is_retry = not is_short && BF.get_bitfield (U8.v f) 4 6 = 3 in
    if is_retry
    then
      Some ({
        Spec.is_short = is_short;
        Spec.is_retry = is_retry;
        Spec.packet = packet;
        Spec.pn_offset = ();
        Spec.pn_len = ();
      })
    else
      match Parse.putative_pn_offset cid_len packet with
      | None -> None
      | Some pn_offset ->
        let sample_offset = pn_offset + 4 in
        if sample_offset + 16 > Seq.length packet
        then None
        else begin
          let sample = Seq.slice packet sample_offset (sample_offset+16) in
          let mask = Seq.seq_reveal (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a) hpk (Seq.seq_hide sample)) in
          (* mask the least significant bits of the first byte *)
          let protected_bits = if is_short 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 packet' = Seq.cons (U8.uint_to_t f') (Seq.slice packet 1 (Seq.length packet)) in
          (* now the packet number length is available, so mask the packet number *)
          let pn_len = BF.get_bitfield f' 0 2 in
          let pnmask = Lemmas.and_inplace (Seq.slice mask 1 5) (pn_sizemask_ct pn_len) 0 in
          let packet'' = Lemmas.xor_inplace packet' pnmask pn_offset in
          Some ({
            Spec.is_short = is_short;
            Spec.is_retry = is_retry;
            Spec.packet = packet'';
            Spec.pn_offset = pn_offset;
            Spec.pn_len = pn_len;
          })
        end

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

#restart-solver
/
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) ->
    cid_len: Prims.nat{cid_len <= 20} ->
    packet: QUIC.Spec.Crypto.packet
  -> FStar.Pervasives.Lemma
    (ensures
      QUIC.Impl.Header.header_decrypt_aux_ct a hpk cid_len packet ==
      QUIC.Spec.Header.header_decrypt_aux a hpk cid_len packet)
QUIC.Spec.Crypto.ea Spec.Agile.Cipher.key Spec.Agile.AEAD.cipher_alg_of_supported_alg Prims.nat Prims.b2t Prims.op_LessThanOrEqual QUIC.Spec.Crypto.packet Prims.op_Equality Prims.int FStar.Seq.Base.length QUIC.Spec.Base.byte Prims.bool QUIC.Spec.Header.Parse.putative_pn_offset Prims.op_GreaterThan Prims.op_Addition QUIC.Spec.Lemmas.xor_inplace_zero FStar.Seq.Base.slice 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 FStar.Seq.Base.seq Prims._assert FStar.Seq.Base.equal FStar.UInt8.logand QUIC.Spec.Base.bytes QUIC.Spec.Lemmas.and_inplace QUIC.Spec.Header.pn_sizemask LowParse.BitFields.ubitfield Prims.op_Subtraction LowParse.BitFields.get_bitfield FStar.UInt8.n FStar.Seq.Base.cons FStar.UInt8.uint_to_t FStar.UInt.uint_t LowParse.BitFields.set_bitfield FStar.UInt8.v FStar.UInt.logxor FStar.Seq.Base.index Prims.l_and 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_AmpAmp Prims.op_Negation Prims.l_True Prims.squash Prims.eq2 FStar.Pervasives.Native.option QUIC.Spec.Header.header_decrypt_aux_t QUIC.Impl.Header.header_decrypt_aux_ct QUIC.Spec.Header.header_decrypt_aux Prims.Nil FStar.Pervasives.pattern
let header_decrypt_aux_ct_correct
      (a: ea)
      (hpk: SCipher.key (SAEAD.cipher_alg_of_supported_alg a))
      (cid_len: nat{cid_len <= 20})
      (packet: packet)
    : Lemma
    (header_decrypt_aux_ct a hpk cid_len packet == Spec.header_decrypt_aux a hpk cid_len packet) =
  
let open FStar.Math.Lemmas in
if Seq.length packet = 0
then ()
else
  let f = Seq.index packet 0 in
  let is_short = (BF.get_bitfield (U8.v f) 7 8 = 0) in
  let is_retry = not is_short && BF.get_bitfield (U8.v f) 4 6 = 3 in
  if is_retry
  then ()
  else
    match Parse.putative_pn_offset cid_len packet with
    | None -> ()
    | Some pn_offset ->
      let sample_offset = pn_offset + 4 in
      if sample_offset + 16 > Seq.length packet
      then ()
      else
        let sample = Seq.slice packet sample_offset (sample_offset + 16) in
        let mask =
          Seq.seq_reveal #Secret.U8
            (Spec.block_of_sample (SAEAD.cipher_alg_of_supported_alg a)
                hpk
                (Seq.seq_hide #Secret.U8 sample))
        in
        let protected_bits = if is_short 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 packet' = Seq.cons (U8.uint_to_t f') (Seq.slice packet 1 (Seq.length packet)) in
        let pn_len = BF.get_bitfield f' 0 2 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)));
        let r = packet' in
        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