val alg:dice_hash_alg
val alg:dice_hash_alg
let alg : dice_hash_alg = S.SHA2_256
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)
}
/
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
DICE.Engine.Definitions.dice_hash_alg
Spec.Hash.Definitions.SHA2_256
let alg:dice_hash_alg =
  
S.SHA2_256