val block_of_sample
      (a: SCipher.cipher_alg)
      (dst: B.buffer Secret.uint8)
      (s: CTR.state a)
      (k 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)
val block_of_sample
      (a: SCipher.cipher_alg)
      (dst: B.buffer Secret.uint8)
      (s: CTR.state a)
      (k 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)
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 ()
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"
/
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: Spec.Agile.Cipher.cipher_alg ->
    dst: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    s: NotEverCrypt.CTR.state a ->
    k: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    sample: LowStar.Buffer.buffer Lib.IntTypes.uint8
  -> FStar.HyperStack.ST.Stack Prims.unit
Spec.Agile.Cipher.cipher_alg LowStar.Buffer.buffer Lib.IntTypes.uint8 NotEverCrypt.CTR.state FStar.HyperStack.ST.pop_frame Prims.unit LowStar.Monotonic.Buffer.blit NotEverCrypt.CTR.uint8 LowStar.Buffer.trivial_preorder FStar.UInt32.__uint_to_t Prims._assert FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Agile.Cipher.ctr_block QUIC.Secret.Int.Base.v Lib.IntTypes.U32 LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.sub FStar.Ghost.hide FStar.UInt32.t QUIC.Impl.Lemmas.seq_map2_xor0 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get NotEverCrypt.CTR.update_block NotEverCrypt.CTR.alg NotEverCrypt.CTR.init Lib.RawIntTypes.u32_to_UInt32 Lib.IntTypes.int_t QUIC.Secret.Buffer.load32_le Lib.IntTypes.uint32 Prims.eq2 Prims.int LowStar.Monotonic.Buffer.length QUIC.Secret.Buffer.load32_be QUIC.Impl.Header.block_len Prims.l_and Prims.nat FStar.UInt32.v FStar.UInt32.uint_to_t Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.alloca Lib.IntTypes.to_u8 Lib.IntTypes.U1 Lib.IntTypes.PUB FStar.UInt8.__uint_to_t FStar.HyperStack.ST.push_frame LowStar.Monotonic.Buffer.all_live Prims.Cons LowStar.Monotonic.Buffer.buf_t LowStar.Monotonic.Buffer.buf Prims.Nil NotEverCrypt.CTR.invariant LowStar.Monotonic.Buffer.all_disjoint LowStar.Monotonic.Buffer.loc NotEverCrypt.CTR.footprint LowStar.Monotonic.Buffer.loc_buffer Prims.l_or Spec.Agile.Cipher.AES128 Spec.Agile.Cipher.AES256 Spec.Agile.Cipher.CHACHA20 Prims.op_Equality Spec.Agile.Cipher.key_length LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union QUIC.Spec.Header.block_of_sample
let block_of_sample
      (a: SCipher.cipher_alg)
      (dst: B.buffer Secret.uint8)
      (s: CTR.state a)
      (k 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
(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
    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
    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);
HST.pop_frame ()