val id_aead: cs:ciphersuite -> Tot (lbytes 2)
let id_aead cs = let _, _, a, _ = cs in
  match a with
  | Seal AEAD.AES128_GCM -> create 1 (u8 0) @| create 1 (u8 1)
  | Seal AEAD.AES256_GCM -> create 1 (u8 0) @| create 1 (u8 2)
  | Seal AEAD.CHACHA20_POLY1305 -> create 1 (u8 0) @| create 1 (u8 3)
  | ExportOnly -> create 1 (u8 255) @| create 1 (u8 255)
val id_aead: cs:ciphersuite -> Tot (lbytes 2)
let id_aead cs =
let _, _, a, _ = cs in
match a with
| Seal AEAD.AES128_GCM -> create 1 (u8 0) @| create 1 (u8 1)
| Seal AEAD.AES256_GCM -> create 1 (u8 0) @| create 1 (u8 2)
| Seal AEAD.CHACHA20_POLY1305 -> create 1 (u8 0) @| create 1 (u8 3)
| ExportOnly -> create 1 (u8 255) @| create 1 (u8 255)
Spec.Agile.HPKE.fst.checked
Spec.P256.fst.checked Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.DH.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Agile.HPKE.fst
Spec.Agile.HPKE.ciphersuite Spec.Agile.DH.algorithm Spec.Agile.HPKE.hash_algorithm Spec.Agile.HPKE.aead Spec.Hash.Definitions.hash_alg Lib.Sequence.op_At_Bar Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Sequence.create Lib.IntTypes.u8 Lib.ByteSequence.lbytes
module Spec.Agile.HPKE

open FStar.Mul
open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence

module DH = Spec.Agile.DH
module AEAD = Spec.Agile.AEAD
module Hash = Spec.Agile.Hash
module HKDF = Spec.Agile.HKDF


let pow2_61 : _:unit{pow2 61 == 2305843009213693952} = assert_norm(pow2 61 == 2305843009213693952)
let pow2_35_less_than_pow2_61 : _:unit{pow2 32 * pow2 3 <= pow2 61 - 1} = assert_norm(pow2 32 * pow2 3 <= pow2 61 - 1)
let pow2_35_less_than_pow2_125 : _:unit{pow2 32 * pow2 3 <= pow2 125 - 1} = assert_norm(pow2 32 * pow2 3 <= pow2 125 - 1)

#set-options "--z3rlimit 20 --fuel 0 --ifuel 1"




/// Types

val id_kem: cs:ciphersuite -> Tot (lbytes 2)
let id_kem cs = let kem_dh, kem_hash, _, _ = cs in
  match kem_dh, kem_hash with
  | DH.DH_P256, Hash.SHA2_256 -> create 1 (u8 0) @| create 1 (u8 16)
  | DH.DH_Curve25519, Hash.SHA2_256 -> create 1 (u8 0) @| create 1 (u8 32)

val id_kdf: cs:ciphersuite -> Tot (lbytes 2)
let id_kdf cs = let _, _, _, h = cs in
  match h with
  | Hash.SHA2_256 -> create 1 (u8 0) @| create 1 (u8 1)
  | Hash.SHA2_384 -> create 1 (u8 0) @| create 1 (u8 2)
  | Hash.SHA2_512 -> create 1 (u8 0) @| create 1 (u8 3)
val id_aead: cs:ciphersuite -> Tot (lbytes 2)
cs: Spec.Agile.HPKE.ciphersuite -> Lib.ByteSequence.lbytes 2