val size_label_eae_prk:size_nat
let size_label_eae_prk: size_nat = 7
val size_label_eae_prk:size_nat
let size_label_eae_prk:size_nat =
7
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
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

let is_valid_not_export_only_ciphersuite (cs:ciphersuite) : bool =
  match aead_of_cs cs with
  | ExportOnly -> false
  | Seal _ -> true

let ciphersuite_not_export_only = cs:ciphersuite{is_valid_not_export_only_ciphersuite cs}

inline_for_extraction
let aead_alg_of (cs:ciphersuite_not_export_only) = match aead_of_cs cs with
  | Seal alg -> alg


/// Constants for HPKE labels
///
/// The code for the following constants was generated
/// with the script make_hpke_constants.py. Ultimately,
/// this should be rewritten in Meta-F*. The idea is to
/// write a tactic `mk_label` that inspects a string
/// character by character, and generates the proper
/// definition. It could be used as follows:
/// %splice [label_version] (mk_label "HPKE-v1")
/// Inspiration can be taken from Test.Lowstarize.fst.

// generated: "HPKE-v1"
inline_for_extraction
let size_label_version: size_nat = 7
let label_version_list : l:list uint8{List.Tot.length l == size_label_version} =
  [@inline_let]
  let l = [u8 0x48; u8 0x50; u8 0x4b; u8 0x45; u8 0x2d; u8 0x76; u8 0x31] in
  assert_norm(List.Tot.length l == size_label_version);
  l
let label_version : lbytes size_label_version = createL label_version_list


// generated: "eae_prk"
val size_label_eae_prk:size_nat
n: Prims.nat{n <= Prims.pow2 32 - 1}