val iv_for_encrypt_decrypt (a: ea) (siv: iv_t a) (h: header{~(is_retry h)}) : GTot (iv_t a)
val iv_for_encrypt_decrypt (a: ea) (siv: iv_t a) (h: header{~(is_retry h)}) : GTot (iv_t a)
let iv_for_encrypt_decrypt
  (a: ea)
  (siv: iv_t a)
  (h: header { ~ (is_retry h) })
: GTot (iv_t a)
=
  let pn_len = Secret.v (pn_length h) - 1 in
  let seqn = packet_number h in
  let _ = assert_norm(pow2 62 < pow2 (8 `op_Multiply` 12)) in
  let pnb = FStar.Endianness.n_to_be 12 (Secret.v seqn) in
  Seq.seq_hide #Secret.U8 (xor_inplace pnb (Seq.seq_reveal siv) 0)
module QUIC.Spec

open QUIC.Spec.Lemmas
open QUIC.Spec.Header.Base

module Seq = QUIC.Secret.Seq
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module H = Spec.Agile.Hash
module HD = Spec.Hash.Definitions
module Cipher = Spec.Agile.Cipher
module AEAD = Spec.Agile.AEAD
module HKDF = Spec.Agile.HKDF
module Parse = QUIC.Spec.Header.Parse
module H = QUIC.Spec.Header
module Secret = QUIC.Secret.Int

/// encryption of a packet
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.Header.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fsti.checked
QUIC.Spec.fst

    a: QUIC.Spec.Crypto.ea ->
    siv: QUIC.Spec.iv_t a ->
    h: QUIC.Spec.Header.Base.header{~(QUIC.Spec.Header.Base.is_retry h)}
  -> Prims.GTot (QUIC.Spec.iv_t a)
QUIC.Spec.Crypto.ea QUIC.Spec.iv_t QUIC.Spec.Header.Base.header Prims.l_not Prims.b2t QUIC.Spec.Header.Base.is_retry QUIC.Secret.Seq.seq_hide Lib.IntTypes.U8 QUIC.Spec.Lemmas.xor_inplace QUIC.Secret.Seq.seq_reveal Lib.IntTypes.SEC FStar.Endianness.bytes Prims.l_and Prims.eq2 Prims.nat FStar.Seq.Base.length FStar.UInt8.t Lib.IntTypes.v Lib.IntTypes.U64 FStar.Endianness.be_to_n FStar.Endianness.n_to_be QUIC.Secret.Int.Base.v Prims.unit FStar.Pervasives.assert_norm Prims.op_LessThan Prims.pow2 Prims.op_Multiply QUIC.Spec.PacketNumber.Base.packet_number_t QUIC.Spec.Header.Base.packet_number Prims.int Prims.op_Subtraction Lib.IntTypes.U32 QUIC.Spec.Header.Base.pn_length
let iv_for_encrypt_decrypt (a: ea) (siv: iv_t a) (h: header{~(is_retry h)}) : GTot (iv_t a) =
  
let pn_len = Secret.v (pn_length h) - 1 in
let seqn = packet_number h in
let _ = assert_norm (pow2 62 < pow2 (8 `op_Multiply` 12)) in
let pnb = FStar.Endianness.n_to_be 12 (Secret.v seqn) in
Seq.seq_hide #Secret.U8 (xor_inplace pnb (Seq.seq_reveal siv) 0)