val cdi_len : n:
Lib.IntTypes.size_t
  {Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length DICE.Engine.Definitions.alg}
let cdi_len = digest_len
module DICE.Engine.Definitions

module HS = FStar.HyperStack

module I = Lib.IntTypes
module B = LowStar.Buffer

module S = Spec.Hash.Definitions
module H = Hacl.Hash.Definitions

open Lib.IntTypes

(*
 * Some common definitions used in the DICE code
 *)

let byte_sec = uint8
let byte_pub = pub_uint8

let bytes_sec = Seq.seq I.uint8
let bytes_pub = Seq.seq I.pub_uint8

let lbytes_sec = Seq.lseq I.uint8
let lbytes_pub = Seq.lseq I.pub_uint8

type dice_hash_alg = a:S.hash_alg {
  a =!= S.MD5 /\ a =!= S.SHA2_224 /\ a =!= S.Blake2S /\ a =!= S.Blake2B /\ a =!= S.SHA1 /\
  (not (S.is_shake a)) /\
  Some? (S.max_input_length a)
}

inline_for_extraction
let alg : dice_hash_alg = S.SHA2_256

inline_for_extraction noextract
let dice_hash (alg:dice_hash_alg) : H.hash_st alg =
  match alg with
  | S.SHA2_256 -> Hacl.Streaming.SHA2.hash_256
  | S.SHA2_384 -> Hacl.Streaming.SHA2.hash_384
  | S.SHA2_512 -> Hacl.Streaming.SHA2.hash_512

inline_for_extraction noextract
let dice_hmac (alg:dice_hash_alg) : Hacl.HMAC.compute_st alg =
  match alg with
  | S.SHA2_256 -> Hacl.HMAC.compute_sha2_256
  | S.SHA2_384 -> Hacl.HMAC.compute_sha2_384
  | S.SHA2_512 -> Hacl.HMAC.compute_sha2_512

unfold let digest_len = H.hash_len alg

unfold type digest_t = H.hash_t alg

unfold type hashable_len = i: size_t {0 < v i /\ v i <= (Some?.v (S.max_input_length alg))}
/
Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Hacl.Streaming.SHA2.fst.checked Hacl.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked
DICE.Engine.Definitions.fst
n:
Lib.IntTypes.size_t
  {Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length DICE.Engine.Definitions.alg}
DICE.Engine.Definitions.digest_len
let cdi_len =
  
digest_len