val bytes_sec : Type0
let bytes_sec = Seq.seq I.uint8
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
/
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
Type0
FStar.Seq.Base.seq Lib.IntTypes.uint8
let bytes_sec =
  
Seq.seq I.uint8