val create_nonce (#i:id) (#rw:rw) (st:state i rw) (n:nonce i): Tot (i:iv i)
val create_nonce (#i:id) (#rw:rw) (st:state i rw) (n:nonce i): Tot (i:iv i)
let create_nonce (#i:id) (#rw:rw) (st:state i rw) (n:nonce i): Tot (i:iv i) =
  let salt = salt_of_state st in
  match (TLSInfo.pv_of_id i, alg i) with
  | (TLS_1p3, _) | (_, EverCrypt.CHACHA20_POLY1305) ->
    xor_ #(iv_length i) n salt
  | _ ->
    assert(Bytes.length salt + Bytes.length n = iv_length i);
    salt @| n
module MiTLS.AEADProvider
open MiTLS

open FStar.Heap
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Seq
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
open FStar.UInt32

module HS = FStar.HyperStack
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module E = MiTLS.EverCrypt
module LB = LowStar.Buffer
module CI = MiTLS.Crypto.Indexing
module Plain = MiTLS.Crypto.Plain
module CB = MiTLS.Crypto.Symmetric.Bytes

let iv (i:id) = lbytes (iv_length i)

let coerce_iv (i:id) (b:lbytes (iv_length i)) : Tot (iv i) = b


#reset-options "--using_facts_from '* -LowParse.Spec.Base'"
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.Crypto.Symmetric.Bytes.fst.checked MiTLS.Crypto.Plain.fsti.checked MiTLS.Crypto.Indexing.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Bytes.fsti.checked
MiTLS.AEADProvider.fst
st: MiTLS.AEADProvider.state i rw -> n: MiTLS.AEADProvider.nonce i -> MiTLS.AEADProvider.iv i
MiTLS.AEADProvider.id MiTLS.TLSConstants.rw MiTLS.AEADProvider.state MiTLS.AEADProvider.nonce FStar.Pervasives.Native.Mktuple2 MiTLS.Parsers.ProtocolVersion.protocolVersion MiTLS.EverCrypt.aead_alg MiTLS.TLSInfo.pv_of_id MiTLS.AEADProvider.alg FStar.Bytes.xor_ MiTLS.AEADProvider.iv_length FStar.Pervasives.Native.tuple2 FStar.Bytes.op_At_Bar Prims.unit Prims._assert Prims.b2t Prims.op_Equality Prims.int Prims.op_Addition FStar.Bytes.length MiTLS.AEADProvider.iv MiTLS.AEADProvider.salt MiTLS.AEADProvider.salt_of_state
let create_nonce (#i: id) (#rw: rw) (st: state i rw) (n: nonce i) : Tot (i : iv i) =
  
let salt = salt_of_state st in
match (TLSInfo.pv_of_id i, alg i) with
| TLS_1p3, _ | _, EverCrypt.CHACHA20_POLY1305 -> xor_ #(iv_length i) n salt
| _ ->
  assert (Bytes.length salt + Bytes.length n = iv_length i);
  salt @| n