val label_shared_secret:lbytes size_label_shared_secret
let label_shared_secret : lbytes size_label_shared_secret = createL label_shared_secret_list
val label_shared_secret:lbytes size_label_shared_secret
let label_shared_secret:lbytes size_label_shared_secret =
createL label_shared_secret_list
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
Lib.Sequence.createL Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Agile.HPKE.label_shared_secret_list
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"
inline_for_extraction
let size_label_eae_prk: size_nat = 7
let label_eae_prk_list : l:list uint8{List.Tot.length l == size_label_eae_prk} =
  [@inline_let]
  let l = [u8 0x65; u8 0x61; u8 0x65; u8 0x5f; u8 0x70; u8 0x72; u8 0x6b] in
  assert_norm(List.Tot.length l == size_label_eae_prk);
  l
let label_eae_prk : lbytes size_label_eae_prk = createL label_eae_prk_list


// generated: "KEM"
inline_for_extraction
let size_label_KEM: size_nat = 3
let label_KEM_list : l:list uint8{List.Tot.length l == size_label_KEM} =
  [@inline_let]
  let l = [u8 0x4b; u8 0x45; u8 0x4d] in
  assert_norm(List.Tot.length l == size_label_KEM);
  l
let label_KEM : lbytes size_label_KEM = createL label_KEM_list


// generated: "HPKE"
inline_for_extraction
let size_label_HPKE: size_nat = 4
let label_HPKE_list : l:list uint8{List.Tot.length l == size_label_HPKE} =
  [@inline_let]
  let l = [u8 0x48; u8 0x50; u8 0x4b; u8 0x45] in
  assert_norm(List.Tot.length l == size_label_HPKE);
  l
let label_HPKE : lbytes size_label_HPKE = createL label_HPKE_list


// generated: "shared_secret"
inline_for_extraction
let size_label_shared_secret: size_nat = 13
let label_shared_secret_list : l:list uint8{List.Tot.length l == size_label_shared_secret} =
  [@inline_let]
  let l = [u8 0x73; u8 0x68; u8 0x61; u8 0x72; u8 0x65; u8 0x64; u8 0x5f; u8 0x73; u8 0x65; u8 0x63; u8 0x72; u8 0x65; u8 0x74] in
  assert_norm(List.Tot.length l == size_label_shared_secret);
val label_shared_secret:lbytes size_label_shared_secret
Lib.Sequence.lseq (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC)
  Spec.Agile.HPKE.size_label_shared_secret