val block_of_sample
  (a: Cipher.cipher_alg)
  (k: Cipher.key a)
  (sample: Seq.lseq Secret.uint8 16)
: GTot (Seq.lseq Secret.uint8 16)
val block_of_sample
  (a: Cipher.cipher_alg)
  (k: Cipher.key a)
  (sample: Seq.lseq Secret.uint8 16)
: GTot (Seq.lseq Secret.uint8 16)
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)
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
/
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: Spec.Agile.Cipher.cipher_alg ->
    k: Spec.Agile.Cipher.key a ->
    sample: FStar.Seq.Properties.lseq Lib.IntTypes.uint8 16
  -> Prims.GTot (FStar.Seq.Properties.lseq Lib.IntTypes.uint8 16)
Spec.Agile.Cipher.cipher_alg Spec.Agile.Cipher.key FStar.Seq.Properties.lseq Lib.IntTypes.uint8 Spec.Agile.Cipher.ctr Spec.Agile.Cipher.nonce FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Agile.Cipher.ctr_block FStar.Pervasives.Native.tuple2 FStar.Seq.Base.seq FStar.Pervasives.Native.Mktuple2 FStar.Endianness.le_to_n QUIC.Secret.Seq.seq_reveal Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.pos Prims.pow2 FStar.Mul.op_Star FStar.Endianness.lemma_le_to_n_is_bounded Lib.IntTypes.int_t FStar.Seq.Properties.split FStar.Endianness.be_to_n FStar.Endianness.lemma_be_to_n_is_bounded
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)