val is_valid_not_export_only_ciphersuite (cs: ciphersuite) : bool
let is_valid_not_export_only_ciphersuite (cs:ciphersuite) : bool =
  match aead_of_cs cs with
  | ExportOnly -> false
  | Seal _ -> true
val is_valid_not_export_only_ciphersuite (cs: ciphersuite) : bool
let is_valid_not_export_only_ciphersuite (cs: ciphersuite) : bool =
match aead_of_cs cs with
| ExportOnly -> false
| Seal _ -> true
Spec.Agile.HPKE.fsti.checked
Spec.Hash.Definitions.fst.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 FStar.List.Tot.fst.checked
Spec.Agile.HPKE.fsti
Spec.Agile.HPKE.ciphersuite Spec.Agile.HPKE.aead_of_cs Spec.Agile.AEAD.alg Prims.bool
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

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

type mode =
  | Base
  | PSK
  | Auth
  | AuthPSK

let is_valid_kem = function
  | DH.DH_Curve25519, Hash.SHA2_256
  | DH.DH_P256,       Hash.SHA2_256 -> true
  | _,_ -> false

noeq type aead =
  | Seal: alg:AEAD.alg -> aead
  | ExportOnly

let is_valid_aead = function
  | Seal AEAD.AES128_GCM
  | Seal AEAD.AES256_GCM
  | Seal AEAD.CHACHA20_POLY1305
  | ExportOnly -> true
  | _ -> false

let is_valid_hash = function
  | Hash.SHA2_256
  | Hash.SHA2_384
  | Hash.SHA2_512 -> true
  | _ -> false

let hash_algorithm = a:Hash.hash_alg{is_valid_hash a}

let is_valid_ciphersuite (cs:DH.algorithm & hash_algorithm & aead & Hash.hash_alg) : bool =
  let kem_dh, kem_hash, aead, hash = cs in
  (is_valid_kem (kem_dh, kem_hash)) && (is_valid_aead aead) && (is_valid_hash hash)

let ciphersuite = cs:(DH.algorithm & hash_algorithm & aead & Hash.hash_alg){is_valid_ciphersuite cs}

inline_for_extraction
let kem_dh_of_cs (cs:ciphersuite) : DH.algorithm =
  let (c,_,_,_) = cs in c

inline_for_extraction
let kem_hash_of_cs (cs:ciphersuite) : hash_algorithm =
  let (_,h,_,_) = cs in h

inline_for_extraction
let aead_of_cs (cs:ciphersuite) : aead =
  let (_,_,a,_) = cs in a

inline_for_extraction
let hash_of_cs (cs:ciphersuite) : hash_algorithm =
  let (_,_,_,h) = cs in h
val is_valid_not_export_only_ciphersuite (cs: ciphersuite) : bool
cs: Spec.Agile.HPKE.ciphersuite -> Prims.bool