val l0_image_is_valid : img: HWState.l0_image_t -> h: FStar.Monotonic.HyperStack.mem -> Prims.logical
let l0_image_is_valid (img:l0_image_t) (h:HS.mem) =
  Spec.Ed25519.verify
    (B.as_seq h img.l0_image_auth_pubkey)
    (B.as_seq h img.l0_image_header)
    (B.as_seq h img.l0_image_header_sig) /\

  Spec.Agile.Hash.hash alg (B.as_seq h img.l0_binary) ==
  B.as_seq h img.l0_binary_hash
module DICE.Engine.Core

open LowStar.Comment

module Fail = LowStar.Failure
module B = LowStar.Buffer
module HS  = FStar.HyperStack
module HST = FStar.HyperStack.ST

open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.ByteBuffer

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

module HW = HWAbstraction

open DICE.Engine.Definitions

module HSeq = Lib.Sequence

module G = FStar.Ghost

open HWAbstraction

open HWState
/
Spec.Hash.Definitions.fst.checked Spec.Ed25519.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked LowStar.Failure.fsti.checked LowStar.Comment.fsti.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked HWState.fsti.checked HWAbstraction.fsti.checked Hacl.Ed25519.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked DICE.Engine.Definitions.fst.checked
DICE.Engine.Core.fst
img: HWState.l0_image_t -> h: FStar.Monotonic.HyperStack.mem -> Prims.logical
HWState.l0_image_t FStar.Monotonic.HyperStack.mem Prims.l_and Prims.b2t Spec.Ed25519.verify LowStar.Monotonic.Buffer.as_seq DICE.Engine.Definitions.byte_sec LowStar.Buffer.trivial_preorder HWState.__proj__Mkl0_image_t__item__l0_image_auth_pubkey HWState.__proj__Mkl0_image_t__item__l0_image_header HWState.__proj__Mkl0_image_t__item__l0_image_header_sig Prims.eq2 FStar.Seq.Base.seq Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Agile.Hash.hash DICE.Engine.Definitions.alg HWState.__proj__Mkl0_image_t__item__l0_binary HWState.__proj__Mkl0_image_t__item__l0_binary_hash Prims.logical
let l0_image_is_valid (img: l0_image_t) (h: HS.mem) =
  
Spec.Ed25519.verify (B.as_seq h img.l0_image_auth_pubkey)
  (B.as_seq h img.l0_image_header)
  (B.as_seq h img.l0_image_header_sig) /\
Spec.Agile.Hash.hash alg (B.as_seq h img.l0_binary) == B.as_seq h img.l0_binary_hash